%querytabled * * D : {A:p}{B:p}search (((atom A) and (atom B)) imp ((atom B) and (atom A))).


%querytabled * * D : {A:p}{B:p}(search ((atom A) imp (atom B) imp (atom A))).



%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) imp (atom B) imp (atom C)) imp (((atom A) and (atom B)) imp (atom C))).


%querytabled * * D :  {A:p}{B:p}{C:p} search ((((atom A) and (atom B)) imp (atom C)) imp ((atom A) imp (atom B) imp (atom C))).

% %querytabled * * D :  {A:p}{B:p}{C:p}search (((atom A) imp (atom B) imp (atom C)) imp (((atom A) imp (atom B)) imp (atom A) imp (atom C))).


% proof of S
%querytabled * * D :  {A:p}{B:p}{C:p}(search (((atom A) imp (atom B) imp (atom C)) imp ((atom A) imp (atom B)) imp (atom A) imp (atom C))).
%querytabled * * D :  {A:p}{B:p}{C:p}search ((((atom A) and (atom B)) and (atom C)) imp ((atom A) and ((atom B) and (atom C)))).
%querytabled * * D :  {A:p}{B:p}{C:p}search (((atom A) and ((atom B) and (atom C))) imp (((atom A) and (atom B)) and (atom C))).



% impDef
% 
%querytabled * * D :  {A:p}{B:p}{C:p}search ((((atom A) and (atom B)) or (atom C)) imp (((atom A) or (atom C)) and ((atom B) or (atom C)))).
%querytabled * * D :  {A:p}{B:p}{C:p}search (((atom A) and ((atom B) or (atom C))) imp (((atom A) and (atom B)) or ((atom A) and (atom C)))).

% new from (atom A)TP notes
% 2
%querytabled * * D : {A:p}{B:p}{C:p}search (((atom A) imp ((atom B) and (atom C))) imp (((atom A) imp (atom B)) and ((atom A) imp (atom C)))).
%querytabled * * D : {A:p}{B:p}{C:p}search ((((atom A) imp (atom B)) and ((atom A) imp (atom C))) imp ((atom A) imp ((atom B) and (atom C)))).

% 3
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) imp ((atom B) or (atom C)))imp (((atom A) imp (atom B)) or ((atom A) imp (atom C)))).
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) imp (atom B)) or ((atom A) imp (atom C))) imp ((atom A) imp ((atom B) or (atom C)))).

% 4
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) imp (atom B)) imp (atom C)) imp (((atom A) or (atom C)) and ((atom B) imp (atom C)))).
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) or (atom C)) and ((atom B) imp (atom C))) imp (((atom A) imp (atom B)) imp (atom C))).

% 5
%querytabled * * D : {A:p}{B:p}{C:p}search ((((atom A) or (atom B)) imp (atom C)) imp (((atom A) imp (atom C)) and ((atom B) imp (atom C)))). 
%querytabled * * D : {A:p}{B:p}{C:p}search ((((atom A) imp (atom C)) and ((atom B) imp (atom C))) imp (((atom A) or (atom B)) imp (atom C))). 

% 6 
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) and ((atom B) or (atom C))) imp (((atom A) and (atom B)) or ((atom A) and (atom C)))).
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) and (atom B)) or ((atom A) and (atom C))) imp ((atom A) and ((atom B) or (atom C)))).

% 7
%querytabled * * D : {A:p}{B:p}{C:p}search (((atom A) or ((atom B) and (atom C))) imp (((atom A) or (atom B)) and ((atom A) or (atom C)))).
%querytabled * * D : {A:p}{B:p}{C:p}search ((((atom A) or (atom B)) and ((atom A) or (atom C))) imp ((atom A) or ((atom B) and (atom C)))).


% Id : (atom A) => (atom A) 
%querytabled * * D : {A:p} search ((atom A) imp (atom A)).

% K : (atom A) => (atom B) => (atom A) 
%querytabled * * D : {A:p}{B:p} search ((atom A) imp (atom B) imp (atom A)).

% S : ((atom A) => (atom B) => (atom C)) => ((atom A) => (atom B)) => ((atom A) => (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) imp ((atom B) imp (atom C))) imp 
			     (((atom A) imp (atom B)) imp ((atom A) imp (atom C)))).

% ((atom A) & (atom B) => (atom C)) <=> ((atom A) => (atom B) => (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) and (atom B)) imp (atom C)) imp
			     ((atom A) imp ((atom B) imp (atom C)))).
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) imp ((atom B) imp (atom C))) imp
			     (((atom A) and (atom B)) imp (atom C))).

