%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG111+4 : 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 : n005.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:23 PM UTC 2026
% Result : Theorem 20.69s 3.17s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG111+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n005.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 04:20:34 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.50 % Drodi V4.1.1
% 20.69/3.17 % Refutation found
% 20.69/3.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.69/3.17 % SZS output start CNFRefutation for theBenchmark
% 20.69/3.17 fof(f45,conjecture,(
% 20.69/3.17 (! [W0] :( ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))& aElementOf0(W0,xI)& W0 != sz00 )=> ( (! [W1] :( ( ( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))| aElementOf0(W1,xI) )& W1 != sz00 )=> ( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))=> (? [W2] :( (? [W3,W4] :( aElementOf0(W3,slsdtgt0(xa))& aElementOf0(W4,slsdtgt0(xb))& sdtpldt0(W3,W4) = W2 ))& aElementOf0(W2,xI)& W2 != sz00& (! [W3] :( ( ( (? [W4,W5] :( aElementOf0(W4,slsdtgt0(xa))& aElementOf0(W5,slsdtgt0(xb))& sdtpldt0(W4,W5) = W3 ))| aElementOf0(W3,xI) )& W3 != sz00 )=> ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2)) ) )) )) ))=> (? [W1] :( ( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))| aElementOf0(W1,xI) )& W1 != sz00& (! [W2] :( ( (? [W3,W4] :( aElementOf0(W3,slsdtgt0(xa))& aElementOf0(W4,slsdtgt0(xb))& sdtpldt0(W3,W4) = W2 ))& aElementOf0(W2,xI)& W2 != sz00 )=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) ) )) )) ) )),
% 20.69/3.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.17 fof(f46,negated_conjecture,(
% 20.69/3.17 ~((! [W0] :( ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))& aElementOf0(W0,xI)& W0 != sz00 )=> ( (! [W1] :( ( ( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))| aElementOf0(W1,xI) )& W1 != sz00 )=> ( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))=> (? [W2] :( (? [W3,W4] :( aElementOf0(W3,slsdtgt0(xa))& aElementOf0(W4,slsdtgt0(xb))& sdtpldt0(W3,W4) = W2 ))& aElementOf0(W2,xI)& W2 != sz00& (! [W3] :( ( ( (? [W4,W5] :( aElementOf0(W4,slsdtgt0(xa))& aElementOf0(W5,slsdtgt0(xb))& sdtpldt0(W4,W5) = W3 ))| aElementOf0(W3,xI) )& W3 != sz00 )=> ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2)) ) )) )) ))=> (? [W1] :( ( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))| aElementOf0(W1,xI) )& W1 != sz00& (! [W2] :( ( (? [W3,W4] :( aElementOf0(W3,slsdtgt0(xa))& aElementOf0(W4,slsdtgt0(xb))& sdtpldt0(W3,W4) = W2 ))& aElementOf0(W2,xI)& W2 != sz00 )=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) ) )) )) ) ))),
% 20.69/3.17 inference(negated_conjecture,[status(cth)],[f45])).
% 20.69/3.17 fof(f266,plain,(
% 20.69/3.17 (?[W0]: ((((?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))&aElementOf0(W0,xI))&~W0=sz00)&((![W1]: ((((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00)|(~iLess0(sbrdtbr0(W1),sbrdtbr0(W0))|(?[W2]: ((((?[W3,W4]: ((aElementOf0(W3,slsdtgt0(xa))&aElementOf0(W4,slsdtgt0(xb)))&sdtpldt0(W3,W4)=W2))&aElementOf0(W2,xI))&~W2=sz00)&(![W3]: ((((![W4,W5]: ((~aElementOf0(W4,slsdtgt0(xa))|~aElementOf0(W5,slsdtgt0(xb)))|~sdtpldt0(W4,W5)=W3))&~aElementOf0(W3,xI))|W3=sz00)|~iLess0(sbrdtbr0(W3),sbrdtbr0(W2)))))))))&(![W1]: ((((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00)|(?[W2]: ((((?[W3,W4]: ((aElementOf0(W3,slsdtgt0(xa))&aElementOf0(W4,slsdtgt0(xb)))&sdtpldt0(W3,W4)=W2))&aElementOf0(W2,xI))&~W2=sz00)&iLess0(sbrdtbr0(W2),sbrdtbr0(W1)))))))))),
% 20.69/3.17 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 20.69/3.17 fof(f267,definition,(
% 20.69/3.17 ![W2]: (sP4_prd(W2)<=>((((?[W3,W4]: ((aElementOf0(W3,slsdtgt0(xa))&aElementOf0(W4,slsdtgt0(xb)))&sdtpldt0(W3,W4)=W2))&aElementOf0(W2,xI))&~W2=sz00)&(![W3]: ((((![W4,W5]: ((~aElementOf0(W4,slsdtgt0(xa))|~aElementOf0(W5,slsdtgt0(xb)))|~sdtpldt0(W4,W5)=W3))&~aElementOf0(W3,xI))|W3=sz00)|~iLess0(sbrdtbr0(W3),sbrdtbr0(W2))))))),
% 20.69/3.17 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 20.69/3.17 fof(f268,definition,(
% 20.69/3.17 ![W1]: (sP5_prd(W1)<=>(((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00))),
% 20.69/3.17 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 20.69/3.17 fof(f269,plain,(
% 20.69/3.17 ?[W0]: ((((?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))&aElementOf0(W0,xI))&~W0=sz00)&((![W1]: ((((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00)|(~iLess0(sbrdtbr0(W1),sbrdtbr0(W0))|(?[W2]: sP4_prd(W2)))))&(![W1]: (sP5_prd(W1)|(?[W2]: ((((?[W3,W4]: ((aElementOf0(W3,slsdtgt0(xa))&aElementOf0(W4,slsdtgt0(xb)))&sdtpldt0(W3,W4)=W2))&aElementOf0(W2,xI))&~W2=sz00)&iLess0(sbrdtbr0(W2),sbrdtbr0(W1))))))))),
% 20.69/3.17 inference(formula_renaming,[status(thm)],[f266,f268,f267])).
% 20.69/3.17 fof(f270,plain,(
% 20.69/3.17 (((((aElementOf0(sK37_skl,slsdtgt0(xa))&aElementOf0(sK38_skl,slsdtgt0(xb)))&sdtpldt0(sK37_skl,sK38_skl)=sK36_skl)&aElementOf0(sK36_skl,xI))&~sK36_skl=sz00)&((![W1]: ((((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00)|(~iLess0(sbrdtbr0(W1),sbrdtbr0(sK36_skl))|sP4_prd(sK39_skl(W1)))))&(![W1]: (sP5_prd(W1)|(((((aElementOf0(sK41_skl(W1),slsdtgt0(xa))&aElementOf0(sK42_skl(W1),slsdtgt0(xb)))&sdtpldt0(sK41_skl(W1),sK42_skl(W1))=sK40_skl(W1))&aElementOf0(sK40_skl(W1),xI))&~sK40_skl(W1)=sz00)&iLess0(sbrdtbr0(sK40_skl(W1)),sbrdtbr0(W1)))))))),
% 20.69/3.17 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl,sK38_skl,sK39_skl,sK40_skl,sK41_skl,sK42_skl]),skolemize(W0,sK36_skl),skolemize(W1,sK37_skl),skolemize(W2,sK38_skl),skolemize(W2,sK39_skl(W1)),skolemize(W2,sK40_skl(W1)),skolemize(W3,sK41_skl(W1)),skolemize(W4,sK42_skl(W1))],[f269])).
% 20.69/3.17 fof(f274,plain,(
% 20.69/3.17 aElementOf0(sK36_skl,xI)),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f270])).
% 20.69/3.17 fof(f275,plain,(
% 20.69/3.17 ~sK36_skl=sz00),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f270])).
% 20.69/3.17 fof(f277,plain,(
% 20.69/3.17 ![X0]: (~aElementOf0(X0,xI)|X0=sz00|~iLess0(sbrdtbr0(X0),sbrdtbr0(sK36_skl))|sP4_prd(sK39_skl(X0)))),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f270])).
% 20.69/3.17 fof(f281,plain,(
% 20.69/3.17 ![X0]: (sP5_prd(X0)|aElementOf0(sK40_skl(X0),xI))),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f270])).
% 20.69/3.17 fof(f282,plain,(
% 20.69/3.17 ![X0]: (sP5_prd(X0)|~sK40_skl(X0)=sz00)),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f270])).
% 20.69/3.17 fof(f283,plain,(
% 20.69/3.17 ![X0]: (sP5_prd(X0)|iLess0(sbrdtbr0(sK40_skl(X0)),sbrdtbr0(X0)))),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f270])).
% 20.69/3.17 fof(f312,plain,(
% 20.69/3.17 ![W2]: ((~sP4_prd(W2)|((((?[W3,W4]: ((aElementOf0(W3,slsdtgt0(xa))&aElementOf0(W4,slsdtgt0(xb)))&sdtpldt0(W3,W4)=W2))&aElementOf0(W2,xI))&~W2=sz00)&(![W3]: ((((![W4,W5]: ((~aElementOf0(W4,slsdtgt0(xa))|~aElementOf0(W5,slsdtgt0(xb)))|~sdtpldt0(W4,W5)=W3))&~aElementOf0(W3,xI))|W3=sz00)|~iLess0(sbrdtbr0(W3),sbrdtbr0(W2))))))&(sP4_prd(W2)|((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))|~aElementOf0(W2,xI))|W2=sz00)|(?[W3]: ((((?[W4,W5]: ((aElementOf0(W4,slsdtgt0(xa))&aElementOf0(W5,slsdtgt0(xb)))&sdtpldt0(W4,W5)=W3))|aElementOf0(W3,xI))&~W3=sz00)&iLess0(sbrdtbr0(W3),sbrdtbr0(W2)))))))),
% 20.69/3.17 inference(NNF_transformation,[status(thm)],[f267])).
% 20.69/3.17 fof(f313,plain,(
% 20.69/3.17 (![W2]: (~sP4_prd(W2)|((((?[W3,W4]: ((aElementOf0(W3,slsdtgt0(xa))&aElementOf0(W4,slsdtgt0(xb)))&sdtpldt0(W3,W4)=W2))&aElementOf0(W2,xI))&~W2=sz00)&(![W3]: ((((![W4,W5]: ((~aElementOf0(W4,slsdtgt0(xa))|~aElementOf0(W5,slsdtgt0(xb)))|~sdtpldt0(W4,W5)=W3))&~aElementOf0(W3,xI))|W3=sz00)|~iLess0(sbrdtbr0(W3),sbrdtbr0(W2)))))))&(![W2]: (sP4_prd(W2)|((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))|~aElementOf0(W2,xI))|W2=sz00)|(?[W3]: ((((?[W4,W5]: ((aElementOf0(W4,slsdtgt0(xa))&aElementOf0(W5,slsdtgt0(xb)))&sdtpldt0(W4,W5)=W3))|aElementOf0(W3,xI))&~W3=sz00)&iLess0(sbrdtbr0(W3),sbrdtbr0(W2)))))))),
% 20.69/3.17 inference(miniscoping,[status(thm)],[f312])).
% 20.69/3.17 fof(f314,plain,(
% 20.69/3.17 (![W2]: (~sP4_prd(W2)|(((((aElementOf0(sK44_skl(W2),slsdtgt0(xa))&aElementOf0(sK45_skl(W2),slsdtgt0(xb)))&sdtpldt0(sK44_skl(W2),sK45_skl(W2))=W2)&aElementOf0(W2,xI))&~W2=sz00)&(![W3]: ((((![W4,W5]: ((~aElementOf0(W4,slsdtgt0(xa))|~aElementOf0(W5,slsdtgt0(xb)))|~sdtpldt0(W4,W5)=W3))&~aElementOf0(W3,xI))|W3=sz00)|~iLess0(sbrdtbr0(W3),sbrdtbr0(W2)))))))&(![W2]: (sP4_prd(W2)|((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))|~aElementOf0(W2,xI))|W2=sz00)|(((((aElementOf0(sK47_skl(W2),slsdtgt0(xa))&aElementOf0(sK48_skl(W2),slsdtgt0(xb)))&sdtpldt0(sK47_skl(W2),sK48_skl(W2))=sK46_skl(W2))|aElementOf0(sK46_skl(W2),xI))&~sK46_skl(W2)=sz00)&iLess0(sbrdtbr0(sK46_skl(W2)),sbrdtbr0(W2))))))),
% 20.69/3.17 inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl,sK45_skl,sK46_skl,sK47_skl,sK48_skl]),skolemize(W3,sK44_skl(W2)),skolemize(W4,sK45_skl(W2)),skolemize(W3,sK46_skl(W2)),skolemize(W4,sK47_skl(W2)),skolemize(W5,sK48_skl(W2))],[f313])).
% 20.69/3.17 fof(f318,plain,(
% 20.69/3.17 ![X0]: (~sP4_prd(X0)|aElementOf0(X0,xI))),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f314])).
% 20.69/3.17 fof(f319,plain,(
% 20.69/3.17 ![X0]: (~sP4_prd(X0)|~X0=sz00)),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f314])).
% 20.69/3.17 fof(f321,plain,(
% 20.69/3.17 ![X0,X1]: (~sP4_prd(X0)|~aElementOf0(X1,xI)|X1=sz00|~iLess0(sbrdtbr0(X1),sbrdtbr0(X0)))),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f314])).
% 20.69/3.17 fof(f327,plain,(
% 20.69/3.17 ![W1]: ((~sP5_prd(W1)|(((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00))&(sP5_prd(W1)|(((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))|aElementOf0(W1,xI))&~W1=sz00)))),
% 20.69/3.17 inference(NNF_transformation,[status(thm)],[f268])).
% 20.69/3.17 fof(f328,plain,(
% 20.69/3.17 (![W1]: (~sP5_prd(W1)|(((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00)))&(![W1]: (sP5_prd(W1)|(((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))|aElementOf0(W1,xI))&~W1=sz00)))),
% 20.69/3.17 inference(miniscoping,[status(thm)],[f327])).
% 20.69/3.17 fof(f329,plain,(
% 20.69/3.17 (![W1]: (~sP5_prd(W1)|(((![W2,W3]: ((~aElementOf0(W2,slsdtgt0(xa))|~aElementOf0(W3,slsdtgt0(xb)))|~sdtpldt0(W2,W3)=W1))&~aElementOf0(W1,xI))|W1=sz00)))&(![W1]: (sP5_prd(W1)|((((aElementOf0(sK49_skl(W1),slsdtgt0(xa))&aElementOf0(sK50_skl(W1),slsdtgt0(xb)))&sdtpldt0(sK49_skl(W1),sK50_skl(W1))=W1)|aElementOf0(W1,xI))&~W1=sz00)))),
% 20.69/3.17 inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl]),skolemize(W2,sK49_skl(W1)),skolemize(W3,sK50_skl(W1))],[f328])).
% 20.69/3.17 fof(f331,plain,(
% 20.69/3.17 ![X0]: (~sP5_prd(X0)|~aElementOf0(X0,xI)|X0=sz00)),
% 20.69/3.17 inference(cnf_transformation,[status(thm)],[f329])).
% 20.69/3.17 fof(f403,plain,(
% 20.69/3.17 ~sP5_prd(sK36_skl)|sK36_skl=sz00),
% 20.69/3.17 inference(resolution,[status(thm)],[f331,f274])).
% 20.69/3.17 fof(f405,plain,(
% 20.69/3.17 ~sP5_prd(sK36_skl)),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f403,f275])).
% 20.69/3.17 fof(f666,plain,(
% 20.69/3.17 ~aElementOf0(sK40_skl(sK36_skl),xI)|sK40_skl(sK36_skl)=sz00|sP4_prd(sK39_skl(sK40_skl(sK36_skl)))|sP5_prd(sK36_skl)),
% 20.69/3.17 inference(resolution,[status(thm)],[f277,f283])).
% 20.69/3.17 fof(f667,plain,(
% 20.69/3.17 sK40_skl(sK36_skl)=sz00|sP4_prd(sK39_skl(sK40_skl(sK36_skl)))|sP5_prd(sK36_skl)),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f666,f281])).
% 20.69/3.17 fof(f821,plain,(
% 20.69/3.17 sP4_prd(sK39_skl(sK40_skl(sK36_skl)))|sP5_prd(sK36_skl)),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f667,f282])).
% 20.69/3.17 fof(f825,plain,(
% 20.69/3.17 sP5_prd(sK36_skl)|aElementOf0(sK39_skl(sK40_skl(sK36_skl)),xI)),
% 20.69/3.17 inference(resolution,[status(thm)],[f821,f318])).
% 20.69/3.17 fof(f826,plain,(
% 20.69/3.17 sP5_prd(sK36_skl)|~sK39_skl(sK40_skl(sK36_skl))=sz00),
% 20.69/3.17 inference(resolution,[status(thm)],[f821,f319])).
% 20.69/3.17 fof(f830,plain,(
% 20.69/3.17 aElementOf0(sK39_skl(sK40_skl(sK36_skl)),xI)),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f825,f405])).
% 20.69/3.17 fof(f831,plain,(
% 20.69/3.17 ~sK39_skl(sK40_skl(sK36_skl))=sz00),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f826,f405])).
% 20.69/3.17 fof(f832,plain,(
% 20.69/3.17 ~sP5_prd(sK39_skl(sK40_skl(sK36_skl)))|sK39_skl(sK40_skl(sK36_skl))=sz00),
% 20.69/3.17 inference(resolution,[status(thm)],[f830,f331])).
% 20.69/3.17 fof(f833,plain,(
% 20.69/3.17 ~sP5_prd(sK39_skl(sK40_skl(sK36_skl)))),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f832,f831])).
% 20.69/3.17 fof(f1237,plain,(
% 20.69/3.17 ![X0]: (~sP4_prd(X0)|~aElementOf0(sK40_skl(X0),xI)|sK40_skl(X0)=sz00|sP5_prd(X0))),
% 20.69/3.17 inference(resolution,[status(thm)],[f321,f283])).
% 20.69/3.17 fof(f1238,plain,(
% 20.69/3.17 ![X0]: (~sP4_prd(X0)|sK40_skl(X0)=sz00|sP5_prd(X0))),
% 20.69/3.17 inference(forward_subsumption_resolution,[status(thm)],[f1237,f281])).
% 20.69/3.20 fof(f54245,plain,(
% 20.69/3.20 ![X0]: (~sP4_prd(X0)|sP5_prd(X0))),
% 20.69/3.20 inference(forward_subsumption_resolution,[status(thm)],[f1238,f282])).
% 20.69/3.20 fof(f54246,plain,(
% 20.69/3.20 sP5_prd(sK39_skl(sK40_skl(sK36_skl)))|sP5_prd(sK36_skl)),
% 20.69/3.20 inference(resolution,[status(thm)],[f54245,f821])).
% 20.69/3.20 fof(f54247,plain,(
% 20.69/3.20 sP5_prd(sK36_skl)),
% 20.69/3.20 inference(forward_subsumption_resolution,[status(thm)],[f54246,f833])).
% 20.69/3.20 fof(f54248,plain,(
% 20.69/3.20 $false),
% 20.69/3.20 inference(forward_subsumption_resolution,[status(thm)],[f54247,f405])).
% 20.69/3.20 % SZS output end CNFRefutation for theBenchmark.p
% 20.69/3.24 % Elapsed time: 2.759686 seconds
% 20.69/3.24 % CPU time: 21.252707 seconds
% 20.69/3.24 % Total memory used: 271.076 MB
% 20.69/3.24 % Net memory used: 257.639 MB
%------------------------------------------------------------------------------