%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM452+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 : n014.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 12.85s 2.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM452+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.14/0.42 % Computer : n014.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 02:31:20 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.45 % Drodi V4.1.1
% 12.85/2.19 % Refutation found
% 12.85/2.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.85/2.19 % SZS output start CNFRefutation for theBenchmark
% 12.85/2.19 fof(f2,axiom,(
% 12.85/2.19 aInteger0(sz00) ),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f3,axiom,(
% 12.85/2.19 aInteger0(sz10) ),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f4,axiom,(
% 12.85/2.19 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f7,axiom,(
% 12.85/2.19 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f8,axiom,(
% 12.85/2.19 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f9,axiom,(
% 12.85/2.19 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f10,axiom,(
% 12.85/2.19 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f12,axiom,(
% 12.85/2.19 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f13,axiom,(
% 12.85/2.19 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f14,axiom,(
% 12.85/2.19 (! [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)) ) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f15,axiom,(
% 12.85/2.19 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f16,axiom,(
% 12.85/2.19 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0)& smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) )),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f46,hypothesis,(
% 12.85/2.19 ( 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))) ) ),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f47,conjecture,(
% 12.85/2.19 ( ( (? [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)) ) ) ),
% 12.85/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.85/2.19 fof(f48,negated_conjecture,(
% 12.85/2.19 ~(( ( (? [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)) ) ) )),
% 12.85/2.19 inference(negated_conjecture,[status(cth)],[f47])).
% 12.85/2.19 fof(f52,plain,(
% 12.85/2.19 aInteger0(sz00)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f2])).
% 12.85/2.19 fof(f53,plain,(
% 12.85/2.19 aInteger0(sz10)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f3])).
% 12.85/2.19 fof(f54,plain,(
% 12.85/2.19 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 12.85/2.19 fof(f55,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f54])).
% 12.85/2.19 fof(f60,plain,(
% 12.85/2.19 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 12.85/2.19 fof(f61,plain,(
% 12.85/2.19 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f60])).
% 12.85/2.19 fof(f62,plain,(
% 12.85/2.19 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 12.85/2.19 fof(f63,plain,(
% 12.85/2.19 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f62])).
% 12.85/2.19 fof(f64,plain,(
% 12.85/2.19 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 12.85/2.19 fof(f65,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=X0)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f64])).
% 12.85/2.19 fof(f66,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f64])).
% 12.85/2.19 fof(f67,plain,(
% 12.85/2.19 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 12.85/2.19 fof(f68,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f67])).
% 12.85/2.19 fof(f72,plain,(
% 12.85/2.19 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 12.85/2.19 fof(f73,plain,(
% 12.85/2.19 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f72])).
% 12.85/2.19 fof(f74,plain,(
% 12.85/2.19 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 12.85/2.19 fof(f75,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=X0)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f74])).
% 12.85/2.19 fof(f77,plain,(
% 12.85/2.19 ![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))))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 12.85/2.19 fof(f79,plain,(
% 12.85/2.19 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f77])).
% 12.85/2.19 fof(f80,plain,(
% 12.85/2.19 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 12.85/2.19 fof(f81,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f80])).
% 12.85/2.19 fof(f83,plain,(
% 12.85/2.19 ![W0]: (~aInteger0(W0)|(sdtasdt0(smndt0(sz10),W0)=smndt0(W0)&smndt0(W0)=sdtasdt0(W0,smndt0(sz10))))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 12.85/2.19 fof(f84,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(smndt0(sz10),X0)=smndt0(X0))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f83])).
% 12.85/2.19 fof(f85,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|smndt0(X0)=sdtasdt0(X0,smndt0(sz10)))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f83])).
% 12.85/2.19 fof(f316,plain,(
% 12.85/2.19 (((((((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)))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 12.85/2.19 fof(f317,plain,(
% 12.85/2.19 (((((((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)))),
% 12.85/2.19 inference(NNF_transformation,[status(thm)],[f316])).
% 12.85/2.19 fof(f318,plain,(
% 12.85/2.19 (((((((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)))),
% 12.85/2.19 inference(miniscoping,[status(thm)],[f317])).
% 12.85/2.19 fof(f319,plain,(
% 12.85/2.19 (((((((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)))),
% 12.85/2.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(W1,sK25_skl(W0)),skolemize(W1,sK26_skl(W0))],[f318])).
% 12.85/2.19 fof(f320,plain,(
% 12.85/2.19 aInteger0(xp)),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f319])).
% 12.85/2.19 fof(f341,plain,(
% 12.85/2.19 (((((![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))))),
% 12.85/2.19 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 12.85/2.19 fof(f342,definition,(
% 12.85/2.19 sP2_prd<=>((((![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)))),
% 12.85/2.19 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 12.85/2.19 fof(f343,plain,(
% 12.85/2.19 sP2_prd|((((![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)))),
% 12.85/2.19 inference(formula_renaming,[status(thm)],[f341,f342])).
% 12.85/2.19 fof(f344,plain,(
% 12.85/2.19 ![X0]: (sP2_prd|~aInteger0(X0)|~sdtasdt0(xp,X0)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f343])).
% 12.85/2.19 fof(f359,plain,(
% 12.85/2.19 (~sP2_prd|((((![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))))&(sP2_prd|((((?[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))))),
% 12.85/2.19 inference(NNF_transformation,[status(thm)],[f342])).
% 12.85/2.19 fof(f360,plain,(
% 12.85/2.19 (~sP2_prd|((((![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))))&(sP2_prd|((((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))))),
% 12.85/2.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(W0,sK27_skl)],[f359])).
% 12.85/2.19 fof(f361,plain,(
% 12.85/2.19 ![X0]: (~sP2_prd|~aInteger0(X0)|~sdtasdt0(xp,X0)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))),
% 12.85/2.19 inference(cnf_transformation,[status(thm)],[f360])).
% 12.85/2.19 fof(f566,plain,(
% 12.85/2.19 aInteger0(smndt0(sz10))),
% 12.85/2.19 inference(resolution,[status(thm)],[f55,f53])).
% 12.85/2.19 fof(f601,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sz00,X0))),
% 12.85/2.19 inference(resolution,[status(thm)],[f63,f52])).
% 12.85/2.19 fof(f602,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sz10,X0))),
% 12.85/2.19 inference(resolution,[status(thm)],[f63,f53])).
% 12.85/2.19 fof(f611,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz00)=sdtasdt0(sz00,X0))),
% 12.85/2.19 inference(resolution,[status(thm)],[f73,f52])).
% 12.85/2.19 fof(f628,plain,(
% 12.85/2.19 sdtpldt0(sz10,smndt0(sz10))=sz00),
% 12.85/2.19 inference(resolution,[status(thm)],[f68,f53])).
% 12.85/2.19 fof(f691,plain,(
% 12.85/2.19 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(sdtpldt0(X0,sz00),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(sz00,X1)))),
% 12.85/2.19 inference(resolution,[status(thm)],[f79,f52])).
% 12.85/2.19 fof(f845,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,sz00),xp)=sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(sz00,xp)))),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f691])).
% 12.85/2.19 fof(f892,plain,(
% 12.85/2.19 sdtasdt0(xp,sz00)=sdtasdt0(sz00,xp)),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f611])).
% 12.85/2.19 fof(f894,plain,(
% 12.85/2.19 sdtpldt0(xp,sz10)=sdtpldt0(sz10,xp)),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f602])).
% 12.85/2.19 fof(f902,plain,(
% 12.85/2.19 smndt0(xp)=sdtasdt0(xp,smndt0(sz10))),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f85])).
% 12.85/2.19 fof(f903,plain,(
% 12.85/2.19 sdtasdt0(smndt0(sz10),xp)=smndt0(xp)),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f84])).
% 12.85/2.19 fof(f909,plain,(
% 12.85/2.19 aInteger0(smndt0(xp))),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f55])).
% 12.85/2.19 fof(f910,plain,(
% 12.85/2.19 sdtasdt0(xp,sz00)=sz00),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f81])).
% 12.85/2.19 fof(f912,plain,(
% 12.85/2.19 sdtasdt0(xp,sz10)=xp),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f75])).
% 12.85/2.19 fof(f914,plain,(
% 12.85/2.19 sdtpldt0(xp,sz00)=xp),
% 12.85/2.19 inference(resolution,[status(thm)],[f320,f65])).
% 12.85/2.19 fof(f929,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,sz00),xp)=sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(xp,sz00)))),
% 12.85/2.19 inference(backward_demodulation,[status(thm)],[f892,f845])).
% 12.85/2.19 fof(f934,plain,(
% 12.85/2.19 ![X0]: (~sP2_prd|~aInteger0(X0)|~sdtasdt0(xp,X0)=sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10)))),
% 12.85/2.19 inference(backward_demodulation,[status(thm)],[f894,f361])).
% 12.85/2.19 fof(f965,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,sz00),xp)=sdtpldt0(sdtasdt0(X0,xp),sz00))),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f910,f929])).
% 12.85/2.19 fof(f1273,plain,(
% 12.85/2.19 sdtasdt0(sdtpldt0(smndt0(sz10),sz00),xp)=sdtpldt0(sdtasdt0(smndt0(sz10),xp),sz00)),
% 12.85/2.19 inference(resolution,[status(thm)],[f566,f965])).
% 12.85/2.19 fof(f1355,plain,(
% 12.85/2.19 sdtpldt0(smndt0(sz10),sz00)=sdtpldt0(sz00,smndt0(sz10))),
% 12.85/2.19 inference(resolution,[status(thm)],[f566,f601])).
% 12.85/2.19 fof(f1359,plain,(
% 12.85/2.19 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,smndt0(sz10)))=sdtpldt0(sdtpldt0(X0,X1),smndt0(sz10)))),
% 12.85/2.19 inference(resolution,[status(thm)],[f566,f61])).
% 12.85/2.19 fof(f1373,plain,(
% 12.85/2.19 smndt0(sz10)=sdtpldt0(sz00,smndt0(sz10))),
% 12.85/2.19 inference(resolution,[status(thm)],[f566,f66])).
% 12.85/2.19 fof(f1384,plain,(
% 12.85/2.19 sdtasdt0(sdtpldt0(smndt0(sz10),sz00),xp)=sdtpldt0(smndt0(xp),sz00)),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f903,f1273])).
% 12.85/2.19 fof(f1460,plain,(
% 12.85/2.19 sdtasdt0(sdtpldt0(sz00,smndt0(sz10)),xp)=sdtpldt0(smndt0(xp),sz00)),
% 12.85/2.19 inference(backward_demodulation,[status(thm)],[f1355,f1384])).
% 12.85/2.19 fof(f1482,plain,(
% 12.85/2.19 sdtasdt0(smndt0(sz10),xp)=sdtpldt0(smndt0(xp),sz00)),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f1373,f1460])).
% 12.85/2.19 fof(f1483,plain,(
% 12.85/2.19 smndt0(xp)=sdtpldt0(smndt0(xp),sz00)),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f903,f1482])).
% 12.85/2.19 fof(f1871,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(sz10,smndt0(sz10)))=sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10)))),
% 12.85/2.19 inference(resolution,[status(thm)],[f1359,f53])).
% 12.85/2.19 fof(f1873,plain,(
% 12.85/2.19 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10)))),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f628,f1871])).
% 12.85/2.19 fof(f1875,plain,(
% 12.85/2.19 sdtpldt0(xp,sz00)=sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10))),
% 12.85/2.19 inference(resolution,[status(thm)],[f1873,f320])).
% 12.85/2.19 fof(f1888,plain,(
% 12.85/2.19 ![X0]: (~sP2_prd|~aInteger0(X0)|~sdtasdt0(xp,X0)=xp)),
% 12.85/2.19 inference(backward_demodulation,[status(thm)],[f1892,f934])).
% 12.85/2.19 fof(f1892,plain,(
% 12.85/2.19 xp=sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10))),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f914,f1875])).
% 12.85/2.19 fof(f2201,plain,(
% 12.85/2.19 sdtpldt0(smndt0(xp),sz00)=sdtpldt0(sdtpldt0(smndt0(xp),sz10),smndt0(sz10))),
% 12.85/2.19 inference(resolution,[status(thm)],[f909,f1873])).
% 12.85/2.19 fof(f2319,plain,(
% 12.85/2.19 sdtpldt0(smndt0(xp),sz10)=sdtpldt0(sz10,smndt0(xp))),
% 12.85/2.19 inference(resolution,[status(thm)],[f909,f602])).
% 12.85/2.19 fof(f2348,plain,(
% 12.85/2.19 smndt0(xp)=sdtpldt0(sdtpldt0(smndt0(xp),sz10),smndt0(sz10))),
% 12.85/2.19 inference(forward_demodulation,[status(thm)],[f1483,f2201])).
% 13.61/2.21 fof(f2470,plain,(
% 13.61/2.21 smndt0(xp)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))),
% 13.61/2.21 inference(backward_demodulation,[status(thm)],[f2319,f2348])).
% 13.61/2.21 fof(f2480,plain,(
% 13.61/2.21 ![X0]: (sP2_prd|~aInteger0(X0)|~sdtasdt0(xp,X0)=smndt0(xp))),
% 13.61/2.21 inference(backward_demodulation,[status(thm)],[f2470,f344])).
% 13.61/2.21 fof(f2557,plain,(
% 13.61/2.21 sP2_prd|~sdtasdt0(xp,smndt0(sz10))=smndt0(xp)),
% 13.61/2.21 inference(resolution,[status(thm)],[f2480,f566])).
% 13.61/2.21 fof(f2562,plain,(
% 13.61/2.21 sP2_prd|~smndt0(xp)=smndt0(xp)),
% 13.61/2.21 inference(forward_demodulation,[status(thm)],[f902,f2557])).
% 13.61/2.21 fof(f2563,plain,(
% 13.61/2.21 ![X0]: (~aInteger0(X0)|~sdtasdt0(xp,X0)=xp)),
% 13.61/2.21 inference(backward_subsumption_resolution,[status(thm)],[f1888,f2567])).
% 13.61/2.21 fof(f2567,plain,(
% 13.61/2.21 sP2_prd),
% 13.61/2.21 inference(trivial_equality_resolution,[status(thm)],[f2562])).
% 13.61/2.21 fof(f2574,plain,(
% 13.61/2.21 ~sdtasdt0(xp,sz10)=xp),
% 13.61/2.21 inference(resolution,[status(thm)],[f2563,f53])).
% 13.61/2.21 fof(f2577,plain,(
% 13.61/2.21 ~xp=xp),
% 13.61/2.21 inference(forward_demodulation,[status(thm)],[f912,f2574])).
% 13.61/2.21 fof(f2578,plain,(
% 13.61/2.21 $false),
% 13.61/2.21 inference(trivial_equality_resolution,[status(thm)],[f2577])).
% 13.61/2.21 % SZS output end CNFRefutation for theBenchmark.p
% 5.54/2.24 % Elapsed time: 1.804715 seconds
% 5.54/2.24 % CPU time: 13.890134 seconds
% 5.54/2.24 % Total memory used: 197.665 MB
% 5.54/2.24 % Net memory used: 190.027 MB
%------------------------------------------------------------------------------