%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM450+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 : n016.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:56 PM UTC 2026
% Result : Theorem 6.73s 26.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM450+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.13/25.42 % Computer : n016.cluster.edu
% 0.13/25.42 % Model : x86_64 x86_64
% 0.13/25.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/25.42 % Memory : 8046.5625MB
% 0.13/25.42 % OS : Linux 6.8.0-71-generic
% 0.13/25.42 % CPULimit : 300
% 0.13/25.43 % WCLimit : 300
% 0.13/25.43 % DateTime : Mon Sep 21 02:35:34 UTC 2026
% 0.13/25.43 % CPUTime :
% 0.13/25.45 % Drodi V4.1.1
% 6.73/26.39 % Refutation found
% 6.73/26.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.73/26.39 % SZS output start CNFRefutation for theBenchmark
% 6.73/26.39 fof(f43,hypothesis,(
% 6.73/26.39 ( aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ))& aSet0(stldt0(sbsmnsldt0(xS)))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( W0 = sz10| W0 = smndt0(sz10) ) ))& stldt0(sbsmnsldt0(xS)) = cS2076 ) ),
% 6.73/26.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.73/26.39 fof(f45,hypothesis,(
% 6.73/26.39 ( aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=> (? [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(sbsmnsldt0(xS))) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) )))& isOpen0(stldt0(sbsmnsldt0(xS)))& isClosed0(sbsmnsldt0(xS))& aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=> (? [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(sbsmnsldt0(xS))) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) )) )) ),
% 6.73/26.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.73/26.39 fof(f46,conjecture,(
% 6.73/26.39 (? [W0] :( aInteger0(W0)& W0 != sz00& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))& (! [W1] :( ( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=> ( aInteger0(W1)& (? [W2] :( aInteger0(W2)& sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10)) ))& aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))& sdteqdtlpzmzozddtrp0(W1,sz10,W0) ) )& ( ( aInteger0(W1)& ( (? [W2] :( aInteger0(W2)& sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10)) ))| aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))| sdteqdtlpzmzozddtrp0(W1,sz10,W0) ) )=> aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) ) ) ))=> ( ( aSet0(sbsmnsldt0(xS))& (! [W1] :( aElementOf0(W1,sbsmnsldt0(xS))<=> ( aInteger0(W1)& (? [W2] :( aElementOf0(W2,xS)& aElementOf0(W1,W2) ) )) ) ))=> ( (! [W1] :( aElementOf0(W1,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W1)& ~ aElementOf0(W1,sbsmnsldt0(xS)) ) ))=> ( (! [W1] :( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=> aElementOf0(W1,stldt0(sbsmnsldt0(xS))) ))| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))) ) ) ) ) ) )),
% 6.73/26.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.73/26.39 fof(f47,negated_conjecture,(
% 6.73/26.39 ~((? [W0] :( aInteger0(W0)& W0 != sz00& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))& (! [W1] :( ( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=> ( aInteger0(W1)& (? [W2] :( aInteger0(W2)& sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10)) ))& aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))& sdteqdtlpzmzozddtrp0(W1,sz10,W0) ) )& ( ( aInteger0(W1)& ( (? [W2] :( aInteger0(W2)& sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10)) ))| aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))| sdteqdtlpzmzozddtrp0(W1,sz10,W0) ) )=> aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) ) ) ))=> ( ( aSet0(sbsmnsldt0(xS))& (! [W1] :( aElementOf0(W1,sbsmnsldt0(xS))<=> ( aInteger0(W1)& (? [W2] :( aElementOf0(W2,xS)& aElementOf0(W1,W2) ) )) ) ))=> ( (! [W1] :( aElementOf0(W1,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W1)& ~ aElementOf0(W1,sbsmnsldt0(xS)) ) ))=> ( (! [W1] :( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))=> aElementOf0(W1,stldt0(sbsmnsldt0(xS))) ))| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))) ) ) ) ) ) ))),
% 6.73/26.39 inference(negated_conjecture,[status(cth)],[f46])).
% 6.73/26.39 fof(f250,plain,(
% 6.73/26.39 ((((aSet0(sbsmnsldt0(xS))&(![W0]: ((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&(aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&aSet0(stldt0(sbsmnsldt0(xS))))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10)))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10))))))&stldt0(sbsmnsldt0(xS))=cS2076),
% 6.73/26.39 inference(NNF_transformation,[status(thm)],[f43])).
% 6.73/26.39 fof(f251,plain,(
% 6.73/26.39 ((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&aSet0(stldt0(sbsmnsldt0(xS))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10))))))&stldt0(sbsmnsldt0(xS))=cS2076),
% 6.73/26.39 inference(miniscoping,[status(thm)],[f250])).
% 6.73/26.39 fof(f252,plain,(
% 6.73/26.39 ((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK18_skl(W0),xS)&aElementOf0(W0,sK18_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&aSet0(stldt0(sbsmnsldt0(xS))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10))))))&stldt0(sbsmnsldt0(xS))=cS2076),
% 6.73/26.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(W1,sK18_skl(W0))],[f251])).
% 6.73/26.39 fof(f263,plain,(
% 6.73/26.39 ![X0]: (aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|~X0=sz10)),
% 6.73/26.39 inference(cnf_transformation,[status(thm)],[f252])).
% 6.73/26.39 fof(f265,plain,(
% 6.73/26.39 stldt0(sbsmnsldt0(xS))=cS2076),
% 6.73/26.39 inference(cnf_transformation,[status(thm)],[f252])).
% 6.73/26.39 fof(f267,plain,(
% 6.73/26.39 ((((((((aSet0(sbsmnsldt0(xS))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[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(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[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(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),
% 6.73/26.39 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 6.73/26.39 fof(f268,plain,(
% 6.73/26.39 ((((((((aSet0(sbsmnsldt0(xS))&(![W0]: ((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&(aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[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(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(![W0]: ((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&(aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[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(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),
% 6.73/26.39 inference(NNF_transformation,[status(thm)],[f267])).
% 6.73/26.39 fof(f269,plain,(
% 6.73/26.39 ((((((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[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(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[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(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),
% 6.73/26.39 inference(miniscoping,[status(thm)],[f268])).
% 6.73/26.39 fof(f270,plain,(
% 6.73/26.39 ((((((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK19_skl(W0),xS)&aElementOf0(W0,sK19_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(sK20_skl(W0))&~sK20_skl(W0)=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK21_skl(W2,W0))&sdtasdt0(sK20_skl(W0),sK21_skl(W2,W0))=sdtpldt0(W2,smndt0(W0))))&aDivisorOf0(sK20_skl(W0),sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,sK20_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK20_skl(W0),W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(sK20_skl(W0),sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,sK20_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)),stldt0(sbsmnsldt0(xS)))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK22_skl(W0),xS)&aElementOf0(W0,sK22_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(sK23_skl(W0))&~sK23_skl(W0)=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK24_skl(W2,W0))&sdtasdt0(sK23_skl(W0),sK24_skl(W2,W0))=sdtpldt0(W2,smndt0(W0))))&aDivisorOf0(sK23_skl(W0),sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,sK23_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK23_skl(W0),W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(sK23_skl(W0),sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,sK23_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)),stldt0(sbsmnsldt0(xS))))))),
% 6.73/26.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0)),skolemize(W3,sK21_skl(W2,W0)),skolemize(W1,sK22_skl(W0)),skolemize(W1,sK23_skl(W0)),skolemize(W3,sK24_skl(W2,W0))],[f269])).
% 6.73/26.39 fof(f279,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|aInteger0(sK20_skl(X0)))),
% 6.73/26.39 inference(cnf_transformation,[status(thm)],[f270])).
% 6.73/26.39 fof(f280,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|~sK20_skl(X0)=sz00)),
% 6.73/26.39 inference(cnf_transformation,[status(thm)],[f270])).
% 6.73/26.39 fof(f291,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,sK20_skl(X0)),stldt0(sbsmnsldt0(xS))))),
% 6.73/26.39 inference(cnf_transformation,[status(thm)],[f270])).
% 6.73/26.39 fof(f315,plain,(
% 6.73/26.39 (![W0]: ((~aInteger0(W0)|W0=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&(![W1]: ((~aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))|(((aInteger0(W1)&(?[W2]: (aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0)))&((~aInteger0(W1)|(((![W2]: (~aInteger0(W2)|~sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))&~aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W1,sz10,W0)))|aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))&((aSet0(sbsmnsldt0(xS))&(![W1]: (aElementOf0(W1,sbsmnsldt0(xS))<=>(aInteger0(W1)&(?[W2]: (aElementOf0(W2,xS)&aElementOf0(W1,W2)))))))&((![W1]: (aElementOf0(W1,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS)))))&((?[W1]: (aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))&~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))))))))),
% 6.73/26.39 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 6.73/26.39 fof(f316,plain,(
% 6.73/26.39 ![W0]: ((~aInteger0(W0)|W0=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&(![W1]: ((~aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))|(((aInteger0(W1)&(?[W2]: (aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0)))&((~aInteger0(W1)|(((![W2]: (~aInteger0(W2)|~sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))&~aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W1,sz10,W0)))|aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))&((aSet0(sbsmnsldt0(xS))&(![W1]: ((~aElementOf0(W1,sbsmnsldt0(xS))|(aInteger0(W1)&(?[W2]: (aElementOf0(W2,xS)&aElementOf0(W1,W2)))))&(aElementOf0(W1,sbsmnsldt0(xS))|(~aInteger0(W1)|(![W2]: (~aElementOf0(W2,xS)|~aElementOf0(W1,W2))))))))&((![W1]: ((~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS))))&(aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W1)|aElementOf0(W1,sbsmnsldt0(xS))))))&((?[W1]: (aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))&~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))))))))),
% 6.73/26.39 inference(NNF_transformation,[status(thm)],[f315])).
% 6.73/26.39 fof(f317,plain,(
% 6.73/26.39 ![W0]: ((~aInteger0(W0)|W0=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&((![W1]: (~aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))|(((aInteger0(W1)&(?[W2]: (aInteger0(W2)&sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10)))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0))))&(![W1]: ((~aInteger0(W1)|(((![W2]: (~aInteger0(W2)|~sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))&~aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W1,sz10,W0)))|aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))&((aSet0(sbsmnsldt0(xS))&((![W1]: (~aElementOf0(W1,sbsmnsldt0(xS))|(aInteger0(W1)&(?[W2]: (aElementOf0(W2,xS)&aElementOf0(W1,W2))))))&(![W1]: (aElementOf0(W1,sbsmnsldt0(xS))|(~aInteger0(W1)|(![W2]: (~aElementOf0(W2,xS)|~aElementOf0(W1,W2))))))))&(((![W1]: (~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS)))))&(![W1]: (aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W1)|aElementOf0(W1,sbsmnsldt0(xS))))))&((?[W1]: (aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))&~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))))))))),
% 6.73/26.39 inference(miniscoping,[status(thm)],[f316])).
% 6.73/26.39 fof(f318,plain,(
% 6.73/26.39 ![W0]: ((~aInteger0(W0)|W0=sz00)|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0))&((![W1]: (~aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))|(((aInteger0(W1)&(aInteger0(sK25_skl(W1,W0))&sdtasdt0(W0,sK25_skl(W1,W0))=sdtpldt0(W1,smndt0(sz10))))&aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W1,sz10,W0))))&(![W1]: ((~aInteger0(W1)|(((![W2]: (~aInteger0(W2)|~sdtasdt0(W0,W2)=sdtpldt0(W1,smndt0(sz10))))&~aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W1,sz10,W0)))|aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))))))&((aSet0(sbsmnsldt0(xS))&((![W1]: (~aElementOf0(W1,sbsmnsldt0(xS))|(aInteger0(W1)&(aElementOf0(sK26_skl(W1,W0),xS)&aElementOf0(W1,sK26_skl(W1,W0))))))&(![W1]: (aElementOf0(W1,sbsmnsldt0(xS))|(~aInteger0(W1)|(![W2]: (~aElementOf0(W2,xS)|~aElementOf0(W1,W2))))))))&(((![W1]: (~aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(aInteger0(W1)&~aElementOf0(W1,sbsmnsldt0(xS)))))&(![W1]: (aElementOf0(W1,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W1)|aElementOf0(W1,sbsmnsldt0(xS))))))&((aElementOf0(sK27_skl(W0),szAzrzSzezqlpdtcmdtrp0(sz10,W0))&~aElementOf0(sK27_skl(W0),stldt0(sbsmnsldt0(xS))))&~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS))))))))),
% 6.73/26.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl,sK27_skl]),skolemize(W2,sK25_skl(W1,W0)),skolemize(W2,sK26_skl(W1,W0)),skolemize(W1,sK27_skl(W0))],[f317])).
% 6.73/26.39 fof(f338,plain,(
% 6.73/26.39 ![X0]: (~aInteger0(X0)|X0=sz00|~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X0),stldt0(sbsmnsldt0(xS))))),
% 6.73/26.39 inference(cnf_transformation,[status(thm)],[f318])).
% 6.73/26.39 fof(f376,plain,(
% 6.73/26.39 aElementOf0(sz10,stldt0(sbsmnsldt0(xS)))),
% 6.73/26.39 inference(destructive_equality_resolution,[status(thm)],[f263])).
% 6.73/26.39 fof(f682,plain,(
% 6.73/26.39 aElementOf0(sz10,cS2076)),
% 6.73/26.39 inference(forward_demodulation,[status(thm)],[f265,f376])).
% 6.73/26.39 fof(f799,plain,(
% 6.73/26.39 ![X0]: (~aInteger0(X0)|X0=sz00|~aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X0),cS2076))),
% 6.73/26.39 inference(forward_demodulation,[status(thm)],[f265,f338])).
% 6.73/26.39 fof(f2267,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,cS2076)|aInteger0(sK20_skl(X0)))),
% 6.73/26.39 inference(forward_demodulation,[status(thm)],[f265,f279])).
% 6.73/26.39 fof(f2269,plain,(
% 6.73/26.39 aInteger0(sK20_skl(sz10))),
% 6.73/26.39 inference(resolution,[status(thm)],[f2267,f682])).
% 6.73/26.39 fof(f2270,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,cS2076)|~sK20_skl(X0)=sz00)),
% 6.73/26.39 inference(forward_demodulation,[status(thm)],[f265,f280])).
% 6.73/26.39 fof(f2272,plain,(
% 6.73/26.39 ~sK20_skl(sz10)=sz00),
% 6.73/26.39 inference(resolution,[status(thm)],[f2270,f682])).
% 6.73/26.39 fof(f3095,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,cS2076)|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,sK20_skl(X0)),stldt0(sbsmnsldt0(xS))))),
% 6.73/26.39 inference(forward_demodulation,[status(thm)],[f265,f291])).
% 6.73/26.39 fof(f3096,plain,(
% 6.73/26.39 ![X0]: (~aElementOf0(X0,cS2076)|aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,sK20_skl(X0)),cS2076))),
% 6.73/26.39 inference(forward_demodulation,[status(thm)],[f265,f3095])).
% 6.73/26.39 fof(f3098,plain,(
% 6.73/26.39 aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,sK20_skl(sz10)),cS2076)),
% 6.73/26.39 inference(resolution,[status(thm)],[f3096,f682])).
% 6.73/26.39 fof(f4206,plain,(
% 6.73/26.39 ~aInteger0(sK20_skl(sz10))|sK20_skl(sz10)=sz00),
% 6.73/26.39 inference(resolution,[status(thm)],[f3098,f799])).
% 6.73/26.39 fof(f4209,plain,(
% 6.73/26.39 sK20_skl(sz10)=sz00),
% 6.73/26.39 inference(forward_subsumption_resolution,[status(thm)],[f4206,f2269])).
% 6.73/26.39 fof(f4211,plain,(
% 6.73/26.39 $false),
% 6.73/26.39 inference(forward_subsumption_resolution,[status(thm)],[f4209,f2272])).
% 6.73/26.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.86/26.43 % Elapsed time: 0.979466 seconds
% 0.86/26.43 % CPU time: 7.426011 seconds
% 0.86/26.43 % Total memory used: 165.729 MB
% 0.86/26.43 % Net memory used: 160.256 MB
%------------------------------------------------------------------------------