%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG099+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 : n006.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:20 PM UTC 2026
% Result : Theorem 38.80s 5.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG099+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.66 % Computer : n006.cluster.edu
% 0.17/0.66 % Model : x86_64 x86_64
% 0.17/0.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.66 % Memory : 8046.5625MB
% 0.17/0.66 % OS : Linux 6.8.0-71-generic
% 0.17/0.66 % CPULimit : 300
% 0.17/0.66 % WCLimit : 300
% 0.17/0.66 % DateTime : Mon Sep 21 04:19:28 UTC 2026
% 0.17/0.66 % CPUTime :
% 0.17/0.68 % Drodi V4.1.1
% 38.80/5.65 % Refutation found
% 38.80/5.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.80/5.65 % SZS output start CNFRefutation for theBenchmark
% 38.80/5.65 fof(f5,axiom,(
% 38.80/5.65 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtpldt0(W0,W1)) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f6,axiom,(
% 38.80/5.65 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtasdt0(W0,W1)) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f11,axiom,(
% 38.80/5.65 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f18,axiom,(
% 38.80/5.65 sz10 != sz00 ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f20,axiom,(
% 38.80/5.65 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f24,definition,(
% 38.80/5.65 (! [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) ) )) ) )) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f25,axiom,(
% 38.80/5.65 (! [W0,W1] :( ( aIdeal0(W0)& aIdeal0(W1) )=> aIdeal0(sdtpldt1(W0,W1)) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f26,axiom,(
% 38.80/5.65 (! [W0,W1] :( ( aIdeal0(W0)& aIdeal0(W1) )=> aIdeal0(sdtasasdt0(W0,W1)) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f27,definition,(
% 38.80/5.65 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aIdeal0(W2) )=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)<=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f28,hypothesis,(
% 38.80/5.65 ( aIdeal0(xI)& aIdeal0(xJ) ) ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f30,hypothesis,(
% 38.80/5.65 ( aElement0(xx)& aElement0(xy) ) ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f31,hypothesis,(
% 38.80/5.65 ( aElementOf0(xa,xI)& aElementOf0(xb,xJ)& sdtpldt0(xa,xb) = sz10 ) ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f32,hypothesis,(
% 38.80/5.65 xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)) ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f33,hypothesis,(
% 38.80/5.65 aElementOf0(sdtpldt0(xw,smndt0(xx)),xI) ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f34,hypothesis,(
% 38.80/5.65 aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ) ),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f35,conjecture,(
% 38.80/5.65 (? [W0] :( aElement0(W0)& sdteqdtlpzmzozddtrp0(W0,xx,xI)& sdteqdtlpzmzozddtrp0(W0,xy,xJ) ) )),
% 38.80/5.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.80/5.65 fof(f36,negated_conjecture,(
% 38.80/5.65 ~((? [W0] :( aElement0(W0)& sdteqdtlpzmzozddtrp0(W0,xx,xI)& sdteqdtlpzmzozddtrp0(W0,xy,xJ) ) ))),
% 38.80/5.65 inference(negated_conjecture,[status(cth)],[f35])).
% 38.80/5.65 fof(f44,plain,(
% 38.80/5.65 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtpldt0(W0,W1)))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 38.80/5.65 fof(f45,plain,(
% 38.80/5.65 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtpldt0(X0,X1)))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f44])).
% 38.80/5.65 fof(f46,plain,(
% 38.80/5.65 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtasdt0(W0,W1)))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 38.80/5.65 fof(f47,plain,(
% 38.80/5.65 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtasdt0(X0,X1)))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f46])).
% 38.80/5.65 fof(f58,plain,(
% 38.80/5.65 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 38.80/5.65 fof(f59,plain,(
% 38.80/5.65 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f58])).
% 38.80/5.65 fof(f76,plain,(
% 38.80/5.65 ~sz10=sz00),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f18])).
% 38.80/5.65 fof(f80,plain,(
% 38.80/5.65 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 38.80/5.65 fof(f81,plain,(
% 38.80/5.65 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f80])).
% 38.80/5.65 fof(f110,plain,(
% 38.80/5.65 ![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))))))))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 38.80/5.65 fof(f111,plain,(
% 38.80/5.65 ![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)))))))))),
% 38.80/5.65 inference(NNF_transformation,[status(thm)],[f110])).
% 38.80/5.65 fof(f112,plain,(
% 38.80/5.65 (![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)))))))))),
% 38.80/5.65 inference(miniscoping,[status(thm)],[f111])).
% 38.80/5.65 fof(f113,plain,(
% 38.80/5.65 (![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)))))))),
% 38.80/5.65 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))],[f112])).
% 38.80/5.65 fof(f114,plain,(
% 38.80/5.65 ![X0]: (~aIdeal0(X0)|aSet0(X0))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f113])).
% 38.80/5.65 fof(f122,plain,(
% 38.80/5.65 ![W0,W1]: ((~aIdeal0(W0)|~aIdeal0(W1))|aIdeal0(sdtpldt1(W0,W1)))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 38.80/5.65 fof(f123,plain,(
% 38.80/5.65 ![X0,X1]: (~aIdeal0(X0)|~aIdeal0(X1)|aIdeal0(sdtpldt1(X0,X1)))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f122])).
% 38.80/5.65 fof(f124,plain,(
% 38.80/5.65 ![W0,W1]: ((~aIdeal0(W0)|~aIdeal0(W1))|aIdeal0(sdtasasdt0(W0,W1)))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 38.80/5.65 fof(f125,plain,(
% 38.80/5.65 ![X0,X1]: (~aIdeal0(X0)|~aIdeal0(X1)|aIdeal0(sdtasasdt0(X0,X1)))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f124])).
% 38.80/5.65 fof(f126,plain,(
% 38.80/5.65 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aIdeal0(W2))|(sdteqdtlpzmzozddtrp0(W0,W1,W2)<=>aElementOf0(sdtpldt0(W0,smndt0(W1)),W2)))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 38.80/5.65 fof(f127,plain,(
% 38.80/5.65 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aIdeal0(W2))|((~sdteqdtlpzmzozddtrp0(W0,W1,W2)|aElementOf0(sdtpldt0(W0,smndt0(W1)),W2))&(sdteqdtlpzmzozddtrp0(W0,W1,W2)|~aElementOf0(sdtpldt0(W0,smndt0(W1)),W2))))),
% 38.80/5.65 inference(NNF_transformation,[status(thm)],[f126])).
% 38.80/5.65 fof(f129,plain,(
% 38.80/5.65 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aIdeal0(X2)|sdteqdtlpzmzozddtrp0(X0,X1,X2)|~aElementOf0(sdtpldt0(X0,smndt0(X1)),X2))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f127])).
% 38.80/5.65 fof(f130,plain,(
% 38.80/5.65 aIdeal0(xI)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f28])).
% 38.80/5.65 fof(f131,plain,(
% 38.80/5.65 aIdeal0(xJ)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f28])).
% 38.80/5.65 fof(f134,plain,(
% 38.80/5.65 aElement0(xx)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f30])).
% 38.80/5.65 fof(f135,plain,(
% 38.80/5.65 aElement0(xy)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f30])).
% 38.80/5.65 fof(f136,plain,(
% 38.80/5.65 aElementOf0(xa,xI)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f31])).
% 38.80/5.65 fof(f137,plain,(
% 38.80/5.65 aElementOf0(xb,xJ)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f31])).
% 38.80/5.65 fof(f139,plain,(
% 38.80/5.65 xw=sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f32])).
% 38.80/5.65 fof(f140,plain,(
% 38.80/5.65 aElementOf0(sdtpldt0(xw,smndt0(xx)),xI)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f33])).
% 38.80/5.65 fof(f141,plain,(
% 38.80/5.65 aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ)),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f34])).
% 38.80/5.65 fof(f142,plain,(
% 38.80/5.65 (![W0]: ((~aElement0(W0)|~sdteqdtlpzmzozddtrp0(W0,xx,xI))|~sdteqdtlpzmzozddtrp0(W0,xy,xJ)))),
% 38.80/5.65 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 38.80/5.65 fof(f143,plain,(
% 38.80/5.65 ![X0]: (~aElement0(X0)|~sdteqdtlpzmzozddtrp0(X0,xx,xI)|~sdteqdtlpzmzozddtrp0(X0,xy,xJ))),
% 38.80/5.65 inference(cnf_transformation,[status(thm)],[f142])).
% 38.80/5.65 fof(f182,plain,(
% 38.80/5.65 ![X0,X1]: (~aElement0(X0)|~aIdeal0(X1)|sdteqdtlpzmzozddtrp0(X0,xx,X1)|~aElementOf0(sdtpldt0(X0,smndt0(xx)),X1))),
% 38.80/5.65 inference(resolution,[status(thm)],[f129,f134])).
% 38.80/5.65 fof(f210,definition,(
% 38.80/5.65 sQ8_spl <=> (aElement0(xa))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f212,plain,(
% 38.80/5.65 ~aElement0(xa)|sQ8_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f210])).
% 38.80/5.65 fof(f213,definition,(
% 38.80/5.65 sQ9_spl <=> (aElement0(xb))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f215,plain,(
% 38.80/5.65 ~aElement0(xb)|sQ9_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f213])).
% 38.80/5.65 fof(f244,definition,(
% 38.80/5.65 sQ12_spl <=> (aElement0(xy))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f246,plain,(
% 38.80/5.65 ~aElement0(xy)|sQ12_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f244])).
% 38.80/5.65 fof(f258,plain,(
% 38.80/5.65 $false|sQ12_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f246,f135])).
% 38.80/5.65 fof(f259,plain,(
% 38.80/5.65 sQ12_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f258])).
% 38.80/5.65 fof(f336,definition,(
% 38.80/5.65 sQ24_spl <=> (aElement0(xx))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f338,plain,(
% 38.80/5.65 ~aElement0(xx)|sQ24_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f336])).
% 38.80/5.65 fof(f435,plain,(
% 38.80/5.65 $false|sQ24_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f338,f134])).
% 38.80/5.65 fof(f436,plain,(
% 38.80/5.65 sQ24_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f435])).
% 38.80/5.65 fof(f548,plain,(
% 38.80/5.65 ![X0]: (~aElement0(X0)|sdtasdt0(X0,xy)=sdtasdt0(xy,X0))),
% 38.80/5.65 inference(resolution,[status(thm)],[f59,f135])).
% 38.80/5.65 fof(f891,plain,(
% 38.80/5.65 ![X0,X1]: (~aElementOf0(X0,X1)|aElement0(X0)|~aIdeal0(X1))),
% 38.80/5.65 inference(resolution,[status(thm)],[f81,f114])).
% 38.80/5.65 fof(f936,plain,(
% 38.80/5.65 ![X0]: (~aElementOf0(X0,xJ)|aElement0(X0))),
% 38.80/5.65 inference(resolution,[status(thm)],[f891,f131])).
% 38.80/5.65 fof(f937,plain,(
% 38.80/5.65 ![X0]: (~aElementOf0(X0,xI)|aElement0(X0))),
% 38.80/5.65 inference(resolution,[status(thm)],[f891,f130])).
% 38.80/5.65 fof(f938,plain,(
% 38.80/5.65 aElement0(xb)),
% 38.80/5.65 inference(resolution,[status(thm)],[f936,f137])).
% 38.80/5.65 fof(f944,definition,(
% 38.80/5.65 sQ78_spl <=> (aIdeal0(xJ))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f946,plain,(
% 38.80/5.65 ~aIdeal0(xJ)|sQ78_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f944])).
% 38.80/5.65 fof(f952,plain,(
% 38.80/5.65 $false|sQ78_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f946,f131])).
% 38.80/5.65 fof(f953,plain,(
% 38.80/5.65 sQ78_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f952])).
% 38.80/5.65 fof(f994,plain,(
% 38.80/5.65 aElement0(xa)),
% 38.80/5.65 inference(resolution,[status(thm)],[f937,f136])).
% 38.80/5.65 fof(f1000,definition,(
% 38.80/5.65 sQ83_spl <=> (aIdeal0(xI))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f1002,plain,(
% 38.80/5.65 ~aIdeal0(xI)|sQ83_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f1000])).
% 38.80/5.65 fof(f1008,plain,(
% 38.80/5.65 $false|sQ83_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f1002,f130])).
% 38.80/5.65 fof(f1009,plain,(
% 38.80/5.65 sQ83_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f1008])).
% 38.80/5.65 fof(f1072,definition,(
% 38.80/5.65 sQ96_spl <=> (sz10=sz00)),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f1073,plain,(
% 38.80/5.65 sz10=sz00|~sQ96_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f1072])).
% 38.80/5.65 fof(f1112,plain,(
% 38.80/5.65 sdtasdt0(xa,xy)=sdtasdt0(xy,xa)),
% 38.80/5.65 inference(resolution,[status(thm)],[f994,f548])).
% 38.80/5.65 fof(f1646,plain,(
% 38.80/5.65 ![X0]: (~aIdeal0(X0)|aIdeal0(sdtpldt1(X0,xJ)))),
% 38.80/5.65 inference(resolution,[status(thm)],[f123,f131])).
% 38.80/5.65 fof(f1647,plain,(
% 38.80/5.65 ![X0]: (~aIdeal0(X0)|aIdeal0(sdtpldt1(X0,xI)))),
% 38.80/5.65 inference(resolution,[status(thm)],[f123,f130])).
% 38.80/5.65 fof(f1648,plain,(
% 38.80/5.65 aIdeal0(sdtpldt1(xJ,xJ))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1646,f131])).
% 38.80/5.65 fof(f1672,plain,(
% 38.80/5.65 aIdeal0(sdtpldt1(xJ,xI))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1647,f131])).
% 38.80/5.65 fof(f1673,plain,(
% 38.80/5.65 aIdeal0(sdtpldt1(xI,xI))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1647,f130])).
% 38.80/5.65 fof(f1810,plain,(
% 38.80/5.65 $false|sQ9_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f215,f938])).
% 38.80/5.65 fof(f1811,plain,(
% 38.80/5.65 sQ9_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f1810])).
% 38.80/5.65 fof(f1919,plain,(
% 38.80/5.65 ![X0]: (~aIdeal0(X0)|aIdeal0(sdtasasdt0(X0,xJ)))),
% 38.80/5.65 inference(resolution,[status(thm)],[f125,f131])).
% 38.80/5.65 fof(f1920,plain,(
% 38.80/5.65 ![X0]: (~aIdeal0(X0)|aIdeal0(sdtasasdt0(X0,xI)))),
% 38.80/5.65 inference(resolution,[status(thm)],[f125,f130])).
% 38.80/5.65 fof(f1925,plain,(
% 38.80/5.65 aIdeal0(sdtasasdt0(xJ,xJ))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1919,f131])).
% 38.80/5.65 fof(f1926,plain,(
% 38.80/5.65 aIdeal0(sdtasasdt0(xI,xJ))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1919,f130])).
% 38.80/5.65 fof(f1957,plain,(
% 38.80/5.65 aIdeal0(sdtasasdt0(xJ,xI))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1920,f131])).
% 38.80/5.65 fof(f1958,plain,(
% 38.80/5.65 aIdeal0(sdtasasdt0(xI,xI))),
% 38.80/5.65 inference(resolution,[status(thm)],[f1920,f130])).
% 38.80/5.65 fof(f2569,plain,(
% 38.80/5.65 $false|sQ8_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f212,f994])).
% 38.80/5.65 fof(f2570,plain,(
% 38.80/5.65 sQ8_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f2569])).
% 38.80/5.65 fof(f2754,plain,(
% 38.80/5.65 ~aElement0(xy)|~aElement0(xa)|aElement0(sdtasdt0(xa,xy))),
% 38.80/5.65 inference(paramodulation,[status(thm)],[f1112,f47])).
% 38.80/5.65 fof(f2762,definition,(
% 38.80/5.65 sQ211_spl <=> (aElement0(sdtasdt0(xa,xy)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f2765,plain,(
% 38.80/5.65 ~sQ12_spl|~sQ8_spl|sQ211_spl),
% 38.80/5.65 inference(split_clause,[status(thm)],[f2754,f244,f210,f2762])).
% 38.80/5.65 fof(f3096,definition,(
% 38.80/5.65 sQ233_spl <=> (aIdeal0(sdtpldt1(xJ,xJ)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3098,plain,(
% 38.80/5.65 ~aIdeal0(sdtpldt1(xJ,xJ))|sQ233_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f3096])).
% 38.80/5.65 fof(f3104,plain,(
% 38.80/5.65 $false|sQ233_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f3098,f1648])).
% 38.80/5.65 fof(f3105,plain,(
% 38.80/5.65 sQ233_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f3104])).
% 38.80/5.65 fof(f3182,plain,(
% 38.80/5.65 xw=sdtpldt0(sdtasdt0(xa,xy),sdtasdt0(xx,xb))),
% 38.80/5.65 inference(forward_demodulation,[status(thm)],[f1112,f139])).
% 38.80/5.65 fof(f3184,plain,(
% 38.80/5.65 ~aElement0(sdtasdt0(xa,xy))|~aElement0(sdtasdt0(xx,xb))|aElement0(xw)),
% 38.80/5.65 inference(paramodulation,[status(thm)],[f3182,f45])).
% 38.80/5.65 fof(f3185,definition,(
% 38.80/5.65 sQ237_spl <=> (aElement0(sdtasdt0(xx,xb)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3187,plain,(
% 38.80/5.65 ~aElement0(sdtasdt0(xx,xb))|sQ237_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f3185])).
% 38.80/5.65 fof(f3191,definition,(
% 38.80/5.65 sQ239_spl <=> (sdteqdtlpzmzozddtrp0(xw,xy,xJ))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3195,definition,(
% 38.80/5.65 sQ240_spl <=> (aElement0(xw))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3196,plain,(
% 38.80/5.65 aElement0(xw)|~sQ240_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f3195])).
% 38.80/5.65 fof(f3198,plain,(
% 38.80/5.65 ~sQ211_spl|~sQ237_spl|sQ240_spl),
% 38.80/5.65 inference(split_clause,[status(thm)],[f3184,f2762,f3185,f3195])).
% 38.80/5.65 fof(f3208,plain,(
% 38.80/5.65 ~aElement0(xx)|~aElement0(xb)|sQ237_spl),
% 38.80/5.65 inference(resolution,[status(thm)],[f3187,f47])).
% 38.80/5.65 fof(f3209,plain,(
% 38.80/5.65 ~sQ24_spl|~sQ9_spl|sQ237_spl),
% 38.80/5.65 inference(split_clause,[status(thm)],[f3208,f336,f213,f3185])).
% 38.80/5.65 fof(f3366,plain,(
% 38.80/5.65 ~sdteqdtlpzmzozddtrp0(xw,xx,xI)|~sdteqdtlpzmzozddtrp0(xw,xy,xJ)|~sQ240_spl),
% 38.80/5.65 inference(resolution,[status(thm)],[f3196,f143])).
% 38.80/5.65 fof(f3367,definition,(
% 38.80/5.65 sQ252_spl <=> (sdteqdtlpzmzozddtrp0(xw,xx,xI))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3370,plain,(
% 38.80/5.65 ~sQ252_spl|~sQ239_spl|~sQ240_spl),
% 38.80/5.65 inference(split_clause,[status(thm)],[f3366,f3367,f3191,f3195])).
% 38.80/5.65 fof(f3528,definition,(
% 38.80/5.65 sQ266_spl <=> (aIdeal0(sdtpldt1(xJ,xI)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3530,plain,(
% 38.80/5.65 ~aIdeal0(sdtpldt1(xJ,xI))|sQ266_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f3528])).
% 38.80/5.65 fof(f3536,plain,(
% 38.80/5.65 $false|sQ266_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f3530,f1672])).
% 38.80/5.65 fof(f3537,plain,(
% 38.80/5.65 sQ266_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f3536])).
% 38.80/5.65 fof(f3942,definition,(
% 38.80/5.65 sQ307_spl <=> (aIdeal0(sdtpldt1(xI,xI)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f3944,plain,(
% 38.80/5.65 ~aIdeal0(sdtpldt1(xI,xI))|sQ307_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f3942])).
% 38.80/5.65 fof(f3950,plain,(
% 38.80/5.65 $false|sQ307_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f3944,f1673])).
% 38.80/5.65 fof(f3951,plain,(
% 38.80/5.65 sQ307_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f3950])).
% 38.80/5.65 fof(f4393,definition,(
% 38.80/5.65 sQ326_spl <=> (aIdeal0(sdtasasdt0(xJ,xJ)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f4395,plain,(
% 38.80/5.65 ~aIdeal0(sdtasasdt0(xJ,xJ))|sQ326_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f4393])).
% 38.80/5.65 fof(f4401,plain,(
% 38.80/5.65 $false|sQ326_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f4395,f1925])).
% 38.80/5.65 fof(f4402,plain,(
% 38.80/5.65 sQ326_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f4401])).
% 38.80/5.65 fof(f4447,definition,(
% 38.80/5.65 sQ329_spl <=> (aIdeal0(sdtasasdt0(xI,xJ)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f4449,plain,(
% 38.80/5.65 ~aIdeal0(sdtasasdt0(xI,xJ))|sQ329_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f4447])).
% 38.80/5.65 fof(f4455,plain,(
% 38.80/5.65 $false|sQ329_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f4449,f1926])).
% 38.80/5.65 fof(f4456,plain,(
% 38.80/5.65 sQ329_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f4455])).
% 38.80/5.65 fof(f4763,definition,(
% 38.80/5.65 sQ333_spl <=> (aIdeal0(sdtasasdt0(xJ,xI)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f4765,plain,(
% 38.80/5.65 ~aIdeal0(sdtasasdt0(xJ,xI))|sQ333_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f4763])).
% 38.80/5.65 fof(f4771,plain,(
% 38.80/5.65 $false|sQ333_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f4765,f1957])).
% 38.80/5.65 fof(f4772,plain,(
% 38.80/5.65 sQ333_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f4771])).
% 38.80/5.65 fof(f4830,definition,(
% 38.80/5.65 sQ336_spl <=> (aIdeal0(sdtasasdt0(xI,xI)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f4832,plain,(
% 38.80/5.65 ~aIdeal0(sdtasasdt0(xI,xI))|sQ336_spl),
% 38.80/5.65 inference(component_clause,[status(thm)],[f4830])).
% 38.80/5.65 fof(f4838,plain,(
% 38.80/5.65 $false|sQ336_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f4832,f1958])).
% 38.80/5.65 fof(f4839,plain,(
% 38.80/5.65 sQ336_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f4838])).
% 38.80/5.65 fof(f8179,plain,(
% 38.80/5.65 $false|~sQ96_spl),
% 38.80/5.65 inference(forward_subsumption_resolution,[status(thm)],[f1073,f76])).
% 38.80/5.65 fof(f8180,plain,(
% 38.80/5.65 ~sQ96_spl),
% 38.80/5.65 inference(contradiction_clause,[status(thm)],[f8179])).
% 38.80/5.65 fof(f10266,definition,(
% 38.80/5.65 ![X2]: (sQ553_spl <=> (~aElement0(X2)))),
% 38.80/5.65 introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition])).
% 38.80/5.65 fof(f10267,plain,(
% 38.80/5.65 ![X0]: (~aElement0(X0)|~sQ553_spl)),
% 38.80/5.65 inference(component_clause,[status(thm)],[f10266])).
% 38.80/5.66 fof(f10323,plain,(
% 38.80/5.66 $false|~sQ553_spl),
% 38.80/5.66 inference(backward_subsumption_resolution,[status(thm)],[f135,f10267])).
% 38.80/5.66 fof(f10334,plain,(
% 38.80/5.66 ~sQ553_spl),
% 38.80/5.66 inference(contradiction_clause,[status(thm)],[f10323])).
% 38.80/5.66 fof(f13333,plain,(
% 38.80/5.66 ~aElement0(xw)|~aElement0(xy)|~aIdeal0(xJ)|sdteqdtlpzmzozddtrp0(xw,xy,xJ)),
% 38.80/5.66 inference(resolution,[status(thm)],[f141,f129])).
% 38.80/5.66 fof(f13335,plain,(
% 38.80/5.66 ~sQ240_spl|~sQ12_spl|~sQ78_spl|sQ239_spl),
% 38.80/5.66 inference(split_clause,[status(thm)],[f13333,f3195,f244,f944,f3191])).
% 38.80/5.66 fof(f15934,plain,(
% 38.80/5.66 ~aElement0(xw)|~aIdeal0(xI)|sdteqdtlpzmzozddtrp0(xw,xx,xI)),
% 38.80/5.66 inference(resolution,[status(thm)],[f140,f182])).
% 38.80/5.66 fof(f15937,plain,(
% 38.80/5.66 ~sQ240_spl|~sQ83_spl|sQ252_spl),
% 38.80/5.66 inference(split_clause,[status(thm)],[f15934,f3195,f1000,f3367])).
% 38.80/5.66 fof(f15939,plain,(
% 38.80/5.66 $false),
% 38.80/5.66 inference(sat_refutation,[status(thm)],[f259,f436,f953,f1009,f1811,f2570,f2765,f3105,f3198,f3209,f3370,f3537,f3951,f4402,f4456,f4772,f4839,f8180,f10334,f13335,f15937])).
% 38.80/5.66 % SZS output end CNFRefutation for theBenchmark.p
% 13.07/5.73 % Elapsed time: 5.046676 seconds
% 13.07/5.73 % CPU time: 39.458648 seconds
% 13.07/5.73 % Total memory used: 389.933 MB
% 13.07/5.73 % Net memory used: 362.647 MB
%------------------------------------------------------------------------------