%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM577+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:24:53 PM UTC 2026
% Result : Theorem 162.24s 41.24s
% Output : Refutation 162.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 30
% Syntax : Number of formulae : 200 ( 26 unt; 15 def)
% Number of atoms : 719 ( 85 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 887 ( 368 ~; 358 |; 114 &)
% ( 29 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 14 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-3 aty)
% Number of variables : 190 ( 0 sgn 177 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f5,axiom,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ~ ? [X1] : aElementOf0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefEmp) ).
fof(f6,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEmpFin) ).
fof(f8,axiom,
! [X0] :
( ( aSet0(X0)
& isCountable0(X0) )
=> ~ isFinite0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin) ).
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aSet0(X0)
& aSet0(X1)
& aSet0(X2) )
=> ( ( aSubsetOf0(X0,X1)
& aSubsetOf0(X1,X2) )
=> aSubsetOf0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubTrans) ).
fof(f16,axiom,
! [X0,X1] :
( ( aSet0(X0)
& aElement0(X1) )
=> ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
fof(f23,axiom,
( aSet0(szNzAzT0)
& isCountable0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNATSet) ).
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(f47,axiom,
! [X0] :
( ( aSubsetOf0(X0,szNzAzT0)
& X0 != slcrc0 )
=> ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( aElementOf0(X2,X0)
=> sdtlseqdt0(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefMin) ).
fof(f81,axiom,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
=> ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3623) ).
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3671) ).
fof(f83,axiom,
! [X0,X1] :
( ( aElementOf0(X0,szNzAzT0)
& aElementOf0(X1,szNzAzT0) )
=> ( sdtlseqdt0(X1,X0)
=> aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3754) ).
fof(f86,axiom,
( aElementOf0(xn,szNzAzT0)
& aElementOf0(xm,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3904) ).
fof(f87,conjecture,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
=> ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& szmzizndt0(sdtlpdtrp0(xN,xm)) != szmzizndt0(sdtlpdtrp0(xN,xn)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f88,negated_conjecture,
~ ( sdtlseqdt0(szszuzczcdt0(xn),xm)
=> ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& szmzizndt0(sdtlpdtrp0(xN,xm)) != szmzizndt0(sdtlpdtrp0(xN,xn)) ) ),
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f96,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f97,plain,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f98,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f99,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(flattening,[],[f98]) ).
fof(f102,plain,
! [X0] :
( ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) ) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f108,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f109,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(flattening,[],[f108]) ).
fof(f112,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f113,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f112]) ).
fof(f125,plain,
! [X0] :
( ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f155,plain,
! [X0] :
( ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(ennf_transformation,[],[f47]) ).
fof(f156,plain,
! [X0] :
( ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(flattening,[],[f155]) ).
fof(f197,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f81]) ).
fof(f198,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(flattening,[],[f197]) ).
fof(f199,plain,
! [X0] :
( ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f200,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f201,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f200]) ).
fof(f204,plain,
( ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)) )
& sdtlseqdt0(szszuzczcdt0(xn),xm) ),
inference(ennf_transformation,[],[f88]) ).
fof(f208,definition,
! [X2,X0,X1] :
( sP2(X2,X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f209,definition,
! [X1,X0] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> sP2(X2,X0,X1) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f210,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f113,f209,f208]) ).
fof(f211,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) )
| slcrc0 != X0 ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f212,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) )
| slcrc0 != X0 ) ),
inference(flattening,[],[f211]) ).
fof(f213,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X2] : ~ aElementOf0(X2,X0) )
| slcrc0 != X0 ) ),
inference(rectify,[],[f212]) ).
fof(f214,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| aElementOf0(sK4(X0),X0) )
& ( ( aSet0(X0)
& ! [X2] : ~ aElementOf0(X2,X0) )
| slcrc0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f213]) ).
fof(f215,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,X0)
& aElementOf0(X2,X1) ) )
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(nnf_transformation,[],[f102]) ).
fof(f216,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,X0)
& aElementOf0(X2,X1) ) )
& ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(flattening,[],[f215]) ).
fof(f217,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,X0)
& aElementOf0(X2,X1) ) )
& ( ( aSet0(X1)
& ! [X3] :
( aElementOf0(X3,X0)
| ~ aElementOf0(X3,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(rectify,[],[f216]) ).
fof(f218,plain,
! [X0] :
( ! [X1] :
( ( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ( ~ aElementOf0(sK5(X0,X1),X0)
& aElementOf0(sK5(X0,X1),X1) ) )
& ( ( aSet0(X1)
& ! [X3] :
( aElementOf0(X3,X0)
| ~ aElementOf0(X3,X1) ) )
| ~ aSubsetOf0(X1,X0) ) )
| ~ aSet0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f217]) ).
fof(f225,plain,
! [X1,X0] :
( ! [X2] :
( ( X2 = sdtmndt0(X0,X1)
| ~ sP2(X2,X0,X1) )
& ( sP2(X2,X0,X1)
| sdtmndt0(X0,X1) != X2 ) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f209]) ).
fof(f226,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtmndt0(X1,X0) = X2
| ~ sP2(X2,X1,X0) )
& ( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2 ) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f225]) ).
fof(f227,plain,
! [X2,X0,X1] :
( ( sP2(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP2(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f208]) ).
fof(f228,plain,
! [X2,X0,X1] :
( ( sP2(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP2(X2,X0,X1) ) ),
inference(flattening,[],[f227]) ).
fof(f229,plain,
! [X0,X1,X2] :
( ( sP2(X0,X1,X2)
| ~ aSet0(X0)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X1)
| X2 = X3
| ~ aElementOf0(X3,X0) )
& ( ( aElement0(X3)
& aElementOf0(X3,X1)
& X2 != X3 )
| aElementOf0(X3,X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ~ aElementOf0(X4,X1)
| X2 = X4 )
& ( ( aElement0(X4)
& aElementOf0(X4,X1)
& X2 != X4 )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP2(X0,X1,X2) ) ),
inference(rectify,[],[f228]) ).
fof(f230,plain,
! [X0,X1,X2] :
( ( sP2(X0,X1,X2)
| ~ aSet0(X0)
| ( ( ~ aElement0(sK7(X0,X1,X2))
| ~ aElementOf0(sK7(X0,X1,X2),X1)
| sK7(X0,X1,X2) = X2
| ~ aElementOf0(sK7(X0,X1,X2),X0) )
& ( ( aElement0(sK7(X0,X1,X2))
& aElementOf0(sK7(X0,X1,X2),X1)
& sK7(X0,X1,X2) != X2 )
| aElementOf0(sK7(X0,X1,X2),X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ~ aElementOf0(X4,X1)
| X2 = X4 )
& ( ( aElement0(X4)
& aElementOf0(X4,X1)
& X2 != X4 )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP2(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f229]) ).
fof(f236,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(nnf_transformation,[],[f156]) ).
fof(f237,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(flattening,[],[f236]) ).
fof(f238,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ? [X2] :
( ~ sdtlseqdt0(X1,X2)
& aElementOf0(X2,X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X3] :
( sdtlseqdt0(X1,X3)
| ~ aElementOf0(X3,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(rectify,[],[f237]) ).
fof(f239,plain,
! [X0] :
( ! [X1] :
( ( X1 = szmzizndt0(X0)
| ~ aElementOf0(X1,X0)
| ( ~ sdtlseqdt0(X1,sK10(X0,X1))
& aElementOf0(sK10(X0,X1),X0) ) )
& ( ( aElementOf0(X1,X0)
& ! [X3] :
( sdtlseqdt0(X1,X3)
| ~ aElementOf0(X3,X0) ) )
| szmzizndt0(X0) != X1 ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f238]) ).
fof(f271,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f96]) ).
fof(f273,plain,
! [X0] :
( aSet0(X0)
| slcrc0 != X0 ),
inference(cnf_transformation,[],[f214]) ).
fof(f275,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[],[f6]) ).
fof(f276,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f278,plain,
! [X3,X0,X1] :
( ~ aSubsetOf0(X1,X0)
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f218]) ).
fof(f279,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,X0)
| aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f218]) ).
fof(f285,plain,
! [X2,X0,X1] :
( ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| aSubsetOf0(X0,X2)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f298,plain,
! [X2,X0,X1] :
( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f226]) ).
fof(f300,plain,
! [X2,X0,X1,X4] :
( X2 != X4
| ~ aElementOf0(X4,X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f230]) ).
fof(f304,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f309,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f210]) ).
fof(f317,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f320,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f346,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| szmzizndt0(X0) != X1
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(cnf_transformation,[],[f239]) ).
fof(f431,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f198]) ).
fof(f435,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f436,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f437,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f441,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f86]) ).
fof(f442,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f86]) ).
fof(f443,plain,
sdtlseqdt0(szszuzczcdt0(xn),xm),
inference(cnf_transformation,[],[f204]) ).
fof(f444,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)) ),
inference(cnf_transformation,[],[f204]) ).
fof(f445,plain,
aSet0(slcrc0),
inference(equality_resolution,[],[f273]) ).
fof(f450,plain,
! [X0,X1] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ sP3(X0,X1) ),
inference(equality_resolution,[],[f298]) ).
fof(f451,plain,
! [X0,X1,X4] :
( ~ sP2(X0,X1,X4)
| ~ aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f300]) ).
fof(f453,plain,
! [X0] :
( aElementOf0(szmzizndt0(X0),X0)
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(equality_resolution,[],[f346]) ).
fof(f484,definition,
( spl25_1
<=> szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)) ),
introduced(definition,[new_symbols(definition,[spl25_1])],[avatar_definition]) ).
fof(f486,plain,
( szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm))
| ~ spl25_1 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f488,definition,
( spl25_2
<=> aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition]) ).
fof(f489,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ spl25_2 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f490,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| spl25_2 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f491,plain,
( spl25_1
| ~ spl25_2 ),
inference(avatar_split_clause,[],[f444,f488,f484]) ).
fof(f506,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f431,f436]) ).
fof(f508,definition,
( spl25_6
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition]) ).
fof(f509,plain,
( aSet0(slcrc0)
| ~ spl25_6 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f521,plain,
spl25_6,
inference(avatar_split_clause,[],[f445,f508]) ).
fof(f523,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f506,f435]) ).
fof(f574,plain,
! [X0] :
( ~ isFinite0(sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f435,f276]) ).
fof(f709,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtmndt0(X1,X0))
| ~ sP3(X0,X1) ),
inference(resolution,[],[f450,f451]) ).
fof(f710,plain,
! [X0,X1] :
( aSet0(sdtmndt0(X1,X0))
| ~ sP3(X0,X1) ),
inference(resolution,[],[f450,f304]) ).
fof(f745,plain,
! [X0] :
( ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0
| aElement0(szmzizndt0(X0))
| ~ aSet0(X0) ),
inference(resolution,[],[f453,f271]) ).
fof(f1413,plain,
! [X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSet0(X1)
| ~ aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(resolution,[],[f523,f285]) ).
fof(f1417,plain,
! [X0] :
( ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f523,f279]) ).
fof(f1426,plain,
! [X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aSubsetOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(forward_subsumption_resolution,[],[f1413,f279]) ).
fof(f3034,plain,
! [X0,X1] :
( aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSubsetOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(forward_subsumption_resolution,[],[f1426,f1417]) ).
fof(f4090,definition,
( spl25_136
<=> aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl25_136])],[avatar_definition]) ).
fof(f4091,plain,
( aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ spl25_136 ),
inference(avatar_component_clause,[],[f4090]) ).
fof(f4092,plain,
( ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| spl25_136 ),
inference(avatar_component_clause,[],[f4090]) ).
fof(f4128,plain,
( ~ aElementOf0(xn,szNzAzT0)
| spl25_136 ),
inference(resolution,[],[f4092,f320]) ).
fof(f4132,plain,
( $false
| spl25_136 ),
inference(forward_subsumption_resolution,[],[f4128,f442]) ).
fof(f4133,plain,
spl25_136,
inference(avatar_contradiction_clause,[],[f4132]) ).
fof(f8723,definition,
( spl25_316
<=> slcrc0 = sdtlpdtrp0(xN,xm) ),
introduced(definition,[new_symbols(definition,[spl25_316])],[avatar_definition]) ).
fof(f8725,plain,
( slcrc0 = sdtlpdtrp0(xN,xm)
| ~ spl25_316 ),
inference(avatar_component_clause,[],[f8723]) ).
fof(f8727,definition,
( spl25_317
<=> aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl25_317])],[avatar_definition]) ).
fof(f8728,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)
| ~ spl25_317 ),
inference(avatar_component_clause,[],[f8727]) ).
fof(f8729,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)
| spl25_317 ),
inference(avatar_component_clause,[],[f8727]) ).
fof(f8754,plain,
( ~ aElementOf0(xm,szNzAzT0)
| spl25_317 ),
inference(resolution,[],[f8729,f436]) ).
fof(f8755,plain,
( $false
| spl25_317 ),
inference(forward_subsumption_resolution,[],[f8754,f441]) ).
fof(f8756,plain,
spl25_317,
inference(avatar_contradiction_clause,[],[f8755]) ).
fof(f8765,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)
| slcrc0 = sdtlpdtrp0(xN,xm)
| ~ spl25_1 ),
inference(superposition,[],[f453,f486]) ).
fof(f8766,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm))
| slcrc0 = sdtlpdtrp0(xN,xm)
| ~ spl25_1
| ~ spl25_317 ),
inference(forward_subsumption_resolution,[],[f8765,f8728]) ).
fof(f8772,definition,
( spl25_323
<=> aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm)) ),
introduced(definition,[new_symbols(definition,[spl25_323])],[avatar_definition]) ).
fof(f8774,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm))
| ~ spl25_323 ),
inference(avatar_component_clause,[],[f8772]) ).
fof(f8775,plain,
( spl25_316
| spl25_323
| ~ spl25_1
| ~ spl25_317 ),
inference(avatar_split_clause,[],[f8766,f8727,f484,f8772,f8723]) ).
fof(f8808,definition,
( spl25_327
<=> aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
introduced(definition,[new_symbols(definition,[spl25_327])],[avatar_definition]) ).
fof(f8809,plain,
( aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ spl25_327 ),
inference(avatar_component_clause,[],[f8808]) ).
fof(f8810,plain,
( ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| spl25_327 ),
inference(avatar_component_clause,[],[f8808]) ).
fof(f8831,plain,
( ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ spl25_316 ),
inference(superposition,[],[f574,f8725]) ).
fof(f8852,plain,
( ~ aSet0(slcrc0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ spl25_316 ),
inference(forward_subsumption_resolution,[],[f8831,f275]) ).
fof(f8867,plain,
( ~ aElementOf0(xm,szNzAzT0)
| ~ spl25_6
| ~ spl25_316 ),
inference(forward_subsumption_resolution,[],[f8852,f509]) ).
fof(f8871,plain,
( $false
| ~ spl25_6
| ~ spl25_316 ),
inference(forward_subsumption_resolution,[],[f8867,f441]) ).
fof(f8872,plain,
( ~ spl25_6
| ~ spl25_316 ),
inference(avatar_contradiction_clause,[],[f8871]) ).
fof(f8971,plain,
( ~ sP3(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| spl25_327 ),
inference(resolution,[],[f8810,f710]) ).
fof(f10360,definition,
( spl25_369
<=> aElement0(szmzizndt0(sdtlpdtrp0(xN,xn))) ),
introduced(definition,[new_symbols(definition,[spl25_369])],[avatar_definition]) ).
fof(f10362,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| spl25_369 ),
inference(avatar_component_clause,[],[f10360]) ).
fof(f10392,definition,
( spl25_375
<=> slcrc0 = sdtlpdtrp0(xN,xn) ),
introduced(definition,[new_symbols(definition,[spl25_375])],[avatar_definition]) ).
fof(f10393,plain,
( slcrc0 != sdtlpdtrp0(xN,xn)
| spl25_375 ),
inference(avatar_component_clause,[],[f10392]) ).
fof(f10394,plain,
( slcrc0 = sdtlpdtrp0(xN,xn)
| ~ spl25_375 ),
inference(avatar_component_clause,[],[f10392]) ).
fof(f10396,definition,
( spl25_376
<=> aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl25_376])],[avatar_definition]) ).
fof(f10397,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| ~ spl25_376 ),
inference(avatar_component_clause,[],[f10396]) ).
fof(f10398,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| spl25_376 ),
inference(avatar_component_clause,[],[f10396]) ).
fof(f40312,plain,
( ~ aSet0(sdtlpdtrp0(xN,xn))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| spl25_327 ),
inference(resolution,[],[f8971,f309]) ).
fof(f41866,plain,
( ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xm))
| aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
| ~ spl25_2 ),
inference(resolution,[],[f489,f278]) ).
fof(f41869,plain,
( ! [X0] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xm)) )
| ~ spl25_2
| ~ spl25_327 ),
inference(forward_subsumption_resolution,[],[f41866,f8809]) ).
fof(f41928,plain,
( ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm))
| ~ sP3(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| ~ spl25_2
| ~ spl25_327 ),
inference(resolution,[],[f41869,f709]) ).
fof(f42018,definition,
( spl25_819
<=> sP3(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) ),
introduced(definition,[new_symbols(definition,[spl25_819])],[avatar_definition]) ).
fof(f42020,plain,
( ~ sP3(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| spl25_819 ),
inference(avatar_component_clause,[],[f42018]) ).
fof(f42025,plain,
( ~ sP3(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| ~ spl25_2
| ~ spl25_323
| ~ spl25_327 ),
inference(forward_subsumption_resolution,[],[f41928,f8774]) ).
fof(f42030,plain,
( ~ spl25_819
| ~ spl25_2
| ~ spl25_323
| ~ spl25_327 ),
inference(avatar_split_clause,[],[f42025,f8808,f8772,f488,f42018]) ).
fof(f42169,plain,
( aSet0(sdtlpdtrp0(xN,xn))
| ~ aSet0(szNzAzT0)
| ~ spl25_376 ),
inference(resolution,[],[f10397,f279]) ).
fof(f42170,plain,
( aSet0(sdtlpdtrp0(xN,xn))
| ~ spl25_376 ),
inference(forward_subsumption_resolution,[],[f42169,f317]) ).
fof(f42175,definition,
( spl25_823
<=> aSet0(sdtlpdtrp0(xN,xn)) ),
introduced(definition,[new_symbols(definition,[spl25_823])],[avatar_definition]) ).
fof(f42177,plain,
( aSet0(sdtlpdtrp0(xN,xn))
| ~ spl25_823 ),
inference(avatar_component_clause,[],[f42175]) ).
fof(f42216,plain,
( spl25_823
| ~ spl25_376 ),
inference(avatar_split_clause,[],[f42170,f10396,f42175]) ).
fof(f42270,plain,
( ~ aElementOf0(xn,szNzAzT0)
| spl25_376 ),
inference(resolution,[],[f10398,f436]) ).
fof(f42278,plain,
( $false
| spl25_376 ),
inference(forward_subsumption_resolution,[],[f42270,f442]) ).
fof(f42279,plain,
spl25_376,
inference(avatar_contradiction_clause,[],[f42278]) ).
fof(f42297,plain,
( slcrc0 = sdtlpdtrp0(xN,xn)
| aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| ~ aSet0(sdtlpdtrp0(xN,xn))
| ~ spl25_376 ),
inference(resolution,[],[f10397,f745]) ).
fof(f43135,plain,
( ~ aSet0(sdtlpdtrp0(xN,xn))
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| spl25_819 ),
inference(resolution,[],[f42020,f309]) ).
fof(f43136,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| spl25_819
| ~ spl25_823 ),
inference(forward_subsumption_resolution,[],[f43135,f42177]) ).
fof(f43141,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| spl25_327
| ~ spl25_823 ),
inference(forward_subsumption_resolution,[],[f40312,f42177]) ).
fof(f50943,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(xn,szNzAzT0)
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| spl25_2 ),
inference(resolution,[],[f490,f3034]) ).
fof(f50952,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| spl25_2 ),
inference(forward_subsumption_resolution,[],[f50943,f442]) ).
fof(f50956,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| spl25_2
| ~ spl25_327 ),
inference(forward_subsumption_resolution,[],[f50952,f8809]) ).
fof(f51529,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| spl25_2
| ~ spl25_327 ),
inference(resolution,[],[f50956,f437]) ).
fof(f51538,plain,
( ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| spl25_2
| ~ spl25_327 ),
inference(forward_subsumption_resolution,[],[f51529,f443]) ).
fof(f51542,plain,
( ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| spl25_2
| ~ spl25_327 ),
inference(forward_subsumption_resolution,[],[f51538,f441]) ).
fof(f51544,plain,
( $false
| spl25_2
| ~ spl25_136
| ~ spl25_327 ),
inference(forward_subsumption_resolution,[],[f51542,f4091]) ).
fof(f51545,plain,
( spl25_2
| ~ spl25_136
| ~ spl25_327 ),
inference(avatar_contradiction_clause,[],[f51544]) ).
fof(f51554,plain,
( aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| ~ aSet0(sdtlpdtrp0(xN,xn))
| spl25_375
| ~ spl25_376 ),
inference(forward_subsumption_resolution,[],[f42297,f10393]) ).
fof(f51598,plain,
( aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| spl25_375
| ~ spl25_376
| ~ spl25_823 ),
inference(forward_subsumption_resolution,[],[f51554,f42177]) ).
fof(f51653,plain,
( ~ spl25_369
| spl25_819
| ~ spl25_823 ),
inference(avatar_split_clause,[],[f43136,f42175,f42018,f10360]) ).
fof(f51737,plain,
( ~ spl25_369
| spl25_327
| ~ spl25_823 ),
inference(avatar_split_clause,[],[f43141,f42175,f8808,f10360]) ).
fof(f51744,plain,
( $false
| spl25_369
| spl25_375
| ~ spl25_376
| ~ spl25_823 ),
inference(forward_subsumption_resolution,[],[f51598,f10362]) ).
fof(f51745,plain,
( spl25_369
| spl25_375
| ~ spl25_376
| ~ spl25_823 ),
inference(avatar_contradiction_clause,[],[f51744]) ).
fof(f52264,plain,
( ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0)
| ~ aElementOf0(xn,szNzAzT0)
| ~ spl25_375 ),
inference(superposition,[],[f574,f10394]) ).
fof(f52304,plain,
( ~ aSet0(slcrc0)
| ~ aElementOf0(xn,szNzAzT0)
| ~ spl25_375 ),
inference(forward_subsumption_resolution,[],[f52264,f275]) ).
fof(f52322,plain,
( ~ aElementOf0(xn,szNzAzT0)
| ~ spl25_6
| ~ spl25_375 ),
inference(forward_subsumption_resolution,[],[f52304,f509]) ).
fof(f52339,plain,
( $false
| ~ spl25_6
| ~ spl25_375 ),
inference(forward_subsumption_resolution,[],[f52322,f442]) ).
fof(f52340,plain,
( ~ spl25_6
| ~ spl25_375 ),
inference(avatar_contradiction_clause,[],[f52339]) ).
cnf(s3,plain,
( spl25_1
| ~ spl25_2 ),
inference(sat_conversion,[],[f491]) ).
cnf(s174,plain,
spl25_6,
inference(sat_conversion,[],[f521]) ).
cnf(s1333,plain,
spl25_136,
inference(sat_conversion,[],[f4133]) ).
cnf(s3013,plain,
spl25_317,
inference(sat_conversion,[],[f8756]) ).
cnf(s3025,plain,
( ~ spl25_1
| spl25_316
| ~ spl25_317
| spl25_323 ),
inference(sat_conversion,[],[f8775]) ).
cnf(s3053,plain,
( ~ spl25_6
| ~ spl25_316 ),
inference(sat_conversion,[],[f8872]) ).
cnf(s17030,plain,
( ~ spl25_2
| ~ spl25_323
| ~ spl25_327
| ~ spl25_819 ),
inference(sat_conversion,[],[f42030]) ).
cnf(s17077,plain,
( ~ spl25_376
| spl25_823 ),
inference(sat_conversion,[],[f42216]) ).
cnf(s17110,plain,
spl25_376,
inference(sat_conversion,[],[f42279]) ).
cnf(s19973,plain,
( spl25_2
| ~ spl25_136
| ~ spl25_327 ),
inference(sat_conversion,[],[f51545]) ).
cnf(s19990,plain,
( ~ spl25_369
| spl25_819
| ~ spl25_823 ),
inference(sat_conversion,[],[f51653]) ).
cnf(s20105,plain,
( spl25_327
| ~ spl25_369
| ~ spl25_823 ),
inference(sat_conversion,[],[f51737]) ).
cnf(s20112,plain,
( spl25_369
| spl25_375
| ~ spl25_376
| ~ spl25_823 ),
inference(sat_conversion,[],[f51745]) ).
cnf(s20183,plain,
( ~ spl25_6
| ~ spl25_375 ),
inference(sat_conversion,[],[f52340]) ).
cnf(s20197,plain,
spl25_823,
inference(rat,[],[s17077,s17110]) ).
cnf(s20264,plain,
~ spl25_375,
inference(rat,[],[s20183,s174]) ).
cnf(s20265,plain,
~ spl25_316,
inference(rat,[],[s3053,s174]) ).
cnf(s20267,plain,
spl25_369,
inference(rat,[],[s20112,s20197,s17110,s20264]) ).
cnf(s20268,plain,
spl25_327,
inference(rat,[],[s20105,s20197,s20267]) ).
cnf(s20269,plain,
spl25_819,
inference(rat,[],[s19990,s20197,s20267]) ).
cnf(s20271,plain,
spl25_2,
inference(rat,[],[s19973,s1333,s20268]) ).
cnf(s20272,plain,
~ spl25_323,
inference(rat,[],[s17030,s20269,s20268,s20271]) ).
cnf(s20274,plain,
~ spl25_1,
inference(rat,[],[s3025,s20265,s3013,s20272]) ).
cnf(s20289,plain,
$false,
inference(rat,[],[s3,s20271,s20274]) ).
fof(f52356,plain,
$false,
inference(avatar_sat_refutation,[],[s20289]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM577+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n003.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:36:41 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.21/4.44 % (900179)Will run a generic schedule for satisfiability detection.
% 28.21/4.44 % (900188)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2554547278:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 28.21/4.44 % (900185)% WARNING: option uhcvi not known.
% 28.21/4.44 % (900184)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3651768479_2999 on theBenchmark for (2999ds/0Mi)
% 28.21/4.44 % (900185)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2616690071:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 28.21/4.44 % (900186)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2249080870:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 28.21/4.44 % (900187)dis+10_1_sil=32000:sp=arity:random_seed=1623887621:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 28.21/4.44 % (900190)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=146464300:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 28.21/4.44 % (900189)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2162615268:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 28.21/4.44 % TRYING [1]
% 28.21/4.44 % TRYING [2]
% 28.21/4.44 % TRYING [3]
% 28.21/4.44 % (900188)Instruction limit reached!
% 28.21/4.44 % (900188)------------------------------
% 28.21/4.44 % (900188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.44 % (900188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.44 % (900188)CaDiCaL version: 2.1.3
% 28.21/4.44 % (900188)Termination reason: Instruction limit
% 28.21/4.44 % (900188)Termination phase: Saturation
% 28.21/4.44 % (900188)Time elapsed: 0.043 s
% 28.21/4.44 % (900188)Peak memory usage: 13 MB
% 28.21/4.44 % (900188)Instructions burned: 118 (million)
% 28.21/4.44 % TRYING [4]
% 28.21/4.44 % (900198)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2511170348:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 28.21/4.44 % TRYING [1]
% 28.21/4.44 % TRYING [2]
% 28.21/4.44 % TRYING [3]
% 28.21/4.44 % (900187)Instruction limit reached!
% 28.21/4.44 % (900187)------------------------------
% 28.21/4.44 % (900187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.44 % (900187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.44 % (900187)CaDiCaL version: 2.1.3
% 28.21/4.44 % (900187)Termination reason: Instruction limit
% 28.21/4.44 % (900187)Termination phase: Saturation
% 28.21/4.44 % (900187)Time elapsed: 0.069 s
% 28.21/4.44 % (900187)Peak memory usage: 13 MB
% 28.21/4.44 % (900187)Instructions burned: 104 (million)
% 28.21/4.44 % TRYING [4]
% 28.21/4.44 % (900189)Instruction limit reached!
% 28.21/4.44 % (900189)------------------------------
% 28.21/4.44 % (900189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.44 % (900189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.44 % (900189)CaDiCaL version: 2.1.3
% 28.21/4.44 % (900189)Termination reason: Instruction limit
% 28.21/4.44 % (900189)Termination phase: Saturation
% 28.21/4.44 % (900189)Time elapsed: 0.084 s
% 28.21/4.44 % (900189)Peak memory usage: 13 MB
% 28.21/4.44 % (900189)Instructions burned: 132 (million)
% 28.21/4.44 % (900200)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1134977810:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.21/4.44 % (900190)Instruction limit reached!
% 28.21/4.44 % (900190)------------------------------
% 28.21/4.44 % (900190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.44 % (900190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.44 % (900190)CaDiCaL version: 2.1.3
% 28.21/4.44 % (900190)Termination reason: Instruction limit
% 28.21/4.44 % (900190)Termination phase: Saturation
% 28.21/4.44 % (900190)Time elapsed: 0.099 s
% 28.21/4.44 % (900190)Peak memory usage: 15 MB
% 28.21/4.44 % (900190)Instructions burned: 160 (million)
% 28.21/4.44 % TRYING [5]
% 28.21/4.44 % TRYING [5]
% 28.21/4.44 % (900201)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1060512117:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.21/4.44 % (900203)ott-21_1_sil=16000:fs=off:random_seed=4146801257:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 28.21/4.44 % (900200)Instruction limit reached!
% 28.21/4.44 % (900200)------------------------------
% 28.21/4.44 % (900200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.44 % (900200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.78/7.30 % (900200)CaDiCaL version: 2.1.3
% 48.78/7.30 % (900200)Termination reason: Instruction limit
% 48.78/7.30 % (900200)Termination phase: Saturation
% 48.78/7.30 % (900200)Time elapsed: 0.087 s
% 48.78/7.30 % (900200)Peak memory usage: 13 MB
% 48.78/7.30 % (900200)Instructions burned: 132 (million)
% 48.78/7.30 % TRYING [6]
% 48.78/7.30 % (900206)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3000220676:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 48.78/7.30 % (900198)Instruction limit reached!
% 48.78/7.30 % (900198)------------------------------
% 48.78/7.30 % (900198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.78/7.30 % (900198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.78/7.30 % (900198)CaDiCaL version: 2.1.3
% 48.78/7.30 % (900198)Termination reason: Instruction limit
% 48.78/7.30 % (900198)Termination phase: Finite model building constraint generation
% 48.78/7.30 % (900198)Time elapsed: 0.154 s
% 48.78/7.30 % (900198)Peak memory usage: 31 MB
% 48.78/7.30 % (900198)Instructions burned: 718 (million)
% 48.78/7.30 % (900208)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1652365805:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 48.78/7.30 % TRYING [1]
% 48.78/7.30 % TRYING [2]
% 48.78/7.30 % (900203)Instruction limit reached!
% 48.78/7.30 % (900203)------------------------------
% 48.78/7.30 % (900203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.78/7.30 % (900203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.78/7.30 % (900203)CaDiCaL version: 2.1.3
% 48.78/7.30 % (900203)Termination reason: Instruction limit
% 48.78/7.30 % (900203)Termination phase: Saturation
% 48.78/7.30 % (900203)Time elapsed: 0.103 s
% 48.78/7.30 % (900203)Peak memory usage: 13 MB
% 48.78/7.30 % (900203)Instructions burned: 181 (million)
% 48.78/7.30 % TRYING [3]
% 48.78/7.30 % (900210)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1614399266:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 48.78/7.30 % TRYING [6]
% 48.78/7.30 % TRYING [4]
% 48.78/7.30 % TRYING [5]
% 48.78/7.30 % (900208)Instruction limit reached!
% 48.78/7.30 % (900208)------------------------------
% 48.78/7.30 % (900208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.78/7.30 % (900208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.78/7.30 % (900208)CaDiCaL version: 2.1.3
% 48.78/7.30 % (900208)Termination reason: Instruction limit
% 48.78/7.30 % (900208)Termination phase: Finite model building constraint generation
% 48.78/7.30 % (900208)Time elapsed: 0.187 s
% 48.78/7.30 % (900208)Peak memory usage: 21 MB
% 48.78/7.30 % (900208)Instructions burned: 867 (million)
% 48.78/7.30 % (900212)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2494186879:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 48.78/7.30 % (900201)Instruction limit reached!
% 48.78/7.30 % (900201)------------------------------
% 48.78/7.30 % (900201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.78/7.30 % (900201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.78/7.30 % (900201)CaDiCaL version: 2.1.3
% 48.78/7.30 % (900201)Termination reason: Instruction limit
% 48.78/7.30 % (900201)Termination phase: Saturation
% 48.78/7.30 % (900201)Time elapsed: 0.407 s
% 48.78/7.30 % (900201)Peak memory usage: 19 MB
% 48.78/7.30 % (900201)Instructions burned: 685 (million)
% 48.78/7.30 % (900206)Instruction limit reached!
% 48.78/7.30 % (900206)------------------------------
% 48.78/7.30 % (900206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.78/7.30 % (900206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.78/7.30 % (900206)CaDiCaL version: 2.1.3
% 48.78/7.30 % (900206)Termination reason: Instruction limit
% 48.78/7.30 % (900206)Termination phase: Saturation
% 48.78/7.30 % (900206)Time elapsed: 0.331 s
% 48.78/7.30 % (900206)Peak memory usage: 15 MB
% 48.78/7.30 % (900206)Instructions burned: 477 (million)
% 48.78/7.30 % (900214)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2048259541:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 48.78/7.30 % (900215)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2152293348:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 48.78/7.30 % TRYING [14]
% 48.78/7.30 % TRYING [7]
% 48.78/7.30 % (900212)Instruction limit reached!
% 48.78/7.30 % (900212)------------------------------
% 48.78/7.30 % (900212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.72/14.97 % (900212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.72/14.97 % (900212)CaDiCaL version: 2.1.3
% 102.72/14.97 % (900212)Termination reason: Instruction limit
% 102.72/14.97 % (900212)Termination phase: Finite model building constraint generation
% 102.72/14.97 % (900212)Time elapsed: 0.222 s
% 102.72/14.97 % (900212)Peak memory usage: 97 MB
% 102.72/14.97 % (900212)Instructions burned: 895 (million)
% 102.72/14.97 % (900218)fmb+10_1_sil=64000:random_seed=332800942:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 102.72/14.97 % TRYING [1]
% 102.72/14.97 % TRYING [2]
% 102.72/14.97 % TRYING [3]
% 102.72/14.97 % TRYING [4]
% 102.72/14.97 % TRYING [5]
% 102.72/14.97 % (900214)Instruction limit reached!
% 102.72/14.97 % (900214)------------------------------
% 102.72/14.97 % (900214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.72/14.97 % (900214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.72/14.97 % (900214)CaDiCaL version: 2.1.3
% 102.72/14.97 % (900214)Termination reason: Instruction limit
% 102.72/14.97 % (900214)Termination phase: Saturation
% 102.72/14.97 % (900214)Time elapsed: 0.382 s
% 102.72/14.98 % (900214)Peak memory usage: 20 MB
% 102.72/14.98 % (900214)Instructions burned: 693 (million)
% 102.72/14.98 % (900220)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2729965293:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 102.72/14.98 % TRYING [20]
% 102.72/14.98 % TRYING [6]
% 102.72/14.98 % (900210)Instruction limit reached!
% 102.72/14.98 % (900210)------------------------------
% 102.72/14.98 % (900210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.72/14.98 % (900210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.72/14.98 % (900210)CaDiCaL version: 2.1.3
% 102.72/14.98 % (900210)Termination reason: Instruction limit
% 102.72/14.98 % (900210)Termination phase: Saturation
% 102.72/14.98 % (900210)Time elapsed: 0.732 s
% 102.72/14.98 % (900210)Peak memory usage: 25 MB
% 102.72/14.98 % (900210)Instructions burned: 1180 (million)
% 102.72/14.98 % (900222)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1974610809:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 102.72/14.98 % TRYING [8]
% 102.72/14.98 % (900215)Instruction limit reached!
% 102.72/14.98 % (900215)------------------------------
% 102.72/14.98 % (900215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.72/14.98 % (900215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.72/14.98 % (900215)CaDiCaL version: 2.1.3
% 102.72/14.98 % (900215)Termination reason: Instruction limit
% 102.72/14.98 % (900215)Termination phase: Saturation
% 102.72/14.98 % (900215)Time elapsed: 0.482 s
% 102.72/14.98 % (900215)Peak memory usage: 20 MB
% 102.72/14.98 % (900215)Instructions burned: 880 (million)
% 102.72/14.98 % (900224)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1691048604:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 102.72/14.98 % (900222)Instruction limit reached!
% 102.72/14.98 % (900222)------------------------------
% 102.72/14.98 % (900222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.72/14.98 % (900222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.72/14.98 % (900222)CaDiCaL version: 2.1.3
% 102.72/14.98 % (900222)Termination reason: Instruction limit
% 102.72/14.98 % (900222)Termination phase: Finite model building constraint generation
% 102.72/14.98 % (900222)Time elapsed: 0.354 s
% 102.72/14.98 % (900222)Peak memory usage: 79 MB
% 102.72/14.98 % (900222)Instructions burned: 920 (million)
% 102.72/14.98 % (900226)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=675657278:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 102.72/14.98 % TRYING [7]
% 102.72/14.98 % TRYING [8]
% 102.72/14.98 % (900226)Instruction limit reached!
% 102.72/14.98 % (900226)------------------------------
% 102.72/14.98 % (900226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.72/14.98 % (900226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.72/14.98 % (900226)CaDiCaL version: 2.1.3
% 102.72/14.98 % (900226)Termination reason: Instruction limit
% 102.72/14.98 % (900226)Termination phase: Saturation
% 102.72/14.98 % (900226)Time elapsed: 0.838 s
% 102.72/14.98 % (900226)Peak memory usage: 30 MB
% 102.72/14.98 % (900226)Instructions burned: 1474 (million)
% 102.72/14.98 % (900228)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3718289821:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 102.72/14.98 % TRYING [77]
% 102.72/14.98 % TRYING [8]
% 102.72/14.98 % (900220)Instruction limit reached!
% 102.72/14.98 % (900220)------------------------------
% 102.72/14.98 % (900220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.00/38.20 % (900220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.00/38.20 % (900220)CaDiCaL version: 2.1.3
% 268.00/38.20 % (900220)Termination reason: Instruction limit
% 268.00/38.20 % (900220)Termination phase: Finite model building constraint generation
% 268.00/38.20 % (900220)Time elapsed: 3.040 s
% 268.00/38.20 % (900220)Peak memory usage: 501 MB
% 268.00/38.20 % (900220)Instructions burned: 9516 (million)
% 268.00/38.20 % (900224)Instruction limit reached!
% 268.00/38.20 % (900224)------------------------------
% 268.00/38.20 % (900224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.00/38.20 % (900224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.00/38.20 % (900224)CaDiCaL version: 2.1.3
% 268.00/38.20 % (900224)Termination reason: Instruction limit
% 268.00/38.20 % (900224)Termination phase: Saturation
% 268.00/38.20 % (900224)Time elapsed: 2.965 s
% 268.00/38.20 % (900224)Peak memory usage: 36 MB
% 268.00/38.20 % (900224)Instructions burned: 5131 (million)
% 268.00/38.20 % (900230)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=841674523:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 268.00/38.20 % (900232)ott-2_1_sil=16000:newcnf=on:random_seed=2966796320:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2959 on theBenchmark for (2959ds/869Mi)
% 268.00/38.20 % TRYING [16]
% 268.00/38.20 % (900228)Instruction limit reached!
% 268.00/38.20 % (900228)------------------------------
% 268.00/38.20 % (900228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.00/38.20 % (900228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.00/38.20 % (900228)CaDiCaL version: 2.1.3
% 268.00/38.20 % (900228)Termination reason: Instruction limit
% 268.00/38.20 % (900228)Termination phase: Finite model building constraint generation
% 268.00/38.20 % (900228)Time elapsed: 2.351 s
% 268.00/38.20 % (900228)Peak memory usage: 523 MB
% 268.00/38.20 % (900228)Instructions burned: 6325 (million)
% 268.00/38.20 % (900232)Instruction limit reached!
% 268.00/38.20 % (900232)------------------------------
% 268.00/38.20 % (900232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.00/38.20 % (900232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.00/38.20 % (900232)CaDiCaL version: 2.1.3
% 268.00/38.20 % (900232)Termination reason: Instruction limit
% 268.00/38.20 % (900232)Termination phase: Saturation
% 268.00/38.20 % (900232)Time elapsed: 0.543 s
% 268.00/38.20 % (900232)Peak memory usage: 21 MB
% 268.00/38.20 % (900232)Instructions burned: 869 (million)
% 268.00/38.20 % (900234)ott+10_1_sil=32000:tgt=ground:random_seed=3335447059:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 268.00/38.20 % (900236)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2413206345:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 268.00/38.20 % TRYING [1]
% 268.00/38.20 % TRYING [2]
% 268.00/38.20 % TRYING [3]
% 268.00/38.20 % TRYING [4]
% 268.00/38.20 % TRYING [5]
% 268.00/38.20 % (900230)Instruction limit reached!
% 268.00/38.20 % (900230)------------------------------
% 268.00/38.20 % (900230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.00/38.20 % (900230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.00/38.20 % (900230)CaDiCaL version: 2.1.3
% 268.00/38.20 % (900230)Termination reason: Instruction limit
% 268.00/38.20 % (900230)Termination phase: Finite model building constraint generation
% 268.00/38.20 % (900230)Time elapsed: 0.775 s
% 268.00/38.20 % (900230)Peak memory usage: 128 MB
% 268.00/38.20 % (900230)Instructions burned: 2176 (million)
% 268.00/38.20 % (900238)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=424669287:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 268.00/38.20 % TRYING [6]
% 268.00/38.20 % TRYING [9]
% 268.00/38.20 % TRYING [7]
% 268.00/38.20 % (900218)Instruction limit reached!
% 268.00/38.20 % (900218)------------------------------
% 268.00/38.20 % (900218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 268.00/38.20 % (900218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 268.00/38.20 % (900218)CaDiCaL version: 2.1.3
% 268.00/38.20 % (900218)Termination reason: Instruction limit
% 268.00/38.20 % (900218)Termination phase: Finite model building SAT solving
% 268.00/38.20 % (900218)Time elapsed: 5.519 s
% 268.00/38.20 % (900218)Peak memory usage: 190 MB
% 268.00/38.20 % (900218)Instructions burned: 22065 (million)
% 268.00/38.20 % (900240)dis+21_1_sil=32000:sas=cadical:random_seed=1743531484:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 268.00/38.20 % TRYING [8]
% 268.00/38.20 % (900238)Instruction limit reached!
% 268.00/38.20 % (900238)------------------------------
% 268.00/38.20 % (900238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900238)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900238)Termination reason: Instruction limit
% 162.24/41.24 % (900238)Termination phase: Saturation
% 162.24/41.24 % (900238)Time elapsed: 1.995 s
% 162.24/41.24 % (900238)Peak memory usage: 30 MB
% 162.24/41.24 % (900238)Instructions burned: 3513 (million)
% 162.24/41.24 % (900243)ott+11_1_sil=16000:gs=on:random_seed=1920710667:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 162.24/41.24 % (900240)Instruction limit reached!
% 162.24/41.24 % (900240)------------------------------
% 162.24/41.24 % (900240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900240)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900240)Termination reason: Instruction limit
% 162.24/41.24 % (900240)Termination phase: Saturation
% 162.24/41.24 % (900240)Time elapsed: 1.131 s
% 162.24/41.24 % (900240)Peak memory usage: 38 MB
% 162.24/41.24 % (900240)Instructions burned: 3774 (million)
% 162.24/41.24 % (900245)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4013480242:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi)
% 162.24/41.24 % TRYING [7]
% 162.24/41.24 % (900234)Instruction limit reached!
% 162.24/41.24 % (900234)------------------------------
% 162.24/41.24 % (900234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900234)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900234)Termination reason: Instruction limit
% 162.24/41.24 % (900234)Termination phase: Saturation
% 162.24/41.24 % (900234)Time elapsed: 3.091 s
% 162.24/41.24 % (900234)Peak memory usage: 49 MB
% 162.24/41.24 % (900234)Instructions burned: 5115 (million)
% 162.24/41.24 % (900247)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=84853871:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2922 on theBenchmark for (2922ds/4591Mi)
% 162.24/41.24 % (900243)Instruction limit reached!
% 162.24/41.24 % (900243)------------------------------
% 162.24/41.24 % (900243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900243)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900243)Termination reason: Instruction limit
% 162.24/41.24 % (900243)Termination phase: Saturation
% 162.24/41.24 % (900243)Time elapsed: 1.671 s
% 162.24/41.24 % (900243)Peak memory usage: 34 MB
% 162.24/41.24 % (900243)Instructions burned: 2252 (million)
% 162.24/41.24 % (900249)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2650113944:i=29340_2914 on theBenchmark for (2914ds/29340Mi)
% 162.24/41.24 % TRYING [8]
% 162.24/41.24 % TRYING [9]
% 162.24/41.24 % (900247)Instruction limit reached!
% 162.24/41.24 % (900247)------------------------------
% 162.24/41.24 % (900247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900247)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900247)Termination reason: Instruction limit
% 162.24/41.24 % (900247)Termination phase: Saturation
% 162.24/41.24 % (900247)Time elapsed: 2.180 s
% 162.24/41.24 % (900247)Peak memory usage: 36 MB
% 162.24/41.24 % (900247)Instructions burned: 4592 (million)
% 162.24/41.24 % (900251)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=464894131:i=5211_2900 on theBenchmark for (2900ds/5211Mi)
% 162.24/41.24 % (900251)Instruction limit reached!
% 162.24/41.24 % (900251)------------------------------
% 162.24/41.24 % (900251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900251)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900251)Termination reason: Instruction limit
% 162.24/41.24 % (900251)Termination phase: Saturation
% 162.24/41.24 % (900251)Time elapsed: 2.597 s
% 162.24/41.24 % (900251)Peak memory usage: 48 MB
% 162.24/41.24 % (900251)Instructions burned: 5212 (million)
% 162.24/41.24 % (900253)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1460592666:i=5497:nm=2_2874 on theBenchmark for (2874ds/5497Mi)
% 162.24/41.24 % TRYING [17]
% 162.24/41.24 % TRYING [9]
% 162.24/41.24 % TRYING [9]
% 162.24/41.24 % (900253)Instruction limit reached!
% 162.24/41.24 % (900253)------------------------------
% 162.24/41.24 % (900253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900253)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900253)Termination reason: Instruction limit
% 162.24/41.24 % (900253)Termination phase: Finite model building constraint generation
% 162.24/41.24 % (900253)Time elapsed: 1.940 s
% 162.24/41.24 % (900253)Peak memory usage: 364 MB
% 162.24/41.24 % (900253)Instructions burned: 5499 (million)
% 162.24/41.24 % (900255)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=974224231:fmbsr=2:i=46332_2854 on theBenchmark for (2854ds/46332Mi)
% 162.24/41.24 % TRYING [15]
% 162.24/41.24 % (900249)Instruction limit reached!
% 162.24/41.24 % (900249)------------------------------
% 162.24/41.24 % (900249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900249)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900249)Termination reason: Instruction limit
% 162.24/41.24 % (900249)Termination phase: Saturation
% 162.24/41.24 % (900249)Time elapsed: 15.385 s
% 162.24/41.24 % (900249)Peak memory usage: 410 MB
% 162.24/41.24 % (900249)Instructions burned: 29341 (million)
% 162.24/41.24 % (900257)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2687706664:i=14071_2759 on theBenchmark for (2759ds/14071Mi)
% 162.24/41.24 % TRYING [12]
% 162.24/41.24 % (900245)Instruction limit reached!
% 162.24/41.24 % (900245)------------------------------
% 162.24/41.24 % (900245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900245)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900245)Termination reason: Instruction limit
% 162.24/41.24 % (900245)Termination phase: Finite model building SAT solving
% 162.24/41.24 % (900245)Time elapsed: 20.632 s
% 162.24/41.24 % (900245)Peak memory usage: 260 MB
% 162.24/41.24 % (900245)Instructions burned: 67536 (million)
% 162.24/41.24 % (900259)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=46301691:i=22565:add=on:rawr=on_2719 on theBenchmark for (2719ds/22565Mi)
% 162.24/41.24 % (900257)Instruction limit reached!
% 162.24/41.24 % (900257)------------------------------
% 162.24/41.24 % (900257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900257)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900257)Termination reason: Instruction limit
% 162.24/41.24 % (900257)Termination phase: Finite model building SAT solving
% 162.24/41.24 % (900257)Time elapsed: 6.568 s
% 162.24/41.24 % (900257)Peak memory usage: 760 MB
% 162.24/41.24 % (900257)Instructions burned: 14071 (million)
% 162.24/41.24 % (900261)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=907902617:i=8173:av=off_2692 on theBenchmark for (2692ds/8173Mi)
% 162.24/41.24 % (900236)Instruction limit reached!
% 162.24/41.24 % (900236)------------------------------
% 162.24/41.24 % (900236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900236)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900236)Termination reason: Instruction limit
% 162.24/41.24 % (900236)Termination phase: Finite model building SAT solving
% 162.24/41.24 % (900236)Time elapsed: 27.946 s
% 162.24/41.24 % (900236)Peak memory usage: 384 MB
% 162.24/41.24 % (900236)Instructions burned: 54282 (million)
% 162.24/41.24 % (900263)dis+10_16:1_sil=16000:random_seed=2326507264:i=9155:fsr=off_2672 on theBenchmark for (2672ds/9155Mi)
% 162.24/41.24 % (900261)Instruction limit reached!
% 162.24/41.24 % (900261)------------------------------
% 162.24/41.24 % (900261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900261)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900261)Termination reason: Instruction limit
% 162.24/41.24 % (900261)Termination phase: Saturation
% 162.24/41.24 % (900261)Time elapsed: 4.887 s
% 162.24/41.24 % (900261)Peak memory usage: 127 MB
% 162.24/41.24 % (900261)Instructions burned: 8174 (million)
% 162.24/41.24 % TRYING [10]
% 162.24/41.24 % (900265)ott-3_8_sil=64000:random_seed=3512014188:i=20139:bs=on_2643 on theBenchmark for (2643ds/20139Mi)
% 162.24/41.24 % (900263)Instruction limit reached!
% 162.24/41.24 % (900263)------------------------------
% 162.24/41.24 % (900263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900263)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900263)Termination reason: Instruction limit
% 162.24/41.24 % (900263)Termination phase: Saturation
% 162.24/41.24 % (900263)Time elapsed: 5.050 s
% 162.24/41.24 % (900263)Peak memory usage: 79 MB
% 162.24/41.24 % (900263)Instructions burned: 9155 (million)
% 162.24/41.24 % (900267)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4147570834:fmbsr=2:i=32576_2622 on theBenchmark for (2622ds/32576Mi)
% 162.24/41.24 % TRYING [9]
% 162.24/41.24 % (900259)Instruction limit reached!
% 162.24/41.24 % (900259)------------------------------
% 162.24/41.24 % (900259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900259)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900259)Termination reason: Instruction limit
% 162.24/41.24 % (900259)Termination phase: Saturation
% 162.24/41.24 % (900259)Time elapsed: 10.593 s
% 162.24/41.24 % (900259)Peak memory usage: 84 MB
% 162.24/41.24 % (900259)Instructions burned: 22567 (million)
% 162.24/41.24 % (900269)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2219034974:i=11404_2613 on theBenchmark for (2613ds/11404Mi)
% 162.24/41.24 % (900255)Instruction limit reached!
% 162.24/41.24 % (900255)------------------------------
% 162.24/41.24 % (900255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900255)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900255)Termination reason: Instruction limit
% 162.24/41.24 % (900255)Termination phase: Finite model building SAT solving
% 162.24/41.24 % (900255)Time elapsed: 25.519 s
% 162.24/41.24 % (900255)Peak memory usage: 2485 MB
% 162.24/41.24 % (900255)Instructions burned: 46335 (million)
% 162.24/41.24 % (900271)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2021131313:i=14134_2595 on theBenchmark for (2595ds/14134Mi)
% 162.24/41.24 % (900269) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-900179-900269"...
% 162.24/41.24 % (900269)...printing done.
% 162.24/41.24 % (900269)Refutation found. Thanks to Tanya!
% 162.24/41.24 % SZS status Theorem for theBenchmark
% 162.24/41.24 % SZS output start Proof for theBenchmark
% See solution above
% 162.24/41.24 % (900269)------------------------------
% 162.24/41.24 % (900269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.24/41.24 % (900269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.24/41.24 % (900269)CaDiCaL version: 2.1.3
% 162.24/41.24 % (900269)Termination reason: Refutation
% 162.24/41.24 % (900269)Time elapsed: 2.086 s
% 162.24/41.24 % (900269)Peak memory usage: 64 MB
% 162.24/41.24 % (900269)Instructions burned: 5772 (million)
% 162.24/41.24 % (900179)Success in time 40.811 s
% 162.24/41.24 % Vampire exiting
%------------------------------------------------------------------------------