%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW619_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:58 PM UTC 2026
% Result : Theorem 1.51s 0.63s
% Output : Refutation 2.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 4
% Syntax : Number of formulae : 26 ( 7 unt; 0 typ; 3 def)
% Number of atoms : 155 ( 16 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 184 ( 55 ~; 30 |; 68 &)
% ( 3 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number arithmetic : 292 ( 91 atm; 103 fun; 53 num; 45 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 17 usr; 4 prp; 0-7 aty)
% Number of functors : 59 ( 55 usr; 18 con; 0-7 aty)
% Number of variables : 66 ( 45 !; 21 ?; 66 :)
% 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,
elt4: $tType ).
tff(type_def_10,type,
array_elt2: $tType ).
tff(type_def_11,type,
map_int_elt2: $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,
elt5: ty ).
tff(func_def_26,type,
t2tb7: elt4 > uni ).
tff(func_def_27,type,
tb2t7: uni > elt4 ).
tff(func_def_28,type,
t2tb8: array_elt2 > uni ).
tff(func_def_29,type,
tb2t8: uni > array_elt2 ).
tff(func_def_30,type,
ref: ty > ty ).
tff(func_def_31,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_32,type,
contents: ( ty * uni ) > uni ).
tff(func_def_33,type,
occ1: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_37,type,
abs: $int > $int ).
tff(func_def_39,type,
div: ( $int * $int ) > $int ).
tff(func_def_40,type,
mod: ( $int * $int ) > $int ).
tff(func_def_41,type,
min: ( $int * $int ) > $int ).
tff(func_def_42,type,
max: ( $int * $int ) > $int ).
tff(func_def_43,type,
t2tb9: map_int_elt2 > uni ).
tff(func_def_44,type,
tb2t9: uni > map_int_elt2 ).
tff(func_def_45,type,
sK1: ( $int * $int * uni * ty * uni * $int * $int ) > $int ).
tff(func_def_46,type,
sK2: ( $int * uni * ty * uni * $int ) > uni ).
tff(func_def_47,type,
sK3: ( $int * $int * array_elt2 ) > $int ).
tff(func_def_48,type,
sK4: ( $int * $int * array_elt2 ) > $int ).
tff(func_def_49,type,
sK5: ( uni * uni * $int * $int * ty ) > $int ).
tff(func_def_50,type,
sK6: map_int_elt2 ).
tff(func_def_51,type,
sK7: $int ).
tff(func_def_52,type,
sK8: $int ).
tff(func_def_53,type,
sK9: map_int_elt2 ).
tff(func_def_54,type,
sK10: map_int_elt2 ).
tff(func_def_55,type,
sK11: $int ).
tff(func_def_56,type,
sK12: $int ).
tff(func_def_57,type,
sK13: ( $int * ty * uni * uni * $int ) > $int ).
tff(func_def_58,type,
sK14: ( uni * ty * $int * $int * uni * $int ) > $int ).
tff(func_def_59,type,
sK15: ( uni * $int * ty * uni * $int ) > $int ).
tff(func_def_60,type,
sK16: ( uni * $int * $int * uni * ty ) > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
le3: ( elt4 * elt4 ) > $o ).
tff(pred_def_4,type,
sorted_sub3: ( array_elt2 * $int * $int ) > $o ).
tff(pred_def_6,type,
sorted3: array_elt2 > $o ).
tff(pred_def_7,type,
permut2: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_8,type,
map_eq_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_9,type,
array_eq_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_10,type,
array_eq: ( ty * uni * uni ) > $o ).
tff(pred_def_11,type,
exchange2: ( ty * uni * uni * $int * $int * $int * $int ) > $o ).
tff(pred_def_12,type,
exchange3: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_13,type,
permut3: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_14,type,
permut_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_15,type,
permut_all: ( ty * uni * uni ) > $o ).
tff(pred_def_16,type,
sP0: ( $int * $int * uni * ty * uni * $int * $int ) > $o ).
tff(f98,conjecture,
! [X1: map_int_elt2,X0: $int] :
( $lesseq(0,X0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( $lesseq(0,X4)
& $less(X4,X2) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& $lesseq(0,X2) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& $lesseq(1,X5)
& ! [X7: $int] :
( ( $lesseq(0,$product(X7,X5))
& $less($product(X7,X5),X0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) )
=> ( $less(X5,X0)
=> ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& $lesseq(0,$product(X7,X5)) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_bottom_up_mergesort) ).
tff(f99,negated_conjecture,
~ ! [X1: map_int_elt2,X0: $int] :
( $lesseq(0,X0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( $lesseq(0,X4)
& $less(X4,X2) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& $lesseq(0,X2) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& $lesseq(1,X5)
& ! [X7: $int] :
( ( $lesseq(0,$product(X7,X5))
& $less($product(X7,X5),X0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) )
=> ( $less(X5,X0)
=> ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& $lesseq(0,$product(X7,X5)) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
tff(f102,plain,
~ ! [X1: map_int_elt2,X0: $int] :
( ~ $less(X0,0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( ~ $less(X4,0)
& $less(X4,X2) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& ~ $less(X2,0) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& ~ $less(X5,1)
& ! [X7: $int] :
( ( ~ $less($product(X7,X5),0)
& $less($product(X7,X5),X0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) )
=> ( $less(X5,X0)
=> ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& ~ $less($product(X7,X5),0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) ) ) ) ),
inference(theory_normalization,[],[f99]) ).
tff(f145,plain,
~ ! [X1: $int,X0: map_int_elt2] :
( ~ $less(X1,0)
=> ! [X3: map_int_elt2,X2: $int] :
( ( ~ $less(X2,0)
& ( X1 = X2 )
& ! [X4: $int] :
( ( ~ $less(X4,0)
& $less(X4,X2) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X0),t2tb(X4))) ) ) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( ~ $less(X5,1)
& ! [X7: $int] :
( ( ~ $less($product(X7,X5),0)
& $less($product(X7,X5),X1) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X6))),$product(X7,X5),min(X1,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X1,t2tb9(X0)),mk_array1(elt5,X1,t2tb9(X6))) )
=> ( $less(X5,X1)
=> ! [X8: $int] :
( ( $less($product(X8,X5),X1)
& ~ $less($product(X8,X5),0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X6))),$product(X8,X5),min(X1,$sum($product(X8,X5),X5))) ) ) ) ) ),
inference(rectify,[],[f102]) ).
tff(f275,plain,
? [X1: $int,X0: map_int_elt2] :
( ? [X3: map_int_elt2,X2: $int] :
( ? [X5: $int,X6: map_int_elt2] :
( ? [X8: $int] :
( ~ sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X6))),$product(X8,X5),min(X1,$sum($product(X8,X5),X5)))
& $less($product(X8,X5),X1)
& ~ $less($product(X8,X5),0) )
& $less(X5,X1)
& ~ $less(X5,1)
& ! [X7: $int] :
( sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X6))),$product(X7,X5),min(X1,$sum($product(X7,X5),X5)))
| $less($product(X7,X5),0)
| ~ $less($product(X7,X5),X1) )
& permut_all(elt5,mk_array1(elt5,X1,t2tb9(X0)),mk_array1(elt5,X1,t2tb9(X6))) )
& ~ $less(X2,0)
& ( X1 = X2 )
& ! [X4: $int] :
( ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X0),t2tb(X4))) )
| $less(X4,0)
| ~ $less(X4,X2) ) )
& ~ $less(X1,0) ),
inference(ennf_transformation,[],[f145]) ).
tff(f276,plain,
? [X0: map_int_elt2,X1: $int] :
( ? [X2: $int,X3: map_int_elt2] :
( ! [X4: $int] :
( ~ $less(X4,X2)
| $less(X4,0)
| ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X0),t2tb(X4))) ) )
& ? [X6: map_int_elt2,X5: $int] :
( ? [X8: $int] :
( $less($product(X8,X5),X1)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X6))),$product(X8,X5),min(X1,$sum($product(X8,X5),X5)))
& ~ $less($product(X8,X5),0) )
& $less(X5,X1)
& ~ $less(X5,1)
& permut_all(elt5,mk_array1(elt5,X1,t2tb9(X0)),mk_array1(elt5,X1,t2tb9(X6)))
& ! [X7: $int] :
( $less($product(X7,X5),0)
| sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X6))),$product(X7,X5),min(X1,$sum($product(X7,X5),X5)))
| ~ $less($product(X7,X5),X1) ) )
& ~ $less(X2,0)
& ( X1 = X2 ) )
& ~ $less(X1,0) ),
inference(flattening,[],[f275]) ).
tff(f310,plain,
? [X0: map_int_elt2,X1: $int] :
( ? [X2: $int,X3: map_int_elt2] :
( ! [X4: $int] :
( ~ $less(X4,X2)
| $less(X4,0)
| ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X0),t2tb(X4))) ) )
& ? [X5: map_int_elt2,X6: $int] :
( ? [X7: $int] :
( $less($product(X7,X6),X1)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X5))),$product(X7,X6),min(X1,$sum($product(X7,X6),X6)))
& ~ $less($product(X7,X6),0) )
& $less(X6,X1)
& ~ $less(X6,1)
& permut_all(elt5,mk_array1(elt5,X1,t2tb9(X0)),mk_array1(elt5,X1,t2tb9(X5)))
& ! [X8: $int] :
( $less($product(X8,X6),0)
| sorted_sub3(tb2t8(mk_array1(elt5,X1,t2tb9(X5))),$product(X8,X6),min(X1,$sum($product(X8,X6),X6)))
| ~ $less($product(X8,X6),X1) ) )
& ~ $less(X2,0)
& ( X1 = X2 ) )
& ~ $less(X1,0) ),
inference(rectify,[],[f276]) ).
tff(f311,plain,
( ! [X4: $int] :
( ~ $less(X4,sK8)
| $less(X4,0)
| ( tb2t7(get(elt5,int,t2tb9(sK9),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(sK6),t2tb(X4))) ) )
& $less($product(sK12,sK11),sK7)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,sK7,t2tb9(sK10))),$product(sK12,sK11),min(sK7,$sum($product(sK12,sK11),sK11)))
& ~ $less($product(sK12,sK11),0)
& $less(sK11,sK7)
& ~ $less(sK11,1)
& permut_all(elt5,mk_array1(elt5,sK7,t2tb9(sK6)),mk_array1(elt5,sK7,t2tb9(sK10)))
& ! [X8: $int] :
( $less($product(X8,sK11),0)
| sorted_sub3(tb2t8(mk_array1(elt5,sK7,t2tb9(sK10))),$product(X8,sK11),min(sK7,$sum($product(X8,sK11),sK11)))
| ~ $less($product(X8,sK11),sK7) )
& ~ $less(sK8,0)
& ( sK8 = sK7 )
& ~ $less(sK7,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9),skolemize(X5,sK10),skolemize(X6,sK11),skolemize(X7,sK12)],[f310]) ).
tff(f423,plain,
! [X8: $int] :
( sorted_sub3(tb2t8(mk_array1(elt5,sK7,t2tb9(sK10))),$product(X8,sK11),min(sK7,$sum($product(X8,sK11),sK11)))
| $less($product(X8,sK11),0)
| ~ $less($product(X8,sK11),sK7) ),
inference(cnf_transformation,[],[f311]) ).
tff(f427,plain,
~ $less($product(sK12,sK11),0),
inference(cnf_transformation,[],[f311]) ).
tff(f428,plain,
~ sorted_sub3(tb2t8(mk_array1(elt5,sK7,t2tb9(sK10))),$product(sK12,sK11),min(sK7,$sum($product(sK12,sK11),sK11))),
inference(cnf_transformation,[],[f311]) ).
tff(f429,plain,
$less($product(sK12,sK11),sK7),
inference(cnf_transformation,[],[f311]) ).
tff(f544,definition,
( spl17_5
<=> $less($product(sK12,sK11),0) ),
introduced(definition,[new_symbols(definition,[spl17_5])],[avatar_definition]) ).
tff(f546,plain,
( ~ $less($product(sK12,sK11),0)
| spl17_5 ),
inference(avatar_component_clause,[],[f544]) ).
tff(f547,plain,
~ spl17_5,
inference(avatar_split_clause,[],[f427,f544]) ).
tff(f549,definition,
( spl17_6
<=> sorted_sub3(tb2t8(mk_array1(elt5,sK7,t2tb9(sK10))),$product(sK12,sK11),min(sK7,$sum($product(sK12,sK11),sK11))) ),
introduced(definition,[new_symbols(definition,[spl17_6])],[avatar_definition]) ).
tff(f551,plain,
( ~ sorted_sub3(tb2t8(mk_array1(elt5,sK7,t2tb9(sK10))),$product(sK12,sK11),min(sK7,$sum($product(sK12,sK11),sK11)))
| spl17_6 ),
inference(avatar_component_clause,[],[f549]) ).
tff(f552,plain,
~ spl17_6,
inference(avatar_split_clause,[],[f428,f549]) ).
tff(f559,definition,
( spl17_8
<=> $less($product(sK12,sK11),sK7) ),
introduced(definition,[new_symbols(definition,[spl17_8])],[avatar_definition]) ).
tff(f561,plain,
( $less($product(sK12,sK11),sK7)
| ~ spl17_8 ),
inference(avatar_component_clause,[],[f559]) ).
tff(f562,plain,
spl17_8,
inference(avatar_split_clause,[],[f429,f559]) ).
tff(f580,plain,
( $less($product(sK12,sK11),0)
| ~ $less($product(sK12,sK11),sK7)
| spl17_6 ),
inference(resolution,[],[f423,f551]) ).
tff(f581,plain,
( ~ $less($product(sK12,sK11),sK7)
| spl17_5
| spl17_6 ),
inference(forward_subsumption_resolution,[],[f580,f546]) ).
tff(f582,plain,
( $false
| spl17_5
| spl17_6
| ~ spl17_8 ),
inference(forward_subsumption_resolution,[],[f581,f561]) ).
tff(f583,plain,
( spl17_5
| spl17_6
| ~ spl17_8 ),
inference(avatar_contradiction_clause,[],[f582]) ).
tff(f584,plain,
$false,
inference(avatar_smt_refutation,[],[f583,f562,f552,f547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW619_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 14:22:34 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.13 Running first-order theorem proving
% 0.09/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.51/0.63 % (3407378)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 1.51/0.63 % (3407392)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1126416749:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 1.51/0.63 % (3407394)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3972958175:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 1.51/0.63 % (3407389)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1221548629:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 1.51/0.63 % (3407390)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1804815403:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 1.51/0.63 % (3407393)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4075725353:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 1.51/0.63 % (3407395)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1137946317:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 1.51/0.63 % (3407391)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3404169805:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 1.51/0.63 % (3407393)Instruction limit reached!
% 1.51/0.63 % (3407393)------------------------------
% 1.51/0.63 % (3407393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.63 % (3407393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.63 % (3407393)CaDiCaL version: 2.1.3
% 1.51/0.63 % (3407393)Termination reason: Instruction limit
% 1.51/0.63 % (3407393)Termination phase: Property scanning
% 1.51/0.63 % (3407393)Time elapsed: 0.002 s
% 1.51/0.63 % (3407393)Peak memory usage: 86 MB
% 1.51/0.63 % (3407393)Instructions burned: 7 (million)
% 1.51/0.63 % (3407392)Instruction limit reached!
% 1.51/0.63 % (3407392)------------------------------
% 1.51/0.63 % (3407392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.63 % (3407392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.63 % (3407392)CaDiCaL version: 2.1.3
% 1.51/0.63 % (3407392)Termination reason: Instruction limit
% 1.51/0.63 % (3407392)Termination phase: Property scanning
% 1.51/0.63 % (3407392)Time elapsed: 0.002 s
% 1.51/0.63 % (3407392)Peak memory usage: 86 MB
% 1.51/0.63 % (3407392)Instructions burned: 7 (million)
% 1.51/0.63 % (3407389)Instruction limit reached!
% 1.51/0.63 % (3407389)------------------------------
% 1.51/0.63 % (3407389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.63 % (3407389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.63 % (3407389)CaDiCaL version: 2.1.3
% 1.51/0.63 % (3407389)Termination reason: Instruction limit
% 1.51/0.63 % (3407389)Termination phase: Saturation
% 1.51/0.63 % (3407389)Time elapsed: 0.008 s
% 1.51/0.63 % (3407389)Peak memory usage: 94 MB
% 1.51/0.63 % (3407389)Instructions burned: 12 (million)
% 1.51/0.63 % (3407395)Instruction limit reached!
% 1.51/0.63 % (3407395)------------------------------
% 1.51/0.63 % (3407395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.63 % (3407395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.63 % (3407395)CaDiCaL version: 2.1.3
% 1.51/0.63 % (3407395)Termination reason: Instruction limit
% 1.51/0.63 % (3407395)Termination phase: Saturation
% 1.51/0.63 % (3407395)Time elapsed: 0.026 s
% 1.51/0.63 % (3407395)Peak memory usage: 117 MB
% 1.51/0.63 % (3407395)Instructions burned: 33 (million)
% 1.51/0.63 % (3407394)First to succeed.
% 1.51/0.63 % (3407390)Also succeeded, but the first one will report.
% 1.51/0.63 % (3407394)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3407378"
% 1.51/0.63 % (3407391)Also succeeded, but the first one will report.
% 1.51/0.63 % (3407403)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2510802767:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.51/0.63 % (3407404)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=3225635707:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 1.51/0.63 % (3407403)Also succeeded, but the first one will report.
% 1.51/0.63 % (3407405)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3330301167:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 1.51/0.63 % (3407404)Also succeeded, but the first one will report.
% 1.51/0.63 % (3407405)Instruction limit reached!
% 1.51/0.63 % (3407405)------------------------------
% 1.51/0.63 % (3407405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.63 % (3407405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.63 % (3407405)CaDiCaL version: 2.1.3
% 1.51/0.63 % (3407405)Termination reason: Instruction limit
% 1.51/0.63 % (3407405)Termination phase: Saturation
% 1.51/0.63 % (3407405)Time elapsed: 0.005 s
% 1.51/0.63 % (3407405)Peak memory usage: 89 MB
% 1.51/0.63 % (3407405)Instructions burned: 16 (million)
% 1.51/0.63 % (3407406)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1980757312:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 1.51/0.63 % (3407406)Also succeeded, but the first one will report.
% 1.51/0.63 % (3407394)Refutation found. Thanks to Tanya!
% 1.51/0.63 % SZS status Theorem for theBenchmark
% 1.51/0.63 % SZS output start Proof for theBenchmark
% See solution above
% 2.33/0.72 % (3407394)------------------------------
% 2.33/0.72 % (3407394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.33/0.72 % (3407394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.72 % (3407394)CaDiCaL version: 2.1.3
% 2.33/0.72 % (3407394)Termination reason: Refutation
% 2.33/0.72 % (3407394)Time elapsed: 0.029 s
% 2.33/0.72 % (3407394)Peak memory usage: 118 MB
% 2.33/0.72 % (3407394)Instructions burned: 31 (million)
% 2.33/0.72 % (3407394)------------------------------
% 2.33/0.72 % (3407394)------------------------------
% 2.33/0.72 % (3407378)Success in time 0.299 s
% 2.33/0.72 % Vampire exiting
%------------------------------------------------------------------------------