%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM597+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:41:08 PM UTC 2026
% Result : Theorem 0.20s 0.50s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 23
% Syntax : Number of formulae : 103 ( 20 unt; 13 def)
% Number of atoms : 315 ( 44 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 330 ( 118 ~; 115 |; 69 &)
% ( 18 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 13 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-2 aty)
% Number of variables : 76 ( 64 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> ~ isFinite0(W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [W0] :
( aFunction0(W0)
=> ( ( isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0)))
& isCountable0(szDzozmdt0(W0)) )
=> ( isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0)))
& aElement0(szDzizrdt0(W0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( ( aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
| ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )
& aSet0(W1) )
=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))
=> aElementOf0(W0,xT) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))
<=> ? [W1] :
( sdtlpdtrp0(xd,W1) = W0
& aElementOf0(W1,szDzozmdt0(xd)) ) )
& aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
~ ( ( ! [W0] :
( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) )
=> ~ ? [W0] : aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,conjecture,
aElementOf0(szDzizrdt0(xd),xT),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
~ aElementOf0(szDzizrdt0(xd),xT),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f107,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f108,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f108]) ).
fof(f110,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))],[f109]) ).
fof(f113,plain,
! [X0] :
( aElementOf0(sK0_skl(X0),X0)
| ~ aSet0(X0)
| X0 = slcrc0 ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f114,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f117,plain,
! [W0] :
( ~ isFinite0(W0)
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f118,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f129,plain,
! [W0] :
( ! [W1] :
( isFinite0(W1)
| ~ aSubsetOf0(W1,W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f130,plain,
! [X0,X1] :
( isFinite0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f174,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f350,plain,
! [W0] :
( ( isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0)))
& aElement0(szDzizrdt0(W0)) )
| ~ isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0)))
| ~ isCountable0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f352,plain,
! [X0] :
( isCountable0(sdtlbdtrb0(X0,szDzizrdt0(X0)))
| ~ isFinite0(sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ~ isCountable0(szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f353,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f354,plain,
isFinite0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f534,plain,
( ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)
| ( ~ aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ? [W2] :
( ~ aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aElementOf0(W2,W1) ) ) ) )
| ~ aSet0(W1) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f535,plain,
( ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)
| ( ~ aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ~ aElementOf0(sK32_skl(W1,W0),sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aElementOf0(sK32_skl(W1,W0),W1) ) ) )
| ~ aSet0(W1) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(W2,sK32_skl(W1,W0))],[f534]) ).
fof(f536,plain,
aFunction0(xd),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f537,plain,
szDzozmdt0(xd) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f542,plain,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))
<=> ? [W1] :
( sdtlpdtrp0(xd,W1) = W0
& aElementOf0(W1,szDzozmdt0(xd)) ) )
& aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(pre_NNF_transformation,[status(thm)],[f93]) ).
fof(f543,plain,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xd,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xd)) )
| aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ( ? [W1] :
( sdtlpdtrp0(xd,W1) = W0
& aElementOf0(W1,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) )
& aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(NNF_transformation,[status(thm)],[f542]) ).
fof(f544,plain,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xd,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xd)) )
| aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ! [W0] :
( ? [W1] :
( sdtlpdtrp0(xd,W1) = W0
& aElementOf0(W1,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(miniscoping,[status(thm)],[f543]) ).
fof(f545,plain,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xd,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xd)) )
| aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& ! [W0] :
( ( sdtlpdtrp0(xd,sK33_skl(W0)) = W0
& aElementOf0(sK33_skl(W0),szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd))) )
& aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(W1,sK33_skl(W0))],[f544]) ).
fof(f549,plain,
! [X0,X1] :
( sdtlpdtrp0(xd,X1) != X0
| ~ aElementOf0(X1,szDzozmdt0(xd))
| aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(cnf_transformation,[status(thm)],[f545]) ).
fof(f550,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(cnf_transformation,[status(thm)],[f545]) ).
fof(f551,plain,
aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT),
inference(cnf_transformation,[status(thm)],[f545]) ).
fof(f552,plain,
( ? [W0] : aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f553,plain,
( ? [W0] : aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(NNF_transformation,[status(thm)],[f552]) ).
fof(f554,plain,
( ? [W0] : aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(miniscoping,[status(thm)],[f553]) ).
fof(f555,plain,
( aElementOf0(sK34_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W0,sK34_skl)],[f554]) ).
fof(f556,plain,
aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))),
inference(cnf_transformation,[status(thm)],[f555]) ).
fof(f557,plain,
! [X0] :
( aElementOf0(X0,szDzozmdt0(xd))
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(cnf_transformation,[status(thm)],[f555]) ).
fof(f558,plain,
! [X0] :
( sdtlpdtrp0(xd,X0) = szDzizrdt0(xd)
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(cnf_transformation,[status(thm)],[f555]) ).
fof(f561,plain,
~ aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f785,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xd))
| aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(destructive_equality_resolution,[status(thm)],[f549]) ).
fof(f800,definition,
( sQ0_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f802,plain,
( sQ0_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f800]) ).
fof(f803,definition,
( sQ1_spl
<=> isCountable0(szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f805,plain,
( sQ1_spl
| ~ isCountable0(szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f803]) ).
fof(f806,definition,
( sQ2_spl
<=> isFinite0(sdtlcdtrc0(xd,szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f814,plain,
aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),xT),
inference(forward_demodulation,[status(thm)],[f537,f551]) ).
fof(f815,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0)) ),
inference(forward_demodulation,[status(thm)],[f537,f550]) ).
fof(f816,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(forward_demodulation,[status(thm)],[f537,f557]) ).
fof(f817,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xd))
| aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0)) ),
inference(forward_demodulation,[status(thm)],[f537,f785]) ).
fof(f818,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0)) ),
inference(forward_demodulation,[status(thm)],[f537,f817]) ).
fof(f819,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xd,X0),xT)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f818,f815]) ).
fof(f820,plain,
( isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ isFinite0(sdtlcdtrc0(xd,szNzAzT0))
| ~ isCountable0(szDzozmdt0(xd))
| ~ aFunction0(xd) ),
inference(paramodulation,[status(thm)],[f537,f352]) ).
fof(f821,definition,
( sQ4_spl
<=> isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f824,plain,
( sQ4_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f820,f800,f803,f806,f821]) ).
fof(f846,plain,
( sdtlpdtrp0(xd,sK0_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)))) = szDzizrdt0(xd)
| ~ aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlbdtrb0(xd,szDzizrdt0(xd)) = slcrc0 ),
inference(resolution,[status(thm)],[f113,f558]) ).
fof(f847,plain,
( aElementOf0(sK0_skl(sdtlbdtrb0(xd,szDzizrdt0(xd))),szNzAzT0)
| ~ aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlbdtrb0(xd,szDzizrdt0(xd)) = slcrc0 ),
inference(resolution,[status(thm)],[f113,f816]) ).
fof(f859,definition,
( sQ11_spl
<=> sdtlbdtrb0(xd,szDzizrdt0(xd)) = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( ~ sQ11_spl
| sdtlbdtrb0(xd,szDzizrdt0(xd)) = slcrc0 ),
inference(component_clause,[status(thm)],[f859]) ).
fof(f862,definition,
( sQ12_spl
<=> aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ12_spl
| ~ aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f865,definition,
( sQ13_spl
<=> sdtlpdtrp0(xd,sK0_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)))) = szDzizrdt0(xd) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( ~ sQ13_spl
| sdtlpdtrp0(xd,sK0_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)))) = szDzizrdt0(xd) ),
inference(component_clause,[status(thm)],[f865]) ).
fof(f868,plain,
( sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f846,f859,f862,f865]) ).
fof(f869,definition,
( sQ14_spl
<=> aElementOf0(sK0_skl(sdtlbdtrb0(xd,szDzizrdt0(xd))),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f872,plain,
( sQ14_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f847,f859,f862,f869]) ).
fof(f891,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f556]) ).
fof(f892,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f891]) ).
fof(f893,plain,
( sQ1_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f537,f805]) ).
fof(f894,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f893,f174]) ).
fof(f895,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f894]) ).
fof(f896,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f536]) ).
fof(f897,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f896]) ).
fof(f902,plain,
( ~ isFinite0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(resolution,[status(thm)],[f118,f556]) ).
fof(f926,definition,
( sQ26_spl
<=> isFinite0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( sQ26_spl
| ~ isFinite0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(component_clause,[status(thm)],[f926]) ).
fof(f929,plain,
( ~ sQ26_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f902,f821,f926]) ).
fof(f937,definition,
( sQ29_spl
<=> isFinite0(xT) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f939,plain,
( sQ29_spl
| ~ isFinite0(xT) ),
inference(component_clause,[status(thm)],[f937]) ).
fof(f945,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f939,f354]) ).
fof(f946,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f945]) ).
fof(f961,plain,
( sQ26_spl
| ~ sQ11_spl
| ~ isFinite0(slcrc0) ),
inference(forward_demodulation,[status(thm)],[f860,f928]) ).
fof(f962,plain,
( sQ26_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f961,f114]) ).
fof(f963,plain,
( sQ26_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f962]) ).
fof(f967,definition,
( sQ30_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f969,plain,
( sQ30_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f967]) ).
fof(f974,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f969,f353]) ).
fof(f975,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f974]) ).
fof(f1171,plain,
( isFinite0(sdtlcdtrc0(xd,szNzAzT0))
| ~ isFinite0(xT)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f130,f814]) ).
fof(f1175,plain,
( sQ2_spl
| ~ sQ29_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1171,f967,f937,f806]) ).
fof(f1209,plain,
( ~ sQ13_spl
| aElementOf0(szDzizrdt0(xd),xT)
| ~ aElementOf0(sK0_skl(sdtlbdtrb0(xd,szDzizrdt0(xd))),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f866,f819]) ).
fof(f1212,definition,
( sQ65_spl
<=> aElementOf0(szDzizrdt0(xd),xT) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1213,plain,
( ~ sQ65_spl
| aElementOf0(szDzizrdt0(xd),xT) ),
inference(component_clause,[status(thm)],[f1212]) ).
fof(f1215,plain,
( ~ sQ13_spl
| sQ65_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1209,f869,f1212,f865]) ).
fof(f1221,plain,
( ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1213,f561]) ).
fof(f1222,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f1221]) ).
fof(f1223,plain,
$false,
inference(sat_refutation,[status(thm)],[f824,f868,f872,f892,f895,f897,f929,f946,f963,f975,f1175,f1215,f1222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM597+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.40 % Computer : n007.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Mon Sep 21 02:41:35 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.20/0.46 % Drodi V4.1.1
% 0.20/0.50 % Refutation found
% 0.20/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.20/0.56 % Elapsed time: 0.141433 seconds
% 0.20/0.56 % CPU time: 0.167041 seconds
% 0.20/0.56 % Total memory used: 27.448 MB
% 0.20/0.56 % Net memory used: 27.364 MB
%------------------------------------------------------------------------------