%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM441+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 6.93s 1.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM441+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n011.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 21 02:29:25 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.18/0.43 % Drodi V4.1.1
% 6.93/1.52 % Refutation found
% 6.93/1.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.93/1.52 % SZS output start CNFRefutation for theBenchmark
% 6.93/1.52 fof(f36,definition,(
% 6.93/1.52 (! [W0] :( aSubsetOf0(W0,cS1395)=> ( isClosed0(W0)<=> isOpen0(stldt0(W0)) ) ) )),
% 6.93/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.93/1.52 fof(f38,axiom,(
% 6.93/1.52 (! [W0,W1] :( ( aSubsetOf0(W0,cS1395)& aSubsetOf0(W1,cS1395)& isOpen0(W0)& isOpen0(W1) )=> isOpen0(sdtslmnbsdt0(W0,W1)) ) )),
% 6.93/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.93/1.52 fof(f39,hypothesis,(
% 6.93/1.52 ( 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) ) ),
% 6.93/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.93/1.52 fof(f40,hypothesis,(
% 6.93/1.52 ( 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)) ) ),
% 6.93/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.93/1.52 fof(f41,conjecture,(
% 6.93/1.52 ( ( 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(sdtbsmnsldt0(xA,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(sdtbsmnsldt0(xA,xB))) ))| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB))) ) ) ) )))| isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ) )| isClosed0(sdtbsmnsldt0(xA,xB)) ) ) ),
% 6.93/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.93/1.52 fof(f42,negated_conjecture,(
% 6.93/1.52 ~(( ( 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(sdtbsmnsldt0(xA,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(sdtbsmnsldt0(xA,xB))) ))| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB))) ) ) ) )))| isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ) )| isClosed0(sdtbsmnsldt0(xA,xB)) ) ) )),
% 6.93/1.52 inference(negated_conjecture,[status(cth)],[f41])).
% 6.93/1.52 fof(f198,plain,(
% 6.93/1.52 ![W0]: (~aSubsetOf0(W0,cS1395)|(isClosed0(W0)<=>isOpen0(stldt0(W0))))),
% 6.93/1.52 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 6.93/1.52 fof(f199,plain,(
% 6.93/1.52 ![W0]: (~aSubsetOf0(W0,cS1395)|((~isClosed0(W0)|isOpen0(stldt0(W0)))&(isClosed0(W0)|~isOpen0(stldt0(W0)))))),
% 6.93/1.52 inference(NNF_transformation,[status(thm)],[f198])).
% 6.93/1.52 fof(f200,plain,(
% 6.93/1.52 ![X0]: (~aSubsetOf0(X0,cS1395)|~isClosed0(X0)|isOpen0(stldt0(X0)))),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f199])).
% 6.93/1.52 fof(f206,plain,(
% 6.93/1.52 ![W0,W1]: ((((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|~isOpen0(W0))|~isOpen0(W1))|isOpen0(sdtslmnbsdt0(W0,W1)))),
% 6.93/1.52 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 6.93/1.52 fof(f207,plain,(
% 6.93/1.52 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|~isOpen0(X0)|~isOpen0(X1)|isOpen0(sdtslmnbsdt0(X0,X1)))),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f206])).
% 6.93/1.52 fof(f208,plain,(
% 6.93/1.52 ((((((((((((((((((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)),
% 6.93/1.52 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 6.93/1.52 fof(f209,plain,(
% 6.93/1.52 ((((((((((((((((((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)),
% 6.93/1.52 inference(NNF_transformation,[status(thm)],[f208])).
% 6.93/1.52 fof(f210,plain,(
% 6.93/1.52 ((((((((((((((((((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)),
% 6.93/1.52 inference(miniscoping,[status(thm)],[f209])).
% 6.93/1.52 fof(f211,plain,(
% 6.93/1.52 ((((((((((((((((((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)),
% 6.93/1.52 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))],[f210])).
% 6.93/1.52 fof(f217,plain,(
% 6.93/1.52 aSubsetOf0(xA,cS1395)),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f211])).
% 6.93/1.52 fof(f223,plain,(
% 6.93/1.52 aSubsetOf0(xB,cS1395)),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f211])).
% 6.93/1.52 fof(f242,plain,(
% 6.93/1.52 isClosed0(xA)),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f211])).
% 6.93/1.52 fof(f261,plain,(
% 6.93/1.52 isClosed0(xB)),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f211])).
% 6.93/1.52 fof(f262,plain,(
% 6.93/1.52 ((((((((((((((((((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))),
% 6.93/1.52 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 6.93/1.52 fof(f263,plain,(
% 6.93/1.52 ((((((((((((((((((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))&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))&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))),
% 6.93/1.52 inference(NNF_transformation,[status(thm)],[f262])).
% 6.93/1.52 fof(f264,plain,(
% 6.93/1.52 ((((((((((((((((((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))&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))&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)))))&(![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))),
% 6.93/1.52 inference(miniscoping,[status(thm)],[f263])).
% 6.93/1.52 fof(f273,plain,(
% 6.93/1.52 aSubsetOf0(stldt0(xA),cS1395)),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f264])).
% 6.93/1.52 fof(f282,plain,(
% 6.93/1.52 aSubsetOf0(stldt0(xB),cS1395)),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f264])).
% 6.93/1.52 fof(f302,plain,(
% 6.93/1.52 stldt0(sdtbsmnsldt0(xA,xB))=sdtslmnbsdt0(stldt0(xA),stldt0(xB))),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f264])).
% 6.93/1.52 fof(f303,plain,(
% 6.93/1.52 ((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(sdtbsmnsldt0(xA,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(sdtbsmnsldt0(xA,xB)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB)))))))))&~isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))))&~isClosed0(sdtbsmnsldt0(xA,xB))))),
% 6.93/1.52 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 6.93/1.52 fof(f304,plain,(
% 6.93/1.52 (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(sdtbsmnsldt0(xA,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(sdtbsmnsldt0(xA,xB)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB)))))))))&~isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))))&~isClosed0(sdtbsmnsldt0(xA,xB)))),
% 6.93/1.52 inference(NNF_transformation,[status(thm)],[f303])).
% 6.93/1.52 fof(f305,plain,(
% 6.93/1.52 (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(sdtbsmnsldt0(xA,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(sdtbsmnsldt0(xA,xB)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB)))))))))&~isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))))&~isClosed0(sdtbsmnsldt0(xA,xB)))),
% 6.93/1.52 inference(miniscoping,[status(thm)],[f304])).
% 6.93/1.52 fof(f306,plain,(
% 6.93/1.52 (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)))))))&((aElementOf0(sK18_skl,stldt0(sdtbsmnsldt0(xA,xB)))&(![W1]: ((~aInteger0(W1)|W1=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sK18_skl,W1))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sK18_skl,W1))|(((aInteger0(W2)&(aInteger0(sK19_skl(W2,W1))&sdtasdt0(W1,sK19_skl(W2,W1))=sdtpldt0(W2,smndt0(sK18_skl))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(sK18_skl))))&sdteqdtlpzmzozddtrp0(W2,sK18_skl,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sK18_skl))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(sK18_skl))))&~sdteqdtlpzmzozddtrp0(W2,sK18_skl,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sK18_skl,W1))))))&((aElementOf0(sK20_skl(W1),szAzrzSzezqlpdtcmdtrp0(sK18_skl,W1))&~aElementOf0(sK20_skl(W1),stldt0(sdtbsmnsldt0(xA,xB))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK18_skl,W1),stldt0(sdtbsmnsldt0(xA,xB))))))))&~isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))))&~isClosed0(sdtbsmnsldt0(xA,xB)))),
% 6.93/1.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(W0,sK18_skl),skolemize(W3,sK19_skl(W2,W1)),skolemize(W2,sK20_skl(W1))],[f305])).
% 6.93/1.52 fof(f329,plain,(
% 6.93/1.52 ~isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))),
% 6.93/1.52 inference(cnf_transformation,[status(thm)],[f306])).
% 6.93/1.52 fof(f865,plain,(
% 6.93/1.52 ~aSubsetOf0(xB,cS1395)|isOpen0(stldt0(xB))),
% 6.93/1.52 inference(resolution,[status(thm)],[f200,f261])).
% 6.93/1.52 fof(f866,plain,(
% 6.93/1.52 ~aSubsetOf0(xA,cS1395)|isOpen0(stldt0(xA))),
% 6.93/1.52 inference(resolution,[status(thm)],[f200,f242])).
% 6.93/1.52 fof(f867,definition,(
% 6.93/1.52 sQ19_spl <=> (aSubsetOf0(xB,cS1395))),
% 6.93/1.52 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 6.93/1.52 fof(f869,plain,(
% 6.93/1.52 ~aSubsetOf0(xB,cS1395)|sQ19_spl),
% 6.93/1.52 inference(component_clause,[status(thm)],[f867])).
% 6.93/1.52 fof(f870,definition,(
% 6.93/1.52 sQ20_spl <=> (isOpen0(stldt0(xB)))),
% 6.93/1.52 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 6.93/1.54 fof(f873,plain,(
% 6.93/1.54 ~sQ19_spl|sQ20_spl),
% 6.93/1.54 inference(split_clause,[status(thm)],[f865,f867,f870])).
% 6.93/1.54 fof(f874,definition,(
% 6.93/1.54 sQ21_spl <=> (aSubsetOf0(xA,cS1395))),
% 6.93/1.54 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 6.93/1.54 fof(f876,plain,(
% 6.93/1.54 ~aSubsetOf0(xA,cS1395)|sQ21_spl),
% 6.93/1.54 inference(component_clause,[status(thm)],[f874])).
% 6.93/1.54 fof(f877,definition,(
% 6.93/1.54 sQ22_spl <=> (isOpen0(stldt0(xA)))),
% 6.93/1.54 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 6.93/1.54 fof(f880,plain,(
% 6.93/1.54 ~sQ21_spl|sQ22_spl),
% 6.93/1.54 inference(split_clause,[status(thm)],[f866,f874,f877])).
% 6.93/1.54 fof(f881,plain,(
% 6.93/1.54 $false|sQ21_spl),
% 6.93/1.54 inference(forward_subsumption_resolution,[status(thm)],[f876,f217])).
% 6.93/1.54 fof(f882,plain,(
% 6.93/1.54 sQ21_spl),
% 6.93/1.54 inference(contradiction_clause,[status(thm)],[f881])).
% 6.93/1.54 fof(f883,plain,(
% 6.93/1.54 $false|sQ19_spl),
% 6.93/1.54 inference(forward_subsumption_resolution,[status(thm)],[f869,f223])).
% 6.93/1.54 fof(f884,plain,(
% 6.93/1.54 sQ19_spl),
% 6.93/1.54 inference(contradiction_clause,[status(thm)],[f883])).
% 6.93/1.54 fof(f1287,definition,(
% 6.93/1.54 sQ43_spl <=> (aSubsetOf0(stldt0(xA),cS1395))),
% 6.93/1.54 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 6.93/1.54 fof(f1289,plain,(
% 6.93/1.54 ~aSubsetOf0(stldt0(xA),cS1395)|sQ43_spl),
% 6.93/1.54 inference(component_clause,[status(thm)],[f1287])).
% 6.93/1.54 fof(f1295,plain,(
% 6.93/1.54 $false|sQ43_spl),
% 6.93/1.54 inference(forward_subsumption_resolution,[status(thm)],[f1289,f273])).
% 6.93/1.54 fof(f1296,plain,(
% 6.93/1.54 sQ43_spl),
% 6.93/1.54 inference(contradiction_clause,[status(thm)],[f1295])).
% 6.93/1.54 fof(f1824,definition,(
% 6.93/1.54 sQ103_spl <=> (aSubsetOf0(stldt0(xB),cS1395))),
% 6.93/1.54 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 6.93/1.54 fof(f1826,plain,(
% 6.93/1.54 ~aSubsetOf0(stldt0(xB),cS1395)|sQ103_spl),
% 6.93/1.54 inference(component_clause,[status(thm)],[f1824])).
% 6.93/1.54 fof(f1854,plain,(
% 6.93/1.54 $false|sQ103_spl),
% 6.93/1.54 inference(forward_subsumption_resolution,[status(thm)],[f1826,f282])).
% 6.93/1.54 fof(f1855,plain,(
% 6.93/1.54 sQ103_spl),
% 6.93/1.54 inference(contradiction_clause,[status(thm)],[f1854])).
% 6.93/1.54 fof(f4295,plain,(
% 6.93/1.54 ~aSubsetOf0(stldt0(xA),cS1395)|~aSubsetOf0(stldt0(xB),cS1395)|~isOpen0(stldt0(xA))|~isOpen0(stldt0(xB))|isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))),
% 6.93/1.54 inference(paramodulation,[status(thm)],[f302,f207])).
% 6.93/1.54 fof(f4298,definition,(
% 6.93/1.54 sQ362_spl <=> (isOpen0(stldt0(sdtbsmnsldt0(xA,xB))))),
% 6.93/1.54 introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition])).
% 6.93/1.54 fof(f4299,plain,(
% 6.93/1.54 isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))|~sQ362_spl),
% 6.93/1.54 inference(component_clause,[status(thm)],[f4298])).
% 6.93/1.54 fof(f4301,plain,(
% 6.93/1.54 ~sQ43_spl|~sQ103_spl|~sQ22_spl|~sQ20_spl|sQ362_spl),
% 6.93/1.54 inference(split_clause,[status(thm)],[f4295,f1287,f1824,f877,f870,f4298])).
% 6.93/1.54 fof(f4307,plain,(
% 6.93/1.54 $false|~sQ362_spl),
% 6.93/1.54 inference(forward_subsumption_resolution,[status(thm)],[f4299,f329])).
% 6.93/1.54 fof(f4308,plain,(
% 6.93/1.54 ~sQ362_spl),
% 6.93/1.54 inference(contradiction_clause,[status(thm)],[f4307])).
% 6.93/1.54 fof(f4309,plain,(
% 6.93/1.54 $false),
% 6.93/1.54 inference(sat_refutation,[status(thm)],[f873,f880,f882,f884,f1296,f1855,f4301,f4308])).
% 6.93/1.54 % SZS output end CNFRefutation for theBenchmark.p
% 3.06/1.57 % Elapsed time: 1.142906 seconds
% 3.06/1.57 % CPU time: 7.531771 seconds
% 3.06/1.57 % Total memory used: 166.120 MB
% 3.06/1.57 % Net memory used: 161.011 MB
%------------------------------------------------------------------------------