%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM592+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:07 PM UTC 2026
% Result : Theorem 1.17s 0.58s
% Output : CNFRefutation 1.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 30
% Syntax : Number of formulae : 121 ( 36 unt; 17 def)
% Number of atoms : 275 ( 37 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 232 ( 78 ~; 83 |; 46 &)
% ( 17 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 18 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 14 con; 0-2 aty)
% Number of variables : 37 ( 32 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> isFinite0(slbdtrb0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
aElementOf0(xK,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(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(f89,hypothesis,
iLess0(xk,xK),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,hypothesis,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
& szDzozmdt0(xd) = slbdtsldtrb0(xY,xk)
& aFunction0(xd)
& isCountable0(xY)
& aSubsetOf0(xY,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,hypothesis,
( ! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xX,xk))
& aSet0(W0) )
=> sdtlpdtrp0(xd,W0) = xu )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& aElementOf0(xu,xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,conjecture,
? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xk))
& aSet0(W2) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) = W0 )
& isCountable0(W1)
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aElementOf0(W0,xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,negated_conjecture,
~ ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xk))
& aSet0(W2) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) = W0 )
& isCountable0(W1)
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aElementOf0(W0,xT) ),
inference(negated_conjecture,[status(cth)],[f94]) ).
fof(f173,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f259,plain,
! [W0] :
( isFinite0(slbdtrb0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f260,plain,
! [X0] :
( isFinite0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f354,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f357,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f368,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f370,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(f371,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f372,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f385,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(f386,plain,
aFunction0(xC),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f387,plain,
szDzozmdt0(xC) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f395,plain,
iLess0(xk,xK),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f396,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f397,plain,
xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f398,plain,
xd = sdtlpdtrp0(xC,xi),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f400,plain,
isCountable0(xY),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f401,plain,
aFunction0(xd),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f404,plain,
( ! [W0] :
( sdtlpdtrp0(xd,W0) = xu
| ~ aElementOf0(W0,slbdtsldtrb0(xX,xk))
| ~ aSet0(W0) )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& aElementOf0(xu,xT) ),
inference(pre_NNF_transformation,[status(thm)],[f93]) ).
fof(f405,plain,
aElementOf0(xu,xT),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f406,plain,
aSubsetOf0(xX,xY),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f407,plain,
isCountable0(xX),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f408,plain,
! [X0] :
( sdtlpdtrp0(xd,X0) = xu
| ~ aElementOf0(X0,slbdtsldtrb0(xX,xk))
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f409,plain,
! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xk))
& aSet0(W2) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aElementOf0(W0,xT) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f410,plain,
! [W0] :
( ! [W1] :
( ( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(W1,W0)) != W0
& aElementOf0(sK21_skl(W1,W0),slbdtsldtrb0(W1,xk))
& aSet0(sK21_skl(W1,W0)) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aElementOf0(W0,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W2,sK21_skl(W1,W0))],[f409]) ).
fof(f411,plain,
! [X0,X1] :
( aSet0(sK21_skl(X1,X0))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f412,plain,
! [X0,X1] :
( aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xk))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f413,plain,
! [X0,X1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(X1,X0)) != X0
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f1182,definition,
( sQ96_spl
<=> isCountable0(xY) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1184,plain,
( sQ96_spl
| ~ isCountable0(xY) ),
inference(component_clause,[status(thm)],[f1182]) ).
fof(f1248,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(X0,xu)) != xu
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(resolution,[status(thm)],[f405,f413]) ).
fof(f1250,plain,
! [X0] :
( aSet0(sK21_skl(X0,xu))
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(resolution,[status(thm)],[f405,f411]) ).
fof(f1369,definition,
( sQ117_spl
<=> isCountable0(xX) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1371,plain,
( sQ117_spl
| ~ isCountable0(xX) ),
inference(component_clause,[status(thm)],[f1369]) ).
fof(f2149,plain,
isFinite0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f368,f260]) ).
fof(f2499,plain,
( sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1371,f407]) ).
fof(f2500,plain,
sQ117_spl,
inference(contradiction_clause,[status(thm)],[f2499]) ).
fof(f2501,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1184,f400]) ).
fof(f2502,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f2501]) ).
fof(f2588,definition,
( sQ258_spl
<=> aFunction0(xC) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f2590,plain,
( sQ258_spl
| ~ aFunction0(xC) ),
inference(component_clause,[status(thm)],[f2588]) ).
fof(f2595,definition,
( sQ260_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f2597,plain,
( sQ260_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f2595]) ).
fof(f2602,plain,
( sQ260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2597,f371]) ).
fof(f2603,plain,
sQ260_spl,
inference(contradiction_clause,[status(thm)],[f2602]) ).
fof(f2604,plain,
( sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2590,f386]) ).
fof(f2605,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f2604]) ).
fof(f2889,definition,
( sQ279_spl
<=> szmzizndt0(sdtlpdtrp0(xN,xk)) = szmzizndt0(sdtlpdtrp0(xN,xk)) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f2891,plain,
( sQ279_spl
| szmzizndt0(sdtlpdtrp0(xN,xk)) != szmzizndt0(sdtlpdtrp0(xN,xk)) ),
inference(component_clause,[status(thm)],[f2889]) ).
fof(f2893,plain,
( sQ279_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2891]) ).
fof(f2894,plain,
sQ279_spl,
inference(contradiction_clause,[status(thm)],[f2893]) ).
fof(f2910,definition,
( sQ280_spl
<=> isFinite0(slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f2912,plain,
( sQ280_spl
| ~ isFinite0(slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f2910]) ).
fof(f3189,definition,
( sQ315_spl
<=> isCountable0(szDzozmdt0(xC)) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f3191,plain,
( sQ315_spl
| ~ isCountable0(szDzozmdt0(xC)) ),
inference(component_clause,[status(thm)],[f3189]) ).
fof(f3199,definition,
( sQ318_spl
<=> isCountable0(szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f3201,plain,
( sQ318_spl
| ~ isCountable0(szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f3199]) ).
fof(f3209,plain,
( sQ318_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f372,f3201]) ).
fof(f3210,plain,
( sQ318_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3209,f173]) ).
fof(f3211,plain,
sQ318_spl,
inference(contradiction_clause,[status(thm)],[f3210]) ).
fof(f3212,plain,
( sQ315_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f387,f3191]) ).
fof(f3213,plain,
( sQ315_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3212,f173]) ).
fof(f3214,plain,
sQ315_spl,
inference(contradiction_clause,[status(thm)],[f3213]) ).
fof(f3231,definition,
( sQ323_spl
<=> aElementOf0(xK,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f3233,plain,
( sQ323_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(component_clause,[status(thm)],[f3231]) ).
fof(f3250,plain,
( sQ323_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3233,f354]) ).
fof(f3251,plain,
sQ323_spl,
inference(contradiction_clause,[status(thm)],[f3250]) ).
fof(f3316,definition,
( sQ338_spl
<=> iLess0(xk,xK) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f3318,plain,
( sQ338_spl
| ~ iLess0(xk,xK) ),
inference(component_clause,[status(thm)],[f3316]) ).
fof(f3320,plain,
( sQ338_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3318,f395]) ).
fof(f3321,plain,
sQ338_spl,
inference(contradiction_clause,[status(thm)],[f3320]) ).
fof(f3354,definition,
( sQ344_spl
<=> aFunction0(xc) ),
introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition]) ).
fof(f3356,plain,
( sQ344_spl
| ~ aFunction0(xc) ),
inference(component_clause,[status(thm)],[f3354]) ).
fof(f3374,plain,
( sQ344_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3356,f357]) ).
fof(f3375,plain,
sQ344_spl,
inference(contradiction_clause,[status(thm)],[f3374]) ).
fof(f3562,plain,
! [X0] :
( aSet0(sK21_skl(X0,xu))
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY) ),
inference(backward_demodulation,[status(thm)],[f397,f1250]) ).
fof(f3567,definition,
( sQ376_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition]) ).
fof(f3569,plain,
( sQ376_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f3567]) ).
fof(f3589,plain,
( sQ376_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3569,f396]) ).
fof(f3590,plain,
sQ376_spl,
inference(contradiction_clause,[status(thm)],[f3589]) ).
fof(f3593,plain,
( aSet0(sK21_skl(xX,xu))
| ~ isCountable0(xX) ),
inference(resolution,[status(thm)],[f3562,f406]) ).
fof(f3598,definition,
( sQ383_spl
<=> aSet0(sK21_skl(xX,xu)) ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f3601,plain,
( sQ383_spl
| ~ sQ117_spl ),
inference(split_clause,[status(thm)],[f3593,f1369,f3598]) ).
fof(f3602,plain,
! [X0,X1] :
( aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xk))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xY)
| ~ aElementOf0(X0,xT) ),
inference(forward_demodulation,[status(thm)],[f397,f412]) ).
fof(f3603,plain,
! [X0] :
( aElementOf0(sK21_skl(X0,xu),slbdtsldtrb0(X0,xk))
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY) ),
inference(resolution,[status(thm)],[f3602,f405]) ).
fof(f3666,definition,
( sQ393_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ393_spl])],[split_symbol_definition]) ).
fof(f3668,plain,
( sQ393_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f3666]) ).
fof(f3697,plain,
( sQ393_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3668,f401]) ).
fof(f3698,plain,
sQ393_spl,
inference(contradiction_clause,[status(thm)],[f3697]) ).
fof(f3727,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(X0,xu)) != xu
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY) ),
inference(forward_demodulation,[status(thm)],[f397,f1248]) ).
fof(f3728,plain,
! [X0] :
( sdtlpdtrp0(xd,sK21_skl(X0,xu)) != xu
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY) ),
inference(forward_demodulation,[status(thm)],[f398,f3727]) ).
fof(f3730,plain,
( sdtlpdtrp0(xd,sK21_skl(xX,xu)) != xu
| ~ isCountable0(xX) ),
inference(resolution,[status(thm)],[f3728,f406]) ).
fof(f3735,definition,
( sQ406_spl
<=> sdtlpdtrp0(xd,sK21_skl(xX,xu)) = xu ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f3738,plain,
( ~ sQ406_spl
| ~ sQ117_spl ),
inference(split_clause,[status(thm)],[f3730,f1369,f3735]) ).
fof(f3757,definition,
( sQ410_spl
<=> szmzizndt0(sdtlpdtrp0(xN,xK)) = szmzizndt0(sdtlpdtrp0(xN,xK)) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f3759,plain,
( sQ410_spl
| szmzizndt0(sdtlpdtrp0(xN,xK)) != szmzizndt0(sdtlpdtrp0(xN,xK)) ),
inference(component_clause,[status(thm)],[f3757]) ).
fof(f3762,plain,
( sQ410_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3759]) ).
fof(f3763,plain,
sQ410_spl,
inference(contradiction_clause,[status(thm)],[f3762]) ).
fof(f3986,plain,
( aElementOf0(sK21_skl(xX,xu),slbdtsldtrb0(xX,xk))
| ~ isCountable0(xX) ),
inference(resolution,[status(thm)],[f3603,f406]) ).
fof(f3991,definition,
( sQ436_spl
<=> aElementOf0(sK21_skl(xX,xu),slbdtsldtrb0(xX,xk)) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f3992,plain,
( ~ sQ436_spl
| aElementOf0(sK21_skl(xX,xu),slbdtsldtrb0(xX,xk)) ),
inference(component_clause,[status(thm)],[f3991]) ).
fof(f3994,plain,
( sQ436_spl
| ~ sQ117_spl ),
inference(split_clause,[status(thm)],[f3986,f1369,f3991]) ).
fof(f4163,plain,
( sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2149,f2912]) ).
fof(f4164,plain,
sQ280_spl,
inference(contradiction_clause,[status(thm)],[f4163]) ).
fof(f4484,plain,
( ~ sQ436_spl
| sdtlpdtrp0(xd,sK21_skl(xX,xu)) = xu
| ~ aSet0(sK21_skl(xX,xu)) ),
inference(resolution,[status(thm)],[f3992,f408]) ).
fof(f4494,plain,
( ~ sQ436_spl
| sQ406_spl
| ~ sQ383_spl ),
inference(split_clause,[status(thm)],[f4484,f3598,f3735,f3991]) ).
fof(f4549,plain,
$false,
inference(sat_refutation,[status(thm)],[f2500,f2502,f2603,f2605,f2894,f3211,f3214,f3251,f3321,f3375,f3590,f3601,f3698,f3738,f3763,f3994,f4164,f4494]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM592+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:42:55 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 1.17/0.58 % Refutation found
% 1.17/0.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.17/0.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.17/0.60 % Elapsed time: 0.228727 seconds
% 1.17/0.60 % CPU time: 1.488949 seconds
% 1.17/0.60 % Total memory used: 134.825 MB
% 1.17/0.60 % Net memory used: 132.838 MB
%------------------------------------------------------------------------------