%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU419+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:48:53 PM UTC 2026
% Result : Theorem 94.90s 28.63s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 27
% Syntax : Number of formulae : 164 ( 42 unt; 21 def)
% Number of atoms : 601 ( 51 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 791 ( 354 ~; 371 |; 37 &)
% ( 22 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 16 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-3 aty)
% Number of variables : 139 ( 0 sgn 131 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f32,axiom,
! [X0,X1,X2] :
( X2 = k4_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f709,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> v1_relat_1(k4_xboole_0(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_relat_1) ).
fof(f71088,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_relset_2) ).
fof(f71091,conjecture,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k4_xboole_0(X1,X2),k1_tarski(X0)) = k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_relset_2) ).
fof(f71092,negated_conjecture,
~ ! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k4_xboole_0(X1,X2),k1_tarski(X0)) = k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))) ) ),
inference(negated_conjecture,[status(cth)],[f71091]) ).
fof(f71194,plain,
? [X0,X1] :
( ? [X2] :
( k9_relat_1(k4_xboole_0(X1,X2),k1_tarski(X0)) != k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0)))
& v1_relat_1(X2) )
& v1_relat_1(X1) ),
inference(ennf_transformation,[],[f71092]) ).
fof(f71232,plain,
! [X0,X1] :
( v1_relat_1(k4_xboole_0(X1,X0))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f709]) ).
fof(f71266,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) )
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f71088]) ).
fof(f71417,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73904,plain,
( k9_relat_1(k4_xboole_0(sK31,sK32),k1_tarski(sK30)) != k4_xboole_0(k9_relat_1(sK31,k1_tarski(sK30)),k9_relat_1(sK32,k1_tarski(sK30)))
& v1_relat_1(sK32)
& v1_relat_1(sK31) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32]),skolemize(X0,sK30),skolemize(X1,sK31),skolemize(X2,sK32)],[f71194]) ).
fof(f73939,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f73940,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f73939]) ).
fof(f73941,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f73940]) ).
fof(f73942,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK43(X0,X1,X2),X0)
| r2_hidden(sK43(X0,X1,X2),X1)
| ~ r2_hidden(sK43(X0,X1,X2),X2) )
& ( ( r2_hidden(sK43(X0,X1,X2),X0)
& ~ r2_hidden(sK43(X0,X1,X2),X1) )
| r2_hidden(sK43(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X3,sK43(X0,X1,X2))],[f73941]) ).
fof(f73947,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| ~ r2_hidden(k4_tarski(X1,X0),X2) )
& ( r2_hidden(k4_tarski(X1,X0),X2)
| ~ r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1))) ) )
| ~ v1_relat_1(X2) ),
inference(nnf_transformation,[],[f71266]) ).
fof(f73987,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f73988,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f73987]) ).
fof(f73989,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f71417]) ).
fof(f73990,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f73989]) ).
fof(f73991,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK76(X0,X1),X1)
& r2_hidden(sK76(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76]),skolemize(X2,sK76(X0,X1))],[f73990]) ).
fof(f74774,plain,
v1_relat_1(sK31),
inference(cnf_transformation,[],[f73904]) ).
fof(f74775,plain,
v1_relat_1(sK32),
inference(cnf_transformation,[],[f73904]) ).
fof(f74776,plain,
k9_relat_1(k4_xboole_0(sK31,sK32),k1_tarski(sK30)) != k4_xboole_0(k9_relat_1(sK31,k1_tarski(sK30)),k9_relat_1(sK32,k1_tarski(sK30))),
inference(cnf_transformation,[],[f73904]) ).
fof(f74840,plain,
! [X0,X1] :
( v1_relat_1(k4_xboole_0(X1,X0))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f71232]) ).
fof(f74925,plain,
! [X2,X0,X1,X4] :
( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k4_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f73942]) ).
fof(f74926,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| ~ r2_hidden(X4,X2)
| k4_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f73942]) ).
fof(f74927,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| k4_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f73942]) ).
fof(f74943,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| r2_hidden(k4_tarski(X1,X0),X2)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f73947]) ).
fof(f74944,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| ~ r2_hidden(k4_tarski(X1,X0),X2)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f73947]) ).
fof(f75111,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f73988]) ).
fof(f75114,plain,
! [X0,X1] :
( r2_hidden(sK76(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f73991]) ).
fof(f75115,plain,
! [X0,X1] :
( ~ r2_hidden(sK76(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f73991]) ).
fof(f78495,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k4_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f74927]) ).
fof(f78496,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k4_xboole_0(X0,X1))
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f74926]) ).
fof(f78497,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k4_xboole_0(X0,X1))
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f74925]) ).
fof(f78795,definition,
sF617 = k4_xboole_0(sK31,sK32),
introduced(definition,[new_symbols(definition,[sF617])],[function_definition]) ).
fof(f78796,plain,
k4_xboole_0(sK31,sK32) = sF617,
inference(reorient_equations,[],[f78795]) ).
fof(f78797,definition,
sF618 = k1_tarski(sK30),
introduced(definition,[new_symbols(definition,[sF618])],[function_definition]) ).
fof(f78798,plain,
k1_tarski(sK30) = sF618,
inference(reorient_equations,[],[f78797]) ).
fof(f78799,definition,
sF619 = k9_relat_1(sF617,sF618),
introduced(definition,[new_symbols(definition,[sF619])],[function_definition]) ).
fof(f78800,plain,
k9_relat_1(sF617,sF618) = sF619,
inference(reorient_equations,[],[f78799]) ).
fof(f78801,definition,
sF620 = k9_relat_1(sK31,sF618),
introduced(definition,[new_symbols(definition,[sF620])],[function_definition]) ).
fof(f78802,plain,
k9_relat_1(sK31,sF618) = sF620,
inference(reorient_equations,[],[f78801]) ).
fof(f78803,definition,
sF621 = k9_relat_1(sK32,sF618),
introduced(definition,[new_symbols(definition,[sF621])],[function_definition]) ).
fof(f78804,plain,
k9_relat_1(sK32,sF618) = sF621,
inference(reorient_equations,[],[f78803]) ).
fof(f78805,definition,
sF622 = k4_xboole_0(sF620,sF621),
introduced(definition,[new_symbols(definition,[sF622])],[function_definition]) ).
fof(f78806,plain,
k4_xboole_0(sF620,sF621) = sF622,
inference(reorient_equations,[],[f78805]) ).
fof(f78807,plain,
sF619 != sF622,
inference(definition_folding,[],[f74776,f78806,f78804,f78798,f78802,f78798,f78800,f78798,f78796]) ).
fof(f80024,definition,
( spl623_240
<=> v1_relat_1(sK31) ),
introduced(definition,[new_symbols(definition,[spl623_240])],[avatar_definition]) ).
fof(f80026,plain,
( v1_relat_1(sK31)
| ~ spl623_240 ),
inference(avatar_component_clause,[],[f80024]) ).
fof(f80027,plain,
spl623_240,
inference(avatar_split_clause,[],[f74774,f80024]) ).
fof(f80029,definition,
( spl623_241
<=> v1_relat_1(sK32) ),
introduced(definition,[new_symbols(definition,[spl623_241])],[avatar_definition]) ).
fof(f80031,plain,
( v1_relat_1(sK32)
| ~ spl623_241 ),
inference(avatar_component_clause,[],[f80029]) ).
fof(f80032,plain,
spl623_241,
inference(avatar_split_clause,[],[f74775,f80029]) ).
fof(f80034,definition,
( spl623_242
<=> sF619 = sF622 ),
introduced(definition,[new_symbols(definition,[spl623_242])],[avatar_definition]) ).
fof(f80036,plain,
( sF619 != sF622
| spl623_242 ),
inference(avatar_component_clause,[],[f80034]) ).
fof(f80037,plain,
~ spl623_242,
inference(avatar_split_clause,[],[f78807,f80034]) ).
fof(f80044,definition,
( spl623_244
<=> k4_xboole_0(sK31,sK32) = sF617 ),
introduced(definition,[new_symbols(definition,[spl623_244])],[avatar_definition]) ).
fof(f80046,plain,
( k4_xboole_0(sK31,sK32) = sF617
| ~ spl623_244 ),
inference(avatar_component_clause,[],[f80044]) ).
fof(f80047,plain,
spl623_244,
inference(avatar_split_clause,[],[f78796,f80044]) ).
fof(f80049,definition,
( spl623_245
<=> k1_tarski(sK30) = sF618 ),
introduced(definition,[new_symbols(definition,[spl623_245])],[avatar_definition]) ).
fof(f80051,plain,
( k1_tarski(sK30) = sF618
| ~ spl623_245 ),
inference(avatar_component_clause,[],[f80049]) ).
fof(f80052,plain,
spl623_245,
inference(avatar_split_clause,[],[f78798,f80049]) ).
fof(f80054,definition,
( spl623_246
<=> k9_relat_1(sF617,sF618) = sF619 ),
introduced(definition,[new_symbols(definition,[spl623_246])],[avatar_definition]) ).
fof(f80056,plain,
( k9_relat_1(sF617,sF618) = sF619
| ~ spl623_246 ),
inference(avatar_component_clause,[],[f80054]) ).
fof(f80057,plain,
spl623_246,
inference(avatar_split_clause,[],[f78800,f80054]) ).
fof(f80059,definition,
( spl623_247
<=> k9_relat_1(sK31,sF618) = sF620 ),
introduced(definition,[new_symbols(definition,[spl623_247])],[avatar_definition]) ).
fof(f80061,plain,
( k9_relat_1(sK31,sF618) = sF620
| ~ spl623_247 ),
inference(avatar_component_clause,[],[f80059]) ).
fof(f80062,plain,
spl623_247,
inference(avatar_split_clause,[],[f78802,f80059]) ).
fof(f80064,definition,
( spl623_248
<=> k9_relat_1(sK32,sF618) = sF621 ),
introduced(definition,[new_symbols(definition,[spl623_248])],[avatar_definition]) ).
fof(f80066,plain,
( k9_relat_1(sK32,sF618) = sF621
| ~ spl623_248 ),
inference(avatar_component_clause,[],[f80064]) ).
fof(f80067,plain,
spl623_248,
inference(avatar_split_clause,[],[f78804,f80064]) ).
fof(f80069,definition,
( spl623_249
<=> k4_xboole_0(sF620,sF621) = sF622 ),
introduced(definition,[new_symbols(definition,[spl623_249])],[avatar_definition]) ).
fof(f80071,plain,
( k4_xboole_0(sF620,sF621) = sF622
| ~ spl623_249 ),
inference(avatar_component_clause,[],[f80069]) ).
fof(f80072,plain,
spl623_249,
inference(avatar_split_clause,[],[f78806,f80069]) ).
fof(f80073,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X1,sF618))
| r2_hidden(k4_tarski(sK30,X0),X1)
| ~ v1_relat_1(X1) )
| ~ spl623_245 ),
inference(superposition,[],[f74943,f80051]) ).
fof(f80074,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF619)
| r2_hidden(k4_tarski(sK30,X0),sF617)
| ~ v1_relat_1(sF617) )
| ~ spl623_245
| ~ spl623_246 ),
inference(superposition,[],[f80073,f80056]) ).
fof(f80075,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF621)
| r2_hidden(k4_tarski(sK30,X0),sK32)
| ~ v1_relat_1(sK32) )
| ~ spl623_245
| ~ spl623_248 ),
inference(superposition,[],[f80073,f80066]) ).
fof(f80076,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF620)
| r2_hidden(k4_tarski(sK30,X0),sK31)
| ~ v1_relat_1(sK31) )
| ~ spl623_245
| ~ spl623_247 ),
inference(superposition,[],[f80073,f80061]) ).
fof(f80077,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sK31)
| ~ r2_hidden(X0,sF620) )
| ~ spl623_240
| ~ spl623_245
| ~ spl623_247 ),
inference(forward_subsumption_resolution,[],[f80076,f80026]) ).
fof(f80078,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sK32)
| ~ r2_hidden(X0,sF621) )
| ~ spl623_241
| ~ spl623_245
| ~ spl623_248 ),
inference(forward_subsumption_resolution,[],[f80075,f80031]) ).
fof(f80080,definition,
( spl623_250
<=> v1_relat_1(sF617) ),
introduced(definition,[new_symbols(definition,[spl623_250])],[avatar_definition]) ).
fof(f80081,plain,
( v1_relat_1(sF617)
| ~ spl623_250 ),
inference(avatar_component_clause,[],[f80080]) ).
fof(f80084,definition,
( spl623_251
<=> ! [X0] :
( ~ r2_hidden(X0,sF619)
| r2_hidden(k4_tarski(sK30,X0),sF617) ) ),
introduced(definition,[new_symbols(definition,[spl623_251])],[avatar_definition]) ).
fof(f80085,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sF617)
| ~ r2_hidden(X0,sF619) )
| ~ spl623_251 ),
inference(avatar_component_clause,[],[f80084]) ).
fof(f80086,plain,
( ~ spl623_250
| spl623_251
| ~ spl623_245
| ~ spl623_246 ),
inference(avatar_split_clause,[],[f80074,f80054,f80049,f80084,f80080]) ).
fof(f80088,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_tarski(sK30,X0),X1)
| r2_hidden(X0,k9_relat_1(X1,sF618))
| ~ v1_relat_1(X1) )
| ~ spl623_245 ),
inference(superposition,[],[f74944,f80051]) ).
fof(f80138,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF617)
| r2_hidden(X0,sK31) )
| ~ spl623_244 ),
inference(superposition,[],[f78496,f80046]) ).
fof(f80139,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF622)
| r2_hidden(X0,sF620) )
| ~ spl623_249 ),
inference(superposition,[],[f78496,f80071]) ).
fof(f80153,plain,
( ! [X0] :
( r2_hidden(sK76(sF622,X0),sF620)
| r1_tarski(sF622,X0) )
| ~ spl623_249 ),
inference(resolution,[],[f80139,f75114]) ).
fof(f80166,plain,
( v1_relat_1(sF617)
| ~ v1_relat_1(sK31)
| ~ spl623_244 ),
inference(superposition,[],[f74840,f80046]) ).
fof(f80173,plain,
( v1_relat_1(sF617)
| ~ spl623_240
| ~ spl623_244 ),
inference(forward_subsumption_resolution,[],[f80166,f80026]) ).
fof(f80174,plain,
( spl623_250
| ~ spl623_240
| ~ spl623_244 ),
inference(avatar_split_clause,[],[f80173,f80044,f80024,f80080]) ).
fof(f80201,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF617)
| ~ r2_hidden(X0,sK32) )
| ~ spl623_244 ),
inference(superposition,[],[f78497,f80046]) ).
fof(f80202,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF622)
| ~ r2_hidden(X0,sF621) )
| ~ spl623_249 ),
inference(superposition,[],[f78497,f80071]) ).
fof(f80212,plain,
( ! [X0] :
( ~ r2_hidden(sK76(sF622,X0),sF621)
| r1_tarski(sF622,X0) )
| ~ spl623_249 ),
inference(resolution,[],[f80202,f75114]) ).
fof(f80266,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK31)
| r2_hidden(X0,sF617)
| r2_hidden(X0,sK32) )
| ~ spl623_244 ),
inference(superposition,[],[f78495,f80046]) ).
fof(f80267,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF620)
| r2_hidden(X0,sF622)
| r2_hidden(X0,sF621) )
| ~ spl623_249 ),
inference(superposition,[],[f78495,f80071]) ).
fof(f80276,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sF617)
| r2_hidden(k4_tarski(sK30,X0),sK32)
| ~ r2_hidden(X0,sF620) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247 ),
inference(resolution,[],[f80266,f80077]) ).
fof(f80302,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sK32)
| ~ r2_hidden(X0,sF620)
| r2_hidden(X0,k9_relat_1(sF617,sF618))
| ~ v1_relat_1(sF617) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247 ),
inference(resolution,[],[f80276,f80088]) ).
fof(f80305,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sK32)
| ~ r2_hidden(X0,sF620)
| r2_hidden(X0,k9_relat_1(sF617,sF618)) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_250 ),
inference(forward_subsumption_resolution,[],[f80302,f80081]) ).
fof(f80306,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sK32)
| r2_hidden(X0,sF619)
| ~ r2_hidden(X0,sF620) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_250 ),
inference(forward_demodulation,[],[f80305,f80056]) ).
fof(f80307,plain,
( ! [X0] :
( r2_hidden(X0,sF619)
| ~ r2_hidden(X0,sF620)
| r2_hidden(X0,k9_relat_1(sK32,sF618))
| ~ v1_relat_1(sK32) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_250 ),
inference(resolution,[],[f80306,f80088]) ).
fof(f80310,plain,
( ! [X0] :
( r2_hidden(X0,sF619)
| ~ r2_hidden(X0,sF620)
| r2_hidden(X0,k9_relat_1(sK32,sF618)) )
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_250 ),
inference(forward_subsumption_resolution,[],[f80307,f80031]) ).
fof(f80311,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF620)
| r2_hidden(X0,sF619)
| r2_hidden(X0,sF621) )
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_250 ),
inference(forward_demodulation,[],[f80310,f80066]) ).
fof(f80317,plain,
( ! [X0] :
( r2_hidden(sK76(sF622,X0),sF619)
| r2_hidden(sK76(sF622,X0),sF621)
| r1_tarski(sF622,X0) )
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_249
| ~ spl623_250 ),
inference(resolution,[],[f80311,f80153]) ).
fof(f80319,plain,
( ! [X0] :
( r2_hidden(sK76(sF622,X0),sF619)
| r1_tarski(sF622,X0) )
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_249
| ~ spl623_250 ),
inference(forward_subsumption_resolution,[],[f80317,f80212]) ).
fof(f80328,plain,
( r1_tarski(sF622,sF619)
| r1_tarski(sF622,sF619)
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_249
| ~ spl623_250 ),
inference(resolution,[],[f80319,f75115]) ).
fof(f80329,plain,
( r1_tarski(sF622,sF619)
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_249
| ~ spl623_250 ),
inference(duplicate_literal_removal,[],[f80328]) ).
fof(f80331,definition,
( spl623_272
<=> r1_tarski(sF622,sF619) ),
introduced(definition,[new_symbols(definition,[spl623_272])],[avatar_definition]) ).
fof(f80333,plain,
( r1_tarski(sF622,sF619)
| ~ spl623_272 ),
inference(avatar_component_clause,[],[f80331]) ).
fof(f80334,plain,
( spl623_272
| ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_249
| ~ spl623_250 ),
inference(avatar_split_clause,[],[f80329,f80080,f80069,f80064,f80059,f80054,f80049,f80044,f80029,f80024,f80331]) ).
fof(f80335,plain,
( ~ r1_tarski(sF619,sF622)
| sF619 = sF622
| ~ spl623_272 ),
inference(resolution,[],[f80333,f75111]) ).
fof(f80336,plain,
( ~ r1_tarski(sF619,sF622)
| spl623_242
| ~ spl623_272 ),
inference(forward_subsumption_resolution,[],[f80335,f80036]) ).
fof(f80338,definition,
( spl623_273
<=> r1_tarski(sF619,sF622) ),
introduced(definition,[new_symbols(definition,[spl623_273])],[avatar_definition]) ).
fof(f80340,plain,
( ~ r1_tarski(sF619,sF622)
| spl623_273 ),
inference(avatar_component_clause,[],[f80338]) ).
fof(f80341,plain,
( ~ spl623_273
| spl623_242
| ~ spl623_272 ),
inference(avatar_split_clause,[],[f80336,f80331,f80034,f80338]) ).
fof(f80485,plain,
( ! [X0] :
( ~ r2_hidden(k4_tarski(sK30,X0),sK32)
| ~ r2_hidden(X0,sF619) )
| ~ spl623_244
| ~ spl623_251 ),
inference(resolution,[],[f80085,f80201]) ).
fof(f80486,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK30,X0),sK31)
| ~ r2_hidden(X0,sF619) )
| ~ spl623_244
| ~ spl623_251 ),
inference(resolution,[],[f80085,f80138]) ).
fof(f80503,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF621)
| ~ r2_hidden(X0,sF619) )
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_248
| ~ spl623_251 ),
inference(resolution,[],[f80485,f80078]) ).
fof(f80523,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF619)
| r2_hidden(X0,k9_relat_1(sK31,sF618))
| ~ v1_relat_1(sK31) )
| ~ spl623_244
| ~ spl623_245
| ~ spl623_251 ),
inference(resolution,[],[f80486,f80088]) ).
fof(f80526,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF619)
| r2_hidden(X0,k9_relat_1(sK31,sF618)) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_251 ),
inference(forward_subsumption_resolution,[],[f80523,f80026]) ).
fof(f80527,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF619)
| r2_hidden(X0,sF620) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_251 ),
inference(forward_demodulation,[],[f80526,f80061]) ).
fof(f80534,plain,
( ! [X0] :
( r2_hidden(sK76(sF619,X0),sF620)
| r1_tarski(sF619,X0) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_251 ),
inference(resolution,[],[f80527,f75114]) ).
fof(f80544,plain,
( ! [X0] :
( r2_hidden(sK76(sF619,X0),sF622)
| r1_tarski(sF619,X0)
| r2_hidden(sK76(sF619,X0),sF621) )
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_249
| ~ spl623_251 ),
inference(resolution,[],[f80534,f80267]) ).
fof(f80564,plain,
( r1_tarski(sF619,sF622)
| r2_hidden(sK76(sF619,sF622),sF621)
| r1_tarski(sF619,sF622)
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_249
| ~ spl623_251 ),
inference(resolution,[],[f80544,f75115]) ).
fof(f80565,plain,
( r1_tarski(sF619,sF622)
| r2_hidden(sK76(sF619,sF622),sF621)
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_249
| ~ spl623_251 ),
inference(duplicate_literal_removal,[],[f80564]) ).
fof(f80566,plain,
( r2_hidden(sK76(sF619,sF622),sF621)
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_249
| ~ spl623_251
| spl623_273 ),
inference(forward_subsumption_resolution,[],[f80565,f80340]) ).
fof(f80568,definition,
( spl623_293
<=> r2_hidden(sK76(sF619,sF622),sF621) ),
introduced(definition,[new_symbols(definition,[spl623_293])],[avatar_definition]) ).
fof(f80570,plain,
( r2_hidden(sK76(sF619,sF622),sF621)
| ~ spl623_293 ),
inference(avatar_component_clause,[],[f80568]) ).
fof(f80571,plain,
( spl623_293
| ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_249
| ~ spl623_251
| spl623_273 ),
inference(avatar_split_clause,[],[f80566,f80338,f80084,f80069,f80059,f80049,f80044,f80024,f80568]) ).
fof(f80572,plain,
( ~ r2_hidden(sK76(sF619,sF622),sF619)
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_248
| ~ spl623_251
| ~ spl623_293 ),
inference(resolution,[],[f80570,f80503]) ).
fof(f80574,definition,
( spl623_294
<=> r2_hidden(sK76(sF619,sF622),sF619) ),
introduced(definition,[new_symbols(definition,[spl623_294])],[avatar_definition]) ).
fof(f80576,plain,
( ~ r2_hidden(sK76(sF619,sF622),sF619)
| spl623_294 ),
inference(avatar_component_clause,[],[f80574]) ).
fof(f80577,plain,
( ~ spl623_294
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_248
| ~ spl623_251
| ~ spl623_293 ),
inference(avatar_split_clause,[],[f80572,f80568,f80084,f80064,f80049,f80044,f80029,f80574]) ).
fof(f80578,plain,
( r1_tarski(sF619,sF622)
| spl623_294 ),
inference(resolution,[],[f80576,f75114]) ).
fof(f80579,plain,
( $false
| spl623_273
| spl623_294 ),
inference(forward_subsumption_resolution,[],[f80578,f80340]) ).
fof(f80580,plain,
( spl623_273
| spl623_294 ),
inference(avatar_contradiction_clause,[],[f80579]) ).
cnf(s244,plain,
spl623_240,
inference(sat_conversion,[],[f80027]) ).
cnf(s245,plain,
spl623_241,
inference(sat_conversion,[],[f80032]) ).
cnf(s246,plain,
~ spl623_242,
inference(sat_conversion,[],[f80037]) ).
cnf(s248,plain,
spl623_244,
inference(sat_conversion,[],[f80047]) ).
cnf(s249,plain,
spl623_245,
inference(sat_conversion,[],[f80052]) ).
cnf(s250,plain,
spl623_246,
inference(sat_conversion,[],[f80057]) ).
cnf(s251,plain,
spl623_247,
inference(sat_conversion,[],[f80062]) ).
cnf(s252,plain,
spl623_248,
inference(sat_conversion,[],[f80067]) ).
cnf(s253,plain,
spl623_249,
inference(sat_conversion,[],[f80072]) ).
cnf(s254,plain,
( ~ spl623_245
| ~ spl623_246
| ~ spl623_250
| spl623_251 ),
inference(sat_conversion,[],[f80086]) ).
cnf(s264,plain,
( ~ spl623_240
| ~ spl623_244
| spl623_250 ),
inference(sat_conversion,[],[f80174]) ).
cnf(s274,plain,
( ~ spl623_240
| ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_246
| ~ spl623_247
| ~ spl623_248
| ~ spl623_249
| ~ spl623_250
| spl623_272 ),
inference(sat_conversion,[],[f80334]) ).
cnf(s275,plain,
( spl623_242
| ~ spl623_272
| ~ spl623_273 ),
inference(sat_conversion,[],[f80341]) ).
cnf(s292,plain,
( ~ spl623_240
| ~ spl623_244
| ~ spl623_245
| ~ spl623_247
| ~ spl623_249
| ~ spl623_251
| spl623_273
| spl623_293 ),
inference(sat_conversion,[],[f80571]) ).
cnf(s293,plain,
( ~ spl623_241
| ~ spl623_244
| ~ spl623_245
| ~ spl623_248
| ~ spl623_251
| ~ spl623_293
| ~ spl623_294 ),
inference(sat_conversion,[],[f80577]) ).
cnf(s294,plain,
( spl623_273
| spl623_294 ),
inference(sat_conversion,[],[f80580]) ).
cnf(s300,plain,
spl623_250,
inference(rat,[],[s264,s248,s244]) ).
cnf(s306,plain,
spl623_251,
inference(rat,[],[s254,s249,s250,s300]) ).
cnf(s308,plain,
spl623_272,
inference(rat,[],[s274,s244,s245,s253,s252,s251,s250,s249,s248,s300]) ).
cnf(s310,plain,
~ spl623_273,
inference(rat,[],[s275,s246,s308]) ).
cnf(s311,plain,
spl623_294,
inference(rat,[],[s294,s310]) ).
cnf(s312,plain,
spl623_293,
inference(rat,[],[s292,s306,s244,s248,s253,s251,s249,s310]) ).
cnf(s313,plain,
$false,
inference(rat,[],[s293,s306,s245,s248,s252,s249,s311,s312]) ).
fof(f80581,plain,
$false,
inference(avatar_sat_refutation,[],[s313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU419+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n002.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Mon Sep 28 05:20:24 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.02/8.37 % (4185760)Detected formulas, will run a generic FOF schedule.
% 19.02/8.37 % (4185768)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=471765033:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 19.02/8.37 % (4185765)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=2769958134:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 19.02/8.37 % (4185766)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=3276586840:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 19.02/8.37 % (4185767)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=1041302216:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 19.02/8.37 % (4185768)Instruction limit reached!
% 19.02/8.37 % (4185768)------------------------------
% 19.02/8.37 % (4185768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/8.37 % (4185768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/8.37 % (4185768)CaDiCaL version: 2.1.3
% 19.02/8.37 % (4185768)Termination reason: Instruction limit
% 19.02/8.37 % (4185768)Termination phase: SInE selection
% 19.02/8.37 % (4185768)Time elapsed: 0.050 s
% 19.02/8.37 % (4185768)Peak memory usage: 201 MB
% 19.02/8.37 % (4185768)Instructions burned: 110 (million)
% 19.02/8.37 % (4185769)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=671902164:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 19.02/8.37 % (4185770)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1241386421:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 19.02/8.37 % (4185771)dis-21_1_sil=8000:lcm=predicate:random_seed=3289951747:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 19.02/8.37 % (4185770)Instruction limit reached!
% 19.02/8.37 % (4185770)------------------------------
% 19.02/8.37 % (4185770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/8.37 % (4185770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/8.37 % (4185770)CaDiCaL version: 2.1.3
% 19.02/8.37 % (4185770)Termination reason: Instruction limit
% 19.02/8.37 % (4185770)Termination phase: Property scanning
% 19.02/8.37 % (4185770)Time elapsed: 0.068 s
% 19.02/8.37 % (4185770)Peak memory usage: 201 MB
% 19.02/8.37 % (4185770)Instructions burned: 140 (million)
% 19.02/8.37 % (4185769)Instruction limit reached!
% 19.02/8.37 % (4185769)------------------------------
% 19.02/8.37 % (4185769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/8.37 % (4185769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/8.37 % (4185769)CaDiCaL version: 2.1.3
% 19.02/8.37 % (4185769)Termination reason: Instruction limit
% 19.02/8.37 % (4185769)Termination phase: SInE selection
% 19.02/8.37 % (4185769)Time elapsed: 0.096 s
% 19.02/8.37 % (4185769)Peak memory usage: 201 MB
% 19.02/8.37 % (4185769)Instructions burned: 120 (million)
% 19.02/8.37 % (4185771)Instruction limit reached!
% 19.02/8.37 % (4185771)------------------------------
% 19.02/8.37 % (4185771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/8.37 % (4185771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/8.37 % (4185771)CaDiCaL version: 2.1.3
% 19.02/8.37 % (4185771)Termination reason: Instruction limit
% 19.02/8.37 % (4185771)Termination phase: SInE selection
% 19.02/8.37 % (4185771)Time elapsed: 0.104 s
% 19.02/8.37 % (4185771)Peak memory usage: 201 MB
% 19.02/8.37 % (4185771)Instructions burned: 130 (million)
% 19.02/8.37 % (4185777)lrs+10_1_sil=8000:sp=occurrence:random_seed=3324314704:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 19.02/8.37 % (4185780)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3718621660:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/157Mi)
% 19.02/8.37 % (4185777)Instruction limit reached!
% 19.02/8.37 % (4185777)------------------------------
% 19.02/8.37 % (4185777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.02/8.37 % (4185777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.02/8.37 % (4185777)CaDiCaL version: 2.1.3
% 19.02/8.37 % (4185777)Termination reason: Instruction limit
% 26.19/9.30 % (4185777)Termination phase: SInE selection
% 26.19/9.30 % (4185777)Time elapsed: 0.125 s
% 26.19/9.30 % (4185777)Peak memory usage: 201 MB
% 26.19/9.30 % (4185777)Instructions burned: 286 (million)
% 26.19/9.30 % (4185781)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2410355786:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 26.19/9.30 % (4185783)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=2833765658:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 26.19/9.30 % (4185780)Instruction limit reached!
% 26.19/9.30 % (4185780)------------------------------
% 26.19/9.30 % (4185780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/9.30 % (4185780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/9.30 % (4185780)CaDiCaL version: 2.1.3
% 26.19/9.30 % (4185780)Termination reason: Instruction limit
% 26.19/9.30 % (4185780)Termination phase: Property scanning
% 26.19/9.30 % (4185780)Time elapsed: 0.076 s
% 26.19/9.30 % (4185780)Peak memory usage: 201 MB
% 26.19/9.30 % (4185780)Instructions burned: 159 (million)
% 26.19/9.30 % (4185786)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2750459269:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 26.19/9.30 % (4185783)Instruction limit reached!
% 26.19/9.30 % (4185783)------------------------------
% 26.19/9.30 % (4185783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/9.30 % (4185783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/9.30 % (4185783)CaDiCaL version: 2.1.3
% 26.19/9.30 % (4185783)Termination reason: Instruction limit
% 26.19/9.30 % (4185783)Termination phase: Property scanning
% 26.19/9.30 % (4185783)Time elapsed: 0.113 s
% 26.19/9.30 % (4185783)Peak memory usage: 201 MB
% 26.19/9.30 % (4185783)Instructions burned: 249 (million)
% 26.19/9.30 % (4185788)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3321074553:i=2350_2939 on theBenchmark for (2939ds/2350Mi)
% 26.19/9.30 % (4185781)Instruction limit reached!
% 26.19/9.30 % (4185781)------------------------------
% 26.19/9.30 % (4185781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/9.30 % (4185781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/9.30 % (4185781)CaDiCaL version: 2.1.3
% 26.19/9.30 % (4185781)Termination reason: Instruction limit
% 26.19/9.30 % (4185781)Termination phase: SInE selection
% 26.19/9.30 % (4185781)Time elapsed: 0.243 s
% 26.19/9.30 % (4185781)Peak memory usage: 201 MB
% 26.19/9.30 % (4185781)Instructions burned: 326 (million)
% 26.19/9.30 % (4185786)Instruction limit reached!
% 26.19/9.30 % (4185786)------------------------------
% 26.19/9.30 % (4185786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/9.30 % (4185786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/9.30 % (4185786)CaDiCaL version: 2.1.3
% 26.19/9.30 % (4185786)Termination reason: Instruction limit
% 26.19/9.30 % (4185786)Termination phase: SInE selection
% 26.19/9.30 % (4185786)Time elapsed: 0.126 s
% 26.19/9.30 % (4185786)Peak memory usage: 201 MB
% 26.19/9.30 % (4185786)Instructions burned: 295 (million)
% 26.19/9.30 % (4185790)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3027811530:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 26.19/9.30 % (4185790)Instruction limit reached!
% 26.19/9.30 % (4185790)------------------------------
% 26.19/9.30 % (4185790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/9.30 % (4185790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/9.30 % (4185790)CaDiCaL version: 2.1.3
% 26.19/9.30 % (4185790)Termination reason: Instruction limit
% 26.19/9.30 % (4185790)Termination phase: SInE selection
% 26.19/9.30 % (4185790)Time elapsed: 0.089 s
% 26.19/9.30 % (4185790)Peak memory usage: 201 MB
% 26.19/9.30 % (4185790)Instructions burned: 113 (million)
% 26.19/9.30 % (4185792)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3824336362:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 26.19/9.30 % (4185793)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1792466388:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2937 on theBenchmark for (2937ds/114Mi)
% 26.19/9.30 % (4185793)Instruction limit reached!
% 26.19/9.30 % (4185793)------------------------------
% 26.19/9.30 % (4185793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.10/14.01 % (4185793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.10/14.01 % (4185793)CaDiCaL version: 2.1.3
% 58.10/14.01 % (4185793)Termination reason: Instruction limit
% 58.10/14.01 % (4185793)Termination phase: Property scanning
% 58.10/14.01 % (4185793)Time elapsed: 0.032 s
% 58.10/14.01 % (4185793)Peak memory usage: 201 MB
% 58.10/14.01 % (4185793)Instructions burned: 116 (million)
% 58.10/14.01 % (4185792)Instruction limit reached!
% 58.10/14.01 % (4185792)------------------------------
% 58.10/14.01 % (4185792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.10/14.01 % (4185792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.10/14.01 % (4185792)CaDiCaL version: 2.1.3
% 58.10/14.01 % (4185792)Termination reason: Instruction limit
% 58.10/14.01 % (4185792)Termination phase: Preprocessing 1
% 58.10/14.01 % (4185792)Time elapsed: 0.101 s
% 58.10/14.01 % (4185792)Peak memory usage: 202 MB
% 58.10/14.01 % (4185792)Instructions burned: 127 (million)
% 58.10/14.01 % (4185796)lrs+10_1_sil=8000:sp=occurrence:random_seed=3391582712:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 58.10/14.01 % (4185798)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1803189971:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 58.10/14.01 % (4185799)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3843837071:i=5202:ss=axioms:sgt=16_2934 on theBenchmark for (2934ds/5202Mi)
% 58.10/14.01 % (4185798)Instruction limit reached!
% 58.10/14.01 % (4185798)------------------------------
% 58.10/14.01 % (4185798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.10/14.01 % (4185798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.10/14.01 % (4185798)CaDiCaL version: 2.1.3
% 58.10/14.01 % (4185798)Termination reason: Instruction limit
% 58.10/14.01 % (4185798)Termination phase: SInE selection
% 58.10/14.01 % (4185798)Time elapsed: 0.185 s
% 58.10/14.01 % (4185798)Peak memory usage: 202 MB
% 58.10/14.01 % (4185798)Instructions burned: 439 (million)
% 58.10/14.01 % (4185803)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4077309937:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2932 on theBenchmark for (2932ds/134Mi)
% 58.10/14.01 % (4185803)Instruction limit reached!
% 58.10/14.01 % (4185803)------------------------------
% 58.10/14.01 % (4185803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.10/14.01 % (4185803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.10/14.01 % (4185803)CaDiCaL version: 2.1.3
% 58.10/14.01 % (4185803)Termination reason: Instruction limit
% 58.10/14.01 % (4185803)Termination phase: SInE selection
% 58.10/14.01 % (4185803)Time elapsed: 0.060 s
% 58.10/14.01 % (4185803)Peak memory usage: 201 MB
% 58.10/14.01 % (4185803)Instructions burned: 136 (million)
% 58.10/14.01 % (4185805)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=922669437:st=8:i=592:sd=3:ep=RST:ss=axioms_2930 on theBenchmark for (2930ds/592Mi)
% 58.10/14.01 % (4185796)Instruction limit reached!
% 58.10/14.01 % (4185796)------------------------------
% 58.10/14.01 % (4185796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.10/14.01 % (4185796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.10/14.01 % (4185796)CaDiCaL version: 2.1.3
% 58.10/14.01 % (4185796)Termination reason: Instruction limit
% 58.10/14.01 % (4185796)Termination phase: Preprocessing 2
% 58.10/14.01 % (4185796)Time elapsed: 0.672 s
% 58.10/14.01 % (4185796)Peak memory usage: 207 MB
% 58.10/14.01 % (4185796)Instructions burned: 907 (million)
% 58.10/14.01 % (4185805)Instruction limit reached!
% 58.10/14.01 % (4185805)------------------------------
% 58.10/14.01 % (4185805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.10/14.01 % (4185805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.10/14.01 % (4185805)CaDiCaL version: 2.1.3
% 58.10/14.01 % (4185805)Termination reason: Instruction limit
% 58.10/14.01 % (4185805)Termination phase: SInE selection
% 58.10/14.01 % (4185805)Time elapsed: 0.220 s
% 58.10/14.01 % (4185805)Peak memory usage: 203 MB
% 58.10/14.01 % (4185805)Instructions burned: 593 (million)
% 58.10/14.01 % (4185807)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=913438106:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 58.10/14.01 % (4185808)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=2158484041:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2926 on theBenchmark for (2926ds/125Mi)
% 85.87/18.01 % (4185808)Instruction limit reached!
% 85.87/18.01 % (4185808)------------------------------
% 85.87/18.01 % (4185808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/18.01 % (4185808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/18.01 % (4185808)CaDiCaL version: 2.1.3
% 85.87/18.01 % (4185808)Termination reason: Instruction limit
% 85.87/18.01 % (4185808)Termination phase: Property scanning
% 85.87/18.01 % (4185808)Time elapsed: 0.049 s
% 85.87/18.01 % (4185808)Peak memory usage: 201 MB
% 85.87/18.01 % (4185808)Instructions burned: 128 (million)
% 85.87/18.01 % (4185811)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1821536708:i=134:gtgl=5:slsql=off:gtg=exists_sym_2924 on theBenchmark for (2924ds/134Mi)
% 85.87/18.01 % (4185811)Instruction limit reached!
% 85.87/18.01 % (4185811)------------------------------
% 85.87/18.01 % (4185811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/18.01 % (4185811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/18.01 % (4185811)CaDiCaL version: 2.1.3
% 85.87/18.01 % (4185811)Termination reason: Instruction limit
% 85.87/18.01 % (4185811)Termination phase: Property scanning
% 85.87/18.01 % (4185811)Time elapsed: 0.037 s
% 85.87/18.01 % (4185811)Peak memory usage: 201 MB
% 85.87/18.01 % (4185811)Instructions burned: 135 (million)
% 85.87/18.01 % (4185813)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1826584908:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2922 on theBenchmark for (2922ds/141Mi)
% 85.87/18.01 % (4185813)Instruction limit reached!
% 85.87/18.01 % (4185813)------------------------------
% 85.87/18.01 % (4185813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/18.01 % (4185813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/18.01 % (4185813)CaDiCaL version: 2.1.3
% 85.87/18.01 % (4185813)Termination reason: Instruction limit
% 85.87/18.01 % (4185813)Termination phase: SInE selection
% 85.87/18.01 % (4185813)Time elapsed: 0.062 s
% 85.87/18.01 % (4185813)Peak memory usage: 201 MB
% 85.87/18.01 % (4185813)Instructions burned: 141 (million)
% 85.87/18.01 % (4185815)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3018580857:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2920 on theBenchmark for (2920ds/431Mi)
% 85.87/18.01 % (4185788)Instruction limit reached!
% 85.87/18.01 % (4185788)------------------------------
% 85.87/18.01 % (4185788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/18.01 % (4185788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/18.01 % (4185788)CaDiCaL version: 2.1.3
% 85.87/18.01 % (4185788)Termination reason: Instruction limit
% 85.87/18.01 % (4185788)Termination phase: Preprocessing 3
% 85.87/18.01 % (4185788)Time elapsed: 1.844 s
% 85.87/18.01 % (4185788)Peak memory usage: 305 MB
% 85.87/18.01 % (4185788)Instructions burned: 2352 (million)
% 85.87/18.01 % (4185815)Instruction limit reached!
% 85.87/18.01 % (4185815)------------------------------
% 85.87/18.01 % (4185815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/18.01 % (4185815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/18.01 % (4185815)CaDiCaL version: 2.1.3
% 85.87/18.01 % (4185815)Termination reason: Instruction limit
% 85.87/18.01 % (4185815)Termination phase: SInE selection
% 85.87/18.01 % (4185815)Time elapsed: 0.182 s
% 85.87/18.01 % (4185815)Peak memory usage: 202 MB
% 85.87/18.01 % (4185815)Instructions burned: 433 (million)
% 85.87/18.01 % (4185817)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=533368437:i=6060:aac=none:ins=25_2918 on theBenchmark for (2918ds/6060Mi)
% 85.87/18.01 % (4185818)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=1429482142:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2917 on theBenchmark for (2917ds/150Mi)
% 85.87/18.01 % (4185818)Instruction limit reached!
% 85.87/18.01 % (4185818)------------------------------
% 85.87/18.01 % (4185818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/18.01 % (4185818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/18.01 % (4185818)CaDiCaL version: 2.1.3
% 85.87/18.01 % (4185818)Termination reason: Instruction limit
% 119.08/22.50 % (4185818)Termination phase: SInE selection
% 119.08/22.50 % (4185818)Time elapsed: 0.067 s
% 119.08/22.50 % (4185818)Peak memory usage: 201 MB
% 119.08/22.50 % (4185818)Instructions burned: 151 (million)
% 119.08/22.50 % (4185821)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2439548797:i=14155:bd=all_2915 on theBenchmark for (2915ds/14155Mi)
% 119.08/22.50 % (4185799)Instruction limit reached!
% 119.08/22.50 % (4185799)------------------------------
% 119.08/22.50 % (4185799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.08/22.50 % (4185799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.08/22.50 % (4185799)CaDiCaL version: 2.1.3
% 119.08/22.50 % (4185799)Termination reason: Instruction limit
% 119.08/22.50 % (4185799)Termination phase: Saturation
% 119.08/22.50 % (4185799)Time elapsed: 3.577 s
% 119.08/22.50 % (4185799)Peak memory usage: 330 MB
% 119.08/22.50 % (4185799)Instructions burned: 5203 (million)
% 119.08/22.50 % (4185823)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3540047010:i=667:av=off:fsr=off_2896 on theBenchmark for (2896ds/667Mi)
% 119.08/22.50 % (4185823)Instruction limit reached!
% 119.08/22.50 % (4185823)------------------------------
% 119.08/22.50 % (4185823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.08/22.50 % (4185823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.08/22.50 % (4185823)CaDiCaL version: 2.1.3
% 119.08/22.50 % (4185823)Termination reason: Instruction limit
% 119.08/22.50 % (4185823)Termination phase: Preprocessing 2
% 119.08/22.50 % (4185823)Time elapsed: 0.606 s
% 119.08/22.50 % (4185823)Peak memory usage: 218 MB
% 119.08/22.50 % (4185823)Instructions burned: 667 (million)
% 119.08/22.50 % (4185825)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=2621367808:s2a=on:i=185:s2at=1.8:fdi=4_2888 on theBenchmark for (2888ds/185Mi)
% 119.08/22.50 % (4185825)Instruction limit reached!
% 119.08/22.50 % (4185825)------------------------------
% 119.08/22.50 % (4185825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.08/22.50 % (4185825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.08/22.50 % (4185825)CaDiCaL version: 2.1.3
% 119.08/22.50 % (4185825)Termination reason: Instruction limit
% 119.08/22.50 % (4185825)Termination phase: SInE selection
% 119.08/22.50 % (4185825)Time elapsed: 0.144 s
% 119.08/22.50 % (4185825)Peak memory usage: 201 MB
% 119.08/22.50 % (4185825)Instructions burned: 186 (million)
% 119.08/22.50 % (4185827)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2699888222:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2885 on theBenchmark for (2885ds/193Mi)
% 119.08/22.50 % (4185827)Instruction limit reached!
% 119.08/22.50 % (4185827)------------------------------
% 119.08/22.50 % (4185827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.08/22.50 % (4185827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.08/22.50 % (4185827)CaDiCaL version: 2.1.3
% 119.08/22.50 % (4185827)Termination reason: Instruction limit
% 119.08/22.50 % (4185827)Termination phase: SInE selection
% 119.08/22.50 % (4185827)Time elapsed: 0.155 s
% 119.08/22.50 % (4185827)Peak memory usage: 201 MB
% 119.08/22.50 % (4185827)Instructions burned: 193 (million)
% 119.08/22.50 % (4185829)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3830245566:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2882 on theBenchmark for (2882ds/4850Mi)
% 119.08/22.50 % (4185821)Instruction limit reached!
% 119.08/22.50 % (4185821)------------------------------
% 119.08/22.50 % (4185821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.08/22.50 % (4185821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.08/22.50 % (4185821)CaDiCaL version: 2.1.3
% 119.08/22.50 % (4185821)Termination reason: Instruction limit
% 119.08/22.50 % (4185821)Termination phase: Property scanning
% 119.08/22.50 % (4185821)Time elapsed: 4.224 s
% 119.08/22.50 % (4185821)Peak memory usage: 447 MB
% 119.08/22.50 % (4185821)Instructions burned: 14160 (million)
% 119.08/22.50 % (4185831)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2694865388:i=12111:sd=1:ss=included_2871 on theBenchmark for (2871ds/12111Mi)
% 119.08/22.50 % (4185817)Instruction limit reached!
% 119.08/22.50 % (4185817)------------------------------
% 119.08/22.50 % (4185817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.88/25.72 % (4185817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.88/25.72 % (4185817)CaDiCaL version: 2.1.3
% 141.88/25.72 % (4185817)Termination reason: Instruction limit
% 141.88/25.72 % (4185817)Termination phase: NewCNF
% 141.88/25.72 % (4185817)Time elapsed: 4.869 s
% 141.88/25.72 % (4185817)Peak memory usage: 381 MB
% 141.88/25.72 % (4185817)Instructions burned: 6061 (million)
% 141.88/25.72 % (4185833)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2963489166:i=319:kws=precedence:fsr=off_2868 on theBenchmark for (2868ds/319Mi)
% 141.88/25.72 % (4185833)Instruction limit reached!
% 141.88/25.72 % (4185833)------------------------------
% 141.88/25.72 % (4185833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.88/25.72 % (4185833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.88/25.72 % (4185833)CaDiCaL version: 2.1.3
% 141.88/25.72 % (4185833)Termination reason: Instruction limit
% 141.88/25.72 % (4185833)Termination phase: Preprocessing 1
% 141.88/25.72 % (4185833)Time elapsed: 0.237 s
% 141.88/25.72 % (4185833)Peak memory usage: 203 MB
% 141.88/25.72 % (4185833)Instructions burned: 320 (million)
% 141.88/25.72 % (4185835)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3085542501:i=2064:ep=RST_2863 on theBenchmark for (2863ds/2064Mi)
% 141.88/25.72 % (4185829)Instruction limit reached!
% 141.88/25.72 % (4185829)------------------------------
% 141.88/25.72 % (4185829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.88/25.72 % (4185829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.88/25.72 % (4185829)CaDiCaL version: 2.1.3
% 141.88/25.72 % (4185829)Termination reason: Instruction limit
% 141.88/25.72 % (4185829)Termination phase: Property scanning
% 141.88/25.72 % (4185829)Time elapsed: 3.309 s
% 141.88/25.72 % (4185829)Peak memory usage: 352 MB
% 141.88/25.72 % (4185829)Instructions burned: 4852 (million)
% 141.88/25.72 % (4185835)Instruction limit reached!
% 141.88/25.72 % (4185835)------------------------------
% 141.88/25.72 % (4185835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.88/25.72 % (4185835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.88/25.72 % (4185835)CaDiCaL version: 2.1.3
% 141.88/25.72 % (4185835)Termination reason: Instruction limit
% 141.88/25.72 % (4185835)Termination phase: Preprocessing 3
% 141.88/25.72 % (4185835)Time elapsed: 1.658 s
% 141.88/25.72 % (4185835)Peak memory usage: 317 MB
% 141.88/25.72 % (4185835)Instructions burned: 2065 (million)
% 141.88/25.72 % (4185837)dis-1011_128_sil=32000:random_seed=2954911058:i=3706:ep=RST:av=off_2846 on theBenchmark for (2846ds/3706Mi)
% 141.88/25.72 % (4185839)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4050960457:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2845 on theBenchmark for (2845ds/757Mi)
% 141.88/25.72 % (4185807)Instruction limit reached!
% 141.88/25.72 % (4185807)------------------------------
% 141.88/25.72 % (4185807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.88/25.72 % (4185807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.88/25.72 % (4185807)CaDiCaL version: 2.1.3
% 141.88/25.72 % (4185807)Termination reason: Instruction limit
% 141.88/25.72 % (4185807)Termination phase: Saturation
% 141.88/25.72 % (4185807)Time elapsed: 8.394 s
% 141.88/25.72 % (4185807)Peak memory usage: 439 MB
% 141.88/25.72 % (4185807)Instructions burned: 13194 (million)
% 141.88/25.72 % (4185841)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3893205686:i=13913:ss=axioms:sgt=8_2841 on theBenchmark for (2841ds/13913Mi)
% 141.88/25.72 % (4185839)Instruction limit reached!
% 141.88/25.72 % (4185839)------------------------------
% 141.88/25.72 % (4185839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.88/25.72 % (4185839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.88/25.72 % (4185839)CaDiCaL version: 2.1.3
% 141.88/25.72 % (4185839)Termination reason: Instruction limit
% 141.88/25.72 % (4185839)Termination phase: Saturation
% 141.88/25.72 % (4185839)Time elapsed: 0.603 s
% 141.88/25.72 % (4185839)Peak memory usage: 211 MB
% 141.88/25.72 % (4185839)Instructions burned: 758 (million)
% 141.88/25.72 % (4185843)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2679289037:i=9925:aac=none_2837 on theBenchmark for (2837ds/9925Mi)
% 141.88/25.72 % (4185831)Instruction limit reached!
% 141.88/25.72 % (4185831)------------------------------
% 141.88/25.72 % (4185831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185831)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185831)Termination reason: Instruction limit
% 94.90/28.63 % (4185831)Termination phase: Saturation
% 94.90/28.63 % (4185831)Time elapsed: 4.167 s
% 94.90/28.63 % (4185831)Peak memory usage: 353 MB
% 94.90/28.63 % (4185831)Instructions burned: 12113 (million)
% 94.90/28.63 % (4185845)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1400399901:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2828 on theBenchmark for (2828ds/2479Mi)
% 94.90/28.63 % (4185837)Instruction limit reached!
% 94.90/28.63 % (4185837)------------------------------
% 94.90/28.63 % (4185837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185837)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185837)Termination reason: Instruction limit
% 94.90/28.63 % (4185837)Termination phase: Preprocessing 3
% 94.90/28.63 % (4185837)Time elapsed: 2.601 s
% 94.90/28.63 % (4185837)Peak memory usage: 378 MB
% 94.90/28.63 % (4185837)Instructions burned: 3707 (million)
% 94.90/28.63 % (4185847)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2901467602:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2818 on theBenchmark for (2818ds/440Mi)
% 94.90/28.63 % (4185845)Instruction limit reached!
% 94.90/28.63 % (4185845)------------------------------
% 94.90/28.63 % (4185845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185845)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185845)Termination reason: Instruction limit
% 94.90/28.63 % (4185845)Termination phase: Saturation
% 94.90/28.63 % (4185845)Time elapsed: 0.944 s
% 94.90/28.63 % (4185845)Peak memory usage: 223 MB
% 94.90/28.63 % (4185845)Instructions burned: 2483 (million)
% 94.90/28.63 % (4185849)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1269610222:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2816 on theBenchmark for (2816ds/11145Mi)
% 94.90/28.63 % (4185847)Instruction limit reached!
% 94.90/28.63 % (4185847)------------------------------
% 94.90/28.63 % (4185847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185847)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185847)Termination reason: Instruction limit
% 94.90/28.63 % (4185847)Termination phase: Property scanning
% 94.90/28.63 % (4185847)Time elapsed: 0.193 s
% 94.90/28.63 % (4185847)Peak memory usage: 201 MB
% 94.90/28.63 % (4185847)Instructions burned: 440 (million)
% 94.90/28.63 % (4185853)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2274076602:cts=off:i=3034:av=off:er=known:fsd=on_2814 on theBenchmark for (2814ds/3034Mi)
% 94.90/28.63 % (4185853)Instruction limit reached!
% 94.90/28.63 % (4185853)------------------------------
% 94.90/28.63 % (4185853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185853)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185853)Termination reason: Instruction limit
% 94.90/28.63 % (4185853)Termination phase: Preprocessing 3
% 94.90/28.63 % (4185853)Time elapsed: 2.232 s
% 94.90/28.63 % (4185853)Peak memory usage: 337 MB
% 94.90/28.63 % (4185853)Instructions burned: 3035 (million)
% 94.90/28.63 % (4185855)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1934184363:st=2:s2a=on:i=524:s2at=2:ss=axioms_2790 on theBenchmark for (2790ds/524Mi)
% 94.90/28.63 % (4185855)Instruction limit reached!
% 94.90/28.63 % (4185855)------------------------------
% 94.90/28.63 % (4185855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185855)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185855)Termination reason: Instruction limit
% 94.90/28.63 % (4185855)Termination phase: SInE selection
% 94.90/28.63 % (4185855)Time elapsed: 0.349 s
% 94.90/28.63 % (4185855)Peak memory usage: 202 MB
% 94.90/28.63 % (4185855)Instructions burned: 525 (million)
% 94.90/28.63 % (4185857)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1372285465:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2785 on theBenchmark for (2785ds/1016Mi)
% 94.90/28.63 % (4185843)Instruction limit reached!
% 94.90/28.63 % (4185843)------------------------------
% 94.90/28.63 % (4185843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185843)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185843)Termination reason: Instruction limit
% 94.90/28.63 % (4185843)Termination phase: Property scanning
% 94.90/28.63 % (4185843)Time elapsed: 5.563 s
% 94.90/28.63 % (4185843)Peak memory usage: 447 MB
% 94.90/28.63 % (4185843)Instructions burned: 9926 (million)
% 94.90/28.63 % (4185859)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1141913848:i=14123:bd=preordered:ins=4_2779 on theBenchmark for (2779ds/14123Mi)
% 94.90/28.63 % (4185849)Instruction limit reached!
% 94.90/28.63 % (4185849)------------------------------
% 94.90/28.63 % (4185849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185849)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185849)Termination reason: Instruction limit
% 94.90/28.63 % (4185849)Termination phase: Saturation
% 94.90/28.63 % (4185849)Time elapsed: 3.893 s
% 94.90/28.63 % (4185849)Peak memory usage: 366 MB
% 94.90/28.63 % (4185849)Instructions burned: 11149 (million)
% 94.90/28.63 % (4185857)Instruction limit reached!
% 94.90/28.63 % (4185857)------------------------------
% 94.90/28.63 % (4185857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185857)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185857)Termination reason: Instruction limit
% 94.90/28.63 % (4185857)Termination phase: Saturation
% 94.90/28.63 % (4185857)Time elapsed: 0.743 s
% 94.90/28.63 % (4185857)Peak memory usage: 214 MB
% 94.90/28.63 % (4185857)Instructions burned: 1016 (million)
% 94.90/28.63 % (4185861)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=662717827:i=5781:kws=precedence:bd=all:rawr=on_2776 on theBenchmark for (2776ds/5781Mi)
% 94.90/28.63 % (4185862)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=946046768:i=2448:gtgl=5:bd=preordered:gtg=all_2776 on theBenchmark for (2776ds/2448Mi)
% 94.90/28.63 % (4185862)Instruction limit reached!
% 94.90/28.63 % (4185862)------------------------------
% 94.90/28.63 % (4185862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185862)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185862)Termination reason: Instruction limit
% 94.90/28.63 % (4185862)Termination phase: Property scanning
% 94.90/28.63 % (4185862)Time elapsed: 1.046 s
% 94.90/28.63 % (4185862)Peak memory usage: 201 MB
% 94.90/28.63 % (4185862)Instructions burned: 2448 (million)
% 94.90/28.63 % (4185865)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2640798747:i=3223:kws=precedence:fgj=on:av=off_2763 on theBenchmark for (2763ds/3223Mi)
% 94.90/28.63 % (4185861)Instruction limit reached!
% 94.90/28.63 % (4185861)------------------------------
% 94.90/28.63 % (4185861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185861)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185861)Termination reason: Instruction limit
% 94.90/28.63 % (4185861)Termination phase: Property scanning
% 94.90/28.63 % (4185861)Time elapsed: 2.201 s
% 94.90/28.63 % (4185861)Peak memory usage: 412 MB
% 94.90/28.63 % (4185861)Instructions burned: 5784 (million)
% 94.90/28.63 % (4185841)Instruction limit reached!
% 94.90/28.63 % (4185841)------------------------------
% 94.90/28.63 % (4185841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185841)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185841)Termination reason: Instruction limit
% 94.90/28.63 % (4185841)Termination phase: Saturation
% 94.90/28.63 % (4185841)Time elapsed: 8.721 s
% 94.90/28.63 % (4185841)Peak memory usage: 376 MB
% 94.90/28.63 % (4185841)Instructions burned: 13913 (million)
% 94.90/28.63 % (4185867)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=824793124:st=5.6:i=2033:sd=3:ss=axioms_2752 on theBenchmark for (2752ds/2033Mi)
% 94.90/28.63 % (4185868)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=7267572:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2751 on theBenchmark for (2751ds/2055Mi)
% 94.90/28.63 % (4185867)Instruction limit reached!
% 94.90/28.63 % (4185867)------------------------------
% 94.90/28.63 % (4185867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185867)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185867)Termination reason: Instruction limit
% 94.90/28.63 % (4185867)Termination phase: Naming
% 94.90/28.63 % (4185867)Time elapsed: 0.917 s
% 94.90/28.63 % (4185867)Peak memory usage: 236 MB
% 94.90/28.63 % (4185867)Instructions burned: 2035 (million)
% 94.90/28.63 % (4185871)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1723594367:i=21611:sd=3:ss=axioms_2742 on theBenchmark for (2742ds/21611Mi)
% 94.90/28.63 % (4185868)Instruction limit reached!
% 94.90/28.63 % (4185868)------------------------------
% 94.90/28.63 % (4185868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185868)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185868)Termination reason: Instruction limit
% 94.90/28.63 % (4185868)Termination phase: SInE selection
% 94.90/28.63 % (4185868)Time elapsed: 1.021 s
% 94.90/28.63 % (4185868)Peak memory usage: 203 MB
% 94.90/28.63 % (4185868)Instructions burned: 2055 (million)
% 94.90/28.63 % (4185865)Instruction limit reached!
% 94.90/28.63 % (4185865)------------------------------
% 94.90/28.63 % (4185865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185865)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185865)Termination reason: Instruction limit
% 94.90/28.63 % (4185865)Termination phase: Preprocessing 3
% 94.90/28.63 % (4185865)Time elapsed: 2.356 s
% 94.90/28.63 % (4185865)Peak memory usage: 343 MB
% 94.90/28.63 % (4185865)Instructions burned: 3223 (million)
% 94.90/28.63 % (4185873)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3401592730:i=4835:sd=13:ss=axioms:sgt=23_2739 on theBenchmark for (2739ds/4835Mi)
% 94.90/28.63 % (4185875)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3139976100:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2737 on theBenchmark for (2737ds/797Mi)
% 94.90/28.63 % (4185875)Instruction limit reached!
% 94.90/28.63 % (4185875)------------------------------
% 94.90/28.63 % (4185875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.90/28.63 % (4185875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/28.63 % (4185875)CaDiCaL version: 2.1.3
% 94.90/28.63 % (4185875)Termination reason: Instruction limit
% 94.90/28.63 % (4185875)Termination phase: SInE selection
% 94.90/28.63 % (4185875)Time elapsed: 0.516 s
% 94.90/28.63 % (4185875)Peak memory usage: 203 MB
% 94.90/28.63 % (4185875)Instructions burned: 798 (million)
% 94.90/28.63 % (4185877)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2923539583:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2731 on theBenchmark for (2731ds/2326Mi)
% 94.90/28.63 % (4185871)First to succeed.
% 94.90/28.63 % (4185871)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4185760"
% 94.90/28.63 % (4185871)Refutation found. Thanks to Tanya!
% 94.90/28.63 % SZS status Theorem for theBenchmark
% 94.90/28.63 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/28.90 % (4185871)------------------------------
% 0.17/28.90 % (4185871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/28.90 % (4185871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/28.90 % (4185871)CaDiCaL version: 2.1.3
% 0.17/28.90 % (4185871)Termination reason: Refutation
% 0.17/28.90 % (4185871)Time elapsed: 1.476 s
% 0.17/28.90 % (4185871)Peak memory usage: 322 MB
% 0.17/28.90 % (4185871)Instructions burned: 3839 (million)
% 0.17/28.90 % (4185871)------------------------------
% 0.17/28.90 % (4185871)------------------------------
% 0.17/28.90 % (4185760)Success in time 27.771 s
% 0.17/28.90 % Vampire exiting
%------------------------------------------------------------------------------