%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM580+3 : 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:04 PM UTC 2026
% Result : Theorem 5.60s 1.10s
% Output : CNFRefutation 5.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 22
% Syntax : Number of formulae : 97 ( 17 unt; 12 def)
% Number of atoms : 330 ( 44 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 350 ( 117 ~; 117 |; 78 &)
% ( 19 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 13 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 62 ( 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [W0,W1] :
( ( aSet0(W1)
& aElement0(W0) )
=> ( ~ aElementOf0(W0,W1)
=> sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( ( isFinite0(W1)
& aSet0(W1) )
=> isFinite0(sdtpldt0(W1,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [W0] :
( aSet0(W0)
=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( ( aElementOf0(W1,W0)
& isFinite0(W0) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,conjecture,
( ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,negated_conjecture,
~ ( ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ),
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f95,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f96,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f155,plain,
! [W0,W1] :
( sdtmndt0(sdtpldt0(W1,W0),W0) = W1
| aElementOf0(W0,W1)
| ~ aSet0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f156,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| aElementOf0(X0,X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f161,plain,
! [W0] :
( ! [W1] :
( isFinite0(sdtpldt0(W1,W0))
| ~ isFinite0(W1)
| ~ aSet0(W1) )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f162,plain,
! [X0,X1] :
( isFinite0(sdtpldt0(X1,X0))
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f205,plain,
! [W0] :
( ( aElementOf0(sbrdtbr0(W0),szNzAzT0)
<=> isFinite0(W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f206,plain,
! [W0] :
( ( ( ~ isFinite0(W0)
| aElementOf0(sbrdtbr0(W0),szNzAzT0) )
& ( isFinite0(W0)
| ~ aElementOf0(sbrdtbr0(W0),szNzAzT0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f205]) ).
fof(f207,plain,
! [X0] :
( isFinite0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f215,plain,
! [W0] :
( ! [W1] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0)
| ~ aElementOf0(W1,W0)
| ~ isFinite0(W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f216,plain,
! [X0,X1] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0)
| ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f383,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f384,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f404,plain,
! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aSet0(sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f405,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f419,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f420,plain,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ)
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f421,plain,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ)
& ! [W0] :
( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi))
| ~ aElement0(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) )
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(NNF_transformation,[status(thm)],[f420]) ).
fof(f422,plain,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ)
& ! [W0] :
( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi))
| ~ aElement0(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) )
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(miniscoping,[status(thm)],[f421]) ).
fof(f423,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f428,plain,
! [X0] :
( X0 != szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f430,plain,
aSet0(xQ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f431,plain,
! [X0] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f433,plain,
sbrdtbr0(xQ) = xk,
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f435,plain,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != xK
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f436,plain,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != xK
& ! [W0] :
( ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(NNF_transformation,[status(thm)],[f435]) ).
fof(f437,plain,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != xK
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(miniscoping,[status(thm)],[f436]) ).
fof(f440,plain,
aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f444,plain,
! [X0] :
( X0 != szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElement0(X0)
| aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f445,plain,
sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != xK,
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f573,plain,
~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(destructive_equality_resolution,[status(thm)],[f428]) ).
fof(f574,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(destructive_equality_resolution,[status(thm)],[f444]) ).
fof(f723,definition,
( sQ7_spl
<=> aElement0(szmzizndt0(sdtlpdtrp0(xN,xi))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( ~ sQ7_spl
| aElement0(szmzizndt0(sdtlpdtrp0(xN,xi))) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f732,definition,
( sQ8_spl
<=> aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f733,plain,
( ~ sQ8_spl
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f735,plain,
( ~ sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f574,f732,f723]) ).
fof(f752,definition,
( sQ12_spl
<=> isFinite0(xQ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f856,definition,
( sQ22_spl
<=> isFinite0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f912,definition,
( sQ23_spl
<=> aSet0(xQ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f914,plain,
( sQ23_spl
| ~ aSet0(xQ) ),
inference(component_clause,[status(thm)],[f912]) ).
fof(f926,definition,
( sQ27_spl
<=> aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( sQ27_spl
| ~ aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(component_clause,[status(thm)],[f926]) ).
fof(f934,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f914,f430]) ).
fof(f935,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f934]) ).
fof(f936,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f928,f440]) ).
fof(f937,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f936]) ).
fof(f964,plain,
( aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))
| ~ aSet0(sdtlpdtrp0(xN,xi)) ),
inference(resolution,[status(thm)],[f423,f96]) ).
fof(f965,definition,
( sQ33_spl
<=> aSet0(sdtlpdtrp0(xN,xi)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( sQ33_spl
| ~ aSet0(sdtlpdtrp0(xN,xi)) ),
inference(component_clause,[status(thm)],[f965]) ).
fof(f972,plain,
( sQ7_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f964,f965,f723]) ).
fof(f986,plain,
! [X0] :
( ~ sQ7_spl
| isFinite0(sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f724,f162]) ).
fof(f988,plain,
! [X0] :
( ~ sQ7_spl
| sdtmndt0(sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))) = X0
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f724,f156]) ).
fof(f1126,plain,
( ~ sQ8_spl
| szszuzczcdt0(sbrdtbr0(sdtmndt0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))))) = sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ isFinite0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(resolution,[status(thm)],[f733,f216]) ).
fof(f1129,definition,
( sQ52_spl
<=> aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xQ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1130,plain,
( ~ sQ52_spl
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xQ) ),
inference(component_clause,[status(thm)],[f1129]) ).
fof(f1138,definition,
( sQ54_spl
<=> szszuzczcdt0(sbrdtbr0(sdtmndt0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))))) = sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1139,plain,
( ~ sQ54_spl
| szszuzczcdt0(sbrdtbr0(sdtmndt0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))))) = sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(component_clause,[status(thm)],[f1138]) ).
fof(f1141,plain,
( ~ sQ8_spl
| sQ54_spl
| ~ sQ22_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1126,f926,f856,f1138,f732]) ).
fof(f1196,plain,
aSet0(sdtlpdtrp0(xN,xi)),
inference(resolution,[status(thm)],[f405,f419]) ).
fof(f1197,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1196,f967]) ).
fof(f1198,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1197]) ).
fof(f3631,plain,
( ~ sQ7_spl
| isFinite0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ isFinite0(xQ) ),
inference(resolution,[status(thm)],[f986,f430]) ).
fof(f3640,plain,
( ~ sQ7_spl
| sQ22_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f3631,f752,f856,f723]) ).
fof(f3722,plain,
( ~ sQ7_spl
| sdtmndt0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))) = xQ
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xQ) ),
inference(resolution,[status(thm)],[f988,f430]) ).
fof(f3731,definition,
( sQ322_spl
<=> sdtmndt0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))) = xQ ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f3732,plain,
( ~ sQ322_spl
| sdtmndt0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szmzizndt0(sdtlpdtrp0(xN,xi))) = xQ ),
inference(component_clause,[status(thm)],[f3731]) ).
fof(f3734,plain,
( ~ sQ7_spl
| sQ322_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f3722,f1129,f3731,f723]) ).
fof(f4881,definition,
( sQ386_spl
<=> aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f4882,plain,
( ~ sQ386_spl
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(component_clause,[status(thm)],[f4881]) ).
fof(f4906,plain,
( ~ sQ386_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4882,f573]) ).
fof(f4907,plain,
~ sQ386_spl,
inference(contradiction_clause,[status(thm)],[f4906]) ).
fof(f5080,definition,
( sQ412_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition]) ).
fof(f5082,plain,
( sQ412_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(component_clause,[status(thm)],[f5080]) ).
fof(f5087,plain,
( sQ412_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5082,f383]) ).
fof(f5088,plain,
sQ412_spl,
inference(contradiction_clause,[status(thm)],[f5087]) ).
fof(f5409,plain,
( isFinite0(xQ)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aSet0(xQ) ),
inference(paramodulation,[status(thm)],[f433,f207]) ).
fof(f5410,plain,
( sQ12_spl
| ~ sQ412_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f5409,f912,f5080,f752]) ).
fof(f5478,plain,
( ~ sQ52_spl
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(resolution,[status(thm)],[f1130,f431]) ).
fof(f5486,plain,
( ~ sQ52_spl
| sQ386_spl ),
inference(split_clause,[status(thm)],[f5478,f4881,f1129]) ).
fof(f5499,plain,
( ~ sQ54_spl
| ~ sQ322_spl
| szszuzczcdt0(sbrdtbr0(xQ)) = sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(backward_demodulation,[status(thm)],[f3732,f1139]) ).
fof(f5504,plain,
( ~ sQ54_spl
| ~ sQ322_spl
| szszuzczcdt0(xk) = sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(forward_demodulation,[status(thm)],[f433,f5499]) ).
fof(f5505,plain,
( ~ sQ54_spl
| ~ sQ322_spl
| xK = sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(forward_demodulation,[status(thm)],[f384,f5504]) ).
fof(f5506,plain,
( ~ sQ54_spl
| ~ sQ322_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5505,f445]) ).
fof(f5507,plain,
( ~ sQ54_spl
| ~ sQ322_spl ),
inference(contradiction_clause,[status(thm)],[f5506]) ).
fof(f5508,plain,
$false,
inference(sat_refutation,[status(thm)],[f735,f935,f937,f972,f1141,f1198,f3640,f3734,f4907,f5088,f5410,f5486,f5507]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM580+3 : 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:41:08 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.32 % Drodi V4.1.1
% 5.60/1.10 % Refutation found
% 5.60/1.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.60/1.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.60/1.13 % Elapsed time: 0.803801 seconds
% 5.60/1.13 % CPU time: 6.095785 seconds
% 5.60/1.13 % Total memory used: 216.208 MB
% 5.60/1.13 % Net memory used: 206.821 MB
%------------------------------------------------------------------------------