%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM594+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 : n012.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:07 PM UTC 2026
% Result : Theorem 0.07s 0.40s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 25
% Syntax : Number of formulae : 105 ( 26 unt; 14 def)
% Number of atoms : 312 ( 63 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 325 ( 118 ~; 117 |; 62 &)
% ( 18 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 13 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 13 con; 0-4 aty)
% Number of variables : 89 ( 76 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
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(f68,definition,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aSubsetOf0(W1,szDzozmdt0(W0))
=> ! [W2] :
( W2 = sdtlcdtrc0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) ) )
& aSet0(W2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
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(f86,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ! [W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& aSet0(W1) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
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(f94,hypothesis,
aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,conjecture,
? [W0] :
( sdtlpdtrp0(xd,W0) = xx
& aElementOf0(W0,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
~ ? [W0] :
( sdtlpdtrp0(xd,W0) = xx
& aElementOf0(W0,szNzAzT0) ),
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(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(f173,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f175,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f322,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( W2 = sdtlcdtrc0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) ) )
& aSet0(W2) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f323,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( ? [W3] :
( ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ( ( ! [W3] :
( ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(NNF_transformation,[status(thm)],[f322]) ).
fof(f324,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( ? [W3] :
( ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ! [W3] :
( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(miniscoping,[status(thm)],[f323]) ).
fof(f325,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( ( ( ( sdtlpdtrp0(W0,sK15_skl(W2,W1,W0)) = sK14_skl(W2,W1,W0)
& aElementOf0(sK15_skl(W2,W1,W0),W1) )
| aElementOf0(sK14_skl(W2,W1,W0),W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != sK14_skl(W2,W1,W0)
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(sK14_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sdtlpdtrp0(W0,sK13_skl(W3,W2,W1,W0)) = W3
& aElementOf0(sK13_skl(W3,W2,W1,W0),W1) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W4,sK13_skl(W3,W2,W1,W0)),skolemize(W3,sK14_skl(W2,W1,W0)),skolemize(W4,sK15_skl(W2,W1,W0))],[f324]) ).
fof(f327,plain,
! [X0,X1,X2,X3] :
( aElementOf0(sK13_skl(X3,X2,X1,X0),X1)
| ~ aElementOf0(X3,X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f328,plain,
! [X0,X1,X2,X3] :
( sdtlpdtrp0(X0,sK13_skl(X3,X2,X1,X0)) = X3
| ~ aElementOf0(X3,X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f353,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f354,plain,
isFinite0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f369,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
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(f372,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f373,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f386,plain,
( ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f387,plain,
aFunction0(xC),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f406,plain,
( ! [W0] :
( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f407,plain,
aFunction0(xe),
inference(cnf_transformation,[status(thm)],[f406]) ).
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(f415,plain,
aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd))),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f416,plain,
! [W0] :
( sdtlpdtrp0(xd,W0) != xx
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f96]) ).
fof(f417,plain,
! [X0] :
( sdtlpdtrp0(xd,X0) != xx
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f424,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f111]) ).
fof(f466,plain,
! [X0,X1,X2] :
( aElementOf0(sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0),X1)
| ~ aElementOf0(X2,sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f327]) ).
fof(f467,plain,
! [X0,X1,X2] :
( sdtlpdtrp0(X0,sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0)) = X2
| ~ aElementOf0(X2,sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f328]) ).
fof(f478,plain,
aElementOf0(xx,sdtlcdtrc0(xd,szNzAzT0)),
inference(forward_demodulation,[status(thm)],[f412,f415]) ).
fof(f498,definition,
( sQ3_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( sQ3_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f498]) ).
fof(f505,definition,
( sQ5_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ5_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f518,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f173]) ).
fof(f519,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f518]) ).
fof(f840,definition,
! [X0] :
( sQ39_spl
<=> ( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f841,plain,
! [X0] :
( ~ sQ39_spl
| ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f857,plain,
! [X0] :
( ~ sQ39_spl
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f841]) ).
fof(f867,definition,
( sQ40_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f869,plain,
( sQ40_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f867]) ).
fof(f874,definition,
( sQ42_spl
<=> aFunction0(xC) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f876,plain,
( sQ42_spl
| ~ aFunction0(xC) ),
inference(component_clause,[status(thm)],[f874]) ).
fof(f881,definition,
( sQ44_spl
<=> aFunction0(xe) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f883,plain,
( sQ44_spl
| ~ aFunction0(xe) ),
inference(component_clause,[status(thm)],[f881]) ).
fof(f888,definition,
( sQ46_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( sQ46_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f888]) ).
fof(f895,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f890,f411]) ).
fof(f896,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f895]) ).
fof(f897,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f883,f407]) ).
fof(f898,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f897]) ).
fof(f899,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f876,f387]) ).
fof(f900,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f899]) ).
fof(f901,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f869,f372]) ).
fof(f902,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f901]) ).
fof(f903,plain,
( ~ sQ39_spl
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f857,f354]) ).
fof(f905,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f903,f353]) ).
fof(f906,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f905]) ).
fof(f908,definition,
( sQ48_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f910,plain,
( sQ48_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(component_clause,[status(thm)],[f908]) ).
fof(f915,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f910,f369]) ).
fof(f916,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f915]) ).
fof(f924,definition,
( sQ51_spl
<=> aElementOf0(sz00,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f926,plain,
( sQ51_spl
| ~ aElementOf0(sz00,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f924]) ).
fof(f938,plain,
( sQ51_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f373,f926]) ).
fof(f939,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f938,f175]) ).
fof(f940,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f939]) ).
fof(f945,plain,
( aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0)
| ~ aSubsetOf0(szNzAzT0,szDzozmdt0(xd))
| ~ aFunction0(xd) ),
inference(resolution,[status(thm)],[f466,f478]) ).
fof(f946,definition,
( sQ55_spl
<=> aSubsetOf0(szNzAzT0,szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f948,plain,
( sQ55_spl
| ~ aSubsetOf0(szNzAzT0,szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f946]) ).
fof(f949,definition,
( sQ56_spl
<=> aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( ~ sQ56_spl
| aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f952,plain,
( sQ56_spl
| ~ sQ55_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f945,f888,f946,f949]) ).
fof(f953,plain,
( sQ55_spl
| ~ aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f412,f948]) ).
fof(f954,plain,
( sQ55_spl
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f953,f132]) ).
fof(f955,plain,
( sQ55_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f954,f505,f946]) ).
fof(f988,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f500,f424]) ).
fof(f989,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f988]) ).
fof(f1005,plain,
( sdtlpdtrp0(xd,sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd)) = xx
| ~ aSubsetOf0(szNzAzT0,szDzozmdt0(xd))
| ~ aFunction0(xd) ),
inference(resolution,[status(thm)],[f467,f478]) ).
fof(f1010,definition,
( sQ64_spl
<=> sdtlpdtrp0(xd,sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd)) = xx ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
( ~ sQ64_spl
| sdtlpdtrp0(xd,sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd)) = xx ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,plain,
( sQ64_spl
| ~ sQ55_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1005,f888,f946,f1010]) ).
fof(f1048,plain,
( ~ sQ64_spl
| ~ aElementOf0(sK13_skl(xx,sdtlcdtrc0(xd,szNzAzT0),szNzAzT0,xd),szNzAzT0) ),
inference(resolution,[status(thm)],[f1011,f417]) ).
fof(f1053,plain,
( ~ sQ64_spl
| ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1048,f950]) ).
fof(f1054,plain,
( ~ sQ64_spl
| ~ sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f1053]) ).
fof(f1055,plain,
$false,
inference(sat_refutation,[status(thm)],[f519,f896,f898,f900,f902,f906,f916,f940,f952,f955,f989,f1013,f1054]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM594+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Mon Sep 21 02:43:00 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.32 % Drodi V4.1.1
% 0.07/0.40 % Refutation found
% 0.07/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.07/0.42 % Elapsed time: 0.110259 seconds
% 0.07/0.42 % CPU time: 0.651515 seconds
% 0.07/0.42 % Total memory used: 127.961 MB
% 0.07/0.42 % Net memory used: 126.531 MB
%------------------------------------------------------------------------------