%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX091_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:45:52 PM UTC 2026
% Result : Theorem 6.76s 1.73s
% Output : Refutation 6.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 9
% Syntax : Number of formulae : 40 ( 7 unt; 0 typ; 7 def)
% Number of atoms : 112 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 119 ( 47 ~; 33 |; 25 &)
% ( 10 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number arithmetic : 330 ( 53 atm; 134 fun; 113 num; 30 var)
% Number of types : 4 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 18 usr; 8 prp; 0-2 aty)
% Number of functors : 13 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 30 ( 26 !; 4 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
general: $tType ).
tff(type_def_6,type,
symbol: $tType ).
tff(func_def_0,type,
f__integer__: $int > general ).
tff(func_def_1,type,
f__symbolic__: symbol > general ).
tff(func_def_2,type,
c__infimum__: general ).
tff(func_def_3,type,
c__supremum__: general ).
tff(func_def_4,type,
n_i: $int ).
tff(func_def_10,type,
sK0: general > $int ).
tff(func_def_11,type,
sK1: $int ).
tff(func_def_12,type,
sK2: $int ).
tff(func_def_13,type,
sK3: general > symbol ).
tff(pred_def_1,type,
p__is_integer__: general > $o ).
tff(pred_def_2,type,
p__is_symbolic__: general > $o ).
tff(pred_def_3,type,
p__less_equal__: ( general * general ) > $o ).
tff(pred_def_4,type,
p__less__: ( general * general ) > $o ).
tff(pred_def_5,type,
p__greater_equal__: ( general * general ) > $o ).
tff(pred_def_6,type,
p__greater__: ( general * general ) > $o ).
tff(pred_def_8,type,
three: general > $o ).
tff(pred_def_9,type,
sqrt: general > $o ).
tff(pred_def_10,type,
three_p: general > $o ).
tff(pred_def_11,type,
more_than_three: general > $o ).
tff(pred_def_12,type,
sqrt: ( general * general ) > $o ).
tff(f21,axiom,
! [X1: $int,X0: $int] :
( sqrt(f__integer__(X0),f__integer__(X1))
<=> ( $less(X1,$product($sum(X0,1),$sum(X0,1)))
& $greatereq(X0,0)
& $lesseq($product(X0,X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_5_unnamed_formula) ).
tff(f22,conjecture,
! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X0),f__integer__(X1))
& $lesseq($product($sum(X0,1),$sum(X0,1)),$sum(X1,1)) )
=> sqrt(f__integer__($sum(X0,1)),f__integer__($sum(X1,1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_6_unnamed_formula) ).
tff(f23,negated_conjecture,
~ ! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X0),f__integer__(X1))
& $lesseq($product($sum(X0,1),$sum(X0,1)),$sum(X1,1)) )
=> sqrt(f__integer__($sum(X0,1)),f__integer__($sum(X1,1))) ),
inference(negated_conjecture,[status(cth)],[f22]) ).
tff(f24,plain,
! [X1: $int,X0: $int] :
( sqrt(f__integer__(X0),f__integer__(X1))
<=> ( $less(X1,$product($sum(X0,1),$sum(X0,1)))
& ~ $less(X0,0)
& ~ $less(X1,$product(X0,X0)) ) ),
inference(theory_normalization,[],[f21]) ).
tff(f31,plain,
~ ! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X0),f__integer__(X1))
& ~ $less($sum(X1,1),$product($sum(X0,1),$sum(X0,1))) )
=> sqrt(f__integer__($sum(X0,1)),f__integer__($sum(X1,1))) ),
inference(theory_normalization,[],[f23]) ).
tff(f51,plain,
! [X1: $int,X0: $int] :
( sqrt(f__integer__(X1),f__integer__(X0))
<=> ( ~ $less(X1,0)
& $less(X0,$product($sum(X1,1),$sum(X1,1)))
& ~ $less(X0,$product(X1,X1)) ) ),
inference(rectify,[],[f24]) ).
tff(f59,plain,
~ ! [X0: $int,X1: $int] :
( ( ~ $less($sum(X0,1),$product($sum(X1,1),$sum(X1,1)))
& sqrt(f__integer__(X1),f__integer__(X0)) )
=> sqrt(f__integer__($sum(X1,1)),f__integer__($sum(X0,1))) ),
inference(rectify,[],[f31]) ).
tff(f70,plain,
? [X0: $int,X1: $int] :
( ~ sqrt(f__integer__($sum(X1,1)),f__integer__($sum(X0,1)))
& ~ $less($sum(X0,1),$product($sum(X1,1),$sum(X1,1)))
& sqrt(f__integer__(X1),f__integer__(X0)) ),
inference(ennf_transformation,[],[f59]) ).
tff(f71,plain,
? [X0: $int,X1: $int] :
( ~ sqrt(f__integer__($sum(X1,1)),f__integer__($sum(X0,1)))
& sqrt(f__integer__(X1),f__integer__(X0))
& ~ $less($sum(X0,1),$product($sum(X1,1),$sum(X1,1))) ),
inference(flattening,[],[f70]) ).
tff(f73,plain,
! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X1),f__integer__(X0))
| $less(X1,0)
| ~ $less(X0,$product($sum(X1,1),$sum(X1,1)))
| $less(X0,$product(X1,X1)) )
& ( ( ~ $less(X1,0)
& $less(X0,$product($sum(X1,1),$sum(X1,1)))
& ~ $less(X0,$product(X1,X1)) )
| ~ sqrt(f__integer__(X1),f__integer__(X0)) ) ),
inference(nnf_transformation,[],[f51]) ).
tff(f74,plain,
! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X1),f__integer__(X0))
| $less(X1,0)
| ~ $less(X0,$product($sum(X1,1),$sum(X1,1)))
| $less(X0,$product(X1,X1)) )
& ( ( ~ $less(X1,0)
& $less(X0,$product($sum(X1,1),$sum(X1,1)))
& ~ $less(X0,$product(X1,X1)) )
| ~ sqrt(f__integer__(X1),f__integer__(X0)) ) ),
inference(flattening,[],[f73]) ).
tff(f75,plain,
! [X0: $int,X1: $int] :
( ( sqrt(f__integer__(X0),f__integer__(X1))
| $less(X0,0)
| ~ $less(X1,$product($sum(X0,1),$sum(X0,1)))
| $less(X1,$product(X0,X0)) )
& ( ( ~ $less(X0,0)
& $less(X1,$product($sum(X0,1),$sum(X0,1)))
& ~ $less(X1,$product(X0,X0)) )
| ~ sqrt(f__integer__(X0),f__integer__(X1)) ) ),
inference(rectify,[],[f74]) ).
tff(f80,plain,
( ~ sqrt(f__integer__($sum(sK2,1)),f__integer__($sum(sK1,1)))
& sqrt(f__integer__(sK2),f__integer__(sK1))
& ~ $less($sum(sK1,1),$product($sum(sK2,1),$sum(sK2,1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f71]) ).
tff(f89,plain,
! [X0: $int,X1: $int] :
( ~ sqrt(f__integer__(X0),f__integer__(X1))
| $less(X1,$product($sum(X0,1),$sum(X0,1))) ),
inference(cnf_transformation,[],[f75]) ).
tff(f90,plain,
! [X0: $int,X1: $int] :
( ~ sqrt(f__integer__(X0),f__integer__(X1))
| ~ $less(X0,0) ),
inference(cnf_transformation,[],[f75]) ).
tff(f91,plain,
! [X0: $int,X1: $int] :
( sqrt(f__integer__(X0),f__integer__(X1))
| $less(X1,$product(X0,X0))
| $less(X0,0)
| ~ $less(X1,$product($sum(X0,1),$sum(X0,1))) ),
inference(cnf_transformation,[],[f75]) ).
tff(f100,plain,
~ $less($sum(sK1,1),$product($sum(sK2,1),$sum(sK2,1))),
inference(cnf_transformation,[],[f80]) ).
tff(f101,plain,
sqrt(f__integer__(sK2),f__integer__(sK1)),
inference(cnf_transformation,[],[f80]) ).
tff(f102,plain,
~ sqrt(f__integer__($sum(sK2,1)),f__integer__($sum(sK1,1))),
inference(cnf_transformation,[],[f80]) ).
tff(f112,definition,
( spl4_1
<=> $less($sum(sK1,1),$product($sum(sK2,1),$sum(sK2,1))) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
tff(f114,plain,
( ~ $less($sum(sK1,1),$product($sum(sK2,1),$sum(sK2,1)))
| spl4_1 ),
inference(avatar_component_clause,[],[f112]) ).
tff(f115,plain,
~ spl4_1,
inference(avatar_split_clause,[],[f100,f112]) ).
tff(f117,definition,
( spl4_2
<=> sqrt(f__integer__(sK2),f__integer__(sK1)) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
tff(f119,plain,
( sqrt(f__integer__(sK2),f__integer__(sK1))
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f117]) ).
tff(f120,plain,
spl4_2,
inference(avatar_split_clause,[],[f101,f117]) ).
tff(f127,definition,
( spl4_4
<=> sqrt(f__integer__($sum(sK2,1)),f__integer__($sum(sK1,1))) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
tff(f129,plain,
( ~ sqrt(f__integer__($sum(sK2,1)),f__integer__($sum(sK1,1)))
| spl4_4 ),
inference(avatar_component_clause,[],[f127]) ).
tff(f130,plain,
~ spl4_4,
inference(avatar_split_clause,[],[f102,f127]) ).
tff(f212,plain,
( ~ $less(sK2,0)
| ~ spl4_2 ),
inference(resolution,[],[f90,f119]) ).
tff(f214,definition,
( spl4_15
<=> $less(sK2,0) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
tff(f217,plain,
( ~ spl4_15
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f212,f117,f214]) ).
tff(f303,plain,
( $less(sK1,$product($sum(sK2,1),$sum(sK2,1)))
| ~ spl4_2 ),
inference(resolution,[],[f89,f119]) ).
tff(f305,definition,
( spl4_23
<=> $less(sK1,$product($sum(sK2,1),$sum(sK2,1))) ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
tff(f308,plain,
( spl4_23
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f303,f117,f305]) ).
tff(f314,plain,
( ~ $less($sum(sK1,1),$product($sum($sum(sK2,1),1),$sum($sum(sK2,1),1)))
| $less($sum(sK2,1),0)
| $less($sum(sK1,1),$product($sum(sK2,1),$sum(sK2,1)))
| spl4_4 ),
inference(resolution,[],[f91,f129]) ).
tff(f318,plain,
( ~ $less($sum(sK1,1),$product($sum($sum(sK2,1),1),$sum($sum(sK2,1),1)))
| $less($sum(sK2,1),0)
| spl4_1
| spl4_4 ),
inference(forward_subsumption_resolution,[],[f314,f114]) ).
tff(f320,definition,
( spl4_25
<=> $less($sum(sK1,1),$product($sum($sum(sK2,1),1),$sum($sum(sK2,1),1))) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
tff(f324,definition,
( spl4_26
<=> $less($sum(sK2,1),0) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
tff(f327,plain,
( ~ spl4_25
| spl4_26
| spl4_1
| spl4_4 ),
inference(avatar_split_clause,[],[f318,f127,f112,f324,f320]) ).
tff(f328,plain,
$false,
inference(avatar_smt_refutation,[],[f327,f308,f217,f130,f120,f115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX091_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n008.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 15:01:40 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.34/1.16 % (2313164)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.34/1.16 % (2313172)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1443658300:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.34/1.16 % (2313172)Instruction limit reached!
% 3.34/1.16 % (2313172)------------------------------
% 3.34/1.16 % (2313172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.34/1.16 % (2313172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/1.16 % (2313172)CaDiCaL version: 2.1.3
% 3.34/1.16 % (2313172)Termination reason: Instruction limit
% 3.34/1.16 % (2313172)Termination phase: Saturation
% 3.34/1.16 % (2313172)Time elapsed: 0.003 s
% 3.34/1.16 % (2313172)Peak memory usage: 88 MB
% 3.34/1.16 % (2313172)Instructions burned: 8 (million)
% 3.34/1.16 % (2313175)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1762413096:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.34/1.16 % (2313173)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2555983054:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.34/1.16 % (2313174)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=568338367:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.34/1.16 % (2313169)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2733837389:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.34/1.16 % (2313170)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=532537263:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.34/1.16 % (2313171)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2476089863:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.34/1.16 % (2313173)Instruction limit reached!
% 3.34/1.16 % (2313173)------------------------------
% 3.34/1.16 % (2313173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.34/1.16 % (2313173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/1.16 % (2313173)CaDiCaL version: 2.1.3
% 3.34/1.16 % (2313173)Termination reason: Instruction limit
% 3.34/1.16 % (2313173)Termination phase: Saturation
% 3.34/1.16 % (2313173)Time elapsed: 0.004 s
% 3.34/1.16 % (2313173)Peak memory usage: 89 MB
% 3.34/1.16 % (2313173)Instructions burned: 5 (million)
% 3.34/1.16 % (2313169)Instruction limit reached!
% 3.34/1.16 % (2313169)------------------------------
% 3.34/1.16 % (2313169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.34/1.16 % (2313169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/1.16 % (2313169)CaDiCaL version: 2.1.3
% 3.34/1.16 % (2313169)Termination reason: Instruction limit
% 3.34/1.16 % (2313169)Termination phase: Saturation
% 3.34/1.16 % (2313169)Time elapsed: 0.031 s
% 3.34/1.16 % (2313169)Peak memory usage: 116 MB
% 3.34/1.16 % (2313169)Instructions burned: 12 (million)
% 3.34/1.16 % (2313175)Instruction limit reached!
% 3.34/1.16 % (2313175)------------------------------
% 3.34/1.16 % (2313175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.34/1.16 % (2313175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/1.16 % (2313175)CaDiCaL version: 2.1.3
% 3.34/1.16 % (2313175)Termination reason: Instruction limit
% 3.34/1.16 % (2313175)Termination phase: Saturation
% 3.34/1.16 % (2313175)Time elapsed: 0.047 s
% 3.34/1.16 % (2313175)Peak memory usage: 117 MB
% 3.34/1.16 % (2313175)Instructions burned: 34 (million)
% 3.34/1.16 % (2313177)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=953329376:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.34/1.16 % (2313174)Instruction limit reached!
% 3.34/1.16 % (2313174)------------------------------
% 3.34/1.16 % (2313174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.34/1.16 % (2313174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/1.16 % (2313174)CaDiCaL version: 2.1.3
% 3.34/1.16 % (2313174)Termination reason: Instruction limit
% 3.34/1.16 % (2313174)Termination phase: Saturation
% 3.34/1.16 % (2313174)Time elapsed: 0.056 s
% 3.34/1.16 % (2313174)Peak memory usage: 117 MB
% 3.34/1.16 % (2313174)Instructions burned: 47 (million)
% 3.34/1.16 % (2313177)Instruction limit reached!
% 3.34/1.16 % (2313177)------------------------------
% 3.34/1.16 % (2313177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.29 % (2313177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.29 % (2313177)CaDiCaL version: 2.1.3
% 3.86/1.29 % (2313177)Termination reason: Instruction limit
% 3.86/1.29 % (2313177)Termination phase: Saturation
% 3.86/1.29 % (2313177)Time elapsed: 0.006 s
% 3.86/1.29 % (2313177)Peak memory usage: 88 MB
% 3.86/1.29 % (2313177)Instructions burned: 17 (million)
% 3.86/1.29 % (2313171)Instruction limit reached!
% 3.86/1.29 % (2313171)------------------------------
% 3.86/1.29 % (2313171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.29 % (2313171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.29 % (2313171)CaDiCaL version: 2.1.3
% 3.86/1.29 % (2313171)Termination reason: Instruction limit
% 3.86/1.29 % (2313171)Termination phase: Saturation
% 3.86/1.29 % (2313171)Time elapsed: 0.124 s
% 3.86/1.29 % (2313171)Peak memory usage: 117 MB
% 3.86/1.29 % (2313171)Instructions burned: 202 (million)
% 3.86/1.29 % (2313188)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=4158761709:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.86/1.29 % (2313184)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=2613127810:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.86/1.29 % (2313188)Instruction limit reached!
% 3.86/1.29 % (2313188)------------------------------
% 3.86/1.29 % (2313188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.29 % (2313188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.29 % (2313188)CaDiCaL version: 2.1.3
% 3.86/1.29 % (2313188)Termination reason: Instruction limit
% 3.86/1.29 % (2313188)Termination phase: Saturation
% 3.86/1.29 % (2313188)Time elapsed: 0.008 s
% 3.86/1.29 % (2313188)Peak memory usage: 89 MB
% 3.86/1.29 % (2313188)Instructions burned: 28 (million)
% 3.86/1.29 % (2313184)Instruction limit reached!
% 3.86/1.29 % (2313184)------------------------------
% 3.86/1.29 % (2313184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.29 % (2313184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.29 % (2313184)CaDiCaL version: 2.1.3
% 3.86/1.29 % (2313184)Termination reason: Instruction limit
% 3.86/1.29 % (2313184)Termination phase: Saturation
% 3.86/1.29 % (2313184)Time elapsed: 0.023 s
% 3.86/1.29 % (2313184)Peak memory usage: 89 MB
% 3.86/1.29 % (2313184)Instructions burned: 29 (million)
% 3.86/1.29 % (2313185)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2067418041:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.86/1.29 % (2313187)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=334609603:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 3.86/1.29 % (2313170)Instruction limit reached!
% 3.86/1.29 % (2313170)------------------------------
% 3.86/1.29 % (2313170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.29 % (2313170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.29 % (2313170)CaDiCaL version: 2.1.3
% 3.86/1.29 % (2313170)Termination reason: Instruction limit
% 3.86/1.29 % (2313170)Termination phase: Saturation
% 3.86/1.29 % (2313170)Time elapsed: 0.173 s
% 3.86/1.29 % (2313170)Peak memory usage: 118 MB
% 3.86/1.29 % (2313170)Instructions burned: 308 (million)
% 3.86/1.29 % (2313185)Instruction limit reached!
% 3.86/1.29 % (2313185)------------------------------
% 3.86/1.29 % (2313185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.29 % (2313185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.29 % (2313185)CaDiCaL version: 2.1.3
% 3.86/1.29 % (2313185)Termination reason: Instruction limit
% 3.86/1.29 % (2313185)Termination phase: Saturation
% 3.86/1.29 % (2313185)Time elapsed: 0.012 s
% 3.86/1.29 % (2313185)Peak memory usage: 90 MB
% 3.86/1.29 % (2313185)Instructions burned: 18 (million)
% 3.86/1.29 % (2313189)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3341286611:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.86/1.29 % (2313187)Instruction limit reached!
% 3.86/1.29 % (2313187)------------------------------
% 3.86/1.29 % (2313187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.45 % (2313187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.45 % (2313187)CaDiCaL version: 2.1.3
% 4.53/1.45 % (2313187)Termination reason: Instruction limit
% 4.53/1.45 % (2313187)Termination phase: Saturation
% 4.53/1.45 % (2313187)Time elapsed: 0.020 s
% 4.53/1.45 % (2313187)Peak memory usage: 89 MB
% 4.53/1.45 % (2313187)Instructions burned: 27 (million)
% 4.53/1.45 % (2313189)Instruction limit reached!
% 4.53/1.45 % (2313189)------------------------------
% 4.53/1.45 % (2313189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.45 % (2313189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.45 % (2313189)CaDiCaL version: 2.1.3
% 4.53/1.45 % (2313189)Termination reason: Instruction limit
% 4.53/1.45 % (2313189)Termination phase: Saturation
% 4.53/1.45 % (2313189)Time elapsed: 0.043 s
% 4.53/1.45 % (2313189)Peak memory usage: 89 MB
% 4.53/1.45 % (2313189)Instructions burned: 87 (million)
% 4.53/1.45 % (2313193)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2737086253:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 4.53/1.45 % (2313190)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=783017012:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 4.53/1.45 % (2313190)Instruction limit reached!
% 4.53/1.45 % (2313190)------------------------------
% 4.53/1.45 % (2313190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.45 % (2313190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.45 % (2313190)CaDiCaL version: 2.1.3
% 4.53/1.45 % (2313190)Termination reason: Instruction limit
% 4.53/1.45 % (2313190)Termination phase: Saturation
% 4.53/1.45 % (2313190)Time elapsed: 0.002 s
% 4.53/1.45 % (2313190)Peak memory usage: 88 MB
% 4.53/1.45 % (2313190)Instructions burned: 2 (million)
% 4.53/1.45 % (2313196)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2606870664:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 4.53/1.45 % (2313196)Instruction limit reached!
% 4.53/1.45 % (2313196)------------------------------
% 4.53/1.45 % (2313196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.45 % (2313196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.45 % (2313196)CaDiCaL version: 2.1.3
% 4.53/1.45 % (2313196)Termination reason: Instruction limit
% 4.53/1.45 % (2313196)Termination phase: Saturation
% 4.53/1.45 % (2313196)Time elapsed: 0.004 s
% 4.53/1.45 % (2313196)Peak memory usage: 88 MB
% 4.53/1.45 % (2313196)Instructions burned: 5 (million)
% 4.53/1.45 % (2313199)lrs+10_1_thi=all:si=on:fd=off:random_seed=651332904:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 4.53/1.45 % (2313193)Instruction limit reached!
% 4.53/1.45 % (2313193)------------------------------
% 4.53/1.45 % (2313193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.45 % (2313193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.45 % (2313193)CaDiCaL version: 2.1.3
% 4.53/1.45 % (2313193)Termination reason: Instruction limit
% 4.53/1.45 % (2313193)Termination phase: Saturation
% 4.53/1.45 % (2313193)Time elapsed: 0.070 s
% 4.53/1.45 % (2313193)Peak memory usage: 91 MB
% 4.53/1.45 % (2313193)Instructions burned: 181 (million)
% 4.53/1.45 % (2313197)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1858635743:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 4.53/1.45 % (2313200)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=1512599937:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 4.53/1.45 % (2313200)Instruction limit reached!
% 4.53/1.45 % (2313200)------------------------------
% 4.53/1.45 % (2313200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.45 % (2313200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.45 % (2313200)CaDiCaL version: 2.1.3
% 4.53/1.45 % (2313200)Termination reason: Instruction limit
% 4.53/1.45 % (2313200)Termination phase: Saturation
% 4.53/1.45 % (2313200)Time elapsed: 0.006 s
% 4.53/1.45 % (2313200)Peak memory usage: 88 MB
% 4.53/1.45 % (2313200)Instructions burned: 8 (million)
% 4.53/1.45 % (2313202)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1469015056:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 5.03/1.54 % (2313202)Instruction limit reached!
% 5.03/1.54 % (2313202)------------------------------
% 5.03/1.54 % (2313202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313202)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313202)Termination reason: Instruction limit
% 5.03/1.54 % (2313202)Termination phase: Saturation
% 5.03/1.54 % (2313202)Time elapsed: 0.002 s
% 5.03/1.54 % (2313202)Peak memory usage: 88 MB
% 5.03/1.54 % (2313202)Instructions burned: 2 (million)
% 5.03/1.54 % (2313199)Instruction limit reached!
% 5.03/1.54 % (2313199)------------------------------
% 5.03/1.54 % (2313199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313199)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313199)Termination reason: Instruction limit
% 5.03/1.54 % (2313199)Termination phase: Saturation
% 5.03/1.54 % (2313199)Time elapsed: 0.065 s
% 5.03/1.54 % (2313199)Peak memory usage: 117 MB
% 5.03/1.54 % (2313199)Instructions burned: 53 (million)
% 5.03/1.54 % (2313204)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3047978353:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.03/1.54 % (2313208)dis+10_1_si=on:random_seed=411602931:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 5.03/1.54 % (2313204)Instruction limit reached!
% 5.03/1.54 % (2313204)------------------------------
% 5.03/1.54 % (2313204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313204)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313204)Termination reason: Instruction limit
% 5.03/1.54 % (2313204)Termination phase: Property scanning
% 5.03/1.54 % (2313204)Time elapsed: 0.002 s
% 5.03/1.54 % (2313204)Peak memory usage: 86 MB
% 5.03/1.54 % (2313204)Instructions burned: 2 (million)
% 5.03/1.54 % (2313208)Instruction limit reached!
% 5.03/1.54 % (2313208)------------------------------
% 5.03/1.54 % (2313208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313208)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313208)Termination reason: Instruction limit
% 5.03/1.54 % (2313208)Termination phase: Saturation
% 5.03/1.54 % (2313208)Time elapsed: 0.004 s
% 5.03/1.54 % (2313208)Peak memory usage: 88 MB
% 5.03/1.54 % (2313208)Instructions burned: 11 (million)
% 5.03/1.54 % (2313197)Instruction limit reached!
% 5.03/1.54 % (2313197)------------------------------
% 5.03/1.54 % (2313197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313197)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313197)Termination reason: Instruction limit
% 5.03/1.54 % (2313197)Termination phase: Saturation
% 5.03/1.54 % (2313197)Time elapsed: 0.098 s
% 5.03/1.54 % (2313197)Peak memory usage: 135 MB
% 5.03/1.54 % (2313197)Instructions burned: 67 (million)
% 5.03/1.54 % (2313206)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2325658074:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 5.03/1.54 % (2313206)First to succeed.
% 5.03/1.54 % (2313206)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2313164"
% 5.03/1.54 % (2313211)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4293535123:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi)
% 5.03/1.54 % (2313213)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=804864391: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.03/1.54 % (2313218)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3863451043:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 5.03/1.54 % (2313211)Refutation not found, incomplete strategy
% 5.03/1.54 % (2313211)------------------------------
% 5.03/1.54 % (2313211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313211)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313211)Termination reason: Refutation not found, incomplete strategy
% 5.03/1.54 % (2313211)Time elapsed: 0.004 s
% 5.03/1.54 % (2313211)Peak memory usage: 89 MB
% 5.03/1.54 % (2313211)Instructions burned: 4 (million)
% 5.03/1.54 % (2313214)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3597077720:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 5.03/1.54 % (2313214)Instruction limit reached!
% 5.03/1.54 % (2313214)------------------------------
% 5.03/1.54 % (2313214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313214)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313214)Termination reason: Instruction limit
% 5.03/1.54 % (2313214)Termination phase: Saturation
% 5.03/1.54 % (2313214)Time elapsed: 0.002 s
% 5.03/1.54 % (2313214)Peak memory usage: 88 MB
% 5.03/1.54 % (2313214)Instructions burned: 2 (million)
% 5.03/1.54 % (2313213)Instruction limit reached!
% 5.03/1.54 % (2313213)------------------------------
% 5.03/1.54 % (2313213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313213)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313213)Termination reason: Instruction limit
% 5.03/1.54 % (2313213)Termination phase: Saturation
% 5.03/1.54 % (2313213)Time elapsed: 0.028 s
% 5.03/1.54 % (2313213)Peak memory usage: 89 MB
% 5.03/1.54 % (2313213)Instructions burned: 35 (million)
% 5.03/1.54 % (2313217)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3789904474:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 5.03/1.54 % (2313217)Instruction limit reached!
% 5.03/1.54 % (2313217)------------------------------
% 5.03/1.54 % (2313217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313217)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313217)Termination reason: Instruction limit
% 5.03/1.54 % (2313217)Termination phase: Saturation
% 5.03/1.54 % (2313217)Time elapsed: 0.007 s
% 5.03/1.54 % (2313217)Peak memory usage: 88 MB
% 5.03/1.54 % (2313217)Instructions burned: 9 (million)
% 5.03/1.54 % (2313220)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=600206164:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi)
% 5.03/1.54 % (2313218)Instruction limit reached!
% 5.03/1.54 % (2313218)------------------------------
% 5.03/1.54 % (2313218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313218)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313218)Termination reason: Instruction limit
% 5.03/1.54 % (2313218)Termination phase: Saturation
% 5.03/1.54 % (2313218)Time elapsed: 0.112 s
% 5.03/1.54 % (2313218)Peak memory usage: 95 MB
% 5.03/1.54 % (2313218)Instructions burned: 373 (million)
% 5.03/1.54 % (2313220)Instruction limit reached!
% 5.03/1.54 % (2313220)------------------------------
% 5.03/1.54 % (2313220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313220)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313220)Termination reason: Instruction limit
% 5.03/1.54 % (2313220)Termination phase: Saturation
% 5.03/1.54 % (2313220)Time elapsed: 0.032 s
% 5.03/1.54 % (2313220)Peak memory usage: 116 MB
% 5.03/1.54 % (2313220)Instructions burned: 14 (million)
% 5.03/1.54 % (2313225)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1496831:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 5.03/1.54 % (2313226)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3592041176:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 5.03/1.54 % (2313226)Instruction limit reached!
% 5.03/1.54 % (2313226)------------------------------
% 5.03/1.54 % (2313226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.54 % (2313226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.54 % (2313226)CaDiCaL version: 2.1.3
% 5.03/1.54 % (2313226)Termination reason: Instruction limit
% 6.76/1.73 % (2313226)Termination phase: Saturation
% 6.76/1.73 % (2313226)Time elapsed: 0.009 s
% 6.76/1.73 % (2313226)Peak memory usage: 88 MB
% 6.76/1.73 % (2313226)Instructions burned: 10 (million)
% 6.76/1.73 % (2313228)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2734359452:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi)
% 6.76/1.73 % (2313230)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=1382344984:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 6.76/1.73 % (2313230)Instruction limit reached!
% 6.76/1.73 % (2313230)------------------------------
% 6.76/1.73 % (2313230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.73 % (2313230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.73 % (2313230)CaDiCaL version: 2.1.3
% 6.76/1.73 % (2313230)Termination reason: Instruction limit
% 6.76/1.73 % (2313230)Termination phase: Saturation
% 6.76/1.73 % (2313230)Time elapsed: 0.031 s
% 6.76/1.73 % (2313230)Peak memory usage: 90 MB
% 6.76/1.73 % (2313230)Instructions burned: 77 (million)
% 6.76/1.73 % (2313231)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=3985695202:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 6.76/1.73 % (2313206)Refutation found. Thanks to Tanya!
% 6.76/1.73 % SZS status Theorem for theBenchmark
% 6.76/1.73 % SZS output start Proof for theBenchmark
% See solution above
% 6.76/1.73 % (2313206)------------------------------
% 6.76/1.73 % (2313206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.73 % (2313206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.73 % (2313206)CaDiCaL version: 2.1.3
% 6.76/1.73 % (2313206)Termination reason: Refutation
% 6.76/1.73 % (2313206)Time elapsed: 0.053 s
% 6.76/1.73 % (2313206)Peak memory usage: 118 MB
% 6.76/1.73 % (2313206)Instructions burned: 35 (million)
% 6.76/1.73 % (2313206)------------------------------
% 6.76/1.73 % (2313206)------------------------------
% 6.76/1.73 % (2313164)Success in time 0.87 s
% 6.76/1.73 % Vampire exiting
%------------------------------------------------------------------------------