%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM440+6 : 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 : n007.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 01:42:54 PM UTC 2026
% Result : Theorem 1.57s 0.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM440+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:27:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 1.57/0.81 % Refutation found
% 1.57/0.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.57/0.81 % SZS output start CNFRefutation for theBenchmark
% 1.57/0.81 fof(f5,axiom,(
% 1.57/0.81 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtpldt0(W0,W1)) ) )),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f10,axiom,(
% 1.57/0.81 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f28,definition,(
% 1.57/0.81 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f30,definition,(
% 1.57/0.81 (! [W0,W1] :( ( aSubsetOf0(W0,cS1395)& aSubsetOf0(W1,cS1395) )=> (! [W2] :( W2 = sdtbsmnsldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aInteger0(W3)& ( aElementOf0(W3,W0)| aElementOf0(W3,W1) ) ) ) )) ) )) )),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f36,definition,(
% 1.57/0.81 (! [W0] :( aSubsetOf0(W0,cS1395)=> ( isClosed0(W0)<=> isOpen0(stldt0(W0)) ) ) )),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f39,hypothesis,(
% 1.57/0.81 ( aSet0(cS1395)& (! [W0] :( aElementOf0(W0,cS1395)<=> aInteger0(W0) ))& aSet0(xA)& (! [W0] :( aElementOf0(W0,xA)=> aElementOf0(W0,cS1395) ))& aSubsetOf0(xA,cS1395)& aSet0(cS1395)& (! [W0] :( aElementOf0(W0,cS1395)<=> aInteger0(W0) ))& aSet0(xB)& (! [W0] :( aElementOf0(W0,xB)=> aElementOf0(W0,cS1395) ))& aSubsetOf0(xB,cS1395)& aSet0(stldt0(xA))& (! [W0] :( aElementOf0(W0,stldt0(xA))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xA) ) ))& (! [W0] :( aElementOf0(W0,stldt0(xA))=> (? [W1] :( aInteger0(W1)& W1 != sz00& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1))& (! [W2] :( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> ( aInteger0(W2)& (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))& sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )& ( ( aInteger0(W2)& ( (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))| sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ))& (! [W2] :( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> aElementOf0(W2,stldt0(xA)) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA)) ) )))& isOpen0(stldt0(xA))& isClosed0(xA)& aSet0(stldt0(xB))& (! [W0] :( aElementOf0(W0,stldt0(xB))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xB) ) ))& (! [W0] :( aElementOf0(W0,stldt0(xB))=> (? [W1] :( aInteger0(W1)& W1 != sz00& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1))& (! [W2] :( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> ( aInteger0(W2)& (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))& sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )& ( ( aInteger0(W2)& ( (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))| sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ))& (! [W2] :( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> aElementOf0(W2,stldt0(xB)) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB)) ) )))& isOpen0(stldt0(xB))& isClosed0(xB) ) ),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f40,conjecture,(
% 1.57/0.81 ( ( ( aSet0(stldt0(xA))& (! [W0] :( aElementOf0(W0,stldt0(xA))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xA) ) ) ))=> ( ( aSet0(cS1395)& (! [W0] :( aElementOf0(W0,cS1395)<=> aInteger0(W0) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xA))=> aElementOf0(W0,cS1395) ))| aSubsetOf0(stldt0(xA),cS1395) ) ) )& ( ( aSet0(stldt0(xB))& (! [W0] :( aElementOf0(W0,stldt0(xB))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xB) ) ) ))=> ( ( aSet0(cS1395)& (! [W0] :( aElementOf0(W0,cS1395)<=> aInteger0(W0) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xB))=> aElementOf0(W0,cS1395) ))| aSubsetOf0(stldt0(xB),cS1395) ) ) )& ( ( aSet0(sdtbsmnsldt0(xA,xB))& (! [W0] :( aElementOf0(W0,sdtbsmnsldt0(xA,xB))<=> ( aInteger0(W0)& ( aElementOf0(W0,xA)| aElementOf0(W0,xB) ) ) ) ))=> ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))& (! [W0] :( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xA))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xA) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xB))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xB) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<=> ( aInteger0(W0)& aElementOf0(W0,stldt0(xA))& aElementOf0(W0,stldt0(xB)) ) ))| stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)) ) ) ) ) ) ) ),
% 1.57/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.57/0.81 fof(f41,negated_conjecture,(
% 1.57/0.81 ~(( ( ( aSet0(stldt0(xA))& (! [W0] :( aElementOf0(W0,stldt0(xA))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xA) ) ) ))=> ( ( aSet0(cS1395)& (! [W0] :( aElementOf0(W0,cS1395)<=> aInteger0(W0) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xA))=> aElementOf0(W0,cS1395) ))| aSubsetOf0(stldt0(xA),cS1395) ) ) )& ( ( aSet0(stldt0(xB))& (! [W0] :( aElementOf0(W0,stldt0(xB))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xB) ) ) ))=> ( ( aSet0(cS1395)& (! [W0] :( aElementOf0(W0,cS1395)<=> aInteger0(W0) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xB))=> aElementOf0(W0,cS1395) ))| aSubsetOf0(stldt0(xB),cS1395) ) ) )& ( ( aSet0(sdtbsmnsldt0(xA,xB))& (! [W0] :( aElementOf0(W0,sdtbsmnsldt0(xA,xB))<=> ( aInteger0(W0)& ( aElementOf0(W0,xA)| aElementOf0(W0,xB) ) ) ) ))=> ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))& (! [W0] :( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xA))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xA) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(xB))<=> ( aInteger0(W0)& ~ aElementOf0(W0,xB) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<=> ( aInteger0(W0)& aElementOf0(W0,stldt0(xA))& aElementOf0(W0,stldt0(xB)) ) ))| stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)) ) ) ) ) ) ) )),
% 1.57/0.81 inference(negated_conjecture,[status(cth)],[f40])).
% 1.57/0.81 fof(f49,plain,(
% 1.57/0.81 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtpldt0(W0,W1)))),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 1.57/0.81 fof(f50,plain,(
% 1.57/0.81 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtpldt0(X0,X1)))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f49])).
% 1.57/0.81 fof(f60,plain,(
% 1.57/0.81 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 1.57/0.81 fof(f61,plain,(
% 1.57/0.81 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f60])).
% 1.57/0.81 fof(f118,plain,(
% 1.57/0.81 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 1.57/0.81 fof(f119,plain,(
% 1.57/0.81 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 1.57/0.81 inference(NNF_transformation,[status(thm)],[f118])).
% 1.57/0.81 fof(f120,plain,(
% 1.57/0.81 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 1.57/0.81 inference(miniscoping,[status(thm)],[f119])).
% 1.57/0.81 fof(f121,plain,(
% 1.57/0.81 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK2_skl(W1,W0),W1)&~aElementOf0(sK2_skl(W1,W0),W0)))))))),
% 1.57/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W2,sK2_skl(W1,W0))],[f120])).
% 1.57/0.81 fof(f122,plain,(
% 1.57/0.81 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f121])).
% 1.57/0.81 fof(f123,plain,(
% 1.57/0.81 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f121])).
% 1.57/0.81 fof(f128,plain,(
% 1.57/0.81 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|(![W2]: (W2=sdtbsmnsldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))))))),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 1.57/0.81 fof(f129,plain,(
% 1.57/0.81 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|(![W2]: ((~W2=sdtbsmnsldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1))))&(aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1))))))))&(W2=sdtbsmnsldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1))))&(aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))))))))),
% 1.57/0.81 inference(NNF_transformation,[status(thm)],[f128])).
% 1.57/0.81 fof(f130,plain,(
% 1.57/0.81 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|((![W2]: (~W2=sdtbsmnsldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))&(![W3]: (aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1)))))))))&(![W2]: (W2=sdtbsmnsldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1))))&(aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))))))))),
% 1.57/0.81 inference(miniscoping,[status(thm)],[f129])).
% 1.57/0.81 fof(f131,plain,(
% 1.57/0.81 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|((![W2]: (~W2=sdtbsmnsldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))&(![W3]: (aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1)))))))))&(![W2]: (W2=sdtbsmnsldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK3_skl(W2,W1,W0),W2)|(~aInteger0(sK3_skl(W2,W1,W0))|(~aElementOf0(sK3_skl(W2,W1,W0),W0)&~aElementOf0(sK3_skl(W2,W1,W0),W1))))&(aElementOf0(sK3_skl(W2,W1,W0),W2)|(aInteger0(sK3_skl(W2,W1,W0))&(aElementOf0(sK3_skl(W2,W1,W0),W0)|aElementOf0(sK3_skl(W2,W1,W0),W1))))))))))),
% 1.57/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f130])).
% 1.57/0.81 fof(f133,plain,(
% 1.57/0.81 ![X0,X1,X2,X3]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|~X2=sdtbsmnsldt0(X0,X1)|~aElementOf0(X3,X2)|aInteger0(X3))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f131])).
% 1.57/0.81 fof(f134,plain,(
% 1.57/0.81 ![X0,X1,X2,X3]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|~X2=sdtbsmnsldt0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(X3,X0)|aElementOf0(X3,X1))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f131])).
% 1.57/0.81 fof(f136,plain,(
% 1.57/0.81 ![X0,X1,X2,X3]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|~X2=sdtbsmnsldt0(X0,X1)|aElementOf0(X3,X2)|~aInteger0(X3)|~aElementOf0(X3,X1))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f131])).
% 1.57/0.81 fof(f197,plain,(
% 1.57/0.81 ![W0]: (~aSubsetOf0(W0,cS1395)|(isClosed0(W0)<=>isOpen0(stldt0(W0))))),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 1.57/0.81 fof(f198,plain,(
% 1.57/0.81 ![W0]: (~aSubsetOf0(W0,cS1395)|((~isClosed0(W0)|isOpen0(stldt0(W0)))&(isClosed0(W0)|~isOpen0(stldt0(W0)))))),
% 1.57/0.81 inference(NNF_transformation,[status(thm)],[f197])).
% 1.57/0.81 fof(f199,plain,(
% 1.57/0.81 ![X0]: (~aSubsetOf0(X0,cS1395)|~isClosed0(X0)|isOpen0(stldt0(X0)))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f198])).
% 1.57/0.81 fof(f207,plain,(
% 1.57/0.81 ((((((((((((((((((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&aSet0(xA))&(![W0]: (~aElementOf0(W0,xA)|aElementOf0(W0,cS1395))))&aSubsetOf0(xA,cS1395))&aSet0(cS1395))&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&aSet0(xB))&(![W0]: (~aElementOf0(W0,xB)|aElementOf0(W0,cS1395))))&aSubsetOf0(xB,cS1395))&aSet0(stldt0(xA)))&(![W0]: (aElementOf0(W0,stldt0(xA))<=>(aInteger0(W0)&~aElementOf0(W0,xA)))))&(![W0]: (~aElementOf0(W0,stldt0(xA))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(xA)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA)))))))&isOpen0(stldt0(xA)))&isClosed0(xA))&aSet0(stldt0(xB)))&(![W0]: (aElementOf0(W0,stldt0(xB))<=>(aInteger0(W0)&~aElementOf0(W0,xB)))))&(![W0]: (~aElementOf0(W0,stldt0(xB))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(xB)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB)))))))&isOpen0(stldt0(xB)))&isClosed0(xB)),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 1.57/0.81 fof(f208,plain,(
% 1.57/0.81 ((((((((((((((((((aSet0(cS1395)&(![W0]: ((~aElementOf0(W0,cS1395)|aInteger0(W0))&(aElementOf0(W0,cS1395)|~aInteger0(W0)))))&aSet0(xA))&(![W0]: (~aElementOf0(W0,xA)|aElementOf0(W0,cS1395))))&aSubsetOf0(xA,cS1395))&aSet0(cS1395))&(![W0]: ((~aElementOf0(W0,cS1395)|aInteger0(W0))&(aElementOf0(W0,cS1395)|~aInteger0(W0)))))&aSet0(xB))&(![W0]: (~aElementOf0(W0,xB)|aElementOf0(W0,cS1395))))&aSubsetOf0(xB,cS1395))&aSet0(stldt0(xA)))&(![W0]: ((~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA)))&(aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA))))))&(![W0]: (~aElementOf0(W0,stldt0(xA))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(xA)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA)))))))&isOpen0(stldt0(xA)))&isClosed0(xA))&aSet0(stldt0(xB)))&(![W0]: ((~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB)))&(aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB))))))&(![W0]: (~aElementOf0(W0,stldt0(xB))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(xB)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB)))))))&isOpen0(stldt0(xB)))&isClosed0(xB)),
% 1.57/0.81 inference(NNF_transformation,[status(thm)],[f207])).
% 1.57/0.81 fof(f209,plain,(
% 1.57/0.81 ((((((((((((((((((aSet0(cS1395)&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&aSet0(xA))&(![W0]: (~aElementOf0(W0,xA)|aElementOf0(W0,cS1395))))&aSubsetOf0(xA,cS1395))&aSet0(cS1395))&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&aSet0(xB))&(![W0]: (~aElementOf0(W0,xB)|aElementOf0(W0,cS1395))))&aSubsetOf0(xB,cS1395))&aSet0(stldt0(xA)))&((![W0]: (~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))&(![W0]: (aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA))))))&(![W0]: (~aElementOf0(W0,stldt0(xA))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(xA)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA)))))))&isOpen0(stldt0(xA)))&isClosed0(xA))&aSet0(stldt0(xB)))&((![W0]: (~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))&(![W0]: (aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB))))))&(![W0]: (~aElementOf0(W0,stldt0(xB))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(xB)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB)))))))&isOpen0(stldt0(xB)))&isClosed0(xB)),
% 1.57/0.81 inference(miniscoping,[status(thm)],[f208])).
% 1.57/0.81 fof(f210,plain,(
% 1.57/0.81 ((((((((((((((((((aSet0(cS1395)&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&aSet0(xA))&(![W0]: (~aElementOf0(W0,xA)|aElementOf0(W0,cS1395))))&aSubsetOf0(xA,cS1395))&aSet0(cS1395))&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&aSet0(xB))&(![W0]: (~aElementOf0(W0,xB)|aElementOf0(W0,cS1395))))&aSubsetOf0(xB,cS1395))&aSet0(stldt0(xA)))&((![W0]: (~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))&(![W0]: (aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA))))))&(![W0]: (~aElementOf0(W0,stldt0(xA))|(((((aInteger0(sK14_skl(W0))&~sK14_skl(W0)=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK14_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK14_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK15_skl(W2,W0))&sdtasdt0(sK14_skl(W0),sK15_skl(W2,W0))=sdtpldt0(W2,smndt0(W0))))&aDivisorOf0(sK14_skl(W0),sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,sK14_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK14_skl(W0),W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(sK14_skl(W0),sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,sK14_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK14_skl(W0)))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK14_skl(W0)))|aElementOf0(W2,stldt0(xA)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK14_skl(W0)),stldt0(xA))))))&isOpen0(stldt0(xA)))&isClosed0(xA))&aSet0(stldt0(xB)))&((![W0]: (~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))&(![W0]: (aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB))))))&(![W0]: (~aElementOf0(W0,stldt0(xB))|(((((aInteger0(sK16_skl(W0))&~sK16_skl(W0)=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK16_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK16_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK17_skl(W2,W0))&sdtasdt0(sK16_skl(W0),sK17_skl(W2,W0))=sdtpldt0(W2,smndt0(W0))))&aDivisorOf0(sK16_skl(W0),sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,sK16_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK16_skl(W0),W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(sK16_skl(W0),sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,sK16_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK16_skl(W0)))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK16_skl(W0)))|aElementOf0(W2,stldt0(xB)))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK16_skl(W0)),stldt0(xB))))))&isOpen0(stldt0(xB)))&isClosed0(xB)),
% 1.57/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(W1,sK14_skl(W0)),skolemize(W3,sK15_skl(W2,W0)),skolemize(W1,sK16_skl(W0)),skolemize(W3,sK17_skl(W2,W0))],[f209])).
% 1.57/0.81 fof(f211,plain,(
% 1.57/0.81 aSet0(cS1395)),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f213,plain,(
% 1.57/0.81 ![X0]: (aElementOf0(X0,cS1395)|~aInteger0(X0))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f216,plain,(
% 1.57/0.81 aSubsetOf0(xA,cS1395)),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f222,plain,(
% 1.57/0.81 aSubsetOf0(xB,cS1395)),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f223,plain,(
% 1.57/0.81 aSet0(stldt0(xA))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f241,plain,(
% 1.57/0.81 isClosed0(xA)),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f242,plain,(
% 1.57/0.81 aSet0(stldt0(xB))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f243,plain,(
% 1.57/0.81 ![X0]: (~aElementOf0(X0,stldt0(xB))|aInteger0(X0))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f244,plain,(
% 1.57/0.81 ![X0]: (~aElementOf0(X0,stldt0(xB))|~aElementOf0(X0,xB))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f260,plain,(
% 1.57/0.81 isClosed0(xB)),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f210])).
% 1.57/0.81 fof(f261,plain,(
% 1.57/0.81 ((((aSet0(stldt0(xA))&(![W0]: (aElementOf0(W0,stldt0(xA))<=>(aInteger0(W0)&~aElementOf0(W0,xA)))))&((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&((?[W0]: (aElementOf0(W0,stldt0(xA))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xA),cS1395))))|((aSet0(stldt0(xB))&(![W0]: (aElementOf0(W0,stldt0(xB))<=>(aInteger0(W0)&~aElementOf0(W0,xB)))))&((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&((?[W0]: (aElementOf0(W0,stldt0(xB))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xB),cS1395)))))|((aSet0(sdtbsmnsldt0(xA,xB))&(![W0]: (aElementOf0(W0,sdtbsmnsldt0(xA,xB))<=>(aInteger0(W0)&(aElementOf0(W0,xA)|aElementOf0(W0,xB))))))&((aSet0(stldt0(sdtbsmnsldt0(xA,xB)))&(![W0]: (aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<=>(aInteger0(W0)&~aElementOf0(W0,sdtbsmnsldt0(xA,xB))))))&((![W0]: (aElementOf0(W0,stldt0(xA))<=>(aInteger0(W0)&~aElementOf0(W0,xA))))&((![W0]: (aElementOf0(W0,stldt0(xB))<=>(aInteger0(W0)&~aElementOf0(W0,xB))))&((?[W0]: (aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<~>((aInteger0(W0)&aElementOf0(W0,stldt0(xA)))&aElementOf0(W0,stldt0(xB)))))&~stldt0(sdtbsmnsldt0(xA,xB))=sdtslmnbsdt0(stldt0(xA),stldt0(xB))))))))),
% 1.57/0.81 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 1.57/0.81 fof(f262,definition,(
% 1.57/0.81 sP2_prd<=>(((aSet0(stldt0(xA))&(![W0]: (aElementOf0(W0,stldt0(xA))<=>(aInteger0(W0)&~aElementOf0(W0,xA)))))&((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&((?[W0]: (aElementOf0(W0,stldt0(xA))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xA),cS1395))))|((aSet0(stldt0(xB))&(![W0]: (aElementOf0(W0,stldt0(xB))<=>(aInteger0(W0)&~aElementOf0(W0,xB)))))&((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&((?[W0]: (aElementOf0(W0,stldt0(xB))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xB),cS1395)))))),
% 1.57/0.81 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 1.57/0.81 fof(f263,plain,(
% 1.57/0.81 sP2_prd|((aSet0(sdtbsmnsldt0(xA,xB))&(![W0]: (aElementOf0(W0,sdtbsmnsldt0(xA,xB))<=>(aInteger0(W0)&(aElementOf0(W0,xA)|aElementOf0(W0,xB))))))&((aSet0(stldt0(sdtbsmnsldt0(xA,xB)))&(![W0]: (aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<=>(aInteger0(W0)&~aElementOf0(W0,sdtbsmnsldt0(xA,xB))))))&((![W0]: (aElementOf0(W0,stldt0(xA))<=>(aInteger0(W0)&~aElementOf0(W0,xA))))&((![W0]: (aElementOf0(W0,stldt0(xB))<=>(aInteger0(W0)&~aElementOf0(W0,xB))))&((?[W0]: (aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))<~>((aInteger0(W0)&aElementOf0(W0,stldt0(xA)))&aElementOf0(W0,stldt0(xB)))))&~stldt0(sdtbsmnsldt0(xA,xB))=sdtslmnbsdt0(stldt0(xA),stldt0(xB)))))))),
% 1.57/0.81 inference(formula_renaming,[status(thm)],[f261,f262])).
% 1.57/0.81 fof(f264,plain,(
% 1.57/0.81 sP2_prd|((aSet0(sdtbsmnsldt0(xA,xB))&(![W0]: ((~aElementOf0(W0,sdtbsmnsldt0(xA,xB))|(aInteger0(W0)&(aElementOf0(W0,xA)|aElementOf0(W0,xB))))&(aElementOf0(W0,sdtbsmnsldt0(xA,xB))|(~aInteger0(W0)|(~aElementOf0(W0,xA)&~aElementOf0(W0,xB)))))))&((aSet0(stldt0(sdtbsmnsldt0(xA,xB)))&(![W0]: ((~aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|(aInteger0(W0)&~aElementOf0(W0,sdtbsmnsldt0(xA,xB))))&(aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|(~aInteger0(W0)|aElementOf0(W0,sdtbsmnsldt0(xA,xB)))))))&((![W0]: ((~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA)))&(aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA)))))&((![W0]: ((~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB)))&(aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB)))))&((?[W0]: ((aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|((aInteger0(W0)&aElementOf0(W0,stldt0(xA)))&aElementOf0(W0,stldt0(xB))))&(~aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|((~aInteger0(W0)|~aElementOf0(W0,stldt0(xA)))|~aElementOf0(W0,stldt0(xB))))))&~stldt0(sdtbsmnsldt0(xA,xB))=sdtslmnbsdt0(stldt0(xA),stldt0(xB)))))))),
% 1.57/0.81 inference(NNF_transformation,[status(thm)],[f263])).
% 1.57/0.81 fof(f265,plain,(
% 1.57/0.81 sP2_prd|((aSet0(sdtbsmnsldt0(xA,xB))&((![W0]: (~aElementOf0(W0,sdtbsmnsldt0(xA,xB))|(aInteger0(W0)&(aElementOf0(W0,xA)|aElementOf0(W0,xB)))))&(![W0]: (aElementOf0(W0,sdtbsmnsldt0(xA,xB))|(~aInteger0(W0)|(~aElementOf0(W0,xA)&~aElementOf0(W0,xB)))))))&((aSet0(stldt0(sdtbsmnsldt0(xA,xB)))&((![W0]: (~aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|(aInteger0(W0)&~aElementOf0(W0,sdtbsmnsldt0(xA,xB)))))&(![W0]: (aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|(~aInteger0(W0)|aElementOf0(W0,sdtbsmnsldt0(xA,xB)))))))&(((![W0]: (~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))&(![W0]: (aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA)))))&(((![W0]: (~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))&(![W0]: (aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB)))))&((?[W0]: ((aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|((aInteger0(W0)&aElementOf0(W0,stldt0(xA)))&aElementOf0(W0,stldt0(xB))))&(~aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|((~aInteger0(W0)|~aElementOf0(W0,stldt0(xA)))|~aElementOf0(W0,stldt0(xB))))))&~stldt0(sdtbsmnsldt0(xA,xB))=sdtslmnbsdt0(stldt0(xA),stldt0(xB)))))))),
% 1.57/0.81 inference(miniscoping,[status(thm)],[f264])).
% 1.57/0.81 fof(f266,plain,(
% 1.57/0.81 sP2_prd|((aSet0(sdtbsmnsldt0(xA,xB))&((![W0]: (~aElementOf0(W0,sdtbsmnsldt0(xA,xB))|(aInteger0(W0)&(aElementOf0(W0,xA)|aElementOf0(W0,xB)))))&(![W0]: (aElementOf0(W0,sdtbsmnsldt0(xA,xB))|(~aInteger0(W0)|(~aElementOf0(W0,xA)&~aElementOf0(W0,xB)))))))&((aSet0(stldt0(sdtbsmnsldt0(xA,xB)))&((![W0]: (~aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|(aInteger0(W0)&~aElementOf0(W0,sdtbsmnsldt0(xA,xB)))))&(![W0]: (aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))|(~aInteger0(W0)|aElementOf0(W0,sdtbsmnsldt0(xA,xB)))))))&(((![W0]: (~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))&(![W0]: (aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA)))))&(((![W0]: (~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))&(![W0]: (aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB)))))&(((aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|((aInteger0(sK18_skl)&aElementOf0(sK18_skl,stldt0(xA)))&aElementOf0(sK18_skl,stldt0(xB))))&(~aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|((~aInteger0(sK18_skl)|~aElementOf0(sK18_skl,stldt0(xA)))|~aElementOf0(sK18_skl,stldt0(xB)))))&~stldt0(sdtbsmnsldt0(xA,xB))=sdtslmnbsdt0(stldt0(xA),stldt0(xB)))))))),
% 1.57/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(W0,sK18_skl)],[f265])).
% 1.57/0.81 fof(f270,plain,(
% 1.57/0.81 ![X0]: (sP2_prd|aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~aInteger0(X0)|~aElementOf0(X0,xA))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.81 fof(f271,plain,(
% 1.57/0.81 ![X0]: (sP2_prd|aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~aInteger0(X0)|~aElementOf0(X0,xB))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.81 fof(f273,plain,(
% 1.57/0.81 ![X0]: (sP2_prd|~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|aInteger0(X0))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.81 fof(f274,plain,(
% 1.57/0.81 ![X0]: (sP2_prd|~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|~aElementOf0(X0,sdtbsmnsldt0(xA,xB)))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.81 fof(f275,plain,(
% 1.57/0.81 ![X0]: (sP2_prd|aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|~aInteger0(X0)|aElementOf0(X0,sdtbsmnsldt0(xA,xB)))),
% 1.57/0.81 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f277,plain,(
% 1.57/0.82 ![X0]: (sP2_prd|~aElementOf0(X0,stldt0(xA))|~aElementOf0(X0,xA))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f278,plain,(
% 1.57/0.82 ![X0]: (sP2_prd|aElementOf0(X0,stldt0(xA))|~aInteger0(X0)|aElementOf0(X0,xA))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f281,plain,(
% 1.57/0.82 ![X0]: (sP2_prd|aElementOf0(X0,stldt0(xB))|~aInteger0(X0)|aElementOf0(X0,xB))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f283,plain,(
% 1.57/0.82 sP2_prd|aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|aElementOf0(sK18_skl,stldt0(xA))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f284,plain,(
% 1.57/0.82 sP2_prd|aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|aElementOf0(sK18_skl,stldt0(xB))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f285,plain,(
% 1.57/0.82 sP2_prd|~aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|~aInteger0(sK18_skl)|~aElementOf0(sK18_skl,stldt0(xA))|~aElementOf0(sK18_skl,stldt0(xB))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f266])).
% 1.57/0.82 fof(f298,definition,(
% 1.57/0.82 sP3_prd<=>((aSet0(stldt0(xA))&(![W0]: (aElementOf0(W0,stldt0(xA))<=>(aInteger0(W0)&~aElementOf0(W0,xA)))))&((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&((?[W0]: (aElementOf0(W0,stldt0(xA))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xA),cS1395))))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 1.57/0.82 fof(f299,plain,(
% 1.57/0.82 sP2_prd<=>(sP3_prd|((aSet0(stldt0(xB))&(![W0]: (aElementOf0(W0,stldt0(xB))<=>(aInteger0(W0)&~aElementOf0(W0,xB)))))&((aSet0(cS1395)&(![W0]: (aElementOf0(W0,cS1395)<=>aInteger0(W0))))&((?[W0]: (aElementOf0(W0,stldt0(xB))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xB),cS1395)))))),
% 1.57/0.82 inference(formula_renaming,[status(thm)],[f262,f298])).
% 1.57/0.82 fof(f300,plain,(
% 1.57/0.82 (~sP2_prd|(sP3_prd|((aSet0(stldt0(xB))&(![W0]: ((~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB)))&(aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB))))))&((aSet0(cS1395)&(![W0]: ((~aElementOf0(W0,cS1395)|aInteger0(W0))&(aElementOf0(W0,cS1395)|~aInteger0(W0)))))&((?[W0]: (aElementOf0(W0,stldt0(xB))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xB),cS1395))))))&(sP2_prd|(~sP3_prd&((~aSet0(stldt0(xB))|(?[W0]: ((~aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB)))&(aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))))|((~aSet0(cS1395)|(?[W0]: ((~aElementOf0(W0,cS1395)|~aInteger0(W0))&(aElementOf0(W0,cS1395)|aInteger0(W0)))))|((![W0]: (~aElementOf0(W0,stldt0(xB))|aElementOf0(W0,cS1395)))|aSubsetOf0(stldt0(xB),cS1395))))))),
% 1.57/0.82 inference(NNF_transformation,[status(thm)],[f299])).
% 1.57/0.82 fof(f301,plain,(
% 1.57/0.82 (~sP2_prd|(sP3_prd|((aSet0(stldt0(xB))&((![W0]: (~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))&(![W0]: (aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB))))))&((aSet0(cS1395)&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&((?[W0]: (aElementOf0(W0,stldt0(xB))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xB),cS1395))))))&(sP2_prd|(~sP3_prd&((~aSet0(stldt0(xB))|(?[W0]: ((~aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB)))&(aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))))|((~aSet0(cS1395)|(?[W0]: ((~aElementOf0(W0,cS1395)|~aInteger0(W0))&(aElementOf0(W0,cS1395)|aInteger0(W0)))))|((![W0]: (~aElementOf0(W0,stldt0(xB))|aElementOf0(W0,cS1395)))|aSubsetOf0(stldt0(xB),cS1395))))))),
% 1.57/0.82 inference(miniscoping,[status(thm)],[f300])).
% 1.57/0.82 fof(f302,plain,(
% 1.57/0.82 (~sP2_prd|(sP3_prd|((aSet0(stldt0(xB))&((![W0]: (~aElementOf0(W0,stldt0(xB))|(aInteger0(W0)&~aElementOf0(W0,xB))))&(![W0]: (aElementOf0(W0,stldt0(xB))|(~aInteger0(W0)|aElementOf0(W0,xB))))))&((aSet0(cS1395)&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&((aElementOf0(sK19_skl,stldt0(xB))&~aElementOf0(sK19_skl,cS1395))&~aSubsetOf0(stldt0(xB),cS1395))))))&(sP2_prd|(~sP3_prd&((~aSet0(stldt0(xB))|((~aElementOf0(sK20_skl,stldt0(xB))|(~aInteger0(sK20_skl)|aElementOf0(sK20_skl,xB)))&(aElementOf0(sK20_skl,stldt0(xB))|(aInteger0(sK20_skl)&~aElementOf0(sK20_skl,xB)))))|((~aSet0(cS1395)|((~aElementOf0(sK21_skl,cS1395)|~aInteger0(sK21_skl))&(aElementOf0(sK21_skl,cS1395)|aInteger0(sK21_skl))))|((![W0]: (~aElementOf0(W0,stldt0(xB))|aElementOf0(W0,cS1395)))|aSubsetOf0(stldt0(xB),cS1395))))))),
% 1.57/0.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(W0,sK19_skl),skolemize(W0,sK20_skl),skolemize(W0,sK21_skl)],[f301])).
% 1.57/0.82 fof(f306,plain,(
% 1.57/0.82 ![X0]: (~sP2_prd|sP3_prd|aElementOf0(X0,stldt0(xB))|~aInteger0(X0)|aElementOf0(X0,xB))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f302])).
% 1.57/0.82 fof(f310,plain,(
% 1.57/0.82 ~sP2_prd|sP3_prd|aElementOf0(sK19_skl,stldt0(xB))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f302])).
% 1.57/0.82 fof(f311,plain,(
% 1.57/0.82 ~sP2_prd|sP3_prd|~aElementOf0(sK19_skl,cS1395)),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f302])).
% 1.57/0.82 fof(f320,plain,(
% 1.57/0.82 (~sP3_prd|((aSet0(stldt0(xA))&(![W0]: ((~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA)))&(aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA))))))&((aSet0(cS1395)&(![W0]: ((~aElementOf0(W0,cS1395)|aInteger0(W0))&(aElementOf0(W0,cS1395)|~aInteger0(W0)))))&((?[W0]: (aElementOf0(W0,stldt0(xA))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xA),cS1395)))))&(sP3_prd|((~aSet0(stldt0(xA))|(?[W0]: ((~aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA)))&(aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))))|((~aSet0(cS1395)|(?[W0]: ((~aElementOf0(W0,cS1395)|~aInteger0(W0))&(aElementOf0(W0,cS1395)|aInteger0(W0)))))|((![W0]: (~aElementOf0(W0,stldt0(xA))|aElementOf0(W0,cS1395)))|aSubsetOf0(stldt0(xA),cS1395)))))),
% 1.57/0.82 inference(NNF_transformation,[status(thm)],[f298])).
% 1.57/0.82 fof(f321,plain,(
% 1.57/0.82 (~sP3_prd|((aSet0(stldt0(xA))&((![W0]: (~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))&(![W0]: (aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA))))))&((aSet0(cS1395)&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&((?[W0]: (aElementOf0(W0,stldt0(xA))&~aElementOf0(W0,cS1395)))&~aSubsetOf0(stldt0(xA),cS1395)))))&(sP3_prd|((~aSet0(stldt0(xA))|(?[W0]: ((~aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA)))&(aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))))|((~aSet0(cS1395)|(?[W0]: ((~aElementOf0(W0,cS1395)|~aInteger0(W0))&(aElementOf0(W0,cS1395)|aInteger0(W0)))))|((![W0]: (~aElementOf0(W0,stldt0(xA))|aElementOf0(W0,cS1395)))|aSubsetOf0(stldt0(xA),cS1395)))))),
% 1.57/0.82 inference(miniscoping,[status(thm)],[f320])).
% 1.57/0.82 fof(f322,plain,(
% 1.57/0.82 (~sP3_prd|((aSet0(stldt0(xA))&((![W0]: (~aElementOf0(W0,stldt0(xA))|(aInteger0(W0)&~aElementOf0(W0,xA))))&(![W0]: (aElementOf0(W0,stldt0(xA))|(~aInteger0(W0)|aElementOf0(W0,xA))))))&((aSet0(cS1395)&((![W0]: (~aElementOf0(W0,cS1395)|aInteger0(W0)))&(![W0]: (aElementOf0(W0,cS1395)|~aInteger0(W0)))))&((aElementOf0(sK22_skl,stldt0(xA))&~aElementOf0(sK22_skl,cS1395))&~aSubsetOf0(stldt0(xA),cS1395)))))&(sP3_prd|((~aSet0(stldt0(xA))|((~aElementOf0(sK23_skl,stldt0(xA))|(~aInteger0(sK23_skl)|aElementOf0(sK23_skl,xA)))&(aElementOf0(sK23_skl,stldt0(xA))|(aInteger0(sK23_skl)&~aElementOf0(sK23_skl,xA)))))|((~aSet0(cS1395)|((~aElementOf0(sK24_skl,cS1395)|~aInteger0(sK24_skl))&(aElementOf0(sK24_skl,cS1395)|aInteger0(sK24_skl))))|((![W0]: (~aElementOf0(W0,stldt0(xA))|aElementOf0(W0,cS1395)))|aSubsetOf0(stldt0(xA),cS1395)))))),
% 1.57/0.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl,sK23_skl,sK24_skl]),skolemize(W0,sK22_skl),skolemize(W0,sK23_skl),skolemize(W0,sK24_skl)],[f321])).
% 1.57/0.82 fof(f324,plain,(
% 1.57/0.82 ![X0]: (~sP3_prd|~aElementOf0(X0,stldt0(xA))|aInteger0(X0))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f322])).
% 1.57/0.82 fof(f326,plain,(
% 1.57/0.82 ![X0]: (~sP3_prd|aElementOf0(X0,stldt0(xA))|~aInteger0(X0)|aElementOf0(X0,xA))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f322])).
% 1.57/0.82 fof(f330,plain,(
% 1.57/0.82 ~sP3_prd|aElementOf0(sK22_skl,stldt0(xA))),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f322])).
% 1.57/0.82 fof(f331,plain,(
% 1.57/0.82 ~sP3_prd|~aElementOf0(sK22_skl,cS1395)),
% 1.57/0.82 inference(cnf_transformation,[status(thm)],[f322])).
% 1.57/0.82 fof(f339,definition,(
% 1.57/0.82 sQ0_spl <=> (sP2_prd)),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f354,definition,(
% 1.57/0.82 ![X0]: (sQ4_spl <=> (aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~aInteger0(X0)|~aElementOf0(X0,xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f355,plain,(
% 1.57/0.82 ![X0]: (aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~aInteger0(X0)|~aElementOf0(X0,xA)|~sQ4_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f354])).
% 1.57/0.82 fof(f357,plain,(
% 1.57/0.82 sQ0_spl|sQ4_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f270,f339,f354])).
% 1.57/0.82 fof(f358,definition,(
% 1.57/0.82 ![X0]: (sQ5_spl <=> (aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~aInteger0(X0)|~aElementOf0(X0,xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f359,plain,(
% 1.57/0.82 ![X0]: (aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~aInteger0(X0)|~aElementOf0(X0,xB)|~sQ5_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f358])).
% 1.57/0.82 fof(f361,plain,(
% 1.57/0.82 sQ0_spl|sQ5_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f271,f339,f358])).
% 1.57/0.82 fof(f366,definition,(
% 1.57/0.82 ![X0]: (sQ7_spl <=> (~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|aInteger0(X0)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f367,plain,(
% 1.57/0.82 ![X0]: (~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|aInteger0(X0)|~sQ7_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f366])).
% 1.57/0.82 fof(f369,plain,(
% 1.57/0.82 sQ0_spl|sQ7_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f273,f339,f366])).
% 1.57/0.82 fof(f370,definition,(
% 1.57/0.82 ![X0]: (sQ8_spl <=> (~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|~aElementOf0(X0,sdtbsmnsldt0(xA,xB))))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f371,plain,(
% 1.57/0.82 ![X0]: (~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|~aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~sQ8_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f370])).
% 1.57/0.82 fof(f373,plain,(
% 1.57/0.82 sQ0_spl|sQ8_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f274,f339,f370])).
% 1.57/0.82 fof(f374,definition,(
% 1.57/0.82 ![X0]: (sQ9_spl <=> (aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|~aInteger0(X0)|aElementOf0(X0,sdtbsmnsldt0(xA,xB))))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f375,plain,(
% 1.57/0.82 ![X0]: (aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))|~aInteger0(X0)|aElementOf0(X0,sdtbsmnsldt0(xA,xB))|~sQ9_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f374])).
% 1.57/0.82 fof(f377,plain,(
% 1.57/0.82 sQ0_spl|sQ9_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f275,f339,f374])).
% 1.57/0.82 fof(f378,definition,(
% 1.57/0.82 ![X0]: (sQ10_spl <=> (~aElementOf0(X0,stldt0(xA))|aInteger0(X0)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f379,plain,(
% 1.57/0.82 ![X0]: (~aElementOf0(X0,stldt0(xA))|aInteger0(X0)|~sQ10_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f378])).
% 1.57/0.82 fof(f382,definition,(
% 1.57/0.82 ![X0]: (sQ11_spl <=> (~aElementOf0(X0,stldt0(xA))|~aElementOf0(X0,xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f383,plain,(
% 1.57/0.82 ![X0]: (~aElementOf0(X0,stldt0(xA))|~aElementOf0(X0,xA)|~sQ11_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f382])).
% 1.57/0.82 fof(f385,plain,(
% 1.57/0.82 sQ0_spl|sQ11_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f277,f339,f382])).
% 1.57/0.82 fof(f386,definition,(
% 1.57/0.82 ![X0]: (sQ12_spl <=> (aElementOf0(X0,stldt0(xA))|~aInteger0(X0)|aElementOf0(X0,xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f387,plain,(
% 1.57/0.82 ![X0]: (aElementOf0(X0,stldt0(xA))|~aInteger0(X0)|aElementOf0(X0,xA)|~sQ12_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f386])).
% 1.57/0.82 fof(f389,plain,(
% 1.57/0.82 sQ0_spl|sQ12_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f278,f339,f386])).
% 1.57/0.82 fof(f398,definition,(
% 1.57/0.82 ![X0]: (sQ15_spl <=> (aElementOf0(X0,stldt0(xB))|~aInteger0(X0)|aElementOf0(X0,xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f399,plain,(
% 1.57/0.82 ![X0]: (aElementOf0(X0,stldt0(xB))|~aInteger0(X0)|aElementOf0(X0,xB)|~sQ15_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f398])).
% 1.57/0.82 fof(f401,plain,(
% 1.57/0.82 sQ0_spl|sQ15_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f281,f339,f398])).
% 1.57/0.82 fof(f402,definition,(
% 1.57/0.82 sQ16_spl <=> (aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB))))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f403,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|~sQ16_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f402])).
% 1.57/0.82 fof(f404,plain,(
% 1.57/0.82 ~aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))|sQ16_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f402])).
% 1.57/0.82 fof(f405,definition,(
% 1.57/0.82 sQ17_spl <=> (aInteger0(sK18_skl))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f406,plain,(
% 1.57/0.82 aInteger0(sK18_skl)|~sQ17_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f405])).
% 1.57/0.82 fof(f407,plain,(
% 1.57/0.82 ~aInteger0(sK18_skl)|sQ17_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f405])).
% 1.57/0.82 fof(f409,definition,(
% 1.57/0.82 sQ18_spl <=> (aElementOf0(sK18_skl,stldt0(xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f410,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,stldt0(xA))|~sQ18_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f409])).
% 1.57/0.82 fof(f411,plain,(
% 1.57/0.82 ~aElementOf0(sK18_skl,stldt0(xA))|sQ18_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f409])).
% 1.57/0.82 fof(f412,plain,(
% 1.57/0.82 sQ0_spl|sQ16_spl|sQ18_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f283,f339,f402,f409])).
% 1.57/0.82 fof(f413,definition,(
% 1.57/0.82 sQ19_spl <=> (aElementOf0(sK18_skl,stldt0(xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f414,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,stldt0(xB))|~sQ19_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f413])).
% 1.57/0.82 fof(f415,plain,(
% 1.57/0.82 ~aElementOf0(sK18_skl,stldt0(xB))|sQ19_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f413])).
% 1.57/0.82 fof(f416,plain,(
% 1.57/0.82 sQ0_spl|sQ16_spl|sQ19_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f284,f339,f402,f413])).
% 1.57/0.82 fof(f417,plain,(
% 1.57/0.82 sQ0_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f285,f339,f402,f405,f409,f413])).
% 1.57/0.82 fof(f422,definition,(
% 1.57/0.82 sQ21_spl <=> (sP3_prd)),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f425,definition,(
% 1.57/0.82 sQ22_spl <=> (aSet0(stldt0(xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f427,plain,(
% 1.57/0.82 ~aSet0(stldt0(xB))|sQ22_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f425])).
% 1.57/0.82 fof(f431,plain,(
% 1.57/0.82 ~sQ0_spl|sQ21_spl|sQ15_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f306,f339,f422,f398])).
% 1.57/0.82 fof(f432,definition,(
% 1.57/0.82 sQ23_spl <=> (aSet0(cS1395))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f434,plain,(
% 1.57/0.82 ~aSet0(cS1395)|sQ23_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f432])).
% 1.57/0.82 fof(f444,definition,(
% 1.57/0.82 sQ26_spl <=> (aElementOf0(sK19_skl,stldt0(xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f445,plain,(
% 1.57/0.82 aElementOf0(sK19_skl,stldt0(xB))|~sQ26_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f444])).
% 1.57/0.82 fof(f447,plain,(
% 1.57/0.82 ~sQ0_spl|sQ21_spl|sQ26_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f310,f339,f422,f444])).
% 1.57/0.82 fof(f448,definition,(
% 1.57/0.82 sQ27_spl <=> (aElementOf0(sK19_skl,cS1395))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f450,plain,(
% 1.57/0.82 ~aElementOf0(sK19_skl,cS1395)|sQ27_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f448])).
% 1.57/0.82 fof(f451,plain,(
% 1.57/0.82 ~sQ0_spl|sQ21_spl|~sQ27_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f311,f339,f422,f448])).
% 1.57/0.82 fof(f481,definition,(
% 1.57/0.82 sQ35_spl <=> (aSet0(stldt0(xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f483,plain,(
% 1.57/0.82 ~aSet0(stldt0(xA))|sQ35_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f481])).
% 1.57/0.82 fof(f485,plain,(
% 1.57/0.82 ~sQ21_spl|sQ10_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f324,f422,f378])).
% 1.57/0.82 fof(f487,plain,(
% 1.57/0.82 ~sQ21_spl|sQ12_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f326,f422,f386])).
% 1.57/0.82 fof(f491,definition,(
% 1.57/0.82 sQ36_spl <=> (aElementOf0(sK22_skl,stldt0(xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f492,plain,(
% 1.57/0.82 aElementOf0(sK22_skl,stldt0(xA))|~sQ36_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f491])).
% 1.57/0.82 fof(f494,plain,(
% 1.57/0.82 ~sQ21_spl|sQ36_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f330,f422,f491])).
% 1.57/0.82 fof(f495,definition,(
% 1.57/0.82 sQ37_spl <=> (aElementOf0(sK22_skl,cS1395))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f497,plain,(
% 1.57/0.82 ~aElementOf0(sK22_skl,cS1395)|sQ37_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f495])).
% 1.57/0.82 fof(f498,plain,(
% 1.57/0.82 ~sQ21_spl|~sQ37_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f331,f422,f495])).
% 1.57/0.82 fof(f532,plain,(
% 1.57/0.82 ![X0,X1,X2]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|~aElementOf0(X2,sdtbsmnsldt0(X0,X1))|aInteger0(X2))),
% 1.57/0.82 inference(destructive_equality_resolution,[status(thm)],[f133])).
% 1.57/0.82 fof(f533,plain,(
% 1.57/0.82 ![X0,X1,X2]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|~aElementOf0(X2,sdtbsmnsldt0(X0,X1))|aElementOf0(X2,X0)|aElementOf0(X2,X1))),
% 1.57/0.82 inference(destructive_equality_resolution,[status(thm)],[f134])).
% 1.57/0.82 fof(f535,plain,(
% 1.57/0.82 ![X0,X1,X2]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|aElementOf0(X2,sdtbsmnsldt0(X0,X1))|~aInteger0(X2)|~aElementOf0(X2,X1))),
% 1.57/0.82 inference(destructive_equality_resolution,[status(thm)],[f136])).
% 1.57/0.82 fof(f552,plain,(
% 1.57/0.82 $false|sQ35_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f483,f223])).
% 1.57/0.82 fof(f553,plain,(
% 1.57/0.82 sQ35_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f552])).
% 1.57/0.82 fof(f560,plain,(
% 1.57/0.82 aInteger0(sK22_skl)|~sQ10_spl|~sQ36_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f379,f492])).
% 1.57/0.82 fof(f561,plain,(
% 1.57/0.82 aElementOf0(sK22_skl,cS1395)|~sQ10_spl|~sQ36_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f560,f213])).
% 1.57/0.82 fof(f562,plain,(
% 1.57/0.82 $false|sQ37_spl|~sQ10_spl|~sQ36_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f561,f497])).
% 1.57/0.82 fof(f563,plain,(
% 1.57/0.82 sQ37_spl|~sQ10_spl|~sQ36_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f562])).
% 1.57/0.82 fof(f576,plain,(
% 1.57/0.82 aInteger0(sK19_skl)|~sQ26_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f243,f445])).
% 1.57/0.82 fof(f578,plain,(
% 1.57/0.82 aElementOf0(sK19_skl,cS1395)|~sQ26_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f576,f213])).
% 1.57/0.82 fof(f579,plain,(
% 1.57/0.82 $false|sQ27_spl|~sQ26_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f578,f450])).
% 1.57/0.82 fof(f580,plain,(
% 1.57/0.82 sQ27_spl|~sQ26_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f579])).
% 1.57/0.82 fof(f581,plain,(
% 1.57/0.82 $false|sQ23_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f434,f211])).
% 1.57/0.82 fof(f582,plain,(
% 1.57/0.82 sQ23_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f581])).
% 1.57/0.82 fof(f583,plain,(
% 1.57/0.82 $false|sQ22_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f427,f242])).
% 1.57/0.82 fof(f584,plain,(
% 1.57/0.82 sQ22_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f583])).
% 1.57/0.82 fof(f660,plain,(
% 1.57/0.82 aInteger0(sK18_skl)|~sQ19_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f414,f243])).
% 1.57/0.82 fof(f662,plain,(
% 1.57/0.82 $false|sQ17_spl|~sQ19_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f660,f407])).
% 1.57/0.82 fof(f663,plain,(
% 1.57/0.82 sQ17_spl|~sQ19_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f662])).
% 1.57/0.82 fof(f700,plain,(
% 1.57/0.82 sdtpldt0(sK18_skl,smndt0(sK18_skl))=sz00|~sQ17_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f61,f406])).
% 1.57/0.82 fof(f719,definition,(
% 1.57/0.82 sQ46_spl <=> (aInteger0(sz00))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f734,plain,(
% 1.57/0.82 ~aInteger0(sK18_skl)|aElementOf0(sK18_skl,xB)|~sQ15_spl|sQ19_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f399,f415])).
% 1.57/0.82 fof(f739,definition,(
% 1.57/0.82 sQ48_spl <=> (aElementOf0(sK18_skl,xB))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f740,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,xB)|~sQ48_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f739])).
% 1.57/0.82 fof(f742,plain,(
% 1.57/0.82 ~sQ17_spl|sQ48_spl|~sQ15_spl|sQ19_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f734,f405,f739,f398,f413])).
% 1.57/0.82 fof(f743,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xB))|~aInteger0(sK18_skl)|~sQ48_spl|~sQ5_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f740,f359])).
% 1.57/0.82 fof(f746,definition,(
% 1.57/0.82 sQ49_spl <=> (aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f747,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xB))|~sQ49_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f746])).
% 1.57/0.82 fof(f749,plain,(
% 1.57/0.82 sQ49_spl|~sQ17_spl|~sQ48_spl|~sQ5_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f743,f746,f405,f739,f358])).
% 1.57/0.82 fof(f750,plain,(
% 1.57/0.82 ~aInteger0(sK18_skl)|aElementOf0(sK18_skl,xA)|sQ18_spl|~sQ12_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f411,f387])).
% 1.57/0.82 fof(f751,definition,(
% 1.57/0.82 sQ50_spl <=> (aElementOf0(sK18_skl,xA))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f752,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,xA)|~sQ50_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f751])).
% 1.57/0.82 fof(f754,plain,(
% 1.57/0.82 ~sQ17_spl|sQ50_spl|sQ18_spl|~sQ12_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f750,f405,f751,f409,f386])).
% 1.57/0.82 fof(f755,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xB))|~aInteger0(sK18_skl)|~sQ50_spl|~sQ4_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f752,f355])).
% 1.57/0.82 fof(f757,plain,(
% 1.57/0.82 ![X0]: (~aSet0(X0)|~aSubsetOf0(xA,X0)|aElementOf0(sK18_skl,X0)|~sQ50_spl)),
% 1.57/0.82 inference(resolution,[status(thm)],[f752,f123])).
% 1.57/0.82 fof(f758,plain,(
% 1.57/0.82 sQ49_spl|~sQ17_spl|~sQ50_spl|~sQ4_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f755,f746,f405,f751,f354])).
% 1.57/0.82 fof(f760,plain,(
% 1.57/0.82 ~aElementOf0(sK18_skl,xA)|~sQ18_spl|~sQ11_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f410,f383])).
% 1.57/0.82 fof(f764,plain,(
% 1.57/0.82 ~aElementOf0(sK18_skl,xB)|~sQ19_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f414,f244])).
% 1.57/0.82 fof(f767,plain,(
% 1.57/0.82 $false|~sQ48_spl|~sQ19_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f764,f740])).
% 1.57/0.82 fof(f768,plain,(
% 1.57/0.82 ~sQ48_spl|~sQ19_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f767])).
% 1.57/0.82 fof(f770,plain,(
% 1.57/0.82 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|aElementOf0(X1,sdtbsmnsldt0(X0,xA))|~aInteger0(X1)|~aElementOf0(X1,xA))),
% 1.57/0.82 inference(resolution,[status(thm)],[f216,f535])).
% 1.57/0.82 fof(f774,plain,(
% 1.57/0.82 ~isClosed0(xA)|isOpen0(stldt0(xA))),
% 1.57/0.82 inference(resolution,[status(thm)],[f216,f199])).
% 1.57/0.82 fof(f776,plain,(
% 1.57/0.82 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|~aElementOf0(X1,sdtbsmnsldt0(X0,xA))|aElementOf0(X1,X0)|aElementOf0(X1,xA))),
% 1.57/0.82 inference(resolution,[status(thm)],[f216,f533])).
% 1.57/0.82 fof(f777,plain,(
% 1.57/0.82 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|~aElementOf0(X1,sdtbsmnsldt0(X0,xA))|aInteger0(X1))),
% 1.57/0.82 inference(resolution,[status(thm)],[f216,f532])).
% 1.57/0.82 fof(f779,plain,(
% 1.57/0.82 ~aSet0(cS1395)|aSet0(xA)),
% 1.57/0.82 inference(resolution,[status(thm)],[f216,f122])).
% 1.57/0.82 fof(f780,definition,(
% 1.57/0.82 sQ51_spl <=> (isClosed0(xA))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f782,plain,(
% 1.57/0.82 ~isClosed0(xA)|sQ51_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f780])).
% 1.57/0.82 fof(f783,definition,(
% 1.57/0.82 sQ52_spl <=> (isOpen0(stldt0(xA)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f786,plain,(
% 1.57/0.82 ~sQ51_spl|sQ52_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f774,f780,f783])).
% 1.57/0.82 fof(f787,definition,(
% 1.57/0.82 sQ53_spl <=> (aSet0(xA))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f790,plain,(
% 1.57/0.82 ~sQ23_spl|sQ53_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f779,f432,f787])).
% 1.57/0.82 fof(f791,plain,(
% 1.57/0.82 $false|sQ51_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f782,f241])).
% 1.57/0.82 fof(f792,plain,(
% 1.57/0.82 sQ51_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f791])).
% 1.57/0.82 fof(f798,plain,(
% 1.57/0.82 ~isClosed0(xB)|isOpen0(stldt0(xB))),
% 1.57/0.82 inference(resolution,[status(thm)],[f222,f199])).
% 1.57/0.82 fof(f800,plain,(
% 1.57/0.82 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|~aElementOf0(X1,sdtbsmnsldt0(X0,xB))|aElementOf0(X1,X0)|aElementOf0(X1,xB))),
% 1.57/0.82 inference(resolution,[status(thm)],[f222,f533])).
% 1.57/0.82 fof(f801,plain,(
% 1.57/0.82 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|~aElementOf0(X1,sdtbsmnsldt0(X0,xB))|aInteger0(X1))),
% 1.57/0.82 inference(resolution,[status(thm)],[f222,f532])).
% 1.57/0.82 fof(f803,plain,(
% 1.57/0.82 ~aSet0(cS1395)|aSet0(xB)),
% 1.57/0.82 inference(resolution,[status(thm)],[f222,f122])).
% 1.57/0.82 fof(f804,definition,(
% 1.57/0.82 sQ54_spl <=> (isClosed0(xB))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f806,plain,(
% 1.57/0.82 ~isClosed0(xB)|sQ54_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f804])).
% 1.57/0.82 fof(f807,definition,(
% 1.57/0.82 sQ55_spl <=> (isOpen0(stldt0(xB)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f810,plain,(
% 1.57/0.82 ~sQ54_spl|sQ55_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f798,f804,f807])).
% 1.57/0.82 fof(f811,definition,(
% 1.57/0.82 sQ56_spl <=> (aSet0(xB))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f814,plain,(
% 1.57/0.82 ~sQ23_spl|sQ56_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f803,f432,f811])).
% 1.57/0.82 fof(f815,plain,(
% 1.57/0.82 $false|sQ54_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f806,f260])).
% 1.57/0.82 fof(f816,plain,(
% 1.57/0.82 sQ54_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f815])).
% 1.57/0.82 fof(f881,plain,(
% 1.57/0.82 ~aInteger0(sK18_skl)|~aInteger0(smndt0(sK18_skl))|aInteger0(sz00)|~sQ17_spl),
% 1.57/0.82 inference(paramodulation,[status(thm)],[f700,f50])).
% 1.57/0.82 fof(f882,definition,(
% 1.57/0.82 sQ59_spl <=> (aInteger0(smndt0(sK18_skl)))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f885,plain,(
% 1.57/0.82 ~sQ17_spl|~sQ59_spl|sQ46_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f881,f405,f882,f719])).
% 1.57/0.82 fof(f899,plain,(
% 1.57/0.82 ~aSubsetOf0(xA,cS1395)|aElementOf0(sK18_skl,xA)|aElementOf0(sK18_skl,xB)|~sQ49_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f747,f800])).
% 1.57/0.82 fof(f900,plain,(
% 1.57/0.82 ~aSubsetOf0(xA,cS1395)|aInteger0(sK18_skl)|~sQ49_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f747,f801])).
% 1.57/0.82 fof(f903,definition,(
% 1.57/0.82 sQ61_spl <=> (aSubsetOf0(xA,cS1395))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f905,plain,(
% 1.57/0.82 ~aSubsetOf0(xA,cS1395)|sQ61_spl),
% 1.57/0.82 inference(component_clause,[status(thm)],[f903])).
% 1.57/0.82 fof(f906,plain,(
% 1.57/0.82 ~sQ61_spl|sQ50_spl|sQ48_spl|~sQ49_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f899,f903,f751,f739,f746])).
% 1.57/0.82 fof(f907,plain,(
% 1.57/0.82 ~sQ61_spl|sQ17_spl|~sQ49_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f900,f903,f405,f746])).
% 1.57/0.82 fof(f908,plain,(
% 1.57/0.82 ![X0]: (~aSubsetOf0(X0,cS1395)|aElementOf0(sK18_skl,sdtbsmnsldt0(X0,xA))|~aInteger0(sK18_skl)|~sQ50_spl)),
% 1.57/0.82 inference(resolution,[status(thm)],[f752,f770])).
% 1.57/0.82 fof(f912,definition,(
% 1.57/0.82 ![X0]: (sQ62_spl <=> (~aSubsetOf0(X0,cS1395)|aElementOf0(sK18_skl,sdtbsmnsldt0(X0,xA))))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f913,plain,(
% 1.57/0.82 ![X0]: (~aSubsetOf0(X0,cS1395)|aElementOf0(sK18_skl,sdtbsmnsldt0(X0,xA))|~sQ62_spl)),
% 1.57/0.82 inference(component_clause,[status(thm)],[f912])).
% 1.57/0.82 fof(f915,plain,(
% 1.57/0.82 sQ62_spl|~sQ17_spl|~sQ50_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f908,f912,f405,f751])).
% 1.57/0.82 fof(f919,plain,(
% 1.57/0.82 ~aSet0(cS1395)|aElementOf0(sK18_skl,cS1395)|~sQ50_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f757,f216])).
% 1.57/0.82 fof(f920,definition,(
% 1.57/0.82 sQ63_spl <=> (aElementOf0(sK18_skl,cS1395))),
% 1.57/0.82 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 1.57/0.82 fof(f923,plain,(
% 1.57/0.82 ~sQ23_spl|sQ63_spl|~sQ50_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f919,f432,f920,f751])).
% 1.57/0.82 fof(f924,plain,(
% 1.57/0.82 $false|~sQ50_spl|~sQ18_spl|~sQ11_spl),
% 1.57/0.82 inference(forward_subsumption_resolution,[status(thm)],[f760,f752])).
% 1.57/0.82 fof(f925,plain,(
% 1.57/0.82 ~sQ50_spl|~sQ18_spl|~sQ11_spl),
% 1.57/0.82 inference(contradiction_clause,[status(thm)],[f924])).
% 1.57/0.82 fof(f931,plain,(
% 1.57/0.82 aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xA))|~sQ62_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f913,f216])).
% 1.57/0.82 fof(f1053,plain,(
% 1.57/0.82 ~aSubsetOf0(xA,cS1395)|aElementOf0(sK18_skl,xA)|aElementOf0(sK18_skl,xA)|~sQ62_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f931,f776])).
% 1.57/0.82 fof(f1054,plain,(
% 1.57/0.82 ~aSubsetOf0(xA,cS1395)|aInteger0(sK18_skl)|~sQ62_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f931,f777])).
% 1.57/0.82 fof(f1056,plain,(
% 1.57/0.82 ~sQ61_spl|sQ50_spl|~sQ62_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f1053,f903,f751,f912])).
% 1.57/0.82 fof(f1057,plain,(
% 1.57/0.82 ~sQ61_spl|sQ17_spl|~sQ62_spl),
% 1.57/0.82 inference(split_clause,[status(thm)],[f1054,f903,f405,f912])).
% 1.57/0.82 fof(f1061,plain,(
% 1.57/0.82 ~aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xB))|~sQ16_spl|~sQ8_spl),
% 1.57/0.82 inference(resolution,[status(thm)],[f403,f371])).
% 1.57/0.83 fof(f1062,plain,(
% 1.57/0.83 aInteger0(sK18_skl)|~sQ16_spl|~sQ7_spl),
% 1.57/0.83 inference(resolution,[status(thm)],[f403,f367])).
% 1.57/0.83 fof(f1064,plain,(
% 1.57/0.83 $false|~sQ49_spl|~sQ16_spl|~sQ8_spl),
% 1.57/0.83 inference(forward_subsumption_resolution,[status(thm)],[f1061,f747])).
% 1.57/0.83 fof(f1065,plain,(
% 1.57/0.83 ~sQ49_spl|~sQ16_spl|~sQ8_spl),
% 1.57/0.83 inference(contradiction_clause,[status(thm)],[f1064])).
% 1.57/0.83 fof(f1070,plain,(
% 1.57/0.83 ~aInteger0(sK18_skl)|aElementOf0(sK18_skl,sdtbsmnsldt0(xA,xB))|sQ16_spl|~sQ9_spl),
% 1.57/0.83 inference(resolution,[status(thm)],[f404,f375])).
% 1.57/0.83 fof(f1071,plain,(
% 1.57/0.83 ~sQ17_spl|sQ49_spl|sQ16_spl|~sQ9_spl),
% 1.57/0.83 inference(split_clause,[status(thm)],[f1070,f405,f746,f402,f374])).
% 1.57/0.83 fof(f1072,plain,(
% 1.57/0.83 $false|sQ61_spl),
% 1.57/0.83 inference(forward_subsumption_resolution,[status(thm)],[f905,f216])).
% 1.57/0.83 fof(f1073,plain,(
% 1.57/0.83 sQ61_spl),
% 1.57/0.83 inference(contradiction_clause,[status(thm)],[f1072])).
% 1.57/0.83 fof(f1074,plain,(
% 1.57/0.83 sQ17_spl|~sQ16_spl|~sQ7_spl),
% 1.57/0.83 inference(split_clause,[status(thm)],[f1062,f405,f402,f366])).
% 1.57/0.83 fof(f1075,plain,(
% 1.57/0.83 $false),
% 1.57/0.83 inference(sat_refutation,[status(thm)],[f357,f361,f369,f373,f377,f385,f389,f401,f412,f416,f417,f431,f447,f451,f485,f487,f494,f498,f553,f563,f580,f582,f584,f663,f742,f749,f754,f758,f768,f786,f790,f792,f810,f814,f816,f885,f906,f907,f915,f923,f925,f1056,f1057,f1065,f1071,f1073,f1074])).
% 1.57/0.83 % SZS output end CNFRefutation for theBenchmark.p
% 1.57/0.85 % Elapsed time: 0.472728 seconds
% 1.57/0.85 % CPU time: 3.388088 seconds
% 1.57/0.85 % Total memory used: 118.536 MB
% 1.57/0.85 % Net memory used: 115.103 MB
%------------------------------------------------------------------------------