% The Dreadsbury Mansion Mystery
% Developed by Tom Larson and Aaron Roe
% 5 February 1998

% Standard initialization statements
set(auto).
assign(max_seconds,60).
formula_list(usable).

% Someone who lives in Dreadsbury Mansion killed Aunt Agatha.
all x (Killer(x) -> Mansion(x)).

% Agatha, butler, Charles live in Dreadsbury Mansion.
Mansion(Agatha).
Mansion(butler).
Mansion(Charles).

% Limit the killer to the three people living in the mansion.  This repeats
% the information in the above four statements, but also explicitly says
% That no one else lives in the mansion.
Killer(Agatha) | Killer(butler) | Killer(Charles).

% A killer always hates his victim.
all x (Killer(x) -> Hates(x,Agatha)).

% and is never richer than his victim.
all x (Killer(x) -> -Richer(x,Agatha)).

% Charles hates no one that Aunt Agatha hates.
all x (Hates(Agatha,x) -> -Hates(Charles,x)).

% Agatha hates everyone but the butler.
all x ((x != butler) -> Hates(Agatha,x)).

% The butler hates everyone not richer than Aunt Agatha.
all x (-(Richer(x,Agatha)) -> Hates(butler,x)).

% The butler hates everyone Agatha hates.
all x (Hates(Agatha, x) -> Hates(butler,x)).

% No one hates everyone.
all x exists y (-Hates(x,y)).

% Agatha is not the butler.
butler != Agatha.


% The tests.  Uncomment _one_ of these statements, and otter will
% tell you if it is consistent with the givens above.  Each statement
% is the negation of what the detective said.

%Bjorn's wrong:
%Killer(Charles).

%Reidar's wrong:
-Killer(Agatha).

%Olaf's wrong:
%Killer(butler).

% We find out that all three Norwegian detectives are right, and
% Agatha is the killer.

end_of_list.