?- ace_to_pkif('A person who loves all animals is loved by someone.',X),kif_to_boxlog(X,BOX),portray_clause(user_error,(fol:-BOX)),!.

:- snark_tell(all(R,'=>'(room(R) , exists(D, '&'(door(D) , has(R,D)))))).

?- kif_to_boxlog(-((a , b ,  c , d)),_S),!,disjuncts_to_list(_S,_L),list_to_set(_L,_SET),member(_P,_SET),writeln(_P),!.


      exists([PERSON_OBJ, SOMEBODY_OBJ, _],
               (tPerson(PERSON_OBJ), implies(exists([ANIMAL_OBJ], tAnimal(ANIMAL_OBJ)), exists([_], mudLove(PERSON_OBJ, ANIMAL_OBJ))), tSomebody(SOMEBODY_OBJ), mudLove(SOMEBODY_OBJ, PERSON_OBJ))).
kif :-
        exists(PERSON_OBJ,
               exists(SOMEBODY_OBJ,
                      &(tPerson(PERSON_OBJ),
                        &(=>(exists(ANIMAL_OBJ,
                                    tAnimal(ANIMAL_OBJ)),
                             mudLove(PERSON_OBJ, ANIMAL_OBJ)),
                          &(tSomebody(SOMEBODY_OBJ),
                            mudLove(SOMEBODY_OBJ, PERSON_OBJ)))))).
%      nnf((-),
%          skolemizing(exists(PERSON_OBJ,
%                         exists(SOMEBODY_OBJ,
%                                &(tPerson(PERSON_OBJ),
%                                  &(=>(exists(ANIMAL_OBJ, tAnimal(ANIMAL_OBJ)),
%                                       mudLove(PERSON_OBJ, ANIMAL_OBJ)),
%                                    &(tSomebody(SOMEBODY_OBJ),
%                                      mudLove(SOMEBODY_OBJ, PERSON_OBJ)))))))).
%
%          succeed(user:asserta(constraintRules(PERSON_OBJ, skIsPersonInArg1ofLoveSomebodyArg2ofFn, exists(SOMEBODY_OBJ, &(tPerson(PERSON_OBJ), &(=>(exists(ANIMAL_OBJ, tAnimal(ANIMAL_OBJ)), mudLove(PERSON_OBJ, ANIMAL_OBJ)), &(tSomebody(SOMEBODY_OBJ), mudLove(SOMEBODY_OBJ, PERSON_OBJ)))))))).
%
%           nnf((-),
%               skolemizing(exists(SOMEBODY_OBJ,
%                                 &(tPerson(PERSON_OBJ),
%                                   &(=>(exists(ANIMAL_OBJ, tAnimal(ANIMAL_OBJ)),
%                                        mudLove(PERSON_OBJ, ANIMAL_OBJ)),
%                                     &(tSomebody(SOMEBODY_OBJ),
%                                       mudLove(SOMEBODY_OBJ, PERSON_OBJ))))))).
%
%               succeed(user:asserta(constraintRules(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn, &(tPerson(PERSON_OBJ), &(=>(exists(ANIMAL_OBJ, tAnimal(ANIMAL_OBJ)), mudLove(PERSON_OBJ, ANIMAL_OBJ)), &(tSomebody(SOMEBODY_OBJ), mudLove(SOMEBODY_OBJ, PERSON_OBJ))))))).
%
conj :-

        [ v(not({ constraintExists(PERSON_OBJ,
                                   skIsPersonInArg1ofLoveSomebodyArg2ofFn)
                }),
            v(not({ constraintExists(SOMEBODY_OBJ,
                                     skIsSomebodyInArg1ofLoveFn)
                  }),
              tPerson(PERSON_OBJ))),
          v(not({ constraintExists(PERSON_OBJ,
                                   skIsPersonInArg1ofLoveSomebodyArg2ofFn)
                }),
            v(not({ constraintExists(SOMEBODY_OBJ,
                                     skIsSomebodyInArg1ofLoveFn)
                  }),
              tSomebody(SOMEBODY_OBJ))),
          v(not({ constraintExists(PERSON_OBJ,
                                   skIsPersonInArg1ofLoveSomebodyArg2ofFn)
                }),
            v(not({ constraintExists(SOMEBODY_OBJ,
                                     skIsSomebodyInArg1ofLoveFn)
                  }),
              mudLove(SOMEBODY_OBJ, PERSON_OBJ))),
          v(not({ constraintExists(PERSON_OBJ,
                                   skIsPersonInArg1ofLoveSomebodyArg2ofFn)
                }),
            v(not({ constraintExists(SOMEBODY_OBJ,
                                     skIsSomebodyInArg1ofLoveFn)
                  }),
              v(not(tAnimal(ANIMAL_OBJ)),
                mudLove(PERSON_OBJ, ANIMAL_OBJ))))
        ].
cf :-
        cl([tPerson(PERSON_OBJ)],

           [ { constraintExists(PERSON_OBJ,
                                skIsPersonInArg1ofLoveSomebodyArg2ofFn)
             },
             { constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)
             }
           ]).
