%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM627+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 : n015.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:15 PM UTC 2026
% Result : Theorem 10.25s 1.75s
% Output : CNFRefutation 10.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 33
% Syntax : Number of formulae : 120 ( 37 unt; 17 def)
% Number of atoms : 299 ( 31 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 281 ( 102 ~; 106 |; 45 &)
% ( 21 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 16 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 17 con; 0-2 aty)
% Number of variables : 61 ( 56 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W1),W0)
| sdtlseqdt0(W0,W1) ) ),
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(f52,axiom,
slbdtrb0(sz00) = slcrc0,
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(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(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(f101,hypothesis,
aSubsetOf0(xQ,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
( aElementOf0(xx,xO)
& aElementOf0(xx,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
( xx = sdtlpdtrp0(xe,xm)
& aElementOf0(xm,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
~ aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f132,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f134,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))],[f133]) ).
fof(f136,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f138,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f199,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f200,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f201,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f223,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f224,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f229,plain,
! [W0,W1] :
( sdtlseqdt0(szszuzczcdt0(W1),W0)
| sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f230,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f273,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(f274,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)],[f273]) ).
fof(f275,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)],[f274]) ).
fof(f276,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))],[f275]) ).
fof(f277,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f286,plain,
slbdtrb0(sz00) = slcrc0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f384,plain,
aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f393,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f404,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(f405,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f430,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(f432,plain,
szDzozmdt0(xe) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f430]) ).
fof(f454,plain,
aSubsetOf0(xQ,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f466,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f470,plain,
aElementOf0(xx,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f472,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f475,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f476,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f485,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f136]) ).
fof(f509,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f277]) ).
fof(f2053,plain,
sdtlseqdt0(sz00,sz00),
inference(resolution,[status(thm)],[f224,f199]) ).
fof(f2233,definition,
( sQ213_spl
<=> aElementOf0(xm,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2235,plain,
( sQ213_spl
| ~ aElementOf0(xm,szNzAzT0) ),
inference(component_clause,[status(thm)],[f2233]) ).
fof(f2274,plain,
( sQ213_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2235,f472]) ).
fof(f2275,plain,
sQ213_spl,
inference(contradiction_clause,[status(thm)],[f2274]) ).
fof(f2524,definition,
( sQ259_spl
<=> aSet0(slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f2526,plain,
( sQ259_spl
| ~ aSet0(slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f2524]) ).
fof(f2532,definition,
( sQ261_spl
<=> aSet0(slbdtrb0(xm)) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f2534,plain,
( sQ261_spl
| ~ aSet0(slbdtrb0(xm)) ),
inference(component_clause,[status(thm)],[f2532]) ).
fof(f2540,definition,
( sQ263_spl
<=> aSet0(slbdtrb0(xx)) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f2542,plain,
( sQ263_spl
| ~ aSet0(slbdtrb0(xx)) ),
inference(component_clause,[status(thm)],[f2540]) ).
fof(f2574,definition,
( sQ269_spl
<=> aSet0(slbdtrb0(xn)) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f2576,plain,
( sQ269_spl
| ~ aSet0(slbdtrb0(xn)) ),
inference(component_clause,[status(thm)],[f2574]) ).
fof(f2673,definition,
( sQ282_spl
<=> aSubsetOf0(xQ,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f2675,plain,
( sQ282_spl
| ~ aSubsetOf0(xQ,szNzAzT0) ),
inference(component_clause,[status(thm)],[f2673]) ).
fof(f2967,definition,
( sQ324_spl
<=> aElementOf0(xn,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f2969,plain,
( sQ324_spl
| ~ aElementOf0(xn,szNzAzT0) ),
inference(component_clause,[status(thm)],[f2967]) ).
fof(f2978,plain,
( sQ324_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2969,f466]) ).
fof(f2979,plain,
sQ324_spl,
inference(contradiction_clause,[status(thm)],[f2978]) ).
fof(f3066,plain,
( sQ282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2675,f454]) ).
fof(f3067,plain,
sQ282_spl,
inference(contradiction_clause,[status(thm)],[f3066]) ).
fof(f3731,plain,
( ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f405,f476]) ).
fof(f3732,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f405,f475]) ).
fof(f3743,definition,
( sQ405_spl
<=> sdtlseqdt0(xm,xn) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f3746,plain,
( ~ sQ405_spl
| ~ sQ213_spl
| ~ sQ324_spl ),
inference(split_clause,[status(thm)],[f3731,f2967,f2233,f3743]) ).
fof(f3747,definition,
( sQ406_spl
<=> aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f3749,plain,
( sQ406_spl
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(component_clause,[status(thm)],[f3747]) ).
fof(f3750,definition,
( sQ407_spl
<=> sdtlseqdt0(szszuzczcdt0(xn),xm) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f3752,plain,
( sQ407_spl
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm) ),
inference(component_clause,[status(thm)],[f3750]) ).
fof(f3753,plain,
( ~ sQ407_spl
| ~ sQ406_spl
| ~ sQ213_spl ),
inference(split_clause,[status(thm)],[f3732,f2233,f3747,f3750]) ).
fof(f3874,definition,
( sQ426_spl
<=> sdtlseqdt0(sz00,sz00) ),
introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition]) ).
fof(f3876,plain,
( sQ426_spl
| ~ sdtlseqdt0(sz00,sz00) ),
inference(component_clause,[status(thm)],[f3874]) ).
fof(f3882,plain,
( sQ426_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3876,f2053]) ).
fof(f3883,plain,
sQ426_spl,
inference(contradiction_clause,[status(thm)],[f3882]) ).
fof(f3917,plain,
( sQ406_spl
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f3749,f201]) ).
fof(f3918,plain,
( sQ406_spl
| ~ sQ324_spl ),
inference(split_clause,[status(thm)],[f3917,f2967,f3747]) ).
fof(f3955,definition,
( sQ437_spl
<=> aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f3957,plain,
( sQ437_spl
| ~ aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(component_clause,[status(thm)],[f3955]) ).
fof(f4198,plain,
aSet0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f509,f393]) ).
fof(f4219,plain,
aSet0(slbdtrb0(xm)),
inference(resolution,[status(thm)],[f509,f472]) ).
fof(f4224,plain,
aSet0(slbdtrb0(xx)),
inference(resolution,[status(thm)],[f509,f470]) ).
fof(f4225,plain,
aSet0(slbdtrb0(xn)),
inference(resolution,[status(thm)],[f509,f466]) ).
fof(f4226,plain,
( sQ259_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4198,f2526]) ).
fof(f4227,plain,
sQ259_spl,
inference(contradiction_clause,[status(thm)],[f4226]) ).
fof(f4254,plain,
( sQ261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4219,f2534]) ).
fof(f4255,plain,
sQ261_spl,
inference(contradiction_clause,[status(thm)],[f4254]) ).
fof(f4265,plain,
( sQ263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4224,f2542]) ).
fof(f4266,plain,
sQ263_spl,
inference(contradiction_clause,[status(thm)],[f4265]) ).
fof(f4267,plain,
( sQ269_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4225,f2576]) ).
fof(f4268,plain,
sQ269_spl,
inference(contradiction_clause,[status(thm)],[f4267]) ).
fof(f4388,definition,
( sQ486_spl
<=> aElementOf0(sz00,szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition]) ).
fof(f4390,plain,
( sQ486_spl
| ~ aElementOf0(sz00,szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f4388]) ).
fof(f4403,plain,
( sQ486_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f432,f4390]) ).
fof(f4404,plain,
( sQ486_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4403,f199]) ).
fof(f4405,plain,
sQ486_spl,
inference(contradiction_clause,[status(thm)],[f4404]) ).
fof(f4557,plain,
( sQ437_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3957,f384]) ).
fof(f4558,plain,
sQ437_spl,
inference(contradiction_clause,[status(thm)],[f4557]) ).
fof(f4956,definition,
( sQ558_spl
<=> aElementOf0(sz00,slbdtrb0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition]) ).
fof(f4957,plain,
( ~ sQ558_spl
| aElementOf0(sz00,slbdtrb0(sz00)) ),
inference(component_clause,[status(thm)],[f4956]) ).
fof(f4970,plain,
( ~ sQ558_spl
| aElementOf0(sz00,slcrc0) ),
inference(forward_demodulation,[status(thm)],[f286,f4957]) ).
fof(f4971,plain,
( ~ sQ558_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4970,f485]) ).
fof(f4972,plain,
~ sQ558_spl,
inference(contradiction_clause,[status(thm)],[f4971]) ).
fof(f5180,definition,
( sQ588_spl
<=> isFinite0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition]) ).
fof(f5182,plain,
( sQ588_spl
| ~ isFinite0(slcrc0) ),
inference(component_clause,[status(thm)],[f5180]) ).
fof(f5188,plain,
( sQ588_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5182,f138]) ).
fof(f5189,plain,
sQ588_spl,
inference(contradiction_clause,[status(thm)],[f5188]) ).
fof(f5992,plain,
( sQ407_spl
| sdtlseqdt0(xm,xn)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f230,f3752]) ).
fof(f6000,plain,
( sQ407_spl
| sQ405_spl
| ~ sQ324_spl
| ~ sQ213_spl ),
inference(split_clause,[status(thm)],[f5992,f2233,f2967,f3743,f3750]) ).
fof(f6006,plain,
$false,
inference(sat_refutation,[status(thm)],[f2275,f2979,f3067,f3746,f3753,f3883,f3918,f4227,f4255,f4266,f4268,f4405,f4558,f4972,f5189,f6000]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM627+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.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:48:50 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 10.25/1.75 % Refutation found
% 10.25/1.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.25/1.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.25/1.78 % Elapsed time: 1.403362 seconds
% 10.25/1.78 % CPU time: 10.786088 seconds
% 10.25/1.78 % Total memory used: 212.819 MB
% 10.25/1.78 % Net memory used: 204.375 MB
%------------------------------------------------------------------------------