%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW589_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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:52 PM UTC 2026
% Result : Theorem 7.20s 1.90s
% Output : Refutation 9.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 17
% Syntax : Number of formulae : 74 ( 15 unt; 0 typ; 11 def)
% Number of atoms : 315 ( 86 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 380 ( 139 ~; 76 |; 96 &)
% ( 11 <=>; 58 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 441 ( 131 atm; 126 fun; 143 num; 41 var)
% Number of types : 10 ( 8 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 19 usr; 12 prp; 0-5 aty)
% Number of functors : 81 ( 76 usr; 19 con; 0-5 aty)
% Number of variables : 150 ( 126 !; 24 ?; 150 :)
% 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,
char1: $tType ).
tff(type_def_10,type,
list_char: $tType ).
tff(type_def_11,type,
array_char: $tType ).
tff(type_def_12,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,
min1: ( $int * $int ) > $int ).
tff(func_def_13,type,
max1: ( $int * $int ) > $int ).
tff(func_def_14,type,
list: ty > ty ).
tff(func_def_15,type,
nil: ty > uni ).
tff(func_def_16,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_17,type,
match_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(func_def_19,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(func_def_20,type,
length2: ( ty * uni ) > $int ).
tff(func_def_23,type,
char: ty ).
tff(func_def_24,type,
t2tb: list_char > uni ).
tff(func_def_25,type,
tb2t: uni > list_char ).
tff(func_def_26,type,
t2tb1: char1 > uni ).
tff(func_def_27,type,
tb2t1: uni > char1 ).
tff(func_def_28,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_29,type,
last_char1: ( char1 * list_char ) > char1 ).
tff(func_def_30,type,
but_last1: ( char1 * list_char ) > list_char ).
tff(func_def_31,type,
ref: ty > ty ).
tff(func_def_32,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_33,type,
contents: ( ty * uni ) > uni ).
tff(func_def_34,type,
map: ( ty * ty ) > ty ).
tff(func_def_35,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_36,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_37,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_38,type,
array: ty > ty ).
tff(func_def_39,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_40,type,
length3: ( ty * uni ) > $int ).
tff(func_def_41,type,
elts: ( ty * uni ) > uni ).
tff(func_def_42,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_43,type,
t2tb2: $int > uni ).
tff(func_def_44,type,
tb2t2: uni > $int ).
tff(func_def_45,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_46,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_47,type,
suffix1: ( array_char * $int ) > list_char ).
tff(func_def_48,type,
t2tb3: array_char > uni ).
tff(func_def_49,type,
tb2t3: uni > array_char ).
tff(func_def_51,type,
t2tb5: map_int_int > uni ).
tff(func_def_52,type,
tb2t5: uni > map_int_int ).
tff(func_def_54,type,
sK3: $int ).
tff(func_def_55,type,
sK4: $int ).
tff(func_def_56,type,
sK5: uni ).
tff(func_def_57,type,
sK6: uni ).
tff(func_def_58,type,
sK7: $int ).
tff(func_def_59,type,
sK8: map_int_int ).
tff(func_def_60,type,
sK9: map_int_int ).
tff(func_def_61,type,
sK10: $int ).
tff(func_def_62,type,
sK11: ( $int * list_char * list_char ) > $int ).
tff(func_def_63,type,
sK12: ( $int * list_char * list_char ) > list_char ).
tff(func_def_64,type,
sK13: ( $int * list_char * list_char ) > list_char ).
tff(func_def_65,type,
sK14: ( $int * list_char * list_char ) > char1 ).
tff(func_def_66,type,
sK15: ( $int * list_char * list_char ) > list_char ).
tff(func_def_67,type,
sK16: ( $int * list_char * list_char ) > list_char ).
tff(func_def_68,type,
sK17: ( $int * list_char * list_char ) > $int ).
tff(func_def_69,type,
sK18: ( $int * list_char * list_char ) > char1 ).
tff(func_def_70,type,
sK19: ( $int * list_char * list_char ) > $int ).
tff(func_def_71,type,
sK20: ( $int * list_char * list_char ) > list_char ).
tff(func_def_72,type,
sK21: ( $int * list_char * list_char ) > list_char ).
tff(func_def_73,type,
sK22: ( $int * list_char * list_char ) > char1 ).
tff(func_def_74,type,
sK23: ( list_char * list_char * $int ) > list_char ).
tff(func_def_75,type,
sK24: ( list_char * list_char * $int ) > $int ).
tff(func_def_76,type,
sK25: ( list_char * list_char * $int ) > list_char ).
tff(func_def_77,type,
sK26: ( char1 * list_char ) > list_char ).
tff(func_def_78,type,
sK27: ( char1 * list_char ) > char1 ).
tff(func_def_79,type,
sK28: ( list_char * $int * list_char ) > $int ).
tff(func_def_80,type,
sK29: ( list_char * $int * list_char ) > list_char ).
tff(func_def_81,type,
sK30: ( list_char * $int * list_char ) > list_char ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
dist1: ( list_char * list_char * $int ) > $o ).
tff(pred_def_4,type,
min_dist1: ( list_char * list_char * $int ) > $o ).
tff(pred_def_5,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_7,type,
min_suffix1: ( array_char * array_char * $int * $int * $int ) > $o ).
tff(pred_def_8,type,
sP0: ( $int * list_char * list_char ) > $o ).
tff(pred_def_9,type,
sP1: ( $int * list_char * list_char ) > $o ).
tff(pred_def_10,type,
sP2: ( $int * list_char * list_char ) > $o ).
tff(f72,axiom,
! [X1: ty,X5: uni,X2: uni,X0: ty,X3: uni,X4: uni] :
( sort1(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_eq) ).
tff(f73,axiom,
! [X2: uni,X1: ty,X4: uni,X0: ty,X3: uni] :
( sort1(X0,X3)
=> ( sort1(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_neq) ).
tff(f82,axiom,
! [X0: $int] : sort1(int,t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort8) ).
tff(f83,axiom,
! [X0: $int] : ( tb2t2(t2tb2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL2) ).
tff(f99,axiom,
! [X0: uni] : ( t2tb5(tb2t5(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR5) ).
tff(f100,conjecture,
! [X0: $int,X2: $int,X1: uni,X3: uni] :
( sort1(map(int,char),X1)
=> ( sort1(map(int,char),X3)
=> ( ( $lesseq(0,X2)
& $lesseq(0,X0) )
=> ( $lesseq(0,$sum(X2,1))
=> ( $lesseq(0,$sum(X2,1))
=> ( $lesseq(0,X2)
=> ! [X5: $int,X4: map_int_int] :
( ( $lesseq(X5,X2)
& $lesseq(0,X5) )
=> ( ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X5) )
=> ( tb2t2(get(int,int,t2tb5(X4),t2tb2(X6))) = $difference(X2,X6) ) )
=> ( ( $lesseq(0,$sum(X2,1))
& $less(X5,$sum(X2,1))
& $lesseq(0,X5) )
=> ! [X7: map_int_int] :
( ( ( X7 = tb2t5(set(int,int,t2tb5(X4),t2tb2(X5),t2tb2($difference(X2,X5)))) )
& $lesseq(0,$sum(X2,1)) )
=> ! [X6: $int] :
( ( $less(X6,$sum(X5,1))
& $lesseq(0,X6) )
=> ( tb2t2(get(int,int,t2tb5(X7),t2tb2(X6))) = $difference(X2,X6) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_distance) ).
tff(f101,negated_conjecture,
~ ! [X0: $int,X2: $int,X1: uni,X3: uni] :
( sort1(map(int,char),X1)
=> ( sort1(map(int,char),X3)
=> ( ( $lesseq(0,X2)
& $lesseq(0,X0) )
=> ( $lesseq(0,$sum(X2,1))
=> ( $lesseq(0,$sum(X2,1))
=> ( $lesseq(0,X2)
=> ! [X5: $int,X4: map_int_int] :
( ( $lesseq(X5,X2)
& $lesseq(0,X5) )
=> ( ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X5) )
=> ( tb2t2(get(int,int,t2tb5(X4),t2tb2(X6))) = $difference(X2,X6) ) )
=> ( ( $lesseq(0,$sum(X2,1))
& $less(X5,$sum(X2,1))
& $lesseq(0,X5) )
=> ! [X7: map_int_int] :
( ( ( X7 = tb2t5(set(int,int,t2tb5(X4),t2tb2(X5),t2tb2($difference(X2,X5)))) )
& $lesseq(0,$sum(X2,1)) )
=> ! [X6: $int] :
( ( $less(X6,$sum(X5,1))
& $lesseq(0,X6) )
=> ( tb2t2(get(int,int,t2tb5(X7),t2tb2(X6))) = $difference(X2,X6) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f100]) ).
tff(f113,plain,
~ ! [X0: $int,X2: $int,X1: uni,X3: uni] :
( sort1(map(int,char),X1)
=> ( sort1(map(int,char),X3)
=> ( ( ~ $less(X2,0)
& ~ $less(X0,0) )
=> ( ~ $less($sum(X2,1),0)
=> ( ~ $less($sum(X2,1),0)
=> ( ~ $less(X2,0)
=> ! [X5: $int,X4: map_int_int] :
( ( ~ $less(X2,X5)
& ~ $less(X5,0) )
=> ( ! [X6: $int] :
( ( ~ $less(X6,0)
& $less(X6,X5) )
=> ( tb2t2(get(int,int,t2tb5(X4),t2tb2(X6))) = $sum(X2,$uminus(X6)) ) )
=> ( ( ~ $less($sum(X2,1),0)
& $less(X5,$sum(X2,1))
& ~ $less(X5,0) )
=> ! [X7: map_int_int] :
( ( ( tb2t5(set(int,int,t2tb5(X4),t2tb2(X5),t2tb2($sum(X2,$uminus(X5))))) = X7 )
& ~ $less($sum(X2,1),0) )
=> ! [X6: $int] :
( ( $less(X6,$sum(X5,1))
& ~ $less(X6,0) )
=> ( tb2t2(get(int,int,t2tb5(X7),t2tb2(X6))) = $sum(X2,$uminus(X6)) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f101]) ).
tff(f118,plain,
~ ! [X3: uni,X0: $int,X1: $int,X2: uni] :
( sort1(map(int,char),X2)
=> ( sort1(map(int,char),X3)
=> ( ( ~ $less(X1,0)
& ~ $less(X0,0) )
=> ( ~ $less($sum(X1,1),0)
=> ( ~ $less($sum(X1,1),0)
=> ( ~ $less(X1,0)
=> ! [X4: $int,X5: map_int_int] :
( ( ~ $less(X4,0)
& ~ $less(X1,X4) )
=> ( ! [X6: $int] :
( ( $less(X6,X4)
& ~ $less(X6,0) )
=> ( $sum(X1,$uminus(X6)) = tb2t2(get(int,int,t2tb5(X5),t2tb2(X6))) ) )
=> ( ( $less(X4,$sum(X1,1))
& ~ $less($sum(X1,1),0)
& ~ $less(X4,0) )
=> ! [X7: map_int_int] :
( ( ~ $less($sum(X1,1),0)
& ( tb2t5(set(int,int,t2tb5(X5),t2tb2(X4),t2tb2($sum(X1,$uminus(X4))))) = X7 ) )
=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,$sum(X4,1)) )
=> ( tb2t2(get(int,int,t2tb5(X7),t2tb2(X8))) = $sum(X1,$uminus(X8)) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f113]) ).
tff(f126,plain,
! [X1: ty,X3: ty,X2: uni,X0: uni,X4: uni] :
( sort1(X3,X4)
=> ( sort1(X3,X2)
=> ! [X5: uni] :
( ( X2 != X4 )
=> ( get(X1,X3,set(X1,X3,X0,X4,X5),X2) = get(X1,X3,X0,X2) ) ) ) ),
inference(rectify,[],[f73]) ).
tff(f127,plain,
! [X0: ty,X3: ty,X5: uni,X4: uni,X2: uni,X1: uni] :
( sort1(X0,X1)
=> ( ( X4 = X5 )
=> ( get(X0,X3,set(X0,X3,X2,X4,X1),X5) = X1 ) ) ),
inference(rectify,[],[f72]) ).
tff(f144,plain,
! [X1: ty,X3: ty,X2: uni,X0: uni,X4: uni] :
( ! [X5: uni] :
( ( X2 = X4 )
| ( get(X1,X3,set(X1,X3,X0,X4,X5),X2) = get(X1,X3,X0,X2) ) )
| ~ sort1(X3,X2)
| ~ sort1(X3,X4) ),
inference(ennf_transformation,[],[f126]) ).
tff(f145,plain,
! [X3: ty,X1: ty,X2: uni,X4: uni,X0: uni] :
( ~ sort1(X3,X2)
| ~ sort1(X3,X4)
| ! [X5: uni] :
( ( X2 = X4 )
| ( get(X1,X3,set(X1,X3,X0,X4,X5),X2) = get(X1,X3,X0,X2) ) ) ),
inference(flattening,[],[f144]) ).
tff(f146,plain,
? [X3: uni,X0: $int,X1: $int,X2: uni] :
( ? [X4: $int,X5: map_int_int] :
( ? [X7: map_int_int] :
( ? [X8: $int] :
( ( tb2t2(get(int,int,t2tb5(X7),t2tb2(X8))) != $sum(X1,$uminus(X8)) )
& ~ $less(X8,0)
& $less(X8,$sum(X4,1)) )
& ~ $less($sum(X1,1),0)
& ( tb2t5(set(int,int,t2tb5(X5),t2tb2(X4),t2tb2($sum(X1,$uminus(X4))))) = X7 ) )
& $less(X4,$sum(X1,1))
& ~ $less($sum(X1,1),0)
& ~ $less(X4,0)
& ! [X6: $int] :
( ( $sum(X1,$uminus(X6)) = tb2t2(get(int,int,t2tb5(X5),t2tb2(X6))) )
| ~ $less(X6,X4)
| $less(X6,0) )
& ~ $less(X4,0)
& ~ $less(X1,X4) )
& ~ $less(X1,0)
& ~ $less($sum(X1,1),0)
& ~ $less($sum(X1,1),0)
& ~ $less(X1,0)
& ~ $less(X0,0)
& sort1(map(int,char),X3)
& sort1(map(int,char),X2) ),
inference(ennf_transformation,[],[f118]) ).
tff(f147,plain,
? [X1: $int,X0: $int,X3: uni,X2: uni] :
( sort1(map(int,char),X2)
& ~ $less(X1,0)
& sort1(map(int,char),X3)
& ? [X4: $int,X5: map_int_int] :
( ~ $less(X4,0)
& ~ $less($sum(X1,1),0)
& $less(X4,$sum(X1,1))
& ? [X7: map_int_int] :
( ( tb2t5(set(int,int,t2tb5(X5),t2tb2(X4),t2tb2($sum(X1,$uminus(X4))))) = X7 )
& ? [X8: $int] :
( $less(X8,$sum(X4,1))
& ( tb2t2(get(int,int,t2tb5(X7),t2tb2(X8))) != $sum(X1,$uminus(X8)) )
& ~ $less(X8,0) )
& ~ $less($sum(X1,1),0) )
& ~ $less(X4,0)
& ! [X6: $int] :
( $less(X6,0)
| ( $sum(X1,$uminus(X6)) = tb2t2(get(int,int,t2tb5(X5),t2tb2(X6))) )
| ~ $less(X6,X4) )
& ~ $less(X1,X4) )
& ~ $less(X1,0)
& ~ $less(X0,0)
& ~ $less($sum(X1,1),0)
& ~ $less($sum(X1,1),0) ),
inference(flattening,[],[f146]) ).
tff(f148,plain,
! [X0: ty,X3: ty,X5: uni,X4: uni,X2: uni,X1: uni] :
( ( get(X0,X3,set(X0,X3,X2,X4,X1),X5) = X1 )
| ( X4 != X5 )
| ~ sort1(X0,X1) ),
inference(ennf_transformation,[],[f127]) ).
tff(f149,plain,
! [X2: uni,X0: ty,X1: uni,X5: uni,X3: ty,X4: uni] :
( ~ sort1(X0,X1)
| ( X4 != X5 )
| ( get(X0,X3,set(X0,X3,X2,X4,X1),X5) = X1 ) ),
inference(flattening,[],[f148]) ).
tff(f163,plain,
! [X0: ty,X1: ty,X2: uni,X3: uni,X4: uni] :
( ~ sort1(X0,X2)
| ~ sort1(X0,X3)
| ! [X5: uni] :
( ( X2 = X3 )
| ( get(X1,X0,X4,X2) = get(X1,X0,set(X1,X0,X4,X3,X5),X2) ) ) ),
inference(rectify,[],[f145]) ).
tff(f164,plain,
? [X0: $int,X1: $int,X2: uni,X3: uni] :
( sort1(map(int,char),X3)
& ~ $less(X0,0)
& sort1(map(int,char),X2)
& ? [X4: $int,X5: map_int_int] :
( ~ $less(X4,0)
& ~ $less($sum(X0,1),0)
& $less(X4,$sum(X0,1))
& ? [X6: map_int_int] :
( ( tb2t5(set(int,int,t2tb5(X5),t2tb2(X4),t2tb2($sum(X0,$uminus(X4))))) = X6 )
& ? [X7: $int] :
( $less(X7,$sum(X4,1))
& ( tb2t2(get(int,int,t2tb5(X6),t2tb2(X7))) != $sum(X0,$uminus(X7)) )
& ~ $less(X7,0) )
& ~ $less($sum(X0,1),0) )
& ~ $less(X4,0)
& ! [X8: $int] :
( $less(X8,0)
| ( $sum(X0,$uminus(X8)) = tb2t2(get(int,int,t2tb5(X5),t2tb2(X8))) )
| ~ $less(X8,X4) )
& ~ $less(X0,X4) )
& ~ $less(X0,0)
& ~ $less(X1,0)
& ~ $less($sum(X0,1),0)
& ~ $less($sum(X0,1),0) ),
inference(rectify,[],[f147]) ).
tff(f165,plain,
( sort1(map(int,char),sK6)
& ~ $less(sK3,0)
& sort1(map(int,char),sK5)
& ~ $less(sK7,0)
& ~ $less($sum(sK3,1),0)
& $less(sK7,$sum(sK3,1))
& ( sK9 = tb2t5(set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7))))) )
& $less(sK10,$sum(sK7,1))
& ( tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) != $sum(sK3,$uminus(sK10)) )
& ~ $less(sK10,0)
& ~ $less($sum(sK3,1),0)
& ~ $less(sK7,0)
& ! [X8: $int] :
( $less(X8,0)
| ( tb2t2(get(int,int,t2tb5(sK8),t2tb2(X8))) = $sum(sK3,$uminus(X8)) )
| ~ $less(X8,sK7) )
& ~ $less(sK3,sK7)
& ~ $less(sK3,0)
& ~ $less(sK4,0)
& ~ $less($sum(sK3,1),0)
& ~ $less($sum(sK3,1),0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7),skolemize(X5,sK8),skolemize(X6,sK9),skolemize(X7,sK10)],[f164]) ).
tff(f192,plain,
! [X0: uni,X1: ty,X2: uni,X3: uni,X4: ty,X5: uni] :
( ~ sort1(X1,X2)
| ( X3 != X5 )
| ( get(X1,X4,set(X1,X4,X0,X5,X2),X3) = X2 ) ),
inference(rectify,[],[f149]) ).
tff(f198,plain,
! [X2: uni,X3: uni,X0: ty,X1: ty,X4: uni,X5: uni] :
( ( get(X1,X0,X4,X2) = get(X1,X0,set(X1,X0,X4,X3,X5),X2) )
| ~ sort1(X0,X2)
| ~ sort1(X0,X3)
| ( X2 = X3 ) ),
inference(cnf_transformation,[],[f163]) ).
tff(f204,plain,
! [X8: $int] :
( ( tb2t2(get(int,int,t2tb5(sK8),t2tb2(X8))) = $sum(sK3,$uminus(X8)) )
| $less(X8,0)
| ~ $less(X8,sK7) ),
inference(cnf_transformation,[],[f165]) ).
tff(f207,plain,
~ $less(sK10,0),
inference(cnf_transformation,[],[f165]) ).
tff(f208,plain,
tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) != $sum(sK3,$uminus(sK10)),
inference(cnf_transformation,[],[f165]) ).
tff(f209,plain,
$less(sK10,$sum(sK7,1)),
inference(cnf_transformation,[],[f165]) ).
tff(f210,plain,
sK9 = tb2t5(set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7))))),
inference(cnf_transformation,[],[f165]) ).
tff(f220,plain,
! [X0: $int] : ( tb2t2(t2tb2(X0)) = X0 ),
inference(cnf_transformation,[],[f83]) ).
tff(f226,plain,
! [X0: $int] : sort1(int,t2tb2(X0)),
inference(cnf_transformation,[],[f82]) ).
tff(f250,plain,
! [X0: uni] : ( t2tb5(tb2t5(X0)) = X0 ),
inference(cnf_transformation,[],[f99]) ).
tff(f266,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty,X4: ty,X5: uni] :
( ~ sort1(X1,X2)
| ( X3 != X5 )
| ( get(X1,X4,set(X1,X4,X0,X5,X2),X3) = X2 ) ),
inference(cnf_transformation,[],[f192]) ).
tff(f272,plain,
! [X2: uni,X0: uni,X1: ty,X4: ty,X5: uni] :
( ( get(X1,X4,set(X1,X4,X0,X5,X2),X5) = X2 )
| ~ sort1(X1,X2) ),
inference(equality_resolution,[],[f266]) ).
tff(f302,definition,
( spl31_6
<=> ( tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) = $sum(sK3,$uminus(sK10)) ) ),
introduced(definition,[new_symbols(definition,[spl31_6])],[avatar_definition]) ).
tff(f304,plain,
( ( tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) != $sum(sK3,$uminus(sK10)) )
| spl31_6 ),
inference(avatar_component_clause,[],[f302]) ).
tff(f305,plain,
~ spl31_6,
inference(avatar_split_clause,[],[f208,f302]) ).
tff(f312,definition,
( spl31_8
<=> $less(sK10,0) ),
introduced(definition,[new_symbols(definition,[spl31_8])],[avatar_definition]) ).
tff(f314,plain,
( ~ $less(sK10,0)
| spl31_8 ),
inference(avatar_component_clause,[],[f312]) ).
tff(f315,plain,
~ spl31_8,
inference(avatar_split_clause,[],[f207,f312]) ).
tff(f317,definition,
( spl31_9
<=> $less(sK10,$sum(sK7,1)) ),
introduced(definition,[new_symbols(definition,[spl31_9])],[avatar_definition]) ).
tff(f320,plain,
spl31_9,
inference(avatar_split_clause,[],[f209,f317]) ).
tff(f327,definition,
( spl31_11
<=> ( sK9 = tb2t5(set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7))))) ) ),
introduced(definition,[new_symbols(definition,[spl31_11])],[avatar_definition]) ).
tff(f329,plain,
( ( sK9 = tb2t5(set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7))))) )
| ~ spl31_11 ),
inference(avatar_component_clause,[],[f327]) ).
tff(f330,plain,
spl31_11,
inference(avatar_split_clause,[],[f210,f327]) ).
tff(f338,plain,
( ( t2tb5(sK9) = set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7)))) )
| ~ spl31_11 ),
inference(superposition,[],[f250,f329]) ).
tff(f340,definition,
( spl31_13
<=> ( t2tb5(sK9) = set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7)))) ) ),
introduced(definition,[new_symbols(definition,[spl31_13])],[avatar_definition]) ).
tff(f342,plain,
( ( t2tb5(sK9) = set(int,int,t2tb5(sK8),t2tb2(sK7),t2tb2($sum(sK3,$uminus(sK7)))) )
| ~ spl31_13 ),
inference(avatar_component_clause,[],[f340]) ).
tff(f343,plain,
( spl31_13
| ~ spl31_11 ),
inference(avatar_split_clause,[],[f338,f327,f340]) ).
tff(f345,plain,
( ! [X0: uni] :
( ~ sort1(int,X0)
| ( t2tb2(sK7) = X0 )
| ~ sort1(int,t2tb2(sK7))
| ( get(int,int,t2tb5(sK8),X0) = get(int,int,t2tb5(sK9),X0) ) )
| ~ spl31_13 ),
inference(superposition,[],[f198,f342]) ).
tff(f347,plain,
( ~ sort1(int,t2tb2($sum(sK3,$uminus(sK7))))
| ( get(int,int,t2tb5(sK9),t2tb2(sK7)) = t2tb2($sum(sK3,$uminus(sK7))) )
| ~ spl31_13 ),
inference(superposition,[],[f272,f342]) ).
tff(f348,plain,
( ! [X0: uni] :
( ( get(int,int,t2tb5(sK8),X0) = get(int,int,t2tb5(sK9),X0) )
| ( t2tb2(sK7) = X0 )
| ~ sort1(int,X0) )
| ~ spl31_13 ),
inference(forward_subsumption_resolution,[],[f345,f226]) ).
tff(f349,plain,
( ( get(int,int,t2tb5(sK9),t2tb2(sK7)) = t2tb2($sum(sK3,$uminus(sK7))) )
| ~ spl31_13 ),
inference(forward_subsumption_resolution,[],[f347,f226]) ).
tff(f351,definition,
( spl31_14
<=> ( get(int,int,t2tb5(sK9),t2tb2(sK7)) = t2tb2($sum(sK3,$uminus(sK7))) ) ),
introduced(definition,[new_symbols(definition,[spl31_14])],[avatar_definition]) ).
tff(f353,plain,
( ( get(int,int,t2tb5(sK9),t2tb2(sK7)) = t2tb2($sum(sK3,$uminus(sK7))) )
| ~ spl31_14 ),
inference(avatar_component_clause,[],[f351]) ).
tff(f354,plain,
( spl31_14
| ~ spl31_13 ),
inference(avatar_split_clause,[],[f349,f340,f351]) ).
tff(f355,plain,
( $less(sK10,0)
| ( tb2t2(get(int,int,t2tb5(sK8),t2tb2(sK10))) != tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) )
| ~ $less(sK10,sK7)
| spl31_6 ),
inference(superposition,[],[f304,f204]) ).
tff(f359,plain,
( ~ $less(sK10,sK7)
| ( tb2t2(get(int,int,t2tb5(sK8),t2tb2(sK10))) != tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) )
| spl31_6
| spl31_8 ),
inference(forward_subsumption_resolution,[],[f355,f314]) ).
tff(f363,definition,
( spl31_15
<=> ( tb2t2(get(int,int,t2tb5(sK8),t2tb2(sK10))) = tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) ) ),
introduced(definition,[new_symbols(definition,[spl31_15])],[avatar_definition]) ).
tff(f365,plain,
( ( tb2t2(get(int,int,t2tb5(sK8),t2tb2(sK10))) != tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) )
| spl31_15 ),
inference(avatar_component_clause,[],[f363]) ).
tff(f367,definition,
( spl31_16
<=> $less(sK10,sK7) ),
introduced(definition,[new_symbols(definition,[spl31_16])],[avatar_definition]) ).
tff(f370,plain,
( ~ spl31_15
| ~ spl31_16
| spl31_6
| spl31_8 ),
inference(avatar_split_clause,[],[f359,f312,f302,f367,f363]) ).
tff(f391,plain,
( ( $sum(sK3,$uminus(sK7)) = tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK7))) )
| ~ spl31_14 ),
inference(superposition,[],[f220,f353]) ).
tff(f393,definition,
( spl31_20
<=> ( $sum(sK3,$uminus(sK7)) = tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK7))) ) ),
introduced(definition,[new_symbols(definition,[spl31_20])],[avatar_definition]) ).
tff(f396,plain,
( spl31_20
| ~ spl31_14 ),
inference(avatar_split_clause,[],[f391,f351,f393]) ).
tff(f419,plain,
( ~ sort1(int,t2tb2(sK10))
| ( t2tb2(sK7) = t2tb2(sK10) )
| ( tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) != tb2t2(get(int,int,t2tb5(sK9),t2tb2(sK10))) )
| ~ spl31_13
| spl31_15 ),
inference(superposition,[],[f365,f348]) ).
tff(f421,plain,
( ~ sort1(int,t2tb2(sK10))
| ( t2tb2(sK7) = t2tb2(sK10) )
| ~ spl31_13
| spl31_15 ),
inference(trivial_inequality_removal,[],[f419]) ).
tff(f422,plain,
( ( t2tb2(sK7) = t2tb2(sK10) )
| ~ spl31_13
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f421,f226]) ).
tff(f424,definition,
( spl31_23
<=> ( t2tb2(sK7) = t2tb2(sK10) ) ),
introduced(definition,[new_symbols(definition,[spl31_23])],[avatar_definition]) ).
tff(f426,plain,
( ( t2tb2(sK7) = t2tb2(sK10) )
| ~ spl31_23 ),
inference(avatar_component_clause,[],[f424]) ).
tff(f427,plain,
( spl31_23
| ~ spl31_13
| spl31_15 ),
inference(avatar_split_clause,[],[f422,f363,f340,f424]) ).
tff(f430,plain,
( ( sK10 = tb2t2(t2tb2(sK7)) )
| ~ spl31_23 ),
inference(superposition,[],[f220,f426]) ).
tff(f431,plain,
( ( sK10 = sK7 )
| ~ spl31_23 ),
inference(forward_demodulation,[],[f430,f220]) ).
tff(f438,definition,
( spl31_25
<=> ( sK10 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl31_25])],[avatar_definition]) ).
tff(f441,plain,
( spl31_25
| ~ spl31_23 ),
inference(avatar_split_clause,[],[f431,f424,f438]) ).
tff(f442,plain,
$false,
inference(avatar_smt_refutation,[],[f441,f427,f396,f370,f354,f343,f330,f320,f315,f305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW589_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 14:21:18 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 3.48/1.21 % (4028988)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.48/1.21 % (4029016)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=353439424:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.48/1.21 % (4029016)Instruction limit reached!
% 3.48/1.21 % (4029016)------------------------------
% 3.48/1.21 % (4029016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.21 % (4029016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.21 % (4029016)CaDiCaL version: 2.1.3
% 3.48/1.21 % (4029016)Termination reason: Instruction limit
% 3.48/1.21 % (4029016)Termination phase: Property scanning
% 3.48/1.21 % (4029016)Time elapsed: 0.003 s
% 3.48/1.21 % (4029016)Peak memory usage: 87 MB
% 3.48/1.21 % (4029016)Instructions burned: 9 (million)
% 3.48/1.21 % (4029017)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2714417961:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.48/1.21 % (4029018)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1733557887:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.48/1.21 % (4029013)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=805969046:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.48/1.21 % (4029015)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4185157884:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.48/1.21 % (4029014)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=786217504:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.48/1.21 % (4029019)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1697892169:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.48/1.21 % (4029017)Instruction limit reached!
% 3.48/1.21 % (4029017)------------------------------
% 3.48/1.21 % (4029017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.21 % (4029017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.21 % (4029017)CaDiCaL version: 2.1.3
% 3.48/1.21 % (4029017)Termination reason: Instruction limit
% 3.48/1.21 % (4029017)Termination phase: Preprocessing 3
% 3.48/1.21 % (4029017)Time elapsed: 0.003 s
% 3.48/1.21 % (4029017)Peak memory usage: 86 MB
% 3.48/1.21 % (4029017)Instructions burned: 4 (million)
% 3.48/1.21 % (4029013)Instruction limit reached!
% 3.48/1.21 % (4029013)------------------------------
% 3.48/1.21 % (4029013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.21 % (4029013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.21 % (4029013)CaDiCaL version: 2.1.3
% 3.48/1.21 % (4029013)Termination reason: Instruction limit
% 3.48/1.21 % (4029013)Termination phase: Saturation
% 3.48/1.21 % (4029013)Time elapsed: 0.030 s
% 3.48/1.21 % (4029013)Peak memory usage: 113 MB
% 3.48/1.21 % (4029013)Instructions burned: 13 (million)
% 3.48/1.21 % (4029019)Instruction limit reached!
% 3.48/1.21 % (4029019)------------------------------
% 3.48/1.21 % (4029019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.21 % (4029019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.21 % (4029019)CaDiCaL version: 2.1.3
% 3.48/1.21 % (4029019)Termination reason: Instruction limit
% 3.48/1.21 % (4029019)Termination phase: Saturation
% 3.48/1.21 % (4029019)Time elapsed: 0.045 s
% 3.48/1.21 % (4029019)Peak memory usage: 116 MB
% 3.48/1.21 % (4029019)Instructions burned: 34 (million)
% 3.48/1.21 % (4029018)Instruction limit reached!
% 3.48/1.21 % (4029018)------------------------------
% 3.48/1.21 % (4029018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.21 % (4029018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.21 % (4029018)CaDiCaL version: 2.1.3
% 3.48/1.21 % (4029018)Termination reason: Instruction limit
% 3.48/1.21 % (4029018)Termination phase: Saturation
% 3.48/1.21 % (4029018)Time elapsed: 0.054 s
% 3.48/1.21 % (4029018)Peak memory usage: 116 MB
% 3.48/1.21 % (4029018)Instructions burned: 46 (million)
% 3.48/1.21 % (4029021)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3253921813:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.48/1.21 % (4029021)Instruction limit reached!
% 3.48/1.21 % (4029021)------------------------------
% 4.47/1.39 % (4029021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (4029021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (4029021)CaDiCaL version: 2.1.3
% 4.47/1.39 % (4029021)Termination reason: Instruction limit
% 4.47/1.39 % (4029021)Termination phase: Saturation
% 4.47/1.39 % (4029021)Time elapsed: 0.006 s
% 4.47/1.39 % (4029021)Peak memory usage: 89 MB
% 4.47/1.39 % (4029021)Instructions burned: 17 (million)
% 4.47/1.39 % (4029015)Instruction limit reached!
% 4.47/1.39 % (4029015)------------------------------
% 4.47/1.39 % (4029015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (4029015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (4029015)CaDiCaL version: 2.1.3
% 4.47/1.39 % (4029015)Termination reason: Instruction limit
% 4.47/1.39 % (4029015)Termination phase: Saturation
% 4.47/1.39 % (4029015)Time elapsed: 0.153 s
% 4.47/1.39 % (4029015)Peak memory usage: 118 MB
% 4.47/1.39 % (4029015)Instructions burned: 201 (million)
% 4.47/1.39 % (4029028)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=4254603831:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.47/1.39 % (4029028)Instruction limit reached!
% 4.47/1.39 % (4029028)------------------------------
% 4.47/1.39 % (4029028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (4029028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (4029028)CaDiCaL version: 2.1.3
% 4.47/1.39 % (4029028)Termination reason: Instruction limit
% 4.47/1.39 % (4029028)Termination phase: Saturation
% 4.47/1.39 % (4029028)Time elapsed: 0.015 s
% 4.47/1.39 % (4029028)Peak memory usage: 89 MB
% 4.47/1.39 % (4029028)Instructions burned: 29 (million)
% 4.47/1.39 % (4029030)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=115795278:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.47/1.39 % (4029029)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=690570358:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.47/1.39 % (4029029)Instruction limit reached!
% 4.47/1.39 % (4029029)------------------------------
% 4.47/1.39 % (4029029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (4029029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (4029029)CaDiCaL version: 2.1.3
% 4.47/1.39 % (4029029)Termination reason: Instruction limit
% 4.47/1.39 % (4029029)Termination phase: Saturation
% 4.47/1.39 % (4029029)Time elapsed: 0.010 s
% 4.47/1.39 % (4029029)Peak memory usage: 89 MB
% 4.47/1.39 % (4029029)Instructions burned: 16 (million)
% 4.47/1.39 % (4029014)Instruction limit reached!
% 4.47/1.39 % (4029014)------------------------------
% 4.47/1.39 % (4029014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (4029014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (4029014)CaDiCaL version: 2.1.3
% 4.47/1.39 % (4029014)Termination reason: Instruction limit
% 4.47/1.39 % (4029014)Termination phase: Saturation
% 4.47/1.39 % (4029014)Time elapsed: 0.204 s
% 4.47/1.39 % (4029014)Peak memory usage: 117 MB
% 4.47/1.39 % (4029014)Instructions burned: 308 (million)
% 4.47/1.39 % (4029030)Instruction limit reached!
% 4.47/1.39 % (4029030)------------------------------
% 4.47/1.39 % (4029030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (4029030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (4029030)CaDiCaL version: 2.1.3
% 4.47/1.39 % (4029030)Termination reason: Instruction limit
% 4.47/1.39 % (4029030)Termination phase: Saturation
% 4.47/1.39 % (4029030)Time elapsed: 0.018 s
% 4.47/1.39 % (4029030)Peak memory usage: 89 MB
% 4.47/1.39 % (4029030)Instructions burned: 24 (million)
% 4.47/1.39 % (4029031)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=3278513732:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.47/1.39 % (4029033)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1244069859:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.47/1.39 % (4029031)Instruction limit reached!
% 4.47/1.39 % (4029031)------------------------------
% 4.47/1.39 % (4029031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.58 % (4029031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.58 % (4029031)CaDiCaL version: 2.1.3
% 5.82/1.58 % (4029031)Termination reason: Instruction limit
% 5.82/1.58 % (4029031)Termination phase: Saturation
% 5.82/1.58 % (4029031)Time elapsed: 0.017 s
% 5.82/1.58 % (4029031)Peak memory usage: 90 MB
% 5.82/1.58 % (4029031)Instructions burned: 27 (million)
% 5.82/1.58 % (4029033)Instruction limit reached!
% 5.82/1.58 % (4029033)------------------------------
% 5.82/1.58 % (4029033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.58 % (4029033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.58 % (4029033)CaDiCaL version: 2.1.3
% 5.82/1.58 % (4029033)Termination reason: Instruction limit
% 5.82/1.58 % (4029033)Termination phase: Saturation
% 5.82/1.58 % (4029033)Time elapsed: 0.025 s
% 5.82/1.58 % (4029033)Peak memory usage: 89 MB
% 5.82/1.58 % (4029033)Instructions burned: 87 (million)
% 5.82/1.58 % (4029035)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=687802184:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.82/1.58 % (4029035)Instruction limit reached!
% 5.82/1.58 % (4029035)------------------------------
% 5.82/1.58 % (4029035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.58 % (4029035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.58 % (4029035)CaDiCaL version: 2.1.3
% 5.82/1.58 % (4029035)Termination reason: Instruction limit
% 5.82/1.58 % (4029035)Termination phase: Preprocessing 1
% 5.82/1.58 % (4029035)Time elapsed: 0.002 s
% 5.82/1.58 % (4029035)Peak memory usage: 86 MB
% 5.82/1.58 % (4029035)Instructions burned: 3 (million)
% 5.82/1.58 % (4029036)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=91035198:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.82/1.58 % (4029039)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3541745977:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.82/1.58 % (4029039)Instruction limit reached!
% 5.82/1.58 % (4029039)------------------------------
% 5.82/1.58 % (4029039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.58 % (4029039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.58 % (4029039)CaDiCaL version: 2.1.3
% 5.82/1.58 % (4029039)Termination reason: Instruction limit
% 5.82/1.58 % (4029039)Termination phase: Preprocessing 3
% 5.82/1.58 % (4029039)Time elapsed: 0.003 s
% 5.82/1.58 % (4029039)Peak memory usage: 86 MB
% 5.82/1.58 % (4029039)Instructions burned: 4 (million)
% 5.82/1.58 % (4029041)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2532239296:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.82/1.58 % (4029042)lrs+10_1_thi=all:si=on:fd=off:random_seed=787001035:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.82/1.58 % (4029044)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=438286837:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.82/1.58 % (4029045)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3667848727:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.82/1.58 % (4029045)Instruction limit reached!
% 5.82/1.58 % (4029045)------------------------------
% 5.82/1.58 % (4029045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.58 % (4029045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.58 % (4029045)CaDiCaL version: 2.1.3
% 5.82/1.58 % (4029045)Termination reason: Instruction limit
% 5.82/1.58 % (4029045)Termination phase: Preprocessing 1
% 5.82/1.58 % (4029045)Time elapsed: 0.001 s
% 5.82/1.58 % (4029045)Peak memory usage: 86 MB
% 5.82/1.58 % (4029045)Instructions burned: 2 (million)
% 5.82/1.58 % (4029044)Instruction limit reached!
% 5.82/1.58 % (4029044)------------------------------
% 5.82/1.58 % (4029044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.82/1.58 % (4029044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.58 % (4029044)CaDiCaL version: 2.1.3
% 5.82/1.58 % (4029044)Termination reason: Instruction limit
% 5.82/1.58 % (4029044)Termination phase: Property scanning
% 7.20/1.82 % (4029044)Time elapsed: 0.005 s
% 7.20/1.82 % (4029044)Peak memory usage: 86 MB
% 7.20/1.82 % (4029044)Instructions burned: 9 (million)
% 7.20/1.82 % (4029042)Instruction limit reached!
% 7.20/1.82 % (4029042)------------------------------
% 7.20/1.82 % (4029042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.82 % (4029042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.82 % (4029042)CaDiCaL version: 2.1.3
% 7.20/1.82 % (4029042)Termination reason: Instruction limit
% 7.20/1.82 % (4029042)Termination phase: Saturation
% 7.20/1.82 % (4029042)Time elapsed: 0.061 s
% 7.20/1.82 % (4029042)Peak memory usage: 118 MB
% 7.20/1.82 % (4029042)Instructions burned: 53 (million)
% 7.20/1.82 % (4029041)Instruction limit reached!
% 7.20/1.82 % (4029041)------------------------------
% 7.20/1.82 % (4029041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.82 % (4029041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.82 % (4029041)CaDiCaL version: 2.1.3
% 7.20/1.82 % (4029041)Termination reason: Instruction limit
% 7.20/1.82 % (4029041)Termination phase: Saturation
% 7.20/1.82 % (4029041)Time elapsed: 0.087 s
% 7.20/1.82 % (4029041)Peak memory usage: 134 MB
% 7.20/1.82 % (4029041)Instructions burned: 67 (million)
% 7.20/1.82 % (4029036)Instruction limit reached!
% 7.20/1.82 % (4029036)------------------------------
% 7.20/1.82 % (4029036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.82 % (4029036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.82 % (4029036)CaDiCaL version: 2.1.3
% 7.20/1.82 % (4029036)Termination reason: Instruction limit
% 7.20/1.82 % (4029036)Termination phase: Saturation
% 7.20/1.82 % (4029036)Time elapsed: 0.124 s
% 7.20/1.82 % (4029036)Peak memory usage: 91 MB
% 7.20/1.82 % (4029036)Instructions burned: 181 (million)
% 7.20/1.82 % (4029047)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=732237396:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.20/1.82 % (4029047)Instruction limit reached!
% 7.20/1.82 % (4029047)------------------------------
% 7.20/1.82 % (4029047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.82 % (4029047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.82 % (4029047)CaDiCaL version: 2.1.3
% 7.20/1.82 % (4029047)Termination reason: Instruction limit
% 7.20/1.82 % (4029047)Termination phase: Unused predicate definition removal
% 7.20/1.82 % (4029047)Time elapsed: 0.002 s
% 7.20/1.82 % (4029047)Peak memory usage: 86 MB
% 7.20/1.82 % (4029047)Instructions burned: 3 (million)
% 7.20/1.82 % (4029050)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=360353624:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.20/1.82 % (4029056)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3556862178:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.20/1.82 % (4029056)Refutation not found, incomplete strategy
% 7.20/1.82 % (4029056)------------------------------
% 7.20/1.82 % (4029056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.82 % (4029056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.82 % (4029056)CaDiCaL version: 2.1.3
% 7.20/1.82 % (4029056)Termination reason: Refutation not found, incomplete strategy
% 7.20/1.82 % (4029056)Time elapsed: 0.006 s
% 7.20/1.82 % (4029056)Peak memory usage: 89 MB
% 7.20/1.82 % (4029056)Instructions burned: 15 (million)
% 7.20/1.82 % (4029055)dis+10_1_si=on:random_seed=10267799:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.20/1.82 % (4029055)Instruction limit reached!
% 7.20/1.82 % (4029055)------------------------------
% 7.20/1.82 % (4029055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.82 % (4029055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.82 % (4029055)CaDiCaL version: 2.1.3
% 7.20/1.82 % (4029055)Termination reason: Instruction limit
% 7.20/1.82 % (4029055)Termination phase: Property scanning
% 7.20/1.82 % (4029055)Time elapsed: 0.006 s
% 7.20/1.82 % (4029055)Peak memory usage: 87 MB
% 7.20/1.82 % (4029055)Instructions burned: 10 (million)
% 7.20/1.82 % (4029057)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1506400070: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_2994 on theBenchmark for (2994ds/35Mi)
% 7.20/1.89 % (4029057)Instruction limit reached!
% 7.20/1.89 % (4029057)------------------------------
% 7.20/1.89 % (4029057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.89 % (4029057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.89 % (4029057)CaDiCaL version: 2.1.3
% 7.20/1.89 % (4029057)Termination reason: Instruction limit
% 7.20/1.89 % (4029057)Termination phase: Saturation
% 7.20/1.89 % (4029057)Time elapsed: 0.025 s
% 7.20/1.89 % (4029057)Peak memory usage: 89 MB
% 7.20/1.89 % (4029057)Instructions burned: 36 (million)
% 7.20/1.89 % (4029050)Instruction limit reached!
% 7.20/1.89 % (4029050)------------------------------
% 7.20/1.89 % (4029050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.89 % (4029050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.89 % (4029050)CaDiCaL version: 2.1.3
% 7.20/1.89 % (4029050)Termination reason: Instruction limit
% 7.20/1.89 % (4029050)Termination phase: Saturation
% 7.20/1.89 % (4029050)Time elapsed: 0.114 s
% 7.20/1.89 % (4029050)Peak memory usage: 118 MB
% 7.20/1.90 % (4029050)Instructions burned: 127 (million)
% 7.20/1.90 % (4029059)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=333234647:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 7.20/1.90 % (4029058)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=566054129:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 7.20/1.90 % (4029058)Instruction limit reached!
% 7.20/1.90 % (4029058)------------------------------
% 7.20/1.90 % (4029058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029058)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029058)Termination reason: Instruction limit
% 7.20/1.90 % (4029058)Termination phase: Preprocessing 1
% 7.20/1.90 % (4029058)Time elapsed: 0.002 s
% 7.20/1.90 % (4029058)Peak memory usage: 85 MB
% 7.20/1.90 % (4029058)Instructions burned: 3 (million)
% 7.20/1.90 % (4029059)Instruction limit reached!
% 7.20/1.90 % (4029059)------------------------------
% 7.20/1.90 % (4029059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029059)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029059)Termination reason: Instruction limit
% 7.20/1.90 % (4029059)Termination phase: Property scanning
% 7.20/1.90 % (4029059)Time elapsed: 0.005 s
% 7.20/1.90 % (4029059)Peak memory usage: 87 MB
% 7.20/1.90 % (4029059)Instructions burned: 8 (million)
% 7.20/1.90 % (4029061)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3901547381:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 7.20/1.90 % (4029056)------------------------------
% 7.20/1.90 % (4029056)------------------------------
% 7.20/1.90 % (4029065)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3406753492:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 7.20/1.90 % (4029065)Instruction limit reached!
% 7.20/1.90 % (4029065)------------------------------
% 7.20/1.90 % (4029065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029065)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029065)Termination reason: Instruction limit
% 7.20/1.90 % (4029065)Termination phase: Saturation
% 7.20/1.90 % (4029065)Time elapsed: 0.019 s
% 7.20/1.90 % (4029065)Peak memory usage: 99 MB
% 7.20/1.90 % (4029065)Instructions burned: 13 (million)
% 7.20/1.90 % (4029070)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3162579716:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 7.20/1.90 % (4029072)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=73742973:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 7.20/1.90 % (4029067)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1189858548:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 7.20/1.90 % (4029071)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2266650806:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 7.20/1.90 % (4029070)Instruction limit reached!
% 7.20/1.90 % (4029070)------------------------------
% 7.20/1.90 % (4029070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029070)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029070)Termination reason: Instruction limit
% 7.20/1.90 % (4029070)Termination phase: Saturation
% 7.20/1.90 % (4029070)Time elapsed: 0.007 s
% 7.20/1.90 % (4029070)Peak memory usage: 88 MB
% 7.20/1.90 % (4029070)Instructions burned: 11 (million)
% 7.20/1.90 % (4029074)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=77932485:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 7.20/1.90 % (4029067)First to succeed.
% 7.20/1.90 % (4029072)Instruction limit reached!
% 7.20/1.90 % (4029072)------------------------------
% 7.20/1.90 % (4029072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029072)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029072)Termination reason: Instruction limit
% 7.20/1.90 % (4029072)Termination phase: Saturation
% 7.20/1.90 % (4029072)Time elapsed: 0.053 s
% 7.20/1.90 % (4029072)Peak memory usage: 90 MB
% 7.20/1.90 % (4029072)Instructions burned: 75 (million)
% 7.20/1.90 % (4029067)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4028988"
% 7.20/1.90 % (4029061)Instruction limit reached!
% 7.20/1.90 % (4029061)------------------------------
% 7.20/1.90 % (4029061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029061)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029061)Termination reason: Instruction limit
% 7.20/1.90 % (4029061)Termination phase: Saturation
% 7.20/1.90 % (4029061)Time elapsed: 0.210 s
% 7.20/1.90 % (4029061)Peak memory usage: 91 MB
% 7.20/1.90 % (4029061)Instructions burned: 372 (million)
% 7.20/1.90 % (4029071)Instruction limit reached!
% 7.20/1.90 % (4029071)------------------------------
% 7.20/1.90 % (4029071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029071)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029071)Termination reason: Instruction limit
% 7.20/1.90 % (4029071)Termination phase: Saturation
% 7.20/1.90 % (4029071)Time elapsed: 0.093 s
% 7.20/1.90 % (4029071)Peak memory usage: 133 MB
% 7.20/1.90 % (4029071)Instructions burned: 71 (million)
% 7.20/1.90 % (4029074)Instruction limit reached!
% 7.20/1.90 % (4029074)------------------------------
% 7.20/1.90 % (4029074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029074)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029074)Termination reason: Instruction limit
% 7.20/1.90 % (4029074)Termination phase: Saturation
% 7.20/1.90 % (4029074)Time elapsed: 0.096 s
% 7.20/1.90 % (4029074)Peak memory usage: 91 MB
% 7.20/1.90 % (4029074)Instructions burned: 296 (million)
% 7.20/1.90 % (4029076)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2723589581:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 7.20/1.90 % (4029081)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3988613716:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 7.20/1.90 % (4029083)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3503801179:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 7.20/1.90 % (4029084)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1791482611:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 7.20/1.90 % (4029086)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1481806151:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 7.20/1.90 % (4029076)Instruction limit reached!
% 7.20/1.90 % (4029076)------------------------------
% 7.20/1.90 % (4029076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029076)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029076)Termination reason: Instruction limit
% 7.20/1.90 % (4029076)Termination phase: Saturation
% 7.20/1.90 % (4029076)Time elapsed: 0.104 s
% 7.20/1.90 % (4029076)Peak memory usage: 117 MB
% 7.20/1.90 % (4029076)Instructions burned: 131 (million)
% 7.20/1.90 % (4029085)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3986968213:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 7.20/1.90 % (4029083)Instruction limit reached!
% 7.20/1.90 % (4029083)------------------------------
% 7.20/1.90 % (4029083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029083)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029083)Termination reason: Instruction limit
% 7.20/1.90 % (4029083)Termination phase: Saturation
% 7.20/1.90 % (4029083)Time elapsed: 0.067 s
% 7.20/1.90 % (4029083)Peak memory usage: 134 MB
% 7.20/1.90 % (4029083)Instructions burned: 41 (million)
% 7.20/1.90 % (4029081)Instruction limit reached!
% 7.20/1.90 % (4029081)------------------------------
% 7.20/1.90 % (4029081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029081)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029081)Termination reason: Instruction limit
% 7.20/1.90 % (4029081)Termination phase: Saturation
% 7.20/1.90 % (4029081)Time elapsed: 0.137 s
% 7.20/1.90 % (4029081)Peak memory usage: 134 MB
% 7.20/1.90 % (4029081)Instructions burned: 131 (million)
% 7.20/1.90 % (4029086)Instruction limit reached!
% 7.20/1.90 % (4029086)------------------------------
% 7.20/1.90 % (4029086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.90 % (4029086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.90 % (4029086)CaDiCaL version: 2.1.3
% 7.20/1.90 % (4029086)Termination reason: Instruction limit
% 7.20/1.90 % (4029086)Termination phase: Saturation
% 7.20/1.90 % (4029086)Time elapsed: 0.061 s
% 7.20/1.90 % (4029086)Peak memory usage: 119 MB
% 7.20/1.90 % (4029086)Instructions burned: 131 (million)
% 7.20/1.90 % (4029067)Refutation found. Thanks to Tanya!
% 7.20/1.90 % SZS status Theorem for theBenchmark
% 7.20/1.90 % SZS output start Proof for theBenchmark
% See solution above
% 9.30/2.09 % (4029067)------------------------------
% 9.30/2.09 % (4029067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.09 % (4029067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.09 % (4029067)CaDiCaL version: 2.1.3
% 9.30/2.09 % (4029067)Termination reason: Refutation
% 9.30/2.09 % (4029067)Time elapsed: 0.053 s
% 9.30/2.09 % (4029067)Peak memory usage: 117 MB
% 9.30/2.09 % (4029067)Instructions burned: 40 (million)
% 9.30/2.09 % (4029067)------------------------------
% 9.30/2.09 % (4029067)------------------------------
% 9.30/2.09 % (4028988)Success in time 1.239 s
% 9.30/2.09 % Vampire exiting
%------------------------------------------------------------------------------