%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG096+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:35:30 PM UTC 2026
% Result : Theorem 86.83s 13.13s
% Output : Refutation 87.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 61
% Syntax : Number of formulae : 323 ( 69 unt; 42 def)
% Number of atoms : 913 ( 91 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1036 ( 446 ~; 443 |; 72 &)
% ( 45 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 43 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 169 ( 0 sgn 160 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aElement0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC) ).
fof(f3,axiom,
aElement0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f4,axiom,
! [X0] :
( aElement0(X0)
=> aElement0(smndt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsU) ).
fof(f6,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> aElement0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f7,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
fof(f8,axiom,
! [X0,X1,X2] :
( ( aElement0(X0)
& aElement0(X1)
& aElement0(X2) )
=> sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddAsso) ).
fof(f9,axiom,
! [X0] :
( aElement0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(f10,axiom,
! [X0] :
( aElement0(X0)
=> ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddInvr) ).
fof(f11,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aElement0(X0)
& aElement0(X1)
& aElement0(X2) )
=> ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAMDistr) ).
fof(f15,axiom,
! [X0] :
( aElement0(X0)
=> ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulMnOne) ).
fof(f16,axiom,
! [X0] :
( aElement0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulZero) ).
fof(f20,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
fof(f24,axiom,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(sdtpldt0(X1,X2),X0) )
& ! [X2] :
( aElement0(X2)
=> aElementOf0(sdtasdt0(X2,X1),X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefIdeal) ).
fof(f28,axiom,
( aSet0(xI)
& ! [X0] :
( aElementOf0(X0,xI)
=> ( ! [X1] :
( aElementOf0(X1,xI)
=> aElementOf0(sdtpldt0(X0,X1),xI) )
& ! [X1] :
( aElement0(X1)
=> aElementOf0(sdtasdt0(X1,X0),xI) ) ) )
& aIdeal0(xI)
& aSet0(xJ)
& ! [X0] :
( aElementOf0(X0,xJ)
=> ( ! [X1] :
( aElementOf0(X1,xJ)
=> aElementOf0(sdtpldt0(X0,X1),xJ) )
& ! [X1] :
( aElement0(X1)
=> aElementOf0(sdtasdt0(X1,X0),xJ) ) ) )
& aIdeal0(xJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1205) ).
fof(f30,axiom,
( aElement0(xx)
& aElement0(xy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1217) ).
fof(f31,axiom,
( aElementOf0(xa,xI)
& aElementOf0(xb,xJ)
& sdtpldt0(xa,xb) = sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1294) ).
fof(f32,axiom,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1319) ).
fof(f33,conjecture,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f34,negated_conjecture,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f35,plain,
( aSet0(xI)
& ! [X0] :
( aElementOf0(X0,xI)
=> ( ! [X1] :
( aElementOf0(X1,xI)
=> aElementOf0(sdtpldt0(X0,X1),xI) )
& ! [X2] :
( aElement0(X2)
=> aElementOf0(sdtasdt0(X2,X0),xI) ) ) )
& aIdeal0(xI)
& aSet0(xJ)
& ! [X3] :
( aElementOf0(X3,xJ)
=> ( ! [X4] :
( aElementOf0(X4,xJ)
=> aElementOf0(sdtpldt0(X3,X4),xJ) )
& ! [X5] :
( aElement0(X5)
=> aElementOf0(sdtasdt0(X5,X3),xJ) ) ) )
& aIdeal0(xJ) ),
inference(rectify,[],[f28]) ).
fof(f36,plain,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(flattening,[],[f34]) ).
fof(f40,plain,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(sdtpldt0(X1,X2),X0) )
& ! [X3] :
( aElement0(X3)
=> aElementOf0(sdtasdt0(X3,X1),X0) ) ) ) ) ),
inference(rectify,[],[f24]) ).
fof(f41,plain,
( aSet0(xI)
& ! [X0] :
( ( ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) )
& ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) ) )
| ~ aElementOf0(X0,xI) )
& aIdeal0(xI)
& aSet0(xJ)
& ! [X3] :
( ( ! [X4] :
( aElementOf0(sdtpldt0(X3,X4),xJ)
| ~ aElementOf0(X4,xJ) )
& ! [X5] :
( aElementOf0(sdtasdt0(X5,X3),xJ)
| ~ aElement0(X5) ) )
| ~ aElementOf0(X3,xJ) )
& aIdeal0(xJ) ),
inference(ennf_transformation,[],[f35]) ).
fof(f45,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f46,plain,
! [X0,X1,X2] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(ennf_transformation,[],[f8]) ).
fof(f47,plain,
! [X0,X1,X2] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(flattening,[],[f46]) ).
fof(f48,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f49,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f48]) ).
fof(f52,plain,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) ) ),
inference(ennf_transformation,[],[f40]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) )
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) )
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(flattening,[],[f53]) ).
fof(f57,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f58,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f57]) ).
fof(f59,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f60,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f59]) ).
fof(f65,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f67,plain,
! [X0] :
( ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f68,plain,
! [X0] :
( aElement0(smndt0(X0))
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f71,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f72,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(nnf_transformation,[],[f52]) ).
fof(f76,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( ! [X5] :
( aElementOf0(sdtpldt0(X4,X5),X0)
| ~ aElementOf0(X5,X0) )
& ! [X6] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6) ) )
| ~ aElementOf0(X4,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(rectify,[],[f76]) ).
fof(f78,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ( ( ( ~ aElementOf0(sdtpldt0(sK4(X0),sK5(X0)),X0)
& aElementOf0(sK5(X0),X0) )
| ( ~ aElementOf0(sdtasdt0(sK6(X0),sK4(X0)),X0)
& aElement0(sK6(X0)) ) )
& aElementOf0(sK4(X0),X0) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( ! [X5] :
( aElementOf0(sdtpldt0(X4,X5),X0)
| ~ aElementOf0(X5,X0) )
& ! [X6] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6) ) )
| ~ aElementOf0(X4,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X1,sK4(X0)),skolemize(X2,sK5(X0)),skolemize(X3,sK6(X0))],[f77]) ).
fof(f83,plain,
aIdeal0(xJ),
inference(cnf_transformation,[],[f41]) ).
fof(f88,plain,
! [X2,X0] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2)
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[],[f41]) ).
fof(f89,plain,
! [X0,X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI)
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[],[f41]) ).
fof(f90,plain,
aSet0(xI),
inference(cnf_transformation,[],[f41]) ).
fof(f95,plain,
aElement0(xy),
inference(cnf_transformation,[],[f30]) ).
fof(f96,plain,
aElement0(xx),
inference(cnf_transformation,[],[f30]) ).
fof(f97,plain,
sz10 = sdtpldt0(xa,xb),
inference(cnf_transformation,[],[f31]) ).
fof(f98,plain,
aElementOf0(xb,xJ),
inference(cnf_transformation,[],[f31]) ).
fof(f99,plain,
aElementOf0(xa,xI),
inference(cnf_transformation,[],[f31]) ).
fof(f100,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(cnf_transformation,[],[f32]) ).
fof(f101,plain,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(cnf_transformation,[],[f36]) ).
fof(f106,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f107,plain,
! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(cnf_transformation,[],[f47]) ).
fof(f108,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f112,plain,
! [X0] :
( aSet0(X0)
| ~ aIdeal0(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f119,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(cnf_transformation,[],[f54]) ).
fof(f121,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f58]) ).
fof(f122,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f60]) ).
fof(f135,plain,
! [X0] :
( smndt0(X0) = sdtasdt0(smndt0(sz10),X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f138,plain,
aElement0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
! [X0] :
( sz00 = sdtpldt0(X0,smndt0(X0))
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f67]) ).
fof(f141,plain,
! [X0] :
( aElement0(smndt0(X0))
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f68]) ).
fof(f143,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f146,plain,
! [X0] :
( sdtpldt0(X0,sz00) = X0
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f147,plain,
aElement0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
( ~ aElementOf0(sdtpldt0(xw,sdtasdt0(smndt0(sz10),xx)),xI)
| ~ aElement0(xx) ),
inference(superposition,[],[f101,f135]) ).
fof(f158,definition,
( spl12_1
<=> aElement0(xx) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f162,definition,
( spl12_2
<=> aElementOf0(sdtpldt0(xw,sdtasdt0(smndt0(sz10),xx)),xI) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f164,plain,
( ~ aElementOf0(sdtpldt0(xw,sdtasdt0(smndt0(sz10),xx)),xI)
| spl12_2 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f165,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(avatar_split_clause,[],[f156,f162,f158]) ).
fof(f187,plain,
spl12_1,
inference(avatar_split_clause,[],[f96,f158]) ).
fof(f202,definition,
( spl12_9
<=> aElement0(smndt0(sz10)) ),
introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition]) ).
fof(f204,plain,
( ~ aElement0(smndt0(sz10))
| spl12_9 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f212,plain,
( $false
| spl12_9 ),
inference(unit_resulting_resolution,[],[f141,f138,f204]) ).
fof(f214,plain,
spl12_9,
inference(avatar_contradiction_clause,[],[f212]) ).
fof(f227,plain,
( aElement0(xb)
| ~ aSet0(xJ) ),
inference(resolution,[],[f98,f106]) ).
fof(f229,definition,
( spl12_12
<=> aSet0(xJ) ),
introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition]) ).
fof(f231,plain,
( ~ aSet0(xJ)
| spl12_12 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl12_13
<=> aElement0(xb) ),
introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition]) ).
fof(f236,plain,
( ~ spl12_12
| spl12_13 ),
inference(avatar_split_clause,[],[f227,f233,f229]) ).
fof(f238,plain,
( $false
| spl12_12 ),
inference(unit_resulting_resolution,[],[f112,f83,f231]) ).
fof(f243,plain,
spl12_12,
inference(avatar_contradiction_clause,[],[f238]) ).
fof(f244,plain,
( aElement0(xa)
| ~ aSet0(xI) ),
inference(resolution,[],[f99,f106]) ).
fof(f246,definition,
( spl12_14
<=> aSet0(xI) ),
introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition]) ).
fof(f248,plain,
( ~ aSet0(xI)
| spl12_14 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f250,definition,
( spl12_15
<=> aElement0(xa) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f253,plain,
( ~ spl12_14
| spl12_15 ),
inference(avatar_split_clause,[],[f244,f250,f246]) ).
fof(f254,plain,
( $false
| spl12_14 ),
inference(unit_resulting_resolution,[],[f248,f90]) ).
fof(f259,plain,
spl12_14,
inference(avatar_contradiction_clause,[],[f254]) ).
fof(f262,plain,
! [X0] :
( sdtpldt0(xa,sdtpldt0(xb,X0)) = sdtpldt0(sz10,X0)
| ~ aElement0(xa)
| ~ aElement0(xb)
| ~ aElement0(X0) ),
inference(superposition,[],[f107,f97]) ).
fof(f268,definition,
( spl12_16
<=> ! [X0] :
( sdtpldt0(xa,sdtpldt0(xb,X0)) = sdtpldt0(sz10,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f269,plain,
( ! [X0] :
( sdtpldt0(xa,sdtpldt0(xb,X0)) = sdtpldt0(sz10,X0)
| ~ aElement0(X0) )
| ~ spl12_16 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f270,plain,
( ~ spl12_13
| ~ spl12_15
| spl12_16 ),
inference(avatar_split_clause,[],[f262,f268,f250,f233]) ).
fof(f334,plain,
! [X0] :
( sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),X0)) = sdtpldt0(xw,X0)
| ~ aElement0(sdtasdt0(xy,xa))
| ~ aElement0(sdtasdt0(xx,xb))
| ~ aElement0(X0) ),
inference(superposition,[],[f107,f100]) ).
fof(f340,definition,
( spl12_27
<=> aElement0(sdtasdt0(xx,xb)) ),
introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition]) ).
fof(f342,plain,
( ~ aElement0(sdtasdt0(xx,xb))
| spl12_27 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f344,definition,
( spl12_28
<=> aElement0(sdtasdt0(xy,xa)) ),
introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition]) ).
fof(f346,plain,
( ~ aElement0(sdtasdt0(xy,xa))
| spl12_28 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f353,definition,
( spl12_30
<=> ! [X0] :
( sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),X0)) = sdtpldt0(xw,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_30])],[avatar_definition]) ).
fof(f354,plain,
( ! [X0] :
( sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),X0)) = sdtpldt0(xw,X0)
| ~ aElement0(X0) )
| ~ spl12_30 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f355,plain,
( ~ spl12_27
| ~ spl12_28
| spl12_30 ),
inference(avatar_split_clause,[],[f334,f353,f344,f340]) ).
fof(f363,plain,
( ~ aElement0(xx)
| ~ aElement0(xb)
| spl12_27 ),
inference(resolution,[],[f342,f122]) ).
fof(f373,plain,
( ~ spl12_13
| ~ spl12_1
| spl12_27 ),
inference(avatar_split_clause,[],[f363,f340,f158,f233]) ).
fof(f377,plain,
( ~ aElement0(xy)
| ~ aElement0(xa)
| spl12_28 ),
inference(resolution,[],[f346,f122]) ).
fof(f380,definition,
( spl12_33
<=> aElement0(xy) ),
introduced(definition,[new_symbols(definition,[spl12_33])],[avatar_definition]) ).
fof(f382,plain,
( ~ aElement0(xy)
| spl12_33 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f383,plain,
( ~ spl12_15
| ~ spl12_33
| spl12_28 ),
inference(avatar_split_clause,[],[f377,f344,f380,f250]) ).
fof(f422,definition,
( spl12_37
<=> aElement0(sz00) ),
introduced(definition,[new_symbols(definition,[spl12_37])],[avatar_definition]) ).
fof(f424,plain,
( ~ aElement0(sz00)
| spl12_37 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f450,plain,
( $false
| spl12_37 ),
inference(unit_resulting_resolution,[],[f424,f147]) ).
fof(f453,plain,
spl12_37,
inference(avatar_contradiction_clause,[],[f450]) ).
fof(f543,plain,
! [X0] :
( aElementOf0(sz00,xI)
| ~ aElement0(sz00)
| ~ aElementOf0(X0,xI)
| ~ aElement0(X0) ),
inference(superposition,[],[f88,f143]) ).
fof(f545,plain,
! [X0] :
( aElementOf0(smndt0(X0),xI)
| ~ aElement0(smndt0(sz10))
| ~ aElementOf0(X0,xI)
| ~ aElement0(X0) ),
inference(superposition,[],[f88,f135]) ).
fof(f553,definition,
( spl12_54
<=> ! [X0] :
( aElementOf0(smndt0(X0),xI)
| ~ aElement0(X0)
| ~ aElementOf0(X0,xI) ) ),
introduced(definition,[new_symbols(definition,[spl12_54])],[avatar_definition]) ).
fof(f554,plain,
( ! [X0] :
( aElementOf0(smndt0(X0),xI)
| ~ aElement0(X0)
| ~ aElementOf0(X0,xI) )
| ~ spl12_54 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f555,plain,
( ~ spl12_9
| spl12_54 ),
inference(avatar_split_clause,[],[f545,f553,f202]) ).
fof(f557,definition,
( spl12_55
<=> ! [X0] :
( ~ aElementOf0(X0,xI)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_55])],[avatar_definition]) ).
fof(f558,plain,
( ! [X0] :
( ~ aElementOf0(X0,xI)
| ~ aElement0(X0) )
| ~ spl12_55 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f560,definition,
( spl12_56
<=> aElementOf0(sz00,xI) ),
introduced(definition,[new_symbols(definition,[spl12_56])],[avatar_definition]) ).
fof(f563,plain,
( spl12_55
| ~ spl12_37
| spl12_56 ),
inference(avatar_split_clause,[],[f543,f560,f422,f557]) ).
fof(f580,plain,
( ~ aElement0(xa)
| ~ spl12_55 ),
inference(resolution,[],[f558,f99]) ).
fof(f620,plain,
( ~ spl12_15
| ~ spl12_55 ),
inference(avatar_split_clause,[],[f580,f557,f250]) ).
fof(f770,plain,
! [X2,X0,X1] :
( aElementOf0(sdtpldt0(X0,sdtpldt0(X1,X2)),xI)
| ~ aElementOf0(X2,xI)
| ~ aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(superposition,[],[f89,f107]) ).
fof(f780,definition,
( spl12_82
<=> aElementOf0(xa,xI) ),
introduced(definition,[new_symbols(definition,[spl12_82])],[avatar_definition]) ).
fof(f782,plain,
( ~ aElementOf0(xa,xI)
| spl12_82 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f789,definition,
( spl12_84
<=> aElementOf0(sdtasdt0(xy,xa),xI) ),
introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition]) ).
fof(f791,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| spl12_84 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f808,plain,
( ~ aElement0(xy)
| ~ aElementOf0(xa,xI)
| spl12_84 ),
inference(resolution,[],[f791,f88]) ).
fof(f813,plain,
( ~ spl12_82
| ~ spl12_33
| spl12_84 ),
inference(avatar_split_clause,[],[f808,f789,f380,f780]) ).
fof(f849,plain,
( sdtpldt0(xa,sz00) = sdtpldt0(sz10,smndt0(xb))
| ~ aElement0(smndt0(xb))
| ~ aElement0(xb)
| ~ spl12_16 ),
inference(superposition,[],[f269,f140]) ).
fof(f850,plain,
( sdtpldt0(xa,xb) = sdtpldt0(sz10,sz00)
| ~ aElement0(sz00)
| ~ aElement0(xb)
| ~ spl12_16 ),
inference(superposition,[],[f269,f146]) ).
fof(f878,plain,
( sz10 = sdtpldt0(sz10,sz00)
| ~ aElement0(sz00)
| ~ aElement0(xb)
| ~ spl12_16 ),
inference(forward_demodulation,[],[f850,f97]) ).
fof(f880,definition,
( spl12_93
<=> aElement0(smndt0(xb)) ),
introduced(definition,[new_symbols(definition,[spl12_93])],[avatar_definition]) ).
fof(f882,plain,
( ~ aElement0(smndt0(xb))
| spl12_93 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,definition,
( spl12_94
<=> sdtpldt0(xa,sz00) = sdtpldt0(sz10,smndt0(xb)) ),
introduced(definition,[new_symbols(definition,[spl12_94])],[avatar_definition]) ).
fof(f886,plain,
( sdtpldt0(xa,sz00) = sdtpldt0(sz10,smndt0(xb))
| ~ spl12_94 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f887,plain,
( ~ spl12_13
| ~ spl12_93
| spl12_94
| ~ spl12_16 ),
inference(avatar_split_clause,[],[f849,f268,f884,f880,f233]) ).
fof(f894,definition,
( spl12_96
<=> sz10 = sdtpldt0(sz10,sz00) ),
introduced(definition,[new_symbols(definition,[spl12_96])],[avatar_definition]) ).
fof(f896,plain,
( sz10 = sdtpldt0(sz10,sz00)
| ~ spl12_96 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f897,plain,
( ~ spl12_13
| ~ spl12_37
| spl12_96
| ~ spl12_16 ),
inference(avatar_split_clause,[],[f878,f268,f894,f422,f233]) ).
fof(f898,plain,
( $false
| spl12_82 ),
inference(unit_resulting_resolution,[],[f782,f99]) ).
fof(f901,plain,
spl12_82,
inference(avatar_contradiction_clause,[],[f898]) ).
fof(f903,plain,
( ~ aElement0(xb)
| spl12_93 ),
inference(resolution,[],[f882,f141]) ).
fof(f917,plain,
( ~ spl12_13
| spl12_93 ),
inference(avatar_split_clause,[],[f903,f880,f233]) ).
fof(f936,definition,
( spl12_99
<=> aElement0(sz10) ),
introduced(definition,[new_symbols(definition,[spl12_99])],[avatar_definition]) ).
fof(f938,plain,
( ~ aElement0(sz10)
| spl12_99 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f943,plain,
( $false
| spl12_99 ),
inference(unit_resulting_resolution,[],[f938,f138]) ).
fof(f946,plain,
spl12_99,
inference(avatar_contradiction_clause,[],[f943]) ).
fof(f949,plain,
( xa = sdtpldt0(sz10,smndt0(xb))
| ~ aElement0(xa)
| ~ spl12_94 ),
inference(superposition,[],[f886,f146]) ).
fof(f986,definition,
( spl12_105
<=> xa = sdtpldt0(sz10,smndt0(xb)) ),
introduced(definition,[new_symbols(definition,[spl12_105])],[avatar_definition]) ).
fof(f988,plain,
( xa = sdtpldt0(sz10,smndt0(xb))
| ~ spl12_105 ),
inference(avatar_component_clause,[],[f986]) ).
fof(f992,plain,
( ~ spl12_15
| spl12_105
| ~ spl12_94 ),
inference(avatar_split_clause,[],[f949,f884,f986,f250]) ).
fof(f1024,plain,
( ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(smndt0(xb),X0))
| ~ aElement0(sz10)
| ~ aElement0(smndt0(xb))
| ~ aElement0(X0) )
| ~ spl12_105 ),
inference(superposition,[],[f107,f988]) ).
fof(f1032,definition,
( spl12_110
<=> ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(smndt0(xb),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_110])],[avatar_definition]) ).
fof(f1033,plain,
( ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(smndt0(xb),X0))
| ~ aElement0(X0) )
| ~ spl12_110 ),
inference(avatar_component_clause,[],[f1032]) ).
fof(f1034,plain,
( ~ spl12_93
| ~ spl12_99
| spl12_110
| ~ spl12_105 ),
inference(avatar_split_clause,[],[f1024,f986,f1032,f936,f880]) ).
fof(f1208,plain,
( $false
| spl12_33 ),
inference(unit_resulting_resolution,[],[f382,f95]) ).
fof(f1211,plain,
spl12_33,
inference(avatar_contradiction_clause,[],[f1208]) ).
fof(f1439,definition,
( spl12_143
<=> aElement0(smndt0(xa)) ),
introduced(definition,[new_symbols(definition,[spl12_143])],[avatar_definition]) ).
fof(f1441,plain,
( ~ aElement0(smndt0(xa))
| spl12_143 ),
inference(avatar_component_clause,[],[f1439]) ).
fof(f1464,plain,
( ~ aElement0(xa)
| spl12_143 ),
inference(resolution,[],[f1441,f141]) ).
fof(f1478,plain,
( ~ spl12_15
| spl12_143 ),
inference(avatar_split_clause,[],[f1464,f1439,f250]) ).
fof(f2242,plain,
( ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0)
| ~ aElement0(X0)
| ~ aElement0(smndt0(xb)) )
| ~ spl12_110 ),
inference(superposition,[],[f1033,f108]) ).
fof(f2265,plain,
( ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0)
| ~ aElement0(smndt0(xb)) )
| ~ spl12_110 ),
inference(duplicate_literal_removal,[],[f2242]) ).
fof(f2277,definition,
( spl12_208
<=> ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_208])],[avatar_definition]) ).
fof(f2278,plain,
( ! [X0] :
( sdtpldt0(xa,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0) )
| ~ spl12_208 ),
inference(avatar_component_clause,[],[f2277]) ).
fof(f2280,plain,
( ~ spl12_93
| spl12_208
| ~ spl12_110 ),
inference(avatar_split_clause,[],[f2265,f1032,f2277,f880]) ).
fof(f3125,plain,
( ! [X0] :
( sdtpldt0(X0,xa) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0)
| ~ aElement0(X0)
| ~ aElement0(xa) )
| ~ spl12_208 ),
inference(superposition,[],[f2278,f108]) ).
fof(f3192,plain,
( ! [X0] :
( sdtpldt0(X0,xa) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0)
| ~ aElement0(xa) )
| ~ spl12_208 ),
inference(duplicate_literal_removal,[],[f3125]) ).
fof(f3240,definition,
( spl12_288
<=> ! [X0] :
( sdtpldt0(X0,xa) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_288])],[avatar_definition]) ).
fof(f3241,plain,
( ! [X0] :
( sdtpldt0(X0,xa) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xb)))
| ~ aElement0(X0) )
| ~ spl12_288 ),
inference(avatar_component_clause,[],[f3240]) ).
fof(f3271,plain,
( ~ spl12_15
| spl12_288
| ~ spl12_208 ),
inference(avatar_split_clause,[],[f3192,f2277,f3240,f250]) ).
fof(f3640,plain,
( sdtpldt0(xb,xa) = sdtpldt0(sz10,sz00)
| ~ aElement0(xb)
| ~ aElement0(xb)
| ~ spl12_288 ),
inference(superposition,[],[f3241,f140]) ).
fof(f3684,plain,
( sdtpldt0(xb,xa) = sdtpldt0(sz10,sz00)
| ~ aElement0(xb)
| ~ spl12_288 ),
inference(duplicate_literal_removal,[],[f3640]) ).
fof(f3729,plain,
( sz10 = sdtpldt0(xb,xa)
| ~ aElement0(xb)
| ~ spl12_96
| ~ spl12_288 ),
inference(forward_demodulation,[],[f3684,f896]) ).
fof(f3750,definition,
( spl12_334
<=> sz10 = sdtpldt0(xb,xa) ),
introduced(definition,[new_symbols(definition,[spl12_334])],[avatar_definition]) ).
fof(f3752,plain,
( sz10 = sdtpldt0(xb,xa)
| ~ spl12_334 ),
inference(avatar_component_clause,[],[f3750]) ).
fof(f3753,plain,
( ~ spl12_13
| spl12_334
| ~ spl12_96
| ~ spl12_288 ),
inference(avatar_split_clause,[],[f3729,f3240,f894,f3750,f233]) ).
fof(f3765,plain,
( ! [X0] :
( sdtpldt0(sz10,X0) = sdtpldt0(xb,sdtpldt0(xa,X0))
| ~ aElement0(xb)
| ~ aElement0(xa)
| ~ aElement0(X0) )
| ~ spl12_334 ),
inference(superposition,[],[f107,f3752]) ).
fof(f3775,definition,
( spl12_335
<=> ! [X0] :
( sdtpldt0(sz10,X0) = sdtpldt0(xb,sdtpldt0(xa,X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_335])],[avatar_definition]) ).
fof(f3776,plain,
( ! [X0] :
( sdtpldt0(sz10,X0) = sdtpldt0(xb,sdtpldt0(xa,X0))
| ~ aElement0(X0) )
| ~ spl12_335 ),
inference(avatar_component_clause,[],[f3775]) ).
fof(f3777,plain,
( ~ spl12_15
| ~ spl12_13
| spl12_335
| ~ spl12_334 ),
inference(avatar_split_clause,[],[f3765,f3750,f3775,f233,f250]) ).
fof(f4165,plain,
( sdtpldt0(xb,sz00) = sdtpldt0(sz10,smndt0(xa))
| ~ aElement0(smndt0(xa))
| ~ aElement0(xa)
| ~ spl12_335 ),
inference(superposition,[],[f3776,f140]) ).
fof(f4199,definition,
( spl12_363
<=> sdtpldt0(xb,sz00) = sdtpldt0(sz10,smndt0(xa)) ),
introduced(definition,[new_symbols(definition,[spl12_363])],[avatar_definition]) ).
fof(f4201,plain,
( sdtpldt0(xb,sz00) = sdtpldt0(sz10,smndt0(xa))
| ~ spl12_363 ),
inference(avatar_component_clause,[],[f4199]) ).
fof(f4202,plain,
( ~ spl12_15
| ~ spl12_143
| spl12_363
| ~ spl12_335 ),
inference(avatar_split_clause,[],[f4165,f3775,f4199,f1439,f250]) ).
fof(f4294,plain,
( xb = sdtpldt0(sz10,smndt0(xa))
| ~ aElement0(xb)
| ~ spl12_363 ),
inference(superposition,[],[f4201,f146]) ).
fof(f4339,definition,
( spl12_382
<=> xb = sdtpldt0(sz10,smndt0(xa)) ),
introduced(definition,[new_symbols(definition,[spl12_382])],[avatar_definition]) ).
fof(f4341,plain,
( xb = sdtpldt0(sz10,smndt0(xa))
| ~ spl12_382 ),
inference(avatar_component_clause,[],[f4339]) ).
fof(f4365,plain,
( ~ spl12_13
| spl12_382
| ~ spl12_363 ),
inference(avatar_split_clause,[],[f4294,f4199,f4339,f233]) ).
fof(f4410,plain,
( ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(smndt0(xa),X0))
| ~ aElement0(sz10)
| ~ aElement0(smndt0(xa))
| ~ aElement0(X0) )
| ~ spl12_382 ),
inference(superposition,[],[f107,f4341]) ).
fof(f4418,definition,
( spl12_391
<=> ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(smndt0(xa),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_391])],[avatar_definition]) ).
fof(f4419,plain,
( ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(smndt0(xa),X0))
| ~ aElement0(X0) )
| ~ spl12_391 ),
inference(avatar_component_clause,[],[f4418]) ).
fof(f4420,plain,
( ~ spl12_143
| ~ spl12_99
| spl12_391
| ~ spl12_382 ),
inference(avatar_split_clause,[],[f4410,f4339,f4418,f936,f1439]) ).
fof(f7023,plain,
( ~ aElementOf0(sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(smndt0(sz10),xx))),xI)
| ~ aElement0(sdtasdt0(smndt0(sz10),xx))
| spl12_2
| ~ spl12_30 ),
inference(superposition,[],[f164,f354]) ).
fof(f7275,definition,
( spl12_624
<=> aElement0(sdtasdt0(smndt0(sz10),xx)) ),
introduced(definition,[new_symbols(definition,[spl12_624])],[avatar_definition]) ).
fof(f7277,plain,
( ~ aElement0(sdtasdt0(smndt0(sz10),xx))
| spl12_624 ),
inference(avatar_component_clause,[],[f7275]) ).
fof(f7279,definition,
( spl12_625
<=> aElementOf0(sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(smndt0(sz10),xx))),xI) ),
introduced(definition,[new_symbols(definition,[spl12_625])],[avatar_definition]) ).
fof(f7281,plain,
( ~ aElementOf0(sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(smndt0(sz10),xx))),xI)
| spl12_625 ),
inference(avatar_component_clause,[],[f7279]) ).
fof(f7282,plain,
( ~ spl12_624
| ~ spl12_625
| spl12_2
| ~ spl12_30 ),
inference(avatar_split_clause,[],[f7023,f353,f162,f7279,f7275]) ).
fof(f7304,plain,
( ~ aElement0(smndt0(sz10))
| ~ aElement0(xx)
| spl12_624 ),
inference(resolution,[],[f7277,f122]) ).
fof(f7310,plain,
( ~ spl12_1
| ~ spl12_9
| spl12_624 ),
inference(avatar_split_clause,[],[f7304,f7275,f202,f158]) ).
fof(f7346,definition,
( spl12_631
<=> aElementOf0(sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(smndt0(sz10),xx)),xI) ),
introduced(definition,[new_symbols(definition,[spl12_631])],[avatar_definition]) ).
fof(f7348,plain,
( ~ aElementOf0(sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(smndt0(sz10),xx)),xI)
| spl12_631 ),
inference(avatar_component_clause,[],[f7346]) ).
fof(f7351,definition,
( spl12_632
<=> aElementOf0(sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(xx,smndt0(sz10))),xI) ),
introduced(definition,[new_symbols(definition,[spl12_632])],[avatar_definition]) ).
fof(f7353,plain,
( ~ aElementOf0(sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(xx,smndt0(sz10))),xI)
| spl12_632 ),
inference(avatar_component_clause,[],[f7351]) ).
fof(f7379,plain,
( ~ aElementOf0(sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(xx,smndt0(sz10))),xI)
| ~ aElement0(xx)
| ~ aElement0(smndt0(sz10))
| spl12_631 ),
inference(superposition,[],[f7348,f121]) ).
fof(f7382,plain,
( ~ spl12_9
| ~ spl12_1
| ~ spl12_632
| spl12_631 ),
inference(avatar_split_clause,[],[f7379,f7346,f7351,f158,f202]) ).
fof(f7389,plain,
( ~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI)
| ~ aElement0(xx)
| ~ aElement0(xb)
| ~ aElement0(smndt0(sz10))
| spl12_632 ),
inference(superposition,[],[f7353,f119]) ).
fof(f7391,definition,
( spl12_636
<=> aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI) ),
introduced(definition,[new_symbols(definition,[spl12_636])],[avatar_definition]) ).
fof(f7393,plain,
( ~ aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI)
| spl12_636 ),
inference(avatar_component_clause,[],[f7391]) ).
fof(f7394,plain,
( ~ spl12_9
| ~ spl12_13
| ~ spl12_1
| ~ spl12_636
| spl12_632 ),
inference(avatar_split_clause,[],[f7389,f7351,f7391,f158,f233,f202]) ).
fof(f7398,plain,
( ~ aElement0(xx)
| ~ aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI)
| spl12_636 ),
inference(resolution,[],[f7393,f88]) ).
fof(f7401,definition,
( spl12_637
<=> aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI) ),
introduced(definition,[new_symbols(definition,[spl12_637])],[avatar_definition]) ).
fof(f7403,plain,
( ~ aElementOf0(sdtpldt0(xb,smndt0(sz10)),xI)
| spl12_637 ),
inference(avatar_component_clause,[],[f7401]) ).
fof(f7405,plain,
( ~ spl12_637
| ~ spl12_1
| spl12_636 ),
inference(avatar_split_clause,[],[f7398,f7391,f158,f7401]) ).
fof(f7455,plain,
( ~ aElementOf0(sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(smndt0(sz10),xx)),xI)
| ~ aElementOf0(sdtasdt0(xy,xa),xI)
| spl12_625 ),
inference(resolution,[],[f7281,f89]) ).
fof(f10183,plain,
( ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xa)))
| ~ aElement0(X0)
| ~ aElement0(X0)
| ~ aElement0(smndt0(xa)) )
| ~ spl12_391 ),
inference(superposition,[],[f4419,f108]) ).
fof(f10220,plain,
( ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xa)))
| ~ aElement0(X0)
| ~ aElement0(smndt0(xa)) )
| ~ spl12_391 ),
inference(duplicate_literal_removal,[],[f10183]) ).
fof(f10262,definition,
( spl12_923
<=> ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xa)))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl12_923])],[avatar_definition]) ).
fof(f10263,plain,
( ! [X0] :
( sdtpldt0(xb,X0) = sdtpldt0(sz10,sdtpldt0(X0,smndt0(xa)))
| ~ aElement0(X0) )
| ~ spl12_923 ),
inference(avatar_component_clause,[],[f10262]) ).
fof(f10265,plain,
( ~ spl12_143
| spl12_923
| ~ spl12_391 ),
inference(avatar_split_clause,[],[f10220,f4418,f10262,f1439]) ).
fof(f10652,definition,
( spl12_966
<=> aElementOf0(smndt0(xa),xI) ),
introduced(definition,[new_symbols(definition,[spl12_966])],[avatar_definition]) ).
fof(f10654,plain,
( ~ aElementOf0(smndt0(xa),xI)
| spl12_966 ),
inference(avatar_component_clause,[],[f10652]) ).
fof(f12316,plain,
( ~ aElement0(xa)
| ~ aElementOf0(xa,xI)
| ~ spl12_54
| spl12_966 ),
inference(resolution,[],[f10654,f554]) ).
fof(f12330,plain,
( ~ spl12_82
| ~ spl12_15
| ~ spl12_54
| spl12_966 ),
inference(avatar_split_clause,[],[f12316,f10652,f553,f250,f780]) ).
fof(f16622,plain,
( ! [X0] :
( aElementOf0(sdtpldt0(xb,X0),xI)
| ~ aElementOf0(smndt0(xa),xI)
| ~ aElementOf0(sdtpldt0(sz10,X0),xI)
| ~ aElement0(sz10)
| ~ aElement0(X0)
| ~ aElement0(smndt0(xa))
| ~ aElement0(X0) )
| ~ spl12_923 ),
inference(superposition,[],[f770,f10263]) ).
fof(f16675,plain,
( ! [X0] :
( aElementOf0(sdtpldt0(xb,X0),xI)
| ~ aElementOf0(smndt0(xa),xI)
| ~ aElementOf0(sdtpldt0(sz10,X0),xI)
| ~ aElement0(sz10)
| ~ aElement0(X0)
| ~ aElement0(smndt0(xa)) )
| ~ spl12_923 ),
inference(duplicate_literal_removal,[],[f16622]) ).
fof(f16725,definition,
( spl12_1443
<=> ! [X0] :
( aElementOf0(sdtpldt0(xb,X0),xI)
| ~ aElement0(X0)
| ~ aElementOf0(sdtpldt0(sz10,X0),xI) ) ),
introduced(definition,[new_symbols(definition,[spl12_1443])],[avatar_definition]) ).
fof(f16726,plain,
( ! [X0] :
( aElementOf0(sdtpldt0(xb,X0),xI)
| ~ aElement0(X0)
| ~ aElementOf0(sdtpldt0(sz10,X0),xI) )
| ~ spl12_1443 ),
inference(avatar_component_clause,[],[f16725]) ).
fof(f16727,plain,
( ~ spl12_143
| ~ spl12_99
| ~ spl12_966
| spl12_1443
| ~ spl12_923 ),
inference(avatar_split_clause,[],[f16675,f10262,f16725,f10652,f936,f1439]) ).
fof(f25984,plain,
( ~ aElement0(smndt0(sz10))
| ~ aElementOf0(sdtpldt0(sz10,smndt0(sz10)),xI)
| spl12_637
| ~ spl12_1443 ),
inference(resolution,[],[f16726,f7403]) ).
fof(f26103,definition,
( spl12_2266
<=> aElementOf0(sdtpldt0(sz10,smndt0(sz10)),xI) ),
introduced(definition,[new_symbols(definition,[spl12_2266])],[avatar_definition]) ).
fof(f26105,plain,
( ~ aElementOf0(sdtpldt0(sz10,smndt0(sz10)),xI)
| spl12_2266 ),
inference(avatar_component_clause,[],[f26103]) ).
fof(f26106,plain,
( ~ spl12_2266
| ~ spl12_9
| spl12_637
| ~ spl12_1443 ),
inference(avatar_split_clause,[],[f25984,f16725,f7401,f202,f26103]) ).
fof(f26152,plain,
( ~ aElementOf0(sz00,xI)
| ~ aElement0(sz10)
| spl12_2266 ),
inference(superposition,[],[f26105,f140]) ).
fof(f26153,plain,
( ~ spl12_99
| ~ spl12_56
| spl12_2266 ),
inference(avatar_split_clause,[],[f26152,f26103,f560,f936]) ).
fof(f26171,plain,
( ~ spl12_84
| ~ spl12_631
| spl12_625 ),
inference(avatar_split_clause,[],[f7455,f7279,f7346,f789]) ).
cnf(s1,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f165]) ).
cnf(s5,plain,
spl12_1,
inference(sat_conversion,[],[f187]) ).
cnf(s11,plain,
spl12_9,
inference(sat_conversion,[],[f214]) ).
cnf(s15,plain,
( ~ spl12_12
| spl12_13 ),
inference(sat_conversion,[],[f236]) ).
cnf(s18,plain,
spl12_12,
inference(sat_conversion,[],[f243]) ).
cnf(s19,plain,
( ~ spl12_14
| spl12_15 ),
inference(sat_conversion,[],[f253]) ).
cnf(s21,plain,
spl12_14,
inference(sat_conversion,[],[f259]) ).
cnf(s24,plain,
( ~ spl12_13
| ~ spl12_15
| spl12_16 ),
inference(sat_conversion,[],[f270]) ).
cnf(s35,plain,
( ~ spl12_27
| ~ spl12_28
| spl12_30 ),
inference(sat_conversion,[],[f355]) ).
cnf(s41,plain,
( ~ spl12_1
| ~ spl12_13
| spl12_27 ),
inference(sat_conversion,[],[f373]) ).
cnf(s43,plain,
( ~ spl12_15
| spl12_28
| ~ spl12_33 ),
inference(sat_conversion,[],[f383]) ).
cnf(s53,plain,
spl12_37,
inference(sat_conversion,[],[f453]) ).
cnf(s66,plain,
( ~ spl12_9
| spl12_54 ),
inference(sat_conversion,[],[f555]) ).
cnf(s67,plain,
( ~ spl12_37
| spl12_55
| spl12_56 ),
inference(sat_conversion,[],[f563]) ).
cnf(s78,plain,
( ~ spl12_15
| ~ spl12_55 ),
inference(sat_conversion,[],[f620]) ).
cnf(s102,plain,
( ~ spl12_33
| ~ spl12_82
| spl12_84 ),
inference(sat_conversion,[],[f813]) ).
cnf(s110,plain,
( ~ spl12_13
| ~ spl12_16
| ~ spl12_93
| spl12_94 ),
inference(sat_conversion,[],[f887]) ).
cnf(s113,plain,
( ~ spl12_13
| ~ spl12_16
| ~ spl12_37
| spl12_96 ),
inference(sat_conversion,[],[f897]) ).
cnf(s115,plain,
spl12_82,
inference(sat_conversion,[],[f901]) ).
cnf(s119,plain,
( ~ spl12_13
| spl12_93 ),
inference(sat_conversion,[],[f917]) ).
cnf(s124,plain,
spl12_99,
inference(sat_conversion,[],[f946]) ).
cnf(s134,plain,
( ~ spl12_15
| ~ spl12_94
| spl12_105 ),
inference(sat_conversion,[],[f992]) ).
cnf(s139,plain,
( ~ spl12_93
| ~ spl12_99
| ~ spl12_105
| spl12_110 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s163,plain,
spl12_33,
inference(sat_conversion,[],[f1211]) ).
cnf(s196,plain,
( ~ spl12_15
| spl12_143 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s272,plain,
( ~ spl12_93
| ~ spl12_110
| spl12_208 ),
inference(sat_conversion,[],[f2280]) ).
cnf(s427,plain,
( ~ spl12_15
| ~ spl12_208
| spl12_288 ),
inference(sat_conversion,[],[f3271]) ).
cnf(s494,plain,
( ~ spl12_13
| ~ spl12_96
| ~ spl12_288
| spl12_334 ),
inference(sat_conversion,[],[f3753]) ).
cnf(s495,plain,
( ~ spl12_13
| ~ spl12_15
| ~ spl12_334
| spl12_335 ),
inference(sat_conversion,[],[f3777]) ).
cnf(s534,plain,
( ~ spl12_15
| ~ spl12_143
| ~ spl12_335
| spl12_363 ),
inference(sat_conversion,[],[f4202]) ).
cnf(s565,plain,
( ~ spl12_13
| ~ spl12_363
| spl12_382 ),
inference(sat_conversion,[],[f4365]) ).
cnf(s571,plain,
( ~ spl12_99
| ~ spl12_143
| ~ spl12_382
| spl12_391 ),
inference(sat_conversion,[],[f4420]) ).
cnf(s982,plain,
( spl12_2
| ~ spl12_30
| ~ spl12_624
| ~ spl12_625 ),
inference(sat_conversion,[],[f7282]) ).
cnf(s993,plain,
( ~ spl12_1
| ~ spl12_9
| spl12_624 ),
inference(sat_conversion,[],[f7310]) ).
cnf(s1009,plain,
( ~ spl12_1
| ~ spl12_9
| spl12_631
| ~ spl12_632 ),
inference(sat_conversion,[],[f7382]) ).
cnf(s1012,plain,
( ~ spl12_1
| ~ spl12_9
| ~ spl12_13
| spl12_632
| ~ spl12_636 ),
inference(sat_conversion,[],[f7394]) ).
cnf(s1016,plain,
( ~ spl12_1
| spl12_636
| ~ spl12_637 ),
inference(sat_conversion,[],[f7405]) ).
cnf(s1518,plain,
( ~ spl12_143
| ~ spl12_391
| spl12_923 ),
inference(sat_conversion,[],[f10265]) ).
cnf(s1850,plain,
( ~ spl12_15
| ~ spl12_54
| ~ spl12_82
| spl12_966 ),
inference(sat_conversion,[],[f12330]) ).
cnf(s2476,plain,
( ~ spl12_99
| ~ spl12_143
| ~ spl12_923
| ~ spl12_966
| spl12_1443 ),
inference(sat_conversion,[],[f16727]) ).
cnf(s3762,plain,
( ~ spl12_9
| spl12_637
| ~ spl12_1443
| ~ spl12_2266 ),
inference(sat_conversion,[],[f26106]) ).
cnf(s3763,plain,
( ~ spl12_56
| ~ spl12_99
| spl12_2266 ),
inference(sat_conversion,[],[f26153]) ).
cnf(s3773,plain,
( ~ spl12_84
| spl12_625
| ~ spl12_631 ),
inference(sat_conversion,[],[f26171]) ).
cnf(s3788,plain,
spl12_84,
inference(rat,[],[s102,s115,s163]) ).
cnf(s3799,plain,
( ~ spl12_15
| spl12_28 ),
inference(rat,[],[s43,s163]) ).
cnf(s3812,plain,
spl12_15,
inference(rat,[],[s19,s21]) ).
cnf(s3815,plain,
spl12_143,
inference(rat,[],[s196,s3812]) ).
cnf(s3816,plain,
~ spl12_55,
inference(rat,[],[s78,s3812]) ).
cnf(s3817,plain,
spl12_28,
inference(rat,[],[s3799,s3812]) ).
cnf(s3825,plain,
spl12_56,
inference(rat,[],[s67,s53,s3816]) ).
cnf(s3835,plain,
spl12_2266,
inference(rat,[],[s3763,s124,s3825]) ).
cnf(s3848,plain,
spl12_13,
inference(rat,[],[s15,s18]) ).
cnf(s3853,plain,
spl12_93,
inference(rat,[],[s119,s3848]) ).
cnf(s3855,plain,
spl12_16,
inference(rat,[],[s24,s3812,s3848]) ).
cnf(s3873,plain,
spl12_96,
inference(rat,[],[s113,s3848,s53,s3855]) ).
cnf(s3875,plain,
spl12_94,
inference(rat,[],[s110,s3848,s3853,s3855]) ).
cnf(s3919,plain,
spl12_105,
inference(rat,[],[s134,s3812,s3875]) ).
cnf(s3974,plain,
spl12_110,
inference(rat,[],[s139,s3853,s124,s3919]) ).
cnf(s4025,plain,
spl12_208,
inference(rat,[],[s272,s3853,s3974]) ).
cnf(s4062,plain,
spl12_288,
inference(rat,[],[s427,s3812,s4025]) ).
cnf(s4125,plain,
spl12_334,
inference(rat,[],[s494,s3873,s3848,s4062]) ).
cnf(s4202,plain,
spl12_335,
inference(rat,[],[s495,s3848,s3812,s4125]) ).
cnf(s4282,plain,
spl12_363,
inference(rat,[],[s534,s3815,s3812,s4202]) ).
cnf(s4359,plain,
spl12_382,
inference(rat,[],[s565,s3848,s4282]) ).
cnf(s4451,plain,
spl12_391,
inference(rat,[],[s571,s3815,s124,s4359]) ).
cnf(s4491,plain,
spl12_923,
inference(rat,[],[s1518,s3815,s4451]) ).
cnf(s4944,plain,
spl12_54,
inference(rat,[],[s66,s11]) ).
cnf(s4980,plain,
spl12_966,
inference(rat,[],[s1850,s3812,s115,s4944]) ).
cnf(s4996,plain,
spl12_1443,
inference(rat,[],[s2476,s4491,s3815,s124,s4980]) ).
cnf(s5025,plain,
spl12_637,
inference(rat,[],[s3762,s3835,s11,s4996]) ).
cnf(s5072,plain,
spl12_636,
inference(rat,[],[s1016,s5025,s5]) ).
cnf(s5073,plain,
spl12_632,
inference(rat,[],[s1012,s5072,s11,s3848,s5]) ).
cnf(s5074,plain,
spl12_631,
inference(rat,[],[s1009,s5073,s11,s5]) ).
cnf(s5076,plain,
spl12_624,
inference(rat,[],[s993,s11,s5]) ).
cnf(s5078,plain,
spl12_27,
inference(rat,[],[s41,s3848,s5]) ).
cnf(s5086,plain,
spl12_625,
inference(rat,[],[s3773,s3788,s5074]) ).
cnf(s5096,plain,
spl12_30,
inference(rat,[],[s35,s3817,s5078]) ).
cnf(s5113,plain,
spl12_2,
inference(rat,[],[s982,s5086,s5076,s5096]) ).
cnf(s5226,plain,
$false,
inference(rat,[],[s1,s5113,s5]) ).
fof(f26172,plain,
$false,
inference(avatar_sat_refutation,[],[s5226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG096+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n008.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 23:15:09 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.61/2.90 % (1718191)Detected formulas, will run a generic FOF schedule.
% 13.61/2.90 % (1718200)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1016706347:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.61/2.90 % (1718202)dis-21_1_sil=8000:lcm=predicate:random_seed=2052906407:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.61/2.90 % (1718197)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1244810106:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.61/2.90 % (1718199)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2166752347:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.61/2.90 % (1718196)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1182243929:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.61/2.90 % (1718198)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3469321871:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.61/2.90 % (1718200)Instruction limit reached!
% 13.61/2.90 % (1718200)------------------------------
% 13.61/2.90 % (1718200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/2.90 % (1718200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.90 % (1718200)CaDiCaL version: 2.1.3
% 13.61/2.90 % (1718200)Termination reason: Instruction limit
% 13.61/2.90 % (1718200)Termination phase: Saturation
% 13.61/2.90 % (1718200)Time elapsed: 0.040 s
% 13.61/2.90 % (1718200)Peak memory usage: 89 MB
% 13.61/2.90 % (1718200)Instructions burned: 121 (million)
% 13.61/2.90 % (1718201)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1905537558:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.61/2.90 % (1718201)Instruction limit reached!
% 13.61/2.90 % (1718201)------------------------------
% 13.61/2.90 % (1718201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/2.90 % (1718201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.90 % (1718201)CaDiCaL version: 2.1.3
% 13.61/2.90 % (1718201)Termination reason: Instruction limit
% 13.61/2.90 % (1718201)Termination phase: Saturation
% 13.61/2.90 % (1718201)Time elapsed: 0.049 s
% 13.61/2.90 % (1718201)Peak memory usage: 90 MB
% 13.61/2.90 % (1718201)Instructions burned: 141 (million)
% 13.61/2.90 % (1718202)Instruction limit reached!
% 13.61/2.90 % (1718202)------------------------------
% 13.61/2.90 % (1718202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/2.90 % (1718202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.90 % (1718202)CaDiCaL version: 2.1.3
% 13.61/2.90 % (1718202)Termination reason: Instruction limit
% 13.61/2.90 % (1718202)Termination phase: Saturation
% 13.61/2.90 % (1718202)Time elapsed: 0.073 s
% 13.61/2.90 % (1718202)Peak memory usage: 90 MB
% 13.61/2.90 % (1718202)Instructions burned: 129 (million)
% 13.61/2.90 % (1718199)Instruction limit reached!
% 13.61/2.90 % (1718199)------------------------------
% 13.61/2.90 % (1718199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.61/2.90 % (1718199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.61/2.90 % (1718199)CaDiCaL version: 2.1.3
% 13.61/2.90 % (1718199)Termination reason: Instruction limit
% 13.61/2.90 % (1718199)Termination phase: Saturation
% 13.61/2.90 % (1718199)Time elapsed: 0.074 s
% 13.61/2.90 % (1718199)Peak memory usage: 89 MB
% 13.61/2.90 % (1718199)Instructions burned: 110 (million)
% 13.61/2.90 % (1718209)lrs+10_1_sil=8000:sp=occurrence:random_seed=609856139:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 13.61/2.90 % (1718212)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3305312172:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.61/2.90 % (1718213)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3676059836:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.61/2.90 % (1718211)lrs+10_1_sil=32000:urr=on:br=off:random_seed=838220098:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.61/2.90 % (1718212)Instruction limit reached!
% 19.98/3.79 % (1718212)------------------------------
% 19.98/3.79 % (1718212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718212)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718212)Termination reason: Instruction limit
% 19.98/3.79 % (1718212)Termination phase: Saturation
% 19.98/3.79 % (1718212)Time elapsed: 0.108 s
% 19.98/3.79 % (1718212)Peak memory usage: 94 MB
% 19.98/3.79 % (1718212)Instructions burned: 326 (million)
% 19.98/3.79 % (1718211)Instruction limit reached!
% 19.98/3.79 % (1718211)------------------------------
% 19.98/3.79 % (1718211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718211)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718211)Termination reason: Instruction limit
% 19.98/3.79 % (1718211)Termination phase: Saturation
% 19.98/3.79 % (1718211)Time elapsed: 0.074 s
% 19.98/3.79 % (1718211)Peak memory usage: 91 MB
% 19.98/3.79 % (1718211)Instructions burned: 159 (million)
% 19.98/3.79 % (1718209)Instruction limit reached!
% 19.98/3.79 % (1718209)------------------------------
% 19.98/3.79 % (1718209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718209)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718209)Termination reason: Instruction limit
% 19.98/3.79 % (1718209)Termination phase: Saturation
% 19.98/3.79 % (1718209)Time elapsed: 0.167 s
% 19.98/3.79 % (1718209)Peak memory usage: 93 MB
% 19.98/3.79 % (1718209)Instructions burned: 285 (million)
% 19.98/3.79 % (1718213)Instruction limit reached!
% 19.98/3.79 % (1718213)------------------------------
% 19.98/3.79 % (1718213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718213)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718213)Termination reason: Instruction limit
% 19.98/3.79 % (1718213)Termination phase: Saturation
% 19.98/3.79 % (1718213)Time elapsed: 0.121 s
% 19.98/3.79 % (1718213)Peak memory usage: 95 MB
% 19.98/3.79 % (1718213)Instructions burned: 249 (million)
% 19.98/3.79 % (1718218)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=520964937:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.98/3.79 % (1718219)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3080817711:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.98/3.79 % (1718220)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2689008893:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.98/3.79 % (1718218)Instruction limit reached!
% 19.98/3.79 % (1718218)------------------------------
% 19.98/3.79 % (1718218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718218)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718218)Termination reason: Instruction limit
% 19.98/3.79 % (1718218)Termination phase: Saturation
% 19.98/3.79 % (1718218)Time elapsed: 0.100 s
% 19.98/3.79 % (1718218)Peak memory usage: 90 MB
% 19.98/3.79 % (1718218)Instructions burned: 295 (million)
% 19.98/3.79 % (1718221)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=526303994:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.98/3.79 % (1718220)Instruction limit reached!
% 19.98/3.79 % (1718220)------------------------------
% 19.98/3.79 % (1718220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718220)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718220)Termination reason: Instruction limit
% 19.98/3.79 % (1718220)Termination phase: Saturation
% 19.98/3.79 % (1718220)Time elapsed: 0.080 s
% 19.98/3.79 % (1718220)Peak memory usage: 91 MB
% 19.98/3.79 % (1718220)Instructions burned: 114 (million)
% 19.98/3.79 % (1718221)Instruction limit reached!
% 19.98/3.79 % (1718221)------------------------------
% 19.98/3.79 % (1718221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.79 % (1718221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.79 % (1718221)CaDiCaL version: 2.1.3
% 19.98/3.79 % (1718221)Termination reason: Instruction limit
% 19.98/3.79 % (1718221)Termination phase: Saturation
% 60.31/9.32 % (1718221)Time elapsed: 0.065 s
% 60.31/9.32 % (1718221)Peak memory usage: 89 MB
% 60.31/9.32 % (1718221)Instructions burned: 128 (million)
% 60.31/9.32 % (1718225)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3185434508:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 60.31/9.32 % (1718225)Refutation not found, incomplete strategy
% 60.31/9.32 % (1718225)------------------------------
% 60.31/9.32 % (1718225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.31/9.32 % (1718225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.31/9.32 % (1718225)CaDiCaL version: 2.1.3
% 60.31/9.32 % (1718225)Termination reason: Refutation not found, incomplete strategy
% 60.31/9.32 % (1718225)Time elapsed: 0.002 s
% 60.31/9.32 % (1718225)Peak memory usage: 89 MB
% 60.31/9.32 % (1718225)Instructions burned: 1 (million)
% 60.31/9.32 % (1718227)lrs+10_1_sil=8000:sp=occurrence:random_seed=3593980906:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 60.31/9.32 % (1718228)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1058319570:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 60.31/9.32 % (1718225)------------------------------
% 60.31/9.32 % (1718225)------------------------------
% 60.31/9.32 % (1718228)Instruction limit reached!
% 60.31/9.32 % (1718228)------------------------------
% 60.31/9.32 % (1718228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.31/9.32 % (1718228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.31/9.32 % (1718228)CaDiCaL version: 2.1.3
% 60.31/9.32 % (1718228)Termination reason: Instruction limit
% 60.31/9.32 % (1718228)Termination phase: Saturation
% 60.31/9.32 % (1718228)Time elapsed: 0.262 s
% 60.31/9.32 % (1718228)Peak memory usage: 94 MB
% 60.31/9.32 % (1718228)Instructions burned: 438 (million)
% 60.31/9.32 % (1718232)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3581403464:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 60.31/9.32 % (1718233)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=53548792:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 60.31/9.32 % (1718227)Instruction limit reached!
% 60.31/9.32 % (1718227)------------------------------
% 60.31/9.32 % (1718227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.31/9.32 % (1718227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.31/9.32 % (1718227)CaDiCaL version: 2.1.3
% 60.31/9.32 % (1718227)Termination reason: Instruction limit
% 60.31/9.32 % (1718227)Termination phase: Saturation
% 60.31/9.32 % (1718227)Time elapsed: 0.510 s
% 60.31/9.32 % (1718227)Peak memory usage: 103 MB
% 60.31/9.32 % (1718227)Instructions burned: 909 (million)
% 60.31/9.32 % (1718233)Instruction limit reached!
% 60.31/9.32 % (1718233)------------------------------
% 60.31/9.32 % (1718233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.31/9.32 % (1718233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.31/9.32 % (1718233)CaDiCaL version: 2.1.3
% 60.31/9.32 % (1718233)Termination reason: Instruction limit
% 60.31/9.32 % (1718233)Termination phase: Saturation
% 60.31/9.32 % (1718233)Time elapsed: 0.060 s
% 60.31/9.32 % (1718233)Peak memory usage: 91 MB
% 60.31/9.32 % (1718233)Instructions burned: 136 (million)
% 60.31/9.32 % (1718237)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1640610178:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 60.31/9.32 % (1718236)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=254032262:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 60.31/9.32 % (1718236)Instruction limit reached!
% 60.31/9.32 % (1718236)------------------------------
% 60.31/9.32 % (1718236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.31/9.32 % (1718236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.31/9.32 % (1718236)CaDiCaL version: 2.1.3
% 60.31/9.32 % (1718236)Termination reason: Instruction limit
% 60.31/9.32 % (1718236)Termination phase: Saturation
% 60.31/9.32 % (1718236)Time elapsed: 0.321 s
% 60.31/9.32 % (1718236)Peak memory usage: 98 MB
% 60.31/9.32 % (1718236)Instructions burned: 593 (million)
% 60.31/9.32 % (1718219)Instruction limit reached!
% 60.31/9.32 % (1718219)------------------------------
% 60.31/9.32 % (1718219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.08/11.98 % (1718219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.08/11.98 % (1718219)CaDiCaL version: 2.1.3
% 78.08/11.98 % (1718219)Termination reason: Instruction limit
% 78.08/11.98 % (1718219)Termination phase: Saturation
% 78.08/11.98 % (1718219)Time elapsed: 1.429 s
% 78.08/11.98 % (1718219)Peak memory usage: 144 MB
% 78.08/11.98 % (1718219)Instructions burned: 2350 (million)
% 78.08/11.98 % (1718240)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=899049332:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 78.08/11.98 % (1718240)Instruction limit reached!
% 78.08/11.98 % (1718240)------------------------------
% 78.08/11.98 % (1718240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.08/11.98 % (1718240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.08/11.98 % (1718240)CaDiCaL version: 2.1.3
% 78.08/11.98 % (1718240)Termination reason: Instruction limit
% 78.08/11.98 % (1718240)Termination phase: Saturation
% 78.08/11.98 % (1718240)Time elapsed: 0.073 s
% 78.08/11.98 % (1718240)Peak memory usage: 91 MB
% 78.08/11.98 % (1718240)Instructions burned: 126 (million)
% 78.08/11.98 % (1718242)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4111323027:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 78.08/11.98 % (1718243)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2097166918:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 78.08/11.98 % (1718242)Instruction limit reached!
% 78.08/11.98 % (1718242)------------------------------
% 78.08/11.98 % (1718242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.08/11.98 % (1718242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.08/11.98 % (1718242)CaDiCaL version: 2.1.3
% 78.08/11.98 % (1718242)Termination reason: Instruction limit
% 78.08/11.98 % (1718242)Termination phase: Saturation
% 78.08/11.98 % (1718242)Time elapsed: 0.073 s
% 78.08/11.98 % (1718242)Peak memory usage: 90 MB
% 78.08/11.98 % (1718242)Instructions burned: 136 (million)
% 78.08/11.98 % (1718243)Instruction limit reached!
% 78.08/11.98 % (1718243)------------------------------
% 78.08/11.98 % (1718243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.08/11.98 % (1718243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.08/11.98 % (1718243)CaDiCaL version: 2.1.3
% 78.08/11.98 % (1718243)Termination reason: Instruction limit
% 78.08/11.98 % (1718243)Termination phase: Saturation
% 78.08/11.98 % (1718243)Time elapsed: 0.084 s
% 78.08/11.98 % (1718243)Peak memory usage: 92 MB
% 78.08/11.98 % (1718243)Instructions burned: 142 (million)
% 78.08/11.98 % (1718246)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3356796217:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 78.08/11.98 % (1718247)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=17343490:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 78.08/11.98 % (1718246)Instruction limit reached!
% 78.08/11.98 % (1718246)------------------------------
% 78.08/11.98 % (1718246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.08/11.98 % (1718246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.08/11.98 % (1718246)CaDiCaL version: 2.1.3
% 78.08/11.98 % (1718246)Termination reason: Instruction limit
% 78.08/11.98 % (1718246)Termination phase: Saturation
% 78.08/11.98 % (1718246)Time elapsed: 0.251 s
% 78.08/11.98 % (1718246)Peak memory usage: 92 MB
% 78.08/11.98 % (1718246)Instructions burned: 431 (million)
% 78.08/11.98 % (1718250)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1477422629:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 78.08/11.98 % (1718250)Instruction limit reached!
% 78.08/11.98 % (1718250)------------------------------
% 78.08/11.98 % (1718250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.08/11.98 % (1718250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.08/11.98 % (1718250)CaDiCaL version: 2.1.3
% 78.08/11.98 % (1718250)Termination reason: Instruction limit
% 78.08/11.98 % (1718250)Termination phase: Saturation
% 86.83/13.13 % (1718250)Time elapsed: 0.081 s
% 86.83/13.13 % (1718250)Peak memory usage: 92 MB
% 86.83/13.13 % (1718250)Instructions burned: 151 (million)
% 86.83/13.13 % (1718252)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2199399439:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 86.83/13.13 % (1718232)Instruction limit reached!
% 86.83/13.13 % (1718232)------------------------------
% 86.83/13.13 % (1718232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718232)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718232)Termination reason: Instruction limit
% 86.83/13.13 % (1718232)Termination phase: Saturation
% 86.83/13.13 % (1718232)Time elapsed: 3.166 s
% 86.83/13.13 % (1718232)Peak memory usage: 148 MB
% 86.83/13.13 % (1718232)Instructions burned: 5202 (million)
% 86.83/13.13 % (1718254)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=630486490:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 86.83/13.13 % (1718254)Instruction limit reached!
% 86.83/13.13 % (1718254)------------------------------
% 86.83/13.13 % (1718254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718254)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718254)Termination reason: Instruction limit
% 86.83/13.13 % (1718254)Termination phase: Saturation
% 86.83/13.13 % (1718254)Time elapsed: 0.283 s
% 86.83/13.13 % (1718254)Peak memory usage: 94 MB
% 86.83/13.13 % (1718254)Instructions burned: 669 (million)
% 86.83/13.13 % (1718256)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4268125593:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi)
% 86.83/13.13 % (1718256)Instruction limit reached!
% 86.83/13.13 % (1718256)------------------------------
% 86.83/13.13 % (1718256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718256)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718256)Termination reason: Instruction limit
% 86.83/13.13 % (1718256)Termination phase: Saturation
% 86.83/13.13 % (1718256)Time elapsed: 0.093 s
% 86.83/13.13 % (1718256)Peak memory usage: 92 MB
% 86.83/13.13 % (1718256)Instructions burned: 186 (million)
% 86.83/13.13 % (1718258)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2579902927:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/193Mi)
% 86.83/13.13 % (1718258)Instruction limit reached!
% 86.83/13.13 % (1718258)------------------------------
% 86.83/13.13 % (1718258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718258)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718258)Termination reason: Instruction limit
% 86.83/13.13 % (1718258)Termination phase: Saturation
% 86.83/13.13 % (1718258)Time elapsed: 0.100 s
% 86.83/13.13 % (1718258)Peak memory usage: 90 MB
% 86.83/13.13 % (1718258)Instructions burned: 195 (million)
% 86.83/13.13 % (1718260)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2888784334:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2946 on theBenchmark for (2946ds/4850Mi)
% 86.83/13.13 % (1718247)Instruction limit reached!
% 86.83/13.13 % (1718247)------------------------------
% 86.83/13.13 % (1718247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718247)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718247)Termination reason: Instruction limit
% 86.83/13.13 % (1718247)Termination phase: Saturation
% 86.83/13.13 % (1718247)Time elapsed: 3.744 s
% 86.83/13.13 % (1718247)Peak memory usage: 163 MB
% 86.83/13.13 % (1718247)Instructions burned: 6062 (million)
% 86.83/13.13 % (1718262)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1059373584:i=12111:sd=1:ss=included_2937 on theBenchmark for (2937ds/12111Mi)
% 86.83/13.13 % (1718260)Instruction limit reached!
% 86.83/13.13 % (1718260)------------------------------
% 86.83/13.13 % (1718260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718260)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718260)Termination reason: Instruction limit
% 86.83/13.13 % (1718260)Termination phase: Saturation
% 86.83/13.13 % (1718260)Time elapsed: 2.907 s
% 86.83/13.13 % (1718260)Peak memory usage: 135 MB
% 86.83/13.13 % (1718260)Instructions burned: 4851 (million)
% 86.83/13.13 % (1718264)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=162607317:i=319:kws=precedence:fsr=off_2915 on theBenchmark for (2915ds/319Mi)
% 86.83/13.13 % (1718264)Instruction limit reached!
% 86.83/13.13 % (1718264)------------------------------
% 86.83/13.13 % (1718264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718264)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718264)Termination reason: Instruction limit
% 86.83/13.13 % (1718264)Termination phase: Saturation
% 86.83/13.13 % (1718264)Time elapsed: 0.177 s
% 86.83/13.13 % (1718264)Peak memory usage: 94 MB
% 86.83/13.13 % (1718264)Instructions burned: 321 (million)
% 86.83/13.13 % (1718237)Instruction limit reached!
% 86.83/13.13 % (1718237)------------------------------
% 86.83/13.13 % (1718237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718237)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718237)Termination reason: Instruction limit
% 86.83/13.13 % (1718237)Termination phase: Saturation
% 86.83/13.13 % (1718237)Time elapsed: 7.278 s
% 86.83/13.13 % (1718237)Peak memory usage: 259 MB
% 86.83/13.13 % (1718237)Instructions burned: 13194 (million)
% 86.83/13.13 % (1718266)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3734985717:i=2064:ep=RST_2911 on theBenchmark for (2911ds/2064Mi)
% 86.83/13.13 % (1718267)dis-1011_128_sil=32000:random_seed=1639878575:i=3706:ep=RST:av=off_2911 on theBenchmark for (2911ds/3706Mi)
% 86.83/13.13 % (1718266)Instruction limit reached!
% 86.83/13.13 % (1718266)------------------------------
% 86.83/13.13 % (1718266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718266)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718266)Termination reason: Instruction limit
% 86.83/13.13 % (1718266)Termination phase: Saturation
% 86.83/13.13 % (1718266)Time elapsed: 1.119 s
% 86.83/13.13 % (1718266)Peak memory usage: 144 MB
% 86.83/13.13 % (1718266)Instructions burned: 2065 (million)
% 86.83/13.13 % (1718270)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2809619487:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2899 on theBenchmark for (2899ds/757Mi)
% 86.83/13.13 % (1718252)Instruction limit reached!
% 86.83/13.13 % (1718252)------------------------------
% 86.83/13.13 % (1718252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718252)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718252)Termination reason: Instruction limit
% 86.83/13.13 % (1718252)Termination phase: Saturation
% 86.83/13.13 % (1718252)Time elapsed: 7.445 s
% 86.83/13.13 % (1718252)Peak memory usage: 282 MB
% 86.83/13.13 % (1718252)Instructions burned: 14155 (million)
% 86.83/13.13 % (1718272)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1865798647:i=13913:ss=axioms:sgt=8_2894 on theBenchmark for (2894ds/13913Mi)
% 86.83/13.13 % (1718270)Instruction limit reached!
% 86.83/13.13 % (1718270)------------------------------
% 86.83/13.13 % (1718270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718270)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718270)Termination reason: Instruction limit
% 86.83/13.13 % (1718270)Termination phase: Saturation
% 86.83/13.13 % (1718270)Time elapsed: 0.592 s
% 86.83/13.13 % (1718270)Peak memory usage: 105 MB
% 86.83/13.13 % (1718270)Instructions burned: 758 (million)
% 86.83/13.13 % (1718274)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=990902:i=9925:aac=none_2891 on theBenchmark for (2891ds/9925Mi)
% 86.83/13.13 % (1718267)Instruction limit reached!
% 86.83/13.13 % (1718267)------------------------------
% 86.83/13.13 % (1718267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.83/13.13 % (1718267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.83/13.13 % (1718267)CaDiCaL version: 2.1.3
% 86.83/13.13 % (1718267)Termination reason: Instruction limit
% 86.83/13.13 % (1718267)Termination phase: Saturation
% 86.83/13.13 % (1718267)Time elapsed: 2.106 s
% 86.83/13.13 % (1718267)Peak memory usage: 140 MB
% 86.83/13.13 % (1718267)Instructions burned: 3707 (million)
% 86.83/13.13 % (1718276)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2106751143:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2888 on theBenchmark for (2888ds/2479Mi)
% 86.83/13.13 % (1718276)First to succeed.
% 86.83/13.13 % (1718276)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1718191"
% 86.83/13.13 % (1718276)Refutation found. Thanks to Tanya!
% 86.83/13.13 % SZS status Theorem for theBenchmark
% 86.83/13.13 % SZS output start Proof for theBenchmark
% See solution above
% 87.56/13.32 % (1718276)------------------------------
% 87.56/13.32 % (1718276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.56/13.32 % (1718276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.56/13.32 % (1718276)CaDiCaL version: 2.1.3
% 87.56/13.32 % (1718276)Termination reason: Refutation
% 87.56/13.32 % (1718276)Time elapsed: 0.688 s
% 87.56/13.32 % (1718276)Peak memory usage: 106 MB
% 87.56/13.32 % (1718276)Instructions burned: 1199 (million)
% 87.56/13.32 % (1718276)------------------------------
% 87.56/13.32 % (1718276)------------------------------
% 87.56/13.32 % (1718191)Success in time 12.277 s
% 87.56/13.32 % Vampire exiting
%------------------------------------------------------------------------------