baseKB: [debug]  ?- KB=kb1,   I=(( (p(Y) =>  q(Z))  =>   (p(X) =>  q(X)))), nnf(KB,I,NNF), cnf(KB,NNF,CNF).
KB = kb1,
I = =>(=>(p(Y), q(Z)), =>(p(X), q(X))),
NNF = p(Y)&not(q(Z))v (not(p(X))v q(X)),
CNF =  (p(Y)v (not(p(X))v q(X)))& (not(q(Z))v (not(p(X))v q(X))).