%------------------------------------------------------------------------------
% File       : Metis---2.2
% Problem    : PUZ001+1 : TPTP v3.5.0. Released v2.0.0.
% Transform  : none
% Format     : tptp
% Command    : metis --show proof --show saturation %s

% Computer   : art06.cs.miami.edu
% Model      : i686 i686
% CPU        : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory     : 1002MB
% OS         : Linux 2.6.18-1.2798.fc6
% CPULimit   : 600s
% DateTime   : Wed May  6 15:09:49 EDT 2009

% Result     : Theorem 0.0s
% Output     : CNFRefutation 0.0s
% Verified   : 
% Statistics : Number of formulae       :   82 ( 105 expanded)
%              Number of clauses        :   46 (  51 expanded)
%              Number of leaves         :   15 (  20 expanded)
%              Depth                    :   16
%              Number of atoms          :  156 ( 192 expanded)
%              Number of equality atoms :   44 (  48 expanded)
%              Maximal formula depth    :    5 (   3 average)
%              Maximal clause size      :    4 (   3 average)
%              Maximal term depth       :    2 (   1 average)

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

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

fof(pel55,conjecture,(
    killed(agatha,agatha) )).

fof(subgoal_0,plain,(
    killed(agatha,agatha) ),
    inference(strip,[],[pel55])).

fof(negate_0_0,plain,(
    ~ killed(agatha,agatha) ),
    inference(negate,[],[subgoal_0])).

fof(normalize_0_0,plain,(
    ! [X] :
      ( X = butler
      | hates(agatha,X) ) ),
    inference(canonicalize,[],[pel55_7])).

fof(normalize_0_1,plain,(
    ! [X] :
      ( X = butler
      | hates(agatha,X) ) ),
    inference(specialize,[],[normalize_0_0])).

fof(normalize_0_2,plain,(
    ! [X] :
      ( ~ hates(agatha,X)
      | ~ hates(charles,X) ) ),
    inference(canonicalize,[],[pel55_6])).

fof(normalize_0_3,plain,(
    ! [X] :
      ( ~ hates(agatha,X)
      | ~ hates(charles,X) ) ),
    inference(specialize,[],[normalize_0_2])).

fof(normalize_0_4,plain,(
    ? [X] :
      ( killed(X,agatha)
      & lives(X) ) ),
    inference(canonicalize,[],[pel55_1])).

fof(normalize_0_5,plain,
    ( killed(skolemFOFtoCNF_X,agatha)
    & lives(skolemFOFtoCNF_X) ),
    inference(skolemize,[],[normalize_0_4])).

fof(normalize_0_6,plain,(
    killed(skolemFOFtoCNF_X,agatha) ),
    inference(conjunct,[],[normalize_0_5])).

fof(normalize_0_7,plain,(
    ! [X,Y] :
      ( ~ killed(X,Y)
      | hates(X,Y) ) ),
    inference(canonicalize,[],[pel55_4])).

fof(normalize_0_8,plain,(
    ! [X,Y] :
      ( ~ killed(X,Y)
      | hates(X,Y) ) ),
    inference(specialize,[],[normalize_0_7])).

fof(normalize_0_9,plain,(
    ! [X] :
      ( hates(butler,X)
      | richer(X,agatha) ) ),
    inference(canonicalize,[],[pel55_8])).

fof(normalize_0_10,plain,(
    ! [X] :
      ( hates(butler,X)
      | richer(X,agatha) ) ),
    inference(specialize,[],[normalize_0_9])).

fof(normalize_0_11,plain,(
    ! [X,Y] :
      ( ~ killed(X,Y)
      | ~ richer(X,Y) ) ),
    inference(canonicalize,[],[pel55_5])).

fof(normalize_0_12,plain,(
    ! [X,Y] :
      ( ~ killed(X,Y)
      | ~ richer(X,Y) ) ),
    inference(specialize,[],[normalize_0_11])).

fof(normalize_0_13,plain,(
    lives(skolemFOFtoCNF_X) ),
    inference(conjunct,[],[normalize_0_5])).

