%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:33:05 PM UTC 2026
% Result : Theorem 0.19s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n026.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 01:51:51 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 0.19/0.50 % Refutation found
% 0.19/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.50 fof(f25,axiom,(
% 0.19/0.50 (! [U,V] :( human_person(U,V)=> animate(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f31,axiom,(
% 0.19/0.50 (! [U,V] :( man(U,V)=> human_person(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f40,axiom,(
% 0.19/0.50 (! [U,V] :( object(U,V)=> nonliving(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f45,axiom,(
% 0.19/0.50 (! [U,V] :( artifact(U,V)=> object(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f46,axiom,(
% 0.19/0.50 (! [U,V] :( instrumentality(U,V)=> artifact(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f47,axiom,(
% 0.19/0.50 (! [U,V] :( device(U,V)=> instrumentality(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f48,axiom,(
% 0.19/0.50 (! [U,V] :( wheel(U,V)=> device(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f57,axiom,(
% 0.19/0.50 (! [U,V] :( animate(U,V)=> ~ nonliving(U,V) ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f71,axiom,(
% 0.19/0.50 (! [U,V,W,X] :( be(U,V,W,X)=> W = X ) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f72,conjecture,(
% 0.19/0.50 ~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1,X2,X3,X4,X5] :( of(U,W,V)& man(U,V)& jules_forename(U,W)& forename(U,W)& frontseat(U,Z)& chevy(U,X)& white(U,X)& dirty(U,X)& old(U,X)& of(U,Y,Z)& city(U,Z)& hollywood_placename(U,Y)& placename(U,Y)& street(U,Z)& lonely(U,Z)& event(U,X1)& agent(U,X1,X)& present(U,X1)& barrel(U,X1)& down(U,X1,Z)& in(U,X1,Z)& (! [X6] :( member(U,X6,X2)=> (? [X7,X8] :( state(U,X7)& be(U,X7,X6,X8)& in(U,X8,Z) ) )))& two(U,X2)& group(U,X2)& (! [X9] :( member(U,X9,X2)=> ( fellow(U,X9)& young(U,X9) ) ))& (! [X10] :( member(U,X10,X3)=> (! [X11] :( member(U,X11,X2)=> (? [X12] :( event(U,X12)& agent(U,X12,X11)& patient(U,X12,X10)& present(U,X12)& nonreflexive(U,X12)& wear(U,X12) ) )) )))& group(U,X3)& (! [X13] :( member(U,X13,X3)=> ( coat(U,X13)& black(U,X13)& cheap(U,X13) ) ))& wheel(U,X5)& state(U,X4)& be(U,X4,V,X5)& behind(U,X5,X5) ) )) )),
% 0.19/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f73,negated_conjecture,(
% 0.19/0.50 ~(~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1,X2,X3,X4,X5] :( of(U,W,V)& man(U,V)& jules_forename(U,W)& forename(U,W)& frontseat(U,Z)& chevy(U,X)& white(U,X)& dirty(U,X)& old(U,X)& of(U,Y,Z)& city(U,Z)& hollywood_placename(U,Y)& placename(U,Y)& street(U,Z)& lonely(U,Z)& event(U,X1)& agent(U,X1,X)& present(U,X1)& barrel(U,X1)& down(U,X1,Z)& in(U,X1,Z)& (! [X6] :( member(U,X6,X2)=> (? [X7,X8] :( state(U,X7)& be(U,X7,X6,X8)& in(U,X8,Z) ) )))& two(U,X2)& group(U,X2)& (! [X9] :( member(U,X9,X2)=> ( fellow(U,X9)& young(U,X9) ) ))& (! [X10] :( member(U,X10,X3)=> (! [X11] :( member(U,X11,X2)=> (? [X12] :( event(U,X12)& agent(U,X12,X11)& patient(U,X12,X10)& present(U,X12)& nonreflexive(U,X12)& wear(U,X12) ) )) )))& group(U,X3)& (! [X13] :( member(U,X13,X3)=> ( coat(U,X13)& black(U,X13)& cheap(U,X13) ) ))& wheel(U,X5)& state(U,X4)& be(U,X4,V,X5)& behind(U,X5,X5) ) )) ))),
% 0.19/0.50 inference(negated_conjecture,[status(cth)],[f72])).
% 0.19/0.50 fof(f122,plain,(
% 0.19/0.50 ![U,V]: (~human_person(U,V)|animate(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.19/0.50 fof(f123,plain,(
% 0.19/0.50 ![X0,X1]: (~human_person(X0,X1)|animate(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f122])).
% 0.19/0.50 fof(f134,plain,(
% 0.19/0.50 ![U,V]: (~man(U,V)|human_person(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.19/0.50 fof(f135,plain,(
% 0.19/0.50 ![X0,X1]: (~man(X0,X1)|human_person(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.19/0.50 fof(f152,plain,(
% 0.19/0.50 ![U,V]: (~object(U,V)|nonliving(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.19/0.50 fof(f153,plain,(
% 0.19/0.50 ![X0,X1]: (~object(X0,X1)|nonliving(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f152])).
% 0.19/0.50 fof(f162,plain,(
% 0.19/0.50 ![U,V]: (~artifact(U,V)|object(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.19/0.50 fof(f163,plain,(
% 0.19/0.50 ![X0,X1]: (~artifact(X0,X1)|object(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f162])).
% 0.19/0.50 fof(f164,plain,(
% 0.19/0.50 ![U,V]: (~instrumentality(U,V)|artifact(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.19/0.50 fof(f165,plain,(
% 0.19/0.50 ![X0,X1]: (~instrumentality(X0,X1)|artifact(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f164])).
% 0.19/0.50 fof(f166,plain,(
% 0.19/0.50 ![U,V]: (~device(U,V)|instrumentality(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.19/0.50 fof(f167,plain,(
% 0.19/0.50 ![X0,X1]: (~device(X0,X1)|instrumentality(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f166])).
% 0.19/0.50 fof(f168,plain,(
% 0.19/0.50 ![U,V]: (~wheel(U,V)|device(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.19/0.50 fof(f169,plain,(
% 0.19/0.50 ![X0,X1]: (~wheel(X0,X1)|device(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f168])).
% 0.19/0.50 fof(f186,plain,(
% 0.19/0.50 ![U,V]: (~animate(U,V)|~nonliving(U,V))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.19/0.50 fof(f187,plain,(
% 0.19/0.50 ![X0,X1]: (~animate(X0,X1)|~nonliving(X0,X1))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f186])).
% 0.19/0.50 fof(f224,plain,(
% 0.19/0.50 ![U,V,W,X]: (~be(U,V,W,X)|W=X)),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.19/0.50 fof(f225,plain,(
% 0.19/0.50 ![W,X]: ((![U,V]: ~be(U,V,W,X))|W=X)),
% 0.19/0.50 inference(miniscoping,[status(thm)],[f224])).
% 0.19/0.50 fof(f226,plain,(
% 0.19/0.50 ![X0,X1,X2,X3]: (~be(X0,X1,X2,X3)|X2=X3)),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f225])).
% 0.19/0.50 fof(f227,plain,(
% 0.19/0.50 ?[U]: (actual_world(U)&(?[V,W,X,Y,Z,X1,X2,X3,X4,X5]: (((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,Z))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&of(U,Y,Z))&city(U,Z))&hollywood_placename(U,Y))&placename(U,Y))&street(U,Z))&lonely(U,Z))&event(U,X1))&agent(U,X1,X))&present(U,X1))&barrel(U,X1))&down(U,X1,Z))&in(U,X1,Z))&(![X6]: (~member(U,X6,X2)|(?[X7,X8]: ((state(U,X7)&be(U,X7,X6,X8))&in(U,X8,Z))))))&two(U,X2))&group(U,X2))&(![X9]: (~member(U,X9,X2)|(fellow(U,X9)&young(U,X9)))))&(![X10]: (~member(U,X10,X3)|(![X11]: (~member(U,X11,X2)|(?[X12]: (((((event(U,X12)&agent(U,X12,X11))&patient(U,X12,X10))&present(U,X12))&nonreflexive(U,X12))&wear(U,X12))))))))&group(U,X3))&(![X13]: (~member(U,X13,X3)|((coat(U,X13)&black(U,X13))&cheap(U,X13)))))&wheel(U,X5))&state(U,X4))&be(U,X4,V,X5))&behind(U,X5,X5))))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.19/0.50 fof(f228,plain,(
% 0.19/0.50 ?[U]: (actual_world(U)&(?[X5]: ((?[V,X4]: ((((?[X3]: (((?[X2]: (((((?[Z]: ((?[X1]: (((((?[X]: (((((?[Y]: ((((((((((?[W]: (((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W)))&frontseat(U,Z))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&of(U,Y,Z))&city(U,Z))&hollywood_placename(U,Y))&placename(U,Y)))&street(U,Z))&lonely(U,Z))&event(U,X1))&agent(U,X1,X)))&present(U,X1))&barrel(U,X1))&down(U,X1,Z))&in(U,X1,Z)))&(![X6]: (~member(U,X6,X2)|(?[X8]: ((?[X7]: (state(U,X7)&be(U,X7,X6,X8)))&in(U,X8,Z)))))))&two(U,X2))&group(U,X2))&(![X9]: (~member(U,X9,X2)|(fellow(U,X9)&young(U,X9)))))&(![X10]: (~member(U,X10,X3)|(![X11]: (~member(U,X11,X2)|(?[X12]: (((((event(U,X12)&agent(U,X12,X11))&patient(U,X12,X10))&present(U,X12))&nonreflexive(U,X12))&wear(U,X12)))))))))&group(U,X3))&(![X13]: (~member(U,X13,X3)|((coat(U,X13)&black(U,X13))&cheap(U,X13))))))&wheel(U,X5))&state(U,X4))&be(U,X4,V,X5)))&behind(U,X5,X5))))),
% 0.19/0.50 inference(miniscoping,[status(thm)],[f227])).
% 0.19/0.50 fof(f229,plain,(
% 0.19/0.50 (actual_world(sK3_skl)&(((((((((((((((((((((((((((((((of(sK3_skl,sK13_skl,sK5_skl)&man(sK3_skl,sK5_skl))&jules_forename(sK3_skl,sK13_skl))&forename(sK3_skl,sK13_skl))&frontseat(sK3_skl,sK9_skl))&chevy(sK3_skl,sK11_skl))&white(sK3_skl,sK11_skl))&dirty(sK3_skl,sK11_skl))&old(sK3_skl,sK11_skl))&of(sK3_skl,sK12_skl,sK9_skl))&city(sK3_skl,sK9_skl))&hollywood_placename(sK3_skl,sK12_skl))&placename(sK3_skl,sK12_skl))&street(sK3_skl,sK9_skl))&lonely(sK3_skl,sK9_skl))&event(sK3_skl,sK10_skl))&agent(sK3_skl,sK10_skl,sK11_skl))&present(sK3_skl,sK10_skl))&barrel(sK3_skl,sK10_skl))&down(sK3_skl,sK10_skl,sK9_skl))&in(sK3_skl,sK10_skl,sK9_skl))&(![X6]: (~member(sK3_skl,X6,sK8_skl)|((state(sK3_skl,sK15_skl(X6))&be(sK3_skl,sK15_skl(X6),X6,sK14_skl(X6)))&in(sK3_skl,sK14_skl(X6),sK9_skl)))))&two(sK3_skl,sK8_skl))&group(sK3_skl,sK8_skl))&(![X9]: (~member(sK3_skl,X9,sK8_skl)|(fellow(sK3_skl,X9)&young(sK3_skl,X9)))))&(![X10]: (~member(sK3_skl,X10,sK7_skl)|(![X11]: (~member(sK3_skl,X11,sK8_skl)|(((((event(sK3_skl,sK16_skl(X11,X10))&agent(sK3_skl,sK16_skl(X11,X10),X11))&patient(sK3_skl,sK16_skl(X11,X10),X10))&present(sK3_skl,sK16_skl(X11,X10)))&nonreflexive(sK3_skl,sK16_skl(X11,X10)))&wear(sK3_skl,sK16_skl(X11,X10))))))))&group(sK3_skl,sK7_skl))&(![X13]: (~member(sK3_skl,X13,sK7_skl)|((coat(sK3_skl,X13)&black(sK3_skl,X13))&cheap(sK3_skl,X13)))))&wheel(sK3_skl,sK4_skl))&state(sK3_skl,sK6_skl))&be(sK3_skl,sK6_skl,sK5_skl,sK4_skl))&behind(sK3_skl,sK4_skl,sK4_skl)))),
% 0.19/0.51 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])).
% 0.19/0.51 fof(f232,plain,(
% 0.19/0.51 man(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f229])).
% 0.19/0.51 fof(f269,plain,(
% 0.19/0.51 wheel(sK3_skl,sK4_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f229])).
% 0.19/0.51 fof(f271,plain,(
% 0.19/0.51 be(sK3_skl,sK6_skl,sK5_skl,sK4_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f229])).
% 0.19/0.51 fof(f281,plain,(
% 0.19/0.51 human_person(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f135,f232])).
% 0.19/0.51 fof(f294,plain,(
% 0.19/0.51 animate(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f123,f281])).
% 0.19/0.51 fof(f306,plain,(
% 0.19/0.51 sK5_skl=sK4_skl),
% 0.19/0.51 inference(resolution,[status(thm)],[f226,f271])).
% 0.19/0.51 fof(f309,plain,(
% 0.19/0.51 wheel(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(backward_demodulation,[status(thm)],[f306,f269])).
% 0.19/0.51 fof(f319,plain,(
% 0.19/0.51 ![X0,X1]: (~device(X0,X1)|artifact(X0,X1))),
% 0.19/0.51 inference(resolution,[status(thm)],[f167,f165])).
% 0.19/0.51 fof(f330,plain,(
% 0.19/0.51 ~nonliving(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f187,f294])).
% 0.19/0.51 fof(f384,plain,(
% 0.19/0.51 ![X0,X1]: (~device(X0,X1)|object(X0,X1))),
% 0.19/0.51 inference(resolution,[status(thm)],[f319,f163])).
% 0.19/0.51 fof(f419,plain,(
% 0.19/0.51 ![X0,X1]: (object(X0,X1)|~wheel(X0,X1))),
% 0.19/0.51 inference(resolution,[status(thm)],[f384,f169])).
% 0.19/0.51 fof(f421,plain,(
% 0.19/0.51 object(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f419,f309])).
% 0.19/0.51 fof(f423,plain,(
% 0.19/0.51 nonliving(sK3_skl,sK5_skl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f421,f153])).
% 0.19/0.51 fof(f426,plain,(
% 0.19/0.51 $false),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f423,f330])).
% 0.19/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.57 % Elapsed time: 0.108728 seconds
% 0.19/0.57 % CPU time: 0.163811 seconds
% 0.19/0.57 % Total memory used: 24.446 MB
% 0.19/0.57 % Net memory used: 24.424 MB
%------------------------------------------------------------------------------