%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM577+1 : 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 : n016.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:05 PM UTC 2026
% Result : Theorem 199.96s 30.72s
% Output : CNFRefutation 199.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 20
% Syntax : Number of formulae : 168 ( 22 unt; 2 def)
% Number of atoms : 659 ( 89 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 851 ( 360 ~; 354 |; 104 &)
% ( 14 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-3 aty)
% Number of variables : 254 ( 0 sgn 245 !; 9 ?; 94 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f6,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEmpFin) ).
fof(f8,axiom,
! [X0] :
( ( isCountable0(X0)
& aSet0(X0) )
=> ~ isFinite0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin) ).
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(f14,axiom,
! [X0,X1,X2] :
( ( aSet0(X2)
& aSet0(X1)
& aSet0(X0) )
=> ( ( aSubsetOf0(X1,X2)
& aSubsetOf0(X0,X1) )
=> aSubsetOf0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubTrans) ).
fof(f16,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aSet0(X0) )
=> ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& aSet0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNATSet) ).
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(f34,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessRefl) ).
fof(f47,axiom,
! [X0] :
( ( X0 != slcrc0
& aSubsetOf0(X0,szNzAzT0) )
=> ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( ! [X2] :
( aElementOf0(X2,X0)
=> sdtlseqdt0(X1,X2) )
& aElementOf0(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefMin) ).
fof(f81,axiom,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3623) ).
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ) ),
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)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3754) ).
fof(f86,axiom,
( aElementOf0(xm,szNzAzT0)
& aElementOf0(xn,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3904) ).
fof(f87,conjecture,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
=> ( szmzizndt0(sdtlpdtrp0(xN,xm)) != szmzizndt0(sdtlpdtrp0(xN,xn))
& aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f88,negated_conjecture,
~ ( sdtlseqdt0(szszuzczcdt0(xn),xm)
=> ( szmzizndt0(sdtlpdtrp0(xN,xm)) != szmzizndt0(sdtlpdtrp0(xN,xn))
& aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ),
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f96,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f98,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f99,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(flattening,[],[f98]) ).
fof(f102,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| aSubsetOf0(X0,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| aSubsetOf0(X0,X2) ),
inference(flattening,[],[f108]) ).
fof(f112,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& aSet0(X2) ) ) ),
inference(ennf_transformation,[],[f16]) ).
fof(f113,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& aSet0(X2) ) ) ),
inference(flattening,[],[f112]) ).
fof(f125,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f136,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(X0,X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f155,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X0)
| sdtlseqdt0(X1,X2) )
& aElementOf0(X1,X0) ) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f156,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X0)
| sdtlseqdt0(X1,X2) )
& aElementOf0(X1,X0) ) ) ),
inference(flattening,[],[f155]) ).
fof(f197,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(ennf_transformation,[],[f81]) ).
fof(f198,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(flattening,[],[f197]) ).
fof(f199,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ) ),
inference(ennf_transformation,[],[f82]) ).
fof(f200,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ),
inference(ennf_transformation,[],[f83]) ).
fof(f201,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ),
inference(flattening,[],[f200]) ).
fof(f204,plain,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
& ( szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ),
inference(ennf_transformation,[],[f88]) ).
fof(f215,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,[],[f102]) ).
fof(f216,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,[],[f215]) ).
fof(f217,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,[],[f216]) ).
fof(f218,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ( aElementOf0(sK5(X0,X1),X1)
& ~ aElementOf0(sK5(X0,X1),X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f217]) ).
fof(f225,plain,
! [X1,X0] :
( ~ sP3(X1,X0)
| ! [X2] :
( ( sdtmndt0(X0,X1) != X2
| sP2(X2,X0,X1) )
& ( ~ sP2(X2,X0,X1)
| X2 = sdtmndt0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f209]) ).
fof(f226,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| ! [X2] :
( ( sdtmndt0(X1,X0) != X2
| sP2(X2,X1,X0) )
& ( ~ sP2(X2,X1,X0)
| sdtmndt0(X1,X0) = X2 ) ) ),
inference(rectify,[],[f225]) ).
fof(f236,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| ! [X1] :
( ( szmzizndt0(X0) != X1
| ( ! [X2] :
( ~ aElementOf0(X2,X0)
| sdtlseqdt0(X1,X2) )
& aElementOf0(X1,X0) ) )
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ sdtlseqdt0(X1,X2) )
| ~ aElementOf0(X1,X0)
| X1 = szmzizndt0(X0) ) ) ),
inference(nnf_transformation,[],[f156]) ).
fof(f237,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| ! [X1] :
( ( szmzizndt0(X0) != X1
| ( ! [X2] :
( ~ aElementOf0(X2,X0)
| sdtlseqdt0(X1,X2) )
& aElementOf0(X1,X0) ) )
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ sdtlseqdt0(X1,X2) )
| ~ aElementOf0(X1,X0)
| X1 = szmzizndt0(X0) ) ) ),
inference(flattening,[],[f236]) ).
fof(f238,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| ! [X1] :
( ( szmzizndt0(X0) != X1
| ( ! [X3] :
( ~ aElementOf0(X3,X0)
| sdtlseqdt0(X1,X3) )
& aElementOf0(X1,X0) ) )
& ( ? [X2] :
( aElementOf0(X2,X0)
& ~ sdtlseqdt0(X1,X2) )
| ~ aElementOf0(X1,X0)
| X1 = szmzizndt0(X0) ) ) ),
inference(rectify,[],[f237]) ).
fof(f239,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| ! [X1] :
( ( szmzizndt0(X0) != X1
| ( ! [X3] :
( ~ aElementOf0(X3,X0)
| sdtlseqdt0(X1,X3) )
& aElementOf0(X1,X0) ) )
& ( ( aElementOf0(sK10(X0,X1),X0)
& ~ sdtlseqdt0(X1,sK10(X0,X1)) )
| ~ aElementOf0(X1,X0)
| X1 = szmzizndt0(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f238]) ).
fof(f271,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| aElement0(X1) ),
inference(cnf_transformation,[],[f96]) ).
fof(f275,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[],[f6]) ).
fof(f276,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f278,plain,
! [X3,X0,X1] :
( ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) ),
inference(cnf_transformation,[],[f218]) ).
fof(f279,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| aSet0(X1) ),
inference(cnf_transformation,[],[f218]) ).
fof(f285,plain,
! [X2,X0,X1] :
( ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| aSubsetOf0(X0,X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f298,plain,
! [X2,X0,X1] :
( ~ sP3(X0,X1)
| sdtmndt0(X1,X0) != X2
| sP2(X2,X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f309,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| sP3(X1,X0) ),
inference(cnf_transformation,[],[f210]) ).
fof(f317,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f320,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(szszuzczcdt0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f330,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(X0,X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f346,plain,
! [X0,X1] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| szmzizndt0(X0) != X1
| aElementOf0(X1,X0) ),
inference(cnf_transformation,[],[f239]) ).
fof(f431,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f198]) ).
fof(f435,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isCountable0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f199]) ).
fof(f436,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f437,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f201]) ).
fof(f441,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f86]) ).
fof(f442,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f86]) ).
fof(f443,plain,
sdtlseqdt0(szszuzczcdt0(xn),xm),
inference(cnf_transformation,[],[f204]) ).
fof(f444,plain,
( szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(cnf_transformation,[],[f204]) ).
fof(f450,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| sP2(sdtmndt0(X1,X0),X1,X0) ),
inference(equality_resolution,[],[f298]) ).
fof(f453,plain,
! [X0] :
( slcrc0 = X0
| ~ aSubsetOf0(X0,szNzAzT0)
| aElementOf0(szmzizndt0(X0),X0) ),
inference(equality_resolution,[],[f346]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( aElement0(X0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_53,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[],[f275]) ).
tcf(c_54,plain,
! [X0: $i] :
( ~ isCountable0(X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( aSet0(X0)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( aSubsetOf0(X2,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f450]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( sP3(X0,X1)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_94,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f317]) ).
tcf(c_97,plain,
! [X0: $i] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_108,plain,
! [X0: $i] :
( sdtlseqdt0(X0,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f330]) ).
tcf(c_125,plain,
! [X0: $i] :
( aElementOf0(szmzizndt0(X0),X0)
| ( X0 = slcrc0 )
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f453]) ).
tcf(c_211,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f431]) ).
tcf(c_213,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f436]) ).
tcf(c_214,plain,
! [X0: $i] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f435]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X1),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f437]) ).
tcf(c_219,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f442]) ).
tcf(c_220,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f441]) ).
tcf(c_221,negated_conjecture,
( ( szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)) )
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(cnf_transformation,[],[f444]) ).
tcf(c_222,negated_conjecture,
sdtlseqdt0(szszuzczcdt0(xn),xm),
inference(cnf_transformation,[],[f443]) ).
tcf(c_354,plain,
! [X0: $i,X1: $i,X2: $i] :
( aSubsetOf0(X2,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_63,c_58,c_63]) ).
tcf(c_355,plain,
! [X0: $i,X1: $i,X2: $i] :
( aSubsetOf0(X2,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(renaming,[status(thm)],[c_354]) ).
tcf(c_356,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_211,c_214,c_213,c_211]) ).
tcf(c_1628,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP2(sdtmndt0(X3,X1),X3,X1)
| ~ aSet0(X2)
| ~ aElement0(X0)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_87,c_77]) ).
tcf(c_1629,plain,
! [X0: $i,X1: $i] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ aSet0(X1)
| ~ aElement0(X0) ),
inference(unflattening,[status(thm)],[c_1628]) ).
tcf(c_12461,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_12465,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( aElementOf0(X0,X2)
| ~ aElementOf0(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_12467,plain,
! [X0: $i,X1: $i] :
( isFinite0(X0)
| ~ isFinite0(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_15159,plain,
! [X0: $i] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aSet0(szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_213,c_58]) ).
tcf(c_15207,plain,
! [X0: $i,X1: $i] :
( aSet0(sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1)
| ~ aSet0(sdtlpdtrp0(xN,X0)) ),
inference(superposition,[status(thm)],[c_215,c_58]) ).
tcf(c_15241,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))
| ( sdtlpdtrp0(xN,xm) = slcrc0 )
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_15251,plain,
sdtlpdtrp0(xN,xm) = sdtlpdtrp0(xN,xm),
inference(instantiation,[status(thm)],[c_12461]) ).
tcf(c_15298,plain,
! [X0: $i,X1: $i] :
( aSet0(sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_15207,c_94,c_15159,c_15207]) ).
tcf(c_15305,plain,
( aSet0(sdtlpdtrp0(xN,xm))
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(superposition,[status(thm)],[c_222,c_15298]) ).
tcf(c_15323,plain,
( aSet0(sdtlpdtrp0(xN,xm))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_15305,c_220,c_15305]) ).
tcf(c_15325,plain,
( aSet0(sdtlpdtrp0(xN,xm))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(superposition,[status(thm)],[c_97,c_15323]) ).
tcf(c_19306,plain,
sdtlseqdt0(xn,xn),
inference(superposition,[status(thm)],[c_219,c_108]) ).
tcf(c_19307,plain,
sdtlseqdt0(xm,xm),
inference(superposition,[status(thm)],[c_220,c_108]) ).
tcf(c_19392,plain,
( aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_19396,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_19397,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_19402,plain,
( isCountable0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_19403,plain,
( isCountable0(sdtlpdtrp0(xN,xm))
| ~ aElementOf0(xm,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_19446,plain,
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_356]) ).
tcf(c_19462,plain,
! [X0: $i] :
( isFinite0(X0)
| ~ isFinite0(slcrc0)
| ( X0 != slcrc0 ) ),
inference(instantiation,[status(thm)],[c_12467]) ).
tcf(c_19516,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(xm,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_19531,plain,
! [X0: $i,X1: $i] :
( aSet0(sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1)
| ~ aSet0(sdtlpdtrp0(xN,X0)) ),
inference(superposition,[status(thm)],[c_215,c_58]) ).
tcf(c_19536,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aSet0(sdtlpdtrp0(xN,xm))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),X0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_19828,plain,
! [X0: $i,X1: $i] :
( aSet0(sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_19531,c_94,c_15159,c_15207]) ).
tcf(c_19842,plain,
( aSet0(sdtlpdtrp0(xN,xm))
| ~ aElementOf0(xm,szNzAzT0) ),
inference(superposition,[status(thm)],[c_19307,c_19828]) ).
tcf(c_19843,plain,
( aSet0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(superposition,[status(thm)],[c_19306,c_19828]) ).
tcf(c_19903,plain,
aSet0(sdtlpdtrp0(xN,xm)),
inference(global_subsumption_just,[status(thm)],[c_19842,c_219,c_15325]) ).
tcf(c_19906,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xm))
| ~ isFinite0(sdtlpdtrp0(xN,xm)) ),
inference(superposition,[status(thm)],[c_19903,c_54]) ).
tcf(c_19914,plain,
aSet0(sdtlpdtrp0(xN,xn)),
inference(global_subsumption_just,[status(thm)],[c_19843,c_219,c_19843]) ).
tcf(c_19917,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xn))
| ~ isFinite0(sdtlpdtrp0(xN,xn)) ),
inference(superposition,[status(thm)],[c_19914,c_54]) ).
tcf(c_20358,plain,
! [X0: $i] :
( aElement0(szmzizndt0(X0))
| ~ aSet0(X0)
| ~ aElementOf0(szmzizndt0(X0),X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_20382,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,X2)
| ~ aElementOf0(szmzizndt0(X1),X1)
| ( X2 != X1 )
| ( X0 != szmzizndt0(X1) ) ),
inference(instantiation,[status(thm)],[c_12465]) ).
tcf(c_20823,plain,
( isFinite0(sdtlpdtrp0(xN,xm))
| ~ isFinite0(slcrc0)
| ( sdtlpdtrp0(xN,xm) != slcrc0 ) ),
inference(instantiation,[status(thm)],[c_19462]) ).
tcf(c_22455,plain,
! [X0: $i,X1: $i] :
( sP2(sdtmndt0(X1,szmzizndt0(X0)),X1,szmzizndt0(X0))
| ~ aSet0(X1)
| ~ aElement0(szmzizndt0(X0)) ),
inference(instantiation,[status(thm)],[c_1629]) ).
tcf(c_24719,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(szmzizndt0(X0),X2)
| ~ aElementOf0(szmzizndt0(X1),X1)
| ( X2 != X1 )
| ( szmzizndt0(X0) != szmzizndt0(X1) ) ),
inference(instantiation,[status(thm)],[c_20382]) ).
tcf(c_31556,plain,
( sP2(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))
| ~ aSet0(sdtlpdtrp0(xN,xn))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn))) ),
inference(instantiation,[status(thm)],[c_22455]) ).
tcf(c_33468,plain,
( aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| ~ aSet0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) ),
inference(instantiation,[status(thm)],[c_20358]) ).
tcf(c_44265,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| ( sdtlpdtrp0(xN,xn) = slcrc0 )
| ~ aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_44691,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aElementOf0(szmzizndt0(X0),X0)
| ( X1 != X0 )
| ( szmzizndt0(sdtlpdtrp0(xN,xn)) != szmzizndt0(X0) ) ),
inference(instantiation,[status(thm)],[c_24719]) ).
tcf(c_47046,plain,
( isFinite0(sdtlpdtrp0(xN,xn))
| ~ isFinite0(slcrc0)
| ( sdtlpdtrp0(xN,xn) != slcrc0 ) ),
inference(instantiation,[status(thm)],[c_19462]) ).
tcf(c_52594,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aSet0(sdtlpdtrp0(xN,xm))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(instantiation,[status(thm)],[c_19536]) ).
tcf(c_58760,plain,
! [X0: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))
| ( X0 != sdtlpdtrp0(xN,xm) )
| ( szmzizndt0(sdtlpdtrp0(xN,xn)) != szmzizndt0(sdtlpdtrp0(xN,xm)) ) ),
inference(instantiation,[status(thm)],[c_44691]) ).
tcf(c_66904,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm))
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))
| ( sdtlpdtrp0(xN,xm) != sdtlpdtrp0(xN,xm) )
| ( szmzizndt0(sdtlpdtrp0(xN,xn)) != szmzizndt0(sdtlpdtrp0(xN,xm)) ) ),
inference(instantiation,[status(thm)],[c_58760]) ).
fof(f208,definition,
! [X2,X0,X1] :
( sP2(X2,X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& aSet0(X2) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f209,definition,
! [X1,X0] :
( ~ sP3(X1,X0)
| ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> sP2(X2,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f210,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| sP3(X1,X0) ),
inference(definition_folding,[],[f113,f209,f208]) ).
fof(f227,plain,
! [X2,X0,X1] :
( ( ~ sP2(X2,X0,X1)
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& ( X1 = X3
| ~ aElementOf0(X3,X0)
| ~ aElement0(X3)
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& ( ~ aElementOf0(X3,X2)
| X1 = X3
| ~ aElementOf0(X3,X0)
| ~ aElement0(X3) ) )
| ~ aSet0(X2)
| sP2(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f208]) ).
fof(f228,plain,
! [X2,X0,X1] :
( ( ~ sP2(X2,X0,X1)
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& ( X1 = X3
| ~ aElementOf0(X3,X0)
| ~ aElement0(X3)
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( X3 != X1
& aElementOf0(X3,X0)
& aElement0(X3) ) )
& ( ~ aElementOf0(X3,X2)
| X1 = X3
| ~ aElementOf0(X3,X0)
| ~ aElement0(X3) ) )
| ~ aSet0(X2)
| sP2(X2,X0,X1) ) ),
inference(flattening,[],[f227]) ).
fof(f229,plain,
! [X0,X1,X2] :
( ( ~ sP2(X0,X1,X2)
| ( ! [X4] :
( ( ~ aElementOf0(X4,X0)
| ( X2 != X4
& aElementOf0(X4,X1)
& aElement0(X4) ) )
& ( X2 = X4
| ~ aElementOf0(X4,X1)
| ~ aElement0(X4)
| aElementOf0(X4,X0) ) )
& aSet0(X0) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X0)
| ( X2 != X3
& aElementOf0(X3,X1)
& aElement0(X3) ) )
& ( ~ aElementOf0(X3,X0)
| X2 = X3
| ~ aElementOf0(X3,X1)
| ~ aElement0(X3) ) )
| ~ aSet0(X0)
| sP2(X0,X1,X2) ) ),
inference(rectify,[],[f228]) ).
fof(f230,plain,
! [X0,X1,X2] :
( ( ~ sP2(X0,X1,X2)
| ( ! [X4] :
( ( ~ aElementOf0(X4,X0)
| ( X2 != X4
& aElementOf0(X4,X1)
& aElement0(X4) ) )
& ( X2 = X4
| ~ aElementOf0(X4,X1)
| ~ aElement0(X4)
| aElementOf0(X4,X0) ) )
& aSet0(X0) ) )
& ( ( ( aElementOf0(sK7(X0,X1,X2),X0)
| ( sK7(X0,X1,X2) != X2
& aElementOf0(sK7(X0,X1,X2),X1)
& aElement0(sK7(X0,X1,X2)) ) )
& ( ~ aElementOf0(sK7(X0,X1,X2),X0)
| sK7(X0,X1,X2) = X2
| ~ aElementOf0(sK7(X0,X1,X2),X1)
| ~ aElement0(sK7(X0,X1,X2)) ) )
| ~ aSet0(X0)
| sP2(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f229]) ).
fof(f300,plain,
! [X2,X0,X1,X4] :
( ~ sP2(X0,X1,X2)
| ~ aElementOf0(X4,X0)
| X2 != X4 ),
inference(cnf_transformation,[],[f230]) ).
fof(f304,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f451,plain,
! [X0,X1,X4] :
( ~ sP2(X0,X1,X4)
| ~ aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f300]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] :
( aSet0(X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ aElementOf0(X2,X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f451]) ).
tcf(c_19606,plain,
! [X0: $i,X1: $i] :
( aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ sP2(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_31557,plain,
( aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ sP2(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) ),
inference(instantiation,[status(thm)],[c_19606]) ).
tcf(c_166442,negated_conjecture,
szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)),
inference(global_subsumption_just,[status(thm)],[c_221,c_53,c_220,c_219,c_222,c_221,c_15325,c_19392,c_19396,c_19402,c_19446,c_19516,c_19843,c_19917,c_31556,c_31557,c_33468,c_44265,c_47046,c_52594]) ).
tcf(c_166475,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm))
| ( sdtlpdtrp0(xN,xm) = slcrc0 )
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(superposition,[status(thm)],[c_166442,c_125]) ).
tcf(c_166492,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm)),
inference(global_subsumption_just,[status(thm)],[c_166475,c_53,c_220,c_219,c_222,c_221,c_15241,c_15251,c_15325,c_19392,c_19396,c_19397,c_19402,c_19403,c_19446,c_19516,c_19843,c_19906,c_19917,c_20823,c_31556,c_31557,c_33468,c_44265,c_47046,c_52594,c_66904]) ).
tcf(c_166501,plain,
! [X0: $i,X1: $i] :
( ~ aSet0(X1)
| ~ aElement0(X0)
| ~ aElementOf0(X0,sdtmndt0(X1,X0)) ),
inference(superposition,[status(thm)],[c_1629,c_86]) ).
tcf(c_166513,plain,
! [X0: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),X0) ),
inference(superposition,[status(thm)],[c_166492,c_59]) ).
tcf(c_166527,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),X0) ),
inference(superposition,[status(thm)],[c_166513,c_59]) ).
tcf(c_166552,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aSet0(X1)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),X0)
| ~ aSubsetOf0(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_166527,c_58,c_166527]) ).
tcf(c_166553,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),X0) ),
inference(renaming,[status(thm)],[c_166552]) ).
tcf(c_166745,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aSet0(X1)
| ~ aElementOf0(xm,szNzAzT0)
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),X1) ),
inference(superposition,[status(thm)],[c_215,c_166553]) ).
tcf(c_167008,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aSet0(X1)
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),X1)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,xm) ),
inference(global_subsumption_just,[status(thm)],[c_166745,c_220,c_166745]) ).
tcf(c_167009,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1)
| ~ aSet0(X1)
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),X1) ),
inference(renaming,[status(thm)],[c_167008]) ).
tcf(c_167013,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X1,xm)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1)
| ~ aSet0(sdtlpdtrp0(xN,X0)) ),
inference(superposition,[status(thm)],[c_215,c_167009]) ).
tcf(c_168071,plain,
! [X0: $i,X1: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X1,xm)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_167013,c_94,c_15159,c_167013]) ).
tcf(c_168079,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ sdtlseqdt0(xm,xm)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(superposition,[status(thm)],[c_222,c_168071]) ).
tcf(c_168188,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(global_subsumption_just,[status(thm)],[c_168079,c_220,c_219,c_19307,c_19392,c_168079]) ).
tcf(c_168191,plain,
! [X0: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),X0) ),
inference(superposition,[status(thm)],[c_168188,c_59]) ).
tcf(c_168206,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aElementOf0(xn,szNzAzT0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(superposition,[status(thm)],[c_356,c_168191]) ).
tcf(c_168436,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
inference(global_subsumption_just,[status(thm)],[c_168206,c_53,c_219,c_19396,c_19402,c_19843,c_19917,c_31556,c_31557,c_33468,c_44265,c_47046,c_168206]) ).
tcf(c_168442,plain,
( ~ aSet0(sdtlpdtrp0(xN,xn))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn))) ),
inference(superposition,[status(thm)],[c_168436,c_166501]) ).
tcf(c_168447,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_168442,c_47046,c_44265,c_33468,c_19917,c_19843,c_19402,c_19396,c_219,c_53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM577+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.44 % Computer : n016.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Thu Sep 24 04:47:42 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.22/0.50 Running first-order theorem proving
% 0.22/0.50 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.22/0.52
% 0.22/0.52 % ======== iProver multi-core TPTP/SMT =========
% 0.22/0.52
% 0.22/0.52 % Detected problem language: tptp
% 0.22/0.54 % Proving...
% 199.96/30.72 % SZS status Started for theBenchmark.p
% 199.96/30.72 % SZS status Theorem for theBenchmark.p
% 199.96/30.72
% 199.96/30.72 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 199.96/30.72
% 199.96/30.72 % ------ iProver source info
% 199.96/30.72
% 199.96/30.72 % git: date: 2026-07-19 20:42:38 +0200
% 199.96/30.72 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 199.96/30.72 % git: non_committed_changes: false
% 199.96/30.72
% 199.96/30.72 % ------ Parsing...
% 199.96/30.72 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 199.96/30.72
% 199.96/30.72 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 199.96/30.72
% 199.96/30.72 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 199.96/30.72
% 199.96/30.72 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 199.96/30.72 % ------ Proving...
% 199.96/30.72 % ------ Problem Properties
% 199.96/30.72
% 199.96/30.72 %
% 199.96/30.72 % clauses 170
% 199.96/30.72 % conjectures 2
% 199.96/30.72 % EPR 42
% 199.96/30.72 % Horn 130
% 199.96/30.72 % unary 28
% 199.96/30.72 % binary 22
% 199.96/30.72 % lits 594
% 199.96/30.72 % lits eq 92
% 199.96/30.72 % fd_pure 0
% 199.96/30.72 % fd_pseudo 0
% 199.96/30.72 % fd_cond 10
% 199.96/30.72 % fd_pseudo_cond 24
% 199.96/30.72 % AC symbols 0
% 199.96/30.72
% 199.96/30.72 % ------ Input Options Time Limit: Unbounded
% 199.96/30.72
% 199.96/30.72
% 199.96/30.72 % ------
% 199.96/30.72 % Current options:
% 199.96/30.72 % ------
% 199.96/30.72
% 199.96/30.72
% 199.96/30.72 %
% 199.96/30.72
% 199.96/30.72 % ------ Proving...
% 199.96/30.72 %
% 199.96/30.72
% 199.96/30.72 % ------ Proving...
% 199.96/30.72 %
% 199.96/30.72
% 199.96/30.72 % ------ Proving...
% 199.96/30.72 %
% 199.96/30.72
% 199.96/30.72 % SZS status Theorem for theBenchmark.p
% 199.96/30.72
% 199.96/30.72 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 199.96/30.73
% 199.96/30.73
%------------------------------------------------------------------------------