%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM580+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.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 7.33s 1.76s
% Output : CNFRefutation 7.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 17
% Syntax : Number of formulae : 125 ( 35 unt; 6 def)
% Number of atoms : 623 ( 87 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 658 ( 215 ~; 193 |; 201 &)
% ( 15 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 5 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-2 aty)
% Number of variables : 145 ( 0 sgn 142 !; 3 ?; 25 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(f18,axiom,
! [X0,X1] :
( ( aSet0(X1)
& aElement0(X0) )
=> ( ~ aElementOf0(X0,X1)
=> sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDiffCons) ).
fof(f21,axiom,
! [X0] :
( aElement0(X0)
=> ! [X1] :
( ( isFinite0(X1)
& aSet0(X1) )
=> isFinite0(sdtpldt0(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mFConsSet) ).
fof(f41,axiom,
! [X0] :
( aSet0(X0)
=> ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mCardDiff) ).
fof(f80,axiom,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3533) ).
fof(f81,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)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( X1 != szmzizndt0(sdtlpdtrp0(xN,X0))
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3623) ).
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/sandbox/benchmark/theBenchmark.p',m__3671) ).
fof(f85,axiom,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3989) ).
fof(f86,axiom,
( 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))))
& ! [X0] :
( aElementOf0(X0,xQ)
=> aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X0] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( X0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(X0,sdtlpdtrp0(xN,xi))
& aElement0(X0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3989_02) ).
fof(f87,conjecture,
( ( ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [X0] :
( aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( X0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X0,xQ) )
& aElement0(X0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f88,negated_conjecture,
~ ( ( ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [X0] :
( aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( X0 = szmzizndt0(sdtlpdtrp0(xN,xi))
| aElementOf0(X0,xQ) )
& aElement0(X0) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ),
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f98,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)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(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)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(rectify,[],[f81]) ).
fof(f100,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))))
& ! [X2] :
( aElementOf0(X2,xQ)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(rectify,[],[f86]) ).
fof(f101,plain,
~ ( ( ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) )
=> ( ( ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) )
=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ),
inference(rectify,[],[f88]) ).
fof(f102,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f121,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ),
inference(ennf_transformation,[],[f18]) ).
fof(f122,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ),
inference(flattening,[],[f121]) ).
fof(f127,plain,
! [X0] :
( ~ aElement0(X0)
| ! [X1] :
( ~ isFinite0(X1)
| ~ aSet0(X1)
| isFinite0(sdtpldt0(X1,X0)) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f128,plain,
! [X0] :
( ~ aElement0(X0)
| ! [X1] :
( ~ isFinite0(X1)
| ~ aSet0(X1)
| isFinite0(sdtpldt0(X1,X0)) ) ),
inference(flattening,[],[f127]) ).
fof(f151,plain,
! [X0] :
( ~ aSet0(X0)
| ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f155,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f156,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) = sbrdtbr0(X0) ) ),
inference(flattening,[],[f155]) ).
fof(f206,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)) ) )
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(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)) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(ennf_transformation,[],[f98]) ).
fof(f207,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)) ) )
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(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)) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(flattening,[],[f206]) ).
fof(f208,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(f213,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))))
& ! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(ennf_transformation,[],[f100]) ).
fof(f214,plain,
( ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& xK != sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(ennf_transformation,[],[f101]) ).
fof(f215,plain,
( ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
<=> ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& xK != sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(flattening,[],[f214]) ).
fof(f252,plain,
! [X0] :
( ~ aSet0(X0)
| ( ( ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| isFinite0(X0) )
& ( ~ isFinite0(X0)
| aElementOf0(sbrdtbr0(X0),szNzAzT0) ) ) ),
inference(nnf_transformation,[],[f151]) ).
fof(f305,plain,
! [X0] :
( ~ sP9(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP8(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)) ) ),
inference(nnf_transformation,[],[f228]) ).
fof(f306,plain,
! [X0] :
( ~ sP9(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP8(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(rectify,[],[f305]) ).
fof(f310,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))],[f229]) ).
fof(f313,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))))
& ! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( ( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(nnf_transformation,[],[f213]) ).
fof(f314,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))))
& ! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
& aSet0(xQ)
& ! [X1] :
( ( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(flattening,[],[f313]) ).
fof(f315,plain,
( ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& ~ aElementOf0(X1,xQ) )
| ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& xK != sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(nnf_transformation,[],[f215]) ).
fof(f316,plain,
( ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| aElementOf0(X1,xQ) )
& aElement0(X1) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& ~ aElementOf0(X1,xQ) )
| ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& xK != sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(flattening,[],[f315]) ).
fof(f317,plain,
( ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( ( ~ aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X0
| aElementOf0(X0,xQ) )
& aElement0(X0) ) )
& ( ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X0
& ~ aElementOf0(X0,xQ) )
| ~ aElement0(X0)
| aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ) )
& aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
& xK != sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(rectify,[],[f316]) ).
fof(f318,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| aElement0(X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f358,plain,
! [X0,X1] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f122]) ).
fof(f361,plain,
! [X0,X1] :
( ~ aElement0(X0)
| ~ isFinite0(X1)
| ~ aSet0(X1)
| isFinite0(sdtpldt0(X1,X0)) ),
inference(cnf_transformation,[],[f128]) ).
fof(f383,plain,
! [X0] :
( ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| isFinite0(X0) ),
inference(cnf_transformation,[],[f252]) ).
fof(f388,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| ~ isFinite0(X0)
| sbrdtbr0(X0) = szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1))) ),
inference(cnf_transformation,[],[f156]) ).
fof(f516,plain,
xK = szszuzczcdt0(xk),
inference(cnf_transformation,[],[f80]) ).
fof(f517,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f80]) ).
fof(f522,plain,
! [X0] :
( ~ sP9(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f306]) ).
fof(f530,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| sP9(X0) ),
inference(cnf_transformation,[],[f310]) ).
fof(f531,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| aElementOf0(sK39(X0),sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0))
| sP9(X0) ),
inference(cnf_transformation,[],[f310]) ).
fof(f536,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isCountable0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f208]) ).
fof(f537,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f539,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f208]) ).
fof(f547,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f85]) ).
fof(f549,plain,
xk = sbrdtbr0(xQ),
inference(cnf_transformation,[],[f314]) ).
fof(f551,plain,
! [X2] :
( ~ aElementOf0(X2,xQ)
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[],[f314]) ).
fof(f552,plain,
aSet0(xQ),
inference(cnf_transformation,[],[f314]) ).
fof(f561,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)),
inference(cnf_transformation,[],[f317]) ).
fof(f564,plain,
! [X0] :
( szmzizndt0(sdtlpdtrp0(xN,xi)) != X0
| ~ aElement0(X0)
| aElementOf0(X0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[],[f317]) ).
fof(f566,plain,
aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[],[f317]) ).
fof(f567,plain,
xK != sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[],[f317]) ).
fof(f612,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(equality_resolution,[],[f564]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( aElement0(X0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,X1)
| ( sdtmndt0(sdtpldt0(X1,X0),X0) = X1 )
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f358]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( isFinite0(sdtpldt0(X1,X0))
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_115,plain,
! [X0: $i] :
( isFinite0(X0)
| ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f383]) ).
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,[],[f388]) ).
tcf(c_247,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f517]) ).
tcf(c_248,plain,
szszuzczcdt0(xk) = xK,
inference(cnf_transformation,[],[f516]) ).
tcf(c_252,plain,
! [X0: $i] :
( sP8(X0)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f522]) ).
tcf(c_265,plain,
! [X0: $i] :
( sP9(X0)
| aElementOf0(sK39(X0),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f531]) ).
tcf(c_266,plain,
! [X0: $i] :
( sP9(X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_267,plain,
! [X0: $i] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f539]) ).
tcf(c_269,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f537]) ).
tcf(c_270,plain,
! [X0: $i] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f536]) ).
tcf(c_278,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f547]) ).
tcf(c_286,plain,
aSet0(xQ),
inference(cnf_transformation,[],[f552]) ).
tcf(c_287,plain,
! [X0: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[],[f551]) ).
tcf(c_289,plain,
sbrdtbr0(xQ) = xk,
inference(cnf_transformation,[],[f549]) ).
tcf(c_291,negated_conjecture,
sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) != xK,
inference(cnf_transformation,[],[f567]) ).
tcf(c_292,negated_conjecture,
aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),
inference(cnf_transformation,[],[f566]) ).
tcf(c_294,negated_conjecture,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xi))) ),
inference(cnf_transformation,[],[f612]) ).
tcf(c_297,negated_conjecture,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)),
inference(cnf_transformation,[],[f561]) ).
tcf(c_500,plain,
! [X0: $i] :
( sP9(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_265,c_270,c_269,c_266]) ).
tcf(c_16832,definition,
iPr_def_10 = sdtlpdtrp0(xN,xi),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_16833,definition,
iPr_def_11 = szmzizndt0(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_16834,definition,
iPr_def_12 = sdtpldt0(xQ,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_16835,definition,
iPr_def_13 = sbrdtbr0(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_16839,negated_conjecture,
( aElementOf0(iPr_def_11,iPr_def_12)
| ~ aElement0(iPr_def_11) ),
inference(demodulation,[status(thm)],[c_294]) ).
tcf(c_16840,negated_conjecture,
aSet0(iPr_def_12),
inference(demodulation,[status(thm)],[c_292]) ).
tcf(c_16841,negated_conjecture,
iPr_def_13 != xK,
inference(demodulation,[status(thm)],[c_291,c_16835]) ).
tcf(c_16843,negated_conjecture,
aElementOf0(iPr_def_11,iPr_def_10),
inference(demodulation,[status(thm)],[c_297]) ).
tcf(c_20531,plain,
( aSet0(iPr_def_10)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(superposition,[status(thm)],[c_16832,c_267]) ).
tcf(c_20532,plain,
aSet0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_20531,c_278]) ).
tcf(c_20552,plain,
( aElement0(iPr_def_11)
| ~ aSet0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_16843,c_49]) ).
tcf(c_20561,plain,
aElement0(iPr_def_11),
inference(global_subsumption_just,[status(thm)],[c_20552,c_20532,c_20552]) ).
tcf(c_20563,plain,
aElementOf0(iPr_def_11,iPr_def_12),
inference(backward_subsumption_resolution,[status(thm)],[c_16839,c_20561]) ).
tcf(c_20834,plain,
( isFinite0(xQ)
| ~ aSet0(xQ)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(superposition,[status(thm)],[c_289,c_115]) ).
tcf(c_20839,plain,
isFinite0(xQ),
inference(forward_subsumption_resolution,[status(thm)],[c_20834,c_286,c_247]) ).
tcf(c_22440,plain,
( isFinite0(iPr_def_12)
| ~ isFinite0(xQ)
| ~ aSet0(xQ)
| ~ aElement0(iPr_def_11) ),
inference(superposition,[status(thm)],[c_16834,c_92]) ).
tcf(c_22441,plain,
isFinite0(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_22440,c_20839,c_286,c_20561]) ).
tcf(c_23966,plain,
! [X0: $i] :
( aElementOf0(X0,sdtmndt0(iPr_def_10,iPr_def_11))
| ~ aElementOf0(X0,xQ) ),
inference(light_normalisation,[status(thm)],[c_287,c_16832,c_16833]) ).
tcf(c_30447,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_20563,c_119]) ).
fof(f227,definition,
! [X0] :
( ~ sP8(X0)
| ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f228,definition,
! [X0] :
( ~ sP9(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP8(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)) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f229,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)) ) )
| sP9(X0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(definition_folding,[],[f207,f228,f227]) ).
fof(f307,plain,
! [X0] :
( ~ sP8(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)))) ) ) ),
inference(nnf_transformation,[],[f227]) ).
fof(f308,plain,
! [X0] :
( ~ sP8(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)))) ) ) ),
inference(flattening,[],[f307]) ).
fof(f309,plain,
! [X0] :
( ~ sP8(X0)
| ! [X1] :
( ( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ),
inference(rectify,[],[f308]) ).
fof(f526,plain,
! [X0,X1] :
( ~ sP8(X0)
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| szmzizndt0(sdtlpdtrp0(xN,X0)) != X1 ),
inference(cnf_transformation,[],[f309]) ).
fof(f610,plain,
! [X0] :
( ~ sP8(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(equality_resolution,[],[f526]) ).
tcf(c_260,plain,
! [X0: $i] :
( ~ sP8(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f610]) ).
tcf(c_3749,plain,
! [X0: $i,X1: $i] :
( ~ sP9(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_252,c_260]) ).
tcf(c_3750,plain,
! [X0: $i] :
( ~ sP9(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(unflattening,[status(thm)],[c_3749]) ).
tcf(c_3813,plain,
! [X0: $i,X1: $i] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_500,c_3750]) ).
tcf(c_3814,plain,
! [X0: $i] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(unflattening,[status(thm)],[c_3813]) ).
tcf(c_20453,plain,
( ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(szmzizndt0(iPr_def_10),sdtmndt0(iPr_def_10,szmzizndt0(iPr_def_10))) ),
inference(superposition,[status(thm)],[c_16832,c_3814]) ).
tcf(c_20454,plain,
( ~ aElementOf0(xi,szNzAzT0)
| ~ aElementOf0(iPr_def_11,sdtmndt0(iPr_def_10,iPr_def_11)) ),
inference(light_normalisation,[status(thm)],[c_20453,c_16833]) ).
tcf(c_20455,plain,
~ aElementOf0(iPr_def_11,sdtmndt0(iPr_def_10,iPr_def_11)),
inference(forward_subsumption_resolution,[status(thm)],[c_20454,c_278]) ).
tcf(c_23975,plain,
~ aElementOf0(iPr_def_11,xQ),
inference(superposition,[status(thm)],[c_23966,c_20455]) ).
tcf(c_26253,plain,
( ( sdtmndt0(sdtpldt0(xQ,iPr_def_11),iPr_def_11) = xQ )
| ~ aSet0(xQ)
| ~ aElement0(iPr_def_11) ),
inference(superposition,[status(thm)],[c_89,c_23975]) ).
tcf(c_26260,plain,
( ( sdtmndt0(iPr_def_12,iPr_def_11) = xQ )
| ~ aSet0(xQ)
| ~ aElement0(iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_26253,c_16834]) ).
tcf(c_26261,plain,
sdtmndt0(iPr_def_12,iPr_def_11) = xQ,
inference(forward_subsumption_resolution,[status(thm)],[c_26260,c_286,c_20561]) ).
tcf(c_30482,plain,
( ( xK = iPr_def_13 )
| ~ isFinite0(iPr_def_12)
| ~ aSet0(iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_30447,c_248,c_289,c_16835,c_26261]) ).
tcf(c_30483,plain,
xK = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_30482,c_22441,c_16840]) ).
tcf(c_30739,plain,
iPr_def_13 != iPr_def_13,
inference(demodulation,[status(thm)],[c_16841,c_30483]) ).
tcf(c_30744,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_30739]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM580+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 04:47:24 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.44
% 0.10/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.44
% 0.10/0.44 % Detected problem language: tptp
% 0.10/0.45 % Proving...
% 7.33/1.76 % SZS status Started for theBenchmark.p
% 7.33/1.76 % SZS status Theorem for theBenchmark.p
% 7.33/1.76
% 7.33/1.76 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.33/1.76
% 7.33/1.76 % ------ iProver source info
% 7.33/1.76
% 7.33/1.76 % git: date: 2026-07-19 20:42:38 +0200
% 7.33/1.76 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.33/1.76 % git: non_committed_changes: false
% 7.33/1.76
% 7.33/1.76 % ------ Parsing...
% 7.33/1.76 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.33/1.76
% 7.33/1.76 % ------ Preprocessing... sup_sim: 0 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 %
% 7.33/1.76
% 7.33/1.76 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 7.33/1.76
% 7.33/1.76 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 7.33/1.76 % ------ Proving...
% 7.33/1.76 % ------ Problem Properties
% 7.33/1.76
% 7.33/1.76 %
% 7.33/1.76 % clauses 242
% 7.33/1.76 % conjectures 8
% 7.33/1.76 % EPR 53
% 7.33/1.76 % Horn 189
% 7.33/1.76 % unary 39
% 7.33/1.76 % binary 53
% 7.33/1.76 % lits 789
% 7.33/1.76 % lits eq 115
% 7.33/1.76 % fd_pure 0
% 7.33/1.76 % fd_pseudo 0
% 7.33/1.76 % fd_cond 12
% 7.33/1.76 % fd_pseudo_cond 33
% 7.33/1.76 % AC symbols 0
% 7.33/1.76
% 7.33/1.76 % ------ Schedule dynamic 5 is on
% 7.33/1.76
% 7.33/1.76 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 7.33/1.76
% 7.33/1.76
% 7.33/1.76 % ------
% 7.33/1.76 % Current options:
% 7.33/1.76 % ------
% 7.33/1.76
% 7.33/1.76
% 7.33/1.76 %
% 7.33/1.76
% 7.33/1.76 % ------ Proving...
% 7.33/1.76 %
% 7.33/1.76
% 7.33/1.76 % SZS status Theorem for theBenchmark.p
% 7.33/1.76
% 7.33/1.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.33/1.77
% 7.33/1.77
%------------------------------------------------------------------------------