%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM578+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 : n018.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 0.21s 5.57s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 27
% Syntax : Number of formulae : 110 ( 24 unt; 15 def)
% Number of atoms : 537 ( 70 equ)
% Maximal formula atoms : 33 ( 4 avg)
% Number of connectives : 613 ( 186 ~; 169 |; 202 &)
% ( 22 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 14 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 11 con; 0-2 aty)
% Number of variables : 142 ( 127 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
slbdtrb0(sz00) = slcrc0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(W0,xT) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
=> aElementOf0(W0,szDzozmdt0(xc)) )
& ( aElementOf0(W0,szDzozmdt0(xc))
=> ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
& aFunction0(xc) ),
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(f84,hypothesis,
( aElementOf0(xj,szNzAzT0)
& aElementOf0(xi,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
( xi != xj
=> ( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,conjecture,
( ! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W0),W1)
=> ( ~ ( ( ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W1)) )
=> ( szmzizndt0(sdtlpdtrp0(xN,W1)) = szmzizndt0(sdtlpdtrp0(xN,W0))
| ( ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W0)) ) ) )
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ) )
=> ( xi != xj
=> ~ ( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xj))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [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,negated_conjecture,
~ ( ! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W0),W1)
=> ( ~ ( ( ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W1)) )
=> ( szmzizndt0(sdtlpdtrp0(xN,W1)) = szmzizndt0(sdtlpdtrp0(xN,W0))
| ( ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W0)) ) ) )
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ) )
=> ( xi != xj
=> ~ ( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xj))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ) ) ),
inference(negated_conjecture,[status(cth)],[f86]) ).
fof(f98,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f99,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f101,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))],[f100]) ).
fof(f102,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f112,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(f113,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)],[f112]) ).
fof(f114,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)],[f113]) ).
fof(f115,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))],[f114]) ).
fof(f117,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f122,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f123,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f164,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f166,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f253,plain,
slbdtrb0(sz00) = slcrc0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f296,plain,
! [W0] :
( aSet0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f297,plain,
! [X0] :
( aSet0(szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f344,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f352,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) ) )
& aFunction0(xc) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f353,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ( ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) ) )
& aFunction0(xc) ),
inference(NNF_transformation,[status(thm)],[f352]) ).
fof(f354,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ! [W0] :
( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) )
& aFunction0(xc) ),
inference(miniscoping,[status(thm)],[f353]) ).
fof(f355,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( sdtlpdtrp0(xc,sK20_skl(W0)) = W0
& aElementOf0(sK20_skl(W0),szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ( ~ aElementOf0(sK19_skl(W0),xS)
& aElementOf0(sK19_skl(W0),W0) )
| ~ aSet0(W0) ) ) )
& ! [W0] :
( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) )
& aFunction0(xc) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0))],[f354]) ).
fof(f356,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f382,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f403,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(f404,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f407,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f411,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f412,plain,
aElementOf0(xj,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f413,plain,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi)
| xi = xj ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f414,plain,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi)
| xi = xj ),
inference(cnf_transformation,[status(thm)],[f413]) ).
fof(f415,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xj)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& xi != xj
& ! [W0,W1] :
( ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& ( ? [W2] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
& aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W0)) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W1))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sdtlseqdt0(szszuzczcdt0(W0),W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f416,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xj)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& xi != xj
& ! [W0,W1] :
( ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& ( ? [W2] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
& aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W0)) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W1))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& ! [W2] :
( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0))
| ~ aElement0(W2)
| aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) )
| ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sdtlseqdt0(szszuzczcdt0(W0),W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ) ),
inference(NNF_transformation,[status(thm)],[f415]) ).
fof(f417,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xj)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& xi != xj
& ! [W0,W1] :
( ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& ( ? [W2] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
& aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W0)) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W1))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& ! [W2] :
( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0))
| ~ aElement0(W2)
| aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) )
| ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sdtlseqdt0(szszuzczcdt0(W0),W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ) ),
inference(miniscoping,[status(thm)],[f416]) ).
fof(f418,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xj)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& xi != xj
& ! [W0,W1] :
( ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& ( ( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),sK23_skl(W1,W0))
& aElementOf0(sK23_skl(W1,W0),sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W0)) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W1)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W1)),sdtlpdtrp0(xN,W1))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W1)) )
& ! [W2] :
( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0))
| ~ aElement0(W2)
| aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) )
| ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sdtlseqdt0(szszuzczcdt0(W0),W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W2,sK23_skl(W1,W0))],[f417]) ).
fof(f432,plain,
! [X0,X1] :
( szmzizndt0(sdtlpdtrp0(xN,X1)) != szmzizndt0(sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(szszuzczcdt0(X0),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f433,plain,
xi != xj,
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f438,plain,
szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f514,definition,
( sQ0_spl
<=> xi = xj ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( ~ sQ0_spl
| xi = xj ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f517,definition,
( sQ1_spl
<=> sdtlseqdt0(szszuzczcdt0(xj),xi) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f520,definition,
( sQ2_spl
<=> sdtlseqdt0(szszuzczcdt0(xi),xj) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f414,f514,f517,f520]) ).
fof(f524,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f102]) ).
fof(f580,definition,
( sQ3_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f582,plain,
( sQ3_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f580]) ).
fof(f590,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f582,f411]) ).
fof(f591,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f590]) ).
fof(f598,definition,
( sQ6_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( sQ6_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f609,definition,
( sQ9_spl
<=> aSet0(sdtlpdtrp0(xN,xj)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( sQ9_spl
| ~ aSet0(sdtlpdtrp0(xN,xj)) ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f616,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f164]) ).
fof(f617,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f693,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f433]) ).
fof(f694,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f693]) ).
fof(f709,plain,
! [X0] :
( aElementOf0(xj,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f117,f412]) ).
fof(f834,definition,
( sQ44_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f836,plain,
( sQ44_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(component_clause,[status(thm)],[f834]) ).
fof(f849,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f382]) ).
fof(f850,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f849]) ).
fof(f862,definition,
( sQ49_spl
<=> aElementOf0(sz00,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ49_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f1116,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f166]) ).
fof(f1117,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1116]) ).
fof(f1503,definition,
( sQ141_spl
<=> aSet0(szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1505,plain,
( sQ141_spl
| ~ aSet0(szDzozmdt0(xc)) ),
inference(component_clause,[status(thm)],[f1503]) ).
fof(f1668,definition,
( sQ165_spl
<=> aSet0(slbdtrb0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1670,plain,
( sQ165_spl
| ~ aSet0(slbdtrb0(sz00)) ),
inference(component_clause,[status(thm)],[f1668]) ).
fof(f1679,plain,
( sQ165_spl
| ~ aSet0(slcrc0) ),
inference(forward_demodulation,[status(thm)],[f253,f1670]) ).
fof(f1680,plain,
( sQ165_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1679,f524]) ).
fof(f1681,plain,
sQ165_spl,
inference(contradiction_clause,[status(thm)],[f1680]) ).
fof(f1709,plain,
( sQ141_spl
| ~ aFunction0(xc) ),
inference(resolution,[status(thm)],[f1505,f297]) ).
fof(f1710,plain,
( sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1709,f356]) ).
fof(f1711,plain,
sQ141_spl,
inference(contradiction_clause,[status(thm)],[f1710]) ).
fof(f1726,definition,
( sQ176_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1728,plain,
( sQ176_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f1726]) ).
fof(f1733,plain,
( sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1728,f344]) ).
fof(f1734,plain,
sQ176_spl,
inference(contradiction_clause,[status(thm)],[f1733]) ).
fof(f1806,plain,
( ~ aSet0(szNzAzT0)
| aElementOf0(xj,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f709,f123]) ).
fof(f1807,definition,
( sQ186_spl
<=> aElementOf0(xj,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1810,plain,
( sQ186_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1806,f598,f1807]) ).
fof(f2370,plain,
( sQ9_spl
| ~ aElementOf0(xj,szNzAzT0) ),
inference(resolution,[status(thm)],[f611,f404]) ).
fof(f2371,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2370,f412]) ).
fof(f2372,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f2371]) ).
fof(f2406,definition,
( sQ267_spl
<=> isCountable0(sdtlpdtrp0(xN,xj)) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f2408,plain,
( sQ267_spl
| ~ isCountable0(sdtlpdtrp0(xN,xj)) ),
inference(component_clause,[status(thm)],[f2406]) ).
fof(f2415,plain,
( sQ267_spl
| ~ aElementOf0(xj,szNzAzT0) ),
inference(resolution,[status(thm)],[f2408,f407]) ).
fof(f2417,plain,
( sQ267_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2415,f412]) ).
fof(f2418,plain,
sQ267_spl,
inference(contradiction_clause,[status(thm)],[f2417]) ).
fof(f2447,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xj),xi)
| ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(xj,szNzAzT0) ),
inference(resolution,[status(thm)],[f432,f438]) ).
fof(f2448,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xi),xj)
| ~ aElementOf0(xj,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f432,f438]) ).
fof(f2454,plain,
( ~ sQ1_spl
| ~ sQ3_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f2447,f1807,f580,f517]) ).
fof(f2455,plain,
( ~ sQ2_spl
| ~ sQ186_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2448,f580,f1807,f520]) ).
fof(f2473,plain,
$false,
inference(sat_refutation,[status(thm)],[f523,f591,f617,f694,f850,f1117,f1681,f1711,f1734,f1810,f2372,f2418,f2454,f2455]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM578+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.44 % Computer : n018.cluster.edu
% 0.16/5.44 % Model : x86_64 x86_64
% 0.16/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.44 % Memory : 8046.5625MB
% 0.16/5.44 % OS : Linux 6.8.0-71-generic
% 0.16/5.44 % CPULimit : 300
% 0.16/5.44 % WCLimit : 300
% 0.16/5.44 % DateTime : Mon Sep 21 02:43:34 UTC 2026
% 0.16/5.44 % CPUTime :
% 0.16/5.47 % Drodi V4.1.1
% 0.21/5.57 % Refutation found
% 0.21/5.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/5.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/5.63 % Elapsed time: 0.170810 seconds
% 0.21/5.63 % CPU time: 0.601992 seconds
% 0.21/5.63 % Total memory used: 119.375 MB
% 0.21/5.63 % Net memory used: 118.935 MB
%------------------------------------------------------------------------------