%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM538+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:40:55 PM UTC 2026
% Result : Theorem 9.15s 1.67s
% Output : CNFRefutation 9.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 21
% Syntax : Number of formulae : 105 ( 22 unt; 12 def)
% Number of atoms : 329 ( 64 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 383 ( 159 ~; 151 |; 41 &)
% ( 20 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 10 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 118 ( 113 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> W0 != slcrc0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,definition,
! [W0,W1] :
( ( aElement0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( ( isFinite0(W1)
& aSet0(W1) )
=> isFinite0(sdtmndt0(W1,W0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aElement0(W1)
=> ( ~ aElementOf0(W1,W0)
=> sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
aSet0(xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( aElementOf0(xx,xS)
& isFinite0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) = sbrdtbr0(xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) != sbrdtbr0(xS),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f54,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f55,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
( ! [W0] :
( aElementOf0(sK0_skl(W0),W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f60]) ).
fof(f62,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f70,plain,
! [W0] :
( W0 != slcrc0
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f71,plain,
! [X0] :
( X0 != slcrc0
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f101,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f102,definition,
! [W0,W1,W3] :
( sP0_prd(W3,W1,W0)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f103,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> sP0_prd(W3,W1,W0) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(formula_renaming,[status(thm)],[f101,f102]) ).
fof(f104,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ~ sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ( ( ! [W3] :
( ( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ~ sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f106,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( sP0_prd(sK3_skl(W2,W1,W0),W1,W0)
| aElementOf0(sK3_skl(W2,W1,W0),W2) )
& ( ~ sP0_prd(sK3_skl(W2,W1,W0),W1,W0)
| ~ aElementOf0(sK3_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X3,X1,X0)
| ~ aElementOf0(X3,X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f112,plain,
! [W0] :
( ! [W1] :
( sdtpldt0(sdtmndt0(W0,W1),W1) = W0
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f113,plain,
! [X0,X1] :
( sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f122,plain,
! [W0] :
( ! [W1] :
( isFinite0(sdtmndt0(W1,W0))
| ~ isFinite0(W1)
| ~ aSet0(W1) )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f123,plain,
! [X0,X1] :
( isFinite0(sdtmndt0(X1,X0))
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f168,plain,
! [W0] :
( ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f169,plain,
! [W0] :
( ( ( W0 != slcrc0
| sbrdtbr0(W0) = sz00 )
& ( W0 = slcrc0
| sbrdtbr0(W0) != sz00 ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f168]) ).
fof(f171,plain,
! [X0] :
( X0 != slcrc0
| sbrdtbr0(X0) = sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f172,plain,
! [W0] :
( ! [W1] :
( sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0))
| aElementOf0(W1,W0)
| ~ aElement0(W1) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f173,plain,
! [X0,X1] :
( sbrdtbr0(sdtpldt0(X0,X1)) = szszuzczcdt0(sbrdtbr0(X0))
| aElementOf0(X1,X0)
| ~ aElement0(X1)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f175,plain,
isFinite0(xS),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f176,plain,
aElementOf0(xx,xS),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f177,plain,
szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) != sbrdtbr0(xS),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f178,plain,
! [W0,W1,W3] :
( ( W3 = W1
| ~ aElementOf0(W3,W0)
| ~ aElement0(W3)
| sP0_prd(W3,W1,W0) )
& ( ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) )
| ~ sP0_prd(W3,W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f102]) ).
fof(f179,plain,
( ! [W0,W1,W3] :
( W3 = W1
| ~ aElementOf0(W3,W0)
| ~ aElement0(W3)
| sP0_prd(W3,W1,W0) )
& ! [W0,W1,W3] :
( ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) )
| ~ sP0_prd(W3,W1,W0) ) ),
inference(miniscoping,[status(thm)],[f178]) ).
fof(f182,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f184,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f62]) ).
fof(f185,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f186,plain,
( ~ isCountable0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f71]) ).
fof(f187,plain,
~ isCountable0(slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f186,f184]) ).
fof(f200,plain,
! [X0,X1] :
( aSet0(sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f107]) ).
fof(f201,plain,
! [X0,X1,X2] :
( sP0_prd(X2,X1,X0)
| ~ aElementOf0(X2,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f108]) ).
fof(f203,plain,
( sbrdtbr0(slcrc0) = sz00
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f171]) ).
fof(f204,plain,
sbrdtbr0(slcrc0) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f203,f184]) ).
fof(f205,plain,
! [X0,X1] : ~ sP0_prd(X0,X0,X1),
inference(destructive_equality_resolution,[status(thm)],[f182]) ).
fof(f207,plain,
! [X0] :
( sdtpldt0(sdtmndt0(xS,X0),X0) = xS
| ~ aElementOf0(X0,xS) ),
inference(resolution,[status(thm)],[f113,f174]) ).
fof(f226,plain,
sdtpldt0(sdtmndt0(xS,xx),xx) = xS,
inference(resolution,[status(thm)],[f207,f176]) ).
fof(f235,definition,
( sQ5_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f237,plain,
( sQ5_spl
| ~ aSet0(xS) ),
inference(component_clause,[status(thm)],[f235]) ).
fof(f243,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f237,f174]) ).
fof(f244,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f243]) ).
fof(f274,definition,
( sQ12_spl
<=> aElement0(xx) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f275,plain,
( ~ sQ12_spl
| aElement0(xx) ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f276,plain,
( sQ12_spl
| ~ aElement0(xx) ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f284,plain,
! [X0] :
( sQ12_spl
| ~ aElementOf0(xx,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f276,f55]) ).
fof(f288,plain,
( sQ12_spl
| ~ aElementOf0(xx,xS) ),
inference(resolution,[status(thm)],[f284,f174]) ).
fof(f289,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f176]) ).
fof(f290,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f289]) ).
fof(f313,definition,
( sQ17_spl
<=> isFinite0(xS) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f315,plain,
( sQ17_spl
| ~ isFinite0(xS) ),
inference(component_clause,[status(thm)],[f313]) ).
fof(f333,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f315,f175]) ).
fof(f334,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f333]) ).
fof(f576,definition,
( sQ49_spl
<=> sbrdtbr0(sdtpldt0(sdtmndt0(xS,xx),xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( ~ sQ49_spl
| sbrdtbr0(sdtpldt0(sdtmndt0(xS,xx),xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) ),
inference(component_clause,[status(thm)],[f576]) ).
fof(f584,plain,
( ~ sQ49_spl
| sbrdtbr0(xS) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) ),
inference(forward_demodulation,[status(thm)],[f226,f577]) ).
fof(f585,plain,
( ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f177]) ).
fof(f586,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f585]) ).
fof(f689,definition,
( sQ64_spl
<=> aElementOf0(xx,sdtmndt0(xS,xx)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( ~ sQ64_spl
| aElementOf0(xx,sdtmndt0(xS,xx)) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f691,plain,
( sQ64_spl
| ~ aElementOf0(xx,sdtmndt0(xS,xx)) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f769,plain,
! [X0,X1,X2] :
( sbrdtbr0(sdtpldt0(sdtmndt0(X1,X0),X2)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X0)))
| aElementOf0(X2,sdtmndt0(X1,X0))
| ~ aElement0(X2)
| ~ aSet0(sdtmndt0(X1,X0))
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f123,f173]) ).
fof(f771,plain,
! [X0,X1,X2] :
( sbrdtbr0(sdtpldt0(sdtmndt0(X1,X0),X2)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X0)))
| aElementOf0(X2,sdtmndt0(X1,X0))
| ~ aElement0(X2)
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f769,f200]) ).
fof(f1364,plain,
! [X0,X1] :
( ~ sQ12_spl
| sP0_prd(X1,xx,X0)
| ~ aElementOf0(X1,sdtmndt0(X0,xx))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f201,f275]) ).
fof(f1376,plain,
( ~ sQ64_spl
| ~ sQ12_spl
| sP0_prd(xx,xx,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1364,f690]) ).
fof(f1379,definition,
( sQ122_spl
<=> sP0_prd(xx,xx,xS) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1380,plain,
( ~ sQ122_spl
| sP0_prd(xx,xx,xS) ),
inference(component_clause,[status(thm)],[f1379]) ).
fof(f1382,plain,
( ~ sQ64_spl
| ~ sQ12_spl
| sQ122_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1376,f235,f1379,f274,f689]) ).
fof(f1384,plain,
( ~ sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1380,f205]) ).
fof(f1385,plain,
~ sQ122_spl,
inference(contradiction_clause,[status(thm)],[f1384]) ).
fof(f1951,definition,
( sQ146_spl
<=> sbrdtbr0(slcrc0) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1953,plain,
( sQ146_spl
| sbrdtbr0(slcrc0) != sz00 ),
inference(component_clause,[status(thm)],[f1951]) ).
fof(f1956,plain,
( sQ146_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f204,f1953]) ).
fof(f1957,plain,
( sQ146_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1956]) ).
fof(f1958,plain,
sQ146_spl,
inference(contradiction_clause,[status(thm)],[f1957]) ).
fof(f2100,definition,
( sQ147_spl
<=> aElementOf0(sK0_skl(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f2101,plain,
( ~ sQ147_spl
| aElementOf0(sK0_skl(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f2100]) ).
fof(f2104,plain,
( ~ sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2101,f185]) ).
fof(f2105,plain,
~ sQ147_spl,
inference(contradiction_clause,[status(thm)],[f2104]) ).
fof(f2472,definition,
( sQ170_spl
<=> isCountable0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f2473,plain,
( ~ sQ170_spl
| isCountable0(slcrc0) ),
inference(component_clause,[status(thm)],[f2472]) ).
fof(f2478,plain,
( ~ sQ170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2473,f187]) ).
fof(f2479,plain,
~ sQ170_spl,
inference(contradiction_clause,[status(thm)],[f2478]) ).
fof(f2599,plain,
( sQ64_spl
| sbrdtbr0(sdtpldt0(sdtmndt0(xS,xx),xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx)))
| ~ aElement0(xx)
| ~ isFinite0(xS)
| ~ aSet0(xS)
| ~ aElement0(xx) ),
inference(resolution,[status(thm)],[f691,f771]) ).
fof(f2602,plain,
( sQ64_spl
| sQ49_spl
| ~ sQ17_spl
| ~ sQ5_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f2599,f274,f235,f313,f576,f689]) ).
fof(f2603,plain,
$false,
inference(sat_refutation,[status(thm)],[f244,f290,f334,f586,f1382,f1385,f1958,f2105,f2479,f2602]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM538+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n016.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 02:43:23 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 9.15/1.67 % Refutation found
% 9.15/1.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.15/1.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.15/1.73 % Elapsed time: 1.272189 seconds
% 9.15/1.73 % CPU time: 9.676760 seconds
% 9.15/1.73 % Total memory used: 166.025 MB
% 9.15/1.73 % Net memory used: 158.345 MB
%------------------------------------------------------------------------------