my use of not_in/2 in might be confusing unless you knew tha

baseKB:  ?- kif_to_boxlog(all([Person,GrandFather], exactly(1,Parent,(parent(Person,Parent) ,   father(Parent,GrandFather)) =>  grand_father(Person,GrandFather))),O),maplist(fmt9,O).
% kif :-
%       all([Person, GrandFather],
%           exactly(1,
%                   Parent,
%                   (parent(Person, Parent)&father(Parent, GrandFather)=>grand_father(Person, GrandFather)))).



% my use of not_in/2 in might be confusing unless you knew
% that they mean "'not' already created 'in' this global deductive context"

proven_tru(father(Parent, GrandFather)) :-
        not_in(Parent,
               skF(1,
                   skParentFalseArg2Parent_1_0FnSk(GrandFather, Person),
                   Parent,

                   [ ((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);q(grand_father(Person, GrandFather))=true)
                   ])).

proven_tru(parent(Person, Parent)) :-
        not_in(Parent,
               skF(1,
                   skParentFalseArg2Parent_1_0FnSk(GrandFather, Person),
                   Parent,

                   [ ((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);q(grand_father(Person, GrandFather))=true)
                   ])).


deduce_tru(grand_father(Person, GrandFather)) :-
        nesc(parent(Person, Parent)),
        skolem(Parent,
               skF(1,
                   skParentFalseArg2Parent_1_0FnSk(GrandFather, Person),
                   Parent,

                   [ ((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);q(grand_father(Person, GrandFather))=true)
                   ])),
        nesc(father(Parent, GrandFather)).


make_existential(Parent, skF(1, skParentFalseArg2Parent_1_0FnSk(GrandFather, Person), Parent,
    [((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);
          q(grand_father(Person, GrandFather))=true)])) :-
        (   ensure_cond(Parent, parent(Person, Parent)),
            never_cond(Parent, father(Parent, GrandFather))
        ;   ensure_cond(Parent, grand_father(Person, GrandFather))
        ).


deduce_neg(father(Parent, GrandFather)) :-
        nesc(parent(Person, Parent)),
        skolem(Parent,
               skF(1,
                   skParentFalseArg2Parent_1_0FnSk(GrandFather, Person),
                   Parent,

                   [ ((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);q(grand_father(Person, GrandFather))=true)
                   ])),
        falsify(grand_father(Person, GrandFather)).


deduce_neg(grand_father(Person, GrandFather)) :-
        not_in(Parent,
               skF(1,
                   skParentFalseArg2Parent_1_0FnSk(GrandFather, Person),
                   Parent,

                   [ ((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);q(grand_father(Person, GrandFather))=true)
                   ])).

deduce_neg(parent(Person, Parent)) :-
        nesc(father(Parent, GrandFather)),
        skolem(Parent,
               skF(1,
                   skParentFalseArg2Parent_1_0FnSk(GrandFather, Person),
                   Parent,

                   [ ((p(parent(Person, Parent))=false;p(father(Parent, GrandFather))=false);q(grand_father(Person, GrandFather))=true)
                   ])),
        falsify(grand_father(Person, GrandFather)).