%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG086+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 02:05:18 PM UTC 2026
% Result : Theorem 16.85s 2.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG086+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.73 % Computer : n026.cluster.edu
% 0.11/0.73 % Model : x86_64 x86_64
% 0.11/0.73 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.73 % Memory : 8046.5625MB
% 0.11/0.73 % OS : Linux 6.8.0-71-generic
% 0.11/0.73 % CPULimit : 300
% 0.11/0.73 % WCLimit : 300
% 0.11/0.73 % DateTime : Mon Sep 21 04:21:23 UTC 2026
% 0.11/0.73 % CPUTime :
% 0.11/0.75 % Drodi V4.1.1
% 16.85/2.99 % Refutation found
% 16.85/2.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.85/2.99 % SZS output start CNFRefutation for theBenchmark
% 16.85/2.99 fof(f22,definition,(
% 16.85/2.99 (! [W0,W1] :( ( aSet0(W0)& aSet0(W1) )=> (! [W2] :( W2 = sdtpldt1(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> (? [W4,W5] :( aElementOf0(W4,W0)& aElementOf0(W5,W1)& sdtpldt0(W4,W5) = W3 ) )) )) ) )) )),
% 16.85/2.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.85/2.99 fof(f24,definition,(
% 16.85/2.99 (! [W0] :( aIdeal0(W0)<=> ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> ( (! [W2] :( aElementOf0(W2,W0)=> aElementOf0(sdtpldt0(W1,W2),W0) ))& (! [W2] :( aElement0(W2)=> aElementOf0(sdtasdt0(W2,W1),W0) ) )) ) )) ) )),
% 16.85/2.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.85/2.99 fof(f25,hypothesis,(
% 16.85/2.99 ( aIdeal0(xI)& aIdeal0(xJ) ) ),
% 16.85/2.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.85/2.99 fof(f26,hypothesis,(
% 16.85/2.99 ( aElementOf0(xx,sdtpldt1(xI,xJ))& aElementOf0(xy,sdtpldt1(xI,xJ))& aElement0(xz) ) ),
% 16.85/2.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.85/2.99 fof(f27,conjecture,(
% 16.85/2.99 (? [W0,W1] :( aElementOf0(W0,xI)& aElementOf0(W1,xJ)& xx = sdtpldt0(W0,W1) ) )),
% 16.85/2.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.85/2.99 fof(f28,negated_conjecture,(
% 16.85/2.99 ~((? [W0,W1] :( aElementOf0(W0,xI)& aElementOf0(W1,xJ)& xx = sdtpldt0(W0,W1) ) ))),
% 16.85/2.99 inference(negated_conjecture,[status(cth)],[f27])).
% 16.85/2.99 fof(f80,plain,(
% 16.85/2.99 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|(![W2]: (W2=sdtpldt1(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(?[W4,W5]: ((aElementOf0(W4,W0)&aElementOf0(W5,W1))&sdtpldt0(W4,W5)=W3))))))))),
% 16.85/2.99 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 16.85/2.99 fof(f81,definition,(
% 16.85/2.99 ![W0,W1,W3,W4,W5]: (sP1_prd(W5,W4,W3,W1,W0)<=>((aElementOf0(W4,W0)&aElementOf0(W5,W1))&sdtpldt0(W4,W5)=W3))),
% 16.85/2.99 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 16.85/2.99 fof(f82,plain,(
% 16.85/2.99 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|(![W2]: (W2=sdtpldt1(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(?[W4,W5]: sP1_prd(W5,W4,W3,W1,W0))))))))),
% 16.85/2.99 inference(formula_renaming,[status(thm)],[f80,f81])).
% 16.85/2.99 fof(f83,plain,(
% 16.85/2.99 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|(![W2]: ((~W2=sdtpldt1(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(?[W4,W5]: sP1_prd(W5,W4,W3,W1,W0)))&(aElementOf0(W3,W2)|(![W4,W5]: ~sP1_prd(W5,W4,W3,W1,W0)))))))&(W2=sdtpldt1(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(![W4,W5]: ~sP1_prd(W5,W4,W3,W1,W0)))&(aElementOf0(W3,W2)|(?[W4,W5]: sP1_prd(W5,W4,W3,W1,W0))))))))))),
% 16.85/2.99 inference(NNF_transformation,[status(thm)],[f82])).
% 16.85/2.99 fof(f84,plain,(
% 16.85/2.99 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|((![W2]: (~W2=sdtpldt1(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(?[W4,W5]: sP1_prd(W5,W4,W3,W1,W0))))&(![W3]: (aElementOf0(W3,W2)|(![W4,W5]: ~sP1_prd(W5,W4,W3,W1,W0))))))))&(![W2]: (W2=sdtpldt1(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(![W4,W5]: ~sP1_prd(W5,W4,W3,W1,W0)))&(aElementOf0(W3,W2)|(?[W4,W5]: sP1_prd(W5,W4,W3,W1,W0))))))))))),
% 16.85/2.99 inference(miniscoping,[status(thm)],[f83])).
% 16.85/2.99 fof(f85,plain,(
% 16.85/2.99 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|((![W2]: (~W2=sdtpldt1(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP1_prd(sK3_skl(W3,W2,W1,W0),sK2_skl(W3,W2,W1,W0),W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|(![W4,W5]: ~sP1_prd(W5,W4,W3,W1,W0))))))))&(![W2]: (W2=sdtpldt1(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK4_skl(W2,W1,W0),W2)|(![W4,W5]: ~sP1_prd(W5,W4,sK4_skl(W2,W1,W0),W1,W0)))&(aElementOf0(sK4_skl(W2,W1,W0),W2)|sP1_prd(sK6_skl(W2,W1,W0),sK5_skl(W2,W1,W0),sK4_skl(W2,W1,W0),W1,W0))))))))),
% 16.85/2.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(W4,sK2_skl(W3,W2,W1,W0)),skolemize(W5,sK3_skl(W3,W2,W1,W0)),skolemize(W3,sK4_skl(W2,W1,W0)),skolemize(W4,sK5_skl(W2,W1,W0)),skolemize(W5,sK6_skl(W2,W1,W0))],[f84])).
% 16.85/2.99 fof(f87,plain,(
% 16.85/2.99 ![X0,X1,X2,X3]: (~aSet0(X0)|~aSet0(X1)|~X2=sdtpldt1(X0,X1)|~aElementOf0(X3,X2)|sP1_prd(sK3_skl(X3,X2,X1,X0),sK2_skl(X3,X2,X1,X0),X3,X1,X0))),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f85])).
% 16.85/2.99 fof(f102,plain,(
% 16.85/2.99 ![W0]: (aIdeal0(W0)<=>(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0))))))))),
% 16.85/2.99 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 16.85/2.99 fof(f103,plain,(
% 16.85/2.99 ![W0]: ((~aIdeal0(W0)|(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0))))))))&(aIdeal0(W0)|(~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&((?[W2]: (aElementOf0(W2,W0)&~aElementOf0(sdtpldt0(W1,W2),W0)))|(?[W2]: (aElement0(W2)&~aElementOf0(sdtasdt0(W2,W1),W0)))))))))),
% 16.85/2.99 inference(NNF_transformation,[status(thm)],[f102])).
% 16.85/2.99 fof(f104,plain,(
% 16.85/2.99 (![W0]: (~aIdeal0(W0)|(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0)))))))))&(![W0]: (aIdeal0(W0)|(~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&((?[W2]: (aElementOf0(W2,W0)&~aElementOf0(sdtpldt0(W1,W2),W0)))|(?[W2]: (aElement0(W2)&~aElementOf0(sdtasdt0(W2,W1),W0)))))))))),
% 16.85/2.99 inference(miniscoping,[status(thm)],[f103])).
% 16.85/2.99 fof(f105,plain,(
% 16.85/2.99 (![W0]: (~aIdeal0(W0)|(aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|((![W2]: (~aElementOf0(W2,W0)|aElementOf0(sdtpldt0(W1,W2),W0)))&(![W2]: (~aElement0(W2)|aElementOf0(sdtasdt0(W2,W1),W0)))))))))&(![W0]: (aIdeal0(W0)|(~aSet0(W0)|(aElementOf0(sK8_skl(W0),W0)&((aElementOf0(sK9_skl(W0),W0)&~aElementOf0(sdtpldt0(sK8_skl(W0),sK9_skl(W0)),W0))|(aElement0(sK10_skl(W0))&~aElementOf0(sdtasdt0(sK10_skl(W0),sK8_skl(W0)),W0)))))))),
% 16.85/2.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl]),skolemize(W1,sK8_skl(W0)),skolemize(W2,sK9_skl(W0)),skolemize(W2,sK10_skl(W0))],[f104])).
% 16.85/2.99 fof(f106,plain,(
% 16.85/2.99 ![X0]: (~aIdeal0(X0)|aSet0(X0))),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f105])).
% 16.85/2.99 fof(f114,plain,(
% 16.85/2.99 aIdeal0(xI)),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f25])).
% 16.85/2.99 fof(f115,plain,(
% 16.85/2.99 aIdeal0(xJ)),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f25])).
% 16.85/2.99 fof(f116,plain,(
% 16.85/2.99 aElementOf0(xx,sdtpldt1(xI,xJ))),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f26])).
% 16.85/2.99 fof(f119,plain,(
% 16.85/2.99 (![W0,W1]: ((~aElementOf0(W0,xI)|~aElementOf0(W1,xJ))|~xx=sdtpldt0(W0,W1)))),
% 16.85/2.99 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 16.85/2.99 fof(f120,plain,(
% 16.85/2.99 ![X0,X1]: (~aElementOf0(X0,xI)|~aElementOf0(X1,xJ)|~xx=sdtpldt0(X0,X1))),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f119])).
% 16.85/2.99 fof(f126,plain,(
% 16.85/2.99 ![W0,W1,W3,W4,W5]: ((~sP1_prd(W5,W4,W3,W1,W0)|((aElementOf0(W4,W0)&aElementOf0(W5,W1))&sdtpldt0(W4,W5)=W3))&(sP1_prd(W5,W4,W3,W1,W0)|((~aElementOf0(W4,W0)|~aElementOf0(W5,W1))|~sdtpldt0(W4,W5)=W3)))),
% 16.85/2.99 inference(NNF_transformation,[status(thm)],[f81])).
% 16.85/2.99 fof(f127,plain,(
% 16.85/2.99 (![W0,W1,W3,W4,W5]: (~sP1_prd(W5,W4,W3,W1,W0)|((aElementOf0(W4,W0)&aElementOf0(W5,W1))&sdtpldt0(W4,W5)=W3)))&(![W0,W1,W3,W4,W5]: (sP1_prd(W5,W4,W3,W1,W0)|((~aElementOf0(W4,W0)|~aElementOf0(W5,W1))|~sdtpldt0(W4,W5)=W3)))),
% 16.85/2.99 inference(miniscoping,[status(thm)],[f126])).
% 16.85/2.99 fof(f128,plain,(
% 16.85/2.99 ![X0,X1,X2,X3,X4]: (~sP1_prd(X0,X1,X2,X3,X4)|aElementOf0(X1,X4))),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f127])).
% 16.85/2.99 fof(f129,plain,(
% 16.85/2.99 ![X0,X1,X2,X3,X4]: (~sP1_prd(X0,X1,X2,X3,X4)|aElementOf0(X0,X3))),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f127])).
% 16.85/2.99 fof(f130,plain,(
% 16.85/2.99 ![X0,X1,X2,X3,X4]: (~sP1_prd(X0,X1,X2,X3,X4)|sdtpldt0(X1,X0)=X2)),
% 16.85/2.99 inference(cnf_transformation,[status(thm)],[f127])).
% 16.85/2.99 fof(f133,plain,(
% 16.85/2.99 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aElementOf0(X2,sdtpldt1(X0,X1))|sP1_prd(sK3_skl(X2,sdtpldt1(X0,X1),X1,X0),sK2_skl(X2,sdtpldt1(X0,X1),X1,X0),X2,X1,X0))),
% 16.85/2.99 inference(destructive_equality_resolution,[status(thm)],[f87])).
% 16.85/2.99 fof(f270,plain,(
% 16.85/2.99 aSet0(xJ)),
% 16.85/2.99 inference(resolution,[status(thm)],[f106,f115])).
% 16.85/2.99 fof(f271,plain,(
% 16.85/2.99 aSet0(xI)),
% 16.85/2.99 inference(resolution,[status(thm)],[f106,f114])).
% 16.85/2.99 fof(f715,plain,(
% 16.85/2.99 ~aSet0(xI)|~aSet0(xJ)|sP1_prd(sK3_skl(xx,sdtpldt1(xI,xJ),xJ,xI),sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xx,xJ,xI)),
% 16.85/2.99 inference(resolution,[status(thm)],[f133,f116])).
% 16.85/2.99 fof(f716,plain,(
% 16.85/2.99 ~aSet0(xJ)|sP1_prd(sK3_skl(xx,sdtpldt1(xI,xJ),xJ,xI),sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xx,xJ,xI)),
% 16.85/2.99 inference(forward_subsumption_resolution,[status(thm)],[f715,f271])).
% 16.85/2.99 fof(f1684,plain,(
% 16.85/2.99 sP1_prd(sK3_skl(xx,sdtpldt1(xI,xJ),xJ,xI),sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xx,xJ,xI)),
% 10.59/3.02 inference(forward_subsumption_resolution,[status(thm)],[f716,f270])).
% 10.59/3.02 fof(f1685,plain,(
% 10.59/3.02 sdtpldt0(sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),sK3_skl(xx,sdtpldt1(xI,xJ),xJ,xI))=xx),
% 10.59/3.02 inference(resolution,[status(thm)],[f1684,f130])).
% 10.59/3.02 fof(f1686,plain,(
% 10.59/3.02 aElementOf0(sK3_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xJ)),
% 10.59/3.02 inference(resolution,[status(thm)],[f1684,f129])).
% 10.59/3.02 fof(f1687,plain,(
% 10.59/3.02 aElementOf0(sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xI)),
% 10.59/3.02 inference(resolution,[status(thm)],[f1684,f128])).
% 10.59/3.02 fof(f15978,plain,(
% 10.59/3.02 ~aElementOf0(sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xI)|~aElementOf0(sK3_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xJ)),
% 10.59/3.02 inference(resolution,[status(thm)],[f1685,f120])).
% 10.59/3.02 fof(f15993,plain,(
% 10.59/3.02 ~aElementOf0(sK2_skl(xx,sdtpldt1(xI,xJ),xJ,xI),xI)),
% 10.59/3.02 inference(forward_subsumption_resolution,[status(thm)],[f15978,f1686])).
% 10.59/3.02 fof(f15994,plain,(
% 10.59/3.02 $false),
% 10.59/3.02 inference(forward_subsumption_resolution,[status(thm)],[f1687,f15993])).
% 10.59/3.02 % SZS output end CNFRefutation for theBenchmark.p
% 10.59/3.03 % Elapsed time: 2.283111 seconds
% 10.59/3.03 % CPU time: 17.825497 seconds
% 10.59/3.03 % Total memory used: 272.450 MB
% 10.59/3.03 % Net memory used: 251.531 MB
%------------------------------------------------------------------------------