%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW659_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 : 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 01:31:04 PM UTC 2026
% Result : Theorem 30.28s 5.54s
% Output : Refutation 30.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 27
% Syntax : Number of formulae : 115 ( 26 unt; 0 typ; 18 def)
% Number of atoms : 473 ( 78 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 506 ( 148 ~; 176 |; 122 &)
% ( 23 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number arithmetic : 905 ( 254 atm; 322 fun; 214 num; 115 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 21 usr; 19 prp; 0-4 aty)
% Number of functors : 40 ( 37 usr; 16 con; 0-5 aty)
% Number of variables : 167 ( 146 !; 21 ?; 167 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
array_int: $tType ).
tff(type_def_10,type,
map_int_int: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
map: ( ty * ty ) > ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_15,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_16,type,
array: ty > ty ).
tff(func_def_17,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_18,type,
length1: ( ty * uni ) > $int ).
tff(func_def_19,type,
elts: ( ty * uni ) > uni ).
tff(func_def_20,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_21,type,
t2tb: $int > uni ).
tff(func_def_22,type,
tb2t: uni > $int ).
tff(func_def_23,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_24,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_25,type,
t2tb1: array_int > uni ).
tff(func_def_26,type,
tb2t1: uni > array_int ).
tff(func_def_29,type,
ref: ty > ty ).
tff(func_def_30,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_31,type,
contents: ( ty * uni ) > uni ).
tff(func_def_32,type,
t2tb2: map_int_int > uni ).
tff(func_def_33,type,
tb2t2: uni > map_int_int ).
tff(func_def_35,type,
sK0: ( $int * array_int * $int * $int ) > $int ).
tff(func_def_36,type,
sK1: map_int_int ).
tff(func_def_37,type,
sK2: $int ).
tff(func_def_38,type,
sK3: $int ).
tff(func_def_39,type,
sK4: $int ).
tff(func_def_40,type,
sK5: $int ).
tff(func_def_41,type,
sK6: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
is_common_prefix1: ( array_int * $int * $int * $int ) > $o ).
tff(pred_def_5,type,
is_longest_common_prefix1: ( array_int * $int * $int * $int ) > $o ).
tff(f16,axiom,
! [X2: uni,X0: ty,X1: $int] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_def1) ).
tff(f18,axiom,
! [X2: uni,X0: ty,X1: $int] :
( sort1(map(int,X0),X2)
=> ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',elts_def1) ).
tff(f23,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f24,axiom,
! [X0: ty,X1: uni,X2: $int] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def) ).
tff(f31,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f32,axiom,
! [X3: $int,X0: array_int,X2: $int,X1: $int] :
( ( $lesseq($sum(X2,X3),length1(int,t2tb1(X0)))
& $lesseq(0,X3)
& ! [X4: $int] :
( ( $lesseq(0,X4)
& $less(X4,X3) )
=> ( tb2t(get2(int,t2tb1(X0),$sum(X1,X4))) = tb2t(get2(int,t2tb1(X0),$sum(X2,X4))) ) )
& $lesseq($sum(X1,X3),length1(int,t2tb1(X0))) )
<=> is_common_prefix1(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',is_common_prefix_def) ).
tff(f40,axiom,
! [X0: map_int_int] : sort1(map(int,int),t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort4) ).
tff(f43,conjecture,
! [X3: $int,X2: $int,X1: map_int_int,X0: $int] :
( ( $lesseq(0,X0)
& $lesseq(X2,X0)
& $lesseq(X3,X0)
& $lesseq(0,X2)
& $lesseq(0,X3) )
=> ! [X4: $int] :
( is_common_prefix1(tb2t1(mk_array1(int,X0,t2tb2(X1))),X2,X3,X4)
=> ( $less($sum(X2,X4),X0)
=> ( $less($sum(X3,X4),X0)
=> ( ( $lesseq(0,$sum(X3,X4))
& $less($sum(X3,X4),X0) )
=> ( ( $less($sum(X2,X4),X0)
& $lesseq(0,$sum(X2,X4)) )
=> ( ( tb2t(get(int,int,t2tb2(X1),t2tb($sum(X2,X4)))) = tb2t(get(int,int,t2tb2(X1),t2tb($sum(X3,X4)))) )
=> ! [X5: $int] :
( ( X5 = $sum(X4,1) )
=> is_common_prefix1(tb2t1(mk_array1(int,X0,t2tb2(X1))),X2,X3,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_lcp) ).
tff(f44,negated_conjecture,
~ ! [X3: $int,X2: $int,X1: map_int_int,X0: $int] :
( ( $lesseq(0,X0)
& $lesseq(X2,X0)
& $lesseq(X3,X0)
& $lesseq(0,X2)
& $lesseq(0,X3) )
=> ! [X4: $int] :
( is_common_prefix1(tb2t1(mk_array1(int,X0,t2tb2(X1))),X2,X3,X4)
=> ( $less($sum(X2,X4),X0)
=> ( $less($sum(X3,X4),X0)
=> ( ( $lesseq(0,$sum(X3,X4))
& $less($sum(X3,X4),X0) )
=> ( ( $less($sum(X2,X4),X0)
& $lesseq(0,$sum(X2,X4)) )
=> ( ( tb2t(get(int,int,t2tb2(X1),t2tb($sum(X2,X4)))) = tb2t(get(int,int,t2tb2(X1),t2tb($sum(X3,X4)))) )
=> ! [X5: $int] :
( ( X5 = $sum(X4,1) )
=> is_common_prefix1(tb2t1(mk_array1(int,X0,t2tb2(X1))),X2,X3,X5) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f43]) ).
tff(f46,plain,
! [X3: $int,X0: array_int,X2: $int,X1: $int] :
( ( ~ $less(length1(int,t2tb1(X0)),$sum(X2,X3))
& ~ $less(X3,0)
& ! [X4: $int] :
( ( ~ $less(X4,0)
& $less(X4,X3) )
=> ( tb2t(get2(int,t2tb1(X0),$sum(X1,X4))) = tb2t(get2(int,t2tb1(X0),$sum(X2,X4))) ) )
& ~ $less(length1(int,t2tb1(X0)),$sum(X1,X3)) )
<=> is_common_prefix1(X0,X1,X2,X3) ),
inference(theory_normalization,[],[f32]) ).
tff(f47,plain,
~ ! [X3: $int,X2: $int,X1: map_int_int,X0: $int] :
( ( ~ $less(X0,0)
& ~ $less(X0,X2)
& ~ $less(X0,X3)
& ~ $less(X2,0)
& ~ $less(X3,0) )
=> ! [X4: $int] :
( is_common_prefix1(tb2t1(mk_array1(int,X0,t2tb2(X1))),X2,X3,X4)
=> ( $less($sum(X2,X4),X0)
=> ( $less($sum(X3,X4),X0)
=> ( ( ~ $less($sum(X3,X4),0)
& $less($sum(X3,X4),X0) )
=> ( ( $less($sum(X2,X4),X0)
& ~ $less($sum(X2,X4),0) )
=> ( ( tb2t(get(int,int,t2tb2(X1),t2tb($sum(X2,X4)))) = tb2t(get(int,int,t2tb2(X1),t2tb($sum(X3,X4)))) )
=> ! [X5: $int] :
( ( X5 = $sum(X4,1) )
=> is_common_prefix1(tb2t1(mk_array1(int,X0,t2tb2(X1))),X2,X3,X5) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f44]) ).
tff(f56,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( X0 = X1 )
| $less(X0,X1) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f67,plain,
~ ! [X2: map_int_int,X1: $int,X0: $int,X3: $int] :
( ( ~ $less(X0,0)
& ~ $less(X1,0)
& ~ $less(X3,X1)
& ~ $less(X3,X0)
& ~ $less(X3,0) )
=> ! [X4: $int] :
( is_common_prefix1(tb2t1(mk_array1(int,X3,t2tb2(X2))),X1,X0,X4)
=> ( $less($sum(X1,X4),X3)
=> ( $less($sum(X0,X4),X3)
=> ( ( ~ $less($sum(X0,X4),0)
& $less($sum(X0,X4),X3) )
=> ( ( ~ $less($sum(X1,X4),0)
& $less($sum(X1,X4),X3) )
=> ( ( tb2t(get(int,int,t2tb2(X2),t2tb($sum(X1,X4)))) = tb2t(get(int,int,t2tb2(X2),t2tb($sum(X0,X4)))) )
=> ! [X5: $int] :
( ( X5 = $sum(X4,1) )
=> is_common_prefix1(tb2t1(mk_array1(int,X3,t2tb2(X2))),X1,X0,X5) ) ) ) ) ) ) ) ),
inference(rectify,[],[f47]) ).
tff(f68,plain,
! [X1: array_int,X3: $int,X0: $int,X2: $int] :
( is_common_prefix1(X1,X3,X2,X0)
<=> ( ~ $less(X0,0)
& ~ $less(length1(int,t2tb1(X1)),$sum(X2,X0))
& ! [X4: $int] :
( ( $less(X4,X0)
& ~ $less(X4,0) )
=> ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) ) )
& ~ $less(length1(int,t2tb1(X1)),$sum(X3,X0)) ) ),
inference(rectify,[],[f46]) ).
tff(f72,plain,
! [X0: uni,X2: $int,X1: ty] : ( length1(X1,mk_array1(X1,X2,X0)) = X2 ),
inference(rectify,[],[f16]) ).
tff(f74,plain,
! [X2: $int,X1: ty,X0: uni] :
( sort1(map(int,X1),X0)
=> ( elts(X1,mk_array1(X1,X2,X0)) = X0 ) ),
inference(rectify,[],[f18]) ).
tff(f76,plain,
! [X1: array_int,X3: $int,X0: $int,X2: $int] :
( is_common_prefix1(X1,X3,X2,X0)
<=> ( ~ $less(X0,0)
& ~ $less(length1(int,t2tb1(X1)),$sum(X2,X0))
& ! [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) )
| ~ $less(X4,X0)
| $less(X4,0) )
& ~ $less(length1(int,t2tb1(X1)),$sum(X3,X0)) ) ),
inference(ennf_transformation,[],[f68]) ).
tff(f77,plain,
! [X2: $int,X1: array_int,X3: $int,X0: $int] :
( ( ~ $less(length1(int,t2tb1(X1)),$sum(X2,X0))
& ~ $less(length1(int,t2tb1(X1)),$sum(X3,X0))
& ! [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) )
| $less(X4,0)
| ~ $less(X4,X0) )
& ~ $less(X0,0) )
<=> is_common_prefix1(X1,X3,X2,X0) ),
inference(flattening,[],[f76]) ).
tff(f78,plain,
! [X1: ty,X0: uni,X2: $int] :
( ~ sort1(map(int,X1),X0)
| ( elts(X1,mk_array1(X1,X2,X0)) = X0 ) ),
inference(ennf_transformation,[],[f74]) ).
tff(f79,plain,
? [X2: map_int_int,X1: $int,X0: $int,X3: $int] :
( ? [X4: $int] :
( ? [X5: $int] :
( ( X5 = $sum(X4,1) )
& ~ is_common_prefix1(tb2t1(mk_array1(int,X3,t2tb2(X2))),X1,X0,X5) )
& ( tb2t(get(int,int,t2tb2(X2),t2tb($sum(X1,X4)))) = tb2t(get(int,int,t2tb2(X2),t2tb($sum(X0,X4)))) )
& ~ $less($sum(X1,X4),0)
& $less($sum(X1,X4),X3)
& ~ $less($sum(X0,X4),0)
& $less($sum(X0,X4),X3)
& $less($sum(X0,X4),X3)
& $less($sum(X1,X4),X3)
& is_common_prefix1(tb2t1(mk_array1(int,X3,t2tb2(X2))),X1,X0,X4) )
& ~ $less(X0,0)
& ~ $less(X1,0)
& ~ $less(X3,X1)
& ~ $less(X3,X0)
& ~ $less(X3,0) ),
inference(ennf_transformation,[],[f67]) ).
tff(f80,plain,
? [X2: map_int_int,X1: $int,X3: $int,X0: $int] :
( ~ $less(X3,X0)
& ~ $less(X3,0)
& ~ $less(X1,0)
& ~ $less(X0,0)
& ~ $less(X3,X1)
& ? [X4: $int] :
( $less($sum(X0,X4),X3)
& ? [X5: $int] :
( ( X5 = $sum(X4,1) )
& ~ is_common_prefix1(tb2t1(mk_array1(int,X3,t2tb2(X2))),X1,X0,X5) )
& $less($sum(X1,X4),X3)
& $less($sum(X1,X4),X3)
& is_common_prefix1(tb2t1(mk_array1(int,X3,t2tb2(X2))),X1,X0,X4)
& ( tb2t(get(int,int,t2tb2(X2),t2tb($sum(X1,X4)))) = tb2t(get(int,int,t2tb2(X2),t2tb($sum(X0,X4)))) )
& ~ $less($sum(X0,X4),0)
& ~ $less($sum(X1,X4),0)
& $less($sum(X0,X4),X3) ) ),
inference(flattening,[],[f79]) ).
tff(f85,plain,
! [X2: $int,X1: array_int,X3: $int,X0: $int] :
( ( ( ~ $less(length1(int,t2tb1(X1)),$sum(X2,X0))
& ~ $less(length1(int,t2tb1(X1)),$sum(X3,X0))
& ! [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) )
| $less(X4,0)
| ~ $less(X4,X0) )
& ~ $less(X0,0) )
| ~ is_common_prefix1(X1,X3,X2,X0) )
& ( is_common_prefix1(X1,X3,X2,X0)
| $less(length1(int,t2tb1(X1)),$sum(X2,X0))
| $less(length1(int,t2tb1(X1)),$sum(X3,X0))
| ? [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) != tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) )
& ~ $less(X4,0)
& $less(X4,X0) )
| $less(X0,0) ) ),
inference(nnf_transformation,[],[f77]) ).
tff(f86,plain,
! [X2: $int,X1: array_int,X3: $int,X0: $int] :
( ( ( ~ $less(length1(int,t2tb1(X1)),$sum(X2,X0))
& ~ $less(length1(int,t2tb1(X1)),$sum(X3,X0))
& ! [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) )
| $less(X4,0)
| ~ $less(X4,X0) )
& ~ $less(X0,0) )
| ~ is_common_prefix1(X1,X3,X2,X0) )
& ( is_common_prefix1(X1,X3,X2,X0)
| $less(length1(int,t2tb1(X1)),$sum(X2,X0))
| $less(length1(int,t2tb1(X1)),$sum(X3,X0))
| ? [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) != tb2t(get2(int,t2tb1(X1),$sum(X3,X4))) )
& ~ $less(X4,0)
& $less(X4,X0) )
| $less(X0,0) ) ),
inference(flattening,[],[f85]) ).
tff(f87,plain,
! [X0: $int,X1: array_int,X2: $int,X3: $int] :
( ( ( ~ $less(length1(int,t2tb1(X1)),$sum(X0,X3))
& ~ $less(length1(int,t2tb1(X1)),$sum(X2,X3))
& ! [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X0,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) )
| $less(X4,0)
| ~ $less(X4,X3) )
& ~ $less(X3,0) )
| ~ is_common_prefix1(X1,X2,X0,X3) )
& ( is_common_prefix1(X1,X2,X0,X3)
| $less(length1(int,t2tb1(X1)),$sum(X0,X3))
| $less(length1(int,t2tb1(X1)),$sum(X2,X3))
| ? [X5: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X2,X5))) != tb2t(get2(int,t2tb1(X1),$sum(X0,X5))) )
& ~ $less(X5,0)
& $less(X5,X3) )
| $less(X3,0) ) ),
inference(rectify,[],[f86]) ).
tff(f88,plain,
! [X0: $int,X1: array_int,X2: $int,X3: $int] :
( ( ( ~ $less(length1(int,t2tb1(X1)),$sum(X0,X3))
& ~ $less(length1(int,t2tb1(X1)),$sum(X2,X3))
& ! [X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X0,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) )
| $less(X4,0)
| ~ $less(X4,X3) )
& ~ $less(X3,0) )
| ~ is_common_prefix1(X1,X2,X0,X3) )
& ( is_common_prefix1(X1,X2,X0,X3)
| $less(length1(int,t2tb1(X1)),$sum(X0,X3))
| $less(length1(int,t2tb1(X1)),$sum(X2,X3))
| ( ( tb2t(get2(int,t2tb1(X1),$sum(X0,sK0(X0,X1,X2,X3)))) != tb2t(get2(int,t2tb1(X1),$sum(X2,sK0(X0,X1,X2,X3)))) )
& ~ $less(sK0(X0,X1,X2,X3),0)
& $less(sK0(X0,X1,X2,X3),X3) )
| $less(X3,0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X5,sK0(X0,X1,X2,X3))],[f87]) ).
tff(f89,plain,
? [X0: map_int_int,X1: $int,X2: $int,X3: $int] :
( ~ $less(X2,X3)
& ~ $less(X2,0)
& ~ $less(X1,0)
& ~ $less(X3,0)
& ~ $less(X2,X1)
& ? [X4: $int] :
( $less($sum(X3,X4),X2)
& ? [X5: $int] :
( ( X5 = $sum(X4,1) )
& ~ is_common_prefix1(tb2t1(mk_array1(int,X2,t2tb2(X0))),X1,X3,X5) )
& $less($sum(X1,X4),X2)
& $less($sum(X1,X4),X2)
& is_common_prefix1(tb2t1(mk_array1(int,X2,t2tb2(X0))),X1,X3,X4)
& ( tb2t(get(int,int,t2tb2(X0),t2tb($sum(X1,X4)))) = tb2t(get(int,int,t2tb2(X0),t2tb($sum(X3,X4)))) )
& ~ $less($sum(X3,X4),0)
& ~ $less($sum(X1,X4),0)
& $less($sum(X3,X4),X2) ) ),
inference(rectify,[],[f80]) ).
tff(f90,plain,
( ~ $less(sK3,sK4)
& ~ $less(sK3,0)
& ~ $less(sK2,0)
& ~ $less(sK4,0)
& ~ $less(sK3,sK2)
& $less($sum(sK4,sK5),sK3)
& ( sK6 = $sum(sK5,1) )
& ~ is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK6)
& $less($sum(sK2,sK5),sK3)
& $less($sum(sK2,sK5),sK3)
& is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK5)
& ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5)))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5)))) )
& ~ $less($sum(sK4,sK5),0)
& ~ $less($sum(sK2,sK5),0)
& $less($sum(sK4,sK5),sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X4,sK5),skolemize(X5,sK6)],[f89]) ).
tff(f91,plain,
! [X0: ty,X1: uni,X2: $int] :
( ~ sort1(map(int,X0),X1)
| ( elts(X0,mk_array1(X0,X2,X1)) = X1 ) ),
inference(rectify,[],[f78]) ).
tff(f92,plain,
! [X0: uni,X1: $int,X2: ty] : ( length1(X2,mk_array1(X2,X1,X0)) = X1 ),
inference(rectify,[],[f72]) ).
tff(f95,plain,
! [X0: map_int_int] : sort1(map(int,int),t2tb2(X0)),
inference(cnf_transformation,[],[f40]) ).
tff(f97,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int] :
( is_common_prefix1(X1,X2,X0,X3)
| $less(sK0(X0,X1,X2,X3),X3)
| $less(X3,0)
| $less(length1(int,t2tb1(X1)),$sum(X0,X3))
| $less(length1(int,t2tb1(X1)),$sum(X2,X3)) ),
inference(cnf_transformation,[],[f88]) ).
tff(f98,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int] :
( is_common_prefix1(X1,X2,X0,X3)
| $less(length1(int,t2tb1(X1)),$sum(X2,X3))
| $less(length1(int,t2tb1(X1)),$sum(X0,X3))
| $less(X3,0)
| ~ $less(sK0(X0,X1,X2,X3),0) ),
inference(cnf_transformation,[],[f88]) ).
tff(f99,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int] :
( is_common_prefix1(X1,X2,X0,X3)
| $less(length1(int,t2tb1(X1)),$sum(X0,X3))
| $less(length1(int,t2tb1(X1)),$sum(X2,X3))
| ( tb2t(get2(int,t2tb1(X1),$sum(X0,sK0(X0,X1,X2,X3)))) != tb2t(get2(int,t2tb1(X1),$sum(X2,sK0(X0,X1,X2,X3)))) )
| $less(X3,0) ),
inference(cnf_transformation,[],[f88]) ).
tff(f100,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int] :
( ~ is_common_prefix1(X1,X2,X0,X3)
| ~ $less(X3,0) ),
inference(cnf_transformation,[],[f88]) ).
tff(f101,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int] :
( ( tb2t(get2(int,t2tb1(X1),$sum(X0,X4))) = tb2t(get2(int,t2tb1(X1),$sum(X2,X4))) )
| $less(X4,0)
| ~ $less(X4,X3)
| ~ is_common_prefix1(X1,X2,X0,X3) ),
inference(cnf_transformation,[],[f88]) ).
tff(f104,plain,
! [X2: $int,X0: ty,X1: uni] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
inference(cnf_transformation,[],[f24]) ).
tff(f106,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f31]) ).
tff(f108,plain,
$less($sum(sK4,sK5),sK3),
inference(cnf_transformation,[],[f90]) ).
tff(f111,plain,
tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5)))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5)))),
inference(cnf_transformation,[],[f90]) ).
tff(f112,plain,
is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK5),
inference(cnf_transformation,[],[f90]) ).
tff(f114,plain,
$less($sum(sK2,sK5),sK3),
inference(cnf_transformation,[],[f90]) ).
tff(f115,plain,
~ is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK6),
inference(cnf_transformation,[],[f90]) ).
tff(f116,plain,
sK6 = $sum(sK5,1),
inference(cnf_transformation,[],[f90]) ).
tff(f125,plain,
! [X2: $int,X0: ty,X1: uni] :
( ~ sort1(map(int,X0),X1)
| ( elts(X0,mk_array1(X0,X2,X1)) = X1 ) ),
inference(cnf_transformation,[],[f91]) ).
tff(f126,plain,
! [X2: ty,X0: uni,X1: $int] : ( length1(X2,mk_array1(X2,X1,X0)) = X1 ),
inference(cnf_transformation,[],[f92]) ).
tff(f129,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f23]) ).
tff(f132,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int] :
( ~ is_common_prefix1(X1,X2,X0,X3)
| ~ $less(X4,X3)
| ( tb2t(get(int,int,elts(int,t2tb1(X1)),t2tb($sum(X2,X4)))) = tb2t(get(int,int,elts(int,t2tb1(X1)),t2tb($sum(X0,X4)))) )
| $less(X4,0) ),
inference(definition_unfolding,[],[f101,f104,f104]) ).
tff(f133,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int] :
( is_common_prefix1(X1,X2,X0,X3)
| ( tb2t(get(int,int,elts(int,t2tb1(X1)),t2tb($sum(X0,sK0(X0,X1,X2,X3))))) != tb2t(get(int,int,elts(int,t2tb1(X1)),t2tb($sum(X2,sK0(X0,X1,X2,X3))))) )
| $less(X3,0)
| $less(length1(int,t2tb1(X1)),$sum(X2,X3))
| $less(length1(int,t2tb1(X1)),$sum(X0,X3)) ),
inference(definition_unfolding,[],[f99,f104,f104]) ).
tff(f145,definition,
( spl7_3
<=> $less($sum(sK2,sK5),sK3) ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
tff(f148,plain,
spl7_3,
inference(avatar_split_clause,[],[f114,f145]) ).
tff(f150,definition,
( spl7_4
<=> is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition]) ).
tff(f152,plain,
( ~ is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK6)
| spl7_4 ),
inference(avatar_component_clause,[],[f150]) ).
tff(f153,plain,
~ spl7_4,
inference(avatar_split_clause,[],[f115,f150]) ).
tff(f160,definition,
( spl7_6
<=> ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5)))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5)))) ) ),
introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition]) ).
tff(f162,plain,
( ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5)))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5)))) )
| ~ spl7_6 ),
inference(avatar_component_clause,[],[f160]) ).
tff(f163,plain,
spl7_6,
inference(avatar_split_clause,[],[f111,f160]) ).
tff(f180,definition,
( spl7_10
<=> $less($sum(sK4,sK5),sK3) ),
introduced(definition,[new_symbols(definition,[spl7_10])],[avatar_definition]) ).
tff(f183,plain,
spl7_10,
inference(avatar_split_clause,[],[f108,f180]) ).
tff(f190,definition,
( spl7_12
<=> is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition]) ).
tff(f192,plain,
( is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,sK5)
| ~ spl7_12 ),
inference(avatar_component_clause,[],[f190]) ).
tff(f193,plain,
spl7_12,
inference(avatar_split_clause,[],[f112,f190]) ).
tff(f195,definition,
( spl7_13
<=> ( sK6 = $sum(sK5,1) ) ),
introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition]) ).
tff(f197,plain,
( ( sK6 = $sum(sK5,1) )
| ~ spl7_13 ),
inference(avatar_component_clause,[],[f195]) ).
tff(f198,plain,
spl7_13,
inference(avatar_split_clause,[],[f116,f195]) ).
tff(f285,plain,
( ~ is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,$sum(sK5,1))
| spl7_4
| ~ spl7_13 ),
inference(forward_demodulation,[],[f152,f197]) ).
tff(f287,definition,
( spl7_26
<=> is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,$sum(sK5,1)) ),
introduced(definition,[new_symbols(definition,[spl7_26])],[avatar_definition]) ).
tff(f289,plain,
( ~ is_common_prefix1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,sK4,$sum(sK5,1))
| spl7_26 ),
inference(avatar_component_clause,[],[f287]) ).
tff(f290,plain,
( ~ spl7_26
| spl7_4
| ~ spl7_13 ),
inference(avatar_split_clause,[],[f285,f195,f150,f287]) ).
tff(f308,plain,
( ( get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5))) = t2tb(tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5))))) )
| ~ spl7_6 ),
inference(superposition,[],[f129,f162]) ).
tff(f310,plain,
( ( get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5))) = get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5))) )
| ~ spl7_6 ),
inference(forward_demodulation,[],[f308,f129]) ).
tff(f312,definition,
( spl7_27
<=> ( get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK5))) = get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK5))) ) ),
introduced(definition,[new_symbols(definition,[spl7_27])],[avatar_definition]) ).
tff(f315,plain,
( spl7_27
| ~ spl7_6 ),
inference(avatar_split_clause,[],[f310,f160,f312]) ).
tff(f341,plain,
( ~ $less(sK5,0)
| ~ spl7_12 ),
inference(resolution,[],[f100,f192]) ).
tff(f343,definition,
( spl7_29
<=> $less(sK5,0) ),
introduced(definition,[new_symbols(definition,[spl7_29])],[avatar_definition]) ).
tff(f346,plain,
( ~ spl7_29
| ~ spl7_12 ),
inference(avatar_split_clause,[],[f341,f190,f343]) ).
tff(f419,plain,
! [X0: $int,X1: map_int_int] : ( t2tb2(X1) = elts(int,mk_array1(int,X0,t2tb2(X1))) ),
inference(resolution,[],[f125,f95]) ).
tff(f425,plain,
( $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),$sum(sK5,1))
| $less($sum(sK5,1),0)
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK2,$sum(sK5,1)))
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK4,$sum(sK5,1)))
| spl7_26 ),
inference(resolution,[],[f97,f289]) ).
tff(f429,plain,
( $less($sum(sK5,1),0)
| $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),$sum(sK5,1))
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK4,$sum(sK5,1)))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f425,f106]) ).
tff(f430,plain,
( $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK2,$sum(sK5,1)))
| $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),$sum(sK5,1))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK4,$sum(sK5,1)))
| $less($sum(sK5,1),0)
| spl7_26 ),
inference(forward_demodulation,[],[f429,f106]) ).
tff(f431,plain,
( $less($sum(sK5,1),0)
| $less(sK3,$sum(sK2,$sum(sK5,1)))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK4,$sum(sK5,1)))
| $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),$sum(sK5,1))
| spl7_26 ),
inference(forward_demodulation,[],[f430,f126]) ).
tff(f432,plain,
( $less($sum(sK5,1),0)
| $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),$sum(sK5,1))
| $less(sK3,$sum(sK2,$sum(sK5,1)))
| $less(sK3,$sum(sK4,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f431,f126]) ).
tff(f434,definition,
( spl7_37
<=> $less(sK3,$sum(sK4,$sum(sK5,1))) ),
introduced(definition,[new_symbols(definition,[spl7_37])],[avatar_definition]) ).
tff(f438,definition,
( spl7_38
<=> $less(sK3,$sum(sK2,$sum(sK5,1))) ),
introduced(definition,[new_symbols(definition,[spl7_38])],[avatar_definition]) ).
tff(f442,definition,
( spl7_39
<=> $less($sum(sK5,1),0) ),
introduced(definition,[new_symbols(definition,[spl7_39])],[avatar_definition]) ).
tff(f446,definition,
( spl7_40
<=> $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),$sum(sK5,1)) ),
introduced(definition,[new_symbols(definition,[spl7_40])],[avatar_definition]) ).
tff(f449,plain,
( spl7_37
| spl7_38
| spl7_39
| spl7_40
| spl7_26 ),
inference(avatar_split_clause,[],[f432,f287,f446,f442,f438,f434]) ).
tff(f450,plain,
( $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK4,$sum(sK5,1)))
| $less($sum(sK5,1),0)
| ~ $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0)
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(resolution,[],[f98,f289]) ).
tff(f454,plain,
( ~ $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0)
| $less($sum(sK5,1),0)
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK2,$sum(sK5,1)))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK4,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f450,f106]) ).
tff(f455,plain,
( ~ $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0)
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK4,$sum(sK5,1)))
| $less($sum(sK5,1),0)
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f454,f106]) ).
tff(f456,plain,
( ~ $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0)
| $less($sum(sK5,1),0)
| $less(sK3,$sum(sK4,$sum(sK5,1)))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f455,f126]) ).
tff(f457,plain,
( $less($sum(sK5,1),0)
| ~ $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0)
| $less(sK3,$sum(sK4,$sum(sK5,1)))
| $less(sK3,$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f456,f126]) ).
tff(f459,definition,
( spl7_41
<=> $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0) ),
introduced(definition,[new_symbols(definition,[spl7_41])],[avatar_definition]) ).
tff(f461,plain,
( ~ $less(sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)),0)
| spl7_41 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f462,plain,
( spl7_38
| spl7_39
| ~ spl7_41
| spl7_37
| spl7_26 ),
inference(avatar_split_clause,[],[f457,f287,f434,f459,f442,f438]) ).
tff(f470,plain,
( ! [X0: $int] :
( $less(X0,0)
| ( tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),t2tb($sum(sK2,X0)))) = tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),t2tb($sum(sK4,X0)))) )
| ~ $less(X0,sK5) )
| ~ spl7_12 ),
inference(resolution,[],[f132,f192]) ).
tff(f473,plain,
( ! [X0: $int] :
( ~ $less(X0,sK5)
| ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,X0)))) = tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,X0)))) )
| $less(X0,0) )
| ~ spl7_12 ),
inference(forward_demodulation,[],[f470,f106]) ).
tff(f481,plain,
( ( tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK4,$sum(sK5,1)))
| $less($sum(sK5,1),0)
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(resolution,[],[f133,f289]) ).
tff(f488,plain,
( ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| $less($sum(sK5,1),0)
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK4,$sum(sK5,1)))
| $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f481,f106]) ).
tff(f489,plain,
( $less(length1(int,t2tb1(tb2t1(mk_array1(int,sK3,t2tb2(sK1))))),$sum(sK2,$sum(sK5,1)))
| $less($sum(sK5,1),0)
| ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK4,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f488,f106]) ).
tff(f490,plain,
( $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK4,$sum(sK5,1)))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK2,$sum(sK5,1)))
| ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| $less($sum(sK5,1),0)
| spl7_26 ),
inference(forward_demodulation,[],[f489,f106]) ).
tff(f491,plain,
( ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| $less($sum(sK5,1),0)
| $less(sK3,$sum(sK4,$sum(sK5,1)))
| $less(length1(int,mk_array1(int,sK3,t2tb2(sK1))),$sum(sK2,$sum(sK5,1)))
| spl7_26 ),
inference(forward_demodulation,[],[f490,f126]) ).
tff(f492,plain,
( ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| $less(sK3,$sum(sK4,$sum(sK5,1)))
| $less(sK3,$sum(sK2,$sum(sK5,1)))
| $less($sum(sK5,1),0)
| spl7_26 ),
inference(forward_demodulation,[],[f491,f126]) ).
tff(f494,definition,
( spl7_42
<=> ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) = tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) ) ),
introduced(definition,[new_symbols(definition,[spl7_42])],[avatar_definition]) ).
tff(f496,plain,
( ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| spl7_42 ),
inference(avatar_component_clause,[],[f494]) ).
tff(f497,plain,
( spl7_37
| spl7_39
| ~ spl7_42
| spl7_38
| spl7_26 ),
inference(avatar_split_clause,[],[f492,f287,f438,f494,f442,f434]) ).
tff(f539,plain,
( ! [X0: $int] :
( $less(X0,0)
| $less(sK5,X0)
| ( sK5 = X0 )
| ( tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK4,X0)))) = tb2t(get(int,int,elts(int,mk_array1(int,sK3,t2tb2(sK1))),t2tb($sum(sK2,X0)))) ) )
| ~ spl7_12 ),
inference(resolution,[],[f473,f56]) ).
tff(f562,plain,
( ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) != tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| spl7_42 ),
inference(superposition,[],[f496,f419]) ).
tff(f566,definition,
( spl7_49
<=> ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) ) ),
introduced(definition,[new_symbols(definition,[spl7_49])],[avatar_definition]) ).
tff(f569,plain,
( ~ spl7_49
| spl7_42 ),
inference(avatar_split_clause,[],[f562,f494,f566]) ).
tff(f643,plain,
( ! [X0: $int] :
( $less(sK5,X0)
| $less(X0,0)
| ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,X0)))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,X0)))) )
| ( sK5 = X0 ) )
| ~ spl7_12 ),
inference(forward_demodulation,[],[f539,f419]) ).
tff(f689,plain,
( $less(sK5,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))
| ( tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK2,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) = tb2t(get(int,int,t2tb2(sK1),t2tb($sum(sK4,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)))))) )
| ( sK5 = sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)) )
| ~ spl7_12
| spl7_41 ),
inference(resolution,[],[f643,f461]) ).
tff(f730,definition,
( spl7_54
<=> ( sK5 = sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1)) ) ),
introduced(definition,[new_symbols(definition,[spl7_54])],[avatar_definition]) ).
tff(f734,definition,
( spl7_55
<=> $less(sK5,sK0(sK4,tb2t1(mk_array1(int,sK3,t2tb2(sK1))),sK2,$sum(sK5,1))) ),
introduced(definition,[new_symbols(definition,[spl7_55])],[avatar_definition]) ).
tff(f737,plain,
( spl7_54
| spl7_55
| spl7_49
| ~ spl7_12
| spl7_41 ),
inference(avatar_split_clause,[],[f689,f459,f190,f566,f734,f730]) ).
tff(f810,plain,
$false,
inference(avatar_smt_refutation,[],[f737,f569,f497,f462,f449,f346,f315,f290,f198,f193,f183,f163,f153,f148]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW659_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.24 % Computer : n017.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Mon Sep 28 14:19:06 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.30 Running first-order theorem proving
% 0.26/0.30 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.52/1.69 % (3587071)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.52/1.69 % (3587106)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=635150090:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.52/1.69 % (3587102)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2349131605:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.52/1.69 % (3587106)Instruction limit reached!
% 4.52/1.69 % (3587106)------------------------------
% 4.52/1.69 % (3587106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.52/1.69 % (3587106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.52/1.69 % (3587106)CaDiCaL version: 2.1.3
% 4.52/1.69 % (3587106)Termination reason: Instruction limit
% 4.52/1.69 % (3587106)Termination phase: Saturation
% 4.52/1.69 % (3587106)Time elapsed: 0.047 s
% 4.52/1.69 % (3587106)Peak memory usage: 116 MB
% 4.52/1.69 % (3587106)Instructions burned: 33 (million)
% 4.52/1.69 % (3587105)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=237942906:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.52/1.69 % (3587103)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1146953230:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.52/1.69 % (3587104)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2545369067:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.52/1.69 % (3587101)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2577173480:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.52/1.69 % (3587100)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=437694416:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.52/1.69 % (3587104)Instruction limit reached!
% 4.52/1.69 % (3587104)------------------------------
% 4.52/1.69 % (3587104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.52/1.69 % (3587104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.52/1.69 % (3587104)CaDiCaL version: 2.1.3
% 4.52/1.69 % (3587104)Termination reason: Instruction limit
% 4.52/1.69 % (3587104)Termination phase: Saturation
% 4.52/1.69 % (3587104)Time elapsed: 0.005 s
% 4.52/1.69 % (3587104)Peak memory usage: 88 MB
% 4.52/1.69 % (3587104)Instructions burned: 4 (million)
% 4.52/1.69 % (3587103)Instruction limit reached!
% 4.52/1.69 % (3587103)------------------------------
% 4.52/1.69 % (3587103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.52/1.69 % (3587103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.52/1.69 % (3587103)CaDiCaL version: 2.1.3
% 4.52/1.69 % (3587103)Termination reason: Instruction limit
% 4.52/1.69 % (3587103)Termination phase: Saturation
% 4.52/1.69 % (3587103)Time elapsed: 0.008 s
% 4.52/1.69 % (3587103)Peak memory usage: 88 MB
% 4.52/1.69 % (3587103)Instructions burned: 7 (million)
% 4.52/1.69 % (3587100)Instruction limit reached!
% 4.52/1.69 % (3587100)------------------------------
% 4.52/1.69 % (3587100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.52/1.69 % (3587100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.52/1.69 % (3587100)CaDiCaL version: 2.1.3
% 4.52/1.69 % (3587100)Termination reason: Instruction limit
% 4.52/1.69 % (3587100)Termination phase: Saturation
% 4.52/1.69 % (3587100)Time elapsed: 0.042 s
% 4.52/1.69 % (3587100)Peak memory usage: 116 MB
% 4.52/1.69 % (3587100)Instructions burned: 12 (million)
% 4.52/1.69 % (3587105)Instruction limit reached!
% 4.52/1.69 % (3587105)------------------------------
% 4.52/1.69 % (3587105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.52/1.69 % (3587105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.52/1.69 % (3587105)CaDiCaL version: 2.1.3
% 4.52/1.69 % (3587105)Termination reason: Instruction limit
% 4.52/1.69 % (3587105)Termination phase: Saturation
% 4.52/1.69 % (3587105)Time elapsed: 0.081 s
% 4.52/1.69 % (3587105)Peak memory usage: 116 MB
% 4.52/1.69 % (3587105)Instructions burned: 46 (million)
% 4.52/1.69 % (3587109)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=463067120:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 4.52/1.69 % (3587109)Instruction limit reached!
% 4.52/1.69 % (3587109)------------------------------
% 4.52/1.69 % (3587109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.93 % (3587109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.93 % (3587109)CaDiCaL version: 2.1.3
% 6.45/1.93 % (3587109)Termination reason: Instruction limit
% 6.45/1.93 % (3587109)Termination phase: Saturation
% 6.45/1.93 % (3587109)Time elapsed: 0.010 s
% 6.45/1.93 % (3587109)Peak memory usage: 88 MB
% 6.45/1.93 % (3587109)Instructions burned: 15 (million)
% 6.45/1.93 % (3587116)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1912693083:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.45/1.93 % (3587115)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=3824938882:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.45/1.93 % (3587116)Instruction limit reached!
% 6.45/1.93 % (3587116)------------------------------
% 6.45/1.93 % (3587116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.93 % (3587116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.93 % (3587116)CaDiCaL version: 2.1.3
% 6.45/1.93 % (3587116)Termination reason: Instruction limit
% 6.45/1.93 % (3587116)Termination phase: Saturation
% 6.45/1.93 % (3587116)Time elapsed: 0.011 s
% 6.45/1.93 % (3587116)Peak memory usage: 90 MB
% 6.45/1.93 % (3587116)Instructions burned: 16 (million)
% 6.45/1.93 % (3587102)Instruction limit reached!
% 6.45/1.93 % (3587102)------------------------------
% 6.45/1.93 % (3587102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.93 % (3587102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.93 % (3587102)CaDiCaL version: 2.1.3
% 6.45/1.93 % (3587102)Termination reason: Instruction limit
% 6.45/1.93 % (3587102)Termination phase: Saturation
% 6.45/1.93 % (3587102)Time elapsed: 0.269 s
% 6.45/1.93 % (3587102)Peak memory usage: 118 MB
% 6.45/1.93 % (3587102)Instructions burned: 201 (million)
% 6.45/1.93 % (3587115)Instruction limit reached!
% 6.45/1.93 % (3587115)------------------------------
% 6.45/1.93 % (3587115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.93 % (3587115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.93 % (3587115)CaDiCaL version: 2.1.3
% 6.45/1.93 % (3587115)Termination reason: Instruction limit
% 6.45/1.93 % (3587115)Termination phase: Saturation
% 6.45/1.93 % (3587115)Time elapsed: 0.035 s
% 6.45/1.93 % (3587115)Peak memory usage: 89 MB
% 6.45/1.93 % (3587115)Instructions burned: 29 (million)
% 6.45/1.93 % (3587117)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=290899978:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.45/1.93 % (3587117)Instruction limit reached!
% 6.45/1.93 % (3587117)------------------------------
% 6.45/1.93 % (3587117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.93 % (3587117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.93 % (3587117)CaDiCaL version: 2.1.3
% 6.45/1.93 % (3587117)Termination reason: Instruction limit
% 6.45/1.93 % (3587117)Termination phase: Saturation
% 6.45/1.93 % (3587117)Time elapsed: 0.030 s
% 6.45/1.93 % (3587117)Peak memory usage: 89 MB
% 6.45/1.93 % (3587117)Instructions burned: 24 (million)
% 6.45/1.93 % (3587118)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=307884771:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 6.45/1.93 % (3587120)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=553280638:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.45/1.93 % (3587101)Instruction limit reached!
% 6.45/1.93 % (3587101)------------------------------
% 6.45/1.93 % (3587101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.93 % (3587101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.93 % (3587101)CaDiCaL version: 2.1.3
% 6.45/1.93 % (3587101)Termination reason: Instruction limit
% 6.45/1.93 % (3587101)Termination phase: Saturation
% 6.45/1.93 % (3587101)Time elapsed: 0.316 s
% 6.45/1.93 % (3587101)Peak memory usage: 117 MB
% 6.45/1.93 % (3587101)Instructions burned: 307 (million)
% 6.45/1.93 % (3587118)Instruction limit reached!
% 6.45/1.93 % (3587118)------------------------------
% 6.45/1.93 % (3587118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.22 % (3587118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.22 % (3587118)CaDiCaL version: 2.1.3
% 8.79/2.22 % (3587118)Termination reason: Instruction limit
% 8.79/2.22 % (3587118)Termination phase: Saturation
% 8.79/2.22 % (3587118)Time elapsed: 0.028 s
% 8.79/2.22 % (3587118)Peak memory usage: 89 MB
% 8.79/2.22 % (3587118)Instructions burned: 27 (million)
% 8.79/2.22 % (3587120)Instruction limit reached!
% 8.79/2.22 % (3587120)------------------------------
% 8.79/2.22 % (3587120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.22 % (3587120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.22 % (3587120)CaDiCaL version: 2.1.3
% 8.79/2.22 % (3587120)Termination reason: Instruction limit
% 8.79/2.22 % (3587120)Termination phase: Saturation
% 8.79/2.22 % (3587120)Time elapsed: 0.041 s
% 8.79/2.22 % (3587120)Peak memory usage: 89 MB
% 8.79/2.22 % (3587120)Instructions burned: 88 (million)
% 8.79/2.22 % (3587125)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=630898612:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 8.79/2.22 % (3587125)Instruction limit reached!
% 8.79/2.22 % (3587125)------------------------------
% 8.79/2.22 % (3587125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.22 % (3587125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.22 % (3587125)CaDiCaL version: 2.1.3
% 8.79/2.22 % (3587125)Termination reason: Instruction limit
% 8.79/2.22 % (3587125)Termination phase: Function definition elimination
% 8.79/2.22 % (3587125)Time elapsed: 0.002 s
% 8.79/2.22 % (3587125)Peak memory usage: 86 MB
% 8.79/2.22 % (3587125)Instructions burned: 3 (million)
% 8.79/2.22 % (3587126)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3975817880:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 8.79/2.22 % (3587128)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1983309052:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 8.79/2.22 % (3587128)Instruction limit reached!
% 8.79/2.22 % (3587128)------------------------------
% 8.79/2.22 % (3587128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.22 % (3587128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.22 % (3587128)CaDiCaL version: 2.1.3
% 8.79/2.22 % (3587128)Termination reason: Instruction limit
% 8.79/2.22 % (3587128)Termination phase: Property scanning
% 8.79/2.22 % (3587128)Time elapsed: 0.005 s
% 8.79/2.22 % (3587128)Peak memory usage: 87 MB
% 8.79/2.22 % (3587128)Instructions burned: 4 (million)
% 8.79/2.22 % (3587134)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=891791273:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 8.79/2.22 % (3587134)Instruction limit reached!
% 8.79/2.22 % (3587134)------------------------------
% 8.79/2.22 % (3587134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.22 % (3587134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.22 % (3587134)CaDiCaL version: 2.1.3
% 8.79/2.22 % (3587134)Termination reason: Instruction limit
% 8.79/2.22 % (3587134)Termination phase: Function definition elimination
% 8.79/2.22 % (3587134)Time elapsed: 0.002 s
% 8.79/2.22 % (3587134)Peak memory usage: 86 MB
% 8.79/2.22 % (3587134)Instructions burned: 2 (million)
% 8.79/2.22 % (3587131)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2397716574:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 8.79/2.22 % (3587132)lrs+10_1_thi=all:si=on:fd=off:random_seed=3684736478:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 8.79/2.22 % (3587133)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=1366756102:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 8.79/2.22 % (3587133)Instruction limit reached!
% 8.79/2.22 % (3587133)------------------------------
% 8.79/2.22 % (3587133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.22 % (3587133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.22 % (3587133)CaDiCaL version: 2.1.3
% 8.79/2.22 % (3587133)Termination reason: Instruction limit
% 10.32/2.50 % (3587133)Termination phase: Saturation
% 10.32/2.50 % (3587133)Time elapsed: 0.009 s
% 10.32/2.50 % (3587133)Peak memory usage: 88 MB
% 10.32/2.50 % (3587133)Instructions burned: 8 (million)
% 10.32/2.50 % (3587136)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3200124960:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 10.32/2.50 % (3587136)Instruction limit reached!
% 10.32/2.50 % (3587136)------------------------------
% 10.32/2.50 % (3587136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.32/2.50 % (3587136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.32/2.50 % (3587136)CaDiCaL version: 2.1.3
% 10.32/2.50 % (3587136)Termination reason: Instruction limit
% 10.32/2.50 % (3587136)Termination phase: Property scanning
% 10.32/2.50 % (3587136)Time elapsed: 0.004 s
% 10.32/2.50 % (3587136)Peak memory usage: 86 MB
% 10.32/2.50 % (3587136)Instructions burned: 3 (million)
% 10.32/2.50 % (3587132)Instruction limit reached!
% 10.32/2.50 % (3587132)------------------------------
% 10.32/2.50 % (3587132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.32/2.50 % (3587132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.32/2.50 % (3587132)CaDiCaL version: 2.1.3
% 10.32/2.50 % (3587132)Termination reason: Instruction limit
% 10.32/2.50 % (3587132)Termination phase: Saturation
% 10.32/2.50 % (3587132)Time elapsed: 0.090 s
% 10.32/2.50 % (3587132)Peak memory usage: 116 MB
% 10.32/2.50 % (3587132)Instructions burned: 53 (million)
% 10.32/2.50 % (3587141)dis+10_1_si=on:random_seed=1931376925:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 10.32/2.50 % (3587141)Instruction limit reached!
% 10.32/2.50 % (3587141)------------------------------
% 10.32/2.50 % (3587141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.32/2.50 % (3587141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.32/2.50 % (3587141)CaDiCaL version: 2.1.3
% 10.32/2.50 % (3587141)Termination reason: Instruction limit
% 10.32/2.50 % (3587141)Termination phase: Saturation
% 10.32/2.50 % (3587141)Time elapsed: 0.006 s
% 10.32/2.50 % (3587141)Peak memory usage: 88 MB
% 10.32/2.50 % (3587141)Instructions burned: 10 (million)
% 10.32/2.50 % (3587126)Instruction limit reached!
% 10.32/2.50 % (3587126)------------------------------
% 10.32/2.50 % (3587126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.32/2.50 % (3587126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.32/2.50 % (3587126)CaDiCaL version: 2.1.3
% 10.32/2.50 % (3587126)Termination reason: Instruction limit
% 10.32/2.50 % (3587126)Termination phase: Saturation
% 10.32/2.50 % (3587126)Time elapsed: 0.167 s
% 10.32/2.50 % (3587126)Peak memory usage: 90 MB
% 10.32/2.50 % (3587126)Instructions burned: 181 (million)
% 10.32/2.50 % (3587131)Instruction limit reached!
% 10.32/2.50 % (3587131)------------------------------
% 10.32/2.50 % (3587131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.32/2.50 % (3587131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.32/2.50 % (3587131)CaDiCaL version: 2.1.3
% 10.32/2.50 % (3587131)Termination reason: Instruction limit
% 10.32/2.50 % (3587131)Termination phase: Saturation
% 10.32/2.50 % (3587131)Time elapsed: 0.134 s
% 10.32/2.50 % (3587131)Peak memory usage: 134 MB
% 10.32/2.50 % (3587131)Instructions burned: 66 (million)
% 10.32/2.50 % (3587140)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4203905267:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 10.32/2.50 % (3587145)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3652056628:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 10.32/2.50 % (3587145)Refutation not found, incomplete strategy
% 10.32/2.50 % (3587145)------------------------------
% 10.32/2.50 % (3587145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.32/2.50 % (3587145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.32/2.50 % (3587145)CaDiCaL version: 2.1.3
% 10.32/2.50 % (3587145)Termination reason: Refutation not found, incomplete strategy
% 10.32/2.50 % (3587145)Time elapsed: 0.006 s
% 10.32/2.50 % (3587145)Peak memory usage: 89 MB
% 10.32/2.50 % (3587145)Instructions burned: 7 (million)
% 10.32/2.50 % (3587147)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1464812956: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)
% 12.07/2.86 % (3587147)Instruction limit reached!
% 12.07/2.86 % (3587147)------------------------------
% 12.07/2.86 % (3587147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.86 % (3587147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.86 % (3587147)CaDiCaL version: 2.1.3
% 12.07/2.86 % (3587147)Termination reason: Instruction limit
% 12.07/2.86 % (3587147)Termination phase: Saturation
% 12.07/2.86 % (3587147)Time elapsed: 0.044 s
% 12.07/2.86 % (3587147)Peak memory usage: 89 MB
% 12.07/2.86 % (3587147)Instructions burned: 35 (million)
% 12.07/2.86 % (3587149)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4249019224:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 12.07/2.86 % (3587151)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=300119837:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 12.07/2.86 % (3587150)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3560276588:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 12.07/2.86 % (3587149)Instruction limit reached!
% 12.07/2.86 % (3587149)------------------------------
% 12.07/2.86 % (3587149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.86 % (3587149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.86 % (3587149)CaDiCaL version: 2.1.3
% 12.07/2.86 % (3587149)Termination reason: Instruction limit
% 12.07/2.86 % (3587149)Termination phase: Saturation
% 12.07/2.86 % (3587149)Time elapsed: 0.005 s
% 12.07/2.86 % (3587149)Peak memory usage: 87 MB
% 12.07/2.86 % (3587149)Instructions burned: 4 (million)
% 12.07/2.86 % (3587150)Instruction limit reached!
% 12.07/2.86 % (3587150)------------------------------
% 12.07/2.86 % (3587150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.86 % (3587150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.86 % (3587150)CaDiCaL version: 2.1.3
% 12.07/2.86 % (3587150)Termination reason: Instruction limit
% 12.07/2.86 % (3587150)Termination phase: Saturation
% 12.07/2.86 % (3587150)Time elapsed: 0.010 s
% 12.07/2.86 % (3587150)Peak memory usage: 88 MB
% 12.07/2.86 % (3587150)Instructions burned: 8 (million)
% 12.07/2.86 % (3587140)Instruction limit reached!
% 12.07/2.86 % (3587140)------------------------------
% 12.07/2.86 % (3587140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.86 % (3587140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.86 % (3587140)CaDiCaL version: 2.1.3
% 12.07/2.86 % (3587140)Termination reason: Instruction limit
% 12.07/2.86 % (3587140)Termination phase: Saturation
% 12.07/2.86 % (3587140)Time elapsed: 0.170 s
% 12.07/2.86 % (3587140)Peak memory usage: 119 MB
% 12.07/2.86 % (3587140)Instructions burned: 127 (million)
% 12.07/2.86 % (3587152)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3855739389:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 12.07/2.86 % (3587152)Instruction limit reached!
% 12.07/2.86 % (3587152)------------------------------
% 12.07/2.86 % (3587152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.86 % (3587152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.86 % (3587152)CaDiCaL version: 2.1.3
% 12.07/2.86 % (3587152)Termination reason: Instruction limit
% 12.07/2.86 % (3587152)Termination phase: Saturation
% 12.07/2.86 % (3587152)Time elapsed: 0.043 s
% 12.07/2.86 % (3587152)Peak memory usage: 113 MB
% 12.07/2.86 % (3587152)Instructions burned: 13 (million)
% 12.07/2.86 % (3587145)------------------------------
% 12.07/2.86 % (3587145)------------------------------
% 12.07/2.86 % (3587156)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=297408014:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 12.07/2.86 % (3587160)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1427764723:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi)
% 12.07/2.86 % (3587162)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=646844563:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 12.07/2.86 % (3587163)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=18227556:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 16.00/3.21 % (3587160)Instruction limit reached!
% 16.00/3.21 % (3587160)------------------------------
% 16.00/3.21 % (3587160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.21 % (3587160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.21 % (3587160)CaDiCaL version: 2.1.3
% 16.00/3.21 % (3587160)Termination reason: Instruction limit
% 16.00/3.21 % (3587160)Termination phase: Saturation
% 16.00/3.21 % (3587160)Time elapsed: 0.012 s
% 16.00/3.21 % (3587160)Peak memory usage: 88 MB
% 16.00/3.21 % (3587160)Instructions burned: 10 (million)
% 16.00/3.21 % (3587156)Refutation not found, incomplete strategy
% 16.00/3.21 % (3587156)------------------------------
% 16.00/3.21 % (3587156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.21 % (3587156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.21 % (3587156)CaDiCaL version: 2.1.3
% 16.00/3.21 % (3587156)Termination reason: Refutation not found, incomplete strategy
% 16.00/3.21 % (3587156)Time elapsed: 0.056 s
% 16.00/3.21 % (3587156)Peak memory usage: 116 MB
% 16.00/3.21 % (3587156)Instructions burned: 19 (million)
% 16.00/3.21 % (3587165)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2477809514:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi)
% 16.00/3.21 % (3587164)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=2689858233:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi)
% 16.00/3.21 % (3587163)Instruction limit reached!
% 16.00/3.21 % (3587163)------------------------------
% 16.00/3.21 % (3587163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.21 % (3587163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.21 % (3587163)CaDiCaL version: 2.1.3
% 16.00/3.21 % (3587163)Termination reason: Instruction limit
% 16.00/3.21 % (3587163)Termination phase: Saturation
% 16.00/3.21 % (3587163)Time elapsed: 0.077 s
% 16.00/3.21 % (3587163)Peak memory usage: 90 MB
% 16.00/3.21 % (3587163)Instructions burned: 75 (million)
% 16.00/3.21 % (3587151)Instruction limit reached!
% 16.00/3.21 % (3587151)------------------------------
% 16.00/3.21 % (3587151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.21 % (3587151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.21 % (3587151)CaDiCaL version: 2.1.3
% 16.00/3.21 % (3587151)Termination reason: Instruction limit
% 16.00/3.21 % (3587151)Termination phase: Saturation
% 16.00/3.21 % (3587151)Time elapsed: 0.317 s
% 16.00/3.21 % (3587151)Peak memory usage: 92 MB
% 16.00/3.21 % (3587151)Instructions burned: 370 (million)
% 16.00/3.21 % (3587165)Instruction limit reached!
% 16.00/3.21 % (3587165)------------------------------
% 16.00/3.21 % (3587165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.21 % (3587165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.21 % (3587165)CaDiCaL version: 2.1.3
% 16.00/3.21 % (3587165)Termination reason: Instruction limit
% 16.00/3.21 % (3587165)Termination phase: Saturation
% 16.00/3.21 % (3587165)Time elapsed: 0.092 s
% 16.00/3.21 % (3587165)Peak memory usage: 117 MB
% 16.00/3.21 % (3587165)Instructions burned: 131 (million)
% 16.00/3.21 % (3587162)Instruction limit reached!
% 16.00/3.21 % (3587162)------------------------------
% 16.00/3.21 % (3587162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.21 % (3587162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.21 % (3587162)CaDiCaL version: 2.1.3
% 16.00/3.21 % (3587162)Termination reason: Instruction limit
% 16.00/3.21 % (3587162)Termination phase: Saturation
% 16.00/3.21 % (3587162)Time elapsed: 0.134 s
% 16.00/3.21 % (3587162)Peak memory usage: 133 MB
% 16.00/3.21 % (3587162)Instructions burned: 71 (million)
% 16.00/3.21 % (3587170)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=762090992:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi)
% 16.00/3.21 % (3587173)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2196472865:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi)
% 16.00/3.21 % (3587175)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=965915697:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi)
% 17.31/3.69 % (3587173)Instruction limit reached!
% 17.31/3.69 % (3587173)------------------------------
% 17.31/3.69 % (3587173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.31/3.69 % (3587173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.31/3.69 % (3587173)CaDiCaL version: 2.1.3
% 17.31/3.69 % (3587173)Termination reason: Instruction limit
% 17.31/3.69 % (3587173)Termination phase: Saturation
% 17.31/3.69 % (3587173)Time elapsed: 0.076 s
% 17.31/3.69 % (3587173)Peak memory usage: 135 MB
% 17.31/3.69 % (3587173)Instructions burned: 40 (million)
% 17.31/3.69 % (3587174)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=992789225:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi)
% 17.31/3.69 % (3587176)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1961497712:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.31/3.69 % (3587164)Instruction limit reached!
% 17.31/3.69 % (3587164)------------------------------
% 17.31/3.69 % (3587164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.31/3.69 % (3587164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.31/3.69 % (3587164)CaDiCaL version: 2.1.3
% 17.31/3.69 % (3587164)Termination reason: Instruction limit
% 17.31/3.69 % (3587164)Termination phase: Saturation
% 17.31/3.69 % (3587164)Time elapsed: 0.318 s
% 17.31/3.69 % (3587164)Peak memory usage: 91 MB
% 17.31/3.69 % (3587164)Instructions burned: 294 (million)
% 17.31/3.69 % (3587170)Instruction limit reached!
% 17.31/3.69 % (3587170)------------------------------
% 17.31/3.69 % (3587170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.31/3.69 % (3587170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.31/3.69 % (3587156)------------------------------
% 17.31/3.69 % (3587156)------------------------------
% 17.31/3.69 % (3587170)CaDiCaL version: 2.1.3
% 17.31/3.69 % (3587170)Termination reason: Instruction limit
% 17.31/3.69 % (3587170)Termination phase: Saturation
% 17.31/3.69 % (3587170)Time elapsed: 0.199 s
% 17.31/3.69 % (3587170)Peak memory usage: 134 MB
% 17.31/3.69 % (3587170)Instructions burned: 132 (million)
% 17.31/3.69 % (3587180)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=2130919347:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi)
% 17.31/3.69 % (3587183)dis+10_1_si=on:random_seed=930357190:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi)
% 17.31/3.69 % (3587176)Instruction limit reached!
% 17.31/3.69 % (3587176)------------------------------
% 17.31/3.69 % (3587176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.31/3.69 % (3587176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.31/3.69 % (3587176)CaDiCaL version: 2.1.3
% 17.31/3.69 % (3587176)Termination reason: Instruction limit
% 17.31/3.69 % (3587176)Termination phase: Saturation
% 17.31/3.69 % (3587176)Time elapsed: 0.165 s
% 17.31/3.69 % (3587176)Peak memory usage: 119 MB
% 17.31/3.69 % (3587176)Instructions burned: 131 (million)
% 17.31/3.69 % (3587174)Instruction limit reached!
% 17.31/3.69 % (3587174)------------------------------
% 17.31/3.69 % (3587174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.31/3.69 % (3587174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.31/3.69 % (3587174)CaDiCaL version: 2.1.3
% 17.31/3.69 % (3587174)Termination reason: Instruction limit
% 17.31/3.69 % (3587174)Termination phase: Saturation
% 17.31/3.69 % (3587174)Time elapsed: 0.291 s
% 17.31/3.69 % (3587174)Peak memory usage: 93 MB
% 17.31/3.69 % (3587174)Instructions burned: 307 (million)
% 17.31/3.69 % (3587175)Instruction limit reached!
% 17.31/3.69 % (3587175)------------------------------
% 17.31/3.69 % (3587175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.31/3.69 % (3587175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.31/3.69 % (3587175)CaDiCaL version: 2.1.3
% 17.31/3.69 % (3587175)Termination reason: Instruction limit
% 17.31/3.69 % (3587175)Termination phase: Saturation
% 17.31/3.69 % (3587175)Time elapsed: 0.341 s
% 17.31/3.69 % (3587175)Peak memory usage: 141 MB
% 17.31/3.69 % (3587175)Instructions burned: 600 (million)
% 17.31/3.69 % (3587185)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3418489188:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi)
% 17.31/3.69 % (3587184)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4152377720:i=383:fsr=off:rtra=on:ev=force_2983 on theBenchmark for (2983ds/383Mi)
% 22.39/4.12 % (3587188)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1759861360:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 22.39/4.12 % (3587192)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=415918826:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi)
% 22.39/4.12 % (3587180)Instruction limit reached!
% 22.39/4.12 % (3587180)------------------------------
% 22.39/4.12 % (3587180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.39/4.12 % (3587180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.39/4.12 % (3587180)CaDiCaL version: 2.1.3
% 22.39/4.12 % (3587180)Termination reason: Instruction limit
% 22.39/4.12 % (3587180)Termination phase: Saturation
% 22.39/4.12 % (3587180)Time elapsed: 0.285 s
% 22.39/4.12 % (3587180)Peak memory usage: 117 MB
% 22.39/4.12 % (3587180)Instructions burned: 260 (million)
% 22.39/4.12 % (3587185)Instruction limit reached!
% 22.39/4.12 % (3587185)------------------------------
% 22.39/4.12 % (3587185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.39/4.12 % (3587185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.39/4.12 % (3587185)CaDiCaL version: 2.1.3
% 22.39/4.12 % (3587185)Termination reason: Instruction limit
% 22.39/4.12 % (3587185)Termination phase: Saturation
% 22.39/4.12 % (3587185)Time elapsed: 0.150 s
% 22.39/4.12 % (3587185)Peak memory usage: 90 MB
% 22.39/4.12 % (3587185)Instructions burned: 141 (million)
% 22.39/4.12 % (3587193)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=339273638:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi)
% 22.39/4.12 % (3587188)Instruction limit reached!
% 22.39/4.12 % (3587188)------------------------------
% 22.39/4.12 % (3587188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.39/4.12 % (3587188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.39/4.12 % (3587188)CaDiCaL version: 2.1.3
% 22.39/4.12 % (3587188)Termination reason: Instruction limit
% 22.39/4.12 % (3587188)Termination phase: Saturation
% 22.39/4.12 % (3587188)Time elapsed: 0.095 s
% 22.39/4.12 % (3587188)Peak memory usage: 116 MB
% 22.39/4.12 % (3587188)Instructions burned: 65 (million)
% 22.39/4.12 % (3587192)Instruction limit reached!
% 22.39/4.12 % (3587192)------------------------------
% 22.39/4.12 % (3587192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.39/4.12 % (3587192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.39/4.12 % (3587192)CaDiCaL version: 2.1.3
% 22.39/4.12 % (3587192)Termination reason: Instruction limit
% 22.39/4.12 % (3587192)Termination phase: Saturation
% 22.39/4.12 % (3587192)Time elapsed: 0.101 s
% 22.39/4.12 % (3587192)Peak memory usage: 90 MB
% 22.39/4.12 % (3587192)Instructions burned: 122 (million)
% 22.39/4.12 % (3587193)Instruction limit reached!
% 22.39/4.12 % (3587193)------------------------------
% 22.39/4.12 % (3587193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.39/4.12 % (3587193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.39/4.12 % (3587193)CaDiCaL version: 2.1.3
% 22.39/4.12 % (3587193)Termination reason: Instruction limit
% 22.39/4.12 % (3587193)Termination phase: Saturation
% 22.39/4.12 % (3587193)Time elapsed: 0.092 s
% 22.39/4.12 % (3587193)Peak memory usage: 119 MB
% 22.39/4.12 % (3587193)Instructions burned: 129 (million)
% 22.39/4.12 % (3587184)Instruction limit reached!
% 22.39/4.12 % (3587184)------------------------------
% 22.39/4.12 % (3587184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.39/4.12 % (3587184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.39/4.12 % (3587184)CaDiCaL version: 2.1.3
% 22.39/4.12 % (3587184)Termination reason: Instruction limit
% 22.39/4.12 % (3587184)Termination phase: Saturation
% 22.39/4.12 % (3587184)Time elapsed: 0.339 s
% 22.39/4.12 % (3587184)Peak memory usage: 91 MB
% 22.39/4.12 % (3587184)Instructions burned: 384 (million)
% 22.39/4.12 % (3587199)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=1824601320:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi)
% 22.39/4.12 % (3587202)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4037937766:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/329Mi)
% 23.97/4.55 % (3587200)dis+1010_1_to=kbo:si=on:random_seed=1364547403:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi)
% 23.97/4.55 % (3587203)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1891448872:s2a=on:i=483:doe=on:nm=32:rtra=on_2978 on theBenchmark for (2978ds/483Mi)
% 23.97/4.55 % (3587199)Instruction limit reached!
% 23.97/4.55 % (3587199)------------------------------
% 23.97/4.55 % (3587199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.55 % (3587199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.55 % (3587199)CaDiCaL version: 2.1.3
% 23.97/4.55 % (3587199)Termination reason: Instruction limit
% 23.97/4.55 % (3587199)Termination phase: Saturation
% 23.97/4.55 % (3587199)Time elapsed: 0.072 s
% 23.97/4.55 % (3587199)Peak memory usage: 116 MB
% 23.97/4.55 % (3587199)Instructions burned: 39 (million)
% 23.97/4.55 % (3587208)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=57757367:i=349:rtra=on_2977 on theBenchmark for (2977ds/349Mi)
% 23.97/4.55 % (3587205)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4022013492:thitd=on:i=215:nm=0:rtra=on:ev=force_2978 on theBenchmark for (2978ds/215Mi)
% 23.97/4.55 % (3587200)Instruction limit reached!
% 23.97/4.55 % (3587200)------------------------------
% 23.97/4.55 % (3587200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.55 % (3587200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.55 % (3587200)CaDiCaL version: 2.1.3
% 23.97/4.55 % (3587200)Termination reason: Instruction limit
% 23.97/4.55 % (3587200)Termination phase: Saturation
% 23.97/4.55 % (3587200)Time elapsed: 0.201 s
% 23.97/4.55 % (3587200)Peak memory usage: 91 MB
% 23.97/4.55 % (3587200)Instructions burned: 175 (million)
% 23.97/4.55 % (3587202)Instruction limit reached!
% 23.97/4.55 % (3587202)------------------------------
% 23.97/4.55 % (3587202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.55 % (3587202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.55 % (3587202)CaDiCaL version: 2.1.3
% 23.97/4.55 % (3587202)Termination reason: Instruction limit
% 23.97/4.55 % (3587202)Termination phase: Saturation
% 23.97/4.55 % (3587202)Time elapsed: 0.223 s
% 23.97/4.55 % (3587202)Peak memory usage: 120 MB
% 23.97/4.55 % (3587202)Instructions burned: 329 (million)
% 23.97/4.55 % (3587212)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3396670416:st=2:i=295:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/295Mi)
% 23.97/4.55 % (3587216)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=806749773:i=281:gtgl=2:rtra=on:gtg=all_2975 on theBenchmark for (2975ds/281Mi)
% 23.97/4.55 % (3587205)Instruction limit reached!
% 23.97/4.55 % (3587205)------------------------------
% 23.97/4.55 % (3587205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.55 % (3587205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.55 % (3587205)CaDiCaL version: 2.1.3
% 23.97/4.55 % (3587205)Termination reason: Instruction limit
% 23.97/4.55 % (3587205)Termination phase: Saturation
% 23.97/4.55 % (3587205)Time elapsed: 0.275 s
% 23.97/4.55 % (3587205)Peak memory usage: 135 MB
% 23.97/4.55 % (3587205)Instructions burned: 215 (million)
% 23.97/4.55 % (3587215)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3435970656:i=328:kws=inv_frequency:nm=20:rtra=on_2975 on theBenchmark for (2975ds/328Mi)
% 23.97/4.55 % (3587208)Instruction limit reached!
% 23.97/4.55 % (3587208)------------------------------
% 23.97/4.55 % (3587208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.55 % (3587208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.55 % (3587208)CaDiCaL version: 2.1.3
% 23.97/4.55 % (3587208)Termination reason: Instruction limit
% 23.97/4.55 % (3587208)Termination phase: Saturation
% 23.97/4.55 % (3587208)Time elapsed: 0.288 s
% 23.97/4.55 % (3587208)Peak memory usage: 117 MB
% 23.97/4.55 % (3587208)Instructions burned: 349 (million)
% 23.97/4.55 % (3587183)Instruction limit reached!
% 23.97/4.55 % (3587183)------------------------------
% 23.97/4.55 % (3587183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.55 % (3587183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.60/4.98 % (3587183)CaDiCaL version: 2.1.3
% 26.60/4.98 % (3587183)Termination reason: Instruction limit
% 26.60/4.98 % (3587183)Termination phase: Saturation
% 26.60/4.98 % (3587183)Time elapsed: 0.961 s
% 26.60/4.98 % (3587183)Peak memory usage: 93 MB
% 26.60/4.98 % (3587183)Instructions burned: 1000 (million)
% 26.60/4.98 % (3587216)Instruction limit reached!
% 26.60/4.98 % (3587216)------------------------------
% 26.60/4.98 % (3587216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.60/4.98 % (3587216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.60/4.98 % (3587216)CaDiCaL version: 2.1.3
% 26.60/4.98 % (3587216)Termination reason: Instruction limit
% 26.60/4.98 % (3587216)Termination phase: Saturation
% 26.60/4.98 % (3587216)Time elapsed: 0.178 s
% 26.60/4.98 % (3587216)Peak memory usage: 118 MB
% 26.60/4.98 % (3587216)Instructions burned: 282 (million)
% 26.60/4.98 % (3587212)Instruction limit reached!
% 26.60/4.98 % (3587212)------------------------------
% 26.60/4.98 % (3587212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.60/4.98 % (3587212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.60/4.98 % (3587212)CaDiCaL version: 2.1.3
% 26.60/4.98 % (3587212)Termination reason: Instruction limit
% 26.60/4.98 % (3587212)Termination phase: Saturation
% 26.60/4.98 % (3587212)Time elapsed: 0.257 s
% 26.60/4.98 % (3587212)Peak memory usage: 91 MB
% 26.60/4.98 % (3587212)Instructions burned: 295 (million)
% 26.60/4.98 % (3587203)Instruction limit reached!
% 26.60/4.98 % (3587203)------------------------------
% 26.60/4.98 % (3587203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.60/4.98 % (3587203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.60/4.98 % (3587203)CaDiCaL version: 2.1.3
% 26.60/4.98 % (3587203)Termination reason: Instruction limit
% 26.60/4.98 % (3587203)Termination phase: Saturation
% 26.60/4.98 % (3587203)Time elapsed: 0.499 s
% 26.60/4.98 % (3587203)Peak memory usage: 134 MB
% 26.60/4.98 % (3587203)Instructions burned: 483 (million)
% 26.60/4.98 % (3587223)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1951874350:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2973 on theBenchmark for (2973ds/321Mi)
% 26.60/4.98 % (3587222)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1905256726:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi)
% 26.60/4.98 % (3587225)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1185865941:i=416:rtra=on:gtg=position:ss=axioms_2972 on theBenchmark for (2972ds/416Mi)
% 26.60/4.98 % (3587234)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=916542192:i=471:thf=on:kws=precedence:rtra=on_2971 on theBenchmark for (2971ds/471Mi)
% 26.60/4.98 % (3587225)Refutation not found, incomplete strategy
% 26.60/4.98 % (3587225)------------------------------
% 26.60/4.98 % (3587225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.60/4.98 % (3587225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.60/4.98 % (3587225)CaDiCaL version: 2.1.3
% 26.60/4.98 % (3587225)Termination reason: Refutation not found, incomplete strategy
% 26.60/4.98 % (3587225)Time elapsed: 0.055 s
% 26.60/4.98 % (3587225)Peak memory usage: 116 MB
% 26.60/4.98 % (3587225)Instructions burned: 19 (million)
% 26.60/4.98 % (3587235)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=3656675828:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi)
% 26.60/4.98 % (3587237)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1325962426:i=375:kws=inv_arity_squared:rtra=on_2971 on theBenchmark for (2971ds/375Mi)
% 26.60/4.98 % (3587215)Instruction limit reached!
% 26.60/4.98 % (3587215)------------------------------
% 26.60/4.98 % (3587215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.60/4.98 % (3587215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.60/4.98 % (3587215)CaDiCaL version: 2.1.3
% 26.60/4.98 % (3587215)Termination reason: Instruction limit
% 26.60/4.98 % (3587215)Termination phase: Saturation
% 26.60/4.98 % (3587215)Time elapsed: 0.382 s
% 26.60/4.98 % (3587215)Peak memory usage: 118 MB
% 26.60/4.98 % (3587215)Instructions burned: 328 (million)
% 26.60/4.98 % (3587223)Instruction limit reached!
% 30.28/5.54 % (3587223)------------------------------
% 30.28/5.54 % (3587223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587223)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587223)Termination reason: Instruction limit
% 30.28/5.54 % (3587223)Termination phase: Saturation
% 30.28/5.54 % (3587223)Time elapsed: 0.280 s
% 30.28/5.54 % (3587223)Peak memory usage: 114 MB
% 30.28/5.54 % (3587223)Instructions burned: 322 (million)
% 30.28/5.54 % (3587234)Instruction limit reached!
% 30.28/5.54 % (3587234)------------------------------
% 30.28/5.54 % (3587234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587234)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587234)Termination reason: Instruction limit
% 30.28/5.54 % (3587234)Termination phase: Saturation
% 30.28/5.54 % (3587234)Time elapsed: 0.258 s
% 30.28/5.54 % (3587234)Peak memory usage: 119 MB
% 30.28/5.54 % (3587234)Instructions burned: 473 (million)
% 30.28/5.54 % (3587244)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2205480434:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi)
% 30.28/5.54 % (3587222)Instruction limit reached!
% 30.28/5.54 % (3587222)------------------------------
% 30.28/5.54 % (3587222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587222)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587222)Termination reason: Instruction limit
% 30.28/5.54 % (3587222)Termination phase: Saturation
% 30.28/5.54 % (3587222)Time elapsed: 0.464 s
% 30.28/5.54 % (3587222)Peak memory usage: 95 MB
% 30.28/5.54 % (3587222)Instructions burned: 484 (million)
% 30.28/5.54 % (3587246)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1865744124:i=334:rtra=on_2967 on theBenchmark for (2967ds/334Mi)
% 30.28/5.54 % (3587225)------------------------------
% 30.28/5.54 % (3587225)------------------------------
% 30.28/5.54 % (3587245)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=627265496:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2968 on theBenchmark for (2968ds/513Mi)
% 30.28/5.54 % (3587235)Instruction limit reached!
% 30.28/5.54 % (3587235)------------------------------
% 30.28/5.54 % (3587235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587235)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587235)Termination reason: Instruction limit
% 30.28/5.54 % (3587235)Termination phase: Saturation
% 30.28/5.54 % (3587235)Time elapsed: 0.378 s
% 30.28/5.54 % (3587235)Peak memory usage: 136 MB
% 30.28/5.54 % (3587235)Instructions burned: 276 (million)
% 30.28/5.54 % (3587237)Instruction limit reached!
% 30.28/5.54 % (3587237)------------------------------
% 30.28/5.54 % (3587237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587237)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587237)Termination reason: Instruction limit
% 30.28/5.54 % (3587237)Termination phase: Saturation
% 30.28/5.54 % (3587237)Time elapsed: 0.391 s
% 30.28/5.54 % (3587237)Peak memory usage: 118 MB
% 30.28/5.54 % (3587237)Instructions burned: 375 (million)
% 30.28/5.54 % (3587248)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2512947004:i=359:rtra=on:gtg=exists_top:ss=axioms_2966 on theBenchmark for (2966ds/359Mi)
% 30.28/5.54 % (3587246)Instruction limit reached!
% 30.28/5.54 % (3587246)------------------------------
% 30.28/5.54 % (3587246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587246)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587246)Termination reason: Instruction limit
% 30.28/5.54 % (3587246)Termination phase: Saturation
% 30.28/5.54 % (3587246)Time elapsed: 0.208 s
% 30.28/5.54 % (3587246)Peak memory usage: 134 MB
% 30.28/5.54 % (3587246)Instructions burned: 335 (million)
% 30.28/5.54 % (3587251)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2738876818:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2966 on theBenchmark for (2966ds/341Mi)
% 30.28/5.54 % (3587252)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1687244063:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/261Mi)
% 30.28/5.54 % (3587253)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=2935554674:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2965 on theBenchmark for (2965ds/235Mi)
% 30.28/5.54 % (3587255)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3151437058:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2964 on theBenchmark for (2964ds/273Mi)
% 30.28/5.54 % (3587244)Instruction limit reached!
% 30.28/5.54 % (3587244)------------------------------
% 30.28/5.54 % (3587244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587244)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587244)Termination reason: Instruction limit
% 30.28/5.54 % (3587244)Termination phase: Saturation
% 30.28/5.54 % (3587244)Time elapsed: 0.484 s
% 30.28/5.54 % (3587244)Peak memory usage: 119 MB
% 30.28/5.54 % (3587244)Instructions burned: 387 (million)
% 30.28/5.54 % (3587253)First to succeed.
% 30.28/5.54 % (3587253)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3587071"
% 30.28/5.54 % (3587245)Instruction limit reached!
% 30.28/5.54 % (3587245)------------------------------
% 30.28/5.54 % (3587245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587245)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587245)Termination reason: Instruction limit
% 30.28/5.54 % (3587245)Termination phase: Saturation
% 30.28/5.54 % (3587245)Time elapsed: 0.501 s
% 30.28/5.54 % (3587245)Peak memory usage: 92 MB
% 30.28/5.54 % (3587245)Instructions burned: 513 (million)
% 30.28/5.54 % (3587255)Instruction limit reached!
% 30.28/5.54 % (3587255)------------------------------
% 30.28/5.54 % (3587255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587255)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587255)Termination reason: Instruction limit
% 30.28/5.54 % (3587255)Termination phase: Saturation
% 30.28/5.54 % (3587255)Time elapsed: 0.171 s
% 30.28/5.54 % (3587255)Peak memory usage: 91 MB
% 30.28/5.54 % (3587255)Instructions burned: 274 (million)
% 30.28/5.54 % (3587252)Instruction limit reached!
% 30.28/5.54 % (3587252)------------------------------
% 30.28/5.54 % (3587252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587252)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587252)Termination reason: Instruction limit
% 30.28/5.54 % (3587252)Termination phase: Saturation
% 30.28/5.54 % (3587252)Time elapsed: 0.286 s
% 30.28/5.54 % (3587252)Peak memory usage: 117 MB
% 30.28/5.54 % (3587252)Instructions burned: 261 (million)
% 30.28/5.54 % (3587260)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3607798232:i=146:doe=on:rtra=on_2962 on theBenchmark for (2962ds/146Mi)
% 30.28/5.54 % (3587248)Instruction limit reached!
% 30.28/5.54 % (3587248)------------------------------
% 30.28/5.54 % (3587248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587248)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587248)Termination reason: Instruction limit
% 30.28/5.54 % (3587248)Termination phase: Saturation
% 30.28/5.54 % (3587248)Time elapsed: 0.376 s
% 30.28/5.54 % (3587248)Peak memory usage: 92 MB
% 30.28/5.54 % (3587248)Instructions burned: 359 (million)
% 30.28/5.54 % (3587251)Instruction limit reached!
% 30.28/5.54 % (3587251)------------------------------
% 30.28/5.54 % (3587251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587251)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587251)Termination reason: Instruction limit
% 30.28/5.54 % (3587251)Termination phase: Saturation
% 30.28/5.54 % (3587251)Time elapsed: 0.353 s
% 30.28/5.54 % (3587251)Peak memory usage: 119 MB
% 30.28/5.54 % (3587251)Instructions burned: 341 (million)
% 30.28/5.54 % (3587260)Instruction limit reached!
% 30.28/5.54 % (3587260)------------------------------
% 30.28/5.54 % (3587260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587260)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587260)Termination reason: Instruction limit
% 30.28/5.54 % (3587260)Termination phase: Saturation
% 30.28/5.54 % (3587260)Time elapsed: 0.087 s
% 30.28/5.54 % (3587260)Peak memory usage: 90 MB
% 30.28/5.54 % (3587260)Instructions burned: 147 (million)
% 30.28/5.54 % (3587263)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2904703556:i=1052:rtra=on_2960 on theBenchmark for (2960ds/1052Mi)
% 30.28/5.54 % (3587261)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2064733363:i=4428:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/4428Mi)
% 30.28/5.54 % (3587262)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=830383133:avsq=on:i=276:avsqr=1,2:rtra=on_2960 on theBenchmark for (2960ds/276Mi)
% 30.28/5.54 % (3587265)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=23742044:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/655Mi)
% 30.28/5.54 % (3587266)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1972992945:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2960 on theBenchmark for (2960ds/1054Mi)
% 30.28/5.54 % (3587267)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=799600581:i=107:rtra=on_2959 on theBenchmark for (2959ds/107Mi)
% 30.28/5.54 % (3587262)Refutation not found, SMT solver inside AVATAR returned Unknown
% 30.28/5.54 % (3587262)------------------------------
% 30.28/5.54 % (3587262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/5.54 % (3587262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/5.54 % (3587262)CaDiCaL version: 2.1.3
% 30.28/5.54 % (3587262)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 30.28/5.54 % (3587262)Time elapsed: 0.116 s
% 30.28/5.54 % (3587262)Peak memory usage: 134 MB
% 30.28/5.54 % (3587262)Instructions burned: 45 (million)
% 30.28/5.54 % (3587262)------------------------------
% 30.28/5.54 % (3587262)------------------------------
% 30.28/5.54 % (3587253)Refutation found. Thanks to Tanya!
% 30.28/5.54 % SZS status Theorem for theBenchmark
% 30.28/5.54 % SZS output start Proof for theBenchmark
% See solution above
% 30.95/5.76 % (3587253)------------------------------
% 30.95/5.76 % (3587253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/5.76 % (3587253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/5.76 % (3587253)CaDiCaL version: 2.1.3
% 30.95/5.76 % (3587253)Termination reason: Refutation
% 30.95/5.76 % (3587253)Time elapsed: 0.153 s
% 30.95/5.76 % (3587253)Peak memory usage: 118 MB
% 30.95/5.76 % (3587253)Instructions burned: 115 (million)
% 30.95/5.76 % (3587253)------------------------------
% 30.95/5.76 % (3587253)------------------------------
% 30.95/5.76 % (3587071)Success in time 4.59 s
% 30.95/5.76 % Vampire exiting
%------------------------------------------------------------------------------