%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM453+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 : n019.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.15s 6.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM453+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.10/5.38 % Computer : n019.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 02:31:41 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 0.15/6.04 % Refutation found
% 0.15/6.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/6.04 % SZS output start CNFRefutation for theBenchmark
% 0.15/6.04 fof(f2,axiom,(
% 0.15/6.04 aInteger0(sz00) ),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f3,axiom,(
% 0.15/6.04 aInteger0(sz10) ),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f4,axiom,(
% 0.15/6.04 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f7,axiom,(
% 0.15/6.04 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f8,axiom,(
% 0.15/6.04 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f9,axiom,(
% 0.15/6.04 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f10,axiom,(
% 0.15/6.04 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f15,axiom,(
% 0.15/6.04 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f17,axiom,(
% 0.15/6.04 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> ( sdtasdt0(W0,W1) = sz00=> ( W0 = sz00| W1 = sz00 ) ) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f19,definition,(
% 0.15/6.04 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2)& W2 != sz00 )=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f23,axiom,(
% 0.15/6.04 (! [W0,W1,W2,W3] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2)& W2 != sz00& aInteger0(W3)& W3 != sz00 )=> ( sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3))=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)& sdteqdtlpzmzozddtrp0(W0,W1,W3) ) ) ) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f34,definition,(
% 0.15/6.04 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1)& W1 != sz00 )=> (! [W2] :( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aInteger0(W3)& sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) )) ) )) )),
% 0.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f46,hypothesis,(
% 0.15/6.04 ( 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.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f47,hypothesis,(
% 0.15/6.04 ( (? [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.15/6.04 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.04 fof(f48,conjecture,(
% 0.15/6.05 ( sdtpldt0(sz10,xp) != sz10& sdtpldt0(sz10,smndt0(xp)) != sz10 ) ),
% 0.15/6.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/6.05 fof(f49,negated_conjecture,(
% 0.15/6.05 ~(( sdtpldt0(sz10,xp) != sz10& sdtpldt0(sz10,smndt0(xp)) != sz10 ) )),
% 0.15/6.05 inference(negated_conjecture,[status(cth)],[f48])).
% 0.15/6.05 fof(f53,plain,(
% 0.15/6.05 aInteger0(sz00)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/6.05 fof(f54,plain,(
% 0.15/6.05 aInteger0(sz10)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/6.05 fof(f55,plain,(
% 0.15/6.05 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.15/6.05 fof(f56,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f55])).
% 0.15/6.05 fof(f61,plain,(
% 0.15/6.05 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.15/6.05 fof(f62,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/6.05 fof(f63,plain,(
% 0.15/6.05 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.15/6.05 fof(f64,plain,(
% 0.15/6.05 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f63])).
% 0.15/6.05 fof(f65,plain,(
% 0.15/6.05 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.15/6.05 fof(f67,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f65])).
% 0.15/6.05 fof(f68,plain,(
% 0.15/6.05 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.15/6.05 fof(f69,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f68])).
% 0.15/6.05 fof(f81,plain,(
% 0.15/6.05 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.15/6.05 fof(f83,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sz00=sdtasdt0(sz00,X0))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f81])).
% 0.15/6.05 fof(f87,plain,(
% 0.15/6.05 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|(~sdtasdt0(W0,W1)=sz00|(W0=sz00|W1=sz00)))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.15/6.05 fof(f88,plain,(
% 0.15/6.05 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz00|X0=sz00|X1=sz00)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f87])).
% 0.15/6.05 fof(f98,plain,(
% 0.15/6.05 ![W0,W1,W2]: ((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|(sdteqdtlpzmzozddtrp0(W0,W1,W2)<=>aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1)))))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.15/6.05 fof(f99,plain,(
% 0.15/6.05 ![W0,W1,W2]: ((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|((~sdteqdtlpzmzozddtrp0(W0,W1,W2)|aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))))&(sdteqdtlpzmzozddtrp0(W0,W1,W2)|~aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))))))),
% 0.15/6.05 inference(NNF_transformation,[status(thm)],[f98])).
% 0.15/6.05 fof(f101,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|sdteqdtlpzmzozddtrp0(X0,X1,X2)|~aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f99])).
% 0.15/6.05 fof(f108,plain,(
% 0.15/6.05 ![W0,W1,W2,W3]: ((((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|~aInteger0(W3))|W3=sz00)|(~sdteqdtlpzmzozddtrp0(W0,W1,sdtasdt0(W2,W3))|(sdteqdtlpzmzozddtrp0(W0,W1,W2)&sdteqdtlpzmzozddtrp0(W0,W1,W3))))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.15/6.05 fof(f109,plain,(
% 0.15/6.05 ![X0,X1,X2,X3]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~aInteger0(X3)|X3=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,X3))|sdteqdtlpzmzozddtrp0(X0,X1,X2))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f108])).
% 0.15/6.05 fof(f110,plain,(
% 0.15/6.05 ![X0,X1,X2,X3]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~aInteger0(X3)|X3=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,X3))|sdteqdtlpzmzozddtrp0(X0,X1,X3))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f108])).
% 0.15/6.05 fof(f186,plain,(
% 0.15/6.05 ![W0,W1]: (((~aInteger0(W0)|~aInteger0(W1))|W1=sz00)|(![W2]: (W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aInteger0(W3)&sdteqdtlpzmzozddtrp0(W3,W0,W1))))))))),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.15/6.05 fof(f187,plain,(
% 0.15/6.05 ![W0,W1]: (((~aInteger0(W0)|~aInteger0(W1))|W1=sz00)|(![W2]: ((~W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aInteger0(W3)&sdteqdtlpzmzozddtrp0(W3,W0,W1)))&(aElementOf0(W3,W2)|(~aInteger0(W3)|~sdteqdtlpzmzozddtrp0(W3,W0,W1)))))))&(W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aInteger0(W3)|~sdteqdtlpzmzozddtrp0(W3,W0,W1)))&(aElementOf0(W3,W2)|(aInteger0(W3)&sdteqdtlpzmzozddtrp0(W3,W0,W1))))))))))),
% 0.15/6.05 inference(NNF_transformation,[status(thm)],[f186])).
% 0.15/6.05 fof(f188,plain,(
% 0.15/6.05 ![W0,W1]: (((~aInteger0(W0)|~aInteger0(W1))|W1=sz00)|((![W2]: (~W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aInteger0(W3)&sdteqdtlpzmzozddtrp0(W3,W0,W1))))&(![W3]: (aElementOf0(W3,W2)|(~aInteger0(W3)|~sdteqdtlpzmzozddtrp0(W3,W0,W1))))))))&(![W2]: (W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aInteger0(W3)|~sdteqdtlpzmzozddtrp0(W3,W0,W1)))&(aElementOf0(W3,W2)|(aInteger0(W3)&sdteqdtlpzmzozddtrp0(W3,W0,W1))))))))))),
% 0.15/6.05 inference(miniscoping,[status(thm)],[f187])).
% 0.15/6.05 fof(f189,plain,(
% 0.15/6.05 ![W0,W1]: (((~aInteger0(W0)|~aInteger0(W1))|W1=sz00)|((![W2]: (~W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aInteger0(W3)&sdteqdtlpzmzozddtrp0(W3,W0,W1))))&(![W3]: (aElementOf0(W3,W2)|(~aInteger0(W3)|~sdteqdtlpzmzozddtrp0(W3,W0,W1))))))))&(![W2]: (W2=szAzrzSzezqlpdtcmdtrp0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK10_skl(W2,W1,W0),W2)|(~aInteger0(sK10_skl(W2,W1,W0))|~sdteqdtlpzmzozddtrp0(sK10_skl(W2,W1,W0),W0,W1)))&(aElementOf0(sK10_skl(W2,W1,W0),W2)|(aInteger0(sK10_skl(W2,W1,W0))&sdteqdtlpzmzozddtrp0(sK10_skl(W2,W1,W0),W0,W1)))))))))),
% 0.15/6.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f188])).
% 0.15/6.05 fof(f190,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|~X2=szAzrzSzezqlpdtcmdtrp0(X0,X1)|aSet0(X2))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f189])).
% 0.15/6.05 fof(f191,plain,(
% 0.15/6.05 ![X0,X1,X2,X3]: (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|~X2=szAzrzSzezqlpdtcmdtrp0(X0,X1)|~aElementOf0(X3,X2)|aInteger0(X3))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f189])).
% 0.15/6.05 fof(f192,plain,(
% 0.15/6.05 ![X0,X1,X2,X3]: (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|~X2=szAzrzSzezqlpdtcmdtrp0(X0,X1)|~aElementOf0(X3,X2)|sdteqdtlpzmzozddtrp0(X3,X0,X1))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f189])).
% 0.15/6.05 fof(f317,plain,(
% 0.15/6.05 (((((((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.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.15/6.05 fof(f318,plain,(
% 0.15/6.05 (((((((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.15/6.05 inference(NNF_transformation,[status(thm)],[f317])).
% 0.15/6.05 fof(f319,plain,(
% 0.15/6.05 (((((((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.15/6.05 inference(miniscoping,[status(thm)],[f318])).
% 0.15/6.05 fof(f320,plain,(
% 0.15/6.05 (((((((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.15/6.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(W1,sK25_skl(W0)),skolemize(W1,sK26_skl(W0))],[f319])).
% 0.15/6.05 fof(f321,plain,(
% 0.15/6.05 aInteger0(xp)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f320])).
% 0.15/6.05 fof(f322,plain,(
% 0.15/6.05 ~xp=sz00),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f320])).
% 0.15/6.05 fof(f342,plain,(
% 0.15/6.05 (((((((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.15/6.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(W0,sK27_skl),skolemize(W0,sK28_skl)],[f47])).
% 0.15/6.05 fof(f343,plain,(
% 0.15/6.05 aInteger0(sK27_skl)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f342])).
% 0.15/6.05 fof(f344,plain,(
% 0.15/6.05 sdtasdt0(xp,sK27_skl)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f342])).
% 0.15/6.05 fof(f347,plain,(
% 0.15/6.05 aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f342])).
% 0.15/6.05 fof(f348,plain,(
% 0.15/6.05 aInteger0(sK28_skl)),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f342])).
% 0.15/6.05 fof(f352,plain,(
% 0.15/6.05 aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f342])).
% 0.15/6.05 fof(f353,plain,(
% 0.15/6.05 (sdtpldt0(sz10,xp)=sz10|sdtpldt0(sz10,smndt0(xp))=sz10)),
% 0.15/6.05 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.15/6.05 fof(f354,plain,(
% 0.15/6.05 sdtpldt0(sz10,xp)=sz10|sdtpldt0(sz10,smndt0(xp))=sz10),
% 0.15/6.05 inference(cnf_transformation,[status(thm)],[f353])).
% 0.15/6.05 fof(f397,definition,(
% 0.15/6.05 sQ8_spl <=> (sdtpldt0(sz10,xp)=sz10)),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f398,plain,(
% 0.15/6.05 sdtpldt0(sz10,xp)=sz10|~sQ8_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f397])).
% 0.15/6.05 fof(f399,plain,(
% 0.15/6.05 ~sdtpldt0(sz10,xp)=sz10|sQ8_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f397])).
% 0.15/6.05 fof(f400,definition,(
% 0.15/6.05 sQ9_spl <=> (sdtpldt0(sz10,smndt0(xp))=sz10)),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f401,plain,(
% 0.15/6.05 sdtpldt0(sz10,smndt0(xp))=sz10|~sQ9_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f400])).
% 0.15/6.05 fof(f403,plain,(
% 0.15/6.05 sQ8_spl|sQ9_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f354,f397,f400])).
% 0.15/6.05 fof(f425,plain,(
% 0.15/6.05 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)))),
% 0.15/6.05 inference(destructive_equality_resolution,[status(thm)],[f190])).
% 0.15/6.05 fof(f426,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))|aInteger0(X2))),
% 0.15/6.05 inference(destructive_equality_resolution,[status(thm)],[f191])).
% 0.15/6.05 fof(f427,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))|sdteqdtlpzmzozddtrp0(X2,X0,X1))),
% 0.15/6.05 inference(destructive_equality_resolution,[status(thm)],[f192])).
% 0.15/6.05 fof(f433,plain,(
% 0.15/6.05 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(sz10,X1))=sdtpldt0(sdtpldt0(X0,sz10),X1))),
% 0.15/6.05 inference(resolution,[status(thm)],[f62,f54])).
% 0.15/6.05 fof(f434,plain,(
% 0.15/6.05 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,sz10))=sdtpldt0(sdtpldt0(X0,X1),sz10))),
% 0.15/6.05 inference(resolution,[status(thm)],[f62,f54])).
% 0.15/6.05 fof(f436,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sz10,X0))),
% 0.15/6.05 inference(resolution,[status(thm)],[f64,f54])).
% 0.15/6.05 fof(f437,plain,(
% 0.15/6.05 aInteger0(smndt0(sz10))),
% 0.15/6.05 inference(resolution,[status(thm)],[f56,f54])).
% 0.15/6.05 fof(f440,plain,(
% 0.15/6.05 sz10=sdtpldt0(sz00,sz10)),
% 0.15/6.05 inference(resolution,[status(thm)],[f67,f54])).
% 0.15/6.05 fof(f454,plain,(
% 0.15/6.05 sdtpldt0(sz00,smndt0(sz00))=sz00),
% 0.15/6.05 inference(resolution,[status(thm)],[f69,f53])).
% 0.15/6.05 fof(f455,plain,(
% 0.15/6.05 sdtpldt0(sz10,smndt0(sz10))=sz00),
% 0.15/6.05 inference(resolution,[status(thm)],[f69,f54])).
% 0.15/6.05 fof(f456,plain,(
% 0.15/6.05 sdtpldt0(xp,smndt0(xp))=sz00),
% 0.15/6.05 inference(resolution,[status(thm)],[f321,f69])).
% 0.15/6.05 fof(f459,plain,(
% 0.15/6.05 xp=sdtpldt0(sz00,xp)),
% 0.15/6.05 inference(resolution,[status(thm)],[f321,f67])).
% 0.15/6.05 fof(f462,plain,(
% 0.15/6.05 aInteger0(smndt0(xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f321,f56])).
% 0.15/6.05 fof(f474,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(sz10,xp))=sdtpldt0(sdtpldt0(X0,sz10),xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f433,f321])).
% 0.15/6.05 fof(f477,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sdtpldt0(X0,sz10),xp)|~sQ8_spl)),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f398,f474])).
% 0.15/6.05 fof(f575,plain,(
% 0.15/6.05 sdtpldt0(xp,sz10)=sdtpldt0(sz10,xp)),
% 0.15/6.05 inference(resolution,[status(thm)],[f436,f321])).
% 0.15/6.05 fof(f579,plain,(
% 0.15/6.05 sdtpldt0(smndt0(sz10),sz10)=sdtpldt0(sz10,smndt0(sz10))),
% 0.15/6.05 inference(resolution,[status(thm)],[f437,f436])).
% 0.15/6.05 fof(f591,plain,(
% 0.15/6.05 sdtpldt0(smndt0(sz10),sz10)=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)|~sQ8_spl),
% 0.15/6.05 inference(resolution,[status(thm)],[f437,f477])).
% 0.15/6.05 fof(f602,plain,(
% 0.15/6.05 sdtpldt0(smndt0(sz10),smndt0(smndt0(sz10)))=sz00),
% 0.15/6.05 inference(resolution,[status(thm)],[f437,f69])).
% 0.15/6.05 fof(f605,plain,(
% 0.15/6.05 smndt0(sz10)=sdtpldt0(sz00,smndt0(sz10))),
% 0.15/6.05 inference(resolution,[status(thm)],[f437,f67])).
% 0.15/6.05 fof(f614,plain,(
% 0.15/6.05 sdtasdt0(xp,sK27_skl)=sdtpldt0(sz10,smndt0(sz10))|~sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f398,f344])).
% 0.15/6.05 fof(f659,plain,(
% 0.15/6.05 sz00=sdtasdt0(sz00,xp)),
% 0.15/6.05 inference(resolution,[status(thm)],[f83,f321])).
% 0.15/6.05 fof(f667,definition,(
% 0.15/6.05 sQ13_spl <=> (aInteger0(smndt0(sz10)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f669,plain,(
% 0.15/6.05 ~aInteger0(smndt0(sz10))|sQ13_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f667])).
% 0.15/6.05 fof(f670,definition,(
% 0.15/6.05 sQ14_spl <=> (aInteger0(sz10))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f672,plain,(
% 0.15/6.05 ~aInteger0(sz10)|sQ14_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f670])).
% 0.15/6.05 fof(f681,definition,(
% 0.15/6.05 sQ17_spl <=> (aInteger0(sz00))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f683,plain,(
% 0.15/6.05 ~aInteger0(sz00)|sQ17_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f681])).
% 0.15/6.05 fof(f687,definition,(
% 0.15/6.05 sQ19_spl <=> (sz00=sz00)),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f691,plain,(
% 0.15/6.05 sdtasdt0(xp,sK27_skl)=sz00|~sQ8_spl),
% 0.15/6.05 inference(backward_demodulation,[status(thm)],[f455,f614])).
% 0.15/6.05 fof(f692,plain,(
% 0.15/6.05 ~aInteger0(xp)|~aInteger0(sK27_skl)|xp=sz00|sK27_skl=sz00|~sQ8_spl),
% 0.15/6.05 inference(resolution,[status(thm)],[f691,f88])).
% 0.15/6.05 fof(f694,definition,(
% 0.15/6.05 sQ20_spl <=> (aInteger0(xp))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f696,plain,(
% 0.15/6.05 ~aInteger0(xp)|sQ20_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f694])).
% 0.15/6.05 fof(f697,definition,(
% 0.15/6.05 sQ21_spl <=> (aInteger0(sK27_skl))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f699,plain,(
% 0.15/6.05 ~aInteger0(sK27_skl)|sQ21_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f697])).
% 0.15/6.05 fof(f700,definition,(
% 0.15/6.05 sQ22_spl <=> (xp=sz00)),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f701,plain,(
% 0.15/6.05 xp=sz00|~sQ22_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f700])).
% 0.15/6.05 fof(f703,definition,(
% 0.15/6.05 sQ23_spl <=> (sK27_skl=sz00)),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f704,plain,(
% 0.15/6.05 sK27_skl=sz00|~sQ23_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f703])).
% 0.15/6.05 fof(f706,plain,(
% 0.15/6.05 ~sQ20_spl|~sQ21_spl|sQ22_spl|sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f692,f694,f697,f700,f703,f397])).
% 0.15/6.05 fof(f708,plain,(
% 0.15/6.05 $false|~sQ22_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f701,f322])).
% 0.15/6.05 fof(f709,plain,(
% 0.15/6.05 ~sQ22_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f708])).
% 0.15/6.05 fof(f710,plain,(
% 0.15/6.05 $false|sQ21_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f699,f343])).
% 0.15/6.05 fof(f711,plain,(
% 0.15/6.05 sQ21_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f710])).
% 0.15/6.05 fof(f712,plain,(
% 0.15/6.05 $false|sQ20_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f696,f321])).
% 0.15/6.05 fof(f713,plain,(
% 0.15/6.05 sQ20_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f712])).
% 0.15/6.05 fof(f725,plain,(
% 0.15/6.05 sdtpldt0(smndt0(xp),sz10)=sdtpldt0(sz10,smndt0(xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f462,f436])).
% 0.15/6.05 fof(f736,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(smndt0(xp),sz10))=sdtpldt0(sdtpldt0(X0,smndt0(xp)),sz10))),
% 0.15/6.05 inference(resolution,[status(thm)],[f462,f434])).
% 0.15/6.05 fof(f791,definition,(
% 0.15/6.05 sQ25_spl <=> (aInteger0(sK28_skl))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f793,plain,(
% 0.15/6.05 ~aInteger0(sK28_skl)|sQ25_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f791])).
% 0.15/6.05 fof(f799,plain,(
% 0.15/6.05 $false|sQ13_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f669,f437])).
% 0.15/6.05 fof(f800,plain,(
% 0.15/6.05 sQ13_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f799])).
% 0.15/6.05 fof(f820,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(xp)|~aInteger0(xp)|~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(xp,xp,X0)|~aDivisorOf0(X0,sz00))),
% 0.15/6.05 inference(paramodulation,[status(thm)],[f456,f101])).
% 0.15/6.05 fof(f821,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(sz10)|~aInteger0(sz10)|~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz10,sz10,X0)|~aDivisorOf0(X0,sz00))),
% 0.15/6.05 inference(paramodulation,[status(thm)],[f455,f101])).
% 0.15/6.05 fof(f822,definition,(
% 0.15/6.05 ![X0]: (sQ27_spl <=> (~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(xp,xp,X0)|~aDivisorOf0(X0,sz00)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f825,plain,(
% 0.15/6.05 ~sQ20_spl|sQ27_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f820,f694,f822])).
% 0.15/6.05 fof(f826,definition,(
% 0.15/6.05 ![X0]: (sQ28_spl <=> (~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz10,sz10,X0)|~aDivisorOf0(X0,sz00)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f829,plain,(
% 0.15/6.05 ~sQ14_spl|sQ28_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f821,f670,f826])).
% 0.15/6.05 fof(f830,plain,(
% 0.15/6.05 $false|sQ14_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f672,f54])).
% 0.15/6.05 fof(f831,plain,(
% 0.15/6.05 sQ14_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f830])).
% 0.15/6.05 fof(f837,plain,(
% 0.15/6.05 sdtasdt0(xp,sz00)=sz00|~sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f704,f691])).
% 0.15/6.05 fof(f842,plain,(
% 0.15/6.05 $false|sQ25_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f793,f348])).
% 0.15/6.05 fof(f843,plain,(
% 0.15/6.05 sQ25_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f842])).
% 0.15/6.05 fof(f857,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|xp=sz00|xp=sz00|~sdteqdtlpzmzozddtrp0(X0,xp,sdtasdt0(xp,xp))|sdteqdtlpzmzozddtrp0(X0,xp,xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f109,f321])).
% 0.15/6.05 fof(f869,plain,(
% 0.15/6.05 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|xp=sz00|xp=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(xp,xp))|sdteqdtlpzmzozddtrp0(X0,X1,xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f109,f321])).
% 0.15/6.05 fof(f870,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|xp=sz00|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(xp,X2))|sdteqdtlpzmzozddtrp0(X0,X1,xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f109,f321])).
% 0.15/6.05 fof(f878,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|xp=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,xp))|sdteqdtlpzmzozddtrp0(X0,X1,X2))),
% 0.15/6.05 inference(resolution,[status(thm)],[f109,f321])).
% 0.15/6.05 fof(f894,definition,(
% 0.15/6.05 ![X0]: (sQ32_spl <=> (~aInteger0(X0)|~sdteqdtlpzmzozddtrp0(X0,xp,sdtasdt0(xp,xp))|sdteqdtlpzmzozddtrp0(X0,xp,xp)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f897,plain,(
% 0.15/6.05 sQ32_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f857,f894,f700])).
% 0.15/6.05 fof(f930,definition,(
% 0.15/6.05 ![X0,X1]: (sQ41_spl <=> (~aInteger0(X0)|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(xp,xp))|sdteqdtlpzmzozddtrp0(X0,X1,xp)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f933,plain,(
% 0.15/6.05 sQ41_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f869,f930,f700])).
% 0.15/6.05 fof(f934,definition,(
% 0.15/6.05 ![X0,X1,X2]: (sQ42_spl <=> (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(xp,X2))|sdteqdtlpzmzozddtrp0(X0,X1,xp)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f937,plain,(
% 0.15/6.05 sQ42_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f870,f934,f700])).
% 0.15/6.05 fof(f966,definition,(
% 0.15/6.05 ![X0,X1,X2]: (sQ50_spl <=> (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,xp))|sdteqdtlpzmzozddtrp0(X0,X1,X2)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f969,plain,(
% 0.15/6.05 sQ50_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f878,f966,f700])).
% 0.15/6.05 fof(f998,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|xp=sz00|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(xp,X2))|sdteqdtlpzmzozddtrp0(X0,X1,X2))),
% 0.15/6.05 inference(resolution,[status(thm)],[f110,f321])).
% 0.15/6.05 fof(f1006,plain,(
% 0.15/6.05 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|xp=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,xp))|sdteqdtlpzmzozddtrp0(X0,X1,xp))),
% 0.15/6.05 inference(resolution,[status(thm)],[f110,f321])).
% 0.15/6.05 fof(f1032,definition,(
% 0.15/6.05 ![X0,X1,X2]: (sQ56_spl <=> (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(xp,X2))|sdteqdtlpzmzozddtrp0(X0,X1,X2)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f1035,plain,(
% 0.15/6.05 sQ56_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f998,f1032,f700])).
% 0.15/6.05 fof(f1058,definition,(
% 0.15/6.05 ![X0,X1,X2]: (sQ62_spl <=> (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,xp))|sdteqdtlpzmzozddtrp0(X0,X1,xp)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f1061,plain,(
% 0.15/6.05 sQ62_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f1006,f1058,f700])).
% 0.15/6.05 fof(f1152,plain,(
% 0.15/6.05 $false|sQ17_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f683,f53])).
% 0.15/6.05 fof(f1153,plain,(
% 0.15/6.05 sQ17_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f1152])).
% 0.15/6.05 fof(f1426,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(smndt0(sz10))|~aInteger0(smndt0(sz10))|~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(smndt0(sz10),smndt0(sz10),X0)|~aDivisorOf0(X0,sz00))),
% 0.15/6.05 inference(paramodulation,[status(thm)],[f602,f101])).
% 0.15/6.05 fof(f1427,definition,(
% 0.15/6.05 ![X0]: (sQ88_spl <=> (~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(smndt0(sz10),smndt0(sz10),X0)|~aDivisorOf0(X0,sz00)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f1430,plain,(
% 0.15/6.05 ~sQ13_spl|sQ88_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f1426,f667,f1427])).
% 0.15/6.05 fof(f1458,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(sz00)|~aInteger0(sz10)|~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz00,sz10,X0)|~aDivisorOf0(X0,smndt0(sz10)))),
% 0.15/6.05 inference(paramodulation,[status(thm)],[f605,f101])).
% 0.15/6.05 fof(f1459,definition,(
% 0.15/6.05 ![X0]: (sQ89_spl <=> (~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz00,sz10,X0)|~aDivisorOf0(X0,smndt0(sz10))))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f1462,plain,(
% 0.15/6.05 ~sQ17_spl|~sQ14_spl|sQ89_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f1458,f681,f670,f1459])).
% 0.15/6.05 fof(f1607,plain,(
% 0.15/6.05 sdtpldt0(sz10,smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)|~sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f579,f591])).
% 0.15/6.05 fof(f1608,plain,(
% 0.15/6.05 sdtpldt0(sz10,smndt0(sz10))=sdtpldt0(sdtpldt0(sz10,smndt0(sz10)),xp)|~sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f579,f1607])).
% 0.15/6.05 fof(f1720,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(sz00)|~aInteger0(sz00)|~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz00,sz00,X0)|~aDivisorOf0(X0,sz00))),
% 0.15/6.05 inference(paramodulation,[status(thm)],[f454,f101])).
% 0.15/6.05 fof(f1721,definition,(
% 0.15/6.05 ![X0]: (sQ103_spl <=> (~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz00,sz00,X0)|~aDivisorOf0(X0,sz00)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f1724,plain,(
% 0.15/6.05 ~sQ17_spl|sQ103_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f1720,f681,f1721])).
% 0.15/6.05 fof(f2000,plain,(
% 0.15/6.05 ~aInteger0(sz00)|~aInteger0(xp)|sz00=sz00|xp=sz00),
% 0.15/6.05 inference(resolution,[status(thm)],[f659,f88])).
% 0.15/6.05 fof(f2002,plain,(
% 0.15/6.05 ~sQ17_spl|~sQ20_spl|sQ19_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f2000,f681,f694,f687,f700])).
% 0.15/6.05 fof(f2023,plain,(
% 0.15/6.05 sdtasdt0(xp,sz00)=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))|~sQ23_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f704,f344])).
% 0.15/6.05 fof(f2024,plain,(
% 0.15/6.05 sz00=sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))|~sQ8_spl|~sQ23_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f837,f2023])).
% 0.15/6.05 fof(f2025,plain,(
% 0.15/6.05 sdtpldt0(sz10,smndt0(sz10))=sdtpldt0(sz00,xp)|~sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(backward_demodulation,[status(thm)],[f2030,f1608])).
% 0.15/6.05 fof(f2030,plain,(
% 0.15/6.05 sz00=sdtpldt0(sz10,smndt0(sz10))|~sQ8_spl|~sQ23_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f398,f2024])).
% 0.15/6.05 fof(f2032,plain,(
% 0.15/6.05 sz00=sdtpldt0(sz00,xp)|~sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f2030,f2025])).
% 0.15/6.05 fof(f2033,plain,(
% 0.15/6.05 sz00=xp|~sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f459,f2032])).
% 0.15/6.05 fof(f2034,plain,(
% 0.15/6.05 $false|~sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f2033,f322])).
% 0.15/6.05 fof(f2035,plain,(
% 0.15/6.05 ~sQ23_spl|~sQ8_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f2034])).
% 0.15/6.05 fof(f2041,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|xp=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(X0,xp)))),
% 0.15/6.05 inference(resolution,[status(thm)],[f425,f321])).
% 0.15/6.05 fof(f2052,definition,(
% 0.15/6.05 ![X0]: (sQ141_spl <=> (~aInteger0(X0)|aSet0(szAzrzSzezqlpdtcmdtrp0(X0,xp))))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f2055,plain,(
% 0.15/6.05 sQ141_spl|sQ22_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f2041,f2052,f700])).
% 0.15/6.05 fof(f2080,definition,(
% 0.15/6.05 sQ144_spl <=> (aInteger0(sdtpldt0(xp,sz10)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f2134,plain,(
% 0.15/6.05 aElementOf0(sdtpldt0(xp,sz10),szAzrzSzezqlpdtcmdtrp0(sz10,xp))),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f575,f347])).
% 0.15/6.05 fof(f2137,plain,(
% 0.15/6.05 ~sdtpldt0(xp,sz10)=sz10|sQ8_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f575,f399])).
% 0.15/6.05 fof(f2341,definition,(
% 0.15/6.05 sQ161_spl <=> (aInteger0(smndt0(xp)))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f2343,plain,(
% 0.15/6.05 ~aInteger0(smndt0(xp))|sQ161_spl),
% 0.15/6.05 inference(component_clause,[status(thm)],[f2341])).
% 0.15/6.05 fof(f2346,plain,(
% 0.15/6.05 $false|sQ161_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f2343,f462])).
% 0.15/6.05 fof(f2347,plain,(
% 0.15/6.05 sQ161_spl),
% 0.15/6.05 inference(contradiction_clause,[status(thm)],[f2346])).
% 0.15/6.05 fof(f2348,plain,(
% 0.15/6.05 ~aInteger0(sz10)|~aInteger0(xp)|xp=sz00|aInteger0(sdtpldt0(xp,sz10))),
% 0.15/6.05 inference(resolution,[status(thm)],[f426,f2134])).
% 0.15/6.05 fof(f2349,plain,(
% 0.15/6.05 ~aInteger0(sz10)|~aInteger0(xp)|xp=sz00|aInteger0(sdtpldt0(sz10,smndt0(xp)))),
% 0.15/6.05 inference(resolution,[status(thm)],[f426,f352])).
% 0.15/6.05 fof(f2350,plain,(
% 0.15/6.05 ~sQ14_spl|~sQ20_spl|sQ22_spl|sQ144_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f2348,f670,f694,f700,f2080])).
% 0.15/6.05 fof(f2351,definition,(
% 0.15/6.05 sQ162_spl <=> (aInteger0(sdtpldt0(sz10,smndt0(xp))))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f2354,plain,(
% 0.15/6.05 ~sQ14_spl|~sQ20_spl|sQ22_spl|sQ162_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f2349,f670,f694,f700,f2351])).
% 0.15/6.05 fof(f2364,plain,(
% 0.15/6.05 ~aInteger0(sz10)|~aInteger0(xp)|xp=sz00|sdteqdtlpzmzozddtrp0(sdtpldt0(xp,sz10),sz10,xp)),
% 0.15/6.05 inference(resolution,[status(thm)],[f427,f2134])).
% 0.15/6.05 fof(f2365,plain,(
% 0.15/6.05 ~aInteger0(sz10)|~aInteger0(xp)|xp=sz00|sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)),
% 0.15/6.05 inference(resolution,[status(thm)],[f427,f352])).
% 0.15/6.05 fof(f2366,definition,(
% 0.15/6.05 sQ163_spl <=> (sdteqdtlpzmzozddtrp0(sdtpldt0(xp,sz10),sz10,xp))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f2369,plain,(
% 0.15/6.05 ~sQ14_spl|~sQ20_spl|sQ22_spl|sQ163_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f2364,f670,f694,f700,f2366])).
% 0.15/6.05 fof(f2370,definition,(
% 0.15/6.05 sQ164_spl <=> (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp))),
% 0.15/6.05 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 0.15/6.05 fof(f2373,plain,(
% 0.15/6.05 ~sQ14_spl|~sQ20_spl|sQ22_spl|sQ164_spl),
% 0.15/6.05 inference(split_clause,[status(thm)],[f2365,f670,f694,f700,f2370])).
% 0.15/6.05 fof(f2388,plain,(
% 0.15/6.05 sdtpldt0(smndt0(xp),sz10)=sz10|~sQ9_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f401,f725])).
% 0.15/6.05 fof(f2404,plain,(
% 0.15/6.05 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sdtpldt0(X0,smndt0(xp)),sz10)|~sQ9_spl)),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f2388,f736])).
% 0.15/6.05 fof(f2407,plain,(
% 0.15/6.05 sdtpldt0(xp,sz10)=sdtpldt0(sdtpldt0(xp,smndt0(xp)),sz10)|~sQ9_spl),
% 0.15/6.05 inference(resolution,[status(thm)],[f2404,f321])).
% 0.15/6.05 fof(f2411,plain,(
% 0.15/6.05 sdtpldt0(xp,sz10)=sdtpldt0(sz00,sz10)|~sQ9_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f456,f2407])).
% 0.15/6.05 fof(f2412,plain,(
% 0.15/6.05 sdtpldt0(xp,sz10)=sz10|~sQ9_spl),
% 0.15/6.05 inference(forward_demodulation,[status(thm)],[f440,f2411])).
% 0.15/6.05 fof(f2413,plain,(
% 0.15/6.05 $false|sQ8_spl|~sQ9_spl),
% 0.15/6.05 inference(forward_subsumption_resolution,[status(thm)],[f2412,f2137])).
% 0.15/6.06 fof(f2414,plain,(
% 0.15/6.06 sQ8_spl|~sQ9_spl),
% 0.15/6.06 inference(contradiction_clause,[status(thm)],[f2413])).
% 0.15/6.06 fof(f2415,plain,(
% 0.15/6.06 $false),
% 0.15/6.06 inference(sat_refutation,[status(thm)],[f403,f706,f709,f711,f713,f800,f825,f829,f831,f843,f897,f933,f937,f969,f1035,f1061,f1153,f1430,f1462,f1724,f2002,f2035,f2055,f2347,f2350,f2354,f2369,f2373,f2414])).
% 0.15/6.06 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/6.06 % Elapsed time: 0.669500 seconds
% 0.15/6.06 % CPU time: 5.008705 seconds
% 0.15/6.06 % Total memory used: 176.971 MB
% 0.15/6.06 % Net memory used: 172.246 MB
%------------------------------------------------------------------------------