%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW636_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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:00 PM UTC 2026
% Result : Theorem 155.39s 23.01s
% Output : Refutation 156.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 70
% Syntax : Number of formulae : 236 ( 70 unt; 0 typ; 60 def)
% Number of atoms : 1011 ( 214 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 1149 ( 374 ~; 300 |; 341 &)
% ( 53 <=>; 81 =>; 0 <=; 0 <~>)
% Maximal formula depth : 45 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 903 ( 464 atm; 34 fun; 170 num; 235 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 : 60 ( 56 usr; 43 prp; 0-7 aty)
% Number of functors : 73 ( 70 usr; 40 con; 0-7 aty)
% Number of variables : 409 ( 370 !; 39 ?; 409 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
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_array1: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length1: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get2: ( 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,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
t2tb1: map_int_int > uni ).
tff(func_def_29,type,
tb2t1: uni > map_int_int ).
tff(func_def_30,type,
t2tb2: array_int > uni ).
tff(func_def_31,type,
tb2t2: uni > array_int ).
tff(func_def_32,type,
occ1: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_37,type,
sK0: ( uni * $int * uni * ty * $int ) > $int ).
tff(func_def_38,type,
sK1: ( $int * $int * uni * uni * ty ) > uni ).
tff(func_def_39,type,
sK2: ( uni * $int * $int * $int * ty * uni * $int ) > $int ).
tff(func_def_40,type,
sK3: ( $int * uni * uni * ty * $int * $int ) > $int ).
tff(func_def_41,type,
sK4: map_int_int ).
tff(func_def_42,type,
sK5: $int ).
tff(func_def_43,type,
sK6: $int ).
tff(func_def_44,type,
sK7: $int ).
tff(func_def_45,type,
sK8: $int ).
tff(func_def_46,type,
sK9: $int ).
tff(func_def_47,type,
sK10: map_int_int ).
tff(func_def_48,type,
sK11: $int ).
tff(func_def_49,type,
sK12: map_int_int ).
tff(func_def_50,type,
sK13: $int ).
tff(func_def_51,type,
sK14: $int ).
tff(func_def_52,type,
sK15: $int ).
tff(func_def_53,type,
sK16: ( $int * uni * ty * uni * $int ) > $int ).
tff(func_def_54,type,
sK17: ( $int * $int * ty * uni * uni ) > $int ).
tff(func_def_55,type,
sK18: ( $int * $int * uni * ty * uni ) > $int ).
tff(func_def_56,type,
sF19: uni ).
tff(func_def_57,type,
sF20: uni ).
tff(func_def_58,type,
sF21: uni ).
tff(func_def_59,type,
sF22: uni ).
tff(func_def_60,type,
sF23: $int > uni ).
tff(func_def_61,type,
sF24: $int > $int ).
tff(func_def_62,type,
sF25: uni ).
tff(func_def_63,type,
sF26: uni ).
tff(func_def_64,type,
sF27: $int ).
tff(func_def_65,type,
sF28: $int ).
tff(func_def_66,type,
sF29: uni ).
tff(func_def_67,type,
sF30: uni ).
tff(func_def_68,type,
sF31: uni ).
tff(func_def_69,type,
sF32: $int ).
tff(func_def_70,type,
sF33: uni ).
tff(func_def_71,type,
sF34: $int ).
tff(func_def_72,type,
sF35: uni ).
tff(func_def_73,type,
sF36: uni ).
tff(func_def_74,type,
sF37: $int ).
tff(func_def_75,type,
sF38: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
sorted_sub2: ( map_int_int * $int * $int ) > $o ).
tff(pred_def_5,type,
sorted_sub3: ( array_int * $int * $int ) > $o ).
tff(pred_def_6,type,
sorted1: array_int > $o ).
tff(pred_def_7,type,
exchange2: ( ty * uni * uni * $int * $int * $int * $int ) > $o ).
tff(pred_def_8,type,
exchange3: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_9,type,
permut2: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_10,type,
map_eq_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_11,type,
array_eq_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_12,type,
array_eq: ( ty * uni * uni ) > $o ).
tff(pred_def_13,type,
permut3: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_14,type,
permut_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_15,type,
permut_all: ( ty * uni * uni ) > $o ).
tff(pred_def_16,type,
qs_partition2: ( array_int * array_int * $int * $int * $int * $int * $int ) > $o ).
tff(f20,axiom,
! [X2: uni,X0: ty,X1: $int] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def2) ).
tff(f22,axiom,
! [X1: $int,X2: uni,X0: ty] :
( sort1(map(int,X0),X2)
=> ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def2) ).
tff(f33,axiom,
! [X0: map_int_int] : sort1(map(int,int),t2tb1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f42,axiom,
! [X3: $int,X4: $int,X1: uni,X0: ty,X5: $int,X6: $int,X2: uni] :
( ( ( get(X0,int,X1,t2tb(X5)) = get(X0,int,X2,t2tb(X6)) )
& $less(X5,X4)
& $lesseq(X3,X5)
& $less(X6,X4)
& ( get(X0,int,X1,t2tb(X6)) = get(X0,int,X2,t2tb(X5)) )
& ! [X7: $int] :
( ( $lesseq(X3,X7)
& $less(X7,X4) )
=> ( ( X7 != X5 )
=> ( ( X7 != X6 )
=> ( get(X0,int,X1,t2tb(X7)) = get(X0,int,X2,t2tb(X7)) ) ) ) )
& $lesseq(X3,X6) )
<=> exchange2(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exchange_def) ).
tff(f44,axiom,
! [X0: ty,X2: uni,X4: $int,X1: uni,X3: $int] :
( ( ( length1(X0,X1) = length1(X0,X2) )
& exchange2(X0,elts(X0,X1),elts(X0,X2),0,length1(X0,X1),X3,X4) )
<=> exchange3(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exchange_def1) ).
tff(f45,axiom,
! [X2: uni,X3: $int,X0: ty,X1: uni,X4: $int] :
( $lesseq(X4,X3)
=> ( occ1(X0,X1,X2,X3,X4) = 0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',occ_empty) ).
tff(f52,axiom,
! [X2: $int,X0: ty,X1: uni,X4: $int,X3: $int] :
( ( $less(X4,X3)
& $lesseq(X2,X4) )
=> $less(0,occ1(X0,get(X0,int,X1,t2tb(X4)),X1,X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',occ_pos) ).
tff(f60,axiom,
! [X2: uni,X0: ty,X1: uni,X3: $int,X4: $int] :
( ( $lesseq(0,X4)
& ( length1(X0,X1) = length1(X0,X2) )
& permut2(X0,elts(X0,X1),elts(X0,X2),X3,X4)
& $lesseq(X4,length1(X0,X1))
& $lesseq(X3,length1(X0,X1))
& $lesseq(0,X3) )
<=> permut3(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_def1) ).
tff(f61,axiom,
! [X4: $int,X1: uni,X3: $int,X2: uni,X0: ty] :
( ( permut3(X0,X1,X2,X3,X4)
& map_eq_sub1(X0,elts(X0,X1),elts(X0,X2),X4,length1(X0,X1))
& map_eq_sub1(X0,elts(X0,X1),elts(X0,X2),0,X3) )
<=> permut_sub1(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_sub_def) ).
tff(f67,conjecture,
! [X0: $int,X3: $int,X2: $int,X1: map_int_int] :
( ( $lesseq(0,X2)
& $lesseq(X3,X0)
& $lesseq(X2,X3)
& $lesseq(0,X0) )
=> ( $less($sum(X2,1),X3)
=> ( ( $less(X2,X0)
& $lesseq(0,X2) )
=> ! [X7: map_int_int,X4: $int,X5: $int,X6: $int] :
( ( ! [X8: $int] :
( ( $less(X8,X4)
& $lesseq(X6,X8) )
=> ( tb2t(get(int,int,t2tb1(X7),t2tb(X8))) = tb2t(get(int,int,t2tb1(X1),t2tb(X2))) ) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X1)),mk_array1(int,X0,t2tb1(X7)),X2,X3)
& ! [X8: $int] :
( ( $less(X8,X3)
& $lesseq(X5,X8) )
=> $less(tb2t(get(int,int,t2tb1(X1),t2tb(X2))),tb2t(get(int,int,t2tb1(X7),t2tb(X8)))) )
& $lesseq(X2,X6)
& $lesseq(X5,X3)
& $lesseq(X4,X5)
& $less(X6,X4)
& ! [X8: $int] :
( ( $less(X8,X6)
& $lesseq(X2,X8) )
=> $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),tb2t(get(int,int,t2tb1(X1),t2tb(X2)))) ) )
=> ( $less(X4,X5)
=> ( ( $lesseq(0,X0)
& $lesseq(0,X4)
& $less(X4,X0) )
=> ( $less(tb2t(get(int,int,t2tb1(X7),t2tb(X4))),tb2t(get(int,int,t2tb1(X1),t2tb(X2))))
=> ( ( $lesseq(0,X6)
& $lesseq(0,X4)
& $less(X6,X0)
& $less(X4,X0) )
=> ! [X9: map_int_int] :
( ( $lesseq(0,X0)
& exchange3(int,mk_array1(int,X0,t2tb1(X7)),mk_array1(int,X0,t2tb1(X9)),X6,X4) )
=> ! [X10: $int] :
( ( X10 = $sum(X6,1) )
=> ! [X11: $int] :
( ( X11 = $sum(X4,1) )
=> ( permut_sub1(int,mk_array1(int,X0,t2tb1(X7)),mk_array1(int,X0,t2tb1(X9)),X2,X3)
=> ! [X8: $int] :
( ( $less(X8,X10)
& $lesseq(X2,X8) )
=> $less(tb2t(get(int,int,t2tb1(X9),t2tb(X8))),tb2t(get(int,int,t2tb1(X1),t2tb(X2)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_quick_rec1) ).
tff(f68,negated_conjecture,
~ ! [X0: $int,X3: $int,X2: $int,X1: map_int_int] :
( ( $lesseq(0,X2)
& $lesseq(X3,X0)
& $lesseq(X2,X3)
& $lesseq(0,X0) )
=> ( $less($sum(X2,1),X3)
=> ( ( $less(X2,X0)
& $lesseq(0,X2) )
=> ! [X7: map_int_int,X4: $int,X5: $int,X6: $int] :
( ( ! [X8: $int] :
( ( $less(X8,X4)
& $lesseq(X6,X8) )
=> ( tb2t(get(int,int,t2tb1(X7),t2tb(X8))) = tb2t(get(int,int,t2tb1(X1),t2tb(X2))) ) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X1)),mk_array1(int,X0,t2tb1(X7)),X2,X3)
& ! [X8: $int] :
( ( $less(X8,X3)
& $lesseq(X5,X8) )
=> $less(tb2t(get(int,int,t2tb1(X1),t2tb(X2))),tb2t(get(int,int,t2tb1(X7),t2tb(X8)))) )
& $lesseq(X2,X6)
& $lesseq(X5,X3)
& $lesseq(X4,X5)
& $less(X6,X4)
& ! [X8: $int] :
( ( $less(X8,X6)
& $lesseq(X2,X8) )
=> $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),tb2t(get(int,int,t2tb1(X1),t2tb(X2)))) ) )
=> ( $less(X4,X5)
=> ( ( $lesseq(0,X0)
& $lesseq(0,X4)
& $less(X4,X0) )
=> ( $less(tb2t(get(int,int,t2tb1(X7),t2tb(X4))),tb2t(get(int,int,t2tb1(X1),t2tb(X2))))
=> ( ( $lesseq(0,X6)
& $lesseq(0,X4)
& $less(X6,X0)
& $less(X4,X0) )
=> ! [X9: map_int_int] :
( ( $lesseq(0,X0)
& exchange3(int,mk_array1(int,X0,t2tb1(X7)),mk_array1(int,X0,t2tb1(X9)),X6,X4) )
=> ! [X10: $int] :
( ( X10 = $sum(X6,1) )
=> ! [X11: $int] :
( ( X11 = $sum(X4,1) )
=> ( permut_sub1(int,mk_array1(int,X0,t2tb1(X7)),mk_array1(int,X0,t2tb1(X9)),X2,X3)
=> ! [X8: $int] :
( ( $less(X8,X10)
& $lesseq(X2,X8) )
=> $less(tb2t(get(int,int,t2tb1(X9),t2tb(X8))),tb2t(get(int,int,t2tb1(X1),t2tb(X2)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f67]) ).
tff(f69,plain,
! [X3: $int,X4: $int,X1: uni,X0: ty,X5: $int,X6: $int,X2: uni] :
( ( ( get(X0,int,X1,t2tb(X5)) = get(X0,int,X2,t2tb(X6)) )
& $less(X5,X4)
& ~ $less(X5,X3)
& $less(X6,X4)
& ( get(X0,int,X1,t2tb(X6)) = get(X0,int,X2,t2tb(X5)) )
& ! [X7: $int] :
( ( ~ $less(X7,X3)
& $less(X7,X4) )
=> ( ( X7 != X5 )
=> ( ( X7 != X6 )
=> ( get(X0,int,X1,t2tb(X7)) = get(X0,int,X2,t2tb(X7)) ) ) ) )
& ~ $less(X6,X3) )
<=> exchange2(X0,X1,X2,X3,X4,X5,X6) ),
inference(theory_normalization,[],[f42]) ).
tff(f74,plain,
! [X2: uni,X0: ty,X1: uni,X3: $int,X4: $int] :
( ( ~ $less(X4,0)
& ( length1(X0,X1) = length1(X0,X2) )
& permut2(X0,elts(X0,X1),elts(X0,X2),X3,X4)
& ~ $less(length1(X0,X1),X4)
& ~ $less(length1(X0,X1),X3)
& ~ $less(X3,0) )
<=> permut3(X0,X1,X2,X3,X4) ),
inference(theory_normalization,[],[f60]) ).
tff(f78,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni,X4: $int] :
( ~ $less(X3,X4)
=> ( occ1(X0,X1,X2,X3,X4) = 0 ) ),
inference(theory_normalization,[],[f45]) ).
tff(f79,plain,
! [X2: $int,X0: ty,X1: uni,X4: $int,X3: $int] :
( ( $less(X4,X3)
& ~ $less(X4,X2) )
=> $less(0,occ1(X0,get(X0,int,X1,t2tb(X4)),X1,X2,X3)) ),
inference(theory_normalization,[],[f52]) ).
tff(f88,plain,
~ ! [X0: $int,X3: $int,X2: $int,X1: map_int_int] :
( ( ~ $less(X2,0)
& ~ $less(X0,X3)
& ~ $less(X3,X2)
& ~ $less(X0,0) )
=> ( $less($sum(X2,1),X3)
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ! [X7: map_int_int,X4: $int,X5: $int,X6: $int] :
( ( ! [X8: $int] :
( ( $less(X8,X4)
& ~ $less(X8,X6) )
=> ( tb2t(get(int,int,t2tb1(X7),t2tb(X8))) = tb2t(get(int,int,t2tb1(X1),t2tb(X2))) ) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X1)),mk_array1(int,X0,t2tb1(X7)),X2,X3)
& ! [X8: $int] :
( ( $less(X8,X3)
& ~ $less(X8,X5) )
=> $less(tb2t(get(int,int,t2tb1(X1),t2tb(X2))),tb2t(get(int,int,t2tb1(X7),t2tb(X8)))) )
& ~ $less(X6,X2)
& ~ $less(X3,X5)
& ~ $less(X5,X4)
& $less(X6,X4)
& ! [X8: $int] :
( ( $less(X8,X6)
& ~ $less(X8,X2) )
=> $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),tb2t(get(int,int,t2tb1(X1),t2tb(X2)))) ) )
=> ( $less(X4,X5)
=> ( ( ~ $less(X0,0)
& ~ $less(X4,0)
& $less(X4,X0) )
=> ( $less(tb2t(get(int,int,t2tb1(X7),t2tb(X4))),tb2t(get(int,int,t2tb1(X1),t2tb(X2))))
=> ( ( ~ $less(X6,0)
& ~ $less(X4,0)
& $less(X6,X0)
& $less(X4,X0) )
=> ! [X9: map_int_int] :
( ( ~ $less(X0,0)
& exchange3(int,mk_array1(int,X0,t2tb1(X7)),mk_array1(int,X0,t2tb1(X9)),X6,X4) )
=> ! [X10: $int] :
( ( X10 = $sum(X6,1) )
=> ! [X11: $int] :
( ( X11 = $sum(X4,1) )
=> ( permut_sub1(int,mk_array1(int,X0,t2tb1(X7)),mk_array1(int,X0,t2tb1(X9)),X2,X3)
=> ! [X8: $int] :
( ( $less(X8,X10)
& ~ $less(X8,X2) )
=> $less(tb2t(get(int,int,t2tb1(X9),t2tb(X8))),tb2t(get(int,int,t2tb1(X1),t2tb(X2)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f68]) ).
tff(f91,plain,
! [X5: $int,X2: uni,X4: $int,X1: $int,X6: uni,X0: $int,X3: ty] :
( exchange2(X3,X2,X6,X0,X1,X4,X5)
<=> ( ( get(X3,int,X6,t2tb(X4)) = get(X3,int,X2,t2tb(X5)) )
& $less(X4,X1)
& ( get(X3,int,X2,t2tb(X4)) = get(X3,int,X6,t2tb(X5)) )
& $less(X5,X1)
& ~ $less(X5,X0)
& ! [X7: $int] :
( ( $less(X7,X1)
& ~ $less(X7,X0) )
=> ( ( X4 != X7 )
=> ( ( X5 != X7 )
=> ( get(X3,int,X6,t2tb(X7)) = get(X3,int,X2,t2tb(X7)) ) ) ) )
& ~ $less(X4,X0) ) ),
inference(rectify,[],[f69]) ).
tff(f94,plain,
! [X3: uni,X2: $int,X4: ty,X1: uni,X0: $int] :
( ( map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),X0,length1(X4,X1))
& permut3(X4,X1,X3,X2,X0)
& map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),0,X2) )
<=> permut_sub1(X4,X1,X3,X2,X0) ),
inference(rectify,[],[f61]) ).
tff(f95,plain,
! [X2: $int,X0: uni,X1: ty] : ( length1(X1,mk_array1(X1,X2,X0)) = X2 ),
inference(rectify,[],[f20]) ).
tff(f101,plain,
! [X4: $int,X0: uni,X2: uni,X1: ty,X3: $int] :
( permut3(X1,X2,X0,X3,X4)
<=> ( ~ $less(X4,0)
& permut2(X1,elts(X1,X2),elts(X1,X0),X3,X4)
& ( length1(X1,X2) = length1(X1,X0) )
& ~ $less(X3,0)
& ~ $less(length1(X1,X2),X3)
& ~ $less(length1(X1,X2),X4) ) ),
inference(rectify,[],[f74]) ).
tff(f113,plain,
! [X2: ty,X4: $int,X0: uni,X3: uni,X1: $int] :
( ~ $less(X1,X4)
=> ( 0 = occ1(X2,X3,X0,X1,X4) ) ),
inference(rectify,[],[f78]) ).
tff(f115,plain,
! [X0: $int,X2: uni,X1: ty,X4: $int,X3: $int] :
( ( ~ $less(X3,X0)
& $less(X3,X4) )
=> $less(0,occ1(X1,get(X1,int,X2,t2tb(X3)),X2,X0,X4)) ),
inference(rectify,[],[f79]) ).
tff(f121,plain,
! [X2: ty,X0: $int,X1: uni] :
( sort1(map(int,X2),X1)
=> ( elts(X2,mk_array1(X2,X0,X1)) = X1 ) ),
inference(rectify,[],[f22]) ).
tff(f134,plain,
~ ! [X0: $int,X1: $int,X3: map_int_int,X2: $int] :
( ( ~ $less(X0,X1)
& ~ $less(X1,X2)
& ~ $less(X2,0)
& ~ $less(X0,0) )
=> ( $less($sum(X2,1),X1)
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ! [X4: map_int_int,X6: $int,X5: $int,X7: $int] :
( ( ! [X10: $int] :
( ( ~ $less(X10,X2)
& $less(X10,X7) )
=> $less(tb2t(get(int,int,t2tb1(X4),t2tb(X10))),tb2t(get(int,int,t2tb1(X3),t2tb(X2)))) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X3)),mk_array1(int,X0,t2tb1(X4)),X2,X1)
& ~ $less(X1,X6)
& ~ $less(X6,X5)
& ! [X8: $int] :
( ( ~ $less(X8,X7)
& $less(X8,X5) )
=> ( tb2t(get(int,int,t2tb1(X3),t2tb(X2))) = tb2t(get(int,int,t2tb1(X4),t2tb(X8))) ) )
& ! [X9: $int] :
( ( ~ $less(X9,X6)
& $less(X9,X1) )
=> $less(tb2t(get(int,int,t2tb1(X3),t2tb(X2))),tb2t(get(int,int,t2tb1(X4),t2tb(X9)))) )
& ~ $less(X7,X2)
& $less(X7,X5) )
=> ( $less(X5,X6)
=> ( ( $less(X5,X0)
& ~ $less(X0,0)
& ~ $less(X5,0) )
=> ( $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),tb2t(get(int,int,t2tb1(X3),t2tb(X2))))
=> ( ( ~ $less(X7,0)
& $less(X5,X0)
& ~ $less(X5,0)
& $less(X7,X0) )
=> ! [X11: map_int_int] :
( ( exchange3(int,mk_array1(int,X0,t2tb1(X4)),mk_array1(int,X0,t2tb1(X11)),X7,X5)
& ~ $less(X0,0) )
=> ! [X12: $int] :
( ( $sum(X7,1) = X12 )
=> ! [X13: $int] :
( ( $sum(X5,1) = X13 )
=> ( permut_sub1(int,mk_array1(int,X0,t2tb1(X4)),mk_array1(int,X0,t2tb1(X11)),X2,X1)
=> ! [X14: $int] :
( ( $less(X14,X12)
& ~ $less(X14,X2) )
=> $less(tb2t(get(int,int,t2tb1(X11),t2tb(X14))),tb2t(get(int,int,t2tb1(X3),t2tb(X2)))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f88]) ).
tff(f138,plain,
! [X0: $int,X2: uni,X1: ty,X4: $int,X3: $int] :
( $less(0,occ1(X1,get(X1,int,X2,t2tb(X3)),X2,X0,X4))
| $less(X3,X0)
| ~ $less(X3,X4) ),
inference(ennf_transformation,[],[f115]) ).
tff(f139,plain,
! [X2: uni,X1: ty,X0: $int,X3: $int,X4: $int] :
( ~ $less(X3,X4)
| $less(0,occ1(X1,get(X1,int,X2,t2tb(X3)),X2,X0,X4))
| $less(X3,X0) ),
inference(flattening,[],[f138]) ).
tff(f141,plain,
? [X0: $int,X1: $int,X3: map_int_int,X2: $int] :
( ? [X4: map_int_int,X6: $int,X5: $int,X7: $int] :
( ? [X11: map_int_int] :
( ? [X12: $int] :
( ? [X13: $int] :
( ? [X14: $int] :
( ~ $less(tb2t(get(int,int,t2tb1(X11),t2tb(X14))),tb2t(get(int,int,t2tb1(X3),t2tb(X2))))
& $less(X14,X12)
& ~ $less(X14,X2) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X4)),mk_array1(int,X0,t2tb1(X11)),X2,X1)
& ( $sum(X5,1) = X13 ) )
& ( $sum(X7,1) = X12 ) )
& exchange3(int,mk_array1(int,X0,t2tb1(X4)),mk_array1(int,X0,t2tb1(X11)),X7,X5)
& ~ $less(X0,0) )
& ~ $less(X7,0)
& $less(X5,X0)
& ~ $less(X5,0)
& $less(X7,X0)
& $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),tb2t(get(int,int,t2tb1(X3),t2tb(X2))))
& $less(X5,X0)
& ~ $less(X0,0)
& ~ $less(X5,0)
& $less(X5,X6)
& ! [X10: $int] :
( $less(tb2t(get(int,int,t2tb1(X4),t2tb(X10))),tb2t(get(int,int,t2tb1(X3),t2tb(X2))))
| $less(X10,X2)
| ~ $less(X10,X7) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X3)),mk_array1(int,X0,t2tb1(X4)),X2,X1)
& ~ $less(X1,X6)
& ~ $less(X6,X5)
& ! [X8: $int] :
( ( tb2t(get(int,int,t2tb1(X3),t2tb(X2))) = tb2t(get(int,int,t2tb1(X4),t2tb(X8))) )
| $less(X8,X7)
| ~ $less(X8,X5) )
& ! [X9: $int] :
( $less(tb2t(get(int,int,t2tb1(X3),t2tb(X2))),tb2t(get(int,int,t2tb1(X4),t2tb(X9))))
| $less(X9,X6)
| ~ $less(X9,X1) )
& ~ $less(X7,X2)
& $less(X7,X5) )
& ~ $less(X2,0)
& $less(X2,X0)
& $less($sum(X2,1),X1)
& ~ $less(X0,X1)
& ~ $less(X1,X2)
& ~ $less(X2,0)
& ~ $less(X0,0) ),
inference(ennf_transformation,[],[f134]) ).
tff(f142,plain,
? [X3: map_int_int,X1: $int,X2: $int,X0: $int] :
( ~ $less(X0,X1)
& ~ $less(X2,0)
& ? [X7: $int,X5: $int,X4: map_int_int,X6: $int] :
( permut_sub1(int,mk_array1(int,X0,t2tb1(X3)),mk_array1(int,X0,t2tb1(X4)),X2,X1)
& $less(X7,X5)
& $less(X5,X0)
& ~ $less(X5,0)
& ~ $less(X5,0)
& $less(X5,X6)
& ! [X10: $int] :
( ~ $less(X10,X7)
| $less(X10,X2)
| $less(tb2t(get(int,int,t2tb1(X4),t2tb(X10))),tb2t(get(int,int,t2tb1(X3),t2tb(X2)))) )
& ~ $less(X6,X5)
& $less(X7,X0)
& ! [X8: $int] :
( ( tb2t(get(int,int,t2tb1(X3),t2tb(X2))) = tb2t(get(int,int,t2tb1(X4),t2tb(X8))) )
| ~ $less(X8,X5)
| $less(X8,X7) )
& ~ $less(X7,X2)
& ? [X11: map_int_int] :
( ~ $less(X0,0)
& ? [X12: $int] :
( ? [X13: $int] :
( ( $sum(X5,1) = X13 )
& ? [X14: $int] :
( ~ $less(X14,X2)
& ~ $less(tb2t(get(int,int,t2tb1(X11),t2tb(X14))),tb2t(get(int,int,t2tb1(X3),t2tb(X2))))
& $less(X14,X12) )
& permut_sub1(int,mk_array1(int,X0,t2tb1(X4)),mk_array1(int,X0,t2tb1(X11)),X2,X1) )
& ( $sum(X7,1) = X12 ) )
& exchange3(int,mk_array1(int,X0,t2tb1(X4)),mk_array1(int,X0,t2tb1(X11)),X7,X5) )
& $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),tb2t(get(int,int,t2tb1(X3),t2tb(X2))))
& ~ $less(X7,0)
& ~ $less(X1,X6)
& ~ $less(X0,0)
& $less(X5,X0)
& ! [X9: $int] :
( ~ $less(X9,X1)
| $less(tb2t(get(int,int,t2tb1(X3),t2tb(X2))),tb2t(get(int,int,t2tb1(X4),t2tb(X9))))
| $less(X9,X6) ) )
& ~ $less(X0,0)
& ~ $less(X1,X2)
& ~ $less(X2,0)
& $less(X2,X0)
& $less($sum(X2,1),X1) ),
inference(flattening,[],[f141]) ).
tff(f153,plain,
! [X1: uni,X2: ty,X0: $int] :
( ( elts(X2,mk_array1(X2,X0,X1)) = X1 )
| ~ sort1(map(int,X2),X1) ),
inference(ennf_transformation,[],[f121]) ).
tff(f154,plain,
! [X3: uni,X4: $int,X2: ty,X1: $int,X0: uni] :
( ( 0 = occ1(X2,X3,X0,X1,X4) )
| $less(X1,X4) ),
inference(ennf_transformation,[],[f113]) ).
tff(f176,plain,
! [X5: $int,X2: uni,X4: $int,X1: $int,X6: uni,X0: $int,X3: ty] :
( exchange2(X3,X2,X6,X0,X1,X4,X5)
<=> ( ( get(X3,int,X6,t2tb(X4)) = get(X3,int,X2,t2tb(X5)) )
& $less(X4,X1)
& ( get(X3,int,X2,t2tb(X4)) = get(X3,int,X6,t2tb(X5)) )
& $less(X5,X1)
& ~ $less(X5,X0)
& ! [X7: $int] :
( ( get(X3,int,X6,t2tb(X7)) = get(X3,int,X2,t2tb(X7)) )
| ( X5 = X7 )
| ( X4 = X7 )
| ~ $less(X7,X1)
| $less(X7,X0) )
& ~ $less(X4,X0) ) ),
inference(ennf_transformation,[],[f91]) ).
tff(f177,plain,
! [X2: uni,X5: $int,X0: $int,X1: $int,X3: ty,X6: uni,X4: $int] :
( ( $less(X5,X1)
& ( get(X3,int,X2,t2tb(X4)) = get(X3,int,X6,t2tb(X5)) )
& ( get(X3,int,X6,t2tb(X4)) = get(X3,int,X2,t2tb(X5)) )
& ! [X7: $int] :
( ( X5 = X7 )
| $less(X7,X0)
| ( X4 = X7 )
| ( get(X3,int,X6,t2tb(X7)) = get(X3,int,X2,t2tb(X7)) )
| ~ $less(X7,X1) )
& ~ $less(X4,X0)
& ~ $less(X5,X0)
& $less(X4,X1) )
<=> exchange2(X3,X2,X6,X0,X1,X4,X5) ),
inference(flattening,[],[f176]) ).
tff(f188,plain,
! [X0: uni,X1: ty,X2: $int,X3: $int,X4: $int] :
( ~ $less(X3,X4)
| $less(0,occ1(X1,get(X1,int,X0,t2tb(X3)),X0,X2,X4))
| $less(X3,X2) ),
inference(rectify,[],[f139]) ).
tff(f193,plain,
! [X0: ty,X2: uni,X4: $int,X1: uni,X3: $int] :
( ( ( ( length1(X0,X1) = length1(X0,X2) )
& exchange2(X0,elts(X0,X1),elts(X0,X2),0,length1(X0,X1),X3,X4) )
| ~ exchange3(X0,X1,X2,X3,X4) )
& ( exchange3(X0,X1,X2,X3,X4)
| ( length1(X0,X1) != length1(X0,X2) )
| ~ exchange2(X0,elts(X0,X1),elts(X0,X2),0,length1(X0,X1),X3,X4) ) ),
inference(nnf_transformation,[],[f44]) ).
tff(f194,plain,
! [X0: ty,X2: uni,X4: $int,X1: uni,X3: $int] :
( ( ( ( length1(X0,X1) = length1(X0,X2) )
& exchange2(X0,elts(X0,X1),elts(X0,X2),0,length1(X0,X1),X3,X4) )
| ~ exchange3(X0,X1,X2,X3,X4) )
& ( exchange3(X0,X1,X2,X3,X4)
| ( length1(X0,X1) != length1(X0,X2) )
| ~ exchange2(X0,elts(X0,X1),elts(X0,X2),0,length1(X0,X1),X3,X4) ) ),
inference(flattening,[],[f193]) ).
tff(f195,plain,
! [X0: ty,X1: uni,X2: $int,X3: uni,X4: $int] :
( ( ( ( length1(X0,X1) = length1(X0,X3) )
& exchange2(X0,elts(X0,X3),elts(X0,X1),0,length1(X0,X3),X4,X2) )
| ~ exchange3(X0,X3,X1,X4,X2) )
& ( exchange3(X0,X3,X1,X4,X2)
| ( length1(X0,X1) != length1(X0,X3) )
| ~ exchange2(X0,elts(X0,X3),elts(X0,X1),0,length1(X0,X3),X4,X2) ) ),
inference(rectify,[],[f194]) ).
tff(f199,plain,
! [X4: $int,X0: uni,X2: uni,X1: ty,X3: $int] :
( ( permut3(X1,X2,X0,X3,X4)
| $less(X4,0)
| ~ permut2(X1,elts(X1,X2),elts(X1,X0),X3,X4)
| ( length1(X1,X2) != length1(X1,X0) )
| $less(X3,0)
| $less(length1(X1,X2),X3)
| $less(length1(X1,X2),X4) )
& ( ( ~ $less(X4,0)
& permut2(X1,elts(X1,X2),elts(X1,X0),X3,X4)
& ( length1(X1,X2) = length1(X1,X0) )
& ~ $less(X3,0)
& ~ $less(length1(X1,X2),X3)
& ~ $less(length1(X1,X2),X4) )
| ~ permut3(X1,X2,X0,X3,X4) ) ),
inference(nnf_transformation,[],[f101]) ).
tff(f200,plain,
! [X4: $int,X0: uni,X2: uni,X1: ty,X3: $int] :
( ( permut3(X1,X2,X0,X3,X4)
| $less(X4,0)
| ~ permut2(X1,elts(X1,X2),elts(X1,X0),X3,X4)
| ( length1(X1,X2) != length1(X1,X0) )
| $less(X3,0)
| $less(length1(X1,X2),X3)
| $less(length1(X1,X2),X4) )
& ( ( ~ $less(X4,0)
& permut2(X1,elts(X1,X2),elts(X1,X0),X3,X4)
& ( length1(X1,X2) = length1(X1,X0) )
& ~ $less(X3,0)
& ~ $less(length1(X1,X2),X3)
& ~ $less(length1(X1,X2),X4) )
| ~ permut3(X1,X2,X0,X3,X4) ) ),
inference(flattening,[],[f199]) ).
tff(f201,plain,
! [X0: $int,X1: uni,X2: uni,X3: ty,X4: $int] :
( ( permut3(X3,X2,X1,X4,X0)
| $less(X0,0)
| ~ permut2(X3,elts(X3,X2),elts(X3,X1),X4,X0)
| ( length1(X3,X1) != length1(X3,X2) )
| $less(X4,0)
| $less(length1(X3,X2),X4)
| $less(length1(X3,X2),X0) )
& ( ( ~ $less(X0,0)
& permut2(X3,elts(X3,X2),elts(X3,X1),X4,X0)
& ( length1(X3,X1) = length1(X3,X2) )
& ~ $less(X4,0)
& ~ $less(length1(X3,X2),X4)
& ~ $less(length1(X3,X2),X0) )
| ~ permut3(X3,X2,X1,X4,X0) ) ),
inference(rectify,[],[f200]) ).
tff(f204,plain,
! [X0: uni,X1: $int,X2: ty,X3: $int,X4: uni] :
( ( 0 = occ1(X2,X0,X4,X3,X1) )
| $less(X3,X1) ),
inference(rectify,[],[f154]) ).
tff(f212,plain,
! [X0: uni,X1: ty,X2: $int] :
( ( elts(X1,mk_array1(X1,X2,X0)) = X0 )
| ~ sort1(map(int,X1),X0) ),
inference(rectify,[],[f153]) ).
tff(f213,plain,
! [X2: uni,X5: $int,X0: $int,X1: $int,X3: ty,X6: uni,X4: $int] :
( ( ( $less(X5,X1)
& ( get(X3,int,X2,t2tb(X4)) = get(X3,int,X6,t2tb(X5)) )
& ( get(X3,int,X6,t2tb(X4)) = get(X3,int,X2,t2tb(X5)) )
& ! [X7: $int] :
( ( X5 = X7 )
| $less(X7,X0)
| ( X4 = X7 )
| ( get(X3,int,X6,t2tb(X7)) = get(X3,int,X2,t2tb(X7)) )
| ~ $less(X7,X1) )
& ~ $less(X4,X0)
& ~ $less(X5,X0)
& $less(X4,X1) )
| ~ exchange2(X3,X2,X6,X0,X1,X4,X5) )
& ( exchange2(X3,X2,X6,X0,X1,X4,X5)
| ~ $less(X5,X1)
| ( get(X3,int,X2,t2tb(X4)) != get(X3,int,X6,t2tb(X5)) )
| ( get(X3,int,X6,t2tb(X4)) != get(X3,int,X2,t2tb(X5)) )
| ? [X7: $int] :
( ( X5 != X7 )
& ~ $less(X7,X0)
& ( X4 != X7 )
& ( get(X3,int,X6,t2tb(X7)) != get(X3,int,X2,t2tb(X7)) )
& $less(X7,X1) )
| $less(X4,X0)
| $less(X5,X0)
| ~ $less(X4,X1) ) ),
inference(nnf_transformation,[],[f177]) ).
tff(f214,plain,
! [X2: uni,X5: $int,X0: $int,X1: $int,X3: ty,X6: uni,X4: $int] :
( ( ( $less(X5,X1)
& ( get(X3,int,X2,t2tb(X4)) = get(X3,int,X6,t2tb(X5)) )
& ( get(X3,int,X6,t2tb(X4)) = get(X3,int,X2,t2tb(X5)) )
& ! [X7: $int] :
( ( X5 = X7 )
| $less(X7,X0)
| ( X4 = X7 )
| ( get(X3,int,X6,t2tb(X7)) = get(X3,int,X2,t2tb(X7)) )
| ~ $less(X7,X1) )
& ~ $less(X4,X0)
& ~ $less(X5,X0)
& $less(X4,X1) )
| ~ exchange2(X3,X2,X6,X0,X1,X4,X5) )
& ( exchange2(X3,X2,X6,X0,X1,X4,X5)
| ~ $less(X5,X1)
| ( get(X3,int,X2,t2tb(X4)) != get(X3,int,X6,t2tb(X5)) )
| ( get(X3,int,X6,t2tb(X4)) != get(X3,int,X2,t2tb(X5)) )
| ? [X7: $int] :
( ( X5 != X7 )
& ~ $less(X7,X0)
& ( X4 != X7 )
& ( get(X3,int,X6,t2tb(X7)) != get(X3,int,X2,t2tb(X7)) )
& $less(X7,X1) )
| $less(X4,X0)
| $less(X5,X0)
| ~ $less(X4,X1) ) ),
inference(flattening,[],[f213]) ).
tff(f215,plain,
! [X0: uni,X1: $int,X2: $int,X3: $int,X4: ty,X5: uni,X6: $int] :
( ( ( $less(X1,X3)
& ( get(X4,int,X0,t2tb(X6)) = get(X4,int,X5,t2tb(X1)) )
& ( get(X4,int,X5,t2tb(X6)) = get(X4,int,X0,t2tb(X1)) )
& ! [X7: $int] :
( ( X1 = X7 )
| $less(X7,X2)
| ( X6 = X7 )
| ( get(X4,int,X5,t2tb(X7)) = get(X4,int,X0,t2tb(X7)) )
| ~ $less(X7,X3) )
& ~ $less(X6,X2)
& ~ $less(X1,X2)
& $less(X6,X3) )
| ~ exchange2(X4,X0,X5,X2,X3,X6,X1) )
& ( exchange2(X4,X0,X5,X2,X3,X6,X1)
| ~ $less(X1,X3)
| ( get(X4,int,X0,t2tb(X6)) != get(X4,int,X5,t2tb(X1)) )
| ( get(X4,int,X5,t2tb(X6)) != get(X4,int,X0,t2tb(X1)) )
| ? [X8: $int] :
( ( X1 != X8 )
& ~ $less(X8,X2)
& ( X6 != X8 )
& ( get(X4,int,X0,t2tb(X8)) != get(X4,int,X5,t2tb(X8)) )
& $less(X8,X3) )
| $less(X6,X2)
| $less(X1,X2)
| ~ $less(X6,X3) ) ),
inference(rectify,[],[f214]) ).
tff(f216,plain,
! [X0: uni,X1: $int,X2: $int,X3: $int,X4: ty,X5: uni,X6: $int] :
( ( ( $less(X1,X3)
& ( get(X4,int,X0,t2tb(X6)) = get(X4,int,X5,t2tb(X1)) )
& ( get(X4,int,X5,t2tb(X6)) = get(X4,int,X0,t2tb(X1)) )
& ! [X7: $int] :
( ( X1 = X7 )
| $less(X7,X2)
| ( X6 = X7 )
| ( get(X4,int,X5,t2tb(X7)) = get(X4,int,X0,t2tb(X7)) )
| ~ $less(X7,X3) )
& ~ $less(X6,X2)
& ~ $less(X1,X2)
& $less(X6,X3) )
| ~ exchange2(X4,X0,X5,X2,X3,X6,X1) )
& ( exchange2(X4,X0,X5,X2,X3,X6,X1)
| ~ $less(X1,X3)
| ( get(X4,int,X0,t2tb(X6)) != get(X4,int,X5,t2tb(X1)) )
| ( get(X4,int,X5,t2tb(X6)) != get(X4,int,X0,t2tb(X1)) )
| ( ( sK2(X0,X1,X2,X3,X4,X5,X6) != X1 )
& ~ $less(sK2(X0,X1,X2,X3,X4,X5,X6),X2)
& ( sK2(X0,X1,X2,X3,X4,X5,X6) != X6 )
& ( get(X4,int,X0,t2tb(sK2(X0,X1,X2,X3,X4,X5,X6))) != get(X4,int,X5,t2tb(sK2(X0,X1,X2,X3,X4,X5,X6))) )
& $less(sK2(X0,X1,X2,X3,X4,X5,X6),X3) )
| $less(X6,X2)
| $less(X1,X2)
| ~ $less(X6,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X8,sK2(X0,X1,X2,X3,X4,X5,X6))],[f215]) ).
tff(f218,plain,
! [X0: $int,X1: uni,X2: ty] : ( length1(X2,mk_array1(X2,X0,X1)) = X0 ),
inference(rectify,[],[f95]) ).
tff(f220,plain,
! [X3: uni,X2: $int,X4: ty,X1: uni,X0: $int] :
( ( ( map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),X0,length1(X4,X1))
& permut3(X4,X1,X3,X2,X0)
& map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),0,X2) )
| ~ permut_sub1(X4,X1,X3,X2,X0) )
& ( permut_sub1(X4,X1,X3,X2,X0)
| ~ map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),X0,length1(X4,X1))
| ~ permut3(X4,X1,X3,X2,X0)
| ~ map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),0,X2) ) ),
inference(nnf_transformation,[],[f94]) ).
tff(f221,plain,
! [X3: uni,X2: $int,X4: ty,X1: uni,X0: $int] :
( ( ( map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),X0,length1(X4,X1))
& permut3(X4,X1,X3,X2,X0)
& map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),0,X2) )
| ~ permut_sub1(X4,X1,X3,X2,X0) )
& ( permut_sub1(X4,X1,X3,X2,X0)
| ~ map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),X0,length1(X4,X1))
| ~ permut3(X4,X1,X3,X2,X0)
| ~ map_eq_sub1(X4,elts(X4,X1),elts(X4,X3),0,X2) ) ),
inference(flattening,[],[f220]) ).
tff(f222,plain,
! [X0: uni,X1: $int,X2: ty,X3: uni,X4: $int] :
( ( ( map_eq_sub1(X2,elts(X2,X3),elts(X2,X0),X4,length1(X2,X3))
& permut3(X2,X3,X0,X1,X4)
& map_eq_sub1(X2,elts(X2,X3),elts(X2,X0),0,X1) )
| ~ permut_sub1(X2,X3,X0,X1,X4) )
& ( permut_sub1(X2,X3,X0,X1,X4)
| ~ map_eq_sub1(X2,elts(X2,X3),elts(X2,X0),X4,length1(X2,X3))
| ~ permut3(X2,X3,X0,X1,X4)
| ~ map_eq_sub1(X2,elts(X2,X3),elts(X2,X0),0,X1) ) ),
inference(rectify,[],[f221]) ).
tff(f225,plain,
? [X0: map_int_int,X1: $int,X2: $int,X3: $int] :
( ~ $less(X3,X1)
& ~ $less(X2,0)
& ? [X4: $int,X5: $int,X6: map_int_int,X7: $int] :
( permut_sub1(int,mk_array1(int,X3,t2tb1(X0)),mk_array1(int,X3,t2tb1(X6)),X2,X1)
& $less(X4,X5)
& $less(X5,X3)
& ~ $less(X5,0)
& ~ $less(X5,0)
& $less(X5,X7)
& ! [X8: $int] :
( ~ $less(X8,X4)
| $less(X8,X2)
| $less(tb2t(get(int,int,t2tb1(X6),t2tb(X8))),tb2t(get(int,int,t2tb1(X0),t2tb(X2)))) )
& ~ $less(X7,X5)
& $less(X4,X3)
& ! [X9: $int] :
( ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) = tb2t(get(int,int,t2tb1(X6),t2tb(X9))) )
| ~ $less(X9,X5)
| $less(X9,X4) )
& ~ $less(X4,X2)
& ? [X10: map_int_int] :
( ~ $less(X3,0)
& ? [X11: $int] :
( ? [X12: $int] :
( ( $sum(X5,1) = X12 )
& ? [X13: $int] :
( ~ $less(X13,X2)
& ~ $less(tb2t(get(int,int,t2tb1(X10),t2tb(X13))),tb2t(get(int,int,t2tb1(X0),t2tb(X2))))
& $less(X13,X11) )
& permut_sub1(int,mk_array1(int,X3,t2tb1(X6)),mk_array1(int,X3,t2tb1(X10)),X2,X1) )
& ( $sum(X4,1) = X11 ) )
& exchange3(int,mk_array1(int,X3,t2tb1(X6)),mk_array1(int,X3,t2tb1(X10)),X4,X5) )
& $less(tb2t(get(int,int,t2tb1(X6),t2tb(X5))),tb2t(get(int,int,t2tb1(X0),t2tb(X2))))
& ~ $less(X4,0)
& ~ $less(X1,X7)
& ~ $less(X3,0)
& $less(X5,X3)
& ! [X14: $int] :
( ~ $less(X14,X1)
| $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),tb2t(get(int,int,t2tb1(X6),t2tb(X14))))
| $less(X14,X7) ) )
& ~ $less(X3,0)
& ~ $less(X1,X2)
& ~ $less(X2,0)
& $less(X2,X3)
& $less($sum(X2,1),X1) ),
inference(rectify,[],[f142]) ).
tff(f226,plain,
( ~ $less(sK7,sK5)
& ~ $less(sK6,0)
& permut_sub1(int,mk_array1(int,sK7,t2tb1(sK4)),mk_array1(int,sK7,t2tb1(sK10)),sK6,sK5)
& $less(sK8,sK9)
& $less(sK9,sK7)
& ~ $less(sK9,0)
& ~ $less(sK9,0)
& $less(sK9,sK11)
& ! [X8: $int] :
( ~ $less(X8,sK8)
| $less(X8,sK6)
| $less(tb2t(get(int,int,t2tb1(sK10),t2tb(X8))),tb2t(get(int,int,t2tb1(sK4),t2tb(sK6)))) )
& ~ $less(sK11,sK9)
& $less(sK8,sK7)
& ! [X9: $int] :
( ( tb2t(get(int,int,t2tb1(sK10),t2tb(X9))) = tb2t(get(int,int,t2tb1(sK4),t2tb(sK6))) )
| ~ $less(X9,sK9)
| $less(X9,sK8) )
& ~ $less(sK8,sK6)
& ~ $less(sK7,0)
& ( sK14 = $sum(sK9,1) )
& ~ $less(sK15,sK6)
& ~ $less(tb2t(get(int,int,t2tb1(sK12),t2tb(sK15))),tb2t(get(int,int,t2tb1(sK4),t2tb(sK6))))
& $less(sK15,sK13)
& permut_sub1(int,mk_array1(int,sK7,t2tb1(sK10)),mk_array1(int,sK7,t2tb1(sK12)),sK6,sK5)
& ( $sum(sK8,1) = sK13 )
& exchange3(int,mk_array1(int,sK7,t2tb1(sK10)),mk_array1(int,sK7,t2tb1(sK12)),sK8,sK9)
& $less(tb2t(get(int,int,t2tb1(sK10),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK4),t2tb(sK6))))
& ~ $less(sK8,0)
& ~ $less(sK5,sK11)
& ~ $less(sK7,0)
& $less(sK9,sK7)
& ! [X14: $int] :
( ~ $less(X14,sK5)
| $less(tb2t(get(int,int,t2tb1(sK4),t2tb(sK6))),tb2t(get(int,int,t2tb1(sK10),t2tb(X14))))
| $less(X14,sK11) )
& ~ $less(sK7,0)
& ~ $less(sK5,sK6)
& ~ $less(sK6,0)
& $less(sK6,sK7)
& $less($sum(sK6,1),sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X3,sK7),skolemize(X4,sK8),skolemize(X5,sK9),skolemize(X6,sK10),skolemize(X7,sK11),skolemize(X10,sK12),skolemize(X11,sK13),skolemize(X12,sK14),skolemize(X13,sK15)],[f225]) ).
tff(f242,plain,
! [X0: map_int_int] : sort1(map(int,int),t2tb1(X0)),
inference(cnf_transformation,[],[f33]) ).
tff(f248,plain,
! [X2: $int,X3: $int,X0: uni,X1: ty,X4: $int] :
( $less(0,occ1(X1,get(X1,int,X0,t2tb(X3)),X0,X2,X4))
| $less(X3,X2)
| ~ $less(X3,X4) ),
inference(cnf_transformation,[],[f188]) ).
tff(f256,plain,
! [X2: $int,X3: uni,X0: ty,X1: uni,X4: $int] :
( ~ exchange3(X0,X3,X1,X4,X2)
| exchange2(X0,elts(X0,X3),elts(X0,X1),0,length1(X0,X3),X4,X2) ),
inference(cnf_transformation,[],[f195]) ).
tff(f263,plain,
! [X2: uni,X3: ty,X0: $int,X1: uni,X4: $int] :
( ~ permut3(X3,X2,X1,X4,X0)
| ~ $less(length1(X3,X2),X0) ),
inference(cnf_transformation,[],[f201]) ).
tff(f274,plain,
! [X2: ty,X3: $int,X0: uni,X1: $int,X4: uni] :
( ( 0 = occ1(X2,X0,X4,X3,X1) )
| $less(X3,X1) ),
inference(cnf_transformation,[],[f204]) ).
tff(f285,plain,
! [X2: $int,X0: uni,X1: ty] :
( ( elts(X1,mk_array1(X1,X2,X0)) = X0 )
| ~ sort1(map(int,X1),X0) ),
inference(cnf_transformation,[],[f212]) ).
tff(f295,plain,
! [X2: $int,X3: $int,X0: uni,X1: $int,X6: $int,X7: $int,X4: ty,X5: uni] :
( ~ exchange2(X4,X0,X5,X2,X3,X6,X1)
| ( X1 = X7 )
| ~ $less(X7,X3)
| ( get(X4,int,X5,t2tb(X7)) = get(X4,int,X0,t2tb(X7)) )
| $less(X7,X2)
| ( X6 = X7 ) ),
inference(cnf_transformation,[],[f216]) ).
tff(f296,plain,
! [X2: $int,X3: $int,X0: uni,X1: $int,X6: $int,X4: ty,X5: uni] :
( ~ exchange2(X4,X0,X5,X2,X3,X6,X1)
| ( get(X4,int,X5,t2tb(X6)) = get(X4,int,X0,t2tb(X1)) ) ),
inference(cnf_transformation,[],[f216]) ).
tff(f301,plain,
! [X2: ty,X0: $int,X1: uni] : ( length1(X2,mk_array1(X2,X0,X1)) = X0 ),
inference(cnf_transformation,[],[f218]) ).
tff(f307,plain,
! [X2: ty,X3: uni,X0: uni,X1: $int,X4: $int] :
( ~ permut_sub1(X2,X3,X0,X1,X4)
| permut3(X2,X3,X0,X1,X4) ),
inference(cnf_transformation,[],[f222]) ).
tff(f314,plain,
~ $less(sK6,0),
inference(cnf_transformation,[],[f226]) ).
tff(f320,plain,
~ $less(sK5,sK11),
inference(cnf_transformation,[],[f226]) ).
tff(f322,plain,
$less(tb2t(get(int,int,t2tb1(sK10),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK4),t2tb(sK6)))),
inference(cnf_transformation,[],[f226]) ).
tff(f323,plain,
exchange3(int,mk_array1(int,sK7,t2tb1(sK10)),mk_array1(int,sK7,t2tb1(sK12)),sK8,sK9),
inference(cnf_transformation,[],[f226]) ).
tff(f324,plain,
$sum(sK8,1) = sK13,
inference(cnf_transformation,[],[f226]) ).
tff(f326,plain,
$less(sK15,sK13),
inference(cnf_transformation,[],[f226]) ).
tff(f327,plain,
~ $less(tb2t(get(int,int,t2tb1(sK12),t2tb(sK15))),tb2t(get(int,int,t2tb1(sK4),t2tb(sK6)))),
inference(cnf_transformation,[],[f226]) ).
tff(f328,plain,
~ $less(sK15,sK6),
inference(cnf_transformation,[],[f226]) ).
tff(f335,plain,
! [X8: $int] :
( ~ $less(X8,sK8)
| $less(X8,sK6)
| $less(tb2t(get(int,int,t2tb1(sK10),t2tb(X8))),tb2t(get(int,int,t2tb1(sK4),t2tb(sK6)))) ),
inference(cnf_transformation,[],[f226]) ).
tff(f336,plain,
$less(sK9,sK11),
inference(cnf_transformation,[],[f226]) ).
tff(f340,plain,
$less(sK8,sK9),
inference(cnf_transformation,[],[f226]) ).
tff(f341,plain,
permut_sub1(int,mk_array1(int,sK7,t2tb1(sK4)),mk_array1(int,sK7,t2tb1(sK10)),sK6,sK5),
inference(cnf_transformation,[],[f226]) ).
tff(f376,definition,
sF19 = t2tb1(sK4),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f377,definition,
sF20 = mk_array1(int,sK7,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f378,definition,
sF21 = t2tb1(sK10),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f379,plain,
t2tb1(sK10) = sF21,
inference(reorient_equations,[],[f378]) ).
tff(f380,definition,
sF22 = mk_array1(int,sK7,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f381,plain,
permut_sub1(int,sF20,sF22,sK6,sK5),
inference(definition_folding,[],[f341,f380,f379,f377,f376]) ).
tff(f382,definition,
! [X8: $int] : ( sF23(X8) = get(int,int,sF21,t2tb(X8)) ),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f383,definition,
! [X8: $int] : ( sF24(X8) = tb2t(sF23(X8)) ),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f384,plain,
! [X8: $int] : ( tb2t(sF23(X8)) = sF24(X8) ),
inference(reorient_equations,[],[f383]) ).
tff(f385,definition,
sF25 = t2tb(sK6),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f386,definition,
sF26 = get(int,int,sF19,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f387,definition,
sF27 = tb2t(sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f388,plain,
tb2t(sF26) = sF27,
inference(reorient_equations,[],[f387]) ).
tff(f389,plain,
! [X8: $int] :
( $less(sF24(X8),sF27)
| ~ $less(X8,sK8)
| $less(X8,sK6) ),
inference(definition_folding,[],[f335,f388,f386,f385,f376,f384,f382,f379]) ).
tff(f394,definition,
sF29 = t2tb1(sK12),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f395,definition,
sF30 = t2tb(sK15),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f396,definition,
sF31 = get(int,int,sF29,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f397,definition,
sF32 = tb2t(sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f398,plain,
~ $less(sF32,sF27),
inference(definition_folding,[],[f327,f388,f386,f385,f376,f397,f396,f395,f394]) ).
tff(f399,definition,
sF33 = mk_array1(int,sK7,sF29),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f400,plain,
mk_array1(int,sK7,sF29) = sF33,
inference(reorient_equations,[],[f399]) ).
tff(f402,definition,
sF34 = $sum(sK8,1),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f403,plain,
$sum(sK8,1) = sF34,
inference(reorient_equations,[],[f402]) ).
tff(f404,plain,
sK13 = sF34,
inference(definition_folding,[],[f324,f403]) ).
tff(f405,plain,
exchange3(int,sF22,sF33,sK8,sK9),
inference(definition_folding,[],[f323,f400,f394,f380,f379]) ).
tff(f406,definition,
sF35 = t2tb(sK9),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f407,definition,
sF36 = get(int,int,sF21,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
tff(f408,definition,
sF37 = tb2t(sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
tff(f409,plain,
$less(sF37,sF27),
inference(definition_folding,[],[f322,f388,f386,f385,f376,f408,f407,f406,f379]) ).
tff(f417,definition,
( spl39_1
<=> ( sF20 = mk_array1(int,sK7,sF19) ) ),
introduced(definition,[new_symbols(definition,[spl39_1])],[avatar_definition]) ).
tff(f419,plain,
( ( sF20 = mk_array1(int,sK7,sF19) )
| ~ spl39_1 ),
inference(avatar_component_clause,[],[f417]) ).
tff(f420,plain,
spl39_1,
inference(avatar_split_clause,[],[f377,f417]) ).
tff(f422,definition,
( spl39_2
<=> ( mk_array1(int,sK7,sF29) = sF33 ) ),
introduced(definition,[new_symbols(definition,[spl39_2])],[avatar_definition]) ).
tff(f424,plain,
( ( mk_array1(int,sK7,sF29) = sF33 )
| ~ spl39_2 ),
inference(avatar_component_clause,[],[f422]) ).
tff(f425,plain,
spl39_2,
inference(avatar_split_clause,[],[f400,f422]) ).
tff(f427,definition,
( spl39_3
<=> ( t2tb1(sK10) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl39_3])],[avatar_definition]) ).
tff(f429,plain,
( ( t2tb1(sK10) = sF21 )
| ~ spl39_3 ),
inference(avatar_component_clause,[],[f427]) ).
tff(f430,plain,
spl39_3,
inference(avatar_split_clause,[],[f379,f427]) ).
tff(f452,definition,
( spl39_8
<=> $less(sF32,sF27) ),
introduced(definition,[new_symbols(definition,[spl39_8])],[avatar_definition]) ).
tff(f455,plain,
~ spl39_8,
inference(avatar_split_clause,[],[f398,f452]) ).
tff(f457,definition,
( spl39_9
<=> $less(sK15,sK13) ),
introduced(definition,[new_symbols(definition,[spl39_9])],[avatar_definition]) ).
tff(f459,plain,
( $less(sK15,sK13)
| ~ spl39_9 ),
inference(avatar_component_clause,[],[f457]) ).
tff(f460,plain,
spl39_9,
inference(avatar_split_clause,[],[f326,f457]) ).
tff(f472,definition,
( spl39_12
<=> ( sF30 = t2tb(sK15) ) ),
introduced(definition,[new_symbols(definition,[spl39_12])],[avatar_definition]) ).
tff(f474,plain,
( ( sF30 = t2tb(sK15) )
| ~ spl39_12 ),
inference(avatar_component_clause,[],[f472]) ).
tff(f475,plain,
spl39_12,
inference(avatar_split_clause,[],[f395,f472]) ).
tff(f477,definition,
( spl39_13
<=> ( sK13 = sF34 ) ),
introduced(definition,[new_symbols(definition,[spl39_13])],[avatar_definition]) ).
tff(f479,plain,
( ( sK13 = sF34 )
| ~ spl39_13 ),
inference(avatar_component_clause,[],[f477]) ).
tff(f480,plain,
spl39_13,
inference(avatar_split_clause,[],[f404,f477]) ).
tff(f482,definition,
( spl39_14
<=> ( $sum(sK8,1) = sF34 ) ),
introduced(definition,[new_symbols(definition,[spl39_14])],[avatar_definition]) ).
tff(f484,plain,
( ( $sum(sK8,1) = sF34 )
| ~ spl39_14 ),
inference(avatar_component_clause,[],[f482]) ).
tff(f485,plain,
spl39_14,
inference(avatar_split_clause,[],[f403,f482]) ).
tff(f487,definition,
( spl39_15
<=> $less(sF37,sF27) ),
introduced(definition,[new_symbols(definition,[spl39_15])],[avatar_definition]) ).
tff(f490,plain,
spl39_15,
inference(avatar_split_clause,[],[f409,f487]) ).
tff(f497,definition,
( spl39_17
<=> $less(sK5,sK11) ),
introduced(definition,[new_symbols(definition,[spl39_17])],[avatar_definition]) ).
tff(f500,plain,
~ spl39_17,
inference(avatar_split_clause,[],[f320,f497]) ).
tff(f507,definition,
( spl39_19
<=> ( sF35 = t2tb(sK9) ) ),
introduced(definition,[new_symbols(definition,[spl39_19])],[avatar_definition]) ).
tff(f509,plain,
( ( sF35 = t2tb(sK9) )
| ~ spl39_19 ),
inference(avatar_component_clause,[],[f507]) ).
tff(f510,plain,
spl39_19,
inference(avatar_split_clause,[],[f406,f507]) ).
tff(f512,definition,
( spl39_20
<=> ( sF22 = mk_array1(int,sK7,sF21) ) ),
introduced(definition,[new_symbols(definition,[spl39_20])],[avatar_definition]) ).
tff(f514,plain,
( ( sF22 = mk_array1(int,sK7,sF21) )
| ~ spl39_20 ),
inference(avatar_component_clause,[],[f512]) ).
tff(f515,plain,
spl39_20,
inference(avatar_split_clause,[],[f380,f512]) ).
tff(f517,definition,
( spl39_21
<=> $less(sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl39_21])],[avatar_definition]) ).
tff(f520,plain,
spl39_21,
inference(avatar_split_clause,[],[f340,f517]) ).
tff(f537,definition,
( spl39_25
<=> ( sF32 = tb2t(sF31) ) ),
introduced(definition,[new_symbols(definition,[spl39_25])],[avatar_definition]) ).
tff(f540,plain,
spl39_25,
inference(avatar_split_clause,[],[f397,f537]) ).
tff(f542,definition,
( spl39_26
<=> ( sF36 = get(int,int,sF21,sF35) ) ),
introduced(definition,[new_symbols(definition,[spl39_26])],[avatar_definition]) ).
tff(f544,plain,
( ( sF36 = get(int,int,sF21,sF35) )
| ~ spl39_26 ),
inference(avatar_component_clause,[],[f542]) ).
tff(f545,plain,
spl39_26,
inference(avatar_split_clause,[],[f407,f542]) ).
tff(f547,definition,
( spl39_27
<=> ( sF31 = get(int,int,sF29,sF30) ) ),
introduced(definition,[new_symbols(definition,[spl39_27])],[avatar_definition]) ).
tff(f549,plain,
( ( sF31 = get(int,int,sF29,sF30) )
| ~ spl39_27 ),
inference(avatar_component_clause,[],[f547]) ).
tff(f550,plain,
spl39_27,
inference(avatar_split_clause,[],[f396,f547]) ).
tff(f552,definition,
( spl39_28
<=> $less(sK15,sK6) ),
introduced(definition,[new_symbols(definition,[spl39_28])],[avatar_definition]) ).
tff(f554,plain,
( ~ $less(sK15,sK6)
| spl39_28 ),
inference(avatar_component_clause,[],[f552]) ).
tff(f555,plain,
~ spl39_28,
inference(avatar_split_clause,[],[f328,f552]) ).
tff(f577,definition,
( spl39_33
<=> $less(sK9,sK11) ),
introduced(definition,[new_symbols(definition,[spl39_33])],[avatar_definition]) ).
tff(f580,plain,
spl39_33,
inference(avatar_split_clause,[],[f336,f577]) ).
tff(f587,definition,
( spl39_35
<=> ( sF29 = t2tb1(sK12) ) ),
introduced(definition,[new_symbols(definition,[spl39_35])],[avatar_definition]) ).
tff(f589,plain,
( ( sF29 = t2tb1(sK12) )
| ~ spl39_35 ),
inference(avatar_component_clause,[],[f587]) ).
tff(f590,plain,
spl39_35,
inference(avatar_split_clause,[],[f394,f587]) ).
tff(f597,definition,
( spl39_37
<=> exchange3(int,sF22,sF33,sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl39_37])],[avatar_definition]) ).
tff(f599,plain,
( exchange3(int,sF22,sF33,sK8,sK9)
| ~ spl39_37 ),
inference(avatar_component_clause,[],[f597]) ).
tff(f600,plain,
spl39_37,
inference(avatar_split_clause,[],[f405,f597]) ).
tff(f602,definition,
( spl39_38
<=> permut_sub1(int,sF20,sF22,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl39_38])],[avatar_definition]) ).
tff(f604,plain,
( permut_sub1(int,sF20,sF22,sK6,sK5)
| ~ spl39_38 ),
inference(avatar_component_clause,[],[f602]) ).
tff(f605,plain,
spl39_38,
inference(avatar_split_clause,[],[f381,f602]) ).
tff(f607,definition,
( spl39_39
<=> $less(sK6,0) ),
introduced(definition,[new_symbols(definition,[spl39_39])],[avatar_definition]) ).
tff(f609,plain,
( ~ $less(sK6,0)
| spl39_39 ),
inference(avatar_component_clause,[],[f607]) ).
tff(f610,plain,
~ spl39_39,
inference(avatar_split_clause,[],[f314,f607]) ).
tff(f627,definition,
( spl39_43
<=> ( sF37 = tb2t(sF36) ) ),
introduced(definition,[new_symbols(definition,[spl39_43])],[avatar_definition]) ).
tff(f630,plain,
spl39_43,
inference(avatar_split_clause,[],[f408,f627]) ).
tff(f653,plain,
( sort1(map(int,int),sF21)
| ~ spl39_3 ),
inference(superposition,[],[f242,f429]) ).
tff(f655,definition,
( spl39_47
<=> sort1(map(int,int),sF21) ),
introduced(definition,[new_symbols(definition,[spl39_47])],[avatar_definition]) ).
tff(f658,plain,
( spl39_47
| ~ spl39_3 ),
inference(avatar_split_clause,[],[f653,f427,f655]) ).
tff(f695,plain,
( sort1(map(int,int),sF29)
| ~ spl39_35 ),
inference(superposition,[],[f242,f589]) ).
tff(f697,definition,
( spl39_54
<=> sort1(map(int,int),sF29) ),
introduced(definition,[new_symbols(definition,[spl39_54])],[avatar_definition]) ).
tff(f700,plain,
( spl39_54
| ~ spl39_35 ),
inference(avatar_split_clause,[],[f695,f587,f697]) ).
tff(f735,plain,
( ! [X2: $int,X3: $int,X0: ty,X1: uni] :
( $less(sK15,X2)
| $less(0,occ1(X0,get(X0,int,X1,sF30),X1,X2,X3))
| ~ $less(sK15,X3) )
| ~ spl39_12 ),
inference(superposition,[],[f248,f474]) ).
tff(f750,plain,
( ( $sum(sK8,1) = sK13 )
| ~ spl39_13
| ~ spl39_14 ),
inference(superposition,[],[f479,f484]) ).
tff(f752,definition,
( spl39_60
<=> ( $sum(sK8,1) = sK13 ) ),
introduced(definition,[new_symbols(definition,[spl39_60])],[avatar_definition]) ).
tff(f754,plain,
( ( $sum(sK8,1) = sK13 )
| ~ spl39_60 ),
inference(avatar_component_clause,[],[f752]) ).
tff(f755,plain,
( spl39_60
| ~ spl39_13
| ~ spl39_14 ),
inference(avatar_split_clause,[],[f750,f482,f477,f752]) ).
tff(f767,plain,
( ( sK7 = length1(int,sF20) )
| ~ spl39_1 ),
inference(superposition,[],[f301,f419]) ).
tff(f774,definition,
( spl39_62
<=> ( sK7 = length1(int,sF20) ) ),
introduced(definition,[new_symbols(definition,[spl39_62])],[avatar_definition]) ).
tff(f777,plain,
( spl39_62
| ~ spl39_1 ),
inference(avatar_split_clause,[],[f767,f417,f774]) ).
tff(f781,plain,
( ( sF29 = elts(int,sF33) )
| ~ sort1(map(int,int),sF29)
| ~ spl39_2 ),
inference(superposition,[],[f285,f424]) ).
tff(f789,definition,
( spl39_64
<=> ( sF29 = elts(int,sF33) ) ),
introduced(definition,[new_symbols(definition,[spl39_64])],[avatar_definition]) ).
tff(f791,plain,
( ( sF29 = elts(int,sF33) )
| ~ spl39_64 ),
inference(avatar_component_clause,[],[f789]) ).
tff(f792,plain,
( spl39_64
| ~ spl39_54
| ~ spl39_2 ),
inference(avatar_split_clause,[],[f781,f422,f697,f789]) ).
tff(f793,plain,
( $less(sK15,$sum(sK8,1))
| ~ spl39_9
| ~ spl39_60 ),
inference(superposition,[],[f459,f754]) ).
tff(f795,definition,
( spl39_65
<=> $less(sK15,$sum(sK8,1)) ),
introduced(definition,[new_symbols(definition,[spl39_65])],[avatar_definition]) ).
tff(f798,plain,
( spl39_65
| ~ spl39_9
| ~ spl39_60 ),
inference(avatar_split_clause,[],[f793,f752,f457,f795]) ).
tff(f809,plain,
( ~ sort1(map(int,int),sF21)
| ( elts(int,sF22) = sF21 )
| ~ spl39_20 ),
inference(superposition,[],[f285,f514]) ).
tff(f810,plain,
( ( length1(int,sF22) = sK7 )
| ~ spl39_20 ),
inference(superposition,[],[f301,f514]) ).
tff(f812,definition,
( spl39_66
<=> ( elts(int,sF22) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl39_66])],[avatar_definition]) ).
tff(f814,plain,
( ( elts(int,sF22) = sF21 )
| ~ spl39_66 ),
inference(avatar_component_clause,[],[f812]) ).
tff(f815,plain,
( ~ spl39_47
| spl39_66
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f809,f512,f812,f655]) ).
tff(f817,definition,
( spl39_67
<=> ( length1(int,sF22) = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl39_67])],[avatar_definition]) ).
tff(f820,plain,
( spl39_67
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f810,f512,f817]) ).
tff(f890,plain,
! [X0: $int] : ( sF24(X0) = tb2t(get(int,int,sF21,t2tb(X0))) ),
inference(superposition,[],[f384,f382]) ).
tff(f941,plain,
( permut3(int,sF20,sF22,sK6,sK5)
| ~ spl39_38 ),
inference(resolution,[],[f307,f604]) ).
tff(f950,definition,
( spl39_77
<=> permut3(int,sF20,sF22,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl39_77])],[avatar_definition]) ).
tff(f952,plain,
( permut3(int,sF20,sF22,sK6,sK5)
| ~ spl39_77 ),
inference(avatar_component_clause,[],[f950]) ).
tff(f953,plain,
( spl39_77
| ~ spl39_38 ),
inference(avatar_split_clause,[],[f941,f602,f950]) ).
tff(f977,plain,
( ~ $less(length1(int,sF20),sK5)
| ~ spl39_77 ),
inference(resolution,[],[f952,f263]) ).
tff(f986,definition,
( spl39_82
<=> $less(length1(int,sF20),sK5) ),
introduced(definition,[new_symbols(definition,[spl39_82])],[avatar_definition]) ).
tff(f989,plain,
( ~ spl39_82
| ~ spl39_77 ),
inference(avatar_split_clause,[],[f977,f950,f986]) ).
tff(f1173,plain,
( exchange2(int,elts(int,sF22),elts(int,sF33),0,length1(int,sF22),sK8,sK9)
| ~ spl39_37 ),
inference(resolution,[],[f256,f599]) ).
tff(f1175,definition,
( spl39_102
<=> exchange2(int,elts(int,sF22),elts(int,sF33),0,length1(int,sF22),sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl39_102])],[avatar_definition]) ).
tff(f1177,plain,
( exchange2(int,elts(int,sF22),elts(int,sF33),0,length1(int,sF22),sK8,sK9)
| ~ spl39_102 ),
inference(avatar_component_clause,[],[f1175]) ).
tff(f1178,plain,
( spl39_102
| ~ spl39_37 ),
inference(avatar_split_clause,[],[f1173,f597,f1175]) ).
tff(f1211,plain,
( ( get(int,int,elts(int,sF22),t2tb(sK9)) = get(int,int,elts(int,sF33),t2tb(sK8)) )
| ~ spl39_102 ),
inference(resolution,[],[f296,f1177]) ).
tff(f1212,plain,
( ( get(int,int,elts(int,sF22),t2tb(sK9)) = get(int,int,sF29,t2tb(sK8)) )
| ~ spl39_64
| ~ spl39_102 ),
inference(forward_demodulation,[],[f1211,f791]) ).
tff(f1213,plain,
( ( get(int,int,sF29,t2tb(sK8)) = get(int,int,elts(int,sF22),sF35) )
| ~ spl39_19
| ~ spl39_64
| ~ spl39_102 ),
inference(forward_demodulation,[],[f1212,f509]) ).
tff(f1214,plain,
( ( get(int,int,sF29,t2tb(sK8)) = get(int,int,sF21,sF35) )
| ~ spl39_19
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(forward_demodulation,[],[f1213,f814]) ).
tff(f1215,plain,
( ( get(int,int,sF29,t2tb(sK8)) = sF36 )
| ~ spl39_19
| ~ spl39_26
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(forward_demodulation,[],[f1214,f544]) ).
tff(f1217,definition,
( spl39_108
<=> ( get(int,int,sF29,t2tb(sK8)) = sF36 ) ),
introduced(definition,[new_symbols(definition,[spl39_108])],[avatar_definition]) ).
tff(f1220,plain,
( spl39_108
| ~ spl39_19
| ~ spl39_26
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(avatar_split_clause,[],[f1215,f1175,f812,f789,f542,f507,f1217]) ).
tff(f1259,plain,
( ! [X2: $int,X0: ty,X1: uni] :
( ~ $less(sK15,X2)
| $less(0,occ1(X0,get(X0,int,X1,sF30),X1,sK6,X2)) )
| ~ spl39_12
| spl39_28 ),
inference(resolution,[],[f735,f554]) ).
tff(f1340,plain,
( ! [X0: $int] :
( ~ $less(X0,length1(int,sF22))
| ( sK9 = X0 )
| ( sK8 = X0 )
| $less(X0,0)
| ( get(int,int,elts(int,sF22),t2tb(X0)) = get(int,int,elts(int,sF33),t2tb(X0)) ) )
| ~ spl39_102 ),
inference(resolution,[],[f295,f1177]) ).
tff(f1341,plain,
( ! [X0: $int] :
( ( sK9 = X0 )
| ( sK8 = X0 )
| $less(X0,0)
| ~ $less(X0,length1(int,sF22))
| ( get(int,int,elts(int,sF22),t2tb(X0)) = get(int,int,sF29,t2tb(X0)) ) )
| ~ spl39_64
| ~ spl39_102 ),
inference(forward_demodulation,[],[f1340,f791]) ).
tff(f1342,plain,
( ! [X0: $int] :
( $less(X0,0)
| ( sK8 = X0 )
| ( sK9 = X0 )
| ( get(int,int,sF21,t2tb(X0)) = get(int,int,sF29,t2tb(X0)) )
| ~ $less(X0,length1(int,sF22)) )
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(forward_demodulation,[],[f1341,f814]) ).
tff(f1726,plain,
! [X0: $int] :
( $less(tb2t(get(int,int,sF21,t2tb(X0))),sF27)
| $less(X0,sK6)
| ~ $less(X0,sK8) ),
inference(superposition,[],[f389,f890]) ).
tff(f3035,plain,
( ~ $less(sK15,sK8)
| $less(sK15,sK6)
| $less(tb2t(get(int,int,sF21,sF30)),sF27)
| ~ spl39_12 ),
inference(superposition,[],[f1726,f474]) ).
tff(f3058,plain,
( ~ $less(sK15,sK8)
| $less(tb2t(get(int,int,sF21,sF30)),sF27)
| ~ spl39_12
| spl39_28 ),
inference(forward_subsumption_resolution,[],[f3035,f554]) ).
tff(f3103,definition,
( spl39_204
<=> $less(tb2t(get(int,int,sF21,sF30)),sF27) ),
introduced(definition,[new_symbols(definition,[spl39_204])],[avatar_definition]) ).
tff(f3107,definition,
( spl39_205
<=> $less(sK15,sK8) ),
introduced(definition,[new_symbols(definition,[spl39_205])],[avatar_definition]) ).
tff(f3110,plain,
( spl39_204
| ~ spl39_205
| ~ spl39_12
| spl39_28 ),
inference(avatar_split_clause,[],[f3058,f552,f472,f3107,f3103]) ).
tff(f3438,definition,
( spl39_232
<=> $less(sK15,length1(int,sF22)) ),
introduced(definition,[new_symbols(definition,[spl39_232])],[avatar_definition]) ).
tff(f3442,definition,
( spl39_233
<=> ( sF31 = get(int,int,sF21,sF30) ) ),
introduced(definition,[new_symbols(definition,[spl39_233])],[avatar_definition]) ).
tff(f3568,plain,
( ! [X0: ty,X1: uni] :
( ~ $less(sK15,length1(int,sF22))
| ( sK8 = sK15 )
| ( get(int,int,sF29,t2tb(sK15)) = get(int,int,sF21,t2tb(sK15)) )
| $less(0,occ1(X0,get(X0,int,X1,sF30),X1,sK6,0))
| ( sK9 = sK15 ) )
| ~ spl39_12
| spl39_28
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(resolution,[],[f1342,f1259]) ).
tff(f3593,plain,
( ! [X0: ty,X1: uni] :
( ( sK8 = sK15 )
| ( get(int,int,sF21,sF30) = get(int,int,sF29,sF30) )
| ~ $less(sK15,length1(int,sF22))
| ( sK9 = sK15 )
| $less(0,occ1(X0,get(X0,int,X1,sF30),X1,sK6,0)) )
| ~ spl39_12
| spl39_28
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(forward_demodulation,[],[f3568,f474]) ).
tff(f3603,plain,
( ! [X0: ty,X1: uni] :
( ( sF31 = get(int,int,sF21,sF30) )
| ( sK8 = sK15 )
| $less(0,occ1(X0,get(X0,int,X1,sF30),X1,sK6,0))
| ( sK9 = sK15 )
| ~ $less(sK15,length1(int,sF22)) )
| ~ spl39_12
| ~ spl39_27
| spl39_28
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(forward_demodulation,[],[f3593,f549]) ).
tff(f3605,definition,
( spl39_257
<=> ( sK9 = sK15 ) ),
introduced(definition,[new_symbols(definition,[spl39_257])],[avatar_definition]) ).
tff(f3609,definition,
( spl39_258
<=> ( sK8 = sK15 ) ),
introduced(definition,[new_symbols(definition,[spl39_258])],[avatar_definition]) ).
tff(f3613,definition,
( spl39_259
<=> ! [X0: ty,X1: uni] : $less(0,occ1(X0,get(X0,int,X1,sF30),X1,sK6,0)) ),
introduced(definition,[new_symbols(definition,[spl39_259])],[avatar_definition]) ).
tff(f3614,plain,
( ! [X0: ty,X1: uni] : $less(0,occ1(X0,get(X0,int,X1,sF30),X1,sK6,0))
| ~ spl39_259 ),
inference(avatar_component_clause,[],[f3613]) ).
tff(f3615,plain,
( spl39_233
| spl39_257
| spl39_258
| ~ spl39_232
| spl39_259
| ~ spl39_12
| ~ spl39_27
| spl39_28
| ~ spl39_64
| ~ spl39_66
| ~ spl39_102 ),
inference(avatar_split_clause,[],[f3603,f1175,f812,f789,f552,f547,f472,f3613,f3438,f3609,f3605,f3442]) ).
tff(f16394,plain,
( $less(0,0)
| $less(sK6,0)
| ~ spl39_259 ),
inference(superposition,[],[f3614,f274]) ).
tff(f16396,plain,
( $less(sK6,0)
| ~ spl39_259 ),
inference(evaluation,[],[f16394]) ).
tff(f16399,plain,
( $false
| spl39_39
| ~ spl39_259 ),
inference(forward_subsumption_resolution,[],[f16396,f609]) ).
tff(f16400,plain,
( spl39_39
| ~ spl39_259 ),
inference(avatar_contradiction_clause,[],[f16399]) ).
tff(f16411,plain,
$false,
inference(avatar_smt_refutation,[],[f16400,f3615,f3110,f1220,f1178,f989,f953,f820,f815,f798,f792,f777,f755,f700,f658,f630,f610,f605,f600,f590,f580,f555,f550,f545,f540,f520,f515,f510,f500,f490,f485,f480,f475,f460,f455,f430,f425,f420]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW636_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 % Computer : n008.cluster.edu
% 0.09/0.24 % Model : x86_64 x86_64
% 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.24 % Memory : 8046.5625MB
% 0.09/0.24 % OS : Linux 6.8.0-71-generic
% 0.09/0.24 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Mon Sep 28 14:23:54 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.30 Running first-order theorem proving
% 0.24/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.89/1.90 % (2285330)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.89/1.90 % (2285337)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2731836777:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.89/1.90 % (2285341)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=653954802:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.89/1.90 % (2285341)Instruction limit reached!
% 5.89/1.90 % (2285341)------------------------------
% 5.89/1.90 % (2285341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.90 % (2285341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.90 % (2285341)CaDiCaL version: 2.1.3
% 5.89/1.90 % (2285341)Termination reason: Instruction limit
% 5.89/1.90 % (2285341)Termination phase: Saturation
% 5.89/1.90 % (2285341)Time elapsed: 0.045 s
% 5.89/1.90 % (2285341)Peak memory usage: 116 MB
% 5.89/1.90 % (2285341)Instructions burned: 33 (million)
% 5.89/1.90 % (2285335)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2282653524:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.89/1.90 % (2285336)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=342091203:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.89/1.90 % (2285337)Instruction limit reached!
% 5.89/1.90 % (2285337)------------------------------
% 5.89/1.90 % (2285337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.90 % (2285337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.90 % (2285337)CaDiCaL version: 2.1.3
% 5.89/1.90 % (2285337)Termination reason: Instruction limit
% 5.89/1.90 % (2285337)Termination phase: Saturation
% 5.89/1.90 % (2285337)Time elapsed: 0.097 s
% 5.89/1.90 % (2285337)Peak memory usage: 117 MB
% 5.89/1.90 % (2285337)Instructions burned: 201 (million)
% 5.89/1.90 % (2285339)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3957354734:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.89/1.90 % (2285338)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3447803445:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.89/1.90 % (2285339)Instruction limit reached!
% 5.89/1.90 % (2285339)------------------------------
% 5.89/1.90 % (2285339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.90 % (2285339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.90 % (2285339)CaDiCaL version: 2.1.3
% 5.89/1.90 % (2285339)Termination reason: Instruction limit
% 5.89/1.90 % (2285339)Termination phase: Preprocessing 3
% 5.89/1.90 % (2285339)Time elapsed: 0.005 s
% 5.89/1.90 % (2285339)Peak memory usage: 86 MB
% 5.89/1.90 % (2285339)Instructions burned: 5 (million)
% 5.89/1.90 % (2285338)Instruction limit reached!
% 5.89/1.90 % (2285338)------------------------------
% 5.89/1.90 % (2285338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.90 % (2285338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.90 % (2285338)CaDiCaL version: 2.1.3
% 5.89/1.90 % (2285338)Termination reason: Instruction limit
% 5.89/1.90 % (2285338)Termination phase: Function definition elimination
% 5.89/1.90 % (2285338)Time elapsed: 0.008 s
% 5.89/1.90 % (2285338)Peak memory usage: 86 MB
% 5.89/1.90 % (2285338)Instructions burned: 7 (million)
% 5.89/1.90 % (2285340)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2317346337:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.89/1.90 % (2285335)Instruction limit reached!
% 5.89/1.90 % (2285335)------------------------------
% 5.89/1.90 % (2285335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.90 % (2285335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.90 % (2285335)CaDiCaL version: 2.1.3
% 5.89/1.90 % (2285335)Termination reason: Instruction limit
% 5.89/1.90 % (2285335)Termination phase: Saturation
% 5.89/1.90 % (2285335)Time elapsed: 0.038 s
% 5.89/1.90 % (2285335)Peak memory usage: 110 MB
% 5.89/1.90 % (2285335)Instructions burned: 12 (million)
% 5.89/1.90 % (2285340)Instruction limit reached!
% 5.89/1.90 % (2285340)------------------------------
% 5.89/1.90 % (2285340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.90 % (2285340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (2285340)CaDiCaL version: 2.1.3
% 8.39/2.17 % (2285340)Termination reason: Instruction limit
% 8.39/2.17 % (2285340)Termination phase: Saturation
% 8.39/2.17 % (2285340)Time elapsed: 0.082 s
% 8.39/2.17 % (2285340)Peak memory usage: 116 MB
% 8.39/2.17 % (2285340)Instructions burned: 46 (million)
% 8.39/2.17 % (2285344)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=564578111:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 8.39/2.17 % (2285349)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=3072796110:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 8.39/2.17 % (2285344)Instruction limit reached!
% 8.39/2.17 % (2285344)------------------------------
% 8.39/2.17 % (2285344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (2285344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (2285344)CaDiCaL version: 2.1.3
% 8.39/2.17 % (2285344)Termination reason: Instruction limit
% 8.39/2.17 % (2285344)Termination phase: Saturation
% 8.39/2.17 % (2285344)Time elapsed: 0.017 s
% 8.39/2.17 % (2285344)Peak memory usage: 88 MB
% 8.39/2.17 % (2285344)Instructions burned: 14 (million)
% 8.39/2.17 % (2285351)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1630600285:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 8.39/2.17 % (2285349)Instruction limit reached!
% 8.39/2.17 % (2285349)------------------------------
% 8.39/2.17 % (2285349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (2285349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (2285349)CaDiCaL version: 2.1.3
% 8.39/2.17 % (2285349)Termination reason: Instruction limit
% 8.39/2.17 % (2285349)Termination phase: Saturation
% 8.39/2.17 % (2285349)Time elapsed: 0.017 s
% 8.39/2.17 % (2285349)Peak memory usage: 89 MB
% 8.39/2.17 % (2285349)Instructions burned: 29 (million)
% 8.39/2.17 % (2285351)Instruction limit reached!
% 8.39/2.17 % (2285351)------------------------------
% 8.39/2.17 % (2285351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (2285351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (2285351)CaDiCaL version: 2.1.3
% 8.39/2.17 % (2285351)Termination reason: Instruction limit
% 8.39/2.17 % (2285351)Termination phase: Saturation
% 8.39/2.17 % (2285351)Time elapsed: 0.017 s
% 8.39/2.17 % (2285351)Peak memory usage: 89 MB
% 8.39/2.17 % (2285351)Instructions burned: 17 (million)
% 8.39/2.17 % (2285352)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2793394303:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 8.39/2.17 % (2285353)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=2519674404:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 8.39/2.17 % (2285352)Instruction limit reached!
% 8.39/2.17 % (2285352)------------------------------
% 8.39/2.17 % (2285352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (2285352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (2285352)CaDiCaL version: 2.1.3
% 8.39/2.17 % (2285352)Termination reason: Instruction limit
% 8.39/2.17 % (2285352)Termination phase: Saturation
% 8.39/2.17 % (2285352)Time elapsed: 0.028 s
% 8.39/2.17 % (2285352)Peak memory usage: 89 MB
% 8.39/2.17 % (2285352)Instructions burned: 24 (million)
% 8.39/2.17 % (2285336)Instruction limit reached!
% 8.39/2.17 % (2285336)------------------------------
% 8.39/2.17 % (2285336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (2285336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (2285336)CaDiCaL version: 2.1.3
% 8.39/2.17 % (2285336)Termination reason: Instruction limit
% 8.39/2.17 % (2285336)Termination phase: Saturation
% 8.39/2.17 % (2285336)Time elapsed: 0.339 s
% 8.39/2.17 % (2285336)Peak memory usage: 117 MB
% 8.39/2.17 % (2285336)Instructions burned: 307 (million)
% 8.39/2.17 % (2285354)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3970559629:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 8.39/2.17 % (2285353)Instruction limit reached!
% 8.39/2.17 % (2285353)------------------------------
% 9.30/2.48 % (2285353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.48 % (2285353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.48 % (2285353)CaDiCaL version: 2.1.3
% 9.30/2.48 % (2285353)Termination reason: Instruction limit
% 9.30/2.48 % (2285353)Termination phase: Saturation
% 9.30/2.48 % (2285353)Time elapsed: 0.031 s
% 9.30/2.48 % (2285353)Peak memory usage: 89 MB
% 9.30/2.48 % (2285353)Instructions burned: 29 (million)
% 9.30/2.48 % (2285359)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=598123002:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 9.30/2.48 % (2285354)Instruction limit reached!
% 9.30/2.48 % (2285354)------------------------------
% 9.30/2.48 % (2285354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.48 % (2285354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.48 % (2285354)CaDiCaL version: 2.1.3
% 9.30/2.48 % (2285354)Termination reason: Instruction limit
% 9.30/2.48 % (2285354)Termination phase: Saturation
% 9.30/2.48 % (2285354)Time elapsed: 0.079 s
% 9.30/2.48 % (2285354)Peak memory usage: 89 MB
% 9.30/2.48 % (2285354)Instructions burned: 85 (million)
% 9.30/2.48 % (2285358)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=54406266:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.30/2.48 % (2285358)Instruction limit reached!
% 9.30/2.48 % (2285358)------------------------------
% 9.30/2.48 % (2285358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.48 % (2285358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.48 % (2285358)CaDiCaL version: 2.1.3
% 9.30/2.48 % (2285358)Termination reason: Instruction limit
% 9.30/2.48 % (2285358)Termination phase: Preprocessing 1
% 9.30/2.48 % (2285358)Time elapsed: 0.003 s
% 9.30/2.48 % (2285358)Peak memory usage: 85 MB
% 9.30/2.48 % (2285358)Instructions burned: 3 (million)
% 9.30/2.48 % (2285360)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3683552831:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 9.30/2.48 % (2285360)Instruction limit reached!
% 9.30/2.48 % (2285360)------------------------------
% 9.30/2.48 % (2285360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.48 % (2285360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.48 % (2285360)CaDiCaL version: 2.1.3
% 9.30/2.48 % (2285360)Termination reason: Instruction limit
% 9.30/2.48 % (2285360)Termination phase: Preprocessing 3
% 9.30/2.48 % (2285360)Time elapsed: 0.005 s
% 9.30/2.48 % (2285360)Peak memory usage: 86 MB
% 9.30/2.48 % (2285360)Instructions burned: 4 (million)
% 9.30/2.48 % (2285359)Instruction limit reached!
% 9.30/2.48 % (2285359)------------------------------
% 9.30/2.48 % (2285359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.48 % (2285359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.48 % (2285359)CaDiCaL version: 2.1.3
% 9.30/2.48 % (2285359)Termination reason: Instruction limit
% 9.30/2.48 % (2285359)Termination phase: Saturation
% 9.30/2.48 % (2285359)Time elapsed: 0.090 s
% 9.30/2.48 % (2285359)Peak memory usage: 90 MB
% 9.30/2.48 % (2285359)Instructions burned: 182 (million)
% 9.30/2.48 % (2285363)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3658685041:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.30/2.48 % (2285366)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=1894297617:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.30/2.48 % (2285366)Instruction limit reached!
% 9.30/2.48 % (2285366)------------------------------
% 9.30/2.48 % (2285366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.48 % (2285366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.48 % (2285366)CaDiCaL version: 2.1.3
% 9.30/2.48 % (2285366)Termination reason: Instruction limit
% 9.30/2.48 % (2285366)Termination phase: Property scanning
% 9.30/2.48 % (2285366)Time elapsed: 0.009 s
% 9.30/2.48 % (2285366)Peak memory usage: 86 MB
% 9.30/2.48 % (2285366)Instructions burned: 9 (million)
% 9.30/2.48 % (2285365)lrs+10_1_thi=all:si=on:fd=off:random_seed=3435666088:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 11.66/2.82 % (2285370)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=545065937:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.66/2.82 % (2285370)Instruction limit reached!
% 11.66/2.82 % (2285370)------------------------------
% 11.66/2.82 % (2285370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.82 % (2285370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.82 % (2285370)CaDiCaL version: 2.1.3
% 11.66/2.82 % (2285370)Termination reason: Instruction limit
% 11.66/2.82 % (2285370)Termination phase: Property scanning
% 11.66/2.82 % (2285370)Time elapsed: 0.002 s
% 11.66/2.82 % (2285370)Peak memory usage: 86 MB
% 11.66/2.82 % (2285370)Instructions burned: 2 (million)
% 11.66/2.82 % (2285368)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=612190991:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 11.66/2.82 % (2285368)Instruction limit reached!
% 11.66/2.82 % (2285368)------------------------------
% 11.66/2.82 % (2285368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.82 % (2285368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.82 % (2285368)CaDiCaL version: 2.1.3
% 11.66/2.82 % (2285368)Termination reason: Instruction limit
% 11.66/2.82 % (2285368)Termination phase: Unused predicate definition removal
% 11.66/2.82 % (2285368)Time elapsed: 0.003 s
% 11.66/2.82 % (2285368)Peak memory usage: 86 MB
% 11.66/2.82 % (2285368)Instructions burned: 2 (million)
% 11.66/2.82 % (2285363)Instruction limit reached!
% 11.66/2.82 % (2285363)------------------------------
% 11.66/2.82 % (2285363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.82 % (2285363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.82 % (2285363)CaDiCaL version: 2.1.3
% 11.66/2.82 % (2285363)Termination reason: Instruction limit
% 11.66/2.82 % (2285363)Termination phase: Saturation
% 11.66/2.82 % (2285363)Time elapsed: 0.118 s
% 11.66/2.82 % (2285363)Peak memory usage: 134 MB
% 11.66/2.82 % (2285363)Instructions burned: 66 (million)
% 11.66/2.82 % (2285373)dis+10_1_si=on:random_seed=3471431187:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 11.66/2.82 % (2285365)Instruction limit reached!
% 11.66/2.82 % (2285365)------------------------------
% 11.66/2.82 % (2285365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.82 % (2285365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.82 % (2285365)CaDiCaL version: 2.1.3
% 11.66/2.82 % (2285365)Termination reason: Instruction limit
% 11.66/2.82 % (2285365)Termination phase: Saturation
% 11.66/2.82 % (2285365)Time elapsed: 0.094 s
% 11.66/2.82 % (2285365)Peak memory usage: 116 MB
% 11.66/2.82 % (2285365)Instructions burned: 53 (million)
% 11.66/2.82 % (2285373)Instruction limit reached!
% 11.66/2.82 % (2285373)------------------------------
% 11.66/2.82 % (2285373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.82 % (2285373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.82 % (2285373)CaDiCaL version: 2.1.3
% 11.66/2.82 % (2285373)Termination reason: Instruction limit
% 11.66/2.82 % (2285373)Termination phase: Saturation
% 11.66/2.82 % (2285373)Time elapsed: 0.008 s
% 11.66/2.82 % (2285373)Peak memory usage: 88 MB
% 11.66/2.82 % (2285373)Instructions burned: 15 (million)
% 11.66/2.82 % (2285372)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=680253529:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.66/2.82 % (2285376)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=393385094:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.66/2.82 % (2285376)Refutation not found, incomplete strategy
% 11.66/2.82 % (2285376)------------------------------
% 11.66/2.82 % (2285376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.82 % (2285376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.82 % (2285376)CaDiCaL version: 2.1.3
% 11.66/2.82 % (2285376)Termination reason: Refutation not found, incomplete strategy
% 11.66/2.82 % (2285376)Time elapsed: 0.017 s
% 11.66/2.82 % (2285376)Peak memory usage: 89 MB
% 11.66/2.82 % (2285376)Instructions burned: 16 (million)
% 11.66/2.82 % (2285379)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1163471752:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi)
% 15.78/3.23 % (2285384)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1242595816:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 15.78/3.23 % (2285381)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2659601515:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 15.78/3.23 % (2285381)Instruction limit reached!
% 15.78/3.23 % (2285381)------------------------------
% 15.78/3.23 % (2285381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.23 % (2285381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.23 % (2285381)CaDiCaL version: 2.1.3
% 15.78/3.23 % (2285381)Termination reason: Instruction limit
% 15.78/3.23 % (2285381)Termination phase: Preprocessing 3
% 15.78/3.23 % (2285381)Time elapsed: 0.005 s
% 15.78/3.23 % (2285381)Peak memory usage: 86 MB
% 15.78/3.23 % (2285381)Instructions burned: 4 (million)
% 15.78/3.23 % (2285379)Instruction limit reached!
% 15.78/3.23 % (2285379)------------------------------
% 15.78/3.23 % (2285379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.23 % (2285379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.23 % (2285379)CaDiCaL version: 2.1.3
% 15.78/3.23 % (2285379)Termination reason: Instruction limit
% 15.78/3.23 % (2285379)Termination phase: Saturation
% 15.78/3.23 % (2285379)Time elapsed: 0.043 s
% 15.78/3.23 % (2285379)Peak memory usage: 89 MB
% 15.78/3.23 % (2285379)Instructions burned: 35 (million)
% 15.78/3.23 % (2285372)Instruction limit reached!
% 15.78/3.23 % (2285372)------------------------------
% 15.78/3.23 % (2285372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.23 % (2285372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.23 % (2285372)CaDiCaL version: 2.1.3
% 15.78/3.23 % (2285372)Termination reason: Instruction limit
% 15.78/3.23 % (2285372)Termination phase: Saturation
% 15.78/3.23 % (2285372)Time elapsed: 0.183 s
% 15.78/3.23 % (2285372)Peak memory usage: 117 MB
% 15.78/3.23 % (2285372)Instructions burned: 127 (million)
% 15.78/3.23 % (2285383)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3561664279:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 15.78/3.23 % (2285383)Instruction limit reached!
% 15.78/3.23 % (2285383)------------------------------
% 15.78/3.23 % (2285383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.23 % (2285383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.23 % (2285383)CaDiCaL version: 2.1.3
% 15.78/3.23 % (2285383)Termination reason: Instruction limit
% 15.78/3.23 % (2285383)Termination phase: Property scanning
% 15.78/3.23 % (2285383)Time elapsed: 0.009 s
% 15.78/3.23 % (2285383)Peak memory usage: 87 MB
% 15.78/3.23 % (2285383)Instructions burned: 8 (million)
% 15.78/3.23 % (2285385)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=816772693:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 15.78/3.23 % (2285385)Instruction limit reached!
% 15.78/3.23 % (2285385)------------------------------
% 15.78/3.23 % (2285385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.23 % (2285385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.23 % (2285385)CaDiCaL version: 2.1.3
% 15.78/3.23 % (2285385)Termination reason: Instruction limit
% 15.78/3.23 % (2285385)Termination phase: Saturation
% 15.78/3.23 % (2285385)Time elapsed: 0.031 s
% 15.78/3.23 % (2285385)Peak memory usage: 99 MB
% 15.78/3.23 % (2285385)Instructions burned: 13 (million)
% 15.78/3.23 % (2285384)Instruction limit reached!
% 15.78/3.23 % (2285384)------------------------------
% 15.78/3.23 % (2285384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.23 % (2285384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.23 % (2285384)CaDiCaL version: 2.1.3
% 15.78/3.23 % (2285384)Termination reason: Instruction limit
% 15.78/3.23 % (2285384)Termination phase: Saturation
% 15.78/3.23 % (2285384)Time elapsed: 0.220 s
% 15.78/3.23 % (2285384)Peak memory usage: 93 MB
% 15.78/3.23 % (2285384)Instructions burned: 371 (million)
% 15.78/3.23 % (2285391)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2813375018:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 15.78/3.23 % (2285392)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3265566586:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 17.67/3.57 % (2285392)Instruction limit reached!
% 17.67/3.57 % (2285392)------------------------------
% 17.67/3.57 % (2285392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.67/3.57 % (2285392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/3.57 % (2285392)CaDiCaL version: 2.1.3
% 17.67/3.57 % (2285392)Termination reason: Instruction limit
% 17.67/3.57 % (2285392)Termination phase: Saturation
% 17.67/3.57 % (2285392)Time elapsed: 0.011 s
% 17.67/3.57 % (2285392)Peak memory usage: 88 MB
% 17.67/3.57 % (2285392)Instructions burned: 10 (million)
% 17.67/3.57 % (2285395)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=3061604072:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 17.67/3.57 % (2285393)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=481507342:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 17.67/3.57 % (2285376)------------------------------
% 17.67/3.57 % (2285376)------------------------------
% 17.67/3.57 % (2285397)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=3070381207:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 17.67/3.57 % (2285398)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2951937343:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi)
% 17.67/3.57 % (2285395)Instruction limit reached!
% 17.67/3.57 % (2285395)------------------------------
% 17.67/3.57 % (2285395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.67/3.57 % (2285395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/3.57 % (2285395)CaDiCaL version: 2.1.3
% 17.67/3.57 % (2285395)Termination reason: Instruction limit
% 17.67/3.57 % (2285395)Termination phase: Saturation
% 17.67/3.57 % (2285395)Time elapsed: 0.082 s
% 17.67/3.57 % (2285395)Peak memory usage: 90 MB
% 17.67/3.57 % (2285395)Instructions burned: 75 (million)
% 17.67/3.57 % (2285391)Instruction limit reached!
% 17.67/3.57 % (2285391)------------------------------
% 17.67/3.57 % (2285391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.67/3.57 % (2285391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/3.57 % (2285391)CaDiCaL version: 2.1.3
% 17.67/3.57 % (2285391)Termination reason: Instruction limit
% 17.67/3.57 % (2285391)Termination phase: Saturation
% 17.67/3.57 % (2285391)Time elapsed: 0.150 s
% 17.67/3.57 % (2285391)Peak memory usage: 118 MB
% 17.67/3.57 % (2285391)Instructions burned: 227 (million)
% 17.67/3.57 % (2285393)Instruction limit reached!
% 17.67/3.57 % (2285393)------------------------------
% 17.67/3.57 % (2285393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.67/3.57 % (2285393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/3.57 % (2285393)CaDiCaL version: 2.1.3
% 17.67/3.57 % (2285393)Termination reason: Instruction limit
% 17.67/3.57 % (2285393)Termination phase: Saturation
% 17.67/3.57 % (2285393)Time elapsed: 0.123 s
% 17.67/3.57 % (2285393)Peak memory usage: 133 MB
% 17.67/3.57 % (2285393)Instructions burned: 71 (million)
% 17.67/3.57 % (2285398)Instruction limit reached!
% 17.67/3.57 % (2285398)------------------------------
% 17.67/3.57 % (2285398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.67/3.57 % (2285398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/3.57 % (2285398)CaDiCaL version: 2.1.3
% 17.67/3.57 % (2285398)Termination reason: Instruction limit
% 17.67/3.57 % (2285398)Termination phase: Saturation
% 17.67/3.57 % (2285398)Time elapsed: 0.163 s
% 17.67/3.57 % (2285398)Peak memory usage: 117 MB
% 17.67/3.57 % (2285398)Instructions burned: 130 (million)
% 17.67/3.57 % (2285401)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=141601952:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.67/3.57 % (2285404)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2125934108:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 17.67/3.57 % (2285408)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1844814105:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 22.05/4.15 % (2285407)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1610319242:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 22.05/4.15 % (2285397)Instruction limit reached!
% 22.05/4.15 % (2285397)------------------------------
% 22.05/4.15 % (2285397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.05/4.15 % (2285397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.05/4.15 % (2285397)CaDiCaL version: 2.1.3
% 22.05/4.15 % (2285397)Termination reason: Instruction limit
% 22.05/4.15 % (2285397)Termination phase: Saturation
% 22.05/4.15 % (2285397)Time elapsed: 0.316 s
% 22.05/4.15 % (2285397)Peak memory usage: 91 MB
% 22.05/4.15 % (2285397)Instructions burned: 294 (million)
% 22.05/4.15 % (2285409)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2136579711:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 22.05/4.15 % (2285404)Instruction limit reached!
% 22.05/4.15 % (2285404)------------------------------
% 22.05/4.15 % (2285404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.05/4.15 % (2285404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.05/4.15 % (2285404)CaDiCaL version: 2.1.3
% 22.05/4.15 % (2285404)Termination reason: Instruction limit
% 22.05/4.15 % (2285404)Termination phase: Saturation
% 22.05/4.15 % (2285404)Time elapsed: 0.098 s
% 22.05/4.15 % (2285404)Peak memory usage: 134 MB
% 22.05/4.15 % (2285404)Instructions burned: 40 (million)
% 22.05/4.15 % (2285410)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=4257117587:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 22.05/4.15 % (2285401)Instruction limit reached!
% 22.05/4.15 % (2285401)------------------------------
% 22.05/4.15 % (2285401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.05/4.15 % (2285401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.05/4.15 % (2285401)CaDiCaL version: 2.1.3
% 22.05/4.15 % (2285401)Termination reason: Instruction limit
% 22.05/4.15 % (2285401)Termination phase: Saturation
% 22.05/4.15 % (2285401)Time elapsed: 0.206 s
% 22.05/4.15 % (2285401)Peak memory usage: 134 MB
% 22.05/4.15 % (2285401)Instructions burned: 131 (million)
% 22.05/4.15 % (2285409)Instruction limit reached!
% 22.05/4.15 % (2285409)------------------------------
% 22.05/4.15 % (2285409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.05/4.15 % (2285409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.05/4.15 % (2285409)CaDiCaL version: 2.1.3
% 22.05/4.15 % (2285409)Termination reason: Instruction limit
% 22.05/4.15 % (2285409)Termination phase: Saturation
% 22.05/4.15 % (2285409)Time elapsed: 0.167 s
% 22.05/4.15 % (2285409)Peak memory usage: 117 MB
% 22.05/4.15 % (2285409)Instructions burned: 132 (million)
% 22.05/4.15 % (2285407)Instruction limit reached!
% 22.05/4.15 % (2285407)------------------------------
% 22.05/4.15 % (2285407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.05/4.15 % (2285407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.05/4.15 % (2285407)CaDiCaL version: 2.1.3
% 22.05/4.15 % (2285407)Termination reason: Instruction limit
% 22.05/4.15 % (2285407)Termination phase: Saturation
% 22.05/4.15 % (2285407)Time elapsed: 0.306 s
% 22.05/4.15 % (2285407)Peak memory usage: 92 MB
% 22.05/4.15 % (2285407)Instructions burned: 307 (million)
% 22.05/4.15 % (2285408)Instruction limit reached!
% 22.05/4.15 % (2285408)------------------------------
% 22.05/4.15 % (2285408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.05/4.15 % (2285408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.05/4.15 % (2285408)CaDiCaL version: 2.1.3
% 22.05/4.15 % (2285408)Termination reason: Instruction limit
% 22.05/4.15 % (2285408)Termination phase: Saturation
% 22.05/4.15 % (2285408)Time elapsed: 0.330 s
% 22.05/4.15 % (2285408)Peak memory usage: 139 MB
% 22.05/4.15 % (2285408)Instructions burned: 599 (million)
% 22.05/4.15 % (2285415)dis+10_1_si=on:random_seed=3580688529:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi)
% 22.05/4.15 % (2285417)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3306292098:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 22.05/4.15 % (2285410)Instruction limit reached!
% 22.05/4.15 % (2285410)------------------------------
% 23.99/4.62 % (2285410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.99/4.62 % (2285410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/4.62 % (2285410)CaDiCaL version: 2.1.3
% 23.99/4.62 % (2285410)Termination reason: Instruction limit
% 23.99/4.62 % (2285410)Termination phase: Saturation
% 23.99/4.62 % (2285410)Time elapsed: 0.300 s
% 23.99/4.62 % (2285410)Peak memory usage: 117 MB
% 23.99/4.62 % (2285410)Instructions burned: 259 (million)
% 23.99/4.62 % (2285419)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1470163365:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 23.99/4.62 % (2285420)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2834383240:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi)
% 23.99/4.62 % (2285423)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=3438925076:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 23.99/4.62 % (2285421)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2905745017:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 23.99/4.62 % (2285419)Instruction limit reached!
% 23.99/4.62 % (2285419)------------------------------
% 23.99/4.62 % (2285419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.99/4.62 % (2285419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/4.62 % (2285419)CaDiCaL version: 2.1.3
% 23.99/4.62 % (2285419)Termination reason: Instruction limit
% 23.99/4.62 % (2285419)Termination phase: Saturation
% 23.99/4.62 % (2285419)Time elapsed: 0.159 s
% 23.99/4.62 % (2285419)Peak memory usage: 90 MB
% 23.99/4.62 % (2285419)Instructions burned: 141 (million)
% 23.99/4.62 % (2285420)Instruction limit reached!
% 23.99/4.62 % (2285420)------------------------------
% 23.99/4.62 % (2285420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.99/4.62 % (2285420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/4.62 % (2285420)CaDiCaL version: 2.1.3
% 23.99/4.62 % (2285420)Termination reason: Instruction limit
% 23.99/4.62 % (2285420)Termination phase: Saturation
% 23.99/4.62 % (2285420)Time elapsed: 0.099 s
% 23.99/4.62 % (2285420)Peak memory usage: 116 MB
% 23.99/4.62 % (2285420)Instructions burned: 65 (million)
% 23.99/4.62 % (2285423)Instruction limit reached!
% 23.99/4.62 % (2285423)------------------------------
% 23.99/4.62 % (2285423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.99/4.62 % (2285423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/4.62 % (2285423)CaDiCaL version: 2.1.3
% 23.99/4.62 % (2285423)Termination reason: Instruction limit
% 23.99/4.62 % (2285423)Termination phase: Saturation
% 23.99/4.62 % (2285423)Time elapsed: 0.084 s
% 23.99/4.62 % (2285423)Peak memory usage: 117 MB
% 23.99/4.62 % (2285423)Instructions burned: 128 (million)
% 23.99/4.62 % (2285421)Instruction limit reached!
% 23.99/4.62 % (2285421)------------------------------
% 23.99/4.62 % (2285421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.99/4.62 % (2285421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/4.62 % (2285421)CaDiCaL version: 2.1.3
% 23.99/4.62 % (2285421)Termination reason: Instruction limit
% 23.99/4.62 % (2285421)Termination phase: Saturation
% 23.99/4.62 % (2285421)Time elapsed: 0.118 s
% 23.99/4.62 % (2285421)Peak memory usage: 90 MB
% 23.99/4.62 % (2285421)Instructions burned: 122 (million)
% 23.99/4.62 % (2285425)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=3492128873:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi)
% 23.99/4.62 % (2285417)Instruction limit reached!
% 23.99/4.62 % (2285417)------------------------------
% 23.99/4.62 % (2285417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.99/4.62 % (2285417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/4.62 % (2285417)CaDiCaL version: 2.1.3
% 23.99/4.62 % (2285417)Termination reason: Instruction limit
% 23.99/4.62 % (2285417)Termination phase: Saturation
% 23.99/4.62 % (2285417)Time elapsed: 0.352 s
% 23.99/4.62 % (2285417)Peak memory usage: 92 MB
% 23.99/4.62 % (2285417)Instructions burned: 384 (million)
% 23.99/4.62 % (2285425)Instruction limit reached!
% 23.99/4.62 % (2285425)------------------------------
% 23.99/4.62 % (2285425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.18 % (2285425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.18 % (2285425)CaDiCaL version: 2.1.3
% 29.78/5.18 % (2285425)Termination reason: Instruction limit
% 29.78/5.18 % (2285425)Termination phase: Saturation
% 29.78/5.18 % (2285425)Time elapsed: 0.074 s
% 29.78/5.18 % (2285425)Peak memory usage: 117 MB
% 29.78/5.18 % (2285425)Instructions burned: 39 (million)
% 29.78/5.18 % (2285430)dis+1010_1_to=kbo:si=on:random_seed=3571443767:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi)
% 29.78/5.18 % (2285433)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1719668377:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 29.78/5.18 % (2285432)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4190083361:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 29.78/5.18 % (2285431)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4230785577:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 29.78/5.18 % (2285430)Instruction limit reached!
% 29.78/5.18 % (2285430)------------------------------
% 29.78/5.18 % (2285430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.18 % (2285430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.18 % (2285430)CaDiCaL version: 2.1.3
% 29.78/5.18 % (2285430)Termination reason: Instruction limit
% 29.78/5.18 % (2285430)Termination phase: Saturation
% 29.78/5.18 % (2285430)Time elapsed: 0.202 s
% 29.78/5.18 % (2285430)Peak memory usage: 91 MB
% 29.78/5.18 % (2285430)Instructions burned: 175 (million)
% 29.78/5.18 % (2285433)Instruction limit reached!
% 29.78/5.18 % (2285433)------------------------------
% 29.78/5.18 % (2285433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.18 % (2285433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.18 % (2285433)CaDiCaL version: 2.1.3
% 29.78/5.18 % (2285433)Termination reason: Instruction limit
% 29.78/5.18 % (2285433)Termination phase: Saturation
% 29.78/5.18 % (2285433)Time elapsed: 0.135 s
% 29.78/5.18 % (2285433)Peak memory usage: 135 MB
% 29.78/5.18 % (2285433)Instructions burned: 215 (million)
% 29.78/5.18 % (2285435)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3606818706:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 29.78/5.18 % (2285436)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1024832871:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi)
% 29.78/5.18 % (2285431)Instruction limit reached!
% 29.78/5.18 % (2285431)------------------------------
% 29.78/5.18 % (2285431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.18 % (2285431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.18 % (2285431)CaDiCaL version: 2.1.3
% 29.78/5.18 % (2285431)Termination reason: Instruction limit
% 29.78/5.18 % (2285431)Termination phase: Saturation
% 29.78/5.18 % (2285431)Time elapsed: 0.258 s
% 29.78/5.18 % (2285431)Peak memory usage: 116 MB
% 29.78/5.18 % (2285431)Instructions burned: 330 (million)
% 29.78/5.18 % (2285443)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=4174975334:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi)
% 29.78/5.18 % (2285441)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=276040637:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi)
% 29.78/5.18 % (2285415)Instruction limit reached!
% 29.78/5.18 % (2285415)------------------------------
% 29.78/5.18 % (2285415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.18 % (2285415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.18 % (2285415)CaDiCaL version: 2.1.3
% 29.78/5.18 % (2285415)Termination reason: Instruction limit
% 29.78/5.18 % (2285415)Termination phase: Saturation
% 29.78/5.18 % (2285415)Time elapsed: 0.965 s
% 29.78/5.18 % (2285415)Peak memory usage: 95 MB
% 29.78/5.18 % (2285415)Instructions burned: 1000 (million)
% 29.78/5.18 % (2285436)Instruction limit reached!
% 29.78/5.18 % (2285436)------------------------------
% 29.78/5.18 % (2285436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.18 % (2285436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.52 % (2285436)CaDiCaL version: 2.1.3
% 31.63/5.52 % (2285436)Termination reason: Instruction limit
% 31.63/5.52 % (2285436)Termination phase: Saturation
% 31.63/5.52 % (2285436)Time elapsed: 0.287 s
% 31.63/5.52 % (2285436)Peak memory usage: 91 MB
% 31.63/5.52 % (2285436)Instructions burned: 296 (million)
% 31.63/5.52 % (2285435)Instruction limit reached!
% 31.63/5.52 % (2285435)------------------------------
% 31.63/5.52 % (2285435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.52 % (2285435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.52 % (2285435)CaDiCaL version: 2.1.3
% 31.63/5.52 % (2285435)Termination reason: Instruction limit
% 31.63/5.52 % (2285435)Termination phase: Saturation
% 31.63/5.52 % (2285435)Time elapsed: 0.336 s
% 31.63/5.52 % (2285435)Peak memory usage: 117 MB
% 31.63/5.52 % (2285435)Instructions burned: 349 (million)
% 31.63/5.52 % (2285443)Instruction limit reached!
% 31.63/5.52 % (2285443)------------------------------
% 31.63/5.52 % (2285443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.52 % (2285443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.52 % (2285443)CaDiCaL version: 2.1.3
% 31.63/5.52 % (2285443)Termination reason: Instruction limit
% 31.63/5.52 % (2285443)Termination phase: Saturation
% 31.63/5.52 % (2285443)Time elapsed: 0.167 s
% 31.63/5.52 % (2285443)Peak memory usage: 118 MB
% 31.63/5.52 % (2285443)Instructions burned: 281 (million)
% 31.63/5.52 % (2285445)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3667230576:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi)
% 31.63/5.52 % (2285432)Instruction limit reached!
% 31.63/5.52 % (2285432)------------------------------
% 31.63/5.52 % (2285432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.52 % (2285432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.52 % (2285432)CaDiCaL version: 2.1.3
% 31.63/5.52 % (2285432)Termination reason: Instruction limit
% 31.63/5.52 % (2285432)Termination phase: Saturation
% 31.63/5.52 % (2285432)Time elapsed: 0.550 s
% 31.63/5.52 % (2285432)Peak memory usage: 135 MB
% 31.63/5.52 % (2285432)Instructions burned: 483 (million)
% 31.63/5.52 % (2285448)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4000293739:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi)
% 31.63/5.52 % (2285451)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=2442791350:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi)
% 31.63/5.52 % (2285450)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1813235165:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 31.63/5.52 % (2285449)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=36187810:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi)
% 31.63/5.52 % (2285441)Instruction limit reached!
% 31.63/5.52 % (2285441)------------------------------
% 31.63/5.52 % (2285441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.52 % (2285441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.52 % (2285441)CaDiCaL version: 2.1.3
% 31.63/5.52 % (2285441)Termination reason: Instruction limit
% 31.63/5.52 % (2285441)Termination phase: Saturation
% 31.63/5.52 % (2285441)Time elapsed: 0.383 s
% 31.63/5.52 % (2285441)Peak memory usage: 118 MB
% 31.63/5.52 % (2285441)Instructions burned: 328 (million)
% 31.63/5.52 % (2285453)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1875256209:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 31.63/5.52 % (2285451)Instruction limit reached!
% 31.63/5.52 % (2285451)------------------------------
% 31.63/5.52 % (2285451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.52 % (2285451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.52 % (2285451)CaDiCaL version: 2.1.3
% 31.63/5.52 % (2285451)Termination reason: Instruction limit
% 31.63/5.52 % (2285451)Termination phase: Saturation
% 31.63/5.52 % (2285451)Time elapsed: 0.183 s
% 31.63/5.52 % (2285451)Peak memory usage: 134 MB
% 31.63/5.52 % (2285451)Instructions burned: 277 (million)
% 31.63/5.52 % (2285448)Instruction limit reached!
% 31.63/5.52 % (2285448)------------------------------
% 37.14/6.28 % (2285448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.14/6.28 % (2285448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/6.28 % (2285448)CaDiCaL version: 2.1.3
% 37.14/6.28 % (2285448)Termination reason: Instruction limit
% 37.14/6.28 % (2285448)Termination phase: Saturation
% 37.14/6.28 % (2285448)Time elapsed: 0.293 s
% 37.14/6.28 % (2285448)Peak memory usage: 114 MB
% 37.14/6.28 % (2285448)Instructions burned: 321 (million)
% 37.14/6.28 % (2285458)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=339444054:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi)
% 37.14/6.28 % (2285445)Instruction limit reached!
% 37.14/6.28 % (2285445)------------------------------
% 37.14/6.28 % (2285445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.14/6.28 % (2285445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/6.28 % (2285445)CaDiCaL version: 2.1.3
% 37.14/6.28 % (2285445)Termination reason: Instruction limit
% 37.14/6.28 % (2285445)Termination phase: Saturation
% 37.14/6.28 % (2285445)Time elapsed: 0.500 s
% 37.14/6.28 % (2285445)Peak memory usage: 96 MB
% 37.14/6.28 % (2285445)Instructions burned: 484 (million)
% 37.14/6.28 % (2285460)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3176648699:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2964 on theBenchmark for (2964ds/513Mi)
% 37.14/6.28 % (2285461)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=943041984:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi)
% 37.14/6.28 % (2285453)Instruction limit reached!
% 37.14/6.28 % (2285453)------------------------------
% 37.14/6.28 % (2285453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.14/6.28 % (2285453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/6.28 % (2285453)CaDiCaL version: 2.1.3
% 37.14/6.28 % (2285453)Termination reason: Instruction limit
% 37.14/6.28 % (2285453)Termination phase: Saturation
% 37.14/6.28 % (2285453)Time elapsed: 0.392 s
% 37.14/6.28 % (2285453)Peak memory usage: 119 MB
% 37.14/6.28 % (2285453)Instructions burned: 375 (million)
% 37.14/6.28 % (2285450)Instruction limit reached!
% 37.14/6.28 % (2285450)------------------------------
% 37.14/6.28 % (2285450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.14/6.28 % (2285450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/6.28 % (2285450)CaDiCaL version: 2.1.3
% 37.14/6.28 % (2285450)Termination reason: Instruction limit
% 37.14/6.28 % (2285450)Termination phase: Saturation
% 37.14/6.28 % (2285450)Time elapsed: 0.494 s
% 37.14/6.28 % (2285450)Peak memory usage: 119 MB
% 37.14/6.28 % (2285450)Instructions burned: 471 (million)
% 37.14/6.28 % (2285449)Instruction limit reached!
% 37.14/6.28 % (2285449)------------------------------
% 37.14/6.28 % (2285449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.14/6.28 % (2285449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/6.28 % (2285449)CaDiCaL version: 2.1.3
% 37.14/6.28 % (2285449)Termination reason: Instruction limit
% 37.14/6.28 % (2285449)Termination phase: Saturation
% 37.14/6.28 % (2285449)Time elapsed: 0.495 s
% 37.14/6.28 % (2285449)Peak memory usage: 119 MB
% 37.14/6.28 % (2285449)Instructions burned: 416 (million)
% 37.14/6.28 % (2285465)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3152305074:i=359:rtra=on:gtg=exists_top:ss=axioms_2963 on theBenchmark for (2963ds/359Mi)
% 37.14/6.28 % (2285460)Instruction limit reached!
% 37.14/6.28 % (2285460)------------------------------
% 37.14/6.28 % (2285460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.14/6.28 % (2285460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/6.28 % (2285460)CaDiCaL version: 2.1.3
% 37.14/6.28 % (2285460)Termination reason: Instruction limit
% 37.14/6.28 % (2285460)Termination phase: Saturation
% 37.14/6.28 % (2285460)Time elapsed: 0.293 s
% 37.14/6.28 % (2285460)Peak memory usage: 93 MB
% 37.14/6.28 % (2285460)Instructions burned: 514 (million)
% 37.14/6.28 % (2285468)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3431234833:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2961 on theBenchmark for (2961ds/341Mi)
% 37.14/6.28 % (2285458)Instruction limit reached!
% 37.14/6.28 % (2285458)------------------------------
% 37.14/6.28 % (2285458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.25/7.10 % (2285458)CaDiCaL version: 2.1.3
% 43.25/7.10 % (2285458)Termination reason: Instruction limit
% 43.25/7.10 % (2285458)Termination phase: Saturation
% 43.25/7.10 % (2285458)Time elapsed: 0.467 s
% 43.25/7.10 % (2285458)Peak memory usage: 119 MB
% 43.25/7.10 % (2285458)Instructions burned: 387 (million)
% 43.25/7.10 % (2285469)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=219978709:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/261Mi)
% 43.25/7.10 % (2285470)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=747039092:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi)
% 43.25/7.10 % (2285461)Instruction limit reached!
% 43.25/7.10 % (2285461)------------------------------
% 43.25/7.10 % (2285461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.25/7.10 % (2285461)CaDiCaL version: 2.1.3
% 43.25/7.10 % (2285461)Termination reason: Instruction limit
% 43.25/7.10 % (2285461)Termination phase: Saturation
% 43.25/7.10 % (2285461)Time elapsed: 0.443 s
% 43.25/7.10 % (2285461)Peak memory usage: 135 MB
% 43.25/7.10 % (2285461)Instructions burned: 334 (million)
% 43.25/7.10 % (2285472)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2965154985:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi)
% 43.25/7.10 % (2285465)Instruction limit reached!
% 43.25/7.10 % (2285465)------------------------------
% 43.25/7.10 % (2285465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.25/7.10 % (2285465)CaDiCaL version: 2.1.3
% 43.25/7.10 % (2285465)Termination reason: Instruction limit
% 43.25/7.10 % (2285465)Termination phase: Saturation
% 43.25/7.10 % (2285465)Time elapsed: 0.360 s
% 43.25/7.10 % (2285465)Peak memory usage: 91 MB
% 43.25/7.10 % (2285465)Instructions burned: 359 (million)
% 43.25/7.10 % (2285476)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1478828994:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi)
% 43.25/7.10 % (2285470)Instruction limit reached!
% 43.25/7.10 % (2285470)------------------------------
% 43.25/7.10 % (2285470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.25/7.10 % (2285470)CaDiCaL version: 2.1.3
% 43.25/7.10 % (2285470)Termination reason: Instruction limit
% 43.25/7.10 % (2285470)Termination phase: Saturation
% 43.25/7.10 % (2285470)Time elapsed: 0.292 s
% 43.25/7.10 % (2285470)Peak memory usage: 117 MB
% 43.25/7.10 % (2285470)Instructions burned: 236 (million)
% 43.25/7.10 % (2285469)Instruction limit reached!
% 43.25/7.10 % (2285469)------------------------------
% 43.25/7.10 % (2285469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.25/7.10 % (2285469)CaDiCaL version: 2.1.3
% 43.25/7.10 % (2285469)Termination reason: Instruction limit
% 43.25/7.10 % (2285469)Termination phase: Saturation
% 43.25/7.10 % (2285469)Time elapsed: 0.299 s
% 43.25/7.10 % (2285469)Peak memory usage: 118 MB
% 43.25/7.10 % (2285469)Instructions burned: 261 (million)
% 43.25/7.10 % (2285472)Instruction limit reached!
% 43.25/7.10 % (2285472)------------------------------
% 43.25/7.10 % (2285472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.25/7.10 % (2285472)CaDiCaL version: 2.1.3
% 43.25/7.10 % (2285472)Termination reason: Instruction limit
% 43.25/7.10 % (2285472)Termination phase: Saturation
% 43.25/7.10 % (2285472)Time elapsed: 0.173 s
% 43.25/7.10 % (2285472)Peak memory usage: 92 MB
% 43.25/7.10 % (2285472)Instructions burned: 274 (million)
% 43.25/7.10 % (2285468)Instruction limit reached!
% 43.25/7.10 % (2285468)------------------------------
% 43.25/7.10 % (2285468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.25/7.10 % (2285468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.94/7.85 % (2285468)CaDiCaL version: 2.1.3
% 45.94/7.85 % (2285468)Termination reason: Instruction limit
% 45.94/7.85 % (2285468)Termination phase: Saturation
% 45.94/7.85 % (2285468)Time elapsed: 0.355 s
% 45.94/7.85 % (2285468)Peak memory usage: 119 MB
% 45.94/7.85 % (2285468)Instructions burned: 341 (million)
% 45.94/7.85 % (2285478)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2779171289:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi)
% 45.94/7.85 % (2285479)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=4294559118:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi)
% 45.94/7.85 % (2285476)Instruction limit reached!
% 45.94/7.85 % (2285476)------------------------------
% 45.94/7.85 % (2285476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.94/7.85 % (2285476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.94/7.85 % (2285476)CaDiCaL version: 2.1.3
% 45.94/7.85 % (2285476)Termination reason: Instruction limit
% 45.94/7.85 % (2285476)Termination phase: Saturation
% 45.94/7.85 % (2285476)Time elapsed: 0.164 s
% 45.94/7.85 % (2285476)Peak memory usage: 91 MB
% 45.94/7.85 % (2285476)Instructions burned: 146 (million)
% 45.94/7.85 % (2285483)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3315791888:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi)
% 45.94/7.85 % (2285484)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1953069456:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi)
% 45.94/7.85 % (2285482)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2650782703:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/655Mi)
% 45.94/7.85 % (2285481)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1822451521:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi)
% 45.94/7.85 % (2285484)Instruction limit reached!
% 45.94/7.85 % (2285484)------------------------------
% 45.94/7.85 % (2285484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.94/7.85 % (2285484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.94/7.85 % (2285484)CaDiCaL version: 2.1.3
% 45.94/7.85 % (2285484)Termination reason: Instruction limit
% 45.94/7.85 % (2285484)Termination phase: Saturation
% 45.94/7.85 % (2285484)Time elapsed: 0.139 s
% 45.94/7.85 % (2285484)Peak memory usage: 117 MB
% 45.94/7.85 % (2285484)Instructions burned: 108 (million)
% 45.94/7.85 % (2285487)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2663031708:s2a=on:i=450:doe=on:nm=32:rtra=on_2953 on theBenchmark for (2953ds/450Mi)
% 45.94/7.85 % (2285479)Instruction limit reached!
% 45.94/7.85 % (2285479)------------------------------
% 45.94/7.85 % (2285479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.94/7.85 % (2285479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.94/7.85 % (2285479)CaDiCaL version: 2.1.3
% 45.94/7.85 % (2285479)Termination reason: Instruction limit
% 45.94/7.85 % (2285479)Termination phase: Saturation
% 45.94/7.85 % (2285479)Time elapsed: 0.354 s
% 45.94/7.85 % (2285479)Peak memory usage: 135 MB
% 45.94/7.85 % (2285479)Instructions burned: 276 (million)
% 45.94/7.85 % (2285492)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
% 45.94/7.85 % (2285492)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3487586434:i=1090:aac=none:nm=0:rtra=on:rawr=on_2951 on theBenchmark for (2951ds/1090Mi)
% 45.94/7.85 % (2285483)Instruction limit reached!
% 45.94/7.85 % (2285483)------------------------------
% 45.94/7.85 % (2285483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.94/7.85 % (2285483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.94/7.85 % (2285483)CaDiCaL version: 2.1.3
% 45.94/7.85 % (2285483)Termination reason: Instruction limit
% 45.94/7.85 % (2285483)Termination phase: Saturation
% 45.94/7.85 % (2285483)Time elapsed: 0.549 s
% 45.94/7.85 % (2285483)Peak memory usage: 98 MB
% 45.94/7.85 % (2285483)Instructions burned: 1056 (million)
% 45.94/7.85 % (2285494)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3950743611:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2950 on theBenchmark for (2950ds/130Mi)
% 53.07/8.64 % (2285487)Instruction limit reached!
% 53.07/8.64 % (2285487)------------------------------
% 53.07/8.64 % (2285487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/8.64 % (2285487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/8.64 % (2285487)CaDiCaL version: 2.1.3
% 53.07/8.64 % (2285487)Termination reason: Instruction limit
% 53.07/8.64 % (2285487)Termination phase: Saturation
% 53.07/8.64 % (2285487)Time elapsed: 0.484 s
% 53.07/8.64 % (2285487)Peak memory usage: 135 MB
% 53.07/8.64 % (2285487)Instructions burned: 450 (million)
% 53.07/8.64 % (2285496)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1425081550:i=312:kws=inv_frequency:nm=20:rtra=on_2947 on theBenchmark for (2947ds/312Mi)
% 53.07/8.64 % (2285494)Instruction limit reached!
% 53.07/8.64 % (2285494)------------------------------
% 53.07/8.64 % (2285494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/8.64 % (2285494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/8.64 % (2285494)CaDiCaL version: 2.1.3
% 53.07/8.64 % (2285494)Termination reason: Instruction limit
% 53.07/8.64 % (2285494)Termination phase: Saturation
% 53.07/8.64 % (2285494)Time elapsed: 0.166 s
% 53.07/8.64 % (2285494)Peak memory usage: 117 MB
% 53.07/8.64 % (2285494)Instructions burned: 130 (million)
% 53.07/8.64 % (2285482)Instruction limit reached!
% 53.07/8.64 % (2285482)------------------------------
% 53.07/8.64 % (2285482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/8.64 % (2285482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/8.64 % (2285482)CaDiCaL version: 2.1.3
% 53.07/8.64 % (2285482)Termination reason: Instruction limit
% 53.07/8.64 % (2285482)Termination phase: Saturation
% 53.07/8.64 % (2285482)Time elapsed: 0.747 s
% 53.07/8.64 % (2285482)Peak memory usage: 94 MB
% 53.07/8.64 % (2285482)Instructions burned: 655 (million)
% 53.07/8.64 % (2285496)Instruction limit reached!
% 53.07/8.64 % (2285496)------------------------------
% 53.07/8.64 % (2285496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/8.64 % (2285496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/8.64 % (2285496)CaDiCaL version: 2.1.3
% 53.07/8.64 % (2285496)Termination reason: Instruction limit
% 53.07/8.64 % (2285496)Termination phase: Saturation
% 53.07/8.64 % (2285496)Time elapsed: 0.196 s
% 53.07/8.64 % (2285496)Peak memory usage: 118 MB
% 53.07/8.64 % (2285496)Instructions burned: 313 (million)
% 53.07/8.64 % (2285505)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1851031218:i=491:doe=on:rtra=on:gtg=position_2946 on theBenchmark for (2946ds/491Mi)
% 53.07/8.64 % (2285506)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1237067256:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi)
% 53.07/8.64 % (2285507)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=695666879:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2945 on theBenchmark for (2945ds/307Mi)
% 53.07/8.64 % (2285481)Instruction limit reached!
% 53.07/8.64 % (2285481)------------------------------
% 53.07/8.64 % (2285481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/8.64 % (2285481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/8.64 % (2285481)CaDiCaL version: 2.1.3
% 53.07/8.64 % (2285481)Termination reason: Instruction limit
% 53.07/8.64 % (2285481)Termination phase: Saturation
% 53.07/8.64 % (2285481)Time elapsed: 1.030 s
% 53.07/8.64 % (2285481)Peak memory usage: 95 MB
% 53.07/8.64 % (2285481)Instructions burned: 1052 (million)
% 53.07/8.64 % (2285508)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3893315447:i=776:doe=on:rtra=on_2944 on theBenchmark for (2944ds/776Mi)
% 53.07/8.64 % (2285512)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2793131044:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2942 on theBenchmark for (2942ds/646Mi)
% 53.07/8.64 % (2285507)Instruction limit reached!
% 53.07/8.64 % (2285507)------------------------------
% 53.07/8.64 % (2285507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/8.64 % (2285507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/8.64 % (2285507)CaDiCaL version: 2.1.3
% 65.49/10.24 % (2285507)Termination reason: Instruction limit
% 65.49/10.24 % (2285507)Termination phase: Saturation
% 65.49/10.24 % (2285507)Time elapsed: 0.348 s
% 65.49/10.24 % (2285507)Peak memory usage: 93 MB
% 65.49/10.24 % (2285507)Instructions burned: 307 (million)
% 65.49/10.24 % (2285505)Instruction limit reached!
% 65.49/10.24 % (2285505)------------------------------
% 65.49/10.24 % (2285505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.49/10.24 % (2285505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.49/10.24 % (2285505)CaDiCaL version: 2.1.3
% 65.49/10.24 % (2285505)Termination reason: Instruction limit
% 65.49/10.24 % (2285505)Termination phase: Saturation
% 65.49/10.24 % (2285505)Time elapsed: 0.493 s
% 65.49/10.24 % (2285505)Peak memory usage: 93 MB
% 65.49/10.24 % (2285505)Instructions burned: 491 (million)
% 65.49/10.24 % (2285492)Instruction limit reached!
% 65.49/10.24 % (2285492)------------------------------
% 65.49/10.24 % (2285492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.49/10.24 % (2285492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.49/10.24 % (2285492)CaDiCaL version: 2.1.3
% 65.49/10.24 % (2285492)Termination reason: Instruction limit
% 65.49/10.24 % (2285492)Termination phase: Saturation
% 65.49/10.24 % (2285492)Time elapsed: 1.133 s
% 65.49/10.24 % (2285492)Peak memory usage: 122 MB
% 65.49/10.24 % (2285492)Instructions burned: 1090 (million)
% 65.49/10.24 % (2285508)Instruction limit reached!
% 65.49/10.24 % (2285508)------------------------------
% 65.49/10.24 % (2285508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.49/10.24 % (2285508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.49/10.24 % (2285508)CaDiCaL version: 2.1.3
% 65.49/10.24 % (2285508)Termination reason: Instruction limit
% 65.49/10.24 % (2285508)Termination phase: Saturation
% 65.49/10.24 % (2285508)Time elapsed: 0.448 s
% 65.49/10.24 % (2285508)Peak memory usage: 123 MB
% 65.49/10.24 % (2285508)Instructions burned: 777 (million)
% 65.49/10.24 % (2285515)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=4197534429:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2939 on theBenchmark for (2939ds/784Mi)
% 65.49/10.24 % (2285516)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=582519399:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi)
% 65.49/10.25 % (2285518)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3689527868:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2937 on theBenchmark for (2937ds/775Mi)
% 65.49/10.25 % (2285517)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=1598703341:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi)
% 65.49/10.25 % (2285506)Instruction limit reached!
% 65.49/10.25 % (2285506)------------------------------
% 65.49/10.25 % (2285506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.49/10.25 % (2285506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.49/10.25 % (2285506)CaDiCaL version: 2.1.3
% 65.49/10.25 % (2285506)Termination reason: Instruction limit
% 65.49/10.25 % (2285506)Termination phase: Saturation
% 65.49/10.25 % (2285506)Time elapsed: 0.927 s
% 65.49/10.25 % (2285506)Peak memory usage: 95 MB
% 65.49/10.25 % (2285506)Instructions burned: 835 (million)
% 65.49/10.25 % (2285512)Instruction limit reached!
% 65.49/10.25 % (2285512)------------------------------
% 65.49/10.25 % (2285512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.49/10.25 % (2285512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.49/10.25 % (2285512)CaDiCaL version: 2.1.3
% 65.49/10.25 % (2285512)Termination reason: Instruction limit
% 65.49/10.25 % (2285512)Termination phase: Saturation
% 65.49/10.25 % (2285512)Time elapsed: 0.679 s
% 65.49/10.25 % (2285512)Peak memory usage: 139 MB
% 65.49/10.25 % (2285512)Instructions burned: 646 (million)
% 65.49/10.25 % (2285517)Instruction limit reached!
% 65.49/10.25 % (2285517)------------------------------
% 65.49/10.25 % (2285517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.49/10.25 % (2285517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.49/10.25 % (2285517)CaDiCaL version: 2.1.3
% 65.49/10.25 % (2285517)Termination reason: Instruction limit
% 65.49/10.25 % (2285517)Termination phase: Saturation
% 85.87/13.16 % (2285517)Time elapsed: 0.299 s
% 85.87/13.16 % (2285517)Peak memory usage: 117 MB
% 85.87/13.16 % (2285517)Instructions burned: 246 (million)
% 85.87/13.16 % (2285518)Instruction limit reached!
% 85.87/13.16 % (2285518)------------------------------
% 85.87/13.16 % (2285518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/13.16 % (2285518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/13.16 % (2285518)CaDiCaL version: 2.1.3
% 85.87/13.16 % (2285518)Termination reason: Instruction limit
% 85.87/13.16 % (2285518)Termination phase: Saturation
% 85.87/13.16 % (2285518)Time elapsed: 0.395 s
% 85.87/13.16 % (2285518)Peak memory usage: 93 MB
% 85.87/13.16 % (2285518)Instructions burned: 777 (million)
% 85.87/13.16 % (2285525)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=46030127:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2933 on theBenchmark for (2933ds/273Mi)
% 85.87/13.16 % (2285526)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4148040984:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi)
% 85.87/13.16 % (2285526)Instruction limit reached!
% 85.87/13.16 % (2285526)------------------------------
% 85.87/13.16 % (2285526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/13.16 % (2285526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/13.16 % (2285526)CaDiCaL version: 2.1.3
% 85.87/13.16 % (2285526)Termination reason: Instruction limit
% 85.87/13.16 % (2285526)Termination phase: Saturation
% 85.87/13.16 % (2285526)Time elapsed: 0.103 s
% 85.87/13.16 % (2285526)Peak memory usage: 89 MB
% 85.87/13.16 % (2285526)Instructions burned: 102 (million)
% 85.87/13.16 % (2285528)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3233569493:i=6400:doe=on:fsr=off:rtra=on_2931 on theBenchmark for (2931ds/6400Mi)
% 85.87/13.16 % (2285527)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3553446482:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi)
% 85.87/13.16 % (2285525)Instruction limit reached!
% 85.87/13.16 % (2285525)------------------------------
% 85.87/13.16 % (2285525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/13.16 % (2285525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/13.16 % (2285525)CaDiCaL version: 2.1.3
% 85.87/13.16 % (2285525)Termination reason: Instruction limit
% 85.87/13.16 % (2285525)Termination phase: Saturation
% 85.87/13.16 % (2285525)Time elapsed: 0.315 s
% 85.87/13.16 % (2285525)Peak memory usage: 92 MB
% 85.87/13.16 % (2285525)Instructions burned: 273 (million)
% 85.87/13.16 % (2285515)Instruction limit reached!
% 85.87/13.16 % (2285515)------------------------------
% 85.87/13.16 % (2285515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/13.16 % (2285515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/13.16 % (2285515)CaDiCaL version: 2.1.3
% 85.87/13.16 % (2285515)Termination reason: Instruction limit
% 85.87/13.16 % (2285515)Termination phase: Saturation
% 85.87/13.16 % (2285515)Time elapsed: 0.962 s
% 85.87/13.16 % (2285515)Peak memory usage: 122 MB
% 85.87/13.16 % (2285515)Instructions burned: 784 (million)
% 85.87/13.16 % (2285531)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=4093941824:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi)
% 85.87/13.16 % (2285538)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=3688311176:i=1846:canc=cautious:fsr=off:rtra=on_2927 on theBenchmark for (2927ds/1846Mi)
% 85.87/13.16 % (2285516)Instruction limit reached!
% 85.87/13.16 % (2285516)------------------------------
% 85.87/13.16 % (2285516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.87/13.16 % (2285516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.87/13.16 % (2285516)CaDiCaL version: 2.1.3
% 85.87/13.16 % (2285516)Termination reason: Instruction limit
% 85.87/13.16 % (2285516)Termination phase: Saturation
% 85.87/13.16 % (2285516)Time elapsed: 1.173 s
% 85.87/13.16 % (2285516)Peak memory usage: 125 MB
% 85.87/13.16 % (2285516)Instructions burned: 1131 (million)
% 85.87/13.16 % (2285540)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2016552463:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2926 on theBenchmark for (2926ds/36816Mi)
% 103.52/15.62 % (2285542)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2107563748:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2924 on theBenchmark for (2924ds/273Mi)
% 103.52/15.62 % (2285542)Instruction limit reached!
% 103.52/15.62 % (2285542)------------------------------
% 103.52/15.62 % (2285542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.52/15.62 % (2285542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.52/15.62 % (2285542)CaDiCaL version: 2.1.3
% 103.52/15.62 % (2285542)Termination reason: Instruction limit
% 103.52/15.62 % (2285542)Termination phase: Saturation
% 103.52/15.62 % (2285542)Time elapsed: 0.275 s
% 103.52/15.62 % (2285542)Peak memory usage: 92 MB
% 103.52/15.62 % (2285542)Instructions burned: 274 (million)
% 103.52/15.62 % (2285531)Instruction limit reached!
% 103.52/15.62 % (2285531)------------------------------
% 103.52/15.62 % (2285531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.52/15.62 % (2285531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.52/15.63 % (2285531)CaDiCaL version: 2.1.3
% 103.52/15.63 % (2285531)Termination reason: Instruction limit
% 103.52/15.63 % (2285531)Termination phase: Saturation
% 103.52/15.63 % (2285531)Time elapsed: 0.924 s
% 103.52/15.63 % (2285531)Peak memory usage: 121 MB
% 103.52/15.63 % (2285531)Instructions burned: 869 (million)
% 103.52/15.63 % (2285527)Instruction limit reached!
% 103.52/15.63 % (2285527)------------------------------
% 103.52/15.63 % (2285527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.52/15.63 % (2285527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.52/15.63 % (2285527)CaDiCaL version: 2.1.3
% 103.52/15.63 % (2285527)Termination reason: Instruction limit
% 103.52/15.63 % (2285527)Termination phase: Saturation
% 103.52/15.63 % (2285527)Time elapsed: 1.178 s
% 103.52/15.63 % (2285527)Peak memory usage: 97 MB
% 103.52/15.63 % (2285527)Instructions burned: 1094 (million)
% 103.52/15.63 % (2285547)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=886172301:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2919 on theBenchmark for (2919ds/863Mi)
% 103.52/15.63 % (2285549)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3793456371:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2917 on theBenchmark for (2917ds/2216Mi)
% 103.52/15.63 % (2285548)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2093645309:i=5811:kws=precedence:nm=0:rtra=on_2917 on theBenchmark for (2917ds/5811Mi)
% 103.52/15.63 % (2285478)Instruction limit reached!
% 103.52/15.63 % (2285478)------------------------------
% 103.52/15.63 % (2285478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.52/15.63 % (2285478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.52/15.63 % (2285478)CaDiCaL version: 2.1.3
% 103.52/15.63 % (2285478)Termination reason: Instruction limit
% 103.52/15.63 % (2285478)Termination phase: Saturation
% 103.52/15.63 % (2285478)Time elapsed: 4.334 s
% 103.52/15.63 % (2285478)Peak memory usage: 106 MB
% 103.52/15.63 % (2285478)Instructions burned: 4428 (million)
% 103.52/15.63 % (2285553)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3999088654:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2911 on theBenchmark for (2911ds/801Mi)
% 103.52/15.63 % (2285538)Instruction limit reached!
% 103.52/15.63 % (2285538)------------------------------
% 103.52/15.63 % (2285538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.52/15.63 % (2285538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.52/15.63 % (2285538)CaDiCaL version: 2.1.3
% 103.52/15.63 % (2285538)Termination reason: Instruction limit
% 103.52/15.63 % (2285538)Termination phase: Saturation
% 103.52/15.63 % (2285538)Time elapsed: 1.714 s
% 103.52/15.63 % (2285538)Peak memory usage: 97 MB
% 103.52/15.63 % (2285538)Instructions burned: 1846 (million)
% 103.52/15.63 % (2285547)Instruction limit reached!
% 103.52/15.63 % (2285547)------------------------------
% 103.52/15.63 % (2285547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.52/15.63 % (2285547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.52/15.63 % (2285547)CaDiCaL version: 2.1.3
% 103.52/15.63 % (2285547)Termination reason: Instruction limit
% 103.52/15.63 % (2285547)Termination phase: Saturation
% 103.52/15.63 % (2285547)Time elapsed: 0.860 s
% 103.52/15.63 % (2285547)Peak memory usage: 120 MB
% 138.53/20.60 % (2285547)Instructions burned: 863 (million)
% 138.53/20.60 % (2285555)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=425901592:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2907 on theBenchmark for (2907ds/1026Mi)
% 138.53/20.60 % (2285556)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1797939111:i=3509:rtra=on_2907 on theBenchmark for (2907ds/3509Mi)
% 138.53/20.60 % (2285553)Instruction limit reached!
% 138.53/20.60 % (2285553)------------------------------
% 138.53/20.60 % (2285553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.53/20.60 % (2285553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.53/20.60 % (2285553)CaDiCaL version: 2.1.3
% 138.53/20.60 % (2285553)Termination reason: Instruction limit
% 138.53/20.60 % (2285553)Termination phase: Saturation
% 138.53/20.60 % (2285553)Time elapsed: 0.863 s
% 138.53/20.60 % (2285553)Peak memory usage: 94 MB
% 138.53/20.60 % (2285553)Instructions burned: 802 (million)
% 138.53/20.60 % (2285559)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3700854631:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2899 on theBenchmark for (2899ds/2127Mi)
% 138.53/20.60 % (2285528)Instruction limit reached!
% 138.53/20.60 % (2285528)------------------------------
% 138.53/20.60 % (2285528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.53/20.60 % (2285528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.53/20.60 % (2285528)CaDiCaL version: 2.1.3
% 138.53/20.60 % (2285528)Termination reason: Instruction limit
% 138.53/20.60 % (2285528)Termination phase: Saturation
% 138.53/20.60 % (2285528)Time elapsed: 3.285 s
% 138.53/20.60 % (2285528)Peak memory usage: 112 MB
% 138.53/20.60 % (2285528)Instructions burned: 6400 (million)
% 138.53/20.60 % (2285555)Instruction limit reached!
% 138.53/20.60 % (2285555)------------------------------
% 138.53/20.60 % (2285555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.53/20.60 % (2285555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.53/20.60 % (2285555)CaDiCaL version: 2.1.3
% 138.53/20.60 % (2285555)Termination reason: Instruction limit
% 138.53/20.60 % (2285555)Termination phase: Saturation
% 138.53/20.60 % (2285555)Time elapsed: 1.127 s
% 138.53/20.60 % (2285555)Peak memory usage: 96 MB
% 138.53/20.60 % (2285555)Instructions burned: 1026 (million)
% 138.53/20.60 % (2285561)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3444745892:i=1959:rtra=on:fsd=on:proc=on_2896 on theBenchmark for (2896ds/1959Mi)
% 138.53/20.60 % (2285549)Instruction limit reached!
% 138.53/20.60 % (2285549)------------------------------
% 138.53/20.60 % (2285549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.53/20.60 % (2285549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.53/20.60 % (2285549)CaDiCaL version: 2.1.3
% 138.53/20.60 % (2285549)Termination reason: Instruction limit
% 138.53/20.60 % (2285549)Termination phase: Saturation
% 138.53/20.60 % (2285549)Time elapsed: 2.258 s
% 138.53/20.60 % (2285549)Peak memory usage: 131 MB
% 138.53/20.60 % (2285549)Instructions burned: 2216 (million)
% 138.53/20.60 % (2285563)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=63718867:s2a=on:i=3553:nm=0:rtra=on_2893 on theBenchmark for (2893ds/3553Mi)
% 138.53/20.60 % (2285564)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=250385893:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/3201Mi)
% 138.53/20.60 % (2285561)Instruction limit reached!
% 138.53/20.60 % (2285561)------------------------------
% 138.53/20.60 % (2285561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.53/20.60 % (2285561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.53/20.60 % (2285561)CaDiCaL version: 2.1.3
% 138.53/20.60 % (2285561)Termination reason: Instruction limit
% 138.53/20.60 % (2285561)Termination phase: Saturation
% 138.53/20.60 % (2285561)Time elapsed: 1.177 s
% 138.53/20.60 % (2285561)Peak memory usage: 128 MB
% 138.53/20.60 % (2285561)Instructions burned: 1960 (million)
% 138.53/20.60 % (2285567)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=695638710:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2882 on theBenchmark for (2882ds/4093Mi)
% 138.53/20.60 % (2285559)Instruction limit reached!
% 138.53/20.60 % (2285559)------------------------------
% 138.53/20.60 % (2285559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285559)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285559)Termination reason: Instruction limit
% 155.39/23.01 % (2285559)Termination phase: Saturation
% 155.39/23.01 % (2285559)Time elapsed: 1.785 s
% 155.39/23.01 % (2285559)Peak memory usage: 98 MB
% 155.39/23.01 % (2285559)Instructions burned: 2128 (million)
% 155.39/23.01 % (2285569)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=3082341968:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2878 on theBenchmark for (2878ds/21173Mi)
% 155.39/23.01 % (2285556)Instruction limit reached!
% 155.39/23.01 % (2285556)------------------------------
% 155.39/23.01 % (2285556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285556)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285556)Termination reason: Instruction limit
% 155.39/23.01 % (2285556)Termination phase: Saturation
% 155.39/23.01 % (2285556)Time elapsed: 3.459 s
% 155.39/23.01 % (2285556)Peak memory usage: 114 MB
% 155.39/23.01 % (2285556)Instructions burned: 3509 (million)
% 155.39/23.01 % (2285573)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=83120801:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2870 on theBenchmark for (2870ds/10544Mi)
% 155.39/23.01 % (2285564)Instruction limit reached!
% 155.39/23.01 % (2285564)------------------------------
% 155.39/23.01 % (2285564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285564)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285564)Termination reason: Instruction limit
% 155.39/23.01 % (2285564)Termination phase: Saturation
% 155.39/23.01 % (2285564)Time elapsed: 2.790 s
% 155.39/23.01 % (2285564)Peak memory usage: 97 MB
% 155.39/23.01 % (2285564)Instructions burned: 3202 (million)
% 155.39/23.01 % (2285548)Instruction limit reached!
% 155.39/23.01 % (2285548)------------------------------
% 155.39/23.01 % (2285548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285548)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285548)Termination reason: Instruction limit
% 155.39/23.01 % (2285548)Termination phase: Saturation
% 155.39/23.01 % (2285548)Time elapsed: 5.436 s
% 155.39/23.01 % (2285548)Peak memory usage: 133 MB
% 155.39/23.01 % (2285548)Instructions burned: 5811 (million)
% 155.39/23.01 % (2285575)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=835971518:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2861 on theBenchmark for (2861ds/1262Mi)
% 155.39/23.01 % (2285576)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=297184424:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2860 on theBenchmark for (2860ds/775Mi)
% 155.39/23.01 % (2285567)Instruction limit reached!
% 155.39/23.01 % (2285567)------------------------------
% 155.39/23.01 % (2285567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285567)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285567)Termination reason: Instruction limit
% 155.39/23.01 % (2285567)Termination phase: Saturation
% 155.39/23.01 % (2285567)Time elapsed: 2.241 s
% 155.39/23.01 % (2285567)Peak memory usage: 147 MB
% 155.39/23.01 % (2285567)Instructions burned: 4094 (million)
% 155.39/23.01 % (2285579)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1671143419:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2857 on theBenchmark for (2857ds/270Mi)
% 155.39/23.01 % (2285563)Instruction limit reached!
% 155.39/23.01 % (2285563)------------------------------
% 155.39/23.01 % (2285563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285563)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285563)Termination reason: Instruction limit
% 155.39/23.01 % (2285563)Termination phase: Saturation
% 155.39/23.01 % (2285563)Time elapsed: 3.700 s
% 155.39/23.01 % (2285563)Peak memory usage: 103 MB
% 155.39/23.01 % (2285563)Instructions burned: 3554 (million)
% 155.39/23.01 % (2285579)Instruction limit reached!
% 155.39/23.01 % (2285579)------------------------------
% 155.39/23.01 % (2285579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285579)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285579)Termination reason: Instruction limit
% 155.39/23.01 % (2285579)Termination phase: Saturation
% 155.39/23.01 % (2285579)Time elapsed: 0.108 s
% 155.39/23.01 % (2285579)Peak memory usage: 92 MB
% 155.39/23.01 % (2285579)Instructions burned: 271 (million)
% 155.39/23.01 % (2285586)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=881938772:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2854 on theBenchmark for (2854ds/17165Mi)
% 155.39/23.01 % (2285576)Instruction limit reached!
% 155.39/23.01 % (2285576)------------------------------
% 155.39/23.01 % (2285576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285576)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285576)Termination reason: Instruction limit
% 155.39/23.01 % (2285576)Termination phase: Saturation
% 155.39/23.01 % (2285576)Time elapsed: 0.570 s
% 155.39/23.01 % (2285576)Peak memory usage: 94 MB
% 155.39/23.01 % (2285576)Instructions burned: 776 (million)
% 155.39/23.01 % (2285587)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3195459218:s2a=on:i=13094:s2at=-1:rtra=on_2853 on theBenchmark for (2853ds/13094Mi)
% 155.39/23.01 % (2285597)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3853430547:st=2:i=12633:rtra=on:ss=axioms_2852 on theBenchmark for (2852ds/12633Mi)
% 155.39/23.01 % (2285575)Instruction limit reached!
% 155.39/23.01 % (2285575)------------------------------
% 155.39/23.01 % (2285575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285575)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285575)Termination reason: Instruction limit
% 155.39/23.01 % (2285575)Termination phase: Saturation
% 155.39/23.01 % (2285575)Time elapsed: 0.941 s
% 155.39/23.01 % (2285575)Peak memory usage: 125 MB
% 155.39/23.01 % (2285575)Instructions burned: 1264 (million)
% 155.39/23.01 % (2285683)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2594876847:i=1783:rtra=on:gtg=position_2849 on theBenchmark for (2849ds/1783Mi)
% 155.39/23.01 % (2285683)Instruction limit reached!
% 155.39/23.01 % (2285683)------------------------------
% 155.39/23.01 % (2285683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285683)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285683)Termination reason: Instruction limit
% 155.39/23.01 % (2285683)Termination phase: Saturation
% 155.39/23.01 % (2285683)Time elapsed: 1.050 s
% 155.39/23.01 % (2285683)Peak memory usage: 123 MB
% 155.39/23.01 % (2285683)Instructions burned: 1783 (million)
% 155.39/23.01 % (2285747)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=1168504645:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2837 on theBenchmark for (2837ds/5451Mi)
% 155.39/23.01 % (2285747)Instruction limit reached!
% 155.39/23.01 % (2285747)------------------------------
% 155.39/23.01 % (2285747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285747)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285747)Termination reason: Instruction limit
% 155.39/23.01 % (2285747)Termination phase: Saturation
% 155.39/23.01 % (2285747)Time elapsed: 3.002 s
% 155.39/23.01 % (2285747)Peak memory usage: 132 MB
% 155.39/23.01 % (2285747)Instructions burned: 5452 (million)
% 155.39/23.01 % (2285586)Instruction limit reached!
% 155.39/23.01 % (2285586)------------------------------
% 155.39/23.01 % (2285586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285586)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285586)Termination reason: Instruction limit
% 155.39/23.01 % (2285586)Termination phase: Saturation
% 155.39/23.01 % (2285586)Time elapsed: 4.773 s
% 155.39/23.01 % (2285586)Peak memory usage: 436 MB
% 155.39/23.01 % (2285586)Instructions burned: 17167 (million)
% 155.39/23.01 % (2285749)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3495803736:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2805 on theBenchmark for (2805ds/4975Mi)
% 155.39/23.01 % (2285750)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3111648994:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2804 on theBenchmark for (2804ds/2076Mi)
% 155.39/23.01 % (2285573)Instruction limit reached!
% 155.39/23.01 % (2285573)------------------------------
% 155.39/23.01 % (2285573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285573)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285573)Termination reason: Instruction limit
% 155.39/23.01 % (2285573)Termination phase: Saturation
% 155.39/23.01 % (2285573)Time elapsed: 6.621 s
% 155.39/23.01 % (2285573)Peak memory usage: 168 MB
% 155.39/23.01 % (2285573)Instructions burned: 10544 (million)
% 155.39/23.01 % (2285753)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1910722999:i=5145:rtra=on_2801 on theBenchmark for (2801ds/5145Mi)
% 155.39/23.01 % (2285750)Instruction limit reached!
% 155.39/23.01 % (2285750)------------------------------
% 155.39/23.01 % (2285750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285750)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285750)Termination reason: Instruction limit
% 155.39/23.01 % (2285750)Termination phase: Saturation
% 155.39/23.01 % (2285750)Time elapsed: 0.685 s
% 155.39/23.01 % (2285750)Peak memory usage: 130 MB
% 155.39/23.01 % (2285750)Instructions burned: 2077 (million)
% 155.39/23.01 % (2285755)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=631839288:i=3509:rtra=on_2796 on theBenchmark for (2796ds/3509Mi)
% 155.39/23.01 % (2285749)First to succeed.
% 155.39/23.01 % (2285749)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2285330"
% 155.39/23.01 % (2285755)Instruction limit reached!
% 155.39/23.01 % (2285755)------------------------------
% 155.39/23.01 % (2285755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.39/23.01 % (2285755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.39/23.01 % (2285755)CaDiCaL version: 2.1.3
% 155.39/23.01 % (2285755)Termination reason: Instruction limit
% 155.39/23.01 % (2285755)Termination phase: Saturation
% 155.39/23.01 % (2285755)Time elapsed: 1.209 s
% 155.39/23.01 % (2285755)Peak memory usage: 113 MB
% 155.39/23.01 % (2285755)Instructions burned: 3510 (million)
% 155.39/23.01 % (2285757)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2580114185:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2783 on theBenchmark for (2783ds/13800Mi)
% 155.39/23.01 % (2285749)Refutation found. Thanks to Tanya!
% 155.39/23.01 % SZS status Theorem for theBenchmark
% 155.39/23.01 % SZS output start Proof for theBenchmark
% See solution above
% 156.55/23.25 % (2285749)------------------------------
% 156.55/23.25 % (2285749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.55/23.25 % (2285749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.55/23.25 % (2285749)CaDiCaL version: 2.1.3
% 156.55/23.25 % (2285749)Termination reason: Refutation
% 156.55/23.25 % (2285749)Time elapsed: 2.086 s
% 156.55/23.25 % (2285749)Peak memory usage: 132 MB
% 156.55/23.25 % (2285749)Instructions burned: 3469 (million)
% 156.55/23.25 % (2285749)------------------------------
% 156.55/23.25 % (2285749)------------------------------
% 156.55/23.25 % (2285330)Success in time 21.977 s
% 156.55/23.25 % Vampire exiting
%------------------------------------------------------------------------------