%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM563+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:24:49 PM UTC 2026
% Result : Theorem 37.85s 6.08s
% Output : Refutation 37.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 11
% Syntax : Number of formulae : 83 ( 22 unt; 2 def)
% Number of atoms : 425 ( 107 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 489 ( 147 ~; 131 |; 177 &)
% ( 8 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-2 aty)
% Number of variables : 139 ( 111 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ~ ? [X1] : aElementOf0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefEmp) ).
fof(f12,axiom,
! [X0] :
( aSet0(X0)
=> aSubsetOf0(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSubRefl) ).
fof(f42,axiom,
! [X0] :
( aSet0(X0)
=> ( sbrdtbr0(X0) = sz00
<=> X0 = slcrc0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardEmpty) ).
fof(f52,axiom,
slbdtrb0(sz00) = slcrc0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSegZero) ).
fof(f56,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sbrdtbr0(slbdtrb0(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardSeg) ).
fof(f74,axiom,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3418) ).
fof(f75,axiom,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,xS)
=> aElementOf0(X0,szNzAzT0) )
& aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3435) ).
fof(f76,axiom,
( aFunction0(xc)
& ! [X0] :
( ( aElementOf0(X0,szDzozmdt0(xc))
=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xS) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK ) )
& ( ( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xS) ) )
| aSubsetOf0(X0,xS) )
& sbrdtbr0(X0) = xK )
=> aElementOf0(X0,szDzozmdt0(xc)) ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X1] :
( aElementOf0(X1,szDzozmdt0(xc))
& sdtlpdtrp0(xc,X1) = X0 ) )
& ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(X0,xT) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3453) ).
fof(f78,conjecture,
( xK = sz00
=> ? [X0] :
( aElementOf0(X0,xT)
& ? [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xS) ) )
| aSubsetOf0(X1,xS) )
& isCountable0(X1)
& ! [X2] :
( ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) )
& aSubsetOf0(X2,X1)
& sbrdtbr0(X2) = xK
& aElementOf0(X2,slbdtsldtrb0(X1,xK)) )
=> sdtlpdtrp0(xc,X2) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f79,negated_conjecture,
~ ( xK = sz00
=> ? [X0] :
( aElementOf0(X0,xT)
& ? [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xS) ) )
| aSubsetOf0(X1,xS) )
& isCountable0(X1)
& ! [X2] :
( ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) )
& aSubsetOf0(X2,X1)
& sbrdtbr0(X2) = xK
& aElementOf0(X2,slbdtsldtrb0(X1,xK)) )
=> sdtlpdtrp0(xc,X2) = X0 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f78]) ).
fof(f87,plain,
( aFunction0(xc)
& ! [X0] :
( ( aElementOf0(X0,szDzozmdt0(xc))
=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xS) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK ) )
& ( ( ( ( aSet0(X0)
& ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(X2,xS) ) )
| aSubsetOf0(X0,xS) )
& sbrdtbr0(X0) = xK )
=> aElementOf0(X0,szDzozmdt0(xc)) ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X4] :
( aElementOf0(X4,szDzozmdt0(xc))
& sdtlpdtrp0(xc,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(X5,xT) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(rectify,[],[f76]) ).
fof(f89,plain,
~ ( xK = sz00
=> ? [X0] :
( aElementOf0(X0,xT)
& ? [X1] :
( ( ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xS) ) )
| aSubsetOf0(X1,xS) )
& isCountable0(X1)
& ! [X3] :
( ( aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X3)
=> aElementOf0(X4,X1) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xK
& aElementOf0(X3,slbdtsldtrb0(X1,xK)) )
=> sdtlpdtrp0(xc,X3) = X0 ) ) ) ),
inference(rectify,[],[f79]) ).
fof(f91,plain,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f99,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f140,plain,
! [X0] :
( ( sbrdtbr0(X0) = sz00
<=> X0 = slcrc0 )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f163,plain,
! [X0] :
( sbrdtbr0(slbdtrb0(X0)) = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f189,plain,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) )
& aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
inference(ennf_transformation,[],[f75]) ).
fof(f190,plain,
( aFunction0(xc)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,X0) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK )
| ~ aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
| ( ( ~ aSet0(X0)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X0) ) )
& ~ aSubsetOf0(X0,xS) )
| sbrdtbr0(X0) != xK ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X4] :
( aElementOf0(X4,szDzozmdt0(xc))
& sdtlpdtrp0(xc,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,xT)
| ~ aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(ennf_transformation,[],[f87]) ).
fof(f191,plain,
( aFunction0(xc)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,X0) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK )
| ~ aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
| ( ( ~ aSet0(X0)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X0) ) )
& ~ aSubsetOf0(X0,xS) )
| sbrdtbr0(X0) != xK ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X3] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [X4] :
( aElementOf0(X4,szDzozmdt0(xc))
& sdtlpdtrp0(xc,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,xT)
| ~ aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(flattening,[],[f190]) ).
fof(f194,plain,
( ! [X0] :
( ~ aElementOf0(X0,xT)
| ! [X1] :
( ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,xS) )
| ~ isCountable0(X1)
| ? [X3] :
( sdtlpdtrp0(xc,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xK
& aElementOf0(X3,slbdtsldtrb0(X1,xK)) ) ) )
& xK = sz00 ),
inference(ennf_transformation,[],[f89]) ).
fof(f195,plain,
( ! [X0] :
( ~ aElementOf0(X0,xT)
| ! [X1] :
( ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,xS) )
| ~ isCountable0(X1)
| ? [X3] :
( sdtlpdtrp0(xc,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xK
& aElementOf0(X3,slbdtsldtrb0(X1,xK)) ) ) )
& xK = sz00 ),
inference(flattening,[],[f194]) ).
fof(f207,definition,
! [X0,X1] :
( ? [X3] :
( sdtlpdtrp0(xc,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xK
& aElementOf0(X3,slbdtsldtrb0(X1,xK)) )
| ~ sP8(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f208,plain,
( ! [X0] :
( ~ aElementOf0(X0,xT)
| ! [X1] :
( ( ( ~ aSet0(X1)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X1) ) )
& ~ aSubsetOf0(X1,xS) )
| ~ isCountable0(X1)
| sP8(X0,X1) ) )
& xK = sz00 ),
inference(definition_folding,[],[f195,f207]) ).
fof(f209,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) )
| slcrc0 != X0 ) ),
inference(nnf_transformation,[],[f91]) ).
fof(f210,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) )
| slcrc0 != X0 ) ),
inference(flattening,[],[f209]) ).
fof(f211,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| ? [X1] : aElementOf0(X1,X0) )
& ( ( aSet0(X0)
& ! [X2] : ~ aElementOf0(X2,X0) )
| slcrc0 != X0 ) ),
inference(rectify,[],[f210]) ).
fof(f212,plain,
! [X0] :
( ( X0 = slcrc0
| ~ aSet0(X0)
| aElementOf0(sK9(X0),X0) )
& ( ( aSet0(X0)
& ! [X2] : ~ aElementOf0(X2,X0) )
| slcrc0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X1,sK9(X0))],[f211]) ).
fof(f232,plain,
! [X0] :
( ( ( sbrdtbr0(X0) = sz00
| slcrc0 != X0 )
& ( X0 = slcrc0
| sz00 != sbrdtbr0(X0) ) )
| ~ aSet0(X0) ),
inference(nnf_transformation,[],[f140]) ).
fof(f268,plain,
( aFunction0(xc)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,X0) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK )
| ~ aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
| ( ( ~ aSet0(X0)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X0) ) )
& ~ aSubsetOf0(X0,xS) )
| sbrdtbr0(X0) != xK ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X3] :
( ( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ! [X4] :
( ~ aElementOf0(X4,szDzozmdt0(xc))
| sdtlpdtrp0(xc,X4) != X3 ) )
& ( ? [X4] :
( aElementOf0(X4,szDzozmdt0(xc))
& sdtlpdtrp0(xc,X4) = X3 )
| ~ aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& ! [X5] :
( aElementOf0(X5,xT)
| ~ aElementOf0(X5,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(nnf_transformation,[],[f191]) ).
fof(f269,plain,
( aFunction0(xc)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,X0) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK )
| ~ aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
| ( ( ~ aSet0(X0)
| ? [X2] :
( ~ aElementOf0(X2,xS)
& aElementOf0(X2,X0) ) )
& ~ aSubsetOf0(X0,xS) )
| sbrdtbr0(X0) != xK ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X3] :
( ( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ! [X4] :
( ~ aElementOf0(X4,szDzozmdt0(xc))
| sdtlpdtrp0(xc,X4) != X3 ) )
& ( ? [X5] :
( aElementOf0(X5,szDzozmdt0(xc))
& sdtlpdtrp0(xc,X5) = X3 )
| ~ aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& ! [X6] :
( aElementOf0(X6,xT)
| ~ aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(rectify,[],[f268]) ).
fof(f270,plain,
( aFunction0(xc)
& ! [X0] :
( ( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,xS)
| ~ aElementOf0(X1,X0) )
& aSubsetOf0(X0,xS)
& sbrdtbr0(X0) = xK )
| ~ aElementOf0(X0,szDzozmdt0(xc)) )
& ( aElementOf0(X0,szDzozmdt0(xc))
| ( ( ~ aSet0(X0)
| ( ~ aElementOf0(sK28(X0),xS)
& aElementOf0(sK28(X0),X0) ) )
& ~ aSubsetOf0(X0,xS) )
| sbrdtbr0(X0) != xK ) )
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& ! [X3] :
( ( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ! [X4] :
( ~ aElementOf0(X4,szDzozmdt0(xc))
| sdtlpdtrp0(xc,X4) != X3 ) )
& ( ( aElementOf0(sK29(X3),szDzozmdt0(xc))
& sdtlpdtrp0(xc,sK29(X3)) = X3 )
| ~ aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& ! [X6] :
( aElementOf0(X6,xT)
| ~ aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28,sK29]),skolemize(X2,sK28(X0)),skolemize(X5,sK29(X3))],[f269]) ).
fof(f284,plain,
! [X0,X1] :
( ? [X3] :
( sdtlpdtrp0(xc,X3) != X0
& aSet0(X3)
& ! [X4] :
( aElementOf0(X4,X1)
| ~ aElementOf0(X4,X3) )
& aSubsetOf0(X3,X1)
& sbrdtbr0(X3) = xK
& aElementOf0(X3,slbdtsldtrb0(X1,xK)) )
| ~ sP8(X0,X1) ),
inference(nnf_transformation,[],[f207]) ).
fof(f285,plain,
! [X0,X1] :
( ? [X2] :
( sdtlpdtrp0(xc,X2) != X0
& aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X1)
| ~ aElementOf0(X3,X2) )
& aSubsetOf0(X2,X1)
& sbrdtbr0(X2) = xK
& aElementOf0(X2,slbdtsldtrb0(X1,xK)) )
| ~ sP8(X0,X1) ),
inference(rectify,[],[f284]) ).
fof(f286,plain,
! [X0,X1] :
( ( sdtlpdtrp0(xc,sK38(X0,X1)) != X0
& aSet0(sK38(X0,X1))
& ! [X3] :
( aElementOf0(X3,X1)
| ~ aElementOf0(X3,sK38(X0,X1)) )
& aSubsetOf0(sK38(X0,X1),X1)
& xK = sbrdtbr0(sK38(X0,X1))
& aElementOf0(sK38(X0,X1),slbdtsldtrb0(X1,xK)) )
| ~ sP8(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X2,sK38(X0,X1))],[f285]) ).
fof(f287,plain,
( ! [X0] :
( ~ aElementOf0(X0,xT)
| ! [X1] :
( ( ( ~ aSet0(X1)
| ( ~ aElementOf0(sK39(X1),xS)
& aElementOf0(sK39(X1),X1) ) )
& ~ aSubsetOf0(X1,xS) )
| ~ isCountable0(X1)
| sP8(X0,X1) ) )
& xK = sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X2,sK39(X1))],[f208]) ).
fof(f289,plain,
! [X2,X0] :
( ~ aElementOf0(X2,X0)
| slcrc0 != X0 ),
inference(cnf_transformation,[],[f212]) ).
fof(f290,plain,
! [X0] :
( aSet0(X0)
| slcrc0 != X0 ),
inference(cnf_transformation,[],[f212]) ).
fof(f300,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f355,plain,
! [X0] :
( slcrc0 = X0
| sz00 != sbrdtbr0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f379,plain,
slcrc0 = slbdtrb0(sz00),
inference(cnf_transformation,[],[f52]) ).
fof(f387,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sbrdtbr0(slbdtrb0(X0)) = X0 ),
inference(cnf_transformation,[],[f163]) ).
fof(f433,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[],[f74]) ).
fof(f434,plain,
isCountable0(xS),
inference(cnf_transformation,[],[f189]) ).
fof(f437,plain,
aSet0(xS),
inference(cnf_transformation,[],[f189]) ).
fof(f439,plain,
! [X6] :
( ~ aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(X6,xT) ),
inference(cnf_transformation,[],[f270]) ).
fof(f442,plain,
! [X3,X4] :
( aElementOf0(X3,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X4,szDzozmdt0(xc))
| sdtlpdtrp0(xc,X4) != X3 ),
inference(cnf_transformation,[],[f270]) ).
fof(f446,plain,
! [X0] :
( sbrdtbr0(X0) != xK
| ~ aSet0(X0)
| aElementOf0(sK28(X0),X0)
| aElementOf0(X0,szDzozmdt0(xc)) ),
inference(cnf_transformation,[],[f270]) ).
fof(f485,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| xK = sbrdtbr0(sK38(X0,X1)) ),
inference(cnf_transformation,[],[f286]) ).
fof(f488,plain,
! [X0,X1] :
( aSet0(sK38(X0,X1))
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f286]) ).
fof(f489,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK38(X0,X1)) != X0
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f286]) ).
fof(f490,plain,
sz00 = xK,
inference(cnf_transformation,[],[f287]) ).
fof(f491,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT)
| ~ isCountable0(X1)
| sP8(X0,X1) ),
inference(cnf_transformation,[],[f287]) ).
fof(f501,plain,
! [X0] :
( sbrdtbr0(X0) != xK
| slcrc0 = X0
| ~ aSet0(X0) ),
inference(definition_unfolding,[],[f355,f490]) ).
fof(f502,plain,
slcrc0 = slbdtrb0(xK),
inference(definition_unfolding,[],[f379,f490]) ).
fof(f505,plain,
aSet0(slcrc0),
inference(equality_resolution,[],[f290]) ).
fof(f506,plain,
! [X2] : ~ aElementOf0(X2,slcrc0),
inference(equality_resolution,[],[f289]) ).
fof(f542,plain,
! [X4] :
( aElementOf0(sdtlpdtrp0(xc,X4),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X4,szDzozmdt0(xc)) ),
inference(equality_resolution,[],[f442]) ).
fof(f550,definition,
sF41 = slbdtrb0(xK),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f551,plain,
slbdtrb0(xK) = sF41,
inference(reorient_equations,[],[f550]) ).
fof(f552,plain,
slcrc0 = sF41,
inference(definition_folding,[],[f502,f551]) ).
fof(f554,plain,
slcrc0 = slbdtrb0(xK),
inference(forward_demodulation,[],[f551,f552]) ).
fof(f568,plain,
! [X0] :
( ~ aSet0(xS)
| ~ aElementOf0(X0,xT)
| ~ isCountable0(xS)
| sP8(X0,xS) ),
inference(resolution,[],[f300,f491]) ).
fof(f571,plain,
! [X0] :
( ~ aElementOf0(X0,xT)
| ~ isCountable0(xS)
| sP8(X0,xS) ),
inference(forward_subsumption_resolution,[],[f568,f437]) ).
fof(f572,plain,
! [X0] :
( ~ aElementOf0(X0,xT)
| sP8(X0,xS) ),
inference(forward_subsumption_resolution,[],[f571,f434]) ).
fof(f667,plain,
xK = sbrdtbr0(slbdtrb0(xK)),
inference(resolution,[],[f387,f433]) ).
fof(f669,plain,
xK = sbrdtbr0(slcrc0),
inference(forward_demodulation,[],[f667,f554]) ).
fof(f989,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xc,X0),xT)
| ~ aElementOf0(X0,szDzozmdt0(xc)) ),
inference(resolution,[],[f542,f439]) ).
fof(f1289,plain,
( xK != xK
| ~ aSet0(slcrc0)
| aElementOf0(sK28(slcrc0),slcrc0)
| aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(superposition,[],[f446,f669]) ).
fof(f1295,plain,
( ~ aSet0(slcrc0)
| aElementOf0(sK28(slcrc0),slcrc0)
| aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(trivial_inequality_removal,[],[f1289]) ).
fof(f1297,plain,
( aElementOf0(sK28(slcrc0),slcrc0)
| aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(forward_subsumption_resolution,[],[f1295,f505]) ).
fof(f1299,plain,
aElementOf0(slcrc0,szDzozmdt0(xc)),
inference(forward_subsumption_resolution,[],[f1297,f506]) ).
fof(f9043,plain,
! [X0] :
( sP8(sdtlpdtrp0(xc,X0),xS)
| ~ aElementOf0(X0,szDzozmdt0(xc)) ),
inference(resolution,[],[f989,f572]) ).
fof(f9148,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xc))
| xK = sbrdtbr0(sK38(sdtlpdtrp0(xc,X0),xS)) ),
inference(resolution,[],[f9043,f485]) ).
fof(f12811,plain,
xK = sbrdtbr0(sK38(sdtlpdtrp0(xc,slcrc0),xS)),
inference(resolution,[],[f9148,f1299]) ).
fof(f12991,plain,
( xK != xK
| slcrc0 = sK38(sdtlpdtrp0(xc,slcrc0),xS)
| ~ aSet0(sK38(sdtlpdtrp0(xc,slcrc0),xS)) ),
inference(superposition,[],[f501,f12811]) ).
fof(f13003,plain,
( ~ aSet0(sK38(sdtlpdtrp0(xc,slcrc0),xS))
| slcrc0 = sK38(sdtlpdtrp0(xc,slcrc0),xS) ),
inference(trivial_inequality_removal,[],[f12991]) ).
fof(f39950,plain,
( ~ sP8(sdtlpdtrp0(xc,slcrc0),xS)
| slcrc0 = sK38(sdtlpdtrp0(xc,slcrc0),xS) ),
inference(resolution,[],[f13003,f488]) ).
fof(f40087,plain,
( slcrc0 = sK38(sdtlpdtrp0(xc,slcrc0),xS)
| ~ aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(resolution,[],[f39950,f9043]) ).
fof(f40096,plain,
slcrc0 = sK38(sdtlpdtrp0(xc,slcrc0),xS),
inference(forward_subsumption_resolution,[],[f40087,f1299]) ).
fof(f40381,plain,
( sdtlpdtrp0(xc,slcrc0) != sdtlpdtrp0(xc,slcrc0)
| ~ sP8(sdtlpdtrp0(xc,slcrc0),xS) ),
inference(superposition,[],[f489,f40096]) ).
fof(f40391,plain,
~ sP8(sdtlpdtrp0(xc,slcrc0),xS),
inference(trivial_inequality_removal,[],[f40381]) ).
fof(f40453,plain,
~ aElementOf0(slcrc0,szDzozmdt0(xc)),
inference(resolution,[],[f40391,f9043]) ).
fof(f40462,plain,
$false,
inference(forward_subsumption_resolution,[],[f40453,f1299]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM563+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 20:26:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.23/2.74 % (2915214)Will run a generic schedule for satisfiability detection.
% 16.23/2.74 % (2915221)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2433434050:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.23/2.74 % (2915225)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3936296995:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.23/2.74 % (2915219)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4073325670_2999 on theBenchmark for (2999ds/0Mi)
% 16.23/2.74 % (2915222)dis+10_1_sil=32000:sp=arity:random_seed=2968418442:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.23/2.74 % (2915223)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1834954168:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.23/2.74 % (2915224)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3929459708:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.23/2.74 % (2915220)% WARNING: option uhcvi not known.
% 16.23/2.74 % (2915220)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=810849140:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.23/2.74 % TRYING [1]
% 16.23/2.74 % TRYING [2]
% 16.23/2.74 % TRYING [3]
% 16.23/2.74 % TRYING [4]
% 16.23/2.74 % (2915222)Instruction limit reached!
% 16.23/2.74 % (2915222)------------------------------
% 16.23/2.74 % (2915222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.74 % (2915222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.74 % (2915222)CaDiCaL version: 2.1.3
% 16.23/2.74 % (2915222)Termination reason: Instruction limit
% 16.23/2.74 % (2915222)Termination phase: Saturation
% 16.23/2.74 % (2915222)Time elapsed: 0.067 s
% 16.23/2.74 % (2915222)Peak memory usage: 13 MB
% 16.23/2.74 % (2915222)Instructions burned: 104 (million)
% 16.23/2.74 % (2915223)Instruction limit reached!
% 16.23/2.74 % (2915223)------------------------------
% 16.23/2.74 % (2915223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.74 % (2915223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.74 % (2915223)CaDiCaL version: 2.1.3
% 16.23/2.74 % (2915223)Termination reason: Instruction limit
% 16.23/2.74 % (2915223)Termination phase: Saturation
% 16.23/2.74 % (2915223)Time elapsed: 0.075 s
% 16.23/2.74 % (2915223)Peak memory usage: 13 MB
% 16.23/2.74 % (2915223)Instructions burned: 116 (million)
% 16.23/2.74 % (2915224)Instruction limit reached!
% 16.23/2.74 % (2915224)------------------------------
% 16.23/2.74 % (2915224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.74 % (2915224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.74 % (2915224)CaDiCaL version: 2.1.3
% 16.23/2.74 % (2915224)Termination reason: Instruction limit
% 16.23/2.74 % (2915224)Termination phase: Saturation
% 16.23/2.74 % (2915224)Time elapsed: 0.083 s
% 16.23/2.74 % (2915224)Peak memory usage: 13 MB
% 16.23/2.74 % (2915224)Instructions burned: 132 (million)
% 16.23/2.74 % (2915233)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1171215160:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.23/2.74 % (2915234)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3580448614:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.23/2.74 % (2915225)Instruction limit reached!
% 16.23/2.74 % (2915225)------------------------------
% 16.23/2.74 % (2915225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.74 % (2915225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.74 % (2915225)CaDiCaL version: 2.1.3
% 16.23/2.74 % (2915225)Termination reason: Instruction limit
% 16.23/2.74 % (2915225)Termination phase: Saturation
% 16.23/2.74 % (2915225)Time elapsed: 0.101 s
% 16.23/2.74 % (2915225)Peak memory usage: 14 MB
% 16.23/2.74 % (2915225)Instructions burned: 161 (million)
% 16.23/2.74 % (2915235)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=543800982:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.23/2.74 % TRYING [1]
% 16.23/2.74 % TRYING [2]
% 16.23/2.74 % TRYING [3]
% 16.23/2.74 % (2915238)ott-21_1_sil=16000:fs=off:random_seed=3150039277:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.23/2.74 % TRYING [4]
% 16.23/2.74 % TRYING [5]
% 16.23/2.74 % (2915234)Instruction limit reached!
% 16.23/2.74 % (2915234)------------------------------
% 16.23/2.74 % (2915234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915234)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915234)Termination reason: Instruction limit
% 37.85/6.08 % (2915234)Termination phase: Saturation
% 37.85/6.08 % (2915234)Time elapsed: 0.093 s
% 37.85/6.08 % (2915234)Peak memory usage: 13 MB
% 37.85/6.08 % (2915234)Instructions burned: 132 (million)
% 37.85/6.08 % (2915241)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=402657267:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 37.85/6.08 % TRYING [5]
% 37.85/6.08 % (2915238)Instruction limit reached!
% 37.85/6.08 % (2915238)------------------------------
% 37.85/6.08 % (2915238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915238)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915238)Termination reason: Instruction limit
% 37.85/6.08 % (2915238)Termination phase: Saturation
% 37.85/6.08 % (2915238)Time elapsed: 0.102 s
% 37.85/6.08 % (2915238)Peak memory usage: 13 MB
% 37.85/6.08 % (2915238)Instructions burned: 182 (million)
% 37.85/6.08 % (2915243)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2367351356:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.85/6.08 % TRYING [1]
% 37.85/6.08 % TRYING [2]
% 37.85/6.08 % TRYING [3]
% 37.85/6.08 % (2915233)Instruction limit reached!
% 37.85/6.08 % (2915233)------------------------------
% 37.85/6.08 % (2915233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915233)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915233)Termination reason: Instruction limit
% 37.85/6.08 % (2915233)Termination phase: Finite model building SAT solving
% 37.85/6.08 % (2915233)Time elapsed: 0.289 s
% 37.85/6.08 % (2915233)Peak memory usage: 35 MB
% 37.85/6.08 % (2915233)Instructions burned: 714 (million)
% 37.85/6.08 % TRYING [4]
% 37.85/6.08 % (2915245)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=101407836:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 37.85/6.08 % (2915235)Instruction limit reached!
% 37.85/6.08 % (2915235)------------------------------
% 37.85/6.08 % (2915235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915235)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915235)Termination reason: Instruction limit
% 37.85/6.08 % (2915235)Termination phase: Saturation
% 37.85/6.08 % (2915235)Time elapsed: 0.392 s
% 37.85/6.08 % (2915235)Peak memory usage: 20 MB
% 37.85/6.08 % (2915235)Instructions burned: 684 (million)
% 37.85/6.08 % (2915247)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=851807786:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 37.85/6.08 % (2915241)Instruction limit reached!
% 37.85/6.08 % (2915241)------------------------------
% 37.85/6.08 % (2915241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915241)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915241)Termination reason: Instruction limit
% 37.85/6.08 % (2915241)Termination phase: Saturation
% 37.85/6.08 % (2915241)Time elapsed: 0.324 s
% 37.85/6.08 % (2915241)Peak memory usage: 15 MB
% 37.85/6.08 % (2915241)Instructions burned: 478 (million)
% 37.85/6.08 % TRYING [6]
% 37.85/6.08 % (2915249)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=4141925314: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)
% 37.85/6.08 % (2915243)Instruction limit reached!
% 37.85/6.08 % (2915243)------------------------------
% 37.85/6.08 % (2915243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915243)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915243)Termination reason: Instruction limit
% 37.85/6.08 % (2915243)Termination phase: Finite model building SAT solving
% 37.85/6.08 % (2915243)Time elapsed: 0.368 s
% 37.85/6.08 % (2915243)Peak memory usage: 27 MB
% 37.85/6.08 % (2915243)Instructions burned: 867 (million)
% 37.85/6.08 % (2915251)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1804278559:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 37.85/6.08 % (2915247)Instruction limit reached!
% 37.85/6.08 % (2915247)------------------------------
% 37.85/6.08 % (2915247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915247)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915247)Termination reason: Instruction limit
% 37.85/6.08 % (2915247)Termination phase: Finite model building constraint generation
% 37.85/6.08 % (2915247)Time elapsed: 0.414 s
% 37.85/6.08 % (2915247)Peak memory usage: 103 MB
% 37.85/6.08 % (2915247)Instructions burned: 889 (million)
% 37.85/6.08 % (2915249)Instruction limit reached!
% 37.85/6.08 % (2915249)------------------------------
% 37.85/6.08 % (2915249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915249)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915249)Termination reason: Instruction limit
% 37.85/6.08 % (2915249)Termination phase: Saturation
% 37.85/6.08 % (2915249)Time elapsed: 0.391 s
% 37.85/6.08 % (2915249)Peak memory usage: 20 MB
% 37.85/6.08 % (2915249)Instructions burned: 693 (million)
% 37.85/6.08 % (2915253)fmb+10_1_sil=64000:random_seed=2960875919:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 37.85/6.08 % (2915254)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3367709577:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 37.85/6.08 % TRYING [1]
% 37.85/6.08 % TRYING [2]
% 37.85/6.08 % TRYING [20]
% 37.85/6.08 % TRYING [3]
% 37.85/6.08 % (2915245)Instruction limit reached!
% 37.85/6.08 % (2915245)------------------------------
% 37.85/6.08 % (2915245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915245)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915245)Termination reason: Instruction limit
% 37.85/6.08 % (2915245)Termination phase: Saturation
% 37.85/6.08 % (2915245)Time elapsed: 0.628 s
% 37.85/6.08 % (2915245)Peak memory usage: 21 MB
% 37.85/6.08 % (2915245)Instructions burned: 1180 (million)
% 37.85/6.08 % (2915257)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1729939871:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 37.85/6.08 % TRYING [4]
% 37.85/6.08 % TRYING [8]
% 37.85/6.08 % (2915251)Instruction limit reached!
% 37.85/6.08 % (2915251)------------------------------
% 37.85/6.08 % (2915251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915251)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915251)Termination reason: Instruction limit
% 37.85/6.08 % (2915251)Termination phase: Saturation
% 37.85/6.08 % (2915251)Time elapsed: 0.497 s
% 37.85/6.08 % (2915251)Peak memory usage: 20 MB
% 37.85/6.08 % (2915251)Instructions burned: 881 (million)
% 37.85/6.08 % (2915259)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1107928602:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 37.85/6.08 % TRYING [5]
% 37.85/6.08 % (2915257)Instruction limit reached!
% 37.85/6.08 % (2915257)------------------------------
% 37.85/6.08 % (2915257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915257)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915257)Termination reason: Instruction limit
% 37.85/6.08 % (2915257)Termination phase: Finite model building constraint generation
% 37.85/6.08 % (2915257)Time elapsed: 0.307 s
% 37.85/6.08 % (2915257)Peak memory usage: 56 MB
% 37.85/6.08 % (2915257)Instructions burned: 921 (million)
% 37.85/6.08 % (2915261)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=763971735:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 37.85/6.08 % TRYING [6]
% 37.85/6.08 % TRYING [7]
% 37.85/6.08 % (2915261)Instruction limit reached!
% 37.85/6.08 % (2915261)------------------------------
% 37.85/6.08 % (2915261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915261)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915261)Termination reason: Instruction limit
% 37.85/6.08 % (2915261)Termination phase: Saturation
% 37.85/6.08 % (2915261)Time elapsed: 0.879 s
% 37.85/6.08 % (2915261)Peak memory usage: 32 MB
% 37.85/6.08 % (2915261)Instructions burned: 1473 (million)
% 37.85/6.08 % (2915263)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1547865087:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 37.85/6.08 % (2915263)Cannot represent all propositional literals internally
% 37.85/6.08 % (2915263)Refutation not found, incomplete strategy
% 37.85/6.08 % (2915263)------------------------------
% 37.85/6.08 % (2915263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915263)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915263)Termination reason: Refutation not found, incomplete strategy
% 37.85/6.08 % (2915263)Time elapsed: 0.020 s
% 37.85/6.08 % (2915263)Peak memory usage: 11 MB
% 37.85/6.08 % (2915263)Instructions burned: 39 (million)
% 37.85/6.08 % (2915263)------------------------------
% 37.85/6.08 % (2915263)------------------------------
% 37.85/6.08 % (2915265)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=58303326:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 37.85/6.08 % TRYING [16]
% 37.85/6.08 % TRYING [7]
% 37.85/6.08 % (2915265)Instruction limit reached!
% 37.85/6.08 % (2915265)------------------------------
% 37.85/6.08 % (2915265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915265)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915265)Termination reason: Instruction limit
% 37.85/6.08 % (2915265)Termination phase: Finite model building constraint generation
% 37.85/6.08 % (2915265)Time elapsed: 0.769 s
% 37.85/6.08 % (2915265)Peak memory usage: 126 MB
% 37.85/6.08 % (2915265)Instructions burned: 2175 (million)
% 37.85/6.08 % (2915267)ott-2_1_sil=16000:newcnf=on:random_seed=4110197937:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi)
% 37.85/6.08 % (2915267)Instruction limit reached!
% 37.85/6.08 % (2915267)------------------------------
% 37.85/6.08 % (2915267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915267)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915267)Termination reason: Instruction limit
% 37.85/6.08 % (2915267)Termination phase: Saturation
% 37.85/6.08 % (2915267)Time elapsed: 0.447 s
% 37.85/6.08 % (2915267)Peak memory usage: 15 MB
% 37.85/6.08 % (2915267)Instructions burned: 869 (million)
% 37.85/6.08 % (2915269)ott+10_1_sil=32000:tgt=ground:random_seed=2964375473:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 37.85/6.08 % (2915259)Instruction limit reached!
% 37.85/6.08 % (2915259)------------------------------
% 37.85/6.08 % (2915259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915259)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915259)Termination reason: Instruction limit
% 37.85/6.08 % (2915259)Termination phase: Saturation
% 37.85/6.08 % (2915259)Time elapsed: 3.019 s
% 37.85/6.08 % (2915259)Peak memory usage: 35 MB
% 37.85/6.08 % (2915259)Instructions burned: 5131 (million)
% 37.85/6.08 % (2915271)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2568333208:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 37.85/6.08 % TRYING [1]
% 37.85/6.08 % TRYING [2]
% 37.85/6.08 % TRYING [3]
% 37.85/6.08 % TRYING [4]
% 37.85/6.08 % (2915254)Instruction limit reached!
% 37.85/6.08 % (2915254)------------------------------
% 37.85/6.08 % (2915254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915254)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915254)Termination reason: Instruction limit
% 37.85/6.08 % (2915254)Termination phase: Finite model building constraint generation
% 37.85/6.08 % (2915254)Time elapsed: 3.300 s
% 37.85/6.08 % (2915254)Peak memory usage: 553 MB
% 37.85/6.08 % (2915254)Instructions burned: 9517 (million)
% 37.85/6.08 % (2915273)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4104811930:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 37.85/6.08 % TRYING [5]
% 37.85/6.08 % TRYING [6]
% 37.85/6.08 % TRYING [8]
% 37.85/6.08 % TRYING [8]
% 37.85/6.08 % (2915269) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2915214-2915269"...
% 37.85/6.08 % (2915269)...printing done.
% 37.85/6.08 % (2915269)Refutation found. Thanks to Tanya!
% 37.85/6.08 % SZS status Theorem for theBenchmark
% 37.85/6.08 % SZS output start Proof for theBenchmark
% See solution above
% 37.85/6.08 % (2915269)------------------------------
% 37.85/6.08 % (2915269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/6.08 % (2915269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.08 % (2915269)CaDiCaL version: 2.1.3
% 37.85/6.08 % (2915269)Termination reason: Refutation
% 37.85/6.08 % (2915269)Time elapsed: 1.995 s
% 37.85/6.08 % (2915269)Peak memory usage: 44 MB
% 37.85/6.08 % (2915269)Instructions burned: 3303 (million)
% 37.85/6.08 % (2915214)Success in time 5.679 s
% 37.85/6.08 % Vampire exiting
%------------------------------------------------------------------------------