%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM454+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 : n002.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 17.14s 2.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM454+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n002.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.05/0.41 % WCLimit : 300
% 0.05/0.41 % DateTime : Mon Sep 21 02:33:46 UTC 2026
% 0.05/0.41 % CPUTime :
% 0.05/0.44 % Drodi V4.1.1
% 17.14/2.75 % Refutation found
% 17.14/2.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.14/2.75 % SZS output start CNFRefutation for theBenchmark
% 17.14/2.75 fof(f3,axiom,(
% 17.14/2.75 aInteger0(sz10) ),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f4,axiom,(
% 17.14/2.75 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f7,axiom,(
% 17.14/2.75 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f8,axiom,(
% 17.14/2.75 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f9,axiom,(
% 17.14/2.75 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f10,axiom,(
% 17.14/2.75 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f13,axiom,(
% 17.14/2.75 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f14,axiom,(
% 17.14/2.75 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f17,axiom,(
% 17.14/2.75 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> ( sdtasdt0(W0,W1) = sz00=> ( W0 = sz00| W1 = sz00 ) ) ) )),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f46,hypothesis,(
% 17.14/2.75 ( 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))) ) ),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f47,hypothesis,(
% 17.14/2.75 ( (? [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)) ) ),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f49,conjecture,(
% 17.14/2.75 ( sdtpldt0(sz10,xp) != smndt0(sz10)| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ) ),
% 17.14/2.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.14/2.75 fof(f50,negated_conjecture,(
% 17.14/2.75 ~(( sdtpldt0(sz10,xp) != smndt0(sz10)| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ) )),
% 17.14/2.75 inference(negated_conjecture,[status(cth)],[f49])).
% 17.14/2.75 fof(f55,plain,(
% 17.14/2.75 aInteger0(sz10)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f3])).
% 17.14/2.75 fof(f56,plain,(
% 17.14/2.75 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 17.14/2.75 fof(f57,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f56])).
% 17.14/2.75 fof(f62,plain,(
% 17.14/2.75 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 17.14/2.75 fof(f63,plain,(
% 17.14/2.75 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f62])).
% 17.14/2.75 fof(f64,plain,(
% 17.14/2.75 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 17.14/2.75 fof(f65,plain,(
% 17.14/2.75 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f64])).
% 17.14/2.75 fof(f66,plain,(
% 17.14/2.75 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 17.14/2.75 fof(f68,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f66])).
% 17.14/2.75 fof(f69,plain,(
% 17.14/2.75 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 17.14/2.75 fof(f70,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f69])).
% 17.14/2.75 fof(f71,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f69])).
% 17.14/2.75 fof(f76,plain,(
% 17.14/2.75 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 17.14/2.75 fof(f77,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=X0)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f76])).
% 17.14/2.75 fof(f79,plain,(
% 17.14/2.75 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W0,W1),W2)=sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 17.14/2.75 fof(f80,plain,(
% 17.14/2.75 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f79])).
% 17.14/2.75 fof(f88,plain,(
% 17.14/2.75 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|(~sdtasdt0(W0,W1)=sz00|(W0=sz00|W1=sz00)))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 17.14/2.75 fof(f89,plain,(
% 17.14/2.75 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz00|X0=sz00|X1=sz00)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f88])).
% 17.14/2.75 fof(f318,plain,(
% 17.14/2.75 (((((((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)))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 17.14/2.75 fof(f319,plain,(
% 17.14/2.75 (((((((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)))),
% 17.14/2.75 inference(NNF_transformation,[status(thm)],[f318])).
% 17.14/2.75 fof(f320,plain,(
% 17.14/2.75 (((((((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)))),
% 17.14/2.75 inference(miniscoping,[status(thm)],[f319])).
% 17.14/2.75 fof(f321,plain,(
% 17.14/2.75 (((((((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)))),
% 17.14/2.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(W1,sK25_skl(W0)),skolemize(W1,sK26_skl(W0))],[f320])).
% 17.14/2.75 fof(f322,plain,(
% 17.14/2.75 aInteger0(xp)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f321])).
% 17.14/2.75 fof(f323,plain,(
% 17.14/2.75 ~xp=sz00),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f321])).
% 17.14/2.75 fof(f343,plain,(
% 17.14/2.75 (((((((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))),
% 17.14/2.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(W0,sK27_skl),skolemize(W0,sK28_skl)],[f47])).
% 17.14/2.75 fof(f345,plain,(
% 17.14/2.75 sdtasdt0(xp,sK27_skl)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f343])).
% 17.14/2.75 fof(f356,plain,(
% 17.14/2.75 (sdtpldt0(sz10,xp)=smndt0(sz10)&sdtpldt0(sz10,smndt0(xp))=smndt0(sz10))),
% 17.14/2.75 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 17.14/2.75 fof(f357,plain,(
% 17.14/2.75 sdtpldt0(sz10,xp)=smndt0(sz10)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f356])).
% 17.14/2.75 fof(f358,plain,(
% 17.14/2.75 sdtpldt0(sz10,smndt0(xp))=smndt0(sz10)),
% 17.14/2.75 inference(cnf_transformation,[status(thm)],[f356])).
% 17.14/2.75 fof(f566,plain,(
% 17.14/2.75 sdtasdt0(xp,sK27_skl)=sdtpldt0(smndt0(sz10),smndt0(sz10))),
% 17.14/2.75 inference(backward_demodulation,[status(thm)],[f357,f345])).
% 17.14/2.75 fof(f573,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sz10,X0))),
% 17.14/2.75 inference(resolution,[status(thm)],[f65,f55])).
% 17.14/2.75 fof(f575,plain,(
% 17.14/2.75 sz10=sdtpldt0(sz00,sz10)),
% 17.14/2.75 inference(resolution,[status(thm)],[f68,f55])).
% 17.14/2.75 fof(f576,plain,(
% 17.14/2.75 xp=sdtpldt0(sz00,xp)),
% 17.14/2.75 inference(resolution,[status(thm)],[f322,f68])).
% 17.14/2.75 fof(f579,plain,(
% 17.14/2.75 aInteger0(smndt0(xp))),
% 17.14/2.75 inference(resolution,[status(thm)],[f57,f322])).
% 17.14/2.75 fof(f580,plain,(
% 17.14/2.75 aInteger0(smndt0(sz10))),
% 17.14/2.75 inference(resolution,[status(thm)],[f57,f55])).
% 17.14/2.75 fof(f605,plain,(
% 17.14/2.75 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,xp))=sdtpldt0(sdtpldt0(X0,X1),xp))),
% 17.14/2.75 inference(resolution,[status(thm)],[f63,f322])).
% 17.14/2.75 fof(f606,plain,(
% 17.14/2.75 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,sz10))=sdtpldt0(sdtpldt0(X0,X1),sz10))),
% 17.14/2.75 inference(resolution,[status(thm)],[f63,f55])).
% 17.14/2.75 fof(f615,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(sz10,xp))=sdtpldt0(sdtpldt0(X0,sz10),xp))),
% 17.14/2.75 inference(resolution,[status(thm)],[f605,f55])).
% 17.14/2.75 fof(f617,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(sz10))=sdtpldt0(sdtpldt0(X0,sz10),xp))),
% 17.14/2.75 inference(forward_demodulation,[status(thm)],[f357,f615])).
% 17.14/2.75 fof(f620,plain,(
% 17.14/2.75 sdtpldt0(sz10,smndt0(sz10))=sdtpldt0(sdtpldt0(sz10,sz10),xp)),
% 17.14/2.75 inference(resolution,[status(thm)],[f617,f55])).
% 17.14/2.75 fof(f624,plain,(
% 17.14/2.75 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(xp,sz10))=sdtpldt0(sdtpldt0(X0,xp),sz10))),
% 17.14/2.75 inference(resolution,[status(thm)],[f606,f322])).
% 17.14/2.75 fof(f641,plain,(
% 17.14/2.75 sdtpldt0(sz10,smndt0(sz10))=sz00),
% 17.14/2.75 inference(resolution,[status(thm)],[f70,f55])).
% 17.14/2.76 fof(f642,plain,(
% 17.14/2.76 sz00=sdtpldt0(sdtpldt0(sz10,sz10),xp)),
% 17.14/2.76 inference(backward_demodulation,[status(thm)],[f641,f620])).
% 17.14/2.76 fof(f644,plain,(
% 17.14/2.76 sz00=sdtpldt0(smndt0(xp),xp)),
% 17.14/2.76 inference(resolution,[status(thm)],[f71,f322])).
% 17.14/2.76 fof(f645,plain,(
% 17.14/2.76 sz00=sdtpldt0(smndt0(sz10),sz10)),
% 17.14/2.76 inference(resolution,[status(thm)],[f71,f55])).
% 17.14/2.76 fof(f661,plain,(
% 17.14/2.76 sdtasdt0(xp,sz10)=xp),
% 17.14/2.76 inference(resolution,[status(thm)],[f77,f322])).
% 17.14/2.76 fof(f671,plain,(
% 17.14/2.76 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(sz10,sz10))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)))),
% 17.14/2.76 inference(resolution,[status(thm)],[f80,f55])).
% 17.14/2.76 fof(f696,plain,(
% 17.14/2.76 ![X0]: (~aInteger0(X0)|~sdtasdt0(X0,xp)=sz00|X0=sz00|xp=sz00)),
% 17.14/2.76 inference(resolution,[status(thm)],[f89,f322])).
% 17.14/2.76 fof(f698,plain,(
% 17.14/2.76 ![X0]: (~aInteger0(X0)|~sdtasdt0(X0,xp)=sz00|X0=sz00)),
% 17.14/2.76 inference(forward_subsumption_resolution,[status(thm)],[f696,f323])).
% 17.14/2.76 fof(f702,plain,(
% 17.14/2.76 sdtpldt0(xp,sz10)=sdtpldt0(sz10,xp)),
% 17.14/2.76 inference(resolution,[status(thm)],[f573,f322])).
% 17.14/2.76 fof(f706,plain,(
% 17.14/2.76 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(sz10))=sdtpldt0(sdtpldt0(X0,xp),sz10))),
% 17.14/2.76 inference(backward_demodulation,[status(thm)],[f707,f624])).
% 17.14/2.76 fof(f707,plain,(
% 17.14/2.76 sdtpldt0(xp,sz10)=smndt0(sz10)),
% 17.14/2.76 inference(forward_demodulation,[status(thm)],[f357,f702])).
% 17.14/2.76 fof(f721,plain,(
% 17.14/2.76 sdtpldt0(smndt0(xp),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(xp),xp),sz10)),
% 17.14/2.76 inference(resolution,[status(thm)],[f579,f706])).
% 17.14/2.76 fof(f722,plain,(
% 17.14/2.76 sdtpldt0(smndt0(xp),sz10)=sdtpldt0(sz10,smndt0(xp))),
% 17.14/2.76 inference(resolution,[status(thm)],[f579,f573])).
% 17.14/2.76 fof(f746,plain,(
% 17.14/2.76 sdtpldt0(smndt0(xp),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(xp),sz10),xp)),
% 17.14/2.76 inference(resolution,[status(thm)],[f579,f617])).
% 17.14/2.76 fof(f762,plain,(
% 17.14/2.76 sdtpldt0(smndt0(xp),smndt0(sz10))=sdtpldt0(sz00,sz10)),
% 17.14/2.76 inference(forward_demodulation,[status(thm)],[f644,f721])).
% 17.14/2.76 fof(f763,plain,(
% 17.14/2.76 sdtpldt0(smndt0(xp),smndt0(sz10))=sz10),
% 17.14/2.76 inference(forward_demodulation,[status(thm)],[f575,f762])).
% 17.14/2.76 fof(f764,plain,(
% 17.14/2.76 sdtpldt0(smndt0(xp),sz10)=smndt0(sz10)),
% 17.14/2.76 inference(forward_demodulation,[status(thm)],[f358,f722])).
% 15.67/2.78 fof(f768,plain,(
% 15.67/2.78 sz10=sdtpldt0(sdtpldt0(smndt0(xp),sz10),xp)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f763,f746])).
% 15.67/2.78 fof(f770,plain,(
% 15.67/2.78 sz10=sdtpldt0(smndt0(sz10),xp)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f764,f768])).
% 15.67/2.78 fof(f779,plain,(
% 15.67/2.78 sdtpldt0(smndt0(sz10),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(sz10),xp),sz10)),
% 15.67/2.78 inference(resolution,[status(thm)],[f580,f706])).
% 15.67/2.78 fof(f804,plain,(
% 15.67/2.78 sdtpldt0(smndt0(sz10),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)),
% 15.67/2.78 inference(resolution,[status(thm)],[f580,f617])).
% 15.67/2.78 fof(f820,plain,(
% 15.67/2.78 sdtasdt0(xp,sK27_skl)=sdtpldt0(sdtpldt0(smndt0(sz10),xp),sz10)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f566,f779])).
% 15.67/2.78 fof(f821,plain,(
% 15.67/2.78 sz00=sdtpldt0(sdtasdt0(xp,sK27_skl),xp)),
% 15.67/2.78 inference(backward_demodulation,[status(thm)],[f824,f642])).
% 15.67/2.78 fof(f822,plain,(
% 15.67/2.78 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xp,sK27_skl))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)))),
% 15.67/2.78 inference(backward_demodulation,[status(thm)],[f824,f671])).
% 15.67/2.78 fof(f824,plain,(
% 15.67/2.78 sdtasdt0(xp,sK27_skl)=sdtpldt0(sz10,sz10)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f770,f820])).
% 15.67/2.78 fof(f833,plain,(
% 15.67/2.78 sdtasdt0(xp,sK27_skl)=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f566,f804])).
% 15.67/2.78 fof(f834,plain,(
% 15.67/2.78 sdtasdt0(xp,sK27_skl)=sdtpldt0(sz00,xp)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f645,f833])).
% 15.67/2.78 fof(f840,plain,(
% 15.67/2.78 sdtasdt0(xp,sK27_skl)=xp),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f576,f834])).
% 15.67/2.78 fof(f854,plain,(
% 15.67/2.78 sz00=sdtpldt0(xp,xp)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f840,f821])).
% 15.67/2.78 fof(f855,plain,(
% 15.67/2.78 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xp)=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)))),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f840,f822])).
% 15.67/2.78 fof(f1143,plain,(
% 15.67/2.78 sdtasdt0(xp,xp)=sdtpldt0(sdtasdt0(xp,sz10),sdtasdt0(xp,sz10))),
% 15.67/2.78 inference(resolution,[status(thm)],[f855,f322])).
% 15.67/2.78 fof(f1151,plain,(
% 15.67/2.78 sdtasdt0(xp,xp)=sdtpldt0(xp,sdtasdt0(xp,sz10))),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f661,f1143])).
% 15.67/2.78 fof(f1152,plain,(
% 15.67/2.78 sdtasdt0(xp,xp)=sdtpldt0(xp,xp)),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f661,f1151])).
% 15.67/2.78 fof(f1155,plain,(
% 15.67/2.78 sdtasdt0(xp,xp)=sz00),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f854,f1152])).
% 15.67/2.78 fof(f1858,plain,(
% 15.67/2.78 ~sdtasdt0(xp,xp)=sz00|xp=sz00),
% 15.67/2.78 inference(resolution,[status(thm)],[f698,f322])).
% 15.67/2.78 fof(f1862,plain,(
% 15.67/2.78 ~sz00=sz00|xp=sz00),
% 15.67/2.78 inference(forward_demodulation,[status(thm)],[f1155,f1858])).
% 15.67/2.78 fof(f1863,plain,(
% 15.67/2.78 xp=sz00),
% 15.67/2.78 inference(trivial_equality_resolution,[status(thm)],[f1862])).
% 15.67/2.78 fof(f1864,plain,(
% 15.67/2.78 $false),
% 15.67/2.78 inference(forward_subsumption_resolution,[status(thm)],[f1863,f323])).
% 15.67/2.78 % SZS output end CNFRefutation for theBenchmark.p
% 15.67/2.80 % Elapsed time: 2.364587 seconds
% 15.67/2.80 % CPU time: 18.252235 seconds
% 15.67/2.80 % Total memory used: 247.888 MB
% 15.67/2.80 % Net memory used: 235.895 MB
%------------------------------------------------------------------------------