%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : PUZ001+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:21:30 AM UTC 2026
% Result : Theorem 10.34s 1.80s
% Output : CNFRefutation 10.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 2
% Syntax : Number of formulae : 36 ( 18 unt; 0 def)
% Number of atoms : 100 ( 34 equ)
% Maximal formula atoms : 37 ( 2 avg)
% Number of connectives : 92 ( 28 ~; 30 |; 24 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 4 usr; 2 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 13 con; 0-2 aty)
% Number of variables : 61 ( 13 sgn 14 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(background,axiom,
? [X0,X1,X2] :
( '\'AuntAgatha\'' != '\'Butler\''
& ! [X25] :
( $true
=> ~ ! [X26] :
( $true
=> ? [X27] : predicate2(X27,hate,X25,X26) ) )
& ! [X22,X23] :
( ( predicate2(X23,hate,'\'AuntAgatha\'',X22)
& $true )
=> ? [X24] : predicate2(X24,hate,'\'Butler\'',X22) )
& ! [X19] :
( ( ~ ? [X20] :
( X19 = X20
& property2(X20,rich,'comp$uthan','\'AuntAgatha\'') )
& $true )
=> ? [X21] : predicate2(X21,hate,'\'Butler\'',X19) )
& ! [X17] :
( ( X17 != '\'Butler\''
& $true )
=> ? [X18] : predicate2(X18,hate,'\'AuntAgatha\'',X17) )
& ~ ? [X16] : predicate2(X16,hate,'\'AuntAgatha\'','\'Butler\'')
& ! [X13,X14] :
( ( predicate2(X14,hate,'\'AuntAgatha\'',X13)
& $true )
=> ~ ? [X15] : predicate2(X15,hate,'\'Charles\'',X13) )
& ! [X9] :
( $true
=> ~ ? [X10,X11,X12] :
( X9 = X12
& property2(X12,rich,'comp$uthan',X10)
& predicate2(X11,kill,X9,X10)
& $true ) )
& ! [X5] :
( $true
=> ! [X6,X7] :
( ( predicate2(X7,kill,X5,X6)
& $true )
=> ? [X8] : predicate2(X8,hate,X5,X6) ) )
& ! [X3,X4] :
( ( 'modifier$upp'(X4,in,'\'DreadburyMansion\'')
& predicate1(X4,live,X3)
& $true )
=> ( X3 = '\'Charles\''
| X3 = '\'Butler\''
| X3 = '\'AuntAgatha\'' ) )
& predicate2(X2,kill,X0,'\'AuntAgatha\'')
& 'modifier$upp'(X1,in,'\'DreadburyMansion\'')
& predicate1(X1,live,X0)
& $true ) ).
fof(prove,conjecture,
? [X0] : predicate2(X0,kill,'\'AuntAgatha\'','\'AuntAgatha\'') ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0] : predicate2(X0,kill,'\'AuntAgatha\'','\'AuntAgatha\''),
inference(negate_conjecture,[status(cth)],[prove]) ).
cnf(c0,plain,
predicate1(sK1,live,sK0),
inference(clausification,[status(esa)],[background]) ).
cnf(c1,plain,
'modifier$upp'(sK1,in,'\'DreadburyMansion\''),
inference(clausification,[status(esa)],[background]) ).
cnf(c2,plain,
predicate2(sK2,kill,sK0,'\'AuntAgatha\''),
inference(clausification,[status(esa)],[background]) ).
cnf(c3,plain,
( ~ predicate1(X0,live,X1)
| X1 = '\'AuntAgatha\''
| X1 = '\'Butler\''
| X1 = '\'Charles\''
| ~ 'modifier$upp'(X0,in,'\'DreadburyMansion\'') ),
inference(clausification,[status(esa)],[background]) ).
cnf(c4,plain,
( predicate2(sK8(X1,X2),hate,X1,X2)
| ~ predicate2(X0,kill,X1,X2) ),
inference(clausification,[status(esa)],[background]) ).
cnf(c5,plain,
( X1 != X3
| ~ property2(X3,rich,'comp$uthan',X2)
| ~ predicate2(X0,kill,X1,X2) ),
inference(clausification,[status(esa)],[background]) ).
cnf(c6,plain,
( ~ predicate2(X2,hate,'\'Charles\'',X1)
| ~ predicate2(X0,hate,'\'AuntAgatha\'',X1) ),
inference(clausification,[status(esa)],[background]) ).
cnf(c8,plain,
( predicate2(sK18(X0),hate,'\'AuntAgatha\'',X0)
| X0 = '\'Butler\'' ),
inference(clausification,[status(esa)],[background]) ).
cnf(c9,plain,
( predicate2(sK21(X0),hate,'\'Butler\'',X0)
| property2(sK20(X0),rich,'comp$uthan','\'AuntAgatha\'') ),
inference(clausification,[status(esa)],[background]) ).
cnf(c10,plain,
( predicate2(sK21(X0),hate,'\'Butler\'',X0)
| X0 = sK20(X0) ),
inference(clausification,[status(esa)],[background]) ).
cnf(c11,plain,
( predicate2(sK24(X1),hate,'\'Butler\'',X1)
| ~ predicate2(X0,hate,'\'AuntAgatha\'',X1) ),
inference(clausification,[status(esa)],[background]) ).
cnf(c12,plain,
~ predicate2(X0,hate,X1,sK26(X1)),
inference(clausification,[status(esa)],[background]) ).
cnf(c13,plain,
'\'AuntAgatha\'' != '\'Butler\'',
inference(clausification,[status(esa)],[background]) ).
cnf(c14,plain,
~ predicate2(X0,kill,'\'AuntAgatha\'','\'AuntAgatha\''),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
predicate2(sK8(sK0,'\'AuntAgatha\''),hate,sK0,'\'AuntAgatha\''),
inference(resolution,[status(thm)],[c4,c2]) ).
cnf(d1,plain,
( ~ predicate1(sK1,live,X0)
| X0 = '\'Charles\''
| X0 = '\'Butler\''
| X0 = '\'AuntAgatha\'' ),
inference(resolution,[status(thm)],[c3,c1]) ).
cnf(d2,plain,
( sK0 = '\'Charles\''
| sK0 = '\'Butler\''
| sK0 = '\'AuntAgatha\'' ),
inference(resolution,[status(thm)],[d1,c0]) ).
cnf(d3,plain,
( sK0 = '\'Butler\''
| sK0 = '\'AuntAgatha\''
| ~ predicate2(X2,hate,'\'AuntAgatha\'',X1)
| ~ predicate2(X0,hate,sK0,X1) ),
inference(superposition,[status(thm)],[d2,c6]) ).
cnf(d4,plain,
( ~ predicate2(X0,hate,'\'AuntAgatha\'','\'AuntAgatha\'')
| sK0 = '\'Butler\''
| sK0 = '\'AuntAgatha\'' ),
inference(resolution,[status(thm)],[d3,d0]) ).
cnf(d5,plain,
( '\'AuntAgatha\'' = '\'Butler\''
| sK0 = '\'Butler\''
| sK0 = '\'AuntAgatha\'' ),
inference(resolution,[status(thm)],[d4,c8]) ).
cnf(d6,plain,
( sK0 = '\'Butler\''
| sK0 = '\'AuntAgatha\'' ),
inference(resolution,[status(thm)],[c13,d5]) ).
cnf(d7,plain,
( sK0 = '\'AuntAgatha\''
| predicate2(sK2,kill,'\'Butler\'','\'AuntAgatha\'') ),
inference(superposition,[status(thm)],[d6,c2]) ).
cnf(d8,plain,
( X0 = '\'Butler\''
| predicate2(sK24(X0),hate,'\'Butler\'',X0) ),
inference(resolution,[status(thm)],[c11,c8]) ).
cnf(d9,plain,
sK26('\'Butler\'') = '\'Butler\'',
inference(resolution,[status(thm)],[d8,c12]) ).
cnf(d10,plain,
sK26('\'Butler\'') = sK20(sK26('\'Butler\'')),
inference(resolution,[status(thm)],[c10,c12]) ).
cnf(d11,plain,
property2(sK20(sK26('\'Butler\'')),rich,'comp$uthan','\'AuntAgatha\''),
inference(resolution,[status(thm)],[c9,c12]) ).
cnf(d12,plain,
property2(sK26('\'Butler\''),rich,'comp$uthan','\'AuntAgatha\''),
inference(demodulation,[status(thm)],[d11,d10]) ).
cnf(d13,plain,
( ~ property2(X1,rich,'comp$uthan',X2)
| ~ predicate2(X0,kill,X1,X2) ),
inference(equality_resolution,[status(thm)],[c5]) ).
cnf(d14,plain,
~ predicate2(X0,kill,sK26('\'Butler\''),'\'AuntAgatha\''),
inference(resolution,[status(thm)],[d13,d12]) ).
cnf(d15,plain,
~ predicate2(X0,kill,'\'Butler\'','\'AuntAgatha\''),
inference(demodulation,[status(thm)],[d14,d9]) ).
cnf(d16,plain,
sK0 = '\'AuntAgatha\'',
inference(resolution,[status(thm)],[d15,d7]) ).
cnf(d17,plain,
predicate2(sK2,kill,'\'AuntAgatha\'','\'AuntAgatha\''),
inference(demodulation,[status(thm)],[c2,d16]) ).
cnf(d18,plain,
$false,
inference(resolution,[status(thm)],[c14,d17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ001+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 05:02:36 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.34/1.80 % SZS status Theorem for theBenchmark.p
% 10.34/1.80 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------