%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM575+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 : n009.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 13.47s 3.35s
% Output : CNFRefutation 13.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 21
% Syntax : Number of formulae : 197 ( 44 unt; 6 def)
% Number of atoms : 913 ( 124 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1094 ( 422 ~; 399 |; 215 &)
% ( 20 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 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 : 16 ( 14 usr; 5 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 277 ( 0 sgn 264 !; 13 ?; 65 :)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(f35,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X0)
& sdtlseqdt0(X0,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessASymm) ).
fof(f37,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessTotal) ).
fof(f41,axiom,
! [X0] :
( aSet0(X0)
=> ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardNum) ).
fof(f45,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( ( aSubsetOf0(X1,X0)
& isFinite0(X0) )
=> sdtlseqdt0(sbrdtbr0(X1),sbrdtbr0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardSub) ).
fof(f50,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
<=> ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& aSet0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSeg) ).
fof(f51,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> isFinite0(slbdtrb0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegFin) ).
fof(f54,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( sdtlseqdt0(X0,X1)
<=> aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegLess) ).
fof(f56,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sbrdtbr0(slbdtrb0(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardSeg) ).
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(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/sandbox2/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/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(f84,conjecture,
! [X0,X1] :
( ( X0 != X1
& aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ~ ( szmzizndt0(sdtlpdtrp0(xN,X0)) = szmzizndt0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f85,negated_conjecture,
~ ! [X0,X1] :
( ( X0 != X1
& aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ~ ( szmzizndt0(sdtlpdtrp0(xN,X0)) = szmzizndt0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(negated_conjecture,[status(cth)],[f84]) ).
fof(f95,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(f96,plain,
~ ! [X0,X1] :
( ( X0 != X1
& aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ~ ( szmzizndt0(sdtlpdtrp0(xN,X0)) = szmzizndt0(sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(rectify,[],[f85]) ).
fof(f126,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f138,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f35]) ).
fof(f139,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f138]) ).
fof(f142,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ),
inference(ennf_transformation,[],[f37]) ).
fof(f143,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ),
inference(flattening,[],[f142]) ).
fof(f146,plain,
! [X0] :
( ~ aSet0(X0)
| ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f152,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| sdtlseqdt0(sbrdtbr0(X1),sbrdtbr0(X0)) ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f153,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| sdtlseqdt0(sbrdtbr0(X1),sbrdtbr0(X0)) ) ),
inference(flattening,[],[f152]) ).
fof(f162,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
<=> ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f163,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isFinite0(slbdtrb0(X0)) ),
inference(ennf_transformation,[],[f51]) ).
fof(f166,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( sdtlseqdt0(X0,X1)
<=> aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f167,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( sdtlseqdt0(X0,X1)
<=> aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1)) ) ),
inference(flattening,[],[f166]) ).
fof(f170,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sbrdtbr0(slbdtrb0(X0)) = X0 ),
inference(ennf_transformation,[],[f56]) ).
fof(f184,plain,
! [X0] :
( ~ aFunction0(X0)
| ! [X1] :
( ~ aElementOf0(X1,szDzozmdt0(X0))
| aElement0(sdtlpdtrp0(X0,X1)) ) ),
inference(ennf_transformation,[],[f65]) ).
fof(f185,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(f186,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,[],[f185]) ).
fof(f201,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,[],[f95]) ).
fof(f202,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,[],[f201]) ).
fof(f203,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(f204,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(f205,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,[],[f204]) ).
fof(f206,plain,
? [X0,X1] :
( X0 != X1
& aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0)
& szmzizndt0(sdtlpdtrp0(xN,X0)) = szmzizndt0(sdtlpdtrp0(xN,X1))
& ! [X3] :
( ~ aElementOf0(X3,sdtlpdtrp0(xN,X1))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ),
inference(ennf_transformation,[],[f96]) ).
fof(f207,plain,
? [X0,X1] :
( X0 != X1
& aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0)
& szmzizndt0(sdtlpdtrp0(xN,X0)) = szmzizndt0(sdtlpdtrp0(xN,X1))
& ! [X3] :
( ~ aElementOf0(X3,sdtlpdtrp0(xN,X1))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ),
inference(flattening,[],[f206]) ).
fof(f244,plain,
! [X0] :
( ~ aSet0(X0)
| ( ( ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| isFinite0(X0) )
& ( ~ isFinite0(X0)
| aElementOf0(sbrdtbr0(X0),szNzAzT0) ) ) ),
inference(nnf_transformation,[],[f146]) ).
fof(f255,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X2] :
( ( ~ aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0)
| aElementOf0(X2,X1) ) )
& aSet0(X1) ) )
& ( ? [X2] :
( ( aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ aElementOf0(X2,X1)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(nnf_transformation,[],[f162]) ).
fof(f256,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X2] :
( ( ~ aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0)
| aElementOf0(X2,X1) ) )
& aSet0(X1) ) )
& ( ? [X2] :
( ( aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ aElementOf0(X2,X1)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(flattening,[],[f255]) ).
fof(f257,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X3] :
( ( ~ aElementOf0(X3,X1)
| ( sdtlseqdt0(szszuzczcdt0(X3),X0)
& aElementOf0(X3,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),X0)
| ~ aElementOf0(X3,szNzAzT0)
| aElementOf0(X3,X1) ) )
& aSet0(X1) ) )
& ( ? [X2] :
( ( aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ aElementOf0(X2,X1)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(rectify,[],[f256]) ).
fof(f258,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X3] :
( ( ~ aElementOf0(X3,X1)
| ( sdtlseqdt0(szszuzczcdt0(X3),X0)
& aElementOf0(X3,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),X0)
| ~ aElementOf0(X3,szNzAzT0)
| aElementOf0(X3,X1) ) )
& aSet0(X1) ) )
& ( ( ( aElementOf0(sK18(X0,X1),X1)
| ( sdtlseqdt0(szszuzczcdt0(sK18(X0,X1)),X0)
& aElementOf0(sK18(X0,X1),szNzAzT0) ) )
& ( ~ aElementOf0(sK18(X0,X1),X1)
| ~ sdtlseqdt0(szszuzczcdt0(sK18(X0,X1)),X0)
| ~ aElementOf0(sK18(X0,X1),szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0,X1))],[f257]) ).
fof(f261,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( ( ~ sdtlseqdt0(X0,X1)
| aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1)) )
& ( ~ aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1))
| sdtlseqdt0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f268,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,[],[f186]) ).
fof(f269,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,[],[f268]) ).
fof(f270,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,[],[f269]) ).
fof(f271,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))],[f270]) ).
fof(f297,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,[],[f220]) ).
fof(f298,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,[],[f297]) ).
fof(f302,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))],[f221]) ).
fof(f303,plain,
( sK40 != sK41
& aElementOf0(sK41,szNzAzT0)
& aElementOf0(sK40,szNzAzT0)
& szmzizndt0(sdtlpdtrp0(xN,sK40)) = szmzizndt0(sdtlpdtrp0(xN,sK41))
& ! [X3] :
( ~ aElementOf0(X3,sdtlpdtrp0(xN,sK41))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK40)),X3) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK40)),sdtlpdtrp0(xN,sK41))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,sK40))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,sK40)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK40)),sdtlpdtrp0(xN,sK40)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40,sK41]),skolemize(X0,sK40),skolemize(X1,sK41)],[f207]) ).
fof(f353,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(szszuzczcdt0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f364,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f139]) ).
fof(f366,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f143]) ).
fof(f370,plain,
! [X0] :
( ~ aSet0(X0)
| ~ isFinite0(X0)
| aElementOf0(sbrdtbr0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f244]) ).
fof(f375,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ isFinite0(X0)
| sdtlseqdt0(sbrdtbr0(X1),sbrdtbr0(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f390,plain,
! [X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| slbdtrb0(X0) != X1
| aSet0(X1) ),
inference(cnf_transformation,[],[f258]) ).
fof(f394,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isFinite0(slbdtrb0(X0)) ),
inference(cnf_transformation,[],[f163]) ).
fof(f399,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1)
| aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1)) ),
inference(cnf_transformation,[],[f261]) ).
fof(f403,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sbrdtbr0(slbdtrb0(X0)) = X0 ),
inference(cnf_transformation,[],[f170]) ).
fof(f419,plain,
! [X0,X1] :
( ~ aFunction0(X0)
| ~ aElementOf0(X1,szDzozmdt0(X0))
| aElement0(sdtlpdtrp0(X0,X1)) ),
inference(cnf_transformation,[],[f184]) ).
fof(f420,plain,
! [X2,X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| sdtlbdtrb0(X0,X1) != X2
| ~ aElementOf0(X4,X2)
| sdtlpdtrp0(X0,X4) = X1 ),
inference(cnf_transformation,[],[f271]) ).
fof(f422,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,[],[f271]) ).
fof(f506,plain,
! [X2,X0] :
( ~ sP9(X0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f298]) ).
fof(f508,plain,
! [X0] :
( ~ sP9(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f298]) ).
fof(f516,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| sP9(X0) ),
inference(cnf_transformation,[],[f302]) ).
fof(f517,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| aElementOf0(sK39(X0),sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0))
| sP9(X0) ),
inference(cnf_transformation,[],[f302]) ).
fof(f520,plain,
szNzAzT0 = szDzozmdt0(xN),
inference(cnf_transformation,[],[f302]) ).
fof(f521,plain,
aFunction0(xN),
inference(cnf_transformation,[],[f302]) ).
fof(f522,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isCountable0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f203]) ).
fof(f523,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f527,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,[],[f205]) ).
fof(f528,plain,
sK40 != sK41,
inference(cnf_transformation,[],[f303]) ).
fof(f529,plain,
aElementOf0(sK41,szNzAzT0),
inference(cnf_transformation,[],[f303]) ).
fof(f530,plain,
aElementOf0(sK40,szNzAzT0),
inference(cnf_transformation,[],[f303]) ).
fof(f531,plain,
szmzizndt0(sdtlpdtrp0(xN,sK40)) = szmzizndt0(sdtlpdtrp0(xN,sK41)),
inference(cnf_transformation,[],[f303]) ).
fof(f533,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK40)),sdtlpdtrp0(xN,sK41)),
inference(cnf_transformation,[],[f303]) ).
fof(f535,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK40)),sdtlpdtrp0(xN,sK40)),
inference(cnf_transformation,[],[f303]) ).
fof(f548,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(slbdtrb0(X0)) ),
inference(equality_resolution,[],[f390]) ).
fof(f559,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,[],[f422]) ).
fof(f560,plain,
! [X0,X4] :
( ~ aElement0(sdtlpdtrp0(X0,X4))
| ~ aFunction0(X0)
| ~ aElementOf0(X4,szDzozmdt0(X0))
| aElementOf0(X4,sdtlbdtrb0(X0,sdtlpdtrp0(X0,X4))) ),
inference(equality_resolution,[],[f559]) ).
fof(f562,plain,
! [X0,X1,X4] :
( ~ aElement0(X1)
| ~ aFunction0(X0)
| ~ aElementOf0(X4,sdtlbdtrb0(X0,X1))
| sdtlpdtrp0(X0,X4) = X1 ),
inference(equality_resolution,[],[f420]) ).
tcf(c_97,plain,
! [X0: $i] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f364]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(szszuzczcdt0(X0),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f366]) ).
tcf(c_114,plain,
! [X0: $i] :
( aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(sbrdtbr0(X0),sbrdtbr0(X1))
| ~ isFinite0(X1)
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_135,plain,
! [X0: $i] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f548]) ).
tcf(c_139,plain,
! [X0: $i] :
( isFinite0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f394]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(slbdtrb0(X0),slbdtrb0(X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f399]) ).
tcf(c_148,plain,
! [X0: $i] :
( ( sbrdtbr0(slbdtrb0(X0)) = X0 )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f403]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( aElement0(sdtlpdtrp0(X1,X0))
| ~ aFunction0(X1)
| ~ aElementOf0(X0,szDzozmdt0(X1)) ),
inference(cnf_transformation,[],[f419]) ).
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,[],[f560]) ).
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,[],[f562]) ).
tcf(c_252,plain,
! [X0: $i] :
( sP8(X0)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f508]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ sP9(X1)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1))) ),
inference(cnf_transformation,[],[f506]) ).
tcf(c_261,plain,
aFunction0(xN),
inference(cnf_transformation,[],[f521]) ).
tcf(c_262,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[],[f520]) ).
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,[],[f517]) ).
tcf(c_266,plain,
! [X0: $i] :
( sP9(X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f516]) ).
tcf(c_269,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f523]) ).
tcf(c_270,plain,
! [X0: $i] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f522]) ).
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,[],[f527]) ).
tcf(c_273,negated_conjecture,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK40)),sdtlpdtrp0(xN,sK40)),
inference(cnf_transformation,[],[f535]) ).
tcf(c_275,negated_conjecture,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK40)),sdtlpdtrp0(xN,sK41)),
inference(cnf_transformation,[],[f533]) ).
tcf(c_277,negated_conjecture,
szmzizndt0(sdtlpdtrp0(xN,sK40)) = szmzizndt0(sdtlpdtrp0(xN,sK41)),
inference(cnf_transformation,[],[f531]) ).
tcf(c_278,negated_conjecture,
aElementOf0(sK40,szNzAzT0),
inference(cnf_transformation,[],[f530]) ).
tcf(c_279,negated_conjecture,
aElementOf0(sK41,szNzAzT0),
inference(cnf_transformation,[],[f529]) ).
tcf(c_280,negated_conjecture,
sK40 != sK41,
inference(cnf_transformation,[],[f528]) ).
tcf(c_468,plain,
! [X0: $i] :
( sP9(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_265,c_270,c_269,c_266]) ).
tcf(c_874,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_3709,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_254,c_468]) ).
tcf(c_3710,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1))) ),
inference(unflattening,[status(thm)],[c_3709]) ).
tcf(c_25310,definition,
iPr_def_10 = sdtlpdtrp0(xN,sK40),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_25311,definition,
iPr_def_11 = szmzizndt0(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_25312,definition,
iPr_def_12 = sdtlpdtrp0(xN,sK41),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_25313,definition,
iPr_def_13 = szmzizndt0(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_25314,negated_conjecture,
sK40 != sK41,
inference(demodulation,[status(thm)],[c_280]) ).
tcf(c_25315,negated_conjecture,
aElementOf0(sK41,szNzAzT0),
inference(demodulation,[status(thm)],[c_279]) ).
tcf(c_25316,negated_conjecture,
aElementOf0(sK40,szNzAzT0),
inference(demodulation,[status(thm)],[c_278]) ).
tcf(c_25317,negated_conjecture,
iPr_def_11 = iPr_def_13,
inference(demodulation,[status(thm)],[c_277,c_25312,c_25313,c_25310,c_25311]) ).
tcf(c_25319,negated_conjecture,
aElementOf0(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_275]) ).
tcf(c_25321,negated_conjecture,
aElementOf0(iPr_def_11,iPr_def_10),
inference(demodulation,[status(thm)],[c_273]) ).
tcf(c_28709,plain,
szmzizndt0(iPr_def_12) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_25313,c_25317]) ).
tcf(c_29277,plain,
! [X0: $i] :
( ( sbrdtbr0(slbdtrb0(szszuzczcdt0(X0))) = szszuzczcdt0(X0) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_97,c_148]) ).
tcf(c_29281,plain,
sbrdtbr0(slbdtrb0(sK40)) = sK40,
inference(superposition,[status(thm)],[c_25316,c_148]) ).
tcf(c_29282,plain,
sbrdtbr0(slbdtrb0(sK41)) = sK41,
inference(superposition,[status(thm)],[c_25315,c_148]) ).
tcf(c_30121,plain,
! [X0: $i] :
( aElement0(sdtlpdtrp0(xN,X0))
| ~ aFunction0(xN)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_262,c_164]) ).
tcf(c_30122,plain,
! [X0: $i] :
( aElement0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30121,c_261]) ).
tcf(c_30165,plain,
( aElementOf0(szszuzczcdt0(sK40),szNzAzT0)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_30166,plain,
( aElementOf0(szszuzczcdt0(sK41),szNzAzT0)
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_30214,plain,
( aElement0(iPr_def_10)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(superposition,[status(thm)],[c_25310,c_30122]) ).
tcf(c_30215,plain,
( aElement0(iPr_def_12)
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(superposition,[status(thm)],[c_25312,c_30122]) ).
tcf(c_30216,plain,
aElement0(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_30215,c_25315]) ).
tcf(c_30217,plain,
aElement0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_30214,c_25316]) ).
tcf(c_30586,plain,
sbrdtbr0(slbdtrb0(szszuzczcdt0(sK40))) = szszuzczcdt0(sK40),
inference(superposition,[status(thm)],[c_25316,c_29277]) ).
tcf(c_30587,plain,
sbrdtbr0(slbdtrb0(szszuzczcdt0(sK41))) = szszuzczcdt0(sK41),
inference(superposition,[status(thm)],[c_25315,c_29277]) ).
tcf(c_30771,plain,
( aElementOf0(szszuzczcdt0(sK40),szNzAzT0)
| ~ isFinite0(slbdtrb0(szszuzczcdt0(sK40)))
| ~ aSet0(slbdtrb0(szszuzczcdt0(sK40))) ),
inference(superposition,[status(thm)],[c_30586,c_114]) ).
tcf(c_30803,plain,
( aElementOf0(szszuzczcdt0(sK41),szNzAzT0)
| ~ isFinite0(slbdtrb0(szszuzczcdt0(sK41)))
| ~ aSet0(slbdtrb0(szszuzczcdt0(sK41))) ),
inference(superposition,[status(thm)],[c_30587,c_114]) ).
tcf(c_30989,plain,
aElementOf0(szszuzczcdt0(sK40),szNzAzT0),
inference(global_subsumption_just,[status(thm)],[c_30771,c_278,c_30165]) ).
tcf(c_31026,plain,
aElementOf0(szszuzczcdt0(sK41),szNzAzT0),
inference(global_subsumption_just,[status(thm)],[c_30803,c_279,c_30166]) ).
tcf(c_32477,plain,
! [X0: $i] :
( sdtlseqdt0(X0,sK40)
| sdtlseqdt0(szszuzczcdt0(sK40),X0)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_32479,plain,
! [X0: $i] :
( sdtlseqdt0(X0,sK41)
| sdtlseqdt0(szszuzczcdt0(sK41),X0)
| ~ aElementOf0(sK41,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_32566,plain,
! [X0: $i] :
( sdtlseqdt0(sK41,sbrdtbr0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(slbdtrb0(sK41),X0) ),
inference(superposition,[status(thm)],[c_29282,c_120]) ).
tcf(c_33259,plain,
( aElementOf0(sK40,sdtlbdtrb0(xN,iPr_def_10))
| ~ aFunction0(xN)
| ~ aElementOf0(sK40,szDzozmdt0(xN)) ),
inference(superposition,[status(thm)],[c_25310,c_874]) ).
tcf(c_33260,plain,
( aElementOf0(sK41,sdtlbdtrb0(xN,iPr_def_12))
| ~ aFunction0(xN)
| ~ aElementOf0(sK41,szDzozmdt0(xN)) ),
inference(superposition,[status(thm)],[c_25312,c_874]) ).
tcf(c_33264,plain,
( aElementOf0(sK41,sdtlbdtrb0(xN,iPr_def_12))
| ~ aFunction0(xN)
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(light_normalisation,[status(thm)],[c_33260,c_262]) ).
tcf(c_33265,plain,
aElementOf0(sK41,sdtlbdtrb0(xN,iPr_def_12)),
inference(forward_subsumption_resolution,[status(thm)],[c_33264,c_261,c_25315]) ).
tcf(c_33266,plain,
( aElementOf0(sK40,sdtlbdtrb0(xN,iPr_def_10))
| ~ aFunction0(xN)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(light_normalisation,[status(thm)],[c_33259,c_262]) ).
tcf(c_33267,plain,
aElementOf0(sK40,sdtlbdtrb0(xN,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_33266,c_261,c_25316]) ).
tcf(c_36377,plain,
( ( sdtlpdtrp0(xN,sK40) = iPr_def_10 )
| ~ aFunction0(xN)
| ~ aElement0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_33267,c_171]) ).
tcf(c_36378,plain,
( ( sdtlpdtrp0(xN,sK41) = iPr_def_12 )
| ~ aFunction0(xN)
| ~ aElement0(iPr_def_12) ),
inference(superposition,[status(thm)],[c_33265,c_171]) ).
tcf(c_36379,plain,
sdtlpdtrp0(xN,sK41) = iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_36378,c_261,c_30216]) ).
tcf(c_36380,plain,
sdtlpdtrp0(xN,sK40) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_36377,c_261,c_30217]) ).
tcf(c_36700,plain,
! [X0: $i] :
( sdtlseqdt0(sK41,sbrdtbr0(slbdtrb0(X0)))
| ~ aElementOf0(sK41,szNzAzT0)
| ~ sdtlseqdt0(sK41,X0)
| ~ isFinite0(slbdtrb0(X0))
| ~ aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_145,c_32566]) ).
tcf(c_36703,plain,
! [X0: $i] :
( sdtlseqdt0(sK41,sbrdtbr0(slbdtrb0(X0)))
| ~ sdtlseqdt0(sK41,X0)
| ~ isFinite0(slbdtrb0(X0))
| ~ aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36700,c_25315]) ).
tcf(c_36715,plain,
! [X0: $i] :
( sdtlseqdt0(sK41,sbrdtbr0(slbdtrb0(X0)))
| ~ sdtlseqdt0(sK41,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_36703,c_139,c_135,c_36703]) ).
tcf(c_39902,plain,
! [X0: $i] :
( ( sbrdtbr0(slbdtrb0(X0)) = sK41 )
| ~ aElementOf0(sK41,szNzAzT0)
| ~ sdtlseqdt0(sK41,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(sbrdtbr0(slbdtrb0(X0)),sK41)
| ~ aElementOf0(sbrdtbr0(slbdtrb0(X0)),szNzAzT0) ),
inference(superposition,[status(thm)],[c_36715,c_109]) ).
tcf(c_40037,plain,
! [X0: $i] :
( ( sbrdtbr0(slbdtrb0(X0)) = sK41 )
| ~ sdtlseqdt0(sK41,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(sbrdtbr0(slbdtrb0(X0)),sK41)
| ~ aElementOf0(sbrdtbr0(slbdtrb0(X0)),szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_39902,c_25315]) ).
tcf(c_41612,plain,
( ( sbrdtbr0(slbdtrb0(sK40)) = sK41 )
| ~ sdtlseqdt0(sK41,sK40)
| ~ sdtlseqdt0(sK40,sK41)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ aElementOf0(sbrdtbr0(slbdtrb0(sK40)),szNzAzT0) ),
inference(superposition,[status(thm)],[c_29281,c_40037]) ).
tcf(c_41635,plain,
( ( sK40 = sK41 )
| ~ sdtlseqdt0(sK41,sK40)
| ~ sdtlseqdt0(sK40,sK41)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(light_normalisation,[status(thm)],[c_41612,c_29281]) ).
tcf(c_41636,plain,
( ~ sdtlseqdt0(sK41,sK40)
| ~ sdtlseqdt0(sK40,sK41) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41635,c_25314,c_25316]) ).
tcf(c_41734,plain,
( sdtlseqdt0(sK41,sK40)
| sdtlseqdt0(szszuzczcdt0(sK40),sK41)
| ~ aElementOf0(sK41,szNzAzT0)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_32477]) ).
tcf(c_41740,plain,
( sdtlseqdt0(sK40,sK41)
| sdtlseqdt0(szszuzczcdt0(sK41),sK40)
| ~ aElementOf0(sK41,szNzAzT0)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_32479]) ).
tcf(c_48950,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ aElementOf0(sK40,szNzAzT0)
| ~ sdtlseqdt0(X1,sK40)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_36380,c_271]) ).
tcf(c_48952,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ aElementOf0(sK41,szNzAzT0)
| ~ sdtlseqdt0(X1,sK41)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_36379,c_271]) ).
tcf(c_48958,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,sK41)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_48952,c_25315]) ).
tcf(c_48963,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,sK40)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_48950,c_25316]) ).
fof(f219,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(f220,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(f221,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,[],[f202,f220,f219]) ).
fof(f299,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,[],[f219]) ).
fof(f300,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,[],[f299]) ).
fof(f301,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,[],[f300]) ).
fof(f512,plain,
! [X0,X1] :
( ~ sP8(X0)
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| szmzizndt0(sdtlpdtrp0(xN,X0)) != X1 ),
inference(cnf_transformation,[],[f301]) ).
fof(f578,plain,
! [X0] :
( ~ sP8(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(equality_resolution,[],[f512]) ).
tcf(c_260,plain,
! [X0: $i] :
( ~ sP8(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f578]) ).
tcf(c_3549,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_3550,plain,
! [X0: $i] :
( ~ sP9(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(unflattening,[status(thm)],[c_3549]) ).
tcf(c_3613,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_468,c_3550]) ).
tcf(c_3614,plain,
! [X0: $i] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(unflattening,[status(thm)],[c_3613]) ).
tcf(c_29042,plain,
! [X0: $i] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0))) ),
inference(superposition,[status(thm)],[c_3710,c_3614]) ).
tcf(c_30246,plain,
( ~ aElementOf0(sK40,szNzAzT0)
| ~ aElementOf0(szmzizndt0(iPr_def_10),sdtlpdtrp0(xN,szszuzczcdt0(sK40))) ),
inference(superposition,[status(thm)],[c_25310,c_29042]) ).
tcf(c_30247,plain,
( ~ aElementOf0(sK41,szNzAzT0)
| ~ aElementOf0(szmzizndt0(iPr_def_12),sdtlpdtrp0(xN,szszuzczcdt0(sK41))) ),
inference(superposition,[status(thm)],[c_25312,c_29042]) ).
tcf(c_30249,plain,
( ~ aElementOf0(sK41,szNzAzT0)
| ~ aElementOf0(iPr_def_11,sdtlpdtrp0(xN,szszuzczcdt0(sK41))) ),
inference(light_normalisation,[status(thm)],[c_30247,c_28709]) ).
tcf(c_30250,plain,
~ aElementOf0(iPr_def_11,sdtlpdtrp0(xN,szszuzczcdt0(sK41))),
inference(forward_subsumption_resolution,[status(thm)],[c_30249,c_25315]) ).
tcf(c_30251,plain,
( ~ aElementOf0(sK40,szNzAzT0)
| ~ aElementOf0(iPr_def_11,sdtlpdtrp0(xN,szszuzczcdt0(sK40))) ),
inference(light_normalisation,[status(thm)],[c_30246,c_25311]) ).
tcf(c_30252,plain,
~ aElementOf0(iPr_def_11,sdtlpdtrp0(xN,szszuzczcdt0(sK40))),
inference(forward_subsumption_resolution,[status(thm)],[c_30251,c_25316]) ).
tcf(c_49355,plain,
( ~ aElementOf0(iPr_def_11,iPr_def_12)
| ~ sdtlseqdt0(szszuzczcdt0(sK40),sK41)
| ~ aElementOf0(szszuzczcdt0(sK40),szNzAzT0) ),
inference(superposition,[status(thm)],[c_48958,c_30252]) ).
tcf(c_49356,plain,
~ sdtlseqdt0(szszuzczcdt0(sK40),sK41),
inference(forward_subsumption_resolution,[status(thm)],[c_49355,c_25319,c_30989]) ).
tcf(c_49753,plain,
( ~ aElementOf0(iPr_def_11,iPr_def_10)
| ~ sdtlseqdt0(szszuzczcdt0(sK41),sK40)
| ~ aElementOf0(szszuzczcdt0(sK41),szNzAzT0) ),
inference(superposition,[status(thm)],[c_48963,c_30250]) ).
tcf(c_49756,plain,
~ sdtlseqdt0(szszuzczcdt0(sK41),sK40),
inference(forward_subsumption_resolution,[status(thm)],[c_49753,c_25321,c_31026]) ).
tcf(c_49826,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_49756,c_49356,c_41740,c_41734,c_41636,c_278,c_279]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM575+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 04:42:43 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.45 % Proving...
% 13.47/3.35 % SZS status Started for theBenchmark.p
% 13.47/3.35 % SZS status Theorem for theBenchmark.p
% 13.47/3.35
% 13.47/3.35 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 13.47/3.35
% 13.47/3.35 % ------ iProver source info
% 13.47/3.35
% 13.47/3.35 % git: date: 2026-07-19 20:42:38 +0200
% 13.47/3.35 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 13.47/3.35 % git: non_committed_changes: false
% 13.47/3.35
% 13.47/3.35 % ------ Parsing...
% 13.47/3.35 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 13.47/3.35
% 13.47/3.35 % ------ 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 %
% 13.47/3.35
% 13.47/3.35 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 13.47/3.35
% 13.47/3.35 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 13.47/3.35 % ------ Proving...
% 13.47/3.35 % ------ Problem Properties
% 13.47/3.35
% 13.47/3.35 %
% 13.47/3.35 % clauses 228
% 13.47/3.35 % conjectures 8
% 13.47/3.35 % EPR 51
% 13.47/3.35 % Horn 178
% 13.47/3.35 % unary 35
% 13.47/3.35 % binary 48
% 13.47/3.35 % lits 754
% 13.47/3.35 % lits eq 109
% 13.47/3.35 % fd_pure 0
% 13.47/3.35 % fd_pseudo 0
% 13.47/3.35 % fd_cond 10
% 13.47/3.35 % fd_pseudo_cond 30
% 13.47/3.35 % AC symbols 0
% 13.47/3.35
% 13.47/3.35 % ------ Schedule dynamic 5 is on
% 13.47/3.35
% 13.47/3.35 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 13.47/3.35
% 13.47/3.35
% 13.47/3.35 % ------
% 13.47/3.35 % Current options:
% 13.47/3.35 % ------
% 13.47/3.35
% 13.47/3.35
% 13.47/3.35 %
% 13.47/3.35
% 13.47/3.35 % ------ Proving...
% 13.47/3.35 %
% 13.47/3.35
% 13.47/3.35 % SZS status Theorem for theBenchmark.p
% 13.47/3.35
% 13.47/3.35 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 13.47/3.36
% 13.47/3.36
%------------------------------------------------------------------------------