%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR087+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:49 AM UTC 2026
% Result : ContradictoryAxioms 195.97s 34.71s
% Output : Refutation 221.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 6
% Syntax : Number of formulae : 65 ( 9 unt; 3 def)
% Number of atoms : 236 ( 36 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 274 ( 103 ~; 117 |; 43 &)
% ( 7 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 163 ( 0 sgn 156 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27191,axiom,
! [X0] : s__instance(X0,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27371) ).
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/sandbox/benchmark/theBenchmark.p',kb_SUMO_32603) ).
fof(f32448,axiom,
! [X0] :
( s__instance(X0,s__SetOrClass)
=> ( s__instance(X0,s__NullSet)
=> ~ ? [X1] : s__instance(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_32640) ).
fof(f162802,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(f162803,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,[],[f162802]) ).
fof(f162804,plain,
! [X0] :
( ! [X1] : ~ s__instance(X1,X0)
| ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f32448]) ).
fof(f162805,plain,
! [X0] :
( ! [X1] : ~ s__instance(X1,X0)
| ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f162804]) ).
fof(f168668,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(f168669,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> sP84(X1,X2,X0) ),
inference(definition_folding,[],[f162803,f168668]) ).
fof(f169895,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,[],[f168668]) ).
fof(f169896,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,[],[f169895]) ).
fof(f169897,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))],[f169896]) ).
fof(f169898,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,[],[f168669]) ).
fof(f195228,plain,
! [X0] : s__instance(X0,s__Entity),
inference(cnf_transformation,[],[f27191]) ).
fof(f200555,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| s__instance(X2,s__SetOrClass) ),
inference(cnf_transformation,[],[f169897]) ).
fof(f200556,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f169897]) ).
fof(f200557,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f169897]) ).
fof(f200558,plain,
! [X2,X0,X1] :
( s__instance(sK1219(X0,X1,X2),X0)
| sP84(X0,X1,X2) ),
inference(cnf_transformation,[],[f169897]) ).
fof(f200559,plain,
! [X2,X0,X1] :
( s__instance(sK1218(X0,X1,X2),X2)
| sP84(X0,X1,X2) ),
inference(cnf_transformation,[],[f169897]) ).
fof(f200560,plain,
! [X2,X0,X1] :
( s__instance(sK1217(X0,X1,X2),X1)
| sP84(X0,X1,X2) ),
inference(cnf_transformation,[],[f169897]) ).
fof(f200564,plain,
! [X2,X0,X1] :
( ~ sP84(X1,X2,X0)
| s__UnionFn(X2,X0) = X1 ),
inference(cnf_transformation,[],[f169898]) ).
fof(f200600,plain,
! [X0,X1] :
( ~ s__instance(X1,X0)
| ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f162805]) ).
fof(f322555,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass)
| sP84(X1,X0,X2) ),
inference(resolution,[],[f200600,f200560]) ).
fof(f322556,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass)
| sP84(X1,X2,X0) ),
inference(resolution,[],[f200600,f200559]) ).
fof(f322567,plain,
! [X2,X0,X1] :
( sP84(X1,X2,X0)
| ~ s__instance(X0,s__NullSet) ),
inference(forward_subsumption_resolution,[],[f322556,f200555]) ).
fof(f322568,plain,
! [X2,X0,X1] :
( sP84(X1,X0,X2)
| ~ s__instance(X0,s__NullSet) ),
inference(forward_subsumption_resolution,[],[f322555,f200557]) ).
fof(f322581,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__NullSet)
| s__UnionFn(X1,X0) = X2 ),
inference(resolution,[],[f322567,f200564]) ).
fof(f322584,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f200558,f200600]) ).
fof(f322585,plain,
! [X2,X3,X0,X1] :
( sP84(s__NullSet,X0,X1)
| s__UnionFn(X2,sK1219(s__NullSet,X0,X1)) = X3 ),
inference(resolution,[],[f200558,f322581]) ).
fof(f322587,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| ~ s__instance(X0,s__NullSet) ),
inference(forward_subsumption_resolution,[],[f322584,f200556]) ).
fof(f322588,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__NullSet)
| s__UnionFn(X1,X2) = X0 ),
inference(resolution,[],[f322587,f200564]) ).
fof(f322589,plain,
! [X2,X3,X0,X1] :
( sP84(X2,s__NullSet,X3)
| s__UnionFn(X0,X1) = sK1217(X2,s__NullSet,X3) ),
inference(resolution,[],[f322588,f200560]) ).
fof(f322599,definition,
( spl3219_743
<=> ! [X4,X5] : s__NullSet = s__UnionFn(X4,X5) ),
introduced(definition,[new_symbols(definition,[spl3219_743])],[avatar_definition]) ).
fof(f322600,plain,
( ! [X4,X5] : s__NullSet = s__UnionFn(X4,X5)
| ~ spl3219_743 ),
inference(avatar_component_clause,[],[f322599]) ).
fof(f322611,plain,
! [X2,X3,X0,X1] :
( s__UnionFn(X0,sK1219(s__NullSet,X1,X2)) = X3
| s__NullSet = s__UnionFn(X1,X2) ),
inference(resolution,[],[f322585,f200564]) ).
fof(f322612,plain,
! [X2,X3,X0,X1] :
( s__UnionFn(X0,X1) = sK1217(X2,s__NullSet,X3)
| s__UnionFn(s__NullSet,X3) = X2 ),
inference(resolution,[],[f322589,f200564]) ).
fof(f322613,plain,
( ! [X2,X3] :
( s__NullSet = sK1217(X2,s__NullSet,X3)
| s__UnionFn(s__NullSet,X3) = X2 )
| ~ spl3219_743 ),
inference(forward_demodulation,[],[f322612,f322600]) ).
fof(f322614,plain,
( ! [X2,X3] :
( s__NullSet = sK1217(X2,s__NullSet,X3)
| s__NullSet = X2 )
| ~ spl3219_743 ),
inference(forward_demodulation,[],[f322613,f322600]) ).
fof(f322615,plain,
( ! [X0,X1] :
( s__instance(s__NullSet,s__NullSet)
| sP84(X0,s__NullSet,X1)
| s__NullSet = X0 )
| ~ spl3219_743 ),
inference(superposition,[],[f200560,f322614]) ).
fof(f322616,plain,
( ! [X0,X1] :
( sP84(X0,s__NullSet,X1)
| s__NullSet = X0 )
| ~ spl3219_743 ),
inference(forward_subsumption_resolution,[],[f322615,f322568]) ).
fof(f322617,plain,
( ! [X0,X1] :
( s__NullSet = X0
| s__UnionFn(s__NullSet,X1) = X0 )
| ~ spl3219_743 ),
inference(resolution,[],[f322616,f200564]) ).
fof(f322618,plain,
( ! [X0] :
( s__NullSet = X0
| s__NullSet = X0 )
| ~ spl3219_743 ),
inference(forward_demodulation,[],[f322617,f322600]) ).
fof(f322619,plain,
( ! [X0] : s__NullSet = X0
| ~ spl3219_743 ),
inference(duplicate_literal_removal,[],[f322618]) ).
fof(f322620,plain,
( ! [X0,X1] : X0 = X1
| ~ spl3219_743 ),
inference(superposition,[],[f322619,f322619]) ).
fof(f322664,plain,
( ! [X0,X1] : s__instance(X1,X0)
| ~ spl3219_743 ),
inference(superposition,[],[f195228,f322620]) ).
fof(f322684,plain,
( ! [X0] :
( ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl3219_743 ),
inference(resolution,[],[f322664,f200600]) ).
fof(f322688,plain,
( ! [X0] : ~ s__instance(X0,s__NullSet)
| ~ spl3219_743 ),
inference(forward_subsumption_resolution,[],[f322684,f322664]) ).
fof(f322689,plain,
( $false
| ~ spl3219_743 ),
inference(forward_subsumption_resolution,[],[f322688,f322664]) ).
fof(f322690,plain,
~ spl3219_743,
inference(avatar_contradiction_clause,[],[f322689]) ).
fof(f322693,plain,
! [X2,X3,X0,X4] :
( X0 = X4
| s__NullSet = s__UnionFn(X2,X3)
| s__NullSet = s__UnionFn(X2,X3) ),
inference(superposition,[],[f322611,f322611]) ).
fof(f322702,plain,
! [X2,X3,X0,X4] :
( X0 = X4
| s__NullSet = s__UnionFn(X2,X3) ),
inference(duplicate_literal_removal,[],[f322693]) ).
fof(f322710,definition,
( spl3219_747
<=> ! [X4,X0] : X0 = X4 ),
introduced(definition,[new_symbols(definition,[spl3219_747])],[avatar_definition]) ).
fof(f322711,plain,
( ! [X0,X4] : X0 = X4
| ~ spl3219_747 ),
inference(avatar_component_clause,[],[f322710]) ).
fof(f322712,plain,
( spl3219_743
| spl3219_747 ),
inference(avatar_split_clause,[],[f322702,f322710,f322599]) ).
fof(f322739,plain,
( ! [X0,X1] : s__instance(X1,X0)
| ~ spl3219_747 ),
inference(superposition,[],[f195228,f322711]) ).
fof(f322757,plain,
( ! [X0] :
( ~ s__instance(X0,s__NullSet)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl3219_747 ),
inference(resolution,[],[f322739,f200600]) ).
fof(f322761,plain,
( ! [X0] : ~ s__instance(X0,s__NullSet)
| ~ spl3219_747 ),
inference(forward_subsumption_resolution,[],[f322757,f322739]) ).
fof(f322762,plain,
( $false
| ~ spl3219_747 ),
inference(forward_subsumption_resolution,[],[f322761,f322739]) ).
fof(f322763,plain,
~ spl3219_747,
inference(avatar_contradiction_clause,[],[f322762]) ).
cnf(s555,plain,
~ spl3219_743,
inference(sat_conversion,[],[f322690]) ).
cnf(s558,plain,
( spl3219_743
| spl3219_747 ),
inference(sat_conversion,[],[f322712]) ).
cnf(s561,plain,
~ spl3219_747,
inference(sat_conversion,[],[f322763]) ).
cnf(s562,plain,
spl3219_743,
inference(rat,[],[s558,s561]) ).
cnf(s563,plain,
$false,
inference(rat,[],[s555,s562]) ).
fof(f322764,plain,
$false,
inference(avatar_sat_refutation,[],[s563]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR087+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.25 % Computer : n017.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Mon Sep 28 22:32:51 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.31 Running first-order theorem proving
% 0.25/0.31 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.83/7.27 % (4112076)Detected formulas, will run a generic FOF schedule.
% 25.83/7.27 % (4112093)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=1011467176:i=141193_2967 on theBenchmark for (2967ds/141193Mi)
% 25.83/7.27 % (4112096)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=841352633:i=109:sd=1:ins=1:gsp=on:ss=axioms_2967 on theBenchmark for (2967ds/109Mi)
% 25.83/7.27 % (4112095)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=1645093996:i=141695:sd=1:nm=32:gsp=on:ss=included_2967 on theBenchmark for (2967ds/141695Mi)
% 25.83/7.27 % (4112094)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=2193523829:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2967 on theBenchmark for (2967ds/134677Mi)
% 25.83/7.27 % (4112099)dis-21_1_sil=8000:lcm=predicate:random_seed=186865996:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2967 on theBenchmark for (2967ds/129Mi)
% 25.83/7.27 % (4112098)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4211762909:s2a=on:i=139:gtg=position_2967 on theBenchmark for (2967ds/139Mi)
% 25.83/7.27 % (4112097)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3925049993:i=119:av=off:ss=axioms_2967 on theBenchmark for (2967ds/119Mi)
% 25.83/7.27 % (4112096)Instruction limit reached!
% 25.83/7.27 % (4112096)------------------------------
% 25.83/7.27 % (4112096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/7.27 % (4112096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/7.27 % (4112096)CaDiCaL version: 2.1.3
% 25.83/7.27 % (4112096)Termination reason: Instruction limit
% 25.83/7.27 % (4112096)Termination phase: SInE selection
% 25.83/7.27 % (4112096)Time elapsed: 0.094 s
% 25.83/7.27 % (4112096)Peak memory usage: 164 MB
% 25.83/7.27 % (4112096)Instructions burned: 109 (million)
% 25.83/7.27 % (4112097)Instruction limit reached!
% 25.83/7.27 % (4112097)------------------------------
% 25.83/7.27 % (4112097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/7.27 % (4112097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/7.27 % (4112097)CaDiCaL version: 2.1.3
% 25.83/7.27 % (4112097)Termination reason: Instruction limit
% 25.83/7.27 % (4112097)Termination phase: SInE selection
% 25.83/7.27 % (4112097)Time elapsed: 0.101 s
% 25.83/7.27 % (4112097)Peak memory usage: 164 MB
% 25.83/7.27 % (4112097)Instructions burned: 119 (million)
% 25.83/7.27 % (4112099)Instruction limit reached!
% 25.83/7.27 % (4112099)------------------------------
% 25.83/7.27 % (4112099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/7.27 % (4112099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/7.27 % (4112099)CaDiCaL version: 2.1.3
% 25.83/7.27 % (4112099)Termination reason: Instruction limit
% 25.83/7.27 % (4112099)Termination phase: SInE selection
% 25.83/7.27 % (4112099)Time elapsed: 0.109 s
% 25.83/7.27 % (4112099)Peak memory usage: 164 MB
% 25.83/7.27 % (4112099)Instructions burned: 130 (million)
% 25.83/7.27 % (4112098)Instruction limit reached!
% 25.83/7.27 % (4112098)------------------------------
% 25.83/7.27 % (4112098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/7.27 % (4112098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/7.27 % (4112098)CaDiCaL version: 2.1.3
% 25.83/7.27 % (4112098)Termination reason: Instruction limit
% 25.83/7.27 % (4112098)Termination phase: Property scanning
% 25.83/7.27 % (4112098)Time elapsed: 0.136 s
% 25.83/7.27 % (4112098)Peak memory usage: 165 MB
% 25.83/7.27 % (4112098)Instructions burned: 140 (million)
% 25.83/7.27 % (4112107)lrs+10_1_sil=8000:sp=occurrence:random_seed=527369740:i=285:sd=3:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/285Mi)
% 25.83/7.27 % (4112110)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=3611823555:s2a=on:i=248:s2at=1.23:gtg=position_2963 on theBenchmark for (2963ds/248Mi)
% 25.83/7.27 % (4112109)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2205815738:i=325:sd=1:ss=axioms:sgt=32_2963 on theBenchmark for (2963ds/325Mi)
% 25.83/7.27 % (4112108)lrs+10_1_sil=32000:urr=on:br=off:random_seed=470867858:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/157Mi)
% 25.83/7.27 % (4112107)Instruction limit reached!
% 30.46/7.96 % (4112107)------------------------------
% 30.46/7.96 % (4112107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112107)CaDiCaL version: 2.1.3
% 30.46/7.96 % (4112107)Termination reason: Instruction limit
% 30.46/7.96 % (4112107)Termination phase: SInE selection
% 30.46/7.96 % (4112107)Time elapsed: 0.146 s
% 30.46/7.96 % (4112107)Peak memory usage: 165 MB
% 30.46/7.96 % (4112107)Instructions burned: 287 (million)
% 30.46/7.96 % (4112110)Instruction limit reached!
% 30.46/7.96 % (4112110)------------------------------
% 30.46/7.96 % (4112110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112110)CaDiCaL version: 2.1.3
% 30.46/7.96 % (4112110)Termination reason: Instruction limit
% 30.46/7.96 % (4112110)Termination phase: Property scanning
% 30.46/7.96 % (4112110)Time elapsed: 0.133 s
% 30.46/7.96 % (4112110)Peak memory usage: 165 MB
% 30.46/7.96 % (4112110)Instructions burned: 249 (million)
% 30.46/7.96 % (4112108)Instruction limit reached!
% 30.46/7.96 % (4112108)------------------------------
% 30.46/7.96 % (4112108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112108)CaDiCaL version: 2.1.3
% 30.46/7.96 % (4112108)Termination reason: Instruction limit
% 30.46/7.96 % (4112108)Termination phase: Property scanning
% 30.46/7.96 % (4112108)Time elapsed: 0.139 s
% 30.46/7.96 % (4112108)Peak memory usage: 165 MB
% 30.46/7.96 % (4112108)Instructions burned: 157 (million)
% 30.46/7.96 % (4112109)Instruction limit reached!
% 30.46/7.96 % (4112109)------------------------------
% 30.46/7.96 % (4112109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112109)CaDiCaL version: 2.1.3
% 30.46/7.96 % (4112109)Termination reason: Instruction limit
% 30.46/7.96 % (4112109)Termination phase: SInE selection
% 30.46/7.96 % (4112109)Time elapsed: 0.216 s
% 30.46/7.96 % (4112109)Peak memory usage: 164 MB
% 30.46/7.96 % (4112109)Instructions burned: 325 (million)
% 30.46/7.96 % (4112117)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3301201134:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2960 on theBenchmark for (2960ds/294Mi)
% 30.46/7.96 % (4112119)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3107244887:i=2350_2959 on theBenchmark for (2959ds/2350Mi)
% 30.46/7.96 % (4112121)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=74385951:cts=off:i=113:fsr=off:ss=included:sgt=4_2959 on theBenchmark for (2959ds/113Mi)
% 30.46/7.96 % (4112117)Instruction limit reached!
% 30.46/7.96 % (4112117)------------------------------
% 30.46/7.96 % (4112117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112117)CaDiCaL version: 2.1.3
% 30.46/7.96 % (4112117)Termination reason: Instruction limit
% 30.46/7.96 % (4112117)Termination phase: SInE selection
% 30.46/7.96 % (4112117)Time elapsed: 0.146 s
% 30.46/7.96 % (4112117)Peak memory usage: 164 MB
% 30.46/7.96 % (4112117)Instructions burned: 296 (million)
% 30.46/7.96 % (4112122)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2398467287:i=127:av=off:fsr=off:sup=off_2958 on theBenchmark for (2958ds/127Mi)
% 30.46/7.96 % (4112121)Instruction limit reached!
% 30.46/7.96 % (4112121)------------------------------
% 30.46/7.96 % (4112121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112121)CaDiCaL version: 2.1.3
% 30.46/7.96 % (4112121)Termination reason: Instruction limit
% 30.46/7.96 % (4112121)Termination phase: SInE selection
% 30.46/7.96 % (4112121)Time elapsed: 0.106 s
% 30.46/7.96 % (4112121)Peak memory usage: 165 MB
% 30.46/7.96 % (4112121)Instructions burned: 113 (million)
% 30.46/7.96 % (4112122)Instruction limit reached!
% 30.46/7.96 % (4112122)------------------------------
% 30.46/7.96 % (4112122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.46/7.96 % (4112122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.46/7.96 % (4112122)CaDiCaL version: 2.1.3
% 41.28/9.41 % (4112122)Termination reason: Instruction limit
% 41.28/9.41 % (4112122)Termination phase: Preprocessing 1
% 41.28/9.41 % (4112122)Time elapsed: 0.143 s
% 41.28/9.41 % (4112122)Peak memory usage: 165 MB
% 41.28/9.41 % (4112122)Instructions burned: 127 (million)
% 41.28/9.41 % (4112126)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1113181560:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2956 on theBenchmark for (2956ds/114Mi)
% 41.28/9.41 % (4112126)Instruction limit reached!
% 41.28/9.41 % (4112126)------------------------------
% 41.28/9.41 % (4112126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.28/9.41 % (4112126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.28/9.41 % (4112126)CaDiCaL version: 2.1.3
% 41.28/9.41 % (4112126)Termination reason: Instruction limit
% 41.28/9.41 % (4112126)Termination phase: Property scanning
% 41.28/9.41 % (4112126)Time elapsed: 0.065 s
% 41.28/9.41 % (4112126)Peak memory usage: 165 MB
% 41.28/9.41 % (4112126)Instructions burned: 116 (million)
% 41.28/9.41 % (4112128)lrs+10_1_sil=8000:sp=occurrence:random_seed=2028573587:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2955 on theBenchmark for (2955ds/907Mi)
% 41.28/9.41 % (4112129)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2024872688:i=437:sd=1:aac=none:ss=included_2954 on theBenchmark for (2954ds/437Mi)
% 41.28/9.41 % (4112131)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=323739089:i=5202:ss=axioms:sgt=16_2953 on theBenchmark for (2953ds/5202Mi)
% 41.28/9.41 % (4112129)Refutation not found, incomplete strategy
% 41.28/9.41 % (4112129)------------------------------
% 41.28/9.41 % (4112129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.28/9.41 % (4112129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.28/9.41 % (4112129)CaDiCaL version: 2.1.3
% 41.28/9.41 % (4112129)Termination reason: Refutation not found, incomplete strategy
% 41.28/9.41 % (4112129)Time elapsed: 0.327 s
% 41.28/9.41 % (4112129)Peak memory usage: 169 MB
% 41.28/9.41 % (4112129)Instructions burned: 397 (million)
% 41.28/9.41 % (4112128)Instruction limit reached!
% 41.28/9.41 % (4112128)------------------------------
% 41.28/9.41 % (4112128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.28/9.41 % (4112128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.28/9.41 % (4112128)CaDiCaL version: 2.1.3
% 41.28/9.41 % (4112128)Termination reason: Instruction limit
% 41.28/9.41 % (4112128)Termination phase: Saturation
% 41.28/9.41 % (4112128)Time elapsed: 0.817 s
% 41.28/9.41 % (4112128)Peak memory usage: 175 MB
% 41.28/9.41 % (4112128)Instructions burned: 907 (million)
% 41.28/9.41 % (4112129)------------------------------
% 41.28/9.41 % (4112129)------------------------------
% 41.28/9.41 % (4112139)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=142523392:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2944 on theBenchmark for (2944ds/134Mi)
% 41.28/9.41 % (4112140)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3372030248:st=8:i=592:sd=3:ep=RST:ss=axioms_2944 on theBenchmark for (2944ds/592Mi)
% 41.28/9.41 % (4112139)Instruction limit reached!
% 41.28/9.41 % (4112139)------------------------------
% 41.28/9.41 % (4112139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.28/9.41 % (4112139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.28/9.41 % (4112139)CaDiCaL version: 2.1.3
% 41.28/9.41 % (4112139)Termination reason: Instruction limit
% 41.28/9.41 % (4112139)Termination phase: SInE selection
% 41.28/9.41 % (4112139)Time elapsed: 0.123 s
% 41.28/9.41 % (4112139)Peak memory usage: 165 MB
% 41.28/9.41 % (4112139)Instructions burned: 134 (million)
% 41.28/9.41 % (4112095)Refutation not found, incomplete strategy
% 41.28/9.41 % (4112095)------------------------------
% 41.28/9.41 % (4112095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.28/9.41 % (4112095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.28/9.41 % (4112095)CaDiCaL version: 2.1.3
% 41.28/9.41 % (4112095)Termination reason: Refutation not found, incomplete strategy
% 41.28/9.41 % (4112095)Time elapsed: 2.624 s
% 41.28/9.41 % (4112095)Peak memory usage: 236 MB
% 41.28/9.41 % (4112095)Instructions burned: 2544 (million)
% 41.28/9.41 % (4112145)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1042617598:st=3:i=13193:sd=3:ss=axioms_2940 on theBenchmark for (2940ds/13193Mi)
% 41.28/9.41 % (4112140)Instruction limit reached!
% 41.28/9.41 % (4112140)------------------------------
% 65.94/12.94 % (4112140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.94/12.94 % (4112140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.94/12.94 % (4112140)CaDiCaL version: 2.1.3
% 65.94/12.94 % (4112140)Termination reason: Instruction limit
% 65.94/12.94 % (4112140)Termination phase: Preprocessing 1
% 65.94/12.94 % (4112140)Time elapsed: 0.516 s
% 65.94/12.94 % (4112140)Peak memory usage: 167 MB
% 65.94/12.94 % (4112140)Instructions burned: 592 (million)
% 65.94/12.94 % (4112119)Instruction limit reached!
% 65.94/12.94 % (4112119)------------------------------
% 65.94/12.94 % (4112119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.94/12.94 % (4112119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.94/12.94 % (4112119)CaDiCaL version: 2.1.3
% 65.94/12.94 % (4112119)Termination reason: Instruction limit
% 65.94/12.94 % (4112119)Termination phase: Property scanning
% 65.94/12.94 % (4112119)Time elapsed: 2.168 s
% 65.94/12.94 % (4112119)Peak memory usage: 193 MB
% 65.94/12.94 % (4112119)Instructions burned: 2351 (million)
% 65.94/12.94 % (4112095)------------------------------
% 65.94/12.94 % (4112095)------------------------------
% 65.94/12.94 % (4112147)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=2732253254:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2935 on theBenchmark for (2935ds/125Mi)
% 65.94/12.94 % (4112148)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3050850932:i=134:gtgl=5:slsql=off:gtg=exists_sym_2935 on theBenchmark for (2935ds/134Mi)
% 65.94/12.94 % (4112147)Instruction limit reached!
% 65.94/12.94 % (4112147)------------------------------
% 65.94/12.94 % (4112147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.94/12.94 % (4112147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.94/12.94 % (4112147)CaDiCaL version: 2.1.3
% 65.94/12.94 % (4112147)Termination reason: Instruction limit
% 65.94/12.94 % (4112147)Termination phase: Property scanning
% 65.94/12.94 % (4112147)Time elapsed: 0.125 s
% 65.94/12.94 % (4112147)Peak memory usage: 165 MB
% 65.94/12.94 % (4112147)Instructions burned: 125 (million)
% 65.94/12.94 % (4112148)Instruction limit reached!
% 65.94/12.94 % (4112148)------------------------------
% 65.94/12.94 % (4112148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.94/12.94 % (4112148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.94/12.94 % (4112148)CaDiCaL version: 2.1.3
% 65.94/12.94 % (4112148)Termination reason: Instruction limit
% 65.94/12.94 % (4112148)Termination phase: Property scanning
% 65.94/12.94 % (4112148)Time elapsed: 0.131 s
% 65.94/12.94 % (4112148)Peak memory usage: 165 MB
% 65.94/12.94 % (4112148)Instructions burned: 134 (million)
% 65.94/12.94 % (4112149)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4283778427:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2933 on theBenchmark for (2933ds/141Mi)
% 65.94/12.94 % (4112149)Instruction limit reached!
% 65.94/12.94 % (4112149)------------------------------
% 65.94/12.94 % (4112149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.94/12.94 % (4112149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.94/12.94 % (4112149)CaDiCaL version: 2.1.3
% 65.94/12.94 % (4112149)Termination reason: Instruction limit
% 65.94/12.94 % (4112149)Termination phase: SInE selection
% 65.94/12.94 % (4112149)Time elapsed: 0.123 s
% 65.94/12.94 % (4112149)Peak memory usage: 165 MB
% 65.94/12.94 % (4112149)Instructions burned: 141 (million)
% 65.94/12.94 % (4112094)Refutation not found, incomplete strategy
% 65.94/12.94 % (4112094)------------------------------
% 65.94/12.94 % (4112094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.94/12.94 % (4112094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.94/12.94 % (4112094)CaDiCaL version: 2.1.3
% 65.94/12.94 % (4112094)Termination reason: Refutation not found, incomplete strategy
% 65.94/12.94 % (4112094)Time elapsed: 3.525 s
% 65.94/12.94 % (4112094)Peak memory usage: 308 MB
% 65.94/12.94 % (4112094)Instructions burned: 3296 (million)
% 65.94/12.94 % (4112155)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=1262442976:i=6060:aac=none:ins=25_2931 on theBenchmark for (2931ds/6060Mi)
% 65.94/12.94 % (4112154)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1727781551:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2931 on theBenchmark for (2931ds/431Mi)
% 121.28/20.74 % (4112157)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=355895669:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2929 on theBenchmark for (2929ds/150Mi)
% 121.28/20.74 % (4112157)Instruction limit reached!
% 121.28/20.74 % (4112157)------------------------------
% 121.28/20.74 % (4112157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.28/20.74 % (4112157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.28/20.74 % (4112157)CaDiCaL version: 2.1.3
% 121.28/20.74 % (4112157)Termination reason: Instruction limit
% 121.28/20.74 % (4112157)Termination phase: SInE selection
% 121.28/20.74 % (4112157)Time elapsed: 0.131 s
% 121.28/20.74 % (4112157)Peak memory usage: 165 MB
% 121.28/20.74 % (4112157)Instructions burned: 150 (million)
% 121.28/20.74 % (4112094)------------------------------
% 121.28/20.74 % (4112094)------------------------------
% 121.28/20.74 % (4112154)Refutation not found, incomplete strategy
% 121.28/20.74 % (4112154)------------------------------
% 121.28/20.74 % (4112154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.28/20.74 % (4112154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.28/20.74 % (4112154)CaDiCaL version: 2.1.3
% 121.28/20.74 % (4112154)Termination reason: Refutation not found, incomplete strategy
% 121.28/20.74 % (4112154)Time elapsed: 0.388 s
% 121.28/20.74 % (4112154)Peak memory usage: 170 MB
% 121.28/20.74 % (4112154)Instructions burned: 404 (million)
% 121.28/20.74 % (4112131)Instruction limit reached!
% 121.28/20.74 % (4112131)------------------------------
% 121.28/20.74 % (4112131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.28/20.74 % (4112131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.28/20.74 % (4112131)CaDiCaL version: 2.1.3
% 121.28/20.74 % (4112131)Termination reason: Instruction limit
% 121.28/20.74 % (4112131)Termination phase: Saturation
% 121.28/20.74 % (4112131)Time elapsed: 2.798 s
% 121.28/20.74 % (4112131)Peak memory usage: 312 MB
% 121.28/20.74 % (4112131)Instructions burned: 5202 (million)
% 121.28/20.74 % (4112161)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2522771910:i=14155:bd=all_2925 on theBenchmark for (2925ds/14155Mi)
% 121.28/20.74 % (4112162)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=522862867:i=667:av=off:fsr=off_2924 on theBenchmark for (2924ds/667Mi)
% 121.28/20.74 % (4112154)------------------------------
% 121.28/20.74 % (4112154)------------------------------
% 121.28/20.74 % (4112163)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=3853648450:s2a=on:i=185:s2at=1.8:fdi=4_2922 on theBenchmark for (2922ds/185Mi)
% 121.28/20.74 % (4112163)Instruction limit reached!
% 121.28/20.74 % (4112163)------------------------------
% 121.28/20.74 % (4112163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.28/20.74 % (4112163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.28/20.74 % (4112163)CaDiCaL version: 2.1.3
% 121.28/20.74 % (4112163)Termination reason: Instruction limit
% 121.28/20.74 % (4112163)Termination phase: SInE selection
% 121.28/20.74 % (4112163)Time elapsed: 0.093 s
% 121.28/20.74 % (4112163)Peak memory usage: 164 MB
% 121.28/20.74 % (4112163)Instructions burned: 186 (million)
% 121.28/20.74 % (4112167)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2982526422:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2920 on theBenchmark for (2920ds/193Mi)
% 121.28/20.74 % (4112168)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2327769877:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2919 on theBenchmark for (2919ds/4850Mi)
% 121.28/20.74 % (4112167)Instruction limit reached!
% 121.28/20.74 % (4112167)------------------------------
% 121.28/20.74 % (4112167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.28/20.74 % (4112167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.28/20.74 % (4112167)CaDiCaL version: 2.1.3
% 121.28/20.74 % (4112167)Termination reason: Instruction limit
% 121.28/20.74 % (4112167)Termination phase: SInE selection
% 121.28/20.74 % (4112167)Time elapsed: 0.171 s
% 121.28/20.74 % (4112167)Peak memory usage: 165 MB
% 121.28/20.74 % (4112167)Instructions burned: 194 (million)
% 121.28/20.74 % (4112162)Instruction limit reached!
% 146.10/24.14 % (4112162)------------------------------
% 146.10/24.14 % (4112162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.10/24.14 % (4112162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.10/24.14 % (4112162)CaDiCaL version: 2.1.3
% 146.10/24.14 % (4112162)Termination reason: Instruction limit
% 146.10/24.14 % (4112162)Termination phase: NewCNF
% 146.10/24.14 % (4112162)Time elapsed: 0.782 s
% 146.10/24.14 % (4112162)Peak memory usage: 184 MB
% 146.10/24.14 % (4112162)Instructions burned: 668 (million)
% 146.10/24.14 % (4112171)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=217031592:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 146.10/24.14 % (4112172)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=911741419:i=319:kws=precedence:fsr=off_2914 on theBenchmark for (2914ds/319Mi)
% 146.10/24.14 % (4112172)Instruction limit reached!
% 146.10/24.14 % (4112172)------------------------------
% 146.10/24.14 % (4112172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.10/24.14 % (4112172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.10/24.14 % (4112172)CaDiCaL version: 2.1.3
% 146.10/24.14 % (4112172)Termination reason: Instruction limit
% 146.10/24.14 % (4112172)Termination phase: Preprocessing 2
% 146.10/24.14 % (4112172)Time elapsed: 0.396 s
% 146.10/24.14 % (4112172)Peak memory usage: 170 MB
% 146.10/24.14 % (4112172)Instructions burned: 319 (million)
% 146.10/24.14 % (4112181)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=463523610:i=2064:ep=RST_2908 on theBenchmark for (2908ds/2064Mi)
% 146.10/24.14 % (4112168)Instruction limit reached!
% 146.10/24.14 % (4112168)------------------------------
% 146.10/24.14 % (4112168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.10/24.14 % (4112168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.10/24.14 % (4112168)CaDiCaL version: 2.1.3
% 146.10/24.14 % (4112168)Termination reason: Instruction limit
% 146.10/24.14 % (4112168)Termination phase: Saturation
% 146.10/24.14 % (4112168)Time elapsed: 2.489 s
% 146.10/24.14 % (4112168)Peak memory usage: 214 MB
% 146.10/24.14 % (4112168)Instructions burned: 4850 (million)
% 146.10/24.14 % (4112191)dis-1011_128_sil=32000:random_seed=2652523392:i=3706:ep=RST:av=off_2892 on theBenchmark for (2892ds/3706Mi)
% 146.10/24.14 % (4112181)Instruction limit reached!
% 146.10/24.14 % (4112181)------------------------------
% 146.10/24.14 % (4112181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.10/24.14 % (4112181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.10/24.14 % (4112181)CaDiCaL version: 2.1.3
% 146.10/24.14 % (4112181)Termination reason: Instruction limit
% 146.10/24.14 % (4112181)Termination phase: Property scanning
% 146.10/24.14 % (4112181)Time elapsed: 1.655 s
% 146.10/24.14 % (4112181)Peak memory usage: 194 MB
% 146.10/24.14 % (4112181)Instructions burned: 2066 (million)
% 146.10/24.14 % (4112193)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1987072092:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2889 on theBenchmark for (2889ds/757Mi)
% 146.10/24.14 % (4112171)Refutation not found, incomplete strategy
% 146.10/24.14 % (4112171)------------------------------
% 146.10/24.14 % (4112171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.10/24.14 % (4112171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.10/24.14 % (4112171)CaDiCaL version: 2.1.3
% 146.10/24.14 % (4112171)Termination reason: Refutation not found, incomplete strategy
% 146.10/24.14 % (4112171)Time elapsed: 2.687 s
% 146.10/24.14 % (4112171)Peak memory usage: 303 MB
% 146.10/24.14 % (4112171)Instructions burned: 2558 (million)
% 146.10/24.14 % (4112193)Instruction limit reached!
% 146.10/24.14 % (4112193)------------------------------
% 146.10/24.14 % (4112193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.10/24.14 % (4112193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.10/24.14 % (4112193)CaDiCaL version: 2.1.3
% 146.10/24.14 % (4112193)Termination reason: Instruction limit
% 146.10/24.14 % (4112193)Termination phase: Saturation
% 146.10/24.14 % (4112193)Time elapsed: 0.463 s
% 146.10/24.14 % (4112193)Peak memory usage: 172 MB
% 146.10/24.14 % (4112193)Instructions burned: 757 (million)
% 146.10/24.14 % (4112171)------------------------------
% 146.10/24.14 % (4112171)------------------------------
% 146.10/24.14 % (4112199)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=887955728:i=13913:ss=axioms:sgt=8_2881 on theBenchmark for (2881ds/13913Mi)
% 165.12/26.96 % (4112200)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=512539622:i=9925:aac=none_2880 on theBenchmark for (2880ds/9925Mi)
% 165.12/26.96 % (4112191)Instruction limit reached!
% 165.12/26.96 % (4112191)------------------------------
% 165.12/26.96 % (4112191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.12/26.96 % (4112191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.12/26.96 % (4112191)CaDiCaL version: 2.1.3
% 165.12/26.96 % (4112191)Termination reason: Instruction limit
% 165.12/26.96 % (4112191)Termination phase: Saturation
% 165.12/26.96 % (4112191)Time elapsed: 3.166 s
% 165.12/26.96 % (4112191)Peak memory usage: 229 MB
% 165.12/26.96 % (4112191)Instructions burned: 3707 (million)
% 165.12/26.96 % (4112155)Instruction limit reached!
% 165.12/26.96 % (4112155)------------------------------
% 165.12/26.96 % (4112155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.12/26.96 % (4112155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.12/26.96 % (4112155)CaDiCaL version: 2.1.3
% 165.12/26.96 % (4112155)Termination reason: Instruction limit
% 165.12/26.96 % (4112155)Termination phase: Saturation
% 165.12/26.96 % (4112155)Time elapsed: 7.374 s
% 165.12/26.96 % (4112155)Peak memory usage: 614 MB
% 165.12/26.96 % (4112155)Instructions burned: 6062 (million)
% 165.12/26.96 % (4112207)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=85274479:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2857 on theBenchmark for (2857ds/2479Mi)
% 165.12/26.96 % (4112211)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3746142662:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2854 on theBenchmark for (2854ds/440Mi)
% 165.12/26.96 % (4112211)Instruction limit reached!
% 165.12/26.96 % (4112211)------------------------------
% 165.12/26.96 % (4112211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.12/26.96 % (4112211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.12/26.96 % (4112211)CaDiCaL version: 2.1.3
% 165.12/26.96 % (4112211)Termination reason: Instruction limit
% 165.12/26.96 % (4112211)Termination phase: Property scanning
% 165.12/26.96 % (4112211)Time elapsed: 0.349 s
% 165.12/26.96 % (4112211)Peak memory usage: 165 MB
% 165.12/26.96 % (4112211)Instructions burned: 440 (million)
% 165.12/26.96 % (4112215)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3087769350:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2847 on theBenchmark for (2847ds/11145Mi)
% 165.12/26.96 % (4112207)Instruction limit reached!
% 165.12/26.96 % (4112207)------------------------------
% 165.12/26.96 % (4112207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.12/26.96 % (4112207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.12/26.96 % (4112207)CaDiCaL version: 2.1.3
% 165.12/26.96 % (4112207)Termination reason: Instruction limit
% 165.12/26.96 % (4112207)Termination phase: Saturation
% 165.12/26.96 % (4112207)Time elapsed: 2.191 s
% 165.12/26.96 % (4112207)Peak memory usage: 178 MB
% 165.12/26.96 % (4112207)Instructions burned: 2481 (million)
% 165.12/26.96 % (4112219)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=1545743550:cts=off:i=3034:av=off:er=known:fsd=on_2832 on theBenchmark for (2832ds/3034Mi)
% 165.12/26.96 % (4112199)Instruction limit reached!
% 165.12/26.96 % (4112199)------------------------------
% 165.12/26.96 % (4112199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.12/26.96 % (4112199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.12/26.96 % (4112199)CaDiCaL version: 2.1.3
% 165.12/26.96 % (4112199)Termination reason: Instruction limit
% 165.12/26.96 % (4112199)Termination phase: Saturation
% 165.12/26.96 % (4112199)Time elapsed: 7.289 s
% 165.12/26.96 % (4112199)Peak memory usage: 291 MB
% 165.12/26.96 % (4112199)Instructions burned: 13914 (million)
% 165.12/26.96 % (4112229)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=175252468:st=2:s2a=on:i=524:s2at=2:ss=axioms_2806 on theBenchmark for (2806ds/524Mi)
% 165.12/26.96 % (4112219)Instruction limit reached!
% 165.12/26.96 % (4112219)------------------------------
% 165.12/26.96 % (4112219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.12/26.96 % (4112219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.12/26.96 % (4112219)CaDiCaL version: 2.1.3
% 190.82/30.52 % (4112219)Termination reason: Instruction limit
% 190.82/30.52 % (4112219)Termination phase: Saturation
% 190.82/30.52 % (4112219)Time elapsed: 2.847 s
% 190.82/30.52 % (4112219)Peak memory usage: 224 MB
% 190.82/30.52 % (4112219)Instructions burned: 3034 (million)
% 190.82/30.52 % (4112145)Instruction limit reached!
% 190.82/30.52 % (4112145)------------------------------
% 190.82/30.52 % (4112145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.82/30.52 % (4112145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.82/30.52 % (4112145)CaDiCaL version: 2.1.3
% 190.82/30.52 % (4112145)Termination reason: Instruction limit
% 190.82/30.52 % (4112145)Termination phase: Saturation
% 190.82/30.52 % (4112145)Time elapsed: 13.686 s
% 190.82/30.52 % (4112145)Peak memory usage: 309 MB
% 190.82/30.52 % (4112145)Instructions burned: 13194 (million)
% 190.82/30.52 % (4112229)Instruction limit reached!
% 190.82/30.52 % (4112229)------------------------------
% 190.82/30.52 % (4112229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.82/30.52 % (4112229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.82/30.52 % (4112229)CaDiCaL version: 2.1.3
% 190.82/30.52 % (4112229)Termination reason: Instruction limit
% 190.82/30.52 % (4112229)Termination phase: SInE selection
% 190.82/30.52 % (4112229)Time elapsed: 0.295 s
% 190.82/30.52 % (4112229)Peak memory usage: 165 MB
% 190.82/30.52 % (4112229)Instructions burned: 525 (million)
% 190.82/30.52 % (4112232)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3741635706:i=14123:bd=preordered:ins=4_2800 on theBenchmark for (2800ds/14123Mi)
% 190.82/30.52 % (4112231)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2084622970:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2800 on theBenchmark for (2800ds/1016Mi)
% 190.82/30.52 % (4112233)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2445842113:i=5781:kws=precedence:bd=all:rawr=on_2800 on theBenchmark for (2800ds/5781Mi)
% 190.82/30.52 % (4112231)Refutation not found, incomplete strategy
% 190.82/30.52 % (4112231)------------------------------
% 190.82/30.52 % (4112231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.82/30.52 % (4112231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.82/30.52 % (4112231)CaDiCaL version: 2.1.3
% 190.82/30.52 % (4112231)Termination reason: Refutation not found, incomplete strategy
% 190.82/30.52 % (4112231)Time elapsed: 0.406 s
% 190.82/30.52 % (4112231)Peak memory usage: 170 MB
% 190.82/30.52 % (4112231)Instructions burned: 450 (million)
% 190.82/30.52 % (4112231)------------------------------
% 190.82/30.52 % (4112231)------------------------------
% 190.82/30.52 % (4112237)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=3811983486:i=2448:gtgl=5:bd=preordered:gtg=all_2789 on theBenchmark for (2789ds/2448Mi)
% 190.82/30.52 % (4112161)Instruction limit reached!
% 190.82/30.52 % (4112161)------------------------------
% 190.82/30.52 % (4112161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.82/30.52 % (4112161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.82/30.52 % (4112161)CaDiCaL version: 2.1.3
% 190.82/30.52 % (4112161)Termination reason: Instruction limit
% 190.82/30.52 % (4112161)Termination phase: Saturation
% 190.82/30.52 % (4112161)Time elapsed: 13.739 s
% 190.82/30.52 % (4112161)Peak memory usage: 575 MB
% 190.82/30.52 % (4112161)Instructions burned: 14156 (million)
% 190.82/30.52 % (4112239)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2813213897:i=3223:kws=precedence:fgj=on:av=off_2784 on theBenchmark for (2784ds/3223Mi)
% 190.82/30.52 % (4112200)Instruction limit reached!
% 190.82/30.52 % (4112200)------------------------------
% 190.82/30.52 % (4112200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.82/30.52 % (4112200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.82/30.52 % (4112200)CaDiCaL version: 2.1.3
% 190.82/30.52 % (4112200)Termination reason: Instruction limit
% 190.82/30.52 % (4112200)Termination phase: Saturation
% 190.82/30.52 % (4112200)Time elapsed: 10.740 s
% 190.82/30.52 % (4112200)Peak memory usage: 691 MB
% 190.82/30.52 % (4112200)Instructions burned: 9925 (million)
% 190.82/30.52 % (4112233)Instruction limit reached!
% 190.82/30.52 % (4112233)------------------------------
% 190.82/30.52 % (4112233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.82/30.52 % (4112233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112233)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112233)Termination reason: Instruction limit
% 195.97/34.71 % (4112233)Termination phase: Saturation
% 195.97/34.71 % (4112233)Time elapsed: 3.072 s
% 195.97/34.71 % (4112233)Peak memory usage: 277 MB
% 195.97/34.71 % (4112233)Instructions burned: 5782 (million)
% 195.97/34.71 % (4112241)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4228968499:st=5.6:i=2033:sd=3:ss=axioms_2768 on theBenchmark for (2768ds/2033Mi)
% 195.97/34.71 % (4112242)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4182723612:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2766 on theBenchmark for (2766ds/2055Mi)
% 195.97/34.71 % (4112237)Instruction limit reached!
% 195.97/34.71 % (4112237)------------------------------
% 195.97/34.71 % (4112237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112237)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112237)Termination reason: Instruction limit
% 195.97/34.71 % (4112237)Termination phase: Naming
% 195.97/34.71 % (4112237)Time elapsed: 2.200 s
% 195.97/34.71 % (4112237)Peak memory usage: 174 MB
% 195.97/34.71 % (4112237)Instructions burned: 2448 (million)
% 195.97/34.71 % (4112245)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=1994586884:i=21611:sd=3:ss=axioms_2764 on theBenchmark for (2764ds/21611Mi)
% 195.97/34.71 % (4112242)Instruction limit reached!
% 195.97/34.71 % (4112242)------------------------------
% 195.97/34.71 % (4112242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112242)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112242)Termination reason: Instruction limit
% 195.97/34.71 % (4112242)Termination phase: Saturation
% 195.97/34.71 % (4112242)Time elapsed: 1.088 s
% 195.97/34.71 % (4112242)Peak memory usage: 197 MB
% 195.97/34.71 % (4112242)Instructions burned: 2056 (million)
% 195.97/34.71 % (4112247)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1028164633:i=4835:sd=13:ss=axioms:sgt=23_2753 on theBenchmark for (2753ds/4835Mi)
% 195.97/34.71 % (4112239)Instruction limit reached!
% 195.97/34.71 % (4112239)------------------------------
% 195.97/34.71 % (4112239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112239)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112239)Termination reason: Instruction limit
% 195.97/34.71 % (4112239)Termination phase: Saturation
% 195.97/34.71 % (4112239)Time elapsed: 3.147 s
% 195.97/34.71 % (4112239)Peak memory usage: 256 MB
% 195.97/34.71 % (4112239)Instructions burned: 3223 (million)
% 195.97/34.71 % (4112251)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=637661002:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2749 on theBenchmark for (2749ds/797Mi)
% 195.97/34.71 % (4112241)Instruction limit reached!
% 195.97/34.71 % (4112241)------------------------------
% 195.97/34.71 % (4112241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112241)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112241)Termination reason: Instruction limit
% 195.97/34.71 % (4112241)Termination phase: Saturation
% 195.97/34.71 % (4112241)Time elapsed: 2.046 s
% 195.97/34.71 % (4112241)Peak memory usage: 217 MB
% 195.97/34.71 % (4112241)Instructions burned: 2033 (million)
% 195.97/34.71 % (4112253)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=296925764:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2745 on theBenchmark for (2745ds/2326Mi)
% 195.97/34.71 % (4112251)Instruction limit reached!
% 195.97/34.71 % (4112251)------------------------------
% 195.97/34.71 % (4112251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112251)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112251)Termination reason: Instruction limit
% 195.97/34.71 % (4112251)Termination phase: SInE selection
% 195.97/34.71 % (4112251)Time elapsed: 0.787 s
% 195.97/34.71 % (4112251)Peak memory usage: 168 MB
% 195.97/34.71 % (4112251)Instructions burned: 797 (million)
% 195.97/34.71 % (4112255)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1118019368:i=6038:nm=6_2738 on theBenchmark for (2738ds/6038Mi)
% 195.97/34.71 % (4112247)Instruction limit reached!
% 195.97/34.71 % (4112247)------------------------------
% 195.97/34.71 % (4112247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112247)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112247)Termination reason: Instruction limit
% 195.97/34.71 % (4112247)Termination phase: Saturation
% 195.97/34.71 % (4112247)Time elapsed: 2.480 s
% 195.97/34.71 % (4112247)Peak memory usage: 226 MB
% 195.97/34.71 % (4112247)Instructions burned: 4836 (million)
% 195.97/34.71 % (4112259)lrs+10_1_sil=32000:sp=occurrence:random_seed=2349710773:st=2:i=33334:sd=3:ss=included:sgt=32_2726 on theBenchmark for (2726ds/33334Mi)
% 195.97/34.71 % (4112253)Instruction limit reached!
% 195.97/34.71 % (4112253)------------------------------
% 195.97/34.71 % (4112253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112253)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112253)Termination reason: Instruction limit
% 195.97/34.71 % (4112253)Termination phase: Saturation
% 195.97/34.71 % (4112253)Time elapsed: 1.850 s
% 195.97/34.71 % (4112253)Peak memory usage: 206 MB
% 195.97/34.71 % (4112253)Instructions burned: 2327 (million)
% 195.97/34.71 % (4112261)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2177299108:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2724 on theBenchmark for (2724ds/1008Mi)
% 195.97/34.71 % (4112215)Instruction limit reached!
% 195.97/34.71 % (4112215)------------------------------
% 195.97/34.71 % (4112215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112215)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112215)Termination reason: Instruction limit
% 195.97/34.71 % (4112215)Termination phase: Saturation
% 195.97/34.71 % (4112215)Time elapsed: 12.306 s
% 195.97/34.71 % (4112215)Peak memory usage: 312 MB
% 195.97/34.71 % (4112215)Instructions burned: 11145 (million)
% 195.97/34.71 % (4112309)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2193892309:i=8327:s2at=5:bd=preordered_2722 on theBenchmark for (2722ds/8327Mi)
% 195.97/34.71 % (4112261)Instruction limit reached!
% 195.97/34.71 % (4112261)------------------------------
% 195.97/34.71 % (4112261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112261)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112261)Termination reason: Instruction limit
% 195.97/34.71 % (4112261)Termination phase: SInE selection
% 195.97/34.71 % (4112261)Time elapsed: 0.512 s
% 195.97/34.71 % (4112261)Peak memory usage: 165 MB
% 195.97/34.71 % (4112261)Instructions burned: 1010 (million)
% 195.97/34.71 % (4112418)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2507117859:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2717 on theBenchmark for (2717ds/1083Mi)
% 195.97/34.71 % (4112418)Instruction limit reached!
% 195.97/34.71 % (4112418)------------------------------
% 195.97/34.71 % (4112418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112418)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112418)Termination reason: Instruction limit
% 195.97/34.71 % (4112418)Termination phase: Preprocessing 3
% 195.97/34.71 % (4112418)Time elapsed: 0.733 s
% 195.97/34.71 % (4112418)Peak memory usage: 174 MB
% 195.97/34.71 % (4112418)Instructions burned: 1084 (million)
% 195.97/34.71 % (4112420)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2588410970:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2708 on theBenchmark for (2708ds/1084Mi)
% 195.97/34.71 % (4112420)Refutation not found, incomplete strategy
% 195.97/34.71 % (4112420)------------------------------
% 195.97/34.71 % (4112420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112420)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112420)Termination reason: Refutation not found, incomplete strategy
% 195.97/34.71 % (4112420)Time elapsed: 0.281 s
% 195.97/34.71 % (4112420)Peak memory usage: 169 MB
% 195.97/34.71 % (4112420)Instructions burned: 446 (million)
% 195.97/34.71 % (4112420)------------------------------
% 195.97/34.71 % (4112420)------------------------------
% 195.97/34.71 % (4112422)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3083772745:i=6995:s2at=5:gtg=all_2700 on theBenchmark for (2700ds/6995Mi)
% 195.97/34.71 % (4112255)Instruction limit reached!
% 195.97/34.71 % (4112255)------------------------------
% 195.97/34.71 % (4112255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112255)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112255)Termination reason: Instruction limit
% 195.97/34.71 % (4112255)Termination phase: Saturation
% 195.97/34.71 % (4112255)Time elapsed: 5.001 s
% 195.97/34.71 % (4112255)Peak memory usage: 748 MB
% 195.97/34.71 % (4112255)Instructions burned: 6041 (million)
% 195.97/34.71 % (4112424)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1782404781:st=2:i=6225:sd=15:ss=axioms_2684 on theBenchmark for (2684ds/6225Mi)
% 195.97/34.71 % (4112232)Instruction limit reached!
% 195.97/34.71 % (4112232)------------------------------
% 195.97/34.71 % (4112232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112232)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112232)Termination reason: Instruction limit
% 195.97/34.71 % (4112232)Termination phase: Saturation
% 195.97/34.71 % (4112232)Time elapsed: 11.884 s
% 195.97/34.71 % (4112232)Peak memory usage: 661 MB
% 195.97/34.71 % (4112232)Instructions burned: 14124 (million)
% 195.97/34.71 % (4112426)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=256607884:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2678 on theBenchmark for (2678ds/3372Mi)
% 195.97/34.71 % (4112093)First to succeed.
% 195.97/34.71 % (4112093)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4112076"
% 195.97/34.71 % (4112309)Instruction limit reached!
% 195.97/34.71 % (4112309)------------------------------
% 195.97/34.71 % (4112309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.97/34.71 % (4112309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.97/34.71 % (4112309)CaDiCaL version: 2.1.3
% 195.97/34.71 % (4112309)Termination reason: Instruction limit
% 195.97/34.71 % (4112309)Termination phase: Saturation
% 195.97/34.71 % (4112309)Time elapsed: 5.635 s
% 195.97/34.71 % (4112309)Peak memory usage: 538 MB
% 195.97/34.71 % (4112309)Instructions burned: 8327 (million)
% 195.97/34.71 % (4112093)Refutation found. Thanks to Tanya!
% 195.97/34.71 % SZS status ContradictoryAxioms for theBenchmark
% 195.97/34.71 % SZS output start Proof for theBenchmark
% See solution above
% 221.14/34.85 % (4112093)------------------------------
% 221.14/34.85 % (4112093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 221.14/34.85 % (4112093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.14/34.85 % (4112093)CaDiCaL version: 2.1.3
% 221.14/34.85 % (4112093)Termination reason: Refutation
% 221.14/34.85 % (4112093)Time elapsed: 29.904 s
% 221.14/34.85 % (4112093)Peak memory usage: 1097 MB
% 221.14/34.85 % (4112093)Instructions burned: 34192 (million)
% 221.14/34.85 % (4112093)------------------------------
% 221.14/34.85 % (4112093)------------------------------
% 221.14/34.85 % (4112076)Success in time 33.846 s
% 221.14/34.85 % Vampire exiting
%------------------------------------------------------------------------------