%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM600+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 : n016.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:08 PM UTC 2026
% Result : Theorem 4.13s 1.05s
% Output : CNFRefutation 4.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 22
% Syntax : Number of formulae : 97 ( 15 unt; 13 def)
% Number of atoms : 340 ( 43 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 405 ( 162 ~; 161 |; 53 &)
% ( 17 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 12 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-4 aty)
% Number of variables : 111 ( 98 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aFunction0(W0) )
=> aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,definition,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aSubsetOf0(W1,szDzozmdt0(W0))
=> ! [W2] :
( W2 = sdtlcdtrc0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) ) )
& aSet0(W2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
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(f95,hypothesis,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,conjecture,
! [W0] :
( aElementOf0(W0,xO)
=> ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(W1,szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,negated_conjecture,
~ ! [W0] :
( aElementOf0(W0,xO)
=> ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(W1,szNzAzT0) ) ),
inference(negated_conjecture,[status(cth)],[f97]) ).
fof(f105,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f106,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f123,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f124,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f126,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f125]) ).
fof(f128,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f175,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f322,plain,
! [W0,W1] :
( aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0))
| ~ aElement0(W1)
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f323,plain,
! [X0,X1] :
( aSubsetOf0(sdtlbdtrb0(X0,X1),szDzozmdt0(X0))
| ~ aElement0(X1)
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f324,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( W2 = sdtlcdtrc0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) ) )
& aSet0(W2) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f325,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( ? [W3] :
( ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ( ( ! [W3] :
( ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(NNF_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( ? [W3] :
( ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ! [W3] :
( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(miniscoping,[status(thm)],[f325]) ).
fof(f327,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( ( ( ( sdtlpdtrp0(W0,sK15_skl(W2,W1,W0)) = sK14_skl(W2,W1,W0)
& aElementOf0(sK15_skl(W2,W1,W0),W1) )
| aElementOf0(sK14_skl(W2,W1,W0),W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != sK14_skl(W2,W1,W0)
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(sK14_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sdtlpdtrp0(W0,sK13_skl(W3,W2,W1,W0)) = W3
& aElementOf0(sK13_skl(W3,W2,W1,W0),W1) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W4,sK13_skl(W3,W2,W1,W0)),skolemize(W3,sK14_skl(W2,W1,W0)),skolemize(W4,sK15_skl(W2,W1,W0))],[f326]) ).
fof(f329,plain,
! [X0,X1,X2,X3] :
( aElementOf0(sK13_skl(X3,X2,X1,X0),X1)
| ~ aElementOf0(X3,X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f330,plain,
! [X0,X1,X2,X3] :
( sdtlpdtrp0(X0,sK13_skl(X3,X2,X1,X0)) = X3
| ~ aElementOf0(X3,X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f355,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f408,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(f409,plain,
aFunction0(xe),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f410,plain,
szDzozmdt0(xe) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f412,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(f413,plain,
aFunction0(xd),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f414,plain,
szDzozmdt0(xd) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f417,plain,
aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f420,plain,
xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f423,plain,
? [W0] :
( ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(W1,szNzAzT0) )
& aElementOf0(W0,xO) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f424,plain,
( ! [W1] :
( sdtlpdtrp0(xe,W1) != sK24_skl
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(W1,szNzAzT0) )
& aElementOf0(sK24_skl,xO) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f423]) ).
fof(f425,plain,
aElementOf0(sK24_skl,xO),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f426,plain,
! [X0] :
( sdtlpdtrp0(xe,X0) != sK24_skl
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f475,plain,
! [X0,X1,X2] :
( aElementOf0(sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0),X1)
| ~ aElementOf0(X2,sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f329]) ).
fof(f476,plain,
! [X0,X1,X2] :
( sdtlpdtrp0(X0,sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0)) = X2
| ~ aElementOf0(X2,sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f330]) ).
fof(f492,plain,
( aElement0(szDzizrdt0(xd))
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f106,f417]) ).
fof(f495,definition,
( sQ0_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( sQ0_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f495]) ).
fof(f498,definition,
( sQ1_spl
<=> aElement0(szDzizrdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( ~ sQ1_spl
| aElement0(szDzizrdt0(xd)) ),
inference(component_clause,[status(thm)],[f498]) ).
fof(f501,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f492,f495,f498]) ).
fof(f511,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f497,f355]) ).
fof(f512,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f511]) ).
fof(f540,definition,
( sQ8_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ8_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f568,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f175]) ).
fof(f569,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f568]) ).
fof(f571,definition,
( sQ15_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( sQ15_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f575,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f413]) ).
fof(f576,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f575]) ).
fof(f577,plain,
! [X0] :
( aSubsetOf0(sdtlbdtrb0(xd,X0),szNzAzT0)
| ~ aElement0(X0)
| ~ aFunction0(xd) ),
inference(paramodulation,[status(thm)],[f414,f323]) ).
fof(f579,definition,
! [X0] :
( sQ16_spl
<=> ( aSubsetOf0(sdtlbdtrb0(xd,X0),szNzAzT0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f580,plain,
! [X0] :
( ~ sQ16_spl
| aSubsetOf0(sdtlbdtrb0(xd,X0),szNzAzT0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f577,f571,f579]) ).
fof(f583,definition,
( sQ17_spl
<=> aFunction0(xe) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( sQ17_spl
| ~ aFunction0(xe) ),
inference(component_clause,[status(thm)],[f583]) ).
fof(f590,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f585,f409]) ).
fof(f591,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f590]) ).
fof(f1410,definition,
( sQ109_spl
<=> aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1411,plain,
( ~ sQ109_spl
| aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f1410]) ).
fof(f1412,plain,
( sQ109_spl
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f1410]) ).
fof(f1417,plain,
( sQ109_spl
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f1412]) ).
fof(f1419,plain,
! [X0] :
( ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),szNzAzT0)
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,X0))
| ~ aSubsetOf0(X0,szDzozmdt0(xe))
| ~ aFunction0(xe) ),
inference(resolution,[status(thm)],[f476,f426]) ).
fof(f1421,definition,
! [X0] :
( sQ111_spl
<=> ( ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),szNzAzT0)
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,X0))
| ~ aSubsetOf0(X0,szDzozmdt0(xe)) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
! [X0] :
( ~ sQ111_spl
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),szNzAzT0)
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,X0))
| ~ aSubsetOf0(X0,szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f1421]) ).
fof(f1424,plain,
( sQ111_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1419,f583,f1421]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ111_spl
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),szNzAzT0)
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,X0))
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f1422]) ).
fof(f1447,definition,
( sQ116_spl
<=> aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1449,plain,
( sQ116_spl
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
inference(component_clause,[status(thm)],[f1447]) ).
fof(f1450,definition,
( sQ117_spl
<=> aElementOf0(sK24_skl,sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1452,plain,
( sQ117_spl
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))) ),
inference(component_clause,[status(thm)],[f1450]) ).
fof(f1462,plain,
( sQ117_spl
| ~ aElementOf0(sK24_skl,xO) ),
inference(forward_demodulation,[status(thm)],[f420,f1452]) ).
fof(f1463,plain,
( sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1462,f425]) ).
fof(f1464,plain,
sQ117_spl,
inference(contradiction_clause,[status(thm)],[f1463]) ).
fof(f1466,plain,
( ~ sQ16_spl
| sQ109_spl
| ~ aElement0(szDzizrdt0(xd)) ),
inference(resolution,[status(thm)],[f1417,f580]) ).
fof(f1467,plain,
( ~ sQ16_spl
| sQ109_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1466,f499]) ).
fof(f1468,plain,
( ~ sQ16_spl
| sQ109_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1467]) ).
fof(f1469,plain,
( ~ sQ109_spl
| aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f1411]) ).
fof(f1470,plain,
( ~ sQ109_spl
| sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1469,f1449]) ).
fof(f1471,plain,
( ~ sQ109_spl
| sQ116_spl ),
inference(contradiction_clause,[status(thm)],[f1470]) ).
fof(f1500,plain,
! [X0] :
( ~ sQ109_spl
| aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f128,f1469]) ).
fof(f1511,definition,
! [X0] :
( sQ121_spl
<=> ( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
! [X0] :
( ~ sQ121_spl
| aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(component_clause,[status(thm)],[f1511]) ).
fof(f1514,plain,
( ~ sQ109_spl
| sQ121_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1500,f540,f1511,f1410]) ).
fof(f1517,plain,
! [X0] :
( ~ sQ111_spl
| ~ sQ121_spl
| ~ aElementOf0(sK13_skl(sK24_skl,sdtlcdtrc0(xe,X0),X0,xe),sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,X0))
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1429,f1512]) ).
fof(f1573,plain,
( ~ sQ111_spl
| ~ sQ121_spl
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))))
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe))
| ~ aFunction0(xe)
| ~ aElementOf0(sK24_skl,sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))))
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
inference(resolution,[status(thm)],[f1517,f475]) ).
fof(f1575,plain,
( ~ sQ111_spl
| ~ sQ121_spl
| ~ sQ109_spl
| ~ sQ17_spl
| ~ sQ117_spl
| ~ sQ116_spl ),
inference(split_clause,[status(thm)],[f1573,f1447,f1450,f583,f1410,f1511,f1421]) ).
fof(f1577,plain,
$false,
inference(sat_refutation,[status(thm)],[f501,f512,f569,f576,f582,f591,f1424,f1464,f1468,f1471,f1514,f1575]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM600+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n016.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 02:48:07 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 4.13/1.05 % Refutation found
% 4.13/1.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.13/1.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.13/1.07 % Elapsed time: 0.632971 seconds
% 4.13/1.07 % CPU time: 4.479859 seconds
% 4.13/1.07 % Total memory used: 155.053 MB
% 4.13/1.07 % Net memory used: 151.695 MB
%------------------------------------------------------------------------------