%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM543+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:40:56 PM UTC 2026
% Result : Theorem 35.07s 5.07s
% Output : CNFRefutation 35.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 8
% Syntax : Number of formulae : 69 ( 13 unt; 3 def)
% Number of atoms : 329 ( 49 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 416 ( 156 ~; 155 |; 82 &)
% ( 13 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 119 ( 107 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W0,W1)
<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,definition,
! [W0] :
( ( W0 != slcrc0
& isFinite0(W0)
& aSubsetOf0(W0,szNzAzT0) )
=> ! [W1] :
( W1 = szmzazxdt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W2,W1) )
& aElementOf0(W1,W0) ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
( isFinite0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
? [W0] :
( ( ( ! [W1] :
( aElementOf0(W1,slbdtrb0(W0))
<=> ( sdtlseqdt0(szszuzczcdt0(W1),W0)
& aElementOf0(W1,szNzAzT0) ) )
& aSet0(slbdtrb0(W0)) )
=> ( aSubsetOf0(xS,slbdtrb0(W0))
| ! [W1] :
( aElementOf0(W1,xS)
=> aElementOf0(W1,slbdtrb0(W0)) ) ) )
& aElementOf0(W0,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ ? [W0] :
( ( ( ! [W1] :
( aElementOf0(W1,slbdtrb0(W0))
<=> ( sdtlseqdt0(szszuzczcdt0(W1),W0)
& aElementOf0(W1,szNzAzT0) ) )
& aSet0(slbdtrb0(W0)) )
=> ( aSubsetOf0(xS,slbdtrb0(W0))
| ! [W1] :
( aElementOf0(W1,xS)
=> aElementOf0(W1,slbdtrb0(W0)) ) ) )
& aElementOf0(W0,szNzAzT0) ),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f68,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f69,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f71,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))],[f70]) ).
fof(f73,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f136,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f137,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f138,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f154,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f155,plain,
! [W0,W1] :
( ( ( ~ sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))
| sdtlseqdt0(W0,W1) )
& ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f200,plain,
! [W0] :
( ! [W1] :
( W1 = szmzazxdt0(W0)
<=> ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f201,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ sdtlseqdt0(W2,W1)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzazxdt0(W0) )
& ( ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzazxdt0(W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ sdtlseqdt0(W2,W1)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzazxdt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzazxdt0(W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f201]) ).
fof(f203,plain,
! [W0] :
( ( ! [W1] :
( ( ~ sdtlseqdt0(sK7_skl(W1,W0),W1)
& aElementOf0(sK7_skl(W1,W0),W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzazxdt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W2,W1)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzazxdt0(W0) ) )
| W0 = slcrc0
| ~ isFinite0(W0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(W2,sK7_skl(W1,W0))],[f202]) ).
fof(f204,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| X1 != szmzazxdt0(X0)
| X0 = slcrc0
| ~ isFinite0(X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f205,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X2,X1)
| ~ aElementOf0(X2,X0)
| X1 != szmzazxdt0(X0)
| X0 = slcrc0
| ~ isFinite0(X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f210,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(f211,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)],[f210]) ).
fof(f212,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)],[f211]) ).
fof(f213,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))],[f212]) ).
fof(f217,plain,
! [X0,X1,X2] :
( ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0)
| aElementOf0(X2,X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f233,plain,
( isFinite0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f235,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f236,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f237,plain,
isFinite0(xS),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f238,plain,
! [W0] :
( ( ~ aSubsetOf0(xS,slbdtrb0(W0))
& ? [W1] :
( ~ aElementOf0(W1,slbdtrb0(W0))
& aElementOf0(W1,xS) )
& ! [W1] :
( aElementOf0(W1,slbdtrb0(W0))
<=> ( sdtlseqdt0(szszuzczcdt0(W1),W0)
& aElementOf0(W1,szNzAzT0) ) )
& aSet0(slbdtrb0(W0)) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f239,plain,
! [W0] :
( ( ~ aSubsetOf0(xS,slbdtrb0(W0))
& ? [W1] :
( ~ aElementOf0(W1,slbdtrb0(W0))
& aElementOf0(W1,xS) )
& ! [W1] :
( ( ~ sdtlseqdt0(szszuzczcdt0(W1),W0)
| ~ aElementOf0(W1,szNzAzT0)
| aElementOf0(W1,slbdtrb0(W0)) )
& ( ( sdtlseqdt0(szszuzczcdt0(W1),W0)
& aElementOf0(W1,szNzAzT0) )
| ~ aElementOf0(W1,slbdtrb0(W0)) ) )
& aSet0(slbdtrb0(W0)) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f238]) ).
fof(f240,plain,
! [W0] :
( ( ~ aSubsetOf0(xS,slbdtrb0(W0))
& ? [W1] :
( ~ aElementOf0(W1,slbdtrb0(W0))
& aElementOf0(W1,xS) )
& ! [W1] :
( ~ sdtlseqdt0(szszuzczcdt0(W1),W0)
| ~ aElementOf0(W1,szNzAzT0)
| aElementOf0(W1,slbdtrb0(W0)) )
& ! [W1] :
( ( sdtlseqdt0(szszuzczcdt0(W1),W0)
& aElementOf0(W1,szNzAzT0) )
| ~ aElementOf0(W1,slbdtrb0(W0)) )
& aSet0(slbdtrb0(W0)) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f239]) ).
fof(f241,plain,
! [W0] :
( ( ~ aSubsetOf0(xS,slbdtrb0(W0))
& ~ aElementOf0(sK9_skl(W0),slbdtrb0(W0))
& aElementOf0(sK9_skl(W0),xS)
& ! [W1] :
( ~ sdtlseqdt0(szszuzczcdt0(W1),W0)
| ~ aElementOf0(W1,szNzAzT0)
| aElementOf0(W1,slbdtrb0(W0)) )
& ! [W1] :
( ( sdtlseqdt0(szszuzczcdt0(W1),W0)
& aElementOf0(W1,szNzAzT0) )
| ~ aElementOf0(W1,slbdtrb0(W0)) )
& aSet0(slbdtrb0(W0)) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W1,sK9_skl(W0))],[f240]) ).
fof(f246,plain,
! [X0] :
( aElementOf0(sK9_skl(X0),xS)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f247,plain,
! [X0] :
( ~ aElementOf0(sK9_skl(X0),slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f256,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f73]) ).
fof(f278,plain,
! [X0] :
( aElementOf0(szmzazxdt0(X0),X0)
| X0 = slcrc0
| ~ isFinite0(X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f204]) ).
fof(f279,plain,
! [X0,X1] :
( sdtlseqdt0(X1,szmzazxdt0(X0))
| ~ aElementOf0(X1,X0)
| X0 = slcrc0
| ~ isFinite0(X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f205]) ).
fof(f283,plain,
! [X0,X1] :
( ~ sdtlseqdt0(szszuzczcdt0(X1),X0)
| ~ aElementOf0(X1,szNzAzT0)
| aElementOf0(X1,slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f217]) ).
fof(f290,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(sK9_skl(X0),szNzAzT0) ),
inference(resolution,[status(thm)],[f235,f246]) ).
fof(f300,plain,
aElementOf0(szszuzczcdt0(sz00),szNzAzT0),
inference(resolution,[status(thm)],[f136,f138]) ).
fof(f314,plain,
aElementOf0(szszuzczcdt0(szszuzczcdt0(sz00)),szNzAzT0),
inference(resolution,[status(thm)],[f300,f138]) ).
fof(f363,plain,
aElementOf0(szszuzczcdt0(szszuzczcdt0(szszuzczcdt0(sz00))),szNzAzT0),
inference(resolution,[status(thm)],[f314,f138]) ).
fof(f459,plain,
aElementOf0(szszuzczcdt0(szszuzczcdt0(szszuzczcdt0(szszuzczcdt0(sz00)))),szNzAzT0),
inference(resolution,[status(thm)],[f363,f138]) ).
fof(f878,plain,
aElementOf0(szszuzczcdt0(szszuzczcdt0(szszuzczcdt0(szszuzczcdt0(szszuzczcdt0(sz00))))),szNzAzT0),
inference(resolution,[status(thm)],[f459,f138]) ).
fof(f918,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| aElementOf0(X1,slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(szszuzczcdt0(X0),szNzAzT0) ),
inference(resolution,[status(thm)],[f283,f156]) ).
fof(f923,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| aElementOf0(X1,slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(szszuzczcdt0(X0),szNzAzT0) ),
inference(duplicate_literals_removal,[status(thm)],[f918]) ).
fof(f924,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f138]) ).
fof(f2392,plain,
( aElementOf0(szmzazxdt0(xS),xS)
| xS = slcrc0
| ~ isFinite0(xS) ),
inference(resolution,[status(thm)],[f278,f236]) ).
fof(f2394,plain,
( aElementOf0(szmzazxdt0(xS),xS)
| xS = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2392,f237]) ).
fof(f2547,plain,
( aElementOf0(szmzazxdt0(xS),szNzAzT0)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f2394,f235]) ).
fof(f2831,plain,
! [X0] :
( sdtlseqdt0(X0,szmzazxdt0(xS))
| ~ aElementOf0(X0,xS)
| xS = slcrc0
| ~ isFinite0(xS) ),
inference(resolution,[status(thm)],[f279,f236]) ).
fof(f2833,plain,
! [X0] :
( sdtlseqdt0(X0,szmzazxdt0(xS))
| ~ aElementOf0(X0,xS)
| xS = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2831,f237]) ).
fof(f3994,plain,
! [X0] :
( ~ aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ sdtlseqdt0(sK9_skl(szszuzczcdt0(X0)),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK9_skl(szszuzczcdt0(X0)),szNzAzT0) ),
inference(resolution,[status(thm)],[f924,f247]) ).
fof(f4005,plain,
! [X0] :
( ~ aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ sdtlseqdt0(sK9_skl(szszuzczcdt0(X0)),X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3994,f290]) ).
fof(f4240,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(sK9_skl(X0),szmzazxdt0(xS))
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f2833,f246]) ).
fof(f4706,plain,
( ~ aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)
| ~ aElementOf0(szmzazxdt0(xS),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f4240,f4005]) ).
fof(f4711,plain,
( ~ aElementOf0(szmzazxdt0(xS),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)
| xS = slcrc0 ),
inference(duplicate_literals_removal,[status(thm)],[f4706]) ).
fof(f4712,plain,
xS = slcrc0,
inference(backward_subsumption_resolution,[status(thm)],[f2547,f4713]) ).
fof(f4713,plain,
( ~ aElementOf0(szmzazxdt0(xS),szNzAzT0)
| xS = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f4711,f138]) ).
fof(f4947,plain,
! [X0] :
( aElementOf0(sK9_skl(X0),slcrc0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(backward_demodulation,[status(thm)],[f4712,f246]) ).
fof(f5745,plain,
! [X0] : ~ aElementOf0(X0,szNzAzT0),
inference(forward_subsumption_resolution,[status(thm)],[f4947,f256]) ).
fof(f5746,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f878,f5745]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM543+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n001.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 02:44:29 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 35.07/5.07 % Refutation found
% 35.07/5.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 35.07/5.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.92/5.13 % Elapsed time: 4.656445 seconds
% 5.92/5.13 % CPU time: 36.290806 seconds
% 5.92/5.13 % Total memory used: 264.542 MB
% 5.92/5.13 % Net memory used: 246.273 MB
%------------------------------------------------------------------------------