% Q:\D\ALL.POS       Revised 2000 August 19
% Conversion of all of the D theorems to clause form.
% Quaife, page 155.

clear(symbol_elim).
set(order_eq).
set(sort_literals).
set(unit_deletion).
set(factor).
set(dynamic_demod_all).
set(back_demod).
set(process_input).
clear(print_given).
set(print_lists_at_end).

set(lrpo).
set(lex_order_vars).
lex([0,V,union(x,x),intersection(x,x),complement(x),
     equal(x,x),subclass(x,x)]).

assign(max_mem,300).
assign(stats_level,1).
assign(max_seconds,10).

list(usable).
subclass(x,x).                                                   % PO-1
equal(x,x).                                                      % EQ-1
end_of_list.

formula_list(sos).
%  Theorem D-0 
(all x y z subclass(intersection(union(x,y),z),
                             union(x,intersection(y,z)))).
%  Theorem D-0A 
(all x y z subclass(intersection(x,union(y,z)),
                   union(intersection(x,y),z))). 
%  Theorem D-1A1       (subsumed by others)
(all x y z subclass(intersection(x,union(y,z)),
                    union(intersection(x,y),intersection(x,z)))).
%  Semi-Distributive Inequality D-1A2     (subsumed)
(all x y z subclass(union(intersection(x,y),intersection(x,z)),
                    intersection(x,union(y,z)))).
%  Theorem D-1A   (Distributive Law)
(all x y z equal(intersection(x,union(y,z)),
                 union(intersection(x,y),intersection(x,z)))).
%  Theorem D-1B1
(all x y z subclass(intersection(union(x,y),z),
                    union(intersection(x,z),intersection(y,z)))).
%  Semi-Distributive Inequality D-1B2
(all x y z subclass(union(intersection(x,z),intersection(y,z)),
                    intersection(union(x,y),z))).
%  Theorem D-1B     (flipped version of D-1A)
(all x y z equal(intersection(union(x,y),z),
                 union(intersection(x,z),intersection(y,z)))).
%  Theorem D-2A
(all x y z equal(union(x,intersection(y,z)),
                  intersection(union(x,y),union(x,z)))).
%  Theorem D-2A1
(all x y z subclass(intersection(union(x,y),union(x,z)),
                    union(x,intersection(y,z)))).
%  Semi-Distributive Inequality D-2A2
(all x y z subclass(union(x,intersection(y,z)),
                    intersection(union(x,y),union(x,z)))).
%  theorem D-2B
(all x y z equal(union(intersection(x,y),z),
                  intersection(union(x,z),union(y,z)))).
%  Theorem D-2B1
(all x y z subclass(intersection(union(x,z),union(y,z)),
                    union(intersection(x,y),z))).
%  Semi-Distributive Inequality D-2B2
(all x y z subclass(union(intersection(x,y),z),
                    intersection(union(x,z),union(y,z)))).

%  Theorem D-3      (subsumed by the other absorptive law D-4)
(all x y equal(intersection(x,union(x,y)),x)).
%  Corollary D-3COR1
(all x y z equal(intersection(x,intersection(y,union(x,z))),
                          intersection(x,y))).
%  Corollary D-3COR2
(all x y z equal(union(x,union(intersection(y,z),
      union(intersection(x,z),intersection(x,y)))),
      union(intersection(y,z),x))).
%  Theorem D-4      (Absorptive Law) 
(all x y equal(union(x,intersection(x,y)),x)).
%  Corollary D-4COR1
(all x y z equal(union(x,union(y,intersection(x,z))),union(x,y))).
%  Corollary D-4COR2
(all x y z equal(union(x,union(intersection(x,y),z)),union(x,z))).
%  Theorem D-4-EXT
(all x y (equal(union(intersection(x,complement(y)),
                      intersection(y,complement(x))),0)
          -> equal(x,y))).
%  Theorem D-5
(all x y equal(union(x,intersection(complement(x),y)),union(x,y))).
%  Theorem D-EQ-V
(all x y (equal(V,union(intersection(x,y),
          intersection(complement(x),complement(y)))) -> equal(x,y))).
%  Corollary D-5A
(all x y z equal(union(x,union(y,intersection(complement(x),z))),
                 union(x,union(y,z)))).
%  Corollary D-5B
(all x y z equal(union(intersection(x,z),
  intersection(complement(x),intersection(y,z))),
  union(intersection(x,z),intersection(y,z)))).
%  Theorem D-6
(all x y equal(union(complement(x),intersection(x,y)),
                    union(complement(x),y))).
%  Corollary D-6A
(all x y z equal(
  union(complement(x),union(y,intersection(x,z))),
  union(complement(x),union(y,z)))).
%  Theorem D-7
(all x y equal(union(intersection(complement(x),y),
                     intersection(x,y)),y)).
%  Theorem D-SU1
(all x y z subclass(union(x,intersection(y,z)),union(x,z))).
%  Theorem D-SU2
(all x y z subclass(union(intersection(x,y),z),union(x,z))).
%  Theorem D-DJ
(all x y (equal(intersection(x,y),0) ->  
          equal(intersection(union(x,y),complement(x)),y))).
%  Theorem SPECIAL
(all w x y ((subclass(w,union(x,y)) & equal(intersection(w,y),0)) 
                      -> subclass(w,x))).
end_of_list.
 
list(demodulators).
equal(intersection(intersection(x,y),z),
      intersection(x,intersection(y,z))).                        % I-1
equal(intersection(x,y),intersection(y,x)).                      % I-2
equal(intersection(y,intersection(x,z)),
      intersection(x,intersection(y,z))).                        % I-3
equal(intersection(x,x),x).                                      % I-6
equal(intersection(x,intersection(y,x)),intersection(x,y)).      % I-6A
equal(intersection(x,intersection(x,y)),intersection(x,y)).      % I-6B
equal(intersection(x,complement(x)),0).                          % C-3A
equal(union(union(x,y),z),union(x,union(y,z))).                  % U-1
equal(union(x,y),union(y,x)).                                    % U-2
equal(union(0,x),x).                                             % U-4
equal(union(x,0),x).                                             % U-4'
equal(union(x,x),x).                                             % U-6
equal(union(x,union(y,x)),union(x,y)).                           % U-6A
equal(union(x,union(x,y)),union(x,y)).                           % U-6B
end_of_list.