%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR105+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 : n014.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:43:05 AM UTC 2026
% Result : ContradictoryAxioms 27.85s 7.87s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 86 ( 13 unt; 10 def)
% Number of atoms : 365 ( 9 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 445 ( 166 ~; 155 |; 105 &)
% ( 13 <=>; 6 =>; 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 : 112 ( 0 sgn 88 !; 24 ?)
% 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(f145431,plain,
! [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__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) ) ),
inference(pure_predicate_removal,[],[f1365]) ).
fof(f145691,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(f145692,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,[],[f145691]) ).
fof(f146108,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(f146109,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,[],[f146108]) ).
fof(f146115,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__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) )
| ~ s__instance(X0,s__Chain) ),
inference(ennf_transformation,[],[f145431]) ).
fof(f146524,definition,
! [X1,X2,X0] :
( sP0(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,[sP0])],[predicate_definition_introduction]) ).
fof(f146525,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> sP0(X1,X2,X0) ),
inference(definition_folding,[],[f145692,f146524]) ).
fof(f146543,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__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f146544,plain,
! [X0] :
( sP10
| ~ s__instance(X0,s__Chain) ),
inference(definition_folding,[],[f146115,f146543]) ).
fof(f146602,plain,
! [X1,X2,X0] :
( ( sP0(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) )
| ~ sP0(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f146524]) ).
fof(f146603,plain,
! [X0,X1,X2] :
( ( sP0(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) )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f146602]) ).
fof(f146604,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ( ( ~ s__instance(sK41(X0,X1,X2),X0)
| ~ s__instance(sK42(X0,X1,X2),X0)
| ( ~ s__instance(sK43(X0,X1,X2),X1)
& ~ s__instance(sK43(X0,X1,X2),X2) ) )
& s__instance(sK41(X0,X1,X2),X1)
& s__instance(sK42(X0,X1,X2),X2)
& s__instance(sK43(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) )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41,sK42,sK43]),skolemize(X3,sK41(X0,X1,X2)),skolemize(X4,sK42(X0,X1,X2)),skolemize(X5,sK43(X0,X1,X2))],[f146603]) ).
fof(f146605,plain,
! [X0,X1,X2] :
( ( X1 = s__UnionFn(X2,X0)
| ~ sP0(X1,X2,X0) )
& ( sP0(X1,X2,X0)
| s__UnionFn(X2,X0) != X1 ) ),
inference(nnf_transformation,[],[f146525]) ).
fof(f146699,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__crosses(X1,X2)
& s__crosses(X2,X3)
& ~ s__crosses(X1,X3) )
| ~ sP10 ),
inference(nnf_transformation,[],[f146543]) ).
fof(f146700,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__crosses(X0,X1)
& s__crosses(X1,X2)
& ~ s__crosses(X0,X2) )
| ~ sP10 ),
inference(rectify,[],[f146699]) ).
fof(f146701,plain,
( ( s__instance(sK146,s__Object)
& s__instance(sK145,s__Object)
& s__instance(sK144,s__Object)
& s__instance(sK144,s__ChainLink)
& s__instance(sK145,s__ChainLink)
& s__instance(sK146,s__ChainLink)
& s__crosses(sK144,sK145)
& s__crosses(sK145,sK146)
& ~ s__crosses(sK144,sK146) )
| ~ sP10 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK144,sK145,sK146]),skolemize(X0,sK144),skolemize(X1,sK145),skolemize(X2,sK146)],[f146700]) ).
fof(f147150,plain,
! [X2,X0,X1] :
( s__instance(sK42(X0,X1,X2),X2)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f146604]) ).
fof(f147155,plain,
! [X2,X0,X1] :
( ~ sP0(X1,X2,X0)
| s__UnionFn(X2,X0) = X1 ),
inference(cnf_transformation,[],[f146605]) ).
fof(f147286,plain,
! [X0] : s__instance(X0,s__Entity),
inference(cnf_transformation,[],[f27191]) ).
fof(f148242,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,[],[f146109]) ).
fof(f148246,plain,
( ~ s__crosses(sK144,sK146)
| ~ sP10 ),
inference(cnf_transformation,[],[f146701]) ).
fof(f148247,plain,
( s__crosses(sK145,sK146)
| ~ sP10 ),
inference(cnf_transformation,[],[f146701]) ).
fof(f148248,plain,
( s__crosses(sK144,sK145)
| ~ sP10 ),
inference(cnf_transformation,[],[f146701]) ).
fof(f148252,plain,
( s__instance(sK144,s__Object)
| ~ sP10 ),
inference(cnf_transformation,[],[f146701]) ).
fof(f148253,plain,
( s__instance(sK145,s__Object)
| ~ sP10 ),
inference(cnf_transformation,[],[f146701]) ).
fof(f148254,plain,
( s__instance(sK146,s__Object)
| ~ sP10 ),
inference(cnf_transformation,[],[f146701]) ).
fof(f148255,plain,
! [X0] :
( sP10
| ~ s__instance(X0,s__Chain) ),
inference(cnf_transformation,[],[f146544]) ).
fof(f149990,definition,
( spl240_9
<=> ! [X0] : ~ s__instance(X0,s__Chain) ),
introduced(definition,[new_symbols(definition,[spl240_9])],[avatar_definition]) ).
fof(f149991,plain,
( ! [X0] : ~ s__instance(X0,s__Chain)
| ~ spl240_9 ),
inference(avatar_component_clause,[],[f149990]) ).
fof(f149993,definition,
( spl240_10
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl240_10])],[avatar_definition]) ).
fof(f149996,plain,
( spl240_9
| spl240_10 ),
inference(avatar_split_clause,[],[f148255,f149993,f149990]) ).
fof(f149998,definition,
( spl240_11
<=> s__crosses(sK144,sK146) ),
introduced(definition,[new_symbols(definition,[spl240_11])],[avatar_definition]) ).
fof(f150000,plain,
( ~ s__crosses(sK144,sK146)
| spl240_11 ),
inference(avatar_component_clause,[],[f149998]) ).
fof(f150001,plain,
( ~ spl240_10
| ~ spl240_11 ),
inference(avatar_split_clause,[],[f148246,f149998,f149993]) ).
fof(f150003,definition,
( spl240_12
<=> s__crosses(sK145,sK146) ),
introduced(definition,[new_symbols(definition,[spl240_12])],[avatar_definition]) ).
fof(f150005,plain,
( s__crosses(sK145,sK146)
| ~ spl240_12 ),
inference(avatar_component_clause,[],[f150003]) ).
fof(f150006,plain,
( ~ spl240_10
| spl240_12 ),
inference(avatar_split_clause,[],[f148247,f150003,f149993]) ).
fof(f150008,definition,
( spl240_13
<=> s__crosses(sK144,sK145) ),
introduced(definition,[new_symbols(definition,[spl240_13])],[avatar_definition]) ).
fof(f150010,plain,
( s__crosses(sK144,sK145)
| ~ spl240_13 ),
inference(avatar_component_clause,[],[f150008]) ).
fof(f150011,plain,
( ~ spl240_10
| spl240_13 ),
inference(avatar_split_clause,[],[f148248,f150008,f149993]) ).
fof(f150028,definition,
( spl240_17
<=> s__instance(sK144,s__Object) ),
introduced(definition,[new_symbols(definition,[spl240_17])],[avatar_definition]) ).
fof(f150030,plain,
( s__instance(sK144,s__Object)
| ~ spl240_17 ),
inference(avatar_component_clause,[],[f150028]) ).
fof(f150031,plain,
( ~ spl240_10
| spl240_17 ),
inference(avatar_split_clause,[],[f148252,f150028,f149993]) ).
fof(f150033,definition,
( spl240_18
<=> s__instance(sK145,s__Object) ),
introduced(definition,[new_symbols(definition,[spl240_18])],[avatar_definition]) ).
fof(f150035,plain,
( s__instance(sK145,s__Object)
| ~ spl240_18 ),
inference(avatar_component_clause,[],[f150033]) ).
fof(f150036,plain,
( ~ spl240_10
| spl240_18 ),
inference(avatar_split_clause,[],[f148253,f150033,f149993]) ).
fof(f150038,definition,
( spl240_19
<=> s__instance(sK146,s__Object) ),
introduced(definition,[new_symbols(definition,[spl240_19])],[avatar_definition]) ).
fof(f150040,plain,
( s__instance(sK146,s__Object)
| ~ spl240_19 ),
inference(avatar_component_clause,[],[f150038]) ).
fof(f150041,plain,
( ~ spl240_10
| spl240_19 ),
inference(avatar_split_clause,[],[f148254,f150038,f149993]) ).
fof(f150198,plain,
( ! [X0,X1] : sP0(X0,X1,s__Chain)
| ~ spl240_9 ),
inference(resolution,[],[f147150,f149991]) ).
fof(f150201,plain,
( ! [X0,X1] : s__UnionFn(X0,s__Chain) = X1
| ~ spl240_9 ),
inference(resolution,[],[f150198,f147155]) ).
fof(f150202,plain,
( ! [X2,X0] : X0 = X2
| ~ spl240_9 ),
inference(superposition,[],[f150201,f150201]) ).
fof(f150215,plain,
( ! [X0,X1] : ~ s__instance(X1,X0)
| ~ spl240_9 ),
inference(superposition,[],[f149991,f150202]) ).
fof(f150241,plain,
( ! [X0,X1] : s__instance(X1,X0)
| ~ spl240_9 ),
inference(superposition,[],[f147286,f150202]) ).
fof(f150286,plain,
( $false
| ~ spl240_9 ),
inference(forward_subsumption_resolution,[],[f150241,f150215]) ).
fof(f150287,plain,
~ spl240_9,
inference(avatar_contradiction_clause,[],[f150286]) ).
fof(f150342,plain,
( ! [X0] :
( ~ s__crosses(X0,sK145)
| s__crosses(X0,sK146)
| ~ s__instance(sK146,s__Object)
| ~ s__instance(sK145,s__Object)
| ~ s__instance(X0,s__Object) )
| ~ spl240_12 ),
inference(resolution,[],[f148242,f150005]) ).
fof(f150345,plain,
( ! [X0] :
( ~ s__crosses(X0,sK145)
| s__crosses(X0,sK146)
| ~ s__instance(sK145,s__Object)
| ~ s__instance(X0,s__Object) )
| ~ spl240_12
| ~ spl240_19 ),
inference(forward_subsumption_resolution,[],[f150342,f150040]) ).
fof(f150347,plain,
( ! [X0] :
( ~ s__crosses(X0,sK145)
| s__crosses(X0,sK146)
| ~ s__instance(X0,s__Object) )
| ~ spl240_12
| ~ spl240_18
| ~ spl240_19 ),
inference(forward_subsumption_resolution,[],[f150345,f150035]) ).
fof(f150358,plain,
( s__crosses(sK144,sK146)
| ~ s__instance(sK144,s__Object)
| ~ spl240_12
| ~ spl240_13
| ~ spl240_18
| ~ spl240_19 ),
inference(resolution,[],[f150347,f150010]) ).
fof(f150359,plain,
( ~ s__instance(sK144,s__Object)
| spl240_11
| ~ spl240_12
| ~ spl240_13
| ~ spl240_18
| ~ spl240_19 ),
inference(forward_subsumption_resolution,[],[f150358,f150000]) ).
fof(f150360,plain,
( $false
| spl240_11
| ~ spl240_12
| ~ spl240_13
| ~ spl240_17
| ~ spl240_18
| ~ spl240_19 ),
inference(forward_subsumption_resolution,[],[f150359,f150030]) ).
fof(f150361,plain,
( spl240_11
| ~ spl240_12
| ~ spl240_13
| ~ spl240_17
| ~ spl240_18
| ~ spl240_19 ),
inference(avatar_contradiction_clause,[],[f150360]) ).
cnf(s5,plain,
( spl240_9
| spl240_10 ),
inference(sat_conversion,[],[f149996]) ).
cnf(s6,plain,
( ~ spl240_10
| ~ spl240_11 ),
inference(sat_conversion,[],[f150001]) ).
cnf(s7,plain,
( ~ spl240_10
| spl240_12 ),
inference(sat_conversion,[],[f150006]) ).
cnf(s8,plain,
( ~ spl240_10
| spl240_13 ),
inference(sat_conversion,[],[f150011]) ).
cnf(s12,plain,
( ~ spl240_10
| spl240_17 ),
inference(sat_conversion,[],[f150031]) ).
cnf(s13,plain,
( ~ spl240_10
| spl240_18 ),
inference(sat_conversion,[],[f150036]) ).
cnf(s14,plain,
( ~ spl240_10
| spl240_19 ),
inference(sat_conversion,[],[f150041]) ).
cnf(s46,plain,
~ spl240_9,
inference(sat_conversion,[],[f150287]) ).
cnf(s54,plain,
( spl240_11
| ~ spl240_12
| ~ spl240_13
| ~ spl240_17
| ~ spl240_18
| ~ spl240_19 ),
inference(sat_conversion,[],[f150361]) ).
cnf(s55,plain,
spl240_10,
inference(rat,[],[s5,s46]) ).
cnf(s56,plain,
spl240_19,
inference(rat,[],[s14,s55]) ).
cnf(s57,plain,
spl240_18,
inference(rat,[],[s13,s55]) ).
cnf(s58,plain,
spl240_17,
inference(rat,[],[s12,s55]) ).
cnf(s62,plain,
spl240_13,
inference(rat,[],[s8,s55]) ).
cnf(s63,plain,
spl240_12,
inference(rat,[],[s7,s55]) ).
cnf(s64,plain,
~ spl240_11,
inference(rat,[],[s6,s55]) ).
cnf(s66,plain,
$false,
inference(rat,[],[s54,s56,s57,s58,s62,s63,s64]) ).
fof(f150362,plain,
$false,
inference(avatar_sat_refutation,[],[s66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR105+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.16 % Computer : n014.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Mon Sep 28 22:55:15 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.16 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 Running first-order theorem proving
% 0.09/0.20 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
% 16.16/5.50 % (2268976)Detected formulas, will run a generic FOF schedule.
% 16.16/5.50 % (2268982)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=2603506512:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 16.16/5.50 % (2268981)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=2151716289:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 16.16/5.50 % (2268983)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=2662703666:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 16.16/5.50 % (2268984)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2104694670:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 16.16/5.50 % (2268985)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1309394637:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 16.16/5.50 % (2268986)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3247123596:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 16.16/5.50 % (2268987)dis-21_1_sil=8000:lcm=predicate:random_seed=350945822: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)
% 16.16/5.50 % (2268984)Instruction limit reached!
% 16.16/5.50 % (2268984)------------------------------
% 16.16/5.50 % (2268984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/5.50 % (2268984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/5.50 % (2268984)CaDiCaL version: 2.1.3
% 16.16/5.50 % (2268984)Termination reason: Instruction limit
% 16.16/5.50 % (2268984)Termination phase: SInE selection
% 16.16/5.50 % (2268984)Time elapsed: 0.061 s
% 16.16/5.50 % (2268984)Peak memory usage: 164 MB
% 16.16/5.50 % (2268984)Instructions burned: 111 (million)
% 16.16/5.50 % (2268985)Instruction limit reached!
% 16.16/5.50 % (2268985)------------------------------
% 16.16/5.50 % (2268985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/5.50 % (2268985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/5.50 % (2268985)CaDiCaL version: 2.1.3
% 16.16/5.50 % (2268985)Termination reason: Instruction limit
% 16.16/5.50 % (2268985)Termination phase: SInE selection
% 16.16/5.50 % (2268985)Time elapsed: 0.071 s
% 16.16/5.50 % (2268985)Peak memory usage: 164 MB
% 16.16/5.50 % (2268985)Instructions burned: 119 (million)
% 16.16/5.50 % (2268986)Instruction limit reached!
% 16.16/5.50 % (2268986)------------------------------
% 16.16/5.50 % (2268986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/5.50 % (2268986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/5.50 % (2268986)CaDiCaL version: 2.1.3
% 16.16/5.50 % (2268986)Termination reason: Instruction limit
% 16.16/5.50 % (2268986)Termination phase: Property scanning
% 16.16/5.50 % (2268986)Time elapsed: 0.074 s
% 16.16/5.50 % (2268986)Peak memory usage: 165 MB
% 16.16/5.50 % (2268986)Instructions burned: 139 (million)
% 16.16/5.50 % (2268987)Instruction limit reached!
% 16.16/5.50 % (2268987)------------------------------
% 16.16/5.50 % (2268987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/5.50 % (2268987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/5.50 % (2268987)CaDiCaL version: 2.1.3
% 16.16/5.50 % (2268987)Termination reason: Instruction limit
% 16.16/5.50 % (2268987)Termination phase: SInE selection
% 16.16/5.50 % (2268987)Time elapsed: 0.077 s
% 16.16/5.50 % (2268987)Peak memory usage: 165 MB
% 16.16/5.50 % (2268987)Instructions burned: 130 (million)
% 16.16/5.50 % (2268995)lrs+10_1_sil=8000:sp=occurrence:random_seed=2332414693:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 16.16/5.50 % (2268997)lrs+1011_1_sil=32000:sp=occurrence:random_seed=256233444:i=325:sd=1:ss=axioms:sgt=32_2969 on theBenchmark for (2969ds/325Mi)
% 16.16/5.50 % (2268996)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2944836559:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/157Mi)
% 16.16/5.50 % (2268998)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=1800520780:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 16.16/5.50 % (2268996)Instruction limit reached!
% 25.89/6.78 % (2268996)------------------------------
% 25.89/6.78 % (2268996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2268996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2268996)CaDiCaL version: 2.1.3
% 25.89/6.78 % (2268996)Termination reason: Instruction limit
% 25.89/6.78 % (2268996)Termination phase: Property scanning
% 25.89/6.78 % (2268996)Time elapsed: 0.084 s
% 25.89/6.78 % (2268996)Peak memory usage: 165 MB
% 25.89/6.78 % (2268996)Instructions burned: 157 (million)
% 25.89/6.78 % (2268995)Instruction limit reached!
% 25.89/6.78 % (2268995)------------------------------
% 25.89/6.78 % (2268995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2268995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2268995)CaDiCaL version: 2.1.3
% 25.89/6.78 % (2268995)Termination reason: Instruction limit
% 25.89/6.78 % (2268995)Termination phase: SInE selection
% 25.89/6.78 % (2268995)Time elapsed: 0.157 s
% 25.89/6.78 % (2268995)Peak memory usage: 165 MB
% 25.89/6.78 % (2268995)Instructions burned: 286 (million)
% 25.89/6.78 % (2268998)Instruction limit reached!
% 25.89/6.78 % (2268998)------------------------------
% 25.89/6.78 % (2268998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2268998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2268998)CaDiCaL version: 2.1.3
% 25.89/6.78 % (2268998)Termination reason: Instruction limit
% 25.89/6.78 % (2268998)Termination phase: Property scanning
% 25.89/6.78 % (2268998)Time elapsed: 0.123 s
% 25.89/6.78 % (2268998)Peak memory usage: 165 MB
% 25.89/6.78 % (2268998)Instructions burned: 249 (million)
% 25.89/6.78 % (2268997)Instruction limit reached!
% 25.89/6.78 % (2268997)------------------------------
% 25.89/6.78 % (2268997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2268997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2268997)CaDiCaL version: 2.1.3
% 25.89/6.78 % (2268997)Termination reason: Instruction limit
% 25.89/6.78 % (2268997)Termination phase: SInE selection
% 25.89/6.78 % (2268997)Time elapsed: 0.187 s
% 25.89/6.78 % (2268997)Peak memory usage: 164 MB
% 25.89/6.78 % (2268997)Instructions burned: 326 (million)
% 25.89/6.78 % (2269003)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2388659273:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2966 on theBenchmark for (2966ds/294Mi)
% 25.89/6.78 % (2269004)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=554489532:i=2350_2966 on theBenchmark for (2966ds/2350Mi)
% 25.89/6.78 % (2269005)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2027304682:cts=off:i=113:fsr=off:ss=included:sgt=4_2965 on theBenchmark for (2965ds/113Mi)
% 25.89/6.78 % (2269006)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3887465515:i=127:av=off:fsr=off:sup=off_2965 on theBenchmark for (2965ds/127Mi)
% 25.89/6.78 % (2269005)Instruction limit reached!
% 25.89/6.78 % (2269005)------------------------------
% 25.89/6.78 % (2269005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2269005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2269005)CaDiCaL version: 2.1.3
% 25.89/6.78 % (2269005)Termination reason: Instruction limit
% 25.89/6.78 % (2269005)Termination phase: SInE selection
% 25.89/6.78 % (2269005)Time elapsed: 0.067 s
% 25.89/6.78 % (2269005)Peak memory usage: 165 MB
% 25.89/6.78 % (2269005)Instructions burned: 115 (million)
% 25.89/6.78 % (2269003)Instruction limit reached!
% 25.89/6.78 % (2269003)------------------------------
% 25.89/6.78 % (2269003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2269003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2269003)CaDiCaL version: 2.1.3
% 25.89/6.78 % (2269003)Termination reason: Instruction limit
% 25.89/6.78 % (2269003)Termination phase: SInE selection
% 25.89/6.78 % (2269003)Time elapsed: 0.161 s
% 25.89/6.78 % (2269003)Peak memory usage: 165 MB
% 25.89/6.78 % (2269003)Instructions burned: 296 (million)
% 25.89/6.78 % (2269006)Instruction limit reached!
% 25.89/6.78 % (2269006)------------------------------
% 25.89/6.78 % (2269006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.89/6.78 % (2269006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.89/6.78 % (2269006)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269006)Termination reason: Instruction limit
% 27.85/7.87 % (2269006)Termination phase: Preprocessing 1
% 27.85/7.87 % (2269006)Time elapsed: 0.086 s
% 27.85/7.87 % (2269006)Peak memory usage: 165 MB
% 27.85/7.87 % (2269006)Instructions burned: 127 (million)
% 27.85/7.87 % (2269011)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3908936141:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2963 on theBenchmark for (2963ds/114Mi)
% 27.85/7.87 % (2269012)lrs+10_1_sil=8000:sp=occurrence:random_seed=3856707957:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 27.85/7.87 % (2269011)Instruction limit reached!
% 27.85/7.87 % (2269011)------------------------------
% 27.85/7.87 % (2269011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269011)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269011)Termination reason: Instruction limit
% 27.85/7.87 % (2269011)Termination phase: Property scanning
% 27.85/7.87 % (2269011)Time elapsed: 0.066 s
% 27.85/7.87 % (2269011)Peak memory usage: 165 MB
% 27.85/7.87 % (2269011)Instructions burned: 116 (million)
% 27.85/7.87 % (2269013)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1474153893:i=437:sd=1:aac=none:ss=included_2962 on theBenchmark for (2962ds/437Mi)
% 27.85/7.87 % (2269016)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1316927945:i=5202:ss=axioms:sgt=16_2961 on theBenchmark for (2961ds/5202Mi)
% 27.85/7.87 % (2269013)Instruction limit reached!
% 27.85/7.87 % (2269013)------------------------------
% 27.85/7.87 % (2269013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269013)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269013)Termination reason: Instruction limit
% 27.85/7.87 % (2269013)Termination phase: Saturation
% 27.85/7.87 % (2269013)Time elapsed: 0.267 s
% 27.85/7.87 % (2269013)Peak memory usage: 169 MB
% 27.85/7.87 % (2269013)Instructions burned: 437 (million)
% 27.85/7.87 % (2269019)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4063419940:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2958 on theBenchmark for (2958ds/134Mi)
% 27.85/7.87 % (2269012)Instruction limit reached!
% 27.85/7.87 % (2269012)------------------------------
% 27.85/7.87 % (2269012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269012)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269012)Termination reason: Instruction limit
% 27.85/7.87 % (2269012)Termination phase: Saturation
% 27.85/7.87 % (2269012)Time elapsed: 0.535 s
% 27.85/7.87 % (2269012)Peak memory usage: 174 MB
% 27.85/7.87 % (2269012)Instructions burned: 908 (million)
% 27.85/7.87 % (2269019)Instruction limit reached!
% 27.85/7.87 % (2269019)------------------------------
% 27.85/7.87 % (2269019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269019)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269019)Termination reason: Instruction limit
% 27.85/7.87 % (2269019)Termination phase: SInE selection
% 27.85/7.87 % (2269019)Time elapsed: 0.080 s
% 27.85/7.87 % (2269019)Peak memory usage: 165 MB
% 27.85/7.87 % (2269019)Instructions burned: 135 (million)
% 27.85/7.87 % (2269021)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3016842439:st=8:i=592:sd=3:ep=RST:ss=axioms_2956 on theBenchmark for (2956ds/592Mi)
% 27.85/7.87 % (2269022)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=796540775:st=3:i=13193:sd=3:ss=axioms_2955 on theBenchmark for (2955ds/13193Mi)
% 27.85/7.87 % (2269004)Instruction limit reached!
% 27.85/7.87 % (2269004)------------------------------
% 27.85/7.87 % (2269004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269004)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269004)Termination reason: Instruction limit
% 27.85/7.87 % (2269004)Termination phase: Property scanning
% 27.85/7.87 % (2269004)Time elapsed: 1.184 s
% 27.85/7.87 % (2269004)Peak memory usage: 194 MB
% 27.85/7.87 % (2269004)Instructions burned: 2351 (million)
% 27.85/7.87 % (2269021)Instruction limit reached!
% 27.85/7.87 % (2269021)------------------------------
% 27.85/7.87 % (2269021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269021)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269021)Termination reason: Instruction limit
% 27.85/7.87 % (2269021)Termination phase: Preprocessing 1
% 27.85/7.87 % (2269021)Time elapsed: 0.315 s
% 27.85/7.87 % (2269021)Peak memory usage: 167 MB
% 27.85/7.87 % (2269021)Instructions burned: 592 (million)
% 27.85/7.87 % (2269025)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=3179448265:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/125Mi)
% 27.85/7.87 % (2269025)Instruction limit reached!
% 27.85/7.87 % (2269025)------------------------------
% 27.85/7.87 % (2269025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269025)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269025)Termination reason: Instruction limit
% 27.85/7.87 % (2269025)Termination phase: Property scanning
% 27.85/7.87 % (2269025)Time elapsed: 0.069 s
% 27.85/7.87 % (2269025)Peak memory usage: 165 MB
% 27.85/7.87 % (2269025)Instructions burned: 125 (million)
% 27.85/7.87 % (2269026)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2200137476:i=134:gtgl=5:slsql=off:gtg=exists_sym_2951 on theBenchmark for (2951ds/134Mi)
% 27.85/7.87 % (2269026)Instruction limit reached!
% 27.85/7.87 % (2269026)------------------------------
% 27.85/7.87 % (2269026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269026)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269026)Termination reason: Instruction limit
% 27.85/7.87 % (2269026)Termination phase: Property scanning
% 27.85/7.87 % (2269026)Time elapsed: 0.077 s
% 27.85/7.87 % (2269026)Peak memory usage: 165 MB
% 27.85/7.87 % (2269026)Instructions burned: 135 (million)
% 27.85/7.87 % (2269028)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1010372498:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2950 on theBenchmark for (2950ds/141Mi)
% 27.85/7.87 % (2269028)Instruction limit reached!
% 27.85/7.87 % (2269028)------------------------------
% 27.85/7.87 % (2269028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269028)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269028)Termination reason: Instruction limit
% 27.85/7.87 % (2269028)Termination phase: SInE selection
% 27.85/7.87 % (2269028)Time elapsed: 0.084 s
% 27.85/7.87 % (2269028)Peak memory usage: 165 MB
% 27.85/7.87 % (2269028)Instructions burned: 141 (million)
% 27.85/7.87 % (2269030)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3487213799:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2948 on theBenchmark for (2948ds/431Mi)
% 27.85/7.87 % (2269032)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=3070529968:i=6060:aac=none:ins=25_2947 on theBenchmark for (2947ds/6060Mi)
% 27.85/7.87 % (2269030)Refutation not found, incomplete strategy
% 27.85/7.87 % (2269030)------------------------------
% 27.85/7.87 % (2269030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269030)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269030)Termination reason: Refutation not found, incomplete strategy
% 27.85/7.87 % (2269030)Time elapsed: 0.263 s
% 27.85/7.87 % (2269030)Peak memory usage: 170 MB
% 27.85/7.87 % (2269030)Instructions burned: 399 (million)
% 27.85/7.87 % (2269030)------------------------------
% 27.85/7.87 % (2269030)------------------------------
% 27.85/7.87 % (2269035)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=1610144961:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2941 on theBenchmark for (2941ds/150Mi)
% 27.85/7.87 % (2269035)Instruction limit reached!
% 27.85/7.87 % (2269035)------------------------------
% 27.85/7.87 % (2269035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269035)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269035)Termination reason: Instruction limit
% 27.85/7.87 % (2269035)Termination phase: SInE selection
% 27.85/7.87 % (2269035)Time elapsed: 0.090 s
% 27.85/7.87 % (2269035)Peak memory usage: 165 MB
% 27.85/7.87 % (2269035)Instructions burned: 150 (million)
% 27.85/7.87 % (2269037)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3834153083:i=14155:bd=all_2938 on theBenchmark for (2938ds/14155Mi)
% 27.85/7.87 % (2269022)First to succeed.
% 27.85/7.87 % (2269022)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2268976"
% 27.85/7.87 % (2269016)Instruction limit reached!
% 27.85/7.87 % (2269016)------------------------------
% 27.85/7.87 % (2269016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/7.87 % (2269016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/7.87 % (2269016)CaDiCaL version: 2.1.3
% 27.85/7.87 % (2269016)Termination reason: Instruction limit
% 27.85/7.87 % (2269016)Termination phase: Saturation
% 27.85/7.87 % (2269016)Time elapsed: 3.108 s
% 27.85/7.87 % (2269016)Peak memory usage: 266 MB
% 27.85/7.87 % (2269016)Instructions burned: 5204 (million)
% 27.85/7.87 % (2269022)Refutation found. Thanks to Tanya!
% 27.85/7.87 % SZS status ContradictoryAxioms for theBenchmark
% 27.85/7.87 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/8.13 % (2269022)------------------------------
% 0.18/8.13 % (2269022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/8.13 % (2269022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/8.13 % (2269022)CaDiCaL version: 2.1.3
% 0.18/8.13 % (2269022)Termination reason: Refutation
% 0.18/8.13 % (2269022)Time elapsed: 2.261 s
% 0.18/8.13 % (2269022)Peak memory usage: 304 MB
% 0.18/8.13 % (2269022)Instructions burned: 3591 (million)
% 0.18/8.13 % (2269022)------------------------------
% 0.18/8.13 % (2269022)------------------------------
% 0.18/8.13 % (2268976)Success in time 7.236 s
% 0.18/8.13 % Vampire exiting
%------------------------------------------------------------------------------