TSTP Solution File: PUZ001+1 by EP---1.2
View Problem
- Process Solution
%------------------------------------------------------------------------------
% File : EP---1.2
% Problem : PUZ001+1 : TPTP v4.1.0. Released v2.0.0.
% Transform : none
% Format : tptp:raw
% Command : eproof --print-statistics -xAuto -tAuto --cpu-limit=%d --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Jul 29 22:06:18 EDT 2010
% Result : Theorem 0.10s
% Output : CNFRefutation 0.10s
% Verified :
% Statistics : Number of formulae : 63 ( 92 expanded)
% Number of clauses : 29 ( 36 expanded)
% Number of leaves : 11 ( 18 expanded)
% Depth : 12
% Number of atoms : 117 ( 176 expanded)
% Number of equality atoms : 34 ( 53 expanded)
% Maximal formula depth : 5 ( 3 average)
% Maximal clause size : 4 ( 4 average)
% Maximal term depth : 2 ( 1 average)
% Comments :
%------------------------------------------------------------------------------
fof(16,axiom,(
? [X1] :
( lives(X1)
& killed(X1,agatha) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_1)).
fof(20,axiom,(
! [X1] :
( lives(X1)
=> ( X1 = agatha
| X1 = butler
| X1 = charles ) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_3)).
fof(21,axiom,(
! [X1,X2] :
( killed(X1,X2)
=> hates(X1,X2) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_4)).
fof(22,axiom,(
! [X1,X2] :
( killed(X1,X2)
=> ~ richer(X1,X2) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_5)).
fof(23,axiom,(
! [X1] :
( hates(agatha,X1)
=> ~ hates(charles,X1) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_6)).
fof(24,axiom,(
! [X1] :
( X1 != butler
=> hates(agatha,X1) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_7)).
fof(25,axiom,(
! [X1] :
( ~ richer(X1,agatha)
=> hates(butler,X1) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_8)).
fof(26,axiom,(
! [X1] :
( hates(agatha,X1)
=> hates(butler,X1) ) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_9)).
fof(27,axiom,(
! [X1] :
? [X2] : ~ hates(X1,X2) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_10)).
fof(28,axiom,(
agatha != butler ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55_11)).
fof(29,negated_conjecture,(
~ killed(agatha,agatha) ),
file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p',pel55)).
fof(30,plain,(
! [X1,X2] :
( killed(X1,X2)
=> ~ richer(X1,X2) ) ),
inference(fof_simplification,[status(thm)],[22,theory(equality)])).
fof(31,plain,(
! [X1] :
( hates(agatha,X1)
=> ~ hates(charles,X1) ) ),
inference(fof_simplification,[status(thm)],[23,theory(equality)])).
fof(32,plain,(
! [X1] :
( ~ richer(X1,agatha)
=> hates(butler,X1) ) ),
inference(fof_simplification,[status(thm)],[25,theory(equality)])).
fof(33,plain,(
! [X1] :
? [X2] : ~ hates(X1,X2) ),
inference(fof_simplification,[status(thm)],[27,theory(equality)])).
fof(34,negated_conjecture,(
~ killed(agatha,agatha) ),
inference(fof_simplification,[status(thm)],[29,theory(equality)])).
fof(35,plain,(
? [X2] :
( lives(X2)
& killed(X2,agatha) ) ),
inference(variable_rename,[status(thm)],[16])).
fof(36,plain,
( lives(esk1_0)
& killed(esk1_0,agatha) ),
inference(skolemize,[status(esa)],[35])).
cnf(37,plain,
( killed(esk1_0,agatha) ),
inference(split_conjunct,[status(thm)],[36])).
cnf(38,plain,
( lives(esk1_0) ),
inference(split_conjunct,[status(thm)],[36])).
fof(42,plain,(
! [X1] :
( ~ lives(X1)
| X1 = agatha
| X1 = butler
| X1 = charles ) ),
inference(fof_nnf,[status(thm)],[20])).
fof(43,plain,(
! [X2] :
( ~ lives(X2)
| X2 = agatha
| X2 = butler
| X2 = charles ) ),
inference(variable_rename,[status(thm)],[42])).
cnf(44,plain,
( X1 = charles
| X1 = butler
| X1 = agatha
| ~ lives(X1) ),
inference(split_conjunct,[status(thm)],[43])).
fof(45,plain,(
! [X1,X2] :
( ~ killed(X1,X2)
| hates(X1,X2) ) ),
inference(fof_nnf,[status(thm)],[21])).
fof(46,plain,(
! [X3,X4] :
( ~ killed(X3,X4)
| hates(X3,X4) ) ),
inference(variable_rename,[status(thm)],[45])).
cnf(47,plain,
( hates(X1,X2)
| ~ killed(X1,X2) ),
inference(split_conjunct,[status(thm)],[46])).
fof(48,plain,(
! [X1,X2] :
( ~ killed(X1,X2)
| ~ richer(X1,X2) ) ),
inference(fof_nnf,[status(thm)],[30])).
fof(49,plain,(
! [X3,X4] :
( ~ killed(X3,X4)
| ~ richer(X3,X4) ) ),
inference(variable_rename,[status(thm)],[48])).
cnf(50,plain,
( ~ richer(X1,X2)
| ~ killed(X1,X2) ),
inference(split_conjunct,[status(thm)],[49])).
fof(51,plain,(
! [X1] :
( ~ hates(agatha,X1)
| ~ hates(charles,X1) ) ),
inference(fof_nnf,[status(thm)],[31])).
fof(52,plain,(
! [X2] :
( ~ hates(agatha,X2)
| ~ hates(charles,X2) ) ),
inference(variable_rename,[status(thm)],[51])).
cnf(53,plain,
( ~ hates(charles,X1)
| ~ hates(agatha,X1) ),
inference(split_conjunct,[status(thm)],[52])).
fof(54,plain,(
! [X1] :
( X1 = butler
| hates(agatha,X1) ) ),
inference(fof_nnf,[status(thm)],[24])).
fof(55,plain,(
! [X2] :
( X2 = butler
| hates(agatha,X2) ) ),
inference(variable_rename,[status(thm)],[54])).
cnf(56,plain,
( hates(agatha,X1)
| X1 = butler ),
inference(split_conjunct,[status(thm)],[55])).
fof(57,plain,(
! [X1] :
( richer(X1,agatha)
| hates(butler,X1) ) ),
inference(fof_nnf,[status(thm)],[32])).
fof(58,plain,(
! [X2] :
( richer(X2,agatha)
| hates(butler,X2) ) ),
inference(variable_rename,[status(thm)],[57])).
cnf(59,plain,
( hates(butler,X1)
| richer(X1,agatha) ),
inference(split_conjunct,[status(thm)],[58])).
fof(60,plain,(
! [X1] :
( ~ hates(agatha,X1)
| hates(butler,X1) ) ),
inference(fof_nnf,[status(thm)],[26])).
fof(61,plain,(
! [X2] :
( ~ hates(agatha,X2)
| hates(butler,X2) ) ),
inference(variable_rename,[status(thm)],[60])).
cnf(62,plain,
( hates(butler,X1)
| ~ hates(agatha,X1) ),
inference(split_conjunct,[status(thm)],[61])).
fof(63,plain,(
! [X3] :
? [X4] : ~ hates(X3,X4) ),
inference(variable_rename,[status(thm)],[33])).
fof(64,plain,(
! [X3] : ~ hates(X3,esk2_1(X3)) ),
inference(skolemize,[status(esa)],[63])).
cnf(65,plain,
( ~ hates(X1,esk2_1(X1)) ),
inference(split_conjunct,[status(thm)],[64])).
cnf(66,plain,
( agatha != butler ),
inference(split_conjunct,[status(thm)],[28])).
cnf(67,negated_conjecture,
( ~ killed(agatha,agatha) ),
inference(split_conjunct,[status(thm)],[34])).
cnf(68,plain,
( hates(esk1_0,agatha) ),
inference(spm,[status(thm)],[47,37,theory(equality)])).
cnf(70,plain,
( agatha = esk1_0
| butler = esk1_0
| charles = esk1_0 ),
inference(spm,[status(thm)],[44,38,theory(equality)])).
cnf(71,plain,
( hates(butler,X1)
| ~ killed(X1,agatha) ),
inference(spm,[status(thm)],[50,59,theory(equality)])).
cnf(72,plain,
( hates(butler,X1)
| butler = X1 ),
inference(spm,[status(thm)],[62,56,theory(equality)])).
cnf(73,plain,
( butler = X1
| ~ hates(charles,X1) ),
inference(spm,[status(thm)],[53,56,theory(equality)])).
cnf(77,plain,
( killed(esk1_0,esk1_0)
| esk1_0 = charles
| esk1_0 = butler ),
inference(spm,[status(thm)],[37,70,theory(equality)])).
cnf(79,negated_conjecture,
( esk1_0 = charles
| esk1_0 = butler
| ~ killed(esk1_0,esk1_0) ),
inference(spm,[status(thm)],[67,70,theory(equality)])).
cnf(86,plain,
( butler = esk2_1(butler) ),
inference(spm,[status(thm)],[65,72,theory(equality)])).
cnf(89,plain,
( hates(butler,esk1_0) ),
inference(spm,[status(thm)],[71,37,theory(equality)])).
cnf(90,plain,
( ~ hates(butler,butler) ),
inference(spm,[status(thm)],[65,86,theory(equality)])).
cnf(92,negated_conjecture,
( esk1_0 = charles
| esk1_0 = butler ),
inference(csr,[status(thm)],[79,77])).
cnf(96,negated_conjecture,
( hates(charles,agatha)
| esk1_0 = butler ),
inference(spm,[status(thm)],[68,92,theory(equality)])).
cnf(107,negated_conjecture,
( butler = agatha
| esk1_0 = butler ),
inference(spm,[status(thm)],[73,96,theory(equality)])).
cnf(108,negated_conjecture,
( esk1_0 = butler ),
inference(sr,[status(thm)],[107,66,theory(equality)])).
cnf(109,plain,
( hates(butler,butler) ),
inference(rw,[status(thm)],[89,108,theory(equality)])).
cnf(110,plain,
( $false ),
inference(sr,[status(thm)],[109,90,theory(equality)])).
cnf(111,plain,
( $false ),
110,
[proof]).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% # Preprocessing time : 0.012 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(16, axiom,?[X1]:(lives(X1)&killed(X1,agatha)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_1)).
% fof(20, axiom,![X1]:(lives(X1)=>((X1=agatha|X1=butler)|X1=charles)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_3)).
% fof(21, axiom,![X1]:![X2]:(killed(X1,X2)=>hates(X1,X2)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_4)).
% fof(22, axiom,![X1]:![X2]:(killed(X1,X2)=>~(richer(X1,X2))),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_5)).
% fof(23, axiom,![X1]:(hates(agatha,X1)=>~(hates(charles,X1))),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_6)).
% fof(24, axiom,![X1]:(~(X1=butler)=>hates(agatha,X1)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_7)).
% fof(25, axiom,![X1]:(~(richer(X1,agatha))=>hates(butler,X1)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_8)).
% fof(26, axiom,![X1]:(hates(agatha,X1)=>hates(butler,X1)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_9)).
% fof(27, axiom,![X1]:?[X2]:~(hates(X1,X2)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_10)).
% fof(28, axiom,~(agatha=butler),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55_11)).
% fof(29, negated_conjecture,~(killed(agatha,agatha)),file('/home/graph/tptp/TPTP/Problems/PUZ/PUZ001+1.p', pel55)).
% fof(30, plain,![X1]:![X2]:(killed(X1,X2)=>~(richer(X1,X2))),inference(fof_simplification,[status(thm)],[22,theory(equality)])).
% fof(31, plain,![X1]:(hates(agatha,X1)=>~(hates(charles,X1))),inference(fof_simplification,[status(thm)],[23,theory(equality)])).
% fof(32, plain,![X1]:(~(richer(X1,agatha))=>hates(butler,X1)),inference(fof_simplification,[status(thm)],[25,theory(equality)])).
% fof(33, plain,![X1]:?[X2]:~(hates(X1,X2)),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(34, negated_conjecture,~(killed(agatha,agatha)),inference(fof_simplification,[status(thm)],[29,theory(equality)])).
% fof(35, plain,?[X2]:(lives(X2)&killed(X2,agatha)),inference(variable_rename,[status(thm)],[16])).
% fof(36, plain,(lives(esk1_0)&killed(esk1_0,agatha)),inference(skolemize,[status(esa)],[35])).
% cnf(37,plain,(killed(esk1_0,agatha)),inference(split_conjunct,[status(thm)],[36])).
% cnf(38,plain,(lives(esk1_0)),inference(split_conjunct,[status(thm)],[36])).
% fof(42, plain,![X1]:(~(lives(X1))|((X1=agatha|X1=butler)|X1=charles)),inference(fof_nnf,[status(thm)],[20])).
% fof(43, plain,![X2]:(~(lives(X2))|((X2=agatha|X2=butler)|X2=charles)),inference(variable_rename,[status(thm)],[42])).
% cnf(44,plain,(X1=charles|X1=butler|X1=agatha|~lives(X1)),inference(split_conjunct,[status(thm)],[43])).
% fof(45, plain,![X1]:![X2]:(~(killed(X1,X2))|hates(X1,X2)),inference(fof_nnf,[status(thm)],[21])).
% fof(46, plain,![X3]:![X4]:(~(killed(X3,X4))|hates(X3,X4)),inference(variable_rename,[status(thm)],[45])).
% cnf(47,plain,(hates(X1,X2)|~killed(X1,X2)),inference(split_conjunct,[status(thm)],[46])).
% fof(48, plain,![X1]:![X2]:(~(killed(X1,X2))|~(richer(X1,X2))),inference(fof_nnf,[status(thm)],[30])).
% fof(49, plain,![X3]:![X4]:(~(killed(X3,X4))|~(richer(X3,X4))),inference(variable_rename,[status(thm)],[48])).
% cnf(50,plain,(~richer(X1,X2)|~killed(X1,X2)),inference(split_conjunct,[status(thm)],[49])).
% fof(51, plain,![X1]:(~(hates(agatha,X1))|~(hates(charles,X1))),inference(fof_nnf,[status(thm)],[31])).
% fof(52, plain,![X2]:(~(hates(agatha,X2))|~(hates(charles,X2))),inference(variable_rename,[status(thm)],[51])).
% cnf(53,plain,(~hates(charles,X1)|~hates(agatha,X1)),inference(split_conjunct,[status(thm)],[52])).
% fof(54, plain,![X1]:(X1=butler|hates(agatha,X1)),inference(fof_nnf,[status(thm)],[24])).
% fof(55, plain,![X2]:(X2=butler|hates(agatha,X2)),inference(variable_rename,[status(thm)],[54])).
% cnf(56,plain,(hates(agatha,X1)|X1=butler),inference(split_conjunct,[status(thm)],[55])).
% fof(57, plain,![X1]:(richer(X1,agatha)|hates(butler,X1)),inference(fof_nnf,[status(thm)],[32])).
% fof(58, plain,![X2]:(richer(X2,agatha)|hates(butler,X2)),inference(variable_rename,[status(thm)],[57])).
% cnf(59,plain,(hates(butler,X1)|richer(X1,agatha)),inference(split_conjunct,[status(thm)],[58])).
% fof(60, plain,![X1]:(~(hates(agatha,X1))|hates(butler,X1)),inference(fof_nnf,[status(thm)],[26])).
% fof(61, plain,![X2]:(~(hates(agatha,X2))|hates(butler,X2)),inference(variable_rename,[status(thm)],[60])).
% cnf(62,plain,(hates(butler,X1)|~hates(agatha,X1)),inference(split_conjunct,[status(thm)],[61])).
% fof(63, plain,![X3]:?[X4]:~(hates(X3,X4)),inference(variable_rename,[status(thm)],[33])).
% fof(64, plain,![X3]:~(hates(X3,esk2_1(X3))),inference(skolemize,[status(esa)],[63])).
% cnf(65,plain,(~hates(X1,esk2_1(X1))),inference(split_conjunct,[status(thm)],[64])).
% cnf(66,plain,(agatha!=butler),inference(split_conjunct,[status(thm)],[28])).
% cnf(67,negated_conjecture,(~killed(agatha,agatha)),inference(split_conjunct,[status(thm)],[34])).
% cnf(68,plain,(hates(esk1_0,agatha)),inference(spm,[status(thm)],[47,37,theory(equality)])).
% cnf(70,plain,(agatha=esk1_0|butler=esk1_0|charles=esk1_0),inference(spm,[status(thm)],[44,38,theory(equality)])).
% cnf(71,plain,(hates(butler,X1)|~killed(X1,agatha)),inference(spm,[status(thm)],[50,59,theory(equality)])).
% cnf(72,plain,(hates(butler,X1)|butler=X1),inference(spm,[status(thm)],[62,56,theory(equality)])).
% cnf(73,plain,(butler=X1|~hates(charles,X1)),inference(spm,[status(thm)],[53,56,theory(equality)])).
% cnf(77,plain,(killed(esk1_0,esk1_0)|esk1_0=charles|esk1_0=butler),inference(spm,[status(thm)],[37,70,theory(equality)])).
% cnf(79,negated_conjecture,(esk1_0=charles|esk1_0=butler|~killed(esk1_0,esk1_0)),inference(spm,[status(thm)],[67,70,theory(equality)])).
% cnf(86,plain,(butler=esk2_1(butler)),inference(spm,[status(thm)],[65,72,theory(equality)])).
% cnf(89,plain,(hates(butler,esk1_0)),inference(spm,[status(thm)],[71,37,theory(equality)])).
% cnf(90,plain,(~hates(butler,butler)),inference(spm,[status(thm)],[65,86,theory(equality)])).
% cnf(92,negated_conjecture,(esk1_0=charles|esk1_0=butler),inference(csr,[status(thm)],[79,77])).
% cnf(96,negated_conjecture,(hates(charles,agatha)|esk1_0=butler),inference(spm,[status(thm)],[68,92,theory(equality)])).
% cnf(107,negated_conjecture,(butler=agatha|esk1_0=butler),inference(spm,[status(thm)],[73,96,theory(equality)])).
% cnf(108,negated_conjecture,(esk1_0=butler),inference(sr,[status(thm)],[107,66,theory(equality)])).
% cnf(109,plain,(hates(butler,butler)),inference(rw,[status(thm)],[89,108,theory(equality)])).
% cnf(110,plain,($false),inference(sr,[status(thm)],[109,90,theory(equality)])).
% cnf(111,plain,($false),110,['proof']).
% # SZS output end CNFRefutation
% # Initial clauses : 15
% # Removed in clause preprocessing : 0
% # Initial clauses in saturation : 15
% # Processed clauses : 46
% # ...of these trivial : 0
% # ...subsumed : 0
% # ...remaining for further processing : 46
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 3
% # Backward-rewritten : 7
% # Generated clauses : 35
% # ...of the previous two non-trivial : 31
% # Contextual simplify-reflections : 1
% # Paramodulations : 34
% # Factorizations : 1
% # Equation resolutions : 0
% # Current number of processed clauses : 21
% # Positive orientable unit clauses : 6
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 5
% # Non-unit-clauses : 10
% # Current number of unprocessed clauses: 0
% # ...number of literals in the above : 0
% # Clause-clause subsumption calls (NU) : 11
% # Rec. Clause-clause subsumption calls : 11
% # Unit Clause-clause subsumption calls : 5
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
%
% # -------------------------------------------------
% # User time : 0.011 s
% # System time : 0.004 s
% # Total time : 0.015 s
% # Maximum resident set size: 0 pages
%
%
%------------------------------------------------------------------------------