% ((atom A) => (atom B) & (atom C)) <=> ((atom A) => (atom B)) & ((atom A) => (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) imp ((atom B) and (atom C))) imp ((atom A) imp (atom B)) and ((atom A) imp (atom C))).
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) imp (atom B)) and ((atom A) imp (atom C))) imp ((atom A) imp ((atom B) and (atom C)))).

% ((atom A) => T) <=> T 
%querytabled * * D : {A:p} search (((atom A) imp true) imp true).
%querytabled * * D : {A:p} search (true imp ((atom A) imp true)).

% ((atom A) v (atom B) => (atom C)) <=> ((atom A) => (atom C)) & ((atom B) => (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) or (atom B)) imp (atom C)) imp
					     (((atom A) imp (atom C)) and ((atom B) imp (atom C)))).


%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) imp (atom C)) and ((atom B) imp (atom C))) imp
					     (((atom A) or (atom B)) imp (atom C))).

% (F => (atom C)) <=> T 
%querytabled * * D : {C:p} search ((false imp (atom C)) imp true).
%querytabled * * D : {C:p}search (true imp (false imp (atom C))).


% ((atom A) => (atom B) v (atom C)) =>((atom A) => (atom B)) v ((atom A) => (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) imp (atom B)) or ((atom A) imp (atom C))) imp
					     ((atom A) imp ((atom B) or (atom C)))).

 % F => (atom C) 
 %querytabled * * D : {C:p}search (false imp (atom C)).

% (atom A) => (((atom A) => F) => F) 
%querytabled * * D : {A:p}search ((atom A) imp (((atom A) imp false) imp false)).

 % (((atom A) => F) & (atom A)) => (atom C) 
%querytabled * * D : {A:p}{C:p} search ((((atom A) imp false) and (atom A)) imp (atom C)).

 % (atom A) & ~(atom B) => ~((atom A) => (atom B)) 
%querytabled * * D : {A:p}{B:p}search (((atom A) and ((atom B) imp false)) imp (((atom A) imp (atom B)) imp false)).



% (atom A) & ((atom B) v (atom C)) <=> ((atom A) & (atom B)) v ((atom A) & (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) and ((atom B) or (atom C))) imp
			     (((atom A) and (atom B)) or ((atom A) and (atom C)))).

%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) and (atom B)) or ((atom A) and (atom C))) imp
			     ((atom A) and ((atom B) or (atom C)))).

% (atom A) & F <=> F 
%querytabled * * D : {A:p}search (((atom A) and false) imp false).
%querytabled * * D : {A:p}search (false imp ((atom A) and false)).

% (atom A) v ((atom B) & (atom C)) <=> ((atom A) v (atom B)) & ((atom A) v (atom C)) 
%querytabled * * D : {A:p}{B:p}{C:p} search (((atom A) or ((atom B) and (atom C))) imp
			     ((atom A) or (atom B)) and ((atom A) or (atom C))).

%querytabled * * D : {A:p}{B:p}{C:p} search ((((atom A) or (atom B)) and ((atom A) or (atom C))) imp
			     ((atom A) or ((atom B) and (atom C)))).

%querytabled * * D : {A:p}search ((atom A) imp ((atom A) and (atom A))).
%querytabled * * D : {A:p}search (((atom A) and (atom A)) imp (atom A)).
%querytabled * * D : {A:p}search ((atom A) imp ((atom A) or (atom A))).
%querytabled * * D : {A:p}search (((atom A) or (atom A)) imp (atom A)).

% ~(atom A) v ~(atom B) => ~((atom A) & (atom B))  
%querytabled * * D : {A:p}{B:p}search ((((atom A) imp false) or ((atom B) imp false))
					 imp (((atom A) and (atom B)) imp false)).

% (atom A) => (atom A) v (atom B)  
%querytabled * * D : {A:p}{B:p}search ((atom A) imp ((atom A) or (atom B))).
% (atom B) => (atom A) v (atom B)  
%querytabled * * D : {A:p}{B:p}search ((atom B) imp ((atom A) or (atom B))).
% (atom A) & (atom B) => (atom A)  
%querytabled * * D : {A:p}{B:p}search (((atom A) and (atom B)) imp (atom A)).
% (atom A) & (atom B) => (atom B)  
%querytabled * * D : {A:p}{B:p}search (((atom A) and (atom B)) imp (atom B)).
 
% (atom A) v ~(atom A) => (((atom A) => (atom B)) => (atom A)) => (atom A) 
%querytabled * * D : {A:p}{B:p}search (((atom A) or ((atom A) imp false)) imp 
			     ((((atom A) imp (atom B)) imp (atom A)) imp (atom A))).