fof(normalize_0_14,plain,(
    ! [X] :
      ( ~ lives(X)
      | X = agatha
      | X = butler
      | X = charles ) ),
    inference(canonicalize,[],[pel55_3])).

fof(normalize_0_15,plain,(
    ! [X] :
      ( ~ lives(X)
      | X = agatha
      | X = butler
      | X = charles ) ),
    inference(specialize,[],[normalize_0_14])).

fof(normalize_0_16,plain,(
    ~ killed(agatha,agatha) ),
    inference(canonicalize,[],[negate_0_0])).

fof(normalize_0_17,plain,(
    ! [X] :
    ? [Y] : ~ hates(X,Y) ),
    inference(canonicalize,[],[pel55_10])).

fof(normalize_0_18,plain,(
    ! [X] :
    ? [Y] : ~ hates(X,Y) ),
    inference(specialize,[],[normalize_0_17])).

fof(normalize_0_19,plain,(
    ! [X] : ~ hates(X,skolemFOFtoCNF_Y(X)) ),
    inference(skolemize,[],[normalize_0_18])).

fof(normalize_0_20,plain,(
    ! [X] :
      ( ~ hates(agatha,X)
      | hates(butler,X) ) ),
    inference(canonicalize,[],[pel55_9])).

fof(normalize_0_21,plain,(
    ! [X] :
      ( ~ hates(agatha,X)
      | hates(butler,X) ) ),
    inference(specialize,[],[normalize_0_20])).

fof(normalize_0_22,plain,(
    agatha != butler ),
    inference(canonicalize,[],[pel55_11])).

cnf(refute_0_0,plain,
    ( X = butler
    | hates(agatha,X) ),
    inference(canonicalize,[],[normalize_0_1])).

cnf(refute_0_1,plain,
    ( agatha = butler
    | hates(agatha,agatha) ),
    inference(subst,[],[refute_0_0:[bind(X,$fot(agatha))]])).

cnf(refute_0_2,plain,
    ( ~ hates(agatha,X)
    | ~ hates(charles,X) ),
    inference(canonicalize,[],[normalize_0_3])).

cnf(refute_0_3,plain,
    ( ~ hates(agatha,agatha)
    | ~ hates(charles,agatha) ),
    inference(subst,[],[refute_0_2:[bind(X,$fot(agatha))]])).

cnf(refute_0_4,plain,
    ( killed(skolemFOFtoCNF_X,agatha) ),
    inference(canonicalize,[],[normalize_0_6])).

cnf(refute_0_5,plain,
    ( ~ killed(X,Y)
    | hates(X,Y) ),
    inference(canonicalize,[],[normalize_0_8])).

cnf(refute_0_6,plain,
    ( ~ killed(skolemFOFtoCNF_X,agatha)
    | hates(skolemFOFtoCNF_X,agatha) ),
    inference(subst,[],[refute_0_5:[bind(X,$fot(skolemFOFtoCNF_X)),bind(Y,$fot(agatha))]])).

cnf(refute_0_7,plain,
    ( hates(skolemFOFtoCNF_X,agatha) ),
    inference(resolve,[$cnf(killed(skolemFOFtoCNF_X,agatha))],[refute_0_4,refute_0_6])).

cnf(refute_0_8,plain,
    ( hates(butler,X)
    | richer(X,agatha) ),
    inference(canonicalize,[],[normalize_0_10])).

cnf(refute_0_9,plain,
    ( hates(butler,X1)
    | richer(X1,agatha) ),
    inference(subst,[],[refute_0_8:[bind(X,$fot(X1))]])).

cnf(refute_0_10,plain,
    ( ~ killed(X,Y)
    | ~ richer(X,Y) ),
    inference(canonicalize,[],[normalize_0_12])).

cnf(refute_0_11,plain,
    ( ~ killed(X1,agatha)
    | ~ richer(X1,agatha) ),
    inference(subst,[],[refute_0_10:[bind(X,$fot(X1)),bind(Y,$fot(agatha))]])).

cnf(refute_0_12,plain,
    ( ~ killed(X1,agatha)
    | hates(butler,X1) ),
    inference(resolve,[$cnf(richer(X1,agatha))],[refute_0_9,refute_0_11])).

