%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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 : Fri Sep 25 02:14:57 PM UTC 2026
% Result : Theorem 4.25s 1.11s
% Output : Proof 4.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 10
% Syntax : Number of formulae : 54 ( 14 unt; 0 def)
% Number of atoms : 278 ( 5 equ)
% Maximal formula atoms : 48 ( 5 avg)
% Number of connectives : 269 ( 45 ~; 37 |; 168 &)
% ( 0 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 52 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 1 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 145 ( 2 sgn 80 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f70,axiom,
! [U,V,W,X] :
( be(U,V,W,X)
=> W = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax71) ).
fof(f70_nnf,plain,
! [U,V,W,X] :
( W = X
| ~ be(U,V,W,X) ),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
! [U,V,W,X] :
( W = X
| ~ be(U,V,W,X) ),
inference(skolemisation,[status(esa)],[f70_nnf]) ).
cnf(c76,plain,
( X2 = X3
| ~ be(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
fof(f71,conjecture,
~ ? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :
( behind(U,X6,X6)
& be(U,X5,V,X6)
& state(U,X5)
& wheel(U,X6)
& ! [X14] :
( member(U,X14,X4)
=> ( cheap(U,X14)
& black(U,X14)
& coat(U,X14) ) )
& group(U,X4)
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( wear(U,X13)
& nonreflexive(U,X13)
& present(U,X13)
& patient(U,X13,X11)
& agent(U,X13,X12)
& event(U,X13) ) ) )
& ! [X10] :
( member(U,X10,X3)
=> ( young(U,X10)
& fellow(U,X10) ) )
& group(U,X3)
& two(U,X3)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( in(U,X9,X)
& be(U,X8,X7,X9)
& state(U,X8) ) )
& in(U,X2,X1)
& down(U,X2,X1)
& barrel(U,X2)
& present(U,X2)
& agent(U,X2,Y)
& event(U,X2)
& lonely(U,X1)
& street(U,X1)
& placename(U,Z)
& hollywood_placename(U,Z)
& city(U,X1)
& of(U,Z,X1)
& old(U,Y)
& dirty(U,Y)
& white(U,Y)
& chevy(U,Y)
& frontseat(U,X)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f71_neg,negated_conjecture,
~ ~ ? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :
( behind(U,X6,X6)
& be(U,X5,V,X6)
& state(U,X5)
& wheel(U,X6)
& ! [X14] :
( member(U,X14,X4)
=> ( cheap(U,X14)
& black(U,X14)
& coat(U,X14) ) )
& group(U,X4)
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( wear(U,X13)
& nonreflexive(U,X13)
& present(U,X13)
& patient(U,X13,X11)
& agent(U,X13,X12)
& event(U,X13) ) ) )
& ! [X10] :
( member(U,X10,X3)
=> ( young(U,X10)
& fellow(U,X10) ) )
& group(U,X3)
& two(U,X3)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( in(U,X9,X)
& be(U,X8,X7,X9)
& state(U,X8) ) )
& in(U,X2,X1)
& down(U,X2,X1)
& barrel(U,X2)
& present(U,X2)
& agent(U,X2,Y)
& event(U,X2)
& lonely(U,X1)
& street(U,X1)
& placename(U,Z)
& hollywood_placename(U,Z)
& city(U,X1)
& of(U,Z,X1)
& old(U,Y)
& dirty(U,Y)
& white(U,Y)
& chevy(U,Y)
& frontseat(U,X)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
inference(negated_conjecture,[status(cth)],[f71]) ).
fof(f71_nnf,plain,
? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :
( behind(U,X6,X6)
& be(U,X5,V,X6)
& state(U,X5)
& wheel(U,X6)
& ! [X14] :
( ( cheap(U,X14)
& black(U,X14)
& coat(U,X14) )
| ~ member(U,X14,X4) )
& group(U,X4)
& ! [X11] :
( ! [X12] :
( ? [X13] :
( wear(U,X13)
& nonreflexive(U,X13)
& present(U,X13)
& patient(U,X13,X11)
& agent(U,X13,X12)
& event(U,X13) )
| ~ member(U,X12,X3) )
| ~ member(U,X11,X4) )
& ! [X10] :
( ( young(U,X10)
& fellow(U,X10) )
| ~ member(U,X10,X3) )
& group(U,X3)
& two(U,X3)
& ! [X7] :
( ? [X8,X9] :
( in(U,X9,X)
& be(U,X8,X7,X9)
& state(U,X8) )
| ~ member(U,X7,X3) )
& in(U,X2,X1)
& down(U,X2,X1)
& barrel(U,X2)
& present(U,X2)
& agent(U,X2,Y)
& event(U,X2)
& lonely(U,X1)
& street(U,X1)
& placename(U,Z)
& hollywood_placename(U,Z)
& city(U,X1)
& of(U,Z,X1)
& old(U,Y)
& dirty(U,Y)
& white(U,Y)
& chevy(U,Y)
& frontseat(U,X)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
inference(nnf_transformation,[status(thm)],[f71_neg]) ).
fof(f71_sk,plain,
! [X7,X10,X11,X12,X14] :
( behind(sk3,sk14,sk14)
& be(sk3,sk13,sk4,sk14)
& state(sk3,sk13)
& wheel(sk3,sk14)
& ( ( cheap(sk3,X14)
& black(sk3,X14)
& coat(sk3,X14) )
| ~ member(sk3,X14,sk12) )
& group(sk3,sk12)
& ( ( wear(sk3,sk17(X11,X12))
& nonreflexive(sk3,sk17(X11,X12))
& present(sk3,sk17(X11,X12))
& patient(sk3,sk17(X11,X12),X11)
& agent(sk3,sk17(X11,X12),X12)
& event(sk3,sk17(X11,X12)) )
| ~ member(sk3,X12,sk11)
| ~ member(sk3,X11,sk12) )
& ( ( young(sk3,X10)
& fellow(sk3,X10) )
| ~ member(sk3,X10,sk11) )
& group(sk3,sk11)
& two(sk3,sk11)
& ( ( in(sk3,sk16(X7),sk6)
& be(sk3,sk15(X7),X7,sk16(X7))
& state(sk3,sk15(X7)) )
| ~ member(sk3,X7,sk11) )
& in(sk3,sk10,sk9)
& down(sk3,sk10,sk9)
& barrel(sk3,sk10)
& present(sk3,sk10)
& agent(sk3,sk10,sk7)
& event(sk3,sk10)
& lonely(sk3,sk9)
& street(sk3,sk9)
& placename(sk3,sk8)
& hollywood_placename(sk3,sk8)
& city(sk3,sk9)
& of(sk3,sk8,sk9)
& old(sk3,sk7)
& dirty(sk3,sk7)
& white(sk3,sk7)
& chevy(sk3,sk7)
& frontseat(sk3,sk6)
& forename(sk3,sk5)
& jules_forename(sk3,sk5)
& man(sk3,sk4)
& of(sk3,sk5,sk4)
& actual_world(sk3) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,sk12,sk13,sk14,sk15,sk16,sk17])],[f71_nnf]) ).
cnf(c118,plain,
be(sk3,sk13,sk4,sk14),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(p312,plain,
sk4 = sk14,
inference(resolution,[status(thm)],[c76,c118]) ).
fof(f47,axiom,
! [U,V] :
( wheel(U,V)
=> device(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax48) ).
fof(f47_nnf,plain,
! [U,V] :
( device(U,V)
| ~ wheel(U,V) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [U,V] :
( device(U,V)
| ~ wheel(U,V) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( device(X0,X1)
| ~ wheel(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(c116,plain,
wheel(sk3,sk14),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(p179,plain,
device(sk3,sk14),
inference(resolution,[status(thm)],[c47,c116]) ).
fof(f46,axiom,
! [U,V] :
( device(U,V)
=> instrumentality(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax47) ).
fof(f46_nnf,plain,
! [U,V] :
( instrumentality(U,V)
| ~ device(U,V) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [U,V] :
( instrumentality(U,V)
| ~ device(U,V) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( instrumentality(X0,X1)
| ~ device(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p187,plain,
instrumentality(sk3,sk14),
inference(resolution,[status(thm)],[p179,c46]) ).
fof(f45,axiom,
! [U,V] :
( instrumentality(U,V)
=> artifact(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax46) ).
fof(f45_nnf,plain,
! [U,V] :
( artifact(U,V)
| ~ instrumentality(U,V) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [U,V] :
( artifact(U,V)
| ~ instrumentality(U,V) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( artifact(X0,X1)
| ~ instrumentality(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p190,plain,
artifact(sk3,sk14),
inference(resolution,[status(thm)],[p187,c45]) ).
fof(f44,axiom,
! [U,V] :
( artifact(U,V)
=> object(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax45) ).
fof(f44_nnf,plain,
! [U,V] :
( object(U,V)
| ~ artifact(U,V) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [U,V] :
( object(U,V)
| ~ artifact(U,V) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( object(X0,X1)
| ~ artifact(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p193,plain,
object(sk3,sk14),
inference(resolution,[status(thm)],[p190,c44]) ).
fof(f39,axiom,
! [U,V] :
( object(U,V)
=> nonliving(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax40) ).
fof(f39_nnf,plain,
! [U,V] :
( nonliving(U,V)
| ~ object(U,V) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [U,V] :
( nonliving(U,V)
| ~ object(U,V) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( nonliving(X0,X1)
| ~ object(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p200,plain,
nonliving(sk3,sk14),
inference(resolution,[status(thm)],[p193,c39]) ).
cnf(p322,plain,
nonliving(sk3,sk4),
inference(superposition,[status(thm)],[p312,p200]) ).
fof(f56,axiom,
! [U,V] :
( animate(U,V)
=> ~ nonliving(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax57) ).
fof(f56_nnf,plain,
! [U,V] :
( ~ nonliving(U,V)
| ~ animate(U,V) ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [U,V] :
( ~ nonliving(U,V)
| ~ animate(U,V) ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
( ~ nonliving(X0,X1)
| ~ animate(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
fof(f30,axiom,
! [U,V] :
( man(U,V)
=> human_person(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
fof(f30_nnf,plain,
! [U,V] :
( human_person(U,V)
| ~ man(U,V) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [U,V] :
( human_person(U,V)
| ~ man(U,V) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( human_person(X0,X1)
| ~ man(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(c79,plain,
man(sk3,sk4),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(p146,plain,
human_person(sk3,sk4),
inference(resolution,[status(thm)],[c30,c79]) ).
fof(f24,axiom,
! [U,V] :
( human_person(U,V)
=> animate(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f24_nnf,plain,
! [U,V] :
( animate(U,V)
| ~ human_person(U,V) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [U,V] :
( animate(U,V)
| ~ human_person(U,V) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( animate(X0,X1)
| ~ human_person(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p147,plain,
animate(sk3,sk4),
inference(resolution,[status(thm)],[p146,c24]) ).
cnf(p214,plain,
~ nonliving(sk3,sk4),
inference(resolution,[status(thm)],[c56,p147]) ).
cnf(p326,plain,
$false,
inference(resolution,[status(thm)],[p322,p214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n017.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 02:16:15 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.25/1.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.25/1.11 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------