%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW597_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 01:30:54 PM UTC 2026
% Result : Theorem 25.98s 4.69s
% Output : Refutation 27.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 16
% Syntax : Number of formulae : 71 ( 16 unt; 0 typ; 10 def)
% Number of atoms : 240 ( 45 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 249 ( 80 ~; 56 |; 69 &)
% ( 15 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 247 ( 85 atm; 32 fun; 62 num; 68 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 21 usr; 11 prp; 0-7 aty)
% Number of functors : 60 ( 57 usr; 25 con; 0-7 aty)
% Number of variables : 120 ( 106 !; 14 ?; 120 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
color: $tType ).
tff(type_def_10,type,
array_color: $tType ).
tff(type_def_11,type,
map_int_color: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
occ: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_32,type,
color1: ty ).
tff(func_def_33,type,
blue: color ).
tff(func_def_34,type,
white: color ).
tff(func_def_35,type,
red: color ).
tff(func_def_36,type,
match_color: ( ty * color * uni * uni * uni ) > uni ).
tff(func_def_37,type,
t2tb1: array_color > uni ).
tff(func_def_38,type,
tb2t1: uni > array_color ).
tff(func_def_39,type,
t2tb2: color > uni ).
tff(func_def_40,type,
tb2t2: uni > color ).
tff(func_def_41,type,
t2tb3: map_int_color > uni ).
tff(func_def_42,type,
tb2t3: uni > map_int_color ).
tff(func_def_44,type,
sK0: ( uni * $int * $int * ty * uni ) > $int ).
tff(func_def_45,type,
sK1: ( ty * $int * uni * uni * $int * $int * $int ) > $int ).
tff(func_def_46,type,
sK2: ( ty * uni * $int * uni * $int ) > $int ).
tff(func_def_47,type,
sK3: ( $int * $int * uni * uni * ty ) > uni ).
tff(func_def_48,type,
sK4: map_int_color ).
tff(func_def_49,type,
sK5: $int ).
tff(func_def_50,type,
sK6: $int ).
tff(func_def_51,type,
sK7: map_int_color ).
tff(func_def_52,type,
sK8: $int ).
tff(func_def_53,type,
sK9: $int ).
tff(func_def_54,type,
sK10: $int ).
tff(func_def_55,type,
sK11: ( uni * $int * uni * ty * $int ) > $int ).
tff(func_def_56,type,
sK12: ( uni * ty * $int * uni * $int ) > $int ).
tff(func_def_57,type,
sK13: ( color * array_color * $int * $int ) > $int ).
tff(func_def_58,type,
sK14: ( $int * $int * uni * uni * ty * $int ) > $int ).
tff(func_def_61,type,
'$inst16': $int ).
tff(func_def_62,type,
'$inst17': $int ).
tff(func_def_63,type,
'$inst18': $int ).
tff(func_def_65,type,
'$inst19': $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
exchange: ( ty * uni * uni * $int * $int * $int * $int ) > $o ).
tff(pred_def_5,type,
exchange1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_6,type,
permut: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_7,type,
map_eq_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_8,type,
array_eq_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_9,type,
array_eq: ( ty * uni * uni ) > $o ).
tff(pred_def_10,type,
permut1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_11,type,
permut_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_12,type,
permut_all: ( ty * uni * uni ) > $o ).
tff(pred_def_13,type,
monochrome: ( array_color * $int * $int * color ) > $o ).
tff(f22,axiom,
! [X1: $int,X2: uni,X0: ty] :
( sort(map(int,X0),X2)
=> ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',elts_def) ).
tff(f28,axiom,
! [X1: uni,X2: $int,X0: ty] : ( get1(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def) ).
tff(f67,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f71,axiom,
! [X3: color,X0: array_color,X2: $int,X1: $int] :
( ! [X4: $int] :
( ( $lesseq(X1,X4)
& $less(X4,X2) )
=> ( tb2t2(get1(color1,t2tb1(X0),X4)) = X3 ) )
<=> monochrome(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monochrome_def) ).
tff(f72,axiom,
! [X0: map_int_color] : sort(map(int,color1),t2tb3(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort3) ).
tff(f75,conjecture,
! [X1: map_int_color,X0: $int] :
( $lesseq(0,X0)
=> ! [X4: $int,X2: $int,X5: map_int_color,X3: $int] :
( ( monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),0,X4,blue)
& monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X4,X3,white)
& $lesseq(X2,X0)
& $lesseq(X3,X2)
& $lesseq(X4,X3)
& permut_all(color1,mk_array(color1,X0,t2tb3(X1)),mk_array(color1,X0,t2tb3(X5)))
& monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X2,X0,red)
& $lesseq(0,X4) )
=> ( $less(X3,X2)
=> ( ( $lesseq(0,X0)
& $less(X3,X0)
& $lesseq(0,X3) )
=> ( ( tb2t2(get(color1,int,t2tb3(X5),t2tb(X3))) = white )
=> ! [X6: $int] :
( ( X6 = $sum(X3,1) )
=> monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X4,X6,white) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_dutch_flag) ).
tff(f76,negated_conjecture,
~ ! [X1: map_int_color,X0: $int] :
( $lesseq(0,X0)
=> ! [X4: $int,X2: $int,X5: map_int_color,X3: $int] :
( ( monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),0,X4,blue)
& monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X4,X3,white)
& $lesseq(X2,X0)
& $lesseq(X3,X2)
& $lesseq(X4,X3)
& permut_all(color1,mk_array(color1,X0,t2tb3(X1)),mk_array(color1,X0,t2tb3(X5)))
& monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X2,X0,red)
& $lesseq(0,X4) )
=> ( $less(X3,X2)
=> ( ( $lesseq(0,X0)
& $less(X3,X0)
& $lesseq(0,X3) )
=> ( ( tb2t2(get(color1,int,t2tb3(X5),t2tb(X3))) = white )
=> ! [X6: $int] :
( ( X6 = $sum(X3,1) )
=> monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X4,X6,white) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f75]) ).
tff(f77,plain,
! [X3: color,X0: array_color,X2: $int,X1: $int] :
( ! [X4: $int] :
( ( ~ $less(X4,X1)
& $less(X4,X2) )
=> ( tb2t2(get1(color1,t2tb1(X0),X4)) = X3 ) )
<=> monochrome(X0,X1,X2,X3) ),
inference(theory_normalization,[],[f71]) ).
tff(f96,plain,
~ ! [X1: map_int_color,X0: $int] :
( ~ $less(X0,0)
=> ! [X4: $int,X2: $int,X5: map_int_color,X3: $int] :
( ( monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),0,X4,blue)
& monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X4,X3,white)
& ~ $less(X0,X2)
& ~ $less(X2,X3)
& ~ $less(X3,X4)
& permut_all(color1,mk_array(color1,X0,t2tb3(X1)),mk_array(color1,X0,t2tb3(X5)))
& monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X2,X0,red)
& ~ $less(X4,0) )
=> ( $less(X3,X2)
=> ( ( ~ $less(X0,0)
& $less(X3,X0)
& ~ $less(X3,0) )
=> ( ( tb2t2(get(color1,int,t2tb3(X5),t2tb(X3))) = white )
=> ! [X6: $int] :
( ( X6 = $sum(X3,1) )
=> monochrome(tb2t1(mk_array(color1,X0,t2tb3(X5))),X4,X6,white) ) ) ) ) ) ),
inference(theory_normalization,[],[f76]) ).
tff(f117,plain,
! [X1: array_color,X0: color,X3: $int,X2: $int] :
( monochrome(X1,X3,X2,X0)
<=> ! [X4: $int] :
( ( ~ $less(X4,X3)
& $less(X4,X2) )
=> ( tb2t2(get1(color1,t2tb1(X1),X4)) = X0 ) ) ),
inference(rectify,[],[f77]) ).
tff(f127,plain,
! [X2: ty,X0: $int,X1: uni] :
( sort(map(int,X2),X1)
=> ( elts(X2,mk_array(X2,X0,X1)) = X1 ) ),
inference(rectify,[],[f22]) ).
tff(f129,plain,
! [X1: $int,X0: uni,X2: ty] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get1(X2,X0,X1) ),
inference(rectify,[],[f28]) ).
tff(f165,plain,
~ ! [X1: $int,X0: map_int_color] :
( ~ $less(X1,0)
=> ! [X2: $int,X3: $int,X5: $int,X4: map_int_color] :
( ( ~ $less(X1,X3)
& ~ $less(X3,X5)
& ~ $less(X2,0)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X2,X5,white)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),0,X2,blue)
& ~ $less(X5,X2)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X3,X1,red)
& permut_all(color1,mk_array(color1,X1,t2tb3(X0)),mk_array(color1,X1,t2tb3(X4))) )
=> ( $less(X5,X3)
=> ( ( ~ $less(X5,0)
& ~ $less(X1,0)
& $less(X5,X1) )
=> ( ( white = tb2t2(get(color1,int,t2tb3(X4),t2tb(X5))) )
=> ! [X6: $int] :
( ( $sum(X5,1) = X6 )
=> monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X2,X6,white) ) ) ) ) ) ),
inference(rectify,[],[f96]) ).
tff(f170,plain,
! [X1: array_color,X0: color,X3: $int,X2: $int] :
( monochrome(X1,X3,X2,X0)
<=> ! [X4: $int] :
( ( tb2t2(get1(color1,t2tb1(X1),X4)) = X0 )
| $less(X4,X3)
| ~ $less(X4,X2) ) ),
inference(ennf_transformation,[],[f117]) ).
tff(f171,plain,
! [X3: $int,X0: color,X1: array_color,X2: $int] :
( ! [X4: $int] :
( ~ $less(X4,X2)
| ( tb2t2(get1(color1,t2tb1(X1),X4)) = X0 )
| $less(X4,X3) )
<=> monochrome(X1,X3,X2,X0) ),
inference(flattening,[],[f170]) ).
tff(f186,plain,
! [X1: uni,X0: $int,X2: ty] :
( ~ sort(map(int,X2),X1)
| ( elts(X2,mk_array(X2,X0,X1)) = X1 ) ),
inference(ennf_transformation,[],[f127]) ).
tff(f196,plain,
? [X1: $int,X0: map_int_color] :
( ? [X2: $int,X3: $int,X5: $int,X4: map_int_color] :
( ? [X6: $int] :
( ~ monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X2,X6,white)
& ( $sum(X5,1) = X6 ) )
& ( white = tb2t2(get(color1,int,t2tb3(X4),t2tb(X5))) )
& ~ $less(X5,0)
& ~ $less(X1,0)
& $less(X5,X1)
& $less(X5,X3)
& ~ $less(X1,X3)
& ~ $less(X3,X5)
& ~ $less(X2,0)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X2,X5,white)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),0,X2,blue)
& ~ $less(X5,X2)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X3,X1,red)
& permut_all(color1,mk_array(color1,X1,t2tb3(X0)),mk_array(color1,X1,t2tb3(X4))) )
& ~ $less(X1,0) ),
inference(ennf_transformation,[],[f165]) ).
tff(f197,plain,
? [X0: map_int_color,X1: $int] :
( ~ $less(X1,0)
& ? [X2: $int,X4: map_int_color,X3: $int,X5: $int] :
( ~ $less(X5,0)
& ~ $less(X1,X3)
& ~ $less(X2,0)
& ~ $less(X3,X5)
& ~ $less(X5,X2)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X3,X1,red)
& $less(X5,X3)
& $less(X5,X1)
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X2,X5,white)
& ~ $less(X1,0)
& permut_all(color1,mk_array(color1,X1,t2tb3(X0)),mk_array(color1,X1,t2tb3(X4)))
& monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),0,X2,blue)
& ( white = tb2t2(get(color1,int,t2tb3(X4),t2tb(X5))) )
& ? [X6: $int] :
( ~ monochrome(tb2t1(mk_array(color1,X1,t2tb3(X4))),X2,X6,white)
& ( $sum(X5,1) = X6 ) ) ) ),
inference(flattening,[],[f196]) ).
tff(f237,plain,
! [X0: map_int_color] : sort(map(int,color1),t2tb3(X0)),
inference(cnf_transformation,[],[f72]) ).
tff(f289,plain,
sK10 = $sum(sK9,1),
inference(cnf_transformation,[],[f197]) ).
tff(f290,plain,
~ monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,sK10,white),
inference(cnf_transformation,[],[f197]) ).
tff(f291,plain,
white = tb2t2(get(color1,int,t2tb3(sK7),t2tb(sK9))),
inference(cnf_transformation,[],[f197]) ).
tff(f295,plain,
monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,sK9,white),
inference(cnf_transformation,[],[f197]) ).
tff(f331,plain,
! [X2: ty,X0: $int,X1: uni] :
( ( elts(X2,mk_array(X2,X0,X1)) = X1 )
| ~ sort(map(int,X2),X1) ),
inference(cnf_transformation,[],[f186]) ).
tff(f334,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f67]) ).
tff(f341,plain,
! [X2: $int,X3: $int,X0: color,X1: array_color] :
( monochrome(X1,X3,X2,X0)
| ~ $less(sK13(X0,X1,X2,X3),X3) ),
inference(cnf_transformation,[],[f171]) ).
tff(f342,plain,
! [X2: $int,X3: $int,X0: color,X1: array_color] :
( monochrome(X1,X3,X2,X0)
| ( tb2t2(get1(color1,t2tb1(X1),sK13(X0,X1,X2,X3))) != X0 ) ),
inference(cnf_transformation,[],[f171]) ).
tff(f343,plain,
! [X2: $int,X3: $int,X0: color,X1: array_color] :
( monochrome(X1,X3,X2,X0)
| $less(sK13(X0,X1,X2,X3),X2) ),
inference(cnf_transformation,[],[f171]) ).
tff(f344,plain,
! [X2: $int,X3: $int,X0: color,X1: array_color,X4: $int] :
( ~ monochrome(X1,X3,X2,X0)
| $less(X4,X3)
| ( tb2t2(get1(color1,t2tb1(X1),X4)) = X0 )
| ~ $less(X4,X2) ),
inference(cnf_transformation,[],[f171]) ).
tff(f347,plain,
! [X2: ty,X0: uni,X1: $int] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get1(X2,X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
tff(f354,plain,
! [X2: $int,X3: $int,X0: color,X1: array_color,X4: $int] :
( ~ monochrome(X1,X3,X2,X0)
| $less(X4,X3)
| ~ $less(X4,X2)
| ( tb2t2(get(color1,int,elts(color1,t2tb1(X1)),t2tb(X4))) = X0 ) ),
inference(definition_unfolding,[],[f344,f347]) ).
tff(f355,plain,
! [X2: $int,X3: $int,X0: color,X1: array_color] :
( monochrome(X1,X3,X2,X0)
| ( tb2t2(get(color1,int,elts(color1,t2tb1(X1)),t2tb(sK13(X0,X1,X2,X3)))) != X0 ) ),
inference(definition_unfolding,[],[f342,f347]) ).
tff(f406,definition,
( spl15_10
<=> ( sK10 = $sum(sK9,1) ) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
tff(f408,plain,
( ( sK10 = $sum(sK9,1) )
| ~ spl15_10 ),
inference(avatar_component_clause,[],[f406]) ).
tff(f409,plain,
spl15_10,
inference(avatar_split_clause,[],[f289,f406]) ).
tff(f416,definition,
( spl15_12
<=> ( white = tb2t2(get(color1,int,t2tb3(sK7),t2tb(sK9))) ) ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
tff(f419,plain,
spl15_12,
inference(avatar_split_clause,[],[f291,f416]) ).
tff(f421,definition,
( spl15_13
<=> monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,sK9,white) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
tff(f423,plain,
( monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,sK9,white)
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f421]) ).
tff(f424,plain,
spl15_13,
inference(avatar_split_clause,[],[f295,f421]) ).
tff(f431,definition,
( spl15_15
<=> monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,sK10,white) ),
introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition]) ).
tff(f433,plain,
( ~ monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,sK10,white)
| spl15_15 ),
inference(avatar_component_clause,[],[f431]) ).
tff(f434,plain,
~ spl15_15,
inference(avatar_split_clause,[],[f290,f431]) ).
tff(f455,plain,
( ~ monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,$sum(sK9,1),white)
| ~ spl15_10
| spl15_15 ),
inference(forward_demodulation,[],[f433,f408]) ).
tff(f457,definition,
( spl15_20
<=> monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,$sum(sK9,1),white) ),
introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition]) ).
tff(f459,plain,
( ~ monochrome(tb2t1(mk_array(color1,sK5,t2tb3(sK7))),sK6,$sum(sK9,1),white)
| spl15_20 ),
inference(avatar_component_clause,[],[f457]) ).
tff(f460,plain,
( ~ spl15_20
| ~ spl15_10
| spl15_15 ),
inference(avatar_split_clause,[],[f455,f431,f406,f457]) ).
tff(f909,plain,
( ~ $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK6)
| spl15_20 ),
inference(resolution,[],[f341,f459]) ).
tff(f1011,plain,
( $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),$sum(sK9,1))
| spl15_20 ),
inference(resolution,[],[f343,f459]) ).
tff(f1029,definition,
( spl15_66
<=> $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),$sum(sK9,1)) ),
introduced(definition,[new_symbols(definition,[spl15_66])],[avatar_definition]) ).
tff(f1032,plain,
( spl15_66
| spl15_20 ),
inference(avatar_split_clause,[],[f1011,f457,f1029]) ).
tff(f1035,definition,
( spl15_67
<=> $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK6) ),
introduced(definition,[new_symbols(definition,[spl15_67])],[avatar_definition]) ).
tff(f1037,plain,
( ~ $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK6)
| spl15_67 ),
inference(avatar_component_clause,[],[f1035]) ).
tff(f1038,plain,
( ~ spl15_67
| spl15_20 ),
inference(avatar_split_clause,[],[f909,f457,f1035]) ).
tff(f1485,plain,
( ( white != tb2t2(get(color1,int,elts(color1,t2tb1(tb2t1(mk_array(color1,sK5,t2tb3(sK7))))),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) )
| spl15_20 ),
inference(resolution,[],[f355,f459]) ).
tff(f1520,plain,
( ( white != tb2t2(get(color1,int,elts(color1,mk_array(color1,sK5,t2tb3(sK7))),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) )
| spl15_20 ),
inference(forward_demodulation,[],[f1485,f334]) ).
tff(f1523,definition,
( spl15_96
<=> ( white = tb2t2(get(color1,int,elts(color1,mk_array(color1,sK5,t2tb3(sK7))),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) ) ),
introduced(definition,[new_symbols(definition,[spl15_96])],[avatar_definition]) ).
tff(f1525,plain,
( ( white != tb2t2(get(color1,int,elts(color1,mk_array(color1,sK5,t2tb3(sK7))),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) )
| spl15_96 ),
inference(avatar_component_clause,[],[f1523]) ).
tff(f1526,plain,
( ~ spl15_96
| spl15_20 ),
inference(avatar_split_clause,[],[f1520,f457,f1523]) ).
tff(f1541,plain,
( ! [X0: $int] :
( ~ $less(X0,sK9)
| $less(X0,sK6)
| ( white = tb2t2(get(color1,int,elts(color1,t2tb1(tb2t1(mk_array(color1,sK5,t2tb3(sK7))))),t2tb(X0))) ) )
| ~ spl15_13 ),
inference(resolution,[],[f354,f423]) ).
tff(f1546,plain,
( ! [X0: $int] :
( ( white = tb2t2(get(color1,int,elts(color1,mk_array(color1,sK5,t2tb3(sK7))),t2tb(X0))) )
| ~ $less(X0,sK9)
| $less(X0,sK6) )
| ~ spl15_13 ),
inference(forward_demodulation,[],[f1541,f334]) ).
tff(f1769,plain,
( ( white != tb2t2(get(color1,int,t2tb3(sK7),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) )
| ~ sort(map(int,color1),t2tb3(sK7))
| spl15_96 ),
inference(superposition,[],[f1525,f331]) ).
tff(f1771,plain,
( $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK6)
| ( white != white )
| ~ $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK9)
| ~ spl15_13
| spl15_96 ),
inference(superposition,[],[f1525,f1546]) ).
tff(f1773,plain,
( $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK6)
| ~ $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK9)
| ~ spl15_13
| spl15_96 ),
inference(trivial_inequality_removal,[],[f1771]) ).
tff(f1775,plain,
( ~ $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK9)
| ~ spl15_13
| spl15_67
| spl15_96 ),
inference(forward_subsumption_resolution,[],[f1773,f1037]) ).
tff(f1776,plain,
( ( white != tb2t2(get(color1,int,t2tb3(sK7),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) )
| spl15_96 ),
inference(forward_subsumption_resolution,[],[f1769,f237]) ).
tff(f1787,definition,
( spl15_120
<=> $less(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6),sK9) ),
introduced(definition,[new_symbols(definition,[spl15_120])],[avatar_definition]) ).
tff(f1790,plain,
( ~ spl15_120
| ~ spl15_13
| spl15_67
| spl15_96 ),
inference(avatar_split_clause,[],[f1775,f1523,f1035,f421,f1787]) ).
tff(f1792,definition,
( spl15_121
<=> ( white = tb2t2(get(color1,int,t2tb3(sK7),t2tb(sK13(white,tb2t1(mk_array(color1,sK5,t2tb3(sK7))),$sum(sK9,1),sK6)))) ) ),
introduced(definition,[new_symbols(definition,[spl15_121])],[avatar_definition]) ).
tff(f1795,plain,
( ~ spl15_121
| spl15_96 ),
inference(avatar_split_clause,[],[f1776,f1523,f1792]) ).
tff(f1796,plain,
$false,
inference(avatar_smt_refutation,[],[f1795,f1790,f1526,f1038,f1032,f460,f434,f424,f419,f409]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW597_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.28 % Computer : n011.cluster.edu
% 0.23/0.28 % Model : x86_64 x86_64
% 0.23/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.28 % Memory : 8046.5625MB
% 0.23/0.28 % OS : Linux 6.8.0-71-generic
% 0.23/0.28 % CPULimit : 300
% 0.23/0.28 % WCLimit : 300
% 0.23/0.28 % DateTime : Mon Sep 28 14:21:16 UTC 2026
% 0.23/0.28 % CPUTime :
% 0.23/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.32 Running first-order theorem proving
% 0.23/0.32 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
% 4.12/1.49 % (3413988)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.12/1.49 % (3414002)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2302205096:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.12/1.49 % (3414007)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2219218465:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.12/1.49 % (3414007)Instruction limit reached!
% 4.12/1.49 % (3414007)------------------------------
% 4.12/1.49 % (3414007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.12/1.49 % (3414007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/1.49 % (3414007)CaDiCaL version: 2.1.3
% 4.12/1.49 % (3414007)Termination reason: Instruction limit
% 4.12/1.49 % (3414007)Termination phase: Saturation
% 4.12/1.49 % (3414007)Time elapsed: 0.055 s
% 4.12/1.49 % (3414007)Peak memory usage: 116 MB
% 4.12/1.49 % (3414007)Instructions burned: 33 (million)
% 4.12/1.49 % (3414006)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3491774022:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.12/1.49 % (3414005)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2581420458:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.12/1.49 % (3414004)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2049247128:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.12/1.49 % (3414001)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1524729682:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.12/1.49 % (3414003)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=96772320:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.12/1.49 % (3414005)Instruction limit reached!
% 4.12/1.49 % (3414005)------------------------------
% 4.12/1.49 % (3414005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.12/1.49 % (3414005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/1.49 % (3414005)CaDiCaL version: 2.1.3
% 4.12/1.49 % (3414005)Termination reason: Instruction limit
% 4.12/1.49 % (3414005)Termination phase: Preprocessing 3
% 4.12/1.49 % (3414005)Time elapsed: 0.005 s
% 4.12/1.49 % (3414005)Peak memory usage: 86 MB
% 4.12/1.49 % (3414005)Instructions burned: 4 (million)
% 4.12/1.49 % (3414004)Instruction limit reached!
% 4.12/1.49 % (3414004)------------------------------
% 4.12/1.49 % (3414004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.12/1.49 % (3414004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/1.49 % (3414004)CaDiCaL version: 2.1.3
% 4.12/1.49 % (3414004)Termination reason: Instruction limit
% 4.12/1.49 % (3414004)Termination phase: Function definition elimination
% 4.12/1.49 % (3414004)Time elapsed: 0.007 s
% 4.12/1.49 % (3414004)Peak memory usage: 86 MB
% 4.12/1.49 % (3414004)Instructions burned: 7 (million)
% 4.12/1.49 % (3414001)Instruction limit reached!
% 4.12/1.49 % (3414001)------------------------------
% 4.12/1.49 % (3414001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.12/1.49 % (3414001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/1.49 % (3414001)CaDiCaL version: 2.1.3
% 4.12/1.49 % (3414001)Termination reason: Instruction limit
% 4.12/1.49 % (3414001)Termination phase: Saturation
% 4.12/1.49 % (3414001)Time elapsed: 0.036 s
% 4.12/1.49 % (3414001)Peak memory usage: 104 MB
% 4.12/1.49 % (3414001)Instructions burned: 12 (million)
% 4.12/1.49 % (3414006)Instruction limit reached!
% 4.12/1.49 % (3414006)------------------------------
% 4.12/1.49 % (3414006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.12/1.49 % (3414006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/1.49 % (3414006)CaDiCaL version: 2.1.3
% 4.12/1.49 % (3414006)Termination reason: Instruction limit
% 4.12/1.49 % (3414006)Termination phase: Saturation
% 4.12/1.49 % (3414006)Time elapsed: 0.078 s
% 4.12/1.49 % (3414006)Peak memory usage: 116 MB
% 4.12/1.49 % (3414006)Instructions burned: 46 (million)
% 4.12/1.49 % (3414002)Instruction limit reached!
% 4.12/1.49 % (3414002)------------------------------
% 4.12/1.49 % (3414002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.12/1.49 % (3414002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.76 % (3414002)CaDiCaL version: 2.1.3
% 6.01/1.76 % (3414002)Termination reason: Instruction limit
% 6.01/1.76 % (3414002)Termination phase: Saturation
% 6.01/1.76 % (3414002)Time elapsed: 0.182 s
% 6.01/1.76 % (3414002)Peak memory usage: 117 MB
% 6.01/1.76 % (3414002)Instructions burned: 307 (million)
% 6.01/1.76 % (3414017)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3508093216:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.01/1.76 % (3414017)Instruction limit reached!
% 6.01/1.76 % (3414017)------------------------------
% 6.01/1.76 % (3414017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.76 % (3414017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.76 % (3414017)CaDiCaL version: 2.1.3
% 6.01/1.76 % (3414017)Termination reason: Instruction limit
% 6.01/1.76 % (3414017)Termination phase: Saturation
% 6.01/1.76 % (3414017)Time elapsed: 0.011 s
% 6.01/1.76 % (3414017)Peak memory usage: 89 MB
% 6.01/1.76 % (3414017)Instructions burned: 16 (million)
% 6.01/1.76 % (3414003)Instruction limit reached!
% 6.01/1.76 % (3414003)------------------------------
% 6.01/1.76 % (3414003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.76 % (3414003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.76 % (3414003)CaDiCaL version: 2.1.3
% 6.01/1.76 % (3414003)Termination reason: Instruction limit
% 6.01/1.76 % (3414003)Termination phase: Saturation
% 6.01/1.76 % (3414003)Time elapsed: 0.184 s
% 6.01/1.76 % (3414003)Peak memory usage: 117 MB
% 6.01/1.76 % (3414003)Instructions burned: 202 (million)
% 6.01/1.76 % (3414015)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=878823980:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.01/1.76 % (3414016)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2617457149:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.01/1.76 % (3414015)Instruction limit reached!
% 6.01/1.76 % (3414015)------------------------------
% 6.01/1.76 % (3414015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.76 % (3414015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.76 % (3414015)CaDiCaL version: 2.1.3
% 6.01/1.76 % (3414015)Termination reason: Instruction limit
% 6.01/1.76 % (3414015)Termination phase: Saturation
% 6.01/1.76 % (3414015)Time elapsed: 0.017 s
% 6.01/1.76 % (3414015)Peak memory usage: 89 MB
% 6.01/1.76 % (3414015)Instructions burned: 14 (million)
% 6.01/1.76 % (3414016)Instruction limit reached!
% 6.01/1.76 % (3414016)------------------------------
% 6.01/1.76 % (3414016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.76 % (3414016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.76 % (3414016)CaDiCaL version: 2.1.3
% 6.01/1.76 % (3414016)Termination reason: Instruction limit
% 6.01/1.76 % (3414016)Termination phase: Saturation
% 6.01/1.76 % (3414016)Time elapsed: 0.036 s
% 6.01/1.76 % (3414016)Peak memory usage: 89 MB
% 6.01/1.76 % (3414016)Instructions burned: 29 (million)
% 6.01/1.76 % (3414018)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1391635839:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.01/1.76 % (3414020)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2272594984:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.01/1.76 % (3414018)Instruction limit reached!
% 6.01/1.76 % (3414018)------------------------------
% 6.01/1.76 % (3414018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.76 % (3414018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.76 % (3414018)CaDiCaL version: 2.1.3
% 6.01/1.76 % (3414018)Termination reason: Instruction limit
% 6.01/1.76 % (3414018)Termination phase: Saturation
% 6.01/1.76 % (3414018)Time elapsed: 0.029 s
% 6.01/1.76 % (3414018)Peak memory usage: 89 MB
% 6.01/1.76 % (3414018)Instructions burned: 24 (million)
% 6.01/1.76 % (3414019)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3933576378:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.01/1.76 % (3414022)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3981953241:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.27/2.02 % (3414022)Instruction limit reached!
% 7.27/2.02 % (3414022)------------------------------
% 7.27/2.02 % (3414022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.27/2.02 % (3414022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.27/2.02 % (3414022)CaDiCaL version: 2.1.3
% 7.27/2.02 % (3414022)Termination reason: Instruction limit
% 7.27/2.02 % (3414022)Termination phase: Unused predicate definition removal
% 7.27/2.02 % (3414022)Time elapsed: 0.002 s
% 7.27/2.02 % (3414022)Peak memory usage: 86 MB
% 7.27/2.02 % (3414022)Instructions burned: 3 (million)
% 7.27/2.02 % (3414020)Instruction limit reached!
% 7.27/2.02 % (3414020)------------------------------
% 7.27/2.02 % (3414020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.27/2.02 % (3414020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.27/2.02 % (3414020)CaDiCaL version: 2.1.3
% 7.27/2.02 % (3414020)Termination reason: Instruction limit
% 7.27/2.02 % (3414020)Termination phase: Saturation
% 7.27/2.02 % (3414020)Time elapsed: 0.040 s
% 7.27/2.02 % (3414020)Peak memory usage: 89 MB
% 7.27/2.02 % (3414020)Instructions burned: 86 (million)
% 7.27/2.02 % (3414019)Instruction limit reached!
% 7.27/2.02 % (3414019)------------------------------
% 7.27/2.02 % (3414019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.27/2.02 % (3414019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.27/2.02 % (3414019)CaDiCaL version: 2.1.3
% 7.27/2.02 % (3414019)Termination reason: Instruction limit
% 7.27/2.02 % (3414019)Termination phase: Saturation
% 7.27/2.02 % (3414019)Time elapsed: 0.030 s
% 7.27/2.02 % (3414019)Peak memory usage: 89 MB
% 7.27/2.02 % (3414019)Instructions burned: 28 (million)
% 7.27/2.02 % (3414023)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3031976522:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 7.27/2.02 % (3414034)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4232429113:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 7.27/2.02 % (3414033)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2805334083:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 7.27/2.02 % (3414034)Instruction limit reached!
% 7.27/2.02 % (3414034)------------------------------
% 7.27/2.02 % (3414034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.27/2.02 % (3414034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.27/2.02 % (3414034)CaDiCaL version: 2.1.3
% 7.27/2.02 % (3414034)Termination reason: Instruction limit
% 7.27/2.02 % (3414034)Termination phase: Preprocessing 2
% 7.27/2.02 % (3414034)Time elapsed: 0.002 s
% 7.27/2.02 % (3414034)Peak memory usage: 86 MB
% 7.27/2.02 % (3414034)Instructions burned: 2 (million)
% 7.27/2.02 % (3414026)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2299305821:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.27/2.02 % (3414033)Instruction limit reached!
% 7.27/2.02 % (3414033)------------------------------
% 7.27/2.02 % (3414033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.27/2.02 % (3414033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.27/2.02 % (3414033)CaDiCaL version: 2.1.3
% 7.27/2.02 % (3414033)Termination reason: Instruction limit
% 7.27/2.02 % (3414033)Termination phase: Saturation
% 7.27/2.02 % (3414033)Time elapsed: 0.007 s
% 7.27/2.02 % (3414033)Peak memory usage: 87 MB
% 7.27/2.02 % (3414033)Instructions burned: 12 (million)
% 7.27/2.02 % (3414026)Instruction limit reached!
% 7.27/2.02 % (3414026)------------------------------
% 7.27/2.02 % (3414026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.27/2.02 % (3414026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.27/2.02 % (3414026)CaDiCaL version: 2.1.3
% 7.27/2.02 % (3414026)Termination reason: Instruction limit
% 7.27/2.02 % (3414026)Termination phase: Preprocessing 3
% 7.27/2.02 % (3414026)Time elapsed: 0.005 s
% 7.27/2.02 % (3414026)Peak memory usage: 86 MB
% 7.27/2.02 % (3414026)Instructions burned: 4 (million)
% 7.27/2.02 % (3414029)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2571809477:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 9.79/2.40 % (3414031)lrs+10_1_thi=all:si=on:fd=off:random_seed=3715393763:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 9.79/2.40 % (3414036)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2767327958:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 9.79/2.40 % (3414036)Instruction limit reached!
% 9.79/2.40 % (3414036)------------------------------
% 9.79/2.40 % (3414036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.40 % (3414036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.40 % (3414036)CaDiCaL version: 2.1.3
% 9.79/2.40 % (3414036)Termination reason: Instruction limit
% 9.79/2.40 % (3414036)Termination phase: Preprocessing 1
% 9.79/2.40 % (3414036)Time elapsed: 0.003 s
% 9.79/2.40 % (3414036)Peak memory usage: 85 MB
% 9.79/2.40 % (3414036)Instructions burned: 2 (million)
% 9.79/2.40 % (3414023)Instruction limit reached!
% 9.79/2.40 % (3414023)------------------------------
% 9.79/2.40 % (3414023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.40 % (3414023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.40 % (3414023)CaDiCaL version: 2.1.3
% 9.79/2.40 % (3414023)Termination reason: Instruction limit
% 9.79/2.40 % (3414023)Termination phase: Saturation
% 9.79/2.40 % (3414023)Time elapsed: 0.176 s
% 9.79/2.40 % (3414023)Peak memory usage: 90 MB
% 9.79/2.40 % (3414023)Instructions burned: 181 (million)
% 9.79/2.40 % (3414043)dis+10_1_si=on:random_seed=585180778:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 9.79/2.40 % (3414031)Instruction limit reached!
% 9.79/2.40 % (3414031)------------------------------
% 9.79/2.40 % (3414031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.40 % (3414031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.40 % (3414031)CaDiCaL version: 2.1.3
% 9.79/2.40 % (3414031)Termination reason: Instruction limit
% 9.79/2.40 % (3414031)Termination phase: Saturation
% 9.79/2.40 % (3414031)Time elapsed: 0.093 s
% 9.79/2.40 % (3414031)Peak memory usage: 117 MB
% 9.79/2.40 % (3414031)Instructions burned: 54 (million)
% 9.79/2.40 % (3414029)Instruction limit reached!
% 9.79/2.40 % (3414029)------------------------------
% 9.79/2.40 % (3414029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.40 % (3414029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.40 % (3414029)CaDiCaL version: 2.1.3
% 9.79/2.40 % (3414029)Termination reason: Instruction limit
% 9.79/2.40 % (3414029)Termination phase: Saturation
% 9.79/2.40 % (3414029)Time elapsed: 0.135 s
% 9.79/2.40 % (3414029)Peak memory usage: 134 MB
% 9.79/2.40 % (3414029)Instructions burned: 66 (million)
% 9.79/2.40 % (3414043)Instruction limit reached!
% 9.79/2.40 % (3414043)------------------------------
% 9.79/2.40 % (3414043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.40 % (3414043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.40 % (3414043)CaDiCaL version: 2.1.3
% 9.79/2.40 % (3414043)Termination reason: Instruction limit
% 9.79/2.40 % (3414043)Termination phase: Saturation
% 9.79/2.40 % (3414043)Time elapsed: 0.006 s
% 9.79/2.40 % (3414043)Peak memory usage: 88 MB
% 9.79/2.40 % (3414043)Instructions burned: 11 (million)
% 9.79/2.40 % (3414042)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=740410721:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 9.79/2.40 % (3414044)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=706925875:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 9.79/2.40 % (3414044)Refutation not found, incomplete strategy
% 9.79/2.40 % (3414044)------------------------------
% 9.79/2.40 % (3414044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.40 % (3414044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.40 % (3414044)CaDiCaL version: 2.1.3
% 9.79/2.40 % (3414044)Termination reason: Refutation not found, incomplete strategy
% 9.79/2.40 % (3414044)Time elapsed: 0.017 s
% 9.79/2.40 % (3414044)Peak memory usage: 89 MB
% 9.79/2.40 % (3414044)Instructions burned: 15 (million)
% 9.79/2.40 % (3414048)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3816518385:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2992 on theBenchmark for (2992ds/35Mi)
% 11.80/2.75 % (3414051)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=570975506:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 11.80/2.75 % (3414052)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3832377820:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 11.80/2.75 % (3414051)Instruction limit reached!
% 11.80/2.75 % (3414051)------------------------------
% 11.80/2.75 % (3414051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.80/2.75 % (3414051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.80/2.75 % (3414051)CaDiCaL version: 2.1.3
% 11.80/2.75 % (3414051)Termination reason: Instruction limit
% 11.80/2.75 % (3414051)Termination phase: Property scanning
% 11.80/2.75 % (3414051)Time elapsed: 0.005 s
% 11.80/2.75 % (3414051)Peak memory usage: 87 MB
% 11.80/2.75 % (3414051)Instructions burned: 9 (million)
% 11.80/2.75 % (3414048)Instruction limit reached!
% 11.80/2.75 % (3414048)------------------------------
% 11.80/2.75 % (3414048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.80/2.75 % (3414048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.80/2.75 % (3414048)CaDiCaL version: 2.1.3
% 11.80/2.75 % (3414048)Termination reason: Instruction limit
% 11.80/2.75 % (3414048)Termination phase: Saturation
% 11.80/2.75 % (3414048)Time elapsed: 0.039 s
% 11.80/2.75 % (3414048)Peak memory usage: 89 MB
% 11.80/2.75 % (3414048)Instructions burned: 35 (million)
% 11.80/2.75 % (3414049)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2251378025:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.80/2.75 % (3414049)Instruction limit reached!
% 11.80/2.75 % (3414049)------------------------------
% 11.80/2.75 % (3414049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.80/2.75 % (3414049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.80/2.75 % (3414049)CaDiCaL version: 2.1.3
% 11.80/2.75 % (3414049)Termination reason: Instruction limit
% 11.80/2.75 % (3414049)Termination phase: Property scanning
% 11.80/2.75 % (3414049)Time elapsed: 0.002 s
% 11.80/2.75 % (3414049)Peak memory usage: 85 MB
% 11.80/2.75 % (3414049)Instructions burned: 2 (million)
% 11.80/2.75 % (3414053)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1518320317:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 11.80/2.75 % (3414042)Instruction limit reached!
% 11.80/2.75 % (3414042)------------------------------
% 11.80/2.75 % (3414042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.80/2.75 % (3414042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.80/2.75 % (3414042)CaDiCaL version: 2.1.3
% 11.80/2.75 % (3414042)Termination reason: Instruction limit
% 11.80/2.75 % (3414042)Termination phase: Saturation
% 11.80/2.75 % (3414042)Time elapsed: 0.173 s
% 11.80/2.75 % (3414042)Peak memory usage: 117 MB
% 11.80/2.75 % (3414042)Instructions burned: 127 (million)
% 11.80/2.75 % (3414053)Instruction limit reached!
% 11.80/2.75 % (3414053)------------------------------
% 11.80/2.75 % (3414053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.80/2.75 % (3414053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.80/2.75 % (3414053)CaDiCaL version: 2.1.3
% 11.80/2.75 % (3414053)Termination reason: Instruction limit
% 11.80/2.75 % (3414053)Termination phase: Saturation
% 11.80/2.75 % (3414053)Time elapsed: 0.039 s
% 11.80/2.75 % (3414053)Peak memory usage: 107 MB
% 11.80/2.75 % (3414053)Instructions burned: 13 (million)
% 11.80/2.75 % (3414059)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3614440656:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 11.80/2.75 % (3414060)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2994023677:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 11.80/2.75 % (3414064)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=1728219846:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 11.80/2.75 % (3414060)Instruction limit reached!
% 11.80/2.75 % (3414060)------------------------------
% 11.80/2.75 % (3414060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.10/3.12 % (3414060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.10/3.12 % (3414060)CaDiCaL version: 2.1.3
% 16.10/3.12 % (3414060)Termination reason: Instruction limit
% 16.10/3.12 % (3414060)Termination phase: Saturation
% 16.10/3.12 % (3414060)Time elapsed: 0.011 s
% 16.10/3.12 % (3414060)Peak memory usage: 88 MB
% 16.10/3.12 % (3414060)Instructions burned: 10 (million)
% 16.10/3.12 % (3414062)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3775370734:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 16.10/3.12 % (3414059)Instruction limit reached!
% 16.10/3.12 % (3414059)------------------------------
% 16.10/3.12 % (3414059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.10/3.12 % (3414059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.10/3.12 % (3414059)CaDiCaL version: 2.1.3
% 16.10/3.12 % (3414059)Termination reason: Instruction limit
% 16.10/3.12 % (3414059)Termination phase: Saturation
% 16.10/3.12 % (3414059)Time elapsed: 0.149 s
% 16.10/3.12 % (3414059)Peak memory usage: 118 MB
% 16.10/3.12 % (3414059)Instructions burned: 226 (million)
% 16.10/3.12 % (3414044)------------------------------
% 16.10/3.12 % (3414044)------------------------------
% 16.10/3.12 % (3414064)Instruction limit reached!
% 16.10/3.12 % (3414064)------------------------------
% 16.10/3.12 % (3414064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.10/3.12 % (3414064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.10/3.12 % (3414064)CaDiCaL version: 2.1.3
% 16.10/3.12 % (3414064)Termination reason: Instruction limit
% 16.10/3.12 % (3414064)Termination phase: Saturation
% 16.10/3.12 % (3414064)Time elapsed: 0.081 s
% 16.10/3.12 % (3414064)Peak memory usage: 90 MB
% 16.10/3.12 % (3414064)Instructions burned: 75 (million)
% 16.10/3.12 % (3414052)Instruction limit reached!
% 16.10/3.12 % (3414052)------------------------------
% 16.10/3.12 % (3414052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.10/3.12 % (3414052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.10/3.12 % (3414052)CaDiCaL version: 2.1.3
% 16.10/3.12 % (3414052)Termination reason: Instruction limit
% 16.10/3.12 % (3414052)Termination phase: Saturation
% 16.10/3.12 % (3414052)Time elapsed: 0.341 s
% 16.10/3.12 % (3414052)Peak memory usage: 92 MB
% 16.10/3.12 % (3414052)Instructions burned: 373 (million)
% 16.10/3.12 % (3414065)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3933696355:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi)
% 16.10/3.12 % (3414062)Instruction limit reached!
% 16.10/3.12 % (3414062)------------------------------
% 16.10/3.12 % (3414062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.10/3.12 % (3414062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.10/3.12 % (3414062)CaDiCaL version: 2.1.3
% 16.10/3.12 % (3414062)Termination reason: Instruction limit
% 16.10/3.12 % (3414062)Termination phase: Saturation
% 16.10/3.12 % (3414062)Time elapsed: 0.102 s
% 16.10/3.12 % (3414062)Peak memory usage: 133 MB
% 16.10/3.12 % (3414062)Instructions burned: 71 (million)
% 16.10/3.12 % (3414069)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2685261567:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 16.10/3.12 % (3414071)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=704771978:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi)
% 16.10/3.12 % (3414073)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3650341054:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi)
% 16.10/3.12 % (3414076)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4081969624:i=131:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 16.10/3.12 % (3414072)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=4272693855:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi)
% 16.10/3.12 % (3414074)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1560666022:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi)
% 16.10/3.12 % (3414076)Instruction limit reached!
% 16.10/3.12 % (3414076)------------------------------
% 16.10/3.12 % (3414076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.21/3.54 % (3414076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.21/3.54 % (3414076)CaDiCaL version: 2.1.3
% 18.21/3.54 % (3414076)Termination reason: Instruction limit
% 18.21/3.54 % (3414076)Termination phase: Saturation
% 18.21/3.54 % (3414076)Time elapsed: 0.093 s
% 18.21/3.54 % (3414076)Peak memory usage: 118 MB
% 18.21/3.54 % (3414076)Instructions burned: 131 (million)
% 18.21/3.54 % (3414069)Instruction limit reached!
% 18.21/3.54 % (3414069)------------------------------
% 18.21/3.54 % (3414069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.21/3.54 % (3414069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.21/3.54 % (3414069)CaDiCaL version: 2.1.3
% 18.21/3.54 % (3414069)Termination reason: Instruction limit
% 18.21/3.54 % (3414069)Termination phase: Saturation
% 18.21/3.54 % (3414069)Time elapsed: 0.172 s
% 18.21/3.54 % (3414069)Peak memory usage: 117 MB
% 18.21/3.54 % (3414069)Instructions burned: 131 (million)
% 18.21/3.54 % (3414072)Instruction limit reached!
% 18.21/3.54 % (3414072)------------------------------
% 18.21/3.54 % (3414072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.21/3.54 % (3414072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.21/3.54 % (3414072)CaDiCaL version: 2.1.3
% 18.21/3.54 % (3414072)Termination reason: Instruction limit
% 18.21/3.54 % (3414072)Termination phase: Saturation
% 18.21/3.54 % (3414072)Time elapsed: 0.100 s
% 18.21/3.54 % (3414072)Peak memory usage: 134 MB
% 18.21/3.54 % (3414072)Instructions burned: 40 (million)
% 18.21/3.54 % (3414065)Instruction limit reached!
% 18.21/3.54 % (3414065)------------------------------
% 18.21/3.54 % (3414065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.21/3.54 % (3414065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.21/3.54 % (3414065)CaDiCaL version: 2.1.3
% 18.21/3.54 % (3414065)Termination reason: Instruction limit
% 18.21/3.54 % (3414065)Termination phase: Saturation
% 18.21/3.54 % (3414065)Time elapsed: 0.317 s
% 18.21/3.54 % (3414065)Peak memory usage: 91 MB
% 18.21/3.54 % (3414065)Instructions burned: 295 (million)
% 18.21/3.54 % (3414071)Instruction limit reached!
% 18.21/3.54 % (3414071)------------------------------
% 18.21/3.54 % (3414071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.21/3.54 % (3414071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.21/3.54 % (3414071)CaDiCaL version: 2.1.3
% 18.21/3.54 % (3414071)Termination reason: Instruction limit
% 18.21/3.54 % (3414071)Termination phase: Saturation
% 18.21/3.54 % (3414071)Time elapsed: 0.208 s
% 18.21/3.54 % (3414071)Peak memory usage: 134 MB
% 18.21/3.54 % (3414071)Instructions burned: 131 (million)
% 18.21/3.54 % (3414087)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1827133432:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi)
% 18.21/3.54 % (3414073)Instruction limit reached!
% 18.21/3.54 % (3414073)------------------------------
% 18.21/3.54 % (3414073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.21/3.54 % (3414073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.21/3.54 % (3414073)CaDiCaL version: 2.1.3
% 18.21/3.54 % (3414073)Termination reason: Instruction limit
% 18.21/3.54 % (3414073)Termination phase: Saturation
% 18.21/3.54 % (3414073)Time elapsed: 0.297 s
% 18.21/3.54 % (3414073)Peak memory usage: 93 MB
% 18.21/3.54 % (3414073)Instructions burned: 307 (million)
% 18.21/3.54 % (3414090)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2478605899:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi)
% 18.21/3.54 % (3414088)dis+10_1_si=on:random_seed=2213106469:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi)
% 18.21/3.54 % (3414089)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3702526409:i=383:fsr=off:rtra=on:ev=force_2983 on theBenchmark for (2983ds/383Mi)
% 18.21/3.54 % (3414091)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=920825579:i=65:nm=16:rtra=on_2983 on theBenchmark for (2983ds/65Mi)
% 18.21/3.54 % (3414093)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1528482008:i=121:nm=16:rtra=on_2982 on theBenchmark for (2982ds/121Mi)
% 18.21/3.54 % (3414090)Instruction limit reached!
% 18.21/3.54 % (3414090)------------------------------
% 20.85/3.91 % (3414090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414090)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414090)Termination reason: Instruction limit
% 20.85/3.91 % (3414090)Termination phase: Saturation
% 20.85/3.91 % (3414090)Time elapsed: 0.147 s
% 20.85/3.91 % (3414090)Peak memory usage: 90 MB
% 20.85/3.91 % (3414090)Instructions burned: 141 (million)
% 20.85/3.91 % (3414091)Refutation not found, incomplete strategy
% 20.85/3.91 % (3414091)------------------------------
% 20.85/3.91 % (3414091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414091)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414091)Termination reason: Refutation not found, incomplete strategy
% 20.85/3.91 % (3414091)Time elapsed: 0.067 s
% 20.85/3.91 % (3414091)Peak memory usage: 116 MB
% 20.85/3.91 % (3414091)Instructions burned: 30 (million)
% 20.85/3.91 % (3414087)Instruction limit reached!
% 20.85/3.91 % (3414087)------------------------------
% 20.85/3.91 % (3414087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414087)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414087)Termination reason: Instruction limit
% 20.85/3.91 % (3414087)Termination phase: Saturation
% 20.85/3.91 % (3414087)Time elapsed: 0.215 s
% 20.85/3.91 % (3414087)Peak memory usage: 117 MB
% 20.85/3.91 % (3414087)Instructions burned: 260 (million)
% 20.85/3.91 % (3414093)Instruction limit reached!
% 20.85/3.91 % (3414093)------------------------------
% 20.85/3.91 % (3414093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414093)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414093)Termination reason: Instruction limit
% 20.85/3.91 % (3414093)Termination phase: Saturation
% 20.85/3.91 % (3414093)Time elapsed: 0.069 s
% 20.85/3.91 % (3414093)Peak memory usage: 90 MB
% 20.85/3.91 % (3414093)Instructions burned: 122 (million)
% 20.85/3.91 % (3414100)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=380670321:i=39:ins=3:rtra=on_2980 on theBenchmark for (2980ds/39Mi)
% 20.85/3.91 % (3414089)Instruction limit reached!
% 20.85/3.91 % (3414089)------------------------------
% 20.85/3.91 % (3414089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414089)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414089)Termination reason: Instruction limit
% 20.85/3.91 % (3414089)Termination phase: Saturation
% 20.85/3.91 % (3414089)Time elapsed: 0.349 s
% 20.85/3.91 % (3414089)Peak memory usage: 91 MB
% 20.85/3.91 % (3414089)Instructions burned: 383 (million)
% 20.85/3.91 % (3414100)Instruction limit reached!
% 20.85/3.91 % (3414100)------------------------------
% 20.85/3.91 % (3414100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414100)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414100)Termination reason: Instruction limit
% 20.85/3.91 % (3414100)Termination phase: Saturation
% 20.85/3.91 % (3414100)Time elapsed: 0.042 s
% 20.85/3.91 % (3414100)Peak memory usage: 116 MB
% 20.85/3.91 % (3414100)Instructions burned: 41 (million)
% 20.85/3.91 % (3414099)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=555665147:s2a=on:i=128:s2at=5:ins=3:rtra=on_2980 on theBenchmark for (2980ds/128Mi)
% 20.85/3.91 % (3414074)Instruction limit reached!
% 20.85/3.91 % (3414074)------------------------------
% 20.85/3.91 % (3414074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.91 % (3414074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.91 % (3414074)CaDiCaL version: 2.1.3
% 20.85/3.91 % (3414074)Termination reason: Instruction limit
% 20.85/3.91 % (3414074)Termination phase: Saturation
% 20.85/3.91 % (3414074)Time elapsed: 0.685 s
% 20.85/3.91 % (3414074)Peak memory usage: 140 MB
% 20.85/3.91 % (3414074)Instructions burned: 600 (million)
% 20.85/3.91 % (3414101)dis+1010_1_to=kbo:si=on:random_seed=926869721:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2980 on theBenchmark for (2980ds/175Mi)
% 20.85/3.91 % (3414101)Instruction limit reached!
% 25.76/4.50 % (3414101)------------------------------
% 25.76/4.50 % (3414101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.76/4.50 % (3414101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.76/4.50 % (3414101)CaDiCaL version: 2.1.3
% 25.76/4.50 % (3414101)Termination reason: Instruction limit
% 25.76/4.50 % (3414101)Termination phase: Saturation
% 25.76/4.50 % (3414101)Time elapsed: 0.108 s
% 25.76/4.50 % (3414101)Peak memory usage: 91 MB
% 25.76/4.50 % (3414101)Instructions burned: 176 (million)
% 25.76/4.50 % (3414091)------------------------------
% 25.76/4.50 % (3414091)------------------------------
% 25.76/4.50 % (3414103)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2580177772:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/329Mi)
% 25.76/4.50 % (3414099)Instruction limit reached!
% 25.76/4.50 % (3414099)------------------------------
% 25.76/4.50 % (3414099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.76/4.50 % (3414099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.76/4.50 % (3414099)CaDiCaL version: 2.1.3
% 25.76/4.50 % (3414099)Termination reason: Instruction limit
% 25.76/4.50 % (3414099)Termination phase: Saturation
% 25.76/4.50 % (3414099)Time elapsed: 0.174 s
% 25.76/4.50 % (3414099)Peak memory usage: 117 MB
% 25.76/4.50 % (3414099)Instructions burned: 128 (million)
% 25.76/4.50 % (3414104)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1974044685:s2a=on:i=483:doe=on:nm=32:rtra=on_2978 on theBenchmark for (2978ds/483Mi)
% 25.76/4.50 % (3414107)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1745785933:thitd=on:i=215:nm=0:rtra=on:ev=force_2978 on theBenchmark for (2978ds/215Mi)
% 25.76/4.50 % (3414108)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2099221818:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi)
% 25.76/4.50 % (3414112)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4083054495:i=328:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/328Mi)
% 25.76/4.50 % (3414111)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=137456841:st=2:i=295:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/295Mi)
% 25.76/4.50 % (3414103)Instruction limit reached!
% 25.76/4.50 % (3414103)------------------------------
% 25.76/4.50 % (3414103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.76/4.50 % (3414103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.76/4.50 % (3414103)CaDiCaL version: 2.1.3
% 25.76/4.50 % (3414103)Termination reason: Instruction limit
% 25.76/4.50 % (3414103)Termination phase: Saturation
% 25.76/4.50 % (3414103)Time elapsed: 0.259 s
% 25.76/4.50 % (3414103)Peak memory usage: 117 MB
% 25.76/4.50 % (3414103)Instructions burned: 329 (million)
% 25.76/4.50 % (3414108)Instruction limit reached!
% 25.76/4.50 % (3414108)------------------------------
% 25.76/4.50 % (3414108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.76/4.50 % (3414108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.76/4.50 % (3414108)CaDiCaL version: 2.1.3
% 25.76/4.50 % (3414108)Termination reason: Instruction limit
% 25.76/4.50 % (3414108)Termination phase: Saturation
% 25.76/4.50 % (3414108)Time elapsed: 0.187 s
% 25.76/4.50 % (3414108)Peak memory usage: 117 MB
% 25.76/4.50 % (3414108)Instructions burned: 351 (million)
% 25.76/4.50 % (3414107)Instruction limit reached!
% 25.76/4.50 % (3414107)------------------------------
% 25.76/4.50 % (3414107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.76/4.50 % (3414107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.76/4.50 % (3414107)CaDiCaL version: 2.1.3
% 25.76/4.50 % (3414107)Termination reason: Instruction limit
% 25.76/4.50 % (3414107)Termination phase: Saturation
% 25.76/4.50 % (3414107)Time elapsed: 0.266 s
% 25.76/4.50 % (3414107)Peak memory usage: 135 MB
% 25.76/4.50 % (3414107)Instructions burned: 215 (million)
% 25.76/4.50 % (3414088)Instruction limit reached!
% 25.76/4.50 % (3414088)------------------------------
% 25.76/4.50 % (3414088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.76/4.50 % (3414088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.76/4.50 % (3414088)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414088)Termination reason: Instruction limit
% 25.98/4.69 % (3414088)Termination phase: Saturation
% 25.98/4.69 % (3414088)Time elapsed: 0.937 s
% 25.98/4.69 % (3414088)Peak memory usage: 95 MB
% 25.98/4.69 % (3414088)Instructions burned: 1000 (million)
% 25.98/4.69 % (3414120)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1015368077:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi)
% 25.98/4.69 % (3414119)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3662064162:i=281:gtgl=2:rtra=on:gtg=all_2973 on theBenchmark for (2973ds/281Mi)
% 25.98/4.69 % (3414104)Instruction limit reached!
% 25.98/4.69 % (3414104)------------------------------
% 25.98/4.69 % (3414104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414104)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414104)Termination reason: Instruction limit
% 25.98/4.69 % (3414104)Termination phase: Saturation
% 25.98/4.69 % (3414104)Time elapsed: 0.499 s
% 25.98/4.69 % (3414104)Peak memory usage: 134 MB
% 25.98/4.69 % (3414104)Instructions burned: 483 (million)
% 25.98/4.69 % (3414121)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=225015810:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2973 on theBenchmark for (2973ds/321Mi)
% 25.98/4.69 % (3414112)Instruction limit reached!
% 25.98/4.69 % (3414112)------------------------------
% 25.98/4.69 % (3414112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414112)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414112)Termination reason: Instruction limit
% 25.98/4.69 % (3414112)Termination phase: Saturation
% 25.98/4.69 % (3414112)Time elapsed: 0.354 s
% 25.98/4.69 % (3414112)Peak memory usage: 118 MB
% 25.98/4.69 % (3414112)Instructions burned: 328 (million)
% 25.98/4.69 % (3414111)Instruction limit reached!
% 25.98/4.69 % (3414111)------------------------------
% 25.98/4.69 % (3414111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414111)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414111)Termination reason: Instruction limit
% 25.98/4.69 % (3414111)Termination phase: Saturation
% 25.98/4.69 % (3414111)Time elapsed: 0.287 s
% 25.98/4.69 % (3414111)Peak memory usage: 91 MB
% 25.98/4.69 % (3414111)Instructions burned: 296 (million)
% 25.98/4.69 % (3414122)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=254026742:i=416:rtra=on:gtg=position:ss=axioms_2972 on theBenchmark for (2972ds/416Mi)
% 25.98/4.69 % (3414119)Instruction limit reached!
% 25.98/4.69 % (3414119)------------------------------
% 25.98/4.69 % (3414119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414119)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414119)Termination reason: Instruction limit
% 25.98/4.69 % (3414119)Termination phase: Saturation
% 25.98/4.69 % (3414119)Time elapsed: 0.237 s
% 25.98/4.69 % (3414119)Peak memory usage: 117 MB
% 25.98/4.69 % (3414119)Instructions burned: 281 (million)
% 25.98/4.69 % (3414120)Instruction limit reached!
% 25.98/4.69 % (3414120)------------------------------
% 25.98/4.69 % (3414120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414120)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414120)Termination reason: Instruction limit
% 25.98/4.69 % (3414120)Termination phase: Saturation
% 25.98/4.69 % (3414120)Time elapsed: 0.257 s
% 25.98/4.69 % (3414120)Peak memory usage: 95 MB
% 25.98/4.69 % (3414120)Instructions burned: 485 (million)
% 25.98/4.69 % (3414126)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3023903852:i=471:thf=on:kws=precedence:rtra=on_2971 on theBenchmark for (2971ds/471Mi)
% 25.98/4.69 % (3414128)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1238023609:i=375:kws=inv_arity_squared:rtra=on_2971 on theBenchmark for (2971ds/375Mi)
% 25.98/4.69 % (3414127)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=4138125725:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi)
% 25.98/4.69 % (3414121)Instruction limit reached!
% 25.98/4.69 % (3414121)------------------------------
% 25.98/4.69 % (3414121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414121)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414121)Termination reason: Instruction limit
% 25.98/4.69 % (3414121)Termination phase: Saturation
% 25.98/4.69 % (3414121)Time elapsed: 0.299 s
% 25.98/4.69 % (3414121)Peak memory usage: 115 MB
% 25.98/4.69 % (3414121)Instructions burned: 321 (million)
% 25.98/4.69 % (3414133)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=4012512823:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2969 on theBenchmark for (2969ds/513Mi)
% 25.98/4.69 % (3414132)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4080116706:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi)
% 25.98/4.69 % (3414137)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1309169477:i=334:rtra=on_2968 on theBenchmark for (2968ds/334Mi)
% 25.98/4.69 % (3414122)Instruction limit reached!
% 25.98/4.69 % (3414122)------------------------------
% 25.98/4.69 % (3414122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414122)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414122)Termination reason: Instruction limit
% 25.98/4.69 % (3414122)Termination phase: Saturation
% 25.98/4.69 % (3414122)Time elapsed: 0.481 s
% 25.98/4.69 % (3414122)Peak memory usage: 120 MB
% 25.98/4.69 % (3414122)Instructions burned: 416 (million)
% 25.98/4.69 % (3414127)First to succeed.
% 25.98/4.69 % (3414127)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3413988"
% 25.98/4.69 % (3414128)Instruction limit reached!
% 25.98/4.69 % (3414128)------------------------------
% 25.98/4.69 % (3414128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414128)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414128)Termination reason: Instruction limit
% 25.98/4.69 % (3414128)Termination phase: Saturation
% 25.98/4.69 % (3414128)Time elapsed: 0.406 s
% 25.98/4.69 % (3414128)Peak memory usage: 119 MB
% 25.98/4.69 % (3414128)Instructions burned: 375 (million)
% 25.98/4.69 % (3414133)Instruction limit reached!
% 25.98/4.69 % (3414133)------------------------------
% 25.98/4.69 % (3414133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414133)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414133)Termination reason: Instruction limit
% 25.98/4.69 % (3414133)Termination phase: Saturation
% 25.98/4.69 % (3414133)Time elapsed: 0.304 s
% 25.98/4.69 % (3414133)Peak memory usage: 94 MB
% 25.98/4.69 % (3414133)Instructions burned: 514 (million)
% 25.98/4.69 % (3414126)Instruction limit reached!
% 25.98/4.69 % (3414126)------------------------------
% 25.98/4.69 % (3414126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414126)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414126)Termination reason: Instruction limit
% 25.98/4.69 % (3414126)Termination phase: Saturation
% 25.98/4.69 % (3414126)Time elapsed: 0.494 s
% 25.98/4.69 % (3414126)Peak memory usage: 119 MB
% 25.98/4.69 % (3414126)Instructions burned: 472 (million)
% 25.98/4.69 % (3414146)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1777083290:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/261Mi)
% 25.98/4.69 % (3414145)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2141074536:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2964 on theBenchmark for (2964ds/341Mi)
% 25.98/4.69 % (3414141)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=581213271:i=359:rtra=on:gtg=exists_top:ss=axioms_2965 on theBenchmark for (2965ds/359Mi)
% 25.98/4.69 % (3414137)Also succeeded, but the first one will report.
% 25.98/4.69 % (3414132)Instruction limit reached!
% 25.98/4.69 % (3414132)------------------------------
% 25.98/4.69 % (3414132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414132)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414132)Termination reason: Instruction limit
% 25.98/4.69 % (3414132)Termination phase: Saturation
% 25.98/4.69 % (3414132)Time elapsed: 0.481 s
% 25.98/4.69 % (3414132)Peak memory usage: 119 MB
% 25.98/4.69 % (3414132)Instructions burned: 387 (million)
% 25.98/4.69 % (3414151)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1004012575:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/235Mi)
% 25.98/4.69 % (3414145)Instruction limit reached!
% 25.98/4.69 % (3414145)------------------------------
% 25.98/4.69 % (3414145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.98/4.69 % (3414145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.98/4.69 % (3414145)CaDiCaL version: 2.1.3
% 25.98/4.69 % (3414145)Termination reason: Instruction limit
% 25.98/4.69 % (3414145)Termination phase: Saturation
% 25.98/4.69 % (3414145)Time elapsed: 0.200 s
% 25.98/4.69 % (3414145)Peak memory usage: 119 MB
% 25.98/4.69 % (3414145)Instructions burned: 342 (million)
% 25.98/4.69 % (3414127)Refutation found. Thanks to Tanya!
% 25.98/4.69 % SZS status Theorem for theBenchmark
% 25.98/4.69 % SZS output start Proof for theBenchmark
% See solution above
% 27.97/4.92 % (3414127)------------------------------
% 27.97/4.92 % (3414127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.97/4.92 % (3414127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.92 % (3414127)CaDiCaL version: 2.1.3
% 27.97/4.92 % (3414127)Termination reason: Refutation
% 27.97/4.92 % (3414127)Time elapsed: 0.371 s
% 27.97/4.92 % (3414127)Peak memory usage: 136 MB
% 27.97/4.92 % (3414127)Instructions burned: 268 (million)
% 27.97/4.92 % (3414127)------------------------------
% 27.97/4.92 % (3414127)------------------------------
% 27.97/4.92 % (3413988)Success in time 3.873 s
% 27.97/4.92 % Vampire exiting
%------------------------------------------------------------------------------