%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM591+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 : n002.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 234.11s 30.03s
% Output : CNFRefutation 234.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 83
% Syntax : Number of formulae : 357 ( 81 unt; 58 def)
% Number of atoms : 1092 ( 129 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 1226 ( 491 ~; 491 |; 147 &)
% ( 71 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 63 ( 61 usr; 54 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 13 con; 0-4 aty)
% Number of variables : 259 ( 233 !; 26 ?)
% 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(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(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [W0,W1,W2] :
( ( aSet0(W2)
& aSet0(W1)
& aSet0(W0) )
=> ( ( aSubsetOf0(W1,W2)
& aSubsetOf0(W0,W1) )
=> aSubsetOf0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
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(f39,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> iLess0(W0,szszuzczcdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
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(f51,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> isFinite0(slbdtrb0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
slbdtrb0(sz00) = slcrc0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,definition,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aSet0(W0) )
=> ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) ) ),
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(f74,hypothesis,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,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(f77,hypothesis,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( isCountable0(W1)
& aSubsetOf0(W1,szNzAzT0) )
=> ! [W2] :
( ( aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT)
& szDzozmdt0(W2) = slbdtsldtrb0(W1,W0)
& aFunction0(W2) )
=> ( iLess0(W0,xK)
=> ? [W3] :
( ? [W4] :
( ! [W5] :
( aElementOf0(W5,slbdtsldtrb0(W4,W0))
=> sdtlpdtrp0(W2,W5) = W3 )
& isCountable0(W4)
& aSubsetOf0(W4,W1) )
& aElementOf0(W3,xT) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
xK != sz00,
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(f82,hypothesis,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) ) ),
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(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,conjecture,
? [W0,W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xk))
& aSet0(W2) )
=> sdtlpdtrp0(xd,W2) = W0 )
& isCountable0(W1)
& aSubsetOf0(W1,xY)
& aElementOf0(W0,xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
~ ? [W0,W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xk))
& aSet0(W2) )
=> sdtlpdtrp0(xd,W2) = W0 )
& isCountable0(W1)
& aSubsetOf0(W1,xY)
& aElementOf0(W0,xT) ),
inference(negated_conjecture,[status(cth)],[f93]) ).
fof(f105,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f106,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f106]) ).
fof(f108,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))],[f107]) ).
fof(f109,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f112,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f119,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(f120,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)],[f119]) ).
fof(f121,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)],[f120]) ).
fof(f122,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))],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f129,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f130,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f133,plain,
! [W0,W1,W2] :
( aSubsetOf0(W0,W2)
| ~ aSubsetOf0(W1,W2)
| ~ aSubsetOf0(W0,W1)
| ~ aSet0(W2)
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f134,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f171,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f172,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f173,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f174,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f175,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f197,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f198,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f207,plain,
! [W0] :
( iLess0(W0,szszuzczcdt0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f208,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f215,plain,
! [W0] :
( ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f216,plain,
! [W0] :
( ( ( W0 != slcrc0
| sbrdtbr0(W0) = sz00 )
& ( W0 = slcrc0
| sbrdtbr0(W0) != sz00 ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f215]) ).
fof(f218,plain,
! [X0] :
( X0 != slcrc0
| sbrdtbr0(X0) = sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f247,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(f248,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)],[f247]) ).
fof(f249,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)],[f248]) ).
fof(f250,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))],[f249]) ).
fof(f251,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f258,plain,
! [W0] :
( isFinite0(slbdtrb0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f259,plain,
! [X0] :
( isFinite0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f260,plain,
slbdtrb0(sz00) = slcrc0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f276,plain,
! [W0,W1] :
( ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f277,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ( ( ! [W3] :
( ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f276]) ).
fof(f278,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f277]) ).
fof(f279,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( ( sbrdtbr0(sK10_skl(W2,W1,W0)) = W1
& aSubsetOf0(sK10_skl(W2,W1,W0),W0) )
| aElementOf0(sK10_skl(W2,W1,W0),W2) )
& ( sbrdtbr0(sK10_skl(W2,W1,W0)) != W1
| ~ aSubsetOf0(sK10_skl(W2,W1,W0),W0)
| ~ aElementOf0(sK10_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f278]) ).
fof(f280,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != slbdtsldtrb0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f320,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(f321,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)],[f320]) ).
fof(f322,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)],[f321]) ).
fof(f323,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))],[f322]) ).
fof(f324,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f351,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f352,plain,
isFinite0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f353,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f354,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f355,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f356,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f359,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ? [W3] :
( ? [W4] :
( ! [W5] :
( sdtlpdtrp0(W2,W5) = W3
| ~ aElementOf0(W5,slbdtsldtrb0(W4,W0)) )
& isCountable0(W4)
& aSubsetOf0(W4,W1) )
& aElementOf0(W3,xT) )
| ~ iLess0(W0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT)
| szDzozmdt0(W2) != slbdtsldtrb0(W1,W0)
| ~ aFunction0(W2) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f360,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( ! [W5] :
( sdtlpdtrp0(W2,W5) = sK19_skl(W2,W1,W0)
| ~ aElementOf0(W5,slbdtsldtrb0(sK20_skl(W2,W1,W0),W0)) )
& isCountable0(sK20_skl(W2,W1,W0))
& aSubsetOf0(sK20_skl(W2,W1,W0),W1)
& aElementOf0(sK19_skl(W2,W1,W0),xT) )
| ~ iLess0(W0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT)
| szDzozmdt0(W2) != slbdtsldtrb0(W1,W0)
| ~ aFunction0(W2) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W3,sK19_skl(W2,W1,W0)),skolemize(W4,sK20_skl(W2,W1,W0))],[f359]) ).
fof(f361,plain,
! [X0,X1,X2] :
( aElementOf0(sK19_skl(X2,X1,X0),xT)
| ~ iLess0(X0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(X2,szDzozmdt0(X2)),xT)
| szDzozmdt0(X2) != slbdtsldtrb0(X1,X0)
| ~ aFunction0(X2)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f362,plain,
! [X0,X1,X2] :
( aSubsetOf0(sK20_skl(X2,X1,X0),X1)
| ~ iLess0(X0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(X2,szDzozmdt0(X2)),xT)
| szDzozmdt0(X2) != slbdtsldtrb0(X1,X0)
| ~ aFunction0(X2)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f363,plain,
! [X0,X1,X2] :
( isCountable0(sK20_skl(X2,X1,X0))
| ~ iLess0(X0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(X2,szDzozmdt0(X2)),xT)
| szDzozmdt0(X2) != slbdtsldtrb0(X1,X0)
| ~ aFunction0(X2)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f364,plain,
! [X0,X1,X2,X3] :
( sdtlpdtrp0(X2,X3) = sK19_skl(X2,X1,X0)
| ~ aElementOf0(X3,slbdtsldtrb0(sK20_skl(X2,X1,X0),X0))
| ~ iLess0(X0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(X2,szDzozmdt0(X2)),xT)
| szDzozmdt0(X2) != slbdtsldtrb0(X1,X0)
| ~ aFunction0(X2)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f365,plain,
xK != sz00,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f367,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f368,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f369,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(f370,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f371,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f372,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f375,plain,
! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f377,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f384,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(f385,plain,
aFunction0(xC),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f386,plain,
szDzozmdt0(xC) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f387,plain,
! [X0] :
( aFunction0(sdtlpdtrp0(xC,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f395,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f397,plain,
xd = sdtlpdtrp0(xC,xi),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f398,plain,
aSubsetOf0(xY,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f399,plain,
isCountable0(xY),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f401,plain,
szDzozmdt0(xd) = slbdtsldtrb0(xY,xk),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f402,plain,
aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f403,plain,
! [W0,W1] :
( ? [W2] :
( sdtlpdtrp0(xd,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xk))
& aSet0(W2) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,xY)
| ~ aElementOf0(W0,xT) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f404,plain,
! [W0,W1] :
( ( sdtlpdtrp0(xd,sK21_skl(W1,W0)) != W0
& aElementOf0(sK21_skl(W1,W0),slbdtsldtrb0(W1,xk))
& aSet0(sK21_skl(W1,W0)) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,xY)
| ~ aElementOf0(W0,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W2,sK21_skl(W1,W0))],[f403]) ).
fof(f406,plain,
! [X0,X1] :
( aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xk))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xY)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f407,plain,
! [X0,X1] :
( sdtlpdtrp0(xd,sK21_skl(X1,X0)) != X0
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xY)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f414,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f109]) ).
fof(f415,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f110]) ).
fof(f426,plain,
( sbrdtbr0(slcrc0) = sz00
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f218]) ).
fof(f431,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f251]) ).
fof(f437,plain,
! [X0,X1] :
( aSet0(slbdtsldtrb0(X0,X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f280]) ).
fof(f445,plain,
! [X0,X1] :
( aSet0(sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f324]) ).
fof(f455,plain,
( aSet0(xY)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f398,f123]) ).
fof(f456,definition,
( sQ0_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f458,plain,
( sQ0_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
( sQ1_spl
<=> aSet0(xY) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f455,f456,f459]) ).
fof(f463,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f458,f171]) ).
fof(f464,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f463]) ).
fof(f473,definition,
( sQ4_spl
<=> isCountable0(xY) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ4_spl
| ~ isCountable0(xY) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f477,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f399]) ).
fof(f478,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f477]) ).
fof(f528,definition,
( sQ14_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( sQ14_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f561,definition,
( sQ21_spl
<=> isFinite0(xT) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( sQ21_spl
| ~ isFinite0(xT) ),
inference(component_clause,[status(thm)],[f561]) ).
fof(f581,definition,
( sQ25_spl
<=> aSet0(szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f607,definition,
( sQ28_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( sQ28_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f607]) ).
fof(f617,definition,
( sQ31_spl
<=> aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f621,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f609,f351]) ).
fof(f622,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f621]) ).
fof(f631,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f134,f123]) ).
fof(f635,plain,
! [X0] :
( aSubsetOf0(xY,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f631,f398]) ).
fof(f649,definition,
! [X0] :
( sQ37_spl
<=> ( aSubsetOf0(xY,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f650,plain,
! [X0] :
( ~ sQ37_spl
| aSubsetOf0(xY,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,plain,
( sQ37_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f635,f456,f649]) ).
fof(f654,plain,
( aSet0(szDzozmdt0(xd))
| ~ aElementOf0(xk,szNzAzT0)
| ~ aSet0(xY) ),
inference(paramodulation,[status(thm)],[f401,f437]) ).
fof(f655,definition,
( sQ38_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ38_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f658,plain,
( sQ25_spl
| ~ sQ38_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f654,f459,f655,f581]) ).
fof(f659,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f367]) ).
fof(f660,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f659]) ).
fof(f662,plain,
! [X0] :
( aElementOf0(xi,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f395,f124]) ).
fof(f678,definition,
( sQ42_spl
<=> aFunction0(xC) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f680,plain,
( sQ42_spl
| ~ aFunction0(xC) ),
inference(component_clause,[status(thm)],[f678]) ).
fof(f682,definition,
( sQ43_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( sQ43_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f695,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f530,f414]) ).
fof(f696,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f695]) ).
fof(f708,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f563,f352]) ).
fof(f709,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f708]) ).
fof(f754,definition,
! [X0] :
( sQ51_spl
<=> ( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f755,plain,
! [X0] :
( ~ sQ51_spl
| ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f760,definition,
! [X0] :
( sQ52_spl
<=> ( ~ aSet0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f761,plain,
! [X0] :
( ~ sQ52_spl
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f760]) ).
fof(f809,plain,
! [X0] :
( ~ sQ51_spl
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f755]) ).
fof(f810,plain,
( ~ sQ51_spl
| ~ isFinite0(slcrc0) ),
inference(resolution,[status(thm)],[f809,f414]) ).
fof(f818,plain,
( ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f810,f112]) ).
fof(f819,plain,
~ sQ51_spl,
inference(contradiction_clause,[status(thm)],[f818]) ).
fof(f826,plain,
sdtlseqdt0(xi,xi),
inference(resolution,[status(thm)],[f198,f395]) ).
fof(f827,plain,
sdtlseqdt0(xK,xK),
inference(resolution,[status(thm)],[f198,f353]) ).
fof(f829,plain,
sdtlseqdt0(xk,xk),
inference(resolution,[status(thm)],[f198,f367]) ).
fof(f889,definition,
( sQ63_spl
<=> aSubsetOf0(szDzozmdt0(xd),szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( ~ sQ63_spl
| aSubsetOf0(szDzozmdt0(xd),szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f889]) ).
fof(f891,plain,
( sQ63_spl
| ~ aSubsetOf0(szDzozmdt0(xd),szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f889]) ).
fof(f977,plain,
sbrdtbr0(slcrc0) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f426,f414]) ).
fof(f985,plain,
aSet0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f431,f367]) ).
fof(f999,definition,
( sQ77_spl
<=> isFinite0(slbdtrb0(xi)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1001,plain,
( sQ77_spl
| ~ isFinite0(slbdtrb0(xi)) ),
inference(component_clause,[status(thm)],[f999]) ).
fof(f1015,definition,
( sQ81_spl
<=> isFinite0(slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1017,plain,
( sQ81_spl
| ~ isFinite0(slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f1015]) ).
fof(f1042,plain,
! [X0] :
( ~ sQ52_spl
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f761]) ).
fof(f1048,plain,
( ~ sQ52_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f985,f1042]) ).
fof(f1060,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f1048]) ).
fof(f1117,plain,
isFinite0(slbdtrb0(xi)),
inference(resolution,[status(thm)],[f259,f395]) ).
fof(f1201,plain,
( ~ sQ37_spl
| ~ aSet0(szNzAzT0)
| aSubsetOf0(xY,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f650,f130]) ).
fof(f1202,definition,
( sQ95_spl
<=> aSubsetOf0(xY,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1205,plain,
( ~ sQ37_spl
| sQ95_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1201,f456,f1202,f649]) ).
fof(f1206,plain,
( ~ aSet0(szNzAzT0)
| aElementOf0(xi,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f662,f130]) ).
fof(f1207,definition,
( sQ96_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1210,plain,
( sQ96_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1206,f456,f1207]) ).
fof(f1268,plain,
! [X0,X1,X2] :
( aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f631,f123]) ).
fof(f1271,plain,
! [X0] :
( aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f1268,f402]) ).
fof(f1281,definition,
! [X0] :
( sQ103_spl
<=> ( aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1282,plain,
! [X0] :
( ~ sQ103_spl
| aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
inference(component_clause,[status(thm)],[f1281]) ).
fof(f1284,plain,
( sQ103_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f1271,f607,f1281]) ).
fof(f1329,plain,
( iLess0(xk,xK)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f368,f208]) ).
fof(f1330,definition,
( sQ111_spl
<=> iLess0(xk,xK) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1333,plain,
( sQ111_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1329,f655,f1330]) ).
fof(f1343,definition,
( sQ113_spl
<=> aSet0(slbdtrb0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1345,plain,
( sQ113_spl
| ~ aSet0(slbdtrb0(sz00)) ),
inference(component_clause,[status(thm)],[f1343]) ).
fof(f1354,plain,
( sQ113_spl
| ~ aSet0(slcrc0) ),
inference(forward_demodulation,[status(thm)],[f260,f1345]) ).
fof(f1355,plain,
( sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1354,f414]) ).
fof(f1356,plain,
sQ113_spl,
inference(contradiction_clause,[status(thm)],[f1355]) ).
fof(f1568,plain,
( aFunction0(xd)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f397,f387]) ).
fof(f1569,definition,
( sQ143_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1572,plain,
( sQ143_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f1568,f1207,f1569]) ).
fof(f1713,definition,
( sQ153_spl
<=> aFunction0(xc) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1715,plain,
( sQ153_spl
| ~ aFunction0(xc) ),
inference(component_clause,[status(thm)],[f1713]) ).
fof(f2043,plain,
( sQ63_spl
| ~ aSet0(szDzozmdt0(xd)) ),
inference(resolution,[status(thm)],[f891,f130]) ).
fof(f2044,plain,
( sQ63_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2043,f581,f889]) ).
fof(f2278,definition,
( sQ209_spl
<=> sdtlseqdt0(xK,xK) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f2280,plain,
( sQ209_spl
| ~ sdtlseqdt0(xK,xK) ),
inference(component_clause,[status(thm)],[f2278]) ).
fof(f2285,definition,
( sQ211_spl
<=> sdtlseqdt0(xk,xk) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2287,plain,
( sQ211_spl
| ~ sdtlseqdt0(xk,xk) ),
inference(component_clause,[status(thm)],[f2285]) ).
fof(f2292,definition,
( sQ213_spl
<=> sdtlseqdt0(xi,xi) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2294,plain,
( sQ213_spl
| ~ sdtlseqdt0(xi,xi) ),
inference(component_clause,[status(thm)],[f2292]) ).
fof(f2940,definition,
( sQ284_spl
<=> isCountable0(szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f2942,plain,
( sQ284_spl
| ~ isCountable0(szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f2940]) ).
fof(f2944,definition,
( sQ285_spl
<=> isCountable0(szDzozmdt0(xC)) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f2946,plain,
( sQ285_spl
| ~ isCountable0(szDzozmdt0(xC)) ),
inference(component_clause,[status(thm)],[f2944]) ).
fof(f2948,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1715,f356]) ).
fof(f2949,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f2948]) ).
fof(f2950,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f680,f385]) ).
fof(f2951,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f2950]) ).
fof(f2952,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f684,f370]) ).
fof(f2953,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f2952]) ).
fof(f2954,plain,
( sQ285_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f386,f2946]) ).
fof(f2955,plain,
( sQ285_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2954,f172]) ).
fof(f2956,plain,
sQ285_spl,
inference(contradiction_clause,[status(thm)],[f2955]) ).
fof(f2957,plain,
( sQ284_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f371,f2942]) ).
fof(f2958,plain,
( sQ284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2957,f172]) ).
fof(f2959,plain,
sQ284_spl,
inference(contradiction_clause,[status(thm)],[f2958]) ).
fof(f4316,definition,
( sQ451_spl
<=> aSet0(slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition]) ).
fof(f4318,plain,
( sQ451_spl
| ~ aSet0(slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f4316]) ).
fof(f4660,plain,
( sQ213_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2294,f826]) ).
fof(f4661,plain,
sQ213_spl,
inference(contradiction_clause,[status(thm)],[f4660]) ).
fof(f4662,plain,
( sQ211_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2287,f829]) ).
fof(f4663,plain,
sQ211_spl,
inference(contradiction_clause,[status(thm)],[f4662]) ).
fof(f4664,plain,
( sQ209_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2280,f827]) ).
fof(f4665,plain,
sQ209_spl,
inference(contradiction_clause,[status(thm)],[f4664]) ).
fof(f4675,plain,
( sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1001,f1117]) ).
fof(f4676,plain,
sQ77_spl,
inference(contradiction_clause,[status(thm)],[f4675]) ).
fof(f4890,definition,
( sQ475_spl
<=> aElementOf0(sbrdtbr0(slcrc0),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition]) ).
fof(f4892,plain,
( sQ475_spl
| ~ aElementOf0(sbrdtbr0(slcrc0),szNzAzT0) ),
inference(component_clause,[status(thm)],[f4890]) ).
fof(f5476,plain,
isFinite0(slbdtrb0(sz00)),
inference(resolution,[status(thm)],[f173,f259]) ).
fof(f5493,definition,
( sQ517_spl
<=> aElementOf0(xi,szDzozmdt0(xC)) ),
introduced(definition,[new_symbols(definition,[sQ517_spl])],[split_symbol_definition]) ).
fof(f5495,plain,
( sQ517_spl
| ~ aElementOf0(xi,szDzozmdt0(xC)) ),
inference(component_clause,[status(thm)],[f5493]) ).
fof(f5497,plain,
( sQ517_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f386,f5495]) ).
fof(f5498,plain,
( sQ517_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5497,f395]) ).
fof(f5499,plain,
sQ517_spl,
inference(contradiction_clause,[status(thm)],[f5498]) ).
fof(f5657,plain,
( sQ475_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(backward_demodulation,[status(thm)],[f977,f4892]) ).
fof(f5663,plain,
( sQ475_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5657,f173]) ).
fof(f5664,plain,
sQ475_spl,
inference(contradiction_clause,[status(thm)],[f5663]) ).
fof(f5724,plain,
( ~ sQ63_spl
| aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ~ aFunction0(xd) ),
inference(resolution,[status(thm)],[f445,f890]) ).
fof(f5731,plain,
( ~ sQ63_spl
| sQ31_spl
| ~ sQ143_spl ),
inference(split_clause,[status(thm)],[f5724,f1569,f617,f889]) ).
fof(f5771,plain,
( ~ sQ103_spl
| ~ aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd)))
| aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT) ),
inference(resolution,[status(thm)],[f1282,f130]) ).
fof(f5780,definition,
( sQ553_spl
<=> aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT) ),
introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition]) ).
fof(f5783,plain,
( ~ sQ103_spl
| ~ sQ31_spl
| sQ553_spl ),
inference(split_clause,[status(thm)],[f5771,f5780,f617,f1281]) ).
fof(f5819,definition,
! [X0] :
( sQ558_spl
<=> ~ aElementOf0(X0,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition]) ).
fof(f5820,plain,
! [X0] :
( ~ sQ558_spl
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f5819]) ).
fof(f5845,plain,
( ~ sQ558_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f395,f5820]) ).
fof(f5850,plain,
~ sQ558_spl,
inference(contradiction_clause,[status(thm)],[f5845]) ).
fof(f5888,definition,
( sQ566_spl
<=> aElementOf0(xi,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition]) ).
fof(f5890,plain,
( sQ566_spl
| ~ aElementOf0(xi,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f5888]) ).
fof(f5892,plain,
( sQ566_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f371,f5890]) ).
fof(f5893,plain,
( sQ566_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5892,f395]) ).
fof(f5894,plain,
sQ566_spl,
inference(contradiction_clause,[status(thm)],[f5893]) ).
fof(f6670,plain,
aSet0(slbdtrb0(xi)),
inference(resolution,[status(thm)],[f431,f395]) ).
fof(f6671,plain,
aSet0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f431,f367]) ).
fof(f6691,plain,
isFinite0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f259,f367]) ).
fof(f7192,definition,
( sQ721_spl
<=> isFinite0(slbdtrb0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition]) ).
fof(f7194,plain,
( sQ721_spl
| ~ isFinite0(slbdtrb0(sz00)) ),
inference(component_clause,[status(thm)],[f7192]) ).
fof(f7196,plain,
( sQ721_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7194,f5476]) ).
fof(f7197,plain,
sQ721_spl,
inference(contradiction_clause,[status(thm)],[f7196]) ).
fof(f7232,plain,
( aElementOf0(sK19_skl(xd,xY,xk),xT)
| ~ iLess0(xk,xK)
| ~ aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
| ~ aFunction0(xd)
| ~ isCountable0(xY)
| ~ aSubsetOf0(xY,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolution,[status(thm)],[f361,f401]) ).
fof(f7243,definition,
( sQ726_spl
<=> aElementOf0(sK19_skl(xd,xY,xk),xT) ),
introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition]) ).
fof(f7246,plain,
( sQ726_spl
| ~ sQ111_spl
| ~ sQ553_spl
| ~ sQ143_spl
| ~ sQ4_spl
| ~ sQ95_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f7232,f655,f1202,f473,f1569,f5780,f1330,f7243]) ).
fof(f7257,plain,
( aSubsetOf0(sK20_skl(xd,xY,xk),xY)
| ~ iLess0(xk,xK)
| ~ aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
| ~ aFunction0(xd)
| ~ isCountable0(xY)
| ~ aSubsetOf0(xY,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolution,[status(thm)],[f362,f401]) ).
fof(f7265,definition,
( sQ730_spl
<=> aSubsetOf0(sK20_skl(xd,xY,xk),xY) ),
introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition]) ).
fof(f7268,plain,
( sQ730_spl
| ~ sQ111_spl
| ~ sQ553_spl
| ~ sQ143_spl
| ~ sQ4_spl
| ~ sQ95_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f7257,f655,f1202,f473,f1569,f5780,f1330,f7265]) ).
fof(f7279,plain,
( isCountable0(sK20_skl(xd,xY,xk))
| ~ iLess0(xk,xK)
| ~ aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
| ~ aFunction0(xd)
| ~ isCountable0(xY)
| ~ aSubsetOf0(xY,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolution,[status(thm)],[f363,f401]) ).
fof(f7287,definition,
( sQ734_spl
<=> isCountable0(sK20_skl(xd,xY,xk)) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f7290,plain,
( sQ734_spl
| ~ sQ111_spl
| ~ sQ553_spl
| ~ sQ143_spl
| ~ sQ4_spl
| ~ sQ95_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f7279,f655,f1202,f473,f1569,f5780,f1330,f7287]) ).
fof(f7407,plain,
! [X0,X1,X2] :
( ~ isCountable0(X2)
| ~ aSubsetOf0(X2,xY)
| ~ aElementOf0(sK19_skl(xd,X1,X0),xT)
| ~ aElementOf0(sK21_skl(X2,sK19_skl(xd,X1,X0)),slbdtsldtrb0(sK20_skl(xd,X1,X0),X0))
| ~ iLess0(X0,xK)
| ~ aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
| szDzozmdt0(xd) != slbdtsldtrb0(X1,X0)
| ~ aFunction0(xd)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f364,f407]) ).
fof(f7409,definition,
! [X0,X1,X2] :
( sQ744_spl
<=> ( ~ isCountable0(X2)
| ~ aSubsetOf0(X2,xY)
| ~ aElementOf0(sK19_skl(xd,X1,X0),xT)
| ~ aElementOf0(sK21_skl(X2,sK19_skl(xd,X1,X0)),slbdtsldtrb0(sK20_skl(xd,X1,X0),X0))
| ~ iLess0(X0,xK)
| szDzozmdt0(xd) != slbdtsldtrb0(X1,X0)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition]) ).
fof(f7410,plain,
! [X0,X1,X2] :
( ~ sQ744_spl
| ~ isCountable0(X2)
| ~ aSubsetOf0(X2,xY)
| ~ aElementOf0(sK19_skl(xd,X1,X0),xT)
| ~ aElementOf0(sK21_skl(X2,sK19_skl(xd,X1,X0)),slbdtsldtrb0(sK20_skl(xd,X1,X0),X0))
| ~ iLess0(X0,xK)
| szDzozmdt0(xd) != slbdtsldtrb0(X1,X0)
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f7409]) ).
fof(f7412,plain,
( ~ sQ553_spl
| ~ sQ143_spl
| sQ744_spl ),
inference(split_clause,[status(thm)],[f7407,f7409,f1569,f5780]) ).
fof(f7434,definition,
( sQ749_spl
<=> isCountable0(sdtlpdtrp0(xN,xi)) ),
introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition]) ).
fof(f7436,plain,
( sQ749_spl
| ~ isCountable0(sdtlpdtrp0(xN,xi)) ),
inference(component_clause,[status(thm)],[f7434]) ).
fof(f7579,definition,
! [X0] :
( sQ765_spl
<=> ( X0 = sz00
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition]) ).
fof(f7580,plain,
! [X0] :
( ~ sQ765_spl
| X0 = sz00
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f7579]) ).
fof(f7615,definition,
( sQ771_spl
<=> isCountable0(sdtlpdtrp0(xN,sz00)) ),
introduced(definition,[new_symbols(definition,[sQ771_spl])],[split_symbol_definition]) ).
fof(f7617,plain,
( sQ771_spl
| ~ isCountable0(sdtlpdtrp0(xN,sz00)) ),
inference(component_clause,[status(thm)],[f7615]) ).
fof(f7622,definition,
( sQ773_spl
<=> aSubsetOf0(sdtlpdtrp0(xN,sz00),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ773_spl])],[split_symbol_definition]) ).
fof(f7624,plain,
( sQ773_spl
| ~ aSubsetOf0(sdtlpdtrp0(xN,sz00),szNzAzT0) ),
inference(component_clause,[status(thm)],[f7622]) ).
fof(f7637,definition,
( sQ776_spl
<=> aElementOf0(sz00,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ776_spl])],[split_symbol_definition]) ).
fof(f7639,plain,
( sQ776_spl
| ~ aElementOf0(sz00,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f7637]) ).
fof(f7649,plain,
( sQ771_spl
| ~ isCountable0(xS) ),
inference(forward_demodulation,[status(thm)],[f372,f7617]) ).
fof(f7650,plain,
( sQ771_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7649,f355]) ).
fof(f7651,plain,
sQ771_spl,
inference(contradiction_clause,[status(thm)],[f7650]) ).
fof(f7652,plain,
( sQ776_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f371,f7639]) ).
fof(f7653,plain,
( sQ776_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7652,f173]) ).
fof(f7654,plain,
sQ776_spl,
inference(contradiction_clause,[status(thm)],[f7653]) ).
fof(f7655,plain,
( sQ773_spl
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f372,f7624]) ).
fof(f7656,plain,
( sQ773_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7655,f354]) ).
fof(f7657,plain,
sQ773_spl,
inference(contradiction_clause,[status(thm)],[f7656]) ).
fof(f7671,plain,
( ~ sQ765_spl
| xK = sz00 ),
inference(resolution,[status(thm)],[f7580,f353]) ).
fof(f7687,plain,
( ~ sQ765_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7671,f365]) ).
fof(f7688,plain,
~ sQ765_spl,
inference(contradiction_clause,[status(thm)],[f7687]) ).
fof(f7874,definition,
( sQ806_spl
<=> aElementOf0(xk,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ806_spl])],[split_symbol_definition]) ).
fof(f7876,plain,
( sQ806_spl
| ~ aElementOf0(xk,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f7874]) ).
fof(f7889,plain,
( sQ806_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f371,f7876]) ).
fof(f7890,plain,
( sQ806_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7889,f367]) ).
fof(f7891,plain,
sQ806_spl,
inference(contradiction_clause,[status(thm)],[f7890]) ).
fof(f9590,plain,
! [X0] :
( ~ sQ744_spl
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY)
| ~ aElementOf0(sK19_skl(xd,xY,xk),xT)
| ~ aElementOf0(sK21_skl(X0,sK19_skl(xd,xY,xk)),slbdtsldtrb0(sK20_skl(xd,xY,xk),xk))
| ~ iLess0(xk,xK)
| ~ isCountable0(xY)
| ~ aSubsetOf0(xY,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolution,[status(thm)],[f7410,f401]) ).
fof(f9593,definition,
! [X0] :
( sQ940_spl
<=> ( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY)
| ~ aElementOf0(sK21_skl(X0,sK19_skl(xd,xY,xk)),slbdtsldtrb0(sK20_skl(xd,xY,xk),xk)) ) ),
introduced(definition,[new_symbols(definition,[sQ940_spl])],[split_symbol_definition]) ).
fof(f9594,plain,
! [X0] :
( ~ sQ940_spl
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xY)
| ~ aElementOf0(sK21_skl(X0,sK19_skl(xd,xY,xk)),slbdtsldtrb0(sK20_skl(xd,xY,xk),xk)) ),
inference(component_clause,[status(thm)],[f9593]) ).
fof(f9596,plain,
( ~ sQ744_spl
| ~ sQ726_spl
| sQ940_spl
| ~ sQ111_spl
| ~ sQ4_spl
| ~ sQ95_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f9590,f655,f1202,f473,f1330,f9593,f7243,f7409]) ).
fof(f12032,definition,
! [X0] :
( sQ1119_spl
<=> ( ~ isFinite0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1119_spl])],[split_symbol_definition]) ).
fof(f12033,plain,
! [X0] :
( ~ sQ1119_spl
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f12032]) ).
fof(f12057,plain,
( ~ sQ1119_spl
| ~ isFinite0(slcrc0) ),
inference(resolution,[status(thm)],[f12033,f414]) ).
fof(f12075,plain,
( ~ sQ1119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12057,f112]) ).
fof(f12076,plain,
~ sQ1119_spl,
inference(contradiction_clause,[status(thm)],[f12075]) ).
fof(f15765,definition,
( sQ1387_spl
<=> aElementOf0(xk,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ1387_spl])],[split_symbol_definition]) ).
fof(f15766,plain,
( ~ sQ1387_spl
| aElementOf0(xk,slcrc0) ),
inference(component_clause,[status(thm)],[f15765]) ).
fof(f15769,plain,
( ~ sQ1387_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15766,f415]) ).
fof(f15770,plain,
~ sQ1387_spl,
inference(contradiction_clause,[status(thm)],[f15769]) ).
fof(f24471,definition,
( sQ1925_spl
<=> sbrdtbr0(slcrc0) = xK ),
introduced(definition,[new_symbols(definition,[sQ1925_spl])],[split_symbol_definition]) ).
fof(f24472,plain,
( ~ sQ1925_spl
| sbrdtbr0(slcrc0) = xK ),
inference(component_clause,[status(thm)],[f24471]) ).
fof(f24477,plain,
( ~ sQ1925_spl
| sz00 = xK ),
inference(forward_demodulation,[status(thm)],[f977,f24472]) ).
fof(f24478,plain,
( ~ sQ1925_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24477,f365]) ).
fof(f24479,plain,
~ sQ1925_spl,
inference(contradiction_clause,[status(thm)],[f24478]) ).
fof(f24585,plain,
( sQ451_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4318,f6671]) ).
fof(f24586,plain,
sQ451_spl,
inference(contradiction_clause,[status(thm)],[f24585]) ).
fof(f24587,plain,
( sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1017,f6691]) ).
fof(f24588,plain,
sQ81_spl,
inference(contradiction_clause,[status(thm)],[f24587]) ).
fof(f25365,plain,
( sQ749_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f377,f7436]) ).
fof(f25368,plain,
( sQ749_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25365,f395]) ).
fof(f25369,plain,
sQ749_spl,
inference(contradiction_clause,[status(thm)],[f25368]) ).
fof(f27007,definition,
( sQ2109_spl
<=> aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ2109_spl])],[split_symbol_definition]) ).
fof(f27009,plain,
( sQ2109_spl
| ~ aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
inference(component_clause,[status(thm)],[f27007]) ).
fof(f27081,definition,
( sQ2127_spl
<=> aElementOf0(szszuzczcdt0(xi),szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ2127_spl])],[split_symbol_definition]) ).
fof(f27083,plain,
( sQ2127_spl
| ~ aElementOf0(szszuzczcdt0(xi),szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f27081]) ).
fof(f27107,plain,
( sQ2127_spl
| ~ aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f371,f27083]) ).
fof(f27139,plain,
( sQ2109_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f27009,f175]) ).
fof(f27141,plain,
( sQ2109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27139,f395]) ).
fof(f27142,plain,
sQ2109_spl,
inference(contradiction_clause,[status(thm)],[f27141]) ).
fof(f27143,plain,
( sQ2127_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f27107,f175]) ).
fof(f27145,plain,
( sQ2127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27143,f395]) ).
fof(f27146,plain,
sQ2127_spl,
inference(contradiction_clause,[status(thm)],[f27145]) ).
fof(f27422,definition,
( sQ2150_spl
<=> aSet0(slbdtrb0(xi)) ),
introduced(definition,[new_symbols(definition,[sQ2150_spl])],[split_symbol_definition]) ).
fof(f27424,plain,
( sQ2150_spl
| ~ aSet0(slbdtrb0(xi)) ),
inference(component_clause,[status(thm)],[f27422]) ).
fof(f27426,plain,
( sQ2150_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27424,f6670]) ).
fof(f27427,plain,
sQ2150_spl,
inference(contradiction_clause,[status(thm)],[f27426]) ).
fof(f34594,plain,
( ~ sQ940_spl
| ~ isCountable0(sK20_skl(xd,xY,xk))
| ~ aSubsetOf0(sK20_skl(xd,xY,xk),xY)
| ~ aElementOf0(sK19_skl(xd,xY,xk),xT)
| ~ isCountable0(sK20_skl(xd,xY,xk))
| ~ aSubsetOf0(sK20_skl(xd,xY,xk),xY) ),
inference(resolution,[status(thm)],[f9594,f406]) ).
fof(f34595,plain,
( ~ sQ940_spl
| ~ sQ726_spl
| ~ sQ734_spl
| ~ sQ730_spl ),
inference(split_clause,[status(thm)],[f34594,f7265,f7287,f7243,f9593]) ).
fof(f34596,plain,
$false,
inference(sat_refutation,[status(thm)],[f462,f464,f478,f622,f652,f658,f660,f696,f709,f819,f1060,f1205,f1210,f1284,f1333,f1356,f1572,f2044,f2949,f2951,f2953,f2956,f2959,f4661,f4663,f4665,f4676,f5499,f5664,f5731,f5783,f5850,f5894,f7197,f7246,f7268,f7290,f7412,f7651,f7654,f7657,f7688,f7891,f9596,f12076,f15770,f24479,f24586,f24588,f25369,f27142,f27146,f27427,f34595]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM591+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n002.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 02:45:17 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 234.11/30.03 % Refutation found
% 234.11/30.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 234.11/30.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.40/30.16 % Elapsed time: 29.722973 seconds
% 14.40/30.16 % CPU time: 234.753537 seconds
% 14.40/30.16 % Total memory used: 569.675 MB
% 14.40/30.16 % Net memory used: 507.145 MB
%------------------------------------------------------------------------------