%------------------------------------------------------------------------------
% File     : PUZ001_4 : TPTP v9.3.1. Released v9.3.0.
% Domain   : Puzzles
% Problem  : Dreadbury Mansion - Necessarily the killer is Agatha
% 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. 

% Refs     : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
% Source   : [TPTP]
% Names    : 

% Status   : Theorem
% Rating   : ? v9.3.0
% Syntax   : Number of formulae    :   24 (   7 unt;   8 typ;   0 def)
%            Number of atoms       :   27 (   7 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :   20 (   8   ~;   2   |;   1   &)
%                                         (   0 <=>;   7  =>;   0  <=;   0 <~>)
%                                         (   1 {.};   0 {#})
%            Maximal formula depth :    5 (   3 avg)
%            Maximal term depth    :    1 (   1 avg)
%            Number of FOOLs       :    1 (   1 fml;   0 var)
%            Number of X terms     :    1 (   1  [];   0 ite;   0 let;   0 dis)
%            Number of types       :    2 (   1 usr)
%            Number of type conns  :    7 (   4   >;   3   *;   0   +;   0  <<)
%            Number of predicates  :    6 (   4 usr;   1 prp; 0-2 aty)
%            Number of functors    :    3 (   3 usr;   3 con; 0-0 aty)
%            Number of variables   :   12 (  10   !;   2   ?;  12   :)
% SPC      : NX0_THM_EQU_NAR_NDT

% Comments : Modified by Geoff Sutcliffe.
%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal == 
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_S5 ] ).

tff(person_type,type,
    person: $tType ).

tff(agatha_decl,type,
    agatha: person ).

tff(butler_decl,type,
    butler: person ).

tff(charles_decl,type,
    charles: person ).

tff(lives_decl,type,
    lives: person > $o ).

tff(killed_decl,type,
    killed: ( person * person ) > $o ).

tff(hates_decl,type,
    hates: ( person * person ) > $o ).

tff(richer_decl,type,
    richer: ( person * person ) > $o ).

tff(pel55_1,axiom,
    ? [X: person] :
      ( lives(X)
      & killed(X,agatha) ) ).

tff(pel55_2_1,axiom,
    lives(agatha) ).

tff(pel55_2_2,axiom,
    lives(butler) ).

tff(pel55_2_3,axiom,
    lives(charles) ).

tff(pel55_3,axiom,
    ! [X: person] :
      ( lives(X)
     => ( ( X = agatha )
        | ( X = butler )
        | ( X = charles ) ) ) ).

tff(pel55_11a,axiom,
    agatha != butler ).

tff(pel55_11b,axiom,
    butler != charles ).

tff(pel55_11c,axiom,
    charles != agatha ).

tff(pel55_4,axiom,
    ! [X: person,Y: person] :
      ( killed(X,Y)
     => hates(X,Y) ) ).

tff(pel55_5,axiom,
    ! [X: person,Y: person] :
      ( killed(X,Y)
     => ~ richer(X,Y) ) ).

tff(pel55_6,axiom,
    ! [X: person] :
      ( hates(agatha,X)
     => ~ hates(charles,X) ) ).

tff(pel55_7,axiom,
    ! [X: person] :
      ( ( X != butler )
     => hates(agatha,X) ) ).

tff(pel55_8,axiom,
    ! [X: person] :
      ( ~ richer(X,agatha)
     => hates(butler,X) ) ).

tff(pel55_9,axiom,
    ! [X: person] :
      ( hates(agatha,X)
     => hates(butler,X) ) ).

tff(pel55_10,axiom,
    ! [X: person] :
    ? [Y: person] : ~ hates(X,Y) ).

%----Provable of course
tff(pel55,conjecture,
    {$necessary} @ (killed(agatha,agatha)) ).

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