%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW624_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:58 PM UTC 2026
% Result : Theorem 26.01s 4.62s
% Output : Refutation 28.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of formulae : 67 ( 17 unt; 0 typ; 8 def)
% Number of atoms : 131 ( 19 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 110 ( 46 ~; 43 |; 6 &)
% ( 8 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 122 ( 24 atm; 30 fun; 56 num; 12 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 13 usr; 9 prp; 0-3 aty)
% Number of functors : 51 ( 45 usr; 14 con; 0-5 aty)
% Number of variables : 96 ( 92 !; 4 ?; 96 :)
% 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(type_def_9,type,
elt: $tType ).
tff(type_def_10,type,
list_elt: $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,
list: ty > ty ).
tff(func_def_13,type,
nil: ty > uni ).
tff(func_def_14,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_18,type,
length: ( ty * uni ) > $int ).
tff(func_def_21,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_22,type,
num_occ: ( ty * uni * uni ) > $int ).
tff(func_def_23,type,
reverse: ( ty * uni ) > uni ).
tff(func_def_24,type,
elt1: ty ).
tff(func_def_25,type,
t2tb: list_elt > uni ).
tff(func_def_26,type,
tb2t: uni > list_elt ).
tff(func_def_27,type,
t2tb1: elt > uni ).
tff(func_def_28,type,
tb2t1: uni > elt ).
tff(func_def_29,type,
rev_append: ( ty * uni * uni ) > uni ).
tff(func_def_30,type,
prefix: ( ty * $int * uni ) > uni ).
tff(func_def_32,type,
abs: $int > $int ).
tff(func_def_34,type,
div: ( $int * $int ) > $int ).
tff(func_def_35,type,
mod: ( $int * $int ) > $int ).
tff(func_def_36,type,
sK0: ( list_elt * list_elt ) > elt ).
tff(func_def_37,type,
sK1: ( list_elt * list_elt ) > elt ).
tff(func_def_38,type,
sK2: ( elt * list_elt ) > elt ).
tff(func_def_39,type,
sK3: list_elt > elt ).
tff(func_def_40,type,
sK4: list_elt > list_elt ).
tff(func_def_41,type,
sK5: list_elt > elt ).
tff(func_def_42,type,
sK6: list_elt > elt ).
tff(func_def_43,type,
sK7: ( uni * uni * ty ) > uni ).
tff(func_def_44,type,
sK8: ( list_elt * list_elt ) > elt ).
tff(func_def_45,type,
sK9: ( list_elt * list_elt ) > elt ).
tff(func_def_46,type,
sK10: ( ty * uni * uni ) > uni ).
tff(func_def_47,type,
sK11: ( ty * uni * uni ) > uni ).
tff(func_def_48,type,
sK12: ( list_elt * elt ) > elt ).
tff(func_def_49,type,
sK13: list_elt ).
tff(func_def_50,type,
sK14: elt ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
permut: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
le: ( elt * elt ) > $o ).
tff(pred_def_7,type,
sorted: list_elt > $o ).
tff(f20,axiom,
! [X0: ty] :
( ! [X1: uni,X2: uni] : ( length(X0,cons(X0,X1,X2)) = $sum(1,length(X0,X2)) )
& ( length(X0,nil(X0)) = 0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def) ).
tff(f21,axiom,
! [X1: uni,X0: ty] : $lesseq(0,length(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_nonnegative) ).
tff(f43,axiom,
! [X1: uni,X0: ty] : permut(X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_refl) ).
tff(f46,axiom,
! [X1: uni,X0: ty,X2: uni,X3: uni] :
( permut(X0,X2,X3)
=> permut(X0,cons(X0,X1,X2),cons(X0,X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_cons) ).
tff(f80,axiom,
! [X1: uni,X0: ty] : ( prefix(X0,0,X1) = nil(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prefix_def1) ).
tff(f81,negated_conjecture,
! [X3: uni,X2: uni,X1: $int,X0: ty] :
( $less(0,X1)
=> ( prefix(X0,X1,cons(X0,X2,X3)) = cons(X0,X2,prefix(X0,$difference(X1,1),X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prefix_def2) ).
tff(f101,conjecture,
( ! [X1: list_elt,X0: elt] :
( permut(elt1,prefix(elt1,length(elt1,t2tb(X1)),t2tb(X1)),t2tb(X1))
=> permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(X0),t2tb(X1))),cons(elt1,t2tb1(X0),t2tb(X1))),cons(elt1,t2tb1(X0),t2tb(X1))) )
& permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_prefix) ).
tff(f102,negated_conjecture,
~ ( ! [X1: list_elt,X0: elt] :
( permut(elt1,prefix(elt1,length(elt1,t2tb(X1)),t2tb(X1)),t2tb(X1))
=> permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(X0),t2tb(X1))),cons(elt1,t2tb1(X0),t2tb(X1))),cons(elt1,t2tb1(X0),t2tb(X1))) )
& permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1)) ),
inference(negated_conjecture,[status(cth)],[f101]) ).
tff(f105,plain,
! [X3: uni,X2: uni,X1: $int,X0: ty] :
( $less(0,X1)
=> ( prefix(X0,X1,cons(X0,X2,X3)) = cons(X0,X2,prefix(X0,$sum(X1,$uminus(1)),X3)) ) ),
inference(theory_normalization,[],[f81]) ).
tff(f111,plain,
! [X1: uni,X0: ty] : ~ $less(length(X0,X1),0),
inference(theory_normalization,[],[f21]) ).
tff(f121,plain,
! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f128,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( X0 = X1 )
| $less(X0,X1) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f142,plain,
! [X2: $int,X0: uni,X3: ty,X1: uni] :
( $less(0,X2)
=> ( cons(X3,X1,prefix(X3,$sum(X2,$uminus(1)),X0)) = prefix(X3,X2,cons(X3,X1,X0)) ) ),
inference(rectify,[],[f105]) ).
tff(f147,plain,
! [X0: uni,X1: ty] : ( prefix(X1,0,X0) = nil(X1) ),
inference(rectify,[],[f80]) ).
tff(f152,plain,
! [X1: ty,X0: uni] : ~ $less(length(X1,X0),0),
inference(rectify,[],[f111]) ).
tff(f156,plain,
! [X1: ty,X0: uni] : permut(X1,X0,X0),
inference(rectify,[],[f43]) ).
tff(f178,plain,
! [X3: uni,X1: ty,X2: uni,X0: uni] :
( permut(X1,X2,X3)
=> permut(X1,cons(X1,X0,X2),cons(X1,X0,X3)) ),
inference(rectify,[],[f46]) ).
tff(f230,plain,
! [X3: ty,X0: uni,X2: $int,X1: uni] :
( ~ $less(0,X2)
| ( cons(X3,X1,prefix(X3,$sum(X2,$uminus(1)),X0)) = prefix(X3,X2,cons(X3,X1,X0)) ) ),
inference(ennf_transformation,[],[f142]) ).
tff(f251,plain,
! [X1: ty,X3: uni,X2: uni,X0: uni] :
( ~ permut(X1,X2,X3)
| permut(X1,cons(X1,X0,X2),cons(X1,X0,X3)) ),
inference(ennf_transformation,[],[f178]) ).
tff(f261,plain,
( ~ permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1))
| ? [X1: list_elt,X0: elt] :
( ~ permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(X0),t2tb(X1))),cons(elt1,t2tb1(X0),t2tb(X1))),cons(elt1,t2tb1(X0),t2tb(X1)))
& permut(elt1,prefix(elt1,length(elt1,t2tb(X1)),t2tb(X1)),t2tb(X1)) ) ),
inference(ennf_transformation,[],[f102]) ).
tff(f268,plain,
! [X0: ty,X1: uni,X2: $int,X3: uni] :
( ~ $less(0,X2)
| ( cons(X0,X3,prefix(X0,$sum(X2,$uminus(1)),X1)) = prefix(X0,X2,cons(X0,X3,X1)) ) ),
inference(rectify,[],[f230]) ).
tff(f283,plain,
! [X0: ty,X1: uni] : ~ $less(length(X0,X1),0),
inference(rectify,[],[f152]) ).
tff(f296,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( ~ permut(X0,X2,X1)
| permut(X0,cons(X0,X3,X2),cons(X0,X3,X1)) ),
inference(rectify,[],[f251]) ).
tff(f324,plain,
! [X0: ty,X1: uni] : permut(X0,X1,X1),
inference(rectify,[],[f156]) ).
tff(f346,plain,
( ~ permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1))
| ? [X0: list_elt,X1: elt] :
( ~ permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(X1),t2tb(X0))),cons(elt1,t2tb1(X1),t2tb(X0))),cons(elt1,t2tb1(X1),t2tb(X0)))
& permut(elt1,prefix(elt1,length(elt1,t2tb(X0)),t2tb(X0)),t2tb(X0)) ) ),
inference(rectify,[],[f261]) ).
tff(f347,plain,
( ~ permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1))
| ( ~ permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13)))
& permut(elt1,prefix(elt1,length(elt1,t2tb(sK13)),t2tb(sK13)),t2tb(sK13)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X0,sK13),skolemize(X1,sK14)],[f346]) ).
tff(f361,plain,
! [X2: $int,X3: uni,X0: ty,X1: uni] :
( ~ $less(0,X2)
| ( cons(X0,X3,prefix(X0,$sum(X2,$uminus(1)),X1)) = prefix(X0,X2,cons(X0,X3,X1)) ) ),
inference(cnf_transformation,[],[f268]) ).
tff(f387,plain,
! [X0: ty,X1: uni] : ~ $less(length(X0,X1),0),
inference(cnf_transformation,[],[f283]) ).
tff(f396,plain,
! [X0: ty] : ( 0 = length(X0,nil(X0)) ),
inference(cnf_transformation,[],[f20]) ).
tff(f397,plain,
! [X2: uni,X0: ty,X1: uni] : ( length(X0,cons(X0,X1,X2)) = $sum(1,length(X0,X2)) ),
inference(cnf_transformation,[],[f20]) ).
tff(f407,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( permut(X0,cons(X0,X3,X2),cons(X0,X3,X1))
| ~ permut(X0,X2,X1) ),
inference(cnf_transformation,[],[f296]) ).
tff(f446,plain,
! [X0: ty,X1: uni] : permut(X0,X1,X1),
inference(cnf_transformation,[],[f324]) ).
tff(f468,plain,
! [X0: uni,X1: ty] : ( prefix(X1,0,X0) = nil(X1) ),
inference(cnf_transformation,[],[f147]) ).
tff(f482,plain,
( permut(elt1,prefix(elt1,length(elt1,t2tb(sK13)),t2tb(sK13)),t2tb(sK13))
| ~ permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1)) ),
inference(cnf_transformation,[],[f347]) ).
tff(f483,plain,
( ~ permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13)))
| ~ permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1)) ),
inference(cnf_transformation,[],[f347]) ).
tff(f502,plain,
! [X2: $int,X3: uni,X0: ty,X1: uni] :
( ( cons(X0,X3,prefix(X0,$sum(X2,-1),X1)) = prefix(X0,X2,cons(X0,X3,X1)) )
| ~ $less(0,X2) ),
inference(evaluation,[],[f361]) ).
tff(f507,definition,
( spl15_1
<=> permut(elt1,prefix(elt1,length(elt1,t2tb(sK13)),t2tb(sK13)),t2tb(sK13)) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
tff(f511,definition,
( spl15_2
<=> permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1)) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
tff(f513,plain,
( ~ permut(elt1,prefix(elt1,length(elt1,nil(elt1)),nil(elt1)),nil(elt1))
| spl15_2 ),
inference(avatar_component_clause,[],[f511]) ).
tff(f514,plain,
( spl15_1
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f482,f511,f507]) ).
tff(f521,definition,
( spl15_4
<=> permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13))) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
tff(f523,plain,
( ~ permut(elt1,prefix(elt1,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13))),cons(elt1,t2tb1(sK14),t2tb(sK13)))
| spl15_4 ),
inference(avatar_component_clause,[],[f521]) ).
tff(f524,plain,
( ~ spl15_4
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f483,f511,f521]) ).
tff(f540,plain,
( ~ permut(elt1,prefix(elt1,0,nil(elt1)),nil(elt1))
| spl15_2 ),
inference(superposition,[],[f513,f396]) ).
tff(f543,definition,
( spl15_6
<=> permut(elt1,prefix(elt1,0,nil(elt1)),nil(elt1)) ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
tff(f545,plain,
( ~ permut(elt1,prefix(elt1,0,nil(elt1)),nil(elt1))
| spl15_6 ),
inference(avatar_component_clause,[],[f543]) ).
tff(f546,plain,
( ~ spl15_6
| spl15_2 ),
inference(avatar_split_clause,[],[f540,f511,f543]) ).
tff(f639,plain,
( ~ permut(elt1,nil(elt1),nil(elt1))
| spl15_6 ),
inference(superposition,[],[f545,f468]) ).
tff(f647,plain,
( $false
| spl15_6 ),
inference(forward_subsumption_resolution,[],[f639,f446]) ).
tff(f648,plain,
spl15_6,
inference(avatar_contradiction_clause,[],[f647]) ).
tff(f1713,plain,
! [X2: uni,X3: uni,X0: ty,X1: $int,X4: uni] :
( permut(X0,prefix(X0,X1,cons(X0,X2,X3)),cons(X0,X2,X4))
| ~ permut(X0,prefix(X0,$sum(X1,-1),X3),X4)
| ~ $less(0,X1) ),
inference(superposition,[],[f407,f502]) ).
tff(f1856,definition,
( spl15_14
<=> $less(0,length(elt1,t2tb(sK13))) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
tff(f1858,plain,
( ~ $less(0,length(elt1,t2tb(sK13)))
| spl15_14 ),
inference(avatar_component_clause,[],[f1856]) ).
tff(f1891,plain,
( ( 0 = length(elt1,t2tb(sK13)) )
| $less(length(elt1,t2tb(sK13)),0)
| spl15_14 ),
inference(resolution,[],[f1858,f128]) ).
tff(f1894,plain,
( ( 0 = length(elt1,t2tb(sK13)) )
| spl15_14 ),
inference(forward_subsumption_resolution,[],[f1891,f387]) ).
tff(f1896,definition,
( spl15_17
<=> ( 0 = length(elt1,t2tb(sK13)) ) ),
introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition]) ).
tff(f1899,plain,
( spl15_17
| spl15_14 ),
inference(avatar_split_clause,[],[f1894,f1856,f1896]) ).
tff(f2075,definition,
( spl15_21
<=> $less(0,$sum(1,length(elt1,t2tb(sK13)))) ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
tff(f2077,plain,
( $less(0,$sum(1,length(elt1,t2tb(sK13))))
| ~ spl15_21 ),
inference(avatar_component_clause,[],[f2075]) ).
tff(f3009,plain,
( ~ permut(elt1,prefix(elt1,$sum(length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))),-1),t2tb(sK13)),t2tb(sK13))
| ~ $less(0,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))))
| spl15_4 ),
inference(resolution,[],[f1713,f523]) ).
tff(f3036,plain,
( ~ permut(elt1,prefix(elt1,$sum(-1,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13)))),t2tb(sK13)),t2tb(sK13))
| ~ $less(0,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))))
| spl15_4 ),
inference(forward_demodulation,[],[f3009,f121]) ).
tff(f3041,plain,
( ~ permut(elt1,prefix(elt1,$sum(-1,$sum(1,length(elt1,t2tb(sK13)))),t2tb(sK13)),t2tb(sK13))
| ~ $less(0,length(elt1,cons(elt1,t2tb1(sK14),t2tb(sK13))))
| spl15_4 ),
inference(forward_demodulation,[],[f3036,f397]) ).
tff(f3043,plain,
( ~ permut(elt1,prefix(elt1,$sum(-1,$sum(1,length(elt1,t2tb(sK13)))),t2tb(sK13)),t2tb(sK13))
| ~ $less(0,$sum(1,length(elt1,t2tb(sK13))))
| spl15_4 ),
inference(forward_demodulation,[],[f3041,f397]) ).
tff(f3045,definition,
( spl15_41
<=> permut(elt1,prefix(elt1,$sum(-1,$sum(1,length(elt1,t2tb(sK13)))),t2tb(sK13)),t2tb(sK13)) ),
introduced(definition,[new_symbols(definition,[spl15_41])],[avatar_definition]) ).
tff(f3049,plain,
( ~ permut(elt1,prefix(elt1,$sum(-1,$sum(1,length(elt1,t2tb(sK13)))),t2tb(sK13)),t2tb(sK13))
| spl15_4
| ~ spl15_21 ),
inference(forward_subsumption_resolution,[],[f3043,f2077]) ).
tff(f3050,plain,
( ~ spl15_41
| spl15_4
| ~ spl15_21 ),
inference(avatar_split_clause,[],[f3049,f2075,f521,f3045]) ).
tff(f3051,plain,
$false,
inference(avatar_smt_refutation,[],[f3050,f1899,f648,f546,f524,f514]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW624_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.27 % Computer : n018.cluster.edu
% 0.23/0.27 % Model : x86_64 x86_64
% 0.23/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.27 % Memory : 8046.5625MB
% 0.23/0.27 % OS : Linux 6.8.0-71-generic
% 0.23/0.27 % CPULimit : 300
% 0.23/0.27 % WCLimit : 300
% 0.23/0.27 % DateTime : Mon Sep 28 14:25:10 UTC 2026
% 0.23/0.28 % CPUTime :
% 0.23/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.32 Running first-order theorem proving
% 0.23/0.32 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
% 5.42/1.61 % (3420545)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.42/1.61 % (3420554)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=383490427:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.42/1.61 % (3420553)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=803571230:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.42/1.61 % (3420558)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1005665456:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.42/1.61 % (3420557)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1943916177:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.42/1.61 % (3420556)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2853559624:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.42/1.61 % (3420555)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=4218302440:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.42/1.61 % (3420552)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3602814465:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.42/1.61 % (3420556)Instruction limit reached!
% 5.42/1.61 % (3420556)------------------------------
% 5.42/1.61 % (3420556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.61 % (3420556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.61 % (3420556)CaDiCaL version: 2.1.3
% 5.42/1.61 % (3420556)Termination reason: Instruction limit
% 5.42/1.61 % (3420556)Termination phase: Preprocessing 3
% 5.42/1.61 % (3420556)Time elapsed: 0.005 s
% 5.42/1.61 % (3420556)Peak memory usage: 86 MB
% 5.42/1.61 % (3420556)Instructions burned: 4 (million)
% 5.42/1.61 % (3420555)Instruction limit reached!
% 5.42/1.61 % (3420555)------------------------------
% 5.42/1.61 % (3420555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.61 % (3420555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.61 % (3420555)CaDiCaL version: 2.1.3
% 5.42/1.61 % (3420555)Termination reason: Instruction limit
% 5.42/1.61 % (3420555)Termination phase: Property scanning
% 5.42/1.61 % (3420555)Time elapsed: 0.008 s
% 5.42/1.61 % (3420555)Peak memory usage: 86 MB
% 5.42/1.61 % (3420555)Instructions burned: 7 (million)
% 5.42/1.61 % (3420552)Instruction limit reached!
% 5.42/1.61 % (3420552)------------------------------
% 5.42/1.61 % (3420552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.61 % (3420552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.61 % (3420552)CaDiCaL version: 2.1.3
% 5.42/1.61 % (3420552)Termination reason: Instruction limit
% 5.42/1.61 % (3420552)Termination phase: Saturation
% 5.42/1.61 % (3420552)Time elapsed: 0.040 s
% 5.42/1.61 % (3420552)Peak memory usage: 112 MB
% 5.42/1.61 % (3420552)Instructions burned: 12 (million)
% 5.42/1.61 % (3420558)Instruction limit reached!
% 5.42/1.61 % (3420558)------------------------------
% 5.42/1.61 % (3420558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.61 % (3420558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.61 % (3420558)CaDiCaL version: 2.1.3
% 5.42/1.61 % (3420558)Termination reason: Instruction limit
% 5.42/1.61 % (3420558)Termination phase: Saturation
% 5.42/1.61 % (3420558)Time elapsed: 0.065 s
% 5.42/1.61 % (3420558)Peak memory usage: 116 MB
% 5.42/1.61 % (3420558)Instructions burned: 33 (million)
% 5.42/1.61 % (3420557)Instruction limit reached!
% 5.42/1.61 % (3420557)------------------------------
% 5.42/1.61 % (3420557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.61 % (3420557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.61 % (3420557)CaDiCaL version: 2.1.3
% 5.42/1.61 % (3420557)Termination reason: Instruction limit
% 5.42/1.61 % (3420557)Termination phase: Saturation
% 5.42/1.61 % (3420557)Time elapsed: 0.081 s
% 5.42/1.61 % (3420557)Peak memory usage: 116 MB
% 5.42/1.61 % (3420557)Instructions burned: 46 (million)
% 5.42/1.61 % (3420554)Instruction limit reached!
% 5.42/1.61 % (3420554)------------------------------
% 5.42/1.61 % (3420554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.61 % (3420554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.87 % (3420554)CaDiCaL version: 2.1.3
% 7.01/1.87 % (3420554)Termination reason: Instruction limit
% 7.01/1.87 % (3420554)Termination phase: Saturation
% 7.01/1.87 % (3420554)Time elapsed: 0.179 s
% 7.01/1.87 % (3420554)Peak memory usage: 118 MB
% 7.01/1.87 % (3420554)Instructions burned: 201 (million)
% 7.01/1.87 % (3420566)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3615372028:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 7.01/1.87 % (3420567)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=2487904922:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 7.01/1.87 % (3420566)Instruction limit reached!
% 7.01/1.87 % (3420566)------------------------------
% 7.01/1.87 % (3420566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.01/1.87 % (3420566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.87 % (3420566)CaDiCaL version: 2.1.3
% 7.01/1.87 % (3420566)Termination reason: Instruction limit
% 7.01/1.87 % (3420566)Termination phase: Saturation
% 7.01/1.87 % (3420566)Time elapsed: 0.016 s
% 7.01/1.87 % (3420566)Peak memory usage: 88 MB
% 7.01/1.87 % (3420566)Instructions burned: 14 (million)
% 7.01/1.87 % (3420571)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3207801369:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 7.01/1.87 % (3420569)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1415895260:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 7.01/1.87 % (3420568)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1561400173:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 7.01/1.87 % (3420567)Instruction limit reached!
% 7.01/1.87 % (3420567)------------------------------
% 7.01/1.87 % (3420567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.01/1.87 % (3420567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.87 % (3420567)CaDiCaL version: 2.1.3
% 7.01/1.87 % (3420567)Termination reason: Instruction limit
% 7.01/1.87 % (3420567)Termination phase: Saturation
% 7.01/1.87 % (3420567)Time elapsed: 0.036 s
% 7.01/1.87 % (3420567)Peak memory usage: 89 MB
% 7.01/1.87 % (3420567)Instructions burned: 29 (million)
% 7.01/1.87 % (3420568)Instruction limit reached!
% 7.01/1.87 % (3420568)------------------------------
% 7.01/1.87 % (3420568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.01/1.87 % (3420568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.87 % (3420568)CaDiCaL version: 2.1.3
% 7.01/1.87 % (3420568)Termination reason: Instruction limit
% 7.01/1.87 % (3420568)Termination phase: Saturation
% 7.01/1.87 % (3420568)Time elapsed: 0.017 s
% 7.01/1.87 % (3420568)Peak memory usage: 89 MB
% 7.01/1.87 % (3420568)Instructions burned: 16 (million)
% 7.01/1.87 % (3420569)Instruction limit reached!
% 7.01/1.87 % (3420569)------------------------------
% 7.01/1.87 % (3420569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.01/1.87 % (3420569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.87 % (3420569)CaDiCaL version: 2.1.3
% 7.01/1.87 % (3420569)Termination reason: Instruction limit
% 7.01/1.87 % (3420569)Termination phase: Saturation
% 7.01/1.87 % (3420569)Time elapsed: 0.028 s
% 7.01/1.87 % (3420569)Peak memory usage: 89 MB
% 7.01/1.87 % (3420569)Instructions burned: 24 (million)
% 7.01/1.87 % (3420571)Instruction limit reached!
% 7.01/1.87 % (3420571)------------------------------
% 7.01/1.87 % (3420571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.01/1.87 % (3420571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.87 % (3420571)CaDiCaL version: 2.1.3
% 7.01/1.87 % (3420571)Termination reason: Instruction limit
% 7.01/1.87 % (3420571)Termination phase: Saturation
% 7.01/1.87 % (3420571)Time elapsed: 0.042 s
% 7.01/1.87 % (3420571)Peak memory usage: 89 MB
% 7.01/1.87 % (3420571)Instructions burned: 87 (million)
% 7.01/1.87 % (3420570)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=1333187983:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.01/1.87 % (3420553)Instruction limit reached!
% 7.01/1.87 % (3420553)------------------------------
% 7.01/1.87 % (3420553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.18 % (3420553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.18 % (3420553)CaDiCaL version: 2.1.3
% 10.42/2.18 % (3420553)Termination reason: Instruction limit
% 10.42/2.18 % (3420553)Termination phase: Saturation
% 10.42/2.18 % (3420553)Time elapsed: 0.363 s
% 10.42/2.18 % (3420553)Peak memory usage: 117 MB
% 10.42/2.18 % (3420553)Instructions burned: 307 (million)
% 10.42/2.18 % (3420570)Instruction limit reached!
% 10.42/2.18 % (3420570)------------------------------
% 10.42/2.18 % (3420570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.18 % (3420570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.18 % (3420570)CaDiCaL version: 2.1.3
% 10.42/2.18 % (3420570)Termination reason: Instruction limit
% 10.42/2.18 % (3420570)Termination phase: Saturation
% 10.42/2.18 % (3420570)Time elapsed: 0.031 s
% 10.42/2.18 % (3420570)Peak memory usage: 90 MB
% 10.42/2.18 % (3420570)Instructions burned: 27 (million)
% 10.42/2.18 % (3420574)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=182500707:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 10.42/2.18 % (3420574)Instruction limit reached!
% 10.42/2.18 % (3420574)------------------------------
% 10.42/2.18 % (3420574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.18 % (3420574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.18 % (3420574)CaDiCaL version: 2.1.3
% 10.42/2.18 % (3420574)Termination reason: Instruction limit
% 10.42/2.18 % (3420574)Termination phase: Property scanning
% 10.42/2.18 % (3420574)Time elapsed: 0.002 s
% 10.42/2.18 % (3420574)Peak memory usage: 85 MB
% 10.42/2.18 % (3420574)Instructions burned: 2 (million)
% 10.42/2.18 % (3420581)lrs+10_1_thi=all:si=on:fd=off:random_seed=3709964676:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 10.42/2.18 % (3420578)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3667262614:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 10.42/2.18 % (3420581)Instruction limit reached!
% 10.42/2.18 % (3420581)------------------------------
% 10.42/2.18 % (3420581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.18 % (3420581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.18 % (3420581)CaDiCaL version: 2.1.3
% 10.42/2.18 % (3420581)Termination reason: Instruction limit
% 10.42/2.18 % (3420581)Termination phase: Saturation
% 10.42/2.18 % (3420581)Time elapsed: 0.053 s
% 10.42/2.18 % (3420581)Peak memory usage: 116 MB
% 10.42/2.18 % (3420581)Instructions burned: 53 (million)
% 10.42/2.18 % (3420579)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4255341496:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 10.42/2.18 % (3420580)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3779861471:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 10.42/2.18 % (3420579)Instruction limit reached!
% 10.42/2.18 % (3420579)------------------------------
% 10.42/2.18 % (3420579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.18 % (3420579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.18 % (3420579)CaDiCaL version: 2.1.3
% 10.42/2.18 % (3420579)Termination reason: Instruction limit
% 10.42/2.18 % (3420579)Termination phase: Preprocessing 3
% 10.42/2.18 % (3420579)Time elapsed: 0.004 s
% 10.42/2.18 % (3420579)Peak memory usage: 85 MB
% 10.42/2.18 % (3420579)Instructions burned: 4 (million)
% 10.42/2.18 % (3420583)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=2641713565:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 10.42/2.18 % (3420583)Instruction limit reached!
% 10.42/2.18 % (3420583)------------------------------
% 10.42/2.18 % (3420583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.18 % (3420583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.18 % (3420583)CaDiCaL version: 2.1.3
% 10.42/2.18 % (3420583)Termination reason: Instruction limit
% 10.42/2.18 % (3420583)Termination phase: Function definition elimination
% 10.42/2.18 % (3420583)Time elapsed: 0.008 s
% 10.42/2.18 % (3420583)Peak memory usage: 86 MB
% 10.42/2.18 % (3420583)Instructions burned: 8 (million)
% 11.59/2.54 % (3420584)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1274359945:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 11.59/2.54 % (3420584)Instruction limit reached!
% 11.59/2.54 % (3420584)------------------------------
% 11.59/2.54 % (3420584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.54 % (3420584)CaDiCaL version: 2.1.3
% 11.59/2.54 % (3420584)Termination reason: Instruction limit
% 11.59/2.54 % (3420584)Termination phase: Preprocessing 1
% 11.59/2.54 % (3420584)Time elapsed: 0.003 s
% 11.59/2.54 % (3420584)Peak memory usage: 85 MB
% 11.59/2.54 % (3420584)Instructions burned: 2 (million)
% 11.59/2.54 % (3420578)Instruction limit reached!
% 11.59/2.54 % (3420578)------------------------------
% 11.59/2.54 % (3420578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.54 % (3420578)CaDiCaL version: 2.1.3
% 11.59/2.54 % (3420578)Termination reason: Instruction limit
% 11.59/2.54 % (3420578)Termination phase: Saturation
% 11.59/2.54 % (3420578)Time elapsed: 0.186 s
% 11.59/2.54 % (3420578)Peak memory usage: 90 MB
% 11.59/2.54 % (3420578)Instructions burned: 181 (million)
% 11.59/2.54 % (3420580)Instruction limit reached!
% 11.59/2.54 % (3420580)------------------------------
% 11.59/2.54 % (3420580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.54 % (3420580)CaDiCaL version: 2.1.3
% 11.59/2.54 % (3420580)Termination reason: Instruction limit
% 11.59/2.54 % (3420580)Termination phase: Saturation
% 11.59/2.54 % (3420580)Time elapsed: 0.140 s
% 11.59/2.54 % (3420580)Peak memory usage: 134 MB
% 11.59/2.54 % (3420580)Instructions burned: 66 (million)
% 11.59/2.54 % (3420586)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1060878985:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.59/2.54 % (3420586)Instruction limit reached!
% 11.59/2.54 % (3420586)------------------------------
% 11.59/2.54 % (3420586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.54 % (3420586)CaDiCaL version: 2.1.3
% 11.59/2.54 % (3420586)Termination reason: Instruction limit
% 11.59/2.54 % (3420586)Termination phase: Preprocessing 1
% 11.59/2.54 % (3420586)Time elapsed: 0.003 s
% 11.59/2.54 % (3420586)Peak memory usage: 85 MB
% 11.59/2.54 % (3420586)Instructions burned: 3 (million)
% 11.59/2.54 % (3420591)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1668540226:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi)
% 11.59/2.54 % (3420592)dis+10_1_si=on:random_seed=2244931760:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.59/2.54 % (3420592)Instruction limit reached!
% 11.59/2.54 % (3420592)------------------------------
% 11.59/2.54 % (3420592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.54 % (3420592)CaDiCaL version: 2.1.3
% 11.59/2.54 % (3420592)Termination reason: Instruction limit
% 11.59/2.54 % (3420592)Termination phase: Saturation
% 11.59/2.54 % (3420592)Time elapsed: 0.011 s
% 11.59/2.54 % (3420592)Peak memory usage: 87 MB
% 11.59/2.54 % (3420592)Instructions burned: 10 (million)
% 11.59/2.54 % (3420591)Instruction limit reached!
% 11.59/2.54 % (3420591)------------------------------
% 11.59/2.54 % (3420591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.54 % (3420591)CaDiCaL version: 2.1.3
% 11.59/2.54 % (3420591)Termination reason: Instruction limit
% 11.59/2.54 % (3420591)Termination phase: Saturation
% 11.59/2.54 % (3420591)Time elapsed: 0.092 s
% 11.59/2.54 % (3420591)Peak memory usage: 117 MB
% 11.59/2.54 % (3420591)Instructions burned: 129 (million)
% 11.59/2.54 % (3420594)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=954377788:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.59/2.54 % (3420594)Refutation not found, incomplete strategy
% 11.59/2.54 % (3420594)------------------------------
% 11.59/2.54 % (3420594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.59/2.54 % (3420594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.96 % (3420594)CaDiCaL version: 2.1.3
% 14.19/2.96 % (3420594)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.96 % (3420594)Time elapsed: 0.016 s
% 14.19/2.96 % (3420594)Peak memory usage: 89 MB
% 14.19/2.96 % (3420594)Instructions burned: 15 (million)
% 14.19/2.96 % (3420596)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=71255003: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_2990 on theBenchmark for (2990ds/35Mi)
% 14.19/2.96 % (3420600)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2369136941:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 14.19/2.96 % (3420597)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=276006572:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 14.19/2.96 % (3420598)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2860427039:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 14.19/2.96 % (3420597)Instruction limit reached!
% 14.19/2.96 % (3420597)------------------------------
% 14.19/2.96 % (3420597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.96 % (3420597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.96 % (3420597)CaDiCaL version: 2.1.3
% 14.19/2.96 % (3420597)Termination reason: Instruction limit
% 14.19/2.96 % (3420597)Termination phase: Preprocessing 1
% 14.19/2.96 % (3420597)Time elapsed: 0.003 s
% 14.19/2.96 % (3420597)Peak memory usage: 85 MB
% 14.19/2.96 % (3420597)Instructions burned: 3 (million)
% 14.19/2.96 % (3420596)Instruction limit reached!
% 14.19/2.96 % (3420596)------------------------------
% 14.19/2.96 % (3420596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.96 % (3420596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.96 % (3420596)CaDiCaL version: 2.1.3
% 14.19/2.96 % (3420596)Termination reason: Instruction limit
% 14.19/2.96 % (3420596)Termination phase: Saturation
% 14.19/2.96 % (3420596)Time elapsed: 0.044 s
% 14.19/2.96 % (3420596)Peak memory usage: 89 MB
% 14.19/2.96 % (3420596)Instructions burned: 35 (million)
% 14.19/2.96 % (3420598)Instruction limit reached!
% 14.19/2.96 % (3420598)------------------------------
% 14.19/2.96 % (3420598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.96 % (3420598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.96 % (3420598)CaDiCaL version: 2.1.3
% 14.19/2.96 % (3420598)Termination reason: Instruction limit
% 14.19/2.96 % (3420598)Termination phase: Saturation
% 14.19/2.96 % (3420598)Time elapsed: 0.010 s
% 14.19/2.96 % (3420598)Peak memory usage: 88 MB
% 14.19/2.96 % (3420598)Instructions burned: 9 (million)
% 14.19/2.96 % (3420604)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1834579982:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 14.19/2.96 % (3420603)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2912962768:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 14.19/2.96 % (3420603)Instruction limit reached!
% 14.19/2.96 % (3420603)------------------------------
% 14.19/2.96 % (3420603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.96 % (3420603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.96 % (3420603)CaDiCaL version: 2.1.3
% 14.19/2.96 % (3420603)Termination reason: Instruction limit
% 14.19/2.96 % (3420603)Termination phase: Saturation
% 14.19/2.96 % (3420603)Time elapsed: 0.034 s
% 14.19/2.96 % (3420603)Peak memory usage: 101 MB
% 14.19/2.96 % (3420603)Instructions burned: 13 (million)
% 14.19/2.96 % (3420604)Instruction limit reached!
% 14.19/2.96 % (3420604)------------------------------
% 14.19/2.96 % (3420604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.96 % (3420604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.96 % (3420604)CaDiCaL version: 2.1.3
% 14.19/2.96 % (3420604)Termination reason: Instruction limit
% 14.19/2.96 % (3420604)Termination phase: Saturation
% 14.19/2.96 % (3420604)Time elapsed: 0.137 s
% 14.19/2.96 % (3420604)Peak memory usage: 117 MB
% 14.19/2.96 % (3420604)Instructions burned: 228 (million)
% 14.19/2.96 % (3420612)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=1775843125:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 17.84/3.34 % (3420610)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3903174981:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 17.84/3.34 % (3420610)Instruction limit reached!
% 17.84/3.34 % (3420610)------------------------------
% 17.84/3.34 % (3420610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.34 % (3420610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.34 % (3420610)CaDiCaL version: 2.1.3
% 17.84/3.34 % (3420610)Termination reason: Instruction limit
% 17.84/3.34 % (3420610)Termination phase: Saturation
% 17.84/3.34 % (3420610)Time elapsed: 0.011 s
% 17.84/3.34 % (3420610)Peak memory usage: 88 MB
% 17.84/3.34 % (3420610)Instructions burned: 10 (million)
% 17.84/3.34 % (3420611)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=891413346:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 17.84/3.34 % (3420594)------------------------------
% 17.84/3.34 % (3420594)------------------------------
% 17.84/3.34 % (3420612)Instruction limit reached!
% 17.84/3.34 % (3420612)------------------------------
% 17.84/3.34 % (3420612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.34 % (3420612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.34 % (3420612)CaDiCaL version: 2.1.3
% 17.84/3.34 % (3420612)Termination reason: Instruction limit
% 17.84/3.34 % (3420612)Termination phase: Saturation
% 17.84/3.34 % (3420612)Time elapsed: 0.084 s
% 17.84/3.34 % (3420612)Peak memory usage: 90 MB
% 17.84/3.34 % (3420612)Instructions burned: 75 (million)
% 17.84/3.34 % (3420615)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=568832063:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi)
% 17.84/3.34 % (3420600)Instruction limit reached!
% 17.84/3.34 % (3420600)------------------------------
% 17.84/3.34 % (3420600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.34 % (3420600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.34 % (3420600)CaDiCaL version: 2.1.3
% 17.84/3.34 % (3420600)Termination reason: Instruction limit
% 17.84/3.34 % (3420600)Termination phase: Saturation
% 17.84/3.34 % (3420600)Time elapsed: 0.385 s
% 17.84/3.34 % (3420600)Peak memory usage: 92 MB
% 17.84/3.34 % (3420600)Instructions burned: 370 (million)
% 17.84/3.34 % (3420611)Instruction limit reached!
% 17.84/3.34 % (3420611)------------------------------
% 17.84/3.34 % (3420611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.34 % (3420611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.34 % (3420611)CaDiCaL version: 2.1.3
% 17.84/3.34 % (3420611)Termination reason: Instruction limit
% 17.84/3.34 % (3420611)Termination phase: Saturation
% 17.84/3.34 % (3420611)Time elapsed: 0.139 s
% 17.84/3.34 % (3420611)Peak memory usage: 134 MB
% 17.84/3.34 % (3420611)Instructions burned: 71 (million)
% 17.84/3.34 % (3420616)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2988576133:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi)
% 17.84/3.34 % (3420616)Instruction limit reached!
% 17.84/3.34 % (3420616)------------------------------
% 17.84/3.34 % (3420616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.34 % (3420616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.34 % (3420616)CaDiCaL version: 2.1.3
% 17.84/3.34 % (3420616)Termination reason: Instruction limit
% 17.84/3.34 % (3420616)Termination phase: Saturation
% 17.84/3.34 % (3420616)Time elapsed: 0.087 s
% 17.84/3.34 % (3420616)Peak memory usage: 116 MB
% 17.84/3.34 % (3420616)Instructions burned: 131 (million)
% 17.84/3.34 % (3420620)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1123655865:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.84/3.34 % (3420621)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2886833814:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 17.84/3.34 % (3420622)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1890884877:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 17.84/3.34 % (3420615)Instruction limit reached!
% 18.87/3.79 % (3420615)------------------------------
% 18.87/3.79 % (3420615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.79 % (3420615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.79 % (3420615)CaDiCaL version: 2.1.3
% 18.87/3.79 % (3420615)Termination reason: Instruction limit
% 18.87/3.79 % (3420615)Termination phase: Saturation
% 18.87/3.79 % (3420615)Time elapsed: 0.250 s
% 18.87/3.79 % (3420615)Peak memory usage: 92 MB
% 18.87/3.79 % (3420615)Instructions burned: 294 (million)
% 18.87/3.79 % (3420624)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1964909245:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 18.87/3.79 % (3420621)Instruction limit reached!
% 18.87/3.79 % (3420621)------------------------------
% 18.87/3.79 % (3420621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.79 % (3420621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.79 % (3420621)CaDiCaL version: 2.1.3
% 18.87/3.79 % (3420621)Termination reason: Instruction limit
% 18.87/3.79 % (3420621)Termination phase: Saturation
% 18.87/3.79 % (3420621)Time elapsed: 0.096 s
% 18.87/3.79 % (3420621)Peak memory usage: 133 MB
% 18.87/3.79 % (3420621)Instructions burned: 40 (million)
% 18.87/3.79 % (3420626)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=748183725:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 18.87/3.79 % (3420627)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=2862241126:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 18.87/3.79 % (3420620)Instruction limit reached!
% 18.87/3.79 % (3420620)------------------------------
% 18.87/3.79 % (3420620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.79 % (3420620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.79 % (3420620)CaDiCaL version: 2.1.3
% 18.87/3.79 % (3420620)Termination reason: Instruction limit
% 18.87/3.79 % (3420620)Termination phase: Saturation
% 18.87/3.79 % (3420620)Time elapsed: 0.210 s
% 18.87/3.79 % (3420620)Peak memory usage: 134 MB
% 18.87/3.79 % (3420620)Instructions burned: 131 (million)
% 18.87/3.79 % (3420622)Instruction limit reached!
% 18.87/3.79 % (3420622)------------------------------
% 18.87/3.79 % (3420622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.79 % (3420622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.79 % (3420622)CaDiCaL version: 2.1.3
% 18.87/3.79 % (3420622)Termination reason: Instruction limit
% 18.87/3.79 % (3420622)Termination phase: Saturation
% 18.87/3.79 % (3420622)Time elapsed: 0.270 s
% 18.87/3.79 % (3420622)Peak memory usage: 91 MB
% 18.87/3.79 % (3420622)Instructions burned: 308 (million)
% 18.87/3.79 % (3420631)dis+10_1_si=on:random_seed=3357585049:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi)
% 18.87/3.79 % (3420633)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2137642896:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 18.87/3.79 % (3420626)Instruction limit reached!
% 18.87/3.79 % (3420626)------------------------------
% 18.87/3.79 % (3420626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.79 % (3420626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.79 % (3420626)CaDiCaL version: 2.1.3
% 18.87/3.79 % (3420626)Termination reason: Instruction limit
% 18.87/3.79 % (3420626)Termination phase: Saturation
% 18.87/3.79 % (3420626)Time elapsed: 0.165 s
% 18.87/3.79 % (3420626)Peak memory usage: 117 MB
% 18.87/3.79 % (3420626)Instructions burned: 131 (million)
% 18.87/3.79 % (3420627)Instruction limit reached!
% 18.87/3.79 % (3420627)------------------------------
% 18.87/3.79 % (3420627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.79 % (3420627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.79 % (3420627)CaDiCaL version: 2.1.3
% 18.87/3.79 % (3420627)Termination reason: Instruction limit
% 18.87/3.79 % (3420627)Termination phase: Saturation
% 18.87/3.79 % (3420627)Time elapsed: 0.154 s
% 18.87/3.79 % (3420627)Peak memory usage: 118 MB
% 18.87/3.79 % (3420627)Instructions burned: 261 (million)
% 18.87/3.79 % (3420636)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=612121153:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 25.00/4.25 % (3420640)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4283312422:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 25.00/4.25 % (3420641)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=2465860889:s2a=on:i=128:s2at=5:ins=3:rtra=on_2979 on theBenchmark for (2979ds/128Mi)
% 25.00/4.25 % (3420639)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2881337629:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi)
% 25.00/4.25 % (3420641)Instruction limit reached!
% 25.00/4.25 % (3420641)------------------------------
% 25.00/4.25 % (3420641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/4.25 % (3420641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/4.25 % (3420641)CaDiCaL version: 2.1.3
% 25.00/4.25 % (3420641)Termination reason: Instruction limit
% 25.00/4.25 % (3420641)Termination phase: Saturation
% 25.00/4.25 % (3420641)Time elapsed: 0.090 s
% 25.00/4.25 % (3420641)Peak memory usage: 118 MB
% 25.00/4.25 % (3420641)Instructions burned: 128 (million)
% 25.00/4.25 % (3420639)Instruction limit reached!
% 25.00/4.25 % (3420639)------------------------------
% 25.00/4.25 % (3420639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/4.25 % (3420639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/4.25 % (3420639)CaDiCaL version: 2.1.3
% 25.00/4.25 % (3420639)Termination reason: Instruction limit
% 25.00/4.25 % (3420639)Termination phase: Saturation
% 25.00/4.25 % (3420639)Time elapsed: 0.088 s
% 25.00/4.25 % (3420639)Peak memory usage: 116 MB
% 25.00/4.25 % (3420639)Instructions burned: 65 (million)
% 25.00/4.25 % (3420636)Instruction limit reached!
% 25.00/4.25 % (3420636)------------------------------
% 25.00/4.25 % (3420636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/4.25 % (3420636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/4.25 % (3420636)CaDiCaL version: 2.1.3
% 25.00/4.25 % (3420636)Termination reason: Instruction limit
% 25.00/4.25 % (3420636)Termination phase: Saturation
% 25.00/4.25 % (3420636)Time elapsed: 0.165 s
% 25.00/4.25 % (3420636)Peak memory usage: 90 MB
% 25.00/4.25 % (3420636)Instructions burned: 142 (million)
% 25.00/4.25 % (3420640)Instruction limit reached!
% 25.00/4.25 % (3420640)------------------------------
% 25.00/4.25 % (3420640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/4.25 % (3420640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/4.25 % (3420640)CaDiCaL version: 2.1.3
% 25.00/4.25 % (3420640)Termination reason: Instruction limit
% 25.00/4.25 % (3420640)Termination phase: Saturation
% 25.00/4.25 % (3420640)Time elapsed: 0.131 s
% 25.00/4.25 % (3420640)Peak memory usage: 90 MB
% 25.00/4.25 % (3420640)Instructions burned: 121 (million)
% 25.00/4.25 % (3420633)Instruction limit reached!
% 25.00/4.25 % (3420633)------------------------------
% 25.00/4.25 % (3420633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/4.25 % (3420633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/4.25 % (3420633)CaDiCaL version: 2.1.3
% 25.00/4.25 % (3420633)Termination reason: Instruction limit
% 25.00/4.25 % (3420633)Termination phase: Saturation
% 25.00/4.25 % (3420633)Time elapsed: 0.400 s
% 25.00/4.25 % (3420633)Peak memory usage: 93 MB
% 25.00/4.25 % (3420633)Instructions burned: 383 (million)
% 25.00/4.25 % (3420624)Instruction limit reached!
% 25.00/4.25 % (3420624)------------------------------
% 25.00/4.25 % (3420624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/4.25 % (3420624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/4.25 % (3420624)CaDiCaL version: 2.1.3
% 25.00/4.25 % (3420624)Termination reason: Instruction limit
% 25.00/4.25 % (3420624)Termination phase: Saturation
% 25.00/4.25 % (3420624)Time elapsed: 0.656 s
% 25.00/4.25 % (3420624)Peak memory usage: 138 MB
% 25.00/4.25 % (3420624)Instructions burned: 599 (million)
% 25.00/4.25 % (3420647)dis+1010_1_to=kbo:si=on:random_seed=4122761817:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi)
% 25.00/4.25 % (3420648)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=795359863:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi)
% 26.01/4.62 % (3420646)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=9077608:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi)
% 26.01/4.62 % (3420649)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3659999244:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 26.01/4.62 % (3420647)Instruction limit reached!
% 26.01/4.62 % (3420647)------------------------------
% 26.01/4.62 % (3420647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420647)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420647)Termination reason: Instruction limit
% 26.01/4.62 % (3420647)Termination phase: Saturation
% 26.01/4.62 % (3420647)Time elapsed: 0.107 s
% 26.01/4.62 % (3420647)Peak memory usage: 91 MB
% 26.01/4.62 % (3420647)Instructions burned: 176 (million)
% 26.01/4.62 % (3420646)Instruction limit reached!
% 26.01/4.62 % (3420646)------------------------------
% 26.01/4.62 % (3420646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420646)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420646)Termination reason: Instruction limit
% 26.01/4.62 % (3420646)Termination phase: Saturation
% 26.01/4.62 % (3420646)Time elapsed: 0.073 s
% 26.01/4.62 % (3420646)Peak memory usage: 115 MB
% 26.01/4.62 % (3420646)Instructions burned: 39 (million)
% 26.01/4.62 % (3420650)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1498734113:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 26.01/4.62 % (3420651)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3965567026:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 26.01/4.62 % (3420656)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2348732842:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi)
% 26.01/4.62 % (3420657)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1586700212:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi)
% 26.01/4.62 % (3420650)Instruction limit reached!
% 26.01/4.62 % (3420650)------------------------------
% 26.01/4.62 % (3420650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420650)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420650)Termination reason: Instruction limit
% 26.01/4.62 % (3420650)Termination phase: Saturation
% 26.01/4.62 % (3420650)Time elapsed: 0.253 s
% 26.01/4.62 % (3420650)Peak memory usage: 135 MB
% 26.01/4.62 % (3420650)Instructions burned: 215 (million)
% 26.01/4.62 % (3420648)Instruction limit reached!
% 26.01/4.62 % (3420648)------------------------------
% 26.01/4.62 % (3420648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420648)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420648)Termination reason: Instruction limit
% 26.01/4.62 % (3420648)Termination phase: Saturation
% 26.01/4.62 % (3420648)Time elapsed: 0.395 s
% 26.01/4.62 % (3420648)Peak memory usage: 119 MB
% 26.01/4.62 % (3420648)Instructions burned: 329 (million)
% 26.01/4.62 % (3420656)Instruction limit reached!
% 26.01/4.62 % (3420656)------------------------------
% 26.01/4.62 % (3420656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420656)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420656)Termination reason: Instruction limit
% 26.01/4.62 % (3420656)Termination phase: Saturation
% 26.01/4.62 % (3420656)Time elapsed: 0.150 s
% 26.01/4.62 % (3420656)Peak memory usage: 91 MB
% 26.01/4.62 % (3420656)Instructions burned: 296 (million)
% 26.01/4.62 % (3420631)Instruction limit reached!
% 26.01/4.62 % (3420631)------------------------------
% 26.01/4.62 % (3420631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420631)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420631)Termination reason: Instruction limit
% 26.01/4.62 % (3420631)Termination phase: Saturation
% 26.01/4.62 % (3420631)Time elapsed: 1.004 s
% 26.01/4.62 % (3420631)Peak memory usage: 96 MB
% 26.01/4.62 % (3420631)Instructions burned: 1000 (million)
% 26.01/4.62 % (3420651)Instruction limit reached!
% 26.01/4.62 % (3420651)------------------------------
% 26.01/4.62 % (3420651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420651)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420651)Termination reason: Instruction limit
% 26.01/4.62 % (3420651)Termination phase: Saturation
% 26.01/4.62 % (3420651)Time elapsed: 0.383 s
% 26.01/4.62 % (3420651)Peak memory usage: 119 MB
% 26.01/4.62 % (3420651)Instructions burned: 349 (million)
% 26.01/4.62 % (3420664)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=232485907:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi)
% 26.01/4.62 % (3420649)Instruction limit reached!
% 26.01/4.62 % (3420649)------------------------------
% 26.01/4.62 % (3420649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420649)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420649)Termination reason: Instruction limit
% 26.01/4.62 % (3420649)Termination phase: Saturation
% 26.01/4.62 % (3420649)Time elapsed: 0.535 s
% 26.01/4.62 % (3420649)Peak memory usage: 135 MB
% 26.01/4.62 % (3420649)Instructions burned: 483 (million)
% 26.01/4.62 % (3420662)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=174031613:i=281:gtgl=2:rtra=on:gtg=all_2969 on theBenchmark for (2969ds/281Mi)
% 26.01/4.62 % (3420657)Instruction limit reached!
% 26.01/4.62 % (3420657)------------------------------
% 26.01/4.62 % (3420657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420657)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420657)Termination reason: Instruction limit
% 26.01/4.62 % (3420657)Termination phase: Saturation
% 26.01/4.62 % (3420657)Time elapsed: 0.355 s
% 26.01/4.62 % (3420657)Peak memory usage: 118 MB
% 26.01/4.62 % (3420657)Instructions burned: 328 (million)
% 26.01/4.62 % (3420663)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1420322070:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi)
% 26.01/4.62 % (3420665)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2284220777:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 26.01/4.62 % (3420666)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3126657053:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 26.01/4.62 % (3420664)Instruction limit reached!
% 26.01/4.62 % (3420664)------------------------------
% 26.01/4.62 % (3420664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420664)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420664)Termination reason: Instruction limit
% 26.01/4.62 % (3420664)Termination phase: Saturation
% 26.01/4.62 % (3420664)Time elapsed: 0.264 s
% 26.01/4.62 % (3420664)Peak memory usage: 114 MB
% 26.01/4.62 % (3420664)Instructions burned: 322 (million)
% 26.01/4.62 % (3420662)First to succeed.
% 26.01/4.62 % (3420669)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=883413358:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi)
% 26.01/4.62 % (3420662)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3420545"
% 26.01/4.62 % (3420665)Instruction limit reached!
% 26.01/4.62 % (3420665)------------------------------
% 26.01/4.62 % (3420665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420665)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420665)Termination reason: Instruction limit
% 26.01/4.62 % (3420665)Termination phase: Saturation
% 26.01/4.62 % (3420665)Time elapsed: 0.222 s
% 26.01/4.62 % (3420665)Peak memory usage: 119 MB
% 26.01/4.62 % (3420665)Instructions burned: 416 (million)
% 26.01/4.62 % (3420671)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3711597807:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 26.01/4.62 % (3420674)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1681953413:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi)
% 26.01/4.62 % (3420663)Instruction limit reached!
% 26.01/4.62 % (3420663)------------------------------
% 26.01/4.62 % (3420663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420663)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420663)Termination reason: Instruction limit
% 26.01/4.62 % (3420663)Termination phase: Saturation
% 26.01/4.62 % (3420663)Time elapsed: 0.440 s
% 26.01/4.62 % (3420663)Peak memory usage: 91 MB
% 26.01/4.62 % (3420663)Instructions burned: 485 (million)
% 26.01/4.62 % (3420676)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3678064212:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi)
% 26.01/4.62 % (3420669)Instruction limit reached!
% 26.01/4.62 % (3420669)------------------------------
% 26.01/4.62 % (3420669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.01/4.62 % (3420669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.01/4.62 % (3420669)CaDiCaL version: 2.1.3
% 26.01/4.62 % (3420669)Termination reason: Instruction limit
% 26.01/4.62 % (3420669)Termination phase: Saturation
% 26.01/4.62 % (3420669)Time elapsed: 0.346 s
% 26.01/4.62 % (3420669)Peak memory usage: 135 MB
% 26.01/4.62 % (3420669)Instructions burned: 277 (million)
% 26.01/4.62 % (3420662)Refutation found. Thanks to Tanya!
% 26.01/4.62 % SZS status Theorem for theBenchmark
% 26.01/4.62 % SZS output start Proof for theBenchmark
% See solution above
% 28.22/4.92 % (3420662)------------------------------
% 28.22/4.92 % (3420662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/4.92 % (3420662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/4.92 % (3420662)CaDiCaL version: 2.1.3
% 28.22/4.92 % (3420662)Termination reason: Refutation
% 28.22/4.92 % (3420662)Time elapsed: 0.268 s
% 28.22/4.92 % (3420662)Peak memory usage: 118 MB
% 28.22/4.92 % (3420662)Instructions burned: 208 (million)
% 28.22/4.92 % (3420662)------------------------------
% 28.22/4.92 % (3420662)------------------------------
% 28.22/4.92 % (3420545)Success in time 3.899 s
% 28.22/4.92 % Vampire exiting
%------------------------------------------------------------------------------