%------------------------------------------------------------------------------
%----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 )).
%------------------------------------------------------------------------------

%------------------------------------------------------------------------------
%----Saturation
cnf(c_0_19,plain, ( hates(butler,butler) | killed(agatha,agatha) )).
cnf(c_0_20,plain, ( hates(butler,charles) | ~ killed(charles,agatha) )).
cnf(c_0_21,plain, ( hates(butler,X1) | richer(X1,agatha) | ~ lives(X1) )).
cnf(c_0_22,plain, ( hates(X1,X2) | ~ killed(X1,X2) )).
cnf(c_0_23,plain, ( ~ hates(butler,butler) | ~ hates(butler,charles) )).
cnf(c_0_24,plain, ( ~ hates(X1,agatha) | ~ hates(X1,butler) |
                    ~ hates(X1,charles) )).
cnf(c_0_25,plain, ( hates(butler,X1) | ~ hates(agatha,X1) )).
cnf(c_0_26,plain, ( ~ richer(X1,X2) | ~ killed(X1,X2) )).
cnf(c_0_27,plain, ( ~ hates(agatha,X1) | ~ hates(charles,X1) )).
cnf(c_0_28,plain, ( ~ hates(agatha,butler) )).
cnf(c_0_29,plain, ( ~ hates(charles,charles) )).
cnf(c_0_30,plain, ( hates(butler,agatha) )).
cnf(c_0_31,plain, ( hates(agatha,charles) )).
cnf(c_0_32,plain, ( hates(agatha,agatha) )).
cnf(c_0_33,plain, ( lives(charles) )).
cnf(c_0_34,plain, ( lives(butler) )).
cnf(c_0_35,plain, ( lives(agatha) )).
%------------------------------------------------------------------------------

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