%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% this rule ...

:- kif_tell((   wearing(A,B)  => has(A,B)  )).

% has TO qualify argument types before canicalization

:-  kif_tell((argInst(has,1,A) & argInst(has,2,B) => (wearing(A,B) => has(A,B)))).

% Which produced this CODE:
%
%       has(A, B):-wearing(A, B), argInst(has, 1, A), argInst(has, 2, B).
%
%       not_wearing(A, B):- not_has(A, B), argInst(has, 1, A), argInst(has, 2, B).  % why are the last two litterals so important?
%
%       not_argInst(has, 1, A):- not_has(A, B), wearing(A, B), argInst(has, 2, B).   % notice we can disprove types
%
%       not_argInst(has, 2, A):- not_has(B, A), wearing(B, A), argInst(has, 1, B).
%

:-kif_tell(has(A,B) => (argInst(has, 1, A) & argInst(has, 2, B))).

%         not_has(A, _):- not_argInst(has, 1, A).
%
%         argInst(has, 1, A):-has(A, _).
%
%         not_has(_, B)):- not_argInst(has, 2, B).
%
%         argInst(has, 2, A):-has(_, A).



:-kif_tell(has(A,B) =>  (kb_argInst(KB, has, 1, A) & kb_argInst(KB, has, 2, B))).

% BAD!
%         (( not_has(A, _)):- not_kb_argInst( _BAD, has, 1, A)).
%
%          (kb_argInst( _BAD, has, 1, A):-has(A, _)).
%
%           (( not_has(_, A)):- not_kb_argInst( _BAD ,  has, 2, A)).
%
%            (kb_argInst( _BAD, has, 2, A):-has(_, A)).


% GOOD! (the software does this FOR us but wanted TO show the singlton in the consequent on the conjuction)

:-kif_tell(   argInst(kb_argInst, 1 , KB) =>  (        has(A,B) =>  (kb_argInst(KB, has, 1, A) & kb_argInst(KB, has, 2, B)))).

%     (( not_argInst(kb_argInst, 1, KB)):-has(A, _),  not_kb_argInst(KB, has, 1, A)).
%
%     (( not_has(A, _)):-argInst(kb_argInst, 1, KB),  not_kb_argInst(KB, has, 1, A)).
%
%     (kb_argInst(KB, has, 1, A):- argInst(kb_argInst, 1, KB), has(A, _)).
%
%    (( not_argInst(kb_argInst, 1, KB)):-has(_, B),  not_kb_argInst(KB, has, 2, B)).
%
%     (( not_has(_, B)):-argInst(kb_argInst, 1, KB),  not_kb_argInst(KB, has, 2, B)).
%
%    (kb_argInst(KB, has, 2, B):-argInst(kb_argInst, 1, KB), has(_, B)).

% EVEN BETTER?
:-kif_tell(   argInst(kb_argInst, 1 , KB) & argInst(has, 1 , A) & argInst(has, 2 , B) =>  (  has(A,B) =>  (kb_argInst(KB, has, 1, A) & kb_argInst(KB, has, 2, B)))).


%   pfc_add= (not_has(A, B)):- not_kb_argInst(C, has, 1, A), argInst(has, 2, B), argInst(kb_argInst, 1, C), argInst(has, 1, A)).
%
%   pfc_add= (kb_argInst(C, has, 1, A):-has(A, B), argInst(has, 2, B), argInst(kb_argInst, 1, C), argInst(has, 1, A)).
%
%   pfc_add= (not_argInst(has, 2, A)):-has(B, A), not_kb_argInst(C, has, 1, B), argInst(kb_argInst, 1, C), argInst(has, 1, B)).
%
%   pfc_add= (not_argInst(kb_argInst, 1, A)):-has(B, C), not_kb_argInst(A, has, 1, B), argInst(has, 2, C), argInst(has, 1, B)).
%
%   pfc_add= (not_argInst(has, 1, A)):-has(A, B), not_kb_argInst(C, has, 1, A), argInst(has, 2, B), argInst(kb_argInst, 1, C)).
%
%   (not_has(C, A)):- not_kb_argInst(B, has, 2, A), argInst(has, 2, A), argInst(kb_argInst, 1, B), argInst(has, 1, C)).
%
%   (kb_argInst(B, has, 2, A):-has(C, A), argInst(has, 2, A), argInst(kb_argInst, 1, B), argInst(has, 1, C)).
%
%   (not_argInst(has, 2, A)):-has(C, A), not_kb_argInst(B, has, 2, A), argInst(kb_argInst, 1, B), argInst(has, 1, C)).
%
%   (not_argInst(kb_argInst, 1, A)):-has(C, B), not_kb_argInst(A, has, 2, B), argInst(has, 2, B), argInst(has, 1, C)).
%
%   (not_argInst(has, 1, A)):-has(A, B), not_kb_argInst(C, has, 2, B), argInst(has, 2, B), argInst(kb_argInst, 1, C)).