%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:07:53 AM UTC 2026
% Result : Theorem 0.13s 10.68s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 40 ( 11 unt; 0 def)
% Number of atoms : 314 ( 3 equ)
% Maximal formula atoms : 63 ( 7 avg)
% Number of connectives : 324 ( 50 ~; 44 |; 210 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 1 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 134 ( 2 sgn 62 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax27,axiom,
! [U,V] :
( organism(U,V)
=> living(U,V) ),
file('theBenchmark.p',ax27) ).
fof(ax30,axiom,
! [U,V] :
( human_person(U,V)
=> organism(U,V) ),
file('theBenchmark.p',ax30) ).
fof(ax31,axiom,
! [U,V] :
( man(U,V)
=> human_person(U,V) ),
file('theBenchmark.p',ax31) ).
fof(ax40,axiom,
! [U,V] :
( object(U,V)
=> nonliving(U,V) ),
file('theBenchmark.p',ax40) ).
fof(ax45,axiom,
! [U,V] :
( artifact(U,V)
=> object(U,V) ),
file('theBenchmark.p',ax45) ).
fof(ax46,axiom,
! [U,V] :
( instrumentality(U,V)
=> artifact(U,V) ),
file('theBenchmark.p',ax46) ).
fof(ax47,axiom,
! [U,V] :
( device(U,V)
=> instrumentality(U,V) ),
file('theBenchmark.p',ax47) ).
fof(ax48,axiom,
! [U,V] :
( wheel(U,V)
=> device(U,V) ),
file('theBenchmark.p',ax48) ).
fof(ax60,axiom,
! [U,V] :
( nonliving(U,V)
=> ~ living(U,V) ),
file('theBenchmark.p',ax60) ).
fof(ax71,axiom,
! [U,V,W,X] :
( be(U,V,W,X)
=> W = X ),
file('theBenchmark.p',ax71) ).
fof(co1,conjecture,
~ ? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5] :
( behind(U,X5,X5)
& be(U,X4,V,X5)
& state(U,X4)
& wheel(U,X5)
& ! [X13] :
( member(U,X13,X3)
=> ( cheap(U,X13)
& black(U,X13)
& coat(U,X13) ) )
& group(U,X3)
& ! [X10] :
( member(U,X10,X3)
=> ! [X11] :
( member(U,X11,X2)
=> ? [X12] :
( wear(U,X12)
& nonreflexive(U,X12)
& present(U,X12)
& patient(U,X12,X10)
& agent(U,X12,X11)
& event(U,X12) ) ) )
& ! [X9] :
( member(U,X9,X2)
=> ( young(U,X9)
& fellow(U,X9) ) )
& group(U,X2)
& two(U,X2)
& ! [X6] :
( member(U,X6,X2)
=> ? [X7,X8] :
( in(U,X8,Z)
& be(U,X7,X6,X8)
& state(U,X7) ) )
& in(U,X1,Z)
& down(U,X1,Z)
& barrel(U,X1)
& present(U,X1)
& agent(U,X1,X)
& event(U,X1)
& lonely(U,Z)
& street(U,Z)
& placename(U,Y)
& hollywood_placename(U,Y)
& city(U,Z)
& of(U,Y,Z)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& frontseat(U,Z)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5] :
( behind(U,X5,X5)
& be(U,X4,V,X5)
& state(U,X4)
& wheel(U,X5)
& ! [X13] :
( member(U,X13,X3)
=> ( cheap(U,X13)
& black(U,X13)
& coat(U,X13) ) )
& group(U,X3)
& ! [X10] :
( member(U,X10,X3)
=> ! [X11] :
( member(U,X11,X2)
=> ? [X12] :
( wear(U,X12)
& nonreflexive(U,X12)
& present(U,X12)
& patient(U,X12,X10)
& agent(U,X12,X11)
& event(U,X12) ) ) )
& ! [X9] :
( member(U,X9,X2)
=> ( young(U,X9)
& fellow(U,X9) ) )
& group(U,X2)
& two(U,X2)
& ! [X6] :
( member(U,X6,X2)
=> ? [X7,X8] :
( in(U,X8,Z)
& be(U,X7,X6,X8)
& state(U,X7) ) )
& in(U,X1,Z)
& down(U,X1,Z)
& barrel(U,X1)
& present(U,X1)
& agent(U,X1,X)
& event(U,X1)
& lonely(U,Z)
& street(U,Z)
& placename(U,Y)
& hollywood_placename(U,Y)
& city(U,Z)
& of(U,Y,Z)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& frontseat(U,Z)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_80,plain,
( artifact(A,B)
| ~ instrumentality(A,B) ),
inference(clausify,[status(thm)],[ax46]) ).
cnf(c_81,plain,
( instrumentality(A,B)
| ~ device(A,B) ),
inference(clausify,[status(thm)],[ax47]) ).
cnf(c_91,plain,
( object(A,B)
| ~ artifact(A,B) ),
inference(clausify,[status(thm)],[ax45]) ).
cnf(c_93,plain,
( nonliving(A,B)
| ~ object(A,B) ),
inference(clausify,[status(thm)],[ax40]) ).
cnf(c_139,plain,
( ~ device(A,B)
| artifact(A,B) ),
inference(resolve,[status(thm)],[c_80,c_81]) ).
cnf(c_142,plain,
( ~ artifact(A,B)
| nonliving(A,B) ),
inference(resolve,[status(thm)],[c_93,c_91]) ).
cnf(c_175,plain,
( human_person(A,B)
| ~ man(A,B) ),
inference(clausify,[status(thm)],[ax31]) ).
fof(nnf_72,plain,
? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5] :
( behind(U,X5,X5)
& be(U,X4,V,X5)
& state(U,X4)
& wheel(U,X5)
& ! [X13] :
( ( cheap(U,X13)
& black(U,X13)
& coat(U,X13) )
| ~ member(U,X13,X3) )
& group(U,X3)
& ! [X10] :
( ! [X11] :
( ? [X12] :
( wear(U,X12)
& nonreflexive(U,X12)
& present(U,X12)
& patient(U,X12,X10)
& agent(U,X12,X11)
& event(U,X12) )
| ~ member(U,X11,X2) )
| ~ member(U,X10,X3) )
& ! [X9] :
( ( young(U,X9)
& fellow(U,X9) )
| ~ member(U,X9,X2) )
& group(U,X2)
& two(U,X2)
& ! [X6] :
( ? [X7,X8] :
( in(U,X8,Z)
& be(U,X7,X6,X8)
& state(U,X7) )
| ~ member(U,X6,X2) )
& in(U,X1,Z)
& down(U,X1,Z)
& barrel(U,X1)
& present(U,X1)
& agent(U,X1,X)
& event(U,X1)
& lonely(U,Z)
& street(U,Z)
& placename(U,Y)
& hollywood_placename(U,Y)
& city(U,Z)
& of(U,Y,Z)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& frontseat(U,Z)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
inference(fof_nnf,[status(thm)],[co1_neg]) ).
fof(sk_co1_neg_sk,plain,
( behind(sK0,sK2,sK2)
& be(sK0,sK3,sK1,sK2)
& state(sK0,sK3)
& wheel(sK0,sK2)
& ! [X13] :
( ( cheap(sK0,X13)
& black(sK0,X13)
& coat(sK0,X13) )
| ~ member(sK0,X13,sK12) )
& group(sK0,sK12)
& ! [X10] :
( ! [X11] :
( ( wear(sK0,sK13(X10,X11))
& nonreflexive(sK0,sK13(X10,X11))
& present(sK0,sK13(X10,X11))
& patient(sK0,sK13(X10,X11),X10)
& agent(sK0,sK13(X10,X11),X11)
& event(sK0,sK13(X10,X11)) )
| ~ member(sK0,X11,sK9) )
| ~ member(sK0,X10,sK12) )
& ! [X9] :
( ( young(sK0,X9)
& fellow(sK0,X9) )
| ~ member(sK0,X9,sK9) )
& group(sK0,sK9)
& two(sK0,sK9)
& ! [X6] :
( ( in(sK0,sK11(X6),sK5)
& be(sK0,sK10(X6),X6,sK11(X6))
& state(sK0,sK10(X6)) )
| ~ member(sK0,X6,sK9) )
& in(sK0,sK8,sK5)
& down(sK0,sK8,sK5)
& barrel(sK0,sK8)
& present(sK0,sK8)
& agent(sK0,sK8,sK6)
& event(sK0,sK8)
& lonely(sK0,sK5)
& street(sK0,sK5)
& placename(sK0,sK7)
& hollywood_placename(sK0,sK7)
& city(sK0,sK5)
& of(sK0,sK7,sK5)
& old(sK0,sK6)
& dirty(sK0,sK6)
& white(sK0,sK6)
& chevy(sK0,sK6)
& frontseat(sK0,sK5)
& forename(sK0,sK4)
& jules_forename(sK0,sK4)
& man(sK0,sK1)
& of(sK0,sK4,sK1)
& actual_world(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK4,sK1,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK2,sK3]),skolemize(U,sK0),skolemize(V,sK1),skolemize(W,sK4),skolemize(X,sK6),skolemize(Y,sK7),skolemize(Z,sK5),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK12),skolemize(X4,sK3),skolemize(X5,sK2),skolemize(X7,sK10(X6)),skolemize(X8,sK11(X6)),skolemize(X12,sK13(X10,X11))],[nnf_72]) ).
fof(sk_co1_neg,plain,
( behind(sK0,sK2,sK2)
& be(sK0,sK3,sK1,sK2)
& state(sK0,sK3)
& wheel(sK0,sK2)
& ! [VAR_0] :
( cheap(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0] :
( black(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0] :
( coat(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK12) )
& group(sK0,sK12)
& ! [VAR_0,VAR_1] :
( wear(sK0,sK13(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK9)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0,VAR_1] :
( nonreflexive(sK0,sK13(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK9)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0,VAR_1] :
( present(sK0,sK13(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK9)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0,VAR_1] :
( patient(sK0,sK13(VAR_0,VAR_1),VAR_0)
| ~ member(sK0,VAR_1,sK9)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0,VAR_1] :
( agent(sK0,sK13(VAR_0,VAR_1),VAR_1)
| ~ member(sK0,VAR_1,sK9)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0,VAR_1] :
( event(sK0,sK13(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK9)
| ~ member(sK0,VAR_0,sK12) )
& ! [VAR_0] :
( young(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK9) )
& ! [VAR_0] :
( fellow(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK9) )
& group(sK0,sK9)
& two(sK0,sK9)
& ! [VAR_0] :
( in(sK0,sK11(VAR_0),sK5)
| ~ member(sK0,VAR_0,sK9) )
& ! [VAR_0] :
( be(sK0,sK10(VAR_0),VAR_0,sK11(VAR_0))
| ~ member(sK0,VAR_0,sK9) )
& ! [VAR_0] :
( state(sK0,sK10(VAR_0))
| ~ member(sK0,VAR_0,sK9) )
& in(sK0,sK8,sK5)
& down(sK0,sK8,sK5)
& barrel(sK0,sK8)
& present(sK0,sK8)
& agent(sK0,sK8,sK6)
& event(sK0,sK8)
& lonely(sK0,sK5)
& street(sK0,sK5)
& placename(sK0,sK7)
& hollywood_placename(sK0,sK7)
& city(sK0,sK5)
& of(sK0,sK7,sK5)
& old(sK0,sK6)
& dirty(sK0,sK6)
& white(sK0,sK6)
& chevy(sK0,sK6)
& frontseat(sK0,sK5)
& forename(sK0,sK4)
& jules_forename(sK0,sK4)
& man(sK0,sK1)
& of(sK0,sK4,sK1)
& actual_world(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_co1_neg_sk]) ).
cnf(c_177,negated_conjecture,
man(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_181,negated_conjecture,
human_person(sK0,sK1),
inference(resolve,[status(thm)],[c_175,c_177]) ).
cnf(c_183,plain,
( organism(A,B)
| ~ human_person(A,B) ),
inference(clausify,[status(thm)],[ax30]) ).
cnf(c_193,negated_conjecture,
organism(sK0,sK1),
inference(resolve,[status(thm)],[c_183,c_181]) ).
cnf(c_195,plain,
( living(A,B)
| ~ organism(A,B) ),
inference(clausify,[status(thm)],[ax27]) ).
cnf(c_196,plain,
( ~ living(A,B)
| ~ nonliving(A,B) ),
inference(clausify,[status(thm)],[ax60]) ).
cnf(c_198,negated_conjecture,
living(sK0,sK1),
inference(resolve,[status(thm)],[c_195,c_193]) ).
cnf(c_268,plain,
( device(A,B)
| ~ wheel(A,B) ),
inference(clausify,[status(thm)],[ax48]) ).
cnf(c_274,plain,
( ~ device(A,B)
| nonliving(A,B) ),
inference(resolve,[status(thm)],[c_142,c_139]) ).
cnf(c_277,negated_conjecture,
wheel(sK0,sK2),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_283,plain,
( ~ wheel(A,B)
| nonliving(A,B) ),
inference(resolve,[status(thm)],[c_274,c_268]) ).
cnf(c_308,plain,
( D = C
| ~ be(A,B,C,D) ),
inference(clausify,[status(thm)],[ax71]) ).
cnf(c_309,negated_conjecture,
be(sK0,sK3,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_310,negated_conjecture,
sK2 = sK1,
inference(resolve,[status(thm)],[c_309,c_308]) ).
cnf(c_327,negated_conjecture,
nonliving(sK0,sK2),
inference(resolve,[status(thm)],[c_277,c_283]) ).
cnf(c_328,negated_conjecture,
nonliving(sK0,sK1),
inference(paramod,[status(thm)],[c_310,c_327]) ).
cnf(c_363,negated_conjecture,
~ nonliving(sK0,sK1),
inference(resolve,[status(thm)],[c_196,c_198]) ).
cnf(c_364,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_328,c_363]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/10.62 % Computer : n019.cluster.edu
% 0.13/10.62 % Model : x86_64 x86_64
% 0.13/10.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.62 % Memory : 8046.5625MB
% 0.13/10.62 % OS : Linux 6.8.0-71-generic
% 0.13/10.62 % CPULimit : 300
% 0.13/10.62 % WCLimit : 300
% 0.13/10.62 % DateTime : Sat Sep 26 01:25:46 UTC 2026
% 0.13/10.63 % CPUTime :
% 0.13/10.63 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/10.63 % Process 4182133 was started by sandbox2 on n019,
% 0.13/10.63 % Sat Sep 26 01:25:46 2026
% 0.13/10.63 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/10.65
% 0.13/10.65 % From the command line: assign(max_seconds, 300).
% 0.13/10.68
% 0.13/10.68 % SZS status Theorem for theBenchmark
% 0.13/10.68
% 0.13/10.68 % Proof 1 at 0.03 (+ 0.00) seconds.
% 0.13/10.68 % Length of proof is 36.
% 0.13/10.68 % Level of proof is 7.
% 0.13/10.68 % Maximum clause weight is 8.000.
% 0.13/10.68 % Given clauses 0.
% 0.13/10.68
% 0.13/10.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------