% benchmark parameters -n2 -N6 -p

%--------------------------------------------------------------------------
% File     : PUZ001-3 : TPTP v2.3.0. Released v1.2.0.
% Domain   : Puzzles
% Problem  : Dreadbury Mansion
% Version  : Especial.
% 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.

% Refs     : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
%          : [MB88]  Manthey & Bry (1988), SATCHMO: A Theorem Prover Implem
% Source   : [MB88]
% Names    : - [MB88]

% Status   : satisfiable
% Rating   : 0.00 v2.1.0, 0.00 v2.0.0
% Syntax   : Number of clauses    :   12 (   2 non-Horn;   5 unit;  12 RR)
%            Number of literals   :   22 (   0 equality)
%            Maximal clause size  :    3 (   1 average)
%            Number of predicates :    4 (   0 propositional; 1-2 arity)
%            Number of functors   :    3 (   3 constant; 0-0 arity)
%            Number of variables  :    8 (   0 singleton)
%            Maximal term depth   :    1 (   1 average)

% Comments : Also known as "Who killed Aunt Agatha"
%          : tptp2X -f otter:hypothesis:[set(tptp_eq),set(auto),clear(print_given)] -t rm_equality:stfp PUZ001-3.p 
%--------------------------------------------------------------------------
set(prolog_style_variables).
set(tptp_eq).
set(auto).
clear(print_given).

list(usable).

% agatha, axiom.
 lives(agatha).

% butler, axiom.
 lives(butler).

% charles, axiom.
 lives(charles).

% poorer_killer, axiom.
-killed(X, Y) |
-richer(X, Y).

% different_hates, axiom.
-hates(agatha, X) |
-hates(charles, X).

% no_one_hates_everyone, axiom.
-hates(X, agatha) |
-hates(X, butler) |
-hates(X, charles).

% agatha_hates_agatha, axiom.
 hates(agatha, agatha).

% agatha_hates_charles, axiom.
 hates(agatha, charles).

% killer_hates_victim, axiom.
-killed(X, Y) |
 hates(X, Y).

% same_hates, axiom.
-hates(agatha, X) |
 hates(butler, X).

% butler_hates_poor, axiom.
-lives(X) |
 richer(X, agatha) |
 hates(butler, X).

end_of_list.

list(sos).

% somebody_did_it, conjecture.
 killed(agatha, agatha) |
 killed(butler, agatha) |
 killed(charles, agatha).

end_of_list.

%--------------------------------------------------------------------------