%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Thu Sep 24 01:31:31 PM UTC 2026
% Result : Theorem 0.17s 0.49s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 43 ( 11 unt; 0 def)
% Number of atoms : 305 ( 5 equ)
% Maximal formula atoms : 48 ( 7 avg)
% Number of connectives : 308 ( 46 ~; 34 |; 210 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 1 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 143 ( 87 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
! [U,V] :
( man(U,V)
=> male(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [U,V] :
( object(U,V)
=> unisex(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U,V] :
( artifact(U,V)
=> object(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [U,V] :
( instrumentality(U,V)
=> artifact(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U,V] :
( device(U,V)
=> instrumentality(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U,V] :
( wheel(U,V)
=> device(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [U,V] :
( unisex(U,V)
=> ~ male(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [U,V,W,X] :
( be(U,V,W,X)
=> W = X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,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(negated_conjecture,[status(cth)],[f72]) ).
fof(f120,plain,
! [U,V] :
( male(U,V)
| ~ man(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f121,plain,
! [X0,X1] :
( male(X0,X1)
| ~ man(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f148,plain,
! [U,V] :
( unisex(U,V)
| ~ object(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f149,plain,
! [X0,X1] :
( unisex(X0,X1)
| ~ object(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f162,plain,
! [U,V] :
( object(U,V)
| ~ artifact(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f163,plain,
! [X0,X1] :
( object(X0,X1)
| ~ artifact(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
! [U,V] :
( artifact(U,V)
| ~ instrumentality(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f165,plain,
! [X0,X1] :
( artifact(X0,X1)
| ~ instrumentality(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f166,plain,
! [U,V] :
( instrumentality(U,V)
| ~ device(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f167,plain,
! [X0,X1] :
( instrumentality(X0,X1)
| ~ device(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f168,plain,
! [U,V] :
( device(U,V)
| ~ wheel(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f169,plain,
! [X0,X1] :
( device(X0,X1)
| ~ wheel(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f198,plain,
! [U,V] :
( ~ male(U,V)
| ~ unisex(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f199,plain,
! [X0,X1] :
( ~ male(X0,X1)
| ~ unisex(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f224,plain,
! [U,V,W,X] :
( W = X
| ~ be(U,V,W,X) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f225,plain,
! [W,X] :
( W = X
| ! [U,V] : ~ be(U,V,W,X) ),
inference(miniscoping,[status(thm)],[f224]) ).
fof(f226,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ be(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f227,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(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f228,plain,
? [U] :
( ? [X5] :
( behind(U,X5,X5)
& ? [V,X4] :
( be(U,X4,V,X5)
& state(U,X4)
& wheel(U,X5)
& ? [X3] :
( ! [X13] :
( ( cheap(U,X13)
& black(U,X13)
& coat(U,X13) )
| ~ member(U,X13,X3) )
& group(U,X3)
& ? [X2] :
( ! [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)
& ? [Z] :
( ! [X6] :
( ? [X8] :
( in(U,X8,Z)
& ? [X7] :
( be(U,X7,X6,X8)
& state(U,X7) ) )
| ~ member(U,X6,X2) )
& ? [X1] :
( in(U,X1,Z)
& down(U,X1,Z)
& barrel(U,X1)
& present(U,X1)
& ? [X] :
( agent(U,X1,X)
& event(U,X1)
& lonely(U,Z)
& street(U,Z)
& ? [Y] :
( 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)
& ? [W] :
( forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) ) ) ) ) ) ) ) ) )
& actual_world(U) ),
inference(miniscoping,[status(thm)],[f227]) ).
fof(f229,plain,
( behind(sK3_skl,sK4_skl,sK4_skl)
& be(sK3_skl,sK6_skl,sK5_skl,sK4_skl)
& state(sK3_skl,sK6_skl)
& wheel(sK3_skl,sK4_skl)
& ! [X13] :
( ( cheap(sK3_skl,X13)
& black(sK3_skl,X13)
& coat(sK3_skl,X13) )
| ~ member(sK3_skl,X13,sK7_skl) )
& group(sK3_skl,sK7_skl)
& ! [X10] :
( ! [X11] :
( ( wear(sK3_skl,sK16_skl(X11,X10))
& nonreflexive(sK3_skl,sK16_skl(X11,X10))
& present(sK3_skl,sK16_skl(X11,X10))
& patient(sK3_skl,sK16_skl(X11,X10),X10)
& agent(sK3_skl,sK16_skl(X11,X10),X11)
& event(sK3_skl,sK16_skl(X11,X10)) )
| ~ member(sK3_skl,X11,sK8_skl) )
| ~ member(sK3_skl,X10,sK7_skl) )
& ! [X9] :
( ( young(sK3_skl,X9)
& fellow(sK3_skl,X9) )
| ~ member(sK3_skl,X9,sK8_skl) )
& group(sK3_skl,sK8_skl)
& two(sK3_skl,sK8_skl)
& ! [X6] :
( ( in(sK3_skl,sK14_skl(X6),sK9_skl)
& be(sK3_skl,sK15_skl(X6),X6,sK14_skl(X6))
& state(sK3_skl,sK15_skl(X6)) )
| ~ member(sK3_skl,X6,sK8_skl) )
& in(sK3_skl,sK10_skl,sK9_skl)
& down(sK3_skl,sK10_skl,sK9_skl)
& barrel(sK3_skl,sK10_skl)
& present(sK3_skl,sK10_skl)
& agent(sK3_skl,sK10_skl,sK11_skl)
& event(sK3_skl,sK10_skl)
& lonely(sK3_skl,sK9_skl)
& street(sK3_skl,sK9_skl)
& placename(sK3_skl,sK12_skl)
& hollywood_placename(sK3_skl,sK12_skl)
& city(sK3_skl,sK9_skl)
& of(sK3_skl,sK12_skl,sK9_skl)
& old(sK3_skl,sK11_skl)
& dirty(sK3_skl,sK11_skl)
& white(sK3_skl,sK11_skl)
& chevy(sK3_skl,sK11_skl)
& frontseat(sK3_skl,sK9_skl)
& forename(sK3_skl,sK13_skl)
& jules_forename(sK3_skl,sK13_skl)
& man(sK3_skl,sK5_skl)
& of(sK3_skl,sK13_skl,sK5_skl)
& actual_world(sK3_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl]),skolemize(U,sK3_skl),skolemize(X5,sK4_skl),skolemize(V,sK5_skl),skolemize(X4,sK6_skl),skolemize(X3,sK7_skl),skolemize(X2,sK8_skl),skolemize(Z,sK9_skl),skolemize(X1,sK10_skl),skolemize(X,sK11_skl),skolemize(Y,sK12_skl),skolemize(W,sK13_skl),skolemize(X8,sK14_skl(X6)),skolemize(X7,sK15_skl(X6)),skolemize(X12,sK16_skl(X11,X10))],[f228]) ).
fof(f232,plain,
man(sK3_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f269,plain,
wheel(sK3_skl,sK4_skl),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f271,plain,
be(sK3_skl,sK6_skl,sK5_skl,sK4_skl),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f279,plain,
sK5_skl = sK4_skl,
inference(resolution,[status(thm)],[f226,f271]) ).
fof(f282,plain,
man(sK3_skl,sK4_skl),
inference(backward_demodulation,[status(thm)],[f279,f232]) ).
fof(f287,plain,
! [X0,X1] :
( object(X0,X1)
| ~ instrumentality(X0,X1) ),
inference(resolution,[status(thm)],[f165,f163]) ).
fof(f298,plain,
! [X0,X1] :
( ~ man(X0,X1)
| ~ unisex(X0,X1) ),
inference(resolution,[status(thm)],[f199,f121]) ).
fof(f360,plain,
~ unisex(sK3_skl,sK4_skl),
inference(resolution,[status(thm)],[f298,f282]) ).
fof(f362,plain,
~ object(sK3_skl,sK4_skl),
inference(resolution,[status(thm)],[f360,f149]) ).
fof(f366,plain,
~ instrumentality(sK3_skl,sK4_skl),
inference(resolution,[status(thm)],[f362,f287]) ).
fof(f406,plain,
~ device(sK3_skl,sK4_skl),
inference(resolution,[status(thm)],[f366,f167]) ).
fof(f425,plain,
~ wheel(sK3_skl,sK4_skl),
inference(resolution,[status(thm)],[f406,f169]) ).
fof(f426,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f425,f269]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n007.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 01:47:05 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.17/0.49 % Refutation found
% 0.17/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/0.54 % Elapsed time: 0.081797 seconds
% 0.17/0.54 % CPU time: 0.145743 seconds
% 0.17/0.54 % Total memory used: 24.559 MB
% 0.17/0.54 % Net memory used: 24.541 MB
%------------------------------------------------------------------------------