%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM581+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 : n001.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:04 PM UTC 2026
% Result : Theorem 4.07s 1.12s
% Output : CNFRefutation 4.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 17
% Syntax : Number of formulae : 104 ( 14 unt; 5 def)
% Number of atoms : 641 ( 72 equ)
% Maximal formula atoms : 22 ( 6 avg)
% Number of connectives : 787 ( 250 ~; 252 |; 231 &)
% ( 24 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-3 aty)
% Number of variables : 217 ( 206 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
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(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(f30,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(sz00,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(f53,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))
<=> ( W0 = W1
| aElementOf0(W0,slbdtrb0(W1)) ) ) ),
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(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(f82,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)) ) ),
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(f88,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(f89,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)],[f88]) ).
fof(f96,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f97,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
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(f143,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(f144,definition,
! [W0,W1,W3] :
( sP0_prd(W3,W1,W0)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f145,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)],[f143,f144]) ).
fof(f146,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)],[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) )
& ! [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)],[f146]) ).
fof(f148,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))],[f147]) ).
fof(f150,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)],[f148]) ).
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(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(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(f256,plain,
! [W0,W1] :
( ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))
<=> ( W0 = W1
| aElementOf0(W0,slbdtrb0(W1)) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f257,plain,
! [W0,W1] :
( ( ( ( W0 != W1
& ~ aElementOf0(W0,slbdtrb0(W1)) )
| aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) )
& ( W0 = W1
| aElementOf0(W0,slbdtrb0(W1))
| ~ aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f256]) ).
fof(f260,plain,
! [X0,X1] :
( X0 != X1
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f257]) ).
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(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(f393,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f405,plain,
! [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) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f406,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f405]) ).
fof(f407,plain,
! [X0,X1] :
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f405]) ).
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(f412,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ 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(f432,plain,
! [X0] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f447,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)],[f89]) ).
fof(f448,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)],[f447]) ).
fof(f449,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)],[f448]) ).
fof(f450,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)],[f449]) ).
fof(f451,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f455,plain,
! [X0] :
( X0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X0,xQ)
| ~ aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f458,plain,
aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f459,plain,
~ aElementOf0(sK24_skl,xS),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f461,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)],[f144]) ).
fof(f462,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)],[f461]) ).
fof(f464,plain,
! [X0,X1,X2] :
( aElementOf0(X0,X2)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f546,plain,
! [X0,X1,X2] :
( sP0_prd(X2,X1,X0)
| ~ aElementOf0(X2,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f150]) ).
fof(f553,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f246]) ).
fof(f557,plain,
! [X1] :
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f260]) ).
fof(f558,plain,
! [X0] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(duplicate_literals_removal,[status(thm)],[f557]) ).
fof(f630,plain,
( sK24_skl = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(sK24_skl,xQ) ),
inference(resolution,[status(thm)],[f455,f458]) ).
fof(f640,plain,
( aElementOf0(sK24_skl,xQ)
| aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)) ),
inference(paramodulation,[status(thm)],[f630,f451]) ).
fof(f667,plain,
sdtlseqdt0(sz00,xi),
inference(resolution,[status(thm)],[f183,f420]) ).
fof(f1032,plain,
! [X0] :
( aSet0(slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f170,f553]) ).
fof(f1180,plain,
! [X0] :
( aElement0(X0)
| ~ aSet0(slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f558,f97]) ).
fof(f1182,plain,
! [X0] :
( aElement0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1180,f1032]) ).
fof(f1282,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f407,f451]) ).
fof(f1288,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),szNzAzT0),
inference(forward_subsumption_resolution,[status(thm)],[f1282,f420]) ).
fof(f1292,plain,
! [X0] :
( aElementOf0(sK24_skl,xQ)
| aElementOf0(sK24_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f411,f640]) ).
fof(f1298,plain,
! [X0] :
( aElementOf0(sK24_skl,xQ)
| aElementOf0(sK24_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1292,f420]) ).
fof(f1304,plain,
aElement0(szmzizndt0(sdtlpdtrp0(xN,xi))),
inference(resolution,[status(thm)],[f1288,f1182]) ).
fof(f1417,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f393,f412]) ).
fof(f1421,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f168]) ).
fof(f1542,plain,
( aElementOf0(sK24_skl,xQ)
| aElementOf0(sK24_skl,xS)
| ~ sdtlseqdt0(sz00,xi)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f393,f1298]) ).
fof(f1546,plain,
( aElementOf0(sK24_skl,xQ)
| aElementOf0(sK24_skl,xS)
| ~ sdtlseqdt0(sz00,xi) ),
inference(forward_subsumption_resolution,[status(thm)],[f1542,f168]) ).
fof(f1547,plain,
( aElementOf0(sK24_skl,xQ)
| aElementOf0(sK24_skl,xS) ),
inference(forward_subsumption_resolution,[status(thm)],[f1546,f667]) ).
fof(f1883,plain,
! [X0] :
( sP0_prd(X0,szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))
| ~ aSet0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(X0,xQ) ),
inference(resolution,[status(thm)],[f432,f546]) ).
fof(f1887,plain,
! [X0] :
( sP0_prd(X0,szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
| ~ aSet0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(X0,xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f1883,f1304]) ).
fof(f2934,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1421,f183]) ).
fof(f2938,plain,
! [X0,X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ aSet0(xS)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f2934,f119]) ).
fof(f2943,plain,
! [X0,X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2938,f350]) ).
fof(f3441,plain,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
| ~ aSet0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(X0,xQ) ),
inference(resolution,[status(thm)],[f1887,f464]) ).
fof(f4070,plain,
! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(xi,szNzAzT0)
| ~ aSet0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(X0,xQ) ),
inference(resolution,[status(thm)],[f3441,f2943]) ).
fof(f4076,plain,
! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(X0,xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f4070,f406]) ).
fof(f4080,plain,
aElementOf0(sK24_skl,xS),
inference(backward_subsumption_resolution,[status(thm)],[f1547,f4081]) ).
fof(f4081,plain,
! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f4076,f420]) ).
fof(f4097,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4080,f459]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM581+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n001.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 02:47:43 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 4.07/1.12 % Refutation found
% 4.07/1.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.07/1.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.88/1.16 % Elapsed time: 0.692995 seconds
% 4.88/1.16 % CPU time: 5.106755 seconds
% 4.88/1.16 % Total memory used: 159.802 MB
% 4.88/1.16 % Net memory used: 155.312 MB
%------------------------------------------------------------------------------