%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG093+2 : 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 : n009.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 20.60s 3.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG093+2 : 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.09/0.56 % Computer : n009.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 04:18:58 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.58 % Drodi V4.1.1
% 20.60/3.50 % Refutation found
% 20.60/3.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.60/3.50 % SZS output start CNFRefutation for theBenchmark
% 20.60/3.50 fof(f7,axiom,(
% 20.60/3.50 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 20.60/3.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.60/3.50 fof(f20,axiom,(
% 20.60/3.50 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 20.60/3.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.60/3.50 fof(f23,definition,(
% 20.60/3.50 (! [W0,W1] :( ( aSet0(W0)& aSet0(W1) )=> (! [W2] :( W2 = sdtasasdt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElementOf0(W3,W0)& aElementOf0(W3,W1) ) ) )) ) )) )),
% 20.60/3.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.60/3.50 fof(f24,definition,(
% 20.60/3.50 (! [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) ) )) ) )) ) )),
% 20.60/3.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.60/3.50 fof(f26,hypothesis,(
% 20.60/3.50 ( aSet0(xI)& (! [W0] :( aElementOf0(W0,xI)=> ( (! [W1] :( aElementOf0(W1,xI)=> aElementOf0(sdtpldt0(W0,W1),xI) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),xI) ) )) ))& aIdeal0(xI)& aSet0(xJ)& (! [W0] :( aElementOf0(W0,xJ)=> ( (! [W1] :( aElementOf0(W1,xJ)=> aElementOf0(sdtpldt0(W0,W1),xJ) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),xJ) ) )) ))& aIdeal0(xJ) ) ),
% 20.60/3.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.60/3.50 fof(f27,conjecture,(
% 20.60/3.50 ( ( aSet0(sdtasasdt0(xI,xJ))& (! [W0] :( aElementOf0(W0,sdtasasdt0(xI,xJ))<=> ( aElementOf0(W0,xI)& aElementOf0(W0,xJ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtasasdt0(xI,xJ))=> ( (! [W1] :( aElementOf0(W1,sdtasasdt0(xI,xJ))=> aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ)) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),sdtasasdt0(xI,xJ)) ) )) ))| aIdeal0(sdtasasdt0(xI,xJ)) ) ) ),
% 20.60/3.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.60/3.50 fof(f28,negated_conjecture,(
% 20.60/3.50 ~(( ( aSet0(sdtasasdt0(xI,xJ))& (! [W0] :( aElementOf0(W0,sdtasasdt0(xI,xJ))<=> ( aElementOf0(W0,xI)& aElementOf0(W0,xJ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtasasdt0(xI,xJ))=> ( (! [W1] :( aElementOf0(W1,sdtasasdt0(xI,xJ))=> aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ)) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),sdtasasdt0(xI,xJ)) ) )) ))| aIdeal0(sdtasasdt0(xI,xJ)) ) ) )),
% 20.60/3.50 inference(negated_conjecture,[status(cth)],[f27])).
% 20.60/3.50 fof(f40,plain,(
% 20.60/3.50 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 20.60/3.50 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 20.60/3.50 fof(f41,plain,(
% 20.60/3.50 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f40])).
% 20.60/3.50 fof(f72,plain,(
% 20.60/3.50 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 20.60/3.50 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 20.60/3.50 fof(f73,plain,(
% 20.60/3.50 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f72])).
% 20.60/3.50 fof(f91,plain,(
% 20.60/3.50 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|(![W2]: (W2=sdtasasdt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElementOf0(W3,W0)&aElementOf0(W3,W1))))))))),
% 20.60/3.50 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 20.60/3.50 fof(f92,plain,(
% 20.60/3.50 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|(![W2]: ((~W2=sdtasasdt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElementOf0(W3,W0)&aElementOf0(W3,W1)))&(aElementOf0(W3,W2)|(~aElementOf0(W3,W0)|~aElementOf0(W3,W1)))))))&(W2=sdtasasdt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElementOf0(W3,W0)|~aElementOf0(W3,W1)))&(aElementOf0(W3,W2)|(aElementOf0(W3,W0)&aElementOf0(W3,W1))))))))))),
% 20.60/3.50 inference(NNF_transformation,[status(thm)],[f91])).
% 20.60/3.50 fof(f93,plain,(
% 20.60/3.50 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|((![W2]: (~W2=sdtasasdt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(W3,W0)&aElementOf0(W3,W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElementOf0(W3,W0)|~aElementOf0(W3,W1))))))))&(![W2]: (W2=sdtasasdt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElementOf0(W3,W0)|~aElementOf0(W3,W1)))&(aElementOf0(W3,W2)|(aElementOf0(W3,W0)&aElementOf0(W3,W1))))))))))),
% 20.60/3.50 inference(miniscoping,[status(thm)],[f92])).
% 20.60/3.50 fof(f94,plain,(
% 20.60/3.50 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|((![W2]: (~W2=sdtasasdt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(W3,W0)&aElementOf0(W3,W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElementOf0(W3,W0)|~aElementOf0(W3,W1))))))))&(![W2]: (W2=sdtasasdt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK7_skl(W2,W1,W0),W2)|(~aElementOf0(sK7_skl(W2,W1,W0),W0)|~aElementOf0(sK7_skl(W2,W1,W0),W1)))&(aElementOf0(sK7_skl(W2,W1,W0),W2)|(aElementOf0(sK7_skl(W2,W1,W0),W0)&aElementOf0(sK7_skl(W2,W1,W0),W1)))))))))),
% 20.60/3.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(W3,sK7_skl(W2,W1,W0))],[f93])).
% 20.60/3.50 fof(f97,plain,(
% 20.60/3.50 ![X0,X1,X2,X3]: (~aSet0(X0)|~aSet0(X1)|~X2=sdtasasdt0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(X3,X1))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f94])).
% 20.60/3.50 fof(f102,plain,(
% 20.60/3.50 ![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))))))))),
% 20.60/3.50 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 20.60/3.50 fof(f103,plain,(
% 20.60/3.50 ![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)))))))))),
% 20.60/3.50 inference(NNF_transformation,[status(thm)],[f102])).
% 20.60/3.50 fof(f104,plain,(
% 20.60/3.50 (![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)))))))))),
% 20.60/3.50 inference(miniscoping,[status(thm)],[f103])).
% 20.60/3.50 fof(f105,plain,(
% 20.60/3.50 (![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)))))))),
% 20.60/3.50 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])).
% 20.60/3.50 fof(f107,plain,(
% 20.60/3.50 ![X0,X1,X2]: (~aIdeal0(X0)|~aElementOf0(X1,X0)|~aElementOf0(X2,X0)|aElementOf0(sdtpldt0(X1,X2),X0))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f105])).
% 20.60/3.50 fof(f108,plain,(
% 20.60/3.50 ![X0,X1,X2]: (~aIdeal0(X0)|~aElementOf0(X1,X0)|~aElement0(X2)|aElementOf0(sdtasdt0(X2,X1),X0))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f105])).
% 20.60/3.50 fof(f109,plain,(
% 20.60/3.50 ![X0]: (aIdeal0(X0)|~aSet0(X0)|aElementOf0(sK8_skl(X0),X0))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f105])).
% 20.60/3.50 fof(f116,plain,(
% 20.60/3.50 ((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&aSet0(xJ))&(![W0]: (~aElementOf0(W0,xJ)|((![W1]: (~aElementOf0(W1,xJ)|aElementOf0(sdtpldt0(W0,W1),xJ)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xJ)))))))&aIdeal0(xJ)),
% 20.60/3.50 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 20.60/3.50 fof(f117,plain,(
% 20.60/3.50 aSet0(xI)),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f116])).
% 20.60/3.50 fof(f119,plain,(
% 20.60/3.50 ![X0,X1]: (~aElementOf0(X0,xI)|~aElement0(X1)|aElementOf0(sdtasdt0(X1,X0),xI))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f116])).
% 20.60/3.50 fof(f120,plain,(
% 20.60/3.50 aIdeal0(xI)),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f116])).
% 20.60/3.50 fof(f121,plain,(
% 20.60/3.50 aSet0(xJ)),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f116])).
% 20.60/3.50 fof(f123,plain,(
% 20.60/3.50 ![X0,X1]: (~aElementOf0(X0,xJ)|~aElement0(X1)|aElementOf0(sdtasdt0(X1,X0),xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f116])).
% 20.60/3.50 fof(f124,plain,(
% 20.60/3.50 aIdeal0(xJ)),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f116])).
% 20.60/3.50 fof(f125,plain,(
% 20.60/3.50 ((aSet0(sdtasasdt0(xI,xJ))&(![W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))<=>(aElementOf0(W0,xI)&aElementOf0(W0,xJ)))))&((?[W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))&((?[W1]: (aElementOf0(W1,sdtasasdt0(xI,xJ))&~aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ))))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),sdtasasdt0(xI,xJ)))))))&~aIdeal0(sdtasasdt0(xI,xJ))))),
% 20.60/3.50 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 20.60/3.50 fof(f126,definition,(
% 20.60/3.50 ![W0,W1]: (sP2_prd(W1,W0)<=>(aElementOf0(W1,sdtasasdt0(xI,xJ))&~aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ))))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 20.60/3.50 fof(f127,plain,(
% 20.60/3.50 (aSet0(sdtasasdt0(xI,xJ))&(![W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))<=>(aElementOf0(W0,xI)&aElementOf0(W0,xJ)))))&((?[W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))&((?[W1]: sP2_prd(W1,W0))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),sdtasasdt0(xI,xJ)))))))&~aIdeal0(sdtasasdt0(xI,xJ)))),
% 20.60/3.50 inference(formula_renaming,[status(thm)],[f125,f126])).
% 20.60/3.50 fof(f128,plain,(
% 20.60/3.50 (aSet0(sdtasasdt0(xI,xJ))&(![W0]: ((~aElementOf0(W0,sdtasasdt0(xI,xJ))|(aElementOf0(W0,xI)&aElementOf0(W0,xJ)))&(aElementOf0(W0,sdtasasdt0(xI,xJ))|(~aElementOf0(W0,xI)|~aElementOf0(W0,xJ))))))&((?[W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))&((?[W1]: sP2_prd(W1,W0))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),sdtasasdt0(xI,xJ)))))))&~aIdeal0(sdtasasdt0(xI,xJ)))),
% 20.60/3.50 inference(NNF_transformation,[status(thm)],[f127])).
% 20.60/3.50 fof(f129,plain,(
% 20.60/3.50 (aSet0(sdtasasdt0(xI,xJ))&((![W0]: (~aElementOf0(W0,sdtasasdt0(xI,xJ))|(aElementOf0(W0,xI)&aElementOf0(W0,xJ))))&(![W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))|(~aElementOf0(W0,xI)|~aElementOf0(W0,xJ))))))&((?[W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))&((?[W1]: sP2_prd(W1,W0))|(?[W1]: (aElement0(W1)&~aElementOf0(sdtasdt0(W1,W0),sdtasasdt0(xI,xJ)))))))&~aIdeal0(sdtasasdt0(xI,xJ)))),
% 20.60/3.50 inference(miniscoping,[status(thm)],[f128])).
% 20.60/3.50 fof(f130,plain,(
% 20.60/3.50 (aSet0(sdtasasdt0(xI,xJ))&((![W0]: (~aElementOf0(W0,sdtasasdt0(xI,xJ))|(aElementOf0(W0,xI)&aElementOf0(W0,xJ))))&(![W0]: (aElementOf0(W0,sdtasasdt0(xI,xJ))|(~aElementOf0(W0,xI)|~aElementOf0(W0,xJ))))))&((aElementOf0(sK11_skl,sdtasasdt0(xI,xJ))&(sP2_prd(sK12_skl,sK11_skl)|(aElement0(sK13_skl)&~aElementOf0(sdtasdt0(sK13_skl,sK11_skl),sdtasasdt0(xI,xJ)))))&~aIdeal0(sdtasasdt0(xI,xJ)))),
% 20.60/3.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl]),skolemize(W0,sK11_skl),skolemize(W1,sK12_skl),skolemize(W1,sK13_skl)],[f129])).
% 20.60/3.50 fof(f131,plain,(
% 20.60/3.50 aSet0(sdtasasdt0(xI,xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f132,plain,(
% 20.60/3.50 ![X0]: (~aElementOf0(X0,sdtasasdt0(xI,xJ))|aElementOf0(X0,xI))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f133,plain,(
% 20.60/3.50 ![X0]: (~aElementOf0(X0,sdtasasdt0(xI,xJ))|aElementOf0(X0,xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f134,plain,(
% 20.60/3.50 ![X0]: (aElementOf0(X0,sdtasasdt0(xI,xJ))|~aElementOf0(X0,xI)|~aElementOf0(X0,xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f135,plain,(
% 20.60/3.50 aElementOf0(sK11_skl,sdtasasdt0(xI,xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f136,plain,(
% 20.60/3.50 sP2_prd(sK12_skl,sK11_skl)|aElement0(sK13_skl)),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f137,plain,(
% 20.60/3.50 sP2_prd(sK12_skl,sK11_skl)|~aElementOf0(sdtasdt0(sK13_skl,sK11_skl),sdtasasdt0(xI,xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f138,plain,(
% 20.60/3.50 ~aIdeal0(sdtasasdt0(xI,xJ))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f130])).
% 20.60/3.50 fof(f150,plain,(
% 20.60/3.50 ![W0,W1]: ((~sP2_prd(W1,W0)|(aElementOf0(W1,sdtasasdt0(xI,xJ))&~aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ))))&(sP2_prd(W1,W0)|(~aElementOf0(W1,sdtasasdt0(xI,xJ))|aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ)))))),
% 20.60/3.50 inference(NNF_transformation,[status(thm)],[f126])).
% 20.60/3.50 fof(f151,plain,(
% 20.60/3.50 (![W0,W1]: (~sP2_prd(W1,W0)|(aElementOf0(W1,sdtasasdt0(xI,xJ))&~aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ)))))&(![W0,W1]: (sP2_prd(W1,W0)|(~aElementOf0(W1,sdtasasdt0(xI,xJ))|aElementOf0(sdtpldt0(W0,W1),sdtasasdt0(xI,xJ)))))),
% 20.60/3.50 inference(miniscoping,[status(thm)],[f150])).
% 20.60/3.50 fof(f152,plain,(
% 20.60/3.50 ![X0,X1]: (~sP2_prd(X0,X1)|aElementOf0(X0,sdtasasdt0(xI,xJ)))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f151])).
% 20.60/3.50 fof(f153,plain,(
% 20.60/3.50 ![X0,X1]: (~sP2_prd(X0,X1)|~aElementOf0(sdtpldt0(X1,X0),sdtasasdt0(xI,xJ)))),
% 20.60/3.50 inference(cnf_transformation,[status(thm)],[f151])).
% 20.60/3.50 fof(f155,definition,(
% 20.60/3.50 sQ0_spl <=> (sP2_prd(sK12_skl,sK11_skl))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f156,plain,(
% 20.60/3.50 sP2_prd(sK12_skl,sK11_skl)|~sQ0_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f155])).
% 20.60/3.50 fof(f158,definition,(
% 20.60/3.50 sQ1_spl <=> (aElement0(sK13_skl))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f159,plain,(
% 20.60/3.50 aElement0(sK13_skl)|~sQ1_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f158])).
% 20.60/3.50 fof(f161,plain,(
% 20.60/3.50 sQ0_spl|sQ1_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f136,f155,f158])).
% 20.60/3.50 fof(f162,definition,(
% 20.60/3.50 sQ2_spl <=> (aElementOf0(sdtasdt0(sK13_skl,sK11_skl),sdtasasdt0(xI,xJ)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f165,plain,(
% 20.60/3.50 sQ0_spl|~sQ2_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f137,f155,f162])).
% 20.60/3.50 fof(f171,plain,(
% 20.60/3.50 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aElementOf0(X2,sdtasasdt0(X0,X1))|aElementOf0(X2,X1))),
% 20.60/3.50 inference(destructive_equality_resolution,[status(thm)],[f97])).
% 20.60/3.50 fof(f174,plain,(
% 20.60/3.50 aElementOf0(sK12_skl,sdtasasdt0(xI,xJ))|~sQ0_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f152,f156])).
% 20.60/3.50 fof(f175,plain,(
% 20.60/3.50 aElementOf0(sK12_skl,xI)|~sQ0_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f132,f174])).
% 20.60/3.50 fof(f176,plain,(
% 20.60/3.50 aElementOf0(sK11_skl,xI)),
% 20.60/3.50 inference(resolution,[status(thm)],[f132,f135])).
% 20.60/3.50 fof(f177,plain,(
% 20.60/3.50 ~aSet0(xI)|aElement0(sK12_skl)|~sQ0_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f73,f175])).
% 20.60/3.50 fof(f180,plain,(
% 20.60/3.50 ~aSet0(sdtasasdt0(xI,xJ))|aElement0(sK11_skl)),
% 20.60/3.50 inference(resolution,[status(thm)],[f73,f135])).
% 20.60/3.50 fof(f181,definition,(
% 20.60/3.50 sQ3_spl <=> (aSet0(xI))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f183,plain,(
% 20.60/3.50 ~aSet0(xI)|sQ3_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f181])).
% 20.60/3.50 fof(f184,definition,(
% 20.60/3.50 sQ4_spl <=> (aElement0(sK12_skl))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f185,plain,(
% 20.60/3.50 aElement0(sK12_skl)|~sQ4_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f184])).
% 20.60/3.50 fof(f187,plain,(
% 20.60/3.50 ~sQ3_spl|sQ4_spl|~sQ0_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f177,f181,f184,f155])).
% 20.60/3.50 fof(f188,definition,(
% 20.60/3.50 sQ5_spl <=> (aSet0(sdtasasdt0(xI,xJ)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f190,plain,(
% 20.60/3.50 ~aSet0(sdtasasdt0(xI,xJ))|sQ5_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f188])).
% 20.60/3.50 fof(f192,definition,(
% 20.60/3.50 sQ6_spl <=> (aElement0(sK11_skl))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f193,plain,(
% 20.60/3.50 aElement0(sK11_skl)|~sQ6_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f192])).
% 20.60/3.50 fof(f196,plain,(
% 20.60/3.50 ~sQ5_spl|sQ6_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f180,f188,f192])).
% 20.60/3.50 fof(f197,plain,(
% 20.60/3.50 $false|sQ5_spl),
% 20.60/3.50 inference(forward_subsumption_resolution,[status(thm)],[f190,f131])).
% 20.60/3.50 fof(f198,plain,(
% 20.60/3.50 sQ5_spl),
% 20.60/3.50 inference(contradiction_clause,[status(thm)],[f197])).
% 20.60/3.50 fof(f211,plain,(
% 20.60/3.50 ![X0]: (~aElement0(X0)|sdtpldt0(X0,sK12_skl)=sdtpldt0(sK12_skl,X0)|~sQ4_spl)),
% 20.60/3.50 inference(resolution,[status(thm)],[f41,f185])).
% 20.60/3.50 fof(f227,plain,(
% 20.60/3.50 aIdeal0(sdtasasdt0(xI,xJ))|aElementOf0(sK8_skl(sdtasasdt0(xI,xJ)),sdtasasdt0(xI,xJ))),
% 20.60/3.50 inference(resolution,[status(thm)],[f109,f131])).
% 20.60/3.50 fof(f228,definition,(
% 20.60/3.50 sQ7_spl <=> (aIdeal0(sdtasasdt0(xI,xJ)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f229,plain,(
% 20.60/3.50 aIdeal0(sdtasasdt0(xI,xJ))|~sQ7_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f228])).
% 20.60/3.50 fof(f231,definition,(
% 20.60/3.50 sQ8_spl <=> (aElementOf0(sK8_skl(sdtasasdt0(xI,xJ)),sdtasasdt0(xI,xJ)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f234,plain,(
% 20.60/3.50 sQ7_spl|sQ8_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f227,f228,f231])).
% 20.60/3.50 fof(f235,plain,(
% 20.60/3.50 $false|~sQ7_spl),
% 20.60/3.50 inference(forward_subsumption_resolution,[status(thm)],[f229,f138])).
% 20.60/3.50 fof(f236,plain,(
% 20.60/3.50 ~sQ7_spl),
% 20.60/3.50 inference(contradiction_clause,[status(thm)],[f235])).
% 20.60/3.50 fof(f240,plain,(
% 20.60/3.50 sdtpldt0(sK11_skl,sK12_skl)=sdtpldt0(sK12_skl,sK11_skl)|~sQ4_spl|~sQ6_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f211,f193])).
% 20.60/3.50 fof(f286,plain,(
% 20.60/3.50 aElementOf0(sK11_skl,xJ)),
% 20.60/3.50 inference(resolution,[status(thm)],[f133,f135])).
% 20.60/3.50 fof(f289,definition,(
% 20.60/3.50 sQ9_spl <=> (aSet0(xJ))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f291,plain,(
% 20.60/3.50 ~aSet0(xJ)|sQ9_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f289])).
% 20.60/3.50 fof(f295,plain,(
% 20.60/3.50 ~sP2_prd(sK12_skl,sK11_skl)|~aElementOf0(sdtpldt0(sK12_skl,sK11_skl),sdtasasdt0(xI,xJ))|~sQ4_spl|~sQ6_spl),
% 20.60/3.50 inference(paramodulation,[status(thm)],[f240,f153])).
% 20.60/3.50 fof(f310,definition,(
% 20.60/3.50 sQ14_spl <=> (aElementOf0(sdtpldt0(sK12_skl,sK11_skl),sdtasasdt0(xI,xJ)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f313,plain,(
% 20.60/3.50 ~sQ0_spl|~sQ14_spl|~sQ4_spl|~sQ6_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f295,f155,f310,f184,f192])).
% 20.60/3.50 fof(f314,plain,(
% 20.60/3.50 $false|sQ3_spl),
% 20.60/3.50 inference(forward_subsumption_resolution,[status(thm)],[f183,f117])).
% 20.60/3.50 fof(f315,plain,(
% 20.60/3.50 sQ3_spl),
% 20.60/3.50 inference(contradiction_clause,[status(thm)],[f314])).
% 20.60/3.50 fof(f316,plain,(
% 20.60/3.50 aElementOf0(sK11_skl,sdtasasdt0(xI,xJ))|~aElementOf0(sK11_skl,xI)),
% 20.60/3.50 inference(resolution,[status(thm)],[f134,f286])).
% 20.60/3.50 fof(f317,definition,(
% 20.60/3.50 sQ15_spl <=> (aElementOf0(sK11_skl,sdtasasdt0(xI,xJ)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f320,definition,(
% 20.60/3.50 sQ16_spl <=> (aElementOf0(sK11_skl,xI))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f322,plain,(
% 20.60/3.50 ~aElementOf0(sK11_skl,xI)|sQ16_spl),
% 20.60/3.50 inference(component_clause,[status(thm)],[f320])).
% 20.60/3.50 fof(f323,plain,(
% 20.60/3.50 sQ15_spl|~sQ16_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f316,f317,f320])).
% 20.60/3.50 fof(f324,plain,(
% 20.60/3.50 $false|sQ16_spl),
% 20.60/3.50 inference(forward_subsumption_resolution,[status(thm)],[f322,f176])).
% 20.60/3.50 fof(f325,plain,(
% 20.60/3.50 sQ16_spl),
% 20.60/3.50 inference(contradiction_clause,[status(thm)],[f324])).
% 20.60/3.50 fof(f343,plain,(
% 20.60/3.50 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sK11_skl),xI))),
% 20.60/3.50 inference(resolution,[status(thm)],[f119,f176])).
% 20.60/3.50 fof(f346,plain,(
% 20.60/3.50 aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xI)|~sQ6_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f343,f193])).
% 20.60/3.50 fof(f347,plain,(
% 20.60/3.50 aElementOf0(sdtasdt0(sK13_skl,sK11_skl),xI)|~sQ1_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f343,f159])).
% 20.60/3.50 fof(f348,plain,(
% 20.60/3.50 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sK11_skl)),xI)|~sQ6_spl)),
% 20.60/3.50 inference(resolution,[status(thm)],[f346,f119])).
% 20.60/3.50 fof(f350,plain,(
% 20.60/3.50 ~aSet0(xI)|aElement0(sdtasdt0(sK11_skl,sK11_skl))|~sQ6_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f346,f73])).
% 20.60/3.50 fof(f351,definition,(
% 20.60/3.50 sQ17_spl <=> (aElement0(sdtasdt0(sK11_skl,sK11_skl)))),
% 20.60/3.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 20.60/3.50 fof(f354,plain,(
% 20.60/3.50 ~sQ3_spl|sQ17_spl|~sQ6_spl),
% 20.60/3.50 inference(split_clause,[status(thm)],[f350,f181,f351,f192])).
% 20.60/3.50 fof(f388,plain,(
% 20.60/3.50 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sK11_skl),xJ))),
% 20.60/3.50 inference(resolution,[status(thm)],[f123,f286])).
% 20.60/3.50 fof(f391,plain,(
% 20.60/3.50 aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xJ)|~sQ6_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f388,f193])).
% 20.60/3.50 fof(f392,plain,(
% 20.60/3.50 aElementOf0(sdtasdt0(sK13_skl,sK11_skl),xJ)|~sQ1_spl),
% 20.60/3.50 inference(resolution,[status(thm)],[f388,f159])).
% 20.60/3.50 fof(f393,plain,(
% 20.60/3.50 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sK11_skl)),xJ)|~sQ6_spl)),
% 20.60/3.50 inference(resolution,[status(thm)],[f391,f123])).
% 20.60/3.50 fof(f394,plain,(
% 20.60/3.50 aElementOf0(sdtasdt0(sK11_skl,sK11_skl),sdtasasdt0(xI,xJ))|~aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xI)|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f391,f134])).
% 20.60/3.51 fof(f397,definition,(
% 20.60/3.51 sQ19_spl <=> (aElementOf0(sdtasdt0(sK11_skl,sK11_skl),sdtasasdt0(xI,xJ)))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f398,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK11_skl,sK11_skl),sdtasasdt0(xI,xJ))|~sQ19_spl),
% 20.60/3.51 inference(component_clause,[status(thm)],[f397])).
% 20.60/3.51 fof(f400,definition,(
% 20.60/3.51 sQ20_spl <=> (aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xI))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f402,plain,(
% 20.60/3.51 ~aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xI)|sQ20_spl),
% 20.60/3.51 inference(component_clause,[status(thm)],[f400])).
% 20.60/3.51 fof(f403,plain,(
% 20.60/3.51 sQ19_spl|~sQ20_spl|~sQ6_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f394,f397,f400,f192])).
% 20.60/3.51 fof(f405,plain,(
% 20.60/3.51 $false|sQ9_spl),
% 20.60/3.51 inference(forward_subsumption_resolution,[status(thm)],[f291,f121])).
% 20.60/3.51 fof(f406,plain,(
% 20.60/3.51 sQ9_spl),
% 20.60/3.51 inference(contradiction_clause,[status(thm)],[f405])).
% 20.60/3.51 fof(f407,plain,(
% 20.60/3.51 $false|~sQ6_spl|sQ20_spl),
% 20.60/3.51 inference(forward_subsumption_resolution,[status(thm)],[f402,f346])).
% 20.60/3.51 fof(f408,plain,(
% 20.60/3.51 ~sQ6_spl|sQ20_spl),
% 20.60/3.51 inference(contradiction_clause,[status(thm)],[f407])).
% 20.60/3.51 fof(f410,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK13_skl,sK11_skl),sdtasasdt0(xI,xJ))|~aElementOf0(sdtasdt0(sK13_skl,sK11_skl),xI)|~sQ1_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f392,f134])).
% 20.60/3.51 fof(f413,definition,(
% 20.60/3.51 sQ21_spl <=> (aElementOf0(sdtasdt0(sK13_skl,sK11_skl),xI))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f415,plain,(
% 20.60/3.51 ~aElementOf0(sdtasdt0(sK13_skl,sK11_skl),xI)|sQ21_spl),
% 20.60/3.51 inference(component_clause,[status(thm)],[f413])).
% 20.60/3.51 fof(f416,plain,(
% 20.60/3.51 sQ2_spl|~sQ21_spl|~sQ1_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f410,f162,f413,f158])).
% 20.60/3.51 fof(f418,plain,(
% 20.60/3.51 $false|~sQ1_spl|sQ21_spl),
% 20.60/3.51 inference(forward_subsumption_resolution,[status(thm)],[f415,f347])).
% 20.60/3.51 fof(f419,plain,(
% 20.60/3.51 ~sQ1_spl|sQ21_spl),
% 20.60/3.51 inference(contradiction_clause,[status(thm)],[f418])).
% 20.60/3.51 fof(f420,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xJ)|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f185,f388])).
% 20.60/3.51 fof(f429,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xI)|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f185,f343])).
% 20.60/3.51 fof(f447,plain,(
% 20.60/3.51 aElementOf0(sK12_skl,xJ)|~sQ0_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f174,f133])).
% 20.60/3.51 fof(f474,plain,(
% 20.60/3.51 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sK11_skl)),xJ)|~sQ4_spl)),
% 20.60/3.51 inference(resolution,[status(thm)],[f420,f123])).
% 20.60/3.51 fof(f475,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sK11_skl),sdtasasdt0(xI,xJ))|~aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xI)|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f420,f134])).
% 20.60/3.51 fof(f477,plain,(
% 20.60/3.51 ~aSet0(xJ)|aElement0(sdtasdt0(sK12_skl,sK11_skl))|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f420,f73])).
% 20.60/3.51 fof(f478,definition,(
% 20.60/3.51 sQ24_spl <=> (aElementOf0(sdtasdt0(sK12_skl,sK11_skl),sdtasasdt0(xI,xJ)))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f479,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sK11_skl),sdtasasdt0(xI,xJ))|~sQ24_spl),
% 20.60/3.51 inference(component_clause,[status(thm)],[f478])).
% 20.60/3.51 fof(f481,definition,(
% 20.60/3.51 sQ25_spl <=> (aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xI))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f483,plain,(
% 20.60/3.51 ~aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xI)|sQ25_spl),
% 20.60/3.51 inference(component_clause,[status(thm)],[f481])).
% 20.60/3.51 fof(f484,plain,(
% 20.60/3.51 sQ24_spl|~sQ25_spl|~sQ4_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f475,f478,f481,f184])).
% 20.60/3.51 fof(f485,definition,(
% 20.60/3.51 sQ26_spl <=> (aElement0(sdtasdt0(sK12_skl,sK11_skl)))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f488,plain,(
% 20.60/3.51 ~sQ9_spl|sQ26_spl|~sQ4_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f477,f289,f485,f184])).
% 20.60/3.51 fof(f489,plain,(
% 20.60/3.51 ![X0]: (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sK11_skl)),xI)|~sQ4_spl)),
% 20.60/3.51 inference(resolution,[status(thm)],[f429,f119])).
% 20.60/3.51 fof(f562,plain,(
% 20.60/3.51 $false|~sQ4_spl|sQ25_spl),
% 20.60/3.51 inference(forward_subsumption_resolution,[status(thm)],[f483,f429])).
% 20.60/3.51 fof(f563,plain,(
% 20.60/3.51 ~sQ4_spl|sQ25_spl),
% 20.60/3.51 inference(contradiction_clause,[status(thm)],[f562])).
% 20.60/3.51 fof(f582,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)),xI)|~sQ6_spl|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f348,f185])).
% 20.60/3.51 fof(f585,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)),xI)|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f348,f193])).
% 20.60/3.51 fof(f616,plain,(
% 20.60/3.51 ~aSet0(xI)|aElement0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)))|~sQ6_spl|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f582,f73])).
% 20.60/3.51 fof(f617,definition,(
% 20.60/3.51 sQ30_spl <=> (aElement0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl))))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f620,plain,(
% 20.60/3.51 ~sQ3_spl|sQ30_spl|~sQ6_spl|~sQ4_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f616,f181,f617,f192,f184])).
% 20.60/3.51 fof(f664,plain,(
% 20.60/3.51 ~aSet0(xI)|aElement0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)))|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f585,f73])).
% 20.60/3.51 fof(f665,definition,(
% 20.60/3.51 sQ31_spl <=> (aElement0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl))))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f668,plain,(
% 20.60/3.51 ~sQ3_spl|sQ31_spl|~sQ6_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f664,f181,f665,f192])).
% 20.60/3.51 fof(f712,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)),xJ)|~sQ6_spl|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f393,f185])).
% 20.60/3.51 fof(f715,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)),xJ)|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f393,f193])).
% 20.60/3.51 fof(f743,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)),xJ)|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f474,f185])).
% 20.60/3.51 fof(f746,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)),xJ)|~sQ4_spl|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f474,f193])).
% 20.60/3.51 fof(f750,plain,(
% 20.60/3.51 ~aSet0(xJ)|aElement0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)))|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f743,f73])).
% 20.60/3.51 fof(f758,definition,(
% 20.60/3.51 sQ38_spl <=> (aElement0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl))))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f761,plain,(
% 20.60/3.51 ~sQ9_spl|sQ38_spl|~sQ4_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f750,f289,f758,f184])).
% 20.60/3.51 fof(f808,plain,(
% 20.60/3.51 ~aSet0(xJ)|aElement0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)))|~sQ4_spl|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f746,f73])).
% 20.60/3.51 fof(f816,definition,(
% 20.60/3.51 sQ41_spl <=> (aElement0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl))))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f819,plain,(
% 20.60/3.51 ~sQ9_spl|sQ41_spl|~sQ4_spl|~sQ6_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f808,f289,f816,f184,f192])).
% 20.60/3.51 fof(f867,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)),xI)|~sQ4_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f489,f185])).
% 20.60/3.51 fof(f870,plain,(
% 20.60/3.51 aElementOf0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)),xI)|~sQ4_spl|~sQ6_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f489,f193])).
% 20.60/3.51 fof(f1375,plain,(
% 20.60/3.51 ~aSet0(xI)|~aSet0(xJ)|aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xJ)|~sQ24_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f171,f479])).
% 20.60/3.51 fof(f1376,plain,(
% 20.60/3.51 ~aSet0(xI)|~aSet0(xJ)|aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xJ)|~sQ19_spl),
% 20.60/3.51 inference(resolution,[status(thm)],[f171,f398])).
% 20.60/3.51 fof(f1377,plain,(
% 20.60/3.51 ~aSet0(xI)|~aSet0(xJ)|aElementOf0(sK11_skl,xJ)),
% 20.60/3.51 inference(resolution,[status(thm)],[f171,f135])).
% 20.60/3.51 fof(f1386,definition,(
% 20.60/3.51 sQ50_spl <=> (aElementOf0(sdtasdt0(sK12_skl,sK11_skl),xJ))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f1389,plain,(
% 20.60/3.51 ~sQ3_spl|~sQ9_spl|sQ50_spl|~sQ24_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f1375,f181,f289,f1386,f478])).
% 20.60/3.51 fof(f1390,definition,(
% 20.60/3.51 sQ51_spl <=> (aElementOf0(sdtasdt0(sK11_skl,sK11_skl),xJ))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f1393,plain,(
% 20.60/3.51 ~sQ3_spl|~sQ9_spl|sQ51_spl|~sQ19_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f1376,f181,f289,f1390,f397])).
% 20.60/3.51 fof(f1394,definition,(
% 20.60/3.51 sQ52_spl <=> (aElementOf0(sK11_skl,xJ))),
% 20.60/3.51 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 20.60/3.51 fof(f1397,plain,(
% 20.60/3.51 ~sQ3_spl|~sQ9_spl|sQ52_spl),
% 20.60/3.51 inference(split_clause,[status(thm)],[f1377,f181,f289,f1394])).
% 20.60/3.51 fof(f2418,plain,(
% 20.60/3.51 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl))),xI)|~sQ4_spl)),
% 20.60/3.51 inference(resolution,[status(thm)],[f108,f867])).
% 20.60/3.51 fof(f2419,plain,(
% 20.60/3.51 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl))),xJ)|~sQ4_spl)),
% 20.60/3.51 inference(resolution,[status(thm)],[f108,f743])).
% 20.60/3.51 fof(f2420,plain,(
% 20.60/3.51 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl))),xJ)|~sQ6_spl|~sQ4_spl)),
% 20.60/3.51 inference(resolution,[status(thm)],[f108,f712])).
% 20.60/3.52 fof(f2421,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl))),xI)|~sQ6_spl|~sQ4_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f582])).
% 20.60/3.52 fof(f2426,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sK11_skl)),xI)|~sQ4_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f429])).
% 20.60/3.52 fof(f2427,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sK11_skl)),xJ)|~sQ4_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f420])).
% 20.60/3.52 fof(f2430,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl))),xI)|~sQ4_spl|~sQ6_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f870])).
% 20.60/3.52 fof(f2431,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl))),xJ)|~sQ4_spl|~sQ6_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f746])).
% 20.60/3.52 fof(f2432,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl))),xJ)|~sQ6_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f715])).
% 20.60/3.52 fof(f2433,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl))),xI)|~sQ6_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f585])).
% 20.60/3.52 fof(f2435,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sK11_skl)),xJ)|~sQ6_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f391])).
% 20.60/3.52 fof(f2436,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sK11_skl)),xI)|~sQ6_spl)),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f346])).
% 20.60/3.52 fof(f2437,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sK11_skl),xJ))),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f286])).
% 20.60/3.52 fof(f2438,plain,(
% 20.60/3.52 ![X0]: (~aIdeal0(xI)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sK11_skl),xI))),
% 20.60/3.52 inference(resolution,[status(thm)],[f108,f176])).
% 20.60/3.52 fof(f2440,definition,(
% 20.60/3.52 sQ56_spl <=> (aIdeal0(xJ))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 20.60/3.52 fof(f2442,plain,(
% 20.60/3.52 ~aIdeal0(xJ)|sQ56_spl),
% 20.60/3.52 inference(component_clause,[status(thm)],[f2440])).
% 20.60/3.52 fof(f2451,definition,(
% 20.60/3.52 sQ59_spl <=> (aIdeal0(xI))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 20.60/3.52 fof(f2453,plain,(
% 20.60/3.52 ~aIdeal0(xI)|sQ59_spl),
% 20.60/3.52 inference(component_clause,[status(thm)],[f2451])).
% 20.60/3.52 fof(f2474,definition,(
% 20.60/3.52 ![X0]: (sQ65_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl))),xI)))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 20.60/3.52 fof(f2477,plain,(
% 20.60/3.52 ~sQ59_spl|sQ65_spl|~sQ4_spl),
% 20.60/3.52 inference(split_clause,[status(thm)],[f2418,f2451,f2474,f184])).
% 20.60/3.52 fof(f2478,definition,(
% 20.60/3.52 ![X0]: (sQ66_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl))),xJ)))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 20.60/3.52 fof(f2481,plain,(
% 20.60/3.52 ~sQ56_spl|sQ66_spl|~sQ4_spl),
% 20.60/3.52 inference(split_clause,[status(thm)],[f2419,f2440,f2478,f184])).
% 20.60/3.52 fof(f2482,definition,(
% 20.60/3.52 ![X0]: (sQ67_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl))),xJ)))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 20.60/3.52 fof(f2485,plain,(
% 20.60/3.52 ~sQ56_spl|sQ67_spl|~sQ6_spl|~sQ4_spl),
% 20.60/3.52 inference(split_clause,[status(thm)],[f2420,f2440,f2482,f192,f184])).
% 20.60/3.52 fof(f2486,definition,(
% 20.60/3.52 ![X0]: (sQ68_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl))),xI)))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 20.60/3.52 fof(f2489,plain,(
% 20.60/3.52 ~sQ59_spl|sQ68_spl|~sQ6_spl|~sQ4_spl),
% 20.60/3.52 inference(split_clause,[status(thm)],[f2421,f2451,f2486,f192,f184])).
% 20.60/3.52 fof(f2506,definition,(
% 20.60/3.52 ![X0]: (sQ73_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sK11_skl)),xI)))),
% 20.60/3.52 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2509,plain,(
% 20.60/3.53 ~sQ59_spl|sQ73_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2426,f2451,f2506,f184])).
% 20.60/3.53 fof(f2510,definition,(
% 20.60/3.53 ![X0]: (sQ74_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK12_skl,sK11_skl)),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2513,plain,(
% 20.60/3.53 ~sQ56_spl|sQ74_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2427,f2440,f2510,f184])).
% 20.60/3.53 fof(f2522,definition,(
% 20.60/3.53 ![X0]: (sQ77_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl))),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2525,plain,(
% 20.60/3.53 ~sQ59_spl|sQ77_spl|~sQ4_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2430,f2451,f2522,f184,f192])).
% 20.60/3.53 fof(f2526,definition,(
% 20.60/3.53 ![X0]: (sQ78_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl))),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2529,plain,(
% 20.60/3.53 ~sQ56_spl|sQ78_spl|~sQ4_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2431,f2440,f2526,f184,f192])).
% 20.60/3.53 fof(f2530,definition,(
% 20.60/3.53 ![X0]: (sQ79_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl))),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2533,plain,(
% 20.60/3.53 ~sQ56_spl|sQ79_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2432,f2440,f2530,f192])).
% 20.60/3.53 fof(f2534,definition,(
% 20.60/3.53 ![X0]: (sQ80_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl))),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2537,plain,(
% 20.60/3.53 ~sQ59_spl|sQ80_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2433,f2451,f2534,f192])).
% 20.60/3.53 fof(f2542,definition,(
% 20.60/3.53 ![X0]: (sQ82_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sK11_skl)),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2545,plain,(
% 20.60/3.53 ~sQ56_spl|sQ82_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2435,f2440,f2542,f192])).
% 20.60/3.53 fof(f2546,definition,(
% 20.60/3.53 ![X0]: (sQ83_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtasdt0(sK11_skl,sK11_skl)),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2549,plain,(
% 20.60/3.53 ~sQ59_spl|sQ83_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2436,f2451,f2546,f192])).
% 20.60/3.53 fof(f2550,definition,(
% 20.60/3.53 ![X0]: (sQ84_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sK11_skl),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2553,plain,(
% 20.60/3.53 ~sQ56_spl|sQ84_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2437,f2440,f2550])).
% 20.60/3.53 fof(f2554,definition,(
% 20.60/3.53 ![X0]: (sQ85_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sK11_skl),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2557,plain,(
% 20.60/3.53 ~sQ59_spl|sQ85_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2438,f2451,f2554])).
% 20.60/3.53 fof(f2562,plain,(
% 20.60/3.53 $false|sQ56_spl),
% 20.60/3.53 inference(forward_subsumption_resolution,[status(thm)],[f2442,f124])).
% 20.60/3.53 fof(f2563,plain,(
% 20.60/3.53 sQ56_spl),
% 20.60/3.53 inference(contradiction_clause,[status(thm)],[f2562])).
% 20.60/3.53 fof(f2564,plain,(
% 20.60/3.53 $false|sQ59_spl),
% 20.60/3.53 inference(forward_subsumption_resolution,[status(thm)],[f2453,f120])).
% 20.60/3.53 fof(f2565,plain,(
% 20.60/3.53 sQ59_spl),
% 20.60/3.53 inference(contradiction_clause,[status(thm)],[f2564])).
% 20.60/3.53 fof(f2573,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xI)|~sQ4_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f867])).
% 20.60/3.53 fof(f2574,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xJ)|~sQ4_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f743])).
% 20.60/3.53 fof(f2575,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xJ)|~sQ6_spl|~sQ4_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f712])).
% 20.60/3.53 fof(f2576,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xI)|~sQ6_spl|~sQ4_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f582])).
% 20.60/3.53 fof(f2581,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sK11_skl),X0),xI)|~sQ4_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f429])).
% 20.60/3.53 fof(f2582,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sK11_skl),X0),xJ)|~sQ4_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f420])).
% 20.60/3.53 fof(f2585,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xI)|~sQ4_spl|~sQ6_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f870])).
% 20.60/3.53 fof(f2586,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xJ)|~sQ4_spl|~sQ6_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f746])).
% 20.60/3.53 fof(f2587,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xJ)|~sQ6_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f715])).
% 20.60/3.53 fof(f2588,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xI)|~sQ6_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f585])).
% 20.60/3.53 fof(f2590,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sK11_skl),X0),xJ)|~sQ6_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f391])).
% 20.60/3.53 fof(f2591,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sK11_skl),X0),xI)|~sQ6_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f346])).
% 20.60/3.53 fof(f2592,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sK11_skl,X0),xJ))),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f286])).
% 20.60/3.53 fof(f2593,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xI)|~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sK11_skl,X0),xI))),
% 20.60/3.53 inference(resolution,[status(thm)],[f107,f176])).
% 20.60/3.53 fof(f2623,definition,(
% 20.60/3.53 ![X0]: (sQ94_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2626,plain,(
% 20.60/3.53 ~sQ59_spl|sQ94_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2573,f2451,f2623,f184])).
% 20.60/3.53 fof(f2627,definition,(
% 20.60/3.53 ![X0]: (sQ95_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2630,plain,(
% 20.60/3.53 ~sQ56_spl|sQ95_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2574,f2440,f2627,f184])).
% 20.60/3.53 fof(f2631,definition,(
% 20.60/3.53 ![X0]: (sQ96_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2634,plain,(
% 20.60/3.53 ~sQ56_spl|sQ96_spl|~sQ6_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2575,f2440,f2631,f192,f184])).
% 20.60/3.53 fof(f2635,definition,(
% 20.60/3.53 ![X0]: (sQ97_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2638,plain,(
% 20.60/3.53 ~sQ59_spl|sQ97_spl|~sQ6_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2576,f2451,f2635,f192,f184])).
% 20.60/3.53 fof(f2655,definition,(
% 20.60/3.53 ![X0]: (sQ102_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sK11_skl),X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2658,plain,(
% 20.60/3.53 ~sQ59_spl|sQ102_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2581,f2451,f2655,f184])).
% 20.60/3.53 fof(f2659,definition,(
% 20.60/3.53 ![X0]: (sQ103_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK12_skl,sK11_skl),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2662,plain,(
% 20.60/3.53 ~sQ56_spl|sQ103_spl|~sQ4_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2582,f2440,f2659,f184])).
% 20.60/3.53 fof(f2671,definition,(
% 20.60/3.53 ![X0]: (sQ106_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2674,plain,(
% 20.60/3.53 ~sQ59_spl|sQ106_spl|~sQ4_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2585,f2451,f2671,f184,f192])).
% 20.60/3.53 fof(f2675,definition,(
% 20.60/3.53 ![X0]: (sQ107_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK12_skl,sK11_skl)),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2678,plain,(
% 20.60/3.53 ~sQ56_spl|sQ107_spl|~sQ4_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2586,f2440,f2675,f184,f192])).
% 20.60/3.53 fof(f2679,definition,(
% 20.60/3.53 ![X0]: (sQ108_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2682,plain,(
% 20.60/3.53 ~sQ56_spl|sQ108_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2587,f2440,f2679,f192])).
% 20.60/3.53 fof(f2683,definition,(
% 20.60/3.53 ![X0]: (sQ109_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sdtasdt0(sK11_skl,sK11_skl)),X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2686,plain,(
% 20.60/3.53 ~sQ59_spl|sQ109_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2588,f2451,f2683,f192])).
% 20.60/3.53 fof(f2691,definition,(
% 20.60/3.53 ![X0]: (sQ111_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sK11_skl),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2694,plain,(
% 20.60/3.53 ~sQ56_spl|sQ111_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2590,f2440,f2691,f192])).
% 20.60/3.53 fof(f2695,definition,(
% 20.60/3.53 ![X0]: (sQ112_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sdtasdt0(sK11_skl,sK11_skl),X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2698,plain,(
% 20.60/3.53 ~sQ59_spl|sQ112_spl|~sQ6_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2591,f2451,f2695,f192])).
% 20.60/3.53 fof(f2699,definition,(
% 20.60/3.53 ![X0]: (sQ113_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sK11_skl,X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2700,plain,(
% 20.60/3.53 ![X0]: (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sK11_skl,X0),xJ)|~sQ113_spl)),
% 20.60/3.53 inference(component_clause,[status(thm)],[f2699])).
% 20.60/3.53 fof(f2702,plain,(
% 20.60/3.53 ~sQ56_spl|sQ113_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2592,f2440,f2699])).
% 20.60/3.53 fof(f2703,definition,(
% 20.60/3.53 ![X0]: (sQ114_spl <=> (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sK11_skl,X0),xI)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2704,plain,(
% 20.60/3.53 ![X0]: (~aElementOf0(X0,xI)|aElementOf0(sdtpldt0(sK11_skl,X0),xI)|~sQ114_spl)),
% 20.60/3.53 inference(component_clause,[status(thm)],[f2703])).
% 20.60/3.53 fof(f2706,plain,(
% 20.60/3.53 ~sQ59_spl|sQ114_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2593,f2451,f2703])).
% 20.60/3.53 fof(f2711,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK11_skl,sK12_skl),xJ)|~sQ113_spl|~sQ0_spl),
% 20.60/3.53 inference(resolution,[status(thm)],[f2700,f447])).
% 20.60/3.53 fof(f2722,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK11_skl,sK11_skl),xJ)|~sQ113_spl),
% 20.60/3.53 inference(resolution,[status(thm)],[f2700,f286])).
% 20.60/3.53 fof(f2723,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK12_skl,sK11_skl),xJ)|~sQ4_spl|~sQ6_spl|~sQ113_spl|~sQ0_spl),
% 20.60/3.53 inference(forward_demodulation,[status(thm)],[f240,f2711])).
% 20.60/3.53 fof(f2726,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK12_skl,sK11_skl),sdtasasdt0(xI,xJ))|~aElementOf0(sdtpldt0(sK12_skl,sK11_skl),xI)|~sQ4_spl|~sQ6_spl|~sQ113_spl|~sQ0_spl),
% 20.60/3.53 inference(resolution,[status(thm)],[f2723,f134])).
% 20.60/3.53 fof(f2731,definition,(
% 20.60/3.53 sQ116_spl <=> (aElementOf0(sdtpldt0(sK12_skl,sK11_skl),xI))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2733,plain,(
% 20.60/3.53 ~aElementOf0(sdtpldt0(sK12_skl,sK11_skl),xI)|sQ116_spl),
% 20.60/3.53 inference(component_clause,[status(thm)],[f2731])).
% 20.60/3.53 fof(f2734,plain,(
% 20.60/3.53 sQ14_spl|~sQ116_spl|~sQ4_spl|~sQ6_spl|~sQ113_spl|~sQ0_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2726,f310,f2731,f184,f192,f2699,f155])).
% 20.60/3.53 fof(f2749,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK11_skl,sK11_skl),sdtasasdt0(xI,xJ))|~aElementOf0(sdtpldt0(sK11_skl,sK11_skl),xI)|~sQ113_spl),
% 20.60/3.53 inference(resolution,[status(thm)],[f2722,f134])).
% 20.60/3.53 fof(f2750,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtpldt0(sK11_skl,sK11_skl),X0),xJ)|~sQ113_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f2722,f107])).
% 20.60/3.53 fof(f2751,plain,(
% 20.60/3.53 ![X0]: (~aIdeal0(xJ)|~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtpldt0(sK11_skl,sK11_skl)),xJ)|~sQ113_spl)),
% 20.60/3.53 inference(resolution,[status(thm)],[f2722,f108])).
% 20.60/3.53 fof(f2753,plain,(
% 20.60/3.53 ~aSet0(xJ)|aElement0(sdtpldt0(sK11_skl,sK11_skl))|~sQ113_spl),
% 20.60/3.53 inference(resolution,[status(thm)],[f2722,f73])).
% 20.60/3.53 fof(f2754,definition,(
% 20.60/3.53 sQ120_spl <=> (aElementOf0(sdtpldt0(sK11_skl,sK11_skl),sdtasasdt0(xI,xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2757,definition,(
% 20.60/3.53 sQ121_spl <=> (aElementOf0(sdtpldt0(sK11_skl,sK11_skl),xI))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2760,plain,(
% 20.60/3.53 sQ120_spl|~sQ121_spl|~sQ113_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2749,f2754,f2757,f2699])).
% 20.60/3.53 fof(f2761,definition,(
% 20.60/3.53 ![X0]: (sQ122_spl <=> (~aElementOf0(X0,xJ)|aElementOf0(sdtpldt0(sdtpldt0(sK11_skl,sK11_skl),X0),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2764,plain,(
% 20.60/3.53 ~sQ56_spl|sQ122_spl|~sQ113_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2750,f2440,f2761,f2699])).
% 20.60/3.53 fof(f2765,definition,(
% 20.60/3.53 ![X0]: (sQ123_spl <=> (~aElement0(X0)|aElementOf0(sdtasdt0(X0,sdtpldt0(sK11_skl,sK11_skl)),xJ)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2768,plain,(
% 20.60/3.53 ~sQ56_spl|sQ123_spl|~sQ113_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2751,f2440,f2765,f2699])).
% 20.60/3.53 fof(f2769,definition,(
% 20.60/3.53 sQ124_spl <=> (aElement0(sdtpldt0(sK11_skl,sK11_skl)))),
% 20.60/3.53 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 20.60/3.53 fof(f2772,plain,(
% 20.60/3.53 ~sQ9_spl|sQ124_spl|~sQ113_spl),
% 20.60/3.53 inference(split_clause,[status(thm)],[f2753,f289,f2769,f2699])).
% 20.60/3.53 fof(f2773,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK11_skl,sK12_skl),xI)|~sQ114_spl|~sQ0_spl),
% 20.60/3.53 inference(resolution,[status(thm)],[f2704,f175])).
% 20.60/3.53 fof(f2785,plain,(
% 20.60/3.53 aElementOf0(sdtpldt0(sK12_skl,sK11_skl),xI)|~sQ4_spl|~sQ6_spl|~sQ114_spl|~sQ0_spl),
% 20.60/3.53 inference(forward_demodulation,[status(thm)],[f240,f2773])).
% 20.60/3.53 fof(f2786,plain,(
% 20.60/3.53 $false|sQ116_spl|~sQ4_spl|~sQ6_spl|~sQ114_spl|~sQ0_spl),
% 20.60/3.53 inference(forward_subsumption_resolution,[status(thm)],[f2785,f2733])).
% 20.60/3.53 fof(f2787,plain,(
% 20.60/3.53 sQ116_spl|~sQ4_spl|~sQ6_spl|~sQ114_spl|~sQ0_spl),
% 20.60/3.53 inference(contradiction_clause,[status(thm)],[f2786])).
% 20.60/3.53 fof(f2788,plain,(
% 20.60/3.53 $false),
% 20.60/3.53 inference(sat_refutation,[status(thm)],[f161,f165,f187,f196,f198,f234,f236,f313,f315,f323,f325,f354,f403,f406,f408,f416,f419,f484,f488,f563,f620,f668,f761,f819,f1389,f1393,f1397,f2477,f2481,f2485,f2489,f2509,f2513,f2525,f2529,f2533,f2537,f2545,f2549,f2553,f2557,f2563,f2565,f2626,f2630,f2634,f2638,f2658,f2662,f2674,f2678,f2682,f2686,f2694,f2698,f2702,f2706,f2734,f2760,f2764,f2768,f2772,f2787])).
% 20.60/3.55 % SZS output end CNFRefutation for theBenchmark.p
% 17.99/3.56 % Elapsed time: 2.982984 seconds
% 17.99/3.56 % CPU time: 23.237590 seconds
% 17.99/3.56 % Total memory used: 232.582 MB
% 17.99/3.56 % Net memory used: 216.759 MB
%------------------------------------------------------------------------------