%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM579+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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 : Fri Sep 25 02:26:06 PM UTC 2026
% Result : Theorem 18.81s 3.31s
% Output : CNFRefutation 18.81s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f225ERROR: Could not build tree for root c_49094ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(f18,axiom,
! [X0,X1] :
( ( aSet0(X1)
& aElement0(X0) )
=> ( ~ aElementOf0(X0,X1)
=> sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDiffCons) ).
fof(f21,axiom,
! [X0] :
( aElement0(X0)
=> ! [X1] :
( ( isFinite0(X1)
& aSet0(X1) )
=> isFinite0(sdtpldt0(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mFConsSet) ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroNum) ).
fof(f30,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sdtlseqdt0(sz00,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroLess) ).
fof(f41,axiom,
! [X0] :
( aSet0(X0)
=> ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardNum) ).
fof(f44,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( ( aElementOf0(X1,X0)
& isFinite0(X0) )
=> szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardDiff) ).
fof(f57,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aSet0(X0) )
=> ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& aSet0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSel) ).
fof(f65,axiom,
! [X0] :
( aFunction0(X0)
=> ! [X1] :
( aElementOf0(X1,szDzozmdt0(X0))
=> aElement0(sdtlpdtrp0(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mImgElm) ).
fof(f66,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aFunction0(X0) )
=> ! [X2] :
( X2 = sdtlbdtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& aSet0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefPtt) ).
fof(f75,axiom,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [X0] :
( aElementOf0(X0,xS)
=> aElementOf0(X0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3435) ).
fof(f80,axiom,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3533) ).
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3671) ).
fof(f83,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( sdtlseqdt0(X1,X0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> aElementOf0(X2,sdtlpdtrp0(xN,X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3754) ).
fof(f85,conjecture,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( X2 != szmzizndt0(sdtlpdtrp0(xN,X0))
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& aElement0(X2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1) )
=> ( ( ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) )
=> ( ( ! [X2] :
( aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( ( X2 = szmzizndt0(sdtlpdtrp0(xN,X0))
| aElementOf0(X2,X1) )
& aElement0(X2) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) )
=> ( aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
| ( sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) = xK
& ( aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
| ! [X2] :
( aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
=> aElementOf0(X2,xS) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f86,negated_conjecture,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( X2 != szmzizndt0(sdtlpdtrp0(xN,X0))
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& aElement0(X2) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1) )
=> ( ( ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) )
=> ( ( ! [X2] :
( aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( ( X2 = szmzizndt0(sdtlpdtrp0(xN,X0))
| aElementOf0(X2,X1) )
& aElement0(X2) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) )
=> ( aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
| ( sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) = xK
& ( aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
| ! [X2] :
( aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
=> aElementOf0(X2,xS) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f85]) ).
fof(f98,plain,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( aElementOf0(X4,X1)
=> aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1) )
=> ( ( ! [X5] :
( aElementOf0(X5,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) )
=> ( ( ! [X6] :
( aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X6
| aElementOf0(X6,X1) )
& aElement0(X6) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) )
=> ( aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
| ( sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) = xK
& ( aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
| ! [X7] :
( aElementOf0(X7,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
=> aElementOf0(X7,xS) ) ) ) ) ) ) ) ),
inference(rectify,[],[f86]) ).
fof(f99,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f105,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f118,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ),
inference(ennf_transformation,[],[f18]) ).
fof(f119,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ),
inference(flattening,[],[f118]) ).
fof(f124,plain,
! [X0] :
( ~ aElement0(X0)
| ! [X1] :
( ~ isFinite0(X1)
| ~ aSet0(X1)
| isFinite0(sdtpldt0(X1,X0)) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f125,plain,
! [X0] :
( ~ aElement0(X0)
| ! [X1] :
( ~ isFinite0(X1)
| ~ aSet0(X1)
| isFinite0(sdtpldt0(X1,X0)) ) ),
inference(flattening,[],[f124]) ).
fof(f134,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(sz00,X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f148,plain,
! [X0] :
( ~ aSet0(X0)
| ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f152,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f153,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0) ) ),
inference(flattening,[],[f152]) ).
fof(f173,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& aSet0(X2) ) ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f174,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& aSet0(X2) ) ) ),
inference(flattening,[],[f173]) ).
fof(f186,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aElementOf0(X1,szDzozmdt0(X0))
| aElement0(sdtlpdtrp0(X0,X1)) ) ),
inference(ennf_transformation,[],[f65]) ).
fof(f187,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( X2 = sdtlbdtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& aSet0(X2) ) ) ),
inference(ennf_transformation,[],[f66]) ).
fof(f188,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( X2 = sdtlbdtrb0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& aSet0(X2) ) ) ),
inference(flattening,[],[f187]) ).
fof(f198,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [X0] :
( ~ aElementOf0(X0,xS)
| aElementOf0(X0,szNzAzT0) )
& aSet0(xS) ),
inference(ennf_transformation,[],[f75]) ).
fof(f205,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ),
inference(ennf_transformation,[],[f82]) ).
fof(f206,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| aElementOf0(X2,sdtlpdtrp0(xN,X1)) ) ) ),
inference(ennf_transformation,[],[f83]) ).
fof(f207,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| aElementOf0(X2,sdtlpdtrp0(xN,X1)) ) ) ),
inference(flattening,[],[f206]) ).
fof(f210,plain,
? [X0] :
( aElementOf0(X0,szNzAzT0)
& ? [X1] :
( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,X1)
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1)
& ! [X5] :
( ~ aElementOf0(X5,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X6] :
( aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X6
| aElementOf0(X6,X1) )
& aElement0(X6) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
& ( xK != sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ~ aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
& ? [X7] :
( aElementOf0(X7,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X7,xS) ) ) ) ) ),
inference(ennf_transformation,[],[f98]) ).
fof(f211,plain,
? [X0] :
( aElementOf0(X0,szNzAzT0)
& ? [X1] :
( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,X1)
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1)
& ! [X5] :
( ~ aElementOf0(X5,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X6] :
( aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X6
| aElementOf0(X6,X1) )
& aElement0(X6) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
& ( xK != sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ~ aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
& ? [X7] :
( aElementOf0(X7,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X7,xS) ) ) ) ) ),
inference(flattening,[],[f210]) ).
fof(f230,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(nnf_transformation,[],[f105]) ).
fof(f231,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(flattening,[],[f230]) ).
fof(f232,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(rectify,[],[f231]) ).
fof(f233,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ( aElementOf0(sK11(X0,X1),X1)
& ~ aElementOf0(sK11(X0,X1),X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f232]) ).
fof(f248,plain,
! [X0] :
( ~ aSet0(X0)
| ( ( ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| isFinite0(X0) )
& ( ~ isFinite0(X0)
| aElementOf0(sbrdtbr0(X0),szNzAzT0) ) ) ),
inference(nnf_transformation,[],[f148]) ).
fof(f267,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ! [X2] :
( ( slbdtsldtrb0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& ( sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0)
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& ( ~ aElementOf0(X3,X2)
| sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0) ) )
| ~ aSet0(X2)
| X2 = slbdtsldtrb0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f174]) ).
fof(f268,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ! [X2] :
( ( slbdtsldtrb0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& ( sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0)
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& ( ~ aElementOf0(X3,X2)
| sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0) ) )
| ~ aSet0(X2)
| X2 = slbdtsldtrb0(X0,X1) ) ) ),
inference(flattening,[],[f267]) ).
fof(f269,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ! [X2] :
( ( slbdtsldtrb0(X0,X1) != X2
| ( ! [X4] :
( ( ~ aElementOf0(X4,X2)
| ( sbrdtbr0(X4) = X1
& aSubsetOf0(X4,X0) ) )
& ( sbrdtbr0(X4) != X1
| ~ aSubsetOf0(X4,X0)
| aElementOf0(X4,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sbrdtbr0(X3) = X1
& aSubsetOf0(X3,X0) ) )
& ( ~ aElementOf0(X3,X2)
| sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0) ) )
| ~ aSet0(X2)
| X2 = slbdtsldtrb0(X0,X1) ) ) ),
inference(rectify,[],[f268]) ).
fof(f270,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ! [X2] :
( ( slbdtsldtrb0(X0,X1) != X2
| ( ! [X4] :
( ( ~ aElementOf0(X4,X2)
| ( sbrdtbr0(X4) = X1
& aSubsetOf0(X4,X0) ) )
& ( sbrdtbr0(X4) != X1
| ~ aSubsetOf0(X4,X0)
| aElementOf0(X4,X2) ) )
& aSet0(X2) ) )
& ( ( ( aElementOf0(sK20(X0,X1,X2),X2)
| ( sbrdtbr0(sK20(X0,X1,X2)) = X1
& aSubsetOf0(sK20(X0,X1,X2),X0) ) )
& ( ~ aElementOf0(sK20(X0,X1,X2),X2)
| sbrdtbr0(sK20(X0,X1,X2)) != X1
| ~ aSubsetOf0(sK20(X0,X1,X2),X0) ) )
| ~ aSet0(X2)
| X2 = slbdtsldtrb0(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X3,sK20(X0,X1,X2))],[f269]) ).
fof(f272,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0))
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(X3,X2)
| sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f188]) ).
fof(f273,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0))
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(X3,X2)
| sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(flattening,[],[f272]) ).
fof(f274,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X4] :
( ( ~ aElementOf0(X4,X2)
| ( sdtlpdtrp0(X0,X4) = X1
& aElementOf0(X4,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X4) != X1
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( sdtlpdtrp0(X0,X3) = X1
& aElementOf0(X3,szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(X3,X2)
| sdtlpdtrp0(X0,X3) != X1
| ~ aElementOf0(X3,szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(rectify,[],[f273]) ).
fof(f275,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ! [X2] :
( ( sdtlbdtrb0(X0,X1) != X2
| ( ! [X4] :
( ( ~ aElementOf0(X4,X2)
| ( sdtlpdtrp0(X0,X4) = X1
& aElementOf0(X4,szDzozmdt0(X0)) ) )
& ( sdtlpdtrp0(X0,X4) != X1
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,X2) ) )
& aSet0(X2) ) )
& ( ( ( aElementOf0(sK22(X0,X1,X2),X2)
| ( sdtlpdtrp0(X0,sK22(X0,X1,X2)) = X1
& aElementOf0(sK22(X0,X1,X2),szDzozmdt0(X0)) ) )
& ( ~ aElementOf0(sK22(X0,X1,X2),X2)
| sdtlpdtrp0(X0,sK22(X0,X1,X2)) != X1
| ~ aElementOf0(sK22(X0,X1,X2),szDzozmdt0(X0)) ) )
| ~ aSet0(X2)
| X2 = sdtlbdtrb0(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X3,sK22(X0,X1,X2))],[f274]) ).
fof(f306,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ( ( aElementOf0(sK39(X0),sdtlpdtrp0(xN,X0))
& ~ aElementOf0(sK39(X0),szNzAzT0) )
| ~ aSet0(sdtlpdtrp0(xN,X0)) ) )
| sP9(X0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X1,sK39(X0))],[f225]) ).
fof(f309,plain,
? [X0] :
( aElementOf0(X0,szNzAzT0)
& ? [X1] :
( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,X1)
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X3
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| ~ aElement0(X3)
| aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1)
& ! [X5] :
( ~ aElementOf0(X5,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X6] :
( ( ~ aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X6
| aElementOf0(X6,X1) )
& aElement0(X6) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X6
& ~ aElementOf0(X6,X1) )
| ~ aElement0(X6)
| aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
& ( xK != sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ~ aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
& ? [X7] :
( aElementOf0(X7,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X7,xS) ) ) ) ) ),
inference(nnf_transformation,[],[f211]) ).
fof(f310,plain,
? [X0] :
( aElementOf0(X0,szNzAzT0)
& ? [X1] :
( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,X1)
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X3] :
( ( ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X3
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| ~ aElement0(X3)
| aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1)
& ! [X5] :
( ~ aElementOf0(X5,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X6] :
( ( ~ aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X6
| aElementOf0(X6,X1) )
& aElement0(X6) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X6
& ~ aElementOf0(X6,X1) )
| ~ aElement0(X6)
| aElementOf0(X6,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
& ( xK != sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ~ aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
& ? [X7] :
( aElementOf0(X7,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X7,xS) ) ) ) ) ),
inference(flattening,[],[f309]) ).
fof(f311,plain,
? [X0] :
( aElementOf0(X0,szNzAzT0)
& ? [X1] :
( aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& sbrdtbr0(X1) = xk
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X7] :
( ~ aElementOf0(X7,X1)
| aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& ! [X6] :
( ( ~ aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X6
& aElementOf0(X6,sdtlpdtrp0(xN,X0))
& aElement0(X6) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X6
| ~ aElementOf0(X6,sdtlpdtrp0(xN,X0))
| ~ aElement0(X6)
| aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X5] :
( ~ aElementOf0(X5,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& aSet0(X1)
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X4) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( ( ~ aElementOf0(X3,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X3
| aElementOf0(X3,X1) )
& aElement0(X3) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& ~ aElementOf0(X3,X1) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK))
& ( xK != sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( ~ aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS)
& ? [X2] :
( aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
& ~ aElementOf0(X2,xS) ) ) ) ) ),
inference(rectify,[],[f310]) ).
fof(f312,plain,
( aElementOf0(sK41,szNzAzT0)
& aElementOf0(sK42,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))),xk))
& xk = sbrdtbr0(sK42)
& aSubsetOf0(sK42,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))))
& ! [X7] :
( ~ aElementOf0(X7,sK42)
| aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))) )
& ! [X6] :
( ( ~ aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ( szmzizndt0(sdtlpdtrp0(xN,sK41)) != X6
& aElementOf0(X6,sdtlpdtrp0(xN,sK41))
& aElement0(X6) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,sK41)) = X6
| ~ aElementOf0(X6,sdtlpdtrp0(xN,sK41))
| ~ aElement0(X6)
| aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))))
& ! [X5] :
( ~ aElementOf0(X5,sdtlpdtrp0(xN,sK41))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK41)),X5) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtlpdtrp0(xN,sK41))
& aSet0(sK42)
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,sK41))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK41)),X4) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtlpdtrp0(xN,sK41))
& ! [X3] :
( ( ~ aElementOf0(X3,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,sK41)) = X3
| aElementOf0(X3,sK42) )
& aElement0(X3) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,sK41)) != X3
& ~ aElementOf0(X3,sK42) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) ) )
& aSet0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
& ~ aElementOf0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))),slbdtsldtrb0(xS,xK))
& ( xK != sbrdtbr0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ( ~ aSubsetOf0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))),xS)
& aElementOf0(sK43,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
& ~ aElementOf0(sK43,xS) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41,sK42,sK43]),skolemize(X0,sK41),skolemize(X1,sK42),skolemize(X2,sK43)],[f311]) ).
fof(f313,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| aElement0(X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f320,plain,
! [X3,X0,X1] :
( ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) ),
inference(cnf_transformation,[],[f233]) ).
fof(f353,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f119]) ).
fof(f356,plain,
! [X0,X1] :
( ~ aElement0(X0)
| ~ isFinite0(X1)
| ~ aSet0(X1)
| isFinite0(sdtpldt0(X1,X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f360,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[],[f24]) ).
fof(f367,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(sz00,X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f378,plain,
! [X0] :
( ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| isFinite0(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f383,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| sbrdtbr0(X0) = szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) ),
inference(cnf_transformation,[],[f153]) ).
fof(f413,plain,
! [X2,X0,X1,X4] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| slbdtsldtrb0(X0,X1) != X2
| ~ aElementOf0(X4,X2)
| sbrdtbr0(X4) = X1 ),
inference(cnf_transformation,[],[f270]) ).
fof(f428,plain,
! [X0,X1] :
( ~ aFunction0(X0)
| ~ aElementOf0(X1,szDzozmdt0(X0))
| aElement0(sdtlpdtrp0(X0,X1)) ),
inference(cnf_transformation,[],[f186]) ).
fof(f429,plain,
! [X2,X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| sdtlbdtrb0(X0,X1) != X2
| ~ aElementOf0(X4,X2)
| sdtlpdtrp0(X0,X4) = X1 ),
inference(cnf_transformation,[],[f275]) ).
fof(f431,plain,
! [X2,X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| sdtlbdtrb0(X0,X1) != X2
| sdtlpdtrp0(X0,X4) != X1
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,X2) ),
inference(cnf_transformation,[],[f275]) ).
fof(f462,plain,
aSet0(xS),
inference(cnf_transformation,[],[f198]) ).
fof(f511,plain,
xK = szszuzczcdt0(xk),
inference(cnf_transformation,[],[f80]) ).
fof(f512,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f80]) ).
fof(f528,plain,
xS = sdtlpdtrp0(xN,sz00),
inference(cnf_transformation,[],[f306]) ).
fof(f529,plain,
szNzAzT0 = szDzozmdt0(xN),
inference(cnf_transformation,[],[f306]) ).
fof(f530,plain,
aFunction0(xN),
inference(cnf_transformation,[],[f306]) ).
fof(f534,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f205]) ).
fof(f535,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f207]) ).
fof(f536,plain,
! [X2,X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| aElementOf0(X2,sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f207]) ).
fof(f542,plain,
aElementOf0(sK41,szNzAzT0),
inference(cnf_transformation,[],[f312]) ).
fof(f543,plain,
aElementOf0(sK42,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))),xk)),
inference(cnf_transformation,[],[f312]) ).
fof(f544,plain,
xk = sbrdtbr0(sK42),
inference(cnf_transformation,[],[f312]) ).
fof(f546,plain,
! [X7] :
( ~ aElementOf0(X7,sK42)
| aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))) ),
inference(cnf_transformation,[],[f312]) ).
fof(f547,plain,
! [X6] :
( ~ aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))))
| szmzizndt0(sdtlpdtrp0(xN,sK41)) != X6 ),
inference(cnf_transformation,[],[f312]) ).
fof(f548,plain,
! [X6] :
( ~ aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))))
| aElementOf0(X6,sdtlpdtrp0(xN,sK41)) ),
inference(cnf_transformation,[],[f312]) ).
fof(f551,plain,
aSet0(sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))),
inference(cnf_transformation,[],[f312]) ).
fof(f553,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtlpdtrp0(xN,sK41)),
inference(cnf_transformation,[],[f312]) ).
fof(f554,plain,
aSet0(sK42),
inference(cnf_transformation,[],[f312]) ).
fof(f557,plain,
! [X3] :
( ~ aElementOf0(X3,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| szmzizndt0(sdtlpdtrp0(xN,sK41)) = X3
| aElementOf0(X3,sK42) ),
inference(cnf_transformation,[],[f312]) ).
fof(f559,plain,
! [X3] :
( szmzizndt0(sdtlpdtrp0(xN,sK41)) != X3
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) ),
inference(cnf_transformation,[],[f312]) ).
fof(f561,plain,
aSet0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))),
inference(cnf_transformation,[],[f312]) ).
fof(f564,plain,
( xK != sbrdtbr0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| aElementOf0(sK43,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) ),
inference(cnf_transformation,[],[f312]) ).
fof(f565,plain,
( xK != sbrdtbr0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ~ aElementOf0(sK43,xS) ),
inference(cnf_transformation,[],[f312]) ).
fof(f587,plain,
! [X0,X1,X4] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| ~ aElementOf0(X4,slbdtsldtrb0(X0,X1))
| sbrdtbr0(X4) = X1 ),
inference(equality_resolution,[],[f413]) ).
fof(f589,plain,
! [X2,X0,X4] :
( ~ aElement0(sdtlpdtrp0(X0,X4))
| ~ aFunction0(X0)
| sdtlbdtrb0(X0,sdtlpdtrp0(X0,X4)) != X2
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,X2) ),
inference(equality_resolution,[],[f431]) ).
fof(f590,plain,
! [X0,X4] :
( ~ aElement0(sdtlpdtrp0(X0,X4))
| ~ aFunction0(X0)
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,sdtlbdtrb0(X0,sdtlpdtrp0(X0,X4))) ),
inference(equality_resolution,[],[f589]) ).
fof(f592,plain,
! [X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ~ aElementOf0(X4,sdtlbdtrb0(X0,X1))
| sdtlpdtrp0(X0,X4) = X1 ),
inference(equality_resolution,[],[f429]) ).
fof(f609,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,sK41)))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) ),
inference(equality_resolution,[],[f559]) ).
fof(f610,plain,
~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))),
inference(equality_resolution,[],[f547]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( aElement0(X0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,X1)
| ( sdtmndt0(sdtpldt0(X1,X0),X0) = X1 )
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( isFinite0(sdtpldt0(X1,X0))
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f356]) ).
tcf(c_96,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[],[f360]) ).
tcf(c_103,plain,
! [X0: $i] :
( sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_115,plain,
! [X0: $i] :
( isFinite0(X0)
| ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] :
( ( szszuzczcdt0(sbrdtbr0(sdtmndt0(X1,X0))) = sbrdtbr0(X1) )
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sbrdtbr0(X0) = X2 )
| ~ aSet0(X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X0,slbdtsldtrb0(X1,X2)) ),
inference(cnf_transformation,[],[f587]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( aElement0(sdtlpdtrp0(X1,X0))
| ~ aFunction0(X1)
| ~ aElementOf0(X0,szDzozmdt0(X1)) ),
inference(cnf_transformation,[],[f428]) ).
tcf(c_169,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X1,sdtlbdtrb0(X0,sdtlpdtrp0(X0,X1)))
| ~ aFunction0(X0)
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ~ aElement0(sdtlpdtrp0(X0,X1)) ),
inference(cnf_transformation,[],[f590]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sdtlpdtrp0(X1,X0) = X2 )
| ~ aFunction0(X1)
| ~ aElement0(X2)
| ~ aElementOf0(X0,sdtlbdtrb0(X1,X2)) ),
inference(cnf_transformation,[],[f592]) ).
tcf(c_195,plain,
aSet0(xS),
inference(cnf_transformation,[],[f462]) ).
tcf(c_247,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f512]) ).
tcf(c_248,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[],[f511]) ).
tcf(c_261,plain,
aFunction0(xN),
inference(cnf_transformation,[],[f530]) ).
tcf(c_262,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[],[f529]) ).
tcf(c_263,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[],[f528]) ).
tcf(c_267,plain,
! [X0: $i] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f534]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X2))
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(X2,X1)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f536]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X1),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f535]) ).
tcf(c_278,negated_conjecture,
( ~ aElementOf0(sK43,xS)
| ( sbrdtbr0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) != xK ) ),
inference(cnf_transformation,[],[f565]) ).
tcf(c_279,negated_conjecture,
( aElementOf0(sK43,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ( sbrdtbr0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) != xK ) ),
inference(cnf_transformation,[],[f564]) ).
tcf(c_282,negated_conjecture,
aSet0(sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))),
inference(cnf_transformation,[],[f561]) ).
tcf(c_284,negated_conjecture,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,sK41))) ),
inference(cnf_transformation,[],[f609]) ).
tcf(c_286,negated_conjecture,
! [X0: $i] :
( aElementOf0(X0,sK42)
| ( szmzizndt0(sdtlpdtrp0(xN,sK41)) = X0 )
| ~ aElementOf0(X0,sdtpldt0(sK42,szmzizndt0(sdtlpdtrp0(xN,sK41)))) ),
inference(cnf_transformation,[],[f557]) ).
tcf(c_289,negated_conjecture,
aSet0(sK42),
inference(cnf_transformation,[],[f554]) ).
tcf(c_290,negated_conjecture,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtlpdtrp0(xN,sK41)),
inference(cnf_transformation,[],[f553]) ).
tcf(c_292,negated_conjecture,
aSet0(sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))),
inference(cnf_transformation,[],[f551]) ).
tcf(c_295,negated_conjecture,
! [X0: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,sK41))
| ~ aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))) ),
inference(cnf_transformation,[],[f548]) ).
tcf(c_296,negated_conjecture,
~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK41)),sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41)))),
inference(cnf_transformation,[],[f610]) ).
tcf(c_297,negated_conjecture,
! [X0: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))))
| ~ aElementOf0(X0,sK42) ),
inference(cnf_transformation,[],[f546]) ).
tcf(c_299,negated_conjecture,
sbrdtbr0(sK42) = xk,
inference(cnf_transformation,[],[f544]) ).
tcf(c_300,negated_conjecture,
aElementOf0(sK42,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK41),szmzizndt0(sdtlpdtrp0(xN,sK41))),xk)),
inference(cnf_transformation,[],[f543]) ).
tcf(c_301,negated_conjecture,
aElementOf0(sK41,szNzAzT0),
inference(cnf_transformation,[],[f542]) ).
tcf(c_949,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlbdtrb0(X1,sdtlpdtrp0(X1,X0)))
| ~ aFunction0(X1)
| ~ aElementOf0(X0,szDzozmdt0(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_169,c_164]) ).
tcf(c_16884,definition,
iPr_def_10 = sdtlpdtrp0(xN,sK41),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_16886,definition,
iPr_def_12 = sdtpldt0(sK42,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_16888,definition,
iPr_def_14 = sdtmndt0(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_16889,definition,
iPr_def_15 = slbdtsldtrb0(iPr_def_14,xk),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_16890,definition,
iPr_def_16 = sbrdtbr0(sK42),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_16891,definition,
iPr_def_17 = sbrdtbr0(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_16894,negated_conjecture,
aElementOf0(sK41,szNzAzT0),
inference(demodulation,[status(thm)],[c_301]) ).
tcf(c_16895,negated_conjecture,
aElementOf0(sK42,iPr_def_15),
inference(demodulation,[status(thm)],[c_300,c_16888,c_16889]) ).
tcf(c_16896,negated_conjecture,
iPr_def_16 = xk,
inference(demodulation,[status(thm)],[c_299,c_16890]) ).
tcf(c_16898,negated_conjecture,
! [X0: $i] :
( aElementOf0(X0,iPr_def_14)
| ~ aElementOf0(X0,sK42) ),
inference(demodulation,[status(thm)],[c_297]) ).
tcf(c_16899,negated_conjecture,
~ aElementOf0(iPr_def_11,iPr_def_14),
inference(demodulation,[status(thm)],[c_296]) ).
tcf(c_16900,negated_conjecture,
! [X0: $i] :
( aElementOf0(X0,iPr_def_10)
| ~ aElementOf0(X0,iPr_def_14) ),
inference(demodulation,[status(thm)],[c_295]) ).
tcf(c_16903,negated_conjecture,
aSet0(iPr_def_14),
inference(demodulation,[status(thm)],[c_292]) ).
tcf(c_16904,negated_conjecture,
aSet0(sK42),
inference(demodulation,[status(thm)],[c_289]) ).
tcf(c_16906,negated_conjecture,
aElementOf0(iPr_def_11,iPr_def_10),
inference(demodulation,[status(thm)],[c_290]) ).
tcf(c_16907,negated_conjecture,
! [X0: $i] :
( aElementOf0(X0,sK42)
| ( iPr_def_11 = X0 )
| ~ aElementOf0(X0,iPr_def_12) ),
inference(demodulation,[status(thm)],[c_286]) ).
tcf(c_16909,negated_conjecture,
( aElementOf0(iPr_def_11,iPr_def_12)
| ~ aElement0(iPr_def_11) ),
inference(demodulation,[status(thm)],[c_284]) ).
tcf(c_16910,negated_conjecture,
aSet0(iPr_def_12),
inference(demodulation,[status(thm)],[c_282]) ).
tcf(c_16912,negated_conjecture,
( aElementOf0(sK43,iPr_def_12)
| ( iPr_def_17 != xK ) ),
inference(demodulation,[status(thm)],[c_279]) ).
tcf(c_16913,negated_conjecture,
( ~ aElementOf0(sK43,xS)
| ( iPr_def_17 != xK ) ),
inference(demodulation,[status(thm)],[c_278]) ).
tcf(c_20511,plain,
aElementOf0(iPr_def_16,szNzAzT0),
inference(light_normalisation,[status(thm)],[c_247,c_16896]) ).
tcf(c_20541,plain,
szszuzczcdt0(iPr_def_16) = xK,
inference(light_normalisation,[status(thm)],[c_248,c_16896]) ).
tcf(c_20564,plain,
slbdtsldtrb0(iPr_def_14,iPr_def_16) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_16889,c_16896]) ).
tcf(c_20579,plain,
sdtlseqdt0(sz00,sK41),
inference(superposition,[status(thm)],[c_16894,c_103]) ).
tcf(c_20705,plain,
( aSet0(iPr_def_10)
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(superposition,[status(thm)],[c_16884,c_267]) ).
tcf(c_20706,plain,
aSet0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_20705,c_16894]) ).
tcf(c_20726,plain,
( aElement0(iPr_def_11)
| ~ aSet0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_16906,c_49]) ).
tcf(c_20748,plain,
aElement0(iPr_def_11),
inference(global_subsumption_just,[status(thm)],[c_20726,c_20706,c_20726]) ).
tcf(c_20750,plain,
aElementOf0(iPr_def_11,iPr_def_12),
inference(backward_subsumption_resolution,[status(thm)],[c_16909,c_20748]) ).
tcf(c_21021,plain,
( isFinite0(sK42)
| ~ aSet0(sK42)
| ~ aElementOf0(iPr_def_16,szNzAzT0) ),
inference(superposition,[status(thm)],[c_16890,c_115]) ).
tcf(c_21026,plain,
isFinite0(sK42),
inference(forward_subsumption_resolution,[status(thm)],[c_21021,c_16904,c_20511]) ).
tcf(c_21851,plain,
! [X0: $i] :
( aElement0(sdtlpdtrp0(xN,X0))
| ~ aFunction0(xN)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_262,c_164]) ).
tcf(c_21852,plain,
! [X0: $i] :
( aElement0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_21851,c_261]) ).
tcf(c_22564,plain,
( isFinite0(iPr_def_12)
| ~ isFinite0(sK42)
| ~ aSet0(sK42)
| ~ aElement0(iPr_def_11) ),
inference(superposition,[status(thm)],[c_16886,c_92]) ).
tcf(c_22565,plain,
isFinite0(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_22564,c_21026,c_16904,c_20748]) ).
tcf(c_23300,plain,
! [X0: $i] :
( aElementOf0(iPr_def_11,X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_16906,c_59]) ).
tcf(c_24168,plain,
( aElement0(iPr_def_10)
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(superposition,[status(thm)],[c_16884,c_21852]) ).
tcf(c_24169,plain,
aElement0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_24168,c_16894]) ).
tcf(c_25420,plain,
( aElementOf0(sK41,sdtlbdtrb0(xN,iPr_def_10))
| ~ aFunction0(xN)
| ~ aElementOf0(sK41,szDzozmdt0(xN)) ),
inference(superposition,[status(thm)],[c_16884,c_949]) ).
tcf(c_25425,plain,
( aElementOf0(sK41,sdtlbdtrb0(xN,iPr_def_10))
| ~ aFunction0(xN)
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(light_normalisation,[status(thm)],[c_25420,c_262]) ).
tcf(c_25426,plain,
aElementOf0(sK41,sdtlbdtrb0(xN,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_25425,c_261,c_16894]) ).
tcf(c_26374,plain,
! [X0: $i] :
( aElementOf0(X0,iPr_def_14)
| ( sdtmndt0(sdtpldt0(sK42,X0),X0) = sK42 )
| ~ aSet0(sK42)
| ~ aElement0(X0) ),
inference(superposition,[status(thm)],[c_89,c_16898]) ).
tcf(c_26468,plain,
! [X0: $i] :
( aElementOf0(X0,iPr_def_14)
| ( sdtmndt0(sdtpldt0(sK42,X0),X0) = sK42 )
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26374,c_16904]) ).
tcf(c_26954,plain,
( ( sdtmndt0(sdtpldt0(sK42,iPr_def_11),iPr_def_11) = sK42 )
| ~ aElement0(iPr_def_11) ),
inference(superposition,[status(thm)],[c_26468,c_16899]) ).
tcf(c_26955,plain,
( ( sdtmndt0(iPr_def_12,iPr_def_11) = sK42 )
| ~ aElement0(iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_26954,c_16886]) ).
tcf(c_26956,plain,
sdtmndt0(iPr_def_12,iPr_def_11) = sK42,
inference(forward_subsumption_resolution,[status(thm)],[c_26955,c_20748]) ).
tcf(c_28780,plain,
! [X0: $i] :
( ( sbrdtbr0(X0) = iPr_def_16 )
| ~ aSet0(iPr_def_14)
| ~ aElementOf0(iPr_def_16,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_15) ),
inference(superposition,[status(thm)],[c_20564,c_155]) ).
tcf(c_28781,plain,
! [X0: $i] :
( ( sbrdtbr0(X0) = iPr_def_16 )
| ~ aElementOf0(X0,iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_28780,c_16903,c_20511]) ).
tcf(c_28862,plain,
( ( sdtlpdtrp0(xN,sK41) = iPr_def_10 )
| ~ aFunction0(xN)
| ~ aElement0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_25426,c_171]) ).
tcf(c_28863,plain,
sdtlpdtrp0(xN,sK41) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_28862,c_261,c_24169]) ).
tcf(c_28997,plain,
sbrdtbr0(sK42) = iPr_def_16,
inference(superposition,[status(thm)],[c_16895,c_28781]) ).
tcf(c_31349,plain,
( ( szszuzczcdt0(sbrdtbr0(sdtmndt0(iPr_def_12,iPr_def_11))) = sbrdtbr0(iPr_def_12) )
| ~ isFinite0(iPr_def_12)
| ~ aSet0(iPr_def_12) ),
inference(superposition,[status(thm)],[c_20750,c_119]) ).
tcf(c_31404,plain,
( ( xK = iPr_def_17 )
| ~ isFinite0(iPr_def_12)
| ~ aSet0(iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_31349,c_16891,c_20541,c_26956,c_28997]) ).
tcf(c_31405,plain,
xK = iPr_def_17,
inference(forward_subsumption_resolution,[status(thm)],[c_31404,c_22565,c_16910]) ).
tcf(c_31636,plain,
( ~ aElementOf0(sK43,xS)
| ( iPr_def_17 != iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_16913,c_31405]) ).
tcf(c_31638,plain,
( aElementOf0(sK43,iPr_def_12)
| ( iPr_def_17 != iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_16912,c_31405]) ).
tcf(c_31640,plain,
aElementOf0(sK43,iPr_def_12),
inference(equality_resolution_simp,[status(thm)],[c_31638]) ).
tcf(c_31642,plain,
~ aElementOf0(sK43,xS),
inference(equality_resolution_simp,[status(thm)],[c_31636]) ).
tcf(c_31930,plain,
( aElementOf0(sK43,sK42)
| ( sK43 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_31640,c_16907]) ).
tcf(c_32039,plain,
( aElementOf0(sK43,iPr_def_14)
| ( sK43 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_31930,c_16898]) ).
tcf(c_32067,plain,
( aElementOf0(sK43,iPr_def_10)
| ( sK43 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_32039,c_16900]) ).
tcf(c_32248,plain,
! [X0: $i] :
( aSubsetOf0(iPr_def_10,sdtlpdtrp0(xN,X0))
| ~ aElementOf0(sK41,szNzAzT0)
| ~ sdtlseqdt0(X0,sK41)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_28863,c_272]) ).
tcf(c_32263,plain,
! [X0: $i] :
( aSubsetOf0(iPr_def_10,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,sK41)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_32248,c_16894]) ).
tcf(c_33828,plain,
( aSubsetOf0(iPr_def_10,xS)
| ~ sdtlseqdt0(sz00,sK41)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(superposition,[status(thm)],[c_263,c_32263]) ).
tcf(c_33834,plain,
aSubsetOf0(iPr_def_10,xS),
inference(forward_subsumption_resolution,[status(thm)],[c_33828,c_20579,c_96]) ).
tcf(c_34862,plain,
( aElementOf0(iPr_def_11,xS)
| ~ aSet0(xS) ),
inference(superposition,[status(thm)],[c_33834,c_23300]) ).
tcf(c_34863,plain,
aElementOf0(iPr_def_11,xS),
inference(forward_subsumption_resolution,[status(thm)],[c_34862,c_195]) ).
tcf(c_41730,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ aElementOf0(sK41,szNzAzT0)
| ~ sdtlseqdt0(X1,sK41)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_28863,c_271]) ).
tcf(c_41736,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,sK41)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41730,c_16894]) ).
tcf(c_46769,plain,
! [X0: $i] :
( aElementOf0(X0,xS)
| ~ sdtlseqdt0(sz00,sK41)
| ~ aElementOf0(sz00,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_263,c_41736]) ).
tcf(c_46785,plain,
! [X0: $i] :
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_46769,c_20579,c_96]) ).
tcf(c_48937,plain,
( aElementOf0(sK43,xS)
| ( sK43 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_32067,c_46785]) ).
tcf(c_48943,plain,
sK43 = iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_48937,c_31642]) ).
tcf(c_49088,plain,
~ aElementOf0(iPr_def_11,xS),
inference(demodulation,[status(thm)],[c_31642,c_48943]) ).
tcf(c_49094,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_49088,c_34863]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM579+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n014.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 04:43:50 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 18.81/3.31 % SZS status Started for theBenchmark.p
% 18.81/3.31 % SZS status Theorem for theBenchmark.p
% 18.81/3.31
% 18.81/3.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 18.81/3.31
% 18.81/3.31 % ------ iProver source info
% 18.81/3.31
% 18.81/3.31 % git: date: 2026-07-19 20:42:38 +0200
% 18.81/3.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 18.81/3.31 % git: non_committed_changes: false
% 18.81/3.31
% 18.81/3.31 % ------ Parsing...
% 18.81/3.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 18.81/3.31
% 18.81/3.31 % ------ Preprocessing... sup_sim: 1 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 18.81/3.31
% 18.81/3.31 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 18.81/3.31
% 18.81/3.31 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 18.81/3.31 % ------ Proving...
% 18.81/3.31 % ------ Problem Properties
% 18.81/3.31
% 18.81/3.31 %
% 18.81/3.31 % clauses 249
% 18.81/3.31 % conjectures 21
% 18.81/3.31 % EPR 65
% 18.81/3.31 % Horn 196
% 18.81/3.31 % unary 43
% 18.81/3.31 % binary 56
% 18.81/3.31 % lits 799
% 18.81/3.31 % lits eq 121
% 18.81/3.31 % fd_pure 0
% 18.81/3.31 % fd_pseudo 0
% 18.81/3.31 % fd_cond 12
% 18.81/3.31 % fd_pseudo_cond 33
% 18.81/3.31 % AC symbols 0
% 18.81/3.31
% 18.81/3.31 % ------ Schedule dynamic 5 is on
% 18.81/3.31
% 18.81/3.31 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 18.81/3.31
% 18.81/3.31
% 18.81/3.31 % ------
% 18.81/3.31 % Current options:
% 18.81/3.31 % ------
% 18.81/3.31
% 18.81/3.31
% 18.81/3.31 %
% 18.81/3.31
% 18.81/3.31 % ------ Proving...
% 18.81/3.31 %
% 18.81/3.31
% 18.81/3.31 % SZS status Theorem for theBenchmark.p
% 18.81/3.31
% 18.81/3.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.81/3.32
% 18.81/3.32
%------------------------------------------------------------------------------