%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM582+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 : n017.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 4.01s 1.19s
% Output : CNFRefutation 4.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 55
% Syntax : Number of formulae : 243 ( 59 unt; 35 def)
% Number of atoms : 866 ( 131 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 931 ( 308 ~; 282 |; 261 &)
% ( 51 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 32 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 12 con; 0-2 aty)
% Number of variables : 195 ( 178 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f30,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(sz00,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
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(f51,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> isFinite0(slbdtrb0(W0)) ),
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(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(f83,hypothesis,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W1,W0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> aElementOf0(W2,sdtlpdtrp0(xN,W1)) ) ) ) ),
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,conjecture,
( aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
| ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,xS) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
~ ( aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
| ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,xS) ) ),
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f100,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f101,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,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))],[f102]) ).
fof(f104,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f114,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(f115,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)],[f114]) ).
fof(f116,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)],[f115]) ).
fof(f117,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))],[f116]) ).
fof(f119,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f124,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f125,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f167,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f168,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f169,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f170,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
! [X0] :
( szszuzczcdt0(X0) != sz00
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f178,plain,
! [W0] :
( W0 != szszuzczcdt0(W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f179,plain,
! [X0] :
( X0 != szszuzczcdt0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f182,plain,
! [W0] :
( sdtlseqdt0(sz00,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f183,plain,
! [X0] :
( sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f210,plain,
! [W0] :
( ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f211,plain,
! [W0] :
( ( ( W0 != slcrc0
| sbrdtbr0(W0) = sz00 )
& ( W0 = slcrc0
| sbrdtbr0(W0) != sz00 ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f210]) ).
fof(f213,plain,
! [X0] :
( X0 != slcrc0
| sbrdtbr0(X0) = sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f242,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(f243,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)],[f242]) ).
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) )
& ! [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)],[f243]) ).
fof(f245,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))],[f244]) ).
fof(f246,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f253,plain,
! [W0] :
( isFinite0(slbdtrb0(W0))
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f254,plain,
! [X0] :
( isFinite0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f269,plain,
! [W0] :
( sbrdtbr0(slbdtrb0(W0)) = W0
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f270,plain,
! [X0] :
( sbrdtbr0(slbdtrb0(X0)) = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f348,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f349,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f350,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f353,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f354,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(f355,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ( ? [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)],[f354]) ).
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))) )
& ! [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)],[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] :
( ( 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))],[f356]) ).
fof(f358,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f362,plain,
! [X0] :
( sbrdtbr0(X0) = xK
| ~ aElementOf0(X0,szDzozmdt0(xc)) ),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f382,plain,
xK != sz00,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f384,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f386,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(f387,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(f388,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)],[f386,f387]) ).
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] :
( ( 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)],[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] :
( ( 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)],[f389]) ).
fof(f391,plain,
aFunction0(xN),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f392,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f393,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f410,plain,
! [W0,W1] :
( ( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) ) )
| ~ sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f411,plain,
! [X0,X1,X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f420,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f421,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(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] :
( ( 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)],[f421]) ).
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] :
( ( 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)],[f422]) ).
fof(f431,plain,
aSet0(xQ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f434,plain,
sbrdtbr0(xQ) = xk,
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f436,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(f437,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)],[f436]) ).
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] :
( ( ( 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)],[f437]) ).
fof(f441,plain,
aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[status(thm)],[f438]) ).
fof(f447,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
& ? [W0] :
( ~ aElementOf0(W0,xS)
& aElementOf0(W0,sdtlpdtrp0(xN,xi)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f448,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),xS)
& ~ aElementOf0(sK24_skl,xS)
& aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f447]) ).
fof(f449,plain,
aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)),
inference(cnf_transformation,[status(thm)],[f448]) ).
fof(f450,plain,
~ aElementOf0(sK24_skl,xS),
inference(cnf_transformation,[status(thm)],[f448]) ).
fof(f527,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f104]) ).
fof(f528,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f105]) ).
fof(f539,plain,
( sbrdtbr0(slcrc0) = sz00
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f213]) ).
fof(f544,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f246]) ).
fof(f581,plain,
! [X0] :
( ~ aElementOf0(sK24_skl,X0)
| ~ aSubsetOf0(X0,xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f119,f450]) ).
fof(f582,definition,
( sQ0_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f584,plain,
( sQ0_spl
| ~ aSet0(xS) ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,definition,
! [X0] :
( sQ1_spl
<=> ( ~ aElementOf0(sK24_skl,X0)
| ~ aSubsetOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f586,plain,
! [X0] :
( ~ sQ1_spl
| ~ aElementOf0(sK24_skl,X0)
| ~ aSubsetOf0(X0,xS) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f581,f582,f585]) ).
fof(f589,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f350]) ).
fof(f590,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f612,plain,
( ~ sQ1_spl
| ~ aSet0(xS)
| ~ aElementOf0(sK24_skl,xS) ),
inference(resolution,[status(thm)],[f586,f125]) ).
fof(f613,definition,
( sQ5_spl
<=> aElementOf0(sK24_skl,xS) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f616,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f612,f613,f582,f585]) ).
fof(f655,definition,
( sQ13_spl
<=> aElementOf0(sz00,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ13_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f757,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f168]) ).
fof(f758,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f757]) ).
fof(f867,plain,
xK != szszuzczcdt0(xK),
inference(resolution,[status(thm)],[f179,f348]) ).
fof(f868,plain,
sz00 != szszuzczcdt0(sz00),
inference(resolution,[status(thm)],[f179,f168]) ).
fof(f1012,plain,
szszuzczcdt0(xK) != sz00,
inference(resolution,[status(thm)],[f171,f348]) ).
fof(f1015,plain,
szszuzczcdt0(xi) != sz00,
inference(resolution,[status(thm)],[f171,f420]) ).
fof(f1191,plain,
sbrdtbr0(slcrc0) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f539,f527]) ).
fof(f1298,definition,
( sQ84_spl
<=> aElementOf0(slcrc0,szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1299,plain,
( ~ sQ84_spl
| aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(component_clause,[status(thm)],[f1298]) ).
fof(f1463,definition,
! [X1] :
( sQ106_spl
<=> ( ~ aSet0(X1)
| ~ aSet0(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1464,plain,
! [X0] :
( ~ sQ106_spl
| ~ aSet0(X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f1463]) ).
fof(f1649,definition,
( sQ133_spl
<=> sbrdtbr0(slcrc0) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1651,plain,
( sQ133_spl
| sbrdtbr0(slcrc0) != sz00 ),
inference(component_clause,[status(thm)],[f1649]) ).
fof(f1925,definition,
( sQ168_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1927,plain,
( sQ168_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1925]) ).
fof(f2123,plain,
( sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1927,f420]) ).
fof(f2124,plain,
sQ168_spl,
inference(contradiction_clause,[status(thm)],[f2123]) ).
fof(f2244,definition,
( sQ210_spl
<=> aElementOf0(szszuzczcdt0(xK),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f2246,plain,
( sQ210_spl
| ~ aElementOf0(szszuzczcdt0(xK),szNzAzT0) ),
inference(component_clause,[status(thm)],[f2244]) ).
fof(f2388,definition,
( sQ226_spl
<=> aElementOf0(sbrdtbr0(xQ),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f2390,plain,
( sQ226_spl
| ~ aElementOf0(sbrdtbr0(xQ),szNzAzT0) ),
inference(component_clause,[status(thm)],[f2388]) ).
fof(f2392,plain,
( sQ226_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f434,f2390]) ).
fof(f2393,plain,
( sQ226_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2392,f384]) ).
fof(f2394,plain,
sQ226_spl,
inference(contradiction_clause,[status(thm)],[f2393]) ).
fof(f2421,plain,
( sQ210_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolution,[status(thm)],[f2246,f170]) ).
fof(f2424,plain,
( sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2421,f348]) ).
fof(f2425,plain,
sQ210_spl,
inference(contradiction_clause,[status(thm)],[f2424]) ).
fof(f2468,definition,
( sQ237_spl
<=> aElementOf0(szmzizndt0(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f2469,plain,
( ~ sQ237_spl
| aElementOf0(szmzizndt0(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f2468]) ).
fof(f2601,definition,
( sQ256_spl
<=> szszuzczcdt0(xK) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f2602,plain,
( ~ sQ256_spl
| szszuzczcdt0(xK) = sz00 ),
inference(component_clause,[status(thm)],[f2601]) ).
fof(f2608,plain,
( ~ sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2602,f1012]) ).
fof(f2609,plain,
~ sQ256_spl,
inference(contradiction_clause,[status(thm)],[f2608]) ).
fof(f2641,definition,
( sQ263_spl
<=> aElementOf0(szmzazxdt0(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f2642,plain,
( ~ sQ263_spl
| aElementOf0(szmzazxdt0(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f2641]) ).
fof(f2838,definition,
( sQ290_spl
<=> isCountable0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f2840,plain,
( sQ290_spl
| ~ isCountable0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f2838]) ).
fof(f2862,plain,
( sQ290_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2840,f167]) ).
fof(f2863,plain,
sQ290_spl,
inference(contradiction_clause,[status(thm)],[f2862]) ).
fof(f3060,definition,
( sQ305_spl
<=> szszuzczcdt0(xi) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f3061,plain,
( ~ sQ305_spl
| szszuzczcdt0(xi) = sz00 ),
inference(component_clause,[status(thm)],[f3060]) ).
fof(f3067,plain,
( ~ sQ305_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3061,f1015]) ).
fof(f3068,plain,
~ sQ305_spl,
inference(contradiction_clause,[status(thm)],[f3067]) ).
fof(f3095,definition,
( sQ307_spl
<=> szszuzczcdt0(sz00) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f3096,plain,
( ~ sQ307_spl
| szszuzczcdt0(sz00) = sz00 ),
inference(component_clause,[status(thm)],[f3095]) ).
fof(f3102,plain,
( ~ sQ307_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3096,f868]) ).
fof(f3103,plain,
~ sQ307_spl,
inference(contradiction_clause,[status(thm)],[f3102]) ).
fof(f3142,definition,
( sQ314_spl
<=> isCountable0(xS) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f3144,plain,
( sQ314_spl
| ~ isCountable0(xS) ),
inference(component_clause,[status(thm)],[f3142]) ).
fof(f3216,plain,
( sQ314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3144,f353]) ).
fof(f3217,plain,
sQ314_spl,
inference(contradiction_clause,[status(thm)],[f3216]) ).
fof(f3604,plain,
sbrdtbr0(slbdtrb0(xk)) = xk,
inference(resolution,[status(thm)],[f270,f384]) ).
fof(f3607,plain,
sbrdtbr0(slbdtrb0(xi)) = xi,
inference(resolution,[status(thm)],[f270,f420]) ).
fof(f3732,definition,
( sQ378_spl
<=> aElementOf0(sbrdtbr0(slbdtrb0(xi)),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition]) ).
fof(f3734,plain,
( sQ378_spl
| ~ aElementOf0(sbrdtbr0(slbdtrb0(xi)),szNzAzT0) ),
inference(component_clause,[status(thm)],[f3732]) ).
fof(f3794,definition,
( sQ388_spl
<=> aElementOf0(sbrdtbr0(slbdtrb0(xk)),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition]) ).
fof(f3796,plain,
( sQ388_spl
| ~ aElementOf0(sbrdtbr0(slbdtrb0(xk)),szNzAzT0) ),
inference(component_clause,[status(thm)],[f3794]) ).
fof(f3935,definition,
( sQ404_spl
<=> aSet0(slbdtrb0(xK)) ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f3937,plain,
( sQ404_spl
| ~ aSet0(slbdtrb0(xK)) ),
inference(component_clause,[status(thm)],[f3935]) ).
fof(f3938,definition,
( sQ405_spl
<=> isFinite0(slbdtrb0(xK)) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f3940,plain,
( sQ405_spl
| ~ isFinite0(slbdtrb0(xK)) ),
inference(component_clause,[status(thm)],[f3938]) ).
fof(f3951,plain,
( sQ404_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolution,[status(thm)],[f3937,f544]) ).
fof(f3953,plain,
( sQ404_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3951,f348]) ).
fof(f3954,plain,
sQ404_spl,
inference(contradiction_clause,[status(thm)],[f3953]) ).
fof(f3956,plain,
( sQ405_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolution,[status(thm)],[f3940,f254]) ).
fof(f3959,plain,
( sQ405_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3956,f348]) ).
fof(f3960,plain,
sQ405_spl,
inference(contradiction_clause,[status(thm)],[f3959]) ).
fof(f4497,definition,
( sQ479_spl
<=> szszuzczcdt0(xK) = xK ),
introduced(definition,[new_symbols(definition,[sQ479_spl])],[split_symbol_definition]) ).
fof(f4498,plain,
( ~ sQ479_spl
| szszuzczcdt0(xK) = xK ),
inference(component_clause,[status(thm)],[f4497]) ).
fof(f4557,definition,
( sQ488_spl
<=> aFunction0(xN) ),
introduced(definition,[new_symbols(definition,[sQ488_spl])],[split_symbol_definition]) ).
fof(f4559,plain,
( sQ488_spl
| ~ aFunction0(xN) ),
inference(component_clause,[status(thm)],[f4557]) ).
fof(f4560,definition,
( sQ489_spl
<=> aElementOf0(sz00,szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition]) ).
fof(f4562,plain,
( sQ489_spl
| ~ aElementOf0(sz00,szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f4560]) ).
fof(f4615,plain,
( ~ sQ237_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2469,f528]) ).
fof(f4616,plain,
~ sQ237_spl,
inference(contradiction_clause,[status(thm)],[f4615]) ).
fof(f4617,plain,
( ~ sQ263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2642,f528]) ).
fof(f4618,plain,
~ sQ263_spl,
inference(contradiction_clause,[status(thm)],[f4617]) ).
fof(f4638,plain,
( sQ489_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f392,f4562]) ).
fof(f4639,plain,
( sQ489_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4638,f168]) ).
fof(f4640,plain,
sQ489_spl,
inference(contradiction_clause,[status(thm)],[f4639]) ).
fof(f4641,plain,
( sQ488_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4559,f391]) ).
fof(f4642,plain,
sQ488_spl,
inference(contradiction_clause,[status(thm)],[f4641]) ).
fof(f4643,plain,
( ~ sQ479_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4498,f867]) ).
fof(f4644,plain,
~ sQ479_spl,
inference(contradiction_clause,[status(thm)],[f4643]) ).
fof(f4648,plain,
( sQ388_spl
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f3604,f3796]) ).
fof(f4649,plain,
( sQ388_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4648,f384]) ).
fof(f4650,plain,
sQ388_spl,
inference(contradiction_clause,[status(thm)],[f4649]) ).
fof(f4651,plain,
( sQ378_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f3607,f3734]) ).
fof(f4652,plain,
( sQ378_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4651,f420]) ).
fof(f4653,plain,
sQ378_spl,
inference(contradiction_clause,[status(thm)],[f4652]) ).
fof(f4837,plain,
( sQ133_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f1191,f1651]) ).
fof(f4838,plain,
( sQ133_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4837]) ).
fof(f4839,plain,
sQ133_spl,
inference(contradiction_clause,[status(thm)],[f4838]) ).
fof(f4840,plain,
! [X0] :
( ~ sQ106_spl
| ~ aSet0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1464]) ).
fof(f4960,definition,
( sQ505_spl
<=> sdtlseqdt0(sz00,xi) ),
introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition]) ).
fof(f4962,plain,
( sQ505_spl
| ~ sdtlseqdt0(sz00,xi) ),
inference(component_clause,[status(thm)],[f4960]) ).
fof(f5093,plain,
xi != szszuzczcdt0(xi),
inference(resolution,[status(thm)],[f420,f179]) ).
fof(f6007,definition,
( sQ594_spl
<=> aFunction0(xc) ),
introduced(definition,[new_symbols(definition,[sQ594_spl])],[split_symbol_definition]) ).
fof(f6009,plain,
( sQ594_spl
| ~ aFunction0(xc) ),
inference(component_clause,[status(thm)],[f6007]) ).
fof(f6035,plain,
( sQ594_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6009,f358]) ).
fof(f6036,plain,
sQ594_spl,
inference(contradiction_clause,[status(thm)],[f6035]) ).
fof(f6167,plain,
( ~ sQ106_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f431,f4840]) ).
fof(f6182,definition,
! [X0] :
( sQ617_spl
<=> ~ aFunction0(X0) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f6183,plain,
! [X0] :
( ~ sQ617_spl
| ~ aFunction0(X0) ),
inference(component_clause,[status(thm)],[f6182]) ).
fof(f6189,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f6167]) ).
fof(f6199,plain,
( ~ sQ617_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f391,f6183]) ).
fof(f6201,plain,
~ sQ617_spl,
inference(contradiction_clause,[status(thm)],[f6199]) ).
fof(f6713,plain,
( sQ505_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f4962,f183]) ).
fof(f6716,plain,
( sQ505_spl
| ~ sQ168_spl ),
inference(split_clause,[status(thm)],[f6713,f1925,f4960]) ).
fof(f6741,plain,
! [X0] :
( aElementOf0(sK24_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f449,f411]) ).
fof(f6745,definition,
! [X0] :
( sQ654_spl
<=> ( aElementOf0(sK24_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f6746,plain,
! [X0] :
( ~ sQ654_spl
| aElementOf0(sK24_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f6745]) ).
fof(f6748,plain,
( sQ654_spl
| ~ sQ168_spl ),
inference(split_clause,[status(thm)],[f6741,f1925,f6745]) ).
fof(f6827,plain,
( ~ sQ84_spl
| sbrdtbr0(slcrc0) = xK ),
inference(resolution,[status(thm)],[f1299,f362]) ).
fof(f6831,plain,
( ~ sQ84_spl
| sz00 = xK ),
inference(forward_demodulation,[status(thm)],[f1191,f6827]) ).
fof(f6832,plain,
( ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6831,f382]) ).
fof(f6833,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f6832]) ).
fof(f7095,definition,
( sQ685_spl
<=> szszuzczcdt0(xi) = szszuzczcdt0(xi) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f7097,plain,
( sQ685_spl
| szszuzczcdt0(xi) != szszuzczcdt0(xi) ),
inference(component_clause,[status(thm)],[f7095]) ).
fof(f7148,definition,
( sQ700_spl
<=> szszuzczcdt0(xi) = xi ),
introduced(definition,[new_symbols(definition,[sQ700_spl])],[split_symbol_definition]) ).
fof(f7149,plain,
( ~ sQ700_spl
| szszuzczcdt0(xi) = xi ),
inference(component_clause,[status(thm)],[f7148]) ).
fof(f7182,plain,
( ~ sQ700_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7149,f5093]) ).
fof(f7183,plain,
~ sQ700_spl,
inference(contradiction_clause,[status(thm)],[f7182]) ).
fof(f7184,plain,
( sQ685_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7097]) ).
fof(f7185,plain,
sQ685_spl,
inference(contradiction_clause,[status(thm)],[f7184]) ).
fof(f7438,definition,
( sQ719_spl
<=> aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
introduced(definition,[new_symbols(definition,[sQ719_spl])],[split_symbol_definition]) ).
fof(f7440,plain,
( sQ719_spl
| ~ aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(component_clause,[status(thm)],[f7438]) ).
fof(f7442,plain,
( sQ719_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7440,f441]) ).
fof(f7443,plain,
sQ719_spl,
inference(contradiction_clause,[status(thm)],[f7442]) ).
fof(f7450,plain,
( ~ sQ654_spl
| aElementOf0(sK24_skl,xS)
| ~ sdtlseqdt0(sz00,xi)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f393,f6746]) ).
fof(f7456,plain,
( ~ sQ654_spl
| sQ5_spl
| ~ sQ505_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f7450,f655,f4960,f613,f6745]) ).
fof(f7457,plain,
$false,
inference(sat_refutation,[status(thm)],[f588,f590,f616,f758,f2124,f2394,f2425,f2609,f2863,f3068,f3103,f3217,f3954,f3960,f4616,f4618,f4640,f4642,f4644,f4650,f4653,f4839,f6036,f6189,f6201,f6716,f6748,f6833,f7183,f7185,f7443,f7456]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM582+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n017.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 02:37:11 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.21/0.46 % Drodi V4.1.1
% 4.01/1.19 % Refutation found
% 4.01/1.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.01/1.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.01/1.21 % Elapsed time: 0.763948 seconds
% 4.01/1.21 % CPU time: 5.773806 seconds
% 4.01/1.21 % Total memory used: 176.818 MB
% 4.01/1.21 % Net memory used: 170.436 MB
%------------------------------------------------------------------------------