%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM591+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 : n017.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 22.42s 7.91s
% Output : Refutation 50.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 19
% Syntax : Number of formulae : 98 ( 22 unt; 10 def)
% Number of atoms : 1044 ( 172 equ)
% Maximal formula atoms : 47 ( 10 avg)
% Number of connectives : 1302 ( 356 ~; 308 |; 529 &)
% ( 30 <=>; 79 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 9 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-4 aty)
% Number of functors : 32 ( 32 usr; 10 con; 0-5 aty)
% Number of variables : 379 ( 300 !; 79 ?)
% Comments :
%------------------------------------------------------------------------------
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(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,axiom,
iLess0(xk,xK),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4423) ).
fof(f90,axiom,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4448) ).
fof(f91,axiom,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aSet0(xY)
& ! [X0] :
( aElementOf0(X0,xY)
<=> ( aElement0(X0)
& aElementOf0(X0,sdtlpdtrp0(xN,xi))
& X0 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) )
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& xd = sdtlpdtrp0(xC,xi) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4448_02) ).
fof(f92,axiom,
( ! [X0] :
( aElementOf0(X0,xY)
=> aElementOf0(X0,szNzAzT0) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X0] :
( ( aElementOf0(X0,szDzozmdt0(xd))
=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xY) )
& aSubsetOf0(X0,xY)
& sbrdtbr0(X0) = xk ) )
& ( ( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xY) ) )
| aSubsetOf0(X0,xY) )
& sbrdtbr0(X0) = xk )
=> aElementOf0(X0,szDzozmdt0(xd)) ) )
& ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))
<=> ? [X1] :
( aElementOf0(X1,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X1) = X0 ) )
& ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))
=> aElementOf0(X0,xT) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4482) ).
fof(f93,conjecture,
? [X0,X1] :
( aElementOf0(X0,xT)
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xY) ) )
| aSubsetOf0(X1,xY) )
& isCountable0(X1)
& ! [X2] :
( ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) )
& aSubsetOf0(X2,X1)
& sbrdtbr0(X2) = xk
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
=> sdtlpdtrp0(xd,X2) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f94,negated_conjecture,
~ ? [X0,X1] :
( aElementOf0(X0,xT)
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xY) ) )
| aSubsetOf0(X1,xY) )
& isCountable0(X1)
& ! [X2] :
( ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) )
& aSubsetOf0(X2,X1)
& sbrdtbr0(X2) = xk
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
=> sdtlpdtrp0(xd,X2) = X0 ) ),
inference(negated_conjecture,[status(cth)],[f93]) ).
fof(f103,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(f107,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(f108,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(f110,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aSet0(xY)
& ! [X1] :
( aElementOf0(X1,xY)
<=> ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& szmzizndt0(sdtlpdtrp0(xN,xi)) != X1 ) )
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& xd = sdtlpdtrp0(xC,xi) ),
inference(rectify,[],[f91]) ).
fof(f111,plain,
( ! [X0] :
( aElementOf0(X0,xY)
=> aElementOf0(X0,szNzAzT0) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X1] :
( ( aElementOf0(X1,szDzozmdt0(xd))
=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xY) )
& aSubsetOf0(X1,xY)
& sbrdtbr0(X1) = xk ) )
& ( ( ( ( aSet0(X1)
& ! [X3] :
( aElementOf0(X3,X1)
=> aElementOf0(X3,xY) ) )
| aSubsetOf0(X1,xY) )
& sbrdtbr0(X1) = xk )
=> aElementOf0(X1,szDzozmdt0(xd)) ) )
& ! [X4] :
( aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd)))
<=> ? [X5] :
( aElementOf0(X5,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X5) = X4 ) )
& ! [X6] :
( aElementOf0(X6,sdtlcdtrc0(xd,szDzozmdt0(xd)))
=> aElementOf0(X6,xT) ) ),
inference(rectify,[],[f92]) ).
fof(f112,plain,
~ ? [X0,X1] :
( aElementOf0(X0,xT)
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xY) ) )
| aSubsetOf0(X1,xY) )
& isCountable0(X1)
& ! [X3] :
( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,X1) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X1,xk)) )
=> sdtlpdtrp0(xd,X3) = X0 ) ),
inference(rectify,[],[f94]) ).
fof(f215,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,[],[f103]) ).
fof(f216,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,[],[f215]) ).
fof(f226,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,[],[f107]) ).
fof(f227,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,[],[f226]) ).
fof(f228,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,[],[f108]) ).
fof(f231,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xi)) )
& aSet0(xY)
& ! [X1] :
( aElementOf0(X1,xY)
<=> ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& szmzizndt0(sdtlpdtrp0(xN,xi)) != X1 ) )
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& xd = sdtlpdtrp0(xC,xi) ),
inference(ennf_transformation,[],[f110]) ).
fof(f232,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xY) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,xY)
| ~ aElementOf0(X2,X1) )
& aSubsetOf0(X1,xY)
& sbrdtbr0(X1) = xk )
| ~ aElementOf0(X1,szDzozmdt0(xd)) )
& ( aElementOf0(X1,szDzozmdt0(xd))
| ( ( ~ aSet0(X1)
| ? [X3] :
( ~ aElementOf0(X3,xY)
& aElementOf0(X3,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| sbrdtbr0(X1) != xk ) )
& ! [X4] :
( aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd)))
<=> ? [X5] :
( aElementOf0(X5,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X5) = X4 ) )
& ! [X6] :
( aElementOf0(X6,xT)
| ~ aElementOf0(X6,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
inference(ennf_transformation,[],[f111]) ).
fof(f233,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xY) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,xY)
| ~ aElementOf0(X2,X1) )
& aSubsetOf0(X1,xY)
& sbrdtbr0(X1) = xk )
| ~ aElementOf0(X1,szDzozmdt0(xd)) )
& ( aElementOf0(X1,szDzozmdt0(xd))
| ( ( ~ aSet0(X1)
| ? [X3] :
( ~ aElementOf0(X3,xY)
& aElementOf0(X3,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| sbrdtbr0(X1) != xk ) )
& ! [X4] :
( aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd)))
<=> ? [X5] :
( aElementOf0(X5,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X5) = X4 ) )
& ! [X6] :
( aElementOf0(X6,xT)
| ~ aElementOf0(X6,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
inference(flattening,[],[f232]) ).
fof(f234,plain,
! [X0,X1] :
( ~ aElementOf0(X0,xT)
| ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,xY)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| ~ isCountable0(X1)
| ? [X3] :
( sdtlpdtrp0(xd,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X1,xk)) ) ),
inference(ennf_transformation,[],[f112]) ).
fof(f235,plain,
! [X0,X1] :
( ~ aElementOf0(X0,xT)
| ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,xY)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| ~ isCountable0(X1)
| ? [X3] :
( sdtlpdtrp0(xd,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X1,xk)) ) ),
inference(flattening,[],[f234]) ).
fof(f242,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(f243,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(f244,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(f245,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(f246,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,[],[f216,f245,f244,f243,f242]) ).
fof(f254,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(f255,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(f256,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(f257,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(f258,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(f259,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,[],[f227,f258,f257,f256,f255,f254]) ).
fof(f265,definition,
! [X0,X1] :
( ? [X3] :
( sdtlpdtrp0(xd,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X1,xk)) )
| ~ sP22(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f266,plain,
! [X0,X1] :
( ~ aElementOf0(X0,xT)
| ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,xY)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| ~ isCountable0(X1)
| sP22(X0,X1) ),
inference(definition_folding,[],[f235,f265]) ).
fof(f329,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,[],[f245]) ).
fof(f330,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,[],[f329]) ).
fof(f331,plain,
! [X0,X1,X2] :
( ( ( ( ( ( ( ~ aSet0(sK44(X0,X1,X2))
| ( ~ aElementOf0(sK45(X0,X1,X2),X0)
& aElementOf0(sK45(X0,X1,X2),sK44(X0,X1,X2)) ) )
& ~ aSubsetOf0(sK44(X0,X1,X2),X0) )
| sbrdtbr0(sK44(X0,X1,X2)) != X1 )
& aElementOf0(sK44(X0,X1,X2),szDzozmdt0(X2)) )
| sP4(X2,sK44(X0,X1,X2),X0,X1) )
& slbdtsldtrb0(X0,X1) != szDzozmdt0(X2) )
| ~ sP7(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44,sK45]),skolemize(X3,sK44(X0,X1,X2)),skolemize(X4,sK45(X0,X1,X2))],[f330]) ).
fof(f332,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,[],[f244]) ).
fof(f333,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,[],[f332]) ).
fof(f334,plain,
! [X0] :
( ( ~ aElementOf0(sK46(X0),xT)
& aElementOf0(sK46(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(sK47(X0,X2),szDzozmdt0(X0))
& sdtlpdtrp0(X0,sK47(X0,X2)) = X2 )
| ~ aElementOf0(X2,sdtlcdtrc0(X0,szDzozmdt0(X0))) ) ) )
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47]),skolemize(X1,sK46(X0)),skolemize(X4,sK47(X0,X2))],[f333]) ).
fof(f335,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,[],[f243]) ).
fof(f336,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,[],[f335]) ).
fof(f337,plain,
! [X0,X1,X2,X3] :
( ( aSet0(sK48(X0,X1,X2,X3))
& ! [X5] :
( aElementOf0(X5,X0)
| ~ aElementOf0(X5,sK48(X0,X1,X2,X3)) )
& aSubsetOf0(sK48(X0,X1,X2,X3),X0)
& isCountable0(sK48(X0,X1,X2,X3))
& ! [X6] :
( sdtlpdtrp0(X2,X6) = X1
| ( ( ( ( ~ aSet0(X6)
| ( ~ aElementOf0(sK49(X0,X1,X2,X3,X6),sK48(X0,X1,X2,X3))
& aElementOf0(sK49(X0,X1,X2,X3,X6),X6) ) )
& ~ aSubsetOf0(X6,sK48(X0,X1,X2,X3)) )
| sbrdtbr0(X6) != X3 )
& ~ aElementOf0(X6,slbdtsldtrb0(sK48(X0,X1,X2,X3),X3)) ) ) )
| ~ sP5(X0,X1,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48,sK49]),skolemize(X4,sK48(X0,X1,X2,X3)),skolemize(X7,sK49(X0,X1,X2,X3,X6))],[f336]) ).
fof(f340,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,[],[f246]) ).
fof(f341,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( aElementOf0(sK50(X0,X1,X2),xT)
& sP5(X1,sK50(X0,X1,X2),X2,X0) )
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2) )
| ( ( ~ aSet0(X1)
| ( ~ aElementOf0(sK51(X1),szNzAzT0)
& aElementOf0(sK51(X1),X1) ) )
& ~ aSubsetOf0(X1,szNzAzT0) )
| ~ isCountable0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50,sK51]),skolemize(X3,sK50(X0,X1,X2)),skolemize(X4,sK51(X1))],[f340]) ).
fof(f375,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,[],[f228]) ).
fof(f376,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,[],[f375]) ).
fof(f377,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(sK57(X0,X1),szDzozmdt0(sdtlpdtrp0(xC,X0)))
& sdtlpdtrp0(sdtlpdtrp0(xC,X0),sK57(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,[sK57]),skolemize(X3,sK57(X0,X1))],[f376]) ).
fof(f391,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xi)) )
& aSet0(xY)
& ! [X1] :
( ( aElementOf0(X1,xY)
| ~ aElement0(X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| szmzizndt0(sdtlpdtrp0(xN,xi)) = X1 )
& ( ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& szmzizndt0(sdtlpdtrp0(xN,xi)) != X1 )
| ~ aElementOf0(X1,xY) ) )
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& xd = sdtlpdtrp0(xC,xi) ),
inference(nnf_transformation,[],[f231]) ).
fof(f392,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xi)) )
& aSet0(xY)
& ! [X1] :
( ( aElementOf0(X1,xY)
| ~ aElement0(X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| szmzizndt0(sdtlpdtrp0(xN,xi)) = X1 )
& ( ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& szmzizndt0(sdtlpdtrp0(xN,xi)) != X1 )
| ~ aElementOf0(X1,xY) ) )
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& xd = sdtlpdtrp0(xC,xi) ),
inference(flattening,[],[f391]) ).
fof(f393,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xY) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,xY)
| ~ aElementOf0(X2,X1) )
& aSubsetOf0(X1,xY)
& sbrdtbr0(X1) = xk )
| ~ aElementOf0(X1,szDzozmdt0(xd)) )
& ( aElementOf0(X1,szDzozmdt0(xd))
| ( ( ~ aSet0(X1)
| ? [X3] :
( ~ aElementOf0(X3,xY)
& aElementOf0(X3,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| sbrdtbr0(X1) != xk ) )
& ! [X4] :
( ( aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ! [X5] :
( ~ aElementOf0(X5,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X5) != X4 ) )
& ( ? [X5] :
( aElementOf0(X5,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X5) = X4 )
| ~ aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) )
& ! [X6] :
( aElementOf0(X6,xT)
| ~ aElementOf0(X6,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
inference(nnf_transformation,[],[f233]) ).
fof(f394,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xY) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,xY)
| ~ aElementOf0(X2,X1) )
& aSubsetOf0(X1,xY)
& sbrdtbr0(X1) = xk )
| ~ aElementOf0(X1,szDzozmdt0(xd)) )
& ( aElementOf0(X1,szDzozmdt0(xd))
| ( ( ~ aSet0(X1)
| ? [X3] :
( ~ aElementOf0(X3,xY)
& aElementOf0(X3,X1) ) )
& ~ aSubsetOf0(X1,xY) )
| sbrdtbr0(X1) != xk ) )
& ! [X4] :
( ( aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ! [X5] :
( ~ aElementOf0(X5,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X5) != X4 ) )
& ( ? [X6] :
( aElementOf0(X6,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X6) = X4 )
| ~ aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) )
& ! [X7] :
( aElementOf0(X7,xT)
| ~ aElementOf0(X7,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
inference(rectify,[],[f393]) ).
fof(f395,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xY) )
& aSubsetOf0(xY,szNzAzT0)
& isCountable0(xY)
& aFunction0(xd)
& ! [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,xY)
| ~ aElementOf0(X2,X1) )
& aSubsetOf0(X1,xY)
& sbrdtbr0(X1) = xk )
| ~ aElementOf0(X1,szDzozmdt0(xd)) )
& ( aElementOf0(X1,szDzozmdt0(xd))
| ( ( ~ aSet0(X1)
| ( ~ aElementOf0(sK60(X1),xY)
& aElementOf0(sK60(X1),X1) ) )
& ~ aSubsetOf0(X1,xY) )
| sbrdtbr0(X1) != xk ) )
& ! [X4] :
( ( aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd)))
| ! [X5] :
( ~ aElementOf0(X5,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X5) != X4 ) )
& ( ( aElementOf0(sK61(X4),szDzozmdt0(xd))
& sdtlpdtrp0(xd,sK61(X4)) = X4 )
| ~ aElementOf0(X4,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) )
& ! [X7] :
( aElementOf0(X7,xT)
| ~ aElementOf0(X7,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60,sK61]),skolemize(X3,sK60(X1)),skolemize(X6,sK61(X4))],[f394]) ).
fof(f396,plain,
! [X0,X1] :
( ? [X3] :
( sdtlpdtrp0(xd,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xk
& aElementOf0(X3,slbdtsldtrb0(X1,xk)) )
| ~ sP22(X0,X1) ),
inference(nnf_transformation,[],[f265]) ).
fof(f397,plain,
! [X0,X1] :
( ? [X2] :
( sdtlpdtrp0(xd,X2) != X0
& aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X1)
| ~ aElementOf0(X3,X2) )
& aSubsetOf0(X2,X1)
& sbrdtbr0(X2) = xk
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
| ~ sP22(X0,X1) ),
inference(rectify,[],[f396]) ).
fof(f398,plain,
! [X0,X1] :
( ( sdtlpdtrp0(xd,sK62(X0,X1)) != X0
& aSet0(sK62(X0,X1))
& ! [X3] :
( aElementOf0(X3,X1)
| ~ aElementOf0(X3,sK62(X0,X1)) )
& aSubsetOf0(sK62(X0,X1),X1)
& xk = sbrdtbr0(sK62(X0,X1))
& aElementOf0(sK62(X0,X1),slbdtsldtrb0(X1,xk)) )
| ~ sP22(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X2,sK62(X0,X1))],[f397]) ).
fof(f399,plain,
! [X0,X1] :
( ~ aElementOf0(X0,xT)
| ( ( ~ aSet0(X1)
| ( ~ aElementOf0(sK63(X1),xY)
& aElementOf0(sK63(X1),X1) ) )
& ~ aSubsetOf0(X1,xY) )
| ~ isCountable0(X1)
| sP22(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X2,sK63(X1))],[f266]) ).
fof(f565,plain,
! [X2,X0,X1] :
( slbdtsldtrb0(X0,X1) != szDzozmdt0(X2)
| ~ sP7(X0,X1,X2) ),
inference(cnf_transformation,[],[f331]) ).
fof(f574,plain,
! [X0] :
( ~ aSubsetOf0(sdtlcdtrc0(X0,szDzozmdt0(X0)),xT)
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f334]) ).
fof(f577,plain,
! [X2,X3,X0,X1,X6] :
( ~ aElementOf0(X6,slbdtsldtrb0(sK48(X0,X1,X2,X3),X3))
| sdtlpdtrp0(X2,X6) = X1
| ~ sP5(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f337]) ).
fof(f581,plain,
! [X2,X3,X0,X1] :
( isCountable0(sK48(X0,X1,X2,X3))
| ~ sP5(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f337]) ).
fof(f582,plain,
! [X2,X3,X0,X1] :
( aSubsetOf0(sK48(X0,X1,X2,X3),X0)
| ~ sP5(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f337]) ).
fof(f590,plain,
! [X2,X0,X1] :
( sP5(X1,sK50(X0,X1,X2),X2,X0)
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f341]) ).
fof(f593,plain,
! [X2,X0,X1] :
( aElementOf0(sK50(X0,X1,X2),xT)
| ~ iLess0(X0,xK)
| ~ aFunction0(X2)
| sP7(X1,X0,X2)
| sP6(X2)
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f341]) ).
fof(f599,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f80]) ).
fof(f684,plain,
! [X0] :
( slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk) = szDzozmdt0(sdtlpdtrp0(xC,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f693,plain,
! [X0] :
( aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f725,plain,
iLess0(xk,xK),
inference(cnf_transformation,[],[f89]) ).
fof(f726,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f90]) ).
fof(f727,plain,
xd = sdtlpdtrp0(xC,xi),
inference(cnf_transformation,[],[f392]) ).
fof(f728,plain,
xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),
inference(cnf_transformation,[],[f392]) ).
fof(f747,plain,
aFunction0(xd),
inference(cnf_transformation,[],[f395]) ).
fof(f748,plain,
isCountable0(xY),
inference(cnf_transformation,[],[f395]) ).
fof(f749,plain,
aSubsetOf0(xY,szNzAzT0),
inference(cnf_transformation,[],[f395]) ).
fof(f751,plain,
! [X0,X1] :
( aElementOf0(sK62(X0,X1),slbdtsldtrb0(X1,xk))
| ~ sP22(X0,X1) ),
inference(cnf_transformation,[],[f398]) ).
fof(f756,plain,
! [X0,X1] :
( sdtlpdtrp0(xd,sK62(X0,X1)) != X0
| ~ sP22(X0,X1) ),
inference(cnf_transformation,[],[f398]) ).
fof(f757,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,xY)
| ~ aElementOf0(X0,xT)
| ~ isCountable0(X1)
| sP22(X0,X1) ),
inference(cnf_transformation,[],[f399]) ).
fof(f1112,plain,
( aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(superposition,[],[f693,f727]) ).
fof(f1113,plain,
aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT),
inference(forward_subsumption_resolution,[],[f1112,f726]) ).
fof(f1721,plain,
( slbdtsldtrb0(xY,xk) = szDzozmdt0(sdtlpdtrp0(xC,xi))
| ~ aElementOf0(xi,szNzAzT0) ),
inference(superposition,[],[f684,f728]) ).
fof(f1723,plain,
slbdtsldtrb0(xY,xk) = szDzozmdt0(sdtlpdtrp0(xC,xi)),
inference(forward_subsumption_resolution,[],[f1721,f726]) ).
fof(f1727,plain,
szDzozmdt0(xd) = slbdtsldtrb0(xY,xk),
inference(forward_demodulation,[],[f1723,f727]) ).
fof(f1738,plain,
~ sP6(xd),
inference(resolution,[],[f574,f1113]) ).
fof(f2255,plain,
~ sP7(xY,xk,xd),
inference(unit_resulting_resolution,[],[f565,f1727]) ).
fof(f2279,plain,
! [X2,X3,X0,X1] :
( ~ sP5(xY,X0,X1,X2)
| ~ aElementOf0(X3,xT)
| ~ isCountable0(sK48(xY,X0,X1,X2))
| sP22(X3,sK48(xY,X0,X1,X2)) ),
inference(resolution,[],[f582,f757]) ).
fof(f2280,plain,
! [X2,X3,X0,X1] :
( sP22(X3,sK48(xY,X0,X1,X2))
| ~ aElementOf0(X3,xT)
| ~ sP5(xY,X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f2279,f581]) ).
fof(f4320,plain,
sP5(xY,sK50(xk,xY,xd),xd,xk),
inference(unit_resulting_resolution,[],[f590,f747,f748,f1738,f749,f2255,f599,f725]) ).
fof(f14968,plain,
aElementOf0(sK50(xk,xY,xd),xT),
inference(unit_resulting_resolution,[],[f593,f747,f748,f1738,f749,f2255,f599,f725]) ).
fof(f25863,plain,
sP22(sK50(xk,xY,xd),sK48(xY,sK50(xk,xY,xd),xd,xk)),
inference(unit_resulting_resolution,[],[f2280,f14968,f4320]) ).
fof(f25937,plain,
aElementOf0(sK62(sK50(xk,xY,xd),sK48(xY,sK50(xk,xY,xd),xd,xk)),slbdtsldtrb0(sK48(xY,sK50(xk,xY,xd),xd,xk),xk)),
inference(unit_resulting_resolution,[],[f751,f25863]) ).
fof(f25941,plain,
sK50(xk,xY,xd) != sdtlpdtrp0(xd,sK62(sK50(xk,xY,xd),sK48(xY,sK50(xk,xY,xd),xd,xk))),
inference(unit_resulting_resolution,[],[f756,f25863]) ).
fof(f30241,plain,
~ aElementOf0(sK62(sK50(xk,xY,xd),sK48(xY,sK50(xk,xY,xd),xd,xk)),slbdtsldtrb0(sK48(xY,sK50(xk,xY,xd),xd,xk),xk)),
inference(unit_resulting_resolution,[],[f577,f4320,f25941]) ).
fof(f30254,plain,
$false,
inference(forward_subsumption_resolution,[],[f30241,f25937]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM591+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.13/0.40 % Computer : n017.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 20:34:50 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.44 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
% 13.63/2.82 % (2921028)Detected formulas, will run a generic FOF schedule.
% 13.63/2.82 % (2921125)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2742451985:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.63/2.82 % (2921121)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=2234673056:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.63/2.82 % (2921124)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2763286779:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.63/2.82 % (2921122)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=3634664558:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.63/2.82 % (2921123)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=2213841510:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.63/2.82 % (2921125)Instruction limit reached!
% 13.63/2.82 % (2921125)------------------------------
% 13.63/2.82 % (2921125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.82 % (2921125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.82 % (2921125)CaDiCaL version: 2.1.3
% 13.63/2.82 % (2921125)Termination reason: Instruction limit
% 13.63/2.82 % (2921125)Termination phase: Saturation
% 13.63/2.82 % (2921125)Time elapsed: 0.041 s
% 13.63/2.82 % (2921125)Peak memory usage: 89 MB
% 13.63/2.82 % (2921125)Instructions burned: 121 (million)
% 13.63/2.82 % (2921127)dis-21_1_sil=8000:lcm=predicate:random_seed=3725574800: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)
% 13.63/2.82 % (2921124)Instruction limit reached!
% 13.63/2.82 % (2921124)------------------------------
% 13.63/2.82 % (2921124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.82 % (2921124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.82 % (2921124)CaDiCaL version: 2.1.3
% 13.63/2.82 % (2921124)Termination reason: Instruction limit
% 13.63/2.82 % (2921124)Termination phase: Saturation
% 13.63/2.82 % (2921124)Time elapsed: 0.069 s
% 13.63/2.82 % (2921124)Peak memory usage: 90 MB
% 13.63/2.82 % (2921124)Instructions burned: 110 (million)
% 13.63/2.82 % (2921126)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=853618555:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.63/2.82 % (2921127)Instruction limit reached!
% 13.63/2.82 % (2921127)------------------------------
% 13.63/2.82 % (2921127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.82 % (2921127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.82 % (2921127)CaDiCaL version: 2.1.3
% 13.63/2.82 % (2921127)Termination reason: Instruction limit
% 13.63/2.82 % (2921127)Termination phase: Saturation
% 13.63/2.82 % (2921127)Time elapsed: 0.066 s
% 13.63/2.82 % (2921127)Peak memory usage: 90 MB
% 13.63/2.82 % (2921127)Instructions burned: 130 (million)
% 13.63/2.82 % (2921146)lrs+10_1_sil=8000:sp=occurrence:random_seed=389701565:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 13.63/2.82 % (2921126)Instruction limit reached!
% 13.63/2.82 % (2921126)------------------------------
% 13.63/2.82 % (2921126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.82 % (2921126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.82 % (2921126)CaDiCaL version: 2.1.3
% 13.63/2.82 % (2921126)Termination reason: Instruction limit
% 13.63/2.82 % (2921126)Termination phase: Saturation
% 13.63/2.82 % (2921126)Time elapsed: 0.125 s
% 13.63/2.82 % (2921126)Peak memory usage: 90 MB
% 13.63/2.82 % (2921126)Instructions burned: 139 (million)
% 13.63/2.82 % (2921149)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3265673967:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.63/2.82 % (2921146)Instruction limit reached!
% 13.63/2.82 % (2921146)------------------------------
% 13.63/2.82 % (2921146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.82 % (2921146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.82 % (2921146)CaDiCaL version: 2.1.3
% 13.63/2.82 % (2921146)Termination reason: Instruction limit
% 13.63/2.82 % (2921146)Termination phase: Saturation
% 20.81/3.92 % (2921146)Time elapsed: 0.105 s
% 20.81/3.92 % (2921146)Peak memory usage: 92 MB
% 20.81/3.92 % (2921146)Instructions burned: 286 (million)
% 20.81/3.92 % (2921150)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2468622159:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.81/3.92 % (2921149)Instruction limit reached!
% 20.81/3.92 % (2921149)------------------------------
% 20.81/3.92 % (2921149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/3.92 % (2921149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/3.92 % (2921149)CaDiCaL version: 2.1.3
% 20.81/3.92 % (2921149)Termination reason: Instruction limit
% 20.81/3.92 % (2921149)Termination phase: Saturation
% 20.81/3.92 % (2921149)Time elapsed: 0.093 s
% 20.81/3.92 % (2921149)Peak memory usage: 91 MB
% 20.81/3.92 % (2921149)Instructions burned: 158 (million)
% 20.81/3.92 % (2921155)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2577706852:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 20.81/3.92 % (2921152)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=4058366565:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 20.81/3.92 % (2921155)Instruction limit reached!
% 20.81/3.92 % (2921155)------------------------------
% 20.81/3.92 % (2921155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/3.92 % (2921155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/3.92 % (2921155)CaDiCaL version: 2.1.3
% 20.81/3.92 % (2921155)Termination reason: Instruction limit
% 20.81/3.92 % (2921155)Termination phase: Saturation
% 20.81/3.92 % (2921155)Time elapsed: 0.094 s
% 20.81/3.92 % (2921155)Peak memory usage: 90 MB
% 20.81/3.92 % (2921155)Instructions burned: 297 (million)
% 20.81/3.92 % (2921156)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=826038510:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 20.81/3.92 % (2921150)Instruction limit reached!
% 20.81/3.92 % (2921150)------------------------------
% 20.81/3.92 % (2921150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/3.92 % (2921150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/3.92 % (2921150)CaDiCaL version: 2.1.3
% 20.81/3.92 % (2921150)Termination reason: Instruction limit
% 20.81/3.92 % (2921150)Termination phase: Saturation
% 20.81/3.92 % (2921150)Time elapsed: 0.229 s
% 20.81/3.92 % (2921150)Peak memory usage: 92 MB
% 20.81/3.92 % (2921150)Instructions burned: 326 (million)
% 20.81/3.92 % (2921152)Instruction limit reached!
% 20.81/3.92 % (2921152)------------------------------
% 20.81/3.92 % (2921152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/3.92 % (2921152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/3.92 % (2921152)CaDiCaL version: 2.1.3
% 20.81/3.92 % (2921152)Termination reason: Instruction limit
% 20.81/3.92 % (2921152)Termination phase: Saturation
% 20.81/3.92 % (2921152)Time elapsed: 0.149 s
% 20.81/3.92 % (2921152)Peak memory usage: 92 MB
% 20.81/3.92 % (2921152)Instructions burned: 249 (million)
% 20.81/3.92 % (2921159)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4211543374:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.81/3.92 % (2921159)Instruction limit reached!
% 20.81/3.92 % (2921159)------------------------------
% 20.81/3.92 % (2921159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/3.92 % (2921159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.81/3.92 % (2921159)CaDiCaL version: 2.1.3
% 20.81/3.92 % (2921159)Termination reason: Instruction limit
% 20.81/3.92 % (2921159)Termination phase: Saturation
% 20.81/3.92 % (2921159)Time elapsed: 0.067 s
% 20.81/3.92 % (2921159)Peak memory usage: 91 MB
% 20.81/3.92 % (2921159)Instructions burned: 113 (million)
% 20.81/3.92 % (2921165)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3135824599:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 20.81/3.92 % (2921161)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3634061911:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.81/3.92 % (2921165)Instruction limit reached!
% 20.81/3.92 % (2921165)------------------------------
% 20.81/3.92 % (2921165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.81/3.92 % (2921165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.49/7.45 % (2921165)CaDiCaL version: 2.1.3
% 46.49/7.45 % (2921165)Termination reason: Instruction limit
% 46.49/7.45 % (2921165)Termination phase: Saturation
% 46.49/7.45 % (2921165)Time elapsed: 0.060 s
% 46.49/7.45 % (2921165)Peak memory usage: 89 MB
% 46.49/7.45 % (2921165)Instructions burned: 115 (million)
% 46.49/7.45 % (2921161)Instruction limit reached!
% 46.49/7.45 % (2921161)------------------------------
% 46.49/7.45 % (2921161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.49/7.45 % (2921161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.49/7.45 % (2921161)CaDiCaL version: 2.1.3
% 46.49/7.45 % (2921161)Termination reason: Instruction limit
% 46.49/7.45 % (2921161)Termination phase: Saturation
% 46.49/7.45 % (2921161)Time elapsed: 0.116 s
% 46.49/7.45 % (2921161)Peak memory usage: 89 MB
% 46.49/7.45 % (2921161)Instructions burned: 127 (million)
% 46.49/7.45 % (2921176)lrs+10_1_sil=8000:sp=occurrence:random_seed=3929635010:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 46.49/7.45 % (2921182)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=700597417:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 46.49/7.45 % (2921183)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=974739669:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 46.49/7.45 % (2921182)Instruction limit reached!
% 46.49/7.45 % (2921182)------------------------------
% 46.49/7.45 % (2921182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.49/7.45 % (2921182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.49/7.45 % (2921182)CaDiCaL version: 2.1.3
% 46.49/7.45 % (2921182)Termination reason: Instruction limit
% 46.49/7.45 % (2921182)Termination phase: Saturation
% 46.49/7.45 % (2921182)Time elapsed: 0.149 s
% 46.49/7.45 % (2921182)Peak memory usage: 93 MB
% 46.49/7.45 % (2921182)Instructions burned: 439 (million)
% 46.49/7.45 % (2921187)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3308907618:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 46.49/7.45 % (2921187)Instruction limit reached!
% 46.49/7.45 % (2921187)------------------------------
% 46.49/7.45 % (2921187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.49/7.45 % (2921187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.49/7.45 % (2921187)CaDiCaL version: 2.1.3
% 46.49/7.45 % (2921187)Termination reason: Instruction limit
% 46.49/7.45 % (2921187)Termination phase: Saturation
% 46.49/7.45 % (2921187)Time elapsed: 0.044 s
% 46.49/7.45 % (2921187)Peak memory usage: 90 MB
% 46.49/7.45 % (2921187)Instructions burned: 135 (million)
% 46.49/7.45 % (2921189)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1435198437:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 46.49/7.45 % (2921176)Instruction limit reached!
% 46.49/7.45 % (2921176)------------------------------
% 46.49/7.45 % (2921176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.49/7.45 % (2921176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.49/7.45 % (2921176)CaDiCaL version: 2.1.3
% 46.49/7.45 % (2921176)Termination reason: Instruction limit
% 46.49/7.45 % (2921176)Termination phase: Saturation
% 46.49/7.45 % (2921176)Time elapsed: 0.653 s
% 46.49/7.45 % (2921176)Peak memory usage: 98 MB
% 46.49/7.45 % (2921176)Instructions burned: 907 (million)
% 46.49/7.45 % (2921189)Instruction limit reached!
% 46.49/7.45 % (2921189)------------------------------
% 46.49/7.45 % (2921189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.49/7.45 % (2921189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.49/7.45 % (2921189)CaDiCaL version: 2.1.3
% 46.49/7.45 % (2921189)Termination reason: Instruction limit
% 46.49/7.45 % (2921189)Termination phase: Saturation
% 46.49/7.45 % (2921189)Time elapsed: 0.192 s
% 46.49/7.45 % (2921189)Peak memory usage: 96 MB
% 46.49/7.45 % (2921189)Instructions burned: 592 (million)
% 46.49/7.45 % (2921233)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=1548460594:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 46.49/7.45 % (2921229)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=691127889:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 22.42/7.91 % (2921233)Instruction limit reached!
% 22.42/7.91 % (2921233)------------------------------
% 22.42/7.91 % (2921233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921233)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921233)Termination reason: Instruction limit
% 22.42/7.91 % (2921233)Termination phase: Saturation
% 22.42/7.91 % (2921233)Time elapsed: 0.048 s
% 22.42/7.91 % (2921233)Peak memory usage: 91 MB
% 22.42/7.91 % (2921233)Instructions burned: 128 (million)
% 22.42/7.91 % (2921281)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3122175072:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 22.42/7.91 % (2921281)Instruction limit reached!
% 22.42/7.91 % (2921281)------------------------------
% 22.42/7.91 % (2921281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921281)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921281)Termination reason: Instruction limit
% 22.42/7.91 % (2921281)Termination phase: Saturation
% 22.42/7.91 % (2921281)Time elapsed: 0.045 s
% 22.42/7.91 % (2921281)Peak memory usage: 91 MB
% 22.42/7.91 % (2921281)Instructions burned: 135 (million)
% 22.42/7.91 % (2921303)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3750571449:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 22.42/7.91 % (2921303)Instruction limit reached!
% 22.42/7.91 % (2921303)------------------------------
% 22.42/7.91 % (2921303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921303)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921303)Termination reason: Instruction limit
% 22.42/7.91 % (2921303)Termination phase: Saturation
% 22.42/7.91 % (2921303)Time elapsed: 0.085 s
% 22.42/7.91 % (2921303)Peak memory usage: 91 MB
% 22.42/7.91 % (2921303)Instructions burned: 141 (million)
% 22.42/7.91 % (2921156)Instruction limit reached!
% 22.42/7.91 % (2921156)------------------------------
% 22.42/7.91 % (2921156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921156)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921156)Termination reason: Instruction limit
% 22.42/7.91 % (2921156)Termination phase: Saturation
% 22.42/7.91 % (2921156)Time elapsed: 1.763 s
% 22.42/7.91 % (2921156)Peak memory usage: 143 MB
% 22.42/7.91 % (2921156)Instructions burned: 2350 (million)
% 22.42/7.91 % (2921352)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3236626008:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 22.42/7.91 % (2921353)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=3898360941:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 22.42/7.91 % (2921352)Instruction limit reached!
% 22.42/7.91 % (2921352)------------------------------
% 22.42/7.91 % (2921352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921352)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921352)Termination reason: Instruction limit
% 22.42/7.91 % (2921352)Termination phase: Saturation
% 22.42/7.91 % (2921352)Time elapsed: 0.254 s
% 22.42/7.91 % (2921352)Peak memory usage: 95 MB
% 22.42/7.91 % (2921352)Instructions burned: 432 (million)
% 22.42/7.91 % (2921356)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=1423787849:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 22.42/7.91 % (2921356)Instruction limit reached!
% 22.42/7.91 % (2921356)------------------------------
% 22.42/7.91 % (2921356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921356)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921356)Termination reason: Instruction limit
% 22.42/7.91 % (2921356)Termination phase: Saturation
% 22.42/7.91 % (2921356)Time elapsed: 0.096 s
% 22.42/7.91 % (2921356)Peak memory usage: 92 MB
% 22.42/7.91 % (2921356)Instructions burned: 151 (million)
% 22.42/7.91 % (2921358)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2617562290:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 22.42/7.91 % (2921183)Instruction limit reached!
% 22.42/7.91 % (2921183)------------------------------
% 22.42/7.91 % (2921183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921183)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921183)Termination reason: Instruction limit
% 22.42/7.91 % (2921183)Termination phase: Saturation
% 22.42/7.91 % (2921183)Time elapsed: 2.338 s
% 22.42/7.91 % (2921183)Peak memory usage: 161 MB
% 22.42/7.91 % (2921183)Instructions burned: 5204 (million)
% 22.42/7.91 % (2921360)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1931545714:i=667:av=off:fsr=off_2963 on theBenchmark for (2963ds/667Mi)
% 22.42/7.91 % (2921360)Instruction limit reached!
% 22.42/7.91 % (2921360)------------------------------
% 22.42/7.91 % (2921360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921360)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921360)Termination reason: Instruction limit
% 22.42/7.91 % (2921360)Termination phase: Saturation
% 22.42/7.91 % (2921360)Time elapsed: 0.180 s
% 22.42/7.91 % (2921360)Peak memory usage: 99 MB
% 22.42/7.91 % (2921360)Instructions burned: 671 (million)
% 22.42/7.91 % (2921362)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=742972234:s2a=on:i=185:s2at=1.8:fdi=4_2960 on theBenchmark for (2960ds/185Mi)
% 22.42/7.91 % (2921362)Instruction limit reached!
% 22.42/7.91 % (2921362)------------------------------
% 22.42/7.91 % (2921362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921362)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921362)Termination reason: Instruction limit
% 22.42/7.91 % (2921362)Termination phase: Saturation
% 22.42/7.91 % (2921362)Time elapsed: 0.062 s
% 22.42/7.91 % (2921362)Peak memory usage: 91 MB
% 22.42/7.91 % (2921362)Instructions burned: 186 (million)
% 22.42/7.91 % (2921364)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2398313835:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2958 on theBenchmark for (2958ds/193Mi)
% 22.42/7.91 % (2921364)Instruction limit reached!
% 22.42/7.91 % (2921364)------------------------------
% 22.42/7.91 % (2921364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921364)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921364)Termination reason: Instruction limit
% 22.42/7.91 % (2921364)Termination phase: Saturation
% 22.42/7.91 % (2921364)Time elapsed: 0.066 s
% 22.42/7.91 % (2921364)Peak memory usage: 93 MB
% 22.42/7.91 % (2921364)Instructions burned: 195 (million)
% 22.42/7.91 % (2921366)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1865276981:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2956 on theBenchmark for (2956ds/4850Mi)
% 22.42/7.91 % (2921366)Instruction limit reached!
% 22.42/7.91 % (2921366)------------------------------
% 22.42/7.91 % (2921366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921366)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921366)Termination reason: Instruction limit
% 22.42/7.91 % (2921366)Termination phase: Saturation
% 22.42/7.91 % (2921366)Time elapsed: 1.475 s
% 22.42/7.91 % (2921366)Peak memory usage: 116 MB
% 22.42/7.91 % (2921366)Instructions burned: 4851 (million)
% 22.42/7.91 % (2921368)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3605742149:i=12111:sd=1:ss=included_2940 on theBenchmark for (2940ds/12111Mi)
% 22.42/7.91 % (2921353)Instruction limit reached!
% 22.42/7.91 % (2921353)------------------------------
% 22.42/7.91 % (2921353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921353)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921353)Termination reason: Instruction limit
% 22.42/7.91 % (2921353)Termination phase: Saturation
% 22.42/7.91 % (2921353)Time elapsed: 4.005 s
% 22.42/7.91 % (2921353)Peak memory usage: 166 MB
% 22.42/7.91 % (2921353)Instructions burned: 6061 (million)
% 22.42/7.91 % (2921358)First to succeed.
% 22.42/7.91 % (2921358)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2921028"
% 22.42/7.91 % (2921370)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2699110910:i=319:kws=precedence:fsr=off_2934 on theBenchmark for (2934ds/319Mi)
% 22.42/7.91 % (2921370)Instruction limit reached!
% 22.42/7.91 % (2921370)------------------------------
% 22.42/7.91 % (2921370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/7.91 % (2921370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/7.91 % (2921370)CaDiCaL version: 2.1.3
% 22.42/7.91 % (2921370)Termination reason: Instruction limit
% 22.42/7.91 % (2921370)Termination phase: Saturation
% 22.42/7.91 % (2921370)Time elapsed: 0.197 s
% 22.42/7.91 % (2921370)Peak memory usage: 92 MB
% 22.42/7.91 % (2921370)Instructions burned: 319 (million)
% 22.42/7.91 % (2921358)Refutation found. Thanks to Tanya!
% 22.42/7.91 % SZS status Theorem for theBenchmark
% 22.42/7.91 % SZS output start Proof for theBenchmark
% See solution above
% 50.19/8.06 % (2921358)------------------------------
% 50.19/8.06 % (2921358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.19/8.06 % (2921358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.19/8.06 % (2921358)CaDiCaL version: 2.1.3
% 50.19/8.06 % (2921358)Termination reason: Refutation
% 50.19/8.06 % (2921358)Time elapsed: 3.529 s
% 50.19/8.06 % (2921358)Peak memory usage: 164 MB
% 50.19/8.06 % (2921358)Instructions burned: 5389 (million)
% 50.19/8.06 % (2921358)------------------------------
% 50.19/8.06 % (2921358)------------------------------
% 50.19/8.06 % (2921028)Success in time 7.017 s
% 50.19/8.06 % Vampire exiting
%------------------------------------------------------------------------------