%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM589+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 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 : Tue Sep 29 12:15:53 PM UTC 2026
% Result : Theorem 34.71s 5.93s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 25
% Syntax : Number of formulae : 169 ( 25 unt; 15 def)
% Number of atoms : 1326 ( 163 equ)
% Maximal formula atoms : 47 ( 7 avg)
% Number of connectives : 1678 ( 521 ~; 479 |; 549 &)
% ( 35 <=>; 94 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 8 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 2 prp; 0-4 aty)
% Number of functors : 32 ( 32 usr; 11 con; 0-5 aty)
% Number of variables : 444 ( 0 sgn 367 !; 77 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(f20,axiom,
! [X0] :
( aElement0(X0)
=> ! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> isCountable0(sdtmndt0(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCDiffSet) ).
fof(f39,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> iLess0(X0,szszuzczcdt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIH) ).
fof(f77,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,szNzAzT0) ) )
| aSubsetOf0(X1,szNzAzT0) )
& isCountable0(X1) )
=> ! [X2] :
( ( aFunction0(X2)
& ( ! [X3] :
( ( aElementOf0(X3,szDzozmdt0(X2))
=> ( ( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,X1) ) )
| aSubsetOf0(X3,X1) )
& sbrdtbr0(X3) = X0 ) )
& ( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,X1) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = X0 )
=> aElementOf0(X3,szDzozmdt0(X2)) ) )
| szDzozmdt0(X2) = slbdtsldtrb0(X1,X0) )
& ( ( aSet0(sdtlcdtrc0(X2,szDzozmdt0(X2)))
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(X2,szDzozmdt0(X2)))
<=> ? [X4] :
( aElementOf0(X4,szDzozmdt0(X2))
& sdtlpdtrp0(X2,X4) = X3 ) ) )
=> ( ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(X2,szDzozmdt0(X2)))
=> aElementOf0(X3,xT) )
| aSubsetOf0(sdtlcdtrc0(X2,szDzozmdt0(X2)),xT) ) ) )
=> ( iLess0(X0,xK)
=> ? [X3] :
( aElementOf0(X3,xT)
& ? [X4] :
( aSet0(X4)
& ! [X5] :
( aElementOf0(X5,X4)
=> aElementOf0(X5,X1) )
& aSubsetOf0(X4,X1)
& isCountable0(X4)
& ! [X5] :
( ( ( ( ( aSet0(X5)
& ! [X6] :
( aElementOf0(X6,X5)
=> aElementOf0(X6,X4) ) )
| aSubsetOf0(X5,X4) )
& sbrdtbr0(X5) = X0 )
| aElementOf0(X5,slbdtsldtrb0(X4,X0)) )
=> sdtlpdtrp0(X2,X5) = X3 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3398) ).
fof(f80,axiom,
( aElementOf0(xk,szNzAzT0)
& szszuzczcdt0(xk) = xK ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3533) ).
fof(f81,axiom,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( ( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,X0)) )
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& X1 != szmzizndt0(sdtlpdtrp0(xN,X0)) ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3623) ).
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3671) ).
fof(f86,axiom,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aFunction0(sdtlpdtrp0(xC,X0))
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& X1 != szmzizndt0(sdtlpdtrp0(xN,X0)) ) )
& ! [X1] :
( ( aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))
=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sbrdtbr0(X1) = xk ) )
& ( ( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& sbrdtbr0(X1) = xk )
=> aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0))) ) )
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( ( aSet0(X1)
& ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) ) )
=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X2)
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& X2 != szmzizndt0(sdtlpdtrp0(xN,X0)) ) ) )
=> ( ( ( ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& sbrdtbr0(X1) = xk )
| aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) ) ) )
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& ! [X2] :
( aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X2)
& ( aElementOf0(X2,X1)
| X2 = szmzizndt0(sdtlpdtrp0(xN,X0)) ) ) )
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4151) ).
fof(f87,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
<=> ? [X2] :
( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) = X1 ) )
& ! [X1] :
( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
=> aElementOf0(X1,xT) )
& aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4182) ).
fof(f89,conjecture,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ? [X1] :
( aElementOf0(X1,xT)
& ? [X2] :
( ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) ) )
=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& X3 != szmzizndt0(sdtlpdtrp0(xN,X0)) ) ) )
=> ( ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) )
& isCountable0(X2)
& ! [X3] :
( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,X2) )
& aSubsetOf0(X3,X2)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X2,xk)) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,X0),X3) = X1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f90,negated_conjecture,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ? [X1] :
( aElementOf0(X1,xT)
& ? [X2] :
( ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) ) )
=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& X3 != szmzizndt0(sdtlpdtrp0(xN,X0)) ) ) )
=> ( ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) )
& isCountable0(X2)
& ! [X3] :
( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,X2) )
& aSubsetOf0(X3,X2)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X2,xk)) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,X0),X3) = X1 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f89]) ).
fof(f99,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,szNzAzT0) ) )
| aSubsetOf0(X1,szNzAzT0) )
& isCountable0(X1) )
=> ! [X3] :
( ( aFunction0(X3)
& ( ! [X4] :
( ( aElementOf0(X4,szDzozmdt0(X3))
=> ( ( ( aSet0(X4)
& ! [X5] :
( aElementOf0(X5,X4)
=> aElementOf0(X5,X1) ) )
| aSubsetOf0(X4,X1) )
& sbrdtbr0(X4) = X0 ) )
& ( ( aSet0(X4)
& ! [X6] :
( aElementOf0(X6,X4)
=> aElementOf0(X6,X1) )
& aSubsetOf0(X4,X1)
& sbrdtbr0(X4) = X0 )
=> aElementOf0(X4,szDzozmdt0(X3)) ) )
| slbdtsldtrb0(X1,X0) = szDzozmdt0(X3) )
& ( ( aSet0(sdtlcdtrc0(X3,szDzozmdt0(X3)))
& ! [X7] :
( aElementOf0(X7,sdtlcdtrc0(X3,szDzozmdt0(X3)))
<=> ? [X8] :
( aElementOf0(X8,szDzozmdt0(X3))
& sdtlpdtrp0(X3,X8) = X7 ) ) )
=> ( ! [X9] :
( aElementOf0(X9,sdtlcdtrc0(X3,szDzozmdt0(X3)))
=> aElementOf0(X9,xT) )
| aSubsetOf0(sdtlcdtrc0(X3,szDzozmdt0(X3)),xT) ) ) )
=> ( iLess0(X0,xK)
=> ? [X10] :
( aElementOf0(X10,xT)
& ? [X11] :
( aSet0(X11)
& ! [X12] :
( aElementOf0(X12,X11)
=> aElementOf0(X12,X1) )
& aSubsetOf0(X11,X1)
& isCountable0(X11)
& ! [X13] :
( ( ( ( ( aSet0(X13)
& ! [X14] :
( aElementOf0(X14,X13)
=> aElementOf0(X14,X11) ) )
| aSubsetOf0(X13,X11) )
& sbrdtbr0(X13) = X0 )
| aElementOf0(X13,slbdtsldtrb0(X11,X0)) )
=> sdtlpdtrp0(X3,X13) = X10 ) ) ) ) ) ) ),
inference(rectify,[],[f77]) ).
fof(f100,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( ( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,X0)) )
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) ) ) ) ),
inference(rectify,[],[f81]) ).
fof(f103,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aFunction0(sdtlpdtrp0(xC,X0))
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X2)
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X2 ) )
& ! [X3] :
( ( aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0)))
=> ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sbrdtbr0(X3) = xk ) )
& ( ( ( ( aSet0(X3)
& ! [X5] :
( aElementOf0(X5,X3)
=> aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& sbrdtbr0(X3) = xk )
=> aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0))) ) )
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X6] :
( ( aSet0(X6)
& ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X7] :
( aElementOf0(X7,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X7) ) )
=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X8] :
( aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X8)
& aElementOf0(X8,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X8 ) ) )
=> ( ( ( ! [X9] :
( aElementOf0(X9,X6)
=> aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| aSubsetOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& xk = sbrdtbr0(X6) )
| aElementOf0(X6,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) ) ) )
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X10] :
( aElementOf0(X10,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X10) )
& ! [X11] :
( aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X11)
& ( aElementOf0(X11,X6)
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X11 ) ) )
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = sdtlpdtrp0(xc,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ) ),
inference(rectify,[],[f86]) ).
fof(f104,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
<=> ? [X2] :
( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) = X1 ) )
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
=> aElementOf0(X3,xT) )
& aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT) ) ),
inference(rectify,[],[f87]) ).
fof(f106,plain,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ? [X1] :
( aElementOf0(X1,xT)
& ? [X2] :
( ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3) ) )
=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X4)
& aElementOf0(X4,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X4 ) ) )
=> ( ( aSet0(X2)
& ! [X5] :
( aElementOf0(X5,X2)
=> aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) )
& isCountable0(X2)
& ! [X6] :
( ( aSet0(X6)
& ! [X7] :
( aElementOf0(X7,X6)
=> aElementOf0(X7,X2) )
& aSubsetOf0(X6,X2)
& xk = sbrdtbr0(X6)
& aElementOf0(X6,slbdtsldtrb0(X2,xk)) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = X1 ) ) ) ),
inference(rectify,[],[f90]) ).
fof(f107,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f130,plain,
! [X0] :
( ! [X1] :
( isCountable0(sdtmndt0(X1,X0))
| ~ aSet0(X1)
| ~ isCountable0(X1) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f131,plain,
! [X0] :
( ! [X1] :
( isCountable0(sdtmndt0(X1,X0))
| ~ aSet0(X1)
| ~ isCountable0(X1) )
| ~ aElement0(X0) ),
inference(flattening,[],[f130]) ).
fof(f154,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f209,plain,
! [X0] :
( ! [X1] :
( ! [X3] :
( ? [X10] :
( aElementOf0(X10,xT)
& ? [X11] :
( aSet0(X11)
& ! [X12] :
( aElementOf0(X12,X1)
| ~ aElementOf0(X12,X11) )
& aSubsetOf0(X11,X1)
& isCountable0(X11)
& ! [X13] :
( sdtlpdtrp0(X3,X13) = X10
| ( ( ( ( ~ aSet0(X13)
| ? [X14] :
( ~ aElementOf0(X14,X11)
& aElementOf0(X14,X13) ) )
& ~ aSubsetOf0(X13,X11) )
| sbrdtbr0(X13) != X0 )
& ~ aElementOf0(X13,slbdtsldtrb0(X11,X0)) ) ) ) )
| ~ iLess0(X0,xK)
| ~ aFunction0(X3)
| ( ? [X4] :
( ( ( ( ( ~ aSet0(X4)
| ? [X5] :
( ~ aElementOf0(X5,X1)
& aElementOf0(X5,X4) ) )
& ~ aSubsetOf0(X4,X1) )
| sbrdtbr0(X4) != X0 )
& aElementOf0(X4,szDzozmdt0(X3)) )
| ( ~ aElementOf0(X4,szDzozmdt0(X3))
& aSet0(X4)
& ! [X6] :
( aElementOf0(X6,X1)
| ~ aElementOf0(X6,X4) )
& aSubsetOf0(X4,X1)
& sbrdtbr0(X4) = X0 ) )
& slbdtsldtrb0(X1,X0) != szDzozmdt0(X3) )
| ( ? [X9] :
( ~ aElementOf0(X9,xT)
& aElementOf0(X9,sdtlcdtrc0(X3,szDzozmdt0(X3))) )
& ~ aSubsetOf0(sdtlcdtrc0(X3,szDzozmdt0(X3)),xT)
& aSet0(sdtlcdtrc0(X3,szDzozmdt0(X3)))
& ! [X7] :
( aElementOf0(X7,sdtlcdtrc0(X3,szDzozmdt0(X3)))
<=> ? [X8] :
( aElementOf0(X8,szDzozmdt0(X3))
& sdtlpdtrp0(X3,X8) = X7 ) ) ) )
| ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,szNzAzT0)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,szNzAzT0) )
| ~ isCountable0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f99]) ).
fof(f210,plain,
! [X0] :
( ! [X1] :
( ! [X3] :
( ? [X10] :
( aElementOf0(X10,xT)
& ? [X11] :
( aSet0(X11)
& ! [X12] :
( aElementOf0(X12,X1)
| ~ aElementOf0(X12,X11) )
& aSubsetOf0(X11,X1)
& isCountable0(X11)
& ! [X13] :
( sdtlpdtrp0(X3,X13) = X10
| ( ( ( ( ~ aSet0(X13)
| ? [X14] :
( ~ aElementOf0(X14,X11)
& aElementOf0(X14,X13) ) )
& ~ aSubsetOf0(X13,X11) )
| sbrdtbr0(X13) != X0 )
& ~ aElementOf0(X13,slbdtsldtrb0(X11,X0)) ) ) ) )
| ~ iLess0(X0,xK)
| ~ aFunction0(X3)
| ( ? [X4] :
( ( ( ( ( ~ aSet0(X4)
| ? [X5] :
( ~ aElementOf0(X5,X1)
& aElementOf0(X5,X4) ) )
& ~ aSubsetOf0(X4,X1) )
| sbrdtbr0(X4) != X0 )
& aElementOf0(X4,szDzozmdt0(X3)) )
| ( ~ aElementOf0(X4,szDzozmdt0(X3))
& aSet0(X4)
& ! [X6] :
( aElementOf0(X6,X1)
| ~ aElementOf0(X6,X4) )
& aSubsetOf0(X4,X1)
& sbrdtbr0(X4) = X0 ) )
& slbdtsldtrb0(X1,X0) != szDzozmdt0(X3) )
| ( ? [X9] :
( ~ aElementOf0(X9,xT)
& aElementOf0(X9,sdtlcdtrc0(X3,szDzozmdt0(X3))) )
& ~ aSubsetOf0(sdtlcdtrc0(X3,szDzozmdt0(X3)),xT)
& aSet0(sdtlcdtrc0(X3,szDzozmdt0(X3)))
& ! [X7] :
( aElementOf0(X7,sdtlcdtrc0(X3,szDzozmdt0(X3)))
<=> ? [X8] :
( aElementOf0(X8,szDzozmdt0(X3))
& sdtlpdtrp0(X3,X8) = X7 ) ) ) )
| ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,szNzAzT0)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,szNzAzT0) )
| ~ isCountable0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f209]) ).
fof(f211,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f100]) ).
fof(f212,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(flattening,[],[f211]) ).
fof(f213,plain,
! [X0] :
( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f220,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X2)
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X2 ) )
& ! [X3] :
( ( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sbrdtbr0(X3) = xk )
| ~ aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0))) )
& ( aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( ( ~ aSet0(X3)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X3) ) )
& ~ aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| sbrdtbr0(X3) != xk ) )
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X6] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X10] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X10)
| ~ aElementOf0(X10,sdtlpdtrp0(xN,X0)) )
& ! [X11] :
( aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X11)
& ( aElementOf0(X11,X6)
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X11 ) ) )
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = sdtlpdtrp0(xc,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| ~ aSet0(X6)
| ( ( ( ? [X9] :
( ~ aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X9,X6) )
& ~ aSubsetOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| xk != sbrdtbr0(X6) )
& ~ aElementOf0(X6,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X8] :
( aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X8)
& aElementOf0(X8,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X8 ) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X7] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X7)
| ~ aElementOf0(X7,sdtlpdtrp0(xN,X0)) ) ) ) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f103]) ).
fof(f221,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X2)
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X2 ) )
& ! [X3] :
( ( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sbrdtbr0(X3) = xk )
| ~ aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0))) )
& ( aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( ( ~ aSet0(X3)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X3) ) )
& ~ aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| sbrdtbr0(X3) != xk ) )
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X6] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X10] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X10)
| ~ aElementOf0(X10,sdtlpdtrp0(xN,X0)) )
& ! [X11] :
( aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X11)
& ( aElementOf0(X11,X6)
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X11 ) ) )
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = sdtlpdtrp0(xc,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| ~ aSet0(X6)
| ( ( ( ? [X9] :
( ~ aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X9,X6) )
& ~ aSubsetOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| xk != sbrdtbr0(X6) )
& ~ aElementOf0(X6,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X8] :
( aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X8)
& aElementOf0(X8,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X8 ) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X7] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X7)
| ~ aElementOf0(X7,sdtlpdtrp0(xN,X0)) ) ) ) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(flattening,[],[f220]) ).
fof(f222,plain,
! [X0] :
( ( aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
<=> ? [X2] :
( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) = X1 ) )
& ! [X3] :
( aElementOf0(X3,xT)
| ~ aElementOf0(X3,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) )
& aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f104]) ).
fof(f225,plain,
? [X0] :
( ! [X1] :
( ~ aElementOf0(X1,xT)
| ! [X2] :
( ( ( ~ aSet0(X2)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X2) ) )
& ~ aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X4)
& aElementOf0(X4,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X4 ) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0)) ) )
| ~ isCountable0(X2)
| ? [X6] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) != X1
& aSet0(X6)
& ! [X7] :
( aElementOf0(X7,X2)
| ~ aElementOf0(X7,X6) )
& aSubsetOf0(X6,X2)
& xk = sbrdtbr0(X6)
& aElementOf0(X6,slbdtsldtrb0(X2,xk)) ) ) )
& aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f106]) ).
fof(f226,plain,
? [X0] :
( ! [X1] :
( ~ aElementOf0(X1,xT)
| ! [X2] :
( ( ( ~ aSet0(X2)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X2) ) )
& ~ aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X4)
& aElementOf0(X4,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X4 ) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0)) ) )
| ~ isCountable0(X2)
| ? [X6] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) != X1
& aSet0(X6)
& ! [X7] :
( aElementOf0(X7,X2)
| ~ aElementOf0(X7,X6) )
& aSubsetOf0(X6,X2)
& xk = sbrdtbr0(X6)
& aElementOf0(X6,slbdtsldtrb0(X2,xk)) ) ) )
& aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f225]) ).
fof(f233,definition,
! [X3,X4,X1,X0] :
( ( ~ aElementOf0(X4,szDzozmdt0(X3))
& aSet0(X4)
& ! [X6] :
( aElementOf0(X6,X1)
| ~ aElementOf0(X6,X4) )
& aSubsetOf0(X4,X1)
& sbrdtbr0(X4) = X0 )
| ~ sP4(X3,X4,X1,X0) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f234,definition,
! [X1,X10,X3,X0] :
( ? [X11] :
( aSet0(X11)
& ! [X12] :
( aElementOf0(X12,X1)
| ~ aElementOf0(X12,X11) )
& aSubsetOf0(X11,X1)
& isCountable0(X11)
& ! [X13] :
( sdtlpdtrp0(X3,X13) = X10
| ( ( ( ( ~ aSet0(X13)
| ? [X14] :
( ~ aElementOf0(X14,X11)
& aElementOf0(X14,X13) ) )
& ~ aSubsetOf0(X13,X11) )
| sbrdtbr0(X13) != X0 )
& ~ aElementOf0(X13,slbdtsldtrb0(X11,X0)) ) ) )
| ~ sP5(X1,X10,X3,X0) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f235,definition,
! [X3] :
( ( ? [X9] :
( ~ aElementOf0(X9,xT)
& aElementOf0(X9,sdtlcdtrc0(X3,szDzozmdt0(X3))) )
& ~ aSubsetOf0(sdtlcdtrc0(X3,szDzozmdt0(X3)),xT)
& aSet0(sdtlcdtrc0(X3,szDzozmdt0(X3)))
& ! [X7] :
( aElementOf0(X7,sdtlcdtrc0(X3,szDzozmdt0(X3)))
<=> ? [X8] :
( aElementOf0(X8,szDzozmdt0(X3))
& sdtlpdtrp0(X3,X8) = X7 ) ) )
| ~ sP6(X3) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f236,definition,
! [X1,X0,X3] :
( ( ? [X4] :
( ( ( ( ( ~ aSet0(X4)
| ? [X5] :
( ~ aElementOf0(X5,X1)
& aElementOf0(X5,X4) ) )
& ~ aSubsetOf0(X4,X1) )
| sbrdtbr0(X4) != X0 )
& aElementOf0(X4,szDzozmdt0(X3)) )
| sP4(X3,X4,X1,X0) )
& slbdtsldtrb0(X1,X0) != szDzozmdt0(X3) )
| ~ sP7(X1,X0,X3) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f237,plain,
! [X0] :
( ! [X1] :
( ! [X3] :
( ? [X10] :
( aElementOf0(X10,xT)
& sP5(X1,X10,X3,X0) )
| ~ iLess0(X0,xK)
| ~ aFunction0(X3)
| sP7(X1,X0,X3)
| sP6(X3) )
| ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,szNzAzT0)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,szNzAzT0) )
| ~ isCountable0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(definition_folding,[],[f210,f236,f235,f234,f233]) ).
fof(f238,definition,
! [X0] :
( ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
| ~ sP8(X0) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f239,definition,
! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP8(X0)
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ sP9(X0) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f240,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( sP9(X0)
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(definition_folding,[],[f212,f239,f238]) ).
fof(f245,definition,
! [X0] :
( ! [X8] :
( aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X8)
& aElementOf0(X8,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X8 ) )
| ~ sP13(X0) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f246,definition,
! [X0,X6] :
( ( ( ( ? [X9] :
( ~ aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X9,X6) )
& ~ aSubsetOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| xk != sbrdtbr0(X6) )
& ~ aElementOf0(X6,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP13(X0)
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X7] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X7)
| ~ aElementOf0(X7,sdtlpdtrp0(xN,X0)) ) )
| ~ sP14(X0,X6) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f247,definition,
! [X0] :
( ! [X6] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X10] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X10)
| ~ aElementOf0(X10,sdtlpdtrp0(xN,X0)) )
& ! [X11] :
( aElementOf0(X11,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X11)
& ( aElementOf0(X11,X6)
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X11 ) ) )
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) = sdtlpdtrp0(xc,sdtpldt0(X6,szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| ~ aSet0(X6)
| sP14(X0,X6) )
| ~ sP15(X0) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f248,definition,
! [X0] :
( ! [X3] :
( ( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sbrdtbr0(X3) = xk )
| ~ aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0))) )
& ( aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| ( ( ~ aSet0(X3)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X3) ) )
& ~ aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
| sbrdtbr0(X3) != xk ) )
| ~ sP16(X0) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f249,definition,
! [X0] :
( ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X2)
& aElementOf0(X2,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X2 ) )
| ~ sP17(X0) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f250,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP17(X0)
& sP16(X0)
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& sP15(X0) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(definition_folding,[],[f221,f249,f248,f247,f246,f245]) ).
fof(f256,definition,
! [X0] :
( ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X4)
& aElementOf0(X4,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X4 ) )
| ~ sP22(X0) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f257,definition,
! [X2,X0] :
( ( ( ~ aSet0(X2)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X2) ) )
& ~ aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP22(X0)
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0)) ) )
| ~ sP23(X2,X0) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f258,plain,
? [X0] :
( ! [X1] :
( ~ aElementOf0(X1,xT)
| ! [X2] :
( sP23(X2,X0)
| ~ isCountable0(X2)
| ? [X6] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X6) != X1
& aSet0(X6)
& ! [X7] :
( aElementOf0(X7,X2)
| ~ aElementOf0(X7,X6) )
& aSubsetOf0(X6,X2)
& xk = sbrdtbr0(X6)
& aElementOf0(X6,slbdtsldtrb0(X2,xk)) ) ) )
& aElementOf0(X0,szNzAzT0) ),
inference(definition_folding,[],[f226,f257,f256]) ).
fof(f321,plain,
! [X1,X0,X3] :
( ( ? [X4] :
( ( ( ( ( ~ aSet0(X4)
| ? [X5] :
( ~ aElementOf0(X5,X1)
& aElementOf0(X5,X4) ) )
& ~ aSubsetOf0(X4,X1) )
| sbrdtbr0(X4) != X0 )
& aElementOf0(X4,szDzozmdt0(X3)) )
| sP4(X3,X4,X1,X0) )
& slbdtsldtrb0(X1,X0) != szDzozmdt0(X3) )
| ~ sP7(X1,X0,X3) ),
inference(nnf_transformation,[],[f236]) ).
fof(f322,plain,
! [X0,X1,X2] :
( ( ? [X3] :
( ( ( ( ( ~ aSet0(X3)
| ? [X4] :
( ~ aElementOf0(X4,X0)
& aElementOf0(X4,X3) ) )
& ~ aSubsetOf0(X3,X0) )
| sbrdtbr0(X3) != X1 )
& aElementOf0(X3,szDzozmdt0(X2)) )
| sP4(X2,X3,X0,X1) )
& slbdtsldtrb0(X0,X1) != szDzozmdt0(X2) )
| ~ sP7(X0,X1,X2) ),
inference(rectify,[],[f321]) ).
fof(f323,plain,
! [X0,X1,X2] :
( ( ( ( ( ( ( ~ aSet0(sK45(X0,X1,X2))
| ( ~ aElementOf0(sK46(X0,X1,X2),X0)
& aElementOf0(sK46(X0,X1,X2),sK45(X0,X1,X2)) ) )
& ~ aSubsetOf0(sK45(X0,X1,X2),X0) )
| sbrdtbr0(sK45(X0,X1,X2)) != X1 )
& aElementOf0(sK45(X0,X1,X2),szDzozmdt0(X2)) )
| sP4(X2,sK45(X0,X1,X2),X0,X1) )
& slbdtsldtrb0(X0,X1) != szDzozmdt0(X2) )
| ~ sP7(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45,sK46]),skolemize(X3,sK45(X0,X1,X2)),skolemize(X4,sK46(X0,X1,X2))],[f322]) ).
fof(f324,plain,
! [X3] :
( ( ? [X9] :
( ~ aElementOf0(X9,xT)
& aElementOf0(X9,sdtlcdtrc0(X3,szDzozmdt0(X3))) )
& ~ aSubsetOf0(sdtlcdtrc0(X3,szDzozmdt0(X3)),xT)
& aSet0(sdtlcdtrc0(X3,szDzozmdt0(X3)))
& ! [X7] :
( ( aElementOf0(X7,sdtlcdtrc0(X3,szDzozmdt0(X3)))
| ! [X8] :
( ~ aElementOf0(X8,szDzozmdt0(X3))
| sdtlpdtrp0(X3,X8) != X7 ) )
& ( ? [X8] :
( aElementOf0(X8,szDzozmdt0(X3))
& sdtlpdtrp0(X3,X8) = X7 )
| ~ aElementOf0(X7,sdtlcdtrc0(X3,szDzozmdt0(X3))) ) ) )
| ~ sP6(X3) ),
inference(nnf_transformation,[],[f235]) ).
fof(f325,plain,
! [X0] :
( ( ? [X1] :
( ~ aElementOf0(X1,xT)
& aElementOf0(X1,sdtlcdtrc0(X0,szDzozmdt0(X0))) )
& ~ aSubsetOf0(sdtlcdtrc0(X0,szDzozmdt0(X0)),xT)
& aSet0(sdtlcdtrc0(X0,szDzozmdt0(X0)))
& ! [X2] :
( ( aElementOf0(X2,sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ! [X3] :
( ~ aElementOf0(X3,szDzozmdt0(X0))
| sdtlpdtrp0(X0,X3) != X2 ) )
& ( ? [X4] :
( aElementOf0(X4,szDzozmdt0(X0))
& sdtlpdtrp0(X0,X4) = X2 )
| ~ aElementOf0(X2,sdtlcdtrc0(X0,szDzozmdt0(X0))) ) ) )
| ~ sP6(X0) ),
inference(rectify,[],[f324]) ).
fof(f326,plain,
! [X0] :
( ( ~ aElementOf0(sK47(X0),xT)
& aElementOf0(sK47(X0),sdtlcdtrc0(X0,szDzozmdt0(X0)))
& ~ aSubsetOf0(sdtlcdtrc0(X0,szDzozmdt0(X0)),xT)
& aSet0(sdtlcdtrc0(X0,szDzozmdt0(X0)))
& ! [X2] :
( ( aElementOf0(X2,sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ! [X3] :
( ~ aElementOf0(X3,szDzozmdt0(X0))
| sdtlpdtrp0(X0,X3) != X2 ) )
& ( ( aElementOf0(sK48(X0,X2),szDzozmdt0(X0))
& sdtlpdtrp0(X0,sK48(X0,X2)) = X2 )
| ~ aElementOf0(X2,sdtlcdtrc0(X0,szDzozmdt0(X0))) ) ) )
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47,sK48]),skolemize(X1,sK47(X0)),skolemize(X4,sK48(X0,X2))],[f325]) ).
fof(f327,plain,
! [X1,X10,X3,X0] :
( ? [X11] :
( aSet0(X11)
& ! [X12] :
( aElementOf0(X12,X1)
| ~ aElementOf0(X12,X11) )
& aSubsetOf0(X11,X1)
& isCountable0(X11)
& ! [X13] :
( sdtlpdtrp0(X3,X13) = X10
| ( ( ( ( ~ aSet0(X13)
| ? [X14] :
( ~ aElementOf0(X14,X11)
& aElementOf0(X14,X13) ) )
& ~ aSubsetOf0(X13,X11) )
| sbrdtbr0(X13) != X0 )
& ~ aElementOf0(X13,slbdtsldtrb0(X11,X0)) ) ) )
| ~ sP5(X1,X10,X3,X0) ),
inference(nnf_transformation,[],[f234]) ).
fof(f328,plain,
! [X0,X1,X2,X3] :
( ? [X4] :
( aSet0(X4)
& ! [X5] :
( aElementOf0(X5,X0)
| ~ aElementOf0(X5,X4) )
& aSubsetOf0(X4,X0)
& isCountable0(X4)
& ! [X6] :
( sdtlpdtrp0(X2,X6) = X1
| ( ( ( ( ~ aSet0(X6)
| ? [X7] :
( ~ aElementOf0(X7,X4)
& aElementOf0(X7,X6) ) )
& ~ aSubsetOf0(X6,X4) )
| sbrdtbr0(X6) != X3 )
& ~ aElementOf0(X6,slbdtsldtrb0(X4,X3)) ) ) )
| ~ sP5(X0,X1,X2,X3) ),
inference(rectify,[],[f327]) ).
fof(f329,plain,
! [X0,X1,X2,X3] :
( ( aSet0(sK49(X0,X1,X2,X3))
& ! [X5] :
( aElementOf0(X5,X0)
| ~ aElementOf0(X5,sK49(X0,X1,X2,X3)) )
& aSubsetOf0(sK49(X0,X1,X2,X3),X0)
& isCountable0(sK49(X0,X1,X2,X3))
& ! [X6] :
( sdtlpdtrp0(X2,X6) = X1
| ( ( ( ( ~ aSet0(X6)
| ( ~ aElementOf0(sK50(X0,X1,X2,X3,X6),sK49(X0,X1,X2,X3))
& aElementOf0(sK50(X0,X1,X2,X3,X6),X6) ) )
& ~ aSubsetOf0(X6,sK49(X0,X1,X2,X3)) )
| sbrdtbr0(X6) != X3 )
& ~ aElementOf0(X6,slbdtsldtrb0(sK49(X0,X1,X2,X3),X3)) ) ) )
| ~ sP5(X0,X1,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49,sK50]),skolemize(X4,sK49(X0,X1,X2,X3)),skolemize(X7,sK50(X0,X1,X2,X3,X6))],[f328]) ).
fof(f332,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ? [X3] :
( aElementOf0(X3,xT)
& sP5(X1,X3,X2,X0) )
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2) )
| ( ( ~ aSet0(X1)
| ? [X4] :
( ~ aElementOf0(X4,szNzAzT0)
& aElementOf0(X4,X1) ) )
& ~ aSubsetOf0(X1,szNzAzT0) )
| ~ isCountable0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(rectify,[],[f237]) ).
fof(f333,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( aElementOf0(sK51(X0,X1,X2),xT)
& sP5(X1,sK51(X0,X1,X2),X2,X0) )
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2) )
| ( ( ~ aSet0(X1)
| ( ~ aElementOf0(sK52(X1),szNzAzT0)
& aElementOf0(sK52(X1),X1) ) )
& ~ aSubsetOf0(X1,szNzAzT0) )
| ~ isCountable0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51,sK52]),skolemize(X3,sK51(X0,X1,X2)),skolemize(X4,sK52(X1))],[f332]) ).
fof(f334,plain,
! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP8(X0)
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ sP9(X0) ),
inference(nnf_transformation,[],[f239]) ).
fof(f335,plain,
! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP8(X0)
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ sP9(X0) ),
inference(rectify,[],[f334]) ).
fof(f336,plain,
! [X0] :
( ! [X3] :
( ( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElement0(X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 )
| ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| ~ sP8(X0) ),
inference(nnf_transformation,[],[f238]) ).
fof(f337,plain,
! [X0] :
( ! [X3] :
( ( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElement0(X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 )
| ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| ~ sP8(X0) ),
inference(flattening,[],[f336]) ).
fof(f338,plain,
! [X0] :
( ! [X1] :
( ( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElement0(X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X1 )
& ( ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X1 )
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| ~ sP8(X0) ),
inference(rectify,[],[f337]) ).
fof(f339,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( sP9(X0)
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ( ~ aElementOf0(sK53(X0),szNzAzT0)
& aElementOf0(sK53(X0),sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(X1,sK53(X0))],[f240]) ).
fof(f367,plain,
! [X0] :
( ( aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
& ! [X1] :
( ( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
| ! [X2] :
( ~ aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) != X1 ) )
& ( ? [X2] :
( aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) = X1 )
| ~ aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) ) )
& ! [X3] :
( aElementOf0(X3,xT)
| ~ aElementOf0(X3,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) )
& aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(nnf_transformation,[],[f222]) ).
fof(f368,plain,
! [X0] :
( ( aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
& ! [X1] :
( ( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
| ! [X2] :
( ~ aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) != X1 ) )
& ( ? [X3] :
( aElementOf0(X3,szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),X3) = X1 )
| ~ aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) ) )
& ! [X4] :
( aElementOf0(X4,xT)
| ~ aElementOf0(X4,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) )
& aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(rectify,[],[f367]) ).
fof(f369,plain,
! [X0] :
( ( aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
& ! [X1] :
( ( aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))))
| ! [X2] :
( ~ aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0)))
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) != X1 ) )
& ( ( aElementOf0(sK58(X0,X1),szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),sK58(X0,X1)) = X1 )
| ~ aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) ) )
& ! [X4] :
( aElementOf0(X4,xT)
| ~ aElementOf0(X4,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) )
& aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X3,sK58(X0,X1))],[f368]) ).
fof(f383,plain,
! [X2,X0] :
( ( ( ~ aSet0(X2)
| ? [X5] :
( ~ aElementOf0(X5,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aElementOf0(X5,X2) ) )
& ~ aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP22(X0)
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X3] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0)) ) )
| ~ sP23(X2,X0) ),
inference(nnf_transformation,[],[f257]) ).
fof(f384,plain,
! [X0,X1] :
( ( ( ~ aSet0(X0)
| ? [X2] :
( ~ aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& aElementOf0(X2,X0) ) )
& ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& sP22(X1)
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X1)) ) )
| ~ sP23(X0,X1) ),
inference(rectify,[],[f383]) ).
fof(f385,plain,
! [X0,X1] :
( ( ( ~ aSet0(X0)
| ( ~ aElementOf0(sK61(X0,X1),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& aElementOf0(sK61(X0,X1),X0) ) )
& ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& sP22(X1)
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X1)) ) )
| ~ sP23(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61]),skolemize(X2,sK61(X0,X1))],[f384]) ).
fof(f389,plain,
? [X0] :
( ! [X1] :
( ~ aElementOf0(X1,xT)
| ! [X2] :
( sP23(X2,X0)
| ~ isCountable0(X2)
| ? [X3] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X3) != X1
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X2)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X2)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X2,xk)) ) ) )
& aElementOf0(X0,szNzAzT0) ),
inference(rectify,[],[f258]) ).
fof(f390,plain,
( ! [X1] :
( ~ aElementOf0(X1,xT)
| ! [X2] :
( sP23(X2,sK62)
| ~ isCountable0(X2)
| ( sdtlpdtrp0(sdtlpdtrp0(xC,sK62),sK63(X1,X2)) != X1
& aSet0(sK63(X1,X2))
& ! [X4] :
( aElementOf0(X4,X2)
| ~ aElementOf0(X4,sK63(X1,X2)) )
& aSubsetOf0(sK63(X1,X2),X2)
& xk = sbrdtbr0(sK63(X1,X2))
& aElementOf0(sK63(X1,X2),slbdtsldtrb0(X2,xk)) ) ) )
& aElementOf0(sK62,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62,sK63]),skolemize(X0,sK62),skolemize(X3,sK63(X1,X2))],[f389]) ).
fof(f391,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f433,plain,
! [X0,X1] :
( isCountable0(sdtmndt0(X1,X0))
| ~ aSet0(X1)
| ~ isCountable0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f454,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f154]) ).
fof(f556,plain,
! [X2,X0,X1] :
( slbdtsldtrb0(X0,X1) != szDzozmdt0(X2)
| ~ sP7(X0,X1,X2) ),
inference(cnf_transformation,[],[f323]) ).
fof(f565,plain,
! [X0] :
( ~ aSubsetOf0(sdtlcdtrc0(X0,szDzozmdt0(X0)),xT)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f326]) ).
fof(f568,plain,
! [X2,X3,X0,X1,X6] :
( ~ aElementOf0(X6,slbdtsldtrb0(sK49(X0,X1,X2,X3),X3))
| sdtlpdtrp0(X2,X6) = X1
| ~ sP5(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f329]) ).
fof(f572,plain,
! [X2,X3,X0,X1] :
( isCountable0(sK49(X0,X1,X2,X3))
| ~ sP5(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f329]) ).
fof(f573,plain,
! [X2,X3,X0,X1] :
( aSubsetOf0(sK49(X0,X1,X2,X3),X0)
| ~ sP5(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f329]) ).
fof(f582,plain,
! [X2,X0,X1] :
( sP5(X1,sK51(X0,X1,X2),X2,X0)
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2)
| ~ aSet0(X1)
| aElementOf0(sK52(X1),X1)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f333]) ).
fof(f583,plain,
! [X2,X0,X1] :
( sP5(X1,sK51(X0,X1,X2),X2,X0)
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2)
| ~ aSet0(X1)
| ~ aElementOf0(sK52(X1),szNzAzT0)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f333]) ).
fof(f585,plain,
! [X2,X0,X1] :
( aElementOf0(sK51(X0,X1,X2),xT)
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2)
| ~ aSet0(X1)
| aElementOf0(sK52(X1),X1)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f333]) ).
fof(f586,plain,
! [X2,X0,X1] :
( aElementOf0(sK51(X0,X1,X2),xT)
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2)
| ~ aSet0(X1)
| ~ aElementOf0(sK52(X1),szNzAzT0)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f333]) ).
fof(f589,plain,
xK = szszuzczcdt0(xk),
inference(cnf_transformation,[],[f80]) ).
fof(f590,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f80]) ).
fof(f595,plain,
! [X0] :
( ~ sP9(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f335]) ).
fof(f600,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f338]) ).
fof(f603,plain,
! [X0] :
( sP9(X0)
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f339]) ).
fof(f609,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f213]) ).
fof(f610,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f213]) ).
fof(f611,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f213]) ).
fof(f612,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f213]) ).
fof(f675,plain,
! [X0] :
( slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk) = szDzozmdt0(sdtlpdtrp0(xC,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f678,plain,
! [X0] :
( aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f680,plain,
! [X0] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f681,plain,
! [X0] :
( aFunction0(sdtlpdtrp0(xC,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f684,plain,
! [X0] :
( aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f369]) ).
fof(f720,plain,
! [X0,X1] :
( ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ sP23(X0,X1) ),
inference(cnf_transformation,[],[f385]) ).
fof(f727,plain,
aElementOf0(sK62,szNzAzT0),
inference(cnf_transformation,[],[f390]) ).
fof(f728,plain,
! [X2,X1] :
( aElementOf0(sK63(X1,X2),slbdtsldtrb0(X2,xk))
| sP23(X2,sK62)
| ~ isCountable0(X2)
| ~ aElementOf0(X1,xT) ),
inference(cnf_transformation,[],[f390]) ).
fof(f733,plain,
! [X2,X1] :
( ~ aElementOf0(X1,xT)
| sP23(X2,sK62)
| ~ isCountable0(X2)
| sdtlpdtrp0(sdtlpdtrp0(xC,sK62),sK63(X1,X2)) != X1 ),
inference(cnf_transformation,[],[f390]) ).
fof(f786,definition,
sF64 = sdtlpdtrp0(xC,sK62),
introduced(definition,[new_symbols(definition,[sF64])],[function_definition]) ).
fof(f787,plain,
sdtlpdtrp0(xC,sK62) = sF64,
inference(reorient_equations,[],[f786]) ).
fof(f788,plain,
! [X2,X1] :
( sdtlpdtrp0(sF64,sK63(X1,X2)) != X1
| sP23(X2,sK62)
| ~ isCountable0(X2)
| ~ aElementOf0(X1,xT) ),
inference(definition_folding,[],[f733,f787]) ).
fof(f792,plain,
! [X0] :
( sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f603,f610]) ).
fof(f822,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sP9(X0) ),
inference(forward_subsumption_resolution,[],[f792,f609]) ).
fof(f825,plain,
( aFunction0(sF64)
| ~ aElementOf0(sK62,szNzAzT0) ),
inference(superposition,[],[f681,f787]) ).
fof(f826,plain,
aFunction0(sF64),
inference(forward_subsumption_resolution,[],[f825,f727]) ).
fof(f831,plain,
isCountable0(sdtlpdtrp0(xN,sK62)),
inference(unit_resulting_resolution,[],[f609,f727]) ).
fof(f833,plain,
sP9(sK62),
inference(resolution,[],[f822,f727]) ).
fof(f836,plain,
szDzozmdt0(sdtlpdtrp0(xC,sK62)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk),
inference(unit_resulting_resolution,[],[f675,f727]) ).
fof(f837,plain,
szDzozmdt0(sF64) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk),
inference(forward_demodulation,[],[f836,f787]) ).
fof(f896,plain,
( aSubsetOf0(sdtlcdtrc0(sF64,szDzozmdt0(sF64)),xT)
| ~ aElementOf0(sK62,szNzAzT0) ),
inference(superposition,[],[f684,f787]) ).
fof(f897,plain,
aSubsetOf0(sdtlcdtrc0(sF64,szDzozmdt0(sF64)),xT),
inference(forward_subsumption_resolution,[],[f896,f727]) ).
fof(f900,plain,
aSet0(sdtlpdtrp0(xN,sK62)),
inference(unit_resulting_resolution,[],[f612,f727]) ).
fof(f907,plain,
( iLess0(xk,xK)
| ~ aElementOf0(xk,szNzAzT0) ),
inference(superposition,[],[f454,f589]) ).
fof(f908,plain,
iLess0(xk,xK),
inference(forward_subsumption_resolution,[],[f907,f590]) ).
fof(f1099,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,sK62)),sdtlpdtrp0(xN,sK62)),
inference(unit_resulting_resolution,[],[f680,f727]) ).
fof(f1125,definition,
( spl65_25
<=> isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))) ),
introduced(definition,[new_symbols(definition,[spl65_25])],[avatar_definition]) ).
fof(f1126,plain,
( isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ spl65_25 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1127,plain,
( ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| spl65_25 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1176,plain,
sP8(sK62),
inference(resolution,[],[f595,f833]) ).
fof(f1226,plain,
( aElement0(szmzizndt0(sdtlpdtrp0(xN,sK62)))
| ~ aSet0(sdtlpdtrp0(xN,sK62)) ),
inference(resolution,[],[f1099,f391]) ).
fof(f1227,plain,
aElement0(szmzizndt0(sdtlpdtrp0(xN,sK62))),
inference(forward_subsumption_resolution,[],[f1226,f900]) ).
fof(f2004,plain,
aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),
inference(unit_resulting_resolution,[],[f678,f727]) ).
fof(f2766,plain,
~ sP6(sF64),
inference(resolution,[],[f565,f897]) ).
fof(f2890,plain,
~ sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64),
inference(unit_resulting_resolution,[],[f556,f837]) ).
fof(f3019,plain,
! [X2,X3,X0,X1] :
( sP23(sK49(X0,X1,X2,xk),sK62)
| ~ isCountable0(sK49(X0,X1,X2,xk))
| ~ aElementOf0(X3,xT)
| sdtlpdtrp0(X2,sK63(X3,sK49(X0,X1,X2,xk))) = X1
| ~ sP5(X0,X1,X2,xk) ),
inference(resolution,[],[f728,f568]) ).
fof(f3026,plain,
! [X2,X3,X0,X1] :
( sdtlpdtrp0(X2,sK63(X3,sK49(X0,X1,X2,xk))) = X1
| ~ aElementOf0(X3,xT)
| sP23(sK49(X0,X1,X2,xk),sK62)
| ~ sP5(X0,X1,X2,xk) ),
inference(forward_subsumption_resolution,[],[f3019,f572]) ).
fof(f3314,plain,
! [X2,X0,X1] :
( X0 != X1
| sP23(sK49(X2,X0,sF64,xk),sK62)
| ~ isCountable0(sK49(X2,X0,sF64,xk))
| ~ aElementOf0(X1,xT)
| ~ aElementOf0(X1,xT)
| sP23(sK49(X2,X0,sF64,xk),sK62)
| ~ sP5(X2,X0,sF64,xk) ),
inference(superposition,[],[f788,f3026]) ).
fof(f3319,plain,
! [X2,X0,X1] :
( X0 != X1
| sP23(sK49(X2,X0,sF64,xk),sK62)
| ~ isCountable0(sK49(X2,X0,sF64,xk))
| ~ aElementOf0(X1,xT)
| ~ sP5(X2,X0,sF64,xk) ),
inference(duplicate_literal_removal,[],[f3314]) ).
fof(f3320,plain,
! [X2,X0,X1] :
( X0 != X1
| sP23(sK49(X2,X0,sF64,xk),sK62)
| ~ aElementOf0(X1,xT)
| ~ sP5(X2,X0,sF64,xk) ),
inference(forward_subsumption_resolution,[],[f3319,f572]) ).
fof(f3321,plain,
! [X0,X1] :
( sP23(sK49(X0,X1,sF64,xk),sK62)
| ~ aElementOf0(X1,xT)
| ~ sP5(X0,X1,sF64,xk) ),
inference(equality_resolution,[],[f3320]) ).
fof(f6168,plain,
! [X2,X3,X0,X1] :
( ~ sP23(sK49(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),X1,X2,X3),X0)
| ~ sP5(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),X1,X2,X3) ),
inference(resolution,[],[f573,f720]) ).
fof(f13526,plain,
! [X0] :
( ~ aElementOf0(X0,xT)
| ~ sP5(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),X0,sF64,xk)
| ~ sP5(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),X0,sF64,xk) ),
inference(resolution,[],[f3321,f6168]) ).
fof(f13529,plain,
! [X0] :
( ~ sP5(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),X0,sF64,xk)
| ~ aElementOf0(X0,xT) ),
inference(duplicate_literal_removal,[],[f13526]) ).
fof(f13668,plain,
( ~ aSet0(sdtlpdtrp0(xN,sK62))
| ~ isCountable0(sdtlpdtrp0(xN,sK62))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,sK62)))
| spl65_25 ),
inference(resolution,[],[f1127,f433]) ).
fof(f13673,plain,
( ~ isCountable0(sdtlpdtrp0(xN,sK62))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,sK62)))
| spl65_25 ),
inference(forward_subsumption_resolution,[],[f13668,f900]) ).
fof(f13679,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,sK62)))
| spl65_25 ),
inference(forward_subsumption_resolution,[],[f13673,f831]) ).
fof(f13680,plain,
( $false
| spl65_25 ),
inference(forward_subsumption_resolution,[],[f13679,f1227]) ).
fof(f13681,plain,
spl65_25,
inference(avatar_contradiction_clause,[],[f13680]) ).
fof(f13840,plain,
( ~ aElementOf0(sK51(xk,sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),sF64),xT)
| ~ iLess0(xk,xK)
| ~ aFunction0(sF64)
| sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolution,[],[f13529,f582]) ).
fof(f13841,plain,
( ~ aElementOf0(sK51(xk,sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),sF64),xT)
| ~ iLess0(xk,xK)
| ~ aFunction0(sF64)
| sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(resolution,[],[f13529,f583]) ).
fof(f13848,plain,
( ~ iLess0(xk,xK)
| ~ aFunction0(sF64)
| sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13841,f586]) ).
fof(f13849,plain,
( ~ iLess0(xk,xK)
| ~ aFunction0(sF64)
| sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13840,f585]) ).
fof(f13856,plain,
( ~ aFunction0(sF64)
| sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13848,f908]) ).
fof(f13857,plain,
( ~ aFunction0(sF64)
| sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13849,f908]) ).
fof(f13859,plain,
( sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13856,f826]) ).
fof(f13860,plain,
( sP7(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))),xk,sF64)
| sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13857,f826]) ).
fof(f13862,plain,
( sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13859,f2890]) ).
fof(f13863,plain,
( sP6(sF64)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13860,f2890]) ).
fof(f13865,plain,
( ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13862,f2766]) ).
fof(f13866,plain,
( ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13863,f2766]) ).
fof(f13868,plain,
( ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13865,f2004]) ).
fof(f13869,plain,
( aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ isCountable0(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f13866,f2004]) ).
fof(f13871,plain,
( ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0)
| ~ spl65_25 ),
inference(forward_subsumption_resolution,[],[f13868,f1126]) ).
fof(f13872,plain,
( aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ aElementOf0(xk,szNzAzT0)
| ~ spl65_25 ),
inference(forward_subsumption_resolution,[],[f13869,f1126]) ).
fof(f13873,plain,
( ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),szNzAzT0)
| ~ spl65_25 ),
inference(forward_subsumption_resolution,[],[f13871,f590]) ).
fof(f13874,plain,
( aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62))))
| ~ spl65_25 ),
inference(forward_subsumption_resolution,[],[f13872,f590]) ).
fof(f13890,plain,
( ~ aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtlpdtrp0(xN,sK62))
| ~ spl65_25 ),
inference(unit_resulting_resolution,[],[f611,f727,f13873]) ).
fof(f14070,plain,
( aElementOf0(sK52(sdtmndt0(sdtlpdtrp0(xN,sK62),szmzizndt0(sdtlpdtrp0(xN,sK62)))),sdtlpdtrp0(xN,sK62))
| ~ sP8(sK62)
| ~ spl65_25 ),
inference(resolution,[],[f13874,f600]) ).
fof(f14091,plain,
( ~ sP8(sK62)
| ~ spl65_25 ),
inference(forward_subsumption_resolution,[],[f14070,f13890]) ).
fof(f14109,plain,
( $false
| ~ spl65_25 ),
inference(forward_subsumption_resolution,[],[f14091,f1176]) ).
fof(f14110,plain,
~ spl65_25,
inference(avatar_contradiction_clause,[],[f14109]) ).
cnf(s401,plain,
spl65_25,
inference(sat_conversion,[],[f13681]) ).
cnf(s426,plain,
~ spl65_25,
inference(sat_conversion,[],[f14110]) ).
cnf(s427,plain,
$false,
inference(rat,[],[s401,s426]) ).
fof(f14111,plain,
$false,
inference(avatar_sat_refutation,[],[s427]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM589+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 20:41:56 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.47/2.53 % (3190100)Detected formulas, will run a generic FOF schedule.
% 11.47/2.53 % (3190105)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3832954924:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.47/2.53 % (3190107)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1997967704:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.47/2.53 % (3190109)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1080093672:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.47/2.53 % (3190110)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=141158844:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.47/2.53 % (3190106)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=779858679:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.47/2.53 % (3190111)dis-21_1_sil=8000:lcm=predicate:random_seed=891686606:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.47/2.53 % (3190108)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2555485126:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.47/2.53 % (3190111)Instruction limit reached!
% 11.47/2.53 % (3190111)------------------------------
% 11.47/2.53 % (3190111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.53 % (3190111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.53 % (3190111)CaDiCaL version: 2.1.3
% 11.47/2.53 % (3190111)Termination reason: Instruction limit
% 11.47/2.53 % (3190111)Termination phase: Saturation
% 11.47/2.53 % (3190111)Time elapsed: 0.066 s
% 11.47/2.53 % (3190111)Peak memory usage: 90 MB
% 11.47/2.53 % (3190111)Instructions burned: 129 (million)
% 11.47/2.53 % (3190108)Instruction limit reached!
% 11.47/2.53 % (3190108)------------------------------
% 11.47/2.53 % (3190108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.53 % (3190108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.53 % (3190108)CaDiCaL version: 2.1.3
% 11.47/2.53 % (3190108)Termination reason: Instruction limit
% 11.47/2.53 % (3190108)Termination phase: Saturation
% 11.47/2.53 % (3190108)Time elapsed: 0.067 s
% 11.47/2.53 % (3190108)Peak memory usage: 90 MB
% 11.47/2.53 % (3190108)Instructions burned: 110 (million)
% 11.47/2.53 % (3190109)Instruction limit reached!
% 11.47/2.53 % (3190109)------------------------------
% 11.47/2.53 % (3190109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.53 % (3190109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.53 % (3190109)CaDiCaL version: 2.1.3
% 11.47/2.53 % (3190109)Termination reason: Instruction limit
% 11.47/2.53 % (3190109)Termination phase: Saturation
% 11.47/2.53 % (3190109)Time elapsed: 0.072 s
% 11.47/2.53 % (3190109)Peak memory usage: 89 MB
% 11.47/2.53 % (3190109)Instructions burned: 119 (million)
% 11.47/2.53 % (3190110)Instruction limit reached!
% 11.47/2.53 % (3190110)------------------------------
% 11.47/2.53 % (3190110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.53 % (3190110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.53 % (3190110)CaDiCaL version: 2.1.3
% 11.47/2.53 % (3190110)Termination reason: Instruction limit
% 11.47/2.53 % (3190110)Termination phase: Saturation
% 11.47/2.53 % (3190110)Time elapsed: 0.098 s
% 11.47/2.53 % (3190110)Peak memory usage: 90 MB
% 11.47/2.53 % (3190110)Instructions burned: 139 (million)
% 11.47/2.53 % (3190120)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1219296653:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.47/2.53 % (3190119)lrs+10_1_sil=8000:sp=occurrence:random_seed=3668359116:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.47/2.53 % (3190121)lrs+1011_1_sil=32000:sp=occurrence:random_seed=745398196:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.47/2.53 % (3190122)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1041008421:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 11.47/2.53 % (3190120)Instruction limit reached!
% 17.45/3.33 % (3190120)------------------------------
% 17.45/3.33 % (3190120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190120)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190120)Termination reason: Instruction limit
% 17.45/3.33 % (3190120)Termination phase: Saturation
% 17.45/3.33 % (3190120)Time elapsed: 0.093 s
% 17.45/3.33 % (3190120)Peak memory usage: 91 MB
% 17.45/3.33 % (3190120)Instructions burned: 159 (million)
% 17.45/3.33 % (3190119)Instruction limit reached!
% 17.45/3.33 % (3190119)------------------------------
% 17.45/3.33 % (3190119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190119)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190119)Termination reason: Instruction limit
% 17.45/3.33 % (3190119)Termination phase: Saturation
% 17.45/3.33 % (3190119)Time elapsed: 0.171 s
% 17.45/3.33 % (3190119)Peak memory usage: 92 MB
% 17.45/3.33 % (3190119)Instructions burned: 285 (million)
% 17.45/3.33 % (3190122)Instruction limit reached!
% 17.45/3.33 % (3190122)------------------------------
% 17.45/3.33 % (3190122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190122)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190122)Termination reason: Instruction limit
% 17.45/3.33 % (3190122)Termination phase: Saturation
% 17.45/3.33 % (3190122)Time elapsed: 0.151 s
% 17.45/3.33 % (3190122)Peak memory usage: 92 MB
% 17.45/3.33 % (3190122)Instructions burned: 248 (million)
% 17.45/3.33 % (3190127)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1104398738:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 17.45/3.33 % (3190121)Instruction limit reached!
% 17.45/3.33 % (3190121)------------------------------
% 17.45/3.33 % (3190121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190121)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190121)Termination reason: Instruction limit
% 17.45/3.33 % (3190121)Termination phase: Saturation
% 17.45/3.33 % (3190121)Time elapsed: 0.229 s
% 17.45/3.33 % (3190121)Peak memory usage: 92 MB
% 17.45/3.33 % (3190121)Instructions burned: 325 (million)
% 17.45/3.33 % (3190128)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2556312523:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 17.45/3.33 % (3190129)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3577356683:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.45/3.33 % (3190131)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4028529182:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 17.45/3.33 % (3190127)Instruction limit reached!
% 17.45/3.33 % (3190127)------------------------------
% 17.45/3.33 % (3190127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190127)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190127)Termination reason: Instruction limit
% 17.45/3.33 % (3190127)Termination phase: Saturation
% 17.45/3.33 % (3190127)Time elapsed: 0.181 s
% 17.45/3.33 % (3190127)Peak memory usage: 90 MB
% 17.45/3.33 % (3190127)Instructions burned: 295 (million)
% 17.45/3.33 % (3190129)Instruction limit reached!
% 17.45/3.33 % (3190129)------------------------------
% 17.45/3.33 % (3190129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190129)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190129)Termination reason: Instruction limit
% 17.45/3.33 % (3190129)Termination phase: Saturation
% 17.45/3.33 % (3190129)Time elapsed: 0.074 s
% 17.45/3.33 % (3190129)Peak memory usage: 91 MB
% 17.45/3.33 % (3190129)Instructions burned: 114 (million)
% 17.45/3.33 % (3190131)Instruction limit reached!
% 17.45/3.33 % (3190131)------------------------------
% 17.45/3.33 % (3190131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.45/3.33 % (3190131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.45/3.33 % (3190131)CaDiCaL version: 2.1.3
% 17.45/3.33 % (3190131)Termination reason: Instruction limit
% 17.45/3.33 % (3190131)Termination phase: Saturation
% 34.71/5.93 % (3190131)Time elapsed: 0.069 s
% 34.71/5.93 % (3190131)Peak memory usage: 89 MB
% 34.71/5.93 % (3190131)Instructions burned: 128 (million)
% 34.71/5.93 % (3190135)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1853867000:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 34.71/5.93 % (3190136)lrs+10_1_sil=8000:sp=occurrence:random_seed=1285845580:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 34.71/5.93 % (3190135)Instruction limit reached!
% 34.71/5.93 % (3190135)------------------------------
% 34.71/5.93 % (3190135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190135)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190135)Termination reason: Instruction limit
% 34.71/5.93 % (3190135)Termination phase: Saturation
% 34.71/5.93 % (3190135)Time elapsed: 0.059 s
% 34.71/5.93 % (3190135)Peak memory usage: 89 MB
% 34.71/5.93 % (3190135)Instructions burned: 114 (million)
% 34.71/5.93 % (3190137)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=486376073:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 34.71/5.93 % (3190140)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3584263538:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 34.71/5.93 % (3190137)Instruction limit reached!
% 34.71/5.93 % (3190137)------------------------------
% 34.71/5.93 % (3190137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190137)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190137)Termination reason: Instruction limit
% 34.71/5.93 % (3190137)Termination phase: Saturation
% 34.71/5.93 % (3190137)Time elapsed: 0.272 s
% 34.71/5.93 % (3190137)Peak memory usage: 93 MB
% 34.71/5.93 % (3190137)Instructions burned: 437 (million)
% 34.71/5.93 % (3190143)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=821824665:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 34.71/5.93 % (3190136)Instruction limit reached!
% 34.71/5.93 % (3190136)------------------------------
% 34.71/5.93 % (3190136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190136)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190136)Termination reason: Instruction limit
% 34.71/5.93 % (3190136)Termination phase: Saturation
% 34.71/5.93 % (3190136)Time elapsed: 0.507 s
% 34.71/5.93 % (3190136)Peak memory usage: 97 MB
% 34.71/5.93 % (3190136)Instructions burned: 908 (million)
% 34.71/5.93 % (3190143)Instruction limit reached!
% 34.71/5.93 % (3190143)------------------------------
% 34.71/5.93 % (3190143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190143)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190143)Termination reason: Instruction limit
% 34.71/5.93 % (3190143)Termination phase: Saturation
% 34.71/5.93 % (3190143)Time elapsed: 0.082 s
% 34.71/5.93 % (3190143)Peak memory usage: 90 MB
% 34.71/5.93 % (3190143)Instructions burned: 134 (million)
% 34.71/5.93 % (3190145)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3420199889:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 34.71/5.93 % (3190146)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=249957029:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 34.71/5.93 % (3190128)Instruction limit reached!
% 34.71/5.93 % (3190128)------------------------------
% 34.71/5.93 % (3190128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190128)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190128)Termination reason: Instruction limit
% 34.71/5.93 % (3190128)Termination phase: Saturation
% 34.71/5.93 % (3190128)Time elapsed: 0.949 s
% 34.71/5.93 % (3190128)Peak memory usage: 143 MB
% 34.71/5.93 % (3190128)Instructions burned: 2351 (million)
% 34.71/5.93 % (3190149)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=411125339:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 34.71/5.93 % (3190149)Instruction limit reached!
% 34.71/5.93 % (3190149)------------------------------
% 34.71/5.93 % (3190149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190149)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190149)Termination reason: Instruction limit
% 34.71/5.93 % (3190149)Termination phase: Saturation
% 34.71/5.93 % (3190149)Time elapsed: 0.045 s
% 34.71/5.93 % (3190149)Peak memory usage: 91 MB
% 34.71/5.93 % (3190149)Instructions burned: 128 (million)
% 34.71/5.93 % (3190151)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1789703697:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 34.71/5.93 % (3190151)Instruction limit reached!
% 34.71/5.93 % (3190151)------------------------------
% 34.71/5.93 % (3190151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190151)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190151)Termination reason: Instruction limit
% 34.71/5.93 % (3190151)Termination phase: Saturation
% 34.71/5.93 % (3190151)Time elapsed: 0.046 s
% 34.71/5.93 % (3190151)Peak memory usage: 91 MB
% 34.71/5.93 % (3190151)Instructions burned: 136 (million)
% 34.71/5.93 % (3190145)Instruction limit reached!
% 34.71/5.93 % (3190145)------------------------------
% 34.71/5.93 % (3190145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190145)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190145)Termination reason: Instruction limit
% 34.71/5.93 % (3190145)Termination phase: Saturation
% 34.71/5.93 % (3190145)Time elapsed: 0.348 s
% 34.71/5.93 % (3190145)Peak memory usage: 95 MB
% 34.71/5.93 % (3190145)Instructions burned: 593 (million)
% 34.71/5.93 % (3190153)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2122794114:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 34.71/5.93 % (3190154)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=729019055:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 34.71/5.93 % (3190153)Instruction limit reached!
% 34.71/5.93 % (3190153)------------------------------
% 34.71/5.93 % (3190153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190153)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190153)Termination reason: Instruction limit
% 34.71/5.93 % (3190153)Termination phase: Saturation
% 34.71/5.93 % (3190153)Time elapsed: 0.047 s
% 34.71/5.93 % (3190153)Peak memory usage: 92 MB
% 34.71/5.93 % (3190153)Instructions burned: 144 (million)
% 34.71/5.93 % (3190157)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1543916674:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 34.71/5.93 % (3190154)Instruction limit reached!
% 34.71/5.93 % (3190154)------------------------------
% 34.71/5.93 % (3190154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190154)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190154)Termination reason: Instruction limit
% 34.71/5.93 % (3190154)Termination phase: Saturation
% 34.71/5.93 % (3190154)Time elapsed: 0.254 s
% 34.71/5.93 % (3190154)Peak memory usage: 95 MB
% 34.71/5.93 % (3190154)Instructions burned: 432 (million)
% 34.71/5.93 % (3190159)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3849702700:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 34.71/5.93 % (3190159)Instruction limit reached!
% 34.71/5.93 % (3190159)------------------------------
% 34.71/5.93 % (3190159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190159)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190159)Termination reason: Instruction limit
% 34.71/5.93 % (3190159)Termination phase: Saturation
% 34.71/5.93 % (3190159)Time elapsed: 0.095 s
% 34.71/5.93 % (3190159)Peak memory usage: 92 MB
% 34.71/5.93 % (3190159)Instructions burned: 151 (million)
% 34.71/5.93 % (3190161)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3170140945:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi)
% 34.71/5.93 % (3190157)Instruction limit reached!
% 34.71/5.93 % (3190157)------------------------------
% 34.71/5.93 % (3190157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190157)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190157)Termination reason: Instruction limit
% 34.71/5.93 % (3190157)Termination phase: Saturation
% 34.71/5.93 % (3190157)Time elapsed: 1.740 s
% 34.71/5.93 % (3190157)Peak memory usage: 139 MB
% 34.71/5.93 % (3190157)Instructions burned: 6062 (million)
% 34.71/5.93 % (3190163)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3087399738:i=667:av=off:fsr=off_2961 on theBenchmark for (2961ds/667Mi)
% 34.71/5.93 % (3190163)Instruction limit reached!
% 34.71/5.93 % (3190163)------------------------------
% 34.71/5.93 % (3190163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190163)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190163)Termination reason: Instruction limit
% 34.71/5.93 % (3190163)Termination phase: Saturation
% 34.71/5.93 % (3190163)Time elapsed: 0.188 s
% 34.71/5.93 % (3190163)Peak memory usage: 96 MB
% 34.71/5.93 % (3190163)Instructions burned: 671 (million)
% 34.71/5.93 % (3190140)Instruction limit reached!
% 34.71/5.93 % (3190140)------------------------------
% 34.71/5.93 % (3190140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190140)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190140)Termination reason: Instruction limit
% 34.71/5.93 % (3190140)Termination phase: Saturation
% 34.71/5.93 % (3190140)Time elapsed: 3.128 s
% 34.71/5.93 % (3190140)Peak memory usage: 162 MB
% 34.71/5.93 % (3190140)Instructions burned: 5202 (million)
% 34.71/5.93 % (3190165)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1203477368:s2a=on:i=185:s2at=1.8:fdi=4_2958 on theBenchmark for (2958ds/185Mi)
% 34.71/5.93 % (3190165)Instruction limit reached!
% 34.71/5.93 % (3190165)------------------------------
% 34.71/5.93 % (3190165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190165)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190165)Termination reason: Instruction limit
% 34.71/5.93 % (3190165)Termination phase: Saturation
% 34.71/5.93 % (3190165)Time elapsed: 0.062 s
% 34.71/5.93 % (3190165)Peak memory usage: 91 MB
% 34.71/5.93 % (3190165)Instructions burned: 186 (million)
% 34.71/5.93 % (3190166)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4259262131:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2958 on theBenchmark for (2958ds/193Mi)
% 34.71/5.93 % (3190168)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1833514594:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2957 on theBenchmark for (2957ds/4850Mi)
% 34.71/5.93 % (3190166)Instruction limit reached!
% 34.71/5.93 % (3190166)------------------------------
% 34.71/5.93 % (3190166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.93 % (3190166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.93 % (3190166)CaDiCaL version: 2.1.3
% 34.71/5.93 % (3190166)Termination reason: Instruction limit
% 34.71/5.93 % (3190166)Termination phase: Saturation
% 34.71/5.93 % (3190166)Time elapsed: 0.116 s
% 34.71/5.93 % (3190166)Peak memory usage: 92 MB
% 34.71/5.93 % (3190166)Instructions burned: 195 (million)
% 34.71/5.93 % (3190171)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2723896064:i=12111:sd=1:ss=included_2955 on theBenchmark for (2955ds/12111Mi)
% 34.71/5.93 % (3190161)First to succeed.
% 34.71/5.93 % (3190161)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3190100"
% 34.71/5.93 % (3190161)Refutation found. Thanks to Tanya!
% 34.71/5.93 % SZS status Theorem for theBenchmark
% 34.71/5.93 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/6.03 % (3190161)------------------------------
% 0.16/6.03 % (3190161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/6.03 % (3190161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/6.03 % (3190161)CaDiCaL version: 2.1.3
% 0.16/6.03 % (3190161)Termination reason: Refutation
% 0.16/6.03 % (3190161)Time elapsed: 2.203 s
% 0.16/6.03 % (3190161)Peak memory usage: 149 MB
% 0.16/6.03 % (3190161)Instructions burned: 3323 (million)
% 0.16/6.03 % (3190161)------------------------------
% 0.16/6.03 % (3190161)------------------------------
% 0.16/6.03 % (3190100)Success in time 5.076 s
% 0.16/6.03 % Vampire exiting
%------------------------------------------------------------------------------