%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:52 AM UTC 2026
% Result : Theorem 0.10s 0.44s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 34 ( 8 unt; 0 def)
% Number of atoms : 305 ( 3 equ)
% Maximal formula atoms : 63 ( 8 avg)
% Number of connectives : 324 ( 53 ~; 43 |; 210 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 52 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 1 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 131 ( 2 sgn 58 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax24,axiom,
! [U,V] :
( man(U,V)
=> male(U,V) ),
file('theBenchmark.p',ax24) ).
fof(ax38,axiom,
! [U,V] :
( object(U,V)
=> unisex(U,V) ),
file('theBenchmark.p',ax38) ).
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(ax63,axiom,
! [U,V] :
( unisex(U,V)
=> ~ male(U,V) ),
file('theBenchmark.p',ax63) ).
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,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('theBenchmark.p',co1) ).
fof(co1_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(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_95,plain,
( unisex(A,B)
| ~ object(A,B) ),
inference(clausify,[status(thm)],[ax38]) ).
cnf(c_108,plain,
( ~ male(A,B)
| ~ unisex(A,B) ),
inference(clausify,[status(thm)],[ax63]) ).
cnf(c_112,plain,
( ~ artifact(A,B)
| unisex(A,B) ),
inference(resolve,[status(thm)],[c_95,c_91]) ).
cnf(c_139,plain,
( ~ device(A,B)
| artifact(A,B) ),
inference(resolve,[status(thm)],[c_80,c_81]) ).
cnf(c_144,plain,
( ~ male(A,B)
| ~ artifact(A,B) ),
inference(resolve,[status(thm)],[c_112,c_108]) ).
fof(nnf_72,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(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)
& ! [X14] :
( ( cheap(sK0,X14)
& black(sK0,X14)
& coat(sK0,X14) )
| ~ member(sK0,X14,sK13) )
& group(sK0,sK13)
& ! [X11] :
( ! [X12] :
( ( wear(sK0,sK14(X11,X12))
& nonreflexive(sK0,sK14(X11,X12))
& present(sK0,sK14(X11,X12))
& patient(sK0,sK14(X11,X12),X11)
& agent(sK0,sK14(X11,X12),X12)
& event(sK0,sK14(X11,X12)) )
| ~ member(sK0,X12,sK10) )
| ~ member(sK0,X11,sK13) )
& ! [X10] :
( ( young(sK0,X10)
& fellow(sK0,X10) )
| ~ member(sK0,X10,sK10) )
& group(sK0,sK10)
& two(sK0,sK10)
& ! [X7] :
( ( in(sK0,sK12(X7),sK5)
& be(sK0,sK11(X7),X7,sK12(X7))
& state(sK0,sK11(X7)) )
| ~ member(sK0,X7,sK10) )
& in(sK0,sK9,sK8)
& down(sK0,sK9,sK8)
& barrel(sK0,sK9)
& present(sK0,sK9)
& agent(sK0,sK9,sK6)
& event(sK0,sK9)
& lonely(sK0,sK8)
& street(sK0,sK8)
& placename(sK0,sK7)
& hollywood_placename(sK0,sK7)
& city(sK0,sK8)
& of(sK0,sK7,sK8)
& 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,sK14,sK2,sK3]),skolemize(U,sK0),skolemize(V,sK1),skolemize(W,sK4),skolemize(X,sK5),skolemize(Y,sK6),skolemize(Z,sK7),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK10),skolemize(X4,sK13),skolemize(X5,sK3),skolemize(X6,sK2),skolemize(X8,sK11(X7)),skolemize(X9,sK12(X7)),skolemize(X13,sK14(X11,X12))],[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,sK13) )
& ! [VAR_0] :
( black(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0] :
( coat(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK13) )
& group(sK0,sK13)
& ! [VAR_0,VAR_1] :
( wear(sK0,sK14(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK10)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0,VAR_1] :
( nonreflexive(sK0,sK14(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK10)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0,VAR_1] :
( present(sK0,sK14(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK10)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0,VAR_1] :
( patient(sK0,sK14(VAR_0,VAR_1),VAR_0)
| ~ member(sK0,VAR_1,sK10)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0,VAR_1] :
( agent(sK0,sK14(VAR_0,VAR_1),VAR_1)
| ~ member(sK0,VAR_1,sK10)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0,VAR_1] :
( event(sK0,sK14(VAR_0,VAR_1))
| ~ member(sK0,VAR_1,sK10)
| ~ member(sK0,VAR_0,sK13) )
& ! [VAR_0] :
( young(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK10) )
& ! [VAR_0] :
( fellow(sK0,VAR_0)
| ~ member(sK0,VAR_0,sK10) )
& group(sK0,sK10)
& two(sK0,sK10)
& ! [VAR_0] :
( in(sK0,sK12(VAR_0),sK5)
| ~ member(sK0,VAR_0,sK10) )
& ! [VAR_0] :
( be(sK0,sK11(VAR_0),VAR_0,sK12(VAR_0))
| ~ member(sK0,VAR_0,sK10) )
& ! [VAR_0] :
( state(sK0,sK11(VAR_0))
| ~ member(sK0,VAR_0,sK10) )
& in(sK0,sK9,sK8)
& down(sK0,sK9,sK8)
& barrel(sK0,sK9)
& present(sK0,sK9)
& agent(sK0,sK9,sK6)
& event(sK0,sK9)
& lonely(sK0,sK8)
& street(sK0,sK8)
& placename(sK0,sK7)
& hollywood_placename(sK0,sK7)
& city(sK0,sK8)
& of(sK0,sK7,sK8)
& 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_178,plain,
( male(A,B)
| ~ man(A,B) ),
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_270,plain,
( device(A,B)
| ~ wheel(A,B) ),
inference(clausify,[status(thm)],[ax48]) ).
cnf(c_277,plain,
( ~ device(A,B)
| ~ male(A,B) ),
inference(resolve,[status(thm)],[c_144,c_139]) ).
cnf(c_279,negated_conjecture,
wheel(sK0,sK2),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_286,plain,
( ~ wheel(A,B)
| ~ male(A,B) ),
inference(resolve,[status(thm)],[c_277,c_270]) ).
cnf(c_310,plain,
( D = C
| ~ be(A,B,C,D) ),
inference(clausify,[status(thm)],[ax71]) ).
cnf(c_311,negated_conjecture,
be(sK0,sK3,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_312,negated_conjecture,
sK2 = sK1,
inference(resolve,[status(thm)],[c_311,c_310]) ).
cnf(c_326,negated_conjecture,
~ male(sK0,sK2),
inference(resolve,[status(thm)],[c_279,c_286]) ).
cnf(c_408,negated_conjecture,
male(sK0,sK1),
inference(resolve,[status(thm)],[c_178,c_177]) ).
cnf(c_445,plain,
~ male(sK0,sK1),
inference(paramod,[status(thm)],[c_312,c_326]) ).
cnf(c_444,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_408,c_445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 01:24:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 3416640 was started by sandbox on n011,
% 0.10/0.38 % Sat Sep 26 01:24:15 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.39
% 0.10/0.39 % From the command line: assign(max_seconds, 300).
% 0.10/0.44
% 0.10/0.44 % SZS status Theorem for theBenchmark
% 0.10/0.44
% 0.10/0.44 % Proof 1 at 0.03 (+ 0.00) seconds.
% 0.10/0.44 % Length of proof is 29.
% 0.10/0.44 % Level of proof is 7.
% 0.10/0.44 % Maximum clause weight is 8.000.
% 0.10/0.44 % Given clauses 15.
% 0.10/0.44
% 0.10/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------