cnf(refute_0_13,plain,
    ( ~ killed(skolemFOFtoCNF_X,agatha)
    | hates(butler,skolemFOFtoCNF_X) ),
    inference(subst,[],[refute_0_12:[bind(X1,$fot(skolemFOFtoCNF_X))]])).

cnf(refute_0_14,plain,
    ( hates(butler,skolemFOFtoCNF_X) ),
    inference(resolve,[$cnf(killed(skolemFOFtoCNF_X,agatha))],[refute_0_4,refute_0_13])).

cnf(refute_0_15,plain,
    ( lives(skolemFOFtoCNF_X) ),
    inference(canonicalize,[],[normalize_0_13])).

cnf(refute_0_16,plain,
    ( ~ lives(X)
    | X = agatha
    | X = butler
    | X = charles ),
    inference(canonicalize,[],[normalize_0_15])).

cnf(refute_0_17,plain,
    ( ~ lives(skolemFOFtoCNF_X)
    | skolemFOFtoCNF_X = agatha
    | skolemFOFtoCNF_X = butler
    | skolemFOFtoCNF_X = charles ),
    inference(subst,[],[refute_0_16:[bind(X,$fot(skolemFOFtoCNF_X))]])).

cnf(refute_0_18,plain,
    ( skolemFOFtoCNF_X = agatha
    | skolemFOFtoCNF_X = butler
    | skolemFOFtoCNF_X = charles ),
    inference(resolve,[$cnf(lives(skolemFOFtoCNF_X))],[refute_0_15,refute_0_17])).

cnf(refute_0_19,plain,
    ( skolemFOFtoCNF_X != agatha
    | ~ killed(skolemFOFtoCNF_X,agatha)
    | killed(agatha,agatha) ),
    introduced(tautology,[equality,[$cnf(killed(skolemFOFtoCNF_X,agatha)),[0],$fot(agatha)]])).

cnf(refute_0_20,plain,
    ( ~ killed(skolemFOFtoCNF_X,agatha)
    | skolemFOFtoCNF_X = butler
    | skolemFOFtoCNF_X = charles
    | killed(agatha,agatha) ),
    inference(resolve,[$cnf('$equal'(skolemFOFtoCNF_X,agatha))],[refute_0_18,refute_0_19])).

cnf(refute_0_21,plain,
    ( skolemFOFtoCNF_X = butler
    | skolemFOFtoCNF_X = charles
    | killed(agatha,agatha) ),
    inference(resolve,[$cnf(killed(skolemFOFtoCNF_X,agatha))],[refute_0_4,refute_0_20])).

cnf(refute_0_22,plain,
    ( ~ killed(agatha,agatha) ),
    inference(canonicalize,[],[normalize_0_16])).

cnf(refute_0_23,plain,
    ( skolemFOFtoCNF_X = butler
    | skolemFOFtoCNF_X = charles ),
    inference(resolve,[$cnf(killed(agatha,agatha))],[refute_0_21,refute_0_22])).

cnf(refute_0_24,plain,
    ( skolemFOFtoCNF_X != butler
    | ~ hates(butler,skolemFOFtoCNF_X)
    | hates(butler,butler) ),
    introduced(tautology,[equality,[$cnf(hates(butler,skolemFOFtoCNF_X)),[1],$fot(butler)]])).

cnf(refute_0_25,plain,
    ( ~ hates(butler,skolemFOFtoCNF_X)
    | skolemFOFtoCNF_X = charles
    | hates(butler,butler) ),
    inference(resolve,[$cnf('$equal'(skolemFOFtoCNF_X,butler))],[refute_0_23,refute_0_24])).

cnf(refute_0_26,plain,
    ( skolemFOFtoCNF_X = charles
    | hates(butler,butler) ),
    inference(resolve,[$cnf(hates(butler,skolemFOFtoCNF_X))],[refute_0_14,refute_0_25])).

cnf(refute_0_27,plain,
    ( ~ hates(X,skolemFOFtoCNF_Y(X)) ),
    inference(canonicalize,[],[normalize_0_19])).

