%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ001+1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:37:32 EDT 2024
% Result : Theorem 1.55s 1.72s
% Output : Refutation 1.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 15
% Syntax : Number of formulae : 72 ( 24 unt; 0 def)
% Number of atoms : 139 ( 45 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 125 ( 58 ~; 54 |; 3 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-1 aty)
% Number of variables : 73 ( 0 sgn 35 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(pel55_11,axiom,
agatha != butler,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_11) ).
cnf(c7,plain,
agatha != butler,
inference(split_conjunct,[status(thm)],[pel55_11]) ).
fof(pel55_7,axiom,
! [X] :
( X != butler
=> hates(agatha,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_7) ).
fof(c19,plain,
! [X] :
( X = butler
| hates(agatha,X) ),
inference(fof_nnf,[status(thm)],[pel55_7]) ).
fof(c20,plain,
! [X6] :
( X6 = butler
| hates(agatha,X6) ),
inference(variable_rename,[status(thm)],[c19]) ).
cnf(c21,plain,
( X38 = butler
| hates(agatha,X38) ),
inference(split_conjunct,[status(thm)],[c20]) ).
cnf(c55,plain,
hates(agatha,agatha),
inference(resolution,[status(thm)],[c21,c7]) ).
fof(pel55_6,axiom,
! [X] :
( hates(agatha,X)
=> ~ hates(charles,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_6) ).
fof(c22,plain,
! [X] :
( hates(agatha,X)
=> ~ hates(charles,X) ),
inference(fof_simplification,[status(thm)],[pel55_6]) ).
fof(c23,plain,
! [X] :
( ~ hates(agatha,X)
| ~ hates(charles,X) ),
inference(fof_nnf,[status(thm)],[c22]) ).
fof(c24,plain,
! [X7] :
( ~ hates(agatha,X7)
| ~ hates(charles,X7) ),
inference(variable_rename,[status(thm)],[c23]) ).
cnf(c25,plain,
( ~ hates(agatha,X43)
| ~ hates(charles,X43) ),
inference(split_conjunct,[status(thm)],[c24]) ).
cnf(reflexivity,axiom,
X14 = X14,
theory(equality) ).
fof(pel55_1,axiom,
? [X] :
( lives(X)
& killed(X,agatha) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_1) ).
fof(c39,plain,
? [X13] :
( lives(X13)
& killed(X13,agatha) ),
inference(variable_rename,[status(thm)],[pel55_1]) ).
fof(c40,plain,
( lives(skolem0002)
& killed(skolem0002,agatha) ),
inference(skolemize,[status(esa)],[c39]) ).
cnf(c42,plain,
killed(skolem0002,agatha),
inference(split_conjunct,[status(thm)],[c40]) ).
fof(pel55_4,axiom,
! [X,Y] :
( killed(X,Y)
=> hates(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_4) ).
fof(c30,plain,
! [X,Y] :
( ~ killed(X,Y)
| hates(X,Y) ),
inference(fof_nnf,[status(thm)],[pel55_4]) ).
fof(c31,plain,
! [X10,X11] :
( ~ killed(X10,X11)
| hates(X10,X11) ),
inference(variable_rename,[status(thm)],[c30]) ).
cnf(c32,plain,
( ~ killed(X24,X25)
| hates(X24,X25) ),
inference(split_conjunct,[status(thm)],[c31]) ).
cnf(c46,plain,
hates(skolem0002,agatha),
inference(resolution,[status(thm)],[c32,c42]) ).
cnf(c2,axiom,
( X42 != X40
| X41 != X39
| ~ hates(X42,X41)
| hates(X40,X39) ),
theory(equality) ).
cnf(c65,plain,
( skolem0002 != X66
| agatha != X67
| hates(X66,X67) ),
inference(resolution,[status(thm)],[c2,c46]) ).
cnf(c132,plain,
( skolem0002 != X68
| hates(X68,agatha) ),
inference(resolution,[status(thm)],[c65,reflexivity]) ).
fof(pel55_5,axiom,
! [X,Y] :
( killed(X,Y)
=> ~ richer(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_5) ).
fof(c26,plain,
! [X,Y] :
( killed(X,Y)
=> ~ richer(X,Y) ),
inference(fof_simplification,[status(thm)],[pel55_5]) ).
fof(c27,plain,
! [X,Y] :
( ~ killed(X,Y)
| ~ richer(X,Y) ),
inference(fof_nnf,[status(thm)],[c26]) ).
fof(c28,plain,
! [X8,X9] :
( ~ killed(X8,X9)
| ~ richer(X8,X9) ),
inference(variable_rename,[status(thm)],[c27]) ).
cnf(c29,plain,
( ~ killed(X22,X23)
| ~ richer(X22,X23) ),
inference(split_conjunct,[status(thm)],[c28]) ).
fof(pel55_10,axiom,
! [X] :
? [Y] : ~ hates(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_10) ).
fof(c8,plain,
! [X] :
? [Y] : ~ hates(X,Y),
inference(fof_simplification,[status(thm)],[pel55_10]) ).
fof(c9,plain,
! [X2] :
? [X3] : ~ hates(X2,X3),
inference(variable_rename,[status(thm)],[c8]) ).
fof(c10,plain,
! [X2] : ~ hates(X2,skolem0001(X2)),
inference(skolemize,[status(esa)],[c9]) ).
cnf(c11,plain,
~ hates(X18,skolem0001(X18)),
inference(split_conjunct,[status(thm)],[c10]) ).
fof(pel55_9,axiom,
! [X] :
( hates(agatha,X)
=> hates(butler,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_9) ).
fof(c12,plain,
! [X] :
( ~ hates(agatha,X)
| hates(butler,X) ),
inference(fof_nnf,[status(thm)],[pel55_9]) ).
fof(c13,plain,
! [X4] :
( ~ hates(agatha,X4)
| hates(butler,X4) ),
inference(variable_rename,[status(thm)],[c12]) ).
cnf(c14,plain,
( ~ hates(agatha,X32)
| hates(butler,X32) ),
inference(split_conjunct,[status(thm)],[c13]) ).
cnf(c56,plain,
( X50 = butler
| hates(butler,X50) ),
inference(resolution,[status(thm)],[c21,c14]) ).
cnf(c85,plain,
skolem0001(butler) = butler,
inference(resolution,[status(thm)],[c56,c11]) ).
fof(pel55_8,axiom,
! [X] :
( ~ richer(X,agatha)
=> hates(butler,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_8) ).
fof(c15,plain,
! [X] :
( ~ richer(X,agatha)
=> hates(butler,X) ),
inference(fof_simplification,[status(thm)],[pel55_8]) ).
fof(c16,plain,
! [X] :
( richer(X,agatha)
| hates(butler,X) ),
inference(fof_nnf,[status(thm)],[c15]) ).
fof(c17,plain,
! [X5] :
( richer(X5,agatha)
| hates(butler,X5) ),
inference(variable_rename,[status(thm)],[c16]) ).
cnf(c18,plain,
( richer(X33,agatha)
| hates(butler,X33) ),
inference(split_conjunct,[status(thm)],[c17]) ).
cnf(c49,plain,
richer(skolem0001(butler),agatha),
inference(resolution,[status(thm)],[c18,c11]) ).
cnf(c3,axiom,
( X49 != X47
| X48 != X46
| ~ richer(X49,X48)
| richer(X47,X46) ),
theory(equality) ).
cnf(c79,plain,
( skolem0001(butler) != X107
| agatha != X106
| richer(X107,X106) ),
inference(resolution,[status(thm)],[c3,c49]) ).
cnf(c271,plain,
( agatha != X108
| richer(butler,X108) ),
inference(resolution,[status(thm)],[c79,c85]) ).
cnf(c276,plain,
richer(butler,agatha),
inference(resolution,[status(thm)],[c271,reflexivity]) ).
cnf(c278,plain,
~ killed(butler,agatha),
inference(resolution,[status(thm)],[c276,c29]) ).
cnf(c1,axiom,
( X37 != X35
| X36 != X34
| ~ killed(X37,X36)
| killed(X35,X34) ),
theory(equality) ).
cnf(c51,plain,
( skolem0002 != X53
| agatha != X54
| killed(X53,X54) ),
inference(resolution,[status(thm)],[c1,c42]) ).
cnf(c104,plain,
( skolem0002 != X59
| killed(X59,agatha) ),
inference(resolution,[status(thm)],[c51,reflexivity]) ).
fof(pel55,conjecture,
killed(agatha,agatha),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55) ).
fof(c4,negated_conjecture,
~ killed(agatha,agatha),
inference(assume_negation,[status(cth)],[pel55]) ).
fof(c5,negated_conjecture,
~ killed(agatha,agatha),
inference(fof_simplification,[status(thm)],[c4]) ).
cnf(c6,negated_conjecture,
~ killed(agatha,agatha),
inference(split_conjunct,[status(thm)],[c5]) ).
cnf(c41,plain,
lives(skolem0002),
inference(split_conjunct,[status(thm)],[c40]) ).
fof(pel55_3,axiom,
! [X] :
( lives(X)
=> ( X = agatha
| X = butler
| X = charles ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel55_3) ).
fof(c33,plain,
! [X] :
( ~ lives(X)
| X = agatha
| X = butler
| X = charles ),
inference(fof_nnf,[status(thm)],[pel55_3]) ).
fof(c34,plain,
! [X12] :
( ~ lives(X12)
| X12 = agatha
| X12 = butler
| X12 = charles ),
inference(variable_rename,[status(thm)],[c33]) ).
cnf(c35,plain,
( ~ lives(X51)
| X51 = agatha
| X51 = butler
| X51 = charles ),
inference(split_conjunct,[status(thm)],[c34]) ).
cnf(c92,plain,
( skolem0002 = agatha
| skolem0002 = butler
| skolem0002 = charles ),
inference(resolution,[status(thm)],[c35,c41]) ).
cnf(c340,plain,
( skolem0002 = butler
| skolem0002 = charles
| killed(agatha,agatha) ),
inference(resolution,[status(thm)],[c92,c104]) ).
cnf(c3715,plain,
( skolem0002 = butler
| skolem0002 = charles ),
inference(resolution,[status(thm)],[c340,c6]) ).
cnf(c3735,plain,
( skolem0002 = charles
| killed(butler,agatha) ),
inference(resolution,[status(thm)],[c3715,c104]) ).
cnf(c3822,plain,
skolem0002 = charles,
inference(resolution,[status(thm)],[c3735,c278]) ).
cnf(c3847,plain,
hates(charles,agatha),
inference(resolution,[status(thm)],[c3822,c132]) ).
cnf(c3886,plain,
~ hates(agatha,agatha),
inference(resolution,[status(thm)],[c3847,c25]) ).
cnf(c3918,plain,
$false,
inference(resolution,[status(thm)],[c3886,c55]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : PUZ001+1 : TPTP v8.1.2. Released v2.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n002.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 20:38:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 1.55/1.72 % Version: 1.5
% 1.55/1.72 % SZS status Theorem
% 1.55/1.72 % SZS output start CNFRefutation
% See solution above
% 1.55/1.72
% 1.55/1.72 % Initial clauses : 22
% 1.55/1.72 % Processed clauses : 277
% 1.55/1.72 % Factors computed : 32
% 1.55/1.72 % Resolvents computed: 3855
% 1.55/1.72 % Tautologies deleted: 4
% 1.55/1.72 % Forward subsumed : 601
% 1.55/1.72 % Backward subsumed : 12
% 1.55/1.72 % -------- CPU Time ---------
% 1.55/1.72 % User time : 1.332 s
% 1.55/1.72 % System time : 0.027 s
% 1.55/1.72 % Total time : 1.359 s
%------------------------------------------------------------------------------