%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM630+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:16 PM UTC 2026
% Result : Theorem 111.98s 14.86s
% Output : CNFRefutation 78.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 58 ( 12 unt; 3 def)
% Number of atoms : 616 ( 126 equ)
% Maximal formula atoms : 47 ( 10 avg)
% Number of connectives : 794 ( 236 ~; 218 |; 294 &)
% ( 24 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 9 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 13 con; 0-3 aty)
% Number of variables : 173 ( 158 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,definition,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aSet0(W0) )
=> ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ! [W1] :
( ( ( ( ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
=> ( ( ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
=> ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) ) ) ) )
& aSet0(W1) )
=> ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) ) )
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( ( ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(W1) ) ) )
=> aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0))) )
& ( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
=> ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(W1) ) ) )
& ! [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))
& aFunction0(sdtlpdtrp0(xC,W0)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( aElementOf0(W0,xP)
<=> ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) ) )
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(szmzizndt0(xQ),W0) )
& aSet0(xP) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
sbrdtbr0(xP) = xk,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,szDzozmdt0(xd)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [W0] :
( aElementOf0(W0,xD)
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) )
& aSet0(xD)
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
( aElementOf0(xP,slbdtsldtrb0(xD,xk))
& aSubsetOf0(xP,xD)
& ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xD) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,conjecture,
( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| aElementOf0(W0,xP) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) )
=> sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,negated_conjecture,
~ ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| aElementOf0(W0,xP) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) )
=> sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) ) ),
inference(negated_conjecture,[status(cth)],[f116]) ).
fof(f299,plain,
! [W0,W1] :
( ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f300,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ( ( ! [W3] :
( ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f299]) ).
fof(f301,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f300]) ).
fof(f302,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( ( sbrdtbr0(sK10_skl(W2,W1,W0)) = W1
& aSubsetOf0(sK10_skl(W2,W1,W0),W0) )
| aElementOf0(sK10_skl(W2,W1,W0),W2) )
& ( sbrdtbr0(sK10_skl(W2,W1,W0)) != W1
| ~ aSubsetOf0(sK10_skl(W2,W1,W0),W0)
| ~ aElementOf0(sK10_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f301]) ).
fof(f306,plain,
! [X0,X1,X2,X3] :
( sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0)
| aElementOf0(X3,X2)
| X2 != slbdtsldtrb0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f412,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f464,plain,
( ! [W0] :
( ( ! [W1] :
( ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) ) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ( ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) ) ) )
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( ( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
| sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
& ( ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,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))
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f465,definition,
! [W0,W1] :
( sP6_prd(W1,W0)
<=> ( ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) ) ) )
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f466,plain,
( ! [W0] :
( ( ! [W1] :
( ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) ) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP6_prd(W1,W0)
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( ( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
| sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
& ( ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,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))
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(formula_renaming,[status(thm)],[f464,f465]) ).
fof(f467,plain,
( ! [W0] :
( ( ! [W1] :
( ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( ( ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& ~ aElementOf0(W2,W1) )
| ~ aElement0(W2)
| aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) )
| ~ aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP6_prd(W1,W0)
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( ( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
| sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
& ( ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,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))
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(NNF_transformation,[status(thm)],[f466]) ).
fof(f468,plain,
( ! [W0] :
( ( ! [W1] :
( ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& ~ aElementOf0(W2,W1) )
| ~ aElement0(W2)
| aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) )
| ~ aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP6_prd(W1,W0)
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
| sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
& ! [W1] :
( ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,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))
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(miniscoping,[status(thm)],[f467]) ).
fof(f469,plain,
( ! [W0] :
( ( ! [W1] :
( ( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& ~ aElementOf0(W2,W1) )
| ~ aElement0(W2)
| aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( ( ( W2 = szmzizndt0(sdtlpdtrp0(xN,W0))
| aElementOf0(W2,W1) )
& aElement0(W2) )
| ~ aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP6_prd(W1,W0)
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& ! [W1] :
( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))
| sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( ( ~ aElementOf0(sK24_skl(W1,W0),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(sK24_skl(W1,W0),W1) )
| ~ aSet0(W1) ) ) )
& ! [W1] :
( ( sbrdtbr0(W1) = xk
& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,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))
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W2,sK24_skl(W1,W0))],[f468]) ).
fof(f494,plain,
! [X0,X1] :
( ~ aSet0(X1)
| sP6_prd(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f629,plain,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( aElementOf0(W0,xP)
<=> ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) ) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xQ),W0)
| ~ aElementOf0(W0,xQ) )
& aSet0(xP) ),
inference(pre_NNF_transformation,[status(thm)],[f104]) ).
fof(f630,plain,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( ( W0 = szmzizndt0(xQ)
| ~ aElementOf0(W0,xQ)
| ~ aElement0(W0)
| aElementOf0(W0,xP) )
& ( ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) )
| ~ aElementOf0(W0,xP) ) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xQ),W0)
| ~ aElementOf0(W0,xQ) )
& aSet0(xP) ),
inference(NNF_transformation,[status(thm)],[f629]) ).
fof(f631,plain,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& ! [W0] :
( W0 = szmzizndt0(xQ)
| ~ aElementOf0(W0,xQ)
| ~ aElement0(W0)
| aElementOf0(W0,xP) )
& ! [W0] :
( ( W0 != szmzizndt0(xQ)
& aElementOf0(W0,xQ)
& aElement0(W0) )
| ~ aElementOf0(W0,xP) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xQ),W0)
| ~ aElementOf0(W0,xQ) )
& aSet0(xP) ),
inference(miniscoping,[status(thm)],[f630]) ).
fof(f632,plain,
aSet0(xP),
inference(cnf_transformation,[status(thm)],[f631]) ).
fof(f649,plain,
xk = sbrdtbr0(xP),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f654,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f660,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [W0] :
( aElementOf0(W0,xD)
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) )
& aSet0(xD)
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f661,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [W0] :
( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn))
| ~ aElement0(W0)
| aElementOf0(W0,xD) )
& ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) )
| ~ aElementOf0(W0,xD) ) )
& aSet0(xD)
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(NNF_transformation,[status(thm)],[f660]) ).
fof(f662,plain,
( xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
& ! [W0] :
( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn))
| ~ aElement0(W0)
| aElementOf0(W0,xD) )
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) )
| ~ aElementOf0(W0,xD) )
& aSet0(xD)
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(miniscoping,[status(thm)],[f661]) ).
fof(f664,plain,
aSet0(xD),
inference(cnf_transformation,[status(thm)],[f662]) ).
fof(f669,plain,
sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) = xD,
inference(cnf_transformation,[status(thm)],[f662]) ).
fof(f670,plain,
( aElementOf0(xP,slbdtsldtrb0(xD,xk))
& aSubsetOf0(xP,xD)
& ! [W0] :
( aElementOf0(W0,xD)
| ~ aElementOf0(W0,xP) ) ),
inference(pre_NNF_transformation,[status(thm)],[f115]) ).
fof(f672,plain,
aSubsetOf0(xP,xD),
inference(cnf_transformation,[status(thm)],[f670]) ).
fof(f674,plain,
( sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)
& ! [W0] :
( aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| aElementOf0(W0,xP) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f117]) ).
fof(f675,plain,
( sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)
& ! [W0] :
( ( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& ~ aElementOf0(W0,xP) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| aElementOf0(W0,xP) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) ) )
& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(NNF_transformation,[status(thm)],[f674]) ).
fof(f676,plain,
( sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)
& ! [W0] :
( ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& ~ aElementOf0(W0,xP) )
| ~ aElement0(W0)
| aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ! [W0] :
( ( ( W0 = szmzizndt0(sdtlpdtrp0(xN,xn))
| aElementOf0(W0,xP) )
& aElement0(W0) )
| ~ aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(miniscoping,[status(thm)],[f675]) ).
fof(f683,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) != sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),
inference(cnf_transformation,[status(thm)],[f676]) ).
fof(f761,definition,
! [W0,W2] :
( sP13_prd(W2,W0)
<=> ( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W2 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W2,sdtlpdtrp0(xN,W0))
& aElement0(W2) ) ) ),
introduced(definition,[new_symbols(definition,[sP13_prd])],[]) ).
fof(f762,plain,
! [W0,W1] :
( sP6_prd(W1,W0)
<=> ( ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) ) ) )
& ! [W2] : sP13_prd(W2,W0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ),
inference(formula_renaming,[status(thm)],[f465,f761]) ).
fof(f763,plain,
! [W0,W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) ) ) )
| ? [W2] : ~ sP13_prd(W2,W0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ? [W2] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
& aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))
| sP6_prd(W1,W0) )
& ( ( ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) ) ) )
& ! [W2] : sP13_prd(W2,W0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sP6_prd(W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f762]) ).
fof(f764,plain,
( ! [W0,W1] :
( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) ) ) )
| ? [W2] : ~ sP13_prd(W2,W0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ? [W2] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
& aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))
| sP6_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ? [W2] :
( ~ aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(W2,W1) ) ) )
& ! [W2] : sP13_prd(W2,W0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sP6_prd(W1,W0) ) ),
inference(miniscoping,[status(thm)],[f763]) ).
fof(f765,plain,
( ! [W0,W1] :
( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ( sbrdtbr0(W1) = xk
& ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ! [W2] :
( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W2,W1) ) ) )
| ~ sP13_prd(sK55_skl(W1,W0),W0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),sK54_skl(W1,W0))
& aElementOf0(sK54_skl(W1,W0),sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))
| sP6_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& ( sbrdtbr0(W1) != xk
| ( ~ aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ~ aElementOf0(sK53_skl(W1,W0),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(sK53_skl(W1,W0),W1) ) )
& ! [W2] : sP13_prd(W2,W0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2)
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ sP6_prd(W1,W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl,sK54_skl,sK55_skl]),skolemize(W2,sK53_skl(W1,W0)),skolemize(W2,sK54_skl(W1,W0)),skolemize(W2,sK55_skl(W1,W0))],[f764]) ).
fof(f773,plain,
! [X0,X1] :
( ~ sP6_prd(X0,X1)
| ~ aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)) ),
inference(cnf_transformation,[status(thm)],[f765]) ).
fof(f867,plain,
! [X0,X1] :
( aElementOf0(X0,slbdtsldtrb0(X1,sbrdtbr0(X0)))
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f306]) ).
fof(f1003,plain,
! [X0] :
( aElementOf0(xP,slbdtsldtrb0(X0,xk))
| ~ aSubsetOf0(xP,X0)
| ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f649,f867]) ).
fof(f1004,plain,
! [X0] :
( aElementOf0(xP,slbdtsldtrb0(X0,xk))
| ~ aSubsetOf0(xP,X0)
| ~ aSet0(X0)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f649,f1003]) ).
fof(f1005,plain,
! [X0] :
( ~ aSet0(X0)
| aElementOf0(xP,slbdtsldtrb0(X0,xk))
| ~ aSubsetOf0(xP,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1004,f412]) ).
fof(f5189,plain,
! [X0] :
( ~ sP6_prd(X0,xn)
| ~ aElementOf0(X0,slbdtsldtrb0(xD,xk)) ),
inference(paramodulation,[status(thm)],[f669,f773]) ).
fof(f5627,plain,
( ~ aSet0(xD)
| ~ aSubsetOf0(xP,xD)
| ~ sP6_prd(xP,xn) ),
inference(resolution,[status(thm)],[f5189,f1005]) ).
fof(f5634,plain,
( ~ sP6_prd(xP,xn)
| ~ aSet0(xD) ),
inference(forward_subsumption_resolution,[status(thm)],[f5627,f672]) ).
fof(f5733,plain,
~ sP6_prd(xP,xn),
inference(forward_subsumption_resolution,[status(thm)],[f5634,f664]) ).
fof(f15608,plain,
( ~ aSet0(xP)
| sP6_prd(xP,xn)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f494,f683]) ).
fof(f15611,plain,
( ~ aSet0(xP)
| sP6_prd(xP,xn) ),
inference(forward_subsumption_resolution,[status(thm)],[f15608,f654]) ).
fof(f15613,plain,
~ aSet0(xP),
inference(forward_subsumption_resolution,[status(thm)],[f15611,f5733]) ).
fof(f15614,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f632,f15613]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM630+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n011.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 02:45:40 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.52 % Drodi V4.1.1
% 111.98/14.86 % Refutation found
% 111.98/14.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 111.98/14.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 78.80/16.12 % Elapsed time: 15.452182 seconds
% 78.80/16.12 % CPU time: 102.250245 seconds
% 78.80/16.12 % Total memory used: 431.662 MB
% 78.80/16.12 % Net memory used: 401.830 MB
%------------------------------------------------------------------------------