%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM448+5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:55 PM UTC 2026
% Result : Theorem 52.45s 7.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM448+5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n003.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 02:32:15 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 52.45/7.21 % Refutation found
% 52.45/7.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 52.45/7.21 % SZS output start CNFRefutation for theBenchmark
% 52.45/7.21 fof(f2,axiom,(
% 52.45/7.21 aInteger0(sz00) ),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f3,axiom,(
% 52.45/7.21 aInteger0(sz10) ),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f4,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f6,axiom,(
% 52.45/7.21 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtasdt0(W0,W1)) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f9,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f10,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f13,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f15,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f16,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0)& smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f17,axiom,(
% 52.45/7.21 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> ( sdtasdt0(W0,W1) = sz00=> ( W0 = sz00| W1 = sz00 ) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f18,definition,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> (! [W1] :( aDivisorOf0(W1,W0)<=> ( aInteger0(W1)& W1 != sz00& (? [W2] :( aInteger0(W2)& sdtasdt0(W1,W2) = W0 ) )) ) )) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f19,definition,(
% 52.45/7.21 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2)& W2 != sz00 )=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f22,axiom,(
% 52.45/7.21 (! [W0,W1,W2,W3] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2)& W2 != sz00& aInteger0(W3) )=> ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2)& sdteqdtlpzmzozddtrp0(W1,W3,W2) )=> sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f23,axiom,(
% 52.45/7.21 (! [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) ) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f25,axiom,(
% 52.45/7.21 (! [W0] :( aInteger0(W0)=> ( (? [W1] :( aDivisorOf0(W1,W0)& isPrime0(W1) ))<=> ( W0 != sz10& W0 != smndt0(sz10) ) ) ) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f28,definition,(
% 52.45/7.21 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f30,definition,(
% 52.45/7.21 (! [W0,W1] :( ( aSubsetOf0(W0,cS1395)& aSubsetOf0(W1,cS1395) )=> (! [W2] :( W2 = sdtbsmnsldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aInteger0(W3)& ( aElementOf0(W3,W0)| aElementOf0(W3,W1) ) ) ) )) ) )) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f31,definition,(
% 52.45/7.21 (! [W0,W1] :( ( aSubsetOf0(W0,cS1395)& aSubsetOf0(W1,cS1395) )=> (! [W2] :( W2 = sdtslmnbsdt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aInteger0(W3)& aElementOf0(W3,W0)& aElementOf0(W3,W1) ) ) )) ) )) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f33,definition,(
% 52.45/7.21 (! [W0] :( aSubsetOf0(W0,cS1395)=> (! [W1] :( W1 = stldt0(W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)<=> ( aInteger0(W2)& ~ aElementOf0(W2,W0) ) ) )) ) )) )),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f42,hypothesis,(
% 52.45/7.21 ( aSet0(xS)& (! [W0] :( ( aElementOf0(W0,xS)=> (? [W1] :( aInteger0(W1)& W1 != sz00& isPrime0(W1)& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))& (! [W2] :( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))=> ( aInteger0(W2)& (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ))& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))& sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) )& ( ( aInteger0(W2)& ( (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ))| aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))| sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) )=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ))& szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ))& ( (? [W1] :( aInteger0(W1)& W1 != sz00& isPrime0(W1)& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))& (! [W2] :( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))=> ( aInteger0(W2)& (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ))& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))& sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) )& ( ( aInteger0(W2)& ( (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00)) ))| aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))| sdteqdtlpzmzozddtrp0(W2,sz00,W1) ) )=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) ) ))=> szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 ) ))=> aElementOf0(W0,xS) ) ))& xS = cS2043 ) ),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f43,conjecture,(
% 52.45/7.21 ( (! [W0] :( aInteger0(W0)=> ( ( ( (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ))| aElementOf0(W0,sbsmnsldt0(xS)) )=> (? [W1] :( aInteger0(W1)& W1 != sz00& (? [W2] :( aInteger0(W2)& sdtasdt0(W1,W2) = W0 ))& aDivisorOf0(W1,W0)& isPrime0(W1) ) ))& ( (? [W1] :( ( ( aInteger0(W1)& W1 != sz00& (? [W2] :( aInteger0(W2)& sdtasdt0(W1,W2) = W0 ) ))| aDivisorOf0(W1,W0) )& isPrime0(W1) ))=> ( (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ))& aElementOf0(W0,sbsmnsldt0(xS)) ) ) ) ))=> ( ( aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ) ))=> ( ( aSet0(stldt0(sbsmnsldt0(xS)))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( W0 = sz10| W0 = smndt0(sz10) ) ))| stldt0(sbsmnsldt0(xS)) = cS2076 ) ) ) ) ),
% 52.45/7.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.45/7.21 fof(f44,negated_conjecture,(
% 52.45/7.21 ~(( (! [W0] :( aInteger0(W0)=> ( ( ( (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ))| aElementOf0(W0,sbsmnsldt0(xS)) )=> (? [W1] :( aInteger0(W1)& W1 != sz00& (? [W2] :( aInteger0(W2)& sdtasdt0(W1,W2) = W0 ))& aDivisorOf0(W1,W0)& isPrime0(W1) ) ))& ( (? [W1] :( ( ( aInteger0(W1)& W1 != sz00& (? [W2] :( aInteger0(W2)& sdtasdt0(W1,W2) = W0 ) ))| aDivisorOf0(W1,W0) )& isPrime0(W1) ))=> ( (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ))& aElementOf0(W0,sbsmnsldt0(xS)) ) ) ) ))=> ( ( aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ) ))=> ( ( aSet0(stldt0(sbsmnsldt0(xS)))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ) ))=> ( (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( W0 = sz10| W0 = smndt0(sz10) ) ))| stldt0(sbsmnsldt0(xS)) = cS2076 ) ) ) ) )),
% 52.45/7.21 inference(negated_conjecture,[status(cth)],[f43])).
% 52.45/7.21 fof(f48,plain,(
% 52.45/7.21 aInteger0(sz00)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f2])).
% 52.45/7.21 fof(f49,plain,(
% 52.45/7.21 aInteger0(sz10)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f3])).
% 52.45/7.21 fof(f50,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 52.45/7.21 fof(f51,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f50])).
% 52.45/7.21 fof(f54,plain,(
% 52.45/7.21 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtasdt0(W0,W1)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 52.45/7.21 fof(f55,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtasdt0(X0,X1)))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f54])).
% 52.45/7.21 fof(f60,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 52.45/7.21 fof(f61,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=X0)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f60])).
% 52.45/7.21 fof(f62,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f60])).
% 52.45/7.21 fof(f63,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 52.45/7.21 fof(f64,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f63])).
% 52.45/7.21 fof(f65,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f63])).
% 52.45/7.21 fof(f70,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 52.45/7.21 fof(f71,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=X0)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f70])).
% 52.45/7.21 fof(f72,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|X0=sdtasdt0(sz10,X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f70])).
% 52.45/7.21 fof(f76,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 52.45/7.21 fof(f77,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f76])).
% 52.45/7.21 fof(f78,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sz00=sdtasdt0(sz00,X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f76])).
% 52.45/7.21 fof(f79,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(sdtasdt0(smndt0(sz10),W0)=smndt0(W0)&smndt0(W0)=sdtasdt0(W0,smndt0(sz10))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 52.45/7.21 fof(f80,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|sdtasdt0(smndt0(sz10),X0)=smndt0(X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f79])).
% 52.45/7.21 fof(f82,plain,(
% 52.45/7.21 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|(~sdtasdt0(W0,W1)=sz00|(W0=sz00|W1=sz00)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 52.45/7.21 fof(f83,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz00|X0=sz00|X1=sz00)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f82])).
% 52.45/7.21 fof(f84,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(![W1]: (aDivisorOf0(W1,W0)<=>((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0))))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 52.45/7.21 fof(f85,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(![W1]: ((~aDivisorOf0(W1,W0)|((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0))))&(aDivisorOf0(W1,W0)|((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))))))),
% 52.45/7.21 inference(NNF_transformation,[status(thm)],[f84])).
% 52.45/7.21 fof(f86,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|((![W1]: (~aDivisorOf0(W1,W0)|((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))))&(![W1]: (aDivisorOf0(W1,W0)|((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))))))),
% 52.45/7.21 inference(miniscoping,[status(thm)],[f85])).
% 52.45/7.21 fof(f87,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|((![W1]: (~aDivisorOf0(W1,W0)|((aInteger0(W1)&~W1=sz00)&(aInteger0(sK0_skl(W1,W0))&sdtasdt0(W1,sK0_skl(W1,W0))=W0))))&(![W1]: (aDivisorOf0(W1,W0)|((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))))))),
% 52.45/7.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f86])).
% 52.45/7.21 fof(f88,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|aInteger0(X1))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f87])).
% 52.45/7.21 fof(f89,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|~X1=sz00)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f87])).
% 52.45/7.21 fof(f90,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|aInteger0(sK0_skl(X1,X0)))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f87])).
% 52.45/7.21 fof(f91,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|sdtasdt0(X1,sK0_skl(X1,X0))=X0)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f87])).
% 52.45/7.21 fof(f92,plain,(
% 52.45/7.21 ![X0,X1,X2]: (~aInteger0(X0)|aDivisorOf0(X1,X0)|~aInteger0(X1)|X1=sz00|~aInteger0(X2)|~sdtasdt0(X1,X2)=X0)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f87])).
% 52.45/7.21 fof(f93,plain,(
% 52.45/7.21 ![W0,W1,W2]: ((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|(sdteqdtlpzmzozddtrp0(W0,W1,W2)<=>aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1)))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 52.45/7.21 fof(f94,plain,(
% 52.45/7.21 ![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))))))),
% 52.45/7.21 inference(NNF_transformation,[status(thm)],[f93])).
% 52.45/7.21 fof(f96,plain,(
% 52.45/7.21 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|sdteqdtlpzmzozddtrp0(X0,X1,X2)|~aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f94])).
% 52.45/7.21 fof(f101,plain,(
% 52.45/7.21 ![W0,W1,W2,W3]: (((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|~aInteger0(W3))|((~sdteqdtlpzmzozddtrp0(W0,W1,W2)|~sdteqdtlpzmzozddtrp0(W1,W3,W2))|sdteqdtlpzmzozddtrp0(W0,W3,W2)))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 52.45/7.21 fof(f102,plain,(
% 52.45/7.21 ![X0,X1,X2,X3]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~aInteger0(X3)|~sdteqdtlpzmzozddtrp0(X0,X1,X2)|~sdteqdtlpzmzozddtrp0(X1,X3,X2)|sdteqdtlpzmzozddtrp0(X0,X3,X2))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f101])).
% 52.45/7.21 fof(f103,plain,(
% 52.45/7.21 ![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))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 52.45/7.21 fof(f104,plain,(
% 52.45/7.21 ![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))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f103])).
% 52.45/7.21 fof(f108,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|((?[W1]: (aDivisorOf0(W1,W0)&isPrime0(W1)))<=>(~W0=sz10&~W0=smndt0(sz10))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 52.45/7.21 fof(f109,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(((![W1]: (~aDivisorOf0(W1,W0)|~isPrime0(W1)))|(~W0=sz10&~W0=smndt0(sz10)))&((?[W1]: (aDivisorOf0(W1,W0)&isPrime0(W1)))|(W0=sz10|W0=smndt0(sz10)))))),
% 52.45/7.21 inference(NNF_transformation,[status(thm)],[f108])).
% 52.45/7.21 fof(f110,plain,(
% 52.45/7.21 ![W0]: (~aInteger0(W0)|(((![W1]: (~aDivisorOf0(W1,W0)|~isPrime0(W1)))|(~W0=sz10&~W0=smndt0(sz10)))&((aDivisorOf0(sK1_skl(W0),W0)&isPrime0(sK1_skl(W0)))|(W0=sz10|W0=smndt0(sz10)))))),
% 52.45/7.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W1,sK1_skl(W0))],[f109])).
% 52.45/7.21 fof(f111,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|~isPrime0(X1)|~X0=sz10)),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f110])).
% 52.45/7.21 fof(f112,plain,(
% 52.45/7.21 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|~isPrime0(X1)|~X0=smndt0(sz10))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f110])).
% 52.45/7.21 fof(f113,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|aDivisorOf0(sK1_skl(X0),X0)|X0=sz10|X0=smndt0(sz10))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f110])).
% 52.45/7.21 fof(f114,plain,(
% 52.45/7.21 ![X0]: (~aInteger0(X0)|isPrime0(sK1_skl(X0))|X0=sz10|X0=smndt0(sz10))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f110])).
% 52.45/7.21 fof(f121,plain,(
% 52.45/7.21 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 52.45/7.21 fof(f122,plain,(
% 52.45/7.21 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 52.45/7.21 inference(NNF_transformation,[status(thm)],[f121])).
% 52.45/7.21 fof(f123,plain,(
% 52.45/7.21 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 52.45/7.21 inference(miniscoping,[status(thm)],[f122])).
% 52.45/7.21 fof(f124,plain,(
% 52.45/7.21 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK2_skl(W1,W0),W1)&~aElementOf0(sK2_skl(W1,W0),W0)))))))),
% 52.45/7.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W2,sK2_skl(W1,W0))],[f123])).
% 52.45/7.21 fof(f128,plain,(
% 52.45/7.21 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|~aElementOf0(sK2_skl(X1,X0),X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f124])).
% 52.45/7.21 fof(f131,plain,(
% 52.45/7.21 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|(![W2]: (W2=sdtbsmnsldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))))))),
% 52.45/7.21 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 52.45/7.21 fof(f132,plain,(
% 52.45/7.21 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|(![W2]: ((~W2=sdtbsmnsldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1))))&(aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1))))))))&(W2=sdtbsmnsldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1))))&(aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))))))))),
% 52.45/7.21 inference(NNF_transformation,[status(thm)],[f131])).
% 52.45/7.21 fof(f133,plain,(
% 52.45/7.21 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|((![W2]: (~W2=sdtbsmnsldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))&(![W3]: (aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1)))))))))&(![W2]: (W2=sdtbsmnsldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1))))&(aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))))))))),
% 52.45/7.21 inference(miniscoping,[status(thm)],[f132])).
% 52.45/7.21 fof(f134,plain,(
% 52.45/7.21 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|((![W2]: (~W2=sdtbsmnsldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aInteger0(W3)&(aElementOf0(W3,W0)|aElementOf0(W3,W1)))))&(![W3]: (aElementOf0(W3,W2)|(~aInteger0(W3)|(~aElementOf0(W3,W0)&~aElementOf0(W3,W1)))))))))&(![W2]: (W2=sdtbsmnsldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK3_skl(W2,W1,W0),W2)|(~aInteger0(sK3_skl(W2,W1,W0))|(~aElementOf0(sK3_skl(W2,W1,W0),W0)&~aElementOf0(sK3_skl(W2,W1,W0),W1))))&(aElementOf0(sK3_skl(W2,W1,W0),W2)|(aInteger0(sK3_skl(W2,W1,W0))&(aElementOf0(sK3_skl(W2,W1,W0),W0)|aElementOf0(sK3_skl(W2,W1,W0),W1))))))))))),
% 52.45/7.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f133])).
% 52.45/7.21 fof(f140,plain,(
% 52.45/7.21 ![X0,X1,X2]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|X2=sdtbsmnsldt0(X0,X1)|~aSet0(X2)|~aElementOf0(sK3_skl(X2,X1,X0),X2)|~aInteger0(sK3_skl(X2,X1,X0))|~aElementOf0(sK3_skl(X2,X1,X0),X0))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f134])).
% 52.45/7.21 fof(f141,plain,(
% 52.45/7.21 ![X0,X1,X2]: (~aSubsetOf0(X0,cS1395)|~aSubsetOf0(X1,cS1395)|X2=sdtbsmnsldt0(X0,X1)|~aSet0(X2)|~aElementOf0(sK3_skl(X2,X1,X0),X2)|~aInteger0(sK3_skl(X2,X1,X0))|~aElementOf0(sK3_skl(X2,X1,X0),X1))),
% 52.45/7.21 inference(cnf_transformation,[status(thm)],[f134])).
% 52.45/7.21 fof(f144,plain,(
% 52.45/7.21 ![W0,W1]: ((~aSubsetOf0(W0,cS1395)|~aSubsetOf0(W1,cS1395))|(![W2]: (W2=sdtslmnbsdt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aInteger0(W3)&aElementOf0(W3,W0))&aElementOf0(W3,W1))))))))),
% 52.45/7.22 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 52.45/7.22 fof(f145,definition,(
% 52.45/7.22 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aInteger0(W3)&aElementOf0(W3,W0))&aElementOf0(W3,W1)))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 52.45/7.22 fof(f170,plain,(
% 52.45/7.22 ![W0]: (~aSubsetOf0(W0,cS1395)|(![W1]: (W1=stldt0(W0)<=>(aSet0(W1)&(![W2]: (aElementOf0(W2,W1)<=>(aInteger0(W2)&~aElementOf0(W2,W0))))))))),
% 52.45/7.22 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 52.45/7.22 fof(f171,plain,(
% 52.45/7.22 ![W0]: (~aSubsetOf0(W0,cS1395)|(![W1]: ((~W1=stldt0(W0)|(aSet0(W1)&(![W2]: ((~aElementOf0(W2,W1)|(aInteger0(W2)&~aElementOf0(W2,W0)))&(aElementOf0(W2,W1)|(~aInteger0(W2)|aElementOf0(W2,W0)))))))&(W1=stldt0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(~aInteger0(W2)|aElementOf0(W2,W0)))&(aElementOf0(W2,W1)|(aInteger0(W2)&~aElementOf0(W2,W0))))))))))),
% 52.45/7.22 inference(NNF_transformation,[status(thm)],[f170])).
% 52.45/7.22 fof(f172,plain,(
% 52.45/7.22 ![W0]: (~aSubsetOf0(W0,cS1395)|((![W1]: (~W1=stldt0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(aInteger0(W2)&~aElementOf0(W2,W0))))&(![W2]: (aElementOf0(W2,W1)|(~aInteger0(W2)|aElementOf0(W2,W0))))))))&(![W1]: (W1=stldt0(W0)|(~aSet0(W1)|(?[W2]: ((~aElementOf0(W2,W1)|(~aInteger0(W2)|aElementOf0(W2,W0)))&(aElementOf0(W2,W1)|(aInteger0(W2)&~aElementOf0(W2,W0))))))))))),
% 52.45/7.22 inference(miniscoping,[status(thm)],[f171])).
% 52.45/7.22 fof(f173,plain,(
% 52.45/7.22 ![W0]: (~aSubsetOf0(W0,cS1395)|((![W1]: (~W1=stldt0(W0)|(aSet0(W1)&((![W2]: (~aElementOf0(W2,W1)|(aInteger0(W2)&~aElementOf0(W2,W0))))&(![W2]: (aElementOf0(W2,W1)|(~aInteger0(W2)|aElementOf0(W2,W0))))))))&(![W1]: (W1=stldt0(W0)|(~aSet0(W1)|((~aElementOf0(sK9_skl(W1,W0),W1)|(~aInteger0(sK9_skl(W1,W0))|aElementOf0(sK9_skl(W1,W0),W0)))&(aElementOf0(sK9_skl(W1,W0),W1)|(aInteger0(sK9_skl(W1,W0))&~aElementOf0(sK9_skl(W1,W0),W0)))))))))),
% 52.45/7.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W2,sK9_skl(W1,W0))],[f172])).
% 52.45/7.22 fof(f178,plain,(
% 52.45/7.22 ![X0,X1]: (~aSubsetOf0(X0,cS1395)|X1=stldt0(X0)|~aSet0(X1)|~aElementOf0(sK9_skl(X1,X0),X1)|~aInteger0(sK9_skl(X1,X0))|aElementOf0(sK9_skl(X1,X0),X0))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f173])).
% 52.45/7.22 fof(f219,plain,(
% 52.45/7.22 (aSet0(xS)&(![W0]: ((~aElementOf0(W0,xS)|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&isPrime0(W1))&aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(W2,sz00,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&~sdteqdtlpzmzozddtrp0(W2,sz00,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))))))&szAzrzSzezqlpdtcmdtrp0(sz00,W1)=W0)))&((![W1]: (((~aInteger0(W1)|W1=sz00)|~isPrime0(W1))|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(W2,sz00,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&~sdteqdtlpzmzozddtrp0(W2,sz00,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))))))&~szAzrzSzezqlpdtcmdtrp0(sz00,W1)=W0)))|aElementOf0(W0,xS)))))&xS=cS2043),
% 52.45/7.22 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 52.45/7.22 fof(f220,plain,(
% 52.45/7.22 (aSet0(xS)&((![W0]: (~aElementOf0(W0,xS)|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&isPrime0(W1))&aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(W2,sz00,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&~sdteqdtlpzmzozddtrp0(W2,sz00,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))))))&szAzrzSzezqlpdtcmdtrp0(sz00,W1)=W0))))&(![W0]: ((![W1]: (((~aInteger0(W1)|W1=sz00)|~isPrime0(W1))|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(W2,sz00,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&~sdteqdtlpzmzozddtrp0(W2,sz00,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))))))&~szAzrzSzezqlpdtcmdtrp0(sz00,W1)=W0)))|aElementOf0(W0,xS)))))&xS=cS2043),
% 52.45/7.22 inference(miniscoping,[status(thm)],[f219])).
% 52.45/7.22 fof(f221,plain,(
% 52.45/7.22 (aSet0(xS)&((![W0]: (~aElementOf0(W0,xS)|(((((aInteger0(sK15_skl(W0))&~sK15_skl(W0)=sz00)&isPrime0(sK15_skl(W0)))&aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK16_skl(W2,W0))&sdtasdt0(sK15_skl(W0),sK16_skl(W2,W0))=sdtpldt0(W2,smndt0(sz00))))&aDivisorOf0(sK15_skl(W0),sdtpldt0(W2,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(W2,sz00,sK15_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK15_skl(W0),W3)=sdtpldt0(W2,smndt0(sz00))))&~aDivisorOf0(sK15_skl(W0),sdtpldt0(W2,smndt0(sz00))))&~sdteqdtlpzmzozddtrp0(W2,sz00,sK15_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0)))))))&szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0))=W0)))&(![W0]: ((![W1]: (((~aInteger0(W1)|W1=sz00)|~isPrime0(W1))|((aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))|(((aInteger0(W2)&(aInteger0(sK17_skl(W2,W1,W0))&sdtasdt0(W1,sK17_skl(W2,W1,W0))=sdtpldt0(W2,smndt0(sz00))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&sdteqdtlpzmzozddtrp0(W2,sz00,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(sz00))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00))))&~sdteqdtlpzmzozddtrp0(W2,sz00,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))))))&~szAzrzSzezqlpdtcmdtrp0(sz00,W1)=W0)))|aElementOf0(W0,xS)))))&xS=cS2043),
% 52.45/7.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(W1,sK15_skl(W0)),skolemize(W3,sK16_skl(W2,W0)),skolemize(W3,sK17_skl(W2,W1,W0))],[f220])).
% 52.45/7.22 fof(f222,plain,(
% 52.45/7.22 aSet0(xS)),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f223,plain,(
% 52.45/7.22 ![X0]: (~aElementOf0(X0,xS)|aInteger0(sK15_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f224,plain,(
% 52.45/7.22 ![X0]: (~aElementOf0(X0,xS)|~sK15_skl(X0)=sz00)),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f225,plain,(
% 52.45/7.22 ![X0]: (~aElementOf0(X0,xS)|isPrime0(sK15_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f233,plain,(
% 52.45/7.22 ![X0,X1]: (~aElementOf0(X0,xS)|~aInteger0(X1)|~aDivisorOf0(sK15_skl(X0),sdtpldt0(X1,smndt0(sz00)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0))))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f234,plain,(
% 52.45/7.22 ![X0,X1]: (~aElementOf0(X0,xS)|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X1,sz00,sK15_skl(X0))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0))))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f236,plain,(
% 52.45/7.22 ![X0,X1]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aElementOf0(X1,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f237,plain,(
% 52.45/7.22 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aInteger0(X1)|aElementOf0(X2,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f240,plain,(
% 52.45/7.22 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))|aElementOf0(X2,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f241,plain,(
% 52.45/7.22 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|sdteqdtlpzmzozddtrp0(X1,sz00,X0)|aElementOf0(X2,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f242,plain,(
% 52.45/7.22 ![X0,X1,X2,X3]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aInteger0(X2)|~sdtasdt0(X0,X2)=sdtpldt0(X1,smndt0(sz00))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aElementOf0(X3,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f243,plain,(
% 52.45/7.22 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aElementOf0(X2,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f244,plain,(
% 52.45/7.22 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X1,sz00,X0)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aElementOf0(X2,xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f221])).
% 52.45/7.22 fof(f247,plain,(
% 52.45/7.22 ((![W0]: (~aInteger0(W0)|((((![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1)))&~aElementOf0(W0,sbsmnsldt0(xS)))|(?[W1]: ((((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))&aDivisorOf0(W1,W0))&isPrime0(W1))))&((![W1]: ((((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))&~aDivisorOf0(W1,W0))|~isPrime0(W1)))|((?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))&aElementOf0(W0,sbsmnsldt0(xS)))))))&((aSet0(sbsmnsldt0(xS))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&((aSet0(stldt0(sbsmnsldt0(xS)))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&((?[W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<~>(W0=sz10|W0=smndt0(sz10))))&~stldt0(sbsmnsldt0(xS))=cS2076))))),
% 52.45/7.22 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 52.45/7.22 fof(f248,definition,(
% 52.45/7.22 ![W0]: (sP2_prd(W0)<=>((![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1)))&~aElementOf0(W0,sbsmnsldt0(xS))))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 52.45/7.22 fof(f249,definition,(
% 52.45/7.22 ![W0,W1]: (sP3_prd(W1,W0)<=>((((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))&~aDivisorOf0(W1,W0))|~isPrime0(W1)))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 52.45/7.22 fof(f250,plain,(
% 52.45/7.22 (![W0]: (~aInteger0(W0)|((sP2_prd(W0)|(?[W1]: ((((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))&aDivisorOf0(W1,W0))&isPrime0(W1))))&((![W1]: sP3_prd(W1,W0))|((?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))&aElementOf0(W0,sbsmnsldt0(xS)))))))&((aSet0(sbsmnsldt0(xS))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&((aSet0(stldt0(sbsmnsldt0(xS)))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&((?[W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<~>(W0=sz10|W0=smndt0(sz10))))&~stldt0(sbsmnsldt0(xS))=cS2076)))),
% 52.45/7.22 inference(formula_renaming,[status(thm)],[f247,f249,f248])).
% 52.45/7.22 fof(f251,plain,(
% 52.45/7.22 (![W0]: (~aInteger0(W0)|((sP2_prd(W0)|(?[W1]: ((((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))&aDivisorOf0(W1,W0))&isPrime0(W1))))&((![W1]: sP3_prd(W1,W0))|((?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))&aElementOf0(W0,sbsmnsldt0(xS)))))))&((aSet0(sbsmnsldt0(xS))&(![W0]: ((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&(aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((aSet0(stldt0(sbsmnsldt0(xS)))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&((?[W0]: ((aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10)))&(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10)))))&~stldt0(sbsmnsldt0(xS))=cS2076)))),
% 52.45/7.22 inference(NNF_transformation,[status(thm)],[f250])).
% 52.45/7.22 fof(f252,plain,(
% 52.45/7.22 (![W0]: (~aInteger0(W0)|((sP2_prd(W0)|(?[W1]: ((((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))&aDivisorOf0(W1,W0))&isPrime0(W1))))&((![W1]: sP3_prd(W1,W0))|((?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))&aElementOf0(W0,sbsmnsldt0(xS)))))))&((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((aSet0(stldt0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&((?[W0]: ((aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10)))&(~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10)))))&~stldt0(sbsmnsldt0(xS))=cS2076)))),
% 52.45/7.22 inference(miniscoping,[status(thm)],[f251])).
% 52.45/7.22 fof(f253,plain,(
% 52.45/7.22 (![W0]: (~aInteger0(W0)|((sP2_prd(W0)|((((aInteger0(sK18_skl(W0))&~sK18_skl(W0)=sz00)&(aInteger0(sK19_skl(W0))&sdtasdt0(sK18_skl(W0),sK19_skl(W0))=W0))&aDivisorOf0(sK18_skl(W0),W0))&isPrime0(sK18_skl(W0))))&((![W1]: sP3_prd(W1,W0))|((aElementOf0(sK20_skl(W0),xS)&aElementOf0(W0,sK20_skl(W0)))&aElementOf0(W0,sbsmnsldt0(xS)))))))&((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK21_skl(W0),xS)&aElementOf0(W0,sK21_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((aSet0(stldt0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(((aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|(sK22_skl=sz10|sK22_skl=smndt0(sz10)))&(~aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|(~sK22_skl=sz10&~sK22_skl=smndt0(sz10))))&~stldt0(sbsmnsldt0(xS))=cS2076)))),
% 52.45/7.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl]),skolemize(W1,sK18_skl(W0)),skolemize(W2,sK19_skl(W0)),skolemize(W1,sK20_skl(W0)),skolemize(W1,sK21_skl(W0)),skolemize(W0,sK22_skl)],[f252])).
% 52.45/7.22 fof(f254,plain,(
% 52.45/7.22 ![X0]: (~aInteger0(X0)|sP2_prd(X0)|aInteger0(sK18_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f256,plain,(
% 52.45/7.22 ![X0]: (~aInteger0(X0)|sP2_prd(X0)|aInteger0(sK19_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f257,plain,(
% 52.45/7.22 ![X0]: (~aInteger0(X0)|sP2_prd(X0)|sdtasdt0(sK18_skl(X0),sK19_skl(X0))=X0)),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f258,plain,(
% 52.45/7.22 ![X0]: (~aInteger0(X0)|sP2_prd(X0)|aDivisorOf0(sK18_skl(X0),X0))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f259,plain,(
% 52.45/7.22 ![X0]: (~aInteger0(X0)|sP2_prd(X0)|isPrime0(sK18_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f260,plain,(
% 52.45/7.22 ![X0,X1]: (~aInteger0(X0)|sP3_prd(X1,X0)|aElementOf0(sK20_skl(X0),xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f261,plain,(
% 52.45/7.22 ![X0,X1]: (~aInteger0(X0)|sP3_prd(X1,X0)|aElementOf0(X0,sK20_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f262,plain,(
% 52.45/7.22 ![X0,X1]: (~aInteger0(X0)|sP3_prd(X1,X0)|aElementOf0(X0,sbsmnsldt0(xS)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f263,plain,(
% 52.45/7.22 aSet0(sbsmnsldt0(xS))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f266,plain,(
% 52.45/7.22 ![X0]: (~aElementOf0(X0,sbsmnsldt0(xS))|aElementOf0(X0,sK21_skl(X0)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f268,plain,(
% 52.45/7.22 aSet0(stldt0(sbsmnsldt0(xS)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f269,plain,(
% 52.45/7.22 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|aInteger0(X0))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f270,plain,(
% 52.45/7.22 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|~aElementOf0(X0,sbsmnsldt0(xS)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f271,plain,(
% 52.45/7.22 ![X0]: (aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|~aInteger0(X0)|aElementOf0(X0,sbsmnsldt0(xS)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f272,plain,(
% 52.45/7.22 aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|sK22_skl=sz10|sK22_skl=smndt0(sz10)),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f273,plain,(
% 52.45/7.22 ~aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|~sK22_skl=sz10),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f274,plain,(
% 52.45/7.22 ~aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|~sK22_skl=smndt0(sz10)),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f253])).
% 52.45/7.22 fof(f276,plain,(
% 52.45/7.22 ![W0,W1,W3]: ((~sP0_prd(W3,W1,W0)|((aInteger0(W3)&aElementOf0(W3,W0))&aElementOf0(W3,W1)))&(sP0_prd(W3,W1,W0)|((~aInteger0(W3)|~aElementOf0(W3,W0))|~aElementOf0(W3,W1))))),
% 52.45/7.22 inference(NNF_transformation,[status(thm)],[f145])).
% 52.45/7.22 fof(f277,plain,(
% 52.45/7.22 (![W0,W1,W3]: (~sP0_prd(W3,W1,W0)|((aInteger0(W3)&aElementOf0(W3,W0))&aElementOf0(W3,W1))))&(![W0,W1,W3]: (sP0_prd(W3,W1,W0)|((~aInteger0(W3)|~aElementOf0(W3,W0))|~aElementOf0(W3,W1))))),
% 52.45/7.22 inference(miniscoping,[status(thm)],[f276])).
% 52.45/7.22 fof(f281,plain,(
% 52.45/7.22 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~aInteger0(X0)|~aElementOf0(X0,X2)|~aElementOf0(X0,X1))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f277])).
% 52.45/7.22 fof(f287,plain,(
% 52.45/7.22 ![W0]: ((~sP2_prd(W0)|((![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1)))&~aElementOf0(W0,sbsmnsldt0(xS))))&(sP2_prd(W0)|((?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))|aElementOf0(W0,sbsmnsldt0(xS)))))),
% 52.45/7.22 inference(NNF_transformation,[status(thm)],[f248])).
% 52.45/7.22 fof(f288,plain,(
% 52.45/7.22 (![W0]: (~sP2_prd(W0)|((![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1)))&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (sP2_prd(W0)|((?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))|aElementOf0(W0,sbsmnsldt0(xS)))))),
% 52.45/7.22 inference(miniscoping,[status(thm)],[f287])).
% 52.45/7.22 fof(f289,plain,(
% 52.45/7.22 (![W0]: (~sP2_prd(W0)|((![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1)))&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (sP2_prd(W0)|((aElementOf0(sK23_skl(W0),xS)&aElementOf0(W0,sK23_skl(W0)))|aElementOf0(W0,sbsmnsldt0(xS)))))),
% 52.45/7.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W1,sK23_skl(W0))],[f288])).
% 52.45/7.22 fof(f290,plain,(
% 52.45/7.22 ![X0,X1]: (~sP2_prd(X0)|~aElementOf0(X1,xS)|~aElementOf0(X0,X1))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f289])).
% 52.45/7.22 fof(f291,plain,(
% 52.45/7.22 ![X0]: (~sP2_prd(X0)|~aElementOf0(X0,sbsmnsldt0(xS)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f289])).
% 52.45/7.22 fof(f293,plain,(
% 52.45/7.22 ![X0]: (sP2_prd(X0)|aElementOf0(X0,sK23_skl(X0))|aElementOf0(X0,sbsmnsldt0(xS)))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f289])).
% 52.45/7.22 fof(f294,plain,(
% 52.45/7.22 ![W0,W1]: ((~sP3_prd(W1,W0)|((((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))&~aDivisorOf0(W1,W0))|~isPrime0(W1)))&(sP3_prd(W1,W0)|((((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))|aDivisorOf0(W1,W0))&isPrime0(W1))))),
% 52.45/7.22 inference(NNF_transformation,[status(thm)],[f249])).
% 52.45/7.22 fof(f295,plain,(
% 52.45/7.22 (![W0,W1]: (~sP3_prd(W1,W0)|((((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))&~aDivisorOf0(W1,W0))|~isPrime0(W1))))&(![W0,W1]: (sP3_prd(W1,W0)|((((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))|aDivisorOf0(W1,W0))&isPrime0(W1))))),
% 52.45/7.22 inference(miniscoping,[status(thm)],[f294])).
% 52.45/7.22 fof(f296,plain,(
% 52.45/7.22 (![W0,W1]: (~sP3_prd(W1,W0)|((((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))&~aDivisorOf0(W1,W0))|~isPrime0(W1))))&(![W0,W1]: (sP3_prd(W1,W0)|((((aInteger0(W1)&~W1=sz00)&(aInteger0(sK24_skl(W1,W0))&sdtasdt0(W1,sK24_skl(W1,W0))=W0))|aDivisorOf0(W1,W0))&isPrime0(W1))))),
% 52.45/7.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W2,sK24_skl(W1,W0))],[f295])).
% 52.45/7.22 fof(f298,plain,(
% 52.45/7.22 ![X0,X1]: (~sP3_prd(X0,X1)|~aDivisorOf0(X0,X1)|~isPrime0(X0))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f296])).
% 52.45/7.22 fof(f300,plain,(
% 52.45/7.22 ![X0,X1]: (sP3_prd(X0,X1)|~X0=sz00|aDivisorOf0(X0,X1))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f296])).
% 52.45/7.22 fof(f303,plain,(
% 52.45/7.22 ![X0,X1]: (sP3_prd(X0,X1)|isPrime0(X0))),
% 52.45/7.22 inference(cnf_transformation,[status(thm)],[f296])).
% 52.45/7.22 fof(f304,definition,(
% 52.45/7.22 ![X0]: (sQ0_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f305,plain,(
% 52.45/7.22 ![X0]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ0_spl)),
% 52.45/7.22 inference(component_clause,[status(thm)],[f304])).
% 52.45/7.22 fof(f307,definition,(
% 52.45/7.22 ![X1]: (sQ1_spl <=> (aElementOf0(X1,xS)))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f308,plain,(
% 52.45/7.22 ![X0]: (aElementOf0(X0,xS)|~sQ1_spl)),
% 52.45/7.22 inference(component_clause,[status(thm)],[f307])).
% 52.45/7.22 fof(f310,plain,(
% 52.45/7.22 sQ0_spl|sQ1_spl),
% 52.45/7.22 inference(split_clause,[status(thm)],[f236,f304,f307])).
% 52.45/7.22 fof(f311,definition,(
% 52.45/7.22 ![X0,X1]: (sQ2_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aInteger0(X1)))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f314,plain,(
% 52.45/7.22 sQ2_spl|sQ1_spl),
% 52.45/7.22 inference(split_clause,[status(thm)],[f237,f311,f307])).
% 52.45/7.22 fof(f315,definition,(
% 52.45/7.22 ![X0,X1]: (sQ3_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f318,plain,(
% 52.45/7.22 sQ3_spl|sQ1_spl),
% 52.45/7.22 inference(split_clause,[status(thm)],[f240,f315,f307])).
% 52.45/7.22 fof(f319,definition,(
% 52.45/7.22 ![X0,X1]: (sQ4_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|sdteqdtlpzmzozddtrp0(X1,sz00,X0)))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f322,plain,(
% 52.45/7.22 sQ4_spl|sQ1_spl),
% 52.45/7.22 inference(split_clause,[status(thm)],[f241,f319,f307])).
% 52.45/7.22 fof(f323,definition,(
% 52.45/7.22 ![X0,X1,X2]: (sQ5_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aInteger0(X2)|~sdtasdt0(X0,X2)=sdtpldt0(X1,smndt0(sz00))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f324,plain,(
% 52.45/7.22 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aInteger0(X2)|~sdtasdt0(X0,X2)=sdtpldt0(X1,smndt0(sz00))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ5_spl)),
% 52.45/7.22 inference(component_clause,[status(thm)],[f323])).
% 52.45/7.22 fof(f326,plain,(
% 52.45/7.22 sQ5_spl|sQ1_spl),
% 52.45/7.22 inference(split_clause,[status(thm)],[f242,f323,f307])).
% 52.45/7.22 fof(f327,definition,(
% 52.45/7.22 ![X0,X1]: (sQ6_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 52.45/7.22 fof(f328,plain,(
% 52.45/7.22 ![X0,X1]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ6_spl)),
% 52.45/7.22 inference(component_clause,[status(thm)],[f327])).
% 52.45/7.22 fof(f330,plain,(
% 52.45/7.22 sQ6_spl|sQ1_spl),
% 52.45/7.22 inference(split_clause,[status(thm)],[f243,f327,f307])).
% 52.45/7.22 fof(f331,definition,(
% 52.45/7.22 ![X0,X1]: (sQ7_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X1,sz00,X0)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 52.45/7.22 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f332,plain,(
% 52.45/7.23 ![X0,X1]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X1,sz00,X0)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ7_spl)),
% 52.45/7.23 inference(component_clause,[status(thm)],[f331])).
% 52.45/7.23 fof(f334,plain,(
% 52.45/7.23 sQ7_spl|sQ1_spl),
% 52.45/7.23 inference(split_clause,[status(thm)],[f244,f331,f307])).
% 52.45/7.23 fof(f335,definition,(
% 52.45/7.23 sQ8_spl <=> (aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS))))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f336,plain,(
% 52.45/7.23 aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|~sQ8_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f335])).
% 52.45/7.23 fof(f338,definition,(
% 52.45/7.23 sQ9_spl <=> (sK22_skl=sz10)),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f339,plain,(
% 52.45/7.23 sK22_skl=sz10|~sQ9_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f338])).
% 52.45/7.23 fof(f340,plain,(
% 52.45/7.23 ~sK22_skl=sz10|sQ9_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f338])).
% 52.45/7.23 fof(f341,definition,(
% 52.45/7.23 sQ10_spl <=> (sK22_skl=smndt0(sz10))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f342,plain,(
% 52.45/7.23 sK22_skl=smndt0(sz10)|~sQ10_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f341])).
% 52.45/7.23 fof(f344,plain,(
% 52.45/7.23 sQ8_spl|sQ9_spl|sQ10_spl),
% 52.45/7.23 inference(split_clause,[status(thm)],[f272,f335,f338,f341])).
% 52.45/7.23 fof(f345,plain,(
% 52.45/7.23 ~sQ8_spl|~sQ9_spl),
% 52.45/7.23 inference(split_clause,[status(thm)],[f273,f335,f338])).
% 52.45/7.23 fof(f346,plain,(
% 52.45/7.23 ~sQ8_spl|~sQ10_spl),
% 52.45/7.23 inference(split_clause,[status(thm)],[f274,f335,f341])).
% 52.45/7.23 fof(f347,plain,(
% 52.45/7.23 sP2_prd(sz00)|aInteger0(sK18_skl(sz00))),
% 52.45/7.23 inference(resolution,[status(thm)],[f48,f254])).
% 52.45/7.23 fof(f348,definition,(
% 52.45/7.23 sQ11_spl <=> (sP2_prd(sz00))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f349,plain,(
% 52.45/7.23 sP2_prd(sz00)|~sQ11_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f348])).
% 52.45/7.23 fof(f351,definition,(
% 52.45/7.23 sQ12_spl <=> (aInteger0(sK18_skl(sz00)))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f354,plain,(
% 52.45/7.23 sQ11_spl|sQ12_spl),
% 52.45/7.23 inference(split_clause,[status(thm)],[f347,f348,f351])).
% 52.45/7.23 fof(f355,plain,(
% 52.45/7.23 aInteger0(sK22_skl)|~sQ9_spl),
% 52.45/7.23 inference(forward_demodulation,[status(thm)],[f339,f49])).
% 52.45/7.23 fof(f357,definition,(
% 52.45/7.23 sQ13_spl <=> (sP2_prd(sK22_skl))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f358,plain,(
% 52.45/7.23 sP2_prd(sK22_skl)|~sQ13_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f357])).
% 52.45/7.23 fof(f365,plain,(
% 52.45/7.23 aInteger0(smndt0(sz00))),
% 52.45/7.23 inference(resolution,[status(thm)],[f51,f48])).
% 52.45/7.23 fof(f375,plain,(
% 52.45/7.23 aInteger0(smndt0(sz10))),
% 52.45/7.23 inference(resolution,[status(thm)],[f49,f51])).
% 52.45/7.23 fof(f377,definition,(
% 52.45/7.23 sQ17_spl <=> (sP2_prd(sz10))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f378,plain,(
% 52.45/7.23 sP2_prd(sz10)|~sQ17_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f377])).
% 52.45/7.23 fof(f384,plain,(
% 52.45/7.23 aInteger0(smndt0(smndt0(sz00)))),
% 52.45/7.23 inference(resolution,[status(thm)],[f365,f51])).
% 52.45/7.23 fof(f386,definition,(
% 52.45/7.23 sQ19_spl <=> (sP2_prd(smndt0(sz00)))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f387,plain,(
% 52.45/7.23 sP2_prd(smndt0(sz00))|~sQ19_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f386])).
% 52.45/7.23 fof(f389,definition,(
% 52.45/7.23 sQ20_spl <=> (aInteger0(sK18_skl(smndt0(sz00))))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f390,plain,(
% 52.45/7.23 aInteger0(sK18_skl(smndt0(sz00)))|~sQ20_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f389])).
% 52.45/7.23 fof(f391,plain,(
% 52.45/7.23 ~aInteger0(sK18_skl(smndt0(sz00)))|sQ20_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f389])).
% 52.45/7.23 fof(f394,plain,(
% 52.45/7.23 ![X0]: (~aInteger0(X0)|aInteger0(sdtasdt0(sz10,X0)))),
% 52.45/7.23 inference(resolution,[status(thm)],[f55,f49])).
% 52.45/7.23 fof(f412,plain,(
% 52.45/7.23 aInteger0(smndt0(smndt0(smndt0(sz00))))),
% 52.45/7.23 inference(resolution,[status(thm)],[f384,f51])).
% 52.45/7.23 fof(f413,plain,(
% 52.45/7.23 sP2_prd(smndt0(smndt0(sz00)))|aInteger0(sK18_skl(smndt0(smndt0(sz00))))),
% 52.45/7.23 inference(resolution,[status(thm)],[f384,f254])).
% 52.45/7.23 fof(f414,definition,(
% 52.45/7.23 sQ23_spl <=> (sP2_prd(smndt0(smndt0(sz00))))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f415,plain,(
% 52.45/7.23 sP2_prd(smndt0(smndt0(sz00)))|~sQ23_spl),
% 52.45/7.23 inference(component_clause,[status(thm)],[f414])).
% 52.45/7.23 fof(f417,definition,(
% 52.45/7.23 sQ24_spl <=> (aInteger0(sK18_skl(smndt0(smndt0(sz00)))))),
% 52.45/7.23 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 52.45/7.23 fof(f420,plain,(
% 52.45/7.23 sQ23_spl|sQ24_spl),
% 52.45/7.23 inference(split_clause,[status(thm)],[f413,f414,f417])).
% 52.45/7.23 fof(f437,plain,(
% 52.45/7.23 sdtpldt0(sz00,sz00)=sz00),
% 52.45/7.23 inference(resolution,[status(thm)],[f61,f48])).
% 52.45/7.23 fof(f442,plain,(
% 52.45/7.23 sz10=sdtpldt0(sz00,sz10)),
% 52.45/7.23 inference(resolution,[status(thm)],[f62,f49])).
% 52.45/7.23 fof(f448,plain,(
% 52.45/7.23 sdtasdt0(sz10,sz10)=sz10),
% 52.45/7.23 inference(resolution,[status(thm)],[f71,f49])).
% 52.45/7.23 fof(f482,plain,(
% 52.45/7.23 sP2_prd(smndt0(smndt0(sz00)))|aInteger0(sK19_skl(smndt0(smndt0(sz00))))),
% 52.45/7.23 inference(resolution,[status(thm)],[f256,f384])).
% 52.45/7.23 fof(f486,plain,(
% 52.45/7.24 sP2_prd(sz00)|aInteger0(sK19_skl(sz00))),
% 52.45/7.24 inference(resolution,[status(thm)],[f256,f48])).
% 52.45/7.24 fof(f491,definition,(
% 52.45/7.24 sQ28_spl <=> (aInteger0(sK19_skl(smndt0(smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f494,plain,(
% 52.45/7.24 sQ23_spl|sQ28_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f482,f414,f491])).
% 52.45/7.24 fof(f499,definition,(
% 52.45/7.24 sQ30_spl <=> (aInteger0(sK19_skl(smndt0(sz00))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f501,plain,(
% 52.45/7.24 ~aInteger0(sK19_skl(smndt0(sz00)))|sQ30_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f499])).
% 52.45/7.24 fof(f507,definition,(
% 52.45/7.24 sQ32_spl <=> (aInteger0(sK19_skl(sz00)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f510,plain,(
% 52.45/7.24 sQ11_spl|sQ32_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f486,f348,f507])).
% 52.45/7.24 fof(f512,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(sz00)))|isPrime0(sK18_skl(smndt0(smndt0(sz00))))),
% 52.45/7.24 inference(resolution,[status(thm)],[f259,f384])).
% 52.45/7.24 fof(f514,plain,(
% 52.45/7.24 sP2_prd(smndt0(sz00))|isPrime0(sK18_skl(smndt0(sz00)))),
% 52.45/7.24 inference(resolution,[status(thm)],[f259,f365])).
% 52.45/7.24 fof(f515,plain,(
% 52.45/7.24 sP2_prd(sz10)|isPrime0(sK18_skl(sz10))),
% 52.45/7.24 inference(resolution,[status(thm)],[f259,f49])).
% 52.45/7.24 fof(f516,plain,(
% 52.45/7.24 sP2_prd(sz00)|isPrime0(sK18_skl(sz00))),
% 52.45/7.24 inference(resolution,[status(thm)],[f259,f48])).
% 52.45/7.24 fof(f521,definition,(
% 52.45/7.24 sQ34_spl <=> (isPrime0(sK18_skl(smndt0(smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f524,plain,(
% 52.45/7.24 sQ23_spl|sQ34_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f512,f414,f521])).
% 52.45/7.24 fof(f529,definition,(
% 52.45/7.24 sQ36_spl <=> (isPrime0(sK18_skl(smndt0(sz00))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f532,plain,(
% 52.45/7.24 sQ19_spl|sQ36_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f514,f386,f529])).
% 52.45/7.24 fof(f533,definition,(
% 52.45/7.24 sQ37_spl <=> (isPrime0(sK18_skl(sz10)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f536,plain,(
% 52.45/7.24 sQ17_spl|sQ37_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f515,f377,f533])).
% 52.45/7.24 fof(f537,definition,(
% 52.45/7.24 sQ38_spl <=> (isPrime0(sK18_skl(sz00)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f538,plain,(
% 52.45/7.24 isPrime0(sK18_skl(sz00))|~sQ38_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f537])).
% 52.45/7.24 fof(f540,plain,(
% 52.45/7.24 sQ11_spl|sQ38_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f516,f348,f537])).
% 52.45/7.24 fof(f542,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(sz00)))|sdtasdt0(sK18_skl(smndt0(smndt0(sz00))),sK19_skl(smndt0(smndt0(sz00))))=smndt0(smndt0(sz00))),
% 52.45/7.24 inference(resolution,[status(thm)],[f257,f384])).
% 52.45/7.24 fof(f544,plain,(
% 52.45/7.24 sP2_prd(smndt0(sz00))|sdtasdt0(sK18_skl(smndt0(sz00)),sK19_skl(smndt0(sz00)))=smndt0(sz00)),
% 52.45/7.24 inference(resolution,[status(thm)],[f257,f365])).
% 52.45/7.24 fof(f546,plain,(
% 52.45/7.24 sP2_prd(sz00)|sdtasdt0(sK18_skl(sz00),sK19_skl(sz00))=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f257,f48])).
% 52.45/7.24 fof(f551,definition,(
% 52.45/7.24 sQ40_spl <=> (sdtasdt0(sK18_skl(smndt0(smndt0(sz00))),sK19_skl(smndt0(smndt0(sz00))))=smndt0(smndt0(sz00)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f554,plain,(
% 52.45/7.24 sQ23_spl|sQ40_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f542,f414,f551])).
% 52.45/7.24 fof(f559,definition,(
% 52.45/7.24 sQ42_spl <=> (sdtasdt0(sK18_skl(smndt0(sz00)),sK19_skl(smndt0(sz00)))=smndt0(sz00))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f562,plain,(
% 52.45/7.24 sQ19_spl|sQ42_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f544,f386,f559])).
% 52.45/7.24 fof(f567,definition,(
% 52.45/7.24 sQ44_spl <=> (sdtasdt0(sK18_skl(sz00),sK19_skl(sz00))=sz00)),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f570,plain,(
% 52.45/7.24 sQ11_spl|sQ44_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f546,f348,f567])).
% 52.45/7.24 fof(f576,plain,(
% 52.45/7.24 sz00=sdtasdt0(sz10,sz00)),
% 52.45/7.24 inference(resolution,[status(thm)],[f72,f48])).
% 52.45/7.24 fof(f579,plain,(
% 52.45/7.24 sdtasdt0(smndt0(sz10),sz00)=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f77,f375])).
% 52.45/7.24 fof(f582,plain,(
% 52.45/7.24 sdtasdt0(sz00,sz00)=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f77,f48])).
% 52.45/7.24 fof(f593,plain,(
% 52.45/7.24 aInteger0(sdtasdt0(sz10,smndt0(sz00)))),
% 52.45/7.24 inference(resolution,[status(thm)],[f394,f365])).
% 52.45/7.24 fof(f632,plain,(
% 52.45/7.24 ![X0]: (aInteger0(sK15_skl(X0))|~sQ1_spl)),
% 52.45/7.24 inference(forward_subsumption_resolution,[status(thm)],[f223,f308])).
% 52.45/7.24 fof(f641,plain,(
% 52.45/7.24 ![X0]: (sdtasdt0(sK15_skl(X0),sz00)=sz00|~sQ1_spl)),
% 52.45/7.24 inference(resolution,[status(thm)],[f632,f77])).
% 52.45/7.24 fof(f652,plain,(
% 52.45/7.24 ![X0]: (sdtasdt0(sK15_skl(X0),sz10)=sK15_skl(X0)|~sQ1_spl)),
% 52.45/7.24 inference(resolution,[status(thm)],[f632,f71])).
% 52.45/7.24 fof(f764,plain,(
% 52.45/7.24 ![X0]: (~sK15_skl(X0)=sz00|~sQ1_spl)),
% 52.45/7.24 inference(forward_subsumption_resolution,[status(thm)],[f224,f308])).
% 52.45/7.24 fof(f775,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(smndt0(sz00))))|sdtasdt0(sK18_skl(smndt0(smndt0(smndt0(sz00)))),sK19_skl(smndt0(smndt0(smndt0(sz00)))))=smndt0(smndt0(smndt0(sz00)))),
% 52.45/7.24 inference(resolution,[status(thm)],[f412,f257])).
% 52.45/7.24 fof(f776,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(smndt0(sz00))))|isPrime0(sK18_skl(smndt0(smndt0(smndt0(sz00)))))),
% 52.45/7.24 inference(resolution,[status(thm)],[f412,f259])).
% 52.45/7.24 fof(f777,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(smndt0(sz00))))|aInteger0(sK19_skl(smndt0(smndt0(smndt0(sz00)))))),
% 52.45/7.24 inference(resolution,[status(thm)],[f412,f256])).
% 52.45/7.24 fof(f790,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(smndt0(sz00))))|aInteger0(sK18_skl(smndt0(smndt0(smndt0(sz00)))))),
% 52.45/7.24 inference(resolution,[status(thm)],[f412,f254])).
% 52.45/7.24 fof(f791,definition,(
% 52.45/7.24 sQ45_spl <=> (sP2_prd(smndt0(smndt0(smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f792,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(smndt0(sz00))))|~sQ45_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f791])).
% 52.45/7.24 fof(f794,definition,(
% 52.45/7.24 sQ46_spl <=> (sdtasdt0(sK18_skl(smndt0(smndt0(smndt0(sz00)))),sK19_skl(smndt0(smndt0(smndt0(sz00)))))=smndt0(smndt0(smndt0(sz00))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f797,plain,(
% 52.45/7.24 sQ45_spl|sQ46_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f775,f791,f794])).
% 52.45/7.24 fof(f798,definition,(
% 52.45/7.24 sQ47_spl <=> (isPrime0(sK18_skl(smndt0(smndt0(smndt0(sz00))))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f799,plain,(
% 52.45/7.24 isPrime0(sK18_skl(smndt0(smndt0(smndt0(sz00)))))|~sQ47_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f798])).
% 52.45/7.24 fof(f801,plain,(
% 52.45/7.24 sQ45_spl|sQ47_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f776,f791,f798])).
% 52.45/7.24 fof(f802,definition,(
% 52.45/7.24 sQ48_spl <=> (aInteger0(sK19_skl(smndt0(smndt0(smndt0(sz00))))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f805,plain,(
% 52.45/7.24 sQ45_spl|sQ48_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f777,f791,f802])).
% 52.45/7.24 fof(f806,definition,(
% 52.45/7.24 sQ49_spl <=> (aInteger0(sK18_skl(smndt0(smndt0(smndt0(sz00))))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f809,plain,(
% 52.45/7.24 sQ45_spl|sQ49_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f790,f791,f806])).
% 52.45/7.24 fof(f1031,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(smndt0(sz00))))|aDivisorOf0(sK18_skl(smndt0(smndt0(smndt0(sz00)))),smndt0(smndt0(smndt0(sz00))))),
% 52.45/7.24 inference(resolution,[status(thm)],[f258,f412])).
% 52.45/7.24 fof(f1034,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(sz00)))|aDivisorOf0(sK18_skl(smndt0(smndt0(sz00))),smndt0(smndt0(sz00)))),
% 52.45/7.24 inference(resolution,[status(thm)],[f258,f384])).
% 52.45/7.24 fof(f1036,plain,(
% 52.45/7.24 sP2_prd(smndt0(sz00))|aDivisorOf0(sK18_skl(smndt0(sz00)),smndt0(sz00))),
% 52.45/7.24 inference(resolution,[status(thm)],[f258,f365])).
% 52.45/7.24 fof(f1037,plain,(
% 52.45/7.24 sP2_prd(sz10)|aDivisorOf0(sK18_skl(sz10),sz10)),
% 52.45/7.24 inference(resolution,[status(thm)],[f258,f49])).
% 52.45/7.24 fof(f1038,plain,(
% 52.45/7.24 sP2_prd(sz00)|aDivisorOf0(sK18_skl(sz00),sz00)),
% 52.45/7.24 inference(resolution,[status(thm)],[f258,f48])).
% 52.45/7.24 fof(f1047,definition,(
% 52.45/7.24 sQ62_spl <=> (aDivisorOf0(sK18_skl(smndt0(smndt0(smndt0(sz00)))),smndt0(smndt0(smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1048,plain,(
% 52.45/7.24 aDivisorOf0(sK18_skl(smndt0(smndt0(smndt0(sz00)))),smndt0(smndt0(smndt0(sz00))))|~sQ62_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1047])).
% 52.45/7.24 fof(f1050,plain,(
% 52.45/7.24 sQ45_spl|sQ62_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1031,f791,f1047])).
% 52.45/7.24 fof(f1055,definition,(
% 52.45/7.24 sQ64_spl <=> (aDivisorOf0(sK18_skl(smndt0(smndt0(sz00))),smndt0(smndt0(sz00))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1058,plain,(
% 52.45/7.24 sQ23_spl|sQ64_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1034,f414,f1055])).
% 52.45/7.24 fof(f1063,definition,(
% 52.45/7.24 sQ66_spl <=> (aDivisorOf0(sK18_skl(smndt0(sz00)),smndt0(sz00)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1066,plain,(
% 52.45/7.24 sQ19_spl|sQ66_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1036,f386,f1063])).
% 52.45/7.24 fof(f1067,definition,(
% 52.45/7.24 sQ67_spl <=> (aDivisorOf0(sK18_skl(sz10),sz10))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1068,plain,(
% 52.45/7.24 aDivisorOf0(sK18_skl(sz10),sz10)|~sQ67_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1067])).
% 52.45/7.24 fof(f1070,plain,(
% 52.45/7.24 sQ17_spl|sQ67_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1037,f377,f1067])).
% 52.45/7.24 fof(f1071,definition,(
% 52.45/7.24 sQ68_spl <=> (aDivisorOf0(sK18_skl(sz00),sz00))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1074,plain,(
% 52.45/7.24 sQ11_spl|sQ68_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1038,f348,f1071])).
% 52.45/7.24 fof(f1232,plain,(
% 52.45/7.24 sP2_prd(sdtasdt0(sz10,smndt0(sz00)))|aDivisorOf0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))),sdtasdt0(sz10,smndt0(sz00)))),
% 52.45/7.24 inference(resolution,[status(thm)],[f593,f258])).
% 52.45/7.24 fof(f1254,plain,(
% 52.45/7.24 sP2_prd(sdtasdt0(sz10,smndt0(sz00)))|sdtasdt0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))),sK19_skl(sdtasdt0(sz10,smndt0(sz00))))=sdtasdt0(sz10,smndt0(sz00))),
% 52.45/7.24 inference(resolution,[status(thm)],[f593,f257])).
% 52.45/7.24 fof(f1255,plain,(
% 52.45/7.24 sP2_prd(sdtasdt0(sz10,smndt0(sz00)))|isPrime0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))))),
% 52.45/7.24 inference(resolution,[status(thm)],[f593,f259])).
% 52.45/7.24 fof(f1270,definition,(
% 52.45/7.24 sQ75_spl <=> (sP2_prd(sdtasdt0(sz10,smndt0(sz00))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1271,plain,(
% 52.45/7.24 sP2_prd(sdtasdt0(sz10,smndt0(sz00)))|~sQ75_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1270])).
% 52.45/7.24 fof(f1273,definition,(
% 52.45/7.24 sQ76_spl <=> (aDivisorOf0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))),sdtasdt0(sz10,smndt0(sz00))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1274,plain,(
% 52.45/7.24 aDivisorOf0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))),sdtasdt0(sz10,smndt0(sz00)))|~sQ76_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1273])).
% 52.45/7.24 fof(f1276,plain,(
% 52.45/7.24 sQ75_spl|sQ76_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1232,f1270,f1273])).
% 52.45/7.24 fof(f1277,definition,(
% 52.45/7.24 sQ77_spl <=> (sdtasdt0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))),sK19_skl(sdtasdt0(sz10,smndt0(sz00))))=sdtasdt0(sz10,smndt0(sz00)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1280,plain,(
% 52.45/7.24 sQ75_spl|sQ77_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1254,f1270,f1277])).
% 52.45/7.24 fof(f1281,definition,(
% 52.45/7.24 sQ78_spl <=> (isPrime0(sK18_skl(sdtasdt0(sz10,smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1284,plain,(
% 52.45/7.24 sQ75_spl|sQ78_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1255,f1270,f1281])).
% 52.45/7.24 fof(f1285,definition,(
% 52.45/7.24 sQ79_spl <=> (aInteger0(sK19_skl(sdtasdt0(sz10,smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1287,plain,(
% 52.45/7.24 ~aInteger0(sK19_skl(sdtasdt0(sz10,smndt0(sz00))))|sQ79_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1285])).
% 52.45/7.24 fof(f1289,definition,(
% 52.45/7.24 sQ80_spl <=> (aInteger0(sK18_skl(sdtasdt0(sz10,smndt0(sz00)))))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1291,plain,(
% 52.45/7.24 ~aInteger0(sK18_skl(sdtasdt0(sz10,smndt0(sz00))))|sQ80_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1289])).
% 52.45/7.24 fof(f1311,plain,(
% 52.45/7.24 sdtasdt0(smndt0(sz10),sz00)=smndt0(sz00)),
% 52.45/7.24 inference(resolution,[status(thm)],[f80,f48])).
% 52.45/7.24 fof(f1312,plain,(
% 52.45/7.24 sz00=smndt0(sz00)),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f579,f1311])).
% 52.45/7.24 fof(f1334,plain,(
% 52.45/7.24 sP2_prd(smndt0(smndt0(sz00)))|~sQ45_spl),
% 52.45/7.24 inference(backward_demodulation,[status(thm)],[f1312,f792])).
% 52.45/7.24 fof(f1337,plain,(
% 52.45/7.24 sP2_prd(smndt0(sz00))|~sQ23_spl),
% 52.45/7.24 inference(backward_demodulation,[status(thm)],[f1312,f415])).
% 52.45/7.24 fof(f1339,plain,(
% 52.45/7.24 sP2_prd(sz00)|~sQ19_spl),
% 52.45/7.24 inference(backward_demodulation,[status(thm)],[f1312,f387])).
% 52.45/7.24 fof(f1342,plain,(
% 52.45/7.24 sP2_prd(smndt0(sz00))|~sQ45_spl),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f1312,f1334])).
% 52.45/7.24 fof(f1343,plain,(
% 52.45/7.24 sP2_prd(sz00)|~sQ45_spl),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f1312,f1342])).
% 52.45/7.24 fof(f1346,plain,(
% 52.45/7.24 sP2_prd(sz00)|~sQ23_spl),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f1312,f1337])).
% 52.45/7.24 fof(f1482,plain,(
% 52.45/7.24 sP2_prd(sdtasdt0(sz10,sz00))|~sQ75_spl),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f1312,f1271])).
% 52.45/7.24 fof(f1483,plain,(
% 52.45/7.24 sP2_prd(sz00)|~sQ75_spl),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f576,f1482])).
% 52.45/7.24 fof(f1484,plain,(
% 52.45/7.24 ![X0]: (sP3_prd(sdtasdt0(smndt0(sz10),sz00),X0)|aDivisorOf0(sdtasdt0(smndt0(sz10),sz00),X0))),
% 52.45/7.24 inference(resolution,[status(thm)],[f300,f579])).
% 52.45/7.24 fof(f1496,plain,(
% 52.45/7.24 ![X0]: (sP3_prd(sz00,X0)|aDivisorOf0(sdtasdt0(smndt0(sz10),sz00),X0))),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f579,f1484])).
% 52.45/7.24 fof(f1497,plain,(
% 52.45/7.24 ![X0]: (sP3_prd(sz00,X0)|aDivisorOf0(sz00,X0))),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f579,f1496])).
% 52.45/7.24 fof(f1520,plain,(
% 52.45/7.24 ~aInteger0(sz00)|~aInteger0(sz00)|sz00=sz00|sz00=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f83,f582])).
% 52.45/7.24 fof(f1535,definition,(
% 52.45/7.24 sQ93_spl <=> (aInteger0(smndt0(sz10)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1537,plain,(
% 52.45/7.24 ~aInteger0(smndt0(sz10))|sQ93_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1535])).
% 52.45/7.24 fof(f1538,definition,(
% 52.45/7.24 sQ94_spl <=> (aInteger0(sz00))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1540,plain,(
% 52.45/7.24 ~aInteger0(sz00)|sQ94_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1538])).
% 52.45/7.24 fof(f1541,definition,(
% 52.45/7.24 sQ95_spl <=> (smndt0(sz10)=sz00)),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1542,plain,(
% 52.45/7.24 smndt0(sz10)=sz00|~sQ95_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1541])).
% 52.45/7.24 fof(f1544,definition,(
% 52.45/7.24 sQ96_spl <=> (sz00=sz00)),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1552,plain,(
% 52.45/7.24 ~sQ94_spl|sQ96_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1520,f1538,f1544])).
% 52.45/7.24 fof(f1553,definition,(
% 52.45/7.24 sQ98_spl <=> (aInteger0(sz10))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1555,plain,(
% 52.45/7.24 ~aInteger0(sz10)|sQ98_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1553])).
% 52.45/7.24 fof(f1556,definition,(
% 52.45/7.24 sQ99_spl <=> (sz10=sz00)),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1557,plain,(
% 52.45/7.24 sz10=sz00|~sQ99_spl),
% 52.45/7.24 inference(component_clause,[status(thm)],[f1556])).
% 52.45/7.24 fof(f1576,plain,(
% 52.45/7.24 $false|sQ94_spl),
% 52.45/7.24 inference(forward_subsumption_resolution,[status(thm)],[f1540,f48])).
% 52.45/7.24 fof(f1577,plain,(
% 52.45/7.24 sQ94_spl),
% 52.45/7.24 inference(contradiction_clause,[status(thm)],[f1576])).
% 52.45/7.24 fof(f1582,plain,(
% 52.45/7.24 ![X0]: (sP3_prd(sz00,X0)|~aInteger0(X0)|~sz00=sz00)),
% 52.45/7.24 inference(resolution,[status(thm)],[f1497,f89])).
% 52.45/7.24 fof(f1585,definition,(
% 52.45/7.24 ![X0]: (sQ101_spl <=> (sP3_prd(sz00,X0)|~aInteger0(X0)))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 52.45/7.24 fof(f1588,plain,(
% 52.45/7.24 sQ101_spl|~sQ96_spl),
% 52.45/7.24 inference(split_clause,[status(thm)],[f1582,f1585,f1544])).
% 52.45/7.24 fof(f1618,plain,(
% 52.45/7.24 ![X0]: (sdtasdt0(sK15_skl(X0),sz00)=sK15_skl(X0)|~sQ99_spl|~sQ1_spl)),
% 52.45/7.24 inference(backward_demodulation,[status(thm)],[f1557,f652])).
% 52.45/7.24 fof(f1640,plain,(
% 52.45/7.24 sz10=sdtpldt0(sz00,sz00)|~sQ99_spl),
% 52.45/7.24 inference(backward_demodulation,[status(thm)],[f1557,f442])).
% 52.45/7.24 fof(f1666,plain,(
% 52.45/7.24 ![X0]: (sz00=sK15_skl(X0)|~sQ99_spl|~sQ1_spl)),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f641,f1618])).
% 52.45/7.24 fof(f1667,plain,(
% 52.45/7.24 $false|~sQ99_spl|~sQ1_spl),
% 52.45/7.24 inference(forward_subsumption_resolution,[status(thm)],[f1666,f764])).
% 52.45/7.24 fof(f1668,plain,(
% 52.45/7.24 ~sQ99_spl|~sQ1_spl),
% 52.45/7.24 inference(contradiction_clause,[status(thm)],[f1667])).
% 52.45/7.24 fof(f1670,plain,(
% 52.45/7.24 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aInteger0(X2)|~sdtasdt0(X0,X2)=sdtpldt0(X1,sz00)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ5_spl)),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f1312,f324])).
% 52.45/7.24 fof(f1671,plain,(
% 52.45/7.24 ![X0,X1]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~aDivisorOf0(X0,sdtpldt0(X1,sz00))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ6_spl)),
% 52.45/7.24 inference(forward_demodulation,[status(thm)],[f1312,f328])).
% 52.45/7.24 fof(f1691,plain,(
% 52.45/7.24 sz00=sdtasdt0(sz00,sz10)),
% 52.45/7.24 inference(resolution,[status(thm)],[f49,f78])).
% 52.45/7.24 fof(f1692,plain,(
% 52.45/7.24 sdtasdt0(sz10,sz00)=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f49,f77])).
% 52.45/7.24 fof(f1702,plain,(
% 52.45/7.24 sz10=sdtpldt0(sz00,sz10)),
% 52.45/7.24 inference(resolution,[status(thm)],[f49,f62])).
% 52.45/7.24 fof(f1703,plain,(
% 52.45/7.24 sdtpldt0(sz10,sz00)=sz10),
% 52.45/7.24 inference(resolution,[status(thm)],[f49,f61])).
% 52.45/7.24 fof(f1704,plain,(
% 52.45/7.24 sdtpldt0(sz10,smndt0(sz10))=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f49,f64])).
% 52.45/7.24 fof(f1713,plain,(
% 52.45/7.24 $false|sQ98_spl),
% 52.45/7.24 inference(forward_subsumption_resolution,[status(thm)],[f1555,f49])).
% 52.45/7.24 fof(f1714,plain,(
% 52.45/7.24 sQ98_spl),
% 52.45/7.24 inference(contradiction_clause,[status(thm)],[f1713])).
% 52.45/7.24 fof(f1771,plain,(
% 52.45/7.24 sdtasdt0(smndt0(sz10),sz00)=sz00),
% 52.45/7.24 inference(resolution,[status(thm)],[f375,f77])).
% 52.45/7.24 fof(f1882,plain,(
% 52.45/7.24 ~aInteger0(sz00)|aDivisorOf0(sz10,sz00)|~aInteger0(sz10)|sz10=sz00|~aInteger0(sz00)),
% 52.45/7.24 inference(resolution,[status(thm)],[f576,f92])).
% 52.45/7.24 fof(f1884,plain,(
% 52.45/7.24 ![X0]: (~aInteger0(X0)|aDivisorOf0(sz10,X0)|~aInteger0(sz10)|sz10=sz00|~aInteger0(sz00)|~sz00=X0)),
% 52.45/7.24 inference(paramodulation,[status(thm)],[f576,f92])).
% 52.45/7.24 fof(f1887,definition,(
% 52.45/7.24 sQ106_spl <=> (aDivisorOf0(sz10,sz00))),
% 52.45/7.24 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f1888,plain,(
% 40.22/7.26 aDivisorOf0(sz10,sz00)|~sQ106_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f1887])).
% 40.22/7.26 fof(f1890,plain,(
% 40.22/7.26 ~sQ94_spl|sQ106_spl|~sQ98_spl|sQ99_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1882,f1538,f1887,f1553,f1556])).
% 40.22/7.26 fof(f1893,definition,(
% 40.22/7.26 ![X0]: (sQ107_spl <=> (~aInteger0(X0)|aDivisorOf0(sz10,X0)|~sz00=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f1896,plain,(
% 40.22/7.26 sQ107_spl|~sQ98_spl|sQ99_spl|~sQ94_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1884,f1893,f1553,f1556,f1538])).
% 40.22/7.26 fof(f1911,plain,(
% 40.22/7.26 sz10=sz00|~sQ99_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f437,f1640])).
% 40.22/7.26 fof(f1944,plain,(
% 40.22/7.26 ![X0,X1]: (~aInteger0(X0)|~aInteger0(sz00)|~aInteger0(X1)|X1=sz00|sdteqdtlpzmzozddtrp0(X0,sz00,X1)|~aDivisorOf0(X1,sdtpldt0(X0,sz00)))),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f1312,f96])).
% 40.22/7.26 fof(f1949,definition,(
% 40.22/7.26 ![X0,X1]: (sQ109_spl <=> (~aInteger0(X0)|~aInteger0(X1)|X1=sz00|sdteqdtlpzmzozddtrp0(X0,sz00,X1)|~aDivisorOf0(X1,sdtpldt0(X0,sz00))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f1952,plain,(
% 40.22/7.26 sQ109_spl|~sQ94_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1944,f1949,f1538])).
% 40.22/7.26 fof(f1962,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sz00)|aElementOf0(sz00,sK20_skl(sz00)))),
% 40.22/7.26 inference(resolution,[status(thm)],[f261,f48])).
% 40.22/7.26 fof(f1963,definition,(
% 40.22/7.26 ![X0]: (sQ110_spl <=> (sP3_prd(X0,sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f1964,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sz00)|~sQ110_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f1963])).
% 40.22/7.26 fof(f1966,definition,(
% 40.22/7.26 sQ111_spl <=> (aElementOf0(sz00,sK20_skl(sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f1967,plain,(
% 40.22/7.26 aElementOf0(sz00,sK20_skl(sz00))|~sQ111_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f1966])).
% 40.22/7.26 fof(f1969,plain,(
% 40.22/7.26 sQ110_spl|sQ111_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1962,f1963,f1966])).
% 40.22/7.26 fof(f2057,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sz00)|aElementOf0(sz00,sbsmnsldt0(xS)))),
% 40.22/7.26 inference(resolution,[status(thm)],[f262,f48])).
% 40.22/7.26 fof(f2058,definition,(
% 40.22/7.26 sQ114_spl <=> (aElementOf0(sz00,sbsmnsldt0(xS)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2059,plain,(
% 40.22/7.26 aElementOf0(sz00,sbsmnsldt0(xS))|~sQ114_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2058])).
% 40.22/7.26 fof(f2061,plain,(
% 40.22/7.26 sQ110_spl|sQ114_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f2057,f1963,f2058])).
% 40.22/7.26 fof(f2124,plain,(
% 40.22/7.26 aInteger0(sK22_skl)|~sQ8_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f269,f336])).
% 40.22/7.26 fof(f2127,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sK22_skl)|aElementOf0(sK22_skl,sbsmnsldt0(xS))|~sQ8_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f2124,f262])).
% 40.22/7.26 fof(f2168,definition,(
% 40.22/7.26 ![X0]: (sQ115_spl <=> (sP3_prd(X0,sK22_skl)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2169,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sK22_skl)|~sQ115_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2168])).
% 40.22/7.26 fof(f2171,definition,(
% 40.22/7.26 sQ116_spl <=> (aElementOf0(sK22_skl,sbsmnsldt0(xS)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2172,plain,(
% 40.22/7.26 aElementOf0(sK22_skl,sbsmnsldt0(xS))|~sQ116_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2171])).
% 40.22/7.26 fof(f2174,plain,(
% 40.22/7.26 sQ115_spl|sQ116_spl|~sQ8_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f2127,f2168,f2171,f335])).
% 40.22/7.26 fof(f2179,definition,(
% 40.22/7.26 sQ118_spl <=> (aDivisorOf0(sK18_skl(sK22_skl),sK22_skl))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2180,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sK22_skl),sK22_skl)|~sQ118_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2179])).
% 40.22/7.26 fof(f2187,definition,(
% 40.22/7.26 sQ120_spl <=> (isPrime0(sK18_skl(sK22_skl)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2201,definition,(
% 40.22/7.26 sQ122_spl <=> (aDivisorOf0(sK1_skl(sz00),sz00))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2202,plain,(
% 40.22/7.26 aDivisorOf0(sK1_skl(sz00),sz00)|~sQ122_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2201])).
% 40.22/7.26 fof(f2205,plain,(
% 40.22/7.26 isPrime0(sK1_skl(sz00))|sz00=sz10|sz00=smndt0(sz10)),
% 40.22/7.26 inference(resolution,[status(thm)],[f114,f48])).
% 40.22/7.26 fof(f2206,definition,(
% 40.22/7.26 sQ123_spl <=> (isPrime0(sK1_skl(sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2207,plain,(
% 40.22/7.26 isPrime0(sK1_skl(sz00))|~sQ123_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2206])).
% 40.22/7.26 fof(f2209,plain,(
% 40.22/7.26 sQ123_spl|sQ99_spl|sQ95_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f2205,f2206,f1556,f1541])).
% 40.22/7.26 fof(f2293,plain,(
% 40.22/7.26 sK22_skl=sz00|~sQ9_spl|~sQ99_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f339,f1911])).
% 40.22/7.26 fof(f2354,definition,(
% 40.22/7.26 sQ129_spl <=> (isPrime0(sK18_skl(smndt0(sK22_skl))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2355,plain,(
% 40.22/7.26 isPrime0(sK18_skl(smndt0(sK22_skl)))|~sQ129_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2354])).
% 40.22/7.26 fof(f2356,plain,(
% 40.22/7.26 ~isPrime0(sK18_skl(smndt0(sK22_skl)))|sQ129_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2354])).
% 40.22/7.26 fof(f2468,definition,(
% 40.22/7.26 ![X0]: (sQ131_spl <=> (sP3_prd(X0,smndt0(sz00))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2469,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,smndt0(sz00))|~sQ131_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2468])).
% 40.22/7.26 fof(f2475,definition,(
% 40.22/7.26 sQ133_spl <=> (aElementOf0(smndt0(sz00),sK20_skl(smndt0(sz00))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2477,plain,(
% 40.22/7.26 ~aElementOf0(smndt0(sz00),sK20_skl(smndt0(sz00)))|sQ133_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2475])).
% 40.22/7.26 fof(f2516,definition,(
% 40.22/7.26 sQ135_spl <=> (aElementOf0(sz10,sbsmnsldt0(xS)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2517,plain,(
% 40.22/7.26 aElementOf0(sz10,sbsmnsldt0(xS))|~sQ135_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2516])).
% 40.22/7.26 fof(f2518,plain,(
% 40.22/7.26 ~aElementOf0(sz10,sbsmnsldt0(xS))|sQ135_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2516])).
% 40.22/7.26 fof(f2561,definition,(
% 40.22/7.26 sQ137_spl <=> (aSet0(xS))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2563,plain,(
% 40.22/7.26 ~aSet0(xS)|sQ137_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2561])).
% 40.22/7.26 fof(f2568,plain,(
% 40.22/7.26 $false|sQ137_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f2563,f222])).
% 40.22/7.26 fof(f2569,plain,(
% 40.22/7.26 sQ137_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f2568])).
% 40.22/7.26 fof(f2701,definition,(
% 40.22/7.26 sQ141_spl <=> (aInteger0(sK22_skl))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2702,plain,(
% 40.22/7.26 aInteger0(sK22_skl)|~sQ141_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2701])).
% 40.22/7.26 fof(f2703,plain,(
% 40.22/7.26 ~aInteger0(sK22_skl)|sQ141_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2701])).
% 40.22/7.26 fof(f2739,plain,(
% 40.22/7.26 aInteger0(smndt0(sz10))),
% 40.22/7.26 inference(resolution,[status(thm)],[f49,f51])).
% 40.22/7.26 fof(f2829,plain,(
% 40.22/7.26 ~aInteger0(sz00)|sdtasdt0(sz10,sK0_skl(sz10,sz00))=sz00|~sQ106_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f1888,f91])).
% 40.22/7.26 fof(f2830,plain,(
% 40.22/7.26 ~aInteger0(sz00)|aInteger0(sK0_skl(sz10,sz00))|~sQ106_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f1888,f90])).
% 40.22/7.26 fof(f2833,definition,(
% 40.22/7.26 sQ147_spl <=> (sdtasdt0(sz10,sK0_skl(sz10,sz00))=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2836,plain,(
% 40.22/7.26 ~sQ94_spl|sQ147_spl|~sQ106_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f2829,f1538,f2833,f1887])).
% 40.22/7.26 fof(f2837,definition,(
% 40.22/7.26 sQ148_spl <=> (aInteger0(sK0_skl(sz10,sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2840,plain,(
% 40.22/7.26 ~sQ94_spl|sQ148_spl|~sQ106_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f2830,f1538,f2837,f1887])).
% 40.22/7.26 fof(f2842,definition,(
% 40.22/7.26 sQ149_spl <=> (sP3_prd(sz10,sz00))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2844,plain,(
% 40.22/7.26 ~sP3_prd(sz10,sz00)|sQ149_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2842])).
% 40.22/7.26 fof(f2845,definition,(
% 40.22/7.26 sQ150_spl <=> (isPrime0(sz10))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f2847,plain,(
% 40.22/7.26 ~isPrime0(sz10)|sQ150_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f2845])).
% 40.22/7.26 fof(f2892,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sz00)|~sQ131_spl)),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f2469])).
% 40.22/7.26 fof(f3397,plain,(
% 40.22/7.26 aElementOf0(sz00,sK21_skl(sz00))|~sQ114_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2059,f266])).
% 40.22/7.26 fof(f3398,plain,(
% 40.22/7.26 ~sP2_prd(sz00)|~sQ114_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2059,f291])).
% 40.22/7.26 fof(f3400,plain,(
% 40.22/7.26 $false|~sQ11_spl|~sQ114_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f3398,f349])).
% 40.22/7.26 fof(f3401,plain,(
% 40.22/7.26 ~sQ11_spl|~sQ114_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f3400])).
% 40.22/7.26 fof(f3404,plain,(
% 40.22/7.26 sQ11_spl|~sQ75_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1483,f348,f1270])).
% 40.22/7.26 fof(f3405,plain,(
% 40.22/7.26 sQ11_spl|~sQ19_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1339,f348,f386])).
% 40.22/7.26 fof(f3406,plain,(
% 40.22/7.26 sQ11_spl|~sQ23_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1346,f348,f414])).
% 40.22/7.26 fof(f3407,plain,(
% 40.22/7.26 sQ11_spl|~sQ45_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f1343,f348,f791])).
% 40.22/7.26 fof(f3435,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sdtasdt0(sz10,sz00)),sdtasdt0(sz10,smndt0(sz00)))|~sQ76_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f1274])).
% 40.22/7.26 fof(f3436,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),sdtasdt0(sz10,smndt0(sz00)))|~sQ76_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1692,f3435])).
% 40.22/7.26 fof(f3437,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),sdtasdt0(sz10,sz00))|~sQ76_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3436])).
% 40.22/7.26 fof(f3438,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),sz00)|~sQ76_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1692,f3437])).
% 40.22/7.26 fof(f3451,plain,(
% 40.22/7.26 aInteger0(sK18_skl(sz00))|~sQ20_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f390])).
% 40.22/7.26 fof(f3484,plain,(
% 40.22/7.26 isPrime0(sK18_skl(smndt0(smndt0(sz00))))|~sQ47_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f799])).
% 40.22/7.26 fof(f3485,plain,(
% 40.22/7.26 isPrime0(sK18_skl(smndt0(sz00)))|~sQ47_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3484])).
% 40.22/7.26 fof(f3486,plain,(
% 40.22/7.26 isPrime0(sK18_skl(sz00))|~sQ47_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3485])).
% 40.22/7.26 fof(f3493,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(smndt0(smndt0(sz00))),smndt0(smndt0(smndt0(sz00))))|~sQ62_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f1048])).
% 40.22/7.26 fof(f3494,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(smndt0(sz00)),smndt0(smndt0(smndt0(sz00))))|~sQ62_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3493])).
% 40.22/7.26 fof(f3495,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),smndt0(smndt0(smndt0(sz00))))|~sQ62_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3494])).
% 40.22/7.26 fof(f3496,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),smndt0(smndt0(sz00)))|~sQ62_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3495])).
% 40.22/7.26 fof(f3497,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),smndt0(sz00))|~sQ62_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3496])).
% 40.22/7.26 fof(f3498,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sz00),sz00)|~sQ62_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f3497])).
% 40.22/7.26 fof(f3507,plain,(
% 40.22/7.26 sQ110_spl|~sQ131_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f2892,f1963,f2468])).
% 40.22/7.26 fof(f3864,plain,(
% 40.22/7.26 ![X0,X1]: (sP2_prd(sK3_skl(sbsmnsldt0(xS),X0,X1))|aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),sK23_skl(sK3_skl(sbsmnsldt0(xS),X0,X1)))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X0,cS1395)|sbsmnsldt0(xS)=sdtbsmnsldt0(X1,X0)|~aSet0(sbsmnsldt0(xS))|~aInteger0(sK3_skl(sbsmnsldt0(xS),X0,X1))|~aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),X0))),
% 40.22/7.26 inference(resolution,[status(thm)],[f293,f141])).
% 40.22/7.26 fof(f3865,plain,(
% 40.22/7.26 ![X0,X1]: (sP2_prd(sK3_skl(sbsmnsldt0(xS),X0,X1))|aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),sK23_skl(sK3_skl(sbsmnsldt0(xS),X0,X1)))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X0,cS1395)|sbsmnsldt0(xS)=sdtbsmnsldt0(X1,X0)|~aSet0(sbsmnsldt0(xS))|~aInteger0(sK3_skl(sbsmnsldt0(xS),X0,X1))|~aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),X1))),
% 40.22/7.26 inference(resolution,[status(thm)],[f293,f140])).
% 40.22/7.26 fof(f3866,plain,(
% 40.22/7.26 ![X0]: (sP2_prd(sK2_skl(X0,sbsmnsldt0(xS)))|aElementOf0(sK2_skl(X0,sbsmnsldt0(xS)),sK23_skl(sK2_skl(X0,sbsmnsldt0(xS))))|~aSet0(sbsmnsldt0(xS))|aSubsetOf0(X0,sbsmnsldt0(xS))|~aSet0(X0))),
% 40.22/7.26 inference(resolution,[status(thm)],[f293,f128])).
% 40.22/7.26 fof(f3870,definition,(
% 40.22/7.26 ![X0,X1]: (sQ258_spl <=> (sP2_prd(sK3_skl(sbsmnsldt0(xS),X0,X1))|aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),sK23_skl(sK3_skl(sbsmnsldt0(xS),X0,X1)))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X0,cS1395)|sbsmnsldt0(xS)=sdtbsmnsldt0(X1,X0)|~aInteger0(sK3_skl(sbsmnsldt0(xS),X0,X1))|~aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),X0)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f3873,definition,(
% 40.22/7.26 sQ259_spl <=> (aSet0(sbsmnsldt0(xS)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f3875,plain,(
% 40.22/7.26 ~aSet0(sbsmnsldt0(xS))|sQ259_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f3873])).
% 40.22/7.26 fof(f3876,plain,(
% 40.22/7.26 sQ258_spl|~sQ259_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f3864,f3870,f3873])).
% 40.22/7.26 fof(f3877,definition,(
% 40.22/7.26 ![X0,X1]: (sQ260_spl <=> (sP2_prd(sK3_skl(sbsmnsldt0(xS),X0,X1))|aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),sK23_skl(sK3_skl(sbsmnsldt0(xS),X0,X1)))|~aSubsetOf0(X1,cS1395)|~aSubsetOf0(X0,cS1395)|sbsmnsldt0(xS)=sdtbsmnsldt0(X1,X0)|~aInteger0(sK3_skl(sbsmnsldt0(xS),X0,X1))|~aElementOf0(sK3_skl(sbsmnsldt0(xS),X0,X1),X1)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f3880,plain,(
% 40.22/7.26 sQ260_spl|~sQ259_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f3865,f3877,f3873])).
% 40.22/7.26 fof(f3881,definition,(
% 40.22/7.26 ![X0]: (sQ261_spl <=> (sP2_prd(sK2_skl(X0,sbsmnsldt0(xS)))|aElementOf0(sK2_skl(X0,sbsmnsldt0(xS)),sK23_skl(sK2_skl(X0,sbsmnsldt0(xS))))|aSubsetOf0(X0,sbsmnsldt0(xS))|~aSet0(X0)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f3884,plain,(
% 40.22/7.26 sQ261_spl|~sQ259_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f3866,f3881,f3873])).
% 40.22/7.26 fof(f3885,plain,(
% 40.22/7.26 $false|sQ259_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f3875,f263])).
% 40.22/7.26 fof(f3886,plain,(
% 40.22/7.26 sQ259_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f3885])).
% 40.22/7.26 fof(f4177,definition,(
% 40.22/7.26 sQ263_spl <=> (sK22_skl=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f4178,plain,(
% 40.22/7.26 sK22_skl=sz00|~sQ263_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f4177])).
% 40.22/7.26 fof(f4202,definition,(
% 40.22/7.26 ![X0]: (sQ268_spl <=> (~sP3_prd(sz10,X0)|~sz10=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f4203,plain,(
% 40.22/7.26 ![X0]: (~sP3_prd(sz10,X0)|~sz10=X0|~sQ268_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f4202])).
% 40.22/7.26 fof(f4206,definition,(
% 40.22/7.26 ![X0]: (sQ269_spl <=> (~sP3_prd(sz10,X0)|~sz00=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f4207,plain,(
% 40.22/7.26 ![X0]: (~sP3_prd(sz10,X0)|~sz00=X0|~sQ269_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f4206])).
% 40.22/7.26 fof(f4300,plain,(
% 40.22/7.26 sz00=smndt0(sK22_skl)|~sQ263_spl),
% 40.22/7.26 inference(backward_demodulation,[status(thm)],[f4178,f1312])).
% 40.22/7.26 fof(f4312,plain,(
% 40.22/7.26 sK22_skl=smndt0(sK22_skl)|~sQ263_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4178,f4300])).
% 40.22/7.26 fof(f4313,plain,(
% 40.22/7.26 sz10=sK22_skl|~sQ263_spl|~sQ99_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4178,f1911])).
% 40.22/7.26 fof(f4314,plain,(
% 40.22/7.26 $false|sQ9_spl|~sQ263_spl|~sQ99_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f4313,f340])).
% 40.22/7.26 fof(f4315,plain,(
% 40.22/7.26 sQ9_spl|~sQ263_spl|~sQ99_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f4314])).
% 40.22/7.26 fof(f4474,plain,(
% 40.22/7.26 ~sP2_prd(sz10)|~sQ135_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2517,f291])).
% 40.22/7.26 fof(f4476,plain,(
% 40.22/7.26 $false|~sQ17_spl|~sQ135_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f4474,f378])).
% 40.22/7.26 fof(f4477,plain,(
% 40.22/7.26 ~sQ17_spl|~sQ135_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f4476])).
% 40.22/7.26 fof(f4550,plain,(
% 40.22/7.26 ![X0]: (sP3_prd(X0,sz00)|aElementOf0(sK20_skl(sz00),xS))),
% 40.22/7.26 inference(resolution,[status(thm)],[f260,f48])).
% 40.22/7.26 fof(f4569,definition,(
% 40.22/7.26 sQ283_spl <=> (aElementOf0(sK20_skl(sz00),xS))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f4570,plain,(
% 40.22/7.26 aElementOf0(sK20_skl(sz00),xS)|~sQ283_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f4569])).
% 40.22/7.26 fof(f4572,plain,(
% 40.22/7.26 sQ110_spl|sQ283_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f4550,f1963,f4569])).
% 40.22/7.26 fof(f6156,plain,(
% 40.22/7.26 ![X0]: (~aInteger0(sz10)|~aInteger0(sz10)|~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz10,sz10,X0)|~aDivisorOf0(X0,sz00))),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f1704,f96])).
% 40.22/7.26 fof(f6158,definition,(
% 40.22/7.26 ![X0]: (sQ474_spl <=> (~aInteger0(X0)|X0=sz00|sdteqdtlpzmzozddtrp0(sz10,sz10,X0)|~aDivisorOf0(X0,sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6161,plain,(
% 40.22/7.26 ~sQ98_spl|sQ474_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6156,f1553,f6158])).
% 40.22/7.26 fof(f6297,plain,(
% 40.22/7.26 ~aInteger0(sz00)|~sz10=sz00|~sQ106_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f89,f1888])).
% 40.22/7.26 fof(f6301,plain,(
% 40.22/7.26 ~sQ94_spl|~sQ99_spl|~sQ106_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6297,f1538,f1556,f1887])).
% 40.22/7.26 fof(f6344,plain,(
% 40.22/7.26 ![X0]: (~aSubsetOf0(X0,cS1395)|sbsmnsldt0(xS)=stldt0(X0)|~aSet0(sbsmnsldt0(xS))|~aInteger0(sK9_skl(sbsmnsldt0(xS),X0))|aElementOf0(sK9_skl(sbsmnsldt0(xS),X0),X0)|sP2_prd(sK9_skl(sbsmnsldt0(xS),X0))|aElementOf0(sK9_skl(sbsmnsldt0(xS),X0),sK23_skl(sK9_skl(sbsmnsldt0(xS),X0))))),
% 40.22/7.26 inference(resolution,[status(thm)],[f178,f293])).
% 40.22/7.26 fof(f6345,definition,(
% 40.22/7.26 ![X0]: (sQ482_spl <=> (~aSubsetOf0(X0,cS1395)|sbsmnsldt0(xS)=stldt0(X0)|~aInteger0(sK9_skl(sbsmnsldt0(xS),X0))|aElementOf0(sK9_skl(sbsmnsldt0(xS),X0),X0)|sP2_prd(sK9_skl(sbsmnsldt0(xS),X0))|aElementOf0(sK9_skl(sbsmnsldt0(xS),X0),sK23_skl(sK9_skl(sbsmnsldt0(xS),X0)))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6348,plain,(
% 40.22/7.26 sQ482_spl|~sQ259_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6344,f6345,f3873])).
% 40.22/7.26 fof(f6365,plain,(
% 40.22/7.26 ~aElementOf0(sK22_skl,sbsmnsldt0(xS))|~sQ8_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f336,f270])).
% 40.22/7.26 fof(f6369,definition,(
% 40.22/7.26 sQ485_spl <=> (aSet0(stldt0(sbsmnsldt0(xS))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ485_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6371,plain,(
% 40.22/7.26 ~aSet0(stldt0(sbsmnsldt0(xS)))|sQ485_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f6369])).
% 40.22/7.26 fof(f6472,plain,(
% 40.22/7.26 $false|sQ93_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f1537,f2739])).
% 40.22/7.26 fof(f6473,plain,(
% 40.22/7.26 sQ93_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f6472])).
% 40.22/7.26 fof(f6650,plain,(
% 40.22/7.26 ~aInteger0(sz00)|aDivisorOf0(smndt0(sz10),sz00)|~aInteger0(smndt0(sz10))|smndt0(sz10)=sz00|~aInteger0(sz00)),
% 40.22/7.26 inference(resolution,[status(thm)],[f92,f1771])).
% 40.22/7.26 fof(f6655,plain,(
% 40.22/7.26 ~aInteger0(sz10)|aDivisorOf0(sz10,sz10)|~aInteger0(sz10)|sz10=sz00|~aInteger0(sz10)),
% 40.22/7.26 inference(resolution,[status(thm)],[f92,f448])).
% 40.22/7.26 fof(f6660,plain,(
% 40.22/7.26 ![X0]: (~aInteger0(X0)|aDivisorOf0(smndt0(sz10),X0)|~aInteger0(smndt0(sz10))|smndt0(sz10)=sz00|~aInteger0(sz00)|~sz00=X0)),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f1771,f92])).
% 40.22/7.26 fof(f6669,plain,(
% 40.22/7.26 ![X0]: (~aInteger0(X0)|aDivisorOf0(sz10,X0)|~aInteger0(sz10)|sz10=sz00|~aInteger0(sz10)|~sz10=X0)),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f448,f92])).
% 40.22/7.26 fof(f6671,definition,(
% 40.22/7.26 sQ518_spl <=> (aDivisorOf0(smndt0(sz10),sz00))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ518_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6672,plain,(
% 40.22/7.26 aDivisorOf0(smndt0(sz10),sz00)|~sQ518_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f6671])).
% 40.22/7.26 fof(f6674,plain,(
% 40.22/7.26 ~sQ94_spl|sQ518_spl|~sQ93_spl|sQ95_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6650,f1538,f6671,f1535,f1541])).
% 40.22/7.26 fof(f6680,definition,(
% 40.22/7.26 sQ520_spl <=> (aDivisorOf0(sK22_skl,sz00))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6681,plain,(
% 40.22/7.26 aDivisorOf0(sK22_skl,sz00)|~sQ520_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f6680])).
% 40.22/7.26 fof(f6682,plain,(
% 40.22/7.26 ~aDivisorOf0(sK22_skl,sz00)|sQ520_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f6680])).
% 40.22/7.26 fof(f6685,definition,(
% 40.22/7.26 sQ521_spl <=> (aDivisorOf0(sz10,sz10))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6686,plain,(
% 40.22/7.26 aDivisorOf0(sz10,sz10)|~sQ521_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f6685])).
% 40.22/7.26 fof(f6688,plain,(
% 40.22/7.26 ~sQ98_spl|sQ521_spl|sQ99_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6655,f1553,f6685,f1556])).
% 40.22/7.26 fof(f6696,definition,(
% 40.22/7.26 ![X0]: (sQ523_spl <=> (~aInteger0(X0)|aDivisorOf0(smndt0(sz10),X0)|~sz00=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6699,plain,(
% 40.22/7.26 sQ523_spl|~sQ93_spl|sQ95_spl|~sQ94_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6660,f6696,f1535,f1541,f1538])).
% 40.22/7.26 fof(f6717,definition,(
% 40.22/7.26 ![X0]: (sQ527_spl <=> (~aInteger0(X0)|aDivisorOf0(sz10,X0)|~sz10=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ527_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6720,plain,(
% 40.22/7.26 sQ527_spl|~sQ98_spl|sQ99_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6669,f6717,f1553,f1556])).
% 40.22/7.26 fof(f6762,plain,(
% 40.22/7.26 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|~X1=sK22_skl|~sQ263_spl)),
% 40.22/7.26 inference(backward_demodulation,[status(thm)],[f4178,f89])).
% 40.22/7.26 fof(f6843,plain,(
% 40.22/7.26 $false|~sQ8_spl|sQ141_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f2703,f2124])).
% 40.22/7.26 fof(f6844,plain,(
% 40.22/7.26 ~sQ8_spl|sQ141_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f6843])).
% 40.22/7.26 fof(f6892,plain,(
% 40.22/7.26 ~aInteger0(sz10)|~isPrime0(sz10)|~sz10=sz10|~sQ521_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f6686,f111])).
% 40.22/7.26 fof(f6894,plain,(
% 40.22/7.26 ~aInteger0(sz10)|sdtasdt0(sz10,sK0_skl(sz10,sz10))=sz10|~sQ521_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f6686,f91])).
% 40.22/7.26 fof(f6895,plain,(
% 40.22/7.26 ~aInteger0(sz10)|aInteger0(sK0_skl(sz10,sz10))|~sQ521_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f6686,f90])).
% 40.22/7.26 fof(f6898,definition,(
% 40.22/7.26 sQ528_spl <=> (sz10=sz10)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ528_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6900,plain,(
% 40.22/7.26 ~sz10=sz10|sQ528_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f6898])).
% 40.22/7.26 fof(f6901,plain,(
% 40.22/7.26 ~sQ98_spl|~sQ150_spl|~sQ528_spl|~sQ521_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6892,f1553,f2845,f6898,f6685])).
% 40.22/7.26 fof(f6906,definition,(
% 40.22/7.26 sQ530_spl <=> (sdtasdt0(sz10,sK0_skl(sz10,sz10))=sz10)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6909,plain,(
% 40.22/7.26 ~sQ98_spl|sQ530_spl|~sQ521_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6894,f1553,f6906,f6685])).
% 40.22/7.26 fof(f6910,definition,(
% 40.22/7.26 sQ531_spl <=> (aInteger0(sK0_skl(sz10,sz10)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ531_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f6913,plain,(
% 40.22/7.26 ~sQ98_spl|sQ531_spl|~sQ521_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f6895,f1553,f6910,f6685])).
% 40.22/7.26 fof(f7196,plain,(
% 40.22/7.26 sz00=sdtpldt0(smndt0(sz10),sz10)),
% 40.22/7.26 inference(resolution,[status(thm)],[f65,f49])).
% 40.22/7.26 fof(f7198,plain,(
% 40.22/7.26 sz00=sdtpldt0(sz00,sz10)|~sQ95_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1542,f7196])).
% 40.22/7.26 fof(f7201,plain,(
% 40.22/7.26 sdtpldt0(sz00,smndt0(sz00))=sz00),
% 40.22/7.26 inference(resolution,[status(thm)],[f64,f48])).
% 40.22/7.26 fof(f7215,plain,(
% 40.22/7.26 sdtpldt0(sz00,sz00)=sz00),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f7201])).
% 40.22/7.26 fof(f7503,plain,(
% 40.22/7.26 ~aInteger0(sz10)|~isPrime0(sK18_skl(sz10))|~sz10=sz10|~sQ67_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f1068,f111])).
% 40.22/7.26 fof(f7508,plain,(
% 40.22/7.26 ~sQ98_spl|~sQ37_spl|~sQ528_spl|~sQ67_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f7503,f1553,f533,f6898,f1067])).
% 40.22/7.26 fof(f7522,plain,(
% 40.22/7.26 $false|sQ528_spl),
% 40.22/7.26 inference(trivial_equality_resolution,[status(thm)],[f6900])).
% 40.22/7.26 fof(f7523,plain,(
% 40.22/7.26 sQ528_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f7522])).
% 40.22/7.26 fof(f7567,plain,(
% 40.22/7.26 $false|~sQ8_spl|~sQ116_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f2172,f6365])).
% 40.22/7.26 fof(f7568,plain,(
% 40.22/7.26 ~sQ8_spl|~sQ116_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f7567])).
% 40.22/7.26 fof(f7839,plain,(
% 40.22/7.26 sz10=sz00|~sQ95_spl),
% 40.22/7.26 inference(backward_demodulation,[status(thm)],[f7198,f1702])).
% 40.22/7.26 fof(f7840,plain,(
% 40.22/7.26 sQ99_spl|~sQ95_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f7839,f1556,f1541])).
% 40.22/7.26 fof(f8209,plain,(
% 40.22/7.26 isPrime0(sK18_skl(sK22_skl))|~sQ263_spl|~sQ129_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4312,f2355])).
% 40.22/7.26 fof(f8225,definition,(
% 40.22/7.26 sQ613_spl <=> (sP3_prd(sK18_skl(sK22_skl),sK22_skl))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f8227,plain,(
% 40.22/7.26 ~sP3_prd(sK18_skl(sK22_skl),sK22_skl)|sQ613_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f8225])).
% 40.22/7.26 fof(f8229,plain,(
% 40.22/7.26 $false|~sQ115_spl|sQ613_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f8227,f2169])).
% 40.22/7.26 fof(f8230,plain,(
% 40.22/7.26 ~sQ115_spl|sQ613_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f8229])).
% 40.22/7.26 fof(f8276,definition,(
% 40.22/7.26 sQ618_spl <=> (sK22_skl=sK22_skl)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f8278,plain,(
% 40.22/7.26 ~sK22_skl=sK22_skl|sQ618_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f8276])).
% 40.22/7.26 fof(f8738,plain,(
% 40.22/7.26 ![X0]: (~sz10=X0|isPrime0(sz10)|~sQ268_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f4203,f303])).
% 40.22/7.26 fof(f8740,definition,(
% 40.22/7.26 ![X0]: (sQ631_spl <=> (~sz10=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f8741,plain,(
% 40.22/7.26 ![X0]: (~sz10=X0|~sQ631_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f8740])).
% 40.22/7.26 fof(f8743,plain,(
% 40.22/7.26 sQ631_spl|sQ150_spl|~sQ268_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f8738,f8740,f2845,f4202])).
% 40.22/7.26 fof(f8744,plain,(
% 40.22/7.26 $false|~sQ631_spl),
% 40.22/7.26 inference(backward_subsumption_resolution,[status(thm)],[f1702,f8741])).
% 40.22/7.26 fof(f8747,plain,(
% 40.22/7.26 ~sQ631_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f8744])).
% 40.22/7.26 fof(f8873,plain,(
% 40.22/7.26 ~aInteger0(sz00)|sdtasdt0(smndt0(sz10),sK0_skl(smndt0(sz10),sz00))=sz00|~sQ518_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f6672,f91])).
% 40.22/7.26 fof(f8874,plain,(
% 40.22/7.26 ~aInteger0(sz00)|aInteger0(sK0_skl(smndt0(sz10),sz00))|~sQ518_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f6672,f90])).
% 40.22/7.26 fof(f8877,definition,(
% 40.22/7.26 sQ632_spl <=> (sdtasdt0(smndt0(sz10),sK0_skl(smndt0(sz10),sz00))=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f8880,plain,(
% 40.22/7.26 ~sQ94_spl|sQ632_spl|~sQ518_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f8873,f1538,f8877,f6671])).
% 40.22/7.26 fof(f8881,definition,(
% 40.22/7.26 sQ633_spl <=> (aInteger0(sK0_skl(smndt0(sz10),sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f8884,plain,(
% 40.22/7.26 ~sQ94_spl|sQ633_spl|~sQ518_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f8874,f1538,f8881,f6671])).
% 40.22/7.26 fof(f8949,plain,(
% 40.22/7.26 ![X0]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(sz00)|~aDivisorOf0(X0,sz00)|aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ6_spl)),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f7215,f1671])).
% 40.22/7.26 fof(f8952,definition,(
% 40.22/7.26 ![X0]: (sQ634_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aDivisorOf0(X0,sz00)|aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ634_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f8955,plain,(
% 40.22/7.26 sQ634_spl|~sQ94_spl|~sQ6_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f8949,f8952,f1538,f327])).
% 40.22/7.26 fof(f9240,plain,(
% 40.22/7.26 ![X0]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(sz10)|~aDivisorOf0(X0,sz10)|aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ6_spl)),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f1703,f1671])).
% 40.22/7.26 fof(f9241,definition,(
% 40.22/7.26 ![X0]: (sQ636_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aDivisorOf0(X0,sz10)|aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f9244,plain,(
% 40.22/7.26 sQ636_spl|~sQ98_spl|~sQ6_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f9240,f9241,f1553,f327])).
% 40.22/7.26 fof(f9939,plain,(
% 40.22/7.26 ~aInteger0(sz00)|~sK22_skl=sz00|~sQ520_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f89,f6681])).
% 40.22/7.26 fof(f9942,plain,(
% 40.22/7.26 ~aInteger0(sz10)|~sz10=sz00|~sQ521_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f89,f6686])).
% 40.22/7.26 fof(f9947,plain,(
% 40.22/7.26 ~sQ94_spl|~sQ263_spl|~sQ520_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f9939,f1538,f4177,f6680])).
% 40.22/7.26 fof(f9950,plain,(
% 40.22/7.26 ~sQ98_spl|~sQ99_spl|~sQ521_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f9942,f1553,f1556,f6685])).
% 40.22/7.26 fof(f10521,plain,(
% 40.22/7.26 ~aInteger0(sK18_skl(sz00))|sQ20_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f391])).
% 40.22/7.26 fof(f10523,plain,(
% 40.22/7.26 ~aInteger0(sK18_skl(sdtasdt0(sz10,sz00)))|sQ80_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f1291])).
% 40.22/7.26 fof(f10524,plain,(
% 40.22/7.26 ~aInteger0(sK18_skl(sz00))|sQ80_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1692,f10523])).
% 40.22/7.26 fof(f10557,plain,(
% 40.22/7.26 ~aInteger0(sK19_skl(sz00))|sQ30_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f501])).
% 40.22/7.26 fof(f10559,plain,(
% 40.22/7.26 ~aInteger0(sK19_skl(sdtasdt0(sz10,sz00)))|sQ79_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f1287])).
% 40.22/7.26 fof(f10560,plain,(
% 40.22/7.26 ~aInteger0(sK19_skl(sz00))|sQ79_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1692,f10559])).
% 40.22/7.26 fof(f10652,plain,(
% 40.22/7.26 ![X0,X1]: (~aElementOf0(X0,xS)|~aInteger0(X1)|~aDivisorOf0(sK15_skl(X0),sdtpldt0(X1,sz00))|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0))))),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f233])).
% 40.22/7.26 fof(f10655,plain,(
% 40.22/7.26 ![X0]: (~aElementOf0(X0,xS)|~aInteger0(sz10)|~aDivisorOf0(sK15_skl(X0),sz10)|aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0))))),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f1703,f10652])).
% 40.22/7.26 fof(f10657,plain,(
% 40.22/7.26 ![X0]: (~aElementOf0(X0,xS)|~aInteger0(sz00)|~aDivisorOf0(sK15_skl(X0),sz00)|aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0))))),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f7215,f10652])).
% 40.22/7.26 fof(f10658,definition,(
% 40.22/7.26 ![X0]: (sQ769_spl <=> (~aElementOf0(X0,xS)|~aDivisorOf0(sK15_skl(X0),sz10)|aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0)))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ769_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f10661,plain,(
% 40.22/7.26 sQ769_spl|~sQ98_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f10655,f10658,f1553])).
% 40.22/7.26 fof(f10666,definition,(
% 40.22/7.26 ![X0]: (sQ771_spl <=> (~aElementOf0(X0,xS)|~aDivisorOf0(sK15_skl(X0),sz00)|aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0)))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ771_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f10669,plain,(
% 40.22/7.26 sQ771_spl|~sQ94_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f10657,f10666,f1538])).
% 40.22/7.26 fof(f10696,plain,(
% 40.22/7.26 $false|sQ485_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f6371,f268])).
% 40.22/7.26 fof(f10697,plain,(
% 40.22/7.26 sQ485_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f10696])).
% 40.22/7.26 fof(f11479,plain,(
% 40.22/7.26 aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS)))|aElementOf0(sK22_skl,sbsmnsldt0(xS))|~sQ141_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2702,f271])).
% 40.22/7.26 fof(f11482,plain,(
% 40.22/7.26 sP2_prd(sK22_skl)|aDivisorOf0(sK18_skl(sK22_skl),sK22_skl)|~sQ141_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2702,f258])).
% 40.22/7.26 fof(f11498,plain,(
% 40.22/7.26 sP2_prd(sK22_skl)|isPrime0(sK18_skl(sK22_skl))|~sQ141_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2702,f259])).
% 40.22/7.26 fof(f11510,plain,(
% 40.22/7.26 sQ8_spl|sQ116_spl|~sQ141_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f11479,f335,f2171,f2701])).
% 40.22/7.26 fof(f11513,plain,(
% 40.22/7.26 sQ13_spl|sQ118_spl|~sQ141_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f11482,f357,f2179,f2701])).
% 40.22/7.26 fof(f11515,plain,(
% 40.22/7.26 sQ13_spl|sQ120_spl|~sQ141_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f11498,f357,f2187,f2701])).
% 40.22/7.26 fof(f11558,plain,(
% 40.22/7.26 ~aElementOf0(sK22_skl,sbsmnsldt0(xS))|~sQ9_spl|sQ135_spl),
% 40.22/7.26 inference(backward_demodulation,[status(thm)],[f339,f2518])).
% 40.22/7.26 fof(f11593,plain,(
% 40.22/7.26 ~sQ116_spl|~sQ9_spl|sQ135_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f11558,f2171,f338,f2516])).
% 40.22/7.26 fof(f11794,plain,(
% 40.22/7.26 sQ120_spl|~sQ263_spl|~sQ129_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f8209,f2187,f4177,f2354])).
% 40.22/7.26 fof(f11895,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sK22_skl),sz00)|~sQ263_spl|~sQ76_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4178,f3438])).
% 40.22/7.26 fof(f11896,plain,(
% 40.22/7.26 aDivisorOf0(sK18_skl(sK22_skl),sK22_skl)|~sQ263_spl|~sQ76_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4178,f11895])).
% 40.22/7.26 fof(f11918,plain,(
% 40.22/7.26 isPrime0(sK18_skl(sK22_skl))|~sQ263_spl|~sQ47_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4178,f3486])).
% 40.22/7.26 fof(f12309,plain,(
% 40.22/7.26 ![X0,X1]: (~sP2_prd(X0)|~aElementOf0(X0,X1)|~sQ1_spl)),
% 40.22/7.26 inference(backward_subsumption_resolution,[status(thm)],[f290,f308])).
% 40.22/7.26 fof(f12597,plain,(
% 40.22/7.26 aDivisorOf0(sK1_skl(sK22_skl),sK22_skl)|sK22_skl=sz10|sK22_skl=smndt0(sz10)|~sQ141_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f113,f2702])).
% 40.22/7.26 fof(f12626,definition,(
% 40.22/7.26 sQ887_spl <=> (aDivisorOf0(sK1_skl(sK22_skl),sK22_skl))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ887_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f12627,plain,(
% 40.22/7.26 aDivisorOf0(sK1_skl(sK22_skl),sK22_skl)|~sQ887_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f12626])).
% 40.22/7.26 fof(f12629,plain,(
% 40.22/7.26 sQ887_spl|sQ9_spl|sQ10_spl|~sQ141_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f12597,f12626,f338,f341,f2701])).
% 40.22/7.26 fof(f12656,plain,(
% 40.22/7.26 ~isPrime0(sK18_skl(sK22_skl))|~sQ263_spl|sQ129_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f4312,f2356])).
% 40.22/7.26 fof(f12680,plain,(
% 40.22/7.26 $false|sQ129_spl|~sQ263_spl|~sQ47_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f11918,f12656])).
% 40.22/7.26 fof(f12681,plain,(
% 40.22/7.26 sQ129_spl|~sQ263_spl|~sQ47_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f12680])).
% 40.22/7.26 fof(f12708,plain,(
% 40.22/7.26 ![X0]: (~sP2_prd(X0)|~sQ1_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f12309,f308])).
% 40.22/7.26 fof(f13680,plain,(
% 40.22/7.26 isPrime0(sK1_skl(sK22_skl))|sK22_skl=sz10|sK22_skl=smndt0(sz10)|~sQ141_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f114,f2702])).
% 40.22/7.26 fof(f13694,definition,(
% 40.22/7.26 sQ941_spl <=> (isPrime0(sK1_skl(sK22_skl)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ941_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f13697,plain,(
% 40.22/7.26 sQ941_spl|sQ9_spl|sQ10_spl|~sQ141_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f13680,f13694,f338,f341,f2701])).
% 40.22/7.26 fof(f13752,plain,(
% 40.22/7.26 ~aInteger0(sz10)|~sz10=sK22_skl|~sQ263_spl|~sQ521_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f6762,f6686])).
% 40.22/7.26 fof(f13755,plain,(
% 40.22/7.26 ~sQ98_spl|~sQ9_spl|~sQ263_spl|~sQ521_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f13752,f1553,f338,f4177,f6685])).
% 40.22/7.26 fof(f13868,definition,(
% 40.22/7.26 ![X0,X1]: (sQ962_spl <=> (~aInteger0(X0)|~aInteger0(X1)|~sdteqdtlpzmzozddtrp0(X0,X1,sz10)|sdteqdtlpzmzozddtrp0(X0,X1,sz10)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ962_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f14280,plain,(
% 40.22/7.26 ~sP3_prd(sK18_skl(sK22_skl),sK22_skl)|~isPrime0(sK18_skl(sK22_skl))|~sQ263_spl|~sQ76_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f11896,f298])).
% 40.22/7.26 fof(f14286,plain,(
% 40.22/7.26 ~sQ613_spl|~sQ120_spl|~sQ263_spl|~sQ76_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f14280,f8225,f2187,f4177,f1273])).
% 40.22/7.26 fof(f14311,plain,(
% 40.22/7.26 ~sQ32_spl|sQ79_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f10560,f507,f1285])).
% 40.22/7.26 fof(f14313,plain,(
% 40.22/7.26 aDivisorOf0(sK1_skl(sz00),sz00)|sz00=sz10|sz00=smndt0(sz10)),
% 40.22/7.26 inference(resolution,[status(thm)],[f48,f113])).
% 40.22/7.26 fof(f14315,plain,(
% 40.22/7.26 sQ122_spl|sQ99_spl|sQ95_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f14313,f2201,f1556,f1541])).
% 40.22/7.26 fof(f14388,plain,(
% 40.22/7.26 aInteger0(sK22_skl)|~sQ10_spl),
% 40.22/7.26 inference(backward_demodulation,[status(thm)],[f342,f2739])).
% 40.22/7.26 fof(f14395,plain,(
% 40.22/7.26 sQ141_spl|~sQ10_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f14388,f2701,f341])).
% 40.22/7.26 fof(f14410,plain,(
% 40.22/7.26 $false|sQ80_spl|~sQ20_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f3451,f10524])).
% 40.22/7.26 fof(f14411,plain,(
% 40.22/7.26 sQ80_spl|~sQ20_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f14410])).
% 40.22/7.26 fof(f14412,plain,(
% 40.22/7.26 ~sQ32_spl|sQ30_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f10557,f507,f499])).
% 40.22/7.26 fof(f14438,plain,(
% 40.22/7.26 ![X0,X1]: (~aInteger0(X0)|~aDivisorOf0(X1,X0)|~isPrime0(X1)|~X0=sK22_skl|~sQ10_spl)),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f342,f112])).
% 40.22/7.26 fof(f14883,plain,(
% 40.22/7.26 ~sP3_prd(sK1_skl(sK22_skl),sK22_skl)|~isPrime0(sK1_skl(sK22_skl))|~sQ887_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f12627,f298])).
% 40.22/7.26 fof(f14886,definition,(
% 40.22/7.26 sQ1022_spl <=> (sP3_prd(sK1_skl(sK22_skl),sK22_skl))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1022_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f14888,plain,(
% 40.22/7.26 ~sP3_prd(sK1_skl(sK22_skl),sK22_skl)|sQ1022_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f14886])).
% 40.22/7.26 fof(f14889,plain,(
% 40.22/7.26 ~sQ1022_spl|~sQ941_spl|~sQ887_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f14883,f14886,f13694,f12626])).
% 40.22/7.26 fof(f14890,plain,(
% 40.22/7.26 $false|~sQ115_spl|sQ1022_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f14888,f2169])).
% 40.22/7.26 fof(f14891,plain,(
% 40.22/7.26 ~sQ115_spl|sQ1022_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f14890])).
% 40.22/7.26 fof(f15444,plain,(
% 40.22/7.26 aDivisorOf0(sK22_skl,sz00)|~sQ10_spl|~sQ518_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f342,f6672])).
% 40.22/7.26 fof(f15473,plain,(
% 40.22/7.26 $false|~sQ10_spl|~sQ518_spl|sQ520_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f6682,f15444])).
% 40.22/7.26 fof(f15474,plain,(
% 40.22/7.26 ~sQ10_spl|~sQ518_spl|sQ520_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f15473])).
% 40.22/7.26 fof(f15656,definition,(
% 40.22/7.26 ![X0]: (sQ1096_spl <=> (sP0_prd(sz00,X0,sK20_skl(sz00))|~aElementOf0(sz00,X0)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1096_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f15660,plain,(
% 40.22/7.26 ~aElementOf0(sz00,sK20_skl(smndt0(sz00)))|sQ133_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f2477])).
% 40.22/7.26 fof(f15661,plain,(
% 40.22/7.26 ~aElementOf0(sz00,sK20_skl(sz00))|sQ133_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f1312,f15660])).
% 40.22/7.26 fof(f15796,plain,(
% 40.22/7.26 ~aInteger0(sz00)|sdtasdt0(sK1_skl(sz00),sK0_skl(sK1_skl(sz00),sz00))=sz00|~sQ122_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2202,f91])).
% 40.22/7.26 fof(f15797,plain,(
% 40.22/7.26 ~aInteger0(sz00)|aInteger0(sK0_skl(sK1_skl(sz00),sz00))|~sQ122_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2202,f90])).
% 40.22/7.26 fof(f15798,plain,(
% 40.22/7.26 ~aInteger0(sz00)|aInteger0(sK1_skl(sz00))|~sQ122_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2202,f88])).
% 40.22/7.26 fof(f15801,plain,(
% 40.22/7.26 ~sP3_prd(sK1_skl(sz00),sz00)|~isPrime0(sK1_skl(sz00))|~sQ122_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f2202,f298])).
% 40.22/7.26 fof(f15802,definition,(
% 40.22/7.26 sQ1120_spl <=> (sdtasdt0(sK1_skl(sz00),sK0_skl(sK1_skl(sz00),sz00))=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1120_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f15805,plain,(
% 40.22/7.26 ~sQ94_spl|sQ1120_spl|~sQ122_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f15796,f1538,f15802,f2201])).
% 40.22/7.26 fof(f15806,definition,(
% 40.22/7.26 sQ1121_spl <=> (aInteger0(sK0_skl(sK1_skl(sz00),sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1121_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f15809,plain,(
% 40.22/7.26 ~sQ94_spl|sQ1121_spl|~sQ122_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f15797,f1538,f15806,f2201])).
% 40.22/7.26 fof(f15810,definition,(
% 40.22/7.26 sQ1122_spl <=> (aInteger0(sK1_skl(sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1122_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f15813,plain,(
% 40.22/7.26 ~sQ94_spl|sQ1122_spl|~sQ122_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f15798,f1538,f15810,f2201])).
% 40.22/7.26 fof(f15816,definition,(
% 40.22/7.26 sQ1123_spl <=> (sP3_prd(sK1_skl(sz00),sz00))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1123_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f15818,plain,(
% 40.22/7.26 ~sP3_prd(sK1_skl(sz00),sz00)|sQ1123_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f15816])).
% 40.22/7.26 fof(f15819,plain,(
% 40.22/7.26 ~sQ1123_spl|~sQ123_spl|~sQ122_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f15801,f15816,f2206,f2201])).
% 40.22/7.26 fof(f15820,plain,(
% 40.22/7.26 $false|~sQ110_spl|sQ1123_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f15818,f1964])).
% 40.22/7.26 fof(f15821,plain,(
% 40.22/7.26 ~sQ110_spl|sQ1123_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f15820])).
% 40.22/7.26 fof(f15927,plain,(
% 40.22/7.26 ![X0]: (sP0_prd(sz00,X0,sK20_skl(sz00))|~aInteger0(sz00)|~aElementOf0(sz00,X0)|~sQ111_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f1967,f281])).
% 40.22/7.26 fof(f15931,plain,(
% 40.22/7.26 sQ1096_spl|~sQ94_spl|~sQ111_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f15927,f15656,f1538,f1966])).
% 40.22/7.26 fof(f16054,definition,(
% 40.22/7.26 ![X0]: (sQ1134_spl <=> (~sz00=X0))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1134_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f16055,plain,(
% 40.22/7.26 ![X0]: (~sz00=X0|~sQ1134_spl)),
% 40.22/7.26 inference(component_clause,[status(thm)],[f16054])).
% 40.22/7.26 fof(f16058,plain,(
% 40.22/7.26 $false|~sQ1134_spl),
% 40.22/7.26 inference(backward_subsumption_resolution,[status(thm)],[f1691,f16055])).
% 40.22/7.26 fof(f16064,plain,(
% 40.22/7.26 ~sQ1134_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f16058])).
% 40.22/7.26 fof(f16080,plain,(
% 40.22/7.26 ![X0]: (~sz00=X0|isPrime0(sz10)|~sQ269_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f4207,f303])).
% 40.22/7.26 fof(f16081,plain,(
% 40.22/7.26 sQ1134_spl|sQ150_spl|~sQ269_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f16080,f16054,f2845,f4206])).
% 40.22/7.26 fof(f16129,plain,(
% 40.22/7.26 $false|~sQ1_spl|~sQ17_spl),
% 40.22/7.26 inference(backward_subsumption_resolution,[status(thm)],[f378,f12708])).
% 40.22/7.26 fof(f16148,plain,(
% 40.22/7.26 ~sQ1_spl|~sQ17_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f16129])).
% 40.22/7.26 fof(f16240,plain,(
% 40.22/7.26 ~aInteger0(sz00)|sdtasdt0(sK18_skl(sz00),sK0_skl(sK18_skl(sz00),sz00))=sz00|~sQ62_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f3498,f91])).
% 40.22/7.26 fof(f16241,plain,(
% 40.22/7.26 ~aInteger0(sz00)|aInteger0(sK0_skl(sK18_skl(sz00),sz00))|~sQ62_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f3498,f90])).
% 40.22/7.26 fof(f16245,plain,(
% 40.22/7.26 ~sP3_prd(sK18_skl(sz00),sz00)|~isPrime0(sK18_skl(sz00))|~sQ62_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f3498,f298])).
% 40.22/7.26 fof(f16246,definition,(
% 40.22/7.26 sQ1147_spl <=> (sdtasdt0(sK18_skl(sz00),sK0_skl(sK18_skl(sz00),sz00))=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1147_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f16249,plain,(
% 40.22/7.26 ~sQ94_spl|sQ1147_spl|~sQ62_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f16240,f1538,f16246,f1047])).
% 40.22/7.26 fof(f16250,definition,(
% 40.22/7.26 sQ1148_spl <=> (aInteger0(sK0_skl(sK18_skl(sz00),sz00)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1148_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f16253,plain,(
% 40.22/7.26 ~sQ94_spl|sQ1148_spl|~sQ62_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f16241,f1538,f16250,f1047])).
% 40.22/7.26 fof(f16257,definition,(
% 40.22/7.26 sQ1149_spl <=> (sP3_prd(sK18_skl(sz00),sz00))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1149_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f16260,plain,(
% 40.22/7.26 ~sQ1149_spl|~sQ38_spl|~sQ62_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f16245,f16257,f537,f1047])).
% 40.22/7.26 fof(f16297,plain,(
% 40.22/7.26 aInteger0(sK15_skl(sK20_skl(sz00)))|~sQ283_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f223,f4570])).
% 40.22/7.26 fof(f16301,plain,(
% 40.22/7.26 isPrime0(sK15_skl(sK20_skl(sz00)))|~sQ283_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f225,f4570])).
% 40.22/7.26 fof(f17455,plain,(
% 40.22/7.26 ~sK15_skl(sK20_skl(sz00))=sz00|~sQ283_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f224,f4570])).
% 40.22/7.26 fof(f17811,plain,(
% 40.22/7.26 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(sz10)|sz10=sz00|~aInteger0(sz10)|sz10=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,sz10)|sdteqdtlpzmzozddtrp0(X0,X1,sz10))),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f448,f104])).
% 40.22/7.26 fof(f17827,plain,(
% 40.22/7.26 sQ962_spl|~sQ98_spl|sQ99_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f17811,f13868,f1553,f1556])).
% 40.22/7.26 fof(f18027,plain,(
% 40.22/7.26 ![X0]: (sP0_prd(sz00,X0,sbsmnsldt0(xS))|~aInteger0(sz00)|~aElementOf0(sz00,X0)|~sQ114_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f2059,f281])).
% 40.22/7.26 fof(f18037,definition,(
% 40.22/7.26 ![X0]: (sQ1347_spl <=> (sP0_prd(sz00,X0,sbsmnsldt0(xS))|~aElementOf0(sz00,X0)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1347_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f18040,plain,(
% 40.22/7.26 sQ1347_spl|~sQ94_spl|~sQ114_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f18027,f18037,f1538,f2058])).
% 40.22/7.26 fof(f18047,plain,(
% 40.22/7.26 ![X0]: (sP0_prd(sz00,X0,sK21_skl(sz00))|~aInteger0(sz00)|~aElementOf0(sz00,X0)|~sQ114_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f3397,f281])).
% 40.22/7.26 fof(f18066,definition,(
% 40.22/7.26 ![X0]: (sQ1353_spl <=> (sP0_prd(sz00,X0,sK21_skl(sz00))|~aElementOf0(sz00,X0)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1353_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f18069,plain,(
% 40.22/7.26 sQ1353_spl|~sQ94_spl|~sQ114_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f18047,f18066,f1538,f2058])).
% 40.22/7.26 fof(f18460,definition,(
% 40.22/7.26 sQ1399_spl <=> (sK18_skl(sz00)=sz10)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1399_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f18461,plain,(
% 40.22/7.26 sK18_skl(sz00)=sz10|~sQ1399_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f18460])).
% 40.22/7.26 fof(f18470,definition,(
% 40.22/7.26 sQ1402_spl <=> (sK1_skl(sz00)=sz10)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1402_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f18471,plain,(
% 40.22/7.26 sK1_skl(sz00)=sz10|~sQ1402_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f18470])).
% 40.22/7.26 fof(f18763,plain,(
% 40.22/7.26 isPrime0(sz10)|~sQ1402_spl|~sQ123_spl),
% 40.22/7.26 inference(forward_demodulation,[status(thm)],[f18471,f2207])).
% 40.22/7.26 fof(f18764,plain,(
% 40.22/7.26 $false|sQ150_spl|~sQ1402_spl|~sQ123_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f18763,f2847])).
% 40.22/7.26 fof(f18765,plain,(
% 40.22/7.26 sQ150_spl|~sQ1402_spl|~sQ123_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f18764])).
% 40.22/7.26 fof(f18915,plain,(
% 40.22/7.26 ![X0,X1,X2]: (~aElementOf0(X0,xS)|~aInteger0(X1)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0)))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(sK15_skl(X0))|sK15_skl(X0)=sz00|~aInteger0(sz00)|~sdteqdtlpzmzozddtrp0(X1,X2,sK15_skl(X0))|~sdteqdtlpzmzozddtrp0(X2,sz00,sK15_skl(X0)))),
% 40.22/7.26 inference(resolution,[status(thm)],[f234,f102])).
% 40.22/7.26 fof(f18916,definition,(
% 40.22/7.26 ![X0,X1,X2]: (sQ1439_spl <=> (~aElementOf0(X0,xS)|~aInteger0(X1)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(X0)))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(sK15_skl(X0))|sK15_skl(X0)=sz00|~sdteqdtlpzmzozddtrp0(X1,X2,sK15_skl(X0))|~sdteqdtlpzmzozddtrp0(X2,sz00,sK15_skl(X0))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1439_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f18919,plain,(
% 40.22/7.26 sQ1439_spl|~sQ94_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f18915,f18916,f1538])).
% 40.22/7.26 fof(f19302,plain,(
% 40.22/7.26 ~sP2_prd(sK22_skl)|~sQ116_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f291,f2172])).
% 40.22/7.26 fof(f19304,plain,(
% 40.22/7.26 $false|~sQ13_spl|~sQ116_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f19302,f358])).
% 40.22/7.26 fof(f19305,plain,(
% 40.22/7.26 ~sQ13_spl|~sQ116_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f19304])).
% 40.22/7.26 fof(f19808,plain,(
% 40.22/7.26 ![X0,X1,X2]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X0)|X0=sz00|~aInteger0(sz00)|~sdteqdtlpzmzozddtrp0(X1,X2,X0)|~sdteqdtlpzmzozddtrp0(X2,sz00,X0)|~sQ7_spl)),
% 40.22/7.26 inference(resolution,[status(thm)],[f332,f102])).
% 40.22/7.26 fof(f19809,definition,(
% 40.22/7.26 ![X0,X1,X2]: (sQ1486_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~aInteger0(X1)|~aInteger0(X2)|~aInteger0(X0)|X0=sz00|~sdteqdtlpzmzozddtrp0(X1,X2,X0)|~sdteqdtlpzmzozddtrp0(X2,sz00,X0)))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1486_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f19812,plain,(
% 40.22/7.26 sQ1486_spl|~sQ94_spl|~sQ7_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f19808,f19809,f1538,f331])).
% 40.22/7.26 fof(f20561,plain,(
% 40.22/7.26 ~aInteger0(sK1_skl(sz00))|sK1_skl(sz00)=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK1_skl(sz00)))|~sQ0_spl|~sQ123_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f305,f2207])).
% 40.22/7.26 fof(f20562,plain,(
% 40.22/7.26 ~aInteger0(sK15_skl(sK20_skl(sz00)))|sK15_skl(sK20_skl(sz00))=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(sK20_skl(sz00))))|~sQ0_spl|~sQ283_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f305,f16301])).
% 40.22/7.26 fof(f20564,plain,(
% 40.22/7.26 ~aInteger0(sK18_skl(sz00))|sK18_skl(sz00)=sz00|aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK18_skl(sz00)))|~sQ0_spl|~sQ38_spl),
% 40.22/7.26 inference(resolution,[status(thm)],[f305,f538])).
% 40.22/7.26 fof(f20580,definition,(
% 40.22/7.26 sQ1576_spl <=> (sK1_skl(sz00)=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1576_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20583,definition,(
% 40.22/7.26 sQ1577_spl <=> (aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK1_skl(sz00))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1577_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20586,plain,(
% 40.22/7.26 ~sQ1122_spl|sQ1576_spl|sQ1577_spl|~sQ0_spl|~sQ123_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f20561,f15810,f20580,f20583,f304,f2206])).
% 40.22/7.26 fof(f20587,definition,(
% 40.22/7.26 sQ1578_spl <=> (aInteger0(sK15_skl(sK20_skl(sz00))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1578_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20589,plain,(
% 40.22/7.26 ~aInteger0(sK15_skl(sK20_skl(sz00)))|sQ1578_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f20587])).
% 40.22/7.26 fof(f20590,definition,(
% 40.22/7.26 sQ1579_spl <=> (sK15_skl(sK20_skl(sz00))=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1579_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20591,plain,(
% 40.22/7.26 sK15_skl(sK20_skl(sz00))=sz00|~sQ1579_spl),
% 40.22/7.26 inference(component_clause,[status(thm)],[f20590])).
% 40.22/7.26 fof(f20593,definition,(
% 40.22/7.26 sQ1580_spl <=> (aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(sK20_skl(sz00)))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1580_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20596,plain,(
% 40.22/7.26 ~sQ1578_spl|sQ1579_spl|sQ1580_spl|~sQ0_spl|~sQ283_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f20562,f20587,f20590,f20593,f304,f4569])).
% 40.22/7.26 fof(f20598,definition,(
% 40.22/7.26 sQ1581_spl <=> (sK18_skl(sz00)=sz00)),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1581_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20601,definition,(
% 40.22/7.26 sQ1582_spl <=> (aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK18_skl(sz00))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1582_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20604,plain,(
% 40.22/7.26 ~sQ12_spl|sQ1581_spl|sQ1582_spl|~sQ0_spl|~sQ38_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f20564,f351,f20598,f20601,f304,f537])).
% 40.22/7.26 fof(f20616,plain,(
% 40.22/7.26 $false|~sQ283_spl|~sQ1579_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f20591,f17455])).
% 40.22/7.26 fof(f20617,plain,(
% 40.22/7.26 ~sQ283_spl|~sQ1579_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f20616])).
% 40.22/7.26 fof(f20618,plain,(
% 40.22/7.26 $false|~sQ283_spl|sQ1578_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f20589,f16297])).
% 40.22/7.26 fof(f20619,plain,(
% 40.22/7.26 ~sQ283_spl|sQ1578_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f20618])).
% 40.22/7.26 fof(f20715,plain,(
% 40.22/7.26 ![X0,X1]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(sz00)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz00|aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ5_spl)),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f7215,f1670])).
% 40.22/7.26 fof(f20716,plain,(
% 40.22/7.26 ![X0,X1]: (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(sz10)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz10|aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz00,X0))|~sQ5_spl)),
% 40.22/7.26 inference(paramodulation,[status(thm)],[f1703,f1670])).
% 40.22/7.26 fof(f20717,definition,(
% 40.22/7.26 ![X0,X1]: (sQ1599_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz00|aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1599_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20720,plain,(
% 40.22/7.26 sQ1599_spl|~sQ94_spl|~sQ5_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f20715,f20717,f1538,f323])).
% 40.22/7.26 fof(f20721,definition,(
% 40.22/7.26 ![X0,X1]: (sQ1600_spl <=> (~aInteger0(X0)|X0=sz00|~isPrime0(X0)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz10|aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz00,X0))))),
% 40.22/7.26 introduced(definition,[new_symbols(definition,[sQ1600_spl])],[split_symbol_definition])).
% 40.22/7.26 fof(f20724,plain,(
% 40.22/7.26 sQ1600_spl|~sQ98_spl|~sQ5_spl),
% 40.22/7.26 inference(split_clause,[status(thm)],[f20716,f20721,f1553,f323])).
% 40.22/7.26 fof(f20772,plain,(
% 40.22/7.26 $false|~sQ111_spl|sQ133_spl),
% 40.22/7.26 inference(forward_subsumption_resolution,[status(thm)],[f15661,f1967])).
% 40.22/7.26 fof(f20773,plain,(
% 40.22/7.26 ~sQ111_spl|sQ133_spl),
% 40.22/7.26 inference(contradiction_clause,[status(thm)],[f20772])).
% 40.22/7.26 fof(f21215,plain,(
% 40.22/7.26 isPrime0(sz10)|~sQ1399_spl|~sQ38_spl),
% 40.22/7.27 inference(backward_demodulation,[status(thm)],[f18461,f538])).
% 40.22/7.27 fof(f21217,plain,(
% 40.22/7.27 $false|sQ150_spl|~sQ1399_spl|~sQ38_spl),
% 40.22/7.27 inference(forward_subsumption_resolution,[status(thm)],[f21215,f2847])).
% 40.22/7.27 fof(f21218,plain,(
% 40.22/7.27 sQ150_spl|~sQ1399_spl|~sQ38_spl),
% 40.22/7.27 inference(contradiction_clause,[status(thm)],[f21217])).
% 40.22/7.27 fof(f21524,plain,(
% 40.22/7.27 isPrime0(sz10)|sQ149_spl),
% 40.22/7.27 inference(resolution,[status(thm)],[f2844,f303])).
% 40.22/7.27 fof(f21525,plain,(
% 40.22/7.27 $false|sQ150_spl|sQ149_spl),
% 40.22/7.27 inference(forward_subsumption_resolution,[status(thm)],[f21524,f2847])).
% 40.22/7.27 fof(f21526,plain,(
% 40.22/7.27 sQ150_spl|sQ149_spl),
% 40.22/7.27 inference(contradiction_clause,[status(thm)],[f21525])).
% 40.22/7.27 fof(f21798,plain,(
% 40.22/7.27 ~aInteger0(sz00)|~sK1_skl(sz00)=sz00|~sQ122_spl),
% 40.22/7.27 inference(resolution,[status(thm)],[f2202,f89])).
% 40.22/7.27 fof(f21805,plain,(
% 40.22/7.27 ~sQ94_spl|~sQ1576_spl|~sQ122_spl),
% 40.22/7.27 inference(split_clause,[status(thm)],[f21798,f1538,f20580,f2201])).
% 40.22/7.27 fof(f21812,plain,(
% 40.22/7.27 ~aInteger0(sz00)|~sK18_skl(sz00)=sz00|~sQ62_spl),
% 40.22/7.27 inference(resolution,[status(thm)],[f3498,f89])).
% 40.22/7.27 fof(f21819,plain,(
% 40.22/7.27 ~sQ94_spl|~sQ1581_spl|~sQ62_spl),
% 40.22/7.27 inference(split_clause,[status(thm)],[f21812,f1538,f20598,f1047])).
% 40.22/7.27 fof(f22280,plain,(
% 40.22/7.27 ~aInteger0(sK22_skl)|~isPrime0(sK18_skl(sK22_skl))|~sK22_skl=sK22_skl|~sQ118_spl|~sQ10_spl),
% 40.22/7.27 inference(resolution,[status(thm)],[f2180,f14438])).
% 40.22/7.27 fof(f22287,plain,(
% 40.22/7.27 ~sQ141_spl|~sQ120_spl|~sQ618_spl|~sQ118_spl|~sQ10_spl),
% 40.22/7.27 inference(split_clause,[status(thm)],[f22280,f2701,f2187,f8276,f2179,f341])).
% 40.22/7.27 fof(f22294,plain,(
% 40.22/7.27 $false|sQ618_spl),
% 40.22/7.27 inference(trivial_equality_resolution,[status(thm)],[f8278])).
% 40.22/7.27 fof(f22295,plain,(
% 40.22/7.27 sQ618_spl),
% 40.22/7.27 inference(contradiction_clause,[status(thm)],[f22294])).
% 40.22/7.27 fof(f22299,plain,(
% 40.22/7.27 ~sQ12_spl|sQ20_spl),
% 40.22/7.27 inference(split_clause,[status(thm)],[f10521,f351,f389])).
% 40.22/7.27 fof(f22306,plain,(
% 40.22/7.27 sQ263_spl|~sQ9_spl|~sQ99_spl),
% 40.22/7.27 inference(split_clause,[status(thm)],[f2293,f4177,f338,f1556])).
% 40.22/7.27 fof(f22312,plain,(
% 40.22/7.27 sQ141_spl|~sQ9_spl),
% 40.22/7.27 inference(split_clause,[status(thm)],[f355,f2701,f338])).
% 40.22/7.27 fof(f22327,plain,(
% 40.22/7.27 $false),
% 40.22/7.27 inference(sat_refutation,[status(thm)],[f310,f314,f318,f322,f326,f330,f334,f344,f345,f346,f354,f420,f494,f510,f524,f532,f536,f540,f554,f562,f570,f797,f801,f805,f809,f1050,f1058,f1066,f1070,f1074,f1276,f1280,f1284,f1552,f1577,f1588,f1668,f1714,f1890,f1896,f1952,f1969,f2061,f2174,f2209,f2569,f2836,f2840,f3401,f3404,f3405,f3406,f3407,f3507,f3876,f3880,f3884,f3886,f4315,f4477,f4572,f6161,f6301,f6348,f6473,f6674,f6688,f6699,f6720,f6844,f6901,f6909,f6913,f7508,f7523,f7568,f7840,f8230,f8743,f8747,f8880,f8884,f8955,f9244,f9947,f9950,f10661,f10669,f10697,f11510,f11513,f11515,f11593,f11794,f12629,f12681,f13697,f13755,f14286,f14311,f14315,f14395,f14411,f14412,f14889,f14891,f15474,f15805,f15809,f15813,f15819,f15821,f15931,f16064,f16081,f16148,f16249,f16253,f16260,f17827,f18040,f18069,f18765,f18919,f19305,f19812,f20586,f20596,f20604,f20617,f20619,f20720,f20724,f20773,f21218,f21526,f21805,f21819,f22287,f22295,f22299,f22306,f22312])).
% 40.22/7.27 % SZS output end CNFRefutation for theBenchmark.p
% 40.22/7.28 % Elapsed time: 6.814249 seconds
% 40.22/7.28 % CPU time: 53.425094 seconds
% 40.22/7.28 % Total memory used: 354.252 MB
% 40.22/7.28 % Net memory used: 333.160 MB
%------------------------------------------------------------------------------