%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM588+3 : 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 : n010.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:43:17 PM UTC 2026
% Result : Theorem 0.12s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM588+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:42:28 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.46 % Refutation found
% 0.12/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.46 fof(f88,conjecture,(
% 0.12/0.46 (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W2] :( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W2)& aElementOf0(W2,sdtlpdtrp0(xN,W0))& W2 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ))& aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(W1) )=> (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xk& aElementOf0(W2,slbdtsldtrb0(W1,xk)) )=> ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W3] :( aElementOf0(W3,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3) ) ))=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W3] :( aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W3)& aElementOf0(W3,sdtlpdtrp0(xN,W0))& W3 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ))=> ( (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))| aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))| aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) ) ) ) )) )) )),
% 0.12/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f89,negated_conjecture,(
% 0.12/0.46 ~((! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W2] :( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W2)& aElementOf0(W2,sdtlpdtrp0(xN,W0))& W2 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ))& aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(W1) )=> (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xk& aElementOf0(W2,slbdtsldtrb0(W1,xk)) )=> ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W3] :( aElementOf0(W3,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3) ) ))=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W3] :( aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W3)& aElementOf0(W3,sdtlpdtrp0(xN,W0))& W3 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ))=> ( (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))| aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))| aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) ) ) ) )) )) ))),
% 0.12/0.46 inference(negated_conjecture,[status(cth)],[f88])).
% 0.12/0.46 fof(f477,plain,(
% 0.12/0.46 (?[W0]: (aElementOf0(W0,szNzAzT0)&(?[W1]: ((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,W0)))&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))&aSet0(W1))&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(W1))&(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xk)&aElementOf0(W2,slbdtsldtrb0(W1,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W3]: (~aElementOf0(W3,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&(![W3]: (aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W3)&aElementOf0(W3,sdtlpdtrp0(xN,W0)))&~W3=szmzizndt0(sdtlpdtrp0(xN,W0))))))&(((?[W3]: (aElementOf0(W3,W2)&~aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))))&~aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&~aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)))))))))))),
% 0.12/0.46 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 0.12/0.46 fof(f478,plain,(
% 0.12/0.46 ?[W0]: (aElementOf0(W0,szNzAzT0)&(?[W1]: ((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W2]: ((~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,W0)))&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))&(aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W2)|~aElementOf0(W2,sdtlpdtrp0(xN,W0)))|W2=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSet0(W1))&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(W1))&(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xk)&aElementOf0(W2,slbdtsldtrb0(W1,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W3]: (~aElementOf0(W3,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&(![W3]: ((~aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W3)&aElementOf0(W3,sdtlpdtrp0(xN,W0)))&~W3=szmzizndt0(sdtlpdtrp0(xN,W0))))&(aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W3)|~aElementOf0(W3,sdtlpdtrp0(xN,W0)))|W3=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&(((?[W3]: (aElementOf0(W3,W2)&~aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))))&~aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&~aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))))))))))),
% 0.12/0.46 inference(NNF_transformation,[status(thm)],[f477])).
% 0.12/0.46 fof(f479,plain,(
% 0.12/0.46 ?[W0]: (aElementOf0(W0,szNzAzT0)&(?[W1]: ((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&((![W2]: (~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,W0)))&~W2=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W2)|~aElementOf0(W2,sdtlpdtrp0(xN,W0)))|W2=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSet0(W1))&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(W1))&(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xk)&aElementOf0(W2,slbdtsldtrb0(W1,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W3]: (~aElementOf0(W3,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W3))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&((![W3]: (~aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W3)&aElementOf0(W3,sdtlpdtrp0(xN,W0)))&~W3=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W3]: (aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W3)|~aElementOf0(W3,sdtlpdtrp0(xN,W0)))|W3=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&(((?[W3]: (aElementOf0(W3,W2)&~aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))))&~aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&~aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))))))))))),
% 0.12/0.47 inference(miniscoping,[status(thm)],[f478])).
% 0.12/0.47 fof(f480,plain,(
% 0.12/0.47 (aElementOf0(sK26_skl,szNzAzT0)&((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK26_skl)),sdtlpdtrp0(xN,sK26_skl))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,sK26_skl))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK26_skl)),W2))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))&((![W2]: (~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))|((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,sK26_skl)))&~W2=szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))|((~aElement0(W2)|~aElementOf0(W2,sdtlpdtrp0(xN,sK26_skl)))|W2=szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))))&aSet0(sK27_skl))&(![W2]: (~aElementOf0(W2,sK27_skl)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))))&aSubsetOf0(sK27_skl,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))&isCountable0(sK27_skl))&(((((aSet0(sK28_skl)&(![W3]: (~aElementOf0(W3,sK28_skl)|aElementOf0(W3,sK27_skl))))&aSubsetOf0(sK28_skl,sK27_skl))&sbrdtbr0(sK28_skl)=xk)&aElementOf0(sK28_skl,slbdtsldtrb0(sK27_skl,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK26_skl)),sdtlpdtrp0(xN,sK26_skl))&(![W3]: (~aElementOf0(W3,sdtlpdtrp0(xN,sK26_skl))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK26_skl)),W3))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))&((![W3]: (~aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))|((aElement0(W3)&aElementOf0(W3,sdtlpdtrp0(xN,sK26_skl)))&~W3=szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))&(![W3]: (aElementOf0(W3,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))|((~aElement0(W3)|~aElementOf0(W3,sdtlpdtrp0(xN,sK26_skl)))|W3=szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))))&(((aElementOf0(sK29_skl,sK28_skl)&~aElementOf0(sK29_skl,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))&~aSubsetOf0(sK28_skl,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))&~aElementOf0(sK28_skl,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))),xk))))))))),
% 0.12/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl,sK29_skl]),skolemize(W0,sK26_skl),skolemize(W1,sK27_skl),skolemize(W2,sK28_skl),skolemize(W3,sK29_skl)],[f479])).
% 0.12/0.47 fof(f490,plain,(
% 0.12/0.47 ![X0]: (~aElementOf0(X0,sK27_skl)|aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl)))))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f480])).
% 0.12/0.47 fof(f494,plain,(
% 0.12/0.47 ![X0]: (~aElementOf0(X0,sK28_skl)|aElementOf0(X0,sK27_skl))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f480])).
% 0.12/0.47 fof(f505,plain,(
% 0.12/0.47 aElementOf0(sK29_skl,sK28_skl)),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f480])).
% 0.12/0.47 fof(f506,plain,(
% 0.12/0.47 ~aElementOf0(sK29_skl,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f480])).
% 0.12/0.47 fof(f954,plain,(
% 0.12/0.47 aElementOf0(sK29_skl,sK27_skl)),
% 0.12/0.47 inference(resolution,[status(thm)],[f505,f494])).
% 0.12/0.47 fof(f1531,plain,(
% 0.12/0.47 aElementOf0(sK29_skl,sdtmndt0(sdtlpdtrp0(xN,sK26_skl),szmzizndt0(sdtlpdtrp0(xN,sK26_skl))))),
% 0.12/0.47 inference(resolution,[status(thm)],[f954,f490])).
% 0.12/0.47 fof(f1534,plain,(
% 0.12/0.47 $false),
% 0.12/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1531,f506])).
% 0.12/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.50 % Elapsed time: 0.131557 seconds
% 0.12/0.50 % CPU time: 0.597511 seconds
% 0.12/0.50 % Total memory used: 127.626 MB
% 0.12/0.50 % Net memory used: 126.723 MB
%------------------------------------------------------------------------------