%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM597+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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 65.89s 8.86s
% Output : CNFRefutation 65.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 34
% Syntax : Number of formulae : 145 ( 26 unt; 22 def)
% Number of atoms : 474 ( 66 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 546 ( 217 ~; 226 |; 62 &)
% ( 27 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 20 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-3 aty)
% Number of variables : 123 ( 116 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,definition,
! [W0,W1] :
( ( aElement0(W1)
& aFunction0(W0) )
=> ! [W2] :
( W2 = sdtlbdtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
& aSet0(W1) )
=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,hypothesis,
aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
sdtlbdtrb0(xd,szDzizrdt0(xd)) != slcrc0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,conjecture,
aElementOf0(szDzizrdt0(xd),xT),
file('/export/starexec/sandbox2/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(f111,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f121,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f122,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f122]) ).
fof(f124,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f123]) ).
fof(f125,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
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(f131,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f132,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f174,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f175,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f309,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtlbdtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) ) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f66]) ).
fof(f310,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) )
| aElementOf0(W3,W2) )
& ( sdtlpdtrp0(W0,W3) != W1
| ~ aElementOf0(W3,szDzozmdt0(W0))
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlbdtrb0(W0,W1) )
& ( ( ! [W3] :
( ( sdtlpdtrp0(W0,W3) != W1
| ~ aElementOf0(W3,szDzozmdt0(W0))
| aElementOf0(W3,W2) )
& ( ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtlbdtrb0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aFunction0(W0) ),
inference(NNF_transformation,[status(thm)],[f309]) ).
fof(f311,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) )
| aElementOf0(W3,W2) )
& ( sdtlpdtrp0(W0,W3) != W1
| ~ aElementOf0(W3,szDzozmdt0(W0))
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlbdtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sdtlpdtrp0(W0,W3) != W1
| ~ aElementOf0(W3,szDzozmdt0(W0))
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlbdtrb0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aFunction0(W0) ),
inference(miniscoping,[status(thm)],[f310]) ).
fof(f312,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( ( sdtlpdtrp0(W0,sK12_skl(W2,W1,W0)) = W1
& aElementOf0(sK12_skl(W2,W1,W0),szDzozmdt0(W0)) )
| aElementOf0(sK12_skl(W2,W1,W0),W2) )
& ( sdtlpdtrp0(W0,sK12_skl(W2,W1,W0)) != W1
| ~ aElementOf0(sK12_skl(W2,W1,W0),szDzozmdt0(W0))
| ~ aElementOf0(sK12_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtlbdtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sdtlpdtrp0(W0,W3) != W1
| ~ aElementOf0(W3,szDzozmdt0(W0))
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sdtlpdtrp0(W0,W3) = W1
& aElementOf0(W3,szDzozmdt0(W0)) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlbdtrb0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aFunction0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(W3,sK12_skl(W2,W1,W0))],[f311]) ).
fof(f318,plain,
! [X0,X1,X2] :
( aElementOf0(sK12_skl(X2,X1,X0),szDzozmdt0(X0))
| aElementOf0(sK12_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f319,plain,
! [X0,X1,X2] :
( sdtlpdtrp0(X0,sK12_skl(X2,X1,X0)) = X1
| aElementOf0(sK12_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f333,plain,
! [W0] :
( ! [W1] :
( aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0)))
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f334,plain,
! [X0,X1] :
( aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f333]) ).
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(f351,plain,
! [X0] :
( aElement0(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(f371,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f373,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f410,plain,
( ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)
| ~ aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
| ~ aSet0(W1) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f411,plain,
aFunction0(xd),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f412,plain,
szDzozmdt0(xd) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f414,plain,
aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f415,plain,
sdtlbdtrb0(xd,szDzizrdt0(xd)) != slcrc0,
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f416,plain,
~ aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f423,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f111]) ).
fof(f424,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f112]) ).
fof(f476,plain,
aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),xT),
inference(forward_demodulation,[status(thm)],[f412,f414]) ).
fof(f485,definition,
( sQ1_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f487,plain,
( sQ1_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f485]) ).
fof(f499,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f487,f423]) ).
fof(f500,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f499]) ).
fof(f503,definition,
( sQ4_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( sQ4_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f503]) ).
fof(f514,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f505,f353]) ).
fof(f515,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f514]) ).
fof(f528,definition,
( sQ9_spl
<=> aElement0(szDzizrdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( sQ9_spl
| ~ aElement0(szDzizrdt0(xd)) ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f553,definition,
( sQ14_spl
<=> isFinite0(xT) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ14_spl
| ~ isFinite0(xT) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f587,plain,
! [X0,X1] :
( sdtlpdtrp0(X0,sK12_skl(slcrc0,X1,X0)) = X1
| ~ aSet0(slcrc0)
| slcrc0 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(resolution,[status(thm)],[f319,f424]) ).
fof(f588,definition,
! [X0,X1] :
( sQ21_spl
<=> ( sdtlpdtrp0(X0,sK12_skl(slcrc0,X1,X0)) = X1
| slcrc0 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f589,plain,
! [X0,X1] :
( ~ sQ21_spl
| sdtlpdtrp0(X0,sK12_skl(slcrc0,X1,X0)) = X1
| slcrc0 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(component_clause,[status(thm)],[f588]) ).
fof(f591,plain,
( ~ sQ1_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f587,f588,f485]) ).
fof(f602,plain,
! [X0,X1] :
( aElementOf0(sK12_skl(slcrc0,X1,X0),szDzozmdt0(X0))
| ~ aSet0(slcrc0)
| slcrc0 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(resolution,[status(thm)],[f318,f424]) ).
fof(f603,definition,
! [X0,X1] :
( sQ24_spl
<=> ( aElementOf0(sK12_skl(slcrc0,X1,X0),szDzozmdt0(X0))
| slcrc0 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f604,plain,
! [X0,X1] :
( ~ sQ24_spl
| aElementOf0(sK12_skl(slcrc0,X1,X0),szDzozmdt0(X0))
| slcrc0 = sdtlbdtrb0(X0,X1)
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f606,plain,
( ~ sQ1_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f602,f603,f485]) ).
fof(f620,plain,
( sQ9_spl
| ~ isFinite0(sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ~ isCountable0(szDzozmdt0(xd))
| ~ aFunction0(xd) ),
inference(resolution,[status(thm)],[f530,f351]) ).
fof(f622,definition,
( sQ27_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f624,plain,
( sQ27_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f622]) ).
fof(f625,definition,
( sQ28_spl
<=> isCountable0(szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( sQ28_spl
| ~ isCountable0(szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f628,definition,
( sQ29_spl
<=> isFinite0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( sQ29_spl
| ~ isFinite0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(component_clause,[status(thm)],[f628]) ).
fof(f631,plain,
( sQ9_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f620,f622,f625,f628,f528]) ).
fof(f632,plain,
( sQ29_spl
| ~ isFinite0(sdtlcdtrc0(xd,szNzAzT0)) ),
inference(forward_demodulation,[status(thm)],[f412,f630]) ).
fof(f654,plain,
( sQ28_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f412,f627]) ).
fof(f655,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f654,f174]) ).
fof(f656,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f655]) ).
fof(f657,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f624,f411]) ).
fof(f658,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f657]) ).
fof(f660,plain,
! [X0] :
( ~ sQ24_spl
| aElementOf0(sK12_skl(slcrc0,X0,xd),szNzAzT0)
| slcrc0 = sdtlbdtrb0(xd,X0)
| ~ aElement0(X0)
| ~ aFunction0(xd) ),
inference(paramodulation,[status(thm)],[f412,f604]) ).
fof(f665,definition,
! [X0] :
( sQ34_spl
<=> ( aElementOf0(sK12_skl(slcrc0,X0,xd),szNzAzT0)
| slcrc0 = sdtlbdtrb0(xd,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f666,plain,
! [X0] :
( ~ sQ34_spl
| aElementOf0(sK12_skl(slcrc0,X0,xd),szNzAzT0)
| slcrc0 = sdtlbdtrb0(xd,X0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f665]) ).
fof(f668,plain,
( ~ sQ24_spl
| sQ34_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f660,f622,f665,f603]) ).
fof(f711,plain,
! [X0] :
( ~ aElementOf0(szDzizrdt0(xd),X0)
| ~ aSubsetOf0(X0,xT)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f126,f416]) ).
fof(f713,definition,
! [X0] :
( sQ43_spl
<=> ( ~ aElementOf0(szDzizrdt0(xd),X0)
| ~ aSubsetOf0(X0,xT) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f714,plain,
! [X0] :
( ~ sQ43_spl
| ~ aElementOf0(szDzizrdt0(xd),X0)
| ~ aSubsetOf0(X0,xT) ),
inference(component_clause,[status(thm)],[f713]) ).
fof(f716,plain,
( sQ43_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f711,f503,f713]) ).
fof(f722,plain,
! [X0,X1] :
( ~ sQ43_spl
| ~ aElementOf0(szDzizrdt0(xd),X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,xT) ),
inference(resolution,[status(thm)],[f714,f126]) ).
fof(f797,definition,
( sQ55_spl
<=> aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f799,plain,
( sQ55_spl
| ~ aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szNzAzT0)) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f820,definition,
( sQ59_spl
<=> aSet0(sdtlcdtrc0(xd,szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f822,plain,
( sQ59_spl
| ~ aSet0(sdtlcdtrc0(xd,szNzAzT0)) ),
inference(component_clause,[status(thm)],[f820]) ).
fof(f823,definition,
! [X0] :
( sQ60_spl
<=> ( ~ aElementOf0(szDzizrdt0(xd),X0)
| ~ aSubsetOf0(X0,sdtlcdtrc0(xd,szNzAzT0)) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f824,plain,
! [X0] :
( ~ sQ60_spl
| ~ aElementOf0(szDzizrdt0(xd),X0)
| ~ aSubsetOf0(X0,sdtlcdtrc0(xd,szNzAzT0)) ),
inference(component_clause,[status(thm)],[f823]) ).
fof(f842,plain,
! [X0] :
( sQ59_spl
| ~ aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f822,f125]) ).
fof(f843,plain,
( sQ59_spl
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f842,f476]) ).
fof(f846,plain,
( sQ59_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f843,f503,f820]) ).
fof(f855,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f354]) ).
fof(f856,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f855]) ).
fof(f870,plain,
! [X0] :
( ~ sQ43_spl
| ~ aElementOf0(szDzizrdt0(xd),X0)
| ~ aSubsetOf0(X0,sdtlcdtrc0(xd,szNzAzT0))
| ~ aSet0(sdtlcdtrc0(xd,szNzAzT0)) ),
inference(resolution,[status(thm)],[f722,f476]) ).
fof(f885,plain,
( ~ sQ43_spl
| sQ60_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f870,f820,f823,f713]) ).
fof(f1147,plain,
! [X0] :
( sQ29_spl
| ~ aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f130,f632]) ).
fof(f1221,plain,
( sQ29_spl
| ~ isFinite0(xT)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f1147,f476]) ).
fof(f1225,plain,
( sQ29_spl
| ~ sQ14_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1221,f503,f553,f628]) ).
fof(f2219,plain,
( ~ sQ60_spl
| ~ aSet0(sdtlcdtrc0(xd,szNzAzT0))
| ~ aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szNzAzT0)) ),
inference(resolution,[status(thm)],[f824,f132]) ).
fof(f2230,plain,
( ~ sQ60_spl
| ~ sQ59_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f2219,f797,f820,f823]) ).
fof(f6607,definition,
( sQ685_spl
<=> aElementOf0(sK12_skl(slcrc0,szDzizrdt0(xd),xd),szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f6609,plain,
( sQ685_spl
| ~ aElementOf0(sK12_skl(slcrc0,szDzizrdt0(xd),xd),szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f6607]) ).
fof(f6610,definition,
( sQ686_spl
<=> sdtlpdtrp0(xd,sK12_skl(slcrc0,szDzizrdt0(xd),xd)) = szDzizrdt0(xd) ),
introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition]) ).
fof(f6611,plain,
( ~ sQ686_spl
| sdtlpdtrp0(xd,sK12_skl(slcrc0,szDzizrdt0(xd),xd)) = szDzizrdt0(xd) ),
inference(component_clause,[status(thm)],[f6610]) ).
fof(f6612,plain,
( sQ686_spl
| sdtlpdtrp0(xd,sK12_skl(slcrc0,szDzizrdt0(xd),xd)) != szDzizrdt0(xd) ),
inference(component_clause,[status(thm)],[f6610]) ).
fof(f6614,plain,
( sQ685_spl
| ~ aElementOf0(sK12_skl(slcrc0,szDzizrdt0(xd),xd),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f412,f6609]) ).
fof(f7527,plain,
( ~ sQ21_spl
| sQ686_spl
| slcrc0 = sdtlbdtrb0(xd,szDzizrdt0(xd))
| ~ aElement0(szDzizrdt0(xd))
| ~ aFunction0(xd) ),
inference(resolution,[status(thm)],[f6612,f589]) ).
fof(f7537,definition,
( sQ781_spl
<=> slcrc0 = sdtlbdtrb0(xd,szDzizrdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ781_spl])],[split_symbol_definition]) ).
fof(f7538,plain,
( ~ sQ781_spl
| slcrc0 = sdtlbdtrb0(xd,szDzizrdt0(xd)) ),
inference(component_clause,[status(thm)],[f7537]) ).
fof(f7540,plain,
( ~ sQ21_spl
| sQ686_spl
| sQ781_spl
| ~ sQ9_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f7527,f622,f528,f7537,f6610,f588]) ).
fof(f7583,plain,
( ~ sQ781_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7538,f415]) ).
fof(f7584,plain,
~ sQ781_spl,
inference(contradiction_clause,[status(thm)],[f7583]) ).
fof(f7599,plain,
( ~ sQ34_spl
| sQ685_spl
| slcrc0 = sdtlbdtrb0(xd,szDzizrdt0(xd))
| ~ aElement0(szDzizrdt0(xd)) ),
inference(resolution,[status(thm)],[f6614,f666]) ).
fof(f7605,plain,
( ~ sQ34_spl
| sQ685_spl
| sQ781_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f7599,f528,f7537,f6607,f665]) ).
fof(f8021,definition,
( sQ842_spl
<=> aElementOf0(sz00,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ842_spl])],[split_symbol_definition]) ).
fof(f8023,plain,
( sQ842_spl
| ~ aElementOf0(sz00,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f8021]) ).
fof(f8033,plain,
( sQ842_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f373,f8023]) ).
fof(f8034,plain,
( sQ842_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8033,f175]) ).
fof(f8035,plain,
sQ842_spl,
inference(contradiction_clause,[status(thm)],[f8034]) ).
fof(f8050,plain,
( ~ sQ686_spl
| aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ~ aElementOf0(sK12_skl(slcrc0,szDzizrdt0(xd),xd),szDzozmdt0(xd))
| ~ aFunction0(xd) ),
inference(paramodulation,[status(thm)],[f6611,f334]) ).
fof(f8059,definition,
( sQ848_spl
<=> aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ848_spl])],[split_symbol_definition]) ).
fof(f8060,plain,
( ~ sQ848_spl
| aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(component_clause,[status(thm)],[f8059]) ).
fof(f8062,plain,
( ~ sQ686_spl
| sQ848_spl
| ~ sQ685_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f8050,f622,f6607,f8059,f6610]) ).
fof(f8079,plain,
( ~ sQ848_spl
| aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szNzAzT0)) ),
inference(forward_demodulation,[status(thm)],[f412,f8060]) ).
fof(f8080,plain,
( ~ sQ848_spl
| sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8079,f799]) ).
fof(f8081,plain,
( ~ sQ848_spl
| sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f8080]) ).
fof(f8082,plain,
$false,
inference(sat_refutation,[status(thm)],[f500,f515,f591,f606,f631,f656,f658,f668,f716,f846,f856,f885,f1225,f2230,f7540,f7584,f7605,f8035,f8062,f8081]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM597+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n007.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 02:41:06 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 65.89/8.86 % Refutation found
% 65.89/8.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 65.89/8.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 68.30/10.09 % Elapsed time: 9.444590 seconds
% 68.30/10.09 % CPU time: 64.852858 seconds
% 68.30/10.09 % Total memory used: 322.696 MB
% 68.30/10.09 % Net memory used: 290.720 MB
%------------------------------------------------------------------------------