%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP204+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 : 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 : Thu Sep 24 01:33:04 PM UTC 2026
% Result : Theorem 0.15s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.46 % Computer : n019.cluster.edu
% 0.15/0.46 % Model : x86_64 x86_64
% 0.15/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.46 % Memory : 8046.5625MB
% 0.15/0.46 % OS : Linux 6.8.0-71-generic
% 0.15/0.46 % CPULimit : 300
% 0.15/0.46 % WCLimit : 300
% 0.15/0.46 % DateTime : Mon Sep 21 01:49:05 UTC 2026
% 0.15/0.46 % CPUTime :
% 0.15/0.50 % Drodi V4.1.1
% 0.15/0.52 % Refutation found
% 0.15/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.52 fof(f24,axiom,(
% 0.15/0.52 (! [U,V] :( man(U,V)=> male(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f38,axiom,(
% 0.15/0.52 (! [U,V] :( object(U,V)=> unisex(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f45,axiom,(
% 0.15/0.52 (! [U,V] :( artifact(U,V)=> object(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f46,axiom,(
% 0.15/0.52 (! [U,V] :( instrumentality(U,V)=> artifact(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f47,axiom,(
% 0.15/0.52 (! [U,V] :( device(U,V)=> instrumentality(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f48,axiom,(
% 0.15/0.52 (! [U,V] :( wheel(U,V)=> device(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f63,axiom,(
% 0.15/0.52 (! [U,V] :( unisex(U,V)=> ~ male(U,V) ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f71,axiom,(
% 0.15/0.52 (! [U,V,W,X] :( be(U,V,W,X)=> W = X ) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f72,conjecture,(
% 0.15/0.52 ~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :( of(U,W,V)& man(U,V)& jules_forename(U,W)& forename(U,W)& frontseat(U,X)& chevy(U,Y)& white(U,Y)& dirty(U,Y)& old(U,Y)& of(U,Z,X1)& city(U,X1)& hollywood_placename(U,Z)& placename(U,Z)& street(U,X1)& lonely(U,X1)& event(U,X2)& agent(U,X2,Y)& present(U,X2)& barrel(U,X2)& down(U,X2,X1)& in(U,X2,X1)& (! [X7] :( member(U,X7,X3)=> (? [X8,X9] :( state(U,X8)& be(U,X8,X7,X9)& in(U,X9,X) ) )))& two(U,X3)& group(U,X3)& (! [X10] :( member(U,X10,X3)=> ( fellow(U,X10)& young(U,X10) ) ))& (! [X11] :( member(U,X11,X4)=> (! [X12] :( member(U,X12,X3)=> (? [X13] :( event(U,X13)& agent(U,X13,X12)& patient(U,X13,X11)& present(U,X13)& nonreflexive(U,X13)& wear(U,X13) ) )) )))& group(U,X4)& (! [X14] :( member(U,X14,X4)=> ( coat(U,X14)& black(U,X14)& cheap(U,X14) ) ))& wheel(U,X6)& state(U,X5)& be(U,X5,V,X6)& behind(U,X6,X6) ) )) )),
% 0.15/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.52 fof(f73,negated_conjecture,(
% 0.15/0.52 ~(~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :( of(U,W,V)& man(U,V)& jules_forename(U,W)& forename(U,W)& frontseat(U,X)& chevy(U,Y)& white(U,Y)& dirty(U,Y)& old(U,Y)& of(U,Z,X1)& city(U,X1)& hollywood_placename(U,Z)& placename(U,Z)& street(U,X1)& lonely(U,X1)& event(U,X2)& agent(U,X2,Y)& present(U,X2)& barrel(U,X2)& down(U,X2,X1)& in(U,X2,X1)& (! [X7] :( member(U,X7,X3)=> (? [X8,X9] :( state(U,X8)& be(U,X8,X7,X9)& in(U,X9,X) ) )))& two(U,X3)& group(U,X3)& (! [X10] :( member(U,X10,X3)=> ( fellow(U,X10)& young(U,X10) ) ))& (! [X11] :( member(U,X11,X4)=> (! [X12] :( member(U,X12,X3)=> (? [X13] :( event(U,X13)& agent(U,X13,X12)& patient(U,X13,X11)& present(U,X13)& nonreflexive(U,X13)& wear(U,X13) ) )) )))& group(U,X4)& (! [X14] :( member(U,X14,X4)=> ( coat(U,X14)& black(U,X14)& cheap(U,X14) ) ))& wheel(U,X6)& state(U,X5)& be(U,X5,V,X6)& behind(U,X6,X6) ) )) ))),
% 0.15/0.52 inference(negated_conjecture,[status(cth)],[f72])).
% 0.15/0.52 fof(f120,plain,(
% 0.15/0.52 ![U,V]: (~man(U,V)|male(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.15/0.52 fof(f121,plain,(
% 0.15/0.52 ![X0,X1]: (~man(X0,X1)|male(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f120])).
% 0.15/0.52 fof(f148,plain,(
% 0.15/0.52 ![U,V]: (~object(U,V)|unisex(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.15/0.52 fof(f149,plain,(
% 0.15/0.52 ![X0,X1]: (~object(X0,X1)|unisex(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f148])).
% 0.15/0.52 fof(f162,plain,(
% 0.15/0.52 ![U,V]: (~artifact(U,V)|object(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.15/0.52 fof(f163,plain,(
% 0.15/0.52 ![X0,X1]: (~artifact(X0,X1)|object(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f162])).
% 0.15/0.52 fof(f164,plain,(
% 0.15/0.52 ![U,V]: (~instrumentality(U,V)|artifact(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.15/0.52 fof(f165,plain,(
% 0.15/0.52 ![X0,X1]: (~instrumentality(X0,X1)|artifact(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f164])).
% 0.15/0.52 fof(f166,plain,(
% 0.15/0.52 ![U,V]: (~device(U,V)|instrumentality(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.15/0.52 fof(f167,plain,(
% 0.15/0.52 ![X0,X1]: (~device(X0,X1)|instrumentality(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f166])).
% 0.15/0.52 fof(f168,plain,(
% 0.15/0.52 ![U,V]: (~wheel(U,V)|device(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.15/0.52 fof(f169,plain,(
% 0.15/0.52 ![X0,X1]: (~wheel(X0,X1)|device(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f168])).
% 0.15/0.52 fof(f198,plain,(
% 0.15/0.52 ![U,V]: (~unisex(U,V)|~male(U,V))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.15/0.52 fof(f199,plain,(
% 0.15/0.52 ![X0,X1]: (~unisex(X0,X1)|~male(X0,X1))),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f198])).
% 0.15/0.52 fof(f224,plain,(
% 0.15/0.52 ![U,V,W,X]: (~be(U,V,W,X)|W=X)),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.15/0.52 fof(f225,plain,(
% 0.15/0.52 ![W,X]: ((![U,V]: ~be(U,V,W,X))|W=X)),
% 0.15/0.52 inference(miniscoping,[status(thm)],[f224])).
% 0.15/0.52 fof(f226,plain,(
% 0.15/0.52 ![X0,X1,X2,X3]: (~be(X0,X1,X2,X3)|X2=X3)),
% 0.15/0.52 inference(cnf_transformation,[status(thm)],[f225])).
% 0.15/0.52 fof(f227,plain,(
% 0.15/0.52 ?[U]: (actual_world(U)&(?[V,W,X,Y,Z,X1,X2,X3,X4,X5,X6]: (((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,X))&chevy(U,Y))&white(U,Y))&dirty(U,Y))&old(U,Y))&of(U,Z,X1))&city(U,X1))&hollywood_placename(U,Z))&placename(U,Z))&street(U,X1))&lonely(U,X1))&event(U,X2))&agent(U,X2,Y))&present(U,X2))&barrel(U,X2))&down(U,X2,X1))&in(U,X2,X1))&(![X7]: (~member(U,X7,X3)|(?[X8,X9]: ((state(U,X8)&be(U,X8,X7,X9))&in(U,X9,X))))))&two(U,X3))&group(U,X3))&(![X10]: (~member(U,X10,X3)|(fellow(U,X10)&young(U,X10)))))&(![X11]: (~member(U,X11,X4)|(![X12]: (~member(U,X12,X3)|(?[X13]: (((((event(U,X13)&agent(U,X13,X12))&patient(U,X13,X11))&present(U,X13))&nonreflexive(U,X13))&wear(U,X13))))))))&group(U,X4))&(![X14]: (~member(U,X14,X4)|((coat(U,X14)&black(U,X14))&cheap(U,X14)))))&wheel(U,X6))&state(U,X5))&be(U,X5,V,X6))&behind(U,X6,X6))))),
% 0.15/0.52 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.15/0.52 fof(f228,plain,(
% 0.15/0.52 ?[U]: (actual_world(U)&(?[X6]: ((?[V,X5]: ((((?[X4]: (((?[X3]: (((((?[X]: ((?[X1,X2]: (((((?[Y]: (((((?[Z]: ((((((((((?[W]: (((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W)))&frontseat(U,X))&chevy(U,Y))&white(U,Y))&dirty(U,Y))&old(U,Y))&of(U,Z,X1))&city(U,X1))&hollywood_placename(U,Z))&placename(U,Z)))&street(U,X1))&lonely(U,X1))&event(U,X2))&agent(U,X2,Y)))&present(U,X2))&barrel(U,X2))&down(U,X2,X1))&in(U,X2,X1)))&(![X7]: (~member(U,X7,X3)|(?[X9]: ((?[X8]: (state(U,X8)&be(U,X8,X7,X9)))&in(U,X9,X)))))))&two(U,X3))&group(U,X3))&(![X10]: (~member(U,X10,X3)|(fellow(U,X10)&young(U,X10)))))&(![X11]: (~member(U,X11,X4)|(![X12]: (~member(U,X12,X3)|(?[X13]: (((((event(U,X13)&agent(U,X13,X12))&patient(U,X13,X11))&present(U,X13))&nonreflexive(U,X13))&wear(U,X13)))))))))&group(U,X4))&(![X14]: (~member(U,X14,X4)|((coat(U,X14)&black(U,X14))&cheap(U,X14))))))&wheel(U,X6))&state(U,X5))&be(U,X5,V,X6)))&behind(U,X6,X6))))),
% 0.15/0.52 inference(miniscoping,[status(thm)],[f227])).
% 0.15/0.52 fof(f229,plain,(
% 0.15/0.52 (actual_world(sK3_skl)&(((((((((((((((((((((((((((((((of(sK3_skl,sK14_skl,sK5_skl)&man(sK3_skl,sK5_skl))&jules_forename(sK3_skl,sK14_skl))&forename(sK3_skl,sK14_skl))&frontseat(sK3_skl,sK9_skl))&chevy(sK3_skl,sK12_skl))&white(sK3_skl,sK12_skl))&dirty(sK3_skl,sK12_skl))&old(sK3_skl,sK12_skl))&of(sK3_skl,sK13_skl,sK10_skl))&city(sK3_skl,sK10_skl))&hollywood_placename(sK3_skl,sK13_skl))&placename(sK3_skl,sK13_skl))&street(sK3_skl,sK10_skl))&lonely(sK3_skl,sK10_skl))&event(sK3_skl,sK11_skl))&agent(sK3_skl,sK11_skl,sK12_skl))&present(sK3_skl,sK11_skl))&barrel(sK3_skl,sK11_skl))&down(sK3_skl,sK11_skl,sK10_skl))&in(sK3_skl,sK11_skl,sK10_skl))&(![X7]: (~member(sK3_skl,X7,sK8_skl)|((state(sK3_skl,sK16_skl(X7))&be(sK3_skl,sK16_skl(X7),X7,sK15_skl(X7)))&in(sK3_skl,sK15_skl(X7),sK9_skl)))))&two(sK3_skl,sK8_skl))&group(sK3_skl,sK8_skl))&(![X10]: (~member(sK3_skl,X10,sK8_skl)|(fellow(sK3_skl,X10)&young(sK3_skl,X10)))))&(![X11]: (~member(sK3_skl,X11,sK7_skl)|(![X12]: (~member(sK3_skl,X12,sK8_skl)|(((((event(sK3_skl,sK17_skl(X12,X11))&agent(sK3_skl,sK17_skl(X12,X11),X12))&patient(sK3_skl,sK17_skl(X12,X11),X11))&present(sK3_skl,sK17_skl(X12,X11)))&nonreflexive(sK3_skl,sK17_skl(X12,X11)))&wear(sK3_skl,sK17_skl(X12,X11))))))))&group(sK3_skl,sK7_skl))&(![X14]: (~member(sK3_skl,X14,sK7_skl)|((coat(sK3_skl,X14)&black(sK3_skl,X14))&cheap(sK3_skl,X14)))))&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.15/0.53 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,sK17_skl]),skolemize(U,sK3_skl),skolemize(X6,sK4_skl),skolemize(V,sK5_skl),skolemize(X5,sK6_skl),skolemize(X4,sK7_skl),skolemize(X3,sK8_skl),skolemize(X,sK9_skl),skolemize(X1,sK10_skl),skolemize(X2,sK11_skl),skolemize(Y,sK12_skl),skolemize(Z,sK13_skl),skolemize(W,sK14_skl),skolemize(X9,sK15_skl(X7)),skolemize(X8,sK16_skl(X7)),skolemize(X13,sK17_skl(X12,X11))],[f228])).
% 0.15/0.53 fof(f232,plain,(
% 0.15/0.53 man(sK3_skl,sK5_skl)),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f229])).
% 0.15/0.53 fof(f269,plain,(
% 0.15/0.53 wheel(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f229])).
% 0.15/0.53 fof(f271,plain,(
% 0.15/0.53 be(sK3_skl,sK6_skl,sK5_skl,sK4_skl)),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f229])).
% 0.15/0.53 fof(f285,plain,(
% 0.15/0.53 male(sK3_skl,sK5_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f121,f232])).
% 0.15/0.53 fof(f286,plain,(
% 0.15/0.53 device(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f169,f269])).
% 0.15/0.53 fof(f310,plain,(
% 0.15/0.53 instrumentality(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f167,f286])).
% 0.15/0.53 fof(f332,plain,(
% 0.15/0.53 sK5_skl=sK4_skl),
% 0.15/0.53 inference(resolution,[status(thm)],[f271,f226])).
% 0.15/0.53 fof(f338,plain,(
% 0.15/0.53 male(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(backward_demodulation,[status(thm)],[f332,f285])).
% 0.15/0.53 fof(f351,plain,(
% 0.15/0.53 artifact(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f310,f165])).
% 0.15/0.53 fof(f370,plain,(
% 0.15/0.53 ~unisex(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f338,f199])).
% 0.15/0.53 fof(f425,plain,(
% 0.15/0.53 object(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f351,f163])).
% 0.15/0.53 fof(f462,plain,(
% 0.15/0.53 unisex(sK3_skl,sK4_skl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f425,f149])).
% 0.15/0.53 fof(f463,plain,(
% 0.15/0.53 $false),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f462,f370])).
% 0.15/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.58 % Elapsed time: 0.103109 seconds
% 0.21/0.58 % CPU time: 0.128751 seconds
% 0.21/0.58 % Total memory used: 13.798 MB
% 0.21/0.58 % Net memory used: 13.783 MB
%------------------------------------------------------------------------------