cf :-
        cl([tSomebody(SOMEBODY_OBJ)],

           [ { constraintExists(PERSON_OBJ,
                                skIsPersonInArg1ofLoveSomebodyArg2ofFn)
             },
             { constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)
             }
           ]).
cf :-
        cl([mudLove(SOMEBODY_OBJ, PERSON_OBJ)],

           [ { constraintExists(PERSON_OBJ,
                                skIsPersonInArg1ofLoveSomebodyArg2ofFn)
             },
             { constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)
             }
           ]).
cf :-
        cl([not(tAnimal(ANIMAL_OBJ))],

           [ { constraintExists(PERSON_OBJ,
                                skIsPersonInArg1ofLoveSomebodyArg2ofFn)
             },
             { constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)
             },
             not(mudLove(PERSON_OBJ, ANIMAL_OBJ))
           ]).
cf :-
        cl([mudLove(PERSON_OBJ, ANIMAL_OBJ)],

           [ { constraintExists(PERSON_OBJ,
                                skIsPersonInArg1ofLoveSomebodyArg2ofFn)
             },
             { constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)
             },
             tAnimal(ANIMAL_OBJ)
           ]).
fol :-

        tPerson(PERSON_OBJ):-{constraintExists(PERSON_OBJ, skIsPersonInArg1ofLoveSomebodyArg2ofFn)}, {constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)}.
        tSomebody(SOMEBODY_OBJ):-{constraintExists(PERSON_OBJ, skIsPersonInArg1ofLoveSomebodyArg2ofFn)}, {constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)}.
        mudLove(SOMEBODY_OBJ, PERSON_OBJ):-{constraintExists(PERSON_OBJ, skIsPersonInArg1ofLoveSomebodyArg2ofFn)}, {constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)}.
        not(tAnimal(ANIMAL_OBJ)):-{constraintExists(PERSON_OBJ, skIsPersonInArg1ofLoveSomebodyArg2ofFn)}, {constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)}, not(mudLove(PERSON_OBJ, ANIMAL_OBJ)).
        mudLove(PERSON_OBJ, ANIMAL_OBJ):-{constraintExists(PERSON_OBJ, skIsPersonInArg1ofLoveSomebodyArg2ofFn)}, {constraintExists(SOMEBODY_OBJ, skIsSomebodyInArg1ofLoveFn)}, tAnimal(ANIMAL_OBJ).

kif :-
        all(R,
            =>(room(R),
               exists(D, &(door(D), has(R, D))))).
% /devel/PrologMUD/runtime/run_mud_server.pl:66
%        nnf(-, skolemizing(exists(D, &(door(D), has(R, D))))).
%
% /devel/PrologMUD/runtime/run_mud_server.pl:66
%            succeed(user:asserta(constraintRules(D, skIsDoorInRoomArg2ofHasFn(R), &(door(D), has(R, D))))).
%
conj :-

        [ v(not(room(R)),
            v(not({ constraintExists(D,
                                     skIsDoorInRoomArg2ofHasFn(R))
                  }),
              door(D))),
          v(not(room(R)),
            v(not({ constraintExists(D,
                                     skIsDoorInRoomArg2ofHasFn(R))
                  }),
              has(R, D)))
        ].
cf :-
        cl([not(room(R))],

           [ { constraintExists(D, skIsDoorInRoomArg2ofHasFn(R))
             },
             not(door(D))
           ]).
cf :-
        cl([door(D)],

           [ room(R),
             { constraintExists(D, skIsDoorInRoomArg2ofHasFn(R))
             }
           ]).
cf :-
        cl([not(room(R))],

           [ { constraintExists(D, skIsDoorInRoomArg2ofHasFn(R))
             },
             not(has(R, D))
           ]).
cf :-
        cl([has(R, D)],

           [ room(R),
             { constraintExists(D, skIsDoorInRoomArg2ofHasFn(R))
             }
           ]).
% /devel/PrologMUD/runtime/run_mud_server.pl:66
%                    pfc_add= (neg room(A):-{constraintExists(B, skIsDoorInRoomArg2ofHasFn(A))}, ~(door(B))).
%
% /devel/PrologMUD/runtime/run_mud_server.pl:66
%                     pfc_add= (door(A):-room(B), {constraintExists(A, skIsDoorInRoomArg2ofHasFn(B))}).
%
% /devel/PrologMUD/runtime/run_mud_server.pl:66
%                      pfc_add= (neg room(A):-{constraintExists(B, skIsDoorInRoomArg2ofHasFn(A))}, ~(has(A, B))).
%
% /devel/PrologMUD/runtime/run_mud_server.pl:66
%                       pfc_add= (has(A, B):-room(A), {constraintExists(B, skIsDoorInRoomArg2ofHasFn(A))}).
%
kif :-
        not(&(a, &(b, &(c, d)))).
conj :-
        [v(not(a), v(not(b), v(not(c), not(d))))].
cf :-
        cl([not(a)], [b, c, d]).
cf :-
        cl([not(b)], [a, c, d]).
cf :-
        cl([not(c)], [a, b, d]).
cf :-
        cl([not(d)], [a, b, c]).
not(a):-b,c,d