%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW670_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:31:06 PM UTC 2026
% Result : Theorem 5.75s 1.69s
% Output : Refutation 7.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 13
% Syntax : Number of formulae : 104 ( 31 unt; 0 typ; 4 def)
% Number of atoms : 364 ( 167 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 391 ( 131 ~; 117 |; 97 &)
% ( 9 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 401 ( 109 atm; 49 fun; 174 num; 69 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 : 11 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 47 ( 42 usr; 16 con; 0-5 aty)
% Number of variables : 149 ( 0 sgn 120 !; 29 ?; 149 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
list_int: $tType ).
tff(type_def_10,type,
option_int: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
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_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(func_def_18,type,
length1: ( ty * uni ) > $int ).
tff(func_def_21,type,
option: ty > ty ).
tff(func_def_22,type,
none: ty > uni ).
tff(func_def_23,type,
some: ( ty * uni ) > uni ).
tff(func_def_24,type,
match_option1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_25,type,
some_proj_11: ( ty * uni ) > uni ).
tff(func_def_26,type,
nth1: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
t2tb: option_int > uni ).
tff(func_def_29,type,
tb2t: uni > option_int ).
tff(func_def_30,type,
t2tb1: list_int > uni ).
tff(func_def_31,type,
tb2t1: uni > list_int ).
tff(func_def_32,type,
t2tb2: $int > uni ).
tff(func_def_33,type,
tb2t2: uni > $int ).
tff(func_def_34,type,
ref: ty > ty ).
tff(func_def_35,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_36,type,
contents: ( ty * uni ) > uni ).
tff(func_def_37,type,
hd: ( ty * uni ) > uni ).
tff(func_def_38,type,
tl: ( ty * uni ) > uni ).
tff(func_def_40,type,
sK0: list_int > $int ).
tff(func_def_41,type,
sK1: ( list_int * $int ) > $int ).
tff(func_def_42,type,
sK2: list_int ).
tff(func_def_43,type,
sK3: list_int ).
tff(func_def_44,type,
sK4: $int ).
tff(func_def_45,type,
sK5: $int ).
tff(func_def_46,type,
sK6: list_int ).
tff(func_def_47,type,
sK7: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
zero_at1: ( list_int * $int ) > $o ).
tff(pred_def_5,type,
no_zero1: list_int > $o ).
tff(f14,axiom,
! [X2: uni,X1: uni,X0: ty] : ( nil(X0) != cons(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nil_Cons1) ).
tff(f21,axiom,
! [X0: ty,X1: uni] : $lesseq(0,length1(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_nonnegative) ).
tff(f22,axiom,
! [X1: uni,X0: ty] :
( ( X1 = nil(X0) )
<=> ( length1(X0,X1) = 0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_nil) ).
tff(f33,axiom,
! [X0: ty,X1: $int] :
( ! [X2: uni,X3: uni] :
( ( ( X1 = 0 )
=> ( nth1(X0,X1,cons(X0,X2,X3)) = some(X0,X2) ) )
& ( ( X1 != 0 )
=> ( nth1(X0,X1,cons(X0,X2,X3)) = nth1(X0,$difference(X1,1),X3) ) ) )
& ( nth1(X0,X1,nil(X0)) = none(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nth_def) ).
tff(f36,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f39,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f43,axiom,
! [X1: $int,X0: list_int] :
( ( ( tb2t(nth1(int,X1,t2tb1(X0))) = tb2t(some(int,t2tb2(0))) )
& ! [X2: $int] :
( ( $lesseq(0,X2)
& $less(X2,X1) )
=> ( tb2t(nth1(int,X2,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) ) )
<=> zero_at1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zero_at_def) ).
tff(f53,conjecture,
! [X2: $int,X1: list_int,X0: list_int] :
( ( $lesseq(0,X2)
& ! [X3: $int] :
( ( $less(X3,X2)
& $lesseq(0,X3) )
=> ( tb2t(nth1(int,X3,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) )
& ( $sum(X2,length1(int,t2tb1(X1))) = length1(int,t2tb1(X0)) )
& ! [X3: $int] :
( $lesseq(0,X3)
=> ( tb2t(nth1(int,X3,t2tb1(X1))) = tb2t(nth1(int,$sum(X2,X3),t2tb1(X0))) ) ) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ! [X4: $int] :
( ? [X5: $int,X6: list_int] :
( ( X1 = tb2t1(cons(int,t2tb2(X5),t2tb1(X6))) )
& ( X4 = X5 ) )
=> ( ( X4 = 0 )
=> ( ( ( X2 = length1(int,t2tb1(X0)) )
& no_zero1(X0) )
| ( zero_at1(X0,X2)
& $less(X2,length1(int,t2tb1(X0)))
& $lesseq(0,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_search_loop) ).
tff(f54,negated_conjecture,
~ ! [X2: $int,X1: list_int,X0: list_int] :
( ( $lesseq(0,X2)
& ! [X3: $int] :
( ( $less(X3,X2)
& $lesseq(0,X3) )
=> ( tb2t(nth1(int,X3,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) )
& ( $sum(X2,length1(int,t2tb1(X1))) = length1(int,t2tb1(X0)) )
& ! [X3: $int] :
( $lesseq(0,X3)
=> ( tb2t(nth1(int,X3,t2tb1(X1))) = tb2t(nth1(int,$sum(X2,X3),t2tb1(X0))) ) ) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ! [X4: $int] :
( ? [X5: $int,X6: list_int] :
( ( X1 = tb2t1(cons(int,t2tb2(X5),t2tb1(X6))) )
& ( X4 = X5 ) )
=> ( ( X4 = 0 )
=> ( ( ( X2 = length1(int,t2tb1(X0)) )
& no_zero1(X0) )
| ( zero_at1(X0,X2)
& $less(X2,length1(int,t2tb1(X0)))
& $lesseq(0,X2) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
tff(f55,plain,
~ ! [X2: $int,X1: list_int,X0: list_int] :
( ( ~ $less(X2,0)
& ! [X3: $int] :
( ( $less(X3,X2)
& ~ $less(X3,0) )
=> ( tb2t(nth1(int,X3,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) )
& ( $sum(X2,length1(int,t2tb1(X1))) = length1(int,t2tb1(X0)) )
& ! [X3: $int] :
( ~ $less(X3,0)
=> ( tb2t(nth1(int,X3,t2tb1(X1))) = tb2t(nth1(int,$sum(X2,X3),t2tb1(X0))) ) ) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ! [X4: $int] :
( ? [X5: $int,X6: list_int] :
( ( X1 = tb2t1(cons(int,t2tb2(X5),t2tb1(X6))) )
& ( X4 = X5 ) )
=> ( ( X4 = 0 )
=> ( ( ( X2 = length1(int,t2tb1(X0)) )
& no_zero1(X0) )
| ( zero_at1(X0,X2)
& $less(X2,length1(int,t2tb1(X0)))
& ~ $less(X2,0) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f54]) ).
tff(f57,plain,
! [X0: ty,X1: uni] : ~ $less(length1(X0,X1),0),
inference(theory_normalization,[],[f21]) ).
tff(f59,plain,
! [X1: $int,X0: list_int] :
( ( ( tb2t(nth1(int,X1,t2tb1(X0))) = tb2t(some(int,t2tb2(0))) )
& ! [X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,X1) )
=> ( tb2t(nth1(int,X2,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) ) )
<=> zero_at1(X0,X1) ),
inference(theory_normalization,[],[f43]) ).
tff(f60,plain,
! [X1: $int,X0: ty] :
( ( nth1(X0,X1,nil(X0)) = none(X0) )
& ! [X2: uni,X3: uni] :
( ( ( X1 != 0 )
=> ( nth1(X0,X1,cons(X0,X2,X3)) = nth1(X0,$sum(X1,$uminus(1)),X3) ) )
& ( ( X1 = 0 )
=> ( nth1(X0,X1,cons(X0,X2,X3)) = some(X0,X2) ) ) ) ),
inference(theory_normalization,[],[f33]) ).
tff(f68,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( X0 = X1 )
| $less(X0,X1) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f81,plain,
~ ! [X1: list_int,X2: list_int,X0: $int] :
( ( ~ $less(X0,0)
& ( length1(int,t2tb1(X2)) = $sum(X0,length1(int,t2tb1(X1))) )
& ! [X3: $int] :
( ( $less(X3,X0)
& ~ $less(X3,0) )
=> ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X3,t2tb1(X2))) ) )
& ! [X4: $int] :
( ~ $less(X4,0)
=> ( tb2t(nth1(int,$sum(X0,X4),t2tb1(X2))) = tb2t(nth1(int,X4,t2tb1(X1))) ) ) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ( ( X1 != tb2t1(nil(int)) )
=> ! [X5: $int] :
( ? [X7: list_int,X6: $int] :
( ( X5 = X6 )
& ( tb2t1(cons(int,t2tb2(X6),t2tb1(X7))) = X1 ) )
=> ( ( 0 = X5 )
=> ( ( no_zero1(X2)
& ( length1(int,t2tb1(X2)) = X0 ) )
| ( $less(X0,length1(int,t2tb1(X2)))
& zero_at1(X2,X0)
& ~ $less(X0,0) ) ) ) ) ) ) ),
inference(rectify,[],[f55]) ).
tff(f93,plain,
! [X0: uni,X1: ty] :
( ( nil(X1) = X0 )
<=> ( 0 = length1(X1,X0) ) ),
inference(rectify,[],[f22]) ).
tff(f98,plain,
! [X1: list_int,X0: $int] :
( zero_at1(X1,X0)
<=> ( ! [X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X2,t2tb1(X1))) ) )
& ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,X0,t2tb1(X1))) ) ) ),
inference(rectify,[],[f59]) ).
tff(f101,plain,
! [X0: uni,X2: ty,X1: uni] : ( cons(X2,X1,X0) != nil(X2) ),
inference(rectify,[],[f14]) ).
tff(f104,plain,
! [X1: list_int,X0: $int] :
( ( ! [X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X2,t2tb1(X1))) ) )
& ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,X0,t2tb1(X1))) ) )
=> zero_at1(X1,X0) ),
inference(unused_predicate_definition_removal,[],[f98]) ).
tff(f111,plain,
! [X1: list_int,X0: $int] :
( zero_at1(X1,X0)
| ? [X2: $int] :
( ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,X2,t2tb1(X1))) )
& ~ $less(X2,0)
& $less(X2,X0) )
| ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X0,t2tb1(X1))) ) ),
inference(ennf_transformation,[],[f104]) ).
tff(f112,plain,
! [X1: list_int,X0: $int] :
( zero_at1(X1,X0)
| ? [X2: $int] :
( ~ $less(X2,0)
& ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,X2,t2tb1(X1))) )
& $less(X2,X0) )
| ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X0,t2tb1(X1))) ) ),
inference(flattening,[],[f111]) ).
tff(f122,plain,
! [X0: ty,X1: $int] :
( ( nth1(X0,X1,nil(X0)) = none(X0) )
& ! [X3: uni,X2: uni] :
( ( ( nth1(X0,X1,cons(X0,X2,X3)) = some(X0,X2) )
| ( 0 != X1 ) )
& ( ( 0 = X1 )
| ( nth1(X0,X1,cons(X0,X2,X3)) = nth1(X0,$sum(X1,$uminus(1)),X3) ) ) ) ),
inference(ennf_transformation,[],[f60]) ).
tff(f124,plain,
? [X1: list_int,X2: list_int,X0: $int] :
( ? [X5: $int] :
( ( ( length1(int,t2tb1(X2)) != X0 )
| ~ no_zero1(X2) )
& ( ~ zero_at1(X2,X0)
| $less(X0,0)
| ~ $less(X0,length1(int,t2tb1(X2))) )
& ( 0 = X5 )
& ? [X7: list_int,X6: $int] :
( ( X5 = X6 )
& ( tb2t1(cons(int,t2tb2(X6),t2tb1(X7))) = X1 ) ) )
& ( X1 != tb2t1(nil(int)) )
& ( X1 != tb2t1(nil(int)) )
& ~ $less(X0,0)
& ( length1(int,t2tb1(X2)) = $sum(X0,length1(int,t2tb1(X1))) )
& ! [X3: $int] :
( ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X3,t2tb1(X2))) )
| ~ $less(X3,X0)
| $less(X3,0) )
& ! [X4: $int] :
( ( tb2t(nth1(int,$sum(X0,X4),t2tb1(X2))) = tb2t(nth1(int,X4,t2tb1(X1))) )
| $less(X4,0) ) ),
inference(ennf_transformation,[],[f81]) ).
tff(f125,plain,
? [X1: list_int,X2: list_int,X0: $int] :
( ! [X4: $int] :
( ( tb2t(nth1(int,$sum(X0,X4),t2tb1(X2))) = tb2t(nth1(int,X4,t2tb1(X1))) )
| $less(X4,0) )
& ! [X3: $int] :
( ~ $less(X3,X0)
| $less(X3,0)
| ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X3,t2tb1(X2))) ) )
& ( X1 != tb2t1(nil(int)) )
& ~ $less(X0,0)
& ( X1 != tb2t1(nil(int)) )
& ? [X5: $int] :
( ( 0 = X5 )
& ( ( length1(int,t2tb1(X2)) != X0 )
| ~ no_zero1(X2) )
& ? [X7: list_int,X6: $int] :
( ( X5 = X6 )
& ( tb2t1(cons(int,t2tb2(X6),t2tb1(X7))) = X1 ) )
& ( ~ zero_at1(X2,X0)
| $less(X0,0)
| ~ $less(X0,length1(int,t2tb1(X2))) ) )
& ( length1(int,t2tb1(X2)) = $sum(X0,length1(int,t2tb1(X1))) ) ),
inference(flattening,[],[f124]) ).
tff(f135,plain,
! [X0: uni,X1: ty,X2: uni] : ( nil(X1) != cons(X1,X2,X0) ),
inference(rectify,[],[f101]) ).
tff(f143,plain,
! [X0: list_int,X1: $int] :
( zero_at1(X0,X1)
| ? [X2: $int] :
( ~ $less(X2,0)
& ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,X2,t2tb1(X0))) )
& $less(X2,X1) )
| ( tb2t(nth1(int,X1,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) ),
inference(rectify,[],[f112]) ).
tff(f144,plain,
! [X0: list_int,X1: $int] :
( zero_at1(X0,X1)
| ( ~ $less(sK1(X0,X1),0)
& ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(X0,X1),t2tb1(X0))) )
& $less(sK1(X0,X1),X1) )
| ( tb2t(nth1(int,X1,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f143]) ).
tff(f147,plain,
! [X0: ty,X1: $int] :
( ( nth1(X0,X1,nil(X0)) = none(X0) )
& ! [X2: uni,X3: uni] :
( ( ( nth1(X0,X1,cons(X0,X3,X2)) = some(X0,X3) )
| ( 0 != X1 ) )
& ( ( 0 = X1 )
| ( nth1(X0,$sum(X1,$uminus(1)),X2) = nth1(X0,X1,cons(X0,X3,X2)) ) ) ) ),
inference(rectify,[],[f122]) ).
tff(f149,plain,
? [X0: list_int,X1: list_int,X2: $int] :
( ! [X3: $int] :
( ( tb2t(nth1(int,X3,t2tb1(X0))) = tb2t(nth1(int,$sum(X2,X3),t2tb1(X1))) )
| $less(X3,0) )
& ! [X4: $int] :
( ~ $less(X4,X2)
| $less(X4,0)
| ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X4,t2tb1(X1))) ) )
& ( tb2t1(nil(int)) != X0 )
& ~ $less(X2,0)
& ( tb2t1(nil(int)) != X0 )
& ? [X5: $int] :
( ( 0 = X5 )
& ( ( length1(int,t2tb1(X1)) != X2 )
| ~ no_zero1(X1) )
& ? [X6: list_int,X7: $int] :
( ( X5 = X7 )
& ( tb2t1(cons(int,t2tb2(X7),t2tb1(X6))) = X0 ) )
& ( ~ zero_at1(X1,X2)
| $less(X2,0)
| ~ $less(X2,length1(int,t2tb1(X1))) ) )
& ( length1(int,t2tb1(X1)) = $sum(X2,length1(int,t2tb1(X0))) ) ),
inference(rectify,[],[f125]) ).
tff(f150,plain,
( ! [X3: $int] :
( ( tb2t(nth1(int,X3,t2tb1(sK2))) = tb2t(nth1(int,$sum(sK4,X3),t2tb1(sK3))) )
| $less(X3,0) )
& ! [X4: $int] :
( ~ $less(X4,sK4)
| $less(X4,0)
| ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X4,t2tb1(sK3))) ) )
& ( tb2t1(nil(int)) != sK2 )
& ~ $less(sK4,0)
& ( tb2t1(nil(int)) != sK2 )
& ( 0 = sK5 )
& ( ( length1(int,t2tb1(sK3)) != sK4 )
| ~ no_zero1(sK3) )
& ( sK5 = sK7 )
& ( tb2t1(cons(int,t2tb2(sK7),t2tb1(sK6))) = sK2 )
& ( ~ zero_at1(sK3,sK4)
| $less(sK4,0)
| ~ $less(sK4,length1(int,t2tb1(sK3))) )
& ( length1(int,t2tb1(sK3)) = $sum(sK4,length1(int,t2tb1(sK2))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7)],[f149]) ).
tff(f153,plain,
! [X0: uni,X1: ty] :
( ( ( nil(X1) = X0 )
| ( 0 != length1(X1,X0) ) )
& ( ( 0 = length1(X1,X0) )
| ( nil(X1) != X0 ) ) ),
inference(nnf_transformation,[],[f93]) ).
tff(f171,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f36]) ).
tff(f177,plain,
! [X2: uni,X0: uni,X1: ty] : ( nil(X1) != cons(X1,X2,X0) ),
inference(cnf_transformation,[],[f135]) ).
tff(f191,plain,
! [X0: list_int,X1: $int] :
( ( tb2t(nth1(int,X1,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) )
| zero_at1(X0,X1)
| $less(sK1(X0,X1),X1) ),
inference(cnf_transformation,[],[f144]) ).
tff(f192,plain,
! [X0: list_int,X1: $int] :
( ( tb2t(nth1(int,X1,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) )
| zero_at1(X0,X1)
| ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(X0,X1),t2tb1(X0))) ) ),
inference(cnf_transformation,[],[f144]) ).
tff(f193,plain,
! [X0: list_int,X1: $int] :
( ( tb2t(nth1(int,X1,t2tb1(X0))) != tb2t(some(int,t2tb2(0))) )
| zero_at1(X0,X1)
| ~ $less(sK1(X0,X1),0) ),
inference(cnf_transformation,[],[f144]) ).
tff(f201,plain,
! [X2: uni,X3: uni,X0: ty,X1: $int] :
( ( nth1(X0,X1,cons(X0,X3,X2)) = some(X0,X3) )
| ( 0 != X1 ) ),
inference(cnf_transformation,[],[f147]) ).
tff(f206,plain,
length1(int,t2tb1(sK3)) = $sum(sK4,length1(int,t2tb1(sK2))),
inference(cnf_transformation,[],[f150]) ).
tff(f207,plain,
( ~ $less(sK4,length1(int,t2tb1(sK3)))
| $less(sK4,0)
| ~ zero_at1(sK3,sK4) ),
inference(cnf_transformation,[],[f150]) ).
tff(f208,plain,
tb2t1(cons(int,t2tb2(sK7),t2tb1(sK6))) = sK2,
inference(cnf_transformation,[],[f150]) ).
tff(f209,plain,
sK5 = sK7,
inference(cnf_transformation,[],[f150]) ).
tff(f211,plain,
0 = sK5,
inference(cnf_transformation,[],[f150]) ).
tff(f213,plain,
~ $less(sK4,0),
inference(cnf_transformation,[],[f150]) ).
tff(f215,plain,
! [X4: $int] :
( ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X4,t2tb1(sK3))) )
| ~ $less(X4,sK4)
| $less(X4,0) ),
inference(cnf_transformation,[],[f150]) ).
tff(f216,plain,
! [X3: $int] :
( ( tb2t(nth1(int,X3,t2tb1(sK2))) = tb2t(nth1(int,$sum(sK4,X3),t2tb1(sK3))) )
| $less(X3,0) ),
inference(cnf_transformation,[],[f150]) ).
tff(f221,plain,
! [X0: uni,X1: ty] :
( ( 0 != length1(X1,X0) )
| ( nil(X1) = X0 ) ),
inference(cnf_transformation,[],[f153]) ).
tff(f222,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f39]) ).
tff(f227,plain,
! [X0: ty,X1: uni] : ~ $less(length1(X0,X1),0),
inference(cnf_transformation,[],[f57]) ).
tff(f234,plain,
0 = sK7,
inference(definition_unfolding,[],[f209,f211]) ).
tff(f236,plain,
! [X2: uni,X3: uni,X0: ty] : ( nth1(X0,0,cons(X0,X3,X2)) = some(X0,X3) ),
inference(equality_resolution,[],[f201]) ).
tff(f242,definition,
( spl8_1
<=> $less(sK4,0) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
tff(f246,definition,
( spl8_2
<=> $less(sK4,length1(int,t2tb1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
tff(f248,plain,
( ~ $less(sK4,length1(int,t2tb1(sK3)))
| spl8_2 ),
inference(avatar_component_clause,[],[f246]) ).
tff(f250,definition,
( spl8_3
<=> zero_at1(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
tff(f252,plain,
( ~ zero_at1(sK3,sK4)
| spl8_3 ),
inference(avatar_component_clause,[],[f250]) ).
tff(f253,plain,
( spl8_1
| ~ spl8_2
| ~ spl8_3 ),
inference(avatar_split_clause,[],[f207,f250,f246,f242]) ).
tff(f254,plain,
~ spl8_1,
inference(avatar_split_clause,[],[f213,f242]) ).
tff(f260,definition,
( spl8_5
<=> ( 0 = length1(int,t2tb1(sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
tff(f261,plain,
( ( 0 = length1(int,t2tb1(sK2)) )
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f260]) ).
tff(f262,plain,
( ( 0 != length1(int,t2tb1(sK2)) )
| spl8_5 ),
inference(avatar_component_clause,[],[f260]) ).
tff(f264,plain,
tb2t1(cons(int,t2tb2(0),t2tb1(sK6))) = sK2,
inference(superposition,[],[f208,f234]) ).
tff(f265,plain,
( ~ $less(sK4,$sum(sK4,length1(int,t2tb1(sK2))))
| spl8_2 ),
inference(superposition,[],[f248,f206]) ).
tff(f266,plain,
( ~ $less(0,length1(int,t2tb1(sK2)))
| spl8_2 ),
inference(cancellation,[],[f265]) ).
tff(f272,plain,
! [X0: $int] :
( ( t2tb(tb2t(nth1(int,X0,t2tb1(sK2)))) = nth1(int,$sum(sK4,X0),t2tb1(sK3)) )
| $less(X0,0) ),
inference(superposition,[],[f171,f216]) ).
tff(f273,plain,
! [X0: $int] :
( ( nth1(int,X0,t2tb1(sK2)) = nth1(int,$sum(sK4,X0),t2tb1(sK3)) )
| $less(X0,0) ),
inference(forward_demodulation,[],[f272,f171]) ).
tff(f275,plain,
t2tb1(sK2) = cons(int,t2tb2(0),t2tb1(sK6)),
inference(superposition,[],[f222,f264]) ).
tff(f282,plain,
nil(int) != t2tb1(sK2),
inference(superposition,[],[f177,f275]) ).
tff(f288,plain,
( $less(length1(int,t2tb1(sK2)),0)
| ( 0 = length1(int,t2tb1(sK2)) )
| spl8_2 ),
inference(resolution,[],[f68,f266]) ).
tff(f295,plain,
( ( 0 = length1(int,t2tb1(sK2)) )
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f288,f227]) ).
tff(f316,plain,
( $false
| spl8_2
| spl8_5 ),
inference(forward_subsumption_resolution,[],[f295,f262]) ).
tff(f317,plain,
( spl8_2
| spl8_5 ),
inference(avatar_contradiction_clause,[],[f316]) ).
tff(f337,plain,
( ( 0 != 0 )
| ( nil(int) = t2tb1(sK2) )
| ~ spl8_5 ),
inference(superposition,[],[f221,f261]) ).
tff(f338,plain,
( ( nil(int) = t2tb1(sK2) )
| ~ spl8_5 ),
inference(trivial_inequality_removal,[],[f337]) ).
tff(f339,plain,
( $false
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f338,f282]) ).
tff(f340,plain,
~ spl8_5,
inference(avatar_contradiction_clause,[],[f339]) ).
tff(f382,plain,
some(int,t2tb2(0)) = nth1(int,0,t2tb1(sK2)),
inference(superposition,[],[f236,f275]) ).
tff(f494,plain,
! [X0: $int] :
( ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X0,t2tb1(sK2))) )
| $less(X0,0)
| $less(sK1(sK3,$sum(sK4,X0)),$sum(sK4,X0))
| zero_at1(sK3,$sum(sK4,X0)) ),
inference(superposition,[],[f191,f273]) ).
tff(f533,plain,
! [X0: $int] :
( ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X0,t2tb1(sK2))) )
| $less(X0,0)
| ~ $less(sK1(sK3,$sum(sK4,X0)),0)
| zero_at1(sK3,$sum(sK4,X0)) ),
inference(superposition,[],[f193,f273]) ).
tff(f542,plain,
! [X0: $int] :
( ( tb2t(some(int,t2tb2(0))) != tb2t(nth1(int,X0,t2tb1(sK2))) )
| ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(sK3,$sum(sK4,X0)),t2tb1(sK3))) )
| zero_at1(sK3,$sum(sK4,X0))
| $less(X0,0) ),
inference(superposition,[],[f192,f273]) ).
tff(f573,plain,
( $less(0,0)
| zero_at1(sK3,$sum(sK4,0))
| ( tb2t(some(int,t2tb2(0))) != tb2t(some(int,t2tb2(0))) )
| ~ $less(sK1(sK3,$sum(sK4,0)),0) ),
inference(superposition,[],[f533,f382]) ).
tff(f576,plain,
( ~ $less(sK1(sK3,$sum(sK4,0)),0)
| $less(0,0)
| zero_at1(sK3,$sum(sK4,0)) ),
inference(trivial_inequality_removal,[],[f573]) ).
tff(f577,plain,
( ~ $less(sK1(sK3,sK4),0)
| zero_at1(sK3,sK4) ),
inference(evaluation,[],[f576]) ).
tff(f580,plain,
( ~ $less(sK1(sK3,sK4),0)
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f577,f252]) ).
tff(f983,plain,
( $less(0,0)
| $less(sK1(sK3,$sum(sK4,0)),$sum(sK4,0))
| zero_at1(sK3,$sum(sK4,0))
| ( tb2t(some(int,t2tb2(0))) != tb2t(some(int,t2tb2(0))) ) ),
inference(superposition,[],[f494,f382]) ).
tff(f988,plain,
( zero_at1(sK3,$sum(sK4,0))
| $less(0,0)
| $less(sK1(sK3,$sum(sK4,0)),$sum(sK4,0)) ),
inference(trivial_inequality_removal,[],[f983]) ).
tff(f989,plain,
( zero_at1(sK3,sK4)
| $less(sK1(sK3,sK4),sK4) ),
inference(evaluation,[],[f988]) ).
tff(f996,plain,
( $less(sK1(sK3,sK4),sK4)
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f989,f252]) ).
tff(f1020,plain,
( ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(sK3,$sum(sK4,0)),t2tb1(sK3))) )
| $less(0,0)
| zero_at1(sK3,$sum(sK4,0))
| ( tb2t(some(int,t2tb2(0))) != tb2t(some(int,t2tb2(0))) ) ),
inference(superposition,[],[f542,f382]) ).
tff(f1030,plain,
( $less(0,0)
| ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(sK3,$sum(sK4,0)),t2tb1(sK3))) )
| zero_at1(sK3,$sum(sK4,0)) ),
inference(trivial_inequality_removal,[],[f1020]) ).
tff(f1031,plain,
( ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(sK3,sK4),t2tb1(sK3))) )
| zero_at1(sK3,sK4) ),
inference(evaluation,[],[f1030]) ).
tff(f1033,plain,
( ( tb2t(some(int,t2tb2(0))) = tb2t(nth1(int,sK1(sK3,sK4),t2tb1(sK3))) )
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f1031,f252]) ).
tff(f1050,plain,
( ( tb2t(some(int,t2tb2(0))) != tb2t(some(int,t2tb2(0))) )
| ~ $less(sK1(sK3,sK4),sK4)
| $less(sK1(sK3,sK4),0)
| spl8_3 ),
inference(superposition,[],[f215,f1033]) ).
tff(f1055,plain,
( $less(sK1(sK3,sK4),0)
| ~ $less(sK1(sK3,sK4),sK4)
| spl8_3 ),
inference(trivial_inequality_removal,[],[f1050]) ).
tff(f1067,plain,
( ~ $less(sK1(sK3,sK4),sK4)
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f1055,f580]) ).
tff(f1078,plain,
( $false
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f1067,f996]) ).
tff(f1079,plain,
spl8_3,
inference(avatar_contradiction_clause,[],[f1078]) ).
cnf(s1,plain,
( spl8_1
| ~ spl8_2
| ~ spl8_3 ),
inference(sat_conversion,[],[f253]) ).
cnf(s2,plain,
~ spl8_1,
inference(sat_conversion,[],[f254]) ).
cnf(s6,plain,
( spl8_2
| spl8_5 ),
inference(sat_conversion,[],[f317]) ).
cnf(s7,plain,
~ spl8_5,
inference(sat_conversion,[],[f340]) ).
cnf(s24,plain,
spl8_3,
inference(sat_conversion,[],[f1079]) ).
cnf(s25,plain,
spl8_2,
inference(rat,[],[s6,s7]) ).
cnf(s26,plain,
$false,
inference(rat,[],[s1,s24,s25,s2]) ).
tff(f1080,plain,
$false,
inference(avatar_sat_refutation,[],[s26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW670_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n018.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 14:26:40 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 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.56/1.24 % (3425451)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.56/1.24 % (3425495)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1103039073:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.56/1.24 % (3425494)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1699198770:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.56/1.24 % (3425500)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=569857001:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.56/1.24 % (3425498)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3048920123:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.56/1.24 % (3425499)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2074519818:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.56/1.24 % (3425497)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1514713447:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.56/1.24 % (3425496)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3260366419:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.56/1.24 % (3425498)Instruction limit reached!
% 3.56/1.24 % (3425498)------------------------------
% 3.56/1.24 % (3425498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.24 % (3425498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.24 % (3425498)CaDiCaL version: 2.1.3
% 3.56/1.24 % (3425498)Termination reason: Instruction limit
% 3.56/1.24 % (3425498)Termination phase: Saturation
% 3.56/1.24 % (3425498)Time elapsed: 0.003 s
% 3.56/1.24 % (3425498)Peak memory usage: 88 MB
% 3.56/1.24 % (3425498)Instructions burned: 4 (million)
% 3.56/1.24 % (3425497)Instruction limit reached!
% 3.56/1.24 % (3425497)------------------------------
% 3.56/1.24 % (3425497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.24 % (3425497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.24 % (3425497)CaDiCaL version: 2.1.3
% 3.56/1.24 % (3425497)Termination reason: Instruction limit
% 3.56/1.24 % (3425497)Termination phase: Saturation
% 3.56/1.24 % (3425497)Time elapsed: 0.006 s
% 3.56/1.24 % (3425497)Peak memory usage: 88 MB
% 3.56/1.24 % (3425497)Instructions burned: 7 (million)
% 3.56/1.24 % (3425494)Instruction limit reached!
% 3.56/1.24 % (3425494)------------------------------
% 3.56/1.24 % (3425494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.24 % (3425494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.24 % (3425494)CaDiCaL version: 2.1.3
% 3.56/1.24 % (3425494)Termination reason: Instruction limit
% 3.56/1.24 % (3425494)Termination phase: Saturation
% 3.56/1.24 % (3425494)Time elapsed: 0.030 s
% 3.56/1.24 % (3425494)Peak memory usage: 115 MB
% 3.56/1.24 % (3425494)Instructions burned: 12 (million)
% 3.56/1.24 % (3425500)Instruction limit reached!
% 3.56/1.24 % (3425500)------------------------------
% 3.56/1.24 % (3425500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.24 % (3425500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.24 % (3425500)CaDiCaL version: 2.1.3
% 3.56/1.24 % (3425500)Termination reason: Instruction limit
% 3.56/1.24 % (3425500)Termination phase: Saturation
% 3.56/1.24 % (3425500)Time elapsed: 0.044 s
% 3.56/1.24 % (3425500)Peak memory usage: 116 MB
% 3.56/1.24 % (3425500)Instructions burned: 33 (million)
% 3.56/1.24 % (3425499)Instruction limit reached!
% 3.56/1.24 % (3425499)------------------------------
% 3.56/1.24 % (3425499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.24 % (3425499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.24 % (3425499)CaDiCaL version: 2.1.3
% 3.56/1.24 % (3425499)Termination reason: Instruction limit
% 3.56/1.24 % (3425499)Termination phase: Saturation
% 3.56/1.24 % (3425499)Time elapsed: 0.055 s
% 3.56/1.24 % (3425499)Peak memory usage: 116 MB
% 3.56/1.24 % (3425499)Instructions burned: 46 (million)
% 3.56/1.24 % (3425495)Instruction limit reached!
% 3.56/1.24 % (3425495)------------------------------
% 3.56/1.24 % (3425495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.24 % (3425495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425495)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425495)Termination reason: Instruction limit
% 4.46/1.38 % (3425495)Termination phase: Saturation
% 4.46/1.38 % (3425495)Time elapsed: 0.120 s
% 4.46/1.38 % (3425495)Peak memory usage: 117 MB
% 4.46/1.38 % (3425495)Instructions burned: 310 (million)
% 4.46/1.38 % (3425509)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=3666640848:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.46/1.38 % (3425508)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=209908775:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.46/1.38 % (3425508)Instruction limit reached!
% 4.46/1.38 % (3425508)------------------------------
% 4.46/1.38 % (3425508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.38 % (3425508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425508)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425508)Termination reason: Instruction limit
% 4.46/1.38 % (3425508)Termination phase: Saturation
% 4.46/1.38 % (3425508)Time elapsed: 0.011 s
% 4.46/1.38 % (3425508)Peak memory usage: 88 MB
% 4.46/1.38 % (3425508)Instructions burned: 14 (million)
% 4.46/1.38 % (3425496)Instruction limit reached!
% 4.46/1.38 % (3425496)------------------------------
% 4.46/1.38 % (3425496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.38 % (3425496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425496)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425496)Termination reason: Instruction limit
% 4.46/1.38 % (3425496)Termination phase: Saturation
% 4.46/1.38 % (3425496)Time elapsed: 0.163 s
% 4.46/1.38 % (3425496)Peak memory usage: 119 MB
% 4.46/1.38 % (3425496)Instructions burned: 202 (million)
% 4.46/1.38 % (3425509)Instruction limit reached!
% 4.46/1.38 % (3425509)------------------------------
% 4.46/1.38 % (3425509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.38 % (3425509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425509)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425509)Termination reason: Instruction limit
% 4.46/1.38 % (3425509)Termination phase: Saturation
% 4.46/1.38 % (3425509)Time elapsed: 0.023 s
% 4.46/1.38 % (3425509)Peak memory usage: 88 MB
% 4.46/1.38 % (3425509)Instructions burned: 30 (million)
% 4.46/1.38 % (3425513)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2117209294:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.46/1.38 % (3425510)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=246706151:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.46/1.38 % (3425510)Instruction limit reached!
% 4.46/1.38 % (3425510)------------------------------
% 4.46/1.38 % (3425510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.38 % (3425510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425510)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425510)Termination reason: Instruction limit
% 4.46/1.38 % (3425510)Termination phase: Saturation
% 4.46/1.38 % (3425510)Time elapsed: 0.011 s
% 4.46/1.38 % (3425510)Peak memory usage: 90 MB
% 4.46/1.38 % (3425510)Instructions burned: 16 (million)
% 4.46/1.38 % (3425511)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1184000819:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.46/1.38 % (3425513)Instruction limit reached!
% 4.46/1.38 % (3425513)------------------------------
% 4.46/1.38 % (3425513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.38 % (3425513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425513)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425513)Termination reason: Instruction limit
% 4.46/1.38 % (3425513)Termination phase: Saturation
% 4.46/1.38 % (3425513)Time elapsed: 0.027 s
% 4.46/1.38 % (3425513)Peak memory usage: 89 MB
% 4.46/1.38 % (3425513)Instructions burned: 88 (million)
% 4.46/1.38 % (3425511)Instruction limit reached!
% 4.46/1.38 % (3425511)------------------------------
% 4.46/1.38 % (3425511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/1.38 % (3425511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/1.38 % (3425511)CaDiCaL version: 2.1.3
% 4.46/1.38 % (3425511)Termination reason: Instruction limit
% 5.60/1.53 % (3425511)Termination phase: Saturation
% 5.60/1.53 % (3425511)Time elapsed: 0.021 s
% 5.60/1.53 % (3425511)Peak memory usage: 89 MB
% 5.60/1.53 % (3425511)Instructions burned: 25 (million)
% 5.60/1.53 % (3425512)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=2029241168:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 5.60/1.53 % (3425512)Instruction limit reached!
% 5.60/1.53 % (3425512)------------------------------
% 5.60/1.53 % (3425512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.53 % (3425512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.53 % (3425512)CaDiCaL version: 2.1.3
% 5.60/1.53 % (3425512)Termination reason: Instruction limit
% 5.60/1.53 % (3425512)Termination phase: Saturation
% 5.60/1.53 % (3425512)Time elapsed: 0.020 s
% 5.60/1.53 % (3425512)Peak memory usage: 90 MB
% 5.60/1.53 % (3425512)Instructions burned: 28 (million)
% 5.60/1.53 % (3425519)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1675718588:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.60/1.53 % (3425520)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3256355953:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.60/1.53 % (3425516)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=300476606:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.60/1.53 % (3425516)Instruction limit reached!
% 5.60/1.53 % (3425516)------------------------------
% 5.60/1.53 % (3425516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.53 % (3425516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.53 % (3425516)CaDiCaL version: 2.1.3
% 5.60/1.53 % (3425516)Termination reason: Instruction limit
% 5.60/1.53 % (3425516)Termination phase: Property scanning
% 5.60/1.53 % (3425516)Time elapsed: 0.002 s
% 5.60/1.53 % (3425516)Peak memory usage: 86 MB
% 5.60/1.53 % (3425516)Instructions burned: 2 (million)
% 5.60/1.53 % (3425520)Instruction limit reached!
% 5.60/1.53 % (3425520)------------------------------
% 5.60/1.53 % (3425520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.53 % (3425520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.53 % (3425520)CaDiCaL version: 2.1.3
% 5.60/1.53 % (3425520)Termination reason: Instruction limit
% 5.60/1.53 % (3425520)Termination phase: Saturation
% 5.60/1.53 % (3425520)Time elapsed: 0.003 s
% 5.60/1.53 % (3425520)Peak memory usage: 87 MB
% 5.60/1.53 % (3425520)Instructions burned: 5 (million)
% 5.60/1.53 % (3425523)lrs+10_1_thi=all:si=on:fd=off:random_seed=2344610157:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.60/1.53 % (3425522)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2652543170:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.60/1.53 % (3425523)Instruction limit reached!
% 5.60/1.53 % (3425523)------------------------------
% 5.60/1.53 % (3425523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.53 % (3425523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.53 % (3425523)CaDiCaL version: 2.1.3
% 5.60/1.53 % (3425523)Termination reason: Instruction limit
% 5.60/1.53 % (3425523)Termination phase: Saturation
% 5.60/1.53 % (3425523)Time elapsed: 0.036 s
% 5.60/1.53 % (3425523)Peak memory usage: 116 MB
% 5.60/1.53 % (3425523)Instructions burned: 53 (million)
% 5.60/1.53 % (3425524)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=332551737:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.60/1.53 % (3425524)Instruction limit reached!
% 5.60/1.53 % (3425524)------------------------------
% 5.60/1.53 % (3425524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.53 % (3425524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.53 % (3425524)CaDiCaL version: 2.1.3
% 5.60/1.53 % (3425524)Termination reason: Instruction limit
% 5.60/1.53 % (3425524)Termination phase: Saturation
% 5.60/1.53 % (3425524)Time elapsed: 0.006 s
% 5.60/1.53 % (3425524)Peak memory usage: 88 MB
% 5.60/1.53 % (3425524)Instructions burned: 9 (million)
% 5.60/1.53 % (3425519)Instruction limit reached!
% 5.75/1.69 % (3425519)------------------------------
% 5.75/1.69 % (3425519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425519)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425519)Termination reason: Instruction limit
% 5.75/1.69 % (3425519)Termination phase: Saturation
% 5.75/1.69 % (3425519)Time elapsed: 0.098 s
% 5.75/1.69 % (3425519)Peak memory usage: 90 MB
% 5.75/1.69 % (3425519)Instructions burned: 182 (million)
% 5.75/1.69 % (3425526)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=155761995:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.75/1.69 % (3425526)Instruction limit reached!
% 5.75/1.69 % (3425526)------------------------------
% 5.75/1.69 % (3425526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425526)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425526)Termination reason: Instruction limit
% 5.75/1.69 % (3425526)Termination phase: Property scanning
% 5.75/1.69 % (3425526)Time elapsed: 0.002 s
% 5.75/1.69 % (3425526)Peak memory usage: 86 MB
% 5.75/1.69 % (3425526)Instructions burned: 2 (million)
% 5.75/1.69 % (3425522)Instruction limit reached!
% 5.75/1.69 % (3425522)------------------------------
% 5.75/1.69 % (3425522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425522)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425522)Termination reason: Instruction limit
% 5.75/1.69 % (3425522)Termination phase: Saturation
% 5.75/1.69 % (3425522)Time elapsed: 0.093 s
% 5.75/1.69 % (3425522)Peak memory usage: 134 MB
% 5.75/1.69 % (3425522)Instructions burned: 66 (million)
% 5.75/1.69 % (3425531)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1588467514:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.75/1.69 % (3425533)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1355912165:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 5.75/1.69 % (3425531)Instruction limit reached!
% 5.75/1.69 % (3425531)------------------------------
% 5.75/1.69 % (3425531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425531)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425531)Termination reason: Instruction limit
% 5.75/1.69 % (3425531)Termination phase: Property scanning
% 5.75/1.69 % (3425531)Time elapsed: 0.002 s
% 5.75/1.69 % (3425531)Peak memory usage: 86 MB
% 5.75/1.69 % (3425531)Instructions burned: 2 (million)
% 5.75/1.69 % (3425534)dis+10_1_si=on:random_seed=270160886:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 5.75/1.69 % (3425534)Instruction limit reached!
% 5.75/1.69 % (3425534)------------------------------
% 5.75/1.69 % (3425534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425534)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425534)Termination reason: Instruction limit
% 5.75/1.69 % (3425534)Termination phase: Saturation
% 5.75/1.69 % (3425534)Time elapsed: 0.004 s
% 5.75/1.69 % (3425534)Peak memory usage: 88 MB
% 5.75/1.69 % (3425534)Instructions burned: 10 (million)
% 5.75/1.69 % (3425536)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2305388559:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 5.75/1.69 % (3425538)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3708686788:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 5.75/1.69 % (3425539)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1819870125:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 5.75/1.69 % (3425540)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2207735622:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 5.75/1.69 % (3425539)Instruction limit reached!
% 5.75/1.69 % (3425539)------------------------------
% 5.75/1.69 % (3425539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425539)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425539)Termination reason: Instruction limit
% 5.75/1.69 % (3425539)Termination phase: Property scanning
% 5.75/1.69 % (3425539)Time elapsed: 0.002 s
% 5.75/1.69 % (3425539)Peak memory usage: 86 MB
% 5.75/1.69 % (3425539)Instructions burned: 2 (million)
% 5.75/1.69 % (3425536)Instruction limit reached!
% 5.75/1.69 % (3425536)------------------------------
% 5.75/1.69 % (3425536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425536)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425536)Termination reason: Instruction limit
% 5.75/1.69 % (3425536)Termination phase: Saturation
% 5.75/1.69 % (3425536)Time elapsed: 0.018 s
% 5.75/1.69 % (3425536)Peak memory usage: 89 MB
% 5.75/1.69 % (3425536)Instructions burned: 26 (million)
% 5.75/1.69 % (3425540)Instruction limit reached!
% 5.75/1.69 % (3425540)------------------------------
% 5.75/1.69 % (3425540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425540)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425540)Termination reason: Instruction limit
% 5.75/1.69 % (3425540)Termination phase: Saturation
% 5.75/1.69 % (3425540)Time elapsed: 0.006 s
% 5.75/1.69 % (3425540)Peak memory usage: 88 MB
% 5.75/1.69 % (3425540)Instructions burned: 8 (million)
% 5.75/1.69 % (3425538)Instruction limit reached!
% 5.75/1.69 % (3425538)------------------------------
% 5.75/1.69 % (3425538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425538)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425538)Termination reason: Instruction limit
% 5.75/1.69 % (3425538)Termination phase: Saturation
% 5.75/1.69 % (3425538)Time elapsed: 0.016 s
% 5.75/1.69 % (3425538)Peak memory usage: 89 MB
% 5.75/1.69 % (3425538)Instructions burned: 37 (million)
% 5.75/1.69 % (3425533)Instruction limit reached!
% 5.75/1.69 % (3425533)------------------------------
% 5.75/1.69 % (3425533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425533)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425533)Termination reason: Instruction limit
% 5.75/1.69 % (3425533)Termination phase: Saturation
% 5.75/1.69 % (3425533)Time elapsed: 0.114 s
% 5.75/1.69 % (3425533)Peak memory usage: 117 MB
% 5.75/1.69 % (3425533)Instructions burned: 128 (million)
% 5.75/1.69 % (3425544)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1180227969:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 5.75/1.69 % (3425545)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3020349067:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 5.75/1.69 % (3425545)Instruction limit reached!
% 5.75/1.69 % (3425545)------------------------------
% 5.75/1.69 % (3425545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425545)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425545)Termination reason: Instruction limit
% 5.75/1.69 % (3425545)Termination phase: Saturation
% 5.75/1.69 % (3425545)Time elapsed: 0.030 s
% 5.75/1.69 % (3425545)Peak memory usage: 113 MB
% 5.75/1.69 % (3425545)Instructions burned: 13 (million)
% 5.75/1.69 % (3425553)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=2660613118:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 5.75/1.69 % (3425550)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1442847612:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 5.75/1.69 % (3425551)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=686876900:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 5.75/1.69 % (3425553)First to succeed.
% 5.75/1.69 % (3425553)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3425451"
% 5.75/1.69 % (3425551)Instruction limit reached!
% 5.75/1.69 % (3425551)------------------------------
% 5.75/1.69 % (3425551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425551)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425551)Termination reason: Instruction limit
% 5.75/1.69 % (3425551)Termination phase: Saturation
% 5.75/1.69 % (3425551)Time elapsed: 0.008 s
% 5.75/1.69 % (3425551)Peak memory usage: 88 MB
% 5.75/1.69 % (3425551)Instructions burned: 10 (million)
% 5.75/1.69 % (3425552)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1707054390:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 5.75/1.69 % (3425554)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=1286369236:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 5.75/1.69 % (3425550)Refutation not found, incomplete strategy
% 5.75/1.69 % (3425550)------------------------------
% 5.75/1.69 % (3425550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425550)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425550)Termination reason: Refutation not found, incomplete strategy
% 5.75/1.69 % (3425550)Time elapsed: 0.073 s
% 5.75/1.69 % (3425550)Peak memory usage: 116 MB
% 5.75/1.69 % (3425550)Instructions burned: 66 (million)
% 5.75/1.69 % (3425544)Instruction limit reached!
% 5.75/1.69 % (3425544)------------------------------
% 5.75/1.69 % (3425544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425544)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425544)Termination reason: Instruction limit
% 5.75/1.69 % (3425544)Termination phase: Saturation
% 5.75/1.69 % (3425544)Time elapsed: 0.197 s
% 5.75/1.69 % (3425544)Peak memory usage: 91 MB
% 5.75/1.69 % (3425544)Instructions burned: 371 (million)
% 5.75/1.69 % (3425552)Instruction limit reached!
% 5.75/1.69 % (3425552)------------------------------
% 5.75/1.69 % (3425552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.75/1.69 % (3425552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.69 % (3425552)CaDiCaL version: 2.1.3
% 5.75/1.69 % (3425552)Termination reason: Instruction limit
% 5.75/1.69 % (3425552)Termination phase: Saturation
% 5.75/1.69 % (3425552)Time elapsed: 0.094 s
% 5.75/1.69 % (3425552)Peak memory usage: 133 MB
% 5.75/1.69 % (3425552)Instructions burned: 71 (million)
% 5.75/1.69 % (3425558)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1349887652:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 5.75/1.69 % (3425553)Refutation found. Thanks to Tanya!
% 5.75/1.69 % SZS status Theorem for theBenchmark
% 5.75/1.69 % SZS output start Proof for theBenchmark
% See solution above
% 7.75/1.88 % (3425553)------------------------------
% 7.75/1.88 % (3425553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/1.88 % (3425553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/1.88 % (3425553)CaDiCaL version: 2.1.3
% 7.75/1.88 % (3425553)Termination reason: Refutation
% 7.75/1.88 % (3425553)Time elapsed: 0.029 s
% 7.75/1.88 % (3425553)Peak memory usage: 91 MB
% 7.75/1.88 % (3425553)Instructions burned: 75 (million)
% 7.75/1.88 % (3425553)------------------------------
% 7.75/1.88 % (3425553)------------------------------
% 7.75/1.88 % (3425451)Success in time 1.02 s
% 7.75/1.88 % Vampire exiting
%------------------------------------------------------------------------------