%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM583+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:41:05 PM UTC 2026
% Result : Theorem 5.33s 1.29s
% Output : CNFRefutation 5.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 63
% Syntax : Number of formulae : 290 ( 69 unt; 42 def)
% Number of atoms : 1073 ( 149 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 1159 ( 376 ~; 359 |; 325 &)
% ( 64 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 37 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 12 con; 0-3 aty)
% Number of variables : 259 ( 238 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> W0 != slcrc0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> W0 != szszuzczcdt0(W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [W0] :
( aSet0(W0)
=> aElement0(sbrdtbr0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,definition,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sbrdtbr0(slbdtrb0(W0)) = W0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(W0,xT) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
=> aElementOf0(W0,szDzozmdt0(xc)) )
& ( aElementOf0(W0,szDzozmdt0(xc))
=> ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
& aFunction0(xc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
xK != sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,hypothesis,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,hypothesis,
( aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,xS) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,conjecture,
( ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> ( aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)
| ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
=> aElementOf0(W0,xS) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
~ ( ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> ( aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)
| ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
=> aElementOf0(W0,xS) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f89]) ).
fof(f97,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f98,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f101,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f102,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f102]) ).
fof(f104,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))],[f103]) ).
fof(f105,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f113,plain,
! [W0] :
( W0 != slcrc0
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f114,plain,
! [X0] :
( X0 != slcrc0
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,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(f116,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)],[f115]) ).
fof(f117,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)],[f116]) ).
fof(f118,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))],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f144,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(f145,definition,
! [W0,W1,W3] :
( sP0_prd(W3,W1,W0)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f146,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)],[f144,f145]) ).
fof(f147,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)],[f146]) ).
fof(f148,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)],[f147]) ).
fof(f149,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))],[f148]) ).
fof(f151,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)],[f149]) ).
fof(f167,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f168,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f169,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f170,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f171,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
! [X0] :
( szszuzczcdt0(X0) != sz00
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f179,plain,
! [W0] :
( W0 != szszuzczcdt0(W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f180,plain,
! [X0] :
( X0 != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f205,plain,
! [W0] :
( aElement0(sbrdtbr0(W0))
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f206,plain,
! [X0] :
( aElement0(sbrdtbr0(X0))
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f243,plain,
! [W0] :
( ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f244,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| aElementOf0(W2,W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ( ( ! [W2] :
( ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) ) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f243]) ).
fof(f245,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| aElementOf0(W2,W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ! [W1] :
( ( ! [W2] :
( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f244]) ).
fof(f246,plain,
! [W0] :
( ( ! [W1] :
( ( ( ( sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)
& aElementOf0(sK8_skl(W1,W0),szNzAzT0) )
| aElementOf0(sK8_skl(W1,W0),W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)
| ~ aElementOf0(sK8_skl(W1,W0),szNzAzT0)
| ~ aElementOf0(sK8_skl(W1,W0),W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ! [W1] :
( ( ! [W2] :
( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W2,sK8_skl(W1,W0))],[f245]) ).
fof(f247,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f270,plain,
! [W0] :
( sbrdtbr0(slbdtrb0(W0)) = W0
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f271,plain,
! [X0] :
( sbrdtbr0(slbdtrb0(X0)) = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f299,plain,
! [W0] :
( aSet0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f300,plain,
! [X0] :
( aSet0(szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f347,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f349,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f350,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f351,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f353,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f354,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f355,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) ) )
& aFunction0(xc) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f356,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ( ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) ) )
& aFunction0(xc) ),
inference(NNF_transformation,[status(thm)],[f355]) ).
fof(f357,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ! [W0] :
( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) )
& aFunction0(xc) ),
inference(miniscoping,[status(thm)],[f356]) ).
fof(f358,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( sdtlpdtrp0(xc,sK20_skl(W0)) = W0
& aElementOf0(sK20_skl(W0),szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ( ~ aElementOf0(sK19_skl(W0),xS)
& aElementOf0(sK19_skl(W0),W0) )
| ~ aSet0(W0) ) ) )
& ! [W0] :
( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) )
& aFunction0(xc) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0))],[f357]) ).
fof(f359,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f383,plain,
xK != sz00,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f385,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f386,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f387,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f388,definition,
! [W0] :
( sP4_prd(W0)
<=> ( ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f389,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(formula_renaming,[status(thm)],[f387,f388]) ).
fof(f390,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( ( W1 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0))
| ~ aElement0(W1)
| aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) )
| ~ aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(NNF_transformation,[status(thm)],[f389]) ).
fof(f391,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( W1 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0))
| ~ aElement0(W1)
| aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W1] :
( ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) )
| ~ aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(miniscoping,[status(thm)],[f390]) ).
fof(f392,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f394,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f421,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f422,plain,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ)
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f423,plain,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ)
& ! [W0] :
( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi))
| ~ aElement0(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) )
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(NNF_transformation,[status(thm)],[f422]) ).
fof(f424,plain,
( aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))
& sbrdtbr0(xQ) = xk
& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ)
& ! [W0] :
( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi))
| ~ aElement0(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(W0,sdtlpdtrp0(xN,xi))
& aElement0(W0) )
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(miniscoping,[status(thm)],[f423]) ).
fof(f425,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f427,plain,
aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f432,plain,
aSet0(xQ),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f433,plain,
! [X0] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f437,plain,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f438,plain,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK
& ! [W0] :
( ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(NNF_transformation,[status(thm)],[f437]) ).
fof(f439,plain,
( sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(miniscoping,[status(thm)],[f438]) ).
fof(f444,plain,
! [X0] :
( X0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X0,xQ)
| ~ aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f448,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
& ! [W0] :
( aElementOf0(W0,xS)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f450,plain,
aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
inference(cnf_transformation,[status(thm)],[f448]) ).
fof(f451,plain,
( ~ aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)
& ? [W0] :
( ~ aElementOf0(W0,xS)
& aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f452,plain,
( ~ aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)
& ? [W0] :
( ~ aElementOf0(W0,xS)
& aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(NNF_transformation,[status(thm)],[f451]) ).
fof(f453,plain,
( ~ aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)
& ? [W0] :
( ~ aElementOf0(W0,xS)
& aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(miniscoping,[status(thm)],[f452]) ).
fof(f454,plain,
( ~ aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)
& ~ aElementOf0(sK24_skl,xS)
& aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& ~ aElementOf0(W0,xQ) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& ! [W0] :
( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(W0,xQ) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f453]) ).
fof(f462,plain,
aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f463,plain,
~ aElementOf0(sK24_skl,xS),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f465,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)],[f145]) ).
fof(f466,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)],[f465]) ).
fof(f468,plain,
! [X0,X1,X2] :
( aElementOf0(X0,X2)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f540,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f105]) ).
fof(f541,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f106]) ).
fof(f542,plain,
( ~ isCountable0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f114]) ).
fof(f543,plain,
~ isCountable0(slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f542,f540]) ).
fof(f557,plain,
! [X0,X1,X2] :
( sP0_prd(X2,X1,X0)
| ~ aElementOf0(X2,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f151]) ).
fof(f565,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f247]) ).
fof(f618,definition,
( sQ2_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f620,plain,
( sQ2_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f618]) ).
fof(f625,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f620,f167]) ).
fof(f626,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f625]) ).
fof(f627,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f119,f353]) ).
fof(f629,definition,
( sQ4_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f627,f618,f629]) ).
fof(f636,plain,
! [X0] :
( ~ aElementOf0(sK24_skl,X0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f120,f463]) ).
fof(f640,definition,
! [X0] :
( sQ5_spl
<=> ( ~ aElementOf0(sK24_skl,X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f641,plain,
! [X0] :
( ~ sQ5_spl
| ~ aElementOf0(sK24_skl,X0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f640]) ).
fof(f643,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f636,f629,f640]) ).
fof(f655,definition,
( sQ8_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ8_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f662,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f540]) ).
fof(f663,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f662]) ).
fof(f735,definition,
( sQ22_spl
<=> xS = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f736,plain,
( ~ sQ22_spl
| xS = slcrc0 ),
inference(component_clause,[status(thm)],[f735]) ).
fof(f743,plain,
( ~ sQ5_spl
| ~ aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)) ),
inference(resolution,[status(thm)],[f450,f641]) ).
fof(f746,plain,
( aSet0(sdtlpdtrp0(xN,xi))
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f450,f119]) ).
fof(f758,definition,
( sQ27_spl
<=> aSet0(sdtlpdtrp0(xN,xi)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( sQ27_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f746,f629,f758]) ).
fof(f773,definition,
( sQ30_spl
<=> aSet0(szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f775,plain,
( sQ30_spl
| ~ aSet0(szDzozmdt0(xc)) ),
inference(component_clause,[status(thm)],[f773]) ).
fof(f792,definition,
( sQ34_spl
<=> aSet0(xQ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f794,plain,
( sQ34_spl
| ~ aSet0(xQ) ),
inference(component_clause,[status(thm)],[f792]) ).
fof(f795,definition,
( sQ35_spl
<=> aElement0(szmzizndt0(sdtlpdtrp0(xN,xi))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f805,definition,
( sQ36_spl
<=> aElementOf0(sK24_skl,xQ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( ~ sQ36_spl
| aElementOf0(sK24_skl,xQ) ),
inference(component_clause,[status(thm)],[f805]) ).
fof(f808,definition,
( sQ37_spl
<=> sK24_skl = szmzizndt0(sdtlpdtrp0(xN,xi)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f809,plain,
( ~ sQ37_spl
| sK24_skl = szmzizndt0(sdtlpdtrp0(xN,xi)) ),
inference(component_clause,[status(thm)],[f808]) ).
fof(f829,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f794,f432]) ).
fof(f830,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f829]) ).
fof(f835,plain,
( sQ30_spl
| ~ aFunction0(xc) ),
inference(resolution,[status(thm)],[f300,f775]) ).
fof(f837,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f835,f359]) ).
fof(f838,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f837]) ).
fof(f839,definition,
( sQ41_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( sQ41_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f839]) ).
fof(f859,plain,
xk != szszuzczcdt0(xk),
inference(resolution,[status(thm)],[f180,f385]) ).
fof(f864,plain,
xi != szszuzczcdt0(xi),
inference(resolution,[status(thm)],[f180,f421]) ).
fof(f867,plain,
xk != xK,
inference(forward_demodulation,[status(thm)],[f386,f859]) ).
fof(f894,definition,
( sQ49_spl
<=> aSet0(xT) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f896,plain,
( sQ49_spl
| ~ aSet0(xT) ),
inference(component_clause,[status(thm)],[f894]) ).
fof(f905,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f896,f347]) ).
fof(f906,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f905]) ).
fof(f950,plain,
( ~ sQ22_spl
| ~ isCountable0(xS) ),
inference(backward_demodulation,[status(thm)],[f736,f543]) ).
fof(f972,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f950,f354]) ).
fof(f973,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f972]) ).
fof(f1034,definition,
( sQ62_spl
<=> aFunction0(xc) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1036,plain,
( sQ62_spl
| ~ aFunction0(xc) ),
inference(component_clause,[status(thm)],[f1034]) ).
fof(f1084,definition,
( sQ65_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1086,plain,
( sQ65_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1084]) ).
fof(f1091,plain,
( sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f385]) ).
fof(f1092,plain,
sQ65_spl,
inference(contradiction_clause,[status(thm)],[f1091]) ).
fof(f1153,definition,
( sQ70_spl
<=> aElementOf0(sz00,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1155,plain,
( sQ70_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1153]) ).
fof(f1160,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1155,f169]) ).
fof(f1161,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1160]) ).
fof(f1231,definition,
( sQ78_spl
<=> xK = sz00 ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1232,plain,
( ~ sQ78_spl
| xK = sz00 ),
inference(component_clause,[status(thm)],[f1231]) ).
fof(f1287,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1232,f383]) ).
fof(f1288,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1287]) ).
fof(f1411,definition,
( sQ86_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1413,plain,
( sQ86_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1411]) ).
fof(f1483,definition,
( sQ93_spl
<=> aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1485,plain,
( sQ93_spl
| ~ aElementOf0(szszuzczcdt0(xi),szNzAzT0) ),
inference(component_clause,[status(thm)],[f1483]) ).
fof(f1497,definition,
( sQ97_spl
<=> szszuzczcdt0(xi) = xi ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1498,plain,
( ~ sQ97_spl
| szszuzczcdt0(xi) = xi ),
inference(component_clause,[status(thm)],[f1497]) ).
fof(f1509,definition,
! [X0] :
( sQ98_spl
<=> ( sz00 = X0
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1510,plain,
! [X0] :
( ~ sQ98_spl
| sz00 = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1509]) ).
fof(f1520,plain,
( sQ93_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f1485,f171]) ).
fof(f1521,plain,
( sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1520,f421]) ).
fof(f1522,plain,
sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1521]) ).
fof(f1525,plain,
! [X0] :
( ~ sQ98_spl
| ~ aElementOf0(X0,szNzAzT0)
| sz00 = szszuzczcdt0(X0) ),
inference(resolution,[status(thm)],[f1510,f171]) ).
fof(f1530,plain,
( ~ sQ98_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f169,f1538]) ).
fof(f1538,plain,
! [X0] :
( ~ sQ98_spl
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1525,f172]) ).
fof(f1542,plain,
~ sQ98_spl,
inference(contradiction_clause,[status(thm)],[f1530]) ).
fof(f1690,plain,
aSet0(slbdtrb0(xK)),
inference(resolution,[status(thm)],[f565,f349]) ).
fof(f1691,plain,
aSet0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f565,f385]) ).
fof(f1693,plain,
aSet0(slbdtrb0(xi)),
inference(resolution,[status(thm)],[f565,f421]) ).
fof(f1708,definition,
( sQ110_spl
<=> aSet0(slbdtrb0(xi)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1710,plain,
( sQ110_spl
| ~ aSet0(slbdtrb0(xi)) ),
inference(component_clause,[status(thm)],[f1708]) ).
fof(f1765,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1413,f421]) ).
fof(f1766,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f1765]) ).
fof(f1821,definition,
( sQ124_spl
<=> sbrdtbr0(slbdtrb0(xK)) = xK ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1823,plain,
( sQ124_spl
| sbrdtbr0(slbdtrb0(xK)) != xK ),
inference(component_clause,[status(thm)],[f1821]) ).
fof(f1839,definition,
( sQ129_spl
<=> aElementOf0(sK19_skl(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1840,plain,
( ~ sQ129_spl
| aElementOf0(sK19_skl(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f1839]) ).
fof(f1873,plain,
( ~ sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1840,f541]) ).
fof(f1874,plain,
~ sQ129_spl,
inference(contradiction_clause,[status(thm)],[f1873]) ).
fof(f1877,definition,
( sQ138_spl
<=> aSet0(slbdtrb0(xK)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1879,plain,
( sQ138_spl
| ~ aSet0(slbdtrb0(xK)) ),
inference(component_clause,[status(thm)],[f1877]) ).
fof(f1882,definition,
( sQ139_spl
<=> aSet0(slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1884,plain,
( sQ139_spl
| ~ aSet0(slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f1882]) ).
fof(f1974,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1036,f359]) ).
fof(f1975,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f1974]) ).
fof(f2077,plain,
( sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1710,f1693]) ).
fof(f2078,plain,
sQ110_spl,
inference(contradiction_clause,[status(thm)],[f2077]) ).
fof(f2087,plain,
( sQ138_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1879,f1690]) ).
fof(f2088,plain,
sQ138_spl,
inference(contradiction_clause,[status(thm)],[f2087]) ).
fof(f2094,plain,
( sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1884,f1691]) ).
fof(f2095,plain,
sQ139_spl,
inference(contradiction_clause,[status(thm)],[f2094]) ).
fof(f2272,plain,
sbrdtbr0(slbdtrb0(xK)) = xK,
inference(resolution,[status(thm)],[f271,f349]) ).
fof(f2364,definition,
( sQ188_spl
<=> sdtlpdtrp0(xN,xi) = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2365,plain,
( ~ sQ188_spl
| sdtlpdtrp0(xN,xi) = slcrc0 ),
inference(component_clause,[status(thm)],[f2364]) ).
fof(f2717,plain,
( sQ124_spl
| xK != xK ),
inference(forward_demodulation,[status(thm)],[f2272,f1823]) ).
fof(f2718,plain,
( sQ124_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2717]) ).
fof(f2719,plain,
sQ124_spl,
inference(contradiction_clause,[status(thm)],[f2718]) ).
fof(f2723,plain,
( aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))
| ~ aSet0(sdtlpdtrp0(xN,xi)) ),
inference(resolution,[status(thm)],[f425,f98]) ).
fof(f2726,plain,
( sQ35_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f2723,f758,f795]) ).
fof(f2731,plain,
( ~ sQ37_spl
| aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)) ),
inference(backward_demodulation,[status(thm)],[f809,f425]) ).
fof(f2754,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2731,f743]) ).
fof(f2755,plain,
( ~ sQ37_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f2754]) ).
fof(f2898,definition,
( sQ203_spl
<=> aElement0(sbrdtbr0(xS)) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2900,plain,
( sQ203_spl
| ~ aElement0(sbrdtbr0(xS)) ),
inference(component_clause,[status(thm)],[f2898]) ).
fof(f2911,plain,
( sQ203_spl
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f2900,f206]) ).
fof(f2912,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2911,f351]) ).
fof(f2913,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f2912]) ).
fof(f3079,plain,
( ~ sQ188_spl
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),slcrc0) ),
inference(backward_demodulation,[status(thm)],[f2365,f425]) ).
fof(f3462,plain,
( ~ sQ188_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3079,f541]) ).
fof(f3463,plain,
~ sQ188_spl,
inference(contradiction_clause,[status(thm)],[f3462]) ).
fof(f3660,definition,
( sQ219_spl
<=> isCountable0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f3662,plain,
( sQ219_spl
| ~ isCountable0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f3660]) ).
fof(f3670,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f841,f392]) ).
fof(f3671,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f3670]) ).
fof(f3678,plain,
( sQ219_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3662,f168]) ).
fof(f3679,plain,
sQ219_spl,
inference(contradiction_clause,[status(thm)],[f3678]) ).
fof(f4059,plain,
( ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1498,f864]) ).
fof(f4060,plain,
~ sQ97_spl,
inference(contradiction_clause,[status(thm)],[f4059]) ).
fof(f4119,definition,
! [X0] :
( sQ236_spl
<=> ( xi = X0
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f4120,plain,
! [X0] :
( ~ sQ236_spl
| xi = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f4119]) ).
fof(f4221,plain,
( ~ sQ36_spl
| aElementOf0(sK24_skl,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(resolution,[status(thm)],[f433,f806]) ).
fof(f4255,definition,
( sQ247_spl
<=> aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f4257,plain,
( sQ247_spl
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(component_clause,[status(thm)],[f4255]) ).
fof(f4267,plain,
( sQ247_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4257,f427]) ).
fof(f4268,plain,
sQ247_spl,
inference(contradiction_clause,[status(thm)],[f4267]) ).
fof(f4353,definition,
( sQ254_spl
<=> aSet0(sdtlpdtrp0(xN,sz00)) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f4355,plain,
( sQ254_spl
| ~ aSet0(sdtlpdtrp0(xN,sz00)) ),
inference(component_clause,[status(thm)],[f4353]) ).
fof(f4359,definition,
( sQ256_spl
<=> isCountable0(sdtlpdtrp0(xN,sz00)) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f4361,plain,
( sQ256_spl
| ~ isCountable0(sdtlpdtrp0(xN,sz00)) ),
inference(component_clause,[status(thm)],[f4359]) ).
fof(f4363,plain,
( sQ256_spl
| ~ isCountable0(xS) ),
inference(forward_demodulation,[status(thm)],[f394,f4361]) ).
fof(f4364,plain,
( sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4363,f354]) ).
fof(f4365,plain,
sQ256_spl,
inference(contradiction_clause,[status(thm)],[f4364]) ).
fof(f4382,plain,
( sQ254_spl
| ~ aSet0(xS) ),
inference(forward_demodulation,[status(thm)],[f394,f4355]) ).
fof(f4383,plain,
( sQ254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4382,f351]) ).
fof(f4384,plain,
sQ254_spl,
inference(contradiction_clause,[status(thm)],[f4383]) ).
fof(f4392,plain,
( sK24_skl = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(sK24_skl,xQ) ),
inference(resolution,[status(thm)],[f444,f462]) ).
fof(f4395,plain,
( sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f4392,f805,f808]) ).
fof(f4444,plain,
( ~ sQ236_spl
| xi = xk ),
inference(resolution,[status(thm)],[f4120,f385]) ).
fof(f4445,plain,
( ~ sQ236_spl
| xi = xK ),
inference(resolution,[status(thm)],[f4120,f349]) ).
fof(f4604,plain,
( ~ sQ236_spl
| xk = xK ),
inference(forward_demodulation,[status(thm)],[f4444,f4445]) ).
fof(f4605,plain,
( ~ sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4604,f867]) ).
fof(f4606,plain,
~ sQ236_spl,
inference(contradiction_clause,[status(thm)],[f4605]) ).
fof(f5289,plain,
aElementOf0(szszuzczcdt0(sz00),szNzAzT0),
inference(resolution,[status(thm)],[f171,f169]) ).
fof(f5291,plain,
aElementOf0(szszuzczcdt0(xK),szNzAzT0),
inference(resolution,[status(thm)],[f171,f349]) ).
fof(f5299,plain,
aSet0(slbdtrb0(szszuzczcdt0(sz00))),
inference(resolution,[status(thm)],[f5289,f565]) ).
fof(f5312,plain,
aSet0(slbdtrb0(szszuzczcdt0(xK))),
inference(resolution,[status(thm)],[f5291,f565]) ).
fof(f5520,definition,
( sQ344_spl
<=> aSet0(slbdtrb0(szszuzczcdt0(sz00))) ),
introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition]) ).
fof(f5522,plain,
( sQ344_spl
| ~ aSet0(slbdtrb0(szszuzczcdt0(sz00))) ),
inference(component_clause,[status(thm)],[f5520]) ).
fof(f5535,plain,
( sQ344_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5522,f5299]) ).
fof(f5536,plain,
sQ344_spl,
inference(contradiction_clause,[status(thm)],[f5535]) ).
fof(f5558,definition,
( sQ350_spl
<=> aSet0(slbdtrb0(szszuzczcdt0(xK))) ),
introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition]) ).
fof(f5560,plain,
( sQ350_spl
| ~ aSet0(slbdtrb0(szszuzczcdt0(xK))) ),
inference(component_clause,[status(thm)],[f5558]) ).
fof(f5573,plain,
( sQ350_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5560,f5312]) ).
fof(f5574,plain,
sQ350_spl,
inference(contradiction_clause,[status(thm)],[f5573]) ).
fof(f5650,plain,
( ~ sQ36_spl
| sP0_prd(sK24_skl,szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))
| ~ aSet0(sdtlpdtrp0(xN,xi)) ),
inference(resolution,[status(thm)],[f557,f4221]) ).
fof(f5651,definition,
( sQ362_spl
<=> sP0_prd(sK24_skl,szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f5652,plain,
( ~ sQ362_spl
| sP0_prd(sK24_skl,szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(component_clause,[status(thm)],[f5651]) ).
fof(f5654,plain,
( ~ sQ36_spl
| sQ362_spl
| ~ sQ35_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f5650,f758,f795,f5651,f805]) ).
fof(f5683,plain,
( ~ sQ362_spl
| aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)) ),
inference(resolution,[status(thm)],[f5652,f468]) ).
fof(f5686,plain,
( ~ sQ362_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5683,f743]) ).
fof(f5687,plain,
( ~ sQ362_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f5686]) ).
fof(f5688,plain,
$false,
inference(sat_refutation,[status(thm)],[f626,f632,f643,f663,f761,f830,f838,f906,f973,f1092,f1161,f1288,f1522,f1542,f1766,f1874,f1975,f2078,f2088,f2095,f2719,f2726,f2755,f2913,f3463,f3671,f3679,f4060,f4268,f4365,f4384,f4395,f4606,f5536,f5574,f5654,f5687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM583+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 02:41:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 5.33/1.29 % Refutation found
% 5.33/1.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.33/1.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.65/1.33 % Elapsed time: 0.941705 seconds
% 0.65/1.33 % CPU time: 7.053798 seconds
% 0.65/1.33 % Total memory used: 187.405 MB
% 0.65/1.33 % Net memory used: 180.655 MB
%------------------------------------------------------------------------------