%------------------------------------------------------------------------------
%----Axioms
fof(pel55_1,axiom,
    ( ? [X] :
        ( lives(X)
        & killed(X,agatha) ) )).

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

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

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

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

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

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

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

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

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

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

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

fof(pel55_11,axiom,
    (  agatha != butler )).
%------------------------------------------------------------------------------

%------------------------------------------------------------------------------
%----Model
%----Negative definition of lives
fof(lives_defn,axiom,(
    ! [X0] : ( ~ lives(X0) <=> $false ) )).

%----Positive definition of killed
fof(killed_defn,axiom,(
    ! [X0,X1] :
      ( killed(X0,X1)
    <=> ( X0 = agatha & X1 = agatha ) ) )).

%----Positive definition of richer
fof(richer_defn,axiom,(
    ! [X0,X1] :
      ( richer(X0,X1)
    <=> ( X0 = butler & X1 = agatha ) ) )).

%----Negative definition of hates
fof(hates_defn,axiom,(
    ! [X0,X1] :
      ( ~ hates(X0,X1)
    <=> ( ( X0 = agatha & X1 = butler )
        | ( X0 = butler & X1 = butler )
        | X0 = charles
        | ( X1 = butler & X0 != butler ) ) ) )).
%------------------------------------------------------------------------------

%------------------------------------------------------------------------------
%----Formulae to evaluate
fof(prove,conjecture, ? [X] : killed(X,X) ).    %----TRUE
 
fof(prove,conjecture, hates(butler,butler) ).   %----FALSE
%------------------------------------------------------------------------------