%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM574+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 : n006.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:03 PM UTC 2026
% Result : Theorem 0.13s 0.67s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 178
% Syntax : Number of formulae : 666 ( 49 unt; 140 def)
% Number of atoms : 1990 ( 193 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 2350 (1026 ~;1048 |; 80 &)
% ( 147 <=>; 49 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 148 ( 146 usr; 138 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-2 aty)
% Number of variables : 424 ( 412 !; 12 ?)
% 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(f8,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> ~ isFinite0(W0) ),
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(f11,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aSubsetOf0(W1,W0)
=> isFinite0(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(f13,axiom,
! [W0,W1] :
( ( aSet0(W1)
& aSet0(W0) )
=> ( ( aSubsetOf0(W1,W0)
& aSubsetOf0(W0,W1) )
=> W0 = W1 ) ),
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(f26,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( szszuzczcdt0(W0) = szszuzczcdt0(W1)
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ? [W1] :
( W0 = szszuzczcdt0(W1)
& aElementOf0(W1,szNzAzT0) )
| W0 = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> W0 != szszuzczcdt0(W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(sz00,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W0,W1)
<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(W0,szszuzczcdt0(W0)) ),
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(f35,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [W0,W1,W2] :
( ( aElementOf0(W2,szNzAzT0)
& aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W1),W0)
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> iLess0(W0,szszuzczcdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [W0] :
( aSet0(W0)
=> aElement0(sbrdtbr0(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(f43,axiom,
! [W0] :
( ( isFinite0(W0)
& aSet0(W0) )
=> ! [W1] :
( aElement0(W1)
=> ( ~ aElementOf0(W1,W0)
=> sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( ( aElementOf0(W1,W0)
& isFinite0(W0) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( ( aSubsetOf0(W1,W0)
& isFinite0(W0) )
=> sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aSet0(W0) )
=> ( ( sdtlseqdt0(W1,sbrdtbr0(W0))
& isFinite0(W0) )
=> ? [W2] :
( sbrdtbr0(W2) = W1
& aSubsetOf0(W2,W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,definition,
! [W0] :
( ( W0 != slcrc0
& aSubsetOf0(W0,szNzAzT0) )
=> ! [W1] :
( W1 = szmzizndt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElement0(sdtlpdtrp0(W0,W1)) ) ),
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(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(f83,hypothesis,
( aElementOf0(xi,szNzAzT0)
& aElementOf0(xj,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
( ( ? [W0] :
( szszuzczcdt0(W0) = xi
& aElementOf0(W0,szNzAzT0) )
& sdtlseqdt0(xj,xi) )
=> ( sdtlseqdt0(xj,xi)
=> aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,conjecture,
( sdtlseqdt0(xj,xi)
=> aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,negated_conjecture,
~ ( sdtlseqdt0(xj,xi)
=> aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj)) ),
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(f103,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f104,plain,
! [X0] :
( aElementOf0(sK0_skl(X0),X0)
| ~ aSet0(X0)
| X0 = slcrc0 ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f105,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f108,plain,
! [W0] :
( ~ isFinite0(W0)
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f109,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
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(f116,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
! [X0,X1] :
( aElementOf0(sK1_skl(X1,X0),X1)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f120,plain,
! [W0] :
( ! [W1] :
( isFinite0(W1)
| ~ aSubsetOf0(W1,W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f121,plain,
! [X0,X1] :
( isFinite0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
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(f124,plain,
! [W0,W1] :
( W0 = W1
| ~ aSubsetOf0(W1,W0)
| ~ aSubsetOf0(W0,W1)
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f125,plain,
! [X0,X1] :
( X0 = X1
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,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(f127,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f164,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f165,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f166,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f167,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f168,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [X0] :
( szszuzczcdt0(X0) != sz00
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f170,plain,
! [W0,W1] :
( W0 = W1
| szszuzczcdt0(W0) != szszuzczcdt0(W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f171,plain,
! [X0,X1] :
( X0 = X1
| szszuzczcdt0(X0) != szszuzczcdt0(X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
! [W0] :
( ? [W1] :
( W0 = szszuzczcdt0(W1)
& aElementOf0(W1,szNzAzT0) )
| W0 = sz00
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f173,plain,
! [W0] :
( ( W0 = szszuzczcdt0(sK4_skl(W0))
& aElementOf0(sK4_skl(W0),szNzAzT0) )
| W0 = sz00
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(W1,sK4_skl(W0))],[f172]) ).
fof(f174,plain,
! [X0] :
( aElementOf0(sK4_skl(X0),szNzAzT0)
| X0 = sz00
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0] :
( X0 = szszuzczcdt0(sK4_skl(X0))
| X0 = sz00
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f176,plain,
! [W0] :
( W0 != szszuzczcdt0(W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f177,plain,
! [X0] :
( X0 != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f180,plain,
! [W0] :
( sdtlseqdt0(sz00,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f181,plain,
! [X0] :
( sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
! [W0] :
( ~ sdtlseqdt0(szszuzczcdt0(W0),sz00)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f183,plain,
! [X0] :
( ~ sdtlseqdt0(szszuzczcdt0(X0),sz00)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f184,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f185,plain,
! [W0,W1] :
( ( ( ~ sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))
| sdtlseqdt0(W0,W1) )
& ( sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1))
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f187,plain,
! [X0,X1] :
( ~ sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f188,plain,
! [W0] :
( sdtlseqdt0(W0,szszuzczcdt0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f189,plain,
! [X0] :
( sdtlseqdt0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f190,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f191,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f192,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f193,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f194,plain,
! [W0,W1,W2] :
( sdtlseqdt0(W0,W2)
| ~ sdtlseqdt0(W1,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f195,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f196,plain,
! [W0,W1] :
( sdtlseqdt0(szszuzczcdt0(W1),W0)
| sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f197,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f200,plain,
! [W0] :
( iLess0(W0,szszuzczcdt0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f201,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [W0] :
( aElement0(sbrdtbr0(W0))
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f203,plain,
! [X0] :
( aElement0(sbrdtbr0(X0))
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f208,plain,
! [W0] :
( ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f209,plain,
! [W0] :
( ( ( W0 != slcrc0
| sbrdtbr0(W0) = sz00 )
& ( W0 = slcrc0
| sbrdtbr0(W0) != sz00 ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f208]) ).
fof(f211,plain,
! [X0] :
( X0 != slcrc0
| sbrdtbr0(X0) = sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f212,plain,
! [W0] :
( ! [W1] :
( sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0))
| aElementOf0(W1,W0)
| ~ aElement0(W1) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f213,plain,
! [X0,X1] :
( sbrdtbr0(sdtpldt0(X0,X1)) = szszuzczcdt0(sbrdtbr0(X0))
| aElementOf0(X1,X0)
| ~ aElement0(X1)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
! [W0] :
( ! [W1] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0)
| ~ aElementOf0(W1,W0)
| ~ isFinite0(W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f215,plain,
! [X0,X1] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0)
| ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f216,plain,
! [W0] :
( ! [W1] :
( sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0))
| ~ aSubsetOf0(W1,W0)
| ~ isFinite0(W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f217,plain,
! [X0,X1] :
( sdtlseqdt0(sbrdtbr0(X1),sbrdtbr0(X0))
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f218,plain,
! [W0,W1] :
( ? [W2] :
( sbrdtbr0(W2) = W1
& aSubsetOf0(W2,W0) )
| ~ sdtlseqdt0(W1,sbrdtbr0(W0))
| ~ isFinite0(W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f219,plain,
! [W0,W1] :
( ( sbrdtbr0(sK5_skl(W1,W0)) = W1
& aSubsetOf0(sK5_skl(W1,W0),W0) )
| ~ sdtlseqdt0(W1,sbrdtbr0(W0))
| ~ isFinite0(W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W2,sK5_skl(W1,W0))],[f218]) ).
fof(f220,plain,
! [X0,X1] :
( aSubsetOf0(sK5_skl(X1,X0),X0)
| ~ sdtlseqdt0(X1,sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f221,plain,
! [X0,X1] :
( sbrdtbr0(sK5_skl(X1,X0)) = X1
| ~ sdtlseqdt0(X1,sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f222,plain,
! [W0] :
( ! [W1] :
( W1 = szmzizndt0(W0)
<=> ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f223,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ sdtlseqdt0(W1,W2)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzizndt0(W0) )
& ( ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzizndt0(W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ sdtlseqdt0(W1,W2)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzizndt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzizndt0(W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f223]) ).
fof(f225,plain,
! [W0] :
( ( ! [W1] :
( ( ~ sdtlseqdt0(W1,sK6_skl(W1,W0))
& aElementOf0(sK6_skl(W1,W0),W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzizndt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzizndt0(W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W2,sK6_skl(W1,W0))],[f224]) ).
fof(f226,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| X1 != szmzizndt0(X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f227,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0)
| X1 != szmzizndt0(X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f228,plain,
! [X0,X1] :
( aElementOf0(sK6_skl(X1,X0),X0)
| ~ aElementOf0(X1,X0)
| X1 = szmzizndt0(X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
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(f298,plain,
! [W0] :
( ! [W1] :
( aElement0(sdtlpdtrp0(W0,W1))
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f65]) ).
fof(f299,plain,
! [X0,X1] :
( aElement0(sdtlpdtrp0(X0,X1))
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f344,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f345,plain,
isFinite0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f346,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f347,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f348,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f360,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f361,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f362,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(f363,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f364,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f365,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f367,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f368,plain,
! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f369,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f370,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f371,plain,
aElementOf0(xj,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f372,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f375,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj))
| ~ sdtlseqdt0(xj,xi)
| ! [W0] :
( szszuzczcdt0(W0) != xi
| ~ aElementOf0(W0,szNzAzT0) )
| ~ sdtlseqdt0(xj,xi) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f376,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj))
| ~ sdtlseqdt0(xj,xi)
| szszuzczcdt0(X0) != xi
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(xj,xi) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f377,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj))
& sdtlseqdt0(xj,xi) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f378,plain,
sdtlseqdt0(xj,xi),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f379,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj)),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f386,definition,
( sQ0_spl
<=> sdtlseqdt0(xj,xi) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f388,plain,
( sQ0_spl
| ~ sdtlseqdt0(xj,xi) ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f389,definition,
! [X0] :
( sQ1_spl
<=> ( szszuzczcdt0(X0) != xi
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f390,plain,
! [X0] :
( ~ sQ1_spl
| szszuzczcdt0(X0) != xi
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f389]) ).
fof(f392,definition,
( sQ2_spl
<=> aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( ~ sQ2_spl
| aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,xj)) ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f395,plain,
( sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f376,f386,f389,f392]) ).
fof(f396,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f102]) ).
fof(f397,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f103]) ).
fof(f408,plain,
( sbrdtbr0(slcrc0) = sz00
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f211]) ).
fof(f409,plain,
! [X0] :
( aElementOf0(szmzizndt0(X0),X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f226]) ).
fof(f410,plain,
! [X0,X1] :
( sdtlseqdt0(szmzizndt0(X0),X1)
| ~ aElementOf0(X1,X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f227]) ).
fof(f438,plain,
! [X0,X1] :
( ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| aSubsetOf0(X0,X0) ),
inference(resolution,[status(thm)],[f123,f116]) ).
fof(f439,plain,
aSubsetOf0(slcrc0,slcrc0),
inference(resolution,[status(thm)],[f396,f123]) ).
fof(f440,plain,
! [X0,X1] :
( aElementOf0(X1,slcrc0)
| ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f396,f117]) ).
fof(f441,plain,
aSubsetOf0(szNzAzT0,szNzAzT0),
inference(resolution,[status(thm)],[f164,f123]) ).
fof(f442,plain,
! [X0,X1] :
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f164,f117]) ).
fof(f443,plain,
aSubsetOf0(xT,xT),
inference(resolution,[status(thm)],[f344,f123]) ).
fof(f444,plain,
! [X0,X1] :
( aElementOf0(X1,xT)
| ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,xT) ),
inference(resolution,[status(thm)],[f344,f117]) ).
fof(f445,plain,
( ~ aSet0(slcrc0)
| slcrc0 = slcrc0 ),
inference(resolution,[status(thm)],[f104,f397]) ).
fof(f446,definition,
( sQ3_spl
<=> slcrc0 = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f449,definition,
( sQ4_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ4_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f445,f446,f449]) ).
fof(f453,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f451,f396]) ).
fof(f454,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f453]) ).
fof(f455,plain,
! [X0,X1] :
( X1 = X0
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f125,f116]) ).
fof(f456,plain,
! [X0] :
( X0 = xT
| ~ aSubsetOf0(xT,X0)
| ~ aSubsetOf0(X0,xT) ),
inference(resolution,[status(thm)],[f455,f344]) ).
fof(f457,plain,
! [X0] :
( X0 = szNzAzT0
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f455,f164]) ).
fof(f458,plain,
! [X0] :
( X0 = slcrc0
| ~ aSubsetOf0(slcrc0,X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f455,f396]) ).
fof(f460,plain,
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sdtlseqdt0(sK0_skl(szNzAzT0),sK0_skl(szNzAzT0)) ),
inference(resolution,[status(thm)],[f191,f104]) ).
fof(f461,plain,
sdtlseqdt0(xi,xi),
inference(resolution,[status(thm)],[f191,f372]) ).
fof(f462,plain,
sdtlseqdt0(xj,xj),
inference(resolution,[status(thm)],[f191,f371]) ).
fof(f463,definition,
( sQ5_spl
<=> sdtlseqdt0(sK0_skl(szNzAzT0),sK0_skl(szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( ~ sQ5_spl
| sdtlseqdt0(sK0_skl(szNzAzT0),sK0_skl(szNzAzT0)) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,definition,
( sQ6_spl
<=> szNzAzT0 = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ6_spl
| szNzAzT0 = slcrc0 ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ7_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ7_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f460,f463,f466,f469]) ).
fof(f473,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f471,f164]) ).
fof(f474,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f473]) ).
fof(f479,plain,
( ~ sQ6_spl
| aElementOf0(xi,slcrc0) ),
inference(backward_demodulation,[status(thm)],[f467,f372]) ).
fof(f483,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f479,f397]) ).
fof(f484,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f483]) ).
fof(f485,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f127,f116]) ).
fof(f486,plain,
! [X0,X1] :
( aSubsetOf0(X1,xT)
| ~ aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f485,f344]) ).
fof(f487,plain,
! [X0,X1] :
( aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f485,f396]) ).
fof(f489,plain,
! [X0] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| X0 = sK0_skl(szNzAzT0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f193,f104]) ).
fof(f490,definition,
! [X0] :
( sQ8_spl
<=> ( X0 = sK0_skl(szNzAzT0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f491,plain,
! [X0] :
( ~ sQ8_spl
| X0 = sK0_skl(szNzAzT0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f493,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f489,f490,f466,f469]) ).
fof(f494,plain,
! [X0,X1] :
( aSubsetOf0(X1,szNzAzT0)
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f164,f485]) ).
fof(f498,plain,
( ~ isFinite0(szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f109,f165]) ).
fof(f499,plain,
( ~ isFinite0(xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f109,f348]) ).
fof(f500,plain,
( ~ isCountable0(xT)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f109,f345]) ).
fof(f501,plain,
( ~ isCountable0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f109,f105]) ).
fof(f502,definition,
( sQ9_spl
<=> isFinite0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( ~ sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f498,f469,f502]) ).
fof(f506,definition,
( sQ10_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( sQ10_spl
| ~ aSet0(xS) ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,definition,
( sQ11_spl
<=> isFinite0(xS) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( sQ11_spl
| ~ isFinite0(xS) ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,plain,
( ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f499,f506,f509]) ).
fof(f513,definition,
( sQ12_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( sQ12_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,definition,
( sQ13_spl
<=> isCountable0(xT) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ13_spl
| ~ isCountable0(xT) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,plain,
( ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f500,f513,f516]) ).
fof(f520,definition,
( sQ14_spl
<=> isCountable0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( ~ sQ14_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f501,f449,f520]) ).
fof(f524,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f344]) ).
fof(f525,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f524]) ).
fof(f529,plain,
! [X0] :
( aElementOf0(sK1_skl(slcrc0,X0),slcrc0)
| aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f118,f396]) ).
fof(f530,plain,
! [X0,X1,X2] :
( ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2)
| aElementOf0(sK1_skl(X1,X0),X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f118,f116]) ).
fof(f531,plain,
! [X0] :
( aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f397]) ).
fof(f532,plain,
! [X0] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f195,f104]) ).
fof(f533,plain,
! [X0,X1] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X1)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f195,f104]) ).
fof(f534,plain,
! [X0,X1] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X1,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f195,f104]) ).
fof(f535,definition,
! [X0] :
( sQ15_spl
<=> ( sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( ~ sQ7_spl
| sQ6_spl
| ~ sQ5_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f532,f535,f463,f466,f469]) ).
fof(f539,definition,
! [X0,X1] :
( sQ16_spl
<=> ( sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X1)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f540,plain,
! [X0,X1] :
( ~ sQ16_spl
| sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X1)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f533,f539,f466,f469]) ).
fof(f543,definition,
! [X0,X1] :
( sQ17_spl
<=> ( sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X1,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f544,plain,
! [X0,X1] :
( ~ sQ17_spl
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X1,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f543]) ).
fof(f546,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f534,f543,f466,f469]) ).
fof(f547,plain,
! [X0] :
( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(xi,xi)
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f372,f195]) ).
fof(f548,plain,
! [X0,X1] :
( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(X1,xi)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f372,f195]) ).
fof(f550,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(xi,X1)
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f372,f195]) ).
fof(f551,plain,
! [X0] :
( X0 = xi
| ~ sdtlseqdt0(xi,X0)
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f372,f193]) ).
fof(f552,definition,
! [X0] :
( sQ18_spl
<=> ( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f555,definition,
( sQ19_spl
<=> sdtlseqdt0(xi,xi) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( sQ19_spl
| ~ sdtlseqdt0(xi,xi) ),
inference(component_clause,[status(thm)],[f555]) ).
fof(f558,plain,
( ~ sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f547,f552,f555]) ).
fof(f560,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f557,f461]) ).
fof(f561,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f560]) ).
fof(f562,plain,
! [X0] :
( sdtlseqdt0(X0,xj)
| ~ sdtlseqdt0(xj,xj)
| ~ sdtlseqdt0(X0,xj)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f371,f195]) ).
fof(f563,plain,
! [X0,X1] :
( sdtlseqdt0(X0,xj)
| ~ sdtlseqdt0(X1,xj)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f371,f195]) ).
fof(f567,definition,
! [X0] :
( sQ20_spl
<=> ( sdtlseqdt0(X0,xj)
| ~ sdtlseqdt0(X0,xj)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f570,definition,
( sQ21_spl
<=> sdtlseqdt0(xj,xj) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f572,plain,
( sQ21_spl
| ~ sdtlseqdt0(xj,xj) ),
inference(component_clause,[status(thm)],[f570]) ).
fof(f573,plain,
( ~ sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f562,f567,f570]) ).
fof(f575,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f572,f462]) ).
fof(f576,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f575]) ).
fof(f577,plain,
! [X0] :
( sQ10_spl
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f508,f116]) ).
fof(f582,plain,
! [X0] :
( isFinite0(X0)
| ~ aSubsetOf0(X0,xT)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f121,f345]) ).
fof(f583,plain,
! [X0] :
( isFinite0(X0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f121,f105]) ).
fof(f584,plain,
! [X0,X1,X2] :
( ~ aSubsetOf0(X0,X2)
| ~ isFinite0(X2)
| ~ aSet0(X2)
| isFinite0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f121,f121]) ).
fof(f588,plain,
! [X0,X1] :
( ~ isCountable0(X1)
| ~ aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f121,f109]) ).
fof(f589,definition,
! [X0] :
( sQ22_spl
<=> ( isFinite0(X0)
| ~ aSubsetOf0(X0,xT) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f592,plain,
( sQ22_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f582,f513,f589]) ).
fof(f593,definition,
! [X0] :
( sQ23_spl
<=> ( isFinite0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f594,plain,
! [X0] :
( ~ sQ23_spl
| isFinite0(X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f596,plain,
( sQ23_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f583,f449,f593]) ).
fof(f597,plain,
! [X0,X1,X2] :
( ~ aSubsetOf0(X1,X2)
| ~ isFinite0(X2)
| ~ aSet0(X2)
| isFinite0(X0)
| ~ aSubsetOf0(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f116]) ).
fof(f599,plain,
! [X0,X1] :
( ~ isCountable0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f588,f116]) ).
fof(f606,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(backward_subsumption_resolution,[status(thm)],[f367,f369]) ).
fof(f612,plain,
! [X0] :
( ~ aSubsetOf0(X0,szNzAzT0)
| aSubsetOf0(X0,X0) ),
inference(resolution,[status(thm)],[f438,f164]) ).
fof(f614,plain,
! [X0] :
( ~ aSubsetOf0(X0,slcrc0)
| aSubsetOf0(X0,X0) ),
inference(resolution,[status(thm)],[f438,f396]) ).
fof(f619,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f379]) ).
fof(f620,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f619]) ).
fof(f621,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f378]) ).
fof(f622,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f621]) ).
fof(f651,plain,
( sQ10_spl
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f347,f577]) ).
fof(f652,plain,
aSubsetOf0(xS,xS),
inference(resolution,[status(thm)],[f347,f612]) ).
fof(f653,plain,
( sQ10_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f651,f469,f506]) ).
fof(f673,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f606,f370]) ).
fof(f697,plain,
( ~ sQ1_spl
| xK != xi
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f390]) ).
fof(f698,plain,
( isCountable0(sdtlpdtrp0(xN,xK))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f673]) ).
fof(f699,definition,
( sQ30_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( sQ30_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(component_clause,[status(thm)],[f699]) ).
fof(f702,definition,
( sQ31_spl
<=> xK = xi ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( ~ sQ1_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f697,f699,f702,f389]) ).
fof(f706,definition,
( sQ32_spl
<=> isCountable0(sdtlpdtrp0(xN,xK)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( ~ sQ32_spl
| isCountable0(sdtlpdtrp0(xN,xK)) ),
inference(component_clause,[status(thm)],[f706]) ).
fof(f709,plain,
( sQ32_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f698,f699,f706]) ).
fof(f710,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f701,f360]) ).
fof(f711,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f710]) ).
fof(f721,plain,
! [X0] :
( aSubsetOf0(szDzozmdt0(X0),szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(resolution,[status(thm)],[f297,f123]) ).
fof(f724,definition,
( sQ33_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f726,plain,
( sQ33_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f724]) ).
fof(f756,plain,
( ~ sQ32_spl
| ~ isFinite0(sdtlpdtrp0(xN,xK))
| ~ aSet0(sdtlpdtrp0(xN,xK)) ),
inference(resolution,[status(thm)],[f707,f109]) ).
fof(f757,definition,
( sQ34_spl
<=> aSet0(sdtlpdtrp0(xN,xK)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f759,plain,
( sQ34_spl
| ~ aSet0(sdtlpdtrp0(xN,xK)) ),
inference(component_clause,[status(thm)],[f757]) ).
fof(f760,definition,
( sQ35_spl
<=> isFinite0(sdtlpdtrp0(xN,xK)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ32_spl
| ~ sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f756,f757,f760,f706]) ).
fof(f764,plain,
! [X0] :
( sQ34_spl
| ~ aSubsetOf0(sdtlpdtrp0(xN,xK),X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f759,f116]) ).
fof(f765,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(forward_subsumption_resolution,[status(thm)],[f440,f397]) ).
fof(f768,plain,
( aSubsetOf0(szNzAzT0,szDzozmdt0(xN))
| ~ aFunction0(xN) ),
inference(paramodulation,[status(thm)],[f364,f721]) ).
fof(f769,plain,
( aSubsetOf0(szDzozmdt0(xN),szNzAzT0)
| ~ aFunction0(xN) ),
inference(paramodulation,[status(thm)],[f364,f721]) ).
fof(f770,definition,
( sQ36_spl
<=> aSubsetOf0(szNzAzT0,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f773,plain,
( sQ36_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f768,f724,f770]) ).
fof(f774,definition,
( sQ37_spl
<=> aSubsetOf0(szDzozmdt0(xN),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( sQ37_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f769,f724,f774]) ).
fof(f778,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f726,f363]) ).
fof(f779,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f778]) ).
fof(f782,plain,
( sQ34_spl
| ~ aElementOf0(xK,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f764,f369]) ).
fof(f783,definition,
( sQ38_spl
<=> aElementOf0(xK,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f785,plain,
( sQ38_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(component_clause,[status(thm)],[f783]) ).
fof(f786,plain,
( sQ34_spl
| ~ sQ38_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f782,f469,f783,f757]) ).
fof(f787,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f785,f346]) ).
fof(f788,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f787]) ).
fof(f790,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) ),
inference(resolution,[status(thm)],[f442,f347]) ).
fof(f794,plain,
( isCountable0(xS)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f365,f370]) ).
fof(f795,plain,
( aSubsetOf0(xS,szNzAzT0)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f365,f369]) ).
fof(f796,plain,
( aElement0(xS)
| ~ aElementOf0(sz00,szDzozmdt0(xN))
| ~ aFunction0(xN) ),
inference(paramodulation,[status(thm)],[f365,f299]) ).
fof(f797,definition,
( sQ39_spl
<=> aElementOf0(sz00,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f799,plain,
( sQ39_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f800,definition,
( sQ40_spl
<=> isCountable0(xS) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f803,plain,
( sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f794,f797,f800]) ).
fof(f804,definition,
( sQ41_spl
<=> aSubsetOf0(xS,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( sQ41_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f795,f797,f804]) ).
fof(f808,definition,
( sQ42_spl
<=> aElementOf0(sz00,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f810,plain,
( sQ42_spl
| ~ aElementOf0(sz00,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f808]) ).
fof(f811,definition,
( sQ43_spl
<=> aElement0(xS) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f814,plain,
( sQ43_spl
| ~ sQ42_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f796,f724,f808,f811]) ).
fof(f815,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f799,f166]) ).
fof(f816,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f815]) ).
fof(f817,plain,
( sQ42_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f364,f810]) ).
fof(f818,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f166]) ).
fof(f819,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f818]) ).
fof(f834,plain,
! [X0] :
( ~ aElementOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f531,f765]) ).
fof(f835,plain,
( aSubsetOf0(slcrc0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f531,f614]) ).
fof(f836,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,slcrc0)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f531,f444]) ).
fof(f838,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slcrc0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f531,f442]) ).
fof(f840,definition,
( sQ44_spl
<=> aSubsetOf0(slcrc0,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f844,definition,
! [X0] :
( sQ45_spl
<=> ~ aElementOf0(X0,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f847,plain,
( sQ45_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f834,f449,f844]) ).
fof(f848,plain,
( sQ44_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f835,f449,f840]) ).
fof(f849,definition,
! [X0] :
( sQ46_spl
<=> ( aElementOf0(X0,xT)
| ~ aElementOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f852,plain,
( sQ46_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f836,f513,f849]) ).
fof(f854,definition,
! [X0] :
( sQ47_spl
<=> ( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f857,plain,
( sQ47_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f838,f469,f854]) ).
fof(f860,plain,
( ~ sQ23_spl
| ~ aSet0(slcrc0)
| isFinite0(slcrc0) ),
inference(resolution,[status(thm)],[f594,f531]) ).
fof(f861,definition,
( sQ48_spl
<=> isFinite0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( ~ sQ23_spl
| ~ sQ4_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f860,f861,f449,f593]) ).
fof(f912,plain,
( ~ aSet0(xS)
| xS = slcrc0
| aElementOf0(sK0_skl(xS),szNzAzT0) ),
inference(resolution,[status(thm)],[f790,f104]) ).
fof(f913,definition,
( sQ49_spl
<=> aElementOf0(sK0_skl(xS),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f916,definition,
( sQ50_spl
<=> xS = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f917,plain,
( ~ sQ50_spl
| xS = slcrc0 ),
inference(component_clause,[status(thm)],[f916]) ).
fof(f919,plain,
( ~ sQ10_spl
| sQ50_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f912,f913,f916,f506]) ).
fof(f920,plain,
( xT = xT
| ~ aSubsetOf0(xT,xT) ),
inference(resolution,[status(thm)],[f456,f443]) ).
fof(f921,definition,
( sQ51_spl
<=> aSubsetOf0(xT,xT) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ51_spl
| ~ aSubsetOf0(xT,xT) ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f924,definition,
( sQ52_spl
<=> xT = xT ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f927,plain,
( sQ52_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f920,f921,f924]) ).
fof(f928,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f443]) ).
fof(f929,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f928]) ).
fof(f950,plain,
( sQ11_spl
| ~ sQ50_spl
| ~ isFinite0(slcrc0) ),
inference(backward_demodulation,[status(thm)],[f917,f511]) ).
fof(f954,plain,
( sQ11_spl
| ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f950,f105]) ).
fof(f955,plain,
( sQ11_spl
| ~ sQ50_spl ),
inference(contradiction_clause,[status(thm)],[f954]) ).
fof(f963,plain,
( szNzAzT0 = szNzAzT0
| ~ aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(resolution,[status(thm)],[f457,f441]) ).
fof(f964,definition,
( sQ55_spl
<=> aSubsetOf0(szNzAzT0,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f966,plain,
( sQ55_spl
| ~ aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f964]) ).
fof(f967,definition,
( sQ56_spl
<=> szNzAzT0 = szNzAzT0 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( sQ56_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f963,f964,f967]) ).
fof(f971,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f966,f441]) ).
fof(f972,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f971]) ).
fof(f1044,plain,
! [X0] :
( aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,xT)
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f486,f443]) ).
fof(f1045,plain,
! [X0] :
( ~ aSet0(xT)
| aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f486,f531]) ).
fof(f1054,definition,
! [X0] :
( sQ57_spl
<=> ( aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,xT) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1057,plain,
( sQ57_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1044,f513,f1054]) ).
fof(f1058,definition,
! [X0] :
( sQ58_spl
<=> ( aSubsetOf0(X0,xT)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1061,plain,
( ~ sQ12_spl
| sQ58_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1045,f449,f1058,f513]) ).
fof(f1079,definition,
( sQ64_spl
<=> xT = szNzAzT0 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1080,plain,
( ~ sQ64_spl
| xT = szNzAzT0 ),
inference(component_clause,[status(thm)],[f1079]) ).
fof(f1088,plain,
! [X0] :
( aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f487,f439]) ).
fof(f1098,definition,
! [X0] :
( sQ66_spl
<=> ( aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1101,plain,
( sQ66_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1088,f449,f1098]) ).
fof(f1108,definition,
! [X0] :
( sQ68_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1111,definition,
( sQ69_spl
<=> aSubsetOf0(slcrc0,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1129,plain,
( sQ13_spl
| ~ sQ64_spl
| ~ isCountable0(szNzAzT0) ),
inference(backward_demodulation,[status(thm)],[f1080,f518]) ).
fof(f1137,plain,
( sQ13_spl
| ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1129,f165]) ).
fof(f1138,plain,
( sQ13_spl
| ~ sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f1137]) ).
fof(f1191,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| sK0_skl(szNzAzT0) = sK0_skl(szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f491,f464]) ).
fof(f1194,definition,
( sQ72_spl
<=> aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1196,plain,
( sQ72_spl
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(component_clause,[status(thm)],[f1194]) ).
fof(f1197,definition,
( sQ73_spl
<=> sK0_skl(szNzAzT0) = sK0_skl(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1200,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| sQ73_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1191,f1194,f1197,f490,f463]) ).
fof(f1203,plain,
! [X0] :
( aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f494,f347]) ).
fof(f1205,plain,
! [X0] :
( aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f494,f441]) ).
fof(f1206,plain,
! [X0] :
( ~ aSet0(szNzAzT0)
| aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f494,f531]) ).
fof(f1213,definition,
! [X0] :
( sQ74_spl
<=> ( aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1214,plain,
! [X0] :
( ~ sQ74_spl
| aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f1213]) ).
fof(f1216,plain,
( sQ74_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1203,f506,f1213]) ).
fof(f1217,definition,
! [X0] :
( sQ75_spl
<=> ( aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1220,plain,
( sQ75_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1205,f469,f1217]) ).
fof(f1221,definition,
! [X0] :
( sQ76_spl
<=> ( aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
! [X0] :
( ~ sQ76_spl
| aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(component_clause,[status(thm)],[f1221]) ).
fof(f1224,plain,
( ~ sQ7_spl
| sQ76_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1206,f449,f1221,f469]) ).
fof(f1226,definition,
! [X0] :
( sQ77_spl
<=> ( ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1227,plain,
! [X0] :
( ~ sQ77_spl
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f1226]) ).
fof(f1229,definition,
( sQ78_spl
<=> aSubsetOf0(szNzAzT0,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1238,plain,
! [X0] :
( ~ sQ77_spl
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1227,f531]) ).
fof(f1246,plain,
( sQ72_spl
| ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0 ),
inference(resolution,[status(thm)],[f1196,f104]) ).
fof(f1247,plain,
( sQ72_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1246,f466,f469,f1194]) ).
fof(f1251,plain,
( ~ sQ77_spl
| ~ aSet0(szNzAzT0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1238,f531]) ).
fof(f1254,plain,
( ~ sQ77_spl
| ~ sQ7_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1251,f449,f469,f1226]) ).
fof(f1272,plain,
( ~ sQ76_spl
| szNzAzT0 = slcrc0
| ~ aSubsetOf0(szNzAzT0,slcrc0)
| ~ aSubsetOf0(slcrc0,slcrc0) ),
inference(resolution,[status(thm)],[f1222,f458]) ).
fof(f1276,plain,
( ~ sQ76_spl
| sQ6_spl
| ~ sQ78_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1272,f840,f1229,f466,f1221]) ).
fof(f1279,plain,
( ~ sQ74_spl
| ~ aSet0(xS)
| aSubsetOf0(slcrc0,szNzAzT0) ),
inference(resolution,[status(thm)],[f1214,f531]) ).
fof(f1280,plain,
( ~ sQ74_spl
| ~ sQ10_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1279,f1111,f506,f1213]) ).
fof(f1286,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f599,f105]) ).
fof(f1290,plain,
! [X0] :
( ~ aSubsetOf0(xS,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f599,f348]) ).
fof(f1294,plain,
! [X0] :
( ~ aSubsetOf0(szNzAzT0,X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f599,f165]) ).
fof(f1296,definition,
! [X0] :
( sQ80_spl
<=> ( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1299,plain,
( sQ80_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1286,f449,f1296]) ).
fof(f1311,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,slcrc0)
| aElementOf0(sK1_skl(X1,X0),X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f530,f396]) ).
fof(f1313,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,slcrc0)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1311,f765]) ).
fof(f1321,plain,
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sK0_skl(szNzAzT0) != szszuzczcdt0(sK0_skl(szNzAzT0)) ),
inference(resolution,[status(thm)],[f177,f104]) ).
fof(f1323,definition,
( sQ81_spl
<=> sK0_skl(szNzAzT0) = szszuzczcdt0(sK0_skl(szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1326,plain,
( ~ sQ7_spl
| sQ6_spl
| ~ sQ81_spl ),
inference(split_clause,[status(thm)],[f1321,f1323,f466,f469]) ).
fof(f1342,plain,
( xK != sz00
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f169]) ).
fof(f1343,definition,
( sQ82_spl
<=> xK = sz00 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1346,plain,
( ~ sQ82_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1342,f699,f1343]) ).
fof(f1357,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ16_spl
| sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f540,f464]) ).
fof(f1387,definition,
! [X0] :
( sQ91_spl
<=> ( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1390,definition,
( sQ92_spl
<=> sdtlseqdt0(sK0_skl(szNzAzT0),xi) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1392,plain,
( sQ92_spl
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),xi) ),
inference(component_clause,[status(thm)],[f1390]) ).
fof(f1404,definition,
! [X0] :
( sQ95_spl
<=> ( sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1407,plain,
( ~ sQ5_spl
| ~ sQ16_spl
| sQ95_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1357,f1194,f1404,f539,f463]) ).
fof(f1411,plain,
( ~ aSubsetOf0(xS,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1290,f105]) ).
fof(f1416,plain,
! [X0] :
( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0)
| ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1290,f487]) ).
fof(f1419,definition,
( sQ96_spl
<=> aSubsetOf0(xS,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( ~ sQ96_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1411,f449,f1419]) ).
fof(f1427,definition,
! [X0] :
( sQ97_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1430,plain,
( sQ97_spl
| ~ sQ48_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1416,f449,f861,f1427]) ).
fof(f1438,plain,
! [X0] :
( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0)
| ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1294,f487]) ).
fof(f1445,plain,
( sQ68_spl
| ~ sQ48_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1438,f449,f861,f1108]) ).
fof(f1447,plain,
! [X0] :
( ~ aSet0(slcrc0)
| aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1313,f531]) ).
fof(f1449,definition,
! [X0] :
( sQ98_spl
<=> ( aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1452,plain,
( ~ sQ4_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1447,f1449,f449]) ).
fof(f1457,plain,
! [X0] :
( ~ sQ17_spl
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(xj,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,xj)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f544,f371]) ).
fof(f1458,plain,
! [X0] :
( ~ sQ17_spl
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(xi,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f544,f372]) ).
fof(f1487,definition,
! [X0] :
( sQ103_spl
<=> ( sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,sz00)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1494,definition,
! [X0] :
( sQ105_spl
<=> ( sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,xj)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1497,definition,
( sQ106_spl
<=> sdtlseqdt0(xj,sK0_skl(szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1500,plain,
( ~ sQ17_spl
| ~ sQ106_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1457,f1494,f1497,f543]) ).
fof(f1501,definition,
! [X0] :
( sQ107_spl
<=> ( sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1504,definition,
( sQ108_spl
<=> sdtlseqdt0(xi,sK0_skl(szNzAzT0)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1505,plain,
( ~ sQ108_spl
| sdtlseqdt0(xi,sK0_skl(szNzAzT0)) ),
inference(component_clause,[status(thm)],[f1504]) ).
fof(f1506,plain,
( sQ108_spl
| ~ sdtlseqdt0(xi,sK0_skl(szNzAzT0)) ),
inference(component_clause,[status(thm)],[f1504]) ).
fof(f1507,plain,
( ~ sQ17_spl
| ~ sQ108_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1458,f1501,f1504,f543]) ).
fof(f1535,plain,
! [X0] :
( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(xj,xi)
| ~ sdtlseqdt0(X0,xj)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f548,f371]) ).
fof(f1543,plain,
! [X0,X1] :
( ~ sQ16_spl
| sdtlseqdt0(X1,xi)
| ~ sdtlseqdt0(X1,sK0_skl(szNzAzT0))
| ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f548,f540]) ).
fof(f1544,plain,
! [X0] :
( ~ sQ8_spl
| xi = sK0_skl(szNzAzT0)
| ~ sdtlseqdt0(xi,sK0_skl(szNzAzT0))
| ~ aElementOf0(xi,szNzAzT0)
| ~ sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f548,f491]) ).
fof(f1560,definition,
! [X0] :
( sQ116_spl
<=> ( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(X0,sz00)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1567,definition,
! [X0] :
( sQ118_spl
<=> ( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(X0,xj)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1570,plain,
( ~ sQ0_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1535,f1567,f386]) ).
fof(f1581,definition,
( sQ121_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1583,plain,
( sQ121_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1581]) ).
fof(f1585,definition,
( sQ122_spl
<=> aElementOf0(xj,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1587,plain,
( sQ122_spl
| ~ aElementOf0(xj,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1585]) ).
fof(f1590,definition,
! [X0] :
( sQ123_spl
<=> ( ~ sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( ~ sQ16_spl
| ~ sQ121_spl
| sQ91_spl
| sQ123_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1543,f1194,f1590,f1387,f1581,f539]) ).
fof(f1594,definition,
( sQ124_spl
<=> xi = sK0_skl(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1597,plain,
( ~ sQ8_spl
| sQ124_spl
| ~ sQ108_spl
| ~ sQ121_spl
| sQ123_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1544,f1194,f1590,f1581,f1504,f1594,f490]) ).
fof(f1599,plain,
( sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1583,f372]) ).
fof(f1600,plain,
sQ121_spl,
inference(contradiction_clause,[status(thm)],[f1599]) ).
fof(f1601,plain,
! [X0] :
( sQ92_spl
| ~ sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f1392,f548]) ).
fof(f1602,plain,
( sQ92_spl
| sQ123_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1601,f1194,f1590,f1390]) ).
fof(f1603,plain,
! [X0] :
( ~ sQ17_spl
| sQ108_spl
| ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f1506,f544]) ).
fof(f1604,definition,
! [X0] :
( sQ125_spl
<=> ( ~ sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1607,plain,
( ~ sQ17_spl
| sQ108_spl
| sQ125_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f1603,f1581,f1604,f1504,f543]) ).
fof(f1620,plain,
! [X0] :
( sdtlseqdt0(X0,xi)
| ~ sdtlseqdt0(X0,sz00)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f181,f548]) ).
fof(f1621,plain,
! [X0] :
( ~ sQ17_spl
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ sdtlseqdt0(X0,sz00)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f181,f544]) ).
fof(f1622,plain,
! [X0] :
( ~ sQ16_spl
| sdtlseqdt0(sz00,X0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f181,f540]) ).
fof(f1624,plain,
( ~ sQ39_spl
| sQ116_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f1620,f1581,f1560,f797]) ).
fof(f1625,plain,
( ~ sQ17_spl
| ~ sQ39_spl
| sQ103_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1621,f1194,f1487,f797,f543]) ).
fof(f1626,definition,
! [X0] :
( sQ126_spl
<=> ( sdtlseqdt0(sz00,X0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1629,plain,
( ~ sQ16_spl
| sQ126_spl
| ~ sQ39_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1622,f1194,f797,f1626,f539]) ).
fof(f1634,plain,
! [X0] :
( xk = X0
| xK != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f171]) ).
fof(f1637,definition,
! [X0] :
( sQ128_spl
<=> ( xk = X0
| xK != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1640,plain,
( sQ128_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1634,f699,f1637]) ).
fof(f1655,plain,
( xK = szszuzczcdt0(sK4_skl(xK))
| xK = sz00 ),
inference(resolution,[status(thm)],[f175,f346]) ).
fof(f1658,plain,
( xi = szszuzczcdt0(sK4_skl(xi))
| xi = sz00 ),
inference(resolution,[status(thm)],[f175,f372]) ).
fof(f1671,definition,
( sQ131_spl
<=> xK = szszuzczcdt0(sK4_skl(xK)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1672,plain,
( ~ sQ131_spl
| xK = szszuzczcdt0(sK4_skl(xK)) ),
inference(component_clause,[status(thm)],[f1671]) ).
fof(f1674,plain,
( sQ131_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1655,f1343,f1671]) ).
fof(f1682,definition,
( sQ134_spl
<=> xj = sz00 ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1683,plain,
( ~ sQ134_spl
| xj = sz00 ),
inference(component_clause,[status(thm)],[f1682]) ).
fof(f1684,plain,
( sQ134_spl
| xj != sz00 ),
inference(component_clause,[status(thm)],[f1682]) ).
fof(f1689,definition,
( sQ136_spl
<=> xi = sz00 ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1690,plain,
( ~ sQ136_spl
| xi = sz00 ),
inference(component_clause,[status(thm)],[f1689]) ).
fof(f1692,definition,
( sQ137_spl
<=> xi = szszuzczcdt0(sK4_skl(xi)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1693,plain,
( ~ sQ137_spl
| xi = szszuzczcdt0(sK4_skl(xi)) ),
inference(component_clause,[status(thm)],[f1692]) ).
fof(f1695,plain,
( sQ137_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f1658,f1689,f1692]) ).
fof(f1714,plain,
( ~ sQ136_spl
| ~ aSubsetOf0(sdtlpdtrp0(xN,sz00),sdtlpdtrp0(xN,xj)) ),
inference(backward_demodulation,[status(thm)],[f1690,f379]) ).
fof(f1719,plain,
( ~ sQ136_spl
| ~ aSubsetOf0(xS,sdtlpdtrp0(xN,xj)) ),
inference(forward_demodulation,[status(thm)],[f365,f1714]) ).
fof(f1720,plain,
( ~ sQ136_spl
| ~ sQ134_spl
| ~ aSubsetOf0(xS,sdtlpdtrp0(xN,sz00)) ),
inference(backward_demodulation,[status(thm)],[f1683,f1719]) ).
fof(f1725,plain,
( ~ sQ136_spl
| ~ sQ134_spl
| ~ aSubsetOf0(xS,xS) ),
inference(forward_demodulation,[status(thm)],[f365,f1720]) ).
fof(f1726,plain,
( ~ sQ136_spl
| ~ sQ134_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1725,f652]) ).
fof(f1727,plain,
( ~ sQ136_spl
| ~ sQ134_spl ),
inference(contradiction_clause,[status(thm)],[f1726]) ).
fof(f1796,plain,
! [X0] :
( sdtlseqdt0(xj,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xj,szNzAzT0) ),
inference(resolution,[status(thm)],[f550,f378]) ).
fof(f1797,plain,
! [X0] :
( ~ aElementOf0(xi,szNzAzT0)
| sdtlseqdt0(sz00,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(resolution,[status(thm)],[f550,f181]) ).
fof(f1802,definition,
( sQ143_spl
<=> sdtlseqdt0(xi,xj) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1804,plain,
( sQ143_spl
| ~ sdtlseqdt0(xi,xj) ),
inference(component_clause,[status(thm)],[f1802]) ).
fof(f1821,definition,
! [X0] :
( sQ148_spl
<=> ( sdtlseqdt0(xj,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1822,plain,
! [X0] :
( ~ sQ148_spl
| sdtlseqdt0(xj,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1821]) ).
fof(f1824,plain,
( sQ148_spl
| ~ sQ122_spl ),
inference(split_clause,[status(thm)],[f1796,f1585,f1821]) ).
fof(f1825,definition,
! [X0] :
( sQ149_spl
<=> ( sdtlseqdt0(sz00,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1828,plain,
( ~ sQ121_spl
| sQ149_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1797,f797,f1825,f1581]) ).
fof(f1829,plain,
( sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1587,f371]) ).
fof(f1830,plain,
sQ122_spl,
inference(contradiction_clause,[status(thm)],[f1829]) ).
fof(f1834,plain,
! [X0] :
( sdtlseqdt0(xi,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f461,f550]) ).
fof(f1838,definition,
! [X0] :
( sQ150_spl
<=> ( sdtlseqdt0(xi,X0)
| ~ sdtlseqdt0(xi,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1841,plain,
( sQ150_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f1834,f1581,f1838]) ).
fof(f1842,plain,
( xi = xi
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f551,f461]) ).
fof(f1844,plain,
( xj = xi
| ~ sdtlseqdt0(xi,xj)
| ~ aElementOf0(xj,szNzAzT0) ),
inference(resolution,[status(thm)],[f551,f378]) ).
fof(f1847,definition,
( sQ151_spl
<=> xi = xi ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1850,plain,
( sQ151_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f1842,f1581,f1847]) ).
fof(f1852,definition,
( sQ152_spl
<=> xj = xi ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1853,plain,
( ~ sQ152_spl
| xj = xi ),
inference(component_clause,[status(thm)],[f1852]) ).
fof(f1855,plain,
( sQ152_spl
| ~ sQ143_spl
| ~ sQ122_spl ),
inference(split_clause,[status(thm)],[f1844,f1585,f1802,f1852]) ).
fof(f1867,plain,
! [X0] :
( ~ aElementOf0(xj,szNzAzT0)
| sdtlseqdt0(X0,xj)
| ~ sdtlseqdt0(X0,sz00)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f563,f181]) ).
fof(f1881,definition,
! [X0] :
( sQ155_spl
<=> ( sdtlseqdt0(X0,xj)
| ~ sdtlseqdt0(X0,sz00)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1890,plain,
( ~ sQ122_spl
| ~ sQ39_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f1867,f1881,f797,f1585]) ).
fof(f1917,plain,
( ~ sQ136_spl
| ~ sQ152_spl
| xj = sz00 ),
inference(forward_demodulation,[status(thm)],[f1853,f1690]) ).
fof(f1921,plain,
( sQ134_spl
| ~ sQ136_spl
| ~ sQ152_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f1917,f1684]) ).
fof(f1922,plain,
( sQ134_spl
| ~ sQ136_spl
| ~ sQ152_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1921]) ).
fof(f1923,plain,
( sQ134_spl
| ~ sQ136_spl
| ~ sQ152_spl ),
inference(contradiction_clause,[status(thm)],[f1922]) ).
fof(f1930,plain,
! [X0] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sdtlseqdt0(szszuzczcdt0(sK0_skl(szNzAzT0)),X0)
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f197,f104]) ).
fof(f1932,definition,
! [X0] :
( sQ158_spl
<=> ( sdtlseqdt0(szszuzczcdt0(sK0_skl(szNzAzT0)),X0)
| sdtlseqdt0(X0,sK0_skl(szNzAzT0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f1935,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f1930,f1932,f466,f469]) ).
fof(f1992,definition,
( sQ165_spl
<=> sdtlseqdt0(xK,sz00) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f2049,plain,
( iLess0(xk,xK)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f201]) ).
fof(f2050,plain,
( sdtlseqdt0(xk,xK)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f189]) ).
fof(f2051,plain,
! [X0] :
( ~ sdtlseqdt0(szszuzczcdt0(X0),xK)
| sdtlseqdt0(X0,xk)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f187]) ).
fof(f2052,plain,
! [X0] :
( ~ sdtlseqdt0(xK,szszuzczcdt0(X0))
| sdtlseqdt0(xk,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f187]) ).
fof(f2053,plain,
! [X0] :
( sdtlseqdt0(szszuzczcdt0(X0),xK)
| ~ sdtlseqdt0(X0,xk)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f186]) ).
fof(f2054,plain,
! [X0] :
( sdtlseqdt0(xK,szszuzczcdt0(X0))
| ~ sdtlseqdt0(xk,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f361,f186]) ).
fof(f2062,definition,
( sQ168_spl
<=> iLess0(xk,xK) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f2065,plain,
( sQ168_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f2049,f699,f2062]) ).
fof(f2066,definition,
( sQ169_spl
<=> sdtlseqdt0(xk,xK) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( sQ169_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f2050,f699,f2066]) ).
fof(f2070,definition,
! [X0] :
( sQ170_spl
<=> ( ~ sdtlseqdt0(szszuzczcdt0(X0),xK)
| sdtlseqdt0(X0,xk)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f2073,plain,
( ~ sQ30_spl
| sQ170_spl ),
inference(split_clause,[status(thm)],[f2051,f2070,f699]) ).
fof(f2074,definition,
! [X0] :
( sQ171_spl
<=> ( ~ sdtlseqdt0(xK,szszuzczcdt0(X0))
| sdtlseqdt0(xk,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f2077,plain,
( sQ171_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f2052,f699,f2074]) ).
fof(f2078,definition,
! [X0] :
( sQ172_spl
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xK)
| ~ sdtlseqdt0(X0,xk)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f2081,plain,
( ~ sQ30_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f2053,f2078,f699]) ).
fof(f2082,definition,
! [X0] :
( sQ173_spl
<=> ( sdtlseqdt0(xK,szszuzczcdt0(X0))
| ~ sdtlseqdt0(xk,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f2085,plain,
( sQ173_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f2054,f699,f2082]) ).
fof(f2106,plain,
sbrdtbr0(slcrc0) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f408,f396]) ).
fof(f2111,plain,
( aElement0(sz00)
| ~ aSet0(slcrc0) ),
inference(paramodulation,[status(thm)],[f2106,f203]) ).
fof(f2116,definition,
( sQ174_spl
<=> aElement0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f2119,plain,
( sQ174_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2111,f449,f2116]) ).
fof(f2122,plain,
! [X0] :
( sbrdtbr0(sdtpldt0(slcrc0,X0)) = szszuzczcdt0(sbrdtbr0(slcrc0))
| aElementOf0(X0,slcrc0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f213,f105]) ).
fof(f2133,definition,
! [X0] :
( sQ175_spl
<=> ( sbrdtbr0(sdtpldt0(slcrc0,X0)) = szszuzczcdt0(sbrdtbr0(slcrc0))
| aElementOf0(X0,slcrc0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f2136,plain,
( sQ175_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2122,f449,f2133]) ).
fof(f2142,plain,
! [X0] :
( szszuzczcdt0(sbrdtbr0(sdtmndt0(slcrc0,X0))) = sbrdtbr0(slcrc0)
| ~ aElementOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f215,f105]) ).
fof(f2146,definition,
! [X0] :
( sQ176_spl
<=> ( szszuzczcdt0(sbrdtbr0(sdtmndt0(slcrc0,X0))) = sbrdtbr0(slcrc0)
| ~ aElementOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f2149,plain,
( sQ176_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2142,f449,f2146]) ).
fof(f2153,plain,
( ~ sQ148_spl
| ~ aElementOf0(xi,szNzAzT0)
| sdtlseqdt0(xj,szszuzczcdt0(xi))
| ~ aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
inference(resolution,[status(thm)],[f1822,f189]) ).
fof(f2155,definition,
( sQ177_spl
<=> aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f2156,plain,
( ~ sQ177_spl
| aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
inference(component_clause,[status(thm)],[f2155]) ).
fof(f2157,plain,
( sQ177_spl
| ~ aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
inference(component_clause,[status(thm)],[f2155]) ).
fof(f2158,definition,
( sQ178_spl
<=> sdtlseqdt0(xj,szszuzczcdt0(xi)) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f2161,plain,
( ~ sQ148_spl
| ~ sQ121_spl
| sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f2153,f2155,f2158,f1581,f1821]) ).
fof(f2196,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,slcrc0)
| ~ aSet0(slcrc0)
| isFinite0(X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f597,f105]) ).
fof(f2200,definition,
! [X0,X1] :
( sQ179_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| isFinite0(X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f2203,plain,
( ~ sQ4_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f2196,f2200,f449]) ).
fof(f2219,plain,
( ~ sQ131_spl
| iLess0(sK4_skl(xK),xK)
| ~ aElementOf0(sK4_skl(xK),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f201]) ).
fof(f2220,plain,
( ~ sQ131_spl
| sdtlseqdt0(sK4_skl(xK),xK)
| ~ aElementOf0(sK4_skl(xK),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f189]) ).
fof(f2221,plain,
! [X0] :
( ~ sQ131_spl
| ~ sdtlseqdt0(szszuzczcdt0(X0),xK)
| sdtlseqdt0(X0,sK4_skl(xK))
| ~ aElementOf0(sK4_skl(xK),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f187]) ).
fof(f2222,plain,
! [X0] :
( ~ sQ131_spl
| ~ sdtlseqdt0(xK,szszuzczcdt0(X0))
| sdtlseqdt0(sK4_skl(xK),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK4_skl(xK),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f187]) ).
fof(f2223,plain,
! [X0] :
( ~ sQ131_spl
| sdtlseqdt0(szszuzczcdt0(X0),xK)
| ~ sdtlseqdt0(X0,sK4_skl(xK))
| ~ aElementOf0(sK4_skl(xK),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f186]) ).
fof(f2224,plain,
! [X0] :
( ~ sQ131_spl
| sdtlseqdt0(xK,szszuzczcdt0(X0))
| ~ sdtlseqdt0(sK4_skl(xK),X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(sK4_skl(xK),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f186]) ).
fof(f2225,plain,
( ~ sQ131_spl
| ~ sdtlseqdt0(xK,sz00)
| ~ aElementOf0(sK4_skl(xK),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f183]) ).
fof(f2226,plain,
! [X0] :
( ~ sQ131_spl
| X0 = sK4_skl(xK)
| szszuzczcdt0(X0) != xK
| ~ aElementOf0(sK4_skl(xK),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1672,f171]) ).
fof(f2231,definition,
( sQ180_spl
<=> aElementOf0(sK4_skl(xK),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f2233,plain,
( sQ180_spl
| ~ aElementOf0(sK4_skl(xK),szNzAzT0) ),
inference(component_clause,[status(thm)],[f2231]) ).
fof(f2235,definition,
( sQ181_spl
<=> iLess0(sK4_skl(xK),xK) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f2238,plain,
( ~ sQ131_spl
| sQ181_spl
| ~ sQ180_spl ),
inference(split_clause,[status(thm)],[f2219,f2231,f2235,f1671]) ).
fof(f2239,definition,
( sQ182_spl
<=> sdtlseqdt0(sK4_skl(xK),xK) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2242,plain,
( ~ sQ131_spl
| sQ182_spl
| ~ sQ180_spl ),
inference(split_clause,[status(thm)],[f2220,f2231,f2239,f1671]) ).
fof(f2243,definition,
! [X0] :
( sQ183_spl
<=> ( ~ sdtlseqdt0(szszuzczcdt0(X0),xK)
| sdtlseqdt0(X0,sK4_skl(xK))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f2246,plain,
( ~ sQ131_spl
| ~ sQ180_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f2221,f2243,f2231,f1671]) ).
fof(f2247,definition,
! [X0] :
( sQ184_spl
<=> ( ~ sdtlseqdt0(xK,szszuzczcdt0(X0))
| sdtlseqdt0(sK4_skl(xK),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f2250,plain,
( ~ sQ131_spl
| sQ184_spl
| ~ sQ180_spl ),
inference(split_clause,[status(thm)],[f2222,f2231,f2247,f1671]) ).
fof(f2251,definition,
! [X0] :
( sQ185_spl
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xK)
| ~ sdtlseqdt0(X0,sK4_skl(xK))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2254,plain,
( ~ sQ131_spl
| ~ sQ180_spl
| sQ185_spl ),
inference(split_clause,[status(thm)],[f2223,f2251,f2231,f1671]) ).
fof(f2255,definition,
! [X0] :
( sQ186_spl
<=> ( sdtlseqdt0(xK,szszuzczcdt0(X0))
| ~ sdtlseqdt0(sK4_skl(xK),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f2258,plain,
( ~ sQ131_spl
| sQ186_spl
| ~ sQ180_spl ),
inference(split_clause,[status(thm)],[f2224,f2231,f2255,f1671]) ).
fof(f2259,plain,
( ~ sQ131_spl
| ~ sQ165_spl
| ~ sQ180_spl ),
inference(split_clause,[status(thm)],[f2225,f2231,f1992,f1671]) ).
fof(f2260,definition,
! [X0] :
( sQ187_spl
<=> ( X0 = sK4_skl(xK)
| szszuzczcdt0(X0) != xK
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f2263,plain,
( ~ sQ131_spl
| ~ sQ180_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f2226,f2260,f2231,f1671]) ).
fof(f2281,plain,
! [X0] :
( sdtlseqdt0(sbrdtbr0(X0),sz00)
| ~ aSubsetOf0(X0,slcrc0)
| ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(paramodulation,[status(thm)],[f2106,f217]) ).
fof(f2283,definition,
! [X0] :
( sQ188_spl
<=> ( sdtlseqdt0(sbrdtbr0(X0),sz00)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2286,plain,
( sQ188_spl
| ~ sQ48_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2281,f449,f861,f2283]) ).
fof(f2297,plain,
! [X0] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| aSubsetOf0(sK5_skl(sK0_skl(szNzAzT0),X0),X0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f220,f104]) ).
fof(f2301,plain,
! [X0] :
( aSubsetOf0(sK5_skl(X0,slcrc0),slcrc0)
| ~ sdtlseqdt0(X0,sbrdtbr0(slcrc0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f220,f105]) ).
fof(f2303,definition,
! [X0] :
( sQ189_spl
<=> ( aSubsetOf0(sK5_skl(sK0_skl(szNzAzT0),X0),X0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2306,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f2297,f2303,f466,f469]) ).
fof(f2309,definition,
! [X0] :
( sQ190_spl
<=> ( aSubsetOf0(sK5_skl(X0,slcrc0),slcrc0)
| ~ sdtlseqdt0(X0,sbrdtbr0(slcrc0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2312,plain,
( sQ190_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2301,f449,f2309]) ).
fof(f2325,plain,
! [X0] :
( ~ aSet0(szNzAzT0)
| szNzAzT0 = slcrc0
| sbrdtbr0(sK5_skl(sK0_skl(szNzAzT0),X0)) = sK0_skl(szNzAzT0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f221,f104]) ).
fof(f2329,plain,
! [X0] :
( sbrdtbr0(sK5_skl(X0,slcrc0)) = X0
| ~ sdtlseqdt0(X0,sbrdtbr0(slcrc0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f221,f105]) ).
fof(f2331,definition,
! [X0] :
( sQ191_spl
<=> ( sbrdtbr0(sK5_skl(sK0_skl(szNzAzT0),X0)) = sK0_skl(szNzAzT0)
| ~ sdtlseqdt0(sK0_skl(szNzAzT0),sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f2334,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f2325,f2331,f466,f469]) ).
fof(f2337,definition,
! [X0] :
( sQ192_spl
<=> ( sbrdtbr0(sK5_skl(X0,slcrc0)) = X0
| ~ sdtlseqdt0(X0,sbrdtbr0(slcrc0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2340,plain,
( sQ192_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2329,f449,f2337]) ).
fof(f2343,plain,
( sQ177_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f2157,f168]) ).
fof(f2345,plain,
( sQ177_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f2343,f1581,f2155]) ).
fof(f2346,plain,
! [X0] :
( ~ sQ177_spl
| sbrdtbr0(sK5_skl(szszuzczcdt0(xi),X0)) = szszuzczcdt0(xi)
| ~ sdtlseqdt0(szszuzczcdt0(xi),sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f2156,f221]) ).
fof(f2349,plain,
( ~ sQ177_spl
| szszuzczcdt0(xi) = szszuzczcdt0(sK4_skl(szszuzczcdt0(xi)))
| szszuzczcdt0(xi) = sz00 ),
inference(resolution,[status(thm)],[f2156,f175]) ).
fof(f2352,plain,
! [X0] :
( ~ sQ177_spl
| sdtlseqdt0(X0,szszuzczcdt0(xi))
| ~ sdtlseqdt0(szszuzczcdt0(xi),szszuzczcdt0(xi))
| ~ sdtlseqdt0(X0,szszuzczcdt0(xi))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f2156,f195]) ).
fof(f2357,definition,
( sQ193_spl
<=> szszuzczcdt0(xi) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f2358,plain,
( ~ sQ193_spl
| szszuzczcdt0(xi) = sz00 ),
inference(component_clause,[status(thm)],[f2357]) ).
fof(f2360,definition,
( sQ194_spl
<=> szszuzczcdt0(xi) = szszuzczcdt0(sK4_skl(szszuzczcdt0(xi))) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2363,plain,
( ~ sQ177_spl
| sQ194_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f2349,f2357,f2360,f2155]) ).
fof(f2364,definition,
! [X0] :
( sQ195_spl
<=> ( sdtlseqdt0(X0,szszuzczcdt0(xi))
| ~ sdtlseqdt0(X0,szszuzczcdt0(xi))
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f2367,definition,
( sQ196_spl
<=> sdtlseqdt0(szszuzczcdt0(xi),szszuzczcdt0(xi)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2370,plain,
( ~ sQ177_spl
| ~ sQ196_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f2352,f2364,f2367,f2155]) ).
fof(f2375,plain,
( ~ sQ193_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f2358,f169]) ).
fof(f2389,plain,
( ~ sQ193_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f2375,f1581,f2357]) ).
fof(f2424,plain,
( ~ sQ148_spl
| ~ sQ108_spl
| sdtlseqdt0(xj,sK0_skl(szNzAzT0))
| ~ aElementOf0(sK0_skl(szNzAzT0),szNzAzT0) ),
inference(resolution,[status(thm)],[f1505,f1822]) ).
fof(f2425,plain,
( ~ sQ148_spl
| ~ sQ108_spl
| sQ106_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f2424,f1194,f1497,f1504,f1821]) ).
fof(f2442,plain,
( ~ sQ1_spl
| ~ sQ137_spl
| ~ aElementOf0(sK4_skl(xi),szNzAzT0) ),
inference(resolution,[status(thm)],[f1693,f390]) ).
fof(f2443,plain,
( ~ sQ137_spl
| ~ sQ1_spl
| xi != xi
| ~ aElementOf0(sK4_skl(xi),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f1693,f390]) ).
fof(f2456,definition,
( sQ204_spl
<=> aElementOf0(sK4_skl(xi),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f2459,plain,
( ~ sQ137_spl
| ~ sQ1_spl
| ~ sQ151_spl
| ~ sQ204_spl ),
inference(split_clause,[status(thm)],[f2443,f2456,f1847,f389,f1692]) ).
fof(f2611,plain,
( sQ180_spl
| xK = sz00
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolution,[status(thm)],[f2233,f174]) ).
fof(f2613,plain,
( sQ180_spl
| sQ82_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f2611,f783,f1343,f2231]) ).
fof(f2614,plain,
( aElementOf0(szmzizndt0(xS),xS)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f409,f347]) ).
fof(f2616,plain,
( aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0)
| szNzAzT0 = slcrc0 ),
inference(resolution,[status(thm)],[f409,f441]) ).
fof(f2620,definition,
( sQ234_spl
<=> aElementOf0(szmzizndt0(xS),xS) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f2623,plain,
( sQ234_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2614,f916,f2620]) ).
fof(f2624,definition,
( sQ235_spl
<=> aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f2627,plain,
( sQ235_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f2616,f466,f2624]) ).
fof(f2628,definition,
( sQ236_spl
<=> aElementOf0(szmzizndt0(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f2629,plain,
( ~ sQ236_spl
| aElementOf0(szmzizndt0(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f2628]) ).
fof(f2634,plain,
( ~ sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2629,f397]) ).
fof(f2635,plain,
~ sQ236_spl,
inference(contradiction_clause,[status(thm)],[f2634]) ).
fof(f2636,plain,
! [X0] :
( sdtlseqdt0(szmzizndt0(xS),X0)
| ~ aElementOf0(X0,xS)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f410,f347]) ).
fof(f2638,plain,
! [X0] :
( sdtlseqdt0(szmzizndt0(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0)
| szNzAzT0 = slcrc0 ),
inference(resolution,[status(thm)],[f410,f441]) ).
fof(f2642,definition,
! [X0] :
( sQ237_spl
<=> ( sdtlseqdt0(szmzizndt0(xS),X0)
| ~ aElementOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f2645,plain,
( sQ237_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2636,f916,f2642]) ).
fof(f2646,definition,
! [X0] :
( sQ238_spl
<=> ( sdtlseqdt0(szmzizndt0(szNzAzT0),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f2649,plain,
( sQ238_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f2638,f466,f2646]) ).
fof(f2655,plain,
! [X0] :
( aElementOf0(sK6_skl(X0,xS),xS)
| ~ aElementOf0(X0,xS)
| X0 = szmzizndt0(xS)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f228,f347]) ).
fof(f2657,plain,
! [X0] :
( aElementOf0(sK6_skl(X0,szNzAzT0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| X0 = szmzizndt0(szNzAzT0)
| szNzAzT0 = slcrc0 ),
inference(resolution,[status(thm)],[f228,f441]) ).
fof(f2661,definition,
! [X0] :
( sQ240_spl
<=> ( aElementOf0(sK6_skl(X0,xS),xS)
| ~ aElementOf0(X0,xS)
| X0 = szmzizndt0(xS) ) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f2664,plain,
( sQ240_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2655,f916,f2661]) ).
fof(f2665,definition,
! [X0] :
( sQ241_spl
<=> ( aElementOf0(sK6_skl(X0,szNzAzT0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| X0 = szmzizndt0(szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f2668,plain,
( sQ241_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f2657,f466,f2665]) ).
fof(f2688,plain,
( ~ sQ177_spl
| sbrdtbr0(sK5_skl(szszuzczcdt0(xi),slcrc0)) = szszuzczcdt0(xi)
| ~ sdtlseqdt0(szszuzczcdt0(xi),sz00)
| ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(paramodulation,[status(thm)],[f2106,f2346]) ).
fof(f2689,definition,
( sQ243_spl
<=> sdtlseqdt0(szszuzczcdt0(xi),sz00) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f2692,definition,
( sQ244_spl
<=> sbrdtbr0(sK5_skl(szszuzczcdt0(xi),slcrc0)) = szszuzczcdt0(xi) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f2695,plain,
( ~ sQ177_spl
| sQ244_spl
| ~ sQ243_spl
| ~ sQ48_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2688,f449,f861,f2689,f2692,f2155]) ).
fof(f2696,plain,
( ~ sQ1_spl
| ~ sQ137_spl
| xi = sz00
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f2442,f174]) ).
fof(f2698,plain,
( ~ sQ1_spl
| ~ sQ137_spl
| sQ136_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f2696,f1581,f1689,f1692,f389]) ).
fof(f2705,plain,
( sQ143_spl
| ~ sQ136_spl
| ~ sdtlseqdt0(sz00,xj) ),
inference(backward_demodulation,[status(thm)],[f1690,f1804]) ).
fof(f2724,plain,
( sQ143_spl
| ~ sQ136_spl
| ~ aElementOf0(xj,szNzAzT0) ),
inference(resolution,[status(thm)],[f2705,f181]) ).
fof(f2725,plain,
( sQ143_spl
| ~ sQ136_spl
| ~ sQ122_spl ),
inference(split_clause,[status(thm)],[f2724,f1585,f1689,f1802]) ).
fof(f2726,plain,
$false,
inference(sat_refutation,[status(thm)],[f395,f452,f454,f472,f474,f484,f493,f505,f512,f519,f523,f525,f538,f542,f546,f558,f561,f573,f576,f592,f596,f620,f622,f653,f705,f709,f711,f763,f773,f777,f779,f786,f788,f803,f807,f814,f816,f819,f847,f848,f852,f857,f864,f919,f927,f929,f955,f970,f972,f1057,f1061,f1101,f1138,f1200,f1216,f1220,f1224,f1247,f1254,f1276,f1280,f1299,f1326,f1346,f1407,f1422,f1430,f1445,f1452,f1500,f1507,f1570,f1593,f1597,f1600,f1602,f1607,f1624,f1625,f1629,f1640,f1674,f1695,f1727,f1824,f1828,f1830,f1841,f1850,f1855,f1890,f1923,f1935,f2065,f2069,f2073,f2077,f2081,f2085,f2119,f2136,f2149,f2161,f2203,f2238,f2242,f2246,f2250,f2254,f2258,f2259,f2263,f2286,f2306,f2312,f2334,f2340,f2345,f2363,f2370,f2389,f2425,f2459,f2613,f2623,f2627,f2635,f2645,f2649,f2664,f2668,f2695,f2698,f2725]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM574+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n006.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 02:41:13 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.13/0.57 % Drodi V4.1.1
% 0.13/0.67 % Refutation found
% 0.13/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.70 % Elapsed time: 0.138264 seconds
% 0.13/0.70 % CPU time: 0.828725 seconds
% 0.13/0.70 % Total memory used: 122.414 MB
% 0.13/0.70 % Net memory used: 121.374 MB
%------------------------------------------------------------------------------