%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM603+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 : n011.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:09 PM UTC 2026
% Result : Theorem 6.30s 1.23s
% Output : CNFRefutation 6.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 40
% Syntax : Number of formulae : 160 ( 49 unt; 22 def)
% Number of atoms : 389 ( 54 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 348 ( 119 ~; 124 |; 65 &)
% ( 26 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 21 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 14 con; 0-3 aty)
% Number of variables : 75 ( 70 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> W0 != szszuzczcdt0(W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(sz00,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,definition,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aFunction0(xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W1,W0)
=> aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
( isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
( sdtlpdtrp0(xe,xi) = xx
& aElementOf0(xi,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,conjecture,
aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,negated_conjecture,
~ aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
inference(negated_conjecture,[status(cth)],[f100]) ).
fof(f112,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f113,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f113]) ).
fof(f115,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))],[f114]) ).
fof(f117,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f136,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f137,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f178,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f179,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f180,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f190,plain,
! [W0] :
( W0 != szszuzczcdt0(W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f191,plain,
! [X0] :
( X0 != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f194,plain,
! [W0] :
( sdtlseqdt0(sz00,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f195,plain,
! [X0] :
( sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f254,plain,
! [W0] :
( ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f255,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| aElementOf0(W2,W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ( ( ! [W2] :
( ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) ) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f254]) ).
fof(f256,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| aElementOf0(W2,W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ! [W1] :
( ( ! [W2] :
( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f255]) ).
fof(f257,plain,
! [W0] :
( ( ! [W1] :
( ( ( ( sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)
& aElementOf0(sK8_skl(W1,W0),szNzAzT0) )
| aElementOf0(sK8_skl(W1,W0),W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)
| ~ aElementOf0(sK8_skl(W1,W0),szNzAzT0)
| ~ aElementOf0(sK8_skl(W1,W0),W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ! [W1] :
( ( ! [W2] :
( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W2,sK8_skl(W1,W0))],[f256]) ).
fof(f258,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f310,plain,
! [W0] :
( aSet0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f311,plain,
! [X0] :
( aSet0(szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f360,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f362,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f363,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f374,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f375,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f376,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(f377,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f379,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f385,plain,
! [W0,W1] :
( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
| ~ sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f386,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f391,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(f392,plain,
aFunction0(xC),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f411,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(f412,plain,
aFunction0(xe),
inference(cnf_transformation,[status(thm)],[f411]) ).
fof(f413,plain,
szDzozmdt0(xe) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f411]) ).
fof(f415,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(f416,plain,
aFunction0(xd),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f420,plain,
aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f421,plain,
isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f432,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f434,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f442,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f117]) ).
fof(f458,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f258]) ).
fof(f484,plain,
aSubsetOf0(szNzAzT0,szNzAzT0),
inference(resolution,[status(thm)],[f178,f137]) ).
fof(f592,definition,
( sQ21_spl
<=> aElementOf0(sz00,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f594,plain,
( sQ21_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(component_clause,[status(thm)],[f592]) ).
fof(f837,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f180,f594]) ).
fof(f838,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f837]) ).
fof(f957,plain,
aSet0(szDzozmdt0(xc)),
inference(resolution,[status(thm)],[f311,f363]) ).
fof(f1038,plain,
aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc)),
inference(resolution,[status(thm)],[f957,f137]) ).
fof(f1124,definition,
( sQ102_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1126,plain,
( sQ102_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1124]) ).
fof(f1131,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1126,f432]) ).
fof(f1132,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f1131]) ).
fof(f1363,plain,
xk != szszuzczcdt0(xk),
inference(resolution,[status(thm)],[f374,f191]) ).
fof(f1374,plain,
xk != xK,
inference(forward_demodulation,[status(thm)],[f375,f1363]) ).
fof(f1382,definition,
( sQ132_spl
<=> xK = xk ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1383,plain,
( ~ sQ132_spl
| xK = xk ),
inference(component_clause,[status(thm)],[f1382]) ).
fof(f1891,definition,
( sQ198_spl
<=> xT = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1892,plain,
( ~ sQ198_spl
| xT = slcrc0 ),
inference(component_clause,[status(thm)],[f1891]) ).
fof(f1958,plain,
( ~ sQ198_spl
| aElementOf0(szDzizrdt0(xd),slcrc0) ),
inference(backward_demodulation,[status(thm)],[f1892,f420]) ).
fof(f1963,plain,
( ~ sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1958,f442]) ).
fof(f1964,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f1963]) ).
fof(f2332,definition,
( sQ251_spl
<=> aSet0(szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f2334,plain,
( sQ251_spl
| ~ aSet0(szDzozmdt0(xc)) ),
inference(component_clause,[status(thm)],[f2332]) ).
fof(f2339,definition,
( sQ253_spl
<=> aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f2341,plain,
( sQ253_spl
| ~ aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc)) ),
inference(component_clause,[status(thm)],[f2339]) ).
fof(f2350,plain,
( sQ251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2334,f957]) ).
fof(f2351,plain,
sQ251_spl,
inference(contradiction_clause,[status(thm)],[f2350]) ).
fof(f2352,plain,
( sQ253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2341,f1038]) ).
fof(f2353,plain,
sQ253_spl,
inference(contradiction_clause,[status(thm)],[f2352]) ).
fof(f2406,plain,
( ~ sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1383,f1374]) ).
fof(f2407,plain,
~ sQ132_spl,
inference(contradiction_clause,[status(thm)],[f2406]) ).
fof(f2576,definition,
( sQ289_spl
<=> aSet0(slbdtrb0(xK)) ),
introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition]) ).
fof(f2578,plain,
( sQ289_spl
| ~ aSet0(slbdtrb0(xK)) ),
inference(component_clause,[status(thm)],[f2576]) ).
fof(f2836,plain,
( sQ289_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolution,[status(thm)],[f2578,f458]) ).
fof(f2838,plain,
( sQ289_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2836,f360]) ).
fof(f2839,plain,
sQ289_spl,
inference(contradiction_clause,[status(thm)],[f2838]) ).
fof(f3225,definition,
( sQ369_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f3227,plain,
( sQ369_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f3225]) ).
fof(f3418,definition,
( sQ404_spl
<=> isCountable0(xS) ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f3420,plain,
( sQ404_spl
| ~ isCountable0(xS) ),
inference(component_clause,[status(thm)],[f3418]) ).
fof(f3422,plain,
( sQ404_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3420,f362]) ).
fof(f3423,plain,
sQ404_spl,
inference(contradiction_clause,[status(thm)],[f3422]) ).
fof(f3702,plain,
( sQ369_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3227,f377]) ).
fof(f3703,plain,
sQ369_spl,
inference(contradiction_clause,[status(thm)],[f3702]) ).
fof(f3714,definition,
( sQ449_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition]) ).
fof(f3716,plain,
( sQ449_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f3714]) ).
fof(f3721,definition,
( sQ451_spl
<=> aFunction0(xe) ),
introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition]) ).
fof(f3723,plain,
( sQ451_spl
| ~ aFunction0(xe) ),
inference(component_clause,[status(thm)],[f3721]) ).
fof(f3728,definition,
( sQ453_spl
<=> aFunction0(xC) ),
introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition]) ).
fof(f3730,plain,
( sQ453_spl
| ~ aFunction0(xC) ),
inference(component_clause,[status(thm)],[f3728]) ).
fof(f3739,plain,
( sQ453_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3730,f392]) ).
fof(f3740,plain,
sQ453_spl,
inference(contradiction_clause,[status(thm)],[f3739]) ).
fof(f3741,plain,
( sQ451_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3723,f412]) ).
fof(f3742,plain,
sQ451_spl,
inference(contradiction_clause,[status(thm)],[f3741]) ).
fof(f3743,plain,
( sQ449_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3716,f416]) ).
fof(f3744,plain,
sQ449_spl,
inference(contradiction_clause,[status(thm)],[f3743]) ).
fof(f4154,definition,
( sQ477_spl
<=> aSubsetOf0(szNzAzT0,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ477_spl])],[split_symbol_definition]) ).
fof(f4156,plain,
( sQ477_spl
| ~ aSubsetOf0(szNzAzT0,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f4154]) ).
fof(f4166,plain,
( sQ477_spl
| ~ aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f378,f4156]) ).
fof(f4167,plain,
( sQ477_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4166,f484]) ).
fof(f4168,plain,
sQ477_spl,
inference(contradiction_clause,[status(thm)],[f4167]) ).
fof(f4574,definition,
( sQ528_spl
<=> isCountable0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ528_spl])],[split_symbol_definition]) ).
fof(f4576,plain,
( sQ528_spl
| ~ isCountable0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f4574]) ).
fof(f4605,plain,
( sQ528_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4576,f179]) ).
fof(f4606,plain,
sQ528_spl,
inference(contradiction_clause,[status(thm)],[f4605]) ).
fof(f4635,definition,
( sQ540_spl
<=> sdtlpdtrp0(xN,sK16_skl(xN,szNzAzT0,xN)) = sdtlpdtrp0(xN,sK16_skl(xN,szNzAzT0,xN)) ),
introduced(definition,[new_symbols(definition,[sQ540_spl])],[split_symbol_definition]) ).
fof(f4637,plain,
( sQ540_spl
| sdtlpdtrp0(xN,sK16_skl(xN,szNzAzT0,xN)) != sdtlpdtrp0(xN,sK16_skl(xN,szNzAzT0,xN)) ),
inference(component_clause,[status(thm)],[f4635]) ).
fof(f4639,plain,
( sQ540_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4637]) ).
fof(f4640,plain,
sQ540_spl,
inference(contradiction_clause,[status(thm)],[f4639]) ).
fof(f4941,definition,
( sQ561_spl
<=> aFunction0(xc) ),
introduced(definition,[new_symbols(definition,[sQ561_spl])],[split_symbol_definition]) ).
fof(f4943,plain,
( sQ561_spl
| ~ aFunction0(xc) ),
inference(component_clause,[status(thm)],[f4941]) ).
fof(f4951,plain,
( sQ561_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4943,f363]) ).
fof(f4952,plain,
sQ561_spl,
inference(contradiction_clause,[status(thm)],[f4951]) ).
fof(f5010,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f379,f386]) ).
fof(f5016,definition,
! [X0] :
( sQ570_spl
<=> ( aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f5017,plain,
! [X0] :
( ~ sQ570_spl
| aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f5016]) ).
fof(f5019,plain,
( ~ sQ21_spl
| sQ570_spl ),
inference(split_clause,[status(thm)],[f5010,f5016,f592]) ).
fof(f5020,plain,
! [X0] :
( ~ sQ570_spl
| aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5017,f195]) ).
fof(f5482,definition,
( sQ647_spl
<=> aElementOf0(xK,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition]) ).
fof(f5484,plain,
( sQ647_spl
| ~ aElementOf0(xK,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f5482]) ).
fof(f5490,plain,
( sQ647_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f378,f5484]) ).
fof(f5491,plain,
( sQ647_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5490,f360]) ).
fof(f5492,plain,
sQ647_spl,
inference(contradiction_clause,[status(thm)],[f5491]) ).
fof(f5587,definition,
( sQ662_spl
<=> aElementOf0(xi,szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ662_spl])],[split_symbol_definition]) ).
fof(f5589,plain,
( sQ662_spl
| ~ aElementOf0(xi,szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f5587]) ).
fof(f5595,plain,
( sQ662_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f413,f5589]) ).
fof(f5596,plain,
( sQ662_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5595,f432]) ).
fof(f5597,plain,
sQ662_spl,
inference(contradiction_clause,[status(thm)],[f5596]) ).
fof(f5901,definition,
( sQ692_spl
<=> isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ692_spl])],[split_symbol_definition]) ).
fof(f5903,plain,
( sQ692_spl
| ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(component_clause,[status(thm)],[f5901]) ).
fof(f5941,plain,
( sQ692_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5903,f421]) ).
fof(f5942,plain,
sQ692_spl,
inference(contradiction_clause,[status(thm)],[f5941]) ).
fof(f6182,plain,
( ~ sQ570_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f5020,f434]) ).
fof(f6187,plain,
( ~ sQ570_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f6182,f1124,f5016]) ).
fof(f6201,plain,
$false,
inference(sat_refutation,[status(thm)],[f838,f1132,f1964,f2351,f2353,f2407,f2839,f3423,f3703,f3740,f3742,f3744,f4168,f4606,f4640,f4952,f5019,f5492,f5597,f5942,f6187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM603+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 02:43:55 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 6.30/1.23 % Refutation found
% 6.30/1.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.30/1.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.30/1.26 % Elapsed time: 0.884745 seconds
% 6.30/1.26 % CPU time: 6.693326 seconds
% 6.30/1.26 % Total memory used: 170.668 MB
% 6.30/1.26 % Net memory used: 163.908 MB
%------------------------------------------------------------------------------