%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG106+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 02:05:22 PM UTC 2026
% Result : Theorem 75.26s 10.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG106+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:22:00 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 75.26/10.29 % Refutation found
% 75.26/10.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 75.26/10.29 % SZS output start CNFRefutation for theBenchmark
% 75.26/10.29 fof(f20,axiom,(
% 75.26/10.29 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 75.26/10.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 75.26/10.29 fof(f39,conjecture,(
% 75.26/10.29 ( (! [W0,W1,W2] :( ( ( (? [W3] :( aElement0(W3)& sdtasdt0(xc,W3) = W0 ))| aElementOf0(W0,slsdtgt0(xc)) )& ( (? [W3] :( aElement0(W3)& sdtasdt0(xc,W3) = W1 ))| aElementOf0(W1,slsdtgt0(xc)) )& aElement0(W2) )=> (? [W3] :( aElement0(W3)& sdtasdt0(xc,W3) = W0& (? [W4] :( aElement0(W4)& sdtasdt0(xc,W4) = W1& sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(W3,W4))& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(W3,W2))& (? [W5] :( aElement0(W5)& sdtasdt0(xc,W5) = sdtpldt0(W0,W1) ))& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))& (? [W5] :( aElement0(W5)& sdtasdt0(xc,W5) = sdtasdt0(W2,W0) ))& aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc)) ) )) )))=> ( ( aSet0(slsdtgt0(xc))& (! [W0] :( aElementOf0(W0,slsdtgt0(xc))<=> (? [W1] :( aElement0(W1)& sdtasdt0(xc,W1) = W0 ) )) ))=> ( (! [W0] :( aElementOf0(W0,slsdtgt0(xc))=> ( (! [W1] :( aElementOf0(W1,slsdtgt0(xc))=> aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),slsdtgt0(xc)) ) )) ))| aIdeal0(slsdtgt0(xc)) ) ) ) ),
% 75.26/10.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 75.26/10.29 fof(f40,negated_conjecture,(
% 75.26/10.29 ~(( (! [W0,W1,W2] :( ( ( (? [W3] :( aElement0(W3)& sdtasdt0(xc,W3) = W0 ))| aElementOf0(W0,slsdtgt0(xc)) )& ( (? [W3] :( aElement0(W3)& sdtasdt0(xc,W3) = W1 ))| aElementOf0(W1,slsdtgt0(xc)) )& aElement0(W2) )=> (? [W3] :( aElement0(W3)& sdtasdt0(xc,W3) = W0& (? [W4] :( aElement0(W4)& sdtasdt0(xc,W4) = W1& sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(W3,W4))& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(W3,W2))& (? [W5] :( aElement0(W5)& sdtasdt0(xc,W5) = sdtpldt0(W0,W1) ))& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))& (? [W5] :( aElement0(W5)& sdtasdt0(xc,W5) = sdtasdt0(W2,W0) ))& aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc)) ) )) )))=> ( ( aSet0(slsdtgt0(xc))& (! [W0] :( aElementOf0(W0,slsdtgt0(xc))<=> (? [W1] :( aElement0(W1)& sdtasdt0(xc,W1) = W0 ) )) ))=> ( (! [W0] :( aElementOf0(W0,slsdtgt0(xc))=> ( (! [W1] :( aElementOf0(W1,slsdtgt0(xc))=> aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),slsdtgt0(xc)) ) )) ))| aIdeal0(slsdtgt0(xc)) ) ) ) )),
% 75.26/10.29 inference(negated_conjecture,[status(cth)],[f39])).
% 75.26/10.29 fof(f84,plain,(
% 75.26/10.29 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 75.26/10.29 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 75.26/10.29 fof(f85,plain,(
% 75.26/10.29 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f84])).
% 75.26/10.29 fof(f192,plain,(
% 75.26/10.29 ((![W0,W1,W2]: (((((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W0))&~aElementOf0(W0,slsdtgt0(xc)))|((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W1))&~aElementOf0(W1,slsdtgt0(xc))))|~aElement0(W2))|(?[W3]: ((aElement0(W3)&sdtasdt0(xc,W3)=W0)&(?[W4]: (((((((aElement0(W4)&sdtasdt0(xc,W4)=W1)&sdtpldt0(W0,W1)=sdtasdt0(xc,sdtpldt0(W3,W4)))&sdtasdt0(W2,W0)=sdtasdt0(xc,sdtasdt0(W3,W2)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtpldt0(W0,W1))))&aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtasdt0(W2,W0))))&aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))))))))&((aSet0(slsdtgt0(xc))&(![W0]: (aElementOf0(W0,slsdtgt0(xc))<=>(?[W1]: (aElement0(W1)&sdtasdt0(xc,W1)=W0)))))&((?[W0]: (aElementOf0(W0,slsdtgt0(xc))&((?[W1]: (aElementOf0(W1,slsdtgt0(xc))&~aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),slsdtgt0(xc)))))))&~aIdeal0(slsdtgt0(xc)))))),
% 75.26/10.29 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 75.26/10.29 fof(f193,definition,(
% 75.26/10.29 ![W0,W1,W2]: (sP3_prd(W2,W1,W0)<=>((((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W0))&~aElementOf0(W0,slsdtgt0(xc)))|((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W1))&~aElementOf0(W1,slsdtgt0(xc))))|~aElement0(W2)))),
% 75.26/10.29 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 75.26/10.29 fof(f194,definition,(
% 75.26/10.29 ![W0,W1]: (sP4_prd(W1,W0)<=>(aElementOf0(W1,slsdtgt0(xc))&~aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))))),
% 75.26/10.29 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 75.26/10.29 fof(f195,plain,(
% 75.26/10.29 (![W0,W1,W2]: (sP3_prd(W2,W1,W0)|(?[W3]: ((aElement0(W3)&sdtasdt0(xc,W3)=W0)&(?[W4]: (((((((aElement0(W4)&sdtasdt0(xc,W4)=W1)&sdtpldt0(W0,W1)=sdtasdt0(xc,sdtpldt0(W3,W4)))&sdtasdt0(W2,W0)=sdtasdt0(xc,sdtasdt0(W3,W2)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtpldt0(W0,W1))))&aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtasdt0(W2,W0))))&aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))))))))&((aSet0(slsdtgt0(xc))&(![W0]: (aElementOf0(W0,slsdtgt0(xc))<=>(?[W1]: (aElement0(W1)&sdtasdt0(xc,W1)=W0)))))&((?[W0]: (aElementOf0(W0,slsdtgt0(xc))&((?[W1]: sP4_prd(W1,W0))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),slsdtgt0(xc)))))))&~aIdeal0(slsdtgt0(xc))))),
% 75.26/10.29 inference(formula_renaming,[status(thm)],[f192,f194,f193])).
% 75.26/10.29 fof(f196,plain,(
% 75.26/10.29 (![W0,W1,W2]: (sP3_prd(W2,W1,W0)|(?[W3]: ((aElement0(W3)&sdtasdt0(xc,W3)=W0)&(?[W4]: (((((((aElement0(W4)&sdtasdt0(xc,W4)=W1)&sdtpldt0(W0,W1)=sdtasdt0(xc,sdtpldt0(W3,W4)))&sdtasdt0(W2,W0)=sdtasdt0(xc,sdtasdt0(W3,W2)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtpldt0(W0,W1))))&aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtasdt0(W2,W0))))&aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))))))))&((aSet0(slsdtgt0(xc))&(![W0]: ((~aElementOf0(W0,slsdtgt0(xc))|(?[W1]: (aElement0(W1)&sdtasdt0(xc,W1)=W0)))&(aElementOf0(W0,slsdtgt0(xc))|(![W1]: (~aElement0(W1)|~sdtasdt0(xc,W1)=W0))))))&((?[W0]: (aElementOf0(W0,slsdtgt0(xc))&((?[W1]: sP4_prd(W1,W0))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),slsdtgt0(xc)))))))&~aIdeal0(slsdtgt0(xc))))),
% 75.26/10.29 inference(NNF_transformation,[status(thm)],[f195])).
% 75.26/10.29 fof(f197,plain,(
% 75.26/10.29 (![W0,W1,W2]: (sP3_prd(W2,W1,W0)|(?[W3]: ((aElement0(W3)&sdtasdt0(xc,W3)=W0)&((((((?[W4]: ((aElement0(W4)&sdtasdt0(xc,W4)=W1)&sdtpldt0(W0,W1)=sdtasdt0(xc,sdtpldt0(W3,W4))))&sdtasdt0(W2,W0)=sdtasdt0(xc,sdtasdt0(W3,W2)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtpldt0(W0,W1))))&aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))&(?[W5]: (aElement0(W5)&sdtasdt0(xc,W5)=sdtasdt0(W2,W0))))&aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc)))))))&((aSet0(slsdtgt0(xc))&((![W0]: (~aElementOf0(W0,slsdtgt0(xc))|(?[W1]: (aElement0(W1)&sdtasdt0(xc,W1)=W0))))&(![W0]: (aElementOf0(W0,slsdtgt0(xc))|(![W1]: (~aElement0(W1)|~sdtasdt0(xc,W1)=W0))))))&((?[W0]: (aElementOf0(W0,slsdtgt0(xc))&((?[W1]: sP4_prd(W1,W0))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),slsdtgt0(xc)))))))&~aIdeal0(slsdtgt0(xc))))),
% 75.26/10.29 inference(miniscoping,[status(thm)],[f196])).
% 75.26/10.29 fof(f198,plain,(
% 75.26/10.29 (![W0,W1,W2]: (sP3_prd(W2,W1,W0)|((aElement0(sK20_skl(W2,W1,W0))&sdtasdt0(xc,sK20_skl(W2,W1,W0))=W0)&(((((((aElement0(sK21_skl(W2,W1,W0))&sdtasdt0(xc,sK21_skl(W2,W1,W0))=W1)&sdtpldt0(W0,W1)=sdtasdt0(xc,sdtpldt0(sK20_skl(W2,W1,W0),sK21_skl(W2,W1,W0))))&sdtasdt0(W2,W0)=sdtasdt0(xc,sdtasdt0(sK20_skl(W2,W1,W0),W2)))&(aElement0(sK22_skl(W2,W1,W0))&sdtasdt0(xc,sK22_skl(W2,W1,W0))=sdtpldt0(W0,W1)))&aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))&(aElement0(sK23_skl(W2,W1,W0))&sdtasdt0(xc,sK23_skl(W2,W1,W0))=sdtasdt0(W2,W0)))&aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))))))&((aSet0(slsdtgt0(xc))&((![W0]: (~aElementOf0(W0,slsdtgt0(xc))|(aElement0(sK24_skl(W0))&sdtasdt0(xc,sK24_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,slsdtgt0(xc))|(![W1]: (~aElement0(W1)|~sdtasdt0(xc,W1)=W0))))))&((aElementOf0(sK25_skl,slsdtgt0(xc))&(sP4_prd(sK26_skl,sK25_skl)|(aElement0(sK27_skl)&~aElementOf0(sdtasdt0(sK27_skl,sK25_skl),slsdtgt0(xc)))))&~aIdeal0(slsdtgt0(xc))))),
% 75.26/10.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl]),skolemize(W3,sK20_skl(W2,W1,W0)),skolemize(W4,sK21_skl(W2,W1,W0)),skolemize(W5,sK22_skl(W2,W1,W0)),skolemize(W5,sK23_skl(W2,W1,W0)),skolemize(W1,sK24_skl(W0)),skolemize(W0,sK25_skl),skolemize(W1,sK26_skl),skolemize(W1,sK27_skl)],[f197])).
% 75.26/10.29 fof(f207,plain,(
% 75.26/10.29 ![X0,X1,X2]: (sP3_prd(X0,X1,X2)|aElementOf0(sdtpldt0(X2,X1),slsdtgt0(xc)))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f198])).
% 75.26/10.29 fof(f210,plain,(
% 75.26/10.29 ![X0,X1,X2]: (sP3_prd(X0,X1,X2)|aElementOf0(sdtasdt0(X0,X2),slsdtgt0(xc)))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f198])).
% 75.26/10.29 fof(f211,plain,(
% 75.26/10.29 aSet0(slsdtgt0(xc))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f198])).
% 75.26/10.29 fof(f215,plain,(
% 75.26/10.29 aElementOf0(sK25_skl,slsdtgt0(xc))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f198])).
% 75.26/10.29 fof(f216,plain,(
% 75.26/10.29 sP4_prd(sK26_skl,sK25_skl)|aElement0(sK27_skl)),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f198])).
% 75.26/10.29 fof(f217,plain,(
% 75.26/10.29 sP4_prd(sK26_skl,sK25_skl)|~aElementOf0(sdtasdt0(sK27_skl,sK25_skl),slsdtgt0(xc))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f198])).
% 75.26/10.29 fof(f236,plain,(
% 75.26/10.29 ![W0,W1,W2]: ((~sP3_prd(W2,W1,W0)|((((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W0))&~aElementOf0(W0,slsdtgt0(xc)))|((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W1))&~aElementOf0(W1,slsdtgt0(xc))))|~aElement0(W2)))&(sP3_prd(W2,W1,W0)|((((?[W3]: (aElement0(W3)&sdtasdt0(xc,W3)=W0))|aElementOf0(W0,slsdtgt0(xc)))&((?[W3]: (aElement0(W3)&sdtasdt0(xc,W3)=W1))|aElementOf0(W1,slsdtgt0(xc))))&aElement0(W2))))),
% 75.26/10.29 inference(NNF_transformation,[status(thm)],[f193])).
% 75.26/10.29 fof(f237,plain,(
% 75.26/10.29 (![W0,W1,W2]: (~sP3_prd(W2,W1,W0)|((((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W0))&~aElementOf0(W0,slsdtgt0(xc)))|((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W1))&~aElementOf0(W1,slsdtgt0(xc))))|~aElement0(W2))))&(![W0,W1,W2]: (sP3_prd(W2,W1,W0)|((((?[W3]: (aElement0(W3)&sdtasdt0(xc,W3)=W0))|aElementOf0(W0,slsdtgt0(xc)))&((?[W3]: (aElement0(W3)&sdtasdt0(xc,W3)=W1))|aElementOf0(W1,slsdtgt0(xc))))&aElement0(W2))))),
% 75.26/10.29 inference(miniscoping,[status(thm)],[f236])).
% 75.26/10.29 fof(f238,plain,(
% 75.26/10.29 (![W0,W1,W2]: (~sP3_prd(W2,W1,W0)|((((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W0))&~aElementOf0(W0,slsdtgt0(xc)))|((![W3]: (~aElement0(W3)|~sdtasdt0(xc,W3)=W1))&~aElementOf0(W1,slsdtgt0(xc))))|~aElement0(W2))))&(![W0,W1,W2]: (sP3_prd(W2,W1,W0)|((((aElement0(sK28_skl(W2,W1,W0))&sdtasdt0(xc,sK28_skl(W2,W1,W0))=W0)|aElementOf0(W0,slsdtgt0(xc)))&((aElement0(sK29_skl(W2,W1,W0))&sdtasdt0(xc,sK29_skl(W2,W1,W0))=W1)|aElementOf0(W1,slsdtgt0(xc))))&aElement0(W2))))),
% 75.26/10.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(W3,sK28_skl(W2,W1,W0)),skolemize(W3,sK29_skl(W2,W1,W0))],[f237])).
% 75.26/10.29 fof(f242,plain,(
% 75.26/10.29 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|~aElementOf0(X2,slsdtgt0(xc))|~aElementOf0(X1,slsdtgt0(xc))|~aElement0(X0))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f238])).
% 75.26/10.29 fof(f248,plain,(
% 75.26/10.29 ![W0,W1]: ((~sP4_prd(W1,W0)|(aElementOf0(W1,slsdtgt0(xc))&~aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))))&(sP4_prd(W1,W0)|(~aElementOf0(W1,slsdtgt0(xc))|aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))))),
% 75.26/10.29 inference(NNF_transformation,[status(thm)],[f194])).
% 75.26/10.29 fof(f249,plain,(
% 75.26/10.29 (![W0,W1]: (~sP4_prd(W1,W0)|(aElementOf0(W1,slsdtgt0(xc))&~aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))))&(![W0,W1]: (sP4_prd(W1,W0)|(~aElementOf0(W1,slsdtgt0(xc))|aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc)))))),
% 75.26/10.29 inference(miniscoping,[status(thm)],[f248])).
% 75.26/10.29 fof(f250,plain,(
% 75.26/10.29 ![X0,X1]: (~sP4_prd(X0,X1)|aElementOf0(X0,slsdtgt0(xc)))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f249])).
% 75.26/10.29 fof(f251,plain,(
% 75.26/10.29 ![X0,X1]: (~sP4_prd(X0,X1)|~aElementOf0(sdtpldt0(X1,X0),slsdtgt0(xc)))),
% 75.26/10.29 inference(cnf_transformation,[status(thm)],[f249])).
% 75.26/10.29 fof(f780,plain,(
% 75.26/10.29 ![X0]: (sP4_prd(sK26_skl,sK25_skl)|sP3_prd(sK27_skl,X0,sK25_skl))),
% 75.26/10.29 inference(resolution,[status(thm)],[f217,f210])).
% 75.26/10.29 fof(f847,plain,(
% 75.26/10.29 ![X0]: (~sP3_prd(X0,sK25_skl,sK25_skl)|~aElement0(X0))),
% 75.26/10.29 inference(resolution,[status(thm)],[f242,f215])).
% 75.26/10.29 fof(f848,plain,(
% 75.26/10.29 ![X0,X1]: (~sP3_prd(X0,X1,sK25_skl)|~aElementOf0(X1,slsdtgt0(xc))|~aElement0(X0))),
% 75.26/10.29 inference(resolution,[status(thm)],[f242,f215])).
% 75.26/10.29 fof(f1070,plain,(
% 75.26/10.29 ![X0,X1,X2]: (~sP4_prd(X0,X1)|sP3_prd(X2,X0,X1))),
% 75.26/10.29 inference(resolution,[status(thm)],[f251,f207])).
% 75.26/10.29 fof(f12418,plain,(
% 75.26/10.29 sP4_prd(sK26_skl,sK25_skl)|~aElement0(sK27_skl)),
% 75.26/10.29 inference(resolution,[status(thm)],[f780,f847])).
% 75.26/10.29 fof(f12420,plain,(
% 75.26/10.29 sP4_prd(sK26_skl,sK25_skl)),
% 75.26/10.29 inference(forward_subsumption_resolution,[status(thm)],[f12418,f216])).
% 75.26/10.29 fof(f12485,plain,(
% 75.26/10.29 ![X0]: (sP3_prd(X0,sK26_skl,sK25_skl))),
% 75.26/10.29 inference(resolution,[status(thm)],[f12420,f1070])).
% 78.20/10.34 fof(f12486,plain,(
% 78.20/10.34 aElementOf0(sK26_skl,slsdtgt0(xc))),
% 78.20/10.34 inference(resolution,[status(thm)],[f12420,f250])).
% 78.20/10.34 fof(f14294,plain,(
% 78.20/10.34 ~aSet0(slsdtgt0(xc))|aElement0(sK26_skl)),
% 78.20/10.34 inference(resolution,[status(thm)],[f12486,f85])).
% 78.20/10.34 fof(f14298,plain,(
% 78.20/10.34 aElement0(sK26_skl)),
% 78.20/10.34 inference(forward_subsumption_resolution,[status(thm)],[f14294,f211])).
% 78.20/10.34 fof(f16884,plain,(
% 78.20/10.34 ![X0]: (~sP3_prd(X0,sK26_skl,sK25_skl)|~aElement0(X0))),
% 78.20/10.34 inference(resolution,[status(thm)],[f848,f12486])).
% 78.20/10.34 fof(f16897,plain,(
% 78.20/10.34 ![X0]: (~aElement0(X0))),
% 78.20/10.34 inference(forward_subsumption_resolution,[status(thm)],[f16884,f12485])).
% 78.20/10.34 fof(f17077,plain,(
% 78.20/10.34 $false),
% 78.20/10.34 inference(backward_subsumption_resolution,[status(thm)],[f14298,f16897])).
% 78.20/10.34 % SZS output end CNFRefutation for theBenchmark.p
% 78.20/10.37 % Elapsed time: 9.990906 seconds
% 78.20/10.37 % CPU time: 78.623574 seconds
% 78.20/10.37 % Total memory used: 433.632 MB
% 78.20/10.37 % Net memory used: 386.748 MB
%------------------------------------------------------------------------------