cnf(refute_0_28,plain,
    ( ~ hates(butler,skolemFOFtoCNF_Y(butler)) ),
    inference(subst,[],[refute_0_27:[bind(X,$fot(butler))]])).

cnf(refute_0_29,plain,
    ( X0 = butler
    | hates(agatha,X0) ),
    inference(subst,[],[refute_0_0:[bind(X,$fot(X0))]])).

cnf(refute_0_30,plain,
    ( ~ hates(agatha,X)
    | hates(butler,X) ),
    inference(canonicalize,[],[normalize_0_21])).

cnf(refute_0_31,plain,
    ( ~ hates(agatha,X0)
    | hates(butler,X0) ),
    inference(subst,[],[refute_0_30:[bind(X,$fot(X0))]])).

cnf(refute_0_32,plain,
    ( X0 = butler
    | hates(butler,X0) ),
    inference(resolve,[$cnf(hates(agatha,X0))],[refute_0_29,refute_0_31])).

cnf(refute_0_33,plain,
    ( skolemFOFtoCNF_Y(butler) = butler
    | hates(butler,skolemFOFtoCNF_Y(butler)) ),
    inference(subst,[],[refute_0_32:[bind(X0,$fot(skolemFOFtoCNF_Y(butler)))]])).

cnf(refute_0_34,plain,
    ( skolemFOFtoCNF_Y(butler) = butler ),
    inference(resolve,[$cnf(hates(butler,skolemFOFtoCNF_Y(butler)))],[refute_0_33,refute_0_28])).

cnf(refute_0_35,plain,
    ( skolemFOFtoCNF_Y(butler) != butler
    | ~ hates(butler,butler)
    | hates(butler,skolemFOFtoCNF_Y(butler)) ),
    introduced(tautology,[equality,[$cnf(~ hates(butler,skolemFOFtoCNF_Y(butler))),[1],$fot(butler)]])).

cnf(refute_0_36,plain,
    ( ~ hates(butler,butler)
    | hates(butler,skolemFOFtoCNF_Y(butler)) ),
    inference(resolve,[$cnf('$equal'(skolemFOFtoCNF_Y(butler),butler))],[refute_0_34,refute_0_35])).

cnf(refute_0_37,plain,
    ( ~ hates(butler,butler) ),
    inference(resolve,[$cnf(hates(butler,skolemFOFtoCNF_Y(butler)))],[refute_0_36,refute_0_28])).

cnf(refute_0_38,plain,
    ( skolemFOFtoCNF_X = charles ),
    inference(resolve,[$cnf(hates(butler,butler))],[refute_0_26,refute_0_37])).

cnf(refute_0_39,plain,
    ( skolemFOFtoCNF_X != charles
    | ~ hates(skolemFOFtoCNF_X,agatha)
    | hates(charles,agatha) ),
    introduced(tautology,[equality,[$cnf(hates(skolemFOFtoCNF_X,agatha)),[0],$fot(charles)]])).

cnf(refute_0_40,plain,
    ( ~ hates(skolemFOFtoCNF_X,agatha)
    | hates(charles,agatha) ),
    inference(resolve,[$cnf('$equal'(skolemFOFtoCNF_X,charles))],[refute_0_38,refute_0_39])).

cnf(refute_0_41,plain,
    ( hates(charles,agatha) ),
    inference(resolve,[$cnf(hates(skolemFOFtoCNF_X,agatha))],[refute_0_7,refute_0_40])).

cnf(refute_0_42,plain,
    ( ~ hates(agatha,agatha) ),
    inference(resolve,[$cnf(hates(charles,agatha))],[refute_0_41,refute_0_3])).

cnf(refute_0_43,plain,
    ( agatha = butler ),
    inference(resolve,[$cnf(hates(agatha,agatha))],[refute_0_1,refute_0_42])).

cnf(refute_0_44,plain,
    ( agatha != butler ),
    inference(canonicalize,[],[normalize_0_22])).

cnf(refute_0_45,plain,
    ( $false ),
    inference(resolve,[$cnf('$equal'(agatha,butler))],[refute_0_43,refute_0_44])).
%------------------------------------------------------------------------------