%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM455+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 : n012.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 0.09s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM455+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 02:31:23 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.55 % Refutation found
% 0.09/0.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.55 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.55 fof(f3,axiom,(
% 0.09/0.55 aInteger0(sz10) ),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f4,axiom,(
% 0.09/0.55 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f5,axiom,(
% 0.09/0.55 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtpldt0(W0,W1)) ) )),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f46,hypothesis,(
% 0.09/0.55 ( aInteger0(xp)& xp != sz00& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))& (! [W0] :( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=> ( aInteger0(W0)& (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))& sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) )& ( ( aInteger0(W0)& ( (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))| aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))| sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) )=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) ))& 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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=> aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ) ),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f47,hypothesis,(
% 0.09/0.55 ( (? [W0] :( aInteger0(W0)& sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) ))& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))& (? [W0] :( aInteger0(W0)& sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) ))& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)& aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) ),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f48,hypothesis,(
% 0.09/0.55 ( sdtpldt0(sz10,xp) != sz10& sdtpldt0(sz10,smndt0(xp)) != sz10 ) ),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f49,hypothesis,(
% 0.09/0.55 ( sdtpldt0(sz10,xp) != smndt0(sz10)| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ) ),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f50,conjecture,(
% 0.09/0.55 (? [W0] :( ( ( aInteger0(W0)& ( (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))| aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))| sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) )| aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )& ~ ( ( W0 = sz10| W0 = smndt0(sz10) )& aElementOf0(W0,cS2200) ) ) )),
% 0.09/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f51,negated_conjecture,(
% 0.09/0.55 ~((? [W0] :( ( ( aInteger0(W0)& ( (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))| aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))| sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) )| aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )& ~ ( ( W0 = sz10| W0 = smndt0(sz10) )& aElementOf0(W0,cS2200) ) ) ))),
% 0.09/0.55 inference(negated_conjecture,[status(cth)],[f50])).
% 0.09/0.55 fof(f56,plain,(
% 0.09/0.55 aInteger0(sz10)),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.55 fof(f57,plain,(
% 0.09/0.55 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.09/0.55 fof(f58,plain,(
% 0.09/0.55 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f57])).
% 0.09/0.55 fof(f59,plain,(
% 0.09/0.55 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtpldt0(W0,W1)))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.09/0.55 fof(f60,plain,(
% 0.09/0.55 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtpldt0(X0,X1)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f59])).
% 0.09/0.55 fof(f319,plain,(
% 0.09/0.55 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(![W0]: ((~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.09/0.55 fof(f320,plain,(
% 0.09/0.55 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(![W0]: ((~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.55 inference(NNF_transformation,[status(thm)],[f319])).
% 0.09/0.55 fof(f321,plain,(
% 0.09/0.55 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp))))&(![W0]: ((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.55 inference(miniscoping,[status(thm)],[f320])).
% 0.09/0.55 fof(f322,plain,(
% 0.09/0.55 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(aInteger0(sK25_skl(W0))&sdtasdt0(xp,sK25_skl(W0))=sdtpldt0(W0,smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp))))&(![W0]: ((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&aSet0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK26_skl(W0),xS)&aElementOf0(W0,sK26_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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(W1,sK25_skl(W0)),skolemize(W1,sK26_skl(W0))],[f321])).
% 0.09/0.55 fof(f323,plain,(
% 0.09/0.55 aInteger0(xp)),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f322])).
% 0.09/0.55 fof(f344,plain,(
% 0.09/0.55 (((((((aInteger0(sK27_skl)&sdtasdt0(xp,sK27_skl)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))&aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp))&aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(aInteger0(sK28_skl)&sdtasdt0(xp,sK28_skl)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp))&aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))),
% 0.09/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(W0,sK27_skl),skolemize(W0,sK28_skl)],[f47])).
% 0.09/0.55 fof(f347,plain,(
% 0.09/0.55 aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f344])).
% 0.09/0.55 fof(f352,plain,(
% 0.09/0.55 aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f344])).
% 0.09/0.55 fof(f355,plain,(
% 0.09/0.55 ~sdtpldt0(sz10,xp)=sz10),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f48])).
% 0.09/0.55 fof(f356,plain,(
% 0.09/0.55 ~sdtpldt0(sz10,smndt0(xp))=sz10),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f48])).
% 0.09/0.55 fof(f357,plain,(
% 0.09/0.55 ~sdtpldt0(sz10,xp)=smndt0(sz10)|~sdtpldt0(sz10,smndt0(xp))=smndt0(sz10)),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f49])).
% 0.09/0.55 fof(f358,plain,(
% 0.09/0.55 (![W0]: (((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))|((W0=sz10|W0=smndt0(sz10))&aElementOf0(W0,cS2200))))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.09/0.55 fof(f359,definition,(
% 0.09/0.55 ![W0]: (sP2_prd(W0)<=>((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.09/0.55 fof(f360,plain,(
% 0.09/0.55 ![W0]: (sP2_prd(W0)|((W0=sz10|W0=smndt0(sz10))&aElementOf0(W0,cS2200)))),
% 0.09/0.55 inference(formula_renaming,[status(thm)],[f358,f359])).
% 0.09/0.55 fof(f361,plain,(
% 0.09/0.55 ![X0]: (sP2_prd(X0)|X0=sz10|X0=smndt0(sz10))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f360])).
% 0.09/0.55 fof(f374,plain,(
% 0.09/0.55 ![W0]: ((~sP2_prd(W0)|((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))&(sP2_prd(W0)|((aInteger0(W0)&(((?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))|aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))|sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))),
% 0.09/0.55 inference(NNF_transformation,[status(thm)],[f359])).
% 0.09/0.55 fof(f375,plain,(
% 0.09/0.55 (![W0]: (~sP2_prd(W0)|((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))&(![W0]: (sP2_prd(W0)|((aInteger0(W0)&(((?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))|aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))|sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))),
% 0.09/0.55 inference(miniscoping,[status(thm)],[f374])).
% 0.09/0.55 fof(f376,plain,(
% 0.09/0.55 (![W0]: (~sP2_prd(W0)|((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))&(![W0]: (sP2_prd(W0)|((aInteger0(W0)&(((aInteger0(sK29_skl(W0))&sdtasdt0(xp,sK29_skl(W0))=sdtpldt0(W0,smndt0(sz10)))|aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))|sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))),
% 0.09/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(W1,sK29_skl(W0))],[f375])).
% 0.09/0.55 fof(f378,plain,(
% 0.09/0.55 ![X0]: (~sP2_prd(X0)|~aInteger0(X0)|~aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f376])).
% 0.09/0.55 fof(f415,definition,(
% 0.09/0.55 sQ8_spl <=> (sdtpldt0(sz10,xp)=smndt0(sz10))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f418,definition,(
% 0.09/0.55 sQ9_spl <=> (sdtpldt0(sz10,smndt0(xp))=smndt0(sz10))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f421,plain,(
% 0.09/0.55 ~sQ8_spl|~sQ9_spl),
% 0.09/0.55 inference(split_clause,[status(thm)],[f357,f415,f418])).
% 0.09/0.55 fof(f512,definition,(
% 0.09/0.55 sQ13_spl <=> (aInteger0(xp))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f514,plain,(
% 0.09/0.55 ~aInteger0(xp)|sQ13_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f512])).
% 0.09/0.55 fof(f517,definition,(
% 0.09/0.55 sQ14_spl <=> (aInteger0(sz10))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f519,plain,(
% 0.09/0.55 ~aInteger0(sz10)|sQ14_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f517])).
% 0.09/0.55 fof(f957,plain,(
% 0.09/0.55 $false|sQ14_spl),
% 0.09/0.55 inference(forward_subsumption_resolution,[status(thm)],[f519,f56])).
% 0.09/0.55 fof(f958,plain,(
% 0.09/0.55 sQ14_spl),
% 0.09/0.55 inference(contradiction_clause,[status(thm)],[f957])).
% 0.09/0.55 fof(f987,definition,(
% 0.09/0.55 sQ40_spl <=> (aInteger0(smndt0(xp)))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f989,plain,(
% 0.09/0.55 ~aInteger0(smndt0(xp))|sQ40_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f987])).
% 0.09/0.55 fof(f991,plain,(
% 0.09/0.55 $false|sQ13_spl),
% 0.09/0.55 inference(forward_subsumption_resolution,[status(thm)],[f514,f323])).
% 0.09/0.55 fof(f992,plain,(
% 0.09/0.55 sQ13_spl),
% 0.09/0.55 inference(contradiction_clause,[status(thm)],[f991])).
% 0.09/0.55 fof(f2000,definition,(
% 0.09/0.55 sQ109_spl <=> (aInteger0(sdtpldt0(sz10,xp)))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f2002,plain,(
% 0.09/0.55 ~aInteger0(sdtpldt0(sz10,xp))|sQ109_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f2000])).
% 0.09/0.55 fof(f2028,plain,(
% 0.09/0.55 ~aInteger0(sz10)|~aInteger0(xp)|sQ109_spl),
% 0.09/0.55 inference(resolution,[status(thm)],[f2002,f60])).
% 0.09/0.55 fof(f2029,plain,(
% 0.09/0.55 ~sQ14_spl|~sQ13_spl|sQ109_spl),
% 0.09/0.55 inference(split_clause,[status(thm)],[f2028,f517,f512,f2000])).
% 0.09/0.55 fof(f2216,plain,(
% 0.09/0.55 ~sP2_prd(sdtpldt0(sz10,xp))|~aInteger0(sdtpldt0(sz10,xp))),
% 0.09/0.55 inference(resolution,[status(thm)],[f347,f378])).
% 0.09/0.55 fof(f2221,definition,(
% 0.09/0.55 sQ115_spl <=> (sP2_prd(sdtpldt0(sz10,xp)))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f2223,plain,(
% 0.09/0.55 ~sP2_prd(sdtpldt0(sz10,xp))|sQ115_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f2221])).
% 0.09/0.55 fof(f2224,plain,(
% 0.09/0.55 ~sQ115_spl|~sQ109_spl),
% 0.09/0.55 inference(split_clause,[status(thm)],[f2216,f2221,f2000])).
% 0.09/0.55 fof(f2269,plain,(
% 0.09/0.55 sdtpldt0(sz10,xp)=sz10|sdtpldt0(sz10,xp)=smndt0(sz10)|sQ115_spl),
% 0.09/0.55 inference(resolution,[status(thm)],[f2223,f361])).
% 0.09/0.55 fof(f2271,definition,(
% 0.09/0.55 sQ119_spl <=> (sdtpldt0(sz10,xp)=sz10)),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f2272,plain,(
% 0.09/0.55 sdtpldt0(sz10,xp)=sz10|~sQ119_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f2271])).
% 0.09/0.55 fof(f2274,plain,(
% 0.09/0.55 sQ119_spl|sQ8_spl|sQ115_spl),
% 0.09/0.55 inference(split_clause,[status(thm)],[f2269,f2271,f415,f2221])).
% 0.09/0.55 fof(f2275,plain,(
% 0.09/0.55 $false|~sQ119_spl),
% 0.09/0.55 inference(forward_subsumption_resolution,[status(thm)],[f2272,f355])).
% 0.09/0.55 fof(f2276,plain,(
% 0.09/0.55 ~sQ119_spl),
% 0.09/0.55 inference(contradiction_clause,[status(thm)],[f2275])).
% 0.09/0.55 fof(f2408,plain,(
% 0.09/0.55 ~sP2_prd(sdtpldt0(sz10,smndt0(xp)))|~aInteger0(sdtpldt0(sz10,smndt0(xp)))),
% 0.09/0.55 inference(resolution,[status(thm)],[f352,f378])).
% 0.09/0.55 fof(f2412,definition,(
% 0.09/0.55 sQ125_spl <=> (aInteger0(sdtpldt0(sz10,smndt0(xp))))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f2414,plain,(
% 0.09/0.56 ~aInteger0(sdtpldt0(sz10,smndt0(xp)))|sQ125_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f2412])).
% 0.09/0.56 fof(f2419,definition,(
% 0.09/0.56 sQ127_spl <=> (sP2_prd(sdtpldt0(sz10,smndt0(xp))))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f2421,plain,(
% 0.09/0.56 ~sP2_prd(sdtpldt0(sz10,smndt0(xp)))|sQ127_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f2419])).
% 0.09/0.56 fof(f2422,plain,(
% 0.09/0.56 ~sQ127_spl|~sQ125_spl),
% 0.09/0.56 inference(split_clause,[status(thm)],[f2408,f2419,f2412])).
% 0.09/0.56 fof(f2437,plain,(
% 0.09/0.56 ~aInteger0(sz10)|~aInteger0(smndt0(xp))|sQ125_spl),
% 0.09/0.56 inference(resolution,[status(thm)],[f2414,f60])).
% 0.09/0.56 fof(f2438,plain,(
% 0.09/0.56 ~sQ14_spl|~sQ40_spl|sQ125_spl),
% 0.09/0.56 inference(split_clause,[status(thm)],[f2437,f517,f987,f2412])).
% 0.09/0.56 fof(f2439,plain,(
% 0.09/0.56 ~aInteger0(xp)|sQ40_spl),
% 0.09/0.56 inference(resolution,[status(thm)],[f989,f58])).
% 0.09/0.56 fof(f2440,plain,(
% 0.09/0.56 ~sQ13_spl|sQ40_spl),
% 1.21/0.56 inference(split_clause,[status(thm)],[f2439,f512,f987])).
% 1.21/0.56 fof(f2469,plain,(
% 1.21/0.56 sdtpldt0(sz10,smndt0(xp))=sz10|sdtpldt0(sz10,smndt0(xp))=smndt0(sz10)|sQ127_spl),
% 1.21/0.56 inference(resolution,[status(thm)],[f2421,f361])).
% 1.21/0.56 fof(f2471,definition,(
% 1.21/0.56 sQ131_spl <=> (sdtpldt0(sz10,smndt0(xp))=sz10)),
% 1.21/0.56 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 1.21/0.56 fof(f2472,plain,(
% 1.21/0.56 sdtpldt0(sz10,smndt0(xp))=sz10|~sQ131_spl),
% 1.21/0.56 inference(component_clause,[status(thm)],[f2471])).
% 1.21/0.56 fof(f2474,plain,(
% 1.21/0.56 sQ131_spl|sQ9_spl|sQ127_spl),
% 1.21/0.56 inference(split_clause,[status(thm)],[f2469,f2471,f418,f2419])).
% 1.21/0.56 fof(f2475,plain,(
% 1.21/0.56 $false|~sQ131_spl),
% 1.21/0.56 inference(forward_subsumption_resolution,[status(thm)],[f2472,f356])).
% 1.21/0.56 fof(f2476,plain,(
% 1.21/0.56 ~sQ131_spl),
% 1.21/0.56 inference(contradiction_clause,[status(thm)],[f2475])).
% 1.21/0.56 fof(f2477,plain,(
% 1.21/0.56 $false),
% 1.21/0.56 inference(sat_refutation,[status(thm)],[f421,f958,f992,f2029,f2224,f2274,f2276,f2422,f2438,f2440,f2474,f2476])).
% 1.21/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 1.21/0.57 % Elapsed time: 0.212242 seconds
% 1.21/0.57 % CPU time: 1.437538 seconds
% 1.21/0.57 % Total memory used: 135.096 MB
% 1.21/0.57 % Net memory used: 132.872 MB
%------------------------------------------------------------------------------