%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW633_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 : 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:31:00 PM UTC 2026
% Result : Theorem 26.01s 4.11s
% Output : Refutation 26.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 43
% Syntax : Number of formulae : 156 ( 21 unt; 0 typ; 32 def)
% Number of atoms : 456 ( 152 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 473 ( 173 ~; 175 |; 53 &)
% ( 26 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 707 ( 181 atm; 93 fun; 317 num; 116 var)
% Number of types : 6 ( 4 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 31 ( 27 usr; 27 prp; 0-2 aty)
% Number of functors : 28 ( 22 usr; 19 con; 0-4 aty)
% Number of variables : 116 ( 114 !; 2 ?; 116 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
power: ( $int * $int ) > $int ).
tff(func_def_16,type,
abs: $int > $int ).
tff(func_def_18,type,
div: ( $int * $int ) > $int ).
tff(func_def_19,type,
mod: ( $int * $int ) > $int ).
tff(func_def_21,type,
sK0: $int ).
tff(func_def_22,type,
sK1: $int ).
tff(func_def_23,type,
sF2: $int ).
tff(func_def_24,type,
sF3: $int ).
tff(func_def_25,type,
sF4: $int ).
tff(func_def_26,type,
sF5: $int ).
tff(func_def_27,type,
sF6: $int ).
tff(func_def_28,type,
sF7: $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(f9,axiom,
! [X0: $int] : ( power(X0,0) = 1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_0) ).
tff(f10,axiom,
! [X1: $int,X0: $int] :
( $lesseq(0,X1)
=> ( power(X0,$sum(X1,1)) = $product(X0,power(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_s) ).
tff(f13,axiom,
! [X0: $int,X1: $int,X2: $int] :
( $lesseq(0,X1)
=> ( $lesseq(0,X2)
=> ( power(X0,$sum(X1,X2)) = $product(power(X0,X1),power(X0,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_sum) ).
tff(f16,axiom,
! [X0: $int] :
( ( $lesseq(0,X0)
=> ( abs(X0) = X0 ) )
& ( ~ $lesseq(0,X0)
=> ( abs(X0) = $uminus(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',abs_def) ).
tff(f19,axiom,
! [X1: $int,X0: $int] :
( ( X1 != 0 )
=> ( X0 = $sum($product(X1,div(X0,X1)),mod(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',div_mod) ).
tff(f20,axiom,
! [X1: $int,X0: $int] :
( ( $lesseq(0,X0)
& $less(0,X1) )
=> ( $lesseq(div(X0,X1),X0)
& $lesseq(0,div(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',div_bound) ).
tff(f21,axiom,
! [X1: $int,X0: $int] :
( ( X1 != 0 )
=> ( $less(mod(X0,X1),abs(X1))
& $less($uminus(abs(X1)),mod(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod_bound) ).
tff(f23,axiom,
! [X1: $int,X0: $int] :
( ( $less(0,X1)
& $lesseq(X0,0) )
=> $lesseq(div(X0,X1),0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',div_sign_neg) ).
tff(f24,axiom,
! [X1: $int,X0: $int] :
( ( ( X1 != 0 )
& $lesseq(0,X0) )
=> $lesseq(0,mod(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mod_sign_pos) ).
tff(f29,axiom,
! [X0: $int,X1: $int] :
( ( $lesseq(0,X0)
& $less(X0,X1) )
=> ( div(X0,X1) = 0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',div_inf) ).
tff(f33,conjecture,
! [X1: $int,X0: $int] :
( $lesseq(0,X1)
=> ( ( ( X1 = 0 )
=> ( 1 = power(X0,X1) ) )
& ( ( X1 != 0 )
=> ( ( ( mod(X1,2) != 0 )
=> ( $product($product(power(X0,div(X1,2)),power(X0,div(X1,2))),X0) = power(X0,X1) ) )
& ( ( mod(X1,2) = 0 )
=> ( $product(power(X0,div(X1,2)),power(X0,div(X1,2))) = power(X0,X1) ) )
& $lesseq(0,div(X1,2))
& $less(div(X1,2),X1)
& $lesseq(0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_fast_exp) ).
tff(f34,negated_conjecture,
~ ! [X1: $int,X0: $int] :
( $lesseq(0,X1)
=> ( ( ( X1 = 0 )
=> ( 1 = power(X0,X1) ) )
& ( ( X1 != 0 )
=> ( ( ( mod(X1,2) != 0 )
=> ( $product($product(power(X0,div(X1,2)),power(X0,div(X1,2))),X0) = power(X0,X1) ) )
& ( ( mod(X1,2) = 0 )
=> ( $product(power(X0,div(X1,2)),power(X0,div(X1,2))) = power(X0,X1) ) )
& $lesseq(0,div(X1,2))
& $less(div(X1,2),X1)
& $lesseq(0,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
tff(f35,plain,
! [X1: $int,X0: $int] :
( ~ $less(X1,0)
=> ( power(X0,$sum(X1,1)) = $product(X0,power(X0,X1)) ) ),
inference(theory_normalization,[],[f10]) ).
tff(f38,plain,
! [X1: $int,X0: $int] :
( ( $less(0,X1)
& ~ $less(0,X0) )
=> ~ $less(0,div(X0,X1)) ),
inference(theory_normalization,[],[f23]) ).
tff(f40,plain,
! [X1: $int,X0: $int] :
( ( ( X1 != 0 )
& ~ $less(X0,0) )
=> ~ $less(mod(X0,X1),0) ),
inference(theory_normalization,[],[f24]) ).
tff(f46,plain,
! [X0: $int] :
( ( ~ $less(X0,0)
=> ( abs(X0) = X0 ) )
& ( $less(X0,0)
=> ( abs(X0) = $uminus(X0) ) ) ),
inference(theory_normalization,[],[f16]) ).
tff(f47,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(X0,0)
& $less(0,X1) )
=> ( ~ $less(X0,div(X0,X1))
& ~ $less(div(X0,X1),0) ) ),
inference(theory_normalization,[],[f20]) ).
tff(f48,plain,
~ ! [X1: $int,X0: $int] :
( ~ $less(X1,0)
=> ( ( ( X1 = 0 )
=> ( 1 = power(X0,X1) ) )
& ( ( X1 != 0 )
=> ( ( ( mod(X1,2) != 0 )
=> ( $product($product(power(X0,div(X1,2)),power(X0,div(X1,2))),X0) = power(X0,X1) ) )
& ( ( mod(X1,2) = 0 )
=> ( $product(power(X0,div(X1,2)),power(X0,div(X1,2))) = power(X0,X1) ) )
& ~ $less(div(X1,2),0)
& $less(div(X1,2),X1)
& ~ $less(X1,0) ) ) ) ),
inference(theory_normalization,[],[f34]) ).
tff(f50,plain,
! [X1: $int,X0: $int] :
( ( $less(X0,X1)
& ~ $less(X0,0) )
=> ( div(X0,X1) = 0 ) ),
inference(theory_normalization,[],[f29]) ).
tff(f53,plain,
! [X2: $int,X1: $int,X0: $int] :
( ~ $less(X1,0)
=> ( ~ $less(X2,0)
=> ( power(X0,$sum(X1,X2)) = $product(power(X0,X1),power(X0,X2)) ) ) ),
inference(theory_normalization,[],[f13]) ).
tff(f55,plain,
! [X1: $int,X0: $int] :
( ~ $less(X0,0)
=> ( $product(X1,power(X1,X0)) = power(X1,$sum(X0,1)) ) ),
inference(rectify,[],[f35]) ).
tff(f58,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(0,X1)
& $less(0,X0) )
=> ~ $less(0,div(X1,X0)) ),
inference(rectify,[],[f38]) ).
tff(f59,plain,
! [X1: $int,X0: $int] :
( ( ( 0 != X0 )
& ~ $less(X1,0) )
=> ~ $less(mod(X1,X0),0) ),
inference(rectify,[],[f40]) ).
tff(f66,plain,
! [X1: $int,X0: $int] :
( ( $less(0,X0)
& ~ $less(X1,0) )
=> ( ~ $less(div(X1,X0),0)
& ~ $less(X1,div(X1,X0)) ) ),
inference(rectify,[],[f47]) ).
tff(f67,plain,
~ ! [X0: $int,X1: $int] :
( ~ $less(X0,0)
=> ( ( ( 0 = X0 )
=> ( 1 = power(X1,X0) ) )
& ( ( 0 != X0 )
=> ( ( ( 0 = mod(X0,2) )
=> ( $product(power(X1,div(X0,2)),power(X1,div(X0,2))) = power(X1,X0) ) )
& $less(div(X0,2),X0)
& ~ $less(div(X0,2),0)
& ~ $less(X0,0)
& ( ( 0 != mod(X0,2) )
=> ( power(X1,X0) = $product($product(power(X1,div(X0,2)),power(X1,div(X0,2))),X1) ) ) ) ) ) ),
inference(rectify,[],[f48]) ).
tff(f68,plain,
! [X1: $int,X0: $int] :
( ( 0 != X0 )
=> ( $sum($product(X0,div(X1,X0)),mod(X1,X0)) = X1 ) ),
inference(rectify,[],[f19]) ).
tff(f69,plain,
! [X1: $int,X0: $int] :
( ( 0 != X0 )
=> ( $less($uminus(abs(X0)),mod(X1,X0))
& $less(mod(X1,X0),abs(X0)) ) ),
inference(rectify,[],[f21]) ).
tff(f78,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( power(X0,$sum(X1,X2)) = $product(power(X0,X1),power(X0,X2)) )
| $less(X2,0)
| $less(X1,0) ),
inference(ennf_transformation,[],[f53]) ).
tff(f79,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( power(X0,$sum(X1,X2)) = $product(power(X0,X1),power(X0,X2)) )
| $less(X2,0)
| $less(X1,0) ),
inference(flattening,[],[f78]) ).
tff(f80,plain,
! [X0: $int,X1: $int] :
( ( $sum($product(X0,div(X1,X0)),mod(X1,X0)) = X1 )
| ( 0 = X0 ) ),
inference(ennf_transformation,[],[f68]) ).
tff(f81,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(div(X1,X0),0)
& ~ $less(X1,div(X1,X0)) )
| ~ $less(0,X0)
| $less(X1,0) ),
inference(ennf_transformation,[],[f66]) ).
tff(f82,plain,
! [X0: $int,X1: $int] :
( ~ $less(0,X0)
| $less(X1,0)
| ( ~ $less(div(X1,X0),0)
& ~ $less(X1,div(X1,X0)) ) ),
inference(flattening,[],[f81]) ).
tff(f85,plain,
! [X1: $int,X0: $int] :
( ~ $less(0,div(X1,X0))
| $less(0,X1)
| ~ $less(0,X0) ),
inference(ennf_transformation,[],[f58]) ).
tff(f86,plain,
! [X1: $int,X0: $int] :
( $less(0,X1)
| ~ $less(0,div(X1,X0))
| ~ $less(0,X0) ),
inference(flattening,[],[f85]) ).
tff(f87,plain,
! [X1: $int,X0: $int] :
( ( $less($uminus(abs(X0)),mod(X1,X0))
& $less(mod(X1,X0),abs(X0)) )
| ( 0 = X0 ) ),
inference(ennf_transformation,[],[f69]) ).
tff(f88,plain,
! [X1: $int,X0: $int] :
( $less(X0,0)
| ( $product(X1,power(X1,X0)) = power(X1,$sum(X0,1)) ) ),
inference(ennf_transformation,[],[f55]) ).
tff(f94,plain,
! [X0: $int] :
( ( ( abs(X0) = X0 )
| $less(X0,0) )
& ( ~ $less(X0,0)
| ( abs(X0) = $uminus(X0) ) ) ),
inference(ennf_transformation,[],[f46]) ).
tff(f96,plain,
! [X1: $int,X0: $int] :
( ( div(X0,X1) = 0 )
| ~ $less(X0,X1)
| $less(X0,0) ),
inference(ennf_transformation,[],[f50]) ).
tff(f97,plain,
! [X0: $int,X1: $int] :
( ( div(X0,X1) = 0 )
| $less(X0,0)
| ~ $less(X0,X1) ),
inference(flattening,[],[f96]) ).
tff(f98,plain,
! [X1: $int,X0: $int] :
( ~ $less(mod(X1,X0),0)
| ( 0 = X0 )
| $less(X1,0) ),
inference(ennf_transformation,[],[f59]) ).
tff(f99,plain,
! [X1: $int,X0: $int] :
( ~ $less(mod(X1,X0),0)
| $less(X1,0)
| ( 0 = X0 ) ),
inference(flattening,[],[f98]) ).
tff(f103,plain,
? [X0: $int,X1: $int] :
( ~ $less(X0,0)
& ( ( ( 0 != X0 )
& ( ~ $less(div(X0,2),X0)
| ( ( 0 = mod(X0,2) )
& ( $product(power(X1,div(X0,2)),power(X1,div(X0,2))) != power(X1,X0) ) )
| $less(X0,0)
| $less(div(X0,2),0)
| ( ( 0 != mod(X0,2) )
& ( power(X1,X0) != $product($product(power(X1,div(X0,2)),power(X1,div(X0,2))),X1) ) ) ) )
| ( ( 0 = X0 )
& ( 1 != power(X1,X0) ) ) ) ),
inference(ennf_transformation,[],[f67]) ).
tff(f107,plain,
! [X0: $int,X1: $int] :
( $less(0,X0)
| ~ $less(0,div(X0,X1))
| ~ $less(0,X1) ),
inference(rectify,[],[f86]) ).
tff(f110,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( $product(power(X2,X1),power(X2,X0)) = power(X2,$sum(X1,X0)) )
| $less(X0,0)
| $less(X1,0) ),
inference(rectify,[],[f79]) ).
tff(f112,plain,
! [X0: $int,X1: $int] :
( ~ $less(mod(X0,X1),0)
| $less(X0,0)
| ( 0 = X1 ) ),
inference(rectify,[],[f99]) ).
tff(f113,plain,
! [X0: $int,X1: $int] :
( ( $less($uminus(abs(X1)),mod(X0,X1))
& $less(mod(X0,X1),abs(X1)) )
| ( 0 = X1 ) ),
inference(rectify,[],[f87]) ).
tff(f118,plain,
( ~ $less(sK0,0)
& ( ( ( 0 != sK0 )
& ( ~ $less(div(sK0,2),sK0)
| ( ( 0 = mod(sK0,2) )
& ( power(sK1,sK0) != $product(power(sK1,div(sK0,2)),power(sK1,div(sK0,2))) ) )
| $less(sK0,0)
| $less(div(sK0,2),0)
| ( ( 0 != mod(sK0,2) )
& ( power(sK1,sK0) != $product($product(power(sK1,div(sK0,2)),power(sK1,div(sK0,2))),sK1) ) ) ) )
| ( ( 0 = sK0 )
& ( 1 != power(sK1,sK0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f103]) ).
tff(f120,plain,
! [X0: $int,X1: $int] :
( $less(X1,0)
| ( power(X0,$sum(X1,1)) = $product(X0,power(X0,X1)) ) ),
inference(rectify,[],[f88]) ).
tff(f127,plain,
! [X0: $int,X1: $int] :
( ( $sum($product(X0,div(X1,X0)),mod(X1,X0)) = X1 )
| ( 0 = X0 ) ),
inference(cnf_transformation,[],[f80]) ).
tff(f129,plain,
! [X0: $int,X1: $int] :
( ~ $less(0,div(X0,X1))
| ~ $less(0,X1)
| $less(0,X0) ),
inference(cnf_transformation,[],[f107]) ).
tff(f132,plain,
! [X2: $int,X0: $int,X1: $int] :
( ( $product(power(X2,X1),power(X2,X0)) = power(X2,$sum(X1,X0)) )
| $less(X1,0)
| $less(X0,0) ),
inference(cnf_transformation,[],[f110]) ).
tff(f135,plain,
! [X0: $int,X1: $int] :
( ~ $less(mod(X0,X1),0)
| $less(X0,0)
| ( 0 = X1 ) ),
inference(cnf_transformation,[],[f112]) ).
tff(f137,plain,
! [X0: $int,X1: $int] :
( $less(mod(X0,X1),abs(X1))
| ( 0 = X1 ) ),
inference(cnf_transformation,[],[f113]) ).
tff(f140,plain,
! [X0: $int,X1: $int] :
( ~ $less(div(X1,X0),0)
| $less(X1,0)
| ~ $less(0,X0) ),
inference(cnf_transformation,[],[f82]) ).
tff(f141,plain,
! [X0: $int,X1: $int] :
( ( 0 = div(X0,X1) )
| ~ $less(X0,X1)
| $less(X0,0) ),
inference(cnf_transformation,[],[f97]) ).
tff(f151,plain,
( ~ $less(div(sK0,2),sK0)
| ( power(sK1,sK0) != $product(power(sK1,div(sK0,2)),power(sK1,div(sK0,2))) )
| $less(sK0,0)
| $less(div(sK0,2),0)
| ( 0 != mod(sK0,2) )
| ( 0 = sK0 ) ),
inference(cnf_transformation,[],[f118]) ).
tff(f153,plain,
( ~ $less(div(sK0,2),sK0)
| ( 0 = mod(sK0,2) )
| $less(sK0,0)
| $less(div(sK0,2),0)
| ( power(sK1,sK0) != $product($product(power(sK1,div(sK0,2)),power(sK1,div(sK0,2))),sK1) )
| ( 0 = sK0 ) ),
inference(cnf_transformation,[],[f118]) ).
tff(f156,plain,
( ( 0 != sK0 )
| ( 1 != power(sK1,sK0) ) ),
inference(cnf_transformation,[],[f118]) ).
tff(f158,plain,
~ $less(sK0,0),
inference(cnf_transformation,[],[f118]) ).
tff(f160,plain,
! [X0: $int,X1: $int] :
( ( power(X0,$sum(X1,1)) = $product(X0,power(X0,X1)) )
| $less(X1,0) ),
inference(cnf_transformation,[],[f120]) ).
tff(f164,plain,
! [X0: $int] :
( ( abs(X0) = X0 )
| $less(X0,0) ),
inference(cnf_transformation,[],[f94]) ).
tff(f165,plain,
! [X0: $int] : ( power(X0,0) = 1 ),
inference(cnf_transformation,[],[f9]) ).
tff(f175,definition,
sF2 = power(sK1,sK0),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
tff(f176,plain,
power(sK1,sK0) = sF2,
inference(reorient_equations,[],[f175]) ).
tff(f177,plain,
( ( 0 != sK0 )
| ( 1 != sF2 ) ),
inference(definition_folding,[],[f156,f176]) ).
tff(f178,definition,
sF3 = div(sK0,2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
tff(f179,plain,
div(sK0,2) = sF3,
inference(reorient_equations,[],[f178]) ).
tff(f180,definition,
sF4 = mod(sK0,2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
tff(f181,plain,
mod(sK0,2) = sF4,
inference(reorient_equations,[],[f180]) ).
tff(f184,definition,
sF5 = power(sK1,sF3),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
tff(f185,definition,
sF6 = $product(sF5,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f186,plain,
$product(sF5,sF5) = sF6,
inference(reorient_equations,[],[f185]) ).
tff(f187,definition,
sF7 = $product(sF6,sK1),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f188,plain,
( $less(sK0,0)
| ( 0 = sK0 )
| ( 0 = sF4 )
| ~ $less(sF3,sK0)
| $less(sF3,0)
| ( sF2 != sF7 ) ),
inference(definition_folding,[],[f153,f187,f186,f184,f179,f184,f179,f176,f179,f181,f179]) ).
tff(f190,plain,
( ( sF2 != sF6 )
| ~ $less(sF3,sK0)
| $less(sK0,0)
| $less(sF3,0)
| ( 0 = sK0 )
| ( 0 != sF4 ) ),
inference(definition_folding,[],[f151,f181,f179,f186,f184,f179,f184,f179,f176,f179]) ).
tff(f196,definition,
( spl8_1
<=> $less(sF3,sK0) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
tff(f200,definition,
( spl8_2
<=> $less(sK0,0) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
tff(f201,plain,
( ~ $less(sK0,0)
| spl8_2 ),
inference(avatar_component_clause,[],[f200]) ).
tff(f204,definition,
( spl8_3
<=> $less(sF3,0) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
tff(f205,plain,
( ~ $less(sF3,0)
| spl8_3 ),
inference(avatar_component_clause,[],[f204]) ).
tff(f208,definition,
( spl8_4
<=> ( 0 = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition]) ).
tff(f212,definition,
( spl8_5
<=> ( sF2 = sF6 ) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
tff(f216,definition,
( spl8_6
<=> ( 0 = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
tff(f219,plain,
( ~ spl8_1
| spl8_2
| spl8_3
| spl8_4
| ~ spl8_5
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f190,f216,f212,f208,f204,f200,f196]) ).
tff(f221,definition,
( spl8_7
<=> ( sF2 = sF7 ) ),
introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition]) ).
tff(f224,plain,
( spl8_3
| ~ spl8_7
| spl8_6
| ~ spl8_1
| spl8_2
| spl8_4 ),
inference(avatar_split_clause,[],[f188,f208,f200,f196,f216,f221,f204]) ).
tff(f226,definition,
( spl8_8
<=> ( div(sK0,2) = sF3 ) ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
tff(f228,plain,
( ( div(sK0,2) = sF3 )
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f226]) ).
tff(f229,plain,
spl8_8,
inference(avatar_split_clause,[],[f179,f226]) ).
tff(f231,definition,
( spl8_9
<=> ( 1 = sF2 ) ),
introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition]) ).
tff(f237,definition,
( spl8_10
<=> ( sF5 = power(sK1,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition]) ).
tff(f239,plain,
( ( sF5 = power(sK1,sF3) )
| ~ spl8_10 ),
inference(avatar_component_clause,[],[f237]) ).
tff(f240,plain,
spl8_10,
inference(avatar_split_clause,[],[f184,f237]) ).
tff(f243,definition,
( spl8_11
<=> ( mod(sK0,2) = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
tff(f245,plain,
( ( mod(sK0,2) = sF4 )
| ~ spl8_11 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f246,plain,
spl8_11,
inference(avatar_split_clause,[],[f181,f243]) ).
tff(f252,plain,
~ spl8_2,
inference(avatar_split_clause,[],[f158,f200]) ).
tff(f254,definition,
( spl8_13
<=> ( sF7 = $product(sF6,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition]) ).
tff(f257,plain,
spl8_13,
inference(avatar_split_clause,[],[f187,f254]) ).
tff(f259,definition,
( spl8_14
<=> ( $product(sF5,sF5) = sF6 ) ),
introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition]) ).
tff(f261,plain,
( ( $product(sF5,sF5) = sF6 )
| ~ spl8_14 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f262,plain,
spl8_14,
inference(avatar_split_clause,[],[f186,f259]) ).
tff(f263,plain,
( ~ spl8_9
| ~ spl8_4 ),
inference(avatar_split_clause,[],[f177,f208,f231]) ).
tff(f266,definition,
( spl8_15
<=> ( power(sK1,sK0) = sF2 ) ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
tff(f269,plain,
spl8_15,
inference(avatar_split_clause,[],[f176,f266]) ).
tff(f285,plain,
( ( 0 = 2 )
| $less(sF4,abs(2))
| ~ spl8_11 ),
inference(superposition,[],[f137,f245]) ).
tff(f289,plain,
( $less(sF4,abs(2))
| ~ spl8_11 ),
inference(evaluation,[],[f285]) ).
tff(f296,definition,
( spl8_17
<=> $less(sF4,abs(2)) ),
introduced(definition,[new_symbols(definition,[spl8_17])],[avatar_definition]) ).
tff(f298,plain,
( $less(sF4,abs(2))
| ~ spl8_17 ),
inference(avatar_component_clause,[],[f296]) ).
tff(f299,plain,
( spl8_17
| ~ spl8_11 ),
inference(avatar_split_clause,[],[f289,f243,f296]) ).
tff(f304,plain,
( $less(sF4,2)
| $less(2,0)
| ~ spl8_17 ),
inference(superposition,[],[f298,f164]) ).
tff(f305,plain,
( $less(sF4,2)
| ~ spl8_17 ),
inference(evaluation,[],[f304]) ).
tff(f307,definition,
( spl8_18
<=> $less(sF4,2) ),
introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition]) ).
tff(f310,plain,
( spl8_18
| ~ spl8_17 ),
inference(avatar_split_clause,[],[f305,f296,f307]) ).
tff(f339,plain,
( ~ $less(0,sF3)
| ~ $less(0,2)
| $less(0,sK0)
| ~ spl8_8 ),
inference(superposition,[],[f129,f228]) ).
tff(f340,plain,
( $less(0,sK0)
| ~ $less(0,sF3)
| ~ spl8_8 ),
inference(evaluation,[],[f339]) ).
tff(f342,definition,
( spl8_22
<=> $less(0,sF3) ),
introduced(definition,[new_symbols(definition,[spl8_22])],[avatar_definition]) ).
tff(f346,definition,
( spl8_23
<=> $less(0,sK0) ),
introduced(definition,[new_symbols(definition,[spl8_23])],[avatar_definition]) ).
tff(f349,plain,
( ~ spl8_22
| spl8_23
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f340,f226,f346,f342]) ).
tff(f351,plain,
( ( 0 = 2 )
| $less(sK0,0)
| ~ $less(sF4,0)
| ~ spl8_11 ),
inference(superposition,[],[f135,f245]) ).
tff(f352,plain,
( ~ $less(sF4,0)
| $less(sK0,0)
| ~ spl8_11 ),
inference(evaluation,[],[f351]) ).
tff(f353,plain,
( ~ $less(sF4,0)
| spl8_2
| ~ spl8_11 ),
inference(forward_subsumption_resolution,[],[f352,f201]) ).
tff(f355,definition,
( spl8_24
<=> $less(sF4,0) ),
introduced(definition,[new_symbols(definition,[spl8_24])],[avatar_definition]) ).
tff(f358,plain,
( ~ spl8_24
| spl8_2
| ~ spl8_11 ),
inference(avatar_split_clause,[],[f353,f243,f200,f355]) ).
tff(f370,plain,
( $less(sK0,0)
| ~ $less(sF3,0)
| ~ $less(0,2)
| ~ spl8_8 ),
inference(superposition,[],[f140,f228]) ).
tff(f371,plain,
( $less(sK0,0)
| ~ $less(sF3,0)
| ~ spl8_8 ),
inference(evaluation,[],[f370]) ).
tff(f372,plain,
( ~ $less(sF3,0)
| spl8_2
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f371,f201]) ).
tff(f373,plain,
( ~ spl8_3
| spl8_2
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f372,f226,f200,f204]) ).
tff(f380,plain,
( $less(sK0,0)
| ~ $less(sK0,2)
| ( 0 = sF3 )
| ~ spl8_8 ),
inference(superposition,[],[f228,f141]) ).
tff(f384,plain,
( ~ $less(sK0,2)
| ( 0 = sF3 )
| spl8_2
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f380,f201]) ).
tff(f386,definition,
( spl8_26
<=> ( 0 = sF3 ) ),
introduced(definition,[new_symbols(definition,[spl8_26])],[avatar_definition]) ).
tff(f388,plain,
( ( 0 = sF3 )
| ~ spl8_26 ),
inference(avatar_component_clause,[],[f386]) ).
tff(f390,definition,
( spl8_27
<=> $less(sK0,2) ),
introduced(definition,[new_symbols(definition,[spl8_27])],[avatar_definition]) ).
tff(f394,plain,
( ~ spl8_27
| spl8_26
| spl8_2
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f384,f226,f200,f386,f390]) ).
tff(f482,plain,
( ( 0 = 2 )
| ( sK0 = $sum($product(2,div(sK0,2)),sF4) )
| ~ spl8_11 ),
inference(superposition,[],[f127,f245]) ).
tff(f483,plain,
( ( sK0 = $sum($product(2,div(sK0,2)),sF4) )
| ~ spl8_11 ),
inference(evaluation,[],[f482]) ).
tff(f488,plain,
( ( $sum($product(2,sF3),sF4) = sK0 )
| ~ spl8_8
| ~ spl8_11 ),
inference(forward_demodulation,[],[f483,f228]) ).
tff(f492,definition,
( spl8_38
<=> ( $sum($product(2,sF3),sF4) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl8_38])],[avatar_definition]) ).
tff(f495,plain,
( spl8_38
| ~ spl8_8
| ~ spl8_11 ),
inference(avatar_split_clause,[],[f488,f243,f226,f492]) ).
tff(f622,plain,
( ! [X0: $int] :
( ( power(sK1,$sum(sF3,X0)) = $product(sF5,power(sK1,X0)) )
| $less(X0,0)
| $less(sF3,0) )
| ~ spl8_10 ),
inference(superposition,[],[f132,f239]) ).
tff(f640,plain,
( ! [X0: $int] :
( ( power(sK1,$sum(sF3,X0)) = $product(sF5,power(sK1,X0)) )
| $less(X0,0) )
| spl8_3
| ~ spl8_10 ),
inference(forward_subsumption_resolution,[],[f622,f205]) ).
tff(f828,plain,
( $less(sF3,0)
| ( $product(sF5,sF5) = power(sK1,$sum(sF3,sF3)) )
| spl8_3
| ~ spl8_10 ),
inference(superposition,[],[f640,f239]) ).
tff(f853,plain,
( ( $product(sF5,sF5) = power(sK1,$sum(sF3,sF3)) )
| spl8_3
| ~ spl8_10 ),
inference(forward_subsumption_resolution,[],[f828,f205]) ).
tff(f870,plain,
( ( sF6 = power(sK1,$sum(sF3,sF3)) )
| spl8_3
| ~ spl8_10
| ~ spl8_14 ),
inference(forward_demodulation,[],[f853,f261]) ).
tff(f872,definition,
( spl8_79
<=> ( sF6 = power(sK1,$sum(sF3,sF3)) ) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
tff(f874,plain,
( ( sF6 = power(sK1,$sum(sF3,sF3)) )
| ~ spl8_79 ),
inference(avatar_component_clause,[],[f872]) ).
tff(f876,plain,
( spl8_79
| spl8_3
| ~ spl8_10
| ~ spl8_14 ),
inference(avatar_split_clause,[],[f870,f259,f237,f204,f872]) ).
tff(f882,plain,
( $less($sum(sF3,sF3),0)
| ( $product(sK1,sF6) = power(sK1,$sum($sum(sF3,sF3),1)) )
| ~ spl8_79 ),
inference(superposition,[],[f160,f874]) ).
tff(f884,definition,
( spl8_80
<=> $less($sum(sF3,sF3),0) ),
introduced(definition,[new_symbols(definition,[spl8_80])],[avatar_definition]) ).
tff(f909,definition,
( spl8_86
<=> ( $product(sK1,sF6) = power(sK1,$sum($sum(sF3,sF3),1)) ) ),
introduced(definition,[new_symbols(definition,[spl8_86])],[avatar_definition]) ).
tff(f912,plain,
( spl8_86
| spl8_80
| ~ spl8_79 ),
inference(avatar_split_clause,[],[f882,f872,f884,f909]) ).
tff(f932,plain,
( ( sF5 = power(sK1,0) )
| ~ spl8_10
| ~ spl8_26 ),
inference(superposition,[],[f239,f388]) ).
tff(f946,plain,
( ( 1 = sF5 )
| ~ spl8_10
| ~ spl8_26 ),
inference(forward_demodulation,[],[f932,f165]) ).
tff(f957,definition,
( spl8_91
<=> ( 1 = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl8_91])],[avatar_definition]) ).
tff(f960,plain,
( spl8_91
| ~ spl8_10
| ~ spl8_26 ),
inference(avatar_split_clause,[],[f946,f386,f237,f957]) ).
tff(f962,plain,
$false,
inference(avatar_smt_refutation,[],[f960,f912,f876,f495,f394,f373,f358,f349,f310,f299,f269,f263,f262,f257,f252,f246,f240,f229,f224,f219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW633_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 14:22:49 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 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
% 2.37/0.75 % (3408129)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.37/0.75 % (3408176)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2056500945:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.37/0.75 % (3408172)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2438551287:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.37/0.75 % (3408174)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4167697232:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.37/0.75 % (3408175)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2727259550:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.37/0.75 % (3408178)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1113488345:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.37/0.75 % (3408173)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2722242242:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.37/0.75 % (3408176)Instruction limit reached!
% 2.37/0.75 % (3408176)------------------------------
% 2.37/0.75 % (3408176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/0.75 % (3408176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/0.75 % (3408176)CaDiCaL version: 2.1.3
% 2.37/0.75 % (3408176)Termination reason: Instruction limit
% 2.37/0.75 % (3408176)Termination phase: Saturation
% 2.37/0.75 % (3408176)Time elapsed: 0.002 s
% 2.37/0.75 % (3408176)Peak memory usage: 88 MB
% 2.37/0.75 % (3408176)Instructions burned: 4 (million)
% 2.37/0.75 % (3408175)Instruction limit reached!
% 2.37/0.75 % (3408175)------------------------------
% 2.37/0.75 % (3408175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/0.75 % (3408175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/0.75 % (3408175)CaDiCaL version: 2.1.3
% 2.37/0.75 % (3408175)Termination reason: Instruction limit
% 2.37/0.75 % (3408175)Termination phase: Saturation
% 2.37/0.75 % (3408175)Time elapsed: 0.003 s
% 2.37/0.75 % (3408175)Peak memory usage: 88 MB
% 2.37/0.75 % (3408175)Instructions burned: 7 (million)
% 2.37/0.75 % (3408177)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=831480799:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.37/0.75 % (3408172)Instruction limit reached!
% 2.37/0.75 % (3408172)------------------------------
% 2.37/0.75 % (3408172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/0.75 % (3408172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/0.75 % (3408172)CaDiCaL version: 2.1.3
% 2.37/0.75 % (3408172)Termination reason: Instruction limit
% 2.37/0.75 % (3408172)Termination phase: Saturation
% 2.37/0.75 % (3408172)Time elapsed: 0.019 s
% 2.37/0.75 % (3408172)Peak memory usage: 115 MB
% 2.37/0.75 % (3408172)Instructions burned: 13 (million)
% 2.37/0.75 % (3408178)Instruction limit reached!
% 2.37/0.75 % (3408178)------------------------------
% 2.37/0.75 % (3408178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/0.75 % (3408178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/0.75 % (3408178)CaDiCaL version: 2.1.3
% 2.37/0.75 % (3408178)Termination reason: Instruction limit
% 2.37/0.75 % (3408178)Termination phase: Saturation
% 2.37/0.75 % (3408178)Time elapsed: 0.029 s
% 2.37/0.75 % (3408178)Peak memory usage: 115 MB
% 2.37/0.75 % (3408178)Instructions burned: 35 (million)
% 2.37/0.75 % (3408177)Instruction limit reached!
% 2.37/0.75 % (3408177)------------------------------
% 2.37/0.75 % (3408177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/0.75 % (3408177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.37/0.75 % (3408177)CaDiCaL version: 2.1.3
% 2.37/0.75 % (3408177)Termination reason: Instruction limit
% 2.37/0.75 % (3408177)Termination phase: Saturation
% 2.37/0.75 % (3408177)Time elapsed: 0.033 s
% 2.37/0.75 % (3408177)Peak memory usage: 116 MB
% 2.37/0.75 % (3408177)Instructions burned: 46 (million)
% 2.37/0.75 % (3408174)Instruction limit reached!
% 2.37/0.75 % (3408174)------------------------------
% 2.37/0.75 % (3408174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.37/0.75 % (3408174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.86 % (3408174)CaDiCaL version: 2.1.3
% 3.09/0.86 % (3408174)Termination reason: Instruction limit
% 3.09/0.86 % (3408174)Termination phase: Saturation
% 3.09/0.86 % (3408174)Time elapsed: 0.063 s
% 3.09/0.86 % (3408174)Peak memory usage: 115 MB
% 3.09/0.86 % (3408174)Instructions burned: 203 (million)
% 3.09/0.86 % (3408173)Instruction limit reached!
% 3.09/0.86 % (3408173)------------------------------
% 3.09/0.86 % (3408173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/0.86 % (3408173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.86 % (3408173)CaDiCaL version: 2.1.3
% 3.09/0.86 % (3408173)Termination reason: Instruction limit
% 3.09/0.86 % (3408173)Termination phase: Saturation
% 3.09/0.86 % (3408173)Time elapsed: 0.118 s
% 3.09/0.86 % (3408173)Peak memory usage: 118 MB
% 3.09/0.86 % (3408173)Instructions burned: 312 (million)
% 3.09/0.86 % (3408185)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2783097561:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.09/0.86 % (3408186)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=1532850688:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.09/0.86 % (3408185)Instruction limit reached!
% 3.09/0.86 % (3408185)------------------------------
% 3.09/0.86 % (3408185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/0.86 % (3408185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.86 % (3408185)CaDiCaL version: 2.1.3
% 3.09/0.86 % (3408185)Termination reason: Instruction limit
% 3.09/0.86 % (3408185)Termination phase: Saturation
% 3.09/0.86 % (3408185)Time elapsed: 0.007 s
% 3.09/0.86 % (3408185)Peak memory usage: 88 MB
% 3.09/0.86 % (3408185)Instructions burned: 16 (million)
% 3.09/0.86 % (3408188)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3126979672:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.09/0.86 % (3408186)Instruction limit reached!
% 3.09/0.86 % (3408186)------------------------------
% 3.09/0.86 % (3408186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/0.86 % (3408186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.86 % (3408186)CaDiCaL version: 2.1.3
% 3.09/0.86 % (3408186)Termination reason: Instruction limit
% 3.09/0.86 % (3408186)Termination phase: Saturation
% 3.09/0.86 % (3408186)Time elapsed: 0.012 s
% 3.09/0.86 % (3408186)Peak memory usage: 88 MB
% 3.09/0.86 % (3408186)Instructions burned: 29 (million)
% 3.09/0.86 % (3408188)Instruction limit reached!
% 3.09/0.86 % (3408188)------------------------------
% 3.09/0.86 % (3408188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/0.86 % (3408188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.86 % (3408188)CaDiCaL version: 2.1.3
% 3.09/0.86 % (3408188)Termination reason: Instruction limit
% 3.09/0.86 % (3408188)Termination phase: Saturation
% 3.09/0.86 % (3408188)Time elapsed: 0.006 s
% 3.09/0.86 % (3408188)Peak memory usage: 90 MB
% 3.09/0.86 % (3408188)Instructions burned: 18 (million)
% 3.09/0.86 % (3408189)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=414023978:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 3.09/0.86 % (3408189)Instruction limit reached!
% 3.09/0.86 % (3408189)------------------------------
% 3.09/0.86 % (3408189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/0.86 % (3408189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/0.86 % (3408189)CaDiCaL version: 2.1.3
% 3.09/0.86 % (3408189)Termination reason: Instruction limit
% 3.09/0.86 % (3408189)Termination phase: Saturation
% 3.09/0.86 % (3408189)Time elapsed: 0.012 s
% 3.09/0.86 % (3408189)Peak memory usage: 89 MB
% 3.09/0.86 % (3408189)Instructions burned: 26 (million)
% 3.09/0.86 % (3408190)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=2067089448:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi)
% 3.09/0.86 % (3408190)Instruction limit reached!
% 3.09/0.86 % (3408190)------------------------------
% 3.09/0.86 % (3408190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/0.86 % (3408190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.00 % (3408190)CaDiCaL version: 2.1.3
% 3.74/1.00 % (3408190)Termination reason: Instruction limit
% 3.74/1.00 % (3408190)Termination phase: Saturation
% 3.74/1.00 % (3408190)Time elapsed: 0.011 s
% 3.74/1.00 % (3408190)Peak memory usage: 90 MB
% 3.74/1.00 % (3408190)Instructions burned: 29 (million)
% 3.74/1.00 % (3408191)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2327409345:i=85:gtgl=4:rtra=on:gtg=exists_sym_2998 on theBenchmark for (2998ds/85Mi)
% 3.74/1.00 % (3408191)Instruction limit reached!
% 3.74/1.00 % (3408191)------------------------------
% 3.74/1.00 % (3408191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.00 % (3408191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.00 % (3408191)CaDiCaL version: 2.1.3
% 3.74/1.00 % (3408191)Termination reason: Instruction limit
% 3.74/1.00 % (3408191)Termination phase: Saturation
% 3.74/1.00 % (3408191)Time elapsed: 0.028 s
% 3.74/1.00 % (3408191)Peak memory usage: 89 MB
% 3.74/1.00 % (3408191)Instructions burned: 86 (million)
% 3.74/1.00 % (3408194)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1937657199:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 3.74/1.00 % (3408194)Instruction limit reached!
% 3.74/1.00 % (3408194)------------------------------
% 3.74/1.00 % (3408194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.00 % (3408194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.00 % (3408194)CaDiCaL version: 2.1.3
% 3.74/1.00 % (3408194)Termination reason: Instruction limit
% 3.74/1.00 % (3408194)Termination phase: Saturation
% 3.74/1.00 % (3408194)Time elapsed: 0.002 s
% 3.74/1.00 % (3408194)Peak memory usage: 88 MB
% 3.74/1.00 % (3408194)Instructions burned: 4 (million)
% 3.74/1.00 % (3408196)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2591191929:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 3.74/1.00 % (3408197)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1423418743:i=4:ep=RST:ins=2:rtra=on_2997 on theBenchmark for (2997ds/4Mi)
% 3.74/1.00 % (3408197)Instruction limit reached!
% 3.74/1.00 % (3408197)------------------------------
% 3.74/1.00 % (3408197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.00 % (3408197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.00 % (3408197)CaDiCaL version: 2.1.3
% 3.74/1.00 % (3408197)Termination reason: Instruction limit
% 3.74/1.00 % (3408197)Termination phase: Saturation
% 3.74/1.00 % (3408197)Time elapsed: 0.002 s
% 3.74/1.00 % (3408197)Peak memory usage: 88 MB
% 3.74/1.00 % (3408197)Instructions burned: 5 (million)
% 3.74/1.00 % (3408198)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4145254025:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2997 on theBenchmark for (2997ds/66Mi)
% 3.74/1.00 % (3408201)lrs+10_1_thi=all:si=on:fd=off:random_seed=3950125241:i=53:rtra=on:gtg=all_2997 on theBenchmark for (2997ds/53Mi)
% 3.74/1.00 % (3408202)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=3795651514:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 3.74/1.00 % (3408202)Instruction limit reached!
% 3.74/1.00 % (3408202)------------------------------
% 3.74/1.00 % (3408202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.00 % (3408202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.00 % (3408202)CaDiCaL version: 2.1.3
% 3.74/1.00 % (3408202)Termination reason: Instruction limit
% 3.74/1.00 % (3408202)Termination phase: Saturation
% 3.74/1.00 % (3408202)Time elapsed: 0.003 s
% 3.74/1.00 % (3408202)Peak memory usage: 88 MB
% 3.74/1.00 % (3408202)Instructions burned: 8 (million)
% 3.74/1.00 % (3408201)Instruction limit reached!
% 3.74/1.00 % (3408201)------------------------------
% 3.74/1.00 % (3408201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.74/1.00 % (3408201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.00 % (3408201)CaDiCaL version: 2.1.3
% 3.74/1.00 % (3408201)Termination reason: Instruction limit
% 3.74/1.00 % (3408201)Termination phase: Saturation
% 3.74/1.00 % (3408201)Time elapsed: 0.037 s
% 3.74/1.00 % (3408201)Peak memory usage: 116 MB
% 3.74/1.00 % (3408201)Instructions burned: 54 (million)
% 3.74/1.00 % (3408196)Instruction limit reached!
% 5.22/1.18 % (3408196)------------------------------
% 5.22/1.18 % (3408196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/1.18 % (3408196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.18 % (3408196)CaDiCaL version: 2.1.3
% 5.22/1.18 % (3408196)Termination reason: Instruction limit
% 5.22/1.18 % (3408196)Termination phase: Saturation
% 5.22/1.18 % (3408196)Time elapsed: 0.066 s
% 5.22/1.18 % (3408196)Peak memory usage: 90 MB
% 5.22/1.18 % (3408196)Instructions burned: 184 (million)
% 5.22/1.18 % (3408198)Instruction limit reached!
% 5.22/1.18 % (3408198)------------------------------
% 5.22/1.18 % (3408198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/1.18 % (3408198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.18 % (3408198)CaDiCaL version: 2.1.3
% 5.22/1.18 % (3408198)Termination reason: Instruction limit
% 5.22/1.18 % (3408198)Termination phase: Saturation
% 5.22/1.18 % (3408198)Time elapsed: 0.055 s
% 5.22/1.18 % (3408198)Peak memory usage: 133 MB
% 5.22/1.18 % (3408198)Instructions burned: 68 (million)
% 5.22/1.18 % (3408204)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2942883113:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 5.22/1.18 % (3408204)Instruction limit reached!
% 5.22/1.18 % (3408204)------------------------------
% 5.22/1.18 % (3408204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/1.18 % (3408204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.18 % (3408204)CaDiCaL version: 2.1.3
% 5.22/1.18 % (3408204)Termination reason: Instruction limit
% 5.22/1.18 % (3408204)Termination phase: Saturation
% 5.22/1.18 % (3408204)Time elapsed: 0.002 s
% 5.22/1.18 % (3408204)Peak memory usage: 88 MB
% 5.22/1.18 % (3408204)Instructions burned: 4 (million)
% 5.22/1.18 % (3408209)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2629646350:i=127:doe=on:rtra=on_2996 on theBenchmark for (2996ds/127Mi)
% 5.22/1.18 % (3408208)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1172727828:i=2:doe=on:canc=force:asg=cautious:rtra=on_2996 on theBenchmark for (2996ds/2Mi)
% 5.22/1.18 % (3408208)Instruction limit reached!
% 5.22/1.18 % (3408208)------------------------------
% 5.22/1.18 % (3408208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/1.18 % (3408208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.18 % (3408208)CaDiCaL version: 2.1.3
% 5.22/1.18 % (3408208)Termination reason: Instruction limit
% 5.22/1.18 % (3408208)Termination phase: Equality resolution with deletion
% 5.22/1.18 % (3408208)Time elapsed: 0.001 s
% 5.22/1.18 % (3408208)Peak memory usage: 86 MB
% 5.22/1.18 % (3408208)Instructions burned: 2 (million)
% 5.22/1.18 % (3408215)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=747401683: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_2995 on theBenchmark for (2995ds/35Mi)
% 5.22/1.18 % (3408214)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2627207628:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi)
% 5.22/1.18 % (3408213)dis+10_1_si=on:random_seed=3302600974:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 5.22/1.18 % (3408209)Instruction limit reached!
% 5.22/1.18 % (3408209)------------------------------
% 5.22/1.18 % (3408209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/1.18 % (3408209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.18 % (3408209)CaDiCaL version: 2.1.3
% 5.22/1.18 % (3408209)Termination reason: Instruction limit
% 5.22/1.18 % (3408209)Termination phase: Saturation
% 5.22/1.18 % (3408209)Time elapsed: 0.067 s
% 5.22/1.18 % (3408209)Peak memory usage: 119 MB
% 5.22/1.18 % (3408209)Instructions burned: 128 (million)
% 5.22/1.18 % (3408214)Refutation not found, incomplete strategy
% 5.22/1.18 % (3408214)------------------------------
% 5.22/1.18 % (3408214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.22/1.18 % (3408214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.18 % (3408214)CaDiCaL version: 2.1.3
% 5.22/1.18 % (3408214)Termination reason: Refutation not found, incomplete strategy
% 5.22/1.18 % (3408214)Time elapsed: 0.002 s
% 5.22/1.18 % (3408214)Peak memory usage: 88 MB
% 5.22/1.18 % (3408214)Instructions burned: 5 (million)
% 6.23/1.36 % (3408213)Instruction limit reached!
% 6.23/1.36 % (3408213)------------------------------
% 6.23/1.36 % (3408213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.23/1.36 % (3408213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.36 % (3408213)CaDiCaL version: 2.1.3
% 6.23/1.36 % (3408213)Termination reason: Instruction limit
% 6.23/1.36 % (3408213)Termination phase: Saturation
% 6.23/1.36 % (3408213)Time elapsed: 0.004 s
% 6.23/1.36 % (3408213)Peak memory usage: 88 MB
% 6.23/1.36 % (3408213)Instructions burned: 11 (million)
% 6.23/1.36 % (3408215)Instruction limit reached!
% 6.23/1.36 % (3408215)------------------------------
% 6.23/1.36 % (3408215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.23/1.36 % (3408215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.36 % (3408215)CaDiCaL version: 2.1.3
% 6.23/1.36 % (3408215)Termination reason: Instruction limit
% 6.23/1.36 % (3408215)Termination phase: Saturation
% 6.23/1.36 % (3408215)Time elapsed: 0.016 s
% 6.23/1.36 % (3408215)Peak memory usage: 88 MB
% 6.23/1.36 % (3408215)Instructions burned: 36 (million)
% 6.23/1.36 % (3408216)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1784313311:i=2:fsr=off:rtra=on:inst=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.23/1.36 % (3408216)Instruction limit reached!
% 6.23/1.36 % (3408216)------------------------------
% 6.23/1.36 % (3408216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.23/1.36 % (3408216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.36 % (3408216)CaDiCaL version: 2.1.3
% 6.23/1.36 % (3408216)Termination reason: Instruction limit
% 6.23/1.36 % (3408216)Termination phase: Equality resolution with deletion
% 6.23/1.36 % (3408216)Time elapsed: 0.001 s
% 6.23/1.36 % (3408216)Peak memory usage: 86 MB
% 6.23/1.36 % (3408216)Instructions burned: 2 (million)
% 6.23/1.36 % (3408218)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2315410941:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2995 on theBenchmark for (2995ds/8Mi)
% 6.23/1.36 % (3408221)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3482513535:i=370:ep=RS:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/370Mi)
% 6.23/1.36 % (3408218)Instruction limit reached!
% 6.23/1.36 % (3408218)------------------------------
% 6.23/1.36 % (3408218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.23/1.36 % (3408218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.36 % (3408218)CaDiCaL version: 2.1.3
% 6.23/1.36 % (3408218)Termination reason: Instruction limit
% 6.23/1.36 % (3408218)Termination phase: Saturation
% 6.23/1.36 % (3408218)Time elapsed: 0.012 s
% 6.23/1.36 % (3408218)Peak memory usage: 88 MB
% 6.23/1.36 % (3408218)Instructions burned: 9 (million)
% 6.23/1.36 % (3408226)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=391554940:i=226:rtra=on:gtg=position:ss=axioms_2994 on theBenchmark for (2994ds/226Mi)
% 6.23/1.36 % (3408225)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2985246639:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi)
% 6.23/1.36 % (3408228)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2688345297:i=10:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.23/1.36 % (3408228)Instruction limit reached!
% 6.23/1.36 % (3408228)------------------------------
% 6.23/1.36 % (3408228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.23/1.36 % (3408228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.36 % (3408228)CaDiCaL version: 2.1.3
% 6.23/1.36 % (3408228)Termination reason: Instruction limit
% 6.23/1.36 % (3408228)Termination phase: Saturation
% 6.23/1.36 % (3408228)Time elapsed: 0.005 s
% 6.23/1.36 % (3408228)Peak memory usage: 88 MB
% 6.23/1.36 % (3408228)Instructions burned: 12 (million)
% 6.23/1.36 % (3408229)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=399040629:i=71:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/71Mi)
% 6.23/1.36 % (3408225)Instruction limit reached!
% 6.23/1.36 % (3408225)------------------------------
% 6.23/1.36 % (3408225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.23/1.36 % (3408225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.33/1.53 % (3408225)CaDiCaL version: 2.1.3
% 7.33/1.53 % (3408225)Termination reason: Instruction limit
% 7.33/1.53 % (3408225)Termination phase: Saturation
% 7.33/1.53 % (3408225)Time elapsed: 0.022 s
% 7.33/1.53 % (3408225)Peak memory usage: 116 MB
% 7.33/1.53 % (3408225)Instructions burned: 21 (million)
% 7.33/1.53 % (3408221)Instruction limit reached!
% 7.33/1.53 % (3408221)------------------------------
% 7.33/1.53 % (3408221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.33/1.53 % (3408221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.33/1.53 % (3408221)CaDiCaL version: 2.1.3
% 7.33/1.53 % (3408221)Termination reason: Instruction limit
% 7.33/1.53 % (3408221)Termination phase: Saturation
% 7.33/1.53 % (3408221)Time elapsed: 0.098 s
% 7.33/1.53 % (3408221)Peak memory usage: 92 MB
% 7.33/1.53 % (3408221)Instructions burned: 374 (million)
% 7.33/1.53 % (3408214)------------------------------
% 7.33/1.53 % (3408214)------------------------------
% 7.33/1.53 % (3408232)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=1940085482:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2994 on theBenchmark for (2994ds/75Mi)
% 7.33/1.53 % (3408229)Instruction limit reached!
% 7.33/1.53 % (3408229)------------------------------
% 7.33/1.53 % (3408229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.33/1.53 % (3408229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.33/1.53 % (3408229)CaDiCaL version: 2.1.3
% 7.33/1.53 % (3408229)Termination reason: Instruction limit
% 7.33/1.53 % (3408229)Termination phase: Saturation
% 7.33/1.53 % (3408229)Time elapsed: 0.055 s
% 7.33/1.53 % (3408229)Peak memory usage: 133 MB
% 7.33/1.53 % (3408229)Instructions burned: 72 (million)
% 7.33/1.53 % (3408232)Instruction limit reached!
% 7.33/1.53 % (3408232)------------------------------
% 7.33/1.53 % (3408232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.33/1.53 % (3408232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.33/1.53 % (3408232)CaDiCaL version: 2.1.3
% 7.33/1.53 % (3408232)Termination reason: Instruction limit
% 7.33/1.53 % (3408232)Termination phase: Saturation
% 7.33/1.53 % (3408232)Time elapsed: 0.028 s
% 7.33/1.53 % (3408232)Peak memory usage: 90 MB
% 7.33/1.53 % (3408232)Instructions burned: 77 (million)
% 7.33/1.53 % (3408226)Instruction limit reached!
% 7.33/1.53 % (3408226)------------------------------
% 7.33/1.53 % (3408226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.33/1.53 % (3408226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.33/1.53 % (3408226)CaDiCaL version: 2.1.3
% 7.33/1.53 % (3408226)Termination reason: Instruction limit
% 7.33/1.53 % (3408226)Termination phase: Saturation
% 7.33/1.53 % (3408226)Time elapsed: 0.083 s
% 7.33/1.53 % (3408226)Peak memory usage: 117 MB
% 7.33/1.53 % (3408226)Instructions burned: 227 (million)
% 7.33/1.53 % (3408236)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=2957730924:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2993 on theBenchmark for (2993ds/294Mi)
% 7.33/1.53 % (3408238)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2840452397:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2993 on theBenchmark for (2993ds/130Mi)
% 7.33/1.53 % (3408239)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1819618595:i=131:rtra=on_2993 on theBenchmark for (2993ds/131Mi)
% 7.33/1.53 % (3408241)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1946951270:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/40Mi)
% 7.33/1.53 % (3408243)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4250159286:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/598Mi)
% 7.33/1.53 % (3408242)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3078884426:i=307:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/307Mi)
% 7.33/1.53 % (3408244)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2842233481:i=131:canc=cautious:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/131Mi)
% 7.33/1.53 % (3408238)Instruction limit reached!
% 7.33/1.53 % (3408238)------------------------------
% 7.33/1.53 % (3408238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/1.74 % (3408238)CaDiCaL version: 2.1.3
% 8.78/1.74 % (3408238)Termination reason: Instruction limit
% 8.78/1.74 % (3408238)Termination phase: Saturation
% 8.78/1.74 % (3408238)Time elapsed: 0.067 s
% 8.78/1.74 % (3408238)Peak memory usage: 118 MB
% 8.78/1.74 % (3408238)Instructions burned: 130 (million)
% 8.78/1.74 % (3408239)Instruction limit reached!
% 8.78/1.74 % (3408239)------------------------------
% 8.78/1.74 % (3408239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/1.74 % (3408239)CaDiCaL version: 2.1.3
% 8.78/1.74 % (3408239)Termination reason: Instruction limit
% 8.78/1.74 % (3408239)Termination phase: Saturation
% 8.78/1.74 % (3408239)Time elapsed: 0.076 s
% 8.78/1.74 % (3408239)Peak memory usage: 135 MB
% 8.78/1.74 % (3408239)Instructions burned: 131 (million)
% 8.78/1.74 % (3408241)Instruction limit reached!
% 8.78/1.74 % (3408241)------------------------------
% 8.78/1.74 % (3408241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/1.74 % (3408241)CaDiCaL version: 2.1.3
% 8.78/1.74 % (3408241)Termination reason: Instruction limit
% 8.78/1.74 % (3408241)Termination phase: Saturation
% 8.78/1.74 % (3408241)Time elapsed: 0.043 s
% 8.78/1.74 % (3408241)Peak memory usage: 134 MB
% 8.78/1.74 % (3408241)Instructions burned: 41 (million)
% 8.78/1.74 % (3408236)Instruction limit reached!
% 8.78/1.74 % (3408236)------------------------------
% 8.78/1.74 % (3408236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/1.74 % (3408236)CaDiCaL version: 2.1.3
% 8.78/1.74 % (3408236)Termination reason: Instruction limit
% 8.78/1.74 % (3408236)Termination phase: Saturation
% 8.78/1.74 % (3408236)Time elapsed: 0.109 s
% 8.78/1.74 % (3408236)Peak memory usage: 91 MB
% 8.78/1.74 % (3408236)Instructions burned: 294 (million)
% 8.78/1.74 % (3408244)Instruction limit reached!
% 8.78/1.74 % (3408244)------------------------------
% 8.78/1.74 % (3408244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/1.74 % (3408244)CaDiCaL version: 2.1.3
% 8.78/1.74 % (3408244)Termination reason: Instruction limit
% 8.78/1.74 % (3408244)Termination phase: Saturation
% 8.78/1.74 % (3408244)Time elapsed: 0.064 s
% 8.78/1.74 % (3408244)Peak memory usage: 117 MB
% 8.78/1.74 % (3408244)Instructions burned: 133 (million)
% 8.78/1.74 % (3408242)Instruction limit reached!
% 8.78/1.74 % (3408242)------------------------------
% 8.78/1.74 % (3408242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/1.74 % (3408242)CaDiCaL version: 2.1.3
% 8.78/1.74 % (3408242)Termination reason: Instruction limit
% 8.78/1.74 % (3408242)Termination phase: Saturation
% 8.78/1.74 % (3408242)Time elapsed: 0.091 s
% 8.78/1.74 % (3408242)Peak memory usage: 92 MB
% 8.78/1.74 % (3408242)Instructions burned: 308 (million)
% 8.78/1.74 % (3408252)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2072195087:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2991 on theBenchmark for (2991ds/259Mi)
% 8.78/1.74 % (3408254)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=705733964:i=383:fsr=off:rtra=on:ev=force_2991 on theBenchmark for (2991ds/383Mi)
% 8.78/1.74 % (3408253)dis+10_1_si=on:random_seed=2790787993:s2a=on:i=1000:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/1000Mi)
% 8.78/1.74 % (3408255)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3154554445:i=141:doe=on:rtra=on_2991 on theBenchmark for (2991ds/141Mi)
% 8.78/1.74 % (3408256)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3831211813:i=65:nm=16:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 8.78/1.74 % (3408252)Instruction limit reached!
% 8.78/1.74 % (3408252)------------------------------
% 8.78/1.74 % (3408252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/1.74 % (3408252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408252)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408252)Termination reason: Instruction limit
% 10.46/1.94 % (3408252)Termination phase: Saturation
% 10.46/1.94 % (3408252)Time elapsed: 0.080 s
% 10.46/1.94 % (3408252)Peak memory usage: 118 MB
% 10.46/1.94 % (3408252)Instructions burned: 261 (million)
% 10.46/1.94 % (3408257)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4073183550:i=121:nm=16:rtra=on_2990 on theBenchmark for (2990ds/121Mi)
% 10.46/1.94 % (3408255)Instruction limit reached!
% 10.46/1.94 % (3408255)------------------------------
% 10.46/1.94 % (3408255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/1.94 % (3408255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408255)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408255)Termination reason: Instruction limit
% 10.46/1.94 % (3408255)Termination phase: Saturation
% 10.46/1.94 % (3408255)Time elapsed: 0.051 s
% 10.46/1.94 % (3408255)Peak memory usage: 90 MB
% 10.46/1.94 % (3408255)Instructions burned: 141 (million)
% 10.46/1.94 % (3408256)Refutation not found, incomplete strategy
% 10.46/1.94 % (3408256)------------------------------
% 10.46/1.94 % (3408256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/1.94 % (3408256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408256)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408256)Termination reason: Refutation not found, incomplete strategy
% 10.46/1.94 % (3408256)Time elapsed: 0.021 s
% 10.46/1.94 % (3408256)Peak memory usage: 117 MB
% 10.46/1.94 % (3408256)Instructions burned: 14 (million)
% 10.46/1.94 % (3408254)Instruction limit reached!
% 10.46/1.94 % (3408254)------------------------------
% 10.46/1.94 % (3408254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/1.94 % (3408254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408254)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408254)Termination reason: Instruction limit
% 10.46/1.94 % (3408254)Termination phase: Saturation
% 10.46/1.94 % (3408254)Time elapsed: 0.114 s
% 10.46/1.94 % (3408254)Peak memory usage: 93 MB
% 10.46/1.94 % (3408254)Instructions burned: 384 (million)
% 10.46/1.94 % (3408257)Instruction limit reached!
% 10.46/1.94 % (3408257)------------------------------
% 10.46/1.94 % (3408257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/1.94 % (3408257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408257)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408257)Termination reason: Instruction limit
% 10.46/1.94 % (3408257)Termination phase: Saturation
% 10.46/1.94 % (3408257)Time elapsed: 0.041 s
% 10.46/1.94 % (3408257)Peak memory usage: 89 MB
% 10.46/1.94 % (3408257)Instructions burned: 121 (million)
% 10.46/1.94 % (3408243)Instruction limit reached!
% 10.46/1.94 % (3408243)------------------------------
% 10.46/1.94 % (3408243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/1.94 % (3408243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408243)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408243)Termination reason: Instruction limit
% 10.46/1.94 % (3408243)Termination phase: Saturation
% 10.46/1.94 % (3408243)Time elapsed: 0.252 s
% 10.46/1.94 % (3408243)Peak memory usage: 141 MB
% 10.46/1.94 % (3408243)Instructions burned: 599 (million)
% 10.46/1.94 % (3408263)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=433068480:s2a=on:i=128:s2at=5:ins=3:rtra=on_2989 on theBenchmark for (2989ds/128Mi)
% 10.46/1.94 % (3408265)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2108391585:i=39:ins=3:rtra=on_2989 on theBenchmark for (2989ds/39Mi)
% 10.46/1.94 % (3408266)dis+1010_1_to=kbo:si=on:random_seed=4256273861:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2989 on theBenchmark for (2989ds/175Mi)
% 10.46/1.94 % (3408267)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2289637558:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/329Mi)
% 10.46/1.94 % (3408265)Instruction limit reached!
% 10.46/1.94 % (3408265)------------------------------
% 10.46/1.94 % (3408265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/1.94 % (3408265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/1.94 % (3408265)CaDiCaL version: 2.1.3
% 10.46/1.94 % (3408265)Termination reason: Instruction limit
% 12.34/2.15 % (3408265)Termination phase: Saturation
% 12.34/2.15 % (3408265)Time elapsed: 0.030 s
% 12.34/2.15 % (3408265)Peak memory usage: 116 MB
% 12.34/2.15 % (3408265)Instructions burned: 39 (million)
% 12.34/2.15 % (3408268)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2594658564:s2a=on:i=483:doe=on:nm=32:rtra=on_2989 on theBenchmark for (2989ds/483Mi)
% 12.34/2.15 % (3408256)------------------------------
% 12.34/2.15 % (3408256)------------------------------
% 12.34/2.15 % (3408263)Instruction limit reached!
% 12.34/2.15 % (3408263)------------------------------
% 12.34/2.15 % (3408263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.34/2.15 % (3408263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.34/2.15 % (3408263)CaDiCaL version: 2.1.3
% 12.34/2.15 % (3408263)Termination reason: Instruction limit
% 12.34/2.15 % (3408263)Termination phase: Saturation
% 12.34/2.15 % (3408263)Time elapsed: 0.063 s
% 12.34/2.15 % (3408263)Peak memory usage: 118 MB
% 12.34/2.15 % (3408263)Instructions burned: 130 (million)
% 12.34/2.15 % (3408266)Instruction limit reached!
% 12.34/2.15 % (3408266)------------------------------
% 12.34/2.15 % (3408266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.34/2.15 % (3408266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.34/2.15 % (3408266)CaDiCaL version: 2.1.3
% 12.34/2.15 % (3408266)Termination reason: Instruction limit
% 12.34/2.15 % (3408266)Termination phase: Saturation
% 12.34/2.15 % (3408266)Time elapsed: 0.065 s
% 12.34/2.15 % (3408266)Peak memory usage: 91 MB
% 12.34/2.15 % (3408266)Instructions burned: 175 (million)
% 12.34/2.15 % (3408267)Instruction limit reached!
% 12.34/2.15 % (3408267)------------------------------
% 12.34/2.15 % (3408267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.34/2.15 % (3408267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.34/2.15 % (3408267)CaDiCaL version: 2.1.3
% 12.34/2.15 % (3408267)Termination reason: Instruction limit
% 12.34/2.15 % (3408267)Termination phase: Saturation
% 12.34/2.15 % (3408267)Time elapsed: 0.091 s
% 12.34/2.15 % (3408267)Peak memory usage: 116 MB
% 12.34/2.15 % (3408267)Instructions burned: 334 (million)
% 12.34/2.15 % (3408253)Instruction limit reached!
% 12.34/2.15 % (3408253)------------------------------
% 12.34/2.15 % (3408253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.34/2.15 % (3408253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.34/2.15 % (3408253)CaDiCaL version: 2.1.3
% 12.34/2.15 % (3408253)Termination reason: Instruction limit
% 12.34/2.15 % (3408253)Termination phase: Saturation
% 12.34/2.15 % (3408253)Time elapsed: 0.323 s
% 12.34/2.15 % (3408253)Peak memory usage: 94 MB
% 12.34/2.15 % (3408253)Instructions burned: 1000 (million)
% 12.34/2.15 % (3408274)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1914971282:thitd=on:i=215:nm=0:rtra=on:ev=force_2987 on theBenchmark for (2987ds/215Mi)
% 12.34/2.15 % (3408276)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3941119626:st=2:i=295:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/295Mi)
% 12.34/2.15 % (3408275)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1602193767:i=349:rtra=on_2987 on theBenchmark for (2987ds/349Mi)
% 12.34/2.15 % (3408277)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1907687691:i=328:kws=inv_frequency:nm=20:rtra=on_2987 on theBenchmark for (2987ds/328Mi)
% 12.34/2.15 % (3408268)Instruction limit reached!
% 12.34/2.15 % (3408268)------------------------------
% 12.34/2.15 % (3408268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.34/2.15 % (3408268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.34/2.15 % (3408268)CaDiCaL version: 2.1.3
% 12.34/2.15 % (3408268)Termination reason: Instruction limit
% 12.34/2.15 % (3408268)Termination phase: Saturation
% 12.34/2.15 % (3408268)Time elapsed: 0.194 s
% 12.34/2.15 % (3408268)Peak memory usage: 137 MB
% 12.34/2.15 % (3408268)Instructions burned: 485 (million)
% 12.34/2.15 % (3408276)Instruction limit reached!
% 12.34/2.15 % (3408276)------------------------------
% 12.34/2.15 % (3408276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.34/2.15 % (3408276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.34/2.15 % (3408276)CaDiCaL version: 2.1.3
% 12.34/2.15 % (3408276)Termination reason: Instruction limit
% 13.29/2.33 % (3408276)Termination phase: Saturation
% 13.29/2.33 % (3408276)Time elapsed: 0.088 s
% 13.29/2.33 % (3408276)Peak memory usage: 90 MB
% 13.29/2.33 % (3408276)Instructions burned: 295 (million)
% 13.29/2.33 % (3408274)Instruction limit reached!
% 13.29/2.33 % (3408274)------------------------------
% 13.29/2.33 % (3408274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.29/2.33 % (3408274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.29/2.33 % (3408274)CaDiCaL version: 2.1.3
% 13.29/2.33 % (3408274)Termination reason: Instruction limit
% 13.29/2.33 % (3408274)Termination phase: Saturation
% 13.29/2.33 % (3408274)Time elapsed: 0.106 s
% 13.29/2.33 % (3408274)Peak memory usage: 137 MB
% 13.29/2.33 % (3408274)Instructions burned: 217 (million)
% 13.29/2.33 % (3408275)Instruction limit reached!
% 13.29/2.33 % (3408275)------------------------------
% 13.29/2.33 % (3408275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.29/2.33 % (3408275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.29/2.33 % (3408275)CaDiCaL version: 2.1.3
% 13.29/2.33 % (3408275)Termination reason: Instruction limit
% 13.29/2.33 % (3408275)Termination phase: Saturation
% 13.29/2.33 % (3408275)Time elapsed: 0.092 s
% 13.29/2.33 % (3408275)Peak memory usage: 115 MB
% 13.29/2.33 % (3408275)Instructions burned: 354 (million)
% 13.29/2.33 % (3408279)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=4008726276:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/484Mi)
% 13.29/2.33 % (3408278)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=255428560:i=281:gtgl=2:rtra=on:gtg=all_2987 on theBenchmark for (2987ds/281Mi)
% 13.29/2.33 % (3408277)Instruction limit reached!
% 13.29/2.33 % (3408277)------------------------------
% 13.29/2.33 % (3408277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.29/2.33 % (3408277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.29/2.33 % (3408277)CaDiCaL version: 2.1.3
% 13.29/2.33 % (3408277)Termination reason: Instruction limit
% 13.29/2.33 % (3408277)Termination phase: Saturation
% 13.29/2.33 % (3408277)Time elapsed: 0.127 s
% 13.29/2.33 % (3408277)Peak memory usage: 119 MB
% 13.29/2.33 % (3408277)Instructions burned: 328 (million)
% 13.29/2.33 % (3408284)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=585520554:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2985 on theBenchmark for (2985ds/321Mi)
% 13.29/2.33 % (3408287)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4128185043:i=416:rtra=on:gtg=position:ss=axioms_2985 on theBenchmark for (2985ds/416Mi)
% 13.29/2.33 % (3408288)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=628709483:i=471:thf=on:kws=precedence:rtra=on_2985 on theBenchmark for (2985ds/471Mi)
% 13.29/2.33 % (3408289)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1641811101:avsq=on:i=276:avsqr=1,2:rtra=on_2985 on theBenchmark for (2985ds/276Mi)
% 13.29/2.33 % (3408278)Instruction limit reached!
% 13.29/2.33 % (3408278)------------------------------
% 13.29/2.33 % (3408278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.29/2.33 % (3408278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.29/2.33 % (3408278)CaDiCaL version: 2.1.3
% 13.29/2.33 % (3408278)Termination reason: Instruction limit
% 13.29/2.33 % (3408278)Termination phase: Saturation
% 13.29/2.33 % (3408278)Time elapsed: 0.120 s
% 13.29/2.33 % (3408278)Peak memory usage: 118 MB
% 13.29/2.33 % (3408278)Instructions burned: 282 (million)
% 13.29/2.33 % (3408279)Instruction limit reached!
% 13.29/2.33 % (3408279)------------------------------
% 13.29/2.33 % (3408279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.29/2.33 % (3408279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.29/2.33 % (3408279)CaDiCaL version: 2.1.3
% 13.29/2.33 % (3408279)Termination reason: Instruction limit
% 13.29/2.33 % (3408279)Termination phase: Saturation
% 13.29/2.33 % (3408279)Time elapsed: 0.122 s
% 13.29/2.33 % (3408279)Peak memory usage: 91 MB
% 13.29/2.33 % (3408279)Instructions burned: 488 (million)
% 13.29/2.33 % (3408290)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2362717869:i=375:kws=inv_arity_squared:rtra=on_2985 on theBenchmark for (2985ds/375Mi)
% 13.29/2.33 % (3408284)Instruction limit reached!
% 14.18/2.60 % (3408284)------------------------------
% 14.18/2.60 % (3408284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.60 % (3408284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.60 % (3408284)CaDiCaL version: 2.1.3
% 14.18/2.60 % (3408284)Termination reason: Instruction limit
% 14.18/2.60 % (3408284)Termination phase: Saturation
% 14.18/2.60 % (3408284)Time elapsed: 0.085 s
% 14.18/2.60 % (3408284)Peak memory usage: 112 MB
% 14.18/2.60 % (3408284)Instructions burned: 325 (million)
% 14.18/2.60 % (3408296)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2927276286:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2984 on theBenchmark for (2984ds/513Mi)
% 14.18/2.60 % (3408295)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=892804964:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/387Mi)
% 14.18/2.60 % (3408287)Instruction limit reached!
% 14.18/2.60 % (3408287)------------------------------
% 14.18/2.60 % (3408287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.60 % (3408287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.60 % (3408287)CaDiCaL version: 2.1.3
% 14.18/2.60 % (3408287)Termination reason: Instruction limit
% 14.18/2.60 % (3408287)Termination phase: Saturation
% 14.18/2.60 % (3408287)Time elapsed: 0.132 s
% 14.18/2.60 % (3408287)Peak memory usage: 119 MB
% 14.18/2.60 % (3408287)Instructions burned: 417 (million)
% 14.18/2.60 % (3408289)Instruction limit reached!
% 14.18/2.60 % (3408289)------------------------------
% 14.18/2.60 % (3408289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.60 % (3408289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.60 % (3408289)CaDiCaL version: 2.1.3
% 14.18/2.60 % (3408289)Termination reason: Instruction limit
% 14.18/2.60 % (3408289)Termination phase: Saturation
% 14.18/2.60 % (3408289)Time elapsed: 0.141 s
% 14.18/2.60 % (3408289)Peak memory usage: 135 MB
% 14.18/2.60 % (3408289)Instructions burned: 276 (million)
% 14.18/2.60 % (3408288)Instruction limit reached!
% 14.18/2.60 % (3408288)------------------------------
% 14.18/2.60 % (3408288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.60 % (3408288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.60 % (3408288)CaDiCaL version: 2.1.3
% 14.18/2.60 % (3408288)Termination reason: Instruction limit
% 14.18/2.60 % (3408288)Termination phase: Saturation
% 14.18/2.60 % (3408288)Time elapsed: 0.146 s
% 14.18/2.60 % (3408288)Peak memory usage: 119 MB
% 14.18/2.60 % (3408288)Instructions burned: 479 (million)
% 14.18/2.60 % (3408298)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1659683714:i=334:rtra=on_2983 on theBenchmark for (2983ds/334Mi)
% 14.18/2.60 % (3408290)Instruction limit reached!
% 14.18/2.60 % (3408290)------------------------------
% 14.18/2.60 % (3408290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.60 % (3408290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.60 % (3408290)CaDiCaL version: 2.1.3
% 14.18/2.60 % (3408290)Termination reason: Instruction limit
% 14.18/2.60 % (3408290)Termination phase: Saturation
% 14.18/2.60 % (3408290)Time elapsed: 0.153 s
% 14.18/2.60 % (3408290)Peak memory usage: 120 MB
% 14.18/2.60 % (3408290)Instructions burned: 376 (million)
% 14.18/2.60 % (3408301)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2835123025:i=359:rtra=on:gtg=exists_top:ss=axioms_2983 on theBenchmark for (2983ds/359Mi)
% 14.18/2.60 % (3408303)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2915233509:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/261Mi)
% 14.18/2.60 % (3408302)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2258071745:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2983 on theBenchmark for (2983ds/341Mi)
% 14.18/2.60 % (3408295)Instruction limit reached!
% 14.18/2.60 % (3408295)------------------------------
% 14.18/2.60 % (3408295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.60 % (3408295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.60 % (3408295)CaDiCaL version: 2.1.3
% 14.18/2.60 % (3408295)Termination reason: Instruction limit
% 16.43/2.92 % (3408295)Termination phase: Saturation
% 16.43/2.92 % (3408295)Time elapsed: 0.169 s
% 16.43/2.92 % (3408295)Peak memory usage: 121 MB
% 16.43/2.92 % (3408295)Instructions burned: 388 (million)
% 16.43/2.92 % (3408296)Instruction limit reached!
% 16.43/2.92 % (3408296)------------------------------
% 16.43/2.92 % (3408296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.43/2.92 % (3408296)CaDiCaL version: 2.1.3
% 16.43/2.92 % (3408296)Termination reason: Instruction limit
% 16.43/2.92 % (3408296)Termination phase: Saturation
% 16.43/2.92 % (3408296)Time elapsed: 0.178 s
% 16.43/2.92 % (3408296)Peak memory usage: 92 MB
% 16.43/2.92 % (3408296)Instructions burned: 514 (million)
% 16.43/2.92 % (3408298)Instruction limit reached!
% 16.43/2.92 % (3408298)------------------------------
% 16.43/2.92 % (3408298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.43/2.92 % (3408298)CaDiCaL version: 2.1.3
% 16.43/2.92 % (3408298)Termination reason: Instruction limit
% 16.43/2.92 % (3408298)Termination phase: Saturation
% 16.43/2.92 % (3408298)Time elapsed: 0.152 s
% 16.43/2.92 % (3408298)Peak memory usage: 136 MB
% 16.43/2.92 % (3408298)Instructions burned: 337 (million)
% 16.43/2.92 % (3408303)Instruction limit reached!
% 16.43/2.92 % (3408303)------------------------------
% 16.43/2.92 % (3408303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.43/2.92 % (3408303)CaDiCaL version: 2.1.3
% 16.43/2.92 % (3408303)Termination reason: Instruction limit
% 16.43/2.92 % (3408303)Termination phase: Saturation
% 16.43/2.92 % (3408303)Time elapsed: 0.095 s
% 16.43/2.92 % (3408303)Peak memory usage: 118 MB
% 16.43/2.92 % (3408303)Instructions burned: 261 (million)
% 16.43/2.92 % (3408305)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=4008794104:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/235Mi)
% 16.43/2.92 % (3408301)Instruction limit reached!
% 16.43/2.92 % (3408301)------------------------------
% 16.43/2.92 % (3408301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.43/2.92 % (3408301)CaDiCaL version: 2.1.3
% 16.43/2.92 % (3408301)Termination reason: Instruction limit
% 16.43/2.92 % (3408301)Termination phase: Saturation
% 16.43/2.92 % (3408301)Time elapsed: 0.123 s
% 16.43/2.92 % (3408301)Peak memory usage: 90 MB
% 16.43/2.92 % (3408301)Instructions burned: 361 (million)
% 16.43/2.92 % (3408302)Instruction limit reached!
% 16.43/2.92 % (3408302)------------------------------
% 16.43/2.92 % (3408302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.43/2.92 % (3408302)CaDiCaL version: 2.1.3
% 16.43/2.92 % (3408302)Termination reason: Instruction limit
% 16.43/2.92 % (3408302)Termination phase: Saturation
% 16.43/2.92 % (3408302)Time elapsed: 0.130 s
% 16.43/2.92 % (3408302)Peak memory usage: 120 MB
% 16.43/2.92 % (3408302)Instructions burned: 341 (million)
% 16.43/2.92 % (3408309)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=195988253:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2981 on theBenchmark for (2981ds/273Mi)
% 16.43/2.92 % (3408310)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3472780622:i=146:doe=on:rtra=on_2981 on theBenchmark for (2981ds/146Mi)
% 16.43/2.92 % (3408305)Instruction limit reached!
% 16.43/2.92 % (3408305)------------------------------
% 16.43/2.92 % (3408305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.43/2.92 % (3408305)CaDiCaL version: 2.1.3
% 16.43/2.92 % (3408305)Termination reason: Instruction limit
% 16.43/2.92 % (3408305)Termination phase: Saturation
% 16.43/2.92 % (3408305)Time elapsed: 0.104 s
% 16.43/2.92 % (3408305)Peak memory usage: 119 MB
% 16.43/2.92 % (3408305)Instructions burned: 235 (million)
% 16.43/2.92 % (3408310)Instruction limit reached!
% 16.43/2.92 % (3408310)------------------------------
% 16.43/2.92 % (3408310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.43/2.92 % (3408310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.24 % (3408310)CaDiCaL version: 2.1.3
% 19.84/3.24 % (3408310)Termination reason: Instruction limit
% 19.84/3.24 % (3408310)Termination phase: Saturation
% 19.84/3.24 % (3408310)Time elapsed: 0.053 s
% 19.84/3.24 % (3408310)Peak memory usage: 90 MB
% 19.84/3.24 % (3408310)Instructions burned: 146 (million)
% 19.84/3.24 % (3408312)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3923319902:i=4428:doe=on:fsr=off:rtra=on_2981 on theBenchmark for (2981ds/4428Mi)
% 19.84/3.24 % (3408313)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=847861461:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi)
% 19.84/3.24 % (3408314)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3361794672:i=1052:rtra=on_2980 on theBenchmark for (2980ds/1052Mi)
% 19.84/3.24 % (3408315)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=303552745:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2980 on theBenchmark for (2980ds/655Mi)
% 19.84/3.24 % (3408309)Instruction limit reached!
% 19.84/3.24 % (3408309)------------------------------
% 19.84/3.24 % (3408309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.24 % (3408309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.24 % (3408309)CaDiCaL version: 2.1.3
% 19.84/3.24 % (3408309)Termination reason: Instruction limit
% 19.84/3.24 % (3408309)Termination phase: Saturation
% 19.84/3.24 % (3408309)Time elapsed: 0.109 s
% 19.84/3.24 % (3408309)Peak memory usage: 93 MB
% 19.84/3.24 % (3408309)Instructions burned: 275 (million)
% 19.84/3.24 % (3408318)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1456885038:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2980 on theBenchmark for (2980ds/1054Mi)
% 19.84/3.24 % (3408319)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=303656372:i=107:rtra=on_2979 on theBenchmark for (2979ds/107Mi)
% 19.84/3.24 % (3408313)Instruction limit reached!
% 19.84/3.24 % (3408313)------------------------------
% 19.84/3.24 % (3408313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.24 % (3408313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.24 % (3408313)CaDiCaL version: 2.1.3
% 19.84/3.24 % (3408313)Termination reason: Instruction limit
% 19.84/3.24 % (3408313)Termination phase: Saturation
% 19.84/3.24 % (3408313)Time elapsed: 0.135 s
% 19.84/3.24 % (3408313)Peak memory usage: 136 MB
% 19.84/3.24 % (3408313)Instructions burned: 276 (million)
% 19.84/3.24 % (3408319)Refutation not found, incomplete strategy
% 19.84/3.24 % (3408319)------------------------------
% 19.84/3.24 % (3408319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.24 % (3408319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.24 % (3408319)CaDiCaL version: 2.1.3
% 19.84/3.24 % (3408319)Termination reason: Refutation not found, incomplete strategy
% 19.84/3.24 % (3408319)Time elapsed: 0.021 s
% 19.84/3.24 % (3408319)Peak memory usage: 116 MB
% 19.84/3.24 % (3408319)Instructions burned: 16 (million)
% 19.84/3.24 % (3408324)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1885761641:s2a=on:i=450:doe=on:nm=32:rtra=on_2979 on theBenchmark for (2979ds/450Mi)
% 19.84/3.24 % (3408327)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 19.84/3.24 % (3408315)Instruction limit reached!
% 19.84/3.24 % (3408315)------------------------------
% 19.84/3.24 % (3408315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.24 % (3408315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.24 % (3408315)CaDiCaL version: 2.1.3
% 19.84/3.24 % (3408315)Termination reason: Instruction limit
% 19.84/3.24 % (3408315)Termination phase: Saturation
% 19.84/3.24 % (3408315)Time elapsed: 0.236 s
% 19.84/3.24 % (3408315)Peak memory usage: 97 MB
% 19.84/3.24 % (3408315)Instructions burned: 658 (million)
% 19.84/3.24 % (3408327)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3767368099:i=1090:aac=none:nm=0:rtra=on:rawr=on_2978 on theBenchmark for (2978ds/1090Mi)
% 22.00/3.63 % (3408319)------------------------------
% 22.00/3.63 % (3408319)------------------------------
% 22.00/3.63 % (3408324)Instruction limit reached!
% 22.00/3.63 % (3408324)------------------------------
% 22.00/3.63 % (3408324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.00/3.63 % (3408324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.63 % (3408324)CaDiCaL version: 2.1.3
% 22.00/3.63 % (3408324)Termination reason: Instruction limit
% 22.00/3.63 % (3408324)Termination phase: Saturation
% 22.00/3.63 % (3408324)Time elapsed: 0.129 s
% 22.00/3.63 % (3408324)Peak memory usage: 134 MB
% 22.00/3.63 % (3408324)Instructions burned: 451 (million)
% 22.00/3.63 % (3408314)Instruction limit reached!
% 22.00/3.63 % (3408314)------------------------------
% 22.00/3.63 % (3408314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.00/3.63 % (3408314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.63 % (3408314)CaDiCaL version: 2.1.3
% 22.00/3.63 % (3408314)Termination reason: Instruction limit
% 22.00/3.63 % (3408314)Termination phase: Saturation
% 22.00/3.63 % (3408314)Time elapsed: 0.360 s
% 22.00/3.63 % (3408314)Peak memory usage: 95 MB
% 22.00/3.63 % (3408314)Instructions burned: 1055 (million)
% 22.00/3.63 % (3408330)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2359575688:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2977 on theBenchmark for (2977ds/130Mi)
% 22.00/3.63 % (3408332)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=282744319:i=491:doe=on:rtra=on:gtg=position_2976 on theBenchmark for (2976ds/491Mi)
% 22.00/3.63 % (3408331)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4116270038:i=312:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/312Mi)
% 22.00/3.63 % (3408318)Instruction limit reached!
% 22.00/3.63 % (3408318)------------------------------
% 22.00/3.63 % (3408318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.00/3.63 % (3408318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.63 % (3408318)CaDiCaL version: 2.1.3
% 22.00/3.63 % (3408318)Termination reason: Instruction limit
% 22.00/3.63 % (3408318)Termination phase: Saturation
% 22.00/3.63 % (3408318)Time elapsed: 0.327 s
% 22.00/3.63 % (3408318)Peak memory usage: 97 MB
% 22.00/3.63 % (3408318)Instructions burned: 1054 (million)
% 22.00/3.63 % (3408330)Instruction limit reached!
% 22.00/3.63 % (3408330)------------------------------
% 22.00/3.63 % (3408330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.00/3.63 % (3408330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.63 % (3408330)CaDiCaL version: 2.1.3
% 22.00/3.63 % (3408330)Termination reason: Instruction limit
% 22.00/3.63 % (3408330)Termination phase: Saturation
% 22.00/3.63 % (3408330)Time elapsed: 0.066 s
% 22.00/3.63 % (3408330)Peak memory usage: 118 MB
% 22.00/3.63 % (3408330)Instructions burned: 130 (million)
% 22.00/3.63 % (3408333)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2099939422:s2a=on:i=835:s2at=2:rtra=on_2976 on theBenchmark for (2976ds/835Mi)
% 22.00/3.63 % (3408331)Instruction limit reached!
% 22.00/3.63 % (3408331)------------------------------
% 22.00/3.63 % (3408331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.00/3.63 % (3408331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.63 % (3408331)CaDiCaL version: 2.1.3
% 22.00/3.63 % (3408331)Termination reason: Instruction limit
% 22.00/3.63 % (3408331)Termination phase: Saturation
% 22.00/3.63 % (3408331)Time elapsed: 0.129 s
% 22.00/3.63 % (3408331)Peak memory usage: 119 MB
% 22.00/3.63 % (3408331)Instructions burned: 313 (million)
% 22.00/3.63 % (3408337)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3876446804:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2975 on theBenchmark for (2975ds/307Mi)
% 22.00/3.63 % (3408338)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2582971767:i=776:doe=on:rtra=on_2975 on theBenchmark for (2975ds/776Mi)
% 22.00/3.63 % (3408332)Instruction limit reached!
% 22.00/3.63 % (3408332)------------------------------
% 22.00/3.63 % (3408332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.00/3.63 % (3408332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.63 % (3408332)CaDiCaL version: 2.1.3
% 22.00/3.63 % (3408332)Termination reason: Instruction limit
% 22.00/3.63 % (3408332)Termination phase: Saturation
% 26.01/4.11 % (3408332)Time elapsed: 0.172 s
% 26.01/4.11 % (3408332)Peak memory usage: 93 MB
% 26.01/4.11 % (3408332)Instructions burned: 494 (million)
% 26.01/4.11 % (3408327)Instruction limit reached!
% 26.01/4.11 % (3408327)------------------------------
% 26.01/4.11 % (3408327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408327)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408327)Termination reason: Instruction limit
% 26.01/4.11 % (3408327)Termination phase: Saturation
% 26.01/4.11 % (3408327)Time elapsed: 0.401 s
% 26.01/4.11 % (3408327)Peak memory usage: 127 MB
% 26.01/4.11 % (3408327)Instructions burned: 1092 (million)
% 26.01/4.11 % (3408337)Instruction limit reached!
% 26.01/4.11 % (3408337)------------------------------
% 26.01/4.11 % (3408337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408337)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408337)Termination reason: Instruction limit
% 26.01/4.11 % (3408337)Termination phase: Saturation
% 26.01/4.11 % (3408337)Time elapsed: 0.119 s
% 26.01/4.11 % (3408337)Peak memory usage: 92 MB
% 26.01/4.11 % (3408337)Instructions burned: 309 (million)
% 26.01/4.11 % (3408340)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=343520099:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/646Mi)
% 26.01/4.11 % (3408343)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=241845055:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2974 on theBenchmark for (2974ds/784Mi)
% 26.01/4.11 % (3408344)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=3081491288:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2973 on theBenchmark for (2973ds/1131Mi)
% 26.01/4.11 % (3408338)Instruction limit reached!
% 26.01/4.11 % (3408338)------------------------------
% 26.01/4.11 % (3408338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408338)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408338)Termination reason: Instruction limit
% 26.01/4.11 % (3408338)Termination phase: Saturation
% 26.01/4.11 % (3408338)Time elapsed: 0.225 s
% 26.01/4.11 % (3408338)Peak memory usage: 121 MB
% 26.01/4.11 % (3408338)Instructions burned: 777 (million)
% 26.01/4.11 % (3408346)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3252602848:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/246Mi)
% 26.01/4.11 % (3408333)Instruction limit reached!
% 26.01/4.11 % (3408333)------------------------------
% 26.01/4.11 % (3408333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408333)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408333)Termination reason: Instruction limit
% 26.01/4.11 % (3408333)Termination phase: Saturation
% 26.01/4.11 % (3408333)Time elapsed: 0.311 s
% 26.01/4.11 % (3408333)Peak memory usage: 95 MB
% 26.01/4.11 % (3408333)Instructions burned: 838 (million)
% 26.01/4.11 % (3408340)Instruction limit reached!
% 26.01/4.11 % (3408340)------------------------------
% 26.01/4.11 % (3408340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408340)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408340)Termination reason: Instruction limit
% 26.01/4.11 % (3408340)Termination phase: Saturation
% 26.01/4.11 % (3408340)Time elapsed: 0.221 s
% 26.01/4.11 % (3408340)Peak memory usage: 139 MB
% 26.01/4.11 % (3408340)Instructions burned: 650 (million)
% 26.01/4.11 % (3408346)Instruction limit reached!
% 26.01/4.11 % (3408346)------------------------------
% 26.01/4.11 % (3408346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408346)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408346)Termination reason: Instruction limit
% 26.01/4.11 % (3408346)Termination phase: Saturation
% 26.01/4.11 % (3408346)Time elapsed: 0.100 s
% 26.01/4.11 % (3408346)Peak memory usage: 119 MB
% 26.01/4.11 % (3408346)Instructions burned: 247 (million)
% 26.01/4.11 % (3408349)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1995255567:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/775Mi)
% 26.01/4.11 % (3408351)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3981150046:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2971 on theBenchmark for (2971ds/273Mi)
% 26.01/4.11 % (3408343)Instruction limit reached!
% 26.01/4.11 % (3408343)------------------------------
% 26.01/4.11 % (3408343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408343)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408343)Termination reason: Instruction limit
% 26.01/4.11 % (3408343)Termination phase: Saturation
% 26.01/4.11 % (3408343)Time elapsed: 0.306 s
% 26.01/4.11 % (3408343)Peak memory usage: 122 MB
% 26.01/4.11 % (3408343)Instructions burned: 784 (million)
% 26.01/4.11 % (3408352)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2461392138:i=102:nm=16:rtra=on_2970 on theBenchmark for (2970ds/102Mi)
% 26.01/4.11 % (3408351)Instruction limit reached!
% 26.01/4.11 % (3408351)------------------------------
% 26.01/4.11 % (3408351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408351)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408351)Termination reason: Instruction limit
% 26.01/4.11 % (3408351)Termination phase: Saturation
% 26.01/4.11 % (3408351)Time elapsed: 0.106 s
% 26.01/4.11 % (3408351)Peak memory usage: 91 MB
% 26.01/4.11 % (3408351)Instructions burned: 275 (million)
% 26.01/4.11 % (3408353)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3501726701:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2970 on theBenchmark for (2970ds/1094Mi)
% 26.01/4.11 % (3408352)Instruction limit reached!
% 26.01/4.11 % (3408352)------------------------------
% 26.01/4.11 % (3408352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408352)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408352)Termination reason: Instruction limit
% 26.01/4.11 % (3408352)Termination phase: Saturation
% 26.01/4.11 % (3408352)Time elapsed: 0.036 s
% 26.01/4.11 % (3408352)Peak memory usage: 89 MB
% 26.01/4.11 % (3408352)Instructions burned: 105 (million)
% 26.01/4.11 % (3408357)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=922601366:i=6400:doe=on:fsr=off:rtra=on_2969 on theBenchmark for (2969ds/6400Mi)
% 26.01/4.11 % (3408359)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=256440867:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2969 on theBenchmark for (2969ds/868Mi)
% 26.01/4.11 % (3408360)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=2060383216:i=1846:canc=cautious:fsr=off:rtra=on_2969 on theBenchmark for (2969ds/1846Mi)
% 26.01/4.11 % (3408349)Instruction limit reached!
% 26.01/4.11 % (3408349)------------------------------
% 26.01/4.11 % (3408349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408349)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408349)Termination reason: Instruction limit
% 26.01/4.11 % (3408349)Termination phase: Saturation
% 26.01/4.11 % (3408349)Time elapsed: 0.271 s
% 26.01/4.11 % (3408349)Peak memory usage: 95 MB
% 26.01/4.11 % (3408349)Instructions burned: 776 (million)
% 26.01/4.11 % (3408344)Instruction limit reached!
% 26.01/4.11 % (3408344)------------------------------
% 26.01/4.11 % (3408344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408344)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408344)Termination reason: Instruction limit
% 26.01/4.11 % (3408344)Termination phase: Saturation
% 26.01/4.11 % (3408344)Time elapsed: 0.414 s
% 26.01/4.11 % (3408344)Peak memory usage: 123 MB
% 26.01/4.11 % (3408344)Instructions burned: 1132 (million)
% 26.01/4.11 % (3408353)Instruction limit reached!
% 26.01/4.11 % (3408353)------------------------------
% 26.01/4.11 % (3408353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408353)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408353)Termination reason: Instruction limit
% 26.01/4.11 % (3408353)Termination phase: Saturation
% 26.01/4.11 % (3408353)Time elapsed: 0.258 s
% 26.01/4.11 % (3408353)Peak memory usage: 92 MB
% 26.01/4.11 % (3408353)Instructions burned: 1095 (million)
% 26.01/4.11 % (3408364)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1040354368:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2967 on theBenchmark for (2967ds/36816Mi)
% 26.01/4.11 % (3408365)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3012424226:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2967 on theBenchmark for (2967ds/273Mi)
% 26.01/4.11 % (3408312)Instruction limit reached!
% 26.01/4.11 % (3408312)------------------------------
% 26.01/4.11 % (3408312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408312)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408312)Termination reason: Instruction limit
% 26.01/4.11 % (3408312)Termination phase: Saturation
% 26.01/4.11 % (3408312)Time elapsed: 1.395 s
% 26.01/4.11 % (3408312)Peak memory usage: 113 MB
% 26.01/4.11 % (3408312)Instructions burned: 4428 (million)
% 26.01/4.11 % (3408359)Instruction limit reached!
% 26.01/4.11 % (3408359)------------------------------
% 26.01/4.11 % (3408359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408359)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408359)Termination reason: Instruction limit
% 26.01/4.11 % (3408359)Termination phase: Saturation
% 26.01/4.11 % (3408359)Time elapsed: 0.255 s
% 26.01/4.11 % (3408359)Peak memory usage: 120 MB
% 26.01/4.11 % (3408359)Instructions burned: 869 (million)
% 26.01/4.11 % (3408366)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3017202082:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2966 on theBenchmark for (2966ds/863Mi)
% 26.01/4.11 % (3408365)Instruction limit reached!
% 26.01/4.11 % (3408365)------------------------------
% 26.01/4.11 % (3408365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408365)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408365)Termination reason: Instruction limit
% 26.01/4.11 % (3408365)Termination phase: Saturation
% 26.01/4.11 % (3408365)Time elapsed: 0.104 s
% 26.01/4.11 % (3408365)Peak memory usage: 92 MB
% 26.01/4.11 % (3408365)Instructions burned: 273 (million)
% 26.01/4.11 % (3408369)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2851886220:i=5811:kws=precedence:nm=0:rtra=on_2965 on theBenchmark for (2965ds/5811Mi)
% 26.01/4.11 % (3408370)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3460410819:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/2216Mi)
% 26.01/4.11 % (3408372)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3300817784:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2965 on theBenchmark for (2965ds/801Mi)
% 26.01/4.11 % (3408369)First to succeed.
% 26.01/4.11 % (3408369)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3408129"
% 26.01/4.11 % (3408366)Instruction limit reached!
% 26.01/4.11 % (3408366)------------------------------
% 26.01/4.11 % (3408366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.11 % (3408366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.11 % (3408366)CaDiCaL version: 2.1.3
% 26.01/4.11 % (3408366)Termination reason: Instruction limit
% 26.01/4.11 % (3408366)Termination phase: Saturation
% 26.01/4.11 % (3408366)Time elapsed: 0.268 s
% 26.01/4.11 % (3408366)Peak memory usage: 120 MB
% 26.01/4.11 % (3408366)Instructions burned: 865 (million)
% 26.01/4.11 % (3408369)Refutation found. Thanks to Tanya!
% 26.01/4.11 % SZS status Theorem for theBenchmark
% 26.01/4.11 % SZS output start Proof for theBenchmark
% See solution above
% 26.83/4.21 % (3408369)------------------------------
% 26.83/4.21 % (3408369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.83/4.21 % (3408369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.83/4.21 % (3408369)CaDiCaL version: 2.1.3
% 26.83/4.21 % (3408369)Termination reason: Refutation
% 26.83/4.21 % (3408369)Time elapsed: 0.093 s
% 26.83/4.21 % (3408369)Peak memory usage: 119 MB
% 26.83/4.21 % (3408369)Instructions burned: 222 (million)
% 26.83/4.21 % (3408369)------------------------------
% 26.83/4.21 % (3408369)------------------------------
% 26.83/4.21 % (3408129)Success in time 3.779 s
% 26.83/4.21 % Vampire exiting
%------------------------------------------------------------------------------