%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP145+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:32:47 PM UTC 2026
% Result : Theorem 0.03s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP145+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n026.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 01:46:21 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.03/0.37 % Drodi V4.1.1
% 0.03/0.40 % Refutation found
% 0.03/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.40 fof(f1,axiom,(
% 0.03/0.40 (! [U,V] :( furniture(U,V)=> instrumentality(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f2,axiom,(
% 0.03/0.40 (! [U,V] :( seat(U,V)=> furniture(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f3,axiom,(
% 0.03/0.40 (! [U,V] :( frontseat(U,V)=> seat(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f18,axiom,(
% 0.03/0.40 (! [U,V] :( object(U,V)=> nonliving(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f20,axiom,(
% 0.03/0.40 (! [U,V] :( artifact(U,V)=> object(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f21,axiom,(
% 0.03/0.40 (! [U,V] :( instrumentality(U,V)=> artifact(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f38,axiom,(
% 0.03/0.40 (! [U,V] :( human_person(U,V)=> animate(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f48,axiom,(
% 0.03/0.40 (! [U,V] :( man(U,V)=> human_person(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f49,axiom,(
% 0.03/0.40 (! [U,V] :( fellow(U,V)=> man(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f50,axiom,(
% 0.03/0.40 (! [U,V] :( animate(U,V)=> ~ nonliving(U,V) ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f59,axiom,(
% 0.03/0.40 (! [U,V,W,X] :( be(U,V,W,X)=> W = X ) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f60,axiom,(
% 0.03/0.40 (! [U,V] :( two(U,V)<=> (? [W] :( member(U,W,V)& (? [X] :( member(U,X,V)& X != W& (! [Y] :( member(U,Y,V)=> ( Y = X| Y = W ) ) )) )) )) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f62,conjecture,(
% 0.03/0.40 ~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1] :( of(U,W,V)& city(U,V)& hollywood_placename(U,W)& placename(U,W)& chevy(U,X)& white(U,X)& dirty(U,X)& old(U,X)& street(U,Y)& lonely(U,Y)& event(U,Z)& agent(U,Z,X)& present(U,Z)& barrel(U,Z)& down(U,Z,Y)& in(U,Z,V)& (! [X2] :( member(U,X2,X1)=> (? [X3,X4] :( frontseat(U,X4)& state(U,X3)& be(U,X3,X2,X4)& in(U,X4,X4) ) )))& two(U,X1)& group(U,X1)& (! [X5] :( member(U,X5,X1)=> ( fellow(U,X5)& young(U,X5) ) ) )) )) )),
% 0.03/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.40 fof(f63,negated_conjecture,(
% 0.03/0.40 ~(~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1] :( of(U,W,V)& city(U,V)& hollywood_placename(U,W)& placename(U,W)& chevy(U,X)& white(U,X)& dirty(U,X)& old(U,X)& street(U,Y)& lonely(U,Y)& event(U,Z)& agent(U,Z,X)& present(U,Z)& barrel(U,Z)& down(U,Z,Y)& in(U,Z,V)& (! [X2] :( member(U,X2,X1)=> (? [X3,X4] :( frontseat(U,X4)& state(U,X3)& be(U,X3,X2,X4)& in(U,X4,X4) ) )))& two(U,X1)& group(U,X1)& (! [X5] :( member(U,X5,X1)=> ( fellow(U,X5)& young(U,X5) ) ) )) )) ))),
% 0.03/0.40 inference(negated_conjecture,[status(cth)],[f62])).
% 0.03/0.40 fof(f64,plain,(
% 0.03/0.40 ![U,V]: (~furniture(U,V)|instrumentality(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.03/0.40 fof(f65,plain,(
% 0.03/0.40 ![X0,X1]: (~furniture(X0,X1)|instrumentality(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f64])).
% 0.03/0.40 fof(f66,plain,(
% 0.03/0.40 ![U,V]: (~seat(U,V)|furniture(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.03/0.40 fof(f67,plain,(
% 0.03/0.40 ![X0,X1]: (~seat(X0,X1)|furniture(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f66])).
% 0.03/0.40 fof(f68,plain,(
% 0.03/0.40 ![U,V]: (~frontseat(U,V)|seat(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.03/0.40 fof(f69,plain,(
% 0.03/0.40 ![X0,X1]: (~frontseat(X0,X1)|seat(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f68])).
% 0.03/0.40 fof(f98,plain,(
% 0.03/0.40 ![U,V]: (~object(U,V)|nonliving(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.03/0.40 fof(f99,plain,(
% 0.03/0.40 ![X0,X1]: (~object(X0,X1)|nonliving(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f98])).
% 0.03/0.40 fof(f102,plain,(
% 0.03/0.40 ![U,V]: (~artifact(U,V)|object(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.03/0.40 fof(f103,plain,(
% 0.03/0.40 ![X0,X1]: (~artifact(X0,X1)|object(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f102])).
% 0.03/0.40 fof(f104,plain,(
% 0.03/0.40 ![U,V]: (~instrumentality(U,V)|artifact(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.03/0.40 fof(f105,plain,(
% 0.03/0.40 ![X0,X1]: (~instrumentality(X0,X1)|artifact(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f104])).
% 0.03/0.40 fof(f138,plain,(
% 0.03/0.40 ![U,V]: (~human_person(U,V)|animate(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.03/0.40 fof(f139,plain,(
% 0.03/0.40 ![X0,X1]: (~human_person(X0,X1)|animate(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f138])).
% 0.03/0.40 fof(f158,plain,(
% 0.03/0.40 ![U,V]: (~man(U,V)|human_person(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.03/0.40 fof(f159,plain,(
% 0.03/0.40 ![X0,X1]: (~man(X0,X1)|human_person(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f158])).
% 0.03/0.40 fof(f160,plain,(
% 0.03/0.40 ![U,V]: (~fellow(U,V)|man(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.03/0.40 fof(f161,plain,(
% 0.03/0.40 ![X0,X1]: (~fellow(X0,X1)|man(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f160])).
% 0.03/0.40 fof(f162,plain,(
% 0.03/0.40 ![U,V]: (~animate(U,V)|~nonliving(U,V))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.03/0.40 fof(f163,plain,(
% 0.03/0.40 ![X0,X1]: (~animate(X0,X1)|~nonliving(X0,X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f162])).
% 0.03/0.40 fof(f180,plain,(
% 0.03/0.40 ![U,V,W,X]: (~be(U,V,W,X)|W=X)),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.03/0.40 fof(f181,plain,(
% 0.03/0.40 ![W,X]: ((![U,V]: ~be(U,V,W,X))|W=X)),
% 0.03/0.40 inference(miniscoping,[status(thm)],[f180])).
% 0.03/0.40 fof(f182,plain,(
% 0.03/0.40 ![X0,X1,X2,X3]: (~be(X0,X1,X2,X3)|X2=X3)),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.03/0.40 fof(f183,plain,(
% 0.03/0.40 ![U,V]: (two(U,V)<=>(?[W]: (member(U,W,V)&(?[X]: ((member(U,X,V)&~X=W)&(![Y]: (~member(U,Y,V)|(Y=X|Y=W))))))))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.03/0.40 fof(f184,plain,(
% 0.03/0.40 ![U,V]: ((~two(U,V)|(?[W]: (member(U,W,V)&(?[X]: ((member(U,X,V)&~X=W)&(![Y]: (~member(U,Y,V)|(Y=X|Y=W))))))))&(two(U,V)|(![W]: (~member(U,W,V)|(![X]: ((~member(U,X,V)|X=W)|(?[Y]: (member(U,Y,V)&(~Y=X&~Y=W)))))))))),
% 0.03/0.40 inference(NNF_transformation,[status(thm)],[f183])).
% 0.03/0.40 fof(f185,plain,(
% 0.03/0.40 (![U,V]: (~two(U,V)|(?[W]: (member(U,W,V)&(?[X]: ((member(U,X,V)&~X=W)&(![Y]: (~member(U,Y,V)|(Y=X|Y=W)))))))))&(![U,V]: (two(U,V)|(![W]: (~member(U,W,V)|(![X]: ((~member(U,X,V)|X=W)|(?[Y]: (member(U,Y,V)&(~Y=X&~Y=W)))))))))),
% 0.03/0.40 inference(miniscoping,[status(thm)],[f184])).
% 0.03/0.40 fof(f186,plain,(
% 0.03/0.40 (![U,V]: (~two(U,V)|(member(U,sK0_skl(V,U),V)&((member(U,sK1_skl(V,U),V)&~sK1_skl(V,U)=sK0_skl(V,U))&(![Y]: (~member(U,Y,V)|(Y=sK1_skl(V,U)|Y=sK0_skl(V,U))))))))&(![U,V]: (two(U,V)|(![W]: (~member(U,W,V)|(![X]: ((~member(U,X,V)|X=W)|(member(U,sK2_skl(X,W,V,U),V)&(~sK2_skl(X,W,V,U)=X&~sK2_skl(X,W,V,U)=W))))))))),
% 0.03/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(W,sK0_skl(V,U)),skolemize(X,sK1_skl(V,U)),skolemize(Y,sK2_skl(X,W,V,U))],[f185])).
% 0.03/0.40 fof(f187,plain,(
% 0.03/0.40 ![X0,X1]: (~two(X0,X1)|member(X0,sK0_skl(X1,X0),X1))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f186])).
% 0.03/0.40 fof(f196,plain,(
% 0.03/0.40 ?[U]: (actual_world(U)&(?[V,W,X,Y,Z,X1]: (((((((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V))&(![X2]: (~member(U,X2,X1)|(?[X3,X4]: (((frontseat(U,X4)&state(U,X3))&be(U,X3,X2,X4))&in(U,X4,X4))))))&two(U,X1))&group(U,X1))&(![X5]: (~member(U,X5,X1)|(fellow(U,X5)&young(U,X5)))))))),
% 0.03/0.40 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.03/0.40 fof(f197,plain,(
% 0.03/0.40 ?[U]: (actual_world(U)&(?[X1]: (((((?[V,Z]: ((?[Y]: ((((?[X]: (((((((((?[W]: (((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W)))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X)))&present(U,Z))&barrel(U,Z))&down(U,Z,Y)))&in(U,Z,V)))&(![X2]: (~member(U,X2,X1)|(?[X4]: ((?[X3]: ((frontseat(U,X4)&state(U,X3))&be(U,X3,X2,X4)))&in(U,X4,X4))))))&two(U,X1))&group(U,X1))&(![X5]: (~member(U,X5,X1)|(fellow(U,X5)&young(U,X5)))))))),
% 0.03/0.40 inference(miniscoping,[status(thm)],[f196])).
% 0.03/0.40 fof(f198,plain,(
% 0.03/0.40 (actual_world(sK3_skl)&(((((((((((((((((((of(sK3_skl,sK9_skl,sK5_skl)&city(sK3_skl,sK5_skl))&hollywood_placename(sK3_skl,sK9_skl))&placename(sK3_skl,sK9_skl))&chevy(sK3_skl,sK8_skl))&white(sK3_skl,sK8_skl))&dirty(sK3_skl,sK8_skl))&old(sK3_skl,sK8_skl))&street(sK3_skl,sK7_skl))&lonely(sK3_skl,sK7_skl))&event(sK3_skl,sK6_skl))&agent(sK3_skl,sK6_skl,sK8_skl))&present(sK3_skl,sK6_skl))&barrel(sK3_skl,sK6_skl))&down(sK3_skl,sK6_skl,sK7_skl))&in(sK3_skl,sK6_skl,sK5_skl))&(![X2]: (~member(sK3_skl,X2,sK4_skl)|(((frontseat(sK3_skl,sK10_skl(X2))&state(sK3_skl,sK11_skl(X2)))&be(sK3_skl,sK11_skl(X2),X2,sK10_skl(X2)))&in(sK3_skl,sK10_skl(X2),sK10_skl(X2))))))&two(sK3_skl,sK4_skl))&group(sK3_skl,sK4_skl))&(![X5]: (~member(sK3_skl,X5,sK4_skl)|(fellow(sK3_skl,X5)&young(sK3_skl,X5))))))),
% 0.03/0.40 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]),skolemize(U,sK3_skl),skolemize(X1,sK4_skl),skolemize(V,sK5_skl),skolemize(Z,sK6_skl),skolemize(Y,sK7_skl),skolemize(X,sK8_skl),skolemize(W,sK9_skl),skolemize(X4,sK10_skl(X2)),skolemize(X3,sK11_skl(X2))],[f197])).
% 0.03/0.40 fof(f216,plain,(
% 0.03/0.40 ![X0]: (~member(sK3_skl,X0,sK4_skl)|frontseat(sK3_skl,sK10_skl(X0)))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.40 fof(f218,plain,(
% 0.03/0.40 ![X0]: (~member(sK3_skl,X0,sK4_skl)|be(sK3_skl,sK11_skl(X0),X0,sK10_skl(X0)))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.40 fof(f220,plain,(
% 0.03/0.40 two(sK3_skl,sK4_skl)),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.40 fof(f222,plain,(
% 0.03/0.40 ![X0]: (~member(sK3_skl,X0,sK4_skl)|fellow(sK3_skl,X0))),
% 0.03/0.40 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.40 fof(f224,plain,(
% 0.03/0.40 ![X0,X1]: (~seat(X0,X1)|instrumentality(X0,X1))),
% 0.03/0.40 inference(resolution,[status(thm)],[f67,f65])).
% 0.03/0.40 fof(f268,plain,(
% 0.03/0.40 ![X0,X1]: (human_person(X0,X1)|~fellow(X0,X1))),
% 0.03/0.40 inference(resolution,[status(thm)],[f159,f161])).
% 0.03/0.40 fof(f273,plain,(
% 0.03/0.40 member(sK3_skl,sK0_skl(sK4_skl,sK3_skl),sK4_skl)),
% 0.03/0.40 inference(resolution,[status(thm)],[f187,f220])).
% 0.03/0.40 fof(f274,plain,(
% 0.03/0.40 be(sK3_skl,sK11_skl(sK0_skl(sK4_skl,sK3_skl)),sK0_skl(sK4_skl,sK3_skl),sK10_skl(sK0_skl(sK4_skl,sK3_skl)))),
% 0.03/0.40 inference(resolution,[status(thm)],[f273,f218])).
% 0.03/0.40 fof(f276,plain,(
% 0.03/0.40 fellow(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f273,f222])).
% 0.03/0.40 fof(f280,plain,(
% 0.03/0.40 human_person(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f276,f268])).
% 0.03/0.40 fof(f284,plain,(
% 0.03/0.40 animate(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f280,f139])).
% 0.03/0.40 fof(f288,plain,(
% 0.03/0.40 sK0_skl(sK4_skl,sK3_skl)=sK10_skl(sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f274,f182])).
% 0.03/0.40 fof(f293,plain,(
% 0.03/0.40 ![X0,X1]: (~seat(X0,X1)|artifact(X0,X1))),
% 0.03/0.40 inference(resolution,[status(thm)],[f224,f105])).
% 0.03/0.40 fof(f299,plain,(
% 0.03/0.40 ![X0,X1]: (artifact(X0,X1)|~frontseat(X0,X1))),
% 0.03/0.40 inference(resolution,[status(thm)],[f293,f69])).
% 0.03/0.40 fof(f308,plain,(
% 0.03/0.40 ~nonliving(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f284,f163])).
% 0.03/0.40 fof(f367,plain,(
% 0.03/0.40 ~member(sK3_skl,sK0_skl(sK4_skl,sK3_skl),sK4_skl)|frontseat(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(paramodulation,[status(thm)],[f288,f216])).
% 0.03/0.40 fof(f371,plain,(
% 0.03/0.40 frontseat(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(forward_subsumption_resolution,[status(thm)],[f367,f273])).
% 0.03/0.40 fof(f379,plain,(
% 0.03/0.40 artifact(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f371,f299])).
% 0.03/0.40 fof(f381,plain,(
% 0.03/0.40 object(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f379,f103])).
% 0.03/0.40 fof(f388,plain,(
% 0.03/0.40 nonliving(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.40 inference(resolution,[status(thm)],[f381,f99])).
% 0.03/0.40 fof(f391,plain,(
% 0.03/0.40 $false),
% 0.03/0.40 inference(forward_subsumption_resolution,[status(thm)],[f388,f308])).
% 0.03/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.43 % Elapsed time: 0.061074 seconds
% 0.03/0.43 % CPU time: 0.184631 seconds
% 0.03/0.43 % Total memory used: 84.097 MB
% 0.03/0.43 % Net memory used: 84.035 MB
%------------------------------------------------------------------------------