%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM456+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:42:57 PM UTC 2026
% Result : Theorem 0.09s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM456+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.49 % Computer : n012.cluster.edu
% 0.04/0.49 % Model : x86_64 x86_64
% 0.04/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.49 % Memory : 8046.5625MB
% 0.04/0.49 % OS : Linux 6.8.0-71-generic
% 0.04/0.49 % CPULimit : 300
% 0.04/0.49 % WCLimit : 300
% 0.04/0.49 % DateTime : Mon Sep 21 02:31:39 UTC 2026
% 0.04/0.49 % CPUTime :
% 0.04/0.50 % Drodi V4.1.1
% 0.09/0.60 % Refutation found
% 0.09/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.60 fof(f43,hypothesis,(
% 0.09/0.60 ( 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 ) ),
% 0.09/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f45,hypothesis,(
% 0.09/0.60 ( aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=> (? [W1] :( aInteger0(W1)& W1 != sz00& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1))& (! [W2] :( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> ( aInteger0(W2)& (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))& sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )& ( ( aInteger0(W2)& ( (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))| sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ))& (! [W2] :( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) )))& isOpen0(stldt0(sbsmnsldt0(xS)))& isClosed0(sbsmnsldt0(xS))& aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))=> (? [W1] :( aInteger0(W1)& W1 != sz00& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1))& (! [W2] :( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> ( aInteger0(W2)& (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))& sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )& ( ( aInteger0(W2)& ( (? [W3] :( aInteger0(W3)& sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ))| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))| sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ))& (! [W2] :( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))=> aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))) ) )) )) ),
% 0.09/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f46,hypothesis,(
% 0.09/0.60 ( aInteger0(xp)& xp != sz00& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))& (! [W0] :( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=> ( aInteger0(W0)& (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))& sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) )& ( ( aInteger0(W0)& ( (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))| aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))| sdteqdtlpzmzozddtrp0(W0,sz10,xp) ) )=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) ))& aSet0(sbsmnsldt0(xS))& (! [W0] :( aElementOf0(W0,sbsmnsldt0(xS))<=> ( aInteger0(W0)& (? [W1] :( aElementOf0(W1,xS)& aElementOf0(W0,W1) ) )) ))& (! [W0] :( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=> ( aInteger0(W0)& ~ aElementOf0(W0,sbsmnsldt0(xS)) ) ))& (! [W0] :( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))=> aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ))& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ) ),
% 0.09/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f47,hypothesis,(
% 0.09/0.60 (? [W0] :( aInteger0(W0)& (? [W1] :( aInteger0(W1)& sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10)) ))& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))& sdteqdtlpzmzozddtrp0(W0,sz10,xp)& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))& ~ ( W0 = sz10| W0 = smndt0(sz10)| aElementOf0(W0,cS2200) ) ) )),
% 0.09/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f252,plain,(
% 0.09/0.60 ((((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),
% 0.09/0.60 inference(NNF_transformation,[status(thm)],[f43])).
% 0.09/0.60 fof(f253,plain,(
% 0.09/0.60 ((((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))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10))))))&stldt0(sbsmnsldt0(xS))=cS2076),
% 0.09/0.60 inference(miniscoping,[status(thm)],[f252])).
% 0.09/0.60 fof(f254,plain,(
% 0.09/0.60 ((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK18_skl(W0),xS)&aElementOf0(W0,sK18_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)))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(W0=sz10|W0=smndt0(sz10))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~W0=sz10&~W0=smndt0(sz10))))))&stldt0(sbsmnsldt0(xS))=cS2076),
% 0.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(W1,sK18_skl(W0))],[f253])).
% 0.09/0.60 fof(f264,plain,(
% 0.09/0.60 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|X0=sz10|X0=smndt0(sz10))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f254])).
% 0.09/0.60 fof(f267,plain,(
% 0.09/0.60 stldt0(sbsmnsldt0(xS))=cS2076),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f254])).
% 0.09/0.60 fof(f269,plain,(
% 0.09/0.60 ((((((((aSet0(sbsmnsldt0(xS))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.09/0.60 fof(f270,plain,(
% 0.09/0.60 ((((((((aSet0(sbsmnsldt0(xS))&(![W0]: ((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&(aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(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))))))))&(![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)))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&(![W2]: ((~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1)))&((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),
% 0.09/0.60 inference(NNF_transformation,[status(thm)],[f269])).
% 0.09/0.60 fof(f271,plain,(
% 0.09/0.60 ((((((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS))))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(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))))))))&((![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)))|(?[W1]: (((((aInteger0(W1)&~W1=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|(((aInteger0(W2)&(?[W3]: (aInteger0(W3)&sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0)))))&aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,W1))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(W1,W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,W1)))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))))))),
% 0.09/0.60 inference(miniscoping,[status(thm)],[f270])).
% 0.09/0.60 fof(f272,plain,(
% 0.09/0.60 ((((((((aSet0(sbsmnsldt0(xS))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK19_skl(W0),xS)&aElementOf0(W0,sK19_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(sK20_skl(W0))&~sK20_skl(W0)=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK21_skl(W2,W0))&sdtasdt0(sK20_skl(W0),sK21_skl(W2,W0))=sdtpldt0(W2,smndt0(W0))))&aDivisorOf0(sK20_skl(W0),sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,sK20_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK20_skl(W0),W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(sK20_skl(W0),sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,sK20_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)),stldt0(sbsmnsldt0(xS)))))))&isOpen0(stldt0(sbsmnsldt0(xS))))&isClosed0(sbsmnsldt0(xS)))&aSet0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK22_skl(W0),xS)&aElementOf0(W0,sK22_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(((((aInteger0(sK23_skl(W0))&~sK23_skl(W0)=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0))))&((![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))|(((aInteger0(W2)&(aInteger0(sK24_skl(W2,W0))&sdtasdt0(sK23_skl(W0),sK24_skl(W2,W0))=sdtpldt0(W2,smndt0(W0))))&aDivisorOf0(sK23_skl(W0),sdtpldt0(W2,smndt0(W0))))&sdteqdtlpzmzozddtrp0(W2,W0,sK23_skl(W0)))))&(![W2]: ((~aInteger0(W2)|(((![W3]: (~aInteger0(W3)|~sdtasdt0(sK23_skl(W0),W3)=sdtpldt0(W2,smndt0(W0))))&~aDivisorOf0(sK23_skl(W0),sdtpldt0(W2,smndt0(W0))))&~sdteqdtlpzmzozddtrp0(W2,W0,sK23_skl(W0))))|aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))))))&(![W2]: (~aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))|aElementOf0(W2,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)),stldt0(sbsmnsldt0(xS))))))),
% 0.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0)),skolemize(W3,sK21_skl(W2,W0)),skolemize(W1,sK22_skl(W0)),skolemize(W1,sK23_skl(W0)),skolemize(W3,sK24_skl(W2,W0))],[f271])).
% 0.09/0.60 fof(f305,plain,(
% 0.09/0.60 ![X0]: (~aElementOf0(X0,stldt0(sbsmnsldt0(xS)))|~sK23_skl(X0)=sz00)),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f272])).
% 0.09/0.60 fof(f317,plain,(
% 0.09/0.60 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(![W0]: ((~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&aSet0(sbsmnsldt0(xS)))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))<=>(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))<=>(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))))&(![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.09/0.60 fof(f318,plain,(
% 0.09/0.60 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&(![W0]: ((~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp)))&((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&aSet0(sbsmnsldt0(xS)))&(![W0]: ((~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1)))))&(aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&(![W0]: ((~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS))))&(aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.60 inference(NNF_transformation,[status(thm)],[f317])).
% 0.09/0.60 fof(f319,plain,(
% 0.09/0.60 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp))))&(![W0]: ((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&aSet0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(?[W1]: (aElementOf0(W1,xS)&aElementOf0(W0,W1))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.60 inference(miniscoping,[status(thm)],[f318])).
% 0.09/0.60 fof(f320,plain,(
% 0.09/0.60 (((((((aInteger0(xp)&~xp=sz00)&aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|(((aInteger0(W0)&(aInteger0(sK25_skl(W0))&sdtasdt0(xp,sK25_skl(W0))=sdtpldt0(W0,smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp))))&(![W0]: ((~aInteger0(W0)|(((![W1]: (~aInteger0(W1)|~sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10))))&~aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&~sdteqdtlpzmzozddtrp0(W0,sz10,xp)))|aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))&aSet0(sbsmnsldt0(xS)))&((![W0]: (~aElementOf0(W0,sbsmnsldt0(xS))|(aInteger0(W0)&(aElementOf0(sK26_skl(W0),xS)&aElementOf0(W0,sK26_skl(W0))))))&(![W0]: (aElementOf0(W0,sbsmnsldt0(xS))|(~aInteger0(W0)|(![W1]: (~aElementOf0(W1,xS)|~aElementOf0(W0,W1))))))))&((![W0]: (~aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(aInteger0(W0)&~aElementOf0(W0,sbsmnsldt0(xS)))))&(![W0]: (aElementOf0(W0,stldt0(sbsmnsldt0(xS)))|(~aInteger0(W0)|aElementOf0(W0,sbsmnsldt0(xS)))))))&(![W0]: (~aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(W0,stldt0(sbsmnsldt0(xS))))))&aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))),
% 0.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(W1,sK25_skl(W0)),skolemize(W1,sK26_skl(W0))],[f319])).
% 0.09/0.60 fof(f340,plain,(
% 0.09/0.60 ![X0]: (~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(X0,stldt0(sbsmnsldt0(xS))))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f320])).
% 0.09/0.60 fof(f342,plain,(
% 0.09/0.60 ?[W0]: (((((aInteger0(W0)&(?[W1]: (aInteger0(W1)&sdtasdt0(xp,W1)=sdtpldt0(W0,smndt0(sz10)))))&aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(W0,sz10,xp))&aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((~W0=sz10&~W0=smndt0(sz10))&~aElementOf0(W0,cS2200)))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.09/0.60 fof(f343,plain,(
% 0.09/0.60 (((((aInteger0(sK27_skl)&(aInteger0(sK28_skl)&sdtasdt0(xp,sK28_skl)=sdtpldt0(sK27_skl,smndt0(sz10))))&aDivisorOf0(xp,sdtpldt0(sK27_skl,smndt0(sz10))))&sdteqdtlpzmzozddtrp0(sK27_skl,sz10,xp))&aElementOf0(sK27_skl,szAzrzSzezqlpdtcmdtrp0(sz10,xp)))&((~sK27_skl=sz10&~sK27_skl=smndt0(sz10))&~aElementOf0(sK27_skl,cS2200)))),
% 0.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(W0,sK27_skl),skolemize(W1,sK28_skl)],[f342])).
% 0.09/0.60 fof(f349,plain,(
% 0.09/0.60 aElementOf0(sK27_skl,szAzrzSzezqlpdtcmdtrp0(sz10,xp))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f343])).
% 0.09/0.60 fof(f350,plain,(
% 0.09/0.60 ~sK27_skl=sz10),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f343])).
% 0.09/0.60 fof(f351,plain,(
% 0.09/0.60 ~sK27_skl=smndt0(sz10)),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f343])).
% 0.09/0.60 fof(f872,definition,(
% 0.09/0.60 sQ51_spl <=> (sK27_skl=sz10)),
% 0.09/0.60 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.09/0.60 fof(f873,plain,(
% 0.09/0.60 sK27_skl=sz10|~sQ51_spl),
% 0.09/0.60 inference(component_clause,[status(thm)],[f872])).
% 0.09/0.60 fof(f875,definition,(
% 0.09/0.60 sQ52_spl <=> (sK27_skl=smndt0(sz10))),
% 0.09/0.60 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.09/0.60 fof(f876,plain,(
% 0.09/0.60 sK27_skl=smndt0(sz10)|~sQ52_spl),
% 0.09/0.60 inference(component_clause,[status(thm)],[f875])).
% 0.09/0.60 fof(f889,plain,(
% 0.09/0.60 $false|~sQ51_spl),
% 0.09/0.60 inference(forward_subsumption_resolution,[status(thm)],[f873,f350])).
% 0.09/0.60 fof(f890,plain,(
% 0.09/0.60 ~sQ51_spl),
% 0.09/0.60 inference(contradiction_clause,[status(thm)],[f889])).
% 0.09/0.60 fof(f1446,plain,(
% 0.09/0.60 ![X0]: (~aElementOf0(X0,cS2076)|X0=sz10|X0=smndt0(sz10))),
% 0.09/0.60 inference(backward_demodulation,[status(thm)],[f267,f264])).
% 0.09/0.60 fof(f1665,plain,(
% 0.09/0.60 ![X0]: (~aElementOf0(X0,cS2076)|~sK23_skl(X0)=sz00)),
% 0.09/0.60 inference(forward_demodulation,[status(thm)],[f267,f305])).
% 0.09/0.60 fof(f1934,plain,(
% 0.09/0.60 ![X0]: (~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))|aElementOf0(X0,cS2076))),
% 0.09/0.60 inference(forward_demodulation,[status(thm)],[f267,f340])).
% 0.09/0.60 fof(f1974,plain,(
% 0.09/0.60 aElementOf0(sK27_skl,cS2076)),
% 0.09/0.60 inference(resolution,[status(thm)],[f349,f1934])).
% 0.09/0.60 fof(f2151,plain,(
% 0.09/0.60 ~sK27_skl=sK27_skl|~sQ52_spl),
% 0.09/0.60 inference(forward_demodulation,[status(thm)],[f876,f351])).
% 0.09/0.60 fof(f2152,plain,(
% 0.09/0.60 $false|~sQ52_spl),
% 0.09/0.60 inference(trivial_equality_resolution,[status(thm)],[f2151])).
% 0.09/0.60 fof(f2153,plain,(
% 0.09/0.60 ~sQ52_spl),
% 0.09/0.60 inference(contradiction_clause,[status(thm)],[f2152])).
% 0.09/0.60 fof(f2337,plain,(
% 0.09/0.60 ~sK23_skl(sK27_skl)=sz00),
% 0.09/0.60 inference(resolution,[status(thm)],[f1974,f1665])).
% 0.09/0.60 fof(f2861,definition,(
% 0.09/0.60 sQ290_spl <=> (sK23_skl(sK27_skl)=sz00)),
% 0.09/0.60 introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition])).
% 0.09/0.60 fof(f2862,plain,(
% 0.09/0.60 sK23_skl(sK27_skl)=sz00|~sQ290_spl),
% 0.09/0.60 inference(component_clause,[status(thm)],[f2861])).
% 0.09/0.60 fof(f2876,plain,(
% 0.09/0.60 $false|~sQ290_spl),
% 0.09/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2862,f2337])).
% 0.09/0.60 fof(f2877,plain,(
% 0.09/0.60 ~sQ290_spl),
% 0.09/0.60 inference(contradiction_clause,[status(thm)],[f2876])).
% 0.09/0.60 fof(f2973,plain,(
% 0.09/0.60 sK27_skl=sz10|sK27_skl=smndt0(sz10)),
% 0.09/0.60 inference(resolution,[status(thm)],[f1446,f1974])).
% 0.09/0.60 fof(f2975,plain,(
% 0.09/0.60 sQ51_spl|sQ52_spl),
% 0.09/0.60 inference(split_clause,[status(thm)],[f2973,f872,f875])).
% 0.09/0.60 fof(f2976,plain,(
% 0.09/0.60 $false),
% 0.09/0.60 inference(sat_refutation,[status(thm)],[f890,f2153,f2877,f2975])).
% 0.09/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.61 % Elapsed time: 0.116609 seconds
% 0.09/0.61 % CPU time: 0.683948 seconds
% 0.09/0.61 % Total memory used: 127.559 MB
% 0.09/0.61 % Net memory used: 126.145 MB
%------------------------------------------------------------------------------