% English  : Someone who lives in Dreadbury Mansion killed Aunt Agatha. 
%            Agatha, the butler, and Charles live in Dreadbury Mansion, 
%            and are the only people who live therein. A killer always 
%            hates his victim, and is never richer than his victim. 
%            Charles hates no one that Aunt Agatha hates. Agatha hates 
%            everyone except the butler. The butler hates everyone not 
%            richer than Aunt Agatha. The butler hates everyone Aunt 
%            Agatha hates. No one hates everyone. Agatha is not the 
%            butler. Therefore : Agatha killed herself.
set(prolog_style_variables).
set(auto).
clear(print_given).

formula_list(usable).

% reflexivity, axiom.
    ( all A equal(A,A) ).

% pel55_1, axiom.
    ( exists X 
      ( lives(X)
       & killed(X,agatha) ) ).

% pel55_2_1, axiom.
    lives(agatha).

% pel55_2_2, axiom.
    lives(butler).

% pel55_2_3, axiom.
    lives(charles).

% pel55_3, axiom.
    ( all X 
      ( lives(X)
      -> ( equal(X,agatha)
         | equal(X,butler)
         | equal(X,charles) ) ) ).

% pel55_4, axiom.
    ( all X Y 
      ( killed(X,Y)
      -> hates(X,Y) ) ).

% pel55_5, axiom.
    ( all X Y 
      ( killed(X,Y)
      -> -(richer(X,Y)) ) ).

% pel55_6, axiom.
    ( all X 
      ( hates(agatha,X)
      -> -(hates(charles,X)) ) ).

% pel55_7, axiom.
    ( all X 
      ( -(equal(X,butler))
      -> hates(agatha,X) ) ).

% pel55_8, axiom.
    ( all X 
      ( -(richer(X,agatha))
      -> hates(butler,X) ) ).

% pel55_9, axiom.
    ( all X 
      ( hates(agatha,X)
      -> hates(butler,X) ) ).

% pel55_10, axiom.
    ( all X 
    ( exists Y -(hates(X,Y)) ) ).

% pel55_11, axiom.
    -(equal(agatha,butler)).

end_of_list.

list(usable).
% pel55, negated_conjecture.

%    -(killed(agatha,agatha)).

%-(killed(X,agatha)) | $ans(X).


%-(killed(X,agatha)) | -eq(X,agatha)  | $ans(X).

%-killed(buttler,agatha).
killed(butler,agatha).
end_of_list.

