%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM588+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 : n010.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:55 PM UTC 2026
% Result : Theorem 5.01s 1.17s
% Output : Refutation 5.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 32
% Syntax : Number of formulae : 216 ( 44 unt; 18 def)
% Number of atoms : 819 ( 118 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1000 ( 397 ~; 400 |; 149 &)
% ( 33 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 15 con; 0-3 aty)
% Number of variables : 238 ( 0 sgn 220 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
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(f41,axiom,
! [X0] :
( aSet0(X0)
=> ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardNum) ).
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(f57,axiom,
! [X0,X1] :
( ( aSet0(X0)
& aElementOf0(X1,szNzAzT0) )
=> ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSel) ).
fof(f80,axiom,
( aElementOf0(xk,szNzAzT0)
& szszuzczcdt0(xk) = xK ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3533) ).
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(f86,axiom,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aFunction0(sdtlpdtrp0(xC,X0))
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( ( aSet0(X1)
& aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4151) ).
fof(f88,conjecture,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(X1) )
=> ! [X2] :
( ( aSet0(X2)
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
=> aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f89,negated_conjecture,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( ( aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(X1) )
=> ! [X2] :
( ( aSet0(X2)
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
=> aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) ) ),
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f97,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f99,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f100,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isCountable0(X0) ),
inference(flattening,[],[f99]) ).
fof(f103,plain,
! [X0] :
( ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) ) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f109,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f110,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(flattening,[],[f109]) ).
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(ennf_transformation,[],[f16]) ).
fof(f114,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,[],[f113]) ).
fof(f146,plain,
! [X0] :
( ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f156,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(f157,plain,
! [X0] :
( ! [X1] :
( X1 = szmzizndt0(X0)
<=> ( aElementOf0(X1,X0)
& ! [X2] :
( sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,X0) ) ) )
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(flattening,[],[f156]) ).
fof(f171,plain,
! [X0,X1] :
( ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f57]) ).
fof(f172,plain,
! [X0,X1] :
( ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f171]) ).
fof(f200,plain,
! [X0] :
( ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f207,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSet0(X1)
| ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f86]) ).
fof(f208,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSet0(X1)
| ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(flattening,[],[f207]) ).
fof(f210,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& aSet0(X2)
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(X1) )
& aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f211,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
& aSet0(X2)
& aElementOf0(X2,slbdtsldtrb0(X1,xk)) )
& aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(X1) )
& aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f210]) ).
fof(f215,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(f216,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(f217,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f114,f216,f215]) ).
fof(f222,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,[],[f103]) ).
fof(f223,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,[],[f222]) ).
fof(f224,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,[],[f223]) ).
fof(f225,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))],[f224]) ).
fof(f232,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,[],[f216]) ).
fof(f233,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,[],[f232]) ).
fof(f234,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,[],[f215]) ).
fof(f235,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,[],[f234]) ).
fof(f236,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,[],[f235]) ).
fof(f237,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))],[f236]) ).
fof(f240,plain,
! [X0] :
( ( ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ isFinite0(X0) )
& ( isFinite0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0) ) )
| ~ aSet0(X0) ),
inference(nnf_transformation,[],[f146]) ).
fof(f243,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,[],[f157]) ).
fof(f244,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,[],[f243]) ).
fof(f245,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,[],[f244]) ).
fof(f246,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))],[f245]) ).
fof(f259,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = slbdtsldtrb0(X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aSubsetOf0(X3,X0)
| sbrdtbr0(X3) != X1
| ~ aElementOf0(X3,X2) )
& ( ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aSubsetOf0(X3,X0)
| sbrdtbr0(X3) != X1 )
& ( ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 )
| ~ aElementOf0(X3,X2) ) ) )
| slbdtsldtrb0(X0,X1) != X2 ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(nnf_transformation,[],[f172]) ).
fof(f260,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = slbdtsldtrb0(X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aSubsetOf0(X3,X0)
| sbrdtbr0(X3) != X1
| ~ aElementOf0(X3,X2) )
& ( ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aSubsetOf0(X3,X0)
| sbrdtbr0(X3) != X1 )
& ( ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 )
| ~ aElementOf0(X3,X2) ) ) )
| slbdtsldtrb0(X0,X1) != X2 ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f259]) ).
fof(f261,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = slbdtsldtrb0(X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aSubsetOf0(X3,X0)
| sbrdtbr0(X3) != X1
| ~ aElementOf0(X3,X2) )
& ( ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X4] :
( ( aElementOf0(X4,X2)
| ~ aSubsetOf0(X4,X0)
| sbrdtbr0(X4) != X1 )
& ( ( aSubsetOf0(X4,X0)
& sbrdtbr0(X4) = X1 )
| ~ aElementOf0(X4,X2) ) ) )
| slbdtsldtrb0(X0,X1) != X2 ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(rectify,[],[f260]) ).
fof(f262,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = slbdtsldtrb0(X0,X1)
| ~ aSet0(X2)
| ( ( ~ aSubsetOf0(sK14(X0,X1,X2),X0)
| sbrdtbr0(sK14(X0,X1,X2)) != X1
| ~ aElementOf0(sK14(X0,X1,X2),X2) )
& ( ( aSubsetOf0(sK14(X0,X1,X2),X0)
& sbrdtbr0(sK14(X0,X1,X2)) = X1 )
| aElementOf0(sK14(X0,X1,X2),X2) ) ) )
& ( ( aSet0(X2)
& ! [X4] :
( ( aElementOf0(X4,X2)
| ~ aSubsetOf0(X4,X0)
| sbrdtbr0(X4) != X1 )
& ( ( aSubsetOf0(X4,X0)
& sbrdtbr0(X4) = X1 )
| ~ aElementOf0(X4,X2) ) ) )
| slbdtsldtrb0(X0,X1) != X2 ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1,X2))],[f261]) ).
fof(f278,plain,
( ~ aElementOf0(sK27,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK25),szmzizndt0(sdtlpdtrp0(xN,sK25))),xk))
& aSet0(sK27)
& aElementOf0(sK27,slbdtsldtrb0(sK26,xk))
& aSubsetOf0(sK26,sdtmndt0(sdtlpdtrp0(xN,sK25),szmzizndt0(sdtlpdtrp0(xN,sK25))))
& isCountable0(sK26)
& aElementOf0(sK25,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27]),skolemize(X0,sK25),skolemize(X1,sK26),skolemize(X2,sK27)],[f211]) ).
fof(f279,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f283,plain,
isFinite0(slcrc0),
inference(cnf_transformation,[],[f6]) ).
fof(f284,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f287,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,X0)
| aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f225]) ).
fof(f293,plain,
! [X2,X0,X1] :
( ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| aSubsetOf0(X0,X2)
| ~ aSet0(X0)
| ~ aSet0(X1)
| ~ aSet0(X2) ),
inference(cnf_transformation,[],[f110]) ).
fof(f306,plain,
! [X2,X0,X1] :
( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f233]) ).
fof(f312,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f317,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| sP3(X1,X0) ),
inference(cnf_transformation,[],[f217]) ).
fof(f325,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f344,plain,
! [X0] :
( isFinite0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f240]) ).
fof(f345,plain,
! [X0] :
( aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f240]) ).
fof(f354,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| szmzizndt0(X0) != X1
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(cnf_transformation,[],[f246]) ).
fof(f379,plain,
! [X2,X0,X1,X4] :
( sbrdtbr0(X4) = X1
| ~ aElementOf0(X4,X2)
| slbdtsldtrb0(X0,X1) != X2
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f262]) ).
fof(f380,plain,
! [X2,X0,X1,X4] :
( aSubsetOf0(X4,X0)
| ~ aElementOf0(X4,X2)
| slbdtsldtrb0(X0,X1) != X2
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f262]) ).
fof(f381,plain,
! [X2,X0,X1,X4] :
( aElementOf0(X4,X2)
| ~ aSubsetOf0(X4,X0)
| sbrdtbr0(X4) != X1
| slbdtsldtrb0(X0,X1) != X2
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f262]) ).
fof(f437,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[],[f80]) ).
fof(f443,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f444,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f451,plain,
szNzAzT0 = szDzozmdt0(xC),
inference(cnf_transformation,[],[f208]) ).
fof(f454,plain,
aElementOf0(sK25,szNzAzT0),
inference(cnf_transformation,[],[f278]) ).
fof(f456,plain,
aSubsetOf0(sK26,sdtmndt0(sdtlpdtrp0(xN,sK25),szmzizndt0(sdtlpdtrp0(xN,sK25)))),
inference(cnf_transformation,[],[f278]) ).
fof(f457,plain,
aElementOf0(sK27,slbdtsldtrb0(sK26,xk)),
inference(cnf_transformation,[],[f278]) ).
fof(f458,plain,
aSet0(sK27),
inference(cnf_transformation,[],[f278]) ).
fof(f459,plain,
~ aElementOf0(sK27,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK25),szmzizndt0(sdtlpdtrp0(xN,sK25))),xk)),
inference(cnf_transformation,[],[f278]) ).
fof(f465,plain,
! [X0,X1] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ sP3(X0,X1) ),
inference(equality_resolution,[],[f306]) ).
fof(f468,plain,
! [X0] :
( aElementOf0(szmzizndt0(X0),X0)
| ~ aSubsetOf0(X0,szNzAzT0)
| slcrc0 = X0 ),
inference(equality_resolution,[],[f354]) ).
fof(f478,plain,
! [X2,X0,X4] :
( aElementOf0(X4,X2)
| ~ aSubsetOf0(X4,X0)
| slbdtsldtrb0(X0,sbrdtbr0(X4)) != X2
| ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(X4),szNzAzT0) ),
inference(equality_resolution,[],[f381]) ).
fof(f479,plain,
! [X0,X4] :
( aElementOf0(X4,slbdtsldtrb0(X0,sbrdtbr0(X4)))
| ~ aSubsetOf0(X4,X0)
| ~ aSet0(X0)
| ~ aElementOf0(sbrdtbr0(X4),szNzAzT0) ),
inference(equality_resolution,[],[f478]) ).
fof(f480,plain,
! [X0,X1,X4] :
( aSubsetOf0(X4,X0)
| ~ aElementOf0(X4,slbdtsldtrb0(X0,X1))
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(equality_resolution,[],[f380]) ).
fof(f481,plain,
! [X0,X1,X4] :
( sbrdtbr0(X4) = X1
| ~ aElementOf0(X4,slbdtsldtrb0(X0,X1))
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(equality_resolution,[],[f379]) ).
fof(f497,definition,
sF28 = sdtlpdtrp0(xN,sK25),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f498,plain,
sdtlpdtrp0(xN,sK25) = sF28,
inference(reorient_equations,[],[f497]) ).
fof(f499,definition,
sF29 = szmzizndt0(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f500,plain,
szmzizndt0(sF28) = sF29,
inference(reorient_equations,[],[f499]) ).
fof(f501,definition,
sF30 = sdtmndt0(sF28,sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f502,plain,
sdtmndt0(sF28,sF29) = sF30,
inference(reorient_equations,[],[f501]) ).
fof(f503,definition,
sF31 = slbdtsldtrb0(sF30,xk),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f504,plain,
slbdtsldtrb0(sF30,xk) = sF31,
inference(reorient_equations,[],[f503]) ).
fof(f505,plain,
~ aElementOf0(sK27,sF31),
inference(definition_folding,[],[f459,f504,f502,f500,f498,f498]) ).
fof(f506,definition,
sF32 = slbdtsldtrb0(sK26,xk),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f507,plain,
slbdtsldtrb0(sK26,xk) = sF32,
inference(reorient_equations,[],[f506]) ).
fof(f508,plain,
aElementOf0(sK27,sF32),
inference(definition_folding,[],[f457,f507]) ).
fof(f509,plain,
aSubsetOf0(sK26,sF30),
inference(definition_folding,[],[f456,f502,f500,f498,f498]) ).
fof(f514,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xC))
| isCountable0(sdtlpdtrp0(xN,X0)) ),
inference(forward_demodulation,[],[f443,f451]) ).
fof(f515,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szDzozmdt0(xC))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_demodulation,[],[f444,f451]) ).
fof(f519,plain,
aElementOf0(xk,szDzozmdt0(xC)),
inference(forward_demodulation,[],[f437,f451]) ).
fof(f533,plain,
! [X0,X1,X4] :
( ~ aElementOf0(X4,slbdtsldtrb0(X0,X1))
| sbrdtbr0(X4) = X1
| ~ aElementOf0(X1,szDzozmdt0(xC))
| ~ aSet0(X0) ),
inference(forward_demodulation,[],[f481,f451]) ).
fof(f534,plain,
! [X0,X1,X4] :
( ~ aElementOf0(X4,slbdtsldtrb0(X0,X1))
| aSubsetOf0(X4,X0)
| ~ aElementOf0(X1,szDzozmdt0(xC))
| ~ aSet0(X0) ),
inference(forward_demodulation,[],[f480,f451]) ).
fof(f535,plain,
! [X0,X4] :
( ~ aElementOf0(sbrdtbr0(X4),szDzozmdt0(xC))
| aElementOf0(X4,slbdtsldtrb0(X0,sbrdtbr0(X4)))
| ~ aSubsetOf0(X4,X0)
| ~ aSet0(X0) ),
inference(forward_demodulation,[],[f479,f451]) ).
fof(f562,plain,
! [X0] :
( ~ aSubsetOf0(X0,szDzozmdt0(xC))
| aElementOf0(szmzizndt0(X0),X0)
| slcrc0 = X0 ),
inference(forward_demodulation,[],[f468,f451]) ).
fof(f576,plain,
! [X0] :
( ~ aElementOf0(sbrdtbr0(X0),szDzozmdt0(xC))
| isFinite0(X0)
| ~ aSet0(X0) ),
inference(forward_demodulation,[],[f344,f451]) ).
fof(f577,plain,
! [X0] :
( aElementOf0(sbrdtbr0(X0),szDzozmdt0(xC))
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(forward_demodulation,[],[f345,f451]) ).
fof(f596,plain,
aSet0(szDzozmdt0(xC)),
inference(forward_demodulation,[],[f325,f451]) ).
fof(f606,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szDzozmdt0(xC))
| ~ aElementOf0(X0,szDzozmdt0(xC)) ),
inference(forward_demodulation,[],[f515,f451]) ).
fof(f636,plain,
aElementOf0(sK25,szDzozmdt0(xC)),
inference(superposition,[],[f454,f451]) ).
fof(f664,definition,
( spl33_7
<=> aSet0(sK26) ),
introduced(definition,[new_symbols(definition,[spl33_7])],[avatar_definition]) ).
fof(f665,plain,
( aSet0(sK26)
| ~ spl33_7 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f666,plain,
( ~ aSet0(sK26)
| spl33_7 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f726,plain,
( aSet0(sK26)
| ~ aSet0(sF30) ),
inference(resolution,[],[f287,f509]) ).
fof(f728,plain,
( ~ aSet0(sF30)
| spl33_7 ),
inference(forward_subsumption_resolution,[],[f726,f666]) ).
fof(f754,plain,
isCountable0(sdtlpdtrp0(xN,sK25)),
inference(resolution,[],[f514,f636]) ).
fof(f755,plain,
isCountable0(sF28),
inference(forward_demodulation,[],[f754,f498]) ).
fof(f758,plain,
( ~ aSet0(sF28)
| ~ isFinite0(sF28) ),
inference(resolution,[],[f755,f284]) ).
fof(f760,definition,
( spl33_10
<=> isFinite0(sF28) ),
introduced(definition,[new_symbols(definition,[spl33_10])],[avatar_definition]) ).
fof(f762,plain,
( ~ isFinite0(sF28)
| spl33_10 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f764,definition,
( spl33_11
<=> aSet0(sF28) ),
introduced(definition,[new_symbols(definition,[spl33_11])],[avatar_definition]) ).
fof(f765,plain,
( aSet0(sF28)
| ~ spl33_11 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f767,plain,
( ~ spl33_10
| ~ spl33_11 ),
inference(avatar_split_clause,[],[f758,f764,f760]) ).
fof(f975,plain,
( sP2(sF30,sF28,sF29)
| ~ sP3(sF29,sF28) ),
inference(superposition,[],[f465,f502]) ).
fof(f977,definition,
( spl33_28
<=> sP3(sF29,sF28) ),
introduced(definition,[new_symbols(definition,[spl33_28])],[avatar_definition]) ).
fof(f979,plain,
( ~ sP3(sF29,sF28)
| spl33_28 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f981,definition,
( spl33_29
<=> sP2(sF30,sF28,sF29) ),
introduced(definition,[new_symbols(definition,[spl33_29])],[avatar_definition]) ).
fof(f983,plain,
( sP2(sF30,sF28,sF29)
| ~ spl33_29 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f984,plain,
( ~ spl33_28
| spl33_29 ),
inference(avatar_split_clause,[],[f975,f981,f977]) ).
fof(f1006,plain,
( aSubsetOf0(sF28,szDzozmdt0(xC))
| ~ aElementOf0(sK25,szDzozmdt0(xC)) ),
inference(superposition,[],[f606,f498]) ).
fof(f1007,plain,
aSubsetOf0(sF28,szDzozmdt0(xC)),
inference(forward_subsumption_resolution,[],[f1006,f636]) ).
fof(f1023,plain,
( aSet0(sF28)
| ~ aSet0(szDzozmdt0(xC)) ),
inference(resolution,[],[f1007,f287]) ).
fof(f1024,plain,
aSet0(sF28),
inference(forward_subsumption_resolution,[],[f1023,f596]) ).
fof(f1025,plain,
spl33_11,
inference(avatar_split_clause,[],[f1024,f764]) ).
fof(f1036,definition,
( spl33_30
<=> aElement0(sF29) ),
introduced(definition,[new_symbols(definition,[spl33_30])],[avatar_definition]) ).
fof(f1037,plain,
( aElement0(sF29)
| ~ spl33_30 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1038,plain,
( ~ aElement0(sF29)
| spl33_30 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1122,plain,
( aElementOf0(szmzizndt0(sF28),sF28)
| slcrc0 = sF28 ),
inference(resolution,[],[f562,f1007]) ).
fof(f1123,plain,
( aElementOf0(sF29,sF28)
| slcrc0 = sF28 ),
inference(forward_demodulation,[],[f1122,f500]) ).
fof(f1136,definition,
( spl33_34
<=> slcrc0 = sF28 ),
introduced(definition,[new_symbols(definition,[spl33_34])],[avatar_definition]) ).
fof(f1138,plain,
( slcrc0 = sF28
| ~ spl33_34 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1140,definition,
( spl33_35
<=> aElementOf0(sF29,sF28) ),
introduced(definition,[new_symbols(definition,[spl33_35])],[avatar_definition]) ).
fof(f1142,plain,
( aElementOf0(sF29,sF28)
| ~ spl33_35 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1143,plain,
( spl33_34
| spl33_35 ),
inference(avatar_split_clause,[],[f1123,f1140,f1136]) ).
fof(f1148,plain,
( ~ isFinite0(slcrc0)
| spl33_10
| ~ spl33_34 ),
inference(superposition,[],[f762,f1138]) ).
fof(f1156,plain,
( $false
| spl33_10
| ~ spl33_34 ),
inference(forward_subsumption_resolution,[],[f1148,f283]) ).
fof(f1157,plain,
( spl33_10
| ~ spl33_34 ),
inference(avatar_contradiction_clause,[],[f1156]) ).
fof(f1179,plain,
( aElement0(sF29)
| ~ aSet0(sF28)
| ~ spl33_35 ),
inference(resolution,[],[f1142,f279]) ).
fof(f1180,plain,
( ~ aSet0(sF28)
| spl33_30
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f1179,f1038]) ).
fof(f1181,plain,
( $false
| ~ spl33_11
| spl33_30
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f1180,f765]) ).
fof(f1182,plain,
( ~ spl33_11
| spl33_30
| ~ spl33_35 ),
inference(avatar_contradiction_clause,[],[f1181]) ).
fof(f1194,plain,
( ! [X0] :
( ~ aSet0(X0)
| sP3(sF29,X0) )
| ~ spl33_30 ),
inference(resolution,[],[f1037,f317]) ).
fof(f1284,plain,
( sP3(sF29,sF28)
| ~ spl33_11
| ~ spl33_30 ),
inference(resolution,[],[f1194,f765]) ).
fof(f1285,plain,
( $false
| ~ spl33_11
| spl33_28
| ~ spl33_30 ),
inference(forward_subsumption_resolution,[],[f1284,f979]) ).
fof(f1286,plain,
( ~ spl33_11
| spl33_28
| ~ spl33_30 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
fof(f1495,plain,
! [X0] :
( ~ aElementOf0(X0,sF32)
| aSubsetOf0(X0,sK26)
| ~ aElementOf0(xk,szDzozmdt0(xC))
| ~ aSet0(sK26) ),
inference(superposition,[],[f534,f507]) ).
fof(f1643,plain,
! [X0] :
( ~ aElementOf0(X0,sF32)
| sbrdtbr0(X0) = xk
| ~ aElementOf0(xk,szDzozmdt0(xC))
| ~ aSet0(sK26) ),
inference(superposition,[],[f533,f507]) ).
fof(f1676,plain,
! [X0] :
( ~ aSubsetOf0(X0,sK26)
| aSubsetOf0(X0,sF30)
| ~ aSet0(X0)
| ~ aSet0(sK26)
| ~ aSet0(sF30) ),
inference(resolution,[],[f293,f509]) ).
fof(f1783,plain,
! [X0,X1] :
( aElementOf0(X0,slbdtsldtrb0(X1,sbrdtbr0(X0)))
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(resolution,[],[f535,f577]) ).
fof(f1788,plain,
! [X0,X1] :
( ~ aSubsetOf0(X0,X1)
| aElementOf0(X0,slbdtsldtrb0(X1,sbrdtbr0(X0)))
| ~ aSet0(X1)
| ~ isFinite0(X0) ),
inference(forward_subsumption_resolution,[],[f1783,f287]) ).
fof(f4781,plain,
( aSet0(sF30)
| ~ spl33_29 ),
inference(resolution,[],[f983,f312]) ).
fof(f4782,plain,
( $false
| spl33_7
| ~ spl33_29 ),
inference(forward_subsumption_resolution,[],[f4781,f728]) ).
fof(f4783,plain,
( spl33_7
| ~ spl33_29 ),
inference(avatar_contradiction_clause,[],[f4782]) ).
fof(f4786,definition,
( spl33_143
<=> aSet0(sF30) ),
introduced(definition,[new_symbols(definition,[spl33_143])],[avatar_definition]) ).
fof(f4787,plain,
( aSet0(sF30)
| ~ spl33_143 ),
inference(avatar_component_clause,[],[f4786]) ).
fof(f4806,plain,
! [X0] :
( ~ aElementOf0(X0,sF32)
| aSubsetOf0(X0,sK26)
| ~ aSet0(sK26) ),
inference(forward_subsumption_resolution,[],[f1495,f519]) ).
fof(f4808,plain,
! [X0] :
( ~ aElementOf0(X0,sF32)
| sbrdtbr0(X0) = xk
| ~ aSet0(sK26) ),
inference(forward_subsumption_resolution,[],[f1643,f519]) ).
fof(f4810,plain,
( ! [X0] :
( ~ aSubsetOf0(X0,sK26)
| aSubsetOf0(X0,sF30)
| ~ aSet0(X0)
| ~ aSet0(sF30) )
| ~ spl33_7 ),
inference(forward_subsumption_resolution,[],[f1676,f665]) ).
fof(f4841,plain,
( spl33_143
| ~ spl33_29 ),
inference(avatar_split_clause,[],[f4781,f981,f4786]) ).
fof(f4846,plain,
( ! [X0] :
( ~ aElementOf0(X0,sF32)
| aSubsetOf0(X0,sK26) )
| ~ spl33_7 ),
inference(forward_subsumption_resolution,[],[f4806,f665]) ).
fof(f4851,plain,
( ! [X0] :
( ~ aElementOf0(X0,sF32)
| sbrdtbr0(X0) = xk )
| ~ spl33_7 ),
inference(forward_subsumption_resolution,[],[f4808,f665]) ).
fof(f4857,definition,
( spl33_153
<=> ! [X0] :
( ~ aSubsetOf0(X0,sK26)
| ~ aSet0(X0)
| aSubsetOf0(X0,sF30) ) ),
introduced(definition,[new_symbols(definition,[spl33_153])],[avatar_definition]) ).
fof(f4858,plain,
( ! [X0] :
( ~ aSubsetOf0(X0,sK26)
| ~ aSet0(X0)
| aSubsetOf0(X0,sF30) )
| ~ spl33_153 ),
inference(avatar_component_clause,[],[f4857]) ).
fof(f4859,plain,
( ~ spl33_143
| spl33_153
| ~ spl33_7 ),
inference(avatar_split_clause,[],[f4810,f664,f4857,f4786]) ).
fof(f5090,plain,
( aSubsetOf0(sK27,sK26)
| ~ spl33_7 ),
inference(resolution,[],[f4846,f508]) ).
fof(f5105,plain,
( xk = sbrdtbr0(sK27)
| ~ spl33_7 ),
inference(resolution,[],[f4851,f508]) ).
fof(f5134,plain,
( ~ aSet0(sK27)
| aSubsetOf0(sK27,sF30)
| ~ spl33_7
| ~ spl33_153 ),
inference(resolution,[],[f4858,f5090]) ).
fof(f5137,plain,
( aSubsetOf0(sK27,sF30)
| ~ spl33_7
| ~ spl33_153 ),
inference(forward_subsumption_resolution,[],[f5134,f458]) ).
fof(f5664,definition,
( spl33_217
<=> isFinite0(sK27) ),
introduced(definition,[new_symbols(definition,[spl33_217])],[avatar_definition]) ).
fof(f5665,plain,
( isFinite0(sK27)
| ~ spl33_217 ),
inference(avatar_component_clause,[],[f5664]) ).
fof(f5758,plain,
( ~ aElementOf0(xk,szDzozmdt0(xC))
| isFinite0(sK27)
| ~ aSet0(sK27)
| ~ spl33_7 ),
inference(superposition,[],[f576,f5105]) ).
fof(f5759,plain,
( isFinite0(sK27)
| ~ aSet0(sK27)
| ~ spl33_7 ),
inference(forward_subsumption_resolution,[],[f5758,f519]) ).
fof(f5763,plain,
( isFinite0(sK27)
| ~ spl33_7 ),
inference(forward_subsumption_resolution,[],[f5759,f458]) ).
fof(f5769,plain,
( spl33_217
| ~ spl33_7 ),
inference(avatar_split_clause,[],[f5763,f664,f5664]) ).
fof(f12133,plain,
( aElementOf0(sK27,slbdtsldtrb0(sF30,sbrdtbr0(sK27)))
| ~ aSet0(sF30)
| ~ isFinite0(sK27)
| ~ spl33_7
| ~ spl33_153 ),
inference(resolution,[],[f1788,f5137]) ).
fof(f12144,plain,
( aElementOf0(sK27,slbdtsldtrb0(sF30,sbrdtbr0(sK27)))
| ~ isFinite0(sK27)
| ~ spl33_7
| ~ spl33_143
| ~ spl33_153 ),
inference(forward_subsumption_resolution,[],[f12133,f4787]) ).
fof(f12163,plain,
( aElementOf0(sK27,slbdtsldtrb0(sF30,sbrdtbr0(sK27)))
| ~ spl33_7
| ~ spl33_143
| ~ spl33_153
| ~ spl33_217 ),
inference(forward_subsumption_resolution,[],[f12144,f5665]) ).
fof(f12174,plain,
( aElementOf0(sK27,slbdtsldtrb0(sF30,xk))
| ~ spl33_7
| ~ spl33_143
| ~ spl33_153
| ~ spl33_217 ),
inference(forward_demodulation,[],[f12163,f5105]) ).
fof(f12183,plain,
( aElementOf0(sK27,sF31)
| ~ spl33_7
| ~ spl33_143
| ~ spl33_153
| ~ spl33_217 ),
inference(forward_demodulation,[],[f12174,f504]) ).
fof(f12197,plain,
( $false
| ~ spl33_7
| ~ spl33_143
| ~ spl33_153
| ~ spl33_217 ),
inference(forward_subsumption_resolution,[],[f12183,f505]) ).
fof(f12198,plain,
( ~ spl33_7
| ~ spl33_143
| ~ spl33_153
| ~ spl33_217 ),
inference(avatar_contradiction_clause,[],[f12197]) ).
cnf(s8,plain,
( ~ spl33_10
| ~ spl33_11 ),
inference(sat_conversion,[],[f767]) ).
cnf(s22,plain,
( ~ spl33_28
| spl33_29 ),
inference(sat_conversion,[],[f984]) ).
cnf(s25,plain,
spl33_11,
inference(sat_conversion,[],[f1025]) ).
cnf(s28,plain,
( spl33_34
| spl33_35 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s29,plain,
( spl33_10
| ~ spl33_34 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s31,plain,
( ~ spl33_11
| spl33_30
| ~ spl33_35 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s34,plain,
( ~ spl33_11
| spl33_28
| ~ spl33_30 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s121,plain,
( spl33_7
| ~ spl33_29 ),
inference(sat_conversion,[],[f4783]) ).
cnf(s129,plain,
( ~ spl33_29
| spl33_143 ),
inference(sat_conversion,[],[f4841]) ).
cnf(s134,plain,
( ~ spl33_7
| ~ spl33_143
| spl33_153 ),
inference(sat_conversion,[],[f4859]) ).
cnf(s199,plain,
( ~ spl33_7
| spl33_217 ),
inference(sat_conversion,[],[f5769]) ).
cnf(s386,plain,
( ~ spl33_7
| ~ spl33_143
| ~ spl33_153
| ~ spl33_217 ),
inference(sat_conversion,[],[f12198]) ).
cnf(s432,plain,
~ spl33_10,
inference(rat,[],[s8,s25]) ).
cnf(s433,plain,
~ spl33_34,
inference(rat,[],[s29,s432]) ).
cnf(s434,plain,
spl33_35,
inference(rat,[],[s28,s433]) ).
cnf(s435,plain,
spl33_30,
inference(rat,[],[s31,s25,s434]) ).
cnf(s437,plain,
spl33_28,
inference(rat,[],[s34,s25,s435]) ).
cnf(s438,plain,
spl33_29,
inference(rat,[],[s22,s437]) ).
cnf(s439,plain,
spl33_143,
inference(rat,[],[s129,s438]) ).
cnf(s440,plain,
spl33_7,
inference(rat,[],[s121,s438]) ).
cnf(s450,plain,
spl33_217,
inference(rat,[],[s199,s440]) ).
cnf(s451,plain,
spl33_153,
inference(rat,[],[s134,s439,s440]) ).
cnf(s476,plain,
$false,
inference(rat,[],[s386,s440,s439,s450,s451]) ).
fof(f12202,plain,
$false,
inference(avatar_sat_refutation,[],[s476]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM588+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n010.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 20:38:32 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.39 Running first-order model finding
% 0.09/0.39 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
% 5.01/1.17 % (1290574)Will run a generic schedule for satisfiability detection.
% 5.01/1.17 % (1290581)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3089006556:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.01/1.17 % (1290579)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1182270496_2999 on theBenchmark for (2999ds/0Mi)
% 5.01/1.17 % (1290582)dis+10_1_sil=32000:sp=arity:random_seed=1462068175:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.01/1.17 % (1290583)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2132728722:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.01/1.17 % (1290584)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1005631752:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.01/1.17 % (1290585)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=490333269:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.01/1.17 % (1290580)% WARNING: option uhcvi not known.
% 5.01/1.17 % (1290580)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1928478914:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.01/1.17 % TRYING [1]
% 5.01/1.17 % TRYING [2]
% 5.01/1.17 % TRYING [3]
% 5.01/1.17 % TRYING [4]
% 5.01/1.17 % (1290582)Instruction limit reached!
% 5.01/1.17 % (1290582)------------------------------
% 5.01/1.17 % (1290582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290582)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290582)Termination reason: Instruction limit
% 5.01/1.17 % (1290582)Termination phase: Saturation
% 5.01/1.17 % (1290582)Time elapsed: 0.067 s
% 5.01/1.17 % (1290582)Peak memory usage: 13 MB
% 5.01/1.17 % (1290582)Instructions burned: 104 (million)
% 5.01/1.17 % (1290583)Instruction limit reached!
% 5.01/1.17 % (1290583)------------------------------
% 5.01/1.17 % (1290583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290583)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290583)Termination reason: Instruction limit
% 5.01/1.17 % (1290583)Termination phase: Saturation
% 5.01/1.17 % (1290583)Time elapsed: 0.074 s
% 5.01/1.17 % (1290583)Peak memory usage: 13 MB
% 5.01/1.17 % (1290583)Instructions burned: 116 (million)
% 5.01/1.17 % (1290584)Instruction limit reached!
% 5.01/1.17 % (1290584)------------------------------
% 5.01/1.17 % (1290584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290584)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290584)Termination reason: Instruction limit
% 5.01/1.17 % (1290584)Termination phase: Saturation
% 5.01/1.17 % (1290584)Time elapsed: 0.082 s
% 5.01/1.17 % (1290584)Peak memory usage: 13 MB
% 5.01/1.17 % (1290584)Instructions burned: 132 (million)
% 5.01/1.17 % (1290593)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=587409395:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 5.01/1.17 % (1290594)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3169401726:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.01/1.17 % (1290595)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=3224206900:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.01/1.17 % TRYING [1]
% 5.01/1.17 % TRYING [2]
% 5.01/1.17 % TRYING [3]
% 5.01/1.17 % TRYING [5]
% 5.01/1.17 % (1290585)Instruction limit reached!
% 5.01/1.17 % (1290585)------------------------------
% 5.01/1.17 % (1290585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290585)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290585)Termination reason: Instruction limit
% 5.01/1.17 % (1290585)Termination phase: Saturation
% 5.01/1.17 % (1290585)Time elapsed: 0.117 s
% 5.01/1.17 % (1290585)Peak memory usage: 14 MB
% 5.01/1.17 % (1290585)Instructions burned: 160 (million)
% 5.01/1.17 % TRYING [4]
% 5.01/1.17 % (1290599)ott-21_1_sil=16000:fs=off:random_seed=52775149:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.01/1.17 % (1290594)Instruction limit reached!
% 5.01/1.17 % (1290594)------------------------------
% 5.01/1.17 % (1290594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290594)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290594)Termination reason: Instruction limit
% 5.01/1.17 % (1290594)Termination phase: Saturation
% 5.01/1.17 % (1290594)Time elapsed: 0.087 s
% 5.01/1.17 % (1290594)Peak memory usage: 13 MB
% 5.01/1.17 % (1290594)Instructions burned: 132 (million)
% 5.01/1.17 % TRYING [5]
% 5.01/1.17 % (1290601)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1824774049:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.01/1.17 % (1290599)Instruction limit reached!
% 5.01/1.17 % (1290599)------------------------------
% 5.01/1.17 % (1290599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290599)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290599)Termination reason: Instruction limit
% 5.01/1.17 % (1290599)Termination phase: Saturation
% 5.01/1.17 % (1290599)Time elapsed: 0.103 s
% 5.01/1.17 % (1290599)Peak memory usage: 13 MB
% 5.01/1.17 % (1290599)Instructions burned: 181 (million)
% 5.01/1.17 % (1290603)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=101125681:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.01/1.17 % TRYING [6]
% 5.01/1.17 % TRYING [1]
% 5.01/1.17 % TRYING [2]
% 5.01/1.17 % TRYING [3]
% 5.01/1.17 % TRYING [6]
% 5.01/1.17 % (1290593)Instruction limit reached!
% 5.01/1.17 % (1290593)------------------------------
% 5.01/1.17 % (1290593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290593)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290593)Termination reason: Instruction limit
% 5.01/1.17 % (1290593)Termination phase: Finite model building constraint generation
% 5.01/1.17 % (1290593)Time elapsed: 0.293 s
% 5.01/1.17 % (1290593)Peak memory usage: 33 MB
% 5.01/1.17 % (1290593)Instructions burned: 714 (million)
% 5.01/1.17 % TRYING [4]
% 5.01/1.17 % (1290605)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1943043668:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 5.01/1.17 % (1290595)Instruction limit reached!
% 5.01/1.17 % (1290595)------------------------------
% 5.01/1.17 % (1290595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290595)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290595)Termination reason: Instruction limit
% 5.01/1.17 % (1290595)Termination phase: Saturation
% 5.01/1.17 % (1290595)Time elapsed: 0.402 s
% 5.01/1.17 % (1290595)Peak memory usage: 19 MB
% 5.01/1.17 % (1290595)Instructions burned: 685 (million)
% 5.01/1.17 % (1290607)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=586401288:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 5.01/1.17 % (1290601)Instruction limit reached!
% 5.01/1.17 % (1290601)------------------------------
% 5.01/1.17 % (1290601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290601)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290601)Termination reason: Instruction limit
% 5.01/1.17 % (1290601)Termination phase: Saturation
% 5.01/1.17 % (1290601)Time elapsed: 0.334 s
% 5.01/1.17 % (1290601)Peak memory usage: 15 MB
% 5.01/1.17 % (1290601)Instructions burned: 477 (million)
% 5.01/1.17 % (1290609)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=1836620619: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)
% 5.01/1.17 % (1290603)Instruction limit reached!
% 5.01/1.17 % (1290603)------------------------------
% 5.01/1.17 % (1290603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290603)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290603)Termination reason: Instruction limit
% 5.01/1.17 % (1290603)Termination phase: Finite model building constraint generation
% 5.01/1.17 % (1290603)Time elapsed: 0.366 s
% 5.01/1.17 % (1290603)Peak memory usage: 22 MB
% 5.01/1.17 % (1290603)Instructions burned: 868 (million)
% 5.01/1.17 % (1290611)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=913171797:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.01/1.17 % TRYING [7]
% 5.01/1.17 % (1290605) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1290574-1290605"...
% 5.01/1.17 % (1290605)...printing done.
% 5.01/1.17 % (1290605)Refutation found. Thanks to Tanya!
% 5.01/1.17 % SZS status Theorem for theBenchmark
% 5.01/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 5.01/1.17 % (1290605)------------------------------
% 5.01/1.17 % (1290605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.01/1.17 % (1290605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.01/1.17 % (1290605)CaDiCaL version: 2.1.3
% 5.01/1.17 % (1290605)Termination reason: Refutation
% 5.01/1.17 % (1290605)Time elapsed: 0.311 s
% 5.01/1.17 % (1290605)Peak memory usage: 18 MB
% 5.01/1.17 % (1290605)Instructions burned: 487 (million)
% 5.01/1.17 % (1290574)Success in time 0.764 s
% 5.01/1.17 % Vampire exiting
%------------------------------------------------------------------------------