%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM544+2 : 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 : n005.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:10 PM UTC 2026
% Result : Theorem 0.17s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM544+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.37 % Computer : n005.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Mon Sep 21 02:38:48 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 0.17/0.58 % Refutation found
% 0.17/0.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.58 fof(f32,axiom,(
% 0.17/0.58 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( sdtlseqdt0(W0,W1)<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) )),
% 0.17/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.58 fof(f55,hypothesis,(
% 0.17/0.58 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isFinite0(xS) ) ),
% 0.17/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.58 fof(f56,conjecture,(
% 0.17/0.58 ( ~ ( ~ (? [W0] : aElementOf0(W0,xS))| xS = slcrc0 )=> ( ( aElementOf0(szmzazxdt0(xS),xS)& (! [W0] :( aElementOf0(W0,xS)=> sdtlseqdt0(W0,szmzazxdt0(xS)) ) ))=> ( ( aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))& (! [W0] :( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=> ( aElementOf0(W0,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))) ) ) ))=> ( (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ))| aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ) ) ) ),
% 0.17/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.58 fof(f57,negated_conjecture,(
% 0.17/0.58 ~(( ~ ( ~ (? [W0] : aElementOf0(W0,xS))| xS = slcrc0 )=> ( ( aElementOf0(szmzazxdt0(xS),xS)& (! [W0] :( aElementOf0(W0,xS)=> sdtlseqdt0(W0,szmzazxdt0(xS)) ) ))=> ( ( aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))& (! [W0] :( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=> ( aElementOf0(W0,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))) ) ) ))=> ( (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ))| aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ) ) ) )),
% 0.17/0.58 inference(negated_conjecture,[status(cth)],[f56])).
% 0.17/0.58 fof(f154,plain,(
% 0.17/0.58 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(sdtlseqdt0(W0,W1)<=>sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))))),
% 0.17/0.58 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.17/0.58 fof(f155,plain,(
% 0.17/0.58 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|((~sdtlseqdt0(W0,W1)|sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)))&(sdtlseqdt0(W0,W1)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)))))),
% 0.17/0.59 inference(NNF_transformation,[status(thm)],[f154])).
% 0.17/0.59 fof(f156,plain,(
% 0.17/0.59 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X0,X1)|sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)))),
% 0.17/0.59 inference(cnf_transformation,[status(thm)],[f155])).
% 0.17/0.59 fof(f233,plain,(
% 0.17/0.59 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isFinite0(xS)),
% 0.17/0.59 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.17/0.59 fof(f235,plain,(
% 0.17/0.59 ![X0]: (~aElementOf0(X0,xS)|aElementOf0(X0,szNzAzT0))),
% 0.17/0.59 inference(cnf_transformation,[status(thm)],[f233])).
% 0.17/0.59 fof(f238,plain,(
% 0.17/0.59 (((?[W0]: aElementOf0(W0,xS))&~xS=slcrc0)&((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&((aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))&(![W0]: (aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=>(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&~aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))))),
% 0.17/0.59 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.17/0.59 fof(f239,plain,(
% 0.17/0.59 ((?[W0]: aElementOf0(W0,xS))&~xS=slcrc0)&((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&((aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))&(![W0]: ((~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))&(aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&~aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))),
% 0.17/0.59 inference(NNF_transformation,[status(thm)],[f238])).
% 0.17/0.59 fof(f240,plain,(
% 0.17/0.59 ((?[W0]: aElementOf0(W0,xS))&~xS=slcrc0)&((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&((aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))&((![W0]: (~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))&(![W0]: (aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))&~aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))),
% 0.17/0.61 inference(miniscoping,[status(thm)],[f239])).
% 0.17/0.61 fof(f241,plain,(
% 0.17/0.61 (aElementOf0(sK9_skl,xS)&~xS=slcrc0)&((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&((aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))&((![W0]: (~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))&(![W0]: (aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))))&((aElementOf0(sK10_skl,xS)&~aElementOf0(sK10_skl,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&~aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))),
% 0.17/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(W0,sK9_skl),skolemize(W0,sK10_skl)],[f240])).
% 0.17/0.61 fof(f244,plain,(
% 0.17/0.61 aElementOf0(szmzazxdt0(xS),xS)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f241])).
% 0.17/0.61 fof(f245,plain,(
% 0.17/0.61 ![X0]: (~aElementOf0(X0,xS)|sdtlseqdt0(X0,szmzazxdt0(xS)))),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f241])).
% 0.17/0.61 fof(f249,plain,(
% 0.17/0.61 ![X0]: (aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(szmzazxdt0(xS))))),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f241])).
% 0.17/0.61 fof(f250,plain,(
% 0.17/0.61 aElementOf0(sK10_skl,xS)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f241])).
% 0.17/0.61 fof(f251,plain,(
% 0.17/0.61 ~aElementOf0(sK10_skl,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f241])).
% 0.17/0.61 fof(f385,plain,(
% 0.17/0.61 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(szmzazxdt0(xS),szNzAzT0)|~sdtlseqdt0(X0,szmzazxdt0(xS))|aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~aElementOf0(X0,szNzAzT0))),
% 0.17/0.61 inference(resolution,[status(thm)],[f156,f249])).
% 0.17/0.61 fof(f386,plain,(
% 0.17/0.61 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(szmzazxdt0(xS),szNzAzT0)|~sdtlseqdt0(X0,szmzazxdt0(xS))|aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.17/0.61 inference(duplicate_literals_removal,[status(thm)],[f385])).
% 0.17/0.61 fof(f387,plain,(
% 0.17/0.61 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(X0,szmzazxdt0(xS))|aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~aElementOf0(szmzazxdt0(xS),xS))),
% 0.17/0.61 inference(resolution,[status(thm)],[f386,f235])).
% 0.17/0.61 fof(f388,plain,(
% 0.17/0.61 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(X0,szmzazxdt0(xS))|aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.17/0.61 inference(forward_subsumption_resolution,[status(thm)],[f387,f244])).
% 0.17/0.61 fof(f390,plain,(
% 0.17/0.61 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~aElementOf0(X0,xS))),
% 0.17/0.61 inference(resolution,[status(thm)],[f388,f245])).
% 0.17/0.61 fof(f393,plain,(
% 0.17/0.61 ![X0]: (aElementOf0(X0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~aElementOf0(X0,xS))),
% 0.17/0.61 inference(forward_subsumption_resolution,[status(thm)],[f390,f235])).
% 0.17/0.61 fof(f395,plain,(
% 0.17/0.61 ~aElementOf0(sK10_skl,xS)),
% 0.17/0.61 inference(resolution,[status(thm)],[f393,f251])).
% 0.17/0.61 fof(f400,plain,(
% 0.17/0.61 $false),
% 0.17/0.61 inference(forward_subsumption_resolution,[status(thm)],[f395,f250])).
% 0.17/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.62 % Elapsed time: 0.219419 seconds
% 0.17/0.62 % CPU time: 1.010288 seconds
% 0.17/0.62 % Total memory used: 111.647 MB
% 0.17/0.62 % Net memory used: 110.626 MB
%------------------------------------------------------------------------------