<oats_> I brought ((P( y) ⊃ Q(z)) ⊃ (P(x) ⊃ Q(x))) to (~P(y)

baseKB:  ?- kif_to_boxlog((( (p(Y) =>  q(Z))  =>   (p(X) =>  q(X)))),O).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% unknown
% kif :-
%       all(X, all(Y, all(Z, =>(=>(p(Y), q(Z)), =>(p(X), q(X)))))).
% pkif :-
%       all(X, all(Y, all(Z, =>(=>(p(Y), q(Z)), =>(p(X), q(X)))))).
% cnf :-
%       (p(Y)v (not(p(X))v q(X)))& (not(q(Z))v (not(p(X))v q(X))).
% horn :-
%
%       [ (not(p(X)):-not(p(Y)), not(q(X))),
%         (not(p(X)):-q(Z), not(q(X))),
%         (not(q(Z)):-p(X), not(q(X))),
%         (p(Y):-p(X), not(q(X))),
%         (q(X):-not(p(Y)), p(X)),
%         (q(X):-q(Z), p(X))
%       ].
O = [(not(p(X)):-not(p(Y)), not(