%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW594_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 : n015.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:53 PM UTC 2026
% Result : Theorem 25.05s 5.01s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of formulae : 99 ( 25 unt; 0 typ; 13 def)
% Number of atoms : 585 ( 54 equ)
% Maximal formula atoms : 37 ( 5 avg)
% Number of connectives : 716 ( 230 ~; 109 |; 296 &)
% ( 19 <=>; 62 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 7 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 618 ( 307 atm; 37 fun; 92 num; 182 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 : 34 ( 30 usr; 14 prp; 0-7 aty)
% Number of functors : 59 ( 53 usr; 24 con; 0-7 aty)
% Number of variables : 244 ( 204 !; 40 ?; 244 :)
% 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,
array_int: $tType ).
tff(type_def_10,type,
map_int_int: $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,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
occ: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_32,type,
usN: $int ).
tff(func_def_33,type,
f: $int ).
tff(func_def_34,type,
t2tb1: array_int > uni ).
tff(func_def_35,type,
tb2t1: uni > array_int ).
tff(func_def_36,type,
t2tb2: map_int_int > uni ).
tff(func_def_37,type,
tb2t2: uni > map_int_int ).
tff(func_def_39,type,
sK1: ( $int * $int * array_int * $int ) > $int ).
tff(func_def_40,type,
sK2: ( ty * $int * uni * $int * uni ) > $int ).
tff(func_def_41,type,
sK3: ( $int * ty * $int * uni * uni ) > $int ).
tff(func_def_42,type,
sK4: ( $int * $int * uni * uni * ty ) > uni ).
tff(func_def_43,type,
sK5: map_int_int ).
tff(func_def_44,type,
sK6: $int ).
tff(func_def_45,type,
sK7: $int ).
tff(func_def_46,type,
sK8: $int ).
tff(func_def_47,type,
sK9: map_int_int ).
tff(func_def_48,type,
sK10: $int ).
tff(func_def_49,type,
sK11: $int ).
tff(func_def_50,type,
sK12: map_int_int ).
tff(func_def_51,type,
sK13: $int ).
tff(func_def_52,type,
sK14: $int ).
tff(func_def_53,type,
sK15: $int ).
tff(func_def_54,type,
sK16: ( $int * uni * uni * $int * ty ) > $int ).
tff(func_def_55,type,
sK17: ( $int * $int * $int * array_int ) > $int ).
tff(func_def_56,type,
sK18: ( ty * $int * $int * uni * uni ) > $int ).
tff(func_def_57,type,
sK19: ( $int * $int * $int * uni * uni * ty ) > $int ).
tff(func_def_58,type,
sK20: ( $int * $int * uni * ty * uni * $int * $int ) > $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_4,type,
permut: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_5,type,
map_eq_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_6,type,
array_eq_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_7,type,
array_eq: ( ty * uni * uni ) > $o ).
tff(pred_def_8,type,
exchange: ( ty * uni * uni * $int * $int * $int * $int ) > $o ).
tff(pred_def_9,type,
exchange1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_10,type,
permut1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_11,type,
permut_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_12,type,
permut_all: ( ty * uni * uni ) > $o ).
tff(pred_def_13,type,
found: array_int > $o ).
tff(pred_def_14,type,
m_invariant: ( $int * array_int ) > $o ).
tff(pred_def_15,type,
n_invariant: ( $int * array_int ) > $o ).
tff(pred_def_16,type,
i_invariant: ( $int * $int * $int * $int * array_int ) > $o ).
tff(pred_def_17,type,
j_invariant: ( $int * $int * $int * $int * array_int ) > $o ).
tff(pred_def_18,type,
termination: ( $int * $int * $int * $int * $int * array_int ) > $o ).
tff(pred_def_19,type,
sP0: ( $int * $int * uni * ty * uni * $int * $int ) > $o ).
tff(f22,axiom,
! [X2: uni,X1: $int,X0: ty] :
( sort(map(int,X0),X2)
=> ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def) ).
tff(f28,axiom,
! [X1: uni,X2: $int,X0: ty] : ( get1(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_def) ).
tff(f60,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f65,axiom,
! [X2: $int,X4: array_int,X3: $int,X0: $int,X1: $int] :
( j_invariant(X0,X1,X2,X3,X4)
<=> ( $lesseq(X2,X1)
& ! [X5: $int] :
( ( $lesseq(X5,usN)
& $less(X2,X5) )
=> $lesseq(X3,tb2t(get1(int,t2tb1(X4),X5))) )
& ( $lesseq(X0,X2)
=> ? [X5: $int] :
( $lesseq(tb2t(get1(int,t2tb1(X4),X5)),X3)
& $lesseq(X0,X5)
& $lesseq(X5,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',j_invariant_def) ).
tff(f66,axiom,
! [X0: $int,X2: $int,X3: $int,X1: $int,X5: array_int,X4: $int] :
( termination(X0,X1,X2,X3,X4,X5)
<=> ( ( $less(X1,X3)
& $less(X2,X0) )
| ( $lesseq(f,X1)
& $lesseq(X0,f)
& ( tb2t(get1(int,t2tb1(X5),f)) = X4 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',termination_def) ).
tff(f67,axiom,
! [X0: map_int_int] : sort(map(int,int),t2tb2(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f70,conjecture,
! [X0: $int,X1: map_int_int] :
( ( $lesseq(0,X0)
& ( X0 = $sum(usN,1) ) )
=> ! [X4: map_int_int,X3: $int,X2: $int] :
( ( $lesseq(1,X3)
& $lesseq(X2,usN)
& permut_all(int,mk_array(int,X0,t2tb2(X4)),mk_array(int,X0,t2tb2(X1)))
& n_invariant(X2,tb2t1(mk_array(int,X0,t2tb2(X4))))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X4)))) )
=> ( $less(X3,X2)
=> ( ( $less(f,X0)
& $lesseq(0,X0)
& $lesseq(0,f) )
=> ! [X7: map_int_int,X6: $int,X5: $int] :
( ( j_invariant(X3,X2,X5,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& termination(X6,X5,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& permut_all(int,mk_array(int,X0,t2tb2(X7)),mk_array(int,X0,t2tb2(X1)))
& $lesseq(X6,$sum(usN,1))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(0,X5)
& i_invariant(X3,X2,X6,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& n_invariant(X2,tb2t1(mk_array(int,X0,t2tb2(X7)))) )
=> ( $lesseq(X6,X5)
=> ! [X8: $int] :
( ( $lesseq(X6,X8)
& i_invariant(X3,X2,X8,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(X8,X2)
& termination(X8,X5,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7)))) )
=> ( ( $lesseq(0,X8)
& $less(X8,X0)
& $lesseq(0,X0) )
=> ( ~ $less(tb2t(get(int,int,t2tb2(X7),t2tb(X8))),tb2t(get(int,int,t2tb2(X4),t2tb(f))))
=> ! [X9: $int] :
( ( termination(X8,X9,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(X3,X9)
& j_invariant(X3,X2,X9,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(X9,X5) )
=> ( ( $less(X9,X0)
& $lesseq(0,X9) )
=> ( $less(tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t(get(int,int,t2tb2(X7),t2tb(X9))))
=> ! [X10: $int] :
( ( X10 = $difference(X9,1) )
=> termination(X8,X10,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_find) ).
tff(f71,negated_conjecture,
~ ! [X0: $int,X1: map_int_int] :
( ( $lesseq(0,X0)
& ( X0 = $sum(usN,1) ) )
=> ! [X4: map_int_int,X3: $int,X2: $int] :
( ( $lesseq(1,X3)
& $lesseq(X2,usN)
& permut_all(int,mk_array(int,X0,t2tb2(X4)),mk_array(int,X0,t2tb2(X1)))
& n_invariant(X2,tb2t1(mk_array(int,X0,t2tb2(X4))))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X4)))) )
=> ( $less(X3,X2)
=> ( ( $less(f,X0)
& $lesseq(0,X0)
& $lesseq(0,f) )
=> ! [X7: map_int_int,X6: $int,X5: $int] :
( ( j_invariant(X3,X2,X5,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& termination(X6,X5,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& permut_all(int,mk_array(int,X0,t2tb2(X7)),mk_array(int,X0,t2tb2(X1)))
& $lesseq(X6,$sum(usN,1))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(0,X5)
& i_invariant(X3,X2,X6,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& n_invariant(X2,tb2t1(mk_array(int,X0,t2tb2(X7)))) )
=> ( $lesseq(X6,X5)
=> ! [X8: $int] :
( ( $lesseq(X6,X8)
& i_invariant(X3,X2,X8,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(X8,X2)
& termination(X8,X5,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7)))) )
=> ( ( $lesseq(0,X8)
& $less(X8,X0)
& $lesseq(0,X0) )
=> ( ~ $less(tb2t(get(int,int,t2tb2(X7),t2tb(X8))),tb2t(get(int,int,t2tb2(X4),t2tb(f))))
=> ! [X9: $int] :
( ( termination(X8,X9,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(X3,X9)
& j_invariant(X3,X2,X9,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& $lesseq(X9,X5) )
=> ( ( $less(X9,X0)
& $lesseq(0,X9) )
=> ( $less(tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t(get(int,int,t2tb2(X7),t2tb(X9))))
=> ! [X10: $int] :
( ( X10 = $difference(X9,1) )
=> termination(X8,X10,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f70]) ).
tff(f78,plain,
! [X0: $int,X2: $int,X3: $int,X1: $int,X5: array_int,X4: $int] :
( termination(X0,X1,X2,X3,X4,X5)
<=> ( ( $less(X1,X3)
& $less(X2,X0) )
| ( ~ $less(X1,f)
& ~ $less(f,X0)
& ( tb2t(get1(int,t2tb1(X5),f)) = X4 ) ) ) ),
inference(theory_normalization,[],[f66]) ).
tff(f85,plain,
~ ! [X0: $int,X1: map_int_int] :
( ( ( X0 = $sum(usN,1) )
& ~ $less(X0,0) )
=> ! [X4: map_int_int,X3: $int,X2: $int] :
( ( ~ $less(X3,1)
& ~ $less(usN,X2)
& permut_all(int,mk_array(int,X0,t2tb2(X4)),mk_array(int,X0,t2tb2(X1)))
& n_invariant(X2,tb2t1(mk_array(int,X0,t2tb2(X4))))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X4)))) )
=> ( $less(X3,X2)
=> ( ( $less(f,X0)
& ~ $less(X0,0)
& ~ $less(f,0) )
=> ! [X7: map_int_int,X6: $int,X5: $int] :
( ( j_invariant(X3,X2,X5,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& termination(X6,X5,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& permut_all(int,mk_array(int,X0,t2tb2(X7)),mk_array(int,X0,t2tb2(X1)))
& ~ $less($sum(usN,1),X6)
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X7))))
& ~ $less(X5,0)
& i_invariant(X3,X2,X6,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& n_invariant(X2,tb2t1(mk_array(int,X0,t2tb2(X7)))) )
=> ( ~ $less(X5,X6)
=> ! [X8: $int] :
( ( ~ $less(X8,X6)
& i_invariant(X3,X2,X8,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& ~ $less(X2,X8)
& termination(X8,X5,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7)))) )
=> ( ( ~ $less(X8,0)
& $less(X8,X0)
& ~ $less(X0,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb2(X7),t2tb(X8))),tb2t(get(int,int,t2tb2(X4),t2tb(f))))
=> ! [X9: $int] :
( ( termination(X8,X9,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& ~ $less(X9,X3)
& j_invariant(X3,X2,X9,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7))))
& ~ $less(X5,X9) )
=> ( ( $less(X9,X0)
& ~ $less(X9,0) )
=> ( $less(tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t(get(int,int,t2tb2(X7),t2tb(X9))))
=> ! [X10: $int] :
( ( $sum(X9,$uminus(1)) = X10 )
=> termination(X8,X10,X3,X2,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X7)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f71]) ).
tff(f90,plain,
! [X2: $int,X4: array_int,X3: $int,X0: $int,X1: $int] :
( j_invariant(X0,X1,X2,X3,X4)
<=> ( ~ $less(X1,X2)
& ! [X5: $int] :
( ( ~ $less(usN,X5)
& $less(X2,X5) )
=> ~ $less(tb2t(get1(int,t2tb1(X4),X5)),X3) )
& ( ~ $less(X2,X0)
=> ? [X5: $int] :
( ~ $less(X3,tb2t(get1(int,t2tb1(X4),X5)))
& ~ $less(X5,X0)
& ~ $less(X2,X5) ) ) ) ),
inference(theory_normalization,[],[f65]) ).
tff(f98,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f127,plain,
! [X0: $int,X4: array_int,X3: $int,X5: $int,X1: $int,X2: $int] :
( ( ( ( tb2t(get1(int,t2tb1(X4),f)) = X5 )
& ~ $less(f,X0)
& ~ $less(X3,f) )
| ( $less(X3,X2)
& $less(X1,X0) ) )
<=> termination(X0,X3,X1,X2,X5,X4) ),
inference(rectify,[],[f78]) ).
tff(f140,plain,
! [X0: uni,X2: ty,X1: $int] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get1(X2,X0,X1) ),
inference(rectify,[],[f28]) ).
tff(f142,plain,
~ ! [X1: map_int_int,X0: $int] :
( ( ( X0 = $sum(usN,1) )
& ~ $less(X0,0) )
=> ! [X2: map_int_int,X3: $int,X4: $int] :
( ( ~ $less(X3,1)
& n_invariant(X4,tb2t1(mk_array(int,X0,t2tb2(X2))))
& permut_all(int,mk_array(int,X0,t2tb2(X2)),mk_array(int,X0,t2tb2(X1)))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X2))))
& ~ $less(usN,X4) )
=> ( $less(X3,X4)
=> ( ( $less(f,X0)
& ~ $less(X0,0)
& ~ $less(f,0) )
=> ! [X5: map_int_int,X7: $int,X6: $int] :
( ( i_invariant(X3,X4,X6,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& termination(X6,X7,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& n_invariant(X4,tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less($sum(usN,1),X6)
& permut_all(int,mk_array(int,X0,t2tb2(X5)),mk_array(int,X0,t2tb2(X1)))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X5))))
& j_invariant(X3,X4,X7,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X7,0) )
=> ( ~ $less(X7,X6)
=> ! [X8: $int] :
( ( ~ $less(X4,X8)
& termination(X8,X7,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& i_invariant(X3,X4,X8,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X8,X6) )
=> ( ( ~ $less(X8,0)
& $less(X8,X0)
& ~ $less(X0,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb2(X5),t2tb(X8))),tb2t(get(int,int,t2tb2(X2),t2tb(f))))
=> ! [X9: $int] :
( ( termination(X8,X9,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X9,X3)
& ~ $less(X7,X9)
& j_invariant(X3,X4,X9,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5)))) )
=> ( ( $less(X9,X0)
& ~ $less(X9,0) )
=> ( $less(tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t(get(int,int,t2tb2(X5),t2tb(X9))))
=> ! [X10: $int] :
( ( $sum(X9,$uminus(1)) = X10 )
=> termination(X8,X10,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f85]) ).
tff(f152,plain,
! [X3: $int,X0: $int,X2: $int,X4: $int,X1: array_int] :
( ( ( ~ $less(X0,X3)
=> ? [X6: $int] :
( ~ $less(X6,X3)
& ~ $less(X0,X6)
& ~ $less(X2,tb2t(get1(int,t2tb1(X1),X6))) ) )
& ~ $less(X4,X0)
& ! [X5: $int] :
( ( ~ $less(usN,X5)
& $less(X0,X5) )
=> ~ $less(tb2t(get1(int,t2tb1(X1),X5)),X2) ) )
<=> j_invariant(X3,X4,X0,X2,X1) ),
inference(rectify,[],[f90]) ).
tff(f166,plain,
! [X3: $int,X0: $int,X2: $int,X4: $int,X1: array_int] :
( j_invariant(X3,X4,X0,X2,X1)
=> ( ( ~ $less(X0,X3)
=> ? [X6: $int] :
( ~ $less(X6,X3)
& ~ $less(X0,X6)
& ~ $less(X2,tb2t(get1(int,t2tb1(X1),X6))) ) )
& ~ $less(X4,X0)
& ! [X5: $int] :
( ( ~ $less(usN,X5)
& $less(X0,X5) )
=> ~ $less(tb2t(get1(int,t2tb1(X1),X5)),X2) ) ) ),
inference(unused_predicate_definition_removal,[],[f152]) ).
tff(f172,plain,
? [X1: map_int_int,X0: $int] :
( ? [X2: map_int_int,X3: $int,X4: $int] :
( ? [X5: map_int_int,X7: $int,X6: $int] :
( ? [X8: $int] :
( ? [X9: $int] :
( ? [X10: $int] :
( ~ termination(X8,X10,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ( $sum(X9,$uminus(1)) = X10 ) )
& $less(tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t(get(int,int,t2tb2(X5),t2tb(X9))))
& $less(X9,X0)
& ~ $less(X9,0)
& termination(X8,X9,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X9,X3)
& ~ $less(X7,X9)
& j_invariant(X3,X4,X9,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5)))) )
& ~ $less(tb2t(get(int,int,t2tb2(X5),t2tb(X8))),tb2t(get(int,int,t2tb2(X2),t2tb(f))))
& ~ $less(X8,0)
& $less(X8,X0)
& ~ $less(X0,0)
& ~ $less(X4,X8)
& termination(X8,X7,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& i_invariant(X3,X4,X8,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X8,X6) )
& ~ $less(X7,X6)
& i_invariant(X3,X4,X6,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& termination(X6,X7,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& n_invariant(X4,tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less($sum(usN,1),X6)
& permut_all(int,mk_array(int,X0,t2tb2(X5)),mk_array(int,X0,t2tb2(X1)))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X5))))
& j_invariant(X3,X4,X7,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X7,0) )
& $less(f,X0)
& ~ $less(X0,0)
& ~ $less(f,0)
& $less(X3,X4)
& ~ $less(X3,1)
& n_invariant(X4,tb2t1(mk_array(int,X0,t2tb2(X2))))
& permut_all(int,mk_array(int,X0,t2tb2(X2)),mk_array(int,X0,t2tb2(X1)))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X2))))
& ~ $less(usN,X4) )
& ( X0 = $sum(usN,1) )
& ~ $less(X0,0) ),
inference(ennf_transformation,[],[f142]) ).
tff(f173,plain,
? [X1: map_int_int,X0: $int] :
( ( X0 = $sum(usN,1) )
& ~ $less(X0,0)
& ? [X3: $int,X4: $int,X2: map_int_int] :
( ~ $less(f,0)
& ~ $less(X0,0)
& permut_all(int,mk_array(int,X0,t2tb2(X2)),mk_array(int,X0,t2tb2(X1)))
& ~ $less(X3,1)
& $less(f,X0)
& $less(X3,X4)
& ~ $less(usN,X4)
& n_invariant(X4,tb2t1(mk_array(int,X0,t2tb2(X2))))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X2))))
& ? [X6: $int,X7: $int,X5: map_int_int] :
( i_invariant(X3,X4,X6,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& permut_all(int,mk_array(int,X0,t2tb2(X5)),mk_array(int,X0,t2tb2(X1)))
& ~ $less(X7,X6)
& ? [X8: $int] :
( $less(X8,X0)
& i_invariant(X3,X4,X8,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ? [X9: $int] :
( $less(tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t(get(int,int,t2tb2(X5),t2tb(X9))))
& termination(X8,X9,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X9,0)
& ~ $less(X7,X9)
& $less(X9,X0)
& ~ $less(X9,X3)
& j_invariant(X3,X4,X9,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ? [X10: $int] :
( ~ termination(X8,X10,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ( $sum(X9,$uminus(1)) = X10 ) ) )
& termination(X8,X7,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less(X0,0)
& ~ $less(X8,X6)
& ~ $less(X4,X8)
& ~ $less(X8,0)
& ~ $less(tb2t(get(int,int,t2tb2(X5),t2tb(X8))),tb2t(get(int,int,t2tb2(X2),t2tb(f)))) )
& ~ $less(X7,0)
& termination(X6,X7,X3,X4,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& m_invariant(X3,tb2t1(mk_array(int,X0,t2tb2(X5))))
& j_invariant(X3,X4,X7,tb2t(get(int,int,t2tb2(X2),t2tb(f))),tb2t1(mk_array(int,X0,t2tb2(X5))))
& ~ $less($sum(usN,1),X6)
& n_invariant(X4,tb2t1(mk_array(int,X0,t2tb2(X5)))) ) ) ),
inference(flattening,[],[f172]) ).
tff(f177,plain,
! [X3: $int,X0: $int,X2: $int,X4: $int,X1: array_int] :
( ( ( ? [X6: $int] :
( ~ $less(X6,X3)
& ~ $less(X0,X6)
& ~ $less(X2,tb2t(get1(int,t2tb1(X1),X6))) )
| $less(X0,X3) )
& ~ $less(X4,X0)
& ! [X5: $int] :
( ~ $less(tb2t(get1(int,t2tb1(X1),X5)),X2)
| $less(usN,X5)
| ~ $less(X0,X5) ) )
| ~ j_invariant(X3,X4,X0,X2,X1) ),
inference(ennf_transformation,[],[f166]) ).
tff(f178,plain,
! [X3: $int,X2: $int,X0: $int,X1: array_int,X4: $int] :
( ~ j_invariant(X3,X4,X0,X2,X1)
| ( ( ? [X6: $int] :
( ~ $less(X6,X3)
& ~ $less(X0,X6)
& ~ $less(X2,tb2t(get1(int,t2tb1(X1),X6))) )
| $less(X0,X3) )
& ~ $less(X4,X0)
& ! [X5: $int] :
( ~ $less(tb2t(get1(int,t2tb1(X1),X5)),X2)
| $less(usN,X5)
| ~ $less(X0,X5) ) ) ),
inference(flattening,[],[f177]) ).
tff(f201,plain,
! [X0: ty,X1: $int,X2: uni] :
( ( elts(X0,mk_array(X0,X1,X2)) = X2 )
| ~ sort(map(int,X0),X2) ),
inference(ennf_transformation,[],[f22]) ).
tff(f263,plain,
! [X0: uni,X1: ty,X2: $int] : ( get(X1,int,elts(X1,X0),t2tb(X2)) = get1(X1,X0,X2) ),
inference(rectify,[],[f140]) ).
tff(f264,plain,
! [X0: $int,X4: array_int,X3: $int,X5: $int,X1: $int,X2: $int] :
( ( ( ( tb2t(get1(int,t2tb1(X4),f)) = X5 )
& ~ $less(f,X0)
& ~ $less(X3,f) )
| ( $less(X3,X2)
& $less(X1,X0) )
| ~ termination(X0,X3,X1,X2,X5,X4) )
& ( termination(X0,X3,X1,X2,X5,X4)
| ( ( ( tb2t(get1(int,t2tb1(X4),f)) != X5 )
| $less(f,X0)
| $less(X3,f) )
& ( ~ $less(X3,X2)
| ~ $less(X1,X0) ) ) ) ),
inference(nnf_transformation,[],[f127]) ).
tff(f265,plain,
! [X0: $int,X4: array_int,X3: $int,X5: $int,X1: $int,X2: $int] :
( ( ( ( tb2t(get1(int,t2tb1(X4),f)) = X5 )
& ~ $less(f,X0)
& ~ $less(X3,f) )
| ( $less(X3,X2)
& $less(X1,X0) )
| ~ termination(X0,X3,X1,X2,X5,X4) )
& ( termination(X0,X3,X1,X2,X5,X4)
| ( ( ( tb2t(get1(int,t2tb1(X4),f)) != X5 )
| $less(f,X0)
| $less(X3,f) )
& ( ~ $less(X3,X2)
| ~ $less(X1,X0) ) ) ) ),
inference(flattening,[],[f264]) ).
tff(f266,plain,
! [X0: $int,X1: array_int,X2: $int,X3: $int,X4: $int,X5: $int] :
( ( ( ( tb2t(get1(int,t2tb1(X1),f)) = X3 )
& ~ $less(f,X0)
& ~ $less(X2,f) )
| ( $less(X2,X5)
& $less(X4,X0) )
| ~ termination(X0,X2,X4,X5,X3,X1) )
& ( termination(X0,X2,X4,X5,X3,X1)
| ( ( ( tb2t(get1(int,t2tb1(X1),f)) != X3 )
| $less(f,X0)
| $less(X2,f) )
& ( ~ $less(X2,X5)
| ~ $less(X4,X0) ) ) ) ),
inference(rectify,[],[f265]) ).
tff(f268,plain,
? [X0: map_int_int,X1: $int] :
( ( $sum(usN,1) = X1 )
& ~ $less(X1,0)
& ? [X2: $int,X3: $int,X4: map_int_int] :
( ~ $less(f,0)
& ~ $less(X1,0)
& permut_all(int,mk_array(int,X1,t2tb2(X4)),mk_array(int,X1,t2tb2(X0)))
& ~ $less(X2,1)
& $less(f,X1)
& $less(X2,X3)
& ~ $less(usN,X3)
& n_invariant(X3,tb2t1(mk_array(int,X1,t2tb2(X4))))
& m_invariant(X2,tb2t1(mk_array(int,X1,t2tb2(X4))))
& ? [X5: $int,X6: $int,X7: map_int_int] :
( i_invariant(X2,X3,X5,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& permut_all(int,mk_array(int,X1,t2tb2(X7)),mk_array(int,X1,t2tb2(X0)))
& ~ $less(X6,X5)
& ? [X8: $int] :
( $less(X8,X1)
& i_invariant(X2,X3,X8,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& ? [X9: $int] :
( $less(tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t(get(int,int,t2tb2(X7),t2tb(X9))))
& termination(X8,X9,X2,X3,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& ~ $less(X9,0)
& ~ $less(X6,X9)
& $less(X9,X1)
& ~ $less(X9,X2)
& j_invariant(X2,X3,X9,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& ? [X10: $int] :
( ~ termination(X8,X10,X2,X3,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& ( $sum(X9,$uminus(1)) = X10 ) ) )
& termination(X8,X6,X2,X3,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& ~ $less(X1,0)
& ~ $less(X8,X5)
& ~ $less(X3,X8)
& ~ $less(X8,0)
& ~ $less(tb2t(get(int,int,t2tb2(X7),t2tb(X8))),tb2t(get(int,int,t2tb2(X4),t2tb(f)))) )
& ~ $less(X6,0)
& termination(X5,X6,X2,X3,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& m_invariant(X2,tb2t1(mk_array(int,X1,t2tb2(X7))))
& j_invariant(X2,X3,X6,tb2t(get(int,int,t2tb2(X4),t2tb(f))),tb2t1(mk_array(int,X1,t2tb2(X7))))
& ~ $less($sum(usN,1),X5)
& n_invariant(X3,tb2t1(mk_array(int,X1,t2tb2(X7)))) ) ) ),
inference(rectify,[],[f173]) ).
tff(f269,plain,
( ( $sum(usN,1) = sK6 )
& ~ $less(sK6,0)
& ~ $less(f,0)
& ~ $less(sK6,0)
& permut_all(int,mk_array(int,sK6,t2tb2(sK9)),mk_array(int,sK6,t2tb2(sK5)))
& ~ $less(sK7,1)
& $less(f,sK6)
& $less(sK7,sK8)
& ~ $less(usN,sK8)
& n_invariant(sK8,tb2t1(mk_array(int,sK6,t2tb2(sK9))))
& m_invariant(sK7,tb2t1(mk_array(int,sK6,t2tb2(sK9))))
& i_invariant(sK7,sK8,sK10,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& permut_all(int,mk_array(int,sK6,t2tb2(sK12)),mk_array(int,sK6,t2tb2(sK5)))
& ~ $less(sK11,sK10)
& $less(sK13,sK6)
& i_invariant(sK7,sK8,sK13,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& $less(tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t(get(int,int,t2tb2(sK12),t2tb(sK14))))
& termination(sK13,sK14,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& ~ $less(sK14,0)
& ~ $less(sK11,sK14)
& $less(sK14,sK6)
& ~ $less(sK14,sK7)
& j_invariant(sK7,sK8,sK14,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& ~ termination(sK13,sK15,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& ( $sum(sK14,$uminus(1)) = sK15 )
& termination(sK13,sK11,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& ~ $less(sK6,0)
& ~ $less(sK13,sK10)
& ~ $less(sK8,sK13)
& ~ $less(sK13,0)
& ~ $less(tb2t(get(int,int,t2tb2(sK12),t2tb(sK13))),tb2t(get(int,int,t2tb2(sK9),t2tb(f))))
& ~ $less(sK11,0)
& termination(sK10,sK11,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& m_invariant(sK7,tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& j_invariant(sK7,sK8,sK11,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
& ~ $less($sum(usN,1),sK10)
& n_invariant(sK8,tb2t1(mk_array(int,sK6,t2tb2(sK12)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15]),skolemize(X0,sK5),skolemize(X1,sK6),skolemize(X2,sK7),skolemize(X3,sK8),skolemize(X4,sK9),skolemize(X5,sK10),skolemize(X6,sK11),skolemize(X7,sK12),skolemize(X8,sK13),skolemize(X9,sK14),skolemize(X10,sK15)],[f268]) ).
tff(f280,plain,
! [X0: $int,X1: $int,X2: $int,X3: array_int,X4: $int] :
( ~ j_invariant(X0,X4,X2,X1,X3)
| ( ( ? [X5: $int] :
( ~ $less(X5,X0)
& ~ $less(X2,X5)
& ~ $less(X1,tb2t(get1(int,t2tb1(X3),X5))) )
| $less(X2,X0) )
& ~ $less(X4,X2)
& ! [X6: $int] :
( ~ $less(tb2t(get1(int,t2tb1(X3),X6)),X1)
| $less(usN,X6)
| ~ $less(X2,X6) ) ) ),
inference(rectify,[],[f178]) ).
tff(f281,plain,
! [X0: $int,X1: $int,X2: $int,X3: array_int,X4: $int] :
( ~ j_invariant(X0,X4,X2,X1,X3)
| ( ( ( ~ $less(sK17(X0,X1,X2,X3),X0)
& ~ $less(X2,sK17(X0,X1,X2,X3))
& ~ $less(X1,tb2t(get1(int,t2tb1(X3),sK17(X0,X1,X2,X3)))) )
| $less(X2,X0) )
& ~ $less(X4,X2)
& ! [X6: $int] :
( ~ $less(tb2t(get1(int,t2tb1(X3),X6)),X1)
| $less(usN,X6)
| ~ $less(X2,X6) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X5,sK17(X0,X1,X2,X3))],[f280]) ).
tff(f317,plain,
! [X2: uni,X0: ty,X1: $int] :
( ( elts(X0,mk_array(X0,X1,X2)) = X2 )
| ~ sort(map(int,X0),X2) ),
inference(cnf_transformation,[],[f201]) ).
tff(f337,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f60]) ).
tff(f357,plain,
! [X2: $int,X0: uni,X1: ty] : ( get(X1,int,elts(X1,X0),t2tb(X2)) = get1(X1,X0,X2) ),
inference(cnf_transformation,[],[f263]) ).
tff(f358,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( termination(X0,X2,X4,X5,X3,X1)
| ~ $less(X4,X0)
| ~ $less(X2,X5) ),
inference(cnf_transformation,[],[f266]) ).
tff(f359,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( termination(X0,X2,X4,X5,X3,X1)
| ( tb2t(get1(int,t2tb1(X1),f)) != X3 )
| $less(f,X0)
| $less(X2,f) ),
inference(cnf_transformation,[],[f266]) ).
tff(f360,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( ~ termination(X0,X2,X4,X5,X3,X1)
| ~ $less(X2,f)
| $less(X4,X0) ),
inference(cnf_transformation,[],[f266]) ).
tff(f362,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( ~ termination(X0,X2,X4,X5,X3,X1)
| $less(X4,X0)
| ~ $less(f,X0) ),
inference(cnf_transformation,[],[f266]) ).
tff(f364,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( ( tb2t(get1(int,t2tb1(X1),f)) = X3 )
| $less(X4,X0)
| ~ termination(X0,X2,X4,X5,X3,X1) ),
inference(cnf_transformation,[],[f266]) ).
tff(f378,plain,
termination(sK13,sK11,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))),
inference(cnf_transformation,[],[f269]) ).
tff(f379,plain,
$sum(sK14,$uminus(1)) = sK15,
inference(cnf_transformation,[],[f269]) ).
tff(f380,plain,
~ termination(sK13,sK15,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))),
inference(cnf_transformation,[],[f269]) ).
tff(f381,plain,
j_invariant(sK7,sK8,sK14,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))),
inference(cnf_transformation,[],[f269]) ).
tff(f386,plain,
termination(sK13,sK14,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))),
inference(cnf_transformation,[],[f269]) ).
tff(f387,plain,
$less(tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t(get(int,int,t2tb2(sK12),t2tb(sK14)))),
inference(cnf_transformation,[],[f269]) ).
tff(f421,plain,
! [X0: map_int_int] : sort(map(int,int),t2tb2(X0)),
inference(cnf_transformation,[],[f67]) ).
tff(f423,plain,
! [X2: $int,X3: array_int,X0: $int,X1: $int,X4: $int] :
( ~ j_invariant(X0,X4,X2,X1,X3)
| ~ $less(X4,X2) ),
inference(cnf_transformation,[],[f281]) ).
tff(f463,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( ~ termination(X0,X2,X4,X5,X3,X1)
| ( tb2t(get(int,int,elts(int,t2tb1(X1)),t2tb(f))) = X3 )
| $less(X4,X0) ),
inference(definition_unfolding,[],[f364,f357]) ).
tff(f464,plain,
! [X2: $int,X3: $int,X0: $int,X1: array_int,X4: $int,X5: $int] :
( termination(X0,X2,X4,X5,X3,X1)
| $less(X2,f)
| ( tb2t(get(int,int,elts(int,t2tb1(X1)),t2tb(f))) != X3 )
| $less(f,X0) ),
inference(definition_unfolding,[],[f359,f357]) ).
tff(f470,plain,
sK15 = $sum(sK14,-1),
inference(evaluation,[],[f379]) ).
tff(f493,definition,
( spl21_5
<=> j_invariant(sK7,sK8,sK14,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))) ),
introduced(definition,[new_symbols(definition,[spl21_5])],[avatar_definition]) ).
tff(f495,plain,
( j_invariant(sK7,sK8,sK14,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
| ~ spl21_5 ),
inference(avatar_component_clause,[],[f493]) ).
tff(f496,plain,
spl21_5,
inference(avatar_split_clause,[],[f381,f493]) ).
tff(f528,definition,
( spl21_12
<=> $less(tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t(get(int,int,t2tb2(sK12),t2tb(sK14)))) ),
introduced(definition,[new_symbols(definition,[spl21_12])],[avatar_definition]) ).
tff(f531,plain,
spl21_12,
inference(avatar_split_clause,[],[f387,f528]) ).
tff(f547,plain,
sK15 = $sum(-1,sK14),
inference(forward_demodulation,[],[f470,f98]) ).
tff(f615,definition,
( spl21_29
<=> termination(sK13,sK14,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))) ),
introduced(definition,[new_symbols(definition,[spl21_29])],[avatar_definition]) ).
tff(f617,plain,
( termination(sK13,sK14,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
| ~ spl21_29 ),
inference(avatar_component_clause,[],[f615]) ).
tff(f618,plain,
spl21_29,
inference(avatar_split_clause,[],[f386,f615]) ).
tff(f645,definition,
( spl21_35
<=> termination(sK13,sK11,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))) ),
introduced(definition,[new_symbols(definition,[spl21_35])],[avatar_definition]) ).
tff(f647,plain,
( termination(sK13,sK11,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
| ~ spl21_35 ),
inference(avatar_component_clause,[],[f645]) ).
tff(f648,plain,
spl21_35,
inference(avatar_split_clause,[],[f378,f645]) ).
tff(f650,definition,
( spl21_36
<=> termination(sK13,sK15,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12)))) ),
introduced(definition,[new_symbols(definition,[spl21_36])],[avatar_definition]) ).
tff(f652,plain,
( ~ termination(sK13,sK15,sK7,sK8,tb2t(get(int,int,t2tb2(sK9),t2tb(f))),tb2t1(mk_array(int,sK6,t2tb2(sK12))))
| spl21_36 ),
inference(avatar_component_clause,[],[f650]) ).
tff(f653,plain,
~ spl21_36,
inference(avatar_split_clause,[],[f380,f650]) ).
tff(f655,definition,
( spl21_37
<=> ( sK15 = $sum(-1,sK14) ) ),
introduced(definition,[new_symbols(definition,[spl21_37])],[avatar_definition]) ).
tff(f658,plain,
spl21_37,
inference(avatar_split_clause,[],[f547,f655]) ).
tff(f1256,plain,
( ~ $less(sK8,sK14)
| ~ spl21_5 ),
inference(resolution,[],[f423,f495]) ).
tff(f1259,definition,
( spl21_115
<=> $less(sK8,sK14) ),
introduced(definition,[new_symbols(definition,[spl21_115])],[avatar_definition]) ).
tff(f1262,plain,
( ~ spl21_115
| ~ spl21_5 ),
inference(avatar_split_clause,[],[f1256,f493,f1259]) ).
tff(f1458,plain,
! [X0: map_int_int,X1: $int] : ( t2tb2(X0) = elts(int,mk_array(int,X1,t2tb2(X0))) ),
inference(unit_resulting_resolution,[],[f317,f421]) ).
tff(f1532,plain,
( ~ $less(sK15,sK8)
| ~ $less(sK7,sK13)
| spl21_36 ),
inference(resolution,[],[f358,f652]) ).
tff(f1534,definition,
( spl21_118
<=> $less(sK7,sK13) ),
introduced(definition,[new_symbols(definition,[spl21_118])],[avatar_definition]) ).
tff(f1536,plain,
( ~ $less(sK7,sK13)
| spl21_118 ),
inference(avatar_component_clause,[],[f1534]) ).
tff(f1538,definition,
( spl21_119
<=> $less(sK15,sK8) ),
introduced(definition,[new_symbols(definition,[spl21_119])],[avatar_definition]) ).
tff(f1541,plain,
( ~ spl21_118
| ~ spl21_119
| spl21_36 ),
inference(avatar_split_clause,[],[f1532,f650,f1538,f1534]) ).
tff(f1543,plain,
( $less(sK7,sK13)
| ~ $less(sK14,f)
| ~ spl21_29 ),
inference(resolution,[],[f360,f617]) ).
tff(f1556,plain,
( ~ $less(sK14,f)
| ~ spl21_29
| spl21_118 ),
inference(forward_subsumption_resolution,[],[f1543,f1536]) ).
tff(f1559,definition,
( spl21_122
<=> $less(sK14,f) ),
introduced(definition,[new_symbols(definition,[spl21_122])],[avatar_definition]) ).
tff(f1562,plain,
( ~ spl21_122
| ~ spl21_29
| spl21_118 ),
inference(avatar_split_clause,[],[f1556,f1534,f615,f1559]) ).
tff(f1570,plain,
( $less(sK7,sK13)
| ~ $less(f,sK13)
| ~ spl21_35 ),
inference(resolution,[],[f362,f647]) ).
tff(f1573,plain,
( ~ $less(f,sK13)
| ~ spl21_35
| spl21_118 ),
inference(forward_subsumption_resolution,[],[f1570,f1536]) ).
tff(f1580,definition,
( spl21_124
<=> $less(f,sK13) ),
introduced(definition,[new_symbols(definition,[spl21_124])],[avatar_definition]) ).
tff(f1582,plain,
( ~ $less(f,sK13)
| spl21_124 ),
inference(avatar_component_clause,[],[f1580]) ).
tff(f1584,plain,
( ~ spl21_124
| ~ spl21_35
| spl21_118 ),
inference(avatar_split_clause,[],[f1573,f1534,f645,f1580]) ).
tff(f2720,definition,
( spl21_227
<=> ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) = tb2t(get(int,int,t2tb2(sK12),t2tb(f))) ) ),
introduced(definition,[new_symbols(definition,[spl21_227])],[avatar_definition]) ).
tff(f2722,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) = tb2t(get(int,int,t2tb2(sK12),t2tb(f))) )
| ~ spl21_227 ),
inference(avatar_component_clause,[],[f2720]) ).
tff(f2732,plain,
( $less(sK7,sK13)
| ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) = tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array(int,sK6,t2tb2(sK12))))),t2tb(f))) )
| ~ spl21_35 ),
inference(resolution,[],[f463,f647]) ).
tff(f2736,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) = tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array(int,sK6,t2tb2(sK12))))),t2tb(f))) )
| ~ spl21_35
| spl21_118 ),
inference(forward_subsumption_resolution,[],[f2732,f1536]) ).
tff(f2739,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) = tb2t(get(int,int,elts(int,mk_array(int,sK6,t2tb2(sK12))),t2tb(f))) )
| ~ spl21_35
| spl21_118 ),
inference(forward_demodulation,[],[f2736,f337]) ).
tff(f2742,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) = tb2t(get(int,int,t2tb2(sK12),t2tb(f))) )
| ~ spl21_35
| spl21_118 ),
inference(forward_demodulation,[],[f2739,f1458]) ).
tff(f2744,plain,
( spl21_227
| ~ spl21_35
| spl21_118 ),
inference(avatar_split_clause,[],[f2742,f1534,f645,f2720]) ).
tff(f2829,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) != tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array(int,sK6,t2tb2(sK12))))),t2tb(f))) )
| $less(f,sK13)
| $less(sK15,f)
| spl21_36 ),
inference(resolution,[],[f464,f652]) ).
tff(f2863,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) != tb2t(get(int,int,elts(int,t2tb1(tb2t1(mk_array(int,sK6,t2tb2(sK12))))),t2tb(f))) )
| $less(sK15,f)
| spl21_36
| spl21_124 ),
inference(forward_subsumption_resolution,[],[f2829,f1582]) ).
tff(f2864,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) != tb2t(get(int,int,elts(int,mk_array(int,sK6,t2tb2(sK12))),t2tb(f))) )
| $less(sK15,f)
| spl21_36
| spl21_124 ),
inference(forward_demodulation,[],[f2863,f337]) ).
tff(f2865,plain,
( ( tb2t(get(int,int,t2tb2(sK9),t2tb(f))) != tb2t(get(int,int,t2tb2(sK12),t2tb(f))) )
| $less(sK15,f)
| spl21_36
| spl21_124 ),
inference(forward_demodulation,[],[f2864,f1458]) ).
tff(f2866,plain,
( $less(sK15,f)
| spl21_36
| spl21_124
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f2865,f2722]) ).
tff(f2868,definition,
( spl21_231
<=> $less(sK15,f) ),
introduced(definition,[new_symbols(definition,[spl21_231])],[avatar_definition]) ).
tff(f2871,plain,
( spl21_231
| spl21_36
| spl21_124
| ~ spl21_227 ),
inference(avatar_split_clause,[],[f2866,f2720,f1580,f650,f2868]) ).
tff(f2872,plain,
$false,
inference(avatar_smt_refutation,[],[f2871,f2744,f1584,f1562,f1541,f1262,f658,f653,f648,f618,f531,f496]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW594_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n015.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 14:23:32 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 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.43/1.16 % (2660178)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.43/1.16 % (2660187)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3123258610:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.43/1.16 % (2660187)Instruction limit reached!
% 3.43/1.16 % (2660187)------------------------------
% 3.43/1.16 % (2660187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.16 % (2660187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.16 % (2660187)CaDiCaL version: 2.1.3
% 3.43/1.16 % (2660187)Termination reason: Instruction limit
% 3.43/1.16 % (2660187)Termination phase: Preprocessing 3
% 3.43/1.16 % (2660187)Time elapsed: 0.002 s
% 3.43/1.16 % (2660187)Peak memory usage: 86 MB
% 3.43/1.16 % (2660187)Instructions burned: 6 (million)
% 3.43/1.16 % (2660184)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=529598024:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.43/1.16 % (2660183)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1363148800:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.43/1.16 % (2660186)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1342546285:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.43/1.16 % (2660185)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1348622829:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.43/1.16 % (2660186)Instruction limit reached!
% 3.43/1.16 % (2660186)------------------------------
% 3.43/1.16 % (2660186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.16 % (2660186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.16 % (2660186)CaDiCaL version: 2.1.3
% 3.43/1.16 % (2660186)Termination reason: Instruction limit
% 3.43/1.16 % (2660186)Termination phase: Property scanning
% 3.43/1.16 % (2660186)Time elapsed: 0.005 s
% 3.43/1.16 % (2660186)Peak memory usage: 86 MB
% 3.43/1.16 % (2660186)Instructions burned: 8 (million)
% 3.43/1.16 % (2660189)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4236806723:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.43/1.16 % (2660188)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3284180030:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.43/1.16 % (2660183)Instruction limit reached!
% 3.43/1.16 % (2660183)------------------------------
% 3.43/1.16 % (2660183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.16 % (2660183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.16 % (2660183)CaDiCaL version: 2.1.3
% 3.43/1.16 % (2660183)Termination reason: Instruction limit
% 3.43/1.16 % (2660183)Termination phase: Saturation
% 3.43/1.16 % (2660183)Time elapsed: 0.007 s
% 3.43/1.16 % (2660183)Peak memory usage: 88 MB
% 3.43/1.16 % (2660183)Instructions burned: 12 (million)
% 3.43/1.16 % (2660191)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3444875182:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.43/1.16 % (2660191)Instruction limit reached!
% 3.43/1.16 % (2660191)------------------------------
% 3.43/1.16 % (2660191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.16 % (2660191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.16 % (2660191)CaDiCaL version: 2.1.3
% 3.43/1.16 % (2660191)Termination reason: Instruction limit
% 3.43/1.16 % (2660191)Termination phase: Saturation
% 3.43/1.16 % (2660191)Time elapsed: 0.005 s
% 3.43/1.16 % (2660191)Peak memory usage: 88 MB
% 3.43/1.16 % (2660191)Instructions burned: 16 (million)
% 3.43/1.16 % (2660189)Instruction limit reached!
% 3.43/1.16 % (2660189)------------------------------
% 3.43/1.16 % (2660189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.16 % (2660189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.16 % (2660189)CaDiCaL version: 2.1.3
% 3.43/1.16 % (2660189)Termination reason: Instruction limit
% 3.43/1.16 % (2660189)Termination phase: Saturation
% 3.43/1.16 % (2660189)Time elapsed: 0.043 s
% 3.43/1.16 % (2660189)Peak memory usage: 116 MB
% 3.43/1.16 % (2660189)Instructions burned: 33 (million)
% 3.43/1.16 % (2660188)Instruction limit reached!
% 3.43/1.16 % (2660188)------------------------------
% 3.89/1.30 % (2660188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.89/1.30 % (2660188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/1.30 % (2660188)CaDiCaL version: 2.1.3
% 3.89/1.30 % (2660188)Termination reason: Instruction limit
% 3.89/1.30 % (2660188)Termination phase: Saturation
% 3.89/1.30 % (2660188)Time elapsed: 0.053 s
% 3.89/1.30 % (2660188)Peak memory usage: 116 MB
% 3.89/1.30 % (2660188)Instructions burned: 46 (million)
% 3.89/1.30 % (2660185)Instruction limit reached!
% 3.89/1.30 % (2660185)------------------------------
% 3.89/1.30 % (2660185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.89/1.30 % (2660185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/1.30 % (2660185)CaDiCaL version: 2.1.3
% 3.89/1.30 % (2660185)Termination reason: Instruction limit
% 3.89/1.30 % (2660185)Termination phase: Saturation
% 3.89/1.30 % (2660185)Time elapsed: 0.117 s
% 3.89/1.30 % (2660185)Peak memory usage: 116 MB
% 3.89/1.30 % (2660185)Instructions burned: 201 (million)
% 3.89/1.30 % (2660198)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=943986678:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.89/1.30 % (2660201)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1483729780:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.89/1.30 % (2660201)Instruction limit reached!
% 3.89/1.30 % (2660201)------------------------------
% 3.89/1.30 % (2660201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.89/1.30 % (2660201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/1.30 % (2660201)CaDiCaL version: 2.1.3
% 3.89/1.30 % (2660201)Termination reason: Instruction limit
% 3.89/1.30 % (2660201)Termination phase: Saturation
% 3.89/1.30 % (2660201)Time elapsed: 0.008 s
% 3.89/1.30 % (2660201)Peak memory usage: 89 MB
% 3.89/1.30 % (2660201)Instructions burned: 24 (million)
% 3.89/1.30 % (2660199)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2244192231:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.89/1.30 % (2660198)Instruction limit reached!
% 3.89/1.30 % (2660198)------------------------------
% 3.89/1.30 % (2660198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.89/1.30 % (2660198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/1.30 % (2660198)CaDiCaL version: 2.1.3
% 3.89/1.30 % (2660198)Termination reason: Instruction limit
% 3.89/1.30 % (2660198)Termination phase: Saturation
% 3.89/1.30 % (2660198)Time elapsed: 0.021 s
% 3.89/1.30 % (2660198)Peak memory usage: 89 MB
% 3.89/1.30 % (2660198)Instructions burned: 29 (million)
% 3.89/1.30 % (2660199)Instruction limit reached!
% 3.89/1.30 % (2660199)------------------------------
% 3.89/1.30 % (2660199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.89/1.30 % (2660199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/1.30 % (2660199)CaDiCaL version: 2.1.3
% 3.89/1.30 % (2660199)Termination reason: Instruction limit
% 3.89/1.30 % (2660199)Termination phase: Saturation
% 3.89/1.30 % (2660199)Time elapsed: 0.010 s
% 3.89/1.30 % (2660199)Peak memory usage: 89 MB
% 3.89/1.30 % (2660199)Instructions burned: 16 (million)
% 3.89/1.30 % (2660202)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=61096782:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.89/1.30 % (2660203)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=590109150:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.89/1.30 % (2660202)Instruction limit reached!
% 3.89/1.30 % (2660202)------------------------------
% 3.89/1.30 % (2660202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.89/1.30 % (2660202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/1.30 % (2660202)CaDiCaL version: 2.1.3
% 3.89/1.30 % (2660202)Termination reason: Instruction limit
% 3.89/1.30 % (2660202)Termination phase: Saturation
% 3.89/1.30 % (2660202)Time elapsed: 0.017 s
% 3.89/1.30 % (2660202)Peak memory usage: 90 MB
% 3.89/1.30 % (2660202)Instructions burned: 28 (million)
% 3.89/1.30 % (2660184)Instruction limit reached!
% 3.89/1.30 % (2660184)------------------------------
% 3.89/1.30 % (2660184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.43 % (2660184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.43 % (2660184)CaDiCaL version: 2.1.3
% 4.94/1.43 % (2660184)Termination reason: Instruction limit
% 4.94/1.43 % (2660184)Termination phase: Saturation
% 4.94/1.43 % (2660184)Time elapsed: 0.221 s
% 4.94/1.43 % (2660184)Peak memory usage: 118 MB
% 4.94/1.43 % (2660184)Instructions burned: 308 (million)
% 4.94/1.43 % (2660208)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2701724657:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 4.94/1.43 % (2660204)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2385947485:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 4.94/1.43 % (2660204)Instruction limit reached!
% 4.94/1.43 % (2660204)------------------------------
% 4.94/1.43 % (2660204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.43 % (2660204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.43 % (2660204)CaDiCaL version: 2.1.3
% 4.94/1.43 % (2660204)Termination reason: Instruction limit
% 4.94/1.43 % (2660204)Termination phase: Preprocessing 1
% 4.94/1.43 % (2660204)Time elapsed: 0.002 s
% 4.94/1.43 % (2660204)Peak memory usage: 85 MB
% 4.94/1.43 % (2660204)Instructions burned: 3 (million)
% 4.94/1.43 % (2660203)Instruction limit reached!
% 4.94/1.43 % (2660203)------------------------------
% 4.94/1.43 % (2660203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.43 % (2660203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.43 % (2660203)CaDiCaL version: 2.1.3
% 4.94/1.43 % (2660203)Termination reason: Instruction limit
% 4.94/1.43 % (2660203)Termination phase: Saturation
% 4.94/1.43 % (2660203)Time elapsed: 0.045 s
% 4.94/1.43 % (2660203)Peak memory usage: 89 MB
% 4.94/1.43 % (2660203)Instructions burned: 85 (million)
% 4.94/1.43 % (2660210)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3006820811:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 4.94/1.43 % (2660209)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=259282838:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 4.94/1.43 % (2660208)Instruction limit reached!
% 4.94/1.43 % (2660208)------------------------------
% 4.94/1.43 % (2660208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.43 % (2660208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.43 % (2660208)CaDiCaL version: 2.1.3
% 4.94/1.43 % (2660208)Termination reason: Instruction limit
% 4.94/1.43 % (2660208)Termination phase: Saturation
% 4.94/1.43 % (2660208)Time elapsed: 0.064 s
% 4.94/1.43 % (2660208)Peak memory usage: 91 MB
% 4.94/1.43 % (2660208)Instructions burned: 183 (million)
% 4.94/1.43 % (2660209)Instruction limit reached!
% 4.94/1.43 % (2660209)------------------------------
% 4.94/1.43 % (2660209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.43 % (2660209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.43 % (2660209)CaDiCaL version: 2.1.3
% 4.94/1.43 % (2660209)Termination reason: Instruction limit
% 4.94/1.43 % (2660209)Termination phase: Preprocessing 3
% 4.94/1.43 % (2660209)Time elapsed: 0.003 s
% 4.94/1.43 % (2660209)Peak memory usage: 86 MB
% 4.94/1.43 % (2660209)Instructions burned: 5 (million)
% 4.94/1.43 % (2660213)lrs+10_1_thi=all:si=on:fd=off:random_seed=3855694151:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 4.94/1.43 % (2660217)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3703471724:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 4.94/1.43 % (2660215)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=1867136390:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 4.94/1.43 % (2660217)Instruction limit reached!
% 4.94/1.43 % (2660217)------------------------------
% 4.94/1.43 % (2660217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.43 % (2660217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.43 % (2660217)CaDiCaL version: 2.1.3
% 4.94/1.43 % (2660217)Termination reason: Instruction limit
% 4.94/1.43 % (2660217)Termination phase: Unused predicate definition removal
% 6.61/1.69 % (2660217)Time elapsed: 0.002 s
% 6.61/1.69 % (2660217)Peak memory usage: 85 MB
% 6.61/1.69 % (2660217)Instructions burned: 3 (million)
% 6.61/1.69 % (2660215)Instruction limit reached!
% 6.61/1.69 % (2660215)------------------------------
% 6.61/1.69 % (2660215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.69 % (2660215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.69 % (2660215)CaDiCaL version: 2.1.3
% 6.61/1.69 % (2660215)Termination reason: Instruction limit
% 6.61/1.69 % (2660215)Termination phase: Property scanning
% 6.61/1.69 % (2660215)Time elapsed: 0.005 s
% 6.61/1.69 % (2660215)Peak memory usage: 86 MB
% 6.61/1.69 % (2660215)Instructions burned: 10 (million)
% 6.61/1.69 % (2660221)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3022619507:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.61/1.69 % (2660210)Instruction limit reached!
% 6.61/1.69 % (2660210)------------------------------
% 6.61/1.69 % (2660210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.69 % (2660210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.69 % (2660210)CaDiCaL version: 2.1.3
% 6.61/1.69 % (2660210)Termination reason: Instruction limit
% 6.61/1.69 % (2660210)Termination phase: Saturation
% 6.61/1.69 % (2660210)Time elapsed: 0.089 s
% 6.61/1.69 % (2660210)Peak memory usage: 134 MB
% 6.61/1.69 % (2660210)Instructions burned: 66 (million)
% 6.61/1.69 % (2660218)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2508258169:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.61/1.69 % (2660218)Instruction limit reached!
% 6.61/1.69 % (2660218)------------------------------
% 6.61/1.69 % (2660218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.69 % (2660218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.69 % (2660218)CaDiCaL version: 2.1.3
% 6.61/1.69 % (2660218)Termination reason: Instruction limit
% 6.61/1.69 % (2660218)Termination phase: Preprocessing 1
% 6.61/1.69 % (2660218)Time elapsed: 0.002 s
% 6.61/1.69 % (2660218)Peak memory usage: 85 MB
% 6.61/1.69 % (2660218)Instructions burned: 3 (million)
% 6.61/1.69 % (2660213)Instruction limit reached!
% 6.61/1.69 % (2660213)------------------------------
% 6.61/1.69 % (2660213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.69 % (2660213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.69 % (2660213)CaDiCaL version: 2.1.3
% 6.61/1.69 % (2660213)Termination reason: Instruction limit
% 6.61/1.69 % (2660213)Termination phase: Saturation
% 6.61/1.69 % (2660213)Time elapsed: 0.059 s
% 6.61/1.69 % (2660213)Peak memory usage: 117 MB
% 6.61/1.69 % (2660213)Instructions burned: 53 (million)
% 6.61/1.69 % (2660222)dis+10_1_si=on:random_seed=265926531:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 6.61/1.69 % (2660222)Instruction limit reached!
% 6.61/1.69 % (2660222)------------------------------
% 6.61/1.69 % (2660222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.69 % (2660222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.69 % (2660222)CaDiCaL version: 2.1.3
% 6.61/1.69 % (2660222)Termination reason: Instruction limit
% 6.61/1.69 % (2660222)Termination phase: Property scanning
% 6.61/1.69 % (2660222)Time elapsed: 0.006 s
% 6.61/1.69 % (2660222)Peak memory usage: 87 MB
% 6.61/1.69 % (2660222)Instructions burned: 11 (million)
% 6.61/1.69 % (2660221)Instruction limit reached!
% 6.61/1.69 % (2660221)------------------------------
% 6.61/1.69 % (2660221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.69 % (2660221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.69 % (2660221)CaDiCaL version: 2.1.3
% 6.61/1.69 % (2660221)Termination reason: Instruction limit
% 6.61/1.69 % (2660221)Termination phase: Saturation
% 6.61/1.69 % (2660221)Time elapsed: 0.060 s
% 6.61/1.69 % (2660221)Peak memory usage: 117 MB
% 6.61/1.69 % (2660221)Instructions burned: 128 (million)
% 6.61/1.69 % (2660226)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2491950833:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.61/1.69 % (2660228)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2737466286: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)
% 7.42/1.87 % (2660231)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1519070455:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 7.42/1.87 % (2660231)Instruction limit reached!
% 7.42/1.87 % (2660231)------------------------------
% 7.42/1.87 % (2660231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.87 % (2660231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.87 % (2660231)CaDiCaL version: 2.1.3
% 7.42/1.87 % (2660231)Termination reason: Instruction limit
% 7.42/1.87 % (2660231)Termination phase: Property scanning
% 7.42/1.87 % (2660231)Time elapsed: 0.005 s
% 7.42/1.87 % (2660231)Peak memory usage: 86 MB
% 7.42/1.87 % (2660231)Instructions burned: 8 (million)
% 7.42/1.87 % (2660226)Refutation not found, incomplete strategy
% 7.42/1.87 % (2660226)------------------------------
% 7.42/1.87 % (2660226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.87 % (2660226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.87 % (2660226)CaDiCaL version: 2.1.3
% 7.42/1.87 % (2660226)Termination reason: Refutation not found, incomplete strategy
% 7.42/1.87 % (2660226)Time elapsed: 0.014 s
% 7.42/1.87 % (2660226)Peak memory usage: 89 MB
% 7.42/1.87 % (2660226)Instructions burned: 21 (million)
% 7.42/1.87 % (2660230)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2157583335:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.42/1.87 % (2660230)Instruction limit reached!
% 7.42/1.87 % (2660230)------------------------------
% 7.42/1.87 % (2660230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.87 % (2660230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.87 % (2660230)CaDiCaL version: 2.1.3
% 7.42/1.87 % (2660230)Termination reason: Instruction limit
% 7.42/1.87 % (2660230)Termination phase: Preprocessing 1
% 7.42/1.87 % (2660230)Time elapsed: 0.002 s
% 7.42/1.87 % (2660230)Peak memory usage: 85 MB
% 7.42/1.87 % (2660230)Instructions burned: 3 (million)
% 7.42/1.87 % (2660235)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2888627088:i=226:rtra=on:gtg=position:ss=axioms_2994 on theBenchmark for (2994ds/226Mi)
% 7.42/1.87 % (2660228)Instruction limit reached!
% 7.42/1.87 % (2660228)------------------------------
% 7.42/1.87 % (2660228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.87 % (2660228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.87 % (2660228)CaDiCaL version: 2.1.3
% 7.42/1.87 % (2660228)Termination reason: Instruction limit
% 7.42/1.87 % (2660228)Termination phase: Saturation
% 7.42/1.87 % (2660228)Time elapsed: 0.025 s
% 7.42/1.87 % (2660228)Peak memory usage: 89 MB
% 7.42/1.87 % (2660228)Instructions burned: 35 (million)
% 7.42/1.87 % (2660234)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1379800582:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi)
% 7.42/1.87 % (2660232)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3010227024:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 7.42/1.87 % (2660234)Instruction limit reached!
% 7.42/1.87 % (2660234)------------------------------
% 7.42/1.87 % (2660234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.87 % (2660234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.87 % (2660234)CaDiCaL version: 2.1.3
% 7.42/1.87 % (2660234)Termination reason: Instruction limit
% 7.42/1.87 % (2660234)Termination phase: Saturation
% 7.42/1.87 % (2660234)Time elapsed: 0.007 s
% 7.42/1.87 % (2660234)Peak memory usage: 88 MB
% 7.42/1.87 % (2660234)Instructions burned: 13 (million)
% 7.42/1.87 % (2660235)Instruction limit reached!
% 7.42/1.87 % (2660235)------------------------------
% 7.42/1.87 % (2660235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.87 % (2660235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.87 % (2660235)CaDiCaL version: 2.1.3
% 7.42/1.87 % (2660235)Termination reason: Instruction limit
% 7.42/1.87 % (2660235)Termination phase: Saturation
% 7.42/1.87 % (2660235)Time elapsed: 0.096 s
% 7.42/1.87 % (2660235)Peak memory usage: 118 MB
% 7.42/1.87 % (2660235)Instructions burned: 227 (million)
% 7.42/1.87 % (2660241)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=15292724:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 10.14/2.10 % (2660241)Instruction limit reached!
% 10.14/2.10 % (2660241)------------------------------
% 10.14/2.10 % (2660241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.10 % (2660241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.10 % (2660241)CaDiCaL version: 2.1.3
% 10.14/2.10 % (2660241)Termination reason: Instruction limit
% 10.14/2.10 % (2660241)Termination phase: Saturation
% 10.14/2.10 % (2660241)Time elapsed: 0.006 s
% 10.14/2.10 % (2660241)Peak memory usage: 88 MB
% 10.14/2.10 % (2660241)Instructions burned: 10 (million)
% 10.14/2.10 % (2660242)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2629006851:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi)
% 10.14/2.10 % (2660243)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=3340261200:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi)
% 10.14/2.10 % (2660246)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=3691314747:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 10.14/2.10 % (2660247)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3157514973:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi)
% 10.14/2.10 % (2660243)Instruction limit reached!
% 10.14/2.10 % (2660243)------------------------------
% 10.14/2.10 % (2660243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.10 % (2660243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.10 % (2660243)CaDiCaL version: 2.1.3
% 10.14/2.10 % (2660243)Termination reason: Instruction limit
% 10.14/2.10 % (2660243)Termination phase: Saturation
% 10.14/2.10 % (2660243)Time elapsed: 0.054 s
% 10.14/2.10 % (2660243)Peak memory usage: 90 MB
% 10.14/2.10 % (2660243)Instructions burned: 76 (million)
% 10.14/2.10 % (2660242)Instruction limit reached!
% 10.14/2.10 % (2660242)------------------------------
% 10.14/2.10 % (2660242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.10 % (2660242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.10 % (2660242)CaDiCaL version: 2.1.3
% 10.14/2.10 % (2660242)Termination reason: Instruction limit
% 10.14/2.10 % (2660242)Termination phase: Saturation
% 10.14/2.10 % (2660242)Time elapsed: 0.090 s
% 10.14/2.10 % (2660242)Peak memory usage: 133 MB
% 10.14/2.10 % (2660242)Instructions burned: 72 (million)
% 10.14/2.10 % (2660226)------------------------------
% 10.14/2.10 % (2660226)------------------------------
% 10.14/2.10 % (2660247)Instruction limit reached!
% 10.14/2.10 % (2660247)------------------------------
% 10.14/2.10 % (2660247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.10 % (2660247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.10 % (2660247)CaDiCaL version: 2.1.3
% 10.14/2.10 % (2660247)Termination reason: Instruction limit
% 10.14/2.10 % (2660247)Termination phase: Saturation
% 10.14/2.10 % (2660247)Time elapsed: 0.059 s
% 10.14/2.10 % (2660247)Peak memory usage: 117 MB
% 10.14/2.10 % (2660247)Instructions burned: 132 (million)
% 10.14/2.10 % (2660249)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1409338985:i=131:rtra=on_2992 on theBenchmark for (2992ds/131Mi)
% 10.14/2.10 % (2660232)Instruction limit reached!
% 10.14/2.10 % (2660232)------------------------------
% 10.14/2.10 % (2660232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.10 % (2660232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.10 % (2660232)CaDiCaL version: 2.1.3
% 10.14/2.10 % (2660232)Termination reason: Instruction limit
% 10.14/2.10 % (2660232)Termination phase: Saturation
% 10.14/2.10 % (2660232)Time elapsed: 0.242 s
% 10.14/2.10 % (2660232)Peak memory usage: 92 MB
% 10.14/2.10 % (2660232)Instructions burned: 370 (million)
% 10.14/2.10 % (2660254)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2602139168:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi)
% 10.14/2.10 % (2660255)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3293328737:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.14/2.10 % (2660246)Instruction limit reached!
% 11.72/2.40 % (2660246)------------------------------
% 11.72/2.40 % (2660246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.40 % (2660246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.40 % (2660246)CaDiCaL version: 2.1.3
% 11.72/2.40 % (2660246)Termination reason: Instruction limit
% 11.72/2.40 % (2660246)Termination phase: Saturation
% 11.72/2.40 % (2660246)Time elapsed: 0.203 s
% 11.72/2.40 % (2660246)Peak memory usage: 91 MB
% 11.72/2.40 % (2660246)Instructions burned: 294 (million)
% 11.72/2.40 % (2660257)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4140010092:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.72/2.40 % (2660256)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2890873542:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 11.72/2.40 % (2660259)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=733996162:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi)
% 11.72/2.40 % (2660254)Instruction limit reached!
% 11.72/2.40 % (2660254)------------------------------
% 11.72/2.40 % (2660254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.40 % (2660254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.40 % (2660254)CaDiCaL version: 2.1.3
% 11.72/2.40 % (2660254)Termination reason: Instruction limit
% 11.72/2.40 % (2660254)Termination phase: Saturation
% 11.72/2.40 % (2660254)Time elapsed: 0.063 s
% 11.72/2.40 % (2660254)Peak memory usage: 133 MB
% 11.72/2.40 % (2660254)Instructions burned: 40 (million)
% 11.72/2.40 % (2660249)Instruction limit reached!
% 11.72/2.40 % (2660249)------------------------------
% 11.72/2.40 % (2660249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.40 % (2660249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.40 % (2660249)CaDiCaL version: 2.1.3
% 11.72/2.40 % (2660249)Termination reason: Instruction limit
% 11.72/2.40 % (2660249)Termination phase: Saturation
% 11.72/2.40 % (2660249)Time elapsed: 0.132 s
% 11.72/2.40 % (2660249)Peak memory usage: 134 MB
% 11.72/2.40 % (2660249)Instructions burned: 132 (million)
% 11.72/2.40 % (2660257)Instruction limit reached!
% 11.72/2.40 % (2660257)------------------------------
% 11.72/2.40 % (2660257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.40 % (2660257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.40 % (2660257)CaDiCaL version: 2.1.3
% 11.72/2.40 % (2660257)Termination reason: Instruction limit
% 11.72/2.40 % (2660257)Termination phase: Saturation
% 11.72/2.40 % (2660257)Time elapsed: 0.109 s
% 11.72/2.40 % (2660257)Peak memory usage: 117 MB
% 11.72/2.40 % (2660257)Instructions burned: 132 (million)
% 11.72/2.40 % (2660267)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3130105321:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi)
% 11.72/2.40 % (2660264)dis+10_1_si=on:random_seed=3789505261:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 11.72/2.40 % (2660266)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1284041807:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi)
% 11.72/2.40 % (2660267)Instruction limit reached!
% 11.72/2.40 % (2660267)------------------------------
% 11.72/2.40 % (2660267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.40 % (2660267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.40 % (2660267)CaDiCaL version: 2.1.3
% 11.72/2.40 % (2660267)Termination reason: Instruction limit
% 11.72/2.40 % (2660267)Termination phase: Saturation
% 11.72/2.40 % (2660267)Time elapsed: 0.052 s
% 11.72/2.40 % (2660267)Peak memory usage: 91 MB
% 11.72/2.40 % (2660267)Instructions burned: 142 (million)
% 11.72/2.40 % (2660255)Instruction limit reached!
% 11.72/2.40 % (2660255)------------------------------
% 11.72/2.40 % (2660255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.40 % (2660255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.40 % (2660255)CaDiCaL version: 2.1.3
% 11.72/2.40 % (2660255)Termination reason: Instruction limit
% 11.72/2.40 % (2660255)Termination phase: Saturation
% 11.72/2.40 % (2660255)Time elapsed: 0.193 s
% 13.09/2.68 % (2660255)Peak memory usage: 93 MB
% 13.09/2.68 % (2660255)Instructions burned: 309 (million)
% 13.09/2.68 % (2660259)Instruction limit reached!
% 13.09/2.68 % (2660259)------------------------------
% 13.09/2.68 % (2660259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.09/2.68 % (2660259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.09/2.68 % (2660259)CaDiCaL version: 2.1.3
% 13.09/2.68 % (2660259)Termination reason: Instruction limit
% 13.09/2.68 % (2660259)Termination phase: Saturation
% 13.09/2.68 % (2660259)Time elapsed: 0.189 s
% 13.09/2.68 % (2660259)Peak memory usage: 117 MB
% 13.09/2.68 % (2660259)Instructions burned: 259 (million)
% 13.09/2.68 % (2660269)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2957374922:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 13.09/2.68 % (2660272)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3729300357:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 13.09/2.68 % (2660272)Instruction limit reached!
% 13.09/2.68 % (2660272)------------------------------
% 13.09/2.68 % (2660272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.09/2.68 % (2660272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.09/2.68 % (2660272)CaDiCaL version: 2.1.3
% 13.09/2.68 % (2660272)Termination reason: Instruction limit
% 13.09/2.68 % (2660272)Termination phase: Saturation
% 13.09/2.68 % (2660272)Time elapsed: 0.040 s
% 13.09/2.68 % (2660272)Peak memory usage: 90 MB
% 13.09/2.68 % (2660272)Instructions burned: 121 (million)
% 13.09/2.68 % (2660269)Instruction limit reached!
% 13.09/2.68 % (2660269)------------------------------
% 13.09/2.68 % (2660269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.09/2.68 % (2660269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.09/2.68 % (2660269)CaDiCaL version: 2.1.3
% 13.09/2.68 % (2660269)Termination reason: Instruction limit
% 13.09/2.68 % (2660269)Termination phase: Saturation
% 13.09/2.68 % (2660269)Time elapsed: 0.063 s
% 13.09/2.68 % (2660269)Peak memory usage: 116 MB
% 13.09/2.68 % (2660269)Instructions burned: 65 (million)
% 13.09/2.68 % (2660273)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=2697001012:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi)
% 13.09/2.68 % (2660274)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=2738120696:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi)
% 13.09/2.68 % (2660266)Instruction limit reached!
% 13.09/2.68 % (2660266)------------------------------
% 13.09/2.68 % (2660266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.09/2.68 % (2660266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.09/2.68 % (2660266)CaDiCaL version: 2.1.3
% 13.09/2.68 % (2660266)Termination reason: Instruction limit
% 13.09/2.68 % (2660266)Termination phase: Saturation
% 13.09/2.68 % (2660266)Time elapsed: 0.206 s
% 13.09/2.68 % (2660266)Peak memory usage: 92 MB
% 13.09/2.68 % (2660266)Instructions burned: 384 (million)
% 13.09/2.68 % (2660274)Instruction limit reached!
% 13.09/2.68 % (2660274)------------------------------
% 13.09/2.68 % (2660274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.09/2.68 % (2660274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.09/2.68 % (2660274)CaDiCaL version: 2.1.3
% 13.09/2.68 % (2660274)Termination reason: Instruction limit
% 13.09/2.68 % (2660274)Termination phase: Saturation
% 13.09/2.68 % (2660274)Time elapsed: 0.049 s
% 13.09/2.68 % (2660274)Peak memory usage: 116 MB
% 13.09/2.68 % (2660274)Instructions burned: 40 (million)
% 13.09/2.68 % (2660277)dis+1010_1_to=kbo:si=on:random_seed=784615529:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi)
% 13.09/2.68 % (2660273)Instruction limit reached!
% 13.09/2.68 % (2660273)------------------------------
% 13.09/2.68 % (2660273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.09/2.68 % (2660273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.09/2.68 % (2660273)CaDiCaL version: 2.1.3
% 13.09/2.68 % (2660273)Termination reason: Instruction limit
% 13.09/2.68 % (2660273)Termination phase: Saturation
% 13.09/2.68 % (2660273)Time elapsed: 0.106 s
% 13.09/2.68 % (2660273)Peak memory usage: 118 MB
% 13.09/2.68 % (2660273)Instructions burned: 128 (million)
% 13.09/2.68 % (2660256)Instruction limit reached!
% 15.65/2.96 % (2660256)------------------------------
% 15.65/2.96 % (2660256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/2.96 % (2660256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/2.96 % (2660256)CaDiCaL version: 2.1.3
% 15.65/2.96 % (2660256)Termination reason: Instruction limit
% 15.65/2.96 % (2660256)Termination phase: Saturation
% 15.65/2.96 % (2660256)Time elapsed: 0.410 s
% 15.65/2.96 % (2660256)Peak memory usage: 139 MB
% 15.65/2.96 % (2660256)Instructions burned: 600 (million)
% 15.65/2.96 % (2660279)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3861796546:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi)
% 15.65/2.96 % (2660277)Instruction limit reached!
% 15.65/2.96 % (2660277)------------------------------
% 15.65/2.96 % (2660277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/2.96 % (2660277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/2.96 % (2660277)CaDiCaL version: 2.1.3
% 15.65/2.96 % (2660277)Termination reason: Instruction limit
% 15.65/2.96 % (2660277)Termination phase: Saturation
% 15.65/2.96 % (2660277)Time elapsed: 0.065 s
% 15.65/2.96 % (2660277)Peak memory usage: 91 MB
% 15.65/2.96 % (2660277)Instructions burned: 176 (million)
% 15.65/2.96 % (2660281)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=385182464:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi)
% 15.65/2.96 % (2660283)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1384609104:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi)
% 15.65/2.96 % (2660287)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2495676225:i=328:kws=inv_frequency:nm=20:rtra=on_2985 on theBenchmark for (2985ds/328Mi)
% 15.65/2.96 % (2660285)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=585464096:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi)
% 15.65/2.96 % (2660284)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1831991287:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi)
% 15.65/2.96 % (2660279)Instruction limit reached!
% 15.65/2.96 % (2660279)------------------------------
% 15.65/2.96 % (2660279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/2.96 % (2660279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/2.96 % (2660279)CaDiCaL version: 2.1.3
% 15.65/2.96 % (2660279)Termination reason: Instruction limit
% 15.65/2.96 % (2660279)Termination phase: Saturation
% 15.65/2.96 % (2660279)Time elapsed: 0.159 s
% 15.65/2.96 % (2660279)Peak memory usage: 117 MB
% 15.65/2.96 % (2660279)Instructions burned: 331 (million)
% 15.65/2.96 % (2660287)Instruction limit reached!
% 15.65/2.96 % (2660287)------------------------------
% 15.65/2.96 % (2660287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/2.96 % (2660287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/2.96 % (2660287)CaDiCaL version: 2.1.3
% 15.65/2.96 % (2660287)Termination reason: Instruction limit
% 15.65/2.96 % (2660287)Termination phase: Saturation
% 15.65/2.96 % (2660287)Time elapsed: 0.120 s
% 15.65/2.96 % (2660287)Peak memory usage: 118 MB
% 15.65/2.96 % (2660287)Instructions burned: 328 (million)
% 15.65/2.96 % (2660283)Instruction limit reached!
% 15.65/2.96 % (2660283)------------------------------
% 15.65/2.96 % (2660283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/2.96 % (2660283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/2.96 % (2660283)CaDiCaL version: 2.1.3
% 15.65/2.96 % (2660283)Termination reason: Instruction limit
% 15.65/2.96 % (2660283)Termination phase: Saturation
% 15.65/2.96 % (2660283)Time elapsed: 0.165 s
% 15.65/2.96 % (2660283)Peak memory usage: 136 MB
% 15.65/2.96 % (2660283)Instructions burned: 216 (million)
% 15.65/2.96 % (2660285)Instruction limit reached!
% 15.65/2.96 % (2660285)------------------------------
% 15.65/2.96 % (2660285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/2.96 % (2660285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/2.96 % (2660285)CaDiCaL version: 2.1.3
% 15.65/2.96 % (2660285)Termination reason: Instruction limit
% 15.65/2.96 % (2660285)Termination phase: Saturation
% 17.82/3.18 % (2660285)Time elapsed: 0.168 s
% 17.82/3.18 % (2660285)Peak memory usage: 91 MB
% 17.82/3.18 % (2660285)Instructions burned: 295 (million)
% 17.82/3.18 % (2660293)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=4050384622:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi)
% 17.82/3.18 % (2660284)Instruction limit reached!
% 17.82/3.18 % (2660284)------------------------------
% 17.82/3.18 % (2660284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.82/3.18 % (2660284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.82/3.18 % (2660284)CaDiCaL version: 2.1.3
% 17.82/3.18 % (2660284)Termination reason: Instruction limit
% 17.82/3.18 % (2660284)Termination phase: Saturation
% 17.82/3.18 % (2660284)Time elapsed: 0.179 s
% 17.82/3.18 % (2660284)Peak memory usage: 116 MB
% 17.82/3.18 % (2660284)Instructions burned: 349 (million)
% 17.82/3.18 % (2660294)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2491435251:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi)
% 17.82/3.18 % (2660281)Instruction limit reached!
% 17.82/3.18 % (2660281)------------------------------
% 17.82/3.18 % (2660281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.82/3.18 % (2660281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.82/3.18 % (2660281)CaDiCaL version: 2.1.3
% 17.82/3.18 % (2660281)Termination reason: Instruction limit
% 17.82/3.18 % (2660281)Termination phase: Saturation
% 17.82/3.18 % (2660281)Time elapsed: 0.286 s
% 17.82/3.18 % (2660281)Peak memory usage: 134 MB
% 17.82/3.18 % (2660281)Instructions burned: 484 (million)
% 17.82/3.18 % (2660264)Instruction limit reached!
% 17.82/3.18 % (2660264)------------------------------
% 17.82/3.18 % (2660264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.82/3.18 % (2660264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.82/3.18 % (2660264)CaDiCaL version: 2.1.3
% 17.82/3.18 % (2660264)Termination reason: Instruction limit
% 17.82/3.18 % (2660264)Termination phase: Saturation
% 17.82/3.18 % (2660264)Time elapsed: 0.639 s
% 17.82/3.18 % (2660264)Peak memory usage: 96 MB
% 17.82/3.18 % (2660264)Instructions burned: 1001 (million)
% 17.82/3.18 % (2660295)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2828595734:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi)
% 17.82/3.18 % (2660296)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1682481890:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi)
% 17.82/3.18 % (2660298)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3640811541:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi)
% 17.82/3.18 % (2660294)Instruction limit reached!
% 17.82/3.18 % (2660294)------------------------------
% 17.82/3.18 % (2660294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.82/3.18 % (2660294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.82/3.18 % (2660294)CaDiCaL version: 2.1.3
% 17.82/3.18 % (2660294)Termination reason: Instruction limit
% 17.82/3.18 % (2660294)Termination phase: Saturation
% 17.82/3.18 % (2660294)Time elapsed: 0.157 s
% 17.82/3.18 % (2660294)Peak memory usage: 94 MB
% 17.82/3.18 % (2660294)Instructions burned: 487 (million)
% 17.82/3.18 % (2660300)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=1916102346:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi)
% 17.82/3.18 % (2660301)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1584827649:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi)
% 17.82/3.18 % (2660293)Instruction limit reached!
% 17.82/3.18 % (2660293)------------------------------
% 17.82/3.18 % (2660293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.82/3.18 % (2660293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.82/3.18 % (2660293)CaDiCaL version: 2.1.3
% 17.82/3.18 % (2660293)Termination reason: Instruction limit
% 17.82/3.18 % (2660293)Termination phase: Saturation
% 17.82/3.18 % (2660293)Time elapsed: 0.202 s
% 17.82/3.18 % (2660293)Peak memory usage: 118 MB
% 17.82/3.18 % (2660293)Instructions burned: 281 (million)
% 17.82/3.18 % (2660295)Instruction limit reached!
% 17.82/3.18 % (2660295)------------------------------
% 18.78/3.62 % (2660295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.62 % (2660295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.62 % (2660295)CaDiCaL version: 2.1.3
% 18.78/3.62 % (2660295)Termination reason: Instruction limit
% 18.78/3.62 % (2660295)Termination phase: Saturation
% 18.78/3.62 % (2660295)Time elapsed: 0.171 s
% 18.78/3.62 % (2660295)Peak memory usage: 116 MB
% 18.78/3.62 % (2660295)Instructions burned: 323 (million)
% 18.78/3.62 % (2660306)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1293970973:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi)
% 18.78/3.62 % (2660308)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1363119886:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2980 on theBenchmark for (2980ds/513Mi)
% 18.78/3.62 % (2660310)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=156004008:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi)
% 18.78/3.62 % (2660300)Instruction limit reached!
% 18.78/3.62 % (2660300)------------------------------
% 18.78/3.62 % (2660300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.62 % (2660300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.62 % (2660300)CaDiCaL version: 2.1.3
% 18.78/3.62 % (2660300)Termination reason: Instruction limit
% 18.78/3.62 % (2660300)Termination phase: Saturation
% 18.78/3.62 % (2660300)Time elapsed: 0.218 s
% 18.78/3.62 % (2660300)Peak memory usage: 135 MB
% 18.78/3.62 % (2660300)Instructions burned: 276 (million)
% 18.78/3.62 % (2660306)Instruction limit reached!
% 18.78/3.62 % (2660306)------------------------------
% 18.78/3.62 % (2660306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.62 % (2660306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.62 % (2660306)CaDiCaL version: 2.1.3
% 18.78/3.62 % (2660306)Termination reason: Instruction limit
% 18.78/3.62 % (2660306)Termination phase: Saturation
% 18.78/3.62 % (2660306)Time elapsed: 0.148 s
% 18.78/3.62 % (2660306)Peak memory usage: 119 MB
% 18.78/3.62 % (2660306)Instructions burned: 387 (million)
% 18.78/3.62 % (2660296)Instruction limit reached!
% 18.78/3.62 % (2660296)------------------------------
% 18.78/3.62 % (2660296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.62 % (2660296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.62 % (2660296)CaDiCaL version: 2.1.3
% 18.78/3.62 % (2660296)Termination reason: Instruction limit
% 18.78/3.62 % (2660296)Termination phase: Saturation
% 18.78/3.62 % (2660296)Time elapsed: 0.295 s
% 18.78/3.62 % (2660296)Peak memory usage: 120 MB
% 18.78/3.62 % (2660296)Instructions burned: 417 (million)
% 18.78/3.62 % (2660301)Instruction limit reached!
% 18.78/3.62 % (2660301)------------------------------
% 18.78/3.62 % (2660301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.62 % (2660301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.62 % (2660301)CaDiCaL version: 2.1.3
% 18.78/3.62 % (2660301)Termination reason: Instruction limit
% 18.78/3.62 % (2660301)Termination phase: Saturation
% 18.78/3.62 % (2660301)Time elapsed: 0.256 s
% 18.78/3.62 % (2660301)Peak memory usage: 119 MB
% 18.78/3.62 % (2660301)Instructions burned: 375 (million)
% 18.78/3.62 % (2660298)Instruction limit reached!
% 18.78/3.62 % (2660298)------------------------------
% 18.78/3.62 % (2660298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.78/3.62 % (2660298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.78/3.62 % (2660298)CaDiCaL version: 2.1.3
% 18.78/3.62 % (2660298)Termination reason: Instruction limit
% 18.78/3.62 % (2660298)Termination phase: Saturation
% 18.78/3.62 % (2660298)Time elapsed: 0.308 s
% 18.78/3.62 % (2660298)Peak memory usage: 120 MB
% 18.78/3.62 % (2660298)Instructions burned: 472 (million)
% 18.78/3.62 % (2660314)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1320959509:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi)
% 18.78/3.62 % (2660313)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=646395193:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi)
% 18.78/3.62 % (2660315)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=640563206:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi)
% 24.32/4.08 % (2660316)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=929562161:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi)
% 24.32/4.08 % (2660317)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=153411327:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2977 on theBenchmark for (2977ds/273Mi)
% 24.32/4.08 % (2660314)Instruction limit reached!
% 24.32/4.08 % (2660314)------------------------------
% 24.32/4.08 % (2660314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/4.08 % (2660314)CaDiCaL version: 2.1.3
% 24.32/4.08 % (2660314)Termination reason: Instruction limit
% 24.32/4.08 % (2660314)Termination phase: Saturation
% 24.32/4.08 % (2660314)Time elapsed: 0.128 s
% 24.32/4.08 % (2660314)Peak memory usage: 120 MB
% 24.32/4.08 % (2660314)Instructions burned: 344 (million)
% 24.32/4.08 % (2660308)Instruction limit reached!
% 24.32/4.08 % (2660308)------------------------------
% 24.32/4.08 % (2660308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/4.08 % (2660308)CaDiCaL version: 2.1.3
% 24.32/4.08 % (2660308)Termination reason: Instruction limit
% 24.32/4.08 % (2660308)Termination phase: Saturation
% 24.32/4.08 % (2660308)Time elapsed: 0.318 s
% 24.32/4.08 % (2660308)Peak memory usage: 93 MB
% 24.32/4.08 % (2660308)Instructions burned: 513 (million)
% 24.32/4.08 % (2660310)Instruction limit reached!
% 24.32/4.08 % (2660310)------------------------------
% 24.32/4.08 % (2660310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/4.08 % (2660310)CaDiCaL version: 2.1.3
% 24.32/4.08 % (2660310)Termination reason: Instruction limit
% 24.32/4.08 % (2660310)Termination phase: Saturation
% 24.32/4.08 % (2660310)Time elapsed: 0.271 s
% 24.32/4.08 % (2660310)Peak memory usage: 135 MB
% 24.32/4.08 % (2660310)Instructions burned: 334 (million)
% 24.32/4.08 % (2660323)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=13517954:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi)
% 24.32/4.08 % (2660315)Instruction limit reached!
% 24.32/4.08 % (2660315)------------------------------
% 24.32/4.08 % (2660315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/4.08 % (2660315)CaDiCaL version: 2.1.3
% 24.32/4.08 % (2660315)Termination reason: Instruction limit
% 24.32/4.08 % (2660315)Termination phase: Saturation
% 24.32/4.08 % (2660315)Time elapsed: 0.185 s
% 24.32/4.08 % (2660315)Peak memory usage: 117 MB
% 24.32/4.08 % (2660315)Instructions burned: 262 (million)
% 24.32/4.08 % (2660313)Instruction limit reached!
% 24.32/4.08 % (2660313)------------------------------
% 24.32/4.08 % (2660313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/4.08 % (2660313)CaDiCaL version: 2.1.3
% 24.32/4.08 % (2660313)Termination reason: Instruction limit
% 24.32/4.08 % (2660313)Termination phase: Saturation
% 24.32/4.08 % (2660313)Time elapsed: 0.225 s
% 24.32/4.08 % (2660313)Peak memory usage: 91 MB
% 24.32/4.08 % (2660313)Instructions burned: 360 (million)
% 24.32/4.08 % (2660316)Instruction limit reached!
% 24.32/4.08 % (2660316)------------------------------
% 24.32/4.08 % (2660316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/4.08 % (2660316)CaDiCaL version: 2.1.3
% 24.32/4.08 % (2660316)Termination reason: Instruction limit
% 24.32/4.08 % (2660316)Termination phase: Saturation
% 24.32/4.08 % (2660316)Time elapsed: 0.175 s
% 24.32/4.08 % (2660316)Peak memory usage: 117 MB
% 24.32/4.08 % (2660316)Instructions burned: 236 (million)
% 24.32/4.08 % (2660323)Instruction limit reached!
% 24.32/4.08 % (2660323)------------------------------
% 24.32/4.08 % (2660323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/4.08 % (2660323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660323)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660323)Termination reason: Instruction limit
% 25.05/5.01 % (2660323)Termination phase: Saturation
% 25.05/5.01 % (2660323)Time elapsed: 0.054 s
% 25.05/5.01 % (2660323)Peak memory usage: 91 MB
% 25.05/5.01 % (2660323)Instructions burned: 148 (million)
% 25.05/5.01 % (2660324)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1096895953:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi)
% 25.05/5.01 % (2660317)Instruction limit reached!
% 25.05/5.01 % (2660317)------------------------------
% 25.05/5.01 % (2660317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660317)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660317)Termination reason: Instruction limit
% 25.05/5.01 % (2660317)Termination phase: Saturation
% 25.05/5.01 % (2660317)Time elapsed: 0.199 s
% 25.05/5.01 % (2660317)Peak memory usage: 92 MB
% 25.05/5.01 % (2660317)Instructions burned: 273 (million)
% 25.05/5.01 % (2660325)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=2280703691:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi)
% 25.05/5.01 % (2660329)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2078368327:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi)
% 25.05/5.01 % (2660327)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2715900778:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi)
% 25.05/5.01 % (2660328)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2294068331:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi)
% 25.05/5.01 % (2660331)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2857164124:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi)
% 25.05/5.01 % (2660332)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1439058865:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi)
% 25.05/5.01 % (2660331)Instruction limit reached!
% 25.05/5.01 % (2660331)------------------------------
% 25.05/5.01 % (2660331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660331)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660331)Termination reason: Instruction limit
% 25.05/5.01 % (2660331)Termination phase: Saturation
% 25.05/5.01 % (2660331)Time elapsed: 0.084 s
% 25.05/5.01 % (2660331)Peak memory usage: 117 MB
% 25.05/5.01 % (2660331)Instructions burned: 107 (million)
% 25.05/5.01 % (2660325)Instruction limit reached!
% 25.05/5.01 % (2660325)------------------------------
% 25.05/5.01 % (2660325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660325)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660325)Termination reason: Instruction limit
% 25.05/5.01 % (2660325)Termination phase: Saturation
% 25.05/5.01 % (2660325)Time elapsed: 0.224 s
% 25.05/5.01 % (2660325)Peak memory usage: 135 MB
% 25.05/5.01 % (2660325)Instructions burned: 276 (million)
% 25.05/5.01 % (2660339)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 25.05/5.01 % (2660339)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1856954639:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi)
% 25.05/5.01 % (2660340)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=524300771:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2971 on theBenchmark for (2971ds/130Mi)
% 25.05/5.01 % (2660332)Instruction limit reached!
% 25.05/5.01 % (2660332)------------------------------
% 25.05/5.01 % (2660332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660332)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660332)Termination reason: Instruction limit
% 25.05/5.01 % (2660332)Termination phase: Saturation
% 25.05/5.01 % (2660332)Time elapsed: 0.266 s
% 25.05/5.01 % (2660332)Peak memory usage: 134 MB
% 25.05/5.01 % (2660332)Instructions burned: 451 (million)
% 25.05/5.01 % (2660329)Instruction limit reached!
% 25.05/5.01 % (2660329)------------------------------
% 25.05/5.01 % (2660329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660329)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660329)Termination reason: Instruction limit
% 25.05/5.01 % (2660329)Termination phase: Saturation
% 25.05/5.01 % (2660329)Time elapsed: 0.392 s
% 25.05/5.01 % (2660329)Peak memory usage: 100 MB
% 25.05/5.01 % (2660329)Instructions burned: 1056 (million)
% 25.05/5.01 % (2660340)Instruction limit reached!
% 25.05/5.01 % (2660340)------------------------------
% 25.05/5.01 % (2660340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660340)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660340)Termination reason: Instruction limit
% 25.05/5.01 % (2660340)Termination phase: Saturation
% 25.05/5.01 % (2660340)Time elapsed: 0.104 s
% 25.05/5.01 % (2660340)Peak memory usage: 117 MB
% 25.05/5.01 % (2660340)Instructions burned: 130 (million)
% 25.05/5.01 % (2660328)Instruction limit reached!
% 25.05/5.01 % (2660328)------------------------------
% 25.05/5.01 % (2660328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660328)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660328)Termination reason: Instruction limit
% 25.05/5.01 % (2660328)Termination phase: Saturation
% 25.05/5.01 % (2660328)Time elapsed: 0.458 s
% 25.05/5.01 % (2660328)Peak memory usage: 95 MB
% 25.05/5.01 % (2660328)Instructions burned: 655 (million)
% 25.05/5.01 % (2660344)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=109338506:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi)
% 25.05/5.01 % (2660343)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3608504314:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi)
% 25.05/5.01 % (2660345)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=4268194852:s2a=on:i=835:s2at=2:rtra=on_2969 on theBenchmark for (2969ds/835Mi)
% 25.05/5.01 % (2660347)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1921440902:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2969 on theBenchmark for (2969ds/307Mi)
% 25.05/5.01 % (2660344)Instruction limit reached!
% 25.05/5.01 % (2660344)------------------------------
% 25.05/5.01 % (2660344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660344)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660344)Termination reason: Instruction limit
% 25.05/5.01 % (2660344)Termination phase: Saturation
% 25.05/5.01 % (2660344)Time elapsed: 0.177 s
% 25.05/5.01 % (2660344)Peak memory usage: 93 MB
% 25.05/5.01 % (2660344)Instructions burned: 493 (million)
% 25.05/5.01 % (2660327)Instruction limit reached!
% 25.05/5.01 % (2660327)------------------------------
% 25.05/5.01 % (2660327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660327)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660327)Termination reason: Instruction limit
% 25.05/5.01 % (2660327)Termination phase: Saturation
% 25.05/5.01 % (2660327)Time elapsed: 0.678 s
% 25.05/5.01 % (2660327)Peak memory usage: 95 MB
% 25.05/5.01 % (2660327)Instructions burned: 1053 (million)
% 25.05/5.01 % (2660343)Instruction limit reached!
% 25.05/5.01 % (2660343)------------------------------
% 25.05/5.01 % (2660343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660343)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660343)Termination reason: Instruction limit
% 25.05/5.01 % (2660343)Termination phase: Saturation
% 25.05/5.01 % (2660343)Time elapsed: 0.215 s
% 25.05/5.01 % (2660343)Peak memory usage: 118 MB
% 25.05/5.01 % (2660343)Instructions burned: 314 (million)
% 25.05/5.01 % (2660351)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3899669869:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi)
% 25.05/5.01 % (2660347)Instruction limit reached!
% 25.05/5.01 % (2660347)------------------------------
% 25.05/5.01 % (2660347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660347)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660347)Termination reason: Instruction limit
% 25.05/5.01 % (2660347)Termination phase: Saturation
% 25.05/5.01 % (2660347)Time elapsed: 0.212 s
% 25.05/5.01 % (2660347)Peak memory usage: 93 MB
% 25.05/5.01 % (2660347)Instructions burned: 307 (million)
% 25.05/5.01 % (2660352)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3026922899:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi)
% 25.05/5.01 % (2660353)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=2181963823:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2966 on theBenchmark for (2966ds/784Mi)
% 25.05/5.01 % (2660351)First to succeed.
% 25.05/5.01 % (2660351)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2660178"
% 25.05/5.01 % (2660339)Instruction limit reached!
% 25.05/5.01 % (2660339)------------------------------
% 25.05/5.01 % (2660339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660339)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660339)Termination reason: Instruction limit
% 25.05/5.01 % (2660339)Termination phase: Saturation
% 25.05/5.01 % (2660339)Time elapsed: 0.705 s
% 25.05/5.01 % (2660339)Peak memory usage: 123 MB
% 25.05/5.01 % (2660339)Instructions burned: 1091 (million)
% 25.05/5.01 % (2660356)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=1330046492:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2965 on theBenchmark for (2965ds/1131Mi)
% 25.05/5.01 % (2660352)Refutation not found, SMT solver inside AVATAR returned Unknown
% 25.05/5.01 % (2660352)------------------------------
% 25.05/5.01 % (2660352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660352)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660352)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 25.05/5.01 % (2660352)Time elapsed: 0.213 s
% 25.05/5.01 % (2660352)Peak memory usage: 137 MB
% 25.05/5.01 % (2660352)Instructions burned: 267 (million)
% 25.05/5.01 % (2660352)------------------------------
% 25.05/5.01 % (2660352)------------------------------
% 25.05/5.01 % (2660356)Instruction limit reached!
% 25.05/5.01 % (2660356)------------------------------
% 25.05/5.01 % (2660356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.05/5.01 % (2660356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.05/5.01 % (2660356)CaDiCaL version: 2.1.3
% 25.05/5.01 % (2660356)Termination reason: Instruction limit
% 25.05/5.01 % (2660356)Termination phase: Saturation
% 25.05/5.01 % (2660356)Time elapsed: 0.779 s
% 25.05/5.01 % (2660356)Peak memory usage: 123 MB
% 25.05/5.01 % (2660356)Instructions burned: 1131 (million)
% 25.05/5.01 % (2660351)Refutation found. Thanks to Tanya!
% 25.05/5.01 % SZS status Theorem for theBenchmark
% 25.05/5.01 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/5.21 % (2660351)------------------------------
% 0.18/5.21 % (2660351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/5.21 % (2660351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/5.21 % (2660351)CaDiCaL version: 2.1.3
% 0.18/5.21 % (2660351)Termination reason: Refutation
% 0.18/5.21 % (2660351)Time elapsed: 0.125 s
% 0.18/5.21 % (2660351)Peak memory usage: 120 MB
% 0.18/5.21 % (2660351)Instructions burned: 322 (million)
% 0.18/5.21 % (2660351)------------------------------
% 0.18/5.21 % (2660351)------------------------------
% 0.18/5.21 % (2660178)Success in time 4.366 s
% 0.18/5.21 % Vampire exiting
%------------------------------------------------------------------------------