%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP141+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 : n016.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:46 PM UTC 2026
% Result : Theorem 0.16s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP141+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n016.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 01:48:07 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.48 % Refutation found
% 0.16/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.48 fof(f1,axiom,(
% 0.16/0.48 (! [U,V] :( furniture(U,V)=> instrumentality(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f2,axiom,(
% 0.16/0.48 (! [U,V] :( seat(U,V)=> furniture(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f3,axiom,(
% 0.16/0.48 (! [U,V] :( frontseat(U,V)=> seat(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f18,axiom,(
% 0.16/0.48 (! [U,V] :( object(U,V)=> nonliving(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f20,axiom,(
% 0.16/0.48 (! [U,V] :( artifact(U,V)=> object(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f21,axiom,(
% 0.16/0.48 (! [U,V] :( instrumentality(U,V)=> artifact(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f40,axiom,(
% 0.16/0.48 (! [U,V] :( organism(U,V)=> living(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f47,axiom,(
% 0.16/0.48 (! [U,V] :( human_person(U,V)=> organism(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f48,axiom,(
% 0.16/0.48 (! [U,V] :( man(U,V)=> human_person(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f49,axiom,(
% 0.16/0.48 (! [U,V] :( fellow(U,V)=> man(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f53,axiom,(
% 0.16/0.48 (! [U,V] :( nonliving(U,V)=> ~ living(U,V) ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f59,axiom,(
% 0.16/0.48 (! [U,V,W,X] :( be(U,V,W,X)=> W = X ) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f60,axiom,(
% 0.16/0.48 (! [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.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f62,conjecture,(
% 0.16/0.48 ~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z] :( chevy(U,V)& white(U,V)& dirty(U,V)& old(U,V)& of(U,W,X)& city(U,X)& hollywood_placename(U,W)& placename(U,W)& street(U,X)& lonely(U,X)& event(U,Y)& agent(U,Y,V)& present(U,Y)& barrel(U,Y)& down(U,Y,X)& in(U,Y,X)& (! [X1] :( member(U,X1,Z)=> (? [X2,X3] :( frontseat(U,X3)& state(U,X2)& be(U,X2,X1,X3)& in(U,X3,X3) ) )))& two(U,Z)& group(U,Z)& (! [X4] :( member(U,X4,Z)=> ( fellow(U,X4)& young(U,X4) ) ) )) )) )),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f63,negated_conjecture,(
% 0.16/0.48 ~(~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z] :( chevy(U,V)& white(U,V)& dirty(U,V)& old(U,V)& of(U,W,X)& city(U,X)& hollywood_placename(U,W)& placename(U,W)& street(U,X)& lonely(U,X)& event(U,Y)& agent(U,Y,V)& present(U,Y)& barrel(U,Y)& down(U,Y,X)& in(U,Y,X)& (! [X1] :( member(U,X1,Z)=> (? [X2,X3] :( frontseat(U,X3)& state(U,X2)& be(U,X2,X1,X3)& in(U,X3,X3) ) )))& two(U,Z)& group(U,Z)& (! [X4] :( member(U,X4,Z)=> ( fellow(U,X4)& young(U,X4) ) ) )) )) ))),
% 0.16/0.48 inference(negated_conjecture,[status(cth)],[f62])).
% 0.16/0.48 fof(f64,plain,(
% 0.16/0.48 ![U,V]: (~furniture(U,V)|instrumentality(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.16/0.48 fof(f65,plain,(
% 0.16/0.48 ![X0,X1]: (~furniture(X0,X1)|instrumentality(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f64])).
% 0.16/0.48 fof(f66,plain,(
% 0.16/0.48 ![U,V]: (~seat(U,V)|furniture(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/0.48 fof(f67,plain,(
% 0.16/0.48 ![X0,X1]: (~seat(X0,X1)|furniture(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f66])).
% 0.16/0.48 fof(f68,plain,(
% 0.16/0.48 ![U,V]: (~frontseat(U,V)|seat(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.16/0.48 fof(f69,plain,(
% 0.16/0.48 ![X0,X1]: (~frontseat(X0,X1)|seat(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f68])).
% 0.16/0.48 fof(f98,plain,(
% 0.16/0.48 ![U,V]: (~object(U,V)|nonliving(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.16/0.48 fof(f99,plain,(
% 0.16/0.48 ![X0,X1]: (~object(X0,X1)|nonliving(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f98])).
% 0.16/0.48 fof(f102,plain,(
% 0.16/0.48 ![U,V]: (~artifact(U,V)|object(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.16/0.48 fof(f103,plain,(
% 0.16/0.48 ![X0,X1]: (~artifact(X0,X1)|object(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f102])).
% 0.16/0.48 fof(f104,plain,(
% 0.16/0.48 ![U,V]: (~instrumentality(U,V)|artifact(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.16/0.48 fof(f105,plain,(
% 0.16/0.48 ![X0,X1]: (~instrumentality(X0,X1)|artifact(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f104])).
% 0.16/0.48 fof(f142,plain,(
% 0.16/0.48 ![U,V]: (~organism(U,V)|living(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.16/0.48 fof(f143,plain,(
% 0.16/0.48 ![X0,X1]: (~organism(X0,X1)|living(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f142])).
% 0.16/0.48 fof(f156,plain,(
% 0.16/0.48 ![U,V]: (~human_person(U,V)|organism(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.16/0.48 fof(f157,plain,(
% 0.16/0.48 ![X0,X1]: (~human_person(X0,X1)|organism(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f156])).
% 0.16/0.48 fof(f158,plain,(
% 0.16/0.48 ![U,V]: (~man(U,V)|human_person(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.16/0.48 fof(f159,plain,(
% 0.16/0.48 ![X0,X1]: (~man(X0,X1)|human_person(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f158])).
% 0.16/0.48 fof(f160,plain,(
% 0.16/0.48 ![U,V]: (~fellow(U,V)|man(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.16/0.48 fof(f161,plain,(
% 0.16/0.48 ![X0,X1]: (~fellow(X0,X1)|man(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f160])).
% 0.16/0.48 fof(f168,plain,(
% 0.16/0.48 ![U,V]: (~nonliving(U,V)|~living(U,V))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.16/0.48 fof(f169,plain,(
% 0.16/0.48 ![X0,X1]: (~nonliving(X0,X1)|~living(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f168])).
% 0.16/0.48 fof(f180,plain,(
% 0.16/0.48 ![U,V,W,X]: (~be(U,V,W,X)|W=X)),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.16/0.48 fof(f181,plain,(
% 0.16/0.48 ![W,X]: ((![U,V]: ~be(U,V,W,X))|W=X)),
% 0.16/0.48 inference(miniscoping,[status(thm)],[f180])).
% 0.16/0.48 fof(f182,plain,(
% 0.16/0.48 ![X0,X1,X2,X3]: (~be(X0,X1,X2,X3)|X2=X3)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f181])).
% 0.16/0.48 fof(f183,plain,(
% 0.16/0.48 ![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.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.16/0.48 fof(f184,plain,(
% 0.16/0.48 ![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.16/0.48 inference(NNF_transformation,[status(thm)],[f183])).
% 0.16/0.48 fof(f185,plain,(
% 0.16/0.48 (![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.16/0.48 inference(miniscoping,[status(thm)],[f184])).
% 0.16/0.48 fof(f186,plain,(
% 0.16/0.48 (![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.16/0.48 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.16/0.48 fof(f187,plain,(
% 0.16/0.48 ![X0,X1]: (~two(X0,X1)|member(X0,sK0_skl(X1,X0),X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f186])).
% 0.16/0.48 fof(f196,plain,(
% 0.16/0.48 ?[U]: (actual_world(U)&(?[V,W,X,Y,Z]: (((((((((((((((((((chevy(U,V)&white(U,V))&dirty(U,V))&old(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,V))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,X))&(![X1]: (~member(U,X1,Z)|(?[X2,X3]: (((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3))&in(U,X3,X3))))))&two(U,Z))&group(U,Z))&(![X4]: (~member(U,X4,Z)|(fellow(U,X4)&young(U,X4)))))))),
% 0.16/0.48 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.16/0.48 fof(f197,plain,(
% 0.16/0.48 ?[U]: (actual_world(U)&(?[Z]: (((((?[X,Y]: (((((?[V]: (((((?[W]: (((((((chevy(U,V)&white(U,V))&dirty(U,V))&old(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W)))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,V)))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,X)))&(![X1]: (~member(U,X1,Z)|(?[X3]: ((?[X2]: ((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3)))&in(U,X3,X3))))))&two(U,Z))&group(U,Z))&(![X4]: (~member(U,X4,Z)|(fellow(U,X4)&young(U,X4)))))))),
% 0.16/0.48 inference(miniscoping,[status(thm)],[f196])).
% 0.16/0.48 fof(f198,plain,(
% 0.16/0.48 (actual_world(sK3_skl)&(((((((((((((((((((chevy(sK3_skl,sK7_skl)&white(sK3_skl,sK7_skl))&dirty(sK3_skl,sK7_skl))&old(sK3_skl,sK7_skl))&of(sK3_skl,sK8_skl,sK5_skl))&city(sK3_skl,sK5_skl))&hollywood_placename(sK3_skl,sK8_skl))&placename(sK3_skl,sK8_skl))&street(sK3_skl,sK5_skl))&lonely(sK3_skl,sK5_skl))&event(sK3_skl,sK6_skl))&agent(sK3_skl,sK6_skl,sK7_skl))&present(sK3_skl,sK6_skl))&barrel(sK3_skl,sK6_skl))&down(sK3_skl,sK6_skl,sK5_skl))&in(sK3_skl,sK6_skl,sK5_skl))&(![X1]: (~member(sK3_skl,X1,sK4_skl)|(((frontseat(sK3_skl,sK9_skl(X1))&state(sK3_skl,sK10_skl(X1)))&be(sK3_skl,sK10_skl(X1),X1,sK9_skl(X1)))&in(sK3_skl,sK9_skl(X1),sK9_skl(X1))))))&two(sK3_skl,sK4_skl))&group(sK3_skl,sK4_skl))&(![X4]: (~member(sK3_skl,X4,sK4_skl)|(fellow(sK3_skl,X4)&young(sK3_skl,X4))))))),
% 0.16/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(U,sK3_skl),skolemize(Z,sK4_skl),skolemize(X,sK5_skl),skolemize(Y,sK6_skl),skolemize(V,sK7_skl),skolemize(W,sK8_skl),skolemize(X3,sK9_skl(X1)),skolemize(X2,sK10_skl(X1))],[f197])).
% 0.16/0.48 fof(f216,plain,(
% 0.16/0.48 ![X0]: (~member(sK3_skl,X0,sK4_skl)|frontseat(sK3_skl,sK9_skl(X0)))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f198])).
% 0.16/0.48 fof(f218,plain,(
% 0.16/0.48 ![X0]: (~member(sK3_skl,X0,sK4_skl)|be(sK3_skl,sK10_skl(X0),X0,sK9_skl(X0)))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f198])).
% 0.16/0.48 fof(f220,plain,(
% 0.16/0.48 two(sK3_skl,sK4_skl)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f198])).
% 0.16/0.48 fof(f222,plain,(
% 0.16/0.48 ![X0]: (~member(sK3_skl,X0,sK4_skl)|fellow(sK3_skl,X0))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f198])).
% 0.16/0.48 fof(f286,plain,(
% 0.16/0.48 member(sK3_skl,sK0_skl(sK4_skl,sK3_skl),sK4_skl)),
% 0.16/0.48 inference(resolution,[status(thm)],[f187,f220])).
% 0.16/0.48 fof(f289,plain,(
% 0.16/0.48 be(sK3_skl,sK10_skl(sK0_skl(sK4_skl,sK3_skl)),sK0_skl(sK4_skl,sK3_skl),sK9_skl(sK0_skl(sK4_skl,sK3_skl)))),
% 0.16/0.48 inference(resolution,[status(thm)],[f286,f218])).
% 0.16/0.48 fof(f291,plain,(
% 0.16/0.48 frontseat(sK3_skl,sK9_skl(sK0_skl(sK4_skl,sK3_skl)))),
% 0.16/0.48 inference(resolution,[status(thm)],[f286,f216])).
% 0.16/0.48 fof(f293,plain,(
% 0.16/0.48 fellow(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f286,f222])).
% 0.16/0.48 fof(f296,plain,(
% 0.16/0.48 man(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f293,f161])).
% 0.16/0.48 fof(f297,plain,(
% 0.16/0.48 human_person(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f296,f159])).
% 0.16/0.48 fof(f306,plain,(
% 0.16/0.48 organism(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f297,f157])).
% 0.16/0.48 fof(f313,plain,(
% 0.16/0.48 living(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f306,f143])).
% 0.16/0.48 fof(f319,plain,(
% 0.16/0.48 sK0_skl(sK4_skl,sK3_skl)=sK9_skl(sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f289,f182])).
% 0.16/0.48 fof(f335,plain,(
% 0.16/0.48 seat(sK3_skl,sK9_skl(sK0_skl(sK4_skl,sK3_skl)))),
% 0.16/0.48 inference(resolution,[status(thm)],[f291,f69])).
% 0.16/0.48 fof(f353,plain,(
% 0.16/0.48 seat(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(backward_demodulation,[status(thm)],[f319,f335])).
% 0.16/0.48 fof(f358,plain,(
% 0.16/0.48 furniture(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f353,f67])).
% 0.16/0.48 fof(f360,plain,(
% 0.16/0.48 instrumentality(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f358,f65])).
% 0.16/0.48 fof(f361,plain,(
% 0.16/0.48 artifact(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f360,f105])).
% 0.16/0.48 fof(f362,plain,(
% 0.16/0.48 object(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f361,f103])).
% 0.16/0.48 fof(f364,plain,(
% 0.16/0.48 nonliving(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f362,f99])).
% 0.16/0.48 fof(f367,plain,(
% 0.16/0.48 ~living(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.16/0.48 inference(resolution,[status(thm)],[f364,f169])).
% 0.16/0.48 fof(f369,plain,(
% 0.16/0.48 $false),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f367,f313])).
% 0.16/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.56 % Elapsed time: 0.122604 seconds
% 0.16/0.56 % CPU time: 0.176415 seconds
% 0.16/0.56 % Total memory used: 32.408 MB
% 0.16/0.56 % Net memory used: 32.385 MB
%------------------------------------------------------------------------------