%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR097+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 09:42:58 AM UTC 2026
% Result : ContradictoryAxioms 115.36s 24.27s
% Output : Refutation 150.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 85 ( 13 unt; 10 def)
% Number of atoms : 370 ( 9 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 465 ( 180 ~; 155 |; 112 &)
% ( 13 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-3 aty)
% Number of variables : 108 ( 0 sgn 87 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1365,axiom,
! [X0] :
( s__instance(X0,s__Chain)
=> ? [X1,X2,X3] :
( s__instance(X3,s__Object)
& s__instance(X2,s__Object)
& s__instance(X1,s__Object)
& s__instance(X1,s__ChainLink)
& s__instance(X2,s__ChainLink)
& s__instance(X3,s__ChainLink)
& ~ s__equals(X1,X2)
& ~ s__equals(X2,X3)
& ~ s__equals(X3,X1)
& s__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_1399) ).
fof(f27191,axiom,
! [X0] : s__instance(X0,s__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_27371) ).
fof(f28244,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__Object)
& s__instance(X1,s__Object)
& s__instance(X0,s__Object) )
=> ( ( s__crosses(X0,X1)
& s__crosses(X1,X2) )
=> s__crosses(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_28426) ).
fof(f32412,axiom,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__instance(X3,X2)
& s__instance(X4,X0)
& s__instance(X5,X1) )
=> ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_32603) ).
fof(f152011,plain,
! [X0] :
( ? [X1,X2,X3] :
( s__instance(X3,s__Object)
& s__instance(X2,s__Object)
& s__instance(X1,s__Object)
& s__instance(X1,s__ChainLink)
& s__instance(X2,s__ChainLink)
& s__instance(X3,s__ChainLink)
& ~ s__equals(X1,X2)
& ~ s__equals(X2,X3)
& ~ s__equals(X3,X1)
& s__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) )
| ~ s__instance(X0,s__Chain) ),
inference(ennf_transformation,[],[f1365]) ).
fof(f156669,plain,
! [X0,X1,X2] :
( s__crosses(X0,X2)
| ~ s__crosses(X0,X1)
| ~ s__crosses(X1,X2)
| ~ s__instance(X2,s__Object)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f28244]) ).
fof(f156670,plain,
! [X0,X1,X2] :
( s__crosses(X0,X2)
| ~ s__crosses(X0,X1)
| ~ s__crosses(X1,X2)
| ~ s__instance(X2,s__Object)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f156669]) ).
fof(f162808,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
inference(ennf_transformation,[],[f32412]) ).
fof(f162809,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
inference(flattening,[],[f162808]) ).
fof(f168541,definition,
( ? [X1,X2,X3] :
( s__instance(X3,s__Object)
& s__instance(X2,s__Object)
& s__instance(X1,s__Object)
& s__instance(X1,s__ChainLink)
& s__instance(X2,s__ChainLink)
& s__instance(X3,s__ChainLink)
& ~ s__equals(X1,X2)
& ~ s__equals(X2,X3)
& ~ s__equals(X3,X1)
& s__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f168542,plain,
! [X0] :
( sP14
| ~ s__instance(X0,s__Chain) ),
inference(definition_folding,[],[f152011,f168541]) ).
fof(f168674,definition,
! [X1,X2,X0] :
( sP84(X1,X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f168675,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> sP84(X1,X2,X0) ),
inference(definition_folding,[],[f162809,f168674]) ).
fof(f169024,plain,
( ? [X1,X2,X3] :
( s__instance(X3,s__Object)
& s__instance(X2,s__Object)
& s__instance(X1,s__Object)
& s__instance(X1,s__ChainLink)
& s__instance(X2,s__ChainLink)
& s__instance(X3,s__ChainLink)
& ~ s__equals(X1,X2)
& ~ s__equals(X2,X3)
& ~ s__equals(X3,X1)
& s__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) )
| ~ sP14 ),
inference(nnf_transformation,[],[f168541]) ).
fof(f169025,plain,
( ? [X0,X1,X2] :
( s__instance(X2,s__Object)
& s__instance(X1,s__Object)
& s__instance(X0,s__Object)
& s__instance(X0,s__ChainLink)
& s__instance(X1,s__ChainLink)
& s__instance(X2,s__ChainLink)
& ~ s__equals(X0,X1)
& ~ s__equals(X1,X2)
& ~ s__equals(X2,X0)
& s__crosses(X0,X1)
& s__crosses(X1,X2)
& ~ s__crosses(X0,X2) )
| ~ sP14 ),
inference(rectify,[],[f169024]) ).
fof(f169026,plain,
( ( s__instance(sK359,s__Object)
& s__instance(sK358,s__Object)
& s__instance(sK357,s__Object)
& s__instance(sK357,s__ChainLink)
& s__instance(sK358,s__ChainLink)
& s__instance(sK359,s__ChainLink)
& ~ s__equals(sK357,sK358)
& ~ s__equals(sK358,sK359)
& ~ s__equals(sK359,sK357)
& s__crosses(sK357,sK358)
& s__crosses(sK358,sK359)
& ~ s__crosses(sK357,sK359) )
| ~ sP14 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK357,sK358,sK359]),skolemize(X0,sK357),skolemize(X1,sK358),skolemize(X2,sK359)],[f169025]) ).
fof(f169901,plain,
! [X1,X2,X0] :
( ( sP84(X1,X2,X0)
| ? [X3,X4,X5] :
( ( ~ s__instance(X3,X1)
| ~ s__instance(X4,X1)
| ( ~ s__instance(X5,X2)
& ~ s__instance(X5,X0) ) )
& s__instance(X3,X2)
& s__instance(X4,X0)
& s__instance(X5,X1)
& s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) ) )
& ( ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ sP84(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f168674]) ).
fof(f169902,plain,
! [X0,X1,X2] :
( ( sP84(X0,X1,X2)
| ? [X3,X4,X5] :
( ( ~ s__instance(X3,X0)
| ~ s__instance(X4,X0)
| ( ~ s__instance(X5,X1)
& ~ s__instance(X5,X2) ) )
& s__instance(X3,X1)
& s__instance(X4,X2)
& s__instance(X5,X0)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass)
& s__instance(X2,s__SetOrClass) ) )
& ( ! [X6,X7,X8] :
( ( s__instance(X6,X0)
& s__instance(X7,X0)
& ( s__instance(X8,X1)
| s__instance(X8,X2) ) )
| ~ s__instance(X6,X1)
| ~ s__instance(X7,X2)
| ~ s__instance(X8,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) )
| ~ sP84(X0,X1,X2) ) ),
inference(rectify,[],[f169901]) ).
fof(f169903,plain,
! [X0,X1,X2] :
( ( sP84(X0,X1,X2)
| ( ( ~ s__instance(sK1217(X0,X1,X2),X0)
| ~ s__instance(sK1218(X0,X1,X2),X0)
| ( ~ s__instance(sK1219(X0,X1,X2),X1)
& ~ s__instance(sK1219(X0,X1,X2),X2) ) )
& s__instance(sK1217(X0,X1,X2),X1)
& s__instance(sK1218(X0,X1,X2),X2)
& s__instance(sK1219(X0,X1,X2),X0)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass)
& s__instance(X2,s__SetOrClass) ) )
& ( ! [X6,X7,X8] :
( ( s__instance(X6,X0)
& s__instance(X7,X0)
& ( s__instance(X8,X1)
| s__instance(X8,X2) ) )
| ~ s__instance(X6,X1)
| ~ s__instance(X7,X2)
| ~ s__instance(X8,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) )
| ~ sP84(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1217,sK1218,sK1219]),skolemize(X3,sK1217(X0,X1,X2)),skolemize(X4,sK1218(X0,X1,X2)),skolemize(X5,sK1219(X0,X1,X2))],[f169902]) ).
fof(f169904,plain,
! [X0,X1,X2] :
( ( X1 = s__UnionFn(X2,X0)
| ~ sP84(X1,X2,X0) )
& ( sP84(X1,X2,X0)
| s__UnionFn(X2,X0) != X1 ) ),
inference(nnf_transformation,[],[f168675]) ).
fof(f173497,plain,
( ~ s__crosses(sK357,sK359)
| ~ sP14 ),
inference(cnf_transformation,[],[f169026]) ).
fof(f173498,plain,
( s__crosses(sK358,sK359)
| ~ sP14 ),
inference(cnf_transformation,[],[f169026]) ).
fof(f173499,plain,
( s__crosses(sK357,sK358)
| ~ sP14 ),
inference(cnf_transformation,[],[f169026]) ).
fof(f173506,plain,
( s__instance(sK357,s__Object)
| ~ sP14 ),
inference(cnf_transformation,[],[f169026]) ).
fof(f173507,plain,
( s__instance(sK358,s__Object)
| ~ sP14 ),
inference(cnf_transformation,[],[f169026]) ).
fof(f173508,plain,
( s__instance(sK359,s__Object)
| ~ sP14 ),
inference(cnf_transformation,[],[f169026]) ).
fof(f173509,plain,
! [X0] :
( sP14
| ~ s__instance(X0,s__Chain) ),
inference(cnf_transformation,[],[f168542]) ).
fof(f195233,plain,
! [X0] : s__instance(X0,s__Entity),
inference(cnf_transformation,[],[f27191]) ).
fof(f196514,plain,
! [X2,X0,X1] :
( ~ s__crosses(X1,X2)
| ~ s__crosses(X0,X1)
| s__crosses(X0,X2)
| ~ s__instance(X2,s__Object)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f156670]) ).
fof(f200565,plain,
! [X2,X0,X1] :
( s__instance(sK1217(X0,X1,X2),X1)
| sP84(X0,X1,X2) ),
inference(cnf_transformation,[],[f169903]) ).
fof(f200569,plain,
! [X2,X0,X1] :
( ~ sP84(X1,X2,X0)
| s__UnionFn(X2,X0) = X1 ),
inference(cnf_transformation,[],[f169904]) ).
fof(f321732,definition,
( spl3218_576
<=> ! [X0] : ~ s__instance(X0,s__Chain) ),
introduced(definition,[new_symbols(definition,[spl3218_576])],[avatar_definition]) ).
fof(f321733,plain,
( ! [X0] : ~ s__instance(X0,s__Chain)
| ~ spl3218_576 ),
inference(avatar_component_clause,[],[f321732]) ).
fof(f321735,definition,
( spl3218_577
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl3218_577])],[avatar_definition]) ).
fof(f321738,plain,
( spl3218_576
| spl3218_577 ),
inference(avatar_split_clause,[],[f173509,f321735,f321732]) ).
fof(f321740,definition,
( spl3218_578
<=> s__crosses(sK357,sK359) ),
introduced(definition,[new_symbols(definition,[spl3218_578])],[avatar_definition]) ).
fof(f321742,plain,
( ~ s__crosses(sK357,sK359)
| spl3218_578 ),
inference(avatar_component_clause,[],[f321740]) ).
fof(f321743,plain,
( ~ spl3218_577
| ~ spl3218_578 ),
inference(avatar_split_clause,[],[f173497,f321740,f321735]) ).
fof(f321745,definition,
( spl3218_579
<=> s__crosses(sK358,sK359) ),
introduced(definition,[new_symbols(definition,[spl3218_579])],[avatar_definition]) ).
fof(f321747,plain,
( s__crosses(sK358,sK359)
| ~ spl3218_579 ),
inference(avatar_component_clause,[],[f321745]) ).
fof(f321748,plain,
( ~ spl3218_577
| spl3218_579 ),
inference(avatar_split_clause,[],[f173498,f321745,f321735]) ).
fof(f321750,definition,
( spl3218_580
<=> s__crosses(sK357,sK358) ),
introduced(definition,[new_symbols(definition,[spl3218_580])],[avatar_definition]) ).
fof(f321752,plain,
( s__crosses(sK357,sK358)
| ~ spl3218_580 ),
inference(avatar_component_clause,[],[f321750]) ).
fof(f321753,plain,
( ~ spl3218_577
| spl3218_580 ),
inference(avatar_split_clause,[],[f173499,f321750,f321735]) ).
fof(f321785,definition,
( spl3218_587
<=> s__instance(sK357,s__Object) ),
introduced(definition,[new_symbols(definition,[spl3218_587])],[avatar_definition]) ).
fof(f321787,plain,
( s__instance(sK357,s__Object)
| ~ spl3218_587 ),
inference(avatar_component_clause,[],[f321785]) ).
fof(f321788,plain,
( ~ spl3218_577
| spl3218_587 ),
inference(avatar_split_clause,[],[f173506,f321785,f321735]) ).
fof(f321790,definition,
( spl3218_588
<=> s__instance(sK358,s__Object) ),
introduced(definition,[new_symbols(definition,[spl3218_588])],[avatar_definition]) ).
fof(f321792,plain,
( s__instance(sK358,s__Object)
| ~ spl3218_588 ),
inference(avatar_component_clause,[],[f321790]) ).
fof(f321793,plain,
( ~ spl3218_577
| spl3218_588 ),
inference(avatar_split_clause,[],[f173507,f321790,f321735]) ).
fof(f321795,definition,
( spl3218_589
<=> s__instance(sK359,s__Object) ),
introduced(definition,[new_symbols(definition,[spl3218_589])],[avatar_definition]) ).
fof(f321797,plain,
( s__instance(sK359,s__Object)
| ~ spl3218_589 ),
inference(avatar_component_clause,[],[f321795]) ).
fof(f321798,plain,
( ~ spl3218_577
| spl3218_589 ),
inference(avatar_split_clause,[],[f173508,f321795,f321735]) ).
fof(f322583,plain,
( ! [X0,X1] : sP84(X0,s__Chain,X1)
| ~ spl3218_576 ),
inference(resolution,[],[f321733,f200565]) ).
fof(f322585,plain,
( ! [X0,X1] : s__UnionFn(s__Chain,X0) = X1
| ~ spl3218_576 ),
inference(resolution,[],[f322583,f200569]) ).
fof(f322586,plain,
( ! [X2,X0] : X0 = X2
| ~ spl3218_576 ),
inference(superposition,[],[f322585,f322585]) ).
fof(f322592,plain,
( ! [X0,X1] : ~ s__instance(X1,X0)
| ~ spl3218_576 ),
inference(superposition,[],[f321733,f322586]) ).
fof(f322602,plain,
( ! [X0,X1] : s__instance(X1,X0)
| ~ spl3218_576 ),
inference(superposition,[],[f195233,f322586]) ).
fof(f322610,plain,
( $false
| ~ spl3218_576 ),
inference(forward_subsumption_resolution,[],[f322592,f322602]) ).
fof(f322611,plain,
~ spl3218_576,
inference(avatar_contradiction_clause,[],[f322610]) ).
fof(f322612,plain,
( ! [X0] :
( ~ s__crosses(X0,sK358)
| s__crosses(X0,sK359)
| ~ s__instance(sK359,s__Object)
| ~ s__instance(sK358,s__Object)
| ~ s__instance(X0,s__Object) )
| ~ spl3218_579 ),
inference(resolution,[],[f321747,f196514]) ).
fof(f322613,plain,
( ! [X0] :
( ~ s__crosses(X0,sK358)
| s__crosses(X0,sK359)
| ~ s__instance(sK358,s__Object)
| ~ s__instance(X0,s__Object) )
| ~ spl3218_579
| ~ spl3218_589 ),
inference(forward_subsumption_resolution,[],[f322612,f321797]) ).
fof(f322614,plain,
( ! [X0] :
( ~ s__crosses(X0,sK358)
| s__crosses(X0,sK359)
| ~ s__instance(X0,s__Object) )
| ~ spl3218_579
| ~ spl3218_588
| ~ spl3218_589 ),
inference(forward_subsumption_resolution,[],[f322613,f321792]) ).
fof(f322615,plain,
( s__crosses(sK357,sK359)
| ~ s__instance(sK357,s__Object)
| ~ spl3218_579
| ~ spl3218_580
| ~ spl3218_588
| ~ spl3218_589 ),
inference(resolution,[],[f321752,f322614]) ).
fof(f322618,plain,
( ~ s__instance(sK357,s__Object)
| spl3218_578
| ~ spl3218_579
| ~ spl3218_580
| ~ spl3218_588
| ~ spl3218_589 ),
inference(forward_subsumption_resolution,[],[f322615,f321742]) ).
fof(f322620,plain,
( $false
| spl3218_578
| ~ spl3218_579
| ~ spl3218_580
| ~ spl3218_587
| ~ spl3218_588
| ~ spl3218_589 ),
inference(forward_subsumption_resolution,[],[f322618,f321787]) ).
fof(f322621,plain,
( spl3218_578
| ~ spl3218_579
| ~ spl3218_580
| ~ spl3218_587
| ~ spl3218_588
| ~ spl3218_589 ),
inference(avatar_contradiction_clause,[],[f322620]) ).
cnf(s435,plain,
( spl3218_576
| spl3218_577 ),
inference(sat_conversion,[],[f321738]) ).
cnf(s436,plain,
( ~ spl3218_577
| ~ spl3218_578 ),
inference(sat_conversion,[],[f321743]) ).
cnf(s437,plain,
( ~ spl3218_577
| spl3218_579 ),
inference(sat_conversion,[],[f321748]) ).
cnf(s438,plain,
( ~ spl3218_577
| spl3218_580 ),
inference(sat_conversion,[],[f321753]) ).
cnf(s445,plain,
( ~ spl3218_577
| spl3218_587 ),
inference(sat_conversion,[],[f321788]) ).
cnf(s446,plain,
( ~ spl3218_577
| spl3218_588 ),
inference(sat_conversion,[],[f321793]) ).
cnf(s447,plain,
( ~ spl3218_577
| spl3218_589 ),
inference(sat_conversion,[],[f321798]) ).
cnf(s553,plain,
~ spl3218_576,
inference(sat_conversion,[],[f322611]) ).
cnf(s554,plain,
( spl3218_578
| ~ spl3218_579
| ~ spl3218_580
| ~ spl3218_587
| ~ spl3218_588
| ~ spl3218_589 ),
inference(sat_conversion,[],[f322621]) ).
cnf(s555,plain,
spl3218_577,
inference(rat,[],[s435,s553]) ).
cnf(s556,plain,
spl3218_589,
inference(rat,[],[s447,s555]) ).
cnf(s557,plain,
spl3218_588,
inference(rat,[],[s446,s555]) ).
cnf(s558,plain,
spl3218_587,
inference(rat,[],[s445,s555]) ).
cnf(s565,plain,
spl3218_580,
inference(rat,[],[s438,s555]) ).
cnf(s566,plain,
spl3218_579,
inference(rat,[],[s437,s555]) ).
cnf(s567,plain,
~ spl3218_578,
inference(rat,[],[s436,s555]) ).
cnf(s568,plain,
$false,
inference(rat,[],[s554,s556,s557,s558,s565,s566,s567]) ).
fof(f322622,plain,
$false,
inference(avatar_sat_refutation,[],[s568]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR097+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 % Computer : n026.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 22:49:58 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.26 Running first-order theorem proving
% 0.20/0.26 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
% 15.89/5.42 % (172475)Detected formulas, will run a generic FOF schedule.
% 15.89/5.42 % (172480)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=2914186704:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 15.89/5.42 % (172481)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=1085183618:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 15.89/5.42 % (172482)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=4244177212:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 15.89/5.42 % (172485)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2815738490:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 15.89/5.42 % (172484)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2438562270:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 15.89/5.42 % (172483)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=828510619:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 15.89/5.42 % (172486)dis-21_1_sil=8000:lcm=predicate:random_seed=4091357579:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 15.89/5.42 % (172483)Instruction limit reached!
% 15.89/5.42 % (172483)------------------------------
% 15.89/5.42 % (172483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.89/5.42 % (172483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.89/5.42 % (172483)CaDiCaL version: 2.1.3
% 15.89/5.42 % (172483)Termination reason: Instruction limit
% 15.89/5.42 % (172483)Termination phase: SInE selection
% 15.89/5.42 % (172483)Time elapsed: 0.064 s
% 15.89/5.42 % (172483)Peak memory usage: 165 MB
% 15.89/5.42 % (172483)Instructions burned: 111 (million)
% 15.89/5.42 % (172484)Instruction limit reached!
% 15.89/5.42 % (172484)------------------------------
% 15.89/5.42 % (172484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.89/5.42 % (172484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.89/5.42 % (172484)CaDiCaL version: 2.1.3
% 15.89/5.42 % (172484)Termination reason: Instruction limit
% 15.89/5.42 % (172484)Termination phase: SInE selection
% 15.89/5.42 % (172484)Time elapsed: 0.069 s
% 15.89/5.42 % (172484)Peak memory usage: 164 MB
% 15.89/5.42 % (172484)Instructions burned: 121 (million)
% 15.89/5.42 % (172485)Instruction limit reached!
% 15.89/5.42 % (172485)------------------------------
% 15.89/5.42 % (172485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.89/5.42 % (172485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.89/5.42 % (172485)CaDiCaL version: 2.1.3
% 15.89/5.42 % (172485)Termination reason: Instruction limit
% 15.89/5.42 % (172485)Termination phase: Property scanning
% 15.89/5.42 % (172485)Time elapsed: 0.075 s
% 15.89/5.42 % (172485)Peak memory usage: 165 MB
% 15.89/5.42 % (172485)Instructions burned: 140 (million)
% 15.89/5.42 % (172486)Instruction limit reached!
% 15.89/5.42 % (172486)------------------------------
% 15.89/5.42 % (172486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.89/5.42 % (172486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.89/5.42 % (172486)CaDiCaL version: 2.1.3
% 15.89/5.42 % (172486)Termination reason: Instruction limit
% 15.89/5.42 % (172486)Termination phase: SInE selection
% 15.89/5.42 % (172486)Time elapsed: 0.075 s
% 15.89/5.42 % (172486)Peak memory usage: 165 MB
% 15.89/5.42 % (172486)Instructions burned: 130 (million)
% 15.89/5.42 % (172494)lrs+10_1_sil=8000:sp=occurrence:random_seed=923292611:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 15.89/5.42 % (172496)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2109141819:i=325:sd=1:ss=axioms:sgt=32_2969 on theBenchmark for (2969ds/325Mi)
% 15.89/5.42 % (172495)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1821518302:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/157Mi)
% 15.89/5.42 % (172497)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=2929860696:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 15.89/5.42 % (172495)Instruction limit reached!
% 15.89/5.42 % (172495)------------------------------
% 20.84/6.08 % (172495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172495)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172495)Termination reason: Instruction limit
% 20.84/6.08 % (172495)Termination phase: Property scanning
% 20.84/6.08 % (172495)Time elapsed: 0.085 s
% 20.84/6.08 % (172495)Peak memory usage: 165 MB
% 20.84/6.08 % (172495)Instructions burned: 159 (million)
% 20.84/6.08 % (172494)Instruction limit reached!
% 20.84/6.08 % (172494)------------------------------
% 20.84/6.08 % (172494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172494)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172494)Termination reason: Instruction limit
% 20.84/6.08 % (172494)Termination phase: SInE selection
% 20.84/6.08 % (172494)Time elapsed: 0.157 s
% 20.84/6.08 % (172494)Peak memory usage: 165 MB
% 20.84/6.08 % (172494)Instructions burned: 286 (million)
% 20.84/6.08 % (172497)Instruction limit reached!
% 20.84/6.08 % (172497)------------------------------
% 20.84/6.08 % (172497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172497)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172497)Termination reason: Instruction limit
% 20.84/6.08 % (172497)Termination phase: Property scanning
% 20.84/6.08 % (172497)Time elapsed: 0.119 s
% 20.84/6.08 % (172497)Peak memory usage: 165 MB
% 20.84/6.08 % (172497)Instructions burned: 249 (million)
% 20.84/6.08 % (172496)Instruction limit reached!
% 20.84/6.08 % (172496)------------------------------
% 20.84/6.08 % (172496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172496)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172496)Termination reason: Instruction limit
% 20.84/6.08 % (172496)Termination phase: SInE selection
% 20.84/6.08 % (172496)Time elapsed: 0.179 s
% 20.84/6.08 % (172496)Peak memory usage: 165 MB
% 20.84/6.08 % (172496)Instructions burned: 327 (million)
% 20.84/6.08 % (172502)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3839721896:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2966 on theBenchmark for (2966ds/294Mi)
% 20.84/6.08 % (172503)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=742546940:i=2350_2966 on theBenchmark for (2966ds/2350Mi)
% 20.84/6.08 % (172504)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=859950895:cts=off:i=113:fsr=off:ss=included:sgt=4_2966 on theBenchmark for (2966ds/113Mi)
% 20.84/6.08 % (172505)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=301090108:i=127:av=off:fsr=off:sup=off_2966 on theBenchmark for (2966ds/127Mi)
% 20.84/6.08 % (172504)Instruction limit reached!
% 20.84/6.08 % (172504)------------------------------
% 20.84/6.08 % (172504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172504)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172504)Termination reason: Instruction limit
% 20.84/6.08 % (172504)Termination phase: SInE selection
% 20.84/6.08 % (172504)Time elapsed: 0.068 s
% 20.84/6.08 % (172504)Peak memory usage: 165 MB
% 20.84/6.08 % (172504)Instructions burned: 115 (million)
% 20.84/6.08 % (172502)Instruction limit reached!
% 20.84/6.08 % (172502)------------------------------
% 20.84/6.08 % (172502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172502)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172502)Termination reason: Instruction limit
% 20.84/6.08 % (172502)Termination phase: SInE selection
% 20.84/6.08 % (172502)Time elapsed: 0.156 s
% 20.84/6.08 % (172502)Peak memory usage: 165 MB
% 20.84/6.08 % (172502)Instructions burned: 294 (million)
% 20.84/6.08 % (172505)Instruction limit reached!
% 20.84/6.08 % (172505)------------------------------
% 20.84/6.08 % (172505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.84/6.08 % (172505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.84/6.08 % (172505)CaDiCaL version: 2.1.3
% 20.84/6.08 % (172505)Termination reason: Instruction limit
% 20.84/6.08 % (172505)Termination phase: Preprocessing 1
% 20.84/6.08 % (172505)Time elapsed: 0.086 s
% 55.39/10.96 % (172505)Peak memory usage: 165 MB
% 55.39/10.96 % (172505)Instructions burned: 128 (million)
% 55.39/10.96 % (172510)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2331854993:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2964 on theBenchmark for (2964ds/114Mi)
% 55.39/10.96 % (172511)lrs+10_1_sil=8000:sp=occurrence:random_seed=1906264356:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 55.39/10.96 % (172512)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=251573061:i=437:sd=1:aac=none:ss=included_2963 on theBenchmark for (2963ds/437Mi)
% 55.39/10.96 % (172510)Instruction limit reached!
% 55.39/10.96 % (172510)------------------------------
% 55.39/10.96 % (172510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.39/10.96 % (172510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.39/10.96 % (172510)CaDiCaL version: 2.1.3
% 55.39/10.96 % (172510)Termination reason: Instruction limit
% 55.39/10.96 % (172510)Termination phase: Property scanning
% 55.39/10.96 % (172510)Time elapsed: 0.066 s
% 55.39/10.96 % (172510)Peak memory usage: 165 MB
% 55.39/10.96 % (172510)Instructions burned: 115 (million)
% 55.39/10.96 % (172516)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=134616356:i=5202:ss=axioms:sgt=16_2962 on theBenchmark for (2962ds/5202Mi)
% 55.39/10.96 % (172512)Refutation not found, incomplete strategy
% 55.39/10.96 % (172512)------------------------------
% 55.39/10.96 % (172512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.39/10.96 % (172512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.39/10.96 % (172512)CaDiCaL version: 2.1.3
% 55.39/10.96 % (172512)Termination reason: Refutation not found, incomplete strategy
% 55.39/10.96 % (172512)Time elapsed: 0.250 s
% 55.39/10.96 % (172512)Peak memory usage: 169 MB
% 55.39/10.96 % (172512)Instructions burned: 397 (million)
% 55.39/10.96 % (172511)Instruction limit reached!
% 55.39/10.96 % (172511)------------------------------
% 55.39/10.96 % (172511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.39/10.96 % (172511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.39/10.96 % (172511)CaDiCaL version: 2.1.3
% 55.39/10.96 % (172511)Termination reason: Instruction limit
% 55.39/10.96 % (172511)Termination phase: Saturation
% 55.39/10.96 % (172511)Time elapsed: 0.544 s
% 55.39/10.96 % (172511)Peak memory usage: 174 MB
% 55.39/10.96 % (172511)Instructions burned: 908 (million)
% 55.39/10.96 % (172512)------------------------------
% 55.39/10.96 % (172512)------------------------------
% 55.39/10.96 % (172518)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2587760735:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2957 on theBenchmark for (2957ds/134Mi)
% 55.39/10.96 % (172519)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1006744169:st=8:i=592:sd=3:ep=RST:ss=axioms_2956 on theBenchmark for (2956ds/592Mi)
% 55.39/10.96 % (172518)Instruction limit reached!
% 55.39/10.96 % (172518)------------------------------
% 55.39/10.96 % (172518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.39/10.96 % (172518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.39/10.96 % (172518)CaDiCaL version: 2.1.3
% 55.39/10.96 % (172518)Termination reason: Instruction limit
% 55.39/10.96 % (172518)Termination phase: SInE selection
% 55.39/10.96 % (172518)Time elapsed: 0.083 s
% 55.39/10.96 % (172518)Peak memory usage: 165 MB
% 55.39/10.96 % (172518)Instructions burned: 135 (million)
% 55.39/10.96 % (172503)Instruction limit reached!
% 55.39/10.96 % (172503)------------------------------
% 55.39/10.96 % (172503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.39/10.96 % (172503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.39/10.96 % (172503)CaDiCaL version: 2.1.3
% 55.39/10.96 % (172503)Termination reason: Instruction limit
% 55.39/10.96 % (172503)Termination phase: Property scanning
% 55.39/10.96 % (172503)Time elapsed: 1.189 s
% 55.39/10.96 % (172503)Peak memory usage: 194 MB
% 55.39/10.96 % (172503)Instructions burned: 2352 (million)
% 55.39/10.96 % (172522)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3772968207:st=3:i=13193:sd=3:ss=axioms_2954 on theBenchmark for (2954ds/13193Mi)
% 55.39/10.96 % (172482)Refutation not found, incomplete strategy
% 55.39/10.96 % (172482)------------------------------
% 55.39/10.96 % (172482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.39/10.96 % (172482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.33/13.37 % (172482)CaDiCaL version: 2.1.3
% 72.33/13.37 % (172482)Termination reason: Refutation not found, incomplete strategy
% 72.33/13.37 % (172482)Time elapsed: 1.726 s
% 72.33/13.37 % (172482)Peak memory usage: 298 MB
% 72.33/13.37 % (172482)Instructions burned: 2527 (million)
% 72.33/13.37 % (172519)Instruction limit reached!
% 72.33/13.37 % (172519)------------------------------
% 72.33/13.37 % (172519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.33/13.37 % (172519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.33/13.37 % (172519)CaDiCaL version: 2.1.3
% 72.33/13.37 % (172519)Termination reason: Instruction limit
% 72.33/13.37 % (172519)Termination phase: Preprocessing 1
% 72.33/13.37 % (172519)Time elapsed: 0.331 s
% 72.33/13.37 % (172519)Peak memory usage: 166 MB
% 72.33/13.37 % (172519)Instructions burned: 592 (million)
% 72.33/13.37 % (172524)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=2732392753:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/125Mi)
% 72.33/13.37 % (172524)Instruction limit reached!
% 72.33/13.37 % (172524)------------------------------
% 72.33/13.37 % (172524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.33/13.37 % (172524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.33/13.37 % (172524)CaDiCaL version: 2.1.3
% 72.33/13.37 % (172524)Termination reason: Instruction limit
% 72.33/13.37 % (172524)Termination phase: Property scanning
% 72.33/13.37 % (172524)Time elapsed: 0.070 s
% 72.33/13.37 % (172524)Peak memory usage: 165 MB
% 72.33/13.37 % (172524)Instructions burned: 125 (million)
% 72.33/13.37 % (172525)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=238278135:i=134:gtgl=5:slsql=off:gtg=exists_sym_2951 on theBenchmark for (2951ds/134Mi)
% 72.33/13.37 % (172525)Instruction limit reached!
% 72.33/13.37 % (172525)------------------------------
% 72.33/13.37 % (172525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.33/13.37 % (172525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.33/13.37 % (172525)CaDiCaL version: 2.1.3
% 72.33/13.37 % (172525)Termination reason: Instruction limit
% 72.33/13.37 % (172525)Termination phase: Property scanning
% 72.33/13.37 % (172525)Time elapsed: 0.073 s
% 72.33/13.37 % (172525)Peak memory usage: 165 MB
% 72.33/13.37 % (172525)Instructions burned: 134 (million)
% 72.33/13.37 % (172482)------------------------------
% 72.33/13.37 % (172482)------------------------------
% 72.33/13.37 % (172527)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=348385636:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2950 on theBenchmark for (2950ds/141Mi)
% 72.33/13.37 % (172527)Instruction limit reached!
% 72.33/13.37 % (172527)------------------------------
% 72.33/13.37 % (172527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.33/13.37 % (172527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.33/13.37 % (172527)CaDiCaL version: 2.1.3
% 72.33/13.37 % (172527)Termination reason: Instruction limit
% 72.33/13.37 % (172527)Termination phase: SInE selection
% 72.33/13.37 % (172527)Time elapsed: 0.085 s
% 72.33/13.37 % (172527)Peak memory usage: 165 MB
% 72.33/13.37 % (172527)Instructions burned: 142 (million)
% 72.33/13.37 % (172529)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1211599187:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2949 on theBenchmark for (2949ds/431Mi)
% 72.33/13.37 % (172530)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=3898636830:i=6060:aac=none:ins=25_2949 on theBenchmark for (2949ds/6060Mi)
% 72.33/13.37 % (172532)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=1091003799:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2948 on theBenchmark for (2948ds/150Mi)
% 72.33/13.37 % (172532)Instruction limit reached!
% 72.33/13.37 % (172532)------------------------------
% 72.33/13.37 % (172532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.33/13.37 % (172532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.33/13.37 % (172532)CaDiCaL version: 2.1.3
% 72.33/13.37 % (172532)Termination reason: Instruction limit
% 72.33/13.37 % (172532)Termination phase: SInE selection
% 72.33/13.37 % (172532)Time elapsed: 0.088 s
% 94.77/16.60 % (172532)Peak memory usage: 165 MB
% 94.77/16.60 % (172532)Instructions burned: 151 (million)
% 94.77/16.60 % (172529)Refutation not found, incomplete strategy
% 94.77/16.60 % (172529)------------------------------
% 94.77/16.60 % (172529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.77/16.60 % (172529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.77/16.60 % (172529)CaDiCaL version: 2.1.3
% 94.77/16.60 % (172529)Termination reason: Refutation not found, incomplete strategy
% 94.77/16.60 % (172529)Time elapsed: 0.261 s
% 94.77/16.60 % (172529)Peak memory usage: 170 MB
% 94.77/16.60 % (172529)Instructions burned: 396 (million)
% 94.77/16.60 % (172536)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1013413331:i=14155:bd=all_2946 on theBenchmark for (2946ds/14155Mi)
% 94.77/16.60 % (172529)------------------------------
% 94.77/16.60 % (172529)------------------------------
% 94.77/16.60 % (172538)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2746084472:i=667:av=off:fsr=off_2942 on theBenchmark for (2942ds/667Mi)
% 94.77/16.60 % (172538)Instruction limit reached!
% 94.77/16.60 % (172538)------------------------------
% 94.77/16.60 % (172538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.77/16.60 % (172538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.77/16.60 % (172538)CaDiCaL version: 2.1.3
% 94.77/16.60 % (172538)Termination reason: Instruction limit
% 94.77/16.60 % (172538)Termination phase: NewCNF
% 94.77/16.60 % (172538)Time elapsed: 0.536 s
% 94.77/16.60 % (172538)Peak memory usage: 184 MB
% 94.77/16.60 % (172538)Instructions burned: 668 (million)
% 94.77/16.60 % (172540)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=291845709:s2a=on:i=185:s2at=1.8:fdi=4_2935 on theBenchmark for (2935ds/185Mi)
% 94.77/16.60 % (172540)Instruction limit reached!
% 94.77/16.60 % (172540)------------------------------
% 94.77/16.60 % (172540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.77/16.60 % (172540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.77/16.60 % (172540)CaDiCaL version: 2.1.3
% 94.77/16.60 % (172540)Termination reason: Instruction limit
% 94.77/16.60 % (172540)Termination phase: SInE selection
% 94.77/16.60 % (172540)Time elapsed: 0.108 s
% 94.77/16.60 % (172540)Peak memory usage: 165 MB
% 94.77/16.60 % (172540)Instructions burned: 186 (million)
% 94.77/16.60 % (172542)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2248730430:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2933 on theBenchmark for (2933ds/193Mi)
% 94.77/16.60 % (172542)Instruction limit reached!
% 94.77/16.60 % (172542)------------------------------
% 94.77/16.60 % (172542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.77/16.60 % (172542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.77/16.60 % (172542)CaDiCaL version: 2.1.3
% 94.77/16.60 % (172542)Termination reason: Instruction limit
% 94.77/16.60 % (172542)Termination phase: SInE selection
% 94.77/16.60 % (172542)Time elapsed: 0.112 s
% 94.77/16.60 % (172542)Peak memory usage: 165 MB
% 94.77/16.60 % (172542)Instructions burned: 194 (million)
% 94.77/16.60 % (172516)Instruction limit reached!
% 94.77/16.60 % (172516)------------------------------
% 94.77/16.60 % (172516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.77/16.60 % (172516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.77/16.60 % (172516)CaDiCaL version: 2.1.3
% 94.77/16.60 % (172516)Termination reason: Instruction limit
% 94.77/16.60 % (172516)Termination phase: Saturation
% 94.77/16.60 % (172516)Time elapsed: 3.080 s
% 94.77/16.60 % (172516)Peak memory usage: 303 MB
% 94.77/16.60 % (172516)Instructions burned: 5203 (million)
% 94.77/16.60 % (172544)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3865263313:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2930 on theBenchmark for (2930ds/4850Mi)
% 94.77/16.60 % (172545)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3332017712:i=12111:sd=1:ss=included_2929 on theBenchmark for (2929ds/12111Mi)
% 94.77/16.60 % (172544)Instruction limit reached!
% 94.77/16.60 % (172544)------------------------------
% 94.77/16.60 % (172544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.77/16.60 % (172544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.27/21.81 % (172544)CaDiCaL version: 2.1.3
% 132.27/21.81 % (172544)Termination reason: Instruction limit
% 132.27/21.81 % (172544)Termination phase: Saturation
% 132.27/21.81 % (172544)Time elapsed: 3.186 s
% 132.27/21.81 % (172544)Peak memory usage: 198 MB
% 132.27/21.81 % (172544)Instructions burned: 4851 (million)
% 132.27/21.81 % (172530)Instruction limit reached!
% 132.27/21.81 % (172530)------------------------------
% 132.27/21.81 % (172530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.27/21.81 % (172530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.27/21.81 % (172530)CaDiCaL version: 2.1.3
% 132.27/21.81 % (172530)Termination reason: Instruction limit
% 132.27/21.81 % (172530)Termination phase: Saturation
% 132.27/21.81 % (172530)Time elapsed: 5.118 s
% 132.27/21.81 % (172530)Peak memory usage: 582 MB
% 132.27/21.81 % (172530)Instructions burned: 6061 (million)
% 132.27/21.81 % (172548)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=393089691:i=319:kws=precedence:fsr=off_2897 on theBenchmark for (2897ds/319Mi)
% 132.27/21.81 % (172549)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=504846165:i=2064:ep=RST_2896 on theBenchmark for (2896ds/2064Mi)
% 132.27/21.81 % (172548)Instruction limit reached!
% 132.27/21.81 % (172548)------------------------------
% 132.27/21.81 % (172548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.27/21.81 % (172548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.27/21.81 % (172548)CaDiCaL version: 2.1.3
% 132.27/21.81 % (172548)Termination reason: Instruction limit
% 132.27/21.81 % (172548)Termination phase: Preprocessing 2
% 132.27/21.81 % (172548)Time elapsed: 0.273 s
% 132.27/21.81 % (172548)Peak memory usage: 170 MB
% 132.27/21.81 % (172548)Instructions burned: 319 (million)
% 132.27/21.81 % (172552)dis-1011_128_sil=32000:random_seed=201331241:i=3706:ep=RST:av=off_2893 on theBenchmark for (2893ds/3706Mi)
% 132.27/21.81 % (172549)Instruction limit reached!
% 132.27/21.81 % (172549)------------------------------
% 132.27/21.81 % (172549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.27/21.81 % (172549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.27/21.81 % (172549)CaDiCaL version: 2.1.3
% 132.27/21.81 % (172549)Termination reason: Instruction limit
% 132.27/21.81 % (172549)Termination phase: Property scanning
% 132.27/21.81 % (172549)Time elapsed: 1.009 s
% 132.27/21.81 % (172549)Peak memory usage: 194 MB
% 132.27/21.81 % (172549)Instructions burned: 2065 (million)
% 132.27/21.81 % (172554)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3912050232:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2884 on theBenchmark for (2884ds/757Mi)
% 132.27/21.81 % (172554)Refutation not found, incomplete strategy
% 132.27/21.81 % (172554)------------------------------
% 132.27/21.81 % (172554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.27/21.81 % (172554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.27/21.81 % (172554)CaDiCaL version: 2.1.3
% 132.27/21.81 % (172554)Termination reason: Refutation not found, incomplete strategy
% 132.27/21.81 % (172554)Time elapsed: 0.244 s
% 132.27/21.81 % (172554)Peak memory usage: 170 MB
% 132.27/21.81 % (172554)Instructions burned: 398 (million)
% 132.27/21.81 % (172554)------------------------------
% 132.27/21.81 % (172554)------------------------------
% 132.27/21.81 % (172556)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1452416378:i=13913:ss=axioms:sgt=8_2878 on theBenchmark for (2878ds/13913Mi)
% 132.27/21.81 % (172545)Instruction limit reached!
% 132.27/21.81 % (172545)------------------------------
% 132.27/21.81 % (172545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.27/21.81 % (172545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.27/21.81 % (172545)CaDiCaL version: 2.1.3
% 132.27/21.81 % (172545)Termination reason: Instruction limit
% 132.27/21.81 % (172545)Termination phase: Saturation
% 132.27/21.81 % (172545)Time elapsed: 5.316 s
% 132.27/21.81 % (172545)Peak memory usage: 240 MB
% 132.27/21.81 % (172545)Instructions burned: 12112 (million)
% 132.27/21.81 % (172558)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1118781336:i=9925:aac=none_2875 on theBenchmark for (2875ds/9925Mi)
% 132.27/21.81 % (172552)Instruction limit reached!
% 132.27/21.81 % (172552)------------------------------
% 132.27/21.81 % (172552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.27/21.81 % (172552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.47/23.91 % (172552)CaDiCaL version: 2.1.3
% 146.47/23.91 % (172552)Termination reason: Instruction limit
% 146.47/23.91 % (172552)Termination phase: Saturation
% 146.47/23.91 % (172552)Time elapsed: 1.822 s
% 146.47/23.91 % (172552)Peak memory usage: 227 MB
% 146.47/23.91 % (172552)Instructions burned: 3707 (million)
% 146.47/23.91 % (172522)Instruction limit reached!
% 146.47/23.91 % (172522)------------------------------
% 146.47/23.91 % (172522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.47/23.91 % (172522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.47/23.91 % (172522)CaDiCaL version: 2.1.3
% 146.47/23.91 % (172522)Termination reason: Instruction limit
% 146.47/23.91 % (172522)Termination phase: Saturation
% 146.47/23.91 % (172522)Time elapsed: 8.108 s
% 146.47/23.91 % (172522)Peak memory usage: 314 MB
% 146.47/23.91 % (172522)Instructions burned: 13195 (million)
% 146.47/23.91 % (172560)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4028870721:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2873 on theBenchmark for (2873ds/2479Mi)
% 146.47/23.91 % (172561)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=839670776:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2871 on theBenchmark for (2871ds/440Mi)
% 146.47/23.91 % (172561)Instruction limit reached!
% 146.47/23.91 % (172561)------------------------------
% 146.47/23.91 % (172561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.47/23.91 % (172561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.47/23.91 % (172561)CaDiCaL version: 2.1.3
% 146.47/23.91 % (172561)Termination reason: Instruction limit
% 146.47/23.91 % (172561)Termination phase: Property scanning
% 146.47/23.91 % (172561)Time elapsed: 0.207 s
% 146.47/23.91 % (172561)Peak memory usage: 165 MB
% 146.47/23.91 % (172561)Instructions burned: 440 (million)
% 146.47/23.91 % (172560)Refutation not found, incomplete strategy
% 146.47/23.91 % (172560)------------------------------
% 146.47/23.91 % (172560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.47/23.91 % (172560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.47/23.91 % (172560)CaDiCaL version: 2.1.3
% 146.47/23.91 % (172560)Termination reason: Refutation not found, incomplete strategy
% 146.47/23.91 % (172560)Time elapsed: 0.489 s
% 146.47/23.91 % (172560)Peak memory usage: 170 MB
% 146.47/23.91 % (172560)Instructions burned: 835 (million)
% 146.47/23.91 % (172564)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2207977559:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2868 on theBenchmark for (2868ds/11145Mi)
% 146.47/23.91 % (172560)------------------------------
% 146.47/23.91 % (172560)------------------------------
% 146.47/23.91 % (172566)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=4013168901:cts=off:i=3034:av=off:er=known:fsd=on_2863 on theBenchmark for (2863ds/3034Mi)
% 146.47/23.91 % (172566)Instruction limit reached!
% 146.47/23.91 % (172566)------------------------------
% 146.47/23.91 % (172566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.47/23.91 % (172566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.47/23.91 % (172566)CaDiCaL version: 2.1.3
% 146.47/23.91 % (172566)Termination reason: Instruction limit
% 146.47/23.91 % (172566)Termination phase: Saturation
% 146.47/23.91 % (172566)Time elapsed: 1.701 s
% 146.47/23.91 % (172566)Peak memory usage: 224 MB
% 146.47/23.91 % (172566)Instructions burned: 3036 (million)
% 146.47/23.91 % (172569)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=759984995:st=2:s2a=on:i=524:s2at=2:ss=axioms_2845 on theBenchmark for (2845ds/524Mi)
% 146.47/23.91 % (172536)Instruction limit reached!
% 146.47/23.91 % (172536)------------------------------
% 146.47/23.91 % (172536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.47/23.91 % (172536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.47/23.91 % (172536)CaDiCaL version: 2.1.3
% 146.47/23.91 % (172536)Termination reason: Instruction limit
% 146.47/23.91 % (172536)Termination phase: Saturation
% 146.47/23.91 % (172536)Time elapsed: 10.096 s
% 146.47/23.91 % (172536)Peak memory usage: 917 MB
% 146.47/23.91 % (172536)Instructions burned: 14155 (million)
% 146.47/23.91 % (172571)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1676927165:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2842 on theBenchmark for (2842ds/1016Mi)
% 146.47/23.91 % (172569)Instruction limit reached!
% 115.36/24.27 % (172569)------------------------------
% 115.36/24.27 % (172569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172569)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172569)Termination reason: Instruction limit
% 115.36/24.27 % (172569)Termination phase: SInE selection
% 115.36/24.27 % (172569)Time elapsed: 0.269 s
% 115.36/24.27 % (172569)Peak memory usage: 165 MB
% 115.36/24.27 % (172569)Instructions burned: 524 (million)
% 115.36/24.27 % (172573)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1565445473:i=14123:bd=preordered:ins=4_2841 on theBenchmark for (2841ds/14123Mi)
% 115.36/24.27 % (172571)Refutation not found, incomplete strategy
% 115.36/24.27 % (172571)------------------------------
% 115.36/24.27 % (172571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172571)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172571)Termination reason: Refutation not found, incomplete strategy
% 115.36/24.27 % (172571)Time elapsed: 0.270 s
% 115.36/24.27 % (172571)Peak memory usage: 170 MB
% 115.36/24.27 % (172571)Instructions burned: 443 (million)
% 115.36/24.27 % (172571)------------------------------
% 115.36/24.27 % (172571)------------------------------
% 115.36/24.27 % (172575)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2910165238:i=5781:kws=precedence:bd=all:rawr=on_2835 on theBenchmark for (2835ds/5781Mi)
% 115.36/24.27 % (172575)Instruction limit reached!
% 115.36/24.27 % (172575)------------------------------
% 115.36/24.27 % (172575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172575)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172575)Termination reason: Instruction limit
% 115.36/24.27 % (172575)Termination phase: Saturation
% 115.36/24.27 % (172575)Time elapsed: 3.044 s
% 115.36/24.27 % (172575)Peak memory usage: 239 MB
% 115.36/24.27 % (172575)Instructions burned: 5783 (million)
% 115.36/24.27 % (172558)Instruction limit reached!
% 115.36/24.27 % (172558)------------------------------
% 115.36/24.27 % (172558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172558)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172558)Termination reason: Instruction limit
% 115.36/24.27 % (172558)Termination phase: Saturation
% 115.36/24.27 % (172558)Time elapsed: 7.005 s
% 115.36/24.27 % (172558)Peak memory usage: 837 MB
% 115.36/24.27 % (172558)Instructions burned: 9926 (million)
% 115.36/24.27 % (172577)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=1791852195:i=2448:gtgl=5:bd=preordered:gtg=all_2803 on theBenchmark for (2803ds/2448Mi)
% 115.36/24.27 % (172578)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1972770828:i=3223:kws=precedence:fgj=on:av=off_2802 on theBenchmark for (2802ds/3223Mi)
% 115.36/24.27 % (172556)Instruction limit reached!
% 115.36/24.27 % (172556)------------------------------
% 115.36/24.27 % (172556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172556)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172556)Termination reason: Instruction limit
% 115.36/24.27 % (172556)Termination phase: Saturation
% 115.36/24.27 % (172556)Time elapsed: 8.208 s
% 115.36/24.27 % (172556)Peak memory usage: 311 MB
% 115.36/24.27 % (172556)Instructions burned: 13913 (million)
% 115.36/24.27 % (172581)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2502512237:st=5.6:i=2033:sd=3:ss=axioms_2794 on theBenchmark for (2794ds/2033Mi)
% 115.36/24.27 % (172564)Instruction limit reached!
% 115.36/24.27 % (172564)------------------------------
% 115.36/24.27 % (172564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172564)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172564)Termination reason: Instruction limit
% 115.36/24.27 % (172564)Termination phase: Saturation
% 115.36/24.27 % (172564)Time elapsed: 7.780 s
% 115.36/24.27 % (172564)Peak memory usage: 303 MB
% 115.36/24.27 % (172564)Instructions burned: 11145 (million)
% 115.36/24.27 % (172577)Instruction limit reached!
% 115.36/24.27 % (172577)------------------------------
% 115.36/24.27 % (172577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172577)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172577)Termination reason: Instruction limit
% 115.36/24.27 % (172577)Termination phase: Naming
% 115.36/24.27 % (172577)Time elapsed: 1.359 s
% 115.36/24.27 % (172577)Peak memory usage: 174 MB
% 115.36/24.27 % (172577)Instructions burned: 2449 (million)
% 115.36/24.27 % (172583)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=382700246:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2788 on theBenchmark for (2788ds/2055Mi)
% 115.36/24.27 % (172584)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=3514586059:i=21611:sd=3:ss=axioms_2788 on theBenchmark for (2788ds/21611Mi)
% 115.36/24.27 % (172578)Instruction limit reached!
% 115.36/24.27 % (172578)------------------------------
% 115.36/24.27 % (172578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172578)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172578)Termination reason: Instruction limit
% 115.36/24.27 % (172578)Termination phase: Saturation
% 115.36/24.27 % (172578)Time elapsed: 1.852 s
% 115.36/24.27 % (172578)Peak memory usage: 255 MB
% 115.36/24.27 % (172578)Instructions burned: 3223 (million)
% 115.36/24.27 % (172587)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1105648592:i=4835:sd=13:ss=axioms:sgt=23_2782 on theBenchmark for (2782ds/4835Mi)
% 115.36/24.27 % (172581)Instruction limit reached!
% 115.36/24.27 % (172581)------------------------------
% 115.36/24.27 % (172581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172581)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172581)Termination reason: Instruction limit
% 115.36/24.27 % (172581)Termination phase: Saturation
% 115.36/24.27 % (172581)Time elapsed: 1.317 s
% 115.36/24.27 % (172581)Peak memory usage: 277 MB
% 115.36/24.27 % (172581)Instructions burned: 2035 (million)
% 115.36/24.27 % (172589)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=3632878584:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2779 on theBenchmark for (2779ds/797Mi)
% 115.36/24.27 % (172583)Instruction limit reached!
% 115.36/24.27 % (172583)------------------------------
% 115.36/24.27 % (172583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172583)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172583)Termination reason: Instruction limit
% 115.36/24.27 % (172583)Termination phase: Saturation
% 115.36/24.27 % (172583)Time elapsed: 1.151 s
% 115.36/24.27 % (172583)Peak memory usage: 197 MB
% 115.36/24.27 % (172583)Instructions burned: 2057 (million)
% 115.36/24.27 % (172591)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=737900595:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2775 on theBenchmark for (2775ds/2326Mi)
% 115.36/24.27 % (172589)Instruction limit reached!
% 115.36/24.27 % (172589)------------------------------
% 115.36/24.27 % (172589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172589)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172589)Termination reason: Instruction limit
% 115.36/24.27 % (172589)Termination phase: SInE selection
% 115.36/24.27 % (172589)Time elapsed: 0.515 s
% 115.36/24.27 % (172589)Peak memory usage: 168 MB
% 115.36/24.27 % (172589)Instructions burned: 798 (million)
% 115.36/24.27 % (172593)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=984356723:i=6038:nm=6_2772 on theBenchmark for (2772ds/6038Mi)
% 115.36/24.27 % (172480)First to succeed.
% 115.36/24.27 % (172480)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-172475"
% 115.36/24.27 % (172584)Refutation not found, incomplete strategy
% 115.36/24.27 % (172584)------------------------------
% 115.36/24.27 % (172584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.36/24.27 % (172584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.36/24.27 % (172584)CaDiCaL version: 2.1.3
% 115.36/24.27 % (172584)Termination reason: Refutation not found, incomplete strategy
% 115.36/24.27 % (172584)Time elapsed: 1.874 s
% 115.36/24.27 % (172584)Peak memory usage: 332 MB
% 115.36/24.27 % (172584)Instructions burned: 2677 (million)
% 115.36/24.27 % (172480)Refutation found. Thanks to Tanya!
% 115.36/24.27 % SZS status ContradictoryAxioms for theBenchmark
% 115.36/24.27 % SZS output start Proof for theBenchmark
% See solution above
% 150.09/24.53 % (172480)------------------------------
% 150.09/24.53 % (172480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.09/24.53 % (172480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.09/24.53 % (172480)CaDiCaL version: 2.1.3
% 150.09/24.53 % (172480)Termination reason: Refutation
% 150.09/24.53 % (172480)Time elapsed: 20.119 s
% 150.09/24.53 % (172480)Peak memory usage: 1061 MB
% 150.09/24.53 % (172480)Instructions burned: 34247 (million)
% 150.09/24.53 % (172480)------------------------------
% 150.09/24.53 % (172480)------------------------------
% 150.09/24.53 % (172475)Success in time 23.562 s
% 150.09/24.53 % Vampire exiting
%------------------------------------------------------------------------------