%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG089+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 : n004.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:19 PM UTC 2026
% Result : Theorem 3.28s 0.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG089+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.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:19:07 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 3.28/0.85 % Refutation found
% 3.28/0.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.28/0.85 % SZS output start CNFRefutation for theBenchmark
% 3.28/0.85 fof(f24,definition,(
% 3.28/0.85 (! [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) ) )) ) )) ) )),
% 3.28/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.85 fof(f25,hypothesis,(
% 3.28/0.85 ( aIdeal0(xI)& aIdeal0(xJ) ) ),
% 3.28/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.85 fof(f26,hypothesis,(
% 3.28/0.85 ( aElementOf0(xx,sdtpldt1(xI,xJ))& aElementOf0(xy,sdtpldt1(xI,xJ))& aElement0(xz) ) ),
% 3.28/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.85 fof(f27,hypothesis,(
% 3.28/0.85 ( aElementOf0(xk,xI)& aElementOf0(xl,xJ)& xx = sdtpldt0(xk,xl) ) ),
% 3.28/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.85 fof(f30,conjecture,(
% 3.28/0.85 ( aElementOf0(sdtasdt0(xz,xk),xI)& aElementOf0(sdtasdt0(xz,xl),xJ) ) ),
% 3.28/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.85 fof(f31,negated_conjecture,(
% 3.28/0.85 ~(( aElementOf0(sdtasdt0(xz,xk),xI)& aElementOf0(sdtasdt0(xz,xl),xJ) ) )),
% 3.28/0.85 inference(negated_conjecture,[status(cth)],[f30])).
% 3.28/0.85 fof(f105,plain,(
% 3.28/0.85 ![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))))))))),
% 3.28/0.85 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 3.28/0.85 fof(f106,plain,(
% 3.28/0.85 ![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)))))))))),
% 3.28/0.85 inference(NNF_transformation,[status(thm)],[f105])).
% 3.28/0.85 fof(f107,plain,(
% 3.28/0.85 (![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)))))))))),
% 3.28/0.85 inference(miniscoping,[status(thm)],[f106])).
% 3.28/0.85 fof(f108,plain,(
% 3.28/0.85 (![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)))))))),
% 3.28/0.85 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))],[f107])).
% 3.28/0.85 fof(f109,plain,(
% 3.28/0.85 ![X0]: (~aIdeal0(X0)|aSet0(X0))),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f108])).
% 3.28/0.85 fof(f111,plain,(
% 3.28/0.85 ![X0,X1,X2]: (~aIdeal0(X0)|~aElementOf0(X1,X0)|~aElement0(X2)|aElementOf0(sdtasdt0(X2,X1),X0))),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f108])).
% 3.28/0.85 fof(f117,plain,(
% 3.28/0.85 aIdeal0(xI)),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f25])).
% 3.28/0.85 fof(f118,plain,(
% 3.28/0.85 aIdeal0(xJ)),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f25])).
% 3.28/0.85 fof(f121,plain,(
% 3.28/0.85 aElement0(xz)),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f26])).
% 3.28/0.85 fof(f122,plain,(
% 3.28/0.85 aElementOf0(xk,xI)),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f27])).
% 3.28/0.85 fof(f123,plain,(
% 3.28/0.85 aElementOf0(xl,xJ)),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f27])).
% 3.28/0.85 fof(f130,plain,(
% 3.28/0.85 (~aElementOf0(sdtasdt0(xz,xk),xI)|~aElementOf0(sdtasdt0(xz,xl),xJ))),
% 3.28/0.85 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 3.28/0.85 fof(f131,plain,(
% 3.28/0.85 ~aElementOf0(sdtasdt0(xz,xk),xI)|~aElementOf0(sdtasdt0(xz,xl),xJ)),
% 3.28/0.85 inference(cnf_transformation,[status(thm)],[f130])).
% 3.28/0.85 fof(f143,definition,(
% 3.28/0.85 sQ0_spl <=> (aElementOf0(sdtasdt0(xz,xk),xI))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f145,plain,(
% 3.28/0.85 ~aElementOf0(sdtasdt0(xz,xk),xI)|sQ0_spl),
% 3.28/0.85 inference(component_clause,[status(thm)],[f143])).
% 3.28/0.85 fof(f146,definition,(
% 3.28/0.85 sQ1_spl <=> (aElementOf0(sdtasdt0(xz,xl),xJ))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f148,plain,(
% 3.28/0.85 ~aElementOf0(sdtasdt0(xz,xl),xJ)|sQ1_spl),
% 3.28/0.85 inference(component_clause,[status(thm)],[f146])).
% 3.28/0.85 fof(f149,plain,(
% 3.28/0.85 ~sQ0_spl|~sQ1_spl),
% 3.28/0.85 inference(split_clause,[status(thm)],[f131,f143,f146])).
% 3.28/0.85 fof(f183,plain,(
% 3.28/0.85 aSet0(xI)),
% 3.28/0.85 inference(resolution,[status(thm)],[f109,f117])).
% 3.28/0.85 fof(f1512,definition,(
% 3.28/0.85 sQ76_spl <=> (aIdeal0(xI))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f1514,plain,(
% 3.28/0.85 ~aIdeal0(xI)|sQ76_spl),
% 3.28/0.85 inference(component_clause,[status(thm)],[f1512])).
% 3.28/0.85 fof(f1519,definition,(
% 3.28/0.85 sQ78_spl <=> (aIdeal0(xJ))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f1521,plain,(
% 3.28/0.85 ~aIdeal0(xJ)|sQ78_spl),
% 3.28/0.85 inference(component_clause,[status(thm)],[f1519])).
% 3.28/0.85 fof(f1526,plain,(
% 3.28/0.85 $false|sQ78_spl),
% 3.28/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1521,f118])).
% 3.28/0.85 fof(f1527,plain,(
% 3.28/0.85 sQ78_spl),
% 3.28/0.85 inference(contradiction_clause,[status(thm)],[f1526])).
% 3.28/0.85 fof(f1528,plain,(
% 3.28/0.85 $false|sQ76_spl),
% 3.28/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1514,f117])).
% 3.28/0.85 fof(f1529,plain,(
% 3.28/0.85 sQ76_spl),
% 3.28/0.85 inference(contradiction_clause,[status(thm)],[f1528])).
% 3.28/0.85 fof(f1560,plain,(
% 3.28/0.85 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,xk),xI))),
% 3.28/0.85 inference(resolution,[status(thm)],[f111,f122])).
% 3.28/0.85 fof(f1561,plain,(
% 3.28/0.85 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,xl),xJ))),
% 3.28/0.85 inference(resolution,[status(thm)],[f111,f123])).
% 3.28/0.85 fof(f1562,definition,(
% 3.28/0.85 ![X0]: (sQ80_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,xk),xI)))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f1563,plain,(
% 3.28/0.85 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,xk),xI)|~sQ80_spl)),
% 3.28/0.85 inference(component_clause,[status(thm)],[f1562])).
% 3.28/0.85 fof(f1565,plain,(
% 3.28/0.85 ~sQ76_spl|sQ80_spl),
% 3.28/0.85 inference(split_clause,[status(thm)],[f1560,f1512,f1562])).
% 3.28/0.85 fof(f1566,definition,(
% 3.28/0.85 ![X0]: (sQ81_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,xl),xJ)))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f1567,plain,(
% 3.28/0.85 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,xl),xJ)|~sQ81_spl)),
% 3.28/0.85 inference(component_clause,[status(thm)],[f1566])).
% 3.28/0.85 fof(f1569,plain,(
% 3.28/0.85 ~sQ78_spl|sQ81_spl),
% 3.28/0.85 inference(split_clause,[status(thm)],[f1561,f1519,f1566])).
% 3.28/0.85 fof(f1917,plain,(
% 3.28/0.85 aElementOf0(sdtasdt0(xz,xk),xI)|~sQ80_spl),
% 3.28/0.85 inference(resolution,[status(thm)],[f1563,f121])).
% 3.28/0.85 fof(f1925,plain,(
% 3.28/0.85 $false|sQ0_spl|~sQ80_spl),
% 3.28/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1917,f145])).
% 3.28/0.85 fof(f1926,plain,(
% 3.28/0.85 sQ0_spl|~sQ80_spl),
% 3.28/0.85 inference(contradiction_clause,[status(thm)],[f1925])).
% 3.28/0.85 fof(f2026,definition,(
% 3.28/0.85 ![X0]: (sQ126_spl <=> (~aSet0(X0)))),
% 3.28/0.85 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 3.28/0.85 fof(f2027,plain,(
% 3.28/0.85 ![X0]: (~aSet0(X0)|~sQ126_spl)),
% 3.28/0.85 inference(component_clause,[status(thm)],[f2026])).
% 3.28/0.85 fof(f2209,plain,(
% 3.28/0.85 $false|~sQ126_spl),
% 3.28/0.85 inference(backward_subsumption_resolution,[status(thm)],[f183,f2027])).
% 3.28/0.85 fof(f2211,plain,(
% 3.28/0.85 ~sQ126_spl),
% 3.28/0.85 inference(contradiction_clause,[status(thm)],[f2209])).
% 3.28/0.85 fof(f5716,plain,(
% 3.28/0.85 aElementOf0(sdtasdt0(xz,xl),xJ)|~sQ81_spl),
% 3.28/0.85 inference(resolution,[status(thm)],[f1567,f121])).
% 3.28/0.85 fof(f5719,plain,(
% 3.28/0.85 $false|sQ1_spl|~sQ81_spl),
% 3.28/0.85 inference(forward_subsumption_resolution,[status(thm)],[f5716,f148])).
% 3.28/0.85 fof(f5720,plain,(
% 3.28/0.85 sQ1_spl|~sQ81_spl),
% 3.28/0.85 inference(contradiction_clause,[status(thm)],[f5719])).
% 3.28/0.85 fof(f5721,plain,(
% 3.28/0.85 $false),
% 3.28/0.85 inference(sat_refutation,[status(thm)],[f149,f1527,f1529,f1565,f1569,f1926,f2211,f5720])).
% 3.28/0.85 % SZS output end CNFRefutation for theBenchmark.p
% 3.28/0.87 % Elapsed time: 0.504354 seconds
% 3.28/0.87 % CPU time: 3.672926 seconds
% 3.28/0.87 % Total memory used: 165.926 MB
% 3.28/0.87 % Net memory used: 160.020 MB
%------------------------------------------------------------------------------