%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW610_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 : n009.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:56 PM UTC 2026
% Result : Theorem 6.07s 1.64s
% Output : Refutation 7.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 17
% Syntax : Number of formulae : 86 ( 10 unt; 0 typ; 13 def)
% Number of atoms : 336 ( 26 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 374 ( 124 ~; 164 |; 59 &)
% ( 18 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 514 ( 174 atm; 164 fun; 73 num; 103 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 : 19 ( 15 usr; 14 prp; 0-5 aty)
% Number of functors : 42 ( 38 usr; 16 con; 0-5 aty)
% Number of variables : 159 ( 138 !; 21 ?; 159 :)
% 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,
array_char: $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,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length1: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
char: ty ).
tff(func_def_29,type,
t2tb1: array_char > uni ).
tff(func_def_30,type,
tb2t1: uni > array_char ).
tff(func_def_31,type,
t2tb2: char1 > uni ).
tff(func_def_32,type,
tb2t2: uni > char1 ).
tff(func_def_37,type,
sK0: array_char ).
tff(func_def_38,type,
sK1: $int ).
tff(func_def_39,type,
sK2: $int ).
tff(func_def_40,type,
sK3: array_char ).
tff(func_def_41,type,
sK4: $int ).
tff(func_def_42,type,
sK5: $int ).
tff(func_def_43,type,
sK6: ( array_char * $int * $int * $int * array_char ) > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
matches1: ( array_char * $int * array_char * $int * $int ) > $o ).
tff(f28,axiom,
! [X2: $int,X1: uni,X0: ty] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def) ).
tff(f39,axiom,
! [X2: array_char,X3: $int,X0: array_char,X1: $int,X4: $int] :
( ( ! [X5: $int] :
( ( $less(X5,X4)
& $lesseq(0,X5) )
=> ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) ) )
& $lesseq(X3,$difference(length1(char,t2tb1(X2)),X4))
& $lesseq(0,X1)
& $lesseq(X1,$difference(length1(char,t2tb1(X0)),X4))
& $lesseq(0,X3) )
<=> matches1(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',matches_def) ).
tff(f44,conjecture,
! [X5: $int,X1: array_char,X0: array_char,X4: $int,X3: $int,X2: $int] :
( matches1(X0,X2,X1,X3,X4)
=> ( $less(X5,X4)
=> matches1(X0,X2,X1,X3,X5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',matches_right_weakening) ).
tff(f45,negated_conjecture,
~ ! [X5: $int,X1: array_char,X0: array_char,X4: $int,X3: $int,X2: $int] :
( matches1(X0,X2,X1,X3,X4)
=> ( $less(X5,X4)
=> matches1(X0,X2,X1,X3,X5) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
tff(f48,plain,
! [X2: array_char,X3: $int,X0: array_char,X1: $int,X4: $int] :
( ( ! [X5: $int] :
( ( $less(X5,X4)
& ~ $less(X5,0) )
=> ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) ) )
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ~ $less(X3,0) )
<=> matches1(X0,X1,X2,X3,X4) ),
inference(theory_normalization,[],[f39]) ).
tff(f57,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X1,X2)
| ~ $less(X0,X1)
| $less(X0,X2) ),
introduced(definition,[],[tha_transitivity]) ).
tff(f82,plain,
! [X0: $int,X1: uni,X2: ty] : ( get2(X2,X1,X0) = get(X2,int,elts(X2,X1),t2tb(X0)) ),
inference(rectify,[],[f28]) ).
tff(f88,plain,
~ ! [X5: $int,X4: $int,X1: array_char,X0: $int,X3: $int,X2: array_char] :
( matches1(X2,X5,X1,X4,X3)
=> ( $less(X0,X3)
=> matches1(X2,X5,X1,X4,X0) ) ),
inference(rectify,[],[f45]) ).
tff(f89,plain,
! [X0: array_char,X1: $int,X3: $int,X4: $int,X2: array_char] :
( ( ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ! [X5: $int] :
( ( $less(X5,X4)
& ~ $less(X5,0) )
=> ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) ) )
& ~ $less(X3,0) )
<=> matches1(X2,X3,X0,X1,X4) ),
inference(rectify,[],[f48]) ).
tff(f109,plain,
? [X5: $int,X4: $int,X1: array_char,X0: $int,X3: $int,X2: array_char] :
( ~ matches1(X2,X5,X1,X4,X0)
& $less(X0,X3)
& matches1(X2,X5,X1,X4,X3) ),
inference(ennf_transformation,[],[f88]) ).
tff(f110,plain,
? [X2: array_char,X3: $int,X4: $int,X1: array_char,X5: $int,X0: $int] :
( $less(X0,X3)
& matches1(X2,X5,X1,X4,X3)
& ~ matches1(X2,X5,X1,X4,X0) ),
inference(flattening,[],[f109]) ).
tff(f111,plain,
! [X0: array_char,X1: $int,X3: $int,X4: $int,X2: array_char] :
( ( ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) )
| ~ $less(X5,X4)
| $less(X5,0) )
& ~ $less(X3,0) )
<=> matches1(X2,X3,X0,X1,X4) ),
inference(ennf_transformation,[],[f89]) ).
tff(f112,plain,
! [X2: array_char,X1: $int,X3: $int,X4: $int,X0: array_char] :
( matches1(X2,X3,X0,X1,X4)
<=> ( ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less(X3,0)
& ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) )
| ~ $less(X5,X4)
| $less(X5,0) ) ) ),
inference(flattening,[],[f111]) ).
tff(f133,plain,
? [X0: array_char,X1: $int,X2: $int,X3: array_char,X4: $int,X5: $int] :
( $less(X5,X1)
& matches1(X0,X4,X3,X2,X1)
& ~ matches1(X0,X4,X3,X2,X5) ),
inference(rectify,[],[f110]) ).
tff(f134,plain,
( $less(sK5,sK1)
& matches1(sK0,sK4,sK3,sK2,sK1)
& ~ matches1(sK0,sK4,sK3,sK2,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5)],[f133]) ).
tff(f146,plain,
! [X2: array_char,X1: $int,X3: $int,X4: $int,X0: array_char] :
( ( matches1(X2,X3,X0,X1,X4)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
| $less(X3,0)
| ? [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) != tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) )
& $less(X5,X4)
& ~ $less(X5,0) ) )
& ( ( ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less(X3,0)
& ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) )
| ~ $less(X5,X4)
| $less(X5,0) ) )
| ~ matches1(X2,X3,X0,X1,X4) ) ),
inference(nnf_transformation,[],[f112]) ).
tff(f147,plain,
! [X2: array_char,X1: $int,X3: $int,X4: $int,X0: array_char] :
( ( matches1(X2,X3,X0,X1,X4)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
| $less(X3,0)
| ? [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) != tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) )
& $less(X5,X4)
& ~ $less(X5,0) ) )
& ( ( ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less(X3,0)
& ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) )
| ~ $less(X5,X4)
| $less(X5,0) ) )
| ~ matches1(X2,X3,X0,X1,X4) ) ),
inference(flattening,[],[f146]) ).
tff(f148,plain,
! [X0: array_char,X1: $int,X2: $int,X3: $int,X4: array_char] :
( ( matches1(X0,X2,X4,X1,X3)
| $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
| $less(X2,0)
| ? [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X4),$sum(X1,X5))) != tb2t2(get2(char,t2tb1(X0),$sum(X2,X5))) )
& $less(X5,X3)
& ~ $less(X5,0) ) )
& ( ( ~ $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
& ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
& ~ $less(X2,0)
& ! [X6: $int] :
( ( tb2t2(get2(char,t2tb1(X4),$sum(X1,X6))) = tb2t2(get2(char,t2tb1(X0),$sum(X2,X6))) )
| ~ $less(X6,X3)
| $less(X6,0) ) )
| ~ matches1(X0,X2,X4,X1,X3) ) ),
inference(rectify,[],[f147]) ).
tff(f149,plain,
! [X0: array_char,X1: $int,X2: $int,X3: $int,X4: array_char] :
( ( matches1(X0,X2,X4,X1,X3)
| $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
| $less(X2,0)
| ( ( tb2t2(get2(char,t2tb1(X0),$sum(X2,sK6(X0,X1,X2,X3,X4)))) != tb2t2(get2(char,t2tb1(X4),$sum(X1,sK6(X0,X1,X2,X3,X4)))) )
& $less(sK6(X0,X1,X2,X3,X4),X3)
& ~ $less(sK6(X0,X1,X2,X3,X4),0) ) )
& ( ( ~ $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
& ~ $less(X1,0)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
& ~ $less(X2,0)
& ! [X6: $int] :
( ( tb2t2(get2(char,t2tb1(X4),$sum(X1,X6))) = tb2t2(get2(char,t2tb1(X0),$sum(X2,X6))) )
| ~ $less(X6,X3)
| $less(X6,0) ) )
| ~ matches1(X0,X2,X4,X1,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X5,sK6(X0,X1,X2,X3,X4))],[f148]) ).
tff(f170,plain,
~ matches1(sK0,sK4,sK3,sK2,sK5),
inference(cnf_transformation,[],[f134]) ).
tff(f171,plain,
matches1(sK0,sK4,sK3,sK2,sK1),
inference(cnf_transformation,[],[f134]) ).
tff(f172,plain,
$less(sK5,sK1),
inference(cnf_transformation,[],[f134]) ).
tff(f183,plain,
! [X2: ty,X0: $int,X1: uni] : ( get2(X2,X1,X0) = get(X2,int,elts(X2,X1),t2tb(X0)) ),
inference(cnf_transformation,[],[f82]) ).
tff(f193,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X6: $int,X4: array_char] :
( ( tb2t2(get2(char,t2tb1(X4),$sum(X1,X6))) = tb2t2(get2(char,t2tb1(X0),$sum(X2,X6))) )
| ~ $less(X6,X3)
| $less(X6,0)
| ~ matches1(X0,X2,X4,X1,X3) ),
inference(cnf_transformation,[],[f149]) ).
tff(f194,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( ~ matches1(X0,X2,X4,X1,X3)
| ~ $less(X2,0) ),
inference(cnf_transformation,[],[f149]) ).
tff(f195,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( ~ matches1(X0,X2,X4,X1,X3)
| ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2) ),
inference(cnf_transformation,[],[f149]) ).
tff(f196,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( ~ matches1(X0,X2,X4,X1,X3)
| ~ $less(X1,0) ),
inference(cnf_transformation,[],[f149]) ).
tff(f197,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( ~ matches1(X0,X2,X4,X1,X3)
| ~ $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1) ),
inference(cnf_transformation,[],[f149]) ).
tff(f198,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( matches1(X0,X2,X4,X1,X3)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
| ~ $less(sK6(X0,X1,X2,X3,X4),0)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
| $less(X2,0) ),
inference(cnf_transformation,[],[f149]) ).
tff(f199,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( matches1(X0,X2,X4,X1,X3)
| $less(sK6(X0,X1,X2,X3,X4),X3)
| $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
| $less(X2,0) ),
inference(cnf_transformation,[],[f149]) ).
tff(f200,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( matches1(X0,X2,X4,X1,X3)
| $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
| $less(X1,0)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
| $less(X2,0)
| ( tb2t2(get2(char,t2tb1(X0),$sum(X2,sK6(X0,X1,X2,X3,X4)))) != tb2t2(get2(char,t2tb1(X4),$sum(X1,sK6(X0,X1,X2,X3,X4)))) ) ),
inference(cnf_transformation,[],[f149]) ).
tff(f212,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( matches1(X0,X2,X4,X1,X3)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X3)),X2)
| $less(X2,0)
| $less($sum(length1(char,t2tb1(X4)),$uminus(X3)),X1)
| $less(X1,0)
| ( tb2t2(get(char,int,elts(char,t2tb1(X4)),t2tb($sum(X1,sK6(X0,X1,X2,X3,X4))))) != tb2t2(get(char,int,elts(char,t2tb1(X0)),t2tb($sum(X2,sK6(X0,X1,X2,X3,X4))))) ) ),
inference(definition_unfolding,[],[f200,f183,f183]) ).
tff(f213,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X6: $int,X4: array_char] :
( ~ matches1(X0,X2,X4,X1,X3)
| ( tb2t2(get(char,int,elts(char,t2tb1(X4)),t2tb($sum(X1,X6)))) = tb2t2(get(char,int,elts(char,t2tb1(X0)),t2tb($sum(X2,X6)))) )
| $less(X6,0)
| ~ $less(X6,X3) ),
inference(definition_unfolding,[],[f193,f183,f183]) ).
tff(f216,definition,
( spl7_1
<=> matches1(sK0,sK4,sK3,sK2,sK5) ),
introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition]) ).
tff(f218,plain,
( ~ matches1(sK0,sK4,sK3,sK2,sK5)
| spl7_1 ),
inference(avatar_component_clause,[],[f216]) ).
tff(f219,plain,
~ spl7_1,
inference(avatar_split_clause,[],[f170,f216]) ).
tff(f221,definition,
( spl7_2
<=> matches1(sK0,sK4,sK3,sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
tff(f223,plain,
( matches1(sK0,sK4,sK3,sK2,sK1)
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f221]) ).
tff(f224,plain,
spl7_2,
inference(avatar_split_clause,[],[f171,f221]) ).
tff(f226,definition,
( spl7_3
<=> $less(sK5,sK1) ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
tff(f228,plain,
( $less(sK5,sK1)
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f226]) ).
tff(f229,plain,
spl7_3,
inference(avatar_split_clause,[],[f172,f226]) ).
tff(f240,plain,
( ! [X0: $int] :
( $less(X0,sK1)
| ~ $less(X0,sK5) )
| ~ spl7_3 ),
inference(resolution,[],[f228,f57]) ).
tff(f307,plain,
( ~ $less(sK4,0)
| ~ spl7_2 ),
inference(unit_resulting_resolution,[],[f194,f223]) ).
tff(f310,definition,
( spl7_12
<=> $less(sK4,0) ),
introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition]) ).
tff(f312,plain,
( ~ $less(sK4,0)
| spl7_12 ),
inference(avatar_component_clause,[],[f310]) ).
tff(f313,plain,
( ~ spl7_12
| ~ spl7_2 ),
inference(avatar_split_clause,[],[f307,f221,f310]) ).
tff(f315,plain,
( ~ $less(sK2,0)
| ~ spl7_2 ),
inference(resolution,[],[f196,f223]) ).
tff(f317,definition,
( spl7_13
<=> $less(sK2,0) ),
introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition]) ).
tff(f319,plain,
( ~ $less(sK2,0)
| spl7_13 ),
inference(avatar_component_clause,[],[f317]) ).
tff(f320,plain,
( ~ spl7_13
| ~ spl7_2 ),
inference(avatar_split_clause,[],[f315,f221,f317]) ).
tff(f452,plain,
( ~ $less($sum(length1(char,t2tb1(sK0)),$uminus(sK1)),sK4)
| ~ spl7_2 ),
inference(unit_resulting_resolution,[],[f195,f223]) ).
tff(f455,definition,
( spl7_20
<=> $less($sum(length1(char,t2tb1(sK0)),$uminus(sK1)),sK4) ),
introduced(definition,[new_symbols(definition,[spl7_20])],[avatar_definition]) ).
tff(f458,plain,
( ~ spl7_20
| ~ spl7_2 ),
inference(avatar_split_clause,[],[f452,f221,f455]) ).
tff(f460,plain,
( ~ $less($sum(length1(char,t2tb1(sK3)),$uminus(sK1)),sK2)
| ~ spl7_2 ),
inference(resolution,[],[f197,f223]) ).
tff(f462,definition,
( spl7_21
<=> $less($sum(length1(char,t2tb1(sK3)),$uminus(sK1)),sK2) ),
introduced(definition,[new_symbols(definition,[spl7_21])],[avatar_definition]) ).
tff(f465,plain,
( ~ spl7_21
| ~ spl7_2 ),
inference(avatar_split_clause,[],[f460,f221,f462]) ).
tff(f662,plain,
( ! [X0: $int] :
( ~ $less(X0,sK1)
| $less(X0,0)
| ( tb2t2(get(char,int,elts(char,t2tb1(sK0)),t2tb($sum(sK4,X0)))) = tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK2,X0)))) ) )
| ~ spl7_2 ),
inference(resolution,[],[f213,f223]) ).
tff(f666,plain,
( ~ $less(sK6(sK0,sK2,sK4,sK5,sK3),0)
| $less(sK4,0)
| $less(sK2,0)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| spl7_1 ),
inference(resolution,[],[f198,f218]) ).
tff(f673,plain,
( $less(sK2,0)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| ~ $less(sK6(sK0,sK2,sK4,sK5,sK3),0)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| spl7_1
| spl7_12 ),
inference(forward_subsumption_resolution,[],[f666,f312]) ).
tff(f674,plain,
( $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| ~ $less(sK6(sK0,sK2,sK4,sK5,sK3),0)
| spl7_1
| spl7_12
| spl7_13 ),
inference(forward_subsumption_resolution,[],[f673,f319]) ).
tff(f676,definition,
( spl7_24
<=> $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2) ),
introduced(definition,[new_symbols(definition,[spl7_24])],[avatar_definition]) ).
tff(f680,definition,
( spl7_25
<=> $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4) ),
introduced(definition,[new_symbols(definition,[spl7_25])],[avatar_definition]) ).
tff(f684,definition,
( spl7_26
<=> $less(sK6(sK0,sK2,sK4,sK5,sK3),0) ),
introduced(definition,[new_symbols(definition,[spl7_26])],[avatar_definition]) ).
tff(f686,plain,
( ~ $less(sK6(sK0,sK2,sK4,sK5,sK3),0)
| spl7_26 ),
inference(avatar_component_clause,[],[f684]) ).
tff(f687,plain,
( spl7_24
| spl7_25
| ~ spl7_26
| spl7_1
| spl7_12
| spl7_13 ),
inference(avatar_split_clause,[],[f674,f317,f310,f216,f684,f680,f676]) ).
tff(f688,plain,
( $less(sK6(sK0,sK2,sK4,sK5,sK3),sK5)
| $less(sK4,0)
| $less(sK2,0)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| spl7_1 ),
inference(resolution,[],[f199,f218]) ).
tff(f695,plain,
( $less(sK6(sK0,sK2,sK4,sK5,sK3),sK5)
| $less(sK2,0)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| spl7_1
| spl7_12 ),
inference(forward_subsumption_resolution,[],[f688,f312]) ).
tff(f696,plain,
( $less(sK6(sK0,sK2,sK4,sK5,sK3),sK5)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| spl7_1
| spl7_12
| spl7_13 ),
inference(forward_subsumption_resolution,[],[f695,f319]) ).
tff(f698,definition,
( spl7_27
<=> $less(sK6(sK0,sK2,sK4,sK5,sK3),sK5) ),
introduced(definition,[new_symbols(definition,[spl7_27])],[avatar_definition]) ).
tff(f700,plain,
( $less(sK6(sK0,sK2,sK4,sK5,sK3),sK5)
| ~ spl7_27 ),
inference(avatar_component_clause,[],[f698]) ).
tff(f701,plain,
( spl7_25
| spl7_24
| spl7_27
| spl7_1
| spl7_12
| spl7_13 ),
inference(avatar_split_clause,[],[f696,f317,f310,f216,f698,f676,f680]) ).
tff(f735,plain,
( $less(sK2,0)
| ( tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK2,sK6(sK0,sK2,sK4,sK5,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK0)),t2tb($sum(sK4,sK6(sK0,sK2,sK4,sK5,sK3))))) )
| $less(sK4,0)
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| spl7_1 ),
inference(resolution,[],[f212,f218]) ).
tff(f744,plain,
( $less(sK4,0)
| ( tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK2,sK6(sK0,sK2,sK4,sK5,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK0)),t2tb($sum(sK4,sK6(sK0,sK2,sK4,sK5,sK3))))) )
| $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| spl7_1
| spl7_13 ),
inference(forward_subsumption_resolution,[],[f735,f319]) ).
tff(f745,plain,
( $less($sum(length1(char,t2tb1(sK0)),$uminus(sK5)),sK4)
| $less($sum(length1(char,t2tb1(sK3)),$uminus(sK5)),sK2)
| ( tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK2,sK6(sK0,sK2,sK4,sK5,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK0)),t2tb($sum(sK4,sK6(sK0,sK2,sK4,sK5,sK3))))) )
| spl7_1
| spl7_12
| spl7_13 ),
inference(forward_subsumption_resolution,[],[f744,f312]) ).
tff(f747,definition,
( spl7_33
<=> ( tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK2,sK6(sK0,sK2,sK4,sK5,sK3))))) = tb2t2(get(char,int,elts(char,t2tb1(sK0)),t2tb($sum(sK4,sK6(sK0,sK2,sK4,sK5,sK3))))) ) ),
introduced(definition,[new_symbols(definition,[spl7_33])],[avatar_definition]) ).
tff(f749,plain,
( ( tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK2,sK6(sK0,sK2,sK4,sK5,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK0)),t2tb($sum(sK4,sK6(sK0,sK2,sK4,sK5,sK3))))) )
| spl7_33 ),
inference(avatar_component_clause,[],[f747]) ).
tff(f750,plain,
( spl7_25
| ~ spl7_33
| spl7_24
| spl7_1
| spl7_12
| spl7_13 ),
inference(avatar_split_clause,[],[f745,f317,f310,f216,f676,f747,f680]) ).
tff(f936,plain,
( $less(sK6(sK0,sK2,sK4,sK5,sK3),sK1)
| ~ spl7_3
| ~ spl7_27 ),
inference(unit_resulting_resolution,[],[f240,f700]) ).
tff(f949,definition,
( spl7_55
<=> $less(sK6(sK0,sK2,sK4,sK5,sK3),sK1) ),
introduced(definition,[new_symbols(definition,[spl7_55])],[avatar_definition]) ).
tff(f951,plain,
( $less(sK6(sK0,sK2,sK4,sK5,sK3),sK1)
| ~ spl7_55 ),
inference(avatar_component_clause,[],[f949]) ).
tff(f952,plain,
( spl7_55
| ~ spl7_3
| ~ spl7_27 ),
inference(avatar_split_clause,[],[f936,f698,f226,f949]) ).
tff(f1115,plain,
( ~ $less(sK6(sK0,sK2,sK4,sK5,sK3),sK1)
| ~ spl7_2
| spl7_26
| spl7_33 ),
inference(unit_resulting_resolution,[],[f662,f686,f749]) ).
tff(f1124,plain,
( $false
| ~ spl7_2
| spl7_26
| spl7_33
| ~ spl7_55 ),
inference(forward_subsumption_resolution,[],[f1115,f951]) ).
tff(f1125,plain,
( ~ spl7_2
| spl7_26
| spl7_33
| ~ spl7_55 ),
inference(avatar_contradiction_clause,[],[f1124]) ).
tff(f1126,plain,
$false,
inference(avatar_smt_refutation,[],[f1125,f952,f750,f701,f687,f465,f458,f320,f313,f229,f224,f219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW610_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.06/0.20 % Computer : n009.cluster.edu
% 0.06/0.20 % Model : x86_64 x86_64
% 0.06/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.20 % Memory : 8046.5625MB
% 0.06/0.20 % OS : Linux 6.8.0-71-generic
% 0.06/0.20 % CPULimit : 300
% 0.06/0.20 % WCLimit : 300
% 0.06/0.20 % DateTime : Mon Sep 28 14:21:45 UTC 2026
% 0.06/0.20 % CPUTime :
% 0.06/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.24 Running first-order theorem proving
% 0.06/0.24 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.13/1.17 % (3058987)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.13/1.17 % (3058992)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3285451765:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.13/1.17 % (3058992)Instruction limit reached!
% 3.13/1.17 % (3058992)------------------------------
% 3.13/1.17 % (3058992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.17 % (3058992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.17 % (3058992)CaDiCaL version: 2.1.3
% 3.13/1.17 % (3058992)Termination reason: Instruction limit
% 3.13/1.17 % (3058992)Termination phase: Saturation
% 3.13/1.17 % (3058992)Time elapsed: 0.019 s
% 3.13/1.17 % (3058992)Peak memory usage: 115 MB
% 3.13/1.17 % (3058992)Instructions burned: 13 (million)
% 3.13/1.17 % (3058996)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=123403052:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.13/1.17 % (3058996)Instruction limit reached!
% 3.13/1.17 % (3058996)------------------------------
% 3.13/1.17 % (3058996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.17 % (3058996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.17 % (3058996)CaDiCaL version: 2.1.3
% 3.13/1.17 % (3058996)Termination reason: Instruction limit
% 3.13/1.17 % (3058996)Termination phase: Saturation
% 3.13/1.17 % (3058996)Time elapsed: 0.003 s
% 3.13/1.17 % (3058996)Peak memory usage: 88 MB
% 3.13/1.17 % (3058996)Instructions burned: 4 (million)
% 3.13/1.17 % (3058994)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3963296422:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.13/1.17 % (3058993)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3178949224:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.13/1.17 % (3058995)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=342881125:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.13/1.17 % (3058995)Instruction limit reached!
% 3.13/1.17 % (3058995)------------------------------
% 3.13/1.17 % (3058995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.17 % (3058995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.17 % (3058995)CaDiCaL version: 2.1.3
% 3.13/1.17 % (3058995)Termination reason: Instruction limit
% 3.13/1.17 % (3058995)Termination phase: Saturation
% 3.13/1.17 % (3058995)Time elapsed: 0.005 s
% 3.13/1.17 % (3058995)Peak memory usage: 88 MB
% 3.13/1.17 % (3058995)Instructions burned: 7 (million)
% 3.13/1.17 % (3058997)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3091573287:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.13/1.17 % (3058998)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2015702180:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.13/1.17 % (3058998)Instruction limit reached!
% 3.13/1.17 % (3058998)------------------------------
% 3.13/1.17 % (3058998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.17 % (3058998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.17 % (3058998)CaDiCaL version: 2.1.3
% 3.13/1.17 % (3058998)Termination reason: Instruction limit
% 3.13/1.17 % (3058998)Termination phase: Saturation
% 3.13/1.17 % (3058998)Time elapsed: 0.046 s
% 3.13/1.17 % (3058998)Peak memory usage: 116 MB
% 3.13/1.17 % (3058998)Instructions burned: 33 (million)
% 3.13/1.17 % (3058997)Instruction limit reached!
% 3.13/1.17 % (3058997)------------------------------
% 3.13/1.17 % (3058997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.17 % (3058997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.17 % (3058997)CaDiCaL version: 2.1.3
% 3.13/1.17 % (3058997)Termination reason: Instruction limit
% 3.13/1.17 % (3058997)Termination phase: Saturation
% 3.13/1.17 % (3058997)Time elapsed: 0.055 s
% 3.13/1.17 % (3058997)Peak memory usage: 116 MB
% 3.13/1.17 % (3058997)Instructions burned: 47 (million)
% 3.13/1.17 % (3059001)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1330760647:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.13/1.17 % (3059001)Instruction limit reached!
% 3.13/1.17 % (3059001)------------------------------
% 4.31/1.33 % (3059001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.33 % (3059001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.33 % (3059001)CaDiCaL version: 2.1.3
% 4.31/1.33 % (3059001)Termination reason: Instruction limit
% 4.31/1.33 % (3059001)Termination phase: Saturation
% 4.31/1.33 % (3059001)Time elapsed: 0.006 s
% 4.31/1.33 % (3059001)Peak memory usage: 88 MB
% 4.31/1.33 % (3059001)Instructions burned: 15 (million)
% 4.31/1.33 % (3059005)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=3390363229:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.31/1.33 % (3059005)Instruction limit reached!
% 4.31/1.33 % (3059005)------------------------------
% 4.31/1.33 % (3059005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.33 % (3059005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.33 % (3059005)CaDiCaL version: 2.1.3
% 4.31/1.33 % (3059006)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2029467389:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.31/1.33 % (3059005)Termination reason: Instruction limit
% 4.31/1.33 % (3059005)Termination phase: Saturation
% 4.31/1.33 % (3059005)Time elapsed: 0.023 s
% 4.31/1.33 % (3059005)Peak memory usage: 89 MB
% 4.31/1.33 % (3059005)Instructions burned: 29 (million)
% 4.31/1.33 % (3059006)Instruction limit reached!
% 4.31/1.33 % (3059006)------------------------------
% 4.31/1.33 % (3059006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.33 % (3059006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.33 % (3059006)CaDiCaL version: 2.1.3
% 4.31/1.33 % (3059006)Termination reason: Instruction limit
% 4.31/1.33 % (3059006)Termination phase: Saturation
% 4.31/1.33 % (3059006)Time elapsed: 0.011 s
% 4.31/1.33 % (3059006)Peak memory usage: 90 MB
% 4.31/1.33 % (3059006)Instructions burned: 17 (million)
% 4.31/1.33 % (3058994)Instruction limit reached!
% 4.31/1.33 % (3058994)------------------------------
% 4.31/1.33 % (3058994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.33 % (3058994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.33 % (3058994)CaDiCaL version: 2.1.3
% 4.31/1.33 % (3058994)Termination reason: Instruction limit
% 4.31/1.33 % (3058994)Termination phase: Saturation
% 4.31/1.33 % (3058994)Time elapsed: 0.165 s
% 4.31/1.33 % (3058994)Peak memory usage: 119 MB
% 4.31/1.33 % (3058994)Instructions burned: 201 (million)
% 4.31/1.33 % (3059012)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2383346063:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.31/1.33 % (3058993)Instruction limit reached!
% 4.31/1.33 % (3058993)------------------------------
% 4.31/1.33 % (3058993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.33 % (3058993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.33 % (3058993)CaDiCaL version: 2.1.3
% 4.31/1.33 % (3058993)Termination reason: Instruction limit
% 4.31/1.33 % (3058993)Termination phase: Saturation
% 4.31/1.33 % (3058993)Time elapsed: 0.193 s
% 4.31/1.33 % (3058993)Peak memory usage: 116 MB
% 4.31/1.33 % (3058993)Instructions burned: 308 (million)
% 4.31/1.33 % (3059009)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1069320794:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.31/1.33 % (3059012)Instruction limit reached!
% 4.31/1.33 % (3059012)------------------------------
% 4.31/1.33 % (3059012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.33 % (3059012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.33 % (3059012)CaDiCaL version: 2.1.3
% 4.31/1.33 % (3059012)Termination reason: Instruction limit
% 4.31/1.33 % (3059012)Termination phase: Saturation
% 4.31/1.33 % (3059012)Time elapsed: 0.024 s
% 4.31/1.33 % (3059012)Peak memory usage: 89 MB
% 4.31/1.33 % (3059012)Instructions burned: 86 (million)
% 4.31/1.33 % (3059010)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=3354782840:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.31/1.33 % (3059009)Instruction limit reached!
% 4.31/1.33 % (3059009)------------------------------
% 4.31/1.33 % (3059009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/1.51 % (3059009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/1.51 % (3059009)CaDiCaL version: 2.1.3
% 4.88/1.51 % (3059009)Termination reason: Instruction limit
% 4.88/1.51 % (3059009)Termination phase: Saturation
% 4.88/1.51 % (3059009)Time elapsed: 0.020 s
% 4.88/1.51 % (3059009)Peak memory usage: 89 MB
% 4.88/1.51 % (3059009)Instructions burned: 25 (million)
% 4.88/1.51 % (3059010)Instruction limit reached!
% 4.88/1.51 % (3059010)------------------------------
% 4.88/1.51 % (3059010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/1.51 % (3059010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/1.51 % (3059010)CaDiCaL version: 2.1.3
% 4.88/1.51 % (3059010)Termination reason: Instruction limit
% 4.88/1.51 % (3059010)Termination phase: Saturation
% 4.88/1.51 % (3059010)Time elapsed: 0.016 s
% 4.88/1.51 % (3059010)Peak memory usage: 89 MB
% 4.88/1.51 % (3059010)Instructions burned: 28 (million)
% 4.88/1.51 % (3059015)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=301463453:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 4.88/1.51 % (3059015)Instruction limit reached!
% 4.88/1.51 % (3059015)------------------------------
% 4.88/1.51 % (3059015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/1.51 % (3059015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/1.51 % (3059015)CaDiCaL version: 2.1.3
% 4.88/1.51 % (3059015)Termination reason: Instruction limit
% 4.88/1.51 % (3059015)Termination phase: Property scanning
% 4.88/1.51 % (3059015)Time elapsed: 0.002 s
% 4.88/1.51 % (3059015)Peak memory usage: 86 MB
% 4.88/1.51 % (3059015)Instructions burned: 2 (million)
% 4.88/1.51 % (3059021)lrs+10_1_thi=all:si=on:fd=off:random_seed=1701891264:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 4.88/1.51 % (3059016)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1412168412:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 4.88/1.51 % (3059016)Refutation not found, incomplete strategy
% 4.88/1.51 % (3059016)------------------------------
% 4.88/1.51 % (3059016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/1.51 % (3059016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/1.51 % (3059016)CaDiCaL version: 2.1.3
% 4.88/1.51 % (3059016)Termination reason: Refutation not found, incomplete strategy
% 4.88/1.51 % (3059016)Time elapsed: 0.002 s
% 4.88/1.51 % (3059016)Peak memory usage: 89 MB
% 4.88/1.51 % (3059016)Instructions burned: 1 (million)
% 4.88/1.51 % (3059017)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3860517754:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 4.88/1.51 % (3059017)Instruction limit reached!
% 4.88/1.51 % (3059017)------------------------------
% 4.88/1.51 % (3059017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/1.51 % (3059017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/1.51 % (3059017)CaDiCaL version: 2.1.3
% 4.88/1.51 % (3059017)Termination reason: Instruction limit
% 4.88/1.51 % (3059017)Termination phase: Saturation
% 4.88/1.51 % (3059017)Time elapsed: 0.003 s
% 4.88/1.51 % (3059017)Peak memory usage: 87 MB
% 4.88/1.51 % (3059017)Instructions burned: 5 (million)
% 4.88/1.51 % (3059021)Instruction limit reached!
% 4.88/1.51 % (3059021)------------------------------
% 4.88/1.51 % (3059021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/1.51 % (3059021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/1.51 % (3059021)CaDiCaL version: 2.1.3
% 4.88/1.51 % (3059021)Termination reason: Instruction limit
% 4.88/1.51 % (3059021)Termination phase: Saturation
% 4.88/1.51 % (3059021)Time elapsed: 0.036 s
% 4.88/1.51 % (3059021)Peak memory usage: 116 MB
% 4.88/1.51 % (3059021)Instructions burned: 55 (million)
% 4.88/1.51 % (3059020)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1245565649:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 4.88/1.51 % (3059024)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=944567634:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 4.88/1.51 % (3059024)Instruction limit reached!
% 4.88/1.51 % (3059024)------------------------------
% 4.88/1.51 % (3059024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059024)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059024)Termination reason: Instruction limit
% 6.07/1.64 % (3059024)Termination phase: Property scanning
% 6.07/1.64 % (3059024)Time elapsed: 0.002 s
% 6.07/1.64 % (3059024)Peak memory usage: 86 MB
% 6.07/1.64 % (3059024)Instructions burned: 2 (million)
% 6.07/1.64 % (3059023)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=684481804:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 6.07/1.64 % (3059023)Instruction limit reached!
% 6.07/1.64 % (3059023)------------------------------
% 6.07/1.64 % (3059023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059023)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059023)Termination reason: Instruction limit
% 6.07/1.64 % (3059023)Termination phase: Saturation
% 6.07/1.64 % (3059023)Time elapsed: 0.005 s
% 6.07/1.64 % (3059023)Peak memory usage: 88 MB
% 6.07/1.64 % (3059023)Instructions burned: 8 (million)
% 6.07/1.64 % (3059027)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3835507913:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.07/1.64 % (3059031)dis+10_1_si=on:random_seed=3416587120:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 6.07/1.64 % (3059027)Instruction limit reached!
% 6.07/1.64 % (3059027)------------------------------
% 6.07/1.64 % (3059027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059027)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059027)Termination reason: Instruction limit
% 6.07/1.64 % (3059027)Termination phase: Property scanning
% 6.07/1.64 % (3059027)Time elapsed: 0.002 s
% 6.07/1.64 % (3059027)Peak memory usage: 86 MB
% 6.07/1.64 % (3059027)Instructions burned: 3 (million)
% 6.07/1.64 % (3059020)Instruction limit reached!
% 6.07/1.64 % (3059020)------------------------------
% 6.07/1.64 % (3059020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059020)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059020)Termination reason: Instruction limit
% 6.07/1.64 % (3059020)Termination phase: Saturation
% 6.07/1.64 % (3059020)Time elapsed: 0.087 s
% 6.07/1.64 % (3059020)Peak memory usage: 134 MB
% 6.07/1.64 % (3059020)Instructions burned: 67 (million)
% 6.07/1.64 % (3059031)Instruction limit reached!
% 6.07/1.64 % (3059031)------------------------------
% 6.07/1.64 % (3059031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059031)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059031)Termination reason: Instruction limit
% 6.07/1.64 % (3059031)Termination phase: Saturation
% 6.07/1.64 % (3059031)Time elapsed: 0.004 s
% 6.07/1.64 % (3059031)Peak memory usage: 88 MB
% 6.07/1.64 % (3059031)Instructions burned: 13 (million)
% 6.07/1.64 % (3059030)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3143832983:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.07/1.64 % (3059035)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1706827975:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.07/1.64 % (3059035)Refutation not found, incomplete strategy
% 6.07/1.64 % (3059035)------------------------------
% 6.07/1.64 % (3059035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059035)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059035)Termination reason: Refutation not found, incomplete strategy
% 6.07/1.64 % (3059035)Time elapsed: 0.005 s
% 6.07/1.64 % (3059035)Peak memory usage: 89 MB
% 6.07/1.64 % (3059035)Instructions burned: 6 (million)
% 6.07/1.64 % (3059036)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2157252229: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)
% 6.07/1.64 % (3059040)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=325759777:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 6.07/1.64 % (3059040)Instruction limit reached!
% 6.07/1.64 % (3059040)------------------------------
% 6.07/1.64 % (3059040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059040)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059040)Termination reason: Instruction limit
% 6.07/1.64 % (3059040)Termination phase: Saturation
% 6.07/1.64 % (3059040)Time elapsed: 0.004 s
% 6.07/1.64 % (3059040)Peak memory usage: 88 MB
% 6.07/1.64 % (3059040)Instructions burned: 9 (million)
% 6.07/1.64 % (3059036)Instruction limit reached!
% 6.07/1.64 % (3059036)------------------------------
% 6.07/1.64 % (3059036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059036)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059036)Termination reason: Instruction limit
% 6.07/1.64 % (3059036)Termination phase: Saturation
% 6.07/1.64 % (3059036)Time elapsed: 0.028 s
% 6.07/1.64 % (3059036)Peak memory usage: 89 MB
% 6.07/1.64 % (3059036)Instructions burned: 36 (million)
% 6.07/1.64 % (3059016)------------------------------
% 6.07/1.64 % (3059016)------------------------------
% 6.07/1.64 % (3059039)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=65207496:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 6.07/1.64 % (3059039)Instruction limit reached!
% 6.07/1.64 % (3059039)------------------------------
% 6.07/1.64 % (3059039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059039)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059039)Termination reason: Instruction limit
% 6.07/1.64 % (3059039)Termination phase: Function definition elimination
% 6.07/1.64 % (3059039)Time elapsed: 0.002 s
% 6.07/1.64 % (3059039)Peak memory usage: 86 MB
% 6.07/1.64 % (3059039)Instructions burned: 3 (million)
% 6.07/1.64 % (3059041)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2790822581:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 6.07/1.64 % (3059030)First to succeed.
% 6.07/1.64 % (3059030)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3058987"
% 6.07/1.64 % (3059046)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3597062935:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 6.07/1.64 % (3059046)Instruction limit reached!
% 6.07/1.64 % (3059046)------------------------------
% 6.07/1.64 % (3059046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059046)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059046)Termination reason: Instruction limit
% 6.07/1.64 % (3059046)Termination phase: Saturation
% 6.07/1.64 % (3059046)Time elapsed: 0.018 s
% 6.07/1.64 % (3059046)Peak memory usage: 115 MB
% 6.07/1.64 % (3059046)Instructions burned: 14 (million)
% 6.07/1.64 % (3059047)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1822478242:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 6.07/1.64 % (3059051)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1764587490:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi)
% 6.07/1.64 % (3059049)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1176815621:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 6.07/1.64 % (3059049)Instruction limit reached!
% 6.07/1.64 % (3059049)------------------------------
% 6.07/1.64 % (3059049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059049)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059049)Termination reason: Instruction limit
% 6.07/1.64 % (3059049)Termination phase: Saturation
% 6.07/1.64 % (3059049)Time elapsed: 0.007 s
% 6.07/1.64 % (3059049)Peak memory usage: 88 MB
% 6.07/1.64 % (3059049)Instructions burned: 10 (million)
% 6.07/1.64 % (3059047)Refutation not found, incomplete strategy
% 6.07/1.64 % (3059047)------------------------------
% 6.07/1.64 % (3059047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059047)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059047)Termination reason: Refutation not found, incomplete strategy
% 6.07/1.64 % (3059047)Time elapsed: 0.029 s
% 6.07/1.64 % (3059047)Peak memory usage: 115 MB
% 6.07/1.64 % (3059047)Instructions burned: 7 (million)
% 6.07/1.64 % (3059053)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=1666678830:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 6.07/1.64 % (3059041)Instruction limit reached!
% 6.07/1.64 % (3059041)------------------------------
% 6.07/1.64 % (3059041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059041)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059041)Termination reason: Instruction limit
% 6.07/1.64 % (3059041)Termination phase: Saturation
% 6.07/1.64 % (3059041)Time elapsed: 0.184 s
% 6.07/1.64 % (3059041)Peak memory usage: 92 MB
% 6.07/1.64 % (3059041)Instructions burned: 370 (million)
% 6.07/1.64 % (3059035)------------------------------
% 6.07/1.64 % (3059035)------------------------------
% 6.07/1.64 % (3059053)Instruction limit reached!
% 6.07/1.64 % (3059053)------------------------------
% 6.07/1.64 % (3059053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059053)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059053)Termination reason: Instruction limit
% 6.07/1.64 % (3059053)Termination phase: Saturation
% 6.07/1.64 % (3059053)Time elapsed: 0.025 s
% 6.07/1.64 % (3059053)Peak memory usage: 89 MB
% 6.07/1.64 % (3059053)Instructions burned: 75 (million)
% 6.07/1.64 % (3059051)Instruction limit reached!
% 6.07/1.64 % (3059051)------------------------------
% 6.07/1.64 % (3059051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.07/1.64 % (3059051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.64 % (3059051)CaDiCaL version: 2.1.3
% 6.07/1.64 % (3059051)Termination reason: Instruction limit
% 6.07/1.64 % (3059051)Termination phase: Saturation
% 6.07/1.64 % (3059051)Time elapsed: 0.086 s
% 6.07/1.64 % (3059051)Peak memory usage: 133 MB
% 6.07/1.64 % (3059051)Instructions burned: 71 (million)
% 6.07/1.64 % (3059030)Refutation found. Thanks to Tanya!
% 6.07/1.64 % SZS status Theorem for theBenchmark
% 6.07/1.64 % SZS output start Proof for theBenchmark
% See solution above
% 7.38/1.84 % (3059030)------------------------------
% 7.38/1.84 % (3059030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.38/1.84 % (3059030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.38/1.84 % (3059030)CaDiCaL version: 2.1.3
% 7.38/1.84 % (3059030)Termination reason: Refutation
% 7.38/1.84 % (3059030)Time elapsed: 0.109 s
% 7.38/1.84 % (3059030)Peak memory usage: 118 MB
% 7.38/1.84 % (3059030)Instructions burned: 119 (million)
% 7.38/1.84 % (3059030)------------------------------
% 7.38/1.84 % (3059030)------------------------------
% 7.38/1.84 % (3058987)Success in time 0.962 s
% 7.38/1.84 % Vampire exiting
%------------------------------------------------------------------------------