%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM534+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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:40:53 PM UTC 2026
% Result : Theorem 0.14s 0.50s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 158
% Syntax : Number of formulae : 630 ( 16 unt; 152 def)
% Number of atoms : 2487 ( 152 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 3596 (1739 ~;1607 |; 79 &)
% ( 162 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 154 ( 152 usr; 148 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 742 ( 733 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(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(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [W0,W1,W2] :
( ( aSet0(W2)
& aSet0(W1)
& aSet0(W0) )
=> ( ( aSubsetOf0(W1,W2)
& aSubsetOf0(W0,W1) )
=> aSubsetOf0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,definition,
! [W0,W1] :
( ( aElement0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtpldt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,definition,
! [W0,W1] :
( ( aElement0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
aSet0(xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
aElementOf0(xx,xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
sdtpldt0(sdtmndt0(xS,xx),xx) = xS,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
sdtpldt0(sdtmndt0(xS,xx),xx) != xS,
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f27,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f28,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f31,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f32,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f33,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f34,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))],[f33]) ).
fof(f35,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f37,plain,
! [X0] :
( aElementOf0(sK0_skl(X0),X0)
| ~ aSet0(X0)
| X0 = slcrc0 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f45,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(f46,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)],[f45]) ).
fof(f47,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)],[f46]) ).
fof(f48,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))],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f51,plain,
! [X0,X1] :
( aElementOf0(sK1_skl(X1,X0),X1)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f52,plain,
! [X0,X1] :
( ~ aElementOf0(sK1_skl(X1,X0),X0)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f55,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f56,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f59,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(f60,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtpldt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) ) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f62,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) )
| aElementOf0(W3,W2) )
& ( ( W3 != W1
& ~ aElementOf0(W3,W0) )
| ~ aElement0(W3)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtpldt0(W0,W1) )
& ( ( ! [W3] :
( ( ( W3 != W1
& ~ aElementOf0(W3,W0) )
| ~ aElement0(W3)
| aElementOf0(W3,W2) )
& ( ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtpldt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) )
| aElementOf0(W3,W2) )
& ( ( W3 != W1
& ~ aElementOf0(W3,W0) )
| ~ aElement0(W3)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtpldt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ( W3 != W1
& ~ aElementOf0(W3,W0) )
| ~ aElement0(W3)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtpldt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f62]) ).
fof(f64,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( ( ( sK2_skl(W2,W1,W0) = W1
| aElementOf0(sK2_skl(W2,W1,W0),W0) )
& aElement0(sK2_skl(W2,W1,W0)) )
| aElementOf0(sK2_skl(W2,W1,W0),W2) )
& ( ( sK2_skl(W2,W1,W0) != W1
& ~ aElementOf0(sK2_skl(W2,W1,W0),W0) )
| ~ aElement0(sK2_skl(W2,W1,W0))
| ~ aElementOf0(sK2_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtpldt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ( W3 != W1
& ~ aElementOf0(W3,W0) )
| ~ aElement0(W3)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtpldt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( aElement0(X3)
| ~ aElementOf0(X3,X2)
| X2 != sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| aElementOf0(X3,X0)
| ~ aElementOf0(X3,X2)
| X2 != sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( ~ aElementOf0(X3,X0)
| ~ aElement0(X3)
| aElementOf0(X3,X2)
| X2 != sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f69,plain,
! [X0,X1,X2,X3] :
( X3 != X1
| ~ aElement0(X3)
| aElementOf0(X3,X2)
| X2 != sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ aElementOf0(sK2_skl(X2,X1,X0),X0)
| ~ aElement0(sK2_skl(X2,X1,X0))
| ~ aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f71,plain,
! [X0,X1,X2] :
( sK2_skl(X2,X1,X0) != X1
| ~ aElement0(sK2_skl(X2,X1,X0))
| ~ aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f72,plain,
! [X0,X1,X2] :
( aElement0(sK2_skl(X2,X1,X0))
| aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f73,plain,
! [X0,X1,X2] :
( sK2_skl(X2,X1,X0) = X1
| aElementOf0(sK2_skl(X2,X1,X0),X0)
| aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f74,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f75,definition,
! [W0,W1,W3] :
( sP0_prd(W3,W1,W0)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f76,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> sP0_prd(W3,W1,W0) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(formula_renaming,[status(thm)],[f74,f75]) ).
fof(f77,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ~ sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ( ( ! [W3] :
( ( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ~ sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( sP0_prd(sK3_skl(W2,W1,W0),W1,W0)
| aElementOf0(sK3_skl(W2,W1,W0),W2) )
& ( ~ sP0_prd(sK3_skl(W2,W1,W0),W1,W0)
| ~ aElementOf0(sK3_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X3,X1,X0)
| ~ aElementOf0(X3,X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ~ sP0_prd(X3,X1,X0)
| aElementOf0(X3,X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f84,plain,
! [X0,X1,X2] :
( sP0_prd(sK3_skl(X2,X1,X0),X1,X0)
| aElementOf0(sK3_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f85,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f86,plain,
aElementOf0(xx,xS),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f87,plain,
sdtpldt0(sdtmndt0(xS,xx),xx) != xS,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f88,plain,
! [W0,W1,W3] :
( ( W3 = W1
| ~ aElementOf0(W3,W0)
| ~ aElement0(W3)
| sP0_prd(W3,W1,W0) )
& ( ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) )
| ~ sP0_prd(W3,W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f75]) ).
fof(f89,plain,
( ! [W0,W1,W3] :
( W3 = W1
| ~ aElementOf0(W3,W0)
| ~ aElement0(W3)
| sP0_prd(W3,W1,W0) )
& ! [W0,W1,W3] :
( ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) )
| ~ sP0_prd(W3,W1,W0) ) ),
inference(miniscoping,[status(thm)],[f88]) ).
fof(f91,plain,
! [X0,X1,X2] :
( aElementOf0(X0,X2)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f92,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f93,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ aElementOf0(X0,X2)
| ~ aElement0(X0)
| sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f94,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f35]) ).
fof(f95,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f36]) ).
fof(f97,plain,
! [X0,X1] :
( aSet0(sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f65]) ).
fof(f98,plain,
! [X0,X1,X2] :
( aElement0(X2)
| ~ aElementOf0(X2,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f66]) ).
fof(f99,plain,
! [X0,X1,X2] :
( X2 = X1
| aElementOf0(X2,X0)
| ~ aElementOf0(X2,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f67]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ aElementOf0(X2,X0)
| ~ aElement0(X2)
| aElementOf0(X2,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f68]) ).
fof(f101,plain,
! [X0,X1] :
( ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f69]) ).
fof(f102,plain,
! [X0,X1] :
( aElementOf0(X1,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1] :
( aSet0(sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f80]) ).
fof(f104,plain,
! [X0,X1,X2] :
( sP0_prd(X2,X1,X0)
| ~ aElementOf0(X2,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f81]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X2,X1,X0)
| aElementOf0(X2,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f82]) ).
fof(f106,plain,
! [X0,X1] : ~ sP0_prd(X0,X0,X1),
inference(destructive_equality_resolution,[status(thm)],[f92]) ).
fof(f108,definition,
( sQ0_spl
<=> aSet0(sdtmndt0(xS,xx)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f110,plain,
( sQ0_spl
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f111,definition,
( sQ1_spl
<=> aElement0(xx) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f113,plain,
( sQ1_spl
| ~ aElement0(xx) ),
inference(component_clause,[status(thm)],[f111]) ).
fof(f114,definition,
( sQ2_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f116,plain,
( sQ2_spl
| ~ aSet0(xS) ),
inference(component_clause,[status(thm)],[f114]) ).
fof(f117,definition,
( sQ3_spl
<=> aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xS) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f119,plain,
( sQ3_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xS) ),
inference(component_clause,[status(thm)],[f117]) ).
fof(f120,definition,
( sQ4_spl
<=> aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f121,plain,
( ~ sQ4_spl
| aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx))) ),
inference(component_clause,[status(thm)],[f120]) ).
fof(f122,plain,
( sQ4_spl
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx))) ),
inference(component_clause,[status(thm)],[f120]) ).
fof(f123,definition,
( sQ5_spl
<=> aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f124,plain,
( ~ sQ5_spl
| aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx)) ),
inference(component_clause,[status(thm)],[f123]) ).
fof(f125,plain,
( sQ5_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx)) ),
inference(component_clause,[status(thm)],[f123]) ).
fof(f127,plain,
! [X0,X1] :
( X1 = X0
| ~ aElementOf0(X1,sdtpldt0(slcrc0,X0))
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f95,f99]) ).
fof(f128,definition,
( sQ6_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f130,plain,
( sQ6_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f128]) ).
fof(f131,definition,
! [X0,X1] :
( sQ7_spl
<=> ( X1 = X0
| ~ aElementOf0(X1,sdtpldt0(slcrc0,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f132,plain,
! [X0,X1] :
( ~ sQ7_spl
| X1 = X0
| ~ aElementOf0(X1,sdtpldt0(slcrc0,X0))
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f131]) ).
fof(f134,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f127,f128,f131]) ).
fof(f135,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f130,f94]) ).
fof(f136,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f106,f104]) ).
fof(f139,plain,
! [X0,X1] : ~ sP0_prd(X0,X1,slcrc0),
inference(resolution,[status(thm)],[f91,f95]) ).
fof(f140,plain,
! [X0,X1,X2] :
( ~ aElementOf0(sK2_skl(X2,X1,X0),X0)
| ~ aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f70,f28]) ).
fof(f141,plain,
! [X0,X1,X2] :
( ~ aElementOf0(X2,X0)
| aElementOf0(X2,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f100,f28]) ).
fof(f142,plain,
( ~ aSet0(slcrc0)
| slcrc0 = slcrc0 ),
inference(resolution,[status(thm)],[f37,f95]) ).
fof(f143,definition,
( sQ8_spl
<=> slcrc0 = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f146,plain,
( ~ sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f142,f143,f128]) ).
fof(f147,plain,
( sQ5_spl
| ~ sP0_prd(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xx,xS)
| ~ aElement0(xx)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f125,f105]) ).
fof(f149,plain,
! [X0] :
( sQ5_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = X0
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtmndt0(xS,xx),X0))
| ~ aElement0(X0)
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f125,f99]) ).
fof(f150,definition,
( sQ9_spl
<=> sP0_prd(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xx,xS) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( ~ sQ9_spl
| sP0_prd(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xx,xS) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f152,plain,
( sQ9_spl
| ~ sP0_prd(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xx,xS) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f153,plain,
( sQ5_spl
| ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f147,f114,f111,f150,f123]) ).
fof(f154,definition,
! [X0] :
( sQ10_spl
<=> ( sK2_skl(xS,xx,sdtmndt0(xS,xx)) = X0
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtmndt0(xS,xx),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( sQ5_spl
| sQ10_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f149,f108,f154,f123]) ).
fof(f158,plain,
! [X0] :
( sQ1_spl
| ~ aElementOf0(xx,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f113,f28]) ).
fof(f162,plain,
( sQ0_spl
| ~ aElement0(xx)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f110,f103]) ).
fof(f164,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f162,f114,f111,f108]) ).
fof(f165,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f116,f85]) ).
fof(f166,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f165]) ).
fof(f167,plain,
( sQ1_spl
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f158,f86]) ).
fof(f172,plain,
( sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f167,f114,f111]) ).
fof(f178,plain,
( ~ sQ7_spl
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(slcrc0,xS))
| ~ aElement0(xS) ),
inference(resolution,[status(thm)],[f132,f87]) ).
fof(f179,plain,
( ~ sQ7_spl
| ~ aElementOf0(xS,sdtpldt0(slcrc0,sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aElement0(sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(resolution,[status(thm)],[f132,f87]) ).
fof(f180,definition,
( sQ12_spl
<=> aElement0(xS) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( sQ12_spl
| ~ aElement0(xS) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,definition,
( sQ13_spl
<=> aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(slcrc0,xS)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( sQ13_spl
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(slcrc0,xS)) ),
inference(component_clause,[status(thm)],[f183]) ).
fof(f186,plain,
( ~ sQ7_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f178,f180,f183,f131]) ).
fof(f187,definition,
( sQ14_spl
<=> aElement0(sdtpldt0(sdtmndt0(xS,xx),xx)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f190,definition,
( sQ15_spl
<=> aElementOf0(xS,sdtpldt0(slcrc0,sdtpldt0(sdtmndt0(xS,xx),xx))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( ~ sQ7_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f179,f187,f190,f131]) ).
fof(f196,plain,
! [X0,X1] :
( sQ12_spl
| ~ aElementOf0(xS,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f182,f98]) ).
fof(f198,plain,
! [X0,X1,X2] :
( sK2_skl(X2,X1,X0) != X1
| ~ aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f71,f28]) ).
fof(f199,plain,
( sK2_skl(xS,xx,sdtmndt0(xS,xx)) != xx
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xS)
| ~ aSet0(xS)
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f198,f87]) ).
fof(f200,definition,
( sQ16_spl
<=> sK2_skl(xS,xx,sdtmndt0(xS,xx)) = xx ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f201,plain,
( ~ sQ16_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = xx ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f202,plain,
( sQ16_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) != xx ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f203,plain,
( ~ sQ16_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f199,f108,f111,f114,f117,f200]) ).
fof(f204,plain,
! [X0,X1,X2] :
( aElement0(sK2_skl(X2,X1,X0))
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f72,f28]) ).
fof(f205,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtmndt0(slcrc0,X0))
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f139,f104]) ).
fof(f206,definition,
! [X0,X1] :
( sQ17_spl
<=> ( ~ aElementOf0(X1,sdtmndt0(slcrc0,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f207,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ aElementOf0(X1,sdtmndt0(slcrc0,X0))
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f206]) ).
fof(f209,plain,
( sQ17_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f205,f128,f206]) ).
fof(f214,definition,
! [X0] :
( sQ18_spl
<=> ( ~ aSet0(X0)
| ~ aSet0(sdtpldt0(X0,xS)) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f220,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ sP0_prd(X1,X0,slcrc0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f207,f105]) ).
fof(f223,definition,
! [X0,X1] :
( sQ19_spl
<=> ( ~ sP0_prd(X1,X0,slcrc0)
| ~ aElement0(X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f226,plain,
( ~ sQ17_spl
| ~ sQ6_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f220,f223,f128,f206]) ).
fof(f234,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ aElementOf0(X1,sdtpldt0(sdtmndt0(X0,X1),X2))
| ~ aElement0(X2)
| ~ aSet0(sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f137,f99]) ).
fof(f237,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ aElementOf0(X1,sdtpldt0(sdtmndt0(X0,X1),X2))
| ~ aElement0(X2)
| ~ aSet0(sdtmndt0(X0,X1))
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f234,f98]) ).
fof(f247,definition,
! [X1] :
( sQ21_spl
<=> xS = X1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f254,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f50,f95]) ).
fof(f257,definition,
! [X0,X1] :
( sQ22_spl
<=> ( ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f258,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aElementOf0(X1,X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(component_clause,[status(thm)],[f257]) ).
fof(f260,plain,
( sQ22_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f254,f128,f257]) ).
fof(f262,plain,
! [X0] :
( ~ aSet0(slcrc0)
| aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f51,f95]) ).
fof(f263,definition,
! [X0] :
( sQ23_spl
<=> ( aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f264,plain,
! [X0] :
( ~ sQ23_spl
| aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,plain,
( ~ sQ6_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f262,f263,f128]) ).
fof(f275,definition,
! [X0] :
( sQ24_spl
<=> ( ~ aSet0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f276,plain,
! [X0] :
( ~ sQ24_spl
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f275]) ).
fof(f284,plain,
! [X0] :
( sQ3_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f119,f50]) ).
fof(f285,plain,
! [X0] :
( sQ3_spl
| ~ sP0_prd(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0,xS) ),
inference(resolution,[status(thm)],[f119,f91]) ).
fof(f287,definition,
! [X0] :
( sQ25_spl
<=> ( ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f288,plain,
! [X0] :
( ~ sQ25_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,plain,
( sQ3_spl
| sQ25_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f284,f114,f287,f117]) ).
fof(f304,plain,
( ~ sQ7_spl
| sQ16_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(slcrc0,xx))
| ~ aElement0(xx) ),
inference(resolution,[status(thm)],[f202,f132]) ).
fof(f305,plain,
( ~ sQ7_spl
| sQ16_spl
| ~ aElementOf0(xx,sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx))) ),
inference(resolution,[status(thm)],[f202,f132]) ).
fof(f306,definition,
( sQ29_spl
<=> aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(slcrc0,xx)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( sQ29_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(slcrc0,xx)) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f309,plain,
( ~ sQ7_spl
| sQ16_spl
| ~ sQ29_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f304,f111,f306,f200,f131]) ).
fof(f310,definition,
( sQ30_spl
<=> aElementOf0(xx,sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f312,plain,
( sQ30_spl
| ~ aElementOf0(xx,sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ),
inference(component_clause,[status(thm)],[f310]) ).
fof(f313,plain,
( ~ sQ7_spl
| sQ16_spl
| ~ sQ30_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f305,f120,f310,f200,f131]) ).
fof(f314,plain,
( sQ4_spl
| ~ aSet0(xS)
| xS = sdtpldt0(sdtmndt0(xS,xx),xx)
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f122,f204]) ).
fof(f318,definition,
( sQ31_spl
<=> xS = sdtpldt0(sdtmndt0(xS,xx),xx) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f319,plain,
( ~ sQ31_spl
| xS = sdtpldt0(sdtmndt0(xS,xx),xx) ),
inference(component_clause,[status(thm)],[f318]) ).
fof(f321,plain,
( sQ4_spl
| ~ sQ2_spl
| sQ31_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f314,f108,f111,f318,f114,f120]) ).
fof(f322,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f319,f87]) ).
fof(f323,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f322]) ).
fof(f336,plain,
! [X0,X1] :
( sQ12_spl
| ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aElementOf0(xS,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f141,f196]) ).
fof(f338,definition,
! [X0] :
( sQ33_spl
<=> ( ~ aSet0(X0)
| ~ aElementOf0(xS,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f339,plain,
! [X0] :
( ~ sQ33_spl
| ~ aSet0(X0)
| ~ aElementOf0(xS,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,definition,
! [X1] :
( sQ34_spl
<=> ( ~ aElement0(X1)
| ~ aElement0(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f342,plain,
! [X0] :
( ~ sQ34_spl
| ~ aElement0(X0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f344,plain,
( sQ12_spl
| sQ34_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f336,f338,f341,f180]) ).
fof(f345,plain,
! [X0] :
( ~ sQ34_spl
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f342]) ).
fof(f348,plain,
! [X0] :
( sK2_skl(slcrc0,X0,slcrc0) = X0
| ~ aSet0(slcrc0)
| slcrc0 = sdtpldt0(slcrc0,X0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f73,f95]) ).
fof(f349,plain,
! [X0,X1] :
( sK2_skl(slcrc0,X1,X0) = X1
| aElementOf0(sK2_skl(slcrc0,X1,X0),X0)
| ~ aSet0(slcrc0)
| slcrc0 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f73,f95]) ).
fof(f351,plain,
! [X0,X1] :
( sK2_skl(X1,X0,slcrc0) = X0
| aElementOf0(sK2_skl(X1,X0,slcrc0),X1)
| ~ aSet0(X1)
| X1 = sdtpldt0(slcrc0,X0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f73,f95]) ).
fof(f354,definition,
! [X0] :
( sQ35_spl
<=> ( sK2_skl(slcrc0,X0,slcrc0) = X0
| slcrc0 = sdtpldt0(slcrc0,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( sQ35_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f348,f128,f354]) ).
fof(f358,definition,
! [X0,X1] :
( sQ36_spl
<=> ( sK2_skl(slcrc0,X1,X0) = X1
| aElementOf0(sK2_skl(slcrc0,X1,X0),X0)
| slcrc0 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f361,plain,
( ~ sQ6_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f349,f358,f128]) ).
fof(f362,definition,
! [X0,X1] :
( sQ37_spl
<=> ( sK2_skl(X1,X0,slcrc0) = X0
| aElementOf0(sK2_skl(X1,X0,slcrc0),X1)
| ~ aSet0(X1)
| X1 = sdtpldt0(slcrc0,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( sQ37_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f351,f128,f362]) ).
fof(f367,plain,
( ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx))
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xS)
| ~ aSet0(xS)
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f140,f87]) ).
fof(f368,plain,
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f367,f108,f111,f114,f117,f123]) ).
fof(f369,plain,
( ~ sQ4_spl
| ~ sQ34_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f121,f345]) ).
fof(f373,plain,
( ~ sQ4_spl
| ~ sQ34_spl ),
inference(contradiction_clause,[status(thm)],[f369]) ).
fof(f374,plain,
! [X0] :
( ~ sQ33_spl
| ~ aElementOf0(xS,X0)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f339]) ).
fof(f375,plain,
! [X0,X1] :
( ~ sQ33_spl
| ~ aElementOf0(xS,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f374,f50]) ).
fof(f376,plain,
! [X0,X1] :
( ~ sQ33_spl
| ~ sP0_prd(xS,X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f374,f91]) ).
fof(f377,plain,
! [X0,X1] :
( ~ sQ33_spl
| ~ aElementOf0(xS,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f375]) ).
fof(f379,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aSet0(slcrc0)
| ~ aElementOf0(X0,X1) ),
inference(resolution,[status(thm)],[f258,f52]) ).
fof(f380,plain,
! [X0] :
( ~ sQ22_spl
| ~ aSet0(slcrc0)
| ~ aElementOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f258,f56]) ).
fof(f381,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aSet0(X0)
| aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f258,f51]) ).
fof(f383,plain,
( ~ sQ22_spl
| ~ aSubsetOf0(xS,slcrc0) ),
inference(resolution,[status(thm)],[f258,f86]) ).
fof(f384,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f258,f50]) ).
fof(f386,definition,
! [X0] :
( sQ38_spl
<=> ~ aElementOf0(X0,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f390,definition,
! [X0,X1] :
( sQ39_spl
<=> ( ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f379,f390,f128,f257]) ).
fof(f394,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f380,f386,f128,f257]) ).
fof(f395,plain,
( ~ sQ22_spl
| ~ aElementOf0(sK1_skl(xS,slcrc0),slcrc0)
| ~ aSet0(xS)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f383,f52]) ).
fof(f396,definition,
( sQ40_spl
<=> aElementOf0(sK1_skl(xS,slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( ~ sQ22_spl
| ~ sQ40_spl
| ~ sQ2_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f395,f128,f114,f396,f257]) ).
fof(f410,definition,
( sQ43_spl
<=> aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( sQ43_spl
| ~ aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(component_clause,[status(thm)],[f410]) ).
fof(f414,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f60,f49]) ).
fof(f415,plain,
! [X0] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(slcrc0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f414,f383]) ).
fof(f416,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(slcrc0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f414,f258]) ).
fof(f417,definition,
! [X0] :
( sQ44_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f418,plain,
! [X0] :
( ~ sQ44_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f420,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f415,f417,f128,f257]) ).
fof(f421,definition,
! [X0,X1,X2] :
( sQ45_spl
<=> ( ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f416,f421,f128,f257]) ).
fof(f427,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ33_spl
| ~ aSet0(X0)
| ~ aElementOf0(xS,slcrc0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f377,f264]) ).
fof(f431,definition,
( sQ46_spl
<=> aElementOf0(xS,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( ~ sQ23_spl
| ~ sQ33_spl
| ~ sQ46_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f427,f275,f431,f338,f263]) ).
fof(f438,plain,
! [X0] :
( ~ sQ24_spl
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f276]) ).
fof(f439,plain,
( ~ sQ24_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f94,f438]) ).
fof(f442,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f439]) ).
fof(f448,plain,
( sQ3_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = xx
| aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx))
| ~ aSet0(xS)
| xS = sdtpldt0(sdtmndt0(xS,xx),xx)
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f73,f119]) ).
fof(f454,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSubsetOf0(X2,slcrc0)
| sK2_skl(X2,X1,X0) = X1
| aElementOf0(sK2_skl(X2,X1,X0),X0)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f73,f258]) ).
fof(f457,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| sK2_skl(X2,X1,X0) = X1
| aElementOf0(sK2_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f73,f258]) ).
fof(f459,plain,
( sQ3_spl
| sQ16_spl
| sQ5_spl
| ~ sQ2_spl
| sQ31_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f448,f108,f111,f318,f114,f123,f200,f117]) ).
fof(f472,plain,
! [X0,X1] :
( sP0_prd(sK3_skl(slcrc0,X1,X0),X1,X0)
| ~ aSet0(slcrc0)
| slcrc0 = sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f84,f95]) ).
fof(f473,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSubsetOf0(X2,slcrc0)
| sP0_prd(sK3_skl(X2,X1,X0),X1,X0)
| ~ aSet0(X2)
| X2 = sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f84,f258]) ).
fof(f474,plain,
! [X0,X1] :
( aElementOf0(sK3_skl(X1,X0,slcrc0),X1)
| ~ aSet0(X1)
| X1 = sdtmndt0(slcrc0,X0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f84,f139]) ).
fof(f476,definition,
! [X0,X1] :
( sQ47_spl
<=> ( sP0_prd(sK3_skl(slcrc0,X1,X0),X1,X0)
| slcrc0 = sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f477,plain,
! [X0,X1] :
( ~ sQ47_spl
| sP0_prd(sK3_skl(slcrc0,X1,X0),X1,X0)
| slcrc0 = sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f479,plain,
( ~ sQ6_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f472,f476,f128]) ).
fof(f480,definition,
! [X0,X1] :
( sQ48_spl
<=> ( aElementOf0(sK3_skl(X1,X0,slcrc0),X1)
| ~ aSet0(X1)
| X1 = sdtmndt0(slcrc0,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f483,plain,
( sQ48_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f474,f128,f480]) ).
fof(f486,plain,
! [X0,X1] :
( ~ sQ33_spl
| ~ aSet0(X0)
| xS = X1
| ~ aElementOf0(xS,X0)
| ~ aElement0(xS) ),
inference(resolution,[status(thm)],[f93,f376]) ).
fof(f492,definition,
! [X0] :
( sQ49_spl
<=> ( ~ aSet0(X0)
| ~ aElementOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( ~ sQ33_spl
| sQ21_spl
| sQ49_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f486,f180,f492,f247,f338]) ).
fof(f518,plain,
! [X0] :
( ~ sQ33_spl
| ~ aSet0(sdtpldt0(X0,xS))
| ~ aElement0(xS)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f102,f374]) ).
fof(f519,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aSubsetOf0(sdtpldt0(X0,X1),slcrc0)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f102,f258]) ).
fof(f520,plain,
( ~ sQ33_spl
| ~ sQ12_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f518,f214,f180,f338]) ).
fof(f521,plain,
( ~ sQ44_spl
| ~ aSet0(xS)
| ~ aSubsetOf0(xS,slcrc0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f418,f56]) ).
fof(f524,definition,
( sQ50_spl
<=> aSubsetOf0(xS,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f527,plain,
( ~ sQ44_spl
| ~ sQ50_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f521,f114,f524,f417]) ).
fof(f535,plain,
( sQ3_spl
| ~ sQ16_spl
| ~ aElementOf0(xx,xS) ),
inference(backward_demodulation,[status(thm)],[f201,f119]) ).
fof(f539,plain,
( sQ3_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f535,f86]) ).
fof(f540,plain,
( sQ3_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f539]) ).
fof(f543,plain,
! [X0,X1,X2] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| X1 = X2
| ~ aElementOf0(X1,sdtpldt0(sdtmndt0(X0,X1),X2))
| ~ aElement0(X2)
| ~ aSet0(sdtmndt0(X0,X1)) ),
inference(resolution,[status(thm)],[f99,f137]) ).
fof(f545,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| X2 = X1
| ~ aElementOf0(X2,sdtpldt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f99,f258]) ).
fof(f547,plain,
! [X0,X1,X2] :
( ~ aElement0(X1)
| ~ aSet0(X2)
| X1 = X0
| ~ aElementOf0(X1,sdtpldt0(sdtmndt0(X2,X1),X0))
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f103]) ).
fof(f552,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSubsetOf0(sdtmndt0(X0,X1),slcrc0)
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f105,f258]) ).
fof(f612,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aSet0(sdtpldt0(X0,X1))
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(sdtpldt0(X0,X1),slcrc0) ),
inference(resolution,[status(thm)],[f381,f519]) ).
fof(f615,plain,
! [X0] :
( ~ sQ44_spl
| ~ sQ22_spl
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0)
| ~ aSet0(X0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f381,f418]) ).
fof(f616,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f381,f258]) ).
fof(f617,plain,
! [X0,X1] :
( ~ sQ33_spl
| ~ sQ22_spl
| ~ aElementOf0(xS,X0)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f381,f377]) ).
fof(f622,definition,
! [X0,X1] :
( sQ56_spl
<=> ( ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aSet0(sdtpldt0(X0,X1))
| ~ aSubsetOf0(sdtpldt0(X0,X1),slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f612,f622,f128,f257]) ).
fof(f627,definition,
! [X0] :
( sQ57_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f628,plain,
! [X0] :
( ~ sQ57_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f627]) ).
fof(f631,definition,
! [X0] :
( sQ58_spl
<=> ( ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( ~ sQ44_spl
| ~ sQ22_spl
| ~ sQ6_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f615,f631,f128,f257,f417]) ).
fof(f635,definition,
! [X0,X1] :
( sQ59_spl
<=> ( ~ aElementOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f616,f635,f128,f257]) ).
fof(f639,definition,
! [X0] :
( sQ60_spl
<=> ( ~ aElementOf0(xS,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f642,plain,
( ~ sQ33_spl
| ~ sQ22_spl
| sQ24_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f617,f639,f275,f257,f338]) ).
fof(f644,plain,
( sQ43_spl
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f412,f97]) ).
fof(f646,plain,
( sQ43_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f644,f108,f111,f410]) ).
fof(f668,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSet0(X0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f384,f381]) ).
fof(f691,definition,
( sQ61_spl
<=> aSubsetOf0(slcrc0,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( ~ sQ61_spl
| aSubsetOf0(slcrc0,slcrc0) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f693,plain,
( sQ61_spl
| ~ aSubsetOf0(slcrc0,slcrc0) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f695,definition,
! [X0,X1,X2] :
( sQ62_spl
<=> ( ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f668,f695,f128,f257]) ).
fof(f716,plain,
! [X0] :
( ~ sQ57_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f628]) ).
fof(f719,plain,
( ~ sQ57_spl
| ~ aSet0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f716,f56]) ).
fof(f721,plain,
( ~ sQ57_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f719,f128,f627]) ).
fof(f722,plain,
! [X0,X1,X2] :
( aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f49]) ).
fof(f724,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(sdtpldt0(X0,X1),X2)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f722,f519]) ).
fof(f726,plain,
! [X0] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f722,f383]) ).
fof(f727,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f722,f258]) ).
fof(f728,plain,
! [X0,X1,X2] :
( ~ sQ33_spl
| ~ aElementOf0(xS,X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f722,f377]) ).
fof(f733,definition,
! [X0,X1,X2] :
( sQ64_spl
<=> ( ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(sdtpldt0(X0,X1),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f736,plain,
( ~ sQ22_spl
| sQ64_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f724,f128,f733,f257]) ).
fof(f741,definition,
! [X0] :
( sQ66_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f742,plain,
! [X0] :
( ~ sQ66_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(xS,X0) ),
inference(component_clause,[status(thm)],[f741]) ).
fof(f744,plain,
( ~ sQ22_spl
| sQ66_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f726,f128,f741,f257]) ).
fof(f745,definition,
! [X0,X1,X2] :
( sQ67_spl
<=> ( ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f746,plain,
! [X0,X1,X2] :
( ~ sQ67_spl
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1) ),
inference(component_clause,[status(thm)],[f745]) ).
fof(f748,plain,
( ~ sQ22_spl
| sQ67_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f727,f128,f745,f257]) ).
fof(f749,plain,
! [X0,X1,X2] :
( ~ sQ33_spl
| ~ aElementOf0(xS,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f728]) ).
fof(f751,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aElementOf0(sK1_skl(sdtpldt0(X0,X1),slcrc0),slcrc0)
| ~ aSet0(sdtpldt0(X0,X1))
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f52,f519]) ).
fof(f759,definition,
! [X0,X1] :
( sQ69_spl
<=> ( ~ aElement0(X1)
| ~ aSet0(X0)
| ~ aElementOf0(sK1_skl(sdtpldt0(X0,X1),slcrc0),slcrc0)
| ~ aSet0(sdtpldt0(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( ~ sQ22_spl
| sQ69_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f751,f128,f759,f257]) ).
fof(f786,plain,
( ~ sQ22_spl
| ~ sQ5_spl
| ~ aSubsetOf0(sdtmndt0(xS,xx),slcrc0) ),
inference(resolution,[status(thm)],[f124,f258]) ).
fof(f797,plain,
! [X0] :
( ~ sQ66_spl
| ~ aElementOf0(sK1_skl(xS,X0),X0)
| ~ aSet0(xS)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f742,f52]) ).
fof(f801,plain,
! [X0] :
( ~ sQ66_spl
| ~ aElementOf0(sK1_skl(X0,slcrc0),slcrc0)
| ~ aSet0(X0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f742,f52]) ).
fof(f802,plain,
! [X0,X1] :
( ~ sQ66_spl
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f742,f722]) ).
fof(f804,definition,
! [X0] :
( sQ75_spl
<=> ( ~ aElementOf0(sK1_skl(xS,X0),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( ~ sQ66_spl
| ~ sQ2_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f797,f804,f114,f741]) ).
fof(f810,definition,
! [X0] :
( sQ76_spl
<=> ( ~ aElementOf0(sK1_skl(X0,slcrc0),slcrc0)
| ~ aSet0(X0)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( ~ sQ66_spl
| ~ sQ6_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f801,f810,f128,f741]) ).
fof(f814,definition,
! [X0,X1] :
( sQ77_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f815,plain,
! [X0,X1] :
( ~ sQ77_spl
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(component_clause,[status(thm)],[f814]) ).
fof(f817,plain,
( ~ sQ66_spl
| ~ sQ6_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f802,f814,f128,f741]) ).
fof(f820,plain,
! [X0] :
( ~ sQ22_spl
| ~ sQ5_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f786,f722]) ).
fof(f821,definition,
( sQ78_spl
<=> aElementOf0(sK1_skl(sdtmndt0(xS,xx),slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f825,definition,
! [X0] :
( sQ79_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f826,plain,
! [X0] :
( ~ sQ79_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0) ),
inference(component_clause,[status(thm)],[f825]) ).
fof(f828,plain,
( ~ sQ22_spl
| ~ sQ5_spl
| sQ79_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f820,f128,f825,f123,f257]) ).
fof(f885,plain,
! [X0,X1,X2] :
( ~ sQ67_spl
| ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aSet0(slcrc0)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f746,f52]) ).
fof(f886,plain,
! [X0,X1,X2,X3] :
( ~ sQ67_spl
| ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aSet0(slcrc0)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f746,f722]) ).
fof(f904,plain,
! [X0,X1,X2,X3] :
( ~ sQ67_spl
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f746,f91]) ).
fof(f907,definition,
! [X0] :
( sQ86_spl
<=> ( ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f908,plain,
! [X0] :
( ~ sQ86_spl
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(component_clause,[status(thm)],[f907]) ).
fof(f915,definition,
! [X1] :
( sQ88_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(slcrc0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f916,plain,
! [X0] :
( ~ sQ88_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(slcrc0,X0) ),
inference(component_clause,[status(thm)],[f915]) ).
fof(f921,definition,
! [X0,X1,X2] :
( sQ89_spl
<=> ( ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f924,plain,
( ~ sQ67_spl
| ~ sQ6_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f885,f921,f128,f745]) ).
fof(f925,definition,
! [X0,X1,X2,X3] :
( sQ90_spl
<=> ( ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f926,plain,
! [X0,X1,X2,X3] :
( ~ sQ90_spl
| ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(component_clause,[status(thm)],[f925]) ).
fof(f928,plain,
( ~ sQ67_spl
| ~ sQ6_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f886,f925,f128,f745]) ).
fof(f936,plain,
( sQ61_spl
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f693,f56]) ).
fof(f940,plain,
( sQ61_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f936,f128,f691]) ).
fof(f950,plain,
( ~ sQ61_spl
| ~ sQ88_spl
| $false ),
inference(resolution,[status(thm)],[f916,f692]) ).
fof(f966,plain,
( ~ sQ61_spl
| ~ sQ88_spl ),
inference(contradiction_clause,[status(thm)],[f950]) ).
fof(f969,plain,
! [X0,X1] :
( ~ sQ77_spl
| ~ aElementOf0(sK1_skl(xS,X0),X0)
| ~ aSet0(xS)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f815,f52]) ).
fof(f986,plain,
! [X0,X1] :
( ~ sQ77_spl
| ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f815,f52]) ).
fof(f987,plain,
! [X0,X1,X2] :
( ~ sQ77_spl
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f815,f722]) ).
fof(f990,definition,
( sQ91_spl
<=> aElementOf0(sK1_skl(xS,xS),xS) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f992,plain,
( sQ91_spl
| ~ aElementOf0(sK1_skl(xS,xS),xS) ),
inference(component_clause,[status(thm)],[f990]) ).
fof(f994,definition,
! [X0,X1] :
( sQ92_spl
<=> ( ~ aElementOf0(sK1_skl(xS,X0),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f997,plain,
( ~ sQ77_spl
| ~ sQ2_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f969,f994,f114,f814]) ).
fof(f998,definition,
! [X0] :
( sQ93_spl
<=> ( ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f999,plain,
! [X0] :
( ~ sQ93_spl
| ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(xS,X0) ),
inference(component_clause,[status(thm)],[f998]) ).
fof(f1011,definition,
! [X0,X1] :
( sQ94_spl
<=> ( ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1014,plain,
( ~ sQ77_spl
| ~ sQ6_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f986,f1011,f128,f814]) ).
fof(f1015,definition,
! [X0,X1,X2] :
( sQ95_spl
<=> ( ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1016,plain,
! [X0,X1,X2] :
( ~ sQ95_spl
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(component_clause,[status(thm)],[f1015]) ).
fof(f1018,plain,
( ~ sQ77_spl
| ~ sQ6_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f987,f1015,f128,f814]) ).
fof(f1020,definition,
( sQ96_spl
<=> aSubsetOf0(xS,xS) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1021,plain,
( ~ sQ96_spl
| aSubsetOf0(xS,xS) ),
inference(component_clause,[status(thm)],[f1020]) ).
fof(f1022,plain,
( sQ96_spl
| ~ aSubsetOf0(xS,xS) ),
inference(component_clause,[status(thm)],[f1020]) ).
fof(f1028,plain,
( ~ sQ86_spl
| ~ aSet0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f908,f56]) ).
fof(f1039,plain,
( ~ sQ86_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1028,f128,f907]) ).
fof(f1046,plain,
! [X0] :
( ~ sQ47_spl
| slcrc0 = sdtmndt0(slcrc0,X0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f477,f139]) ).
fof(f1048,definition,
! [X0] :
( sQ99_spl
<=> ( slcrc0 = sdtmndt0(slcrc0,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( ~ sQ47_spl
| sQ99_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1046,f128,f1048,f476]) ).
fof(f1052,plain,
! [X0] :
( ~ sQ79_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),X0),X0)
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f826,f52]) ).
fof(f1054,plain,
( ~ sQ79_spl
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSubsetOf0(sdtmndt0(xS,xx),slcrc0) ),
inference(resolution,[status(thm)],[f826,f56]) ).
fof(f1055,definition,
! [X0] :
( sQ100_spl
<=> ( ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),X0),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1058,plain,
( ~ sQ79_spl
| ~ sQ0_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1052,f1055,f108,f825]) ).
fof(f1059,definition,
( sQ101_spl
<=> aSubsetOf0(sdtmndt0(xS,xx),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1061,plain,
( sQ101_spl
| ~ aSubsetOf0(sdtmndt0(xS,xx),slcrc0) ),
inference(component_clause,[status(thm)],[f1059]) ).
fof(f1062,plain,
( ~ sQ79_spl
| ~ sQ0_spl
| ~ sQ101_spl ),
inference(split_clause,[status(thm)],[f1054,f1059,f108,f825]) ).
fof(f1073,plain,
! [X0] :
( ~ sQ61_spl
| ~ sQ33_spl
| ~ aElementOf0(xS,X0)
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f749,f692]) ).
fof(f1092,definition,
! [X0] :
( sQ104_spl
<=> ( ~ aElementOf0(xS,X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1095,plain,
( ~ sQ61_spl
| ~ sQ33_spl
| sQ104_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1073,f128,f1092,f338,f691]) ).
fof(f1101,plain,
( ~ sQ25_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = xx
| aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xS)
| ~ aSet0(xS)
| xS = sdtpldt0(sdtmndt0(xS,xx),xx)
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSubsetOf0(sdtmndt0(xS,xx),xS) ),
inference(resolution,[status(thm)],[f288,f73]) ).
fof(f1102,plain,
( ~ sQ25_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = xx
| aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx))
| ~ aSet0(xS)
| xS = sdtpldt0(sdtmndt0(xS,xx),xx)
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSubsetOf0(xS,xS) ),
inference(resolution,[status(thm)],[f288,f73]) ).
fof(f1109,definition,
( sQ105_spl
<=> aSubsetOf0(sdtmndt0(xS,xx),xS) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1110,plain,
( ~ sQ105_spl
| aSubsetOf0(sdtmndt0(xS,xx),xS) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1111,plain,
( sQ105_spl
| ~ aSubsetOf0(sdtmndt0(xS,xx),xS) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1112,plain,
( ~ sQ25_spl
| sQ16_spl
| sQ3_spl
| ~ sQ2_spl
| sQ31_spl
| ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f1101,f1109,f108,f111,f318,f114,f117,f200,f287]) ).
fof(f1113,plain,
( ~ sQ25_spl
| sQ16_spl
| sQ5_spl
| ~ sQ2_spl
| sQ31_spl
| ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f1102,f1020,f108,f111,f318,f114,f123,f200,f287]) ).
fof(f1120,plain,
( sQ96_spl
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1022,f56]) ).
fof(f1123,plain,
( sQ96_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1120,f114,f1020]) ).
fof(f1127,plain,
( ~ sQ33_spl
| ~ sQ96_spl
| ~ aElementOf0(xS,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1021,f749]) ).
fof(f1135,definition,
( sQ107_spl
<=> aElementOf0(xS,xS) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1137,plain,
( sQ107_spl
| ~ aElementOf0(xS,xS) ),
inference(component_clause,[status(thm)],[f1135]) ).
fof(f1138,plain,
( ~ sQ33_spl
| ~ sQ96_spl
| ~ sQ107_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1127,f114,f1135,f1020,f338]) ).
fof(f1139,definition,
! [X0] :
( sQ108_spl
<=> ( ~ aElementOf0(xS,X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
! [X0] :
( ~ sQ108_spl
| ~ aElementOf0(xS,X0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f1139]) ).
fof(f1154,plain,
! [X0] :
( sQ107_spl
| ~ aElementOf0(xS,X0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1137,f50]) ).
fof(f1155,plain,
! [X0] :
( sQ107_spl
| xS = X0
| ~ aElementOf0(xS,sdtpldt0(xS,X0))
| ~ aElement0(X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1137,f99]) ).
fof(f1157,plain,
( sQ107_spl
| sQ108_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1154,f114,f1139,f1135]) ).
fof(f1158,definition,
! [X0] :
( sQ111_spl
<=> ( xS = X0
| ~ aElementOf0(xS,sdtpldt0(xS,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1159,plain,
! [X0] :
( ~ sQ111_spl
| xS = X0
| ~ aElementOf0(xS,sdtpldt0(xS,X0))
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f1158]) ).
fof(f1161,plain,
( sQ107_spl
| sQ111_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1155,f114,f1158,f1135]) ).
fof(f1162,plain,
( sQ101_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),slcrc0),slcrc0)
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1061,f52]) ).
fof(f1163,plain,
! [X0] :
( sQ101_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1061,f722]) ).
fof(f1164,plain,
( sQ101_spl
| ~ sQ78_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1162,f128,f108,f821,f1059]) ).
fof(f1165,plain,
( sQ101_spl
| sQ79_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1163,f128,f825,f1059]) ).
fof(f1166,plain,
( ~ sQ96_spl
| ~ sQ93_spl
| $false ),
inference(resolution,[status(thm)],[f999,f1021]) ).
fof(f1180,plain,
( ~ sQ96_spl
| ~ sQ93_spl ),
inference(contradiction_clause,[status(thm)],[f1166]) ).
fof(f1185,plain,
! [X0] :
( sQ5_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,sdtmndt0(xS,xx))
| ~ aSet0(sdtmndt0(xS,xx)) ),
inference(resolution,[status(thm)],[f125,f50]) ).
fof(f1190,definition,
! [X0] :
( sQ112_spl
<=> ( ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,sdtmndt0(xS,xx)) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1193,plain,
( sQ5_spl
| sQ112_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1185,f108,f1190,f123]) ).
fof(f1196,plain,
! [X0] :
( sQ91_spl
| ~ aElementOf0(sK1_skl(xS,xS),X0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f992,f50]) ).
fof(f1197,plain,
! [X0] :
( sQ91_spl
| sK1_skl(xS,xS) = X0
| ~ aElementOf0(sK1_skl(xS,xS),sdtpldt0(xS,X0))
| ~ aElement0(X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f992,f99]) ).
fof(f1200,definition,
! [X0] :
( sQ113_spl
<=> ( ~ aElementOf0(sK1_skl(xS,xS),X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1201,plain,
! [X0] :
( ~ sQ113_spl
| ~ aElementOf0(sK1_skl(xS,xS),X0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f1200]) ).
fof(f1203,plain,
( sQ91_spl
| sQ113_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1196,f114,f1200,f990]) ).
fof(f1204,definition,
! [X0] :
( sQ114_spl
<=> ( sK1_skl(xS,xS) = X0
| ~ aElementOf0(sK1_skl(xS,xS),sdtpldt0(xS,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1207,plain,
( sQ91_spl
| sQ114_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1197,f114,f1204,f990]) ).
fof(f1208,plain,
( ~ sQ96_spl
| ~ sQ108_spl
| ~ aElementOf0(xS,xS) ),
inference(resolution,[status(thm)],[f1140,f1021]) ).
fof(f1209,plain,
( ~ sQ23_spl
| ~ sQ108_spl
| ~ aSet0(xS)
| ~ aElementOf0(xS,slcrc0) ),
inference(resolution,[status(thm)],[f1140,f264]) ).
fof(f1210,plain,
! [X0] :
( ~ sQ108_spl
| ~ aElementOf0(sK1_skl(X0,xS),xS)
| ~ aSet0(X0)
| ~ aSet0(xS)
| ~ aElementOf0(xS,X0) ),
inference(resolution,[status(thm)],[f1140,f52]) ).
fof(f1211,plain,
! [X0,X1] :
( ~ sQ108_spl
| ~ aSubsetOf0(X1,xS)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(xS)
| ~ aElementOf0(xS,X0) ),
inference(resolution,[status(thm)],[f1140,f722]) ).
fof(f1212,plain,
( ~ sQ108_spl
| ~ aSet0(xS)
| ~ aElementOf0(xS,xS) ),
inference(resolution,[status(thm)],[f1140,f56]) ).
fof(f1213,plain,
( ~ sQ23_spl
| ~ sQ108_spl
| ~ sQ2_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f1209,f431,f114,f1139,f263]) ).
fof(f1214,definition,
! [X0] :
( sQ115_spl
<=> ( ~ aElementOf0(sK1_skl(X0,xS),xS)
| ~ aSet0(X0)
| ~ aElementOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1217,plain,
( ~ sQ108_spl
| ~ sQ2_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f1210,f1214,f114,f1139]) ).
fof(f1218,definition,
! [X0,X1] :
( sQ116_spl
<=> ( ~ aSubsetOf0(X1,xS)
| ~ aSubsetOf0(X0,X1)
| ~ aElementOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1221,plain,
( ~ sQ108_spl
| ~ sQ2_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f1211,f1218,f114,f1139]) ).
fof(f1222,plain,
( ~ sQ108_spl
| ~ sQ2_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f1212,f1135,f114,f1139]) ).
fof(f1224,plain,
! [X0] :
( ~ sQ96_spl
| ~ sQ108_spl
| xS = X0
| ~ aElementOf0(xS,sdtpldt0(xS,X0))
| ~ aElement0(X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1208,f99]) ).
fof(f1227,plain,
( ~ sQ96_spl
| ~ sQ108_spl
| sQ111_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1224,f114,f1158,f1139,f1020]) ).
fof(f1239,plain,
! [X0,X1] :
( ~ sQ67_spl
| ~ aSet0(slcrc0)
| ~ sP0_prd(X0,X1,slcrc0) ),
inference(resolution,[status(thm)],[f904,f56]) ).
fof(f1243,plain,
! [X0,X1,X2,X3] :
( ~ sQ67_spl
| ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ aSet0(slcrc0)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f904,f52]) ).
fof(f1244,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ67_spl
| ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ aSet0(slcrc0)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f904,f722]) ).
fof(f1255,definition,
! [X0,X1] :
( sQ118_spl
<=> ~ sP0_prd(X0,X1,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1263,plain,
( ~ sQ67_spl
| ~ sQ6_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1239,f1255,f128,f745]) ).
fof(f1264,definition,
! [X0,X1,X2] :
( sQ119_spl
<=> ( ~ sP0_prd(X1,X2,X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1268,definition,
! [X0,X1,X2,X3] :
( sQ120_spl
<=> ( ~ aElementOf0(sK1_skl(X1,slcrc0),slcrc0)
| ~ aSet0(X1)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
( ~ sQ67_spl
| ~ sQ6_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f1243,f1268,f128,f745]) ).
fof(f1272,definition,
! [X0,X1,X2,X3,X4] :
( sQ121_spl
<=> ( ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1273,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ121_spl
| ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(component_clause,[status(thm)],[f1272]) ).
fof(f1275,plain,
( ~ sQ67_spl
| ~ sQ6_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f1244,f1272,f128,f745]) ).
fof(f1285,plain,
! [X0] :
( ~ sQ113_spl
| ~ aElement0(sK1_skl(xS,xS))
| ~ aSet0(X0)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),xS) ),
inference(resolution,[status(thm)],[f1201,f102]) ).
fof(f1291,definition,
! [X0] :
( sQ122_spl
<=> ( ~ aSet0(X0)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),xS) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1292,plain,
! [X0] :
( ~ sQ122_spl
| ~ aSet0(X0)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),xS) ),
inference(component_clause,[status(thm)],[f1291]) ).
fof(f1294,definition,
( sQ123_spl
<=> aElement0(sK1_skl(xS,xS)) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1296,plain,
( sQ123_spl
| ~ aElement0(sK1_skl(xS,xS)) ),
inference(component_clause,[status(thm)],[f1294]) ).
fof(f1297,plain,
( ~ sQ113_spl
| ~ sQ123_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1285,f1291,f1294,f1200]) ).
fof(f1298,plain,
! [X0] :
( sQ16_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtmndt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))),xx))
| ~ aElement0(xx)
| ~ aSet0(sdtmndt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f237,f202]) ).
fof(f1299,plain,
! [X0] :
( ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(sdtmndt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)),xS))
| ~ aElement0(xS)
| ~ aSet0(sdtmndt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f237,f87]) ).
fof(f1300,plain,
! [X0] :
( sQ16_spl
| ~ aElementOf0(xx,sdtpldt0(sdtmndt0(X0,xx),sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx)))
| ~ aSet0(sdtmndt0(X0,xx))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f237,f202]) ).
fof(f1301,plain,
! [X0] :
( ~ aElementOf0(xS,sdtpldt0(sdtmndt0(X0,xS),sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aElement0(sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSet0(sdtmndt0(X0,xS))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f237,f87]) ).
fof(f1302,definition,
! [X0] :
( sQ124_spl
<=> ( ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtmndt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))),xx))
| ~ aSet0(sdtmndt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1305,plain,
( sQ16_spl
| ~ sQ1_spl
| sQ124_spl ),
inference(split_clause,[status(thm)],[f1298,f1302,f111,f200]) ).
fof(f1306,definition,
! [X0] :
( sQ125_spl
<=> ( ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(sdtmndt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)),xS))
| ~ aSet0(sdtmndt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1309,plain,
( ~ sQ12_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1299,f1306,f180]) ).
fof(f1310,definition,
! [X0] :
( sQ126_spl
<=> ( ~ aElementOf0(xx,sdtpldt0(sdtmndt0(X0,xx),sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aSet0(sdtmndt0(X0,xx))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1313,plain,
( sQ16_spl
| ~ sQ4_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f1300,f1310,f120,f200]) ).
fof(f1314,definition,
! [X0] :
( sQ127_spl
<=> ( ~ aElementOf0(xS,sdtpldt0(sdtmndt0(X0,xS),sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aSet0(sdtmndt0(X0,xS))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1317,plain,
( ~ sQ14_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f1301,f1314,f187]) ).
fof(f1324,plain,
( ~ sQ111_spl
| ~ aElementOf0(xS,sdtpldt0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aElement0(sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(resolution,[status(thm)],[f1159,f87]) ).
fof(f1325,definition,
( sQ128_spl
<=> aElementOf0(xS,sdtpldt0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1328,plain,
( ~ sQ111_spl
| ~ sQ128_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1324,f187,f1325,f1158]) ).
fof(f1343,plain,
( sQ30_spl
| ~ aElementOf0(xx,slcrc0)
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx)))
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f312,f141]) ).
fof(f1344,plain,
! [X0] :
( sQ30_spl
| ~ aElementOf0(xx,X0)
| ~ aSubsetOf0(X0,sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aSet0(sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ),
inference(resolution,[status(thm)],[f312,f50]) ).
fof(f1345,plain,
! [X0] :
( sQ30_spl
| xx = X0
| ~ aElementOf0(xx,sdtpldt0(sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx))),X0))
| ~ aElement0(X0)
| ~ aSet0(sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ),
inference(resolution,[status(thm)],[f312,f99]) ).
fof(f1347,definition,
( sQ131_spl
<=> aElementOf0(xx,slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1350,plain,
( sQ30_spl
| ~ sQ131_spl
| ~ sQ4_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1343,f128,f120,f1347,f310]) ).
fof(f1351,definition,
( sQ132_spl
<=> aSet0(sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1353,plain,
( sQ132_spl
| ~ aSet0(sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ),
inference(component_clause,[status(thm)],[f1351]) ).
fof(f1354,definition,
! [X0] :
( sQ133_spl
<=> ( ~ aElementOf0(xx,X0)
| ~ aSubsetOf0(X0,sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1357,plain,
( sQ30_spl
| sQ133_spl
| ~ sQ132_spl ),
inference(split_clause,[status(thm)],[f1344,f1351,f1354,f310]) ).
fof(f1358,definition,
! [X0] :
( sQ134_spl
<=> ( xx = X0
| ~ aElementOf0(xx,sdtpldt0(sdtpldt0(slcrc0,sK2_skl(xS,xx,sdtmndt0(xS,xx))),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1361,plain,
( sQ30_spl
| sQ134_spl
| ~ sQ132_spl ),
inference(split_clause,[status(thm)],[f1345,f1351,f1358,f310]) ).
fof(f1368,plain,
! [X0] :
( ~ sQ122_spl
| ~ aElementOf0(sK1_skl(sdtpldt0(X0,sK1_skl(xS,xS)),xS),xS)
| ~ aSet0(sdtpldt0(X0,sK1_skl(xS,xS)))
| ~ aSet0(xS)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1292,f52]) ).
fof(f1369,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ aSubsetOf0(X1,xS)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),X1)
| ~ aSet0(xS)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1292,f722]) ).
fof(f1370,definition,
! [X0] :
( sQ136_spl
<=> ( ~ aElementOf0(sK1_skl(sdtpldt0(X0,sK1_skl(xS,xS)),xS),xS)
| ~ aSet0(sdtpldt0(X0,sK1_skl(xS,xS)))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1373,plain,
( ~ sQ122_spl
| ~ sQ2_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f1368,f1370,f114,f1291]) ).
fof(f1374,definition,
! [X0,X1] :
( sQ137_spl
<=> ( ~ aSubsetOf0(X1,xS)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
( ~ sQ122_spl
| ~ sQ2_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f1369,f1374,f114,f1291]) ).
fof(f1380,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aSubsetOf0(X1,slcrc0)
| sK2_skl(X1,X0,slcrc0) = X0
| ~ aSet0(X1)
| X1 = sdtpldt0(slcrc0,X0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f454,f95]) ).
fof(f1384,definition,
! [X0,X1] :
( sQ138_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| sK2_skl(X1,X0,slcrc0) = X0
| ~ aSet0(X1)
| X1 = sdtpldt0(slcrc0,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1387,plain,
( ~ sQ22_spl
| sQ138_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1380,f128,f1384,f257]) ).
fof(f1388,plain,
( sQ105_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),xS)
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1111,f52]) ).
fof(f1389,plain,
! [X0] :
( sQ105_spl
| ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1111,f722]) ).
fof(f1390,definition,
( sQ139_spl
<=> aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),xS) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1392,plain,
( sQ139_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),xS) ),
inference(component_clause,[status(thm)],[f1390]) ).
fof(f1393,plain,
( sQ105_spl
| ~ sQ139_spl
| ~ sQ0_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1388,f114,f108,f1390,f1109]) ).
fof(f1394,definition,
! [X0] :
( sQ140_spl
<=> ( ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1395,plain,
! [X0] :
( ~ sQ140_spl
| ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(sdtmndt0(xS,xx),X0) ),
inference(component_clause,[status(thm)],[f1394]) ).
fof(f1397,plain,
( sQ105_spl
| sQ140_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1389,f114,f1394,f1109]) ).
fof(f1398,plain,
! [X0] :
( sQ139_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),X0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1392,f50]) ).
fof(f1399,plain,
! [X0] :
( sQ139_spl
| sK1_skl(sdtmndt0(xS,xx),xS) = X0
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),sdtpldt0(xS,X0))
| ~ aElement0(X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1392,f99]) ).
fof(f1400,plain,
! [X0] :
( sQ139_spl
| ~ sP0_prd(sK1_skl(sdtmndt0(xS,xx),xS),X0,xS) ),
inference(resolution,[status(thm)],[f1392,f91]) ).
fof(f1401,definition,
! [X0] :
( sQ141_spl
<=> ( ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
! [X0] :
( ~ sQ141_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),X0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f1401]) ).
fof(f1404,plain,
( sQ139_spl
| sQ141_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1398,f114,f1401,f1390]) ).
fof(f1405,definition,
! [X0] :
( sQ142_spl
<=> ( sK1_skl(sdtmndt0(xS,xx),xS) = X0
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),sdtpldt0(xS,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1408,plain,
( sQ139_spl
| sQ142_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1399,f114,f1405,f1390]) ).
fof(f1409,plain,
! [X0] :
( ~ sQ140_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),X0),X0)
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,xS) ),
inference(resolution,[status(thm)],[f1395,f52]) ).
fof(f1411,plain,
( ~ sQ140_spl
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSubsetOf0(sdtmndt0(xS,xx),xS) ),
inference(resolution,[status(thm)],[f1395,f56]) ).
fof(f1412,definition,
! [X0] :
( sQ143_spl
<=> ( ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),X0),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1415,plain,
( ~ sQ140_spl
| ~ sQ0_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f1409,f1412,f108,f1394]) ).
fof(f1416,plain,
( ~ sQ140_spl
| ~ sQ0_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f1411,f1109,f108,f1394]) ).
fof(f1418,plain,
( sQ105_spl
| ~ sQ22_spl
| ~ aSet0(sdtmndt0(xS,xx))
| ~ aSet0(xS)
| ~ aSubsetOf0(sdtmndt0(xS,xx),slcrc0) ),
inference(resolution,[status(thm)],[f381,f1111]) ).
fof(f1424,plain,
! [X0] :
( ~ sQ122_spl
| ~ sQ22_spl
| ~ aSet0(X0)
| ~ aSet0(sdtpldt0(X0,sK1_skl(xS,xS)))
| ~ aSet0(xS)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),slcrc0) ),
inference(resolution,[status(thm)],[f381,f1292]) ).
fof(f1432,plain,
! [X0,X1,X2,X3] :
( ~ sQ67_spl
| ~ sQ22_spl
| ~ sP0_prd(X2,X3,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f381,f904]) ).
fof(f1434,plain,
! [X0,X1] :
( ~ sQ77_spl
| ~ sQ22_spl
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(xS,X1)
| ~ aSet0(X0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f381,f815]) ).
fof(f1440,plain,
! [X0,X1,X2,X3] :
( ~ sQ67_spl
| ~ sQ22_spl
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f381,f904]) ).
fof(f1449,plain,
( sQ105_spl
| ~ sQ22_spl
| ~ sQ0_spl
| ~ sQ2_spl
| ~ sQ101_spl ),
inference(split_clause,[status(thm)],[f1418,f1059,f114,f108,f257,f1109]) ).
fof(f1458,definition,
! [X0] :
( sQ146_spl
<=> ( ~ aSet0(X0)
| ~ aSet0(sdtpldt0(X0,sK1_skl(xS,xS)))
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(xS,xS)),slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1461,plain,
( ~ sQ122_spl
| ~ sQ22_spl
| ~ sQ2_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f1424,f1458,f114,f257,f1291]) ).
fof(f1468,definition,
! [X0,X1,X2,X3] :
( sQ147_spl
<=> ( ~ sP0_prd(X2,X3,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1471,plain,
( ~ sQ67_spl
| ~ sQ22_spl
| ~ sQ6_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f1432,f1468,f128,f257,f745]) ).
fof(f1476,definition,
! [X0,X1] :
( sQ149_spl
<=> ( ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(xS,X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1479,plain,
( ~ sQ77_spl
| ~ sQ22_spl
| ~ sQ6_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1434,f1476,f128,f257,f814]) ).
fof(f1485,definition,
! [X0,X2,X3] :
( sQ150_spl
<=> ( ~ sP0_prd(X2,X3,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,slcrc0) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1488,plain,
( ~ sQ67_spl
| ~ sQ22_spl
| sQ86_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f1440,f1485,f907,f257,f745]) ).
fof(f1494,plain,
! [X0] :
( sQ123_spl
| ~ aElementOf0(sK1_skl(xS,xS),X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1296,f28]) ).
fof(f1506,plain,
! [X0,X1] :
( sQ123_spl
| ~ aElementOf0(sK1_skl(xS,xS),X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1494,f50]) ).
fof(f1514,plain,
! [X0,X1] :
( sQ123_spl
| ~ aElementOf0(sK1_skl(xS,xS),X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1506]) ).
fof(f1527,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| sK2_skl(slcrc0,X1,X0) = X1
| ~ aSet0(slcrc0)
| slcrc0 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f457,f95]) ).
fof(f1531,definition,
! [X0,X1] :
( sQ153_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| sK2_skl(slcrc0,X1,X0) = X1
| slcrc0 = sdtpldt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1534,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f1527,f1531,f128,f257]) ).
fof(f1574,plain,
( ~ sQ105_spl
| sQ123_spl
| ~ aElementOf0(sK1_skl(xS,xS),sdtmndt0(xS,xx))
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1514,f1110]) ).
fof(f1575,plain,
( ~ sQ96_spl
| sQ123_spl
| ~ aElementOf0(sK1_skl(xS,xS),xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1514,f1021]) ).
fof(f1576,plain,
( ~ sQ61_spl
| sQ123_spl
| ~ aElementOf0(sK1_skl(xS,xS),slcrc0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1514,f692]) ).
fof(f1578,plain,
! [X0,X1] :
( ~ sQ22_spl
| sQ123_spl
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aElementOf0(sK1_skl(xS,xS),X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1514,f381]) ).
fof(f1589,definition,
( sQ158_spl
<=> aElementOf0(sK1_skl(xS,xS),sdtmndt0(xS,xx)) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f1592,plain,
( ~ sQ105_spl
| sQ123_spl
| ~ sQ158_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1574,f114,f1589,f1294,f1109]) ).
fof(f1593,plain,
( ~ sQ96_spl
| sQ123_spl
| ~ sQ91_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1575,f114,f990,f1294,f1020]) ).
fof(f1594,definition,
( sQ159_spl
<=> aElementOf0(sK1_skl(xS,xS),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1597,plain,
( ~ sQ61_spl
| sQ123_spl
| ~ sQ159_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1576,f128,f1594,f1294,f691]) ).
fof(f1599,definition,
! [X1] :
( sQ160_spl
<=> ( ~ aSet0(X1)
| ~ aSubsetOf0(X1,slcrc0)
| ~ aElementOf0(sK1_skl(xS,xS),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1602,plain,
( ~ sQ22_spl
| sQ123_spl
| sQ160_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1578,f275,f1599,f1294,f257]) ).
fof(f1653,plain,
( sQ29_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),slcrc0)
| ~ aElement0(xx)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f308,f141]) ).
fof(f1654,plain,
! [X0] :
( sQ29_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,sdtpldt0(slcrc0,xx))
| ~ aSet0(sdtpldt0(slcrc0,xx)) ),
inference(resolution,[status(thm)],[f308,f50]) ).
fof(f1655,plain,
! [X0] :
( sQ29_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = X0
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtpldt0(slcrc0,xx),X0))
| ~ aElement0(X0)
| ~ aSet0(sdtpldt0(slcrc0,xx)) ),
inference(resolution,[status(thm)],[f308,f99]) ).
fof(f1657,definition,
( sQ162_spl
<=> aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1660,plain,
( sQ29_spl
| ~ sQ162_spl
| ~ sQ1_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1653,f128,f111,f1657,f306]) ).
fof(f1661,definition,
( sQ163_spl
<=> aSet0(sdtpldt0(slcrc0,xx)) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
( sQ163_spl
| ~ aSet0(sdtpldt0(slcrc0,xx)) ),
inference(component_clause,[status(thm)],[f1661]) ).
fof(f1664,definition,
! [X0] :
( sQ164_spl
<=> ( ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),X0)
| ~ aSubsetOf0(X0,sdtpldt0(slcrc0,xx)) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1667,plain,
( sQ29_spl
| sQ164_spl
| ~ sQ163_spl ),
inference(split_clause,[status(thm)],[f1654,f1661,f1664,f306]) ).
fof(f1668,definition,
! [X0] :
( sQ165_spl
<=> ( sK2_skl(xS,xx,sdtmndt0(xS,xx)) = X0
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtpldt0(slcrc0,xx),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1671,plain,
( sQ29_spl
| sQ165_spl
| ~ sQ163_spl ),
inference(split_clause,[status(thm)],[f1655,f1661,f1668,f306]) ).
fof(f1672,plain,
! [X0] :
( sQ16_spl
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx)))
| ~ aSet0(X0)
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtmndt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))),xx))
| ~ aElement0(xx) ),
inference(resolution,[status(thm)],[f547,f202]) ).
fof(f1673,plain,
! [X0] :
( ~ aElement0(sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSet0(X0)
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(sdtmndt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)),xS))
| ~ aElement0(xS) ),
inference(resolution,[status(thm)],[f547,f87]) ).
fof(f1674,plain,
! [X0] :
( sQ16_spl
| ~ aElement0(xx)
| ~ aSet0(X0)
| ~ aElementOf0(xx,sdtpldt0(sdtmndt0(X0,xx),sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx))) ),
inference(resolution,[status(thm)],[f547,f202]) ).
fof(f1675,plain,
! [X0] :
( ~ aElement0(xS)
| ~ aSet0(X0)
| ~ aElementOf0(xS,sdtpldt0(sdtmndt0(X0,xS),sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aElement0(sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(resolution,[status(thm)],[f547,f87]) ).
fof(f1676,definition,
! [X0] :
( sQ166_spl
<=> ( ~ aSet0(X0)
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(sdtmndt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))),xx)) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1679,plain,
( sQ16_spl
| ~ sQ4_spl
| sQ166_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1672,f111,f1676,f120,f200]) ).
fof(f1680,definition,
! [X0] :
( sQ167_spl
<=> ( ~ aSet0(X0)
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(sdtmndt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)),xS)) ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f1683,plain,
( ~ sQ14_spl
| sQ167_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1673,f180,f1680,f187]) ).
fof(f1684,definition,
! [X0] :
( sQ168_spl
<=> ( ~ aSet0(X0)
| ~ aElementOf0(xx,sdtpldt0(sdtmndt0(X0,xx),sK2_skl(xS,xx,sdtmndt0(xS,xx)))) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1687,plain,
( sQ16_spl
| ~ sQ1_spl
| sQ168_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1674,f120,f1684,f111,f200]) ).
fof(f1688,definition,
! [X0] :
( sQ169_spl
<=> ( ~ aSet0(X0)
| ~ aElementOf0(xS,sdtpldt0(sdtmndt0(X0,xS),sdtpldt0(sdtmndt0(xS,xx),xx))) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1691,plain,
( ~ sQ12_spl
| sQ169_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1675,f187,f1688,f180]) ).
fof(f1692,plain,
( sQ163_spl
| ~ aElement0(xx)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1663,f97]) ).
fof(f1694,plain,
( sQ163_spl
| ~ sQ1_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1692,f128,f111,f1661]) ).
fof(f1748,plain,
! [X0,X1,X2,X3] :
( ~ sQ22_spl
| ~ sQ90_spl
| ~ aSet0(X3)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f926,f381]) ).
fof(f1749,plain,
! [X0,X1,X2,X3] :
( ~ sQ90_spl
| ~ aElementOf0(sK1_skl(X3,slcrc0),slcrc0)
| ~ aSet0(X3)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f926,f52]) ).
fof(f1750,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ90_spl
| ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X3,X4)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f926,f722]) ).
fof(f1783,definition,
! [X0,X1,X2,X3] :
( sQ172_spl
<=> ( ~ aSet0(X3)
| ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1786,plain,
( ~ sQ22_spl
| ~ sQ90_spl
| ~ sQ6_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f1748,f1783,f128,f925,f257]) ).
fof(f1787,definition,
! [X0,X1,X2,X3] :
( sQ173_spl
<=> ( ~ aElementOf0(sK1_skl(X3,slcrc0),slcrc0)
| ~ aSet0(X3)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1790,plain,
( ~ sQ90_spl
| ~ sQ6_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f1749,f1787,f128,f925]) ).
fof(f1791,definition,
! [X0,X1,X2,X3,X4] :
( sQ174_spl
<=> ( ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X3,X4)
| ~ aSubsetOf0(X1,X3)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1794,plain,
( ~ sQ90_spl
| ~ sQ6_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f1750,f1791,f128,f925]) ).
fof(f1798,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ aSubsetOf0(X1,slcrc0)
| ~ aSet0(X1)
| X1 = sdtmndt0(slcrc0,X0)
| ~ aElement0(X0)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f473,f139]) ).
fof(f1801,definition,
! [X0,X1] :
( sQ175_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| ~ aSet0(X1)
| X1 = sdtmndt0(slcrc0,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f1804,plain,
( ~ sQ22_spl
| sQ175_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1798,f128,f1801,f257]) ).
fof(f1813,plain,
! [X0] :
( sQ16_spl
| ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(X0,xx))
| ~ aElement0(xx)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f545,f202]) ).
fof(f1814,plain,
! [X0] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(X0,xS))
| ~ aElement0(xS)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f545,f87]) ).
fof(f1815,plain,
! [X0] :
( sQ16_spl
| ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(xx,sdtpldt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx)))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f545,f202]) ).
fof(f1816,plain,
! [X0] :
( ~ sQ22_spl
| ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(xS,sdtpldt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aElement0(sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f545,f87]) ).
fof(f1817,definition,
! [X0] :
( sQ176_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtpldt0(X0,xx))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1820,plain,
( sQ16_spl
| ~ sQ22_spl
| ~ sQ1_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f1813,f1817,f111,f257,f200]) ).
fof(f1821,definition,
! [X0] :
( sQ177_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(X0,xS))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1824,plain,
( ~ sQ22_spl
| ~ sQ12_spl
| sQ177_spl ),
inference(split_clause,[status(thm)],[f1814,f1821,f180,f257]) ).
fof(f1825,definition,
! [X0] :
( sQ178_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(xx,sdtpldt0(X0,sK2_skl(xS,xx,sdtmndt0(xS,xx))))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1828,plain,
( sQ16_spl
| ~ sQ22_spl
| ~ sQ4_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f1815,f1825,f120,f257,f200]) ).
fof(f1829,definition,
! [X0] :
( sQ179_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| ~ aElementOf0(xS,sdtpldt0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1832,plain,
( ~ sQ22_spl
| ~ sQ14_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f1816,f1829,f187,f257]) ).
fof(f1934,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aSet0(sdtmndt0(X0,X1))
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(sdtmndt0(X0,X1),slcrc0)
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f552,f381]) ).
fof(f1935,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(X0,X1),slcrc0),slcrc0)
| ~ aSet0(sdtmndt0(X0,X1))
| ~ aSet0(slcrc0)
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f552,f52]) ).
fof(f1936,plain,
! [X0,X1,X2,X3] :
( ~ sQ22_spl
| ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(sdtmndt0(X0,X1),X3)
| ~ aSet0(slcrc0)
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f552,f722]) ).
fof(f1942,definition,
! [X0,X1,X2] :
( sQ190_spl
<=> ( ~ aSet0(sdtmndt0(X0,X1))
| ~ aSubsetOf0(sdtmndt0(X0,X1),slcrc0)
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1945,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f1934,f1942,f128,f257]) ).
fof(f1946,definition,
! [X0,X1,X2] :
( sQ191_spl
<=> ( ~ aElementOf0(sK1_skl(sdtmndt0(X0,X1),slcrc0),slcrc0)
| ~ aSet0(sdtmndt0(X0,X1))
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f1949,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f1935,f1946,f128,f257]) ).
fof(f1950,definition,
! [X0,X1,X2,X3] :
( sQ192_spl
<=> ( ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(sdtmndt0(X0,X1),X3)
| ~ sP0_prd(X2,X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1953,plain,
( ~ sQ22_spl
| ~ sQ6_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f1936,f1950,f128,f257]) ).
fof(f1959,plain,
! [X0,X1,X2] :
( ~ sQ95_spl
| ~ aElementOf0(sK1_skl(xS,X0),X0)
| ~ aSet0(xS)
| ~ aSet0(X0)
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f1016,f52]) ).
fof(f1995,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| ~ sQ95_spl
| ~ aSet0(X2)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f1016,f381]) ).
fof(f1996,plain,
! [X0,X1,X2] :
( ~ sQ95_spl
| ~ aElementOf0(sK1_skl(X2,slcrc0),slcrc0)
| ~ aSet0(X2)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f1016,f52]) ).
fof(f1997,plain,
! [X0,X1,X2,X3] :
( ~ sQ95_spl
| ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X2,X3)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ),
inference(resolution,[status(thm)],[f1016,f722]) ).
fof(f2006,definition,
! [X0,X1,X2] :
( sQ194_spl
<=> ( ~ aElementOf0(sK1_skl(xS,X0),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2009,plain,
( ~ sQ95_spl
| ~ sQ2_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f1959,f2006,f114,f1015]) ).
fof(f2038,definition,
! [X0,X1,X2] :
( sQ196_spl
<=> ( ~ aSet0(X2)
| ~ aSubsetOf0(X2,slcrc0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2041,plain,
( ~ sQ22_spl
| ~ sQ95_spl
| ~ sQ6_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f1995,f2038,f128,f1015,f257]) ).
fof(f2042,definition,
! [X0,X1,X2] :
( sQ197_spl
<=> ( ~ aElementOf0(sK1_skl(X2,slcrc0),slcrc0)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f2045,plain,
( ~ sQ95_spl
| ~ sQ6_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f1996,f2042,f128,f1015]) ).
fof(f2046,definition,
! [X0,X1,X2,X3] :
( sQ198_spl
<=> ( ~ aSubsetOf0(X3,slcrc0)
| ~ aSubsetOf0(X2,X3)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f2049,plain,
( ~ sQ95_spl
| ~ sQ6_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f1997,f2046,f128,f1015]) ).
fof(f2052,plain,
( sQ13_spl
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),slcrc0)
| ~ aElement0(xS)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f185,f141]) ).
fof(f2053,plain,
! [X0] :
( sQ13_spl
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),X0)
| ~ aSubsetOf0(X0,sdtpldt0(slcrc0,xS))
| ~ aSet0(sdtpldt0(slcrc0,xS)) ),
inference(resolution,[status(thm)],[f185,f50]) ).
fof(f2054,plain,
! [X0] :
( sQ13_spl
| sdtpldt0(sdtmndt0(xS,xx),xx) = X0
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(sdtpldt0(slcrc0,xS),X0))
| ~ aElement0(X0)
| ~ aSet0(sdtpldt0(slcrc0,xS)) ),
inference(resolution,[status(thm)],[f185,f99]) ).
fof(f2056,definition,
( sQ199_spl
<=> aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f2059,plain,
( sQ13_spl
| ~ sQ199_spl
| ~ sQ12_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2052,f128,f180,f2056,f183]) ).
fof(f2060,definition,
( sQ200_spl
<=> aSet0(sdtpldt0(slcrc0,xS)) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f2062,plain,
( sQ200_spl
| ~ aSet0(sdtpldt0(slcrc0,xS)) ),
inference(component_clause,[status(thm)],[f2060]) ).
fof(f2063,definition,
! [X0] :
( sQ201_spl
<=> ( ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),X0)
| ~ aSubsetOf0(X0,sdtpldt0(slcrc0,xS)) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f2066,plain,
( sQ13_spl
| sQ201_spl
| ~ sQ200_spl ),
inference(split_clause,[status(thm)],[f2053,f2060,f2063,f183]) ).
fof(f2067,definition,
! [X0] :
( sQ202_spl
<=> ( sdtpldt0(sdtmndt0(xS,xx),xx) = X0
| ~ aElementOf0(sdtpldt0(sdtmndt0(xS,xx),xx),sdtpldt0(sdtpldt0(slcrc0,xS),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f2070,plain,
( sQ13_spl
| sQ202_spl
| ~ sQ200_spl ),
inference(split_clause,[status(thm)],[f2054,f2060,f2067,f183]) ).
fof(f2071,plain,
( sQ200_spl
| ~ aElement0(xS)
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f2062,f97]) ).
fof(f2073,plain,
( sQ200_spl
| ~ sQ12_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2071,f128,f180,f2060]) ).
fof(f2106,plain,
! [X0,X1,X2] :
( ~ sQ121_spl
| ~ aSet0(slcrc0)
| ~ sP0_prd(X1,X2,X0)
| ~ aSubsetOf0(X0,slcrc0) ),
inference(resolution,[status(thm)],[f1273,f56]) ).
fof(f2110,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ22_spl
| ~ sQ121_spl
| ~ aSet0(X4)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f1273,f381]) ).
fof(f2111,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ121_spl
| ~ aElementOf0(sK1_skl(X4,slcrc0),slcrc0)
| ~ aSet0(X4)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f1273,f52]) ).
fof(f2112,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ121_spl
| ~ aSubsetOf0(X5,slcrc0)
| ~ aSubsetOf0(X4,X5)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f1273,f722]) ).
fof(f2113,plain,
! [X0,X1,X2,X3] :
( ~ sQ121_spl
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X1,slcrc0)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(resolution,[status(thm)],[f1273,f56]) ).
fof(f2141,plain,
( ~ sQ121_spl
| ~ sQ6_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2106,f1264,f128,f1272]) ).
fof(f2142,definition,
! [X0,X1,X2,X3] :
( sQ205_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f2146,definition,
! [X0,X1,X2,X3,X4] :
( sQ206_spl
<=> ( ~ aSet0(X4)
| ~ aSubsetOf0(X4,slcrc0)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f2149,plain,
( ~ sQ22_spl
| ~ sQ121_spl
| ~ sQ6_spl
| sQ206_spl ),
inference(split_clause,[status(thm)],[f2110,f2146,f128,f1272,f257]) ).
fof(f2150,definition,
! [X0,X1,X2,X3,X4] :
( sQ207_spl
<=> ( ~ aElementOf0(sK1_skl(X4,slcrc0),slcrc0)
| ~ aSet0(X4)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f2153,plain,
( ~ sQ121_spl
| ~ sQ6_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f2111,f2150,f128,f1272]) ).
fof(f2154,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ208_spl
<=> ( ~ aSubsetOf0(X5,slcrc0)
| ~ aSubsetOf0(X4,X5)
| ~ aSubsetOf0(X1,X4)
| ~ sP0_prd(X2,X3,X0)
| ~ aSubsetOf0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f2157,plain,
( ~ sQ121_spl
| ~ sQ6_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f2112,f2154,f128,f1272]) ).
fof(f2158,plain,
( ~ sQ121_spl
| ~ sQ6_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f2113,f2142,f128,f1272]) ).
fof(f2160,plain,
( sQ132_spl
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx)))
| ~ aSet0(slcrc0) ),
inference(resolution,[status(thm)],[f1353,f97]) ).
fof(f2162,plain,
( sQ132_spl
| ~ sQ4_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2160,f128,f120,f1351]) ).
fof(f2165,plain,
! [X0] :
( ~ sQ141_spl
| ~ aElement0(sK1_skl(sdtmndt0(xS,xx),xS))
| ~ aSet0(X0)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(sdtmndt0(xS,xx),xS)),xS) ),
inference(resolution,[status(thm)],[f1402,f102]) ).
fof(f2171,definition,
! [X0] :
( sQ209_spl
<=> ( ~ aSet0(X0)
| ~ aSubsetOf0(sdtpldt0(X0,sK1_skl(sdtmndt0(xS,xx),xS)),xS) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f2174,definition,
( sQ210_spl
<=> aElement0(sK1_skl(sdtmndt0(xS,xx),xS)) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f2177,plain,
( ~ sQ141_spl
| ~ sQ210_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f2165,f2171,f2174,f1401]) ).
fof(f2178,plain,
( sQ9_spl
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),sdtmndt0(xS,xx))
| ~ aElement0(xx)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f152,f104]) ).
fof(f2179,plain,
( sQ9_spl
| sK2_skl(xS,xx,sdtmndt0(xS,xx)) = xx
| ~ aElementOf0(sK2_skl(xS,xx,sdtmndt0(xS,xx)),xS)
| ~ aElement0(sK2_skl(xS,xx,sdtmndt0(xS,xx))) ),
inference(resolution,[status(thm)],[f152,f93]) ).
fof(f2180,plain,
( sQ9_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2178,f114,f111,f123,f150]) ).
fof(f2181,plain,
( sQ9_spl
| sQ16_spl
| ~ sQ3_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2179,f120,f117,f200,f150]) ).
fof(f2209,plain,
! [X0] :
( sQ139_spl
| ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),sdtmndt0(xS,X0))
| ~ aElement0(X0)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f1400,f104]) ).
fof(f2211,definition,
! [X0] :
( sQ211_spl
<=> ( ~ aElementOf0(sK1_skl(sdtmndt0(xS,xx),xS),sdtmndt0(xS,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2214,plain,
( sQ139_spl
| sQ211_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2209,f114,f2211,f1390]) ).
fof(f2257,plain,
( ~ sQ9_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f151,f285]) ).
fof(f2258,plain,
( ~ sQ9_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f2257]) ).
fof(f2259,plain,
$false,
inference(sat_refutation,[status(thm)],[f134,f136,f146,f153,f157,f164,f166,f172,f186,f193,f203,f209,f226,f260,f266,f290,f309,f313,f321,f323,f344,f357,f361,f365,f368,f373,f393,f394,f399,f420,f424,f434,f442,f459,f479,f483,f495,f520,f527,f540,f625,f634,f638,f642,f646,f698,f721,f736,f744,f748,f762,f807,f813,f817,f828,f924,f928,f940,f966,f997,f1014,f1018,f1039,f1051,f1058,f1062,f1095,f1112,f1113,f1123,f1138,f1157,f1161,f1164,f1165,f1180,f1193,f1203,f1207,f1213,f1217,f1221,f1222,f1227,f1263,f1271,f1275,f1297,f1305,f1309,f1313,f1317,f1328,f1350,f1357,f1361,f1373,f1377,f1387,f1393,f1397,f1404,f1408,f1415,f1416,f1449,f1461,f1471,f1479,f1488,f1534,f1592,f1593,f1597,f1602,f1660,f1667,f1671,f1679,f1683,f1687,f1691,f1694,f1786,f1790,f1794,f1804,f1820,f1824,f1828,f1832,f1945,f1949,f1953,f2009,f2041,f2045,f2049,f2059,f2066,f2070,f2073,f2141,f2149,f2153,f2157,f2158,f2162,f2177,f2180,f2181,f2214,f2258]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM534+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n019.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 02:38:19 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.14/0.50 % Refutation found
% 0.14/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.52 % Elapsed time: 0.158964 seconds
% 0.14/0.52 % CPU time: 0.964039 seconds
% 0.14/0.52 % Total memory used: 97.644 MB
% 0.14/0.52 % Net memory used: 95.494 MB
%------------------------------------------------------------------------------