%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW583_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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:30:51 PM UTC 2026
% Result : Theorem 32.22s 5.43s
% Output : Refutation 33.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 29
% Syntax : Number of formulae : 147 ( 57 unt; 0 typ; 19 def)
% Number of atoms : 648 ( 164 equ)
% Maximal formula atoms : 48 ( 4 avg)
% Number of connectives : 769 ( 268 ~; 152 |; 248 &)
% ( 7 <=>; 94 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 911 ( 336 atm; 113 fun; 351 num; 111 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 15 usr; 8 prp; 0-3 aty)
% Number of functors : 118 ( 113 usr; 58 con; 0-5 aty)
% Number of variables : 234 ( 3 sgn 195 !; 39 ?; 234 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $tType ).
tff(type_def_11,type,
lparray_intcm_intrp: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
map: ( ty * ty ) > ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_15,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_16,type,
array: ty > ty ).
tff(func_def_17,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_18,type,
length: ( ty * uni ) > $int ).
tff(func_def_19,type,
elts: ( ty * uni ) > uni ).
tff(func_def_20,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_21,type,
t2tb: $int > uni ).
tff(func_def_22,type,
tb2t: uni > $int ).
tff(func_def_23,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_24,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_25,type,
t2tb1: map_int_int > uni ).
tff(func_def_26,type,
tb2t1: uni > map_int_int ).
tff(func_def_27,type,
t2tb2: array_int > uni ).
tff(func_def_28,type,
tb2t2: uni > array_int ).
tff(func_def_29,type,
k: $int ).
tff(func_def_30,type,
tuple2: ( ty * ty ) > ty ).
tff(func_def_31,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(func_def_32,type,
tuple2_proj_1: ( ty * ty * uni ) > uni ).
tff(func_def_33,type,
tuple2_proj_2: ( ty * ty * uni ) > uni ).
tff(func_def_34,type,
t2tb3: lparray_intcm_intrp > uni ).
tff(func_def_35,type,
tb2t3: uni > lparray_intcm_intrp ).
tff(func_def_36,type,
num_of: ( lparray_intcm_intrp * $int * $int ) > $int ).
tff(func_def_40,type,
numeq: ( array_int * $int * $int * $int ) > $int ).
tff(func_def_41,type,
num_of1: ( lparray_intcm_intrp * $int * $int ) > $int ).
tff(func_def_42,type,
numlt: ( array_int * $int * $int * $int ) > $int ).
tff(func_def_43,type,
ref: ty > ty ).
tff(func_def_44,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_45,type,
contents: ( ty * uni ) > uni ).
tff(func_def_47,type,
sK0: ( $int * lparray_intcm_intrp * $int ) > $int ).
tff(func_def_48,type,
sK1: ( $int * lparray_intcm_intrp * $int * lparray_intcm_intrp ) > $int ).
tff(func_def_49,type,
sK2: map_int_int ).
tff(func_def_50,type,
sK3: $int ).
tff(func_def_51,type,
sK4: $int ).
tff(func_def_52,type,
sK5: map_int_int ).
tff(func_def_53,type,
sK6: $int ).
tff(func_def_54,type,
sK7: map_int_int ).
tff(func_def_55,type,
sK8: $int ).
tff(func_def_56,type,
sK9: map_int_int ).
tff(func_def_57,type,
sK10: $int ).
tff(func_def_58,type,
sK11: $int ).
tff(func_def_59,type,
sK12: map_int_int ).
tff(func_def_60,type,
sK13: $int ).
tff(func_def_61,type,
sK14: $int ).
tff(func_def_62,type,
sK15: ( $int * lparray_intcm_intrp * lparray_intcm_intrp * $int ) > $int ).
tff(func_def_63,type,
sK16: ( $int * lparray_intcm_intrp * $int ) > $int ).
tff(func_def_64,type,
sK17: ( $int * lparray_intcm_intrp * $int ) > $int ).
tff(func_def_65,type,
sK18: array_int > $int ).
tff(func_def_66,type,
sK19: ( lparray_intcm_intrp * lparray_intcm_intrp * $int * $int ) > $int ).
tff(func_def_67,type,
sK20: ( $int * lparray_intcm_intrp * lparray_intcm_intrp * $int ) > $int ).
tff(func_def_68,type,
sK21: ( $int * lparray_intcm_intrp * $int ) > $int ).
tff(func_def_69,type,
sF22: uni ).
tff(func_def_70,type,
sF23: uni ).
tff(func_def_71,type,
sF24: uni ).
tff(func_def_72,type,
sF25: uni ).
tff(func_def_73,type,
sF26: map_int_int ).
tff(func_def_74,type,
sF27: uni ).
tff(func_def_75,type,
sF28: uni ).
tff(func_def_76,type,
sF29: uni ).
tff(func_def_77,type,
sF30: $int ).
tff(func_def_78,type,
sF31: $int ).
tff(func_def_79,type,
sF32: ty ).
tff(func_def_80,type,
sF33: uni ).
tff(func_def_81,type,
sF34: uni ).
tff(func_def_82,type,
sF35: $int > uni ).
tff(func_def_83,type,
sF36: $int > lparray_intcm_intrp ).
tff(func_def_84,type,
sF37: $int > $int ).
tff(func_def_85,type,
sF38: uni ).
tff(func_def_86,type,
sF39: $int > uni ).
tff(func_def_87,type,
sF40: $int > lparray_intcm_intrp ).
tff(func_def_88,type,
sF41: $int > $int ).
tff(func_def_89,type,
sF42: uni ).
tff(func_def_90,type,
sF43: uni ).
tff(func_def_91,type,
sF44: $int ).
tff(func_def_92,type,
sF45: uni ).
tff(func_def_93,type,
sF46: lparray_intcm_intrp ).
tff(func_def_94,type,
sF47: $int ).
tff(func_def_95,type,
sF48: $int ).
tff(func_def_96,type,
sF49: $int ).
tff(func_def_97,type,
sF50: uni ).
tff(func_def_98,type,
sF51: lparray_intcm_intrp ).
tff(func_def_99,type,
sF52: $int ).
tff(func_def_100,type,
sF53: $int ).
tff(func_def_101,type,
sF54: $int ).
tff(func_def_102,type,
sF55: $int ).
tff(func_def_103,type,
sF56: $int > uni ).
tff(func_def_104,type,
sF57: $int > $int ).
tff(func_def_105,type,
sF58: $int ).
tff(func_def_106,type,
sF59: uni ).
tff(func_def_107,type,
sF60: uni ).
tff(func_def_108,type,
sF61: $int > uni ).
tff(func_def_109,type,
sF62: $int > lparray_intcm_intrp ).
tff(func_def_110,type,
sF63: $int > $int ).
tff(func_def_111,type,
sF64: $int > uni ).
tff(func_def_112,type,
sF65: $int > $int ).
tff(func_def_113,type,
sF66: $int > uni ).
tff(func_def_114,type,
sF67: $int > $int ).
tff(func_def_115,type,
sF68: $int ).
tff(func_def_116,type,
sF69: $int ).
tff(func_def_117,type,
sF70: $int > $int ).
tff(func_def_118,type,
sF71: array_int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
sorted_sub: ( map_int_int * $int * $int ) > $o ).
tff(pred_def_5,type,
sorted_sub1: ( array_int * $int * $int ) > $o ).
tff(pred_def_6,type,
sorted: array_int > $o ).
tff(pred_def_7,type,
k_values: array_int > $o ).
tff(pred_def_8,type,
eq: ( lparray_intcm_intrp * $int ) > $o ).
tff(pred_def_9,type,
lt: ( lparray_intcm_intrp * $int ) > $o ).
tff(pred_def_10,type,
permut: ( array_int * array_int ) > $o ).
tff(f11,axiom,
! [X5: uni,X1: ty,X4: uni,X2: uni,X3: uni,X0: ty] :
( sort(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_eq) ).
tff(f12,axiom,
! [X1: ty,X2: uni,X4: uni,X3: uni,X0: ty] :
( sort(X0,X3)
=> ( sort(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_neq) ).
tff(f21,axiom,
! [X0: $int] : sort(int,t2tb(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort) ).
tff(f22,axiom,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(f23,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f31,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f85,conjecture,
! [X3: map_int_int,X0: $int,X2: $int,X1: map_int_int] :
( ( $lesseq(0,X0)
& k_values(tb2t2(mk_array(int,X0,t2tb1(X1))))
& $lesseq(0,X2)
& ( X0 = X2 ) )
=> ( $lesseq(0,k)
=> ( $lesseq(0,k)
=> ( $lesseq(0,$difference(X0,1))
=> ! [X4: map_int_int] :
( ! [X5: $int] :
( ( $lesseq(0,X5)
& $less(X5,k) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,$sum($difference(X0,1),1)) ) )
=> ( $lesseq(0,$difference(k,1))
=> ! [X6: $int,X5: $int,X7: map_int_int] :
( ( $lesseq(X5,$difference(k,1))
& $lesseq(0,X5) )
=> ( ( ( X6 = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,X0) )
& ! [X8: $int] :
( ( $less(X8,X6)
& $lesseq(0,X8) )
=> ( $lesseq(0,tb2t(get(int,int,t2tb1(X7),t2tb(X8))))
& $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),X5) ) )
& ! [X9: $int] :
( ( $less(X9,X5)
& $lesseq(0,X9) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X7)),t2tb(X9))),0,X6) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X9))),0,X0) ) )
& sorted_sub(X7,0,X6) )
=> ( ( $lesseq(0,X5)
& $lesseq(0,k)
& $less(X5,k) )
=> ( $lesseq(1,tb2t(get(int,int,t2tb1(X4),t2tb(X5))))
=> ! [X10: $int,X12: $int,X11: map_int_int] :
( ( $lesseq(1,X12)
& $lesseq(X12,tb2t(get(int,int,t2tb1(X4),t2tb(X5)))) )
=> ( ( sorted_sub(X11,0,X10)
& ! [X8: $int] :
( ( $less(X8,X10)
& $lesseq(0,X8) )
=> ( $lesseq(tb2t(get(int,int,t2tb1(X11),t2tb(X8))),X5)
& $lesseq(0,tb2t(get(int,int,t2tb1(X11),t2tb(X8)))) ) )
& ! [X9: $int] :
( ( $lesseq(0,X9)
& $less(X9,X5) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X11)),t2tb(X9))),0,X10) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X9))),0,X0) ) )
& ( $sum($difference(X10,X12),1) = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,X0) )
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X11)),t2tb(X5))),0,X10) = $difference(X12,1) ) )
=> ( ( $lesseq(0,X2)
& $lesseq(0,X10)
& $less(X10,X2) )
=> ! [X13: map_int_int] :
( ( ( X13 = tb2t1(set(int,int,t2tb1(X11),t2tb(X10),t2tb(X5))) )
& $lesseq(0,X2) )
=> ! [X14: $int] :
( ( X14 = $sum(X10,1) )
=> ! [X8: $int] :
( ( $lesseq(0,X8)
& $less(X8,X14) )
=> ( $lesseq(tb2t(get(int,int,t2tb1(X13),t2tb(X8))),X5)
& $lesseq(0,tb2t(get(int,int,t2tb1(X13),t2tb(X8)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_counting_sort) ).
tff(f86,negated_conjecture,
~ ! [X3: map_int_int,X0: $int,X2: $int,X1: map_int_int] :
( ( $lesseq(0,X0)
& k_values(tb2t2(mk_array(int,X0,t2tb1(X1))))
& $lesseq(0,X2)
& ( X0 = X2 ) )
=> ( $lesseq(0,k)
=> ( $lesseq(0,k)
=> ( $lesseq(0,$difference(X0,1))
=> ! [X4: map_int_int] :
( ! [X5: $int] :
( ( $lesseq(0,X5)
& $less(X5,k) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,$sum($difference(X0,1),1)) ) )
=> ( $lesseq(0,$difference(k,1))
=> ! [X6: $int,X5: $int,X7: map_int_int] :
( ( $lesseq(X5,$difference(k,1))
& $lesseq(0,X5) )
=> ( ( ( X6 = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,X0) )
& ! [X8: $int] :
( ( $less(X8,X6)
& $lesseq(0,X8) )
=> ( $lesseq(0,tb2t(get(int,int,t2tb1(X7),t2tb(X8))))
& $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),X5) ) )
& ! [X9: $int] :
( ( $less(X9,X5)
& $lesseq(0,X9) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X7)),t2tb(X9))),0,X6) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X9))),0,X0) ) )
& sorted_sub(X7,0,X6) )
=> ( ( $lesseq(0,X5)
& $lesseq(0,k)
& $less(X5,k) )
=> ( $lesseq(1,tb2t(get(int,int,t2tb1(X4),t2tb(X5))))
=> ! [X10: $int,X12: $int,X11: map_int_int] :
( ( $lesseq(1,X12)
& $lesseq(X12,tb2t(get(int,int,t2tb1(X4),t2tb(X5)))) )
=> ( ( sorted_sub(X11,0,X10)
& ! [X8: $int] :
( ( $less(X8,X10)
& $lesseq(0,X8) )
=> ( $lesseq(tb2t(get(int,int,t2tb1(X11),t2tb(X8))),X5)
& $lesseq(0,tb2t(get(int,int,t2tb1(X11),t2tb(X8)))) ) )
& ! [X9: $int] :
( ( $lesseq(0,X9)
& $less(X9,X5) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X11)),t2tb(X9))),0,X10) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X9))),0,X0) ) )
& ( $sum($difference(X10,X12),1) = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,X0) )
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X11)),t2tb(X5))),0,X10) = $difference(X12,1) ) )
=> ( ( $lesseq(0,X2)
& $lesseq(0,X10)
& $less(X10,X2) )
=> ! [X13: map_int_int] :
( ( ( X13 = tb2t1(set(int,int,t2tb1(X11),t2tb(X10),t2tb(X5))) )
& $lesseq(0,X2) )
=> ! [X14: $int] :
( ( X14 = $sum(X10,1) )
=> ! [X8: $int] :
( ( $lesseq(0,X8)
& $less(X8,X14) )
=> ( $lesseq(tb2t(get(int,int,t2tb1(X13),t2tb(X8))),X5)
& $lesseq(0,tb2t(get(int,int,t2tb1(X13),t2tb(X8)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f85]) ).
tff(f88,plain,
~ ! [X3: map_int_int,X0: $int,X2: $int,X1: map_int_int] :
( ( ~ $less(X0,0)
& k_values(tb2t2(mk_array(int,X0,t2tb1(X1))))
& ~ $less(X2,0)
& ( X0 = X2 ) )
=> ( ~ $less(k,0)
=> ( ~ $less(k,0)
=> ( ~ $less($sum(X0,$uminus(1)),0)
=> ! [X4: map_int_int] :
( ! [X5: $int] :
( ( $less(X5,k)
& ~ $less(X5,0) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,$sum($sum(X0,$uminus(1)),1)) ) )
=> ( ~ $less($sum(k,$uminus(1)),0)
=> ! [X6: $int,X5: $int,X7: map_int_int] :
( ( ~ $less($sum(k,$uminus(1)),X5)
& ~ $less(X5,0) )
=> ( ( ( X6 = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,X0) )
& ! [X8: $int] :
( ( $less(X8,X6)
& ~ $less(X8,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),0)
& $less(tb2t(get(int,int,t2tb1(X7),t2tb(X8))),X5) ) )
& ! [X9: $int] :
( ( $less(X9,X5)
& ~ $less(X9,0) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X7)),t2tb(X9))),0,X6) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X9))),0,X0) ) )
& sorted_sub(X7,0,X6) )
=> ( ( ~ $less(X5,0)
& ~ $less(k,0)
& $less(X5,k) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),1)
=> ! [X10: $int,X12: $int,X11: map_int_int] :
( ( ~ $less(X12,1)
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),X12) )
=> ( ( sorted_sub(X11,0,X10)
& ! [X8: $int] :
( ( $less(X8,X10)
& ~ $less(X8,0) )
=> ( ~ $less(X5,tb2t(get(int,int,t2tb1(X11),t2tb(X8))))
& ~ $less(tb2t(get(int,int,t2tb1(X11),t2tb(X8))),0) ) )
& ! [X9: $int] :
( ( ~ $less(X9,0)
& $less(X9,X5) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X11)),t2tb(X9))),0,X10) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X9))),0,X0) ) )
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X0,t2tb1(X1)),t2tb(X5))),0,X0) = $sum($sum(X10,$uminus(X12)),1) )
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X11)),t2tb(X5))),0,X10) = $sum(X12,$uminus(1)) ) )
=> ( ( ~ $less(X2,0)
& ~ $less(X10,0)
& $less(X10,X2) )
=> ! [X13: map_int_int] :
( ( ( X13 = tb2t1(set(int,int,t2tb1(X11),t2tb(X10),t2tb(X5))) )
& ~ $less(X2,0) )
=> ! [X14: $int] :
( ( X14 = $sum(X10,1) )
=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,X14) )
=> ( ~ $less(X5,tb2t(get(int,int,t2tb1(X13),t2tb(X8))))
& ~ $less(tb2t(get(int,int,t2tb1(X13),t2tb(X8))),0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f86]) ).
tff(f120,plain,
! [X0: $int] : ~ $less(X0,X0),
introduced(definition,[],[tha_non-reflexivity]) ).
tff(f122,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,X0)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f132,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,$sum(X0,1))
| ~ $less(X0,X1) ),
introduced(definition,[],[tha_extra_integer_ordering]) ).
tff(f135,plain,
~ ! [X2: $int,X3: map_int_int,X1: $int] :
( ( ( X1 = X2 )
& ~ $less(X1,0)
& ~ $less(X2,0)
& k_values(tb2t2(mk_array(int,X1,t2tb1(X3)))) )
=> ( ~ $less(k,0)
=> ( ~ $less(k,0)
=> ( ~ $less($sum(X1,$uminus(1)),0)
=> ! [X4: map_int_int] :
( ! [X5: $int] :
( ( $less(X5,k)
& ~ $less(X5,0) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X5))),0,$sum($sum(X1,$uminus(1)),1)) ) )
=> ( ~ $less($sum(k,$uminus(1)),0)
=> ! [X6: $int,X8: map_int_int,X7: $int] :
( ( ~ $less(X7,0)
& ~ $less($sum(k,$uminus(1)),X7) )
=> ( ( ! [X9: $int] :
( ( ~ $less(X9,0)
& $less(X9,X6) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X8),t2tb(X9))),0)
& $less(tb2t(get(int,int,t2tb1(X8),t2tb(X9))),X7) ) )
& sorted_sub(X8,0,X6)
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X7))),0,X1) = X6 )
& ! [X10: $int] :
( ( ~ $less(X10,0)
& $less(X10,X7) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X10))),0,X1) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X8)),t2tb(X10))),0,X6) ) ) )
=> ( ( $less(X7,k)
& ~ $less(X7,0)
& ~ $less(k,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),1)
=> ! [X12: $int,X13: map_int_int,X11: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),X12)
& ~ $less(X12,1) )
=> ( ( ! [X14: $int] :
( ( $less(X14,X11)
& ~ $less(X14,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X13),t2tb(X14))),0)
& ~ $less(X7,tb2t(get(int,int,t2tb1(X13),t2tb(X14)))) ) )
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X13)),t2tb(X7))),0,X11) = $sum(X12,$uminus(1)) )
& ( $sum($sum(X11,$uminus(X12)),1) = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X7))),0,X1) )
& ! [X15: $int] :
( ( ~ $less(X15,0)
& $less(X15,X7) )
=> ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X15))),0,X1) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X13)),t2tb(X15))),0,X11) ) )
& sorted_sub(X13,0,X11) )
=> ( ( ~ $less(X2,0)
& $less(X11,X2)
& ~ $less(X11,0) )
=> ! [X16: map_int_int] :
( ( ~ $less(X2,0)
& ( tb2t1(set(int,int,t2tb1(X13),t2tb(X11),t2tb(X7))) = X16 ) )
=> ! [X17: $int] :
( ( $sum(X11,1) = X17 )
=> ! [X18: $int] :
( ( ~ $less(X18,0)
& $less(X18,X17) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X16),t2tb(X18))),0)
& ~ $less(X7,tb2t(get(int,int,t2tb1(X16),t2tb(X18)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f88]) ).
tff(f165,plain,
! [X4: uni,X5: ty,X2: uni,X0: uni,X3: uni,X1: ty] :
( sort(X1,X0)
=> ( ( X2 = X4 )
=> ( get(X1,X5,set(X1,X5,X3,X4,X0),X2) = X0 ) ) ),
inference(rectify,[],[f11]) ).
tff(f171,plain,
! [X0: ty,X2: uni,X3: uni,X1: uni,X4: ty] :
( sort(X4,X3)
=> ( sort(X4,X2)
=> ! [X5: uni] :
( ( X2 != X3 )
=> ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) ) ) ) ),
inference(rectify,[],[f12]) ).
tff(f227,plain,
! [X0: ty,X2: uni,X3: uni,X1: uni,X4: ty] :
( ! [X5: uni] :
( ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) )
| ( X2 = X3 ) )
| ~ sort(X4,X2)
| ~ sort(X4,X3) ),
inference(ennf_transformation,[],[f171]) ).
tff(f228,plain,
! [X3: uni,X4: ty,X2: uni,X0: ty,X1: uni] :
( ! [X5: uni] :
( ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) )
| ( X2 = X3 ) )
| ~ sort(X4,X3)
| ~ sort(X4,X2) ),
inference(flattening,[],[f227]) ).
tff(f244,plain,
! [X4: uni,X5: ty,X2: uni,X0: uni,X3: uni,X1: ty] :
( ( get(X1,X5,set(X1,X5,X3,X4,X0),X2) = X0 )
| ( X2 != X4 )
| ~ sort(X1,X0) ),
inference(ennf_transformation,[],[f165]) ).
tff(f245,plain,
! [X0: uni,X1: ty,X4: uni,X3: uni,X2: uni,X5: ty] :
( ~ sort(X1,X0)
| ( X2 != X4 )
| ( get(X1,X5,set(X1,X5,X3,X4,X0),X2) = X0 ) ),
inference(flattening,[],[f244]) ).
tff(f248,plain,
? [X2: $int,X3: map_int_int,X1: $int] :
( ? [X4: map_int_int] :
( ? [X6: $int,X8: map_int_int,X7: $int] :
( ? [X12: $int,X13: map_int_int,X11: $int] :
( ? [X16: map_int_int] :
( ? [X17: $int] :
( ? [X18: $int] :
( ( $less(tb2t(get(int,int,t2tb1(X16),t2tb(X18))),0)
| $less(X7,tb2t(get(int,int,t2tb1(X16),t2tb(X18)))) )
& ~ $less(X18,0)
& $less(X18,X17) )
& ( $sum(X11,1) = X17 ) )
& ~ $less(X2,0)
& ( tb2t1(set(int,int,t2tb1(X13),t2tb(X11),t2tb(X7))) = X16 ) )
& ~ $less(X2,0)
& $less(X11,X2)
& ~ $less(X11,0)
& ! [X14: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X13),t2tb(X14))),0)
& ~ $less(X7,tb2t(get(int,int,t2tb1(X13),t2tb(X14)))) )
| ~ $less(X14,X11)
| $less(X14,0) )
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X13)),t2tb(X7))),0,X11) = $sum(X12,$uminus(1)) )
& ( $sum($sum(X11,$uminus(X12)),1) = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X7))),0,X1) )
& ! [X15: $int] :
( ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X15))),0,X1) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X13)),t2tb(X15))),0,X11) )
| $less(X15,0)
| ~ $less(X15,X7) )
& sorted_sub(X13,0,X11)
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),X12)
& ~ $less(X12,1) )
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),1)
& $less(X7,k)
& ~ $less(X7,0)
& ~ $less(k,0)
& ! [X9: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X8),t2tb(X9))),0)
& $less(tb2t(get(int,int,t2tb1(X8),t2tb(X9))),X7) )
| $less(X9,0)
| ~ $less(X9,X6) )
& sorted_sub(X8,0,X6)
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X7))),0,X1) = X6 )
& ! [X10: $int] :
( ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X10))),0,X1) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X8)),t2tb(X10))),0,X6) )
| $less(X10,0)
| ~ $less(X10,X7) )
& ~ $less(X7,0)
& ~ $less($sum(k,$uminus(1)),X7) )
& ~ $less($sum(k,$uminus(1)),0)
& ! [X5: $int] :
( ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X5))),0,$sum($sum(X1,$uminus(1)),1)) )
| ~ $less(X5,k)
| $less(X5,0) ) )
& ~ $less($sum(X1,$uminus(1)),0)
& ~ $less(k,0)
& ~ $less(k,0)
& ( X1 = X2 )
& ~ $less(X1,0)
& ~ $less(X2,0)
& k_values(tb2t2(mk_array(int,X1,t2tb1(X3)))) ),
inference(ennf_transformation,[],[f135]) ).
tff(f249,plain,
? [X3: map_int_int,X2: $int,X1: $int] :
( ? [X4: map_int_int] :
( ? [X7: $int,X8: map_int_int,X6: $int] :
( ~ $less(X7,0)
& ~ $less(X7,0)
& ~ $less(k,0)
& ? [X13: map_int_int,X11: $int,X12: $int] :
( ~ $less(X12,1)
& $less(X11,X2)
& ? [X16: map_int_int] :
( ( tb2t1(set(int,int,t2tb1(X13),t2tb(X11),t2tb(X7))) = X16 )
& ~ $less(X2,0)
& ? [X17: $int] :
( ? [X18: $int] :
( $less(X18,X17)
& ~ $less(X18,0)
& ( $less(tb2t(get(int,int,t2tb1(X16),t2tb(X18))),0)
| $less(X7,tb2t(get(int,int,t2tb1(X16),t2tb(X18)))) ) )
& ( $sum(X11,1) = X17 ) ) )
& ! [X15: $int] :
( ~ $less(X15,X7)
| $less(X15,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X15))),0,X1) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X13)),t2tb(X15))),0,X11) ) )
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),X12)
& ~ $less(X11,0)
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X13)),t2tb(X7))),0,X11) = $sum(X12,$uminus(1)) )
& ( $sum($sum(X11,$uminus(X12)),1) = num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X7))),0,X1) )
& sorted_sub(X13,0,X11)
& ! [X14: $int] :
( $less(X14,0)
| ~ $less(X14,X11)
| ( ~ $less(tb2t(get(int,int,t2tb1(X13),t2tb(X14))),0)
& ~ $less(X7,tb2t(get(int,int,t2tb1(X13),t2tb(X14)))) ) )
& ~ $less(X2,0) )
& $less(X7,k)
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),1)
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X7))),0,X1) = X6 )
& sorted_sub(X8,0,X6)
& ~ $less($sum(k,$uminus(1)),X7)
& ! [X10: $int] :
( ~ $less(X10,X7)
| $less(X10,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X10))),0,X1) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X8)),t2tb(X10))),0,X6) ) )
& ! [X9: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X8),t2tb(X9))),0)
& $less(tb2t(get(int,int,t2tb1(X8),t2tb(X9))),X7) )
| ~ $less(X9,X6)
| $less(X9,0) ) )
& ~ $less($sum(k,$uminus(1)),0)
& ! [X5: $int] :
( $less(X5,0)
| ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X3)),t2tb(X5))),0,$sum($sum(X1,$uminus(1)),1)) )
| ~ $less(X5,k) ) )
& ~ $less($sum(X1,$uminus(1)),0)
& ~ $less(X1,0)
& ~ $less(k,0)
& ~ $less(k,0)
& ( X1 = X2 )
& ~ $less(X2,0)
& k_values(tb2t2(mk_array(int,X1,t2tb1(X3)))) ),
inference(flattening,[],[f248]) ).
tff(f266,plain,
! [X0: uni,X1: ty,X2: uni,X3: ty,X4: uni] :
( ! [X5: uni] :
( ( get(X3,X1,X4,X2) = get(X3,X1,set(X3,X1,X4,X0,X5),X2) )
| ( X0 = X2 ) )
| ~ sort(X1,X0)
| ~ sort(X1,X2) ),
inference(rectify,[],[f228]) ).
tff(f278,plain,
? [X0: map_int_int,X1: $int,X2: $int] :
( ? [X3: map_int_int] :
( ? [X4: $int,X5: map_int_int,X6: $int] :
( ~ $less(X4,0)
& ~ $less(X4,0)
& ~ $less(k,0)
& ? [X7: map_int_int,X8: $int,X9: $int] :
( ~ $less(X9,1)
& $less(X8,X1)
& ? [X10: map_int_int] :
( ( tb2t1(set(int,int,t2tb1(X7),t2tb(X8),t2tb(X4))) = X10 )
& ~ $less(X1,0)
& ? [X11: $int] :
( ? [X12: $int] :
( $less(X12,X11)
& ~ $less(X12,0)
& ( $less(tb2t(get(int,int,t2tb1(X10),t2tb(X12))),0)
| $less(X4,tb2t(get(int,int,t2tb1(X10),t2tb(X12)))) ) )
& ( $sum(X8,1) = X11 ) ) )
& ! [X13: $int] :
( ~ $less(X13,X4)
| $less(X13,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X7)),t2tb(X13))),0,X8) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X0)),t2tb(X13))),0,X2) ) )
& ~ $less(tb2t(get(int,int,t2tb1(X3),t2tb(X4))),X9)
& ~ $less(X8,0)
& ( $sum(X9,$uminus(1)) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X7)),t2tb(X4))),0,X8) )
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X0)),t2tb(X4))),0,X2) = $sum($sum(X8,$uminus(X9)),1) )
& sorted_sub(X7,0,X8)
& ! [X14: $int] :
( $less(X14,0)
| ~ $less(X14,X8)
| ( ~ $less(tb2t(get(int,int,t2tb1(X7),t2tb(X14))),0)
& ~ $less(X4,tb2t(get(int,int,t2tb1(X7),t2tb(X14)))) ) )
& ~ $less(X1,0) )
& $less(X4,k)
& ~ $less(tb2t(get(int,int,t2tb1(X3),t2tb(X4))),1)
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X0)),t2tb(X4))),0,X2) = X6 )
& sorted_sub(X5,0,X6)
& ~ $less($sum(k,$uminus(1)),X4)
& ! [X15: $int] :
( ~ $less(X15,X4)
| $less(X15,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X1,t2tb1(X5)),t2tb(X15))),0,X6) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X0)),t2tb(X15))),0,X2) ) )
& ! [X16: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X5),t2tb(X16))),0)
& $less(tb2t(get(int,int,t2tb1(X5),t2tb(X16))),X4) )
| ~ $less(X16,X6)
| $less(X16,0) ) )
& ~ $less($sum(k,$uminus(1)),0)
& ! [X17: $int] :
( $less(X17,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,X2,t2tb1(X0)),t2tb(X17))),0,$sum($sum(X2,$uminus(1)),1)) = tb2t(get(int,int,t2tb1(X3),t2tb(X17))) )
| ~ $less(X17,k) ) )
& ~ $less($sum(X2,$uminus(1)),0)
& ~ $less(X2,0)
& ~ $less(k,0)
& ~ $less(k,0)
& ( X1 = X2 )
& ~ $less(X1,0)
& k_values(tb2t2(mk_array(int,X2,t2tb1(X0)))) ),
inference(rectify,[],[f249]) ).
tff(f279,plain,
( ~ $less(sK6,0)
& ~ $less(sK6,0)
& ~ $less(k,0)
& ~ $less(sK11,1)
& $less(sK10,sK3)
& ( tb2t1(set(int,int,t2tb1(sK9),t2tb(sK10),t2tb(sK6))) = sK12 )
& ~ $less(sK3,0)
& $less(sK14,sK13)
& ~ $less(sK14,0)
& ( $less(tb2t(get(int,int,t2tb1(sK12),t2tb(sK14))),0)
| $less(sK6,tb2t(get(int,int,t2tb1(sK12),t2tb(sK14)))) )
& ( $sum(sK10,1) = sK13 )
& ! [X13: $int] :
( ~ $less(X13,sK6)
| $less(X13,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,sK4,t2tb1(sK2)),t2tb(X13))),0,sK4) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,sK3,t2tb1(sK9)),t2tb(X13))),0,sK10) ) )
& ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),sK11)
& ~ $less(sK10,0)
& ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,sK3,t2tb1(sK9)),t2tb(sK6))),0,sK10) = $sum(sK11,$uminus(1)) )
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,sK4,t2tb1(sK2)),t2tb(sK6))),0,sK4) = $sum($sum(sK10,$uminus(sK11)),1) )
& sorted_sub(sK9,0,sK10)
& ! [X14: $int] :
( $less(X14,0)
| ~ $less(X14,sK10)
| ( ~ $less(tb2t(get(int,int,t2tb1(sK9),t2tb(X14))),0)
& ~ $less(sK6,tb2t(get(int,int,t2tb1(sK9),t2tb(X14)))) ) )
& ~ $less(sK3,0)
& $less(sK6,k)
& ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),1)
& ( num_of1(tb2t3(tuple21(array(int),int,mk_array(int,sK4,t2tb1(sK2)),t2tb(sK6))),0,sK4) = sK8 )
& sorted_sub(sK7,0,sK8)
& ~ $less($sum(k,$uminus(1)),sK6)
& ! [X15: $int] :
( ~ $less(X15,sK6)
| $less(X15,0)
| ( num_of(tb2t3(tuple21(array(int),int,mk_array(int,sK3,t2tb1(sK7)),t2tb(X15))),0,sK8) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,sK4,t2tb1(sK2)),t2tb(X15))),0,sK4) ) )
& ! [X16: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(sK7),t2tb(X16))),0)
& $less(tb2t(get(int,int,t2tb1(sK7),t2tb(X16))),sK6) )
| ~ $less(X16,sK8)
| $less(X16,0) )
& ~ $less($sum(k,$uminus(1)),0)
& ! [X17: $int] :
( $less(X17,0)
| ( tb2t(get(int,int,t2tb1(sK5),t2tb(X17))) = num_of(tb2t3(tuple21(array(int),int,mk_array(int,sK4,t2tb1(sK2)),t2tb(X17))),0,$sum($sum(sK4,$uminus(1)),1)) )
| ~ $less(X17,k) )
& ~ $less($sum(sK4,$uminus(1)),0)
& ~ $less(sK4,0)
& ~ $less(k,0)
& ~ $less(k,0)
& ( sK4 = sK3 )
& ~ $less(sK3,0)
& k_values(tb2t2(mk_array(int,sK4,t2tb1(sK2)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10),skolemize(X9,sK11),skolemize(X10,sK12),skolemize(X11,sK13),skolemize(X12,sK14)],[f278]) ).
tff(f299,plain,
! [X0: uni,X1: ty,X2: uni,X3: uni,X4: uni,X5: ty] :
( ~ sort(X1,X0)
| ( X2 != X4 )
| ( get(X1,X5,set(X1,X5,X3,X2,X0),X4) = X0 ) ),
inference(rectify,[],[f245]) ).
tff(f338,plain,
! [X2: uni,X3: ty,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( get(X3,X1,X4,X2) = get(X3,X1,set(X3,X1,X4,X0,X5),X2) )
| ~ sort(X1,X0)
| ( X0 = X2 )
| ~ sort(X1,X2) ),
inference(cnf_transformation,[],[f266]) ).
tff(f376,plain,
! [X14: $int] :
( $less(X14,0)
| ~ $less(X14,sK10)
| ~ $less(sK6,tb2t(get(int,int,t2tb1(sK9),t2tb(X14)))) ),
inference(cnf_transformation,[],[f279]) ).
tff(f377,plain,
! [X14: $int] :
( $less(X14,0)
| ~ $less(X14,sK10)
| ~ $less(tb2t(get(int,int,t2tb1(sK9),t2tb(X14))),0) ),
inference(cnf_transformation,[],[f279]) ).
tff(f384,plain,
$sum(sK10,1) = sK13,
inference(cnf_transformation,[],[f279]) ).
tff(f385,plain,
( $less(tb2t(get(int,int,t2tb1(sK12),t2tb(sK14))),0)
| $less(sK6,tb2t(get(int,int,t2tb1(sK12),t2tb(sK14)))) ),
inference(cnf_transformation,[],[f279]) ).
tff(f386,plain,
~ $less(sK14,0),
inference(cnf_transformation,[],[f279]) ).
tff(f387,plain,
$less(sK14,sK13),
inference(cnf_transformation,[],[f279]) ).
tff(f389,plain,
tb2t1(set(int,int,t2tb1(sK9),t2tb(sK10),t2tb(sK6))) = sK12,
inference(cnf_transformation,[],[f279]) ).
tff(f393,plain,
~ $less(sK6,0),
inference(cnf_transformation,[],[f279]) ).
tff(f402,plain,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f22]) ).
tff(f410,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f31]) ).
tff(f425,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty,X4: uni,X5: ty] :
( ~ sort(X1,X0)
| ( X2 != X4 )
| ( get(X1,X5,set(X1,X5,X3,X2,X0),X4) = X0 ) ),
inference(cnf_transformation,[],[f299]) ).
tff(f451,plain,
! [X0: $int] : sort(int,t2tb(X0)),
inference(cnf_transformation,[],[f21]) ).
tff(f460,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f23]) ).
tff(f494,plain,
! [X3: uni,X0: uni,X1: ty,X4: uni,X5: ty] :
( ( get(X1,X5,set(X1,X5,X3,X4,X0),X4) = X0 )
| ~ sort(X1,X0) ),
inference(equality_resolution,[],[f425]) ).
tff(f496,definition,
sF22 = t2tb1(sK9),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f497,definition,
sF23 = t2tb(sK10),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f498,definition,
sF24 = t2tb(sK6),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f499,definition,
sF25 = set(int,int,sF22,sF23,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f500,plain,
set(int,int,sF22,sF23,sF24) = sF25,
inference(reorient_equations,[],[f499]) ).
tff(f501,definition,
sF26 = tb2t1(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f502,plain,
sF26 = sK12,
inference(definition_folding,[],[f389,f501,f500,f498,f497,f496]) ).
tff(f503,definition,
sF27 = t2tb1(sK12),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f504,plain,
t2tb1(sK12) = sF27,
inference(reorient_equations,[],[f503]) ).
tff(f505,definition,
sF28 = t2tb(sK14),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f506,plain,
t2tb(sK14) = sF28,
inference(reorient_equations,[],[f505]) ).
tff(f507,definition,
sF29 = get(int,int,sF27,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f508,definition,
sF30 = tb2t(sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f509,plain,
tb2t(sF29) = sF30,
inference(reorient_equations,[],[f508]) ).
tff(f510,plain,
( $less(sK6,sF30)
| $less(sF30,0) ),
inference(definition_folding,[],[f385,f509,f507,f506,f504,f509,f507,f506,f504]) ).
tff(f511,definition,
sF31 = $sum(sK10,1),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f512,plain,
$sum(sK10,1) = sF31,
inference(reorient_equations,[],[f511]) ).
tff(f513,plain,
sF31 = sK13,
inference(definition_folding,[],[f384,f512]) ).
tff(f552,definition,
! [X14: $int] : ( sF56(X14) = get(int,int,sF22,t2tb(X14)) ),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
tff(f553,definition,
! [X14: $int] : ( sF57(X14) = tb2t(sF56(X14)) ),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
tff(f554,plain,
! [X14: $int] :
( ~ $less(sF57(X14),0)
| ~ $less(X14,sK10)
| $less(X14,0) ),
inference(definition_folding,[],[f377,f553,f552,f496]) ).
tff(f555,plain,
! [X14: $int] :
( ~ $less(sK6,sF57(X14))
| ~ $less(X14,sK10)
| $less(X14,0) ),
inference(definition_folding,[],[f376,f553,f552,f496]) ).
tff(f589,definition,
( spl72_1
<=> $less(sF30,0) ),
introduced(definition,[new_symbols(definition,[spl72_1])],[avatar_definition]) ).
tff(f591,plain,
( $less(sF30,0)
| ~ spl72_1 ),
inference(avatar_component_clause,[],[f589]) ).
tff(f593,definition,
( spl72_2
<=> $less(sK6,sF30) ),
introduced(definition,[new_symbols(definition,[spl72_2])],[avatar_definition]) ).
tff(f595,plain,
( $less(sK6,sF30)
| ~ spl72_2 ),
inference(avatar_component_clause,[],[f593]) ).
tff(f596,plain,
( spl72_1
| spl72_2 ),
inference(avatar_split_clause,[],[f510,f593,f589]) ).
tff(f597,plain,
$less(sK14,sF31),
inference(superposition,[],[f387,f513]) ).
tff(f602,plain,
sort(int,sF23),
inference(superposition,[],[f451,f497]) ).
tff(f603,plain,
sort(int,sF24),
inference(superposition,[],[f451,f498]) ).
tff(f604,plain,
sF27 = t2tb1(sF26),
inference(forward_demodulation,[],[f504,f502]) ).
tff(f617,plain,
tb2t(sF23) = sK10,
inference(superposition,[],[f402,f497]) ).
tff(f618,plain,
tb2t(sF24) = sK6,
inference(superposition,[],[f402,f498]) ).
tff(f619,plain,
tb2t(sF28) = sK14,
inference(superposition,[],[f402,f506]) ).
tff(f621,plain,
t2tb1(sF26) = sF25,
inference(superposition,[],[f410,f501]) ).
tff(f626,plain,
sF27 = sF25,
inference(forward_demodulation,[],[f621,f604]) ).
tff(f637,plain,
! [X0: uni] : sort(int,X0),
inference(superposition,[],[f451,f460]) ).
tff(f646,plain,
$less(sK14,$sum(sK10,1)),
inference(superposition,[],[f597,f512]) ).
tff(f746,plain,
~ $less(sK10,sK14),
inference(resolution,[],[f132,f646]) ).
tff(f756,plain,
set(int,int,sF22,sF23,sF24) = sF27,
inference(forward_demodulation,[],[f500,f626]) ).
tff(f816,plain,
( $less(sK14,sK10)
| ( sK14 = sK10 ) ),
inference(resolution,[],[f122,f746]) ).
tff(f865,definition,
( spl72_15
<=> ( sK14 = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl72_15])],[avatar_definition]) ).
tff(f866,plain,
( ( sK14 != sK10 )
| spl72_15 ),
inference(avatar_component_clause,[],[f865]) ).
tff(f867,plain,
( ( sK14 = sK10 )
| ~ spl72_15 ),
inference(avatar_component_clause,[],[f865]) ).
tff(f869,definition,
( spl72_16
<=> $less(sK14,sK10) ),
introduced(definition,[new_symbols(definition,[spl72_16])],[avatar_definition]) ).
tff(f871,plain,
( $less(sK14,sK10)
| ~ spl72_16 ),
inference(avatar_component_clause,[],[f869]) ).
tff(f872,plain,
( spl72_15
| spl72_16 ),
inference(avatar_split_clause,[],[f816,f869,f865]) ).
tff(f1202,plain,
sF56(sK14) = get(int,int,sF22,sF28),
inference(superposition,[],[f552,f506]) ).
tff(f1902,plain,
( ( sF24 = get(int,int,sF27,sF23) )
| ~ sort(int,sF24) ),
inference(superposition,[],[f494,f756]) ).
tff(f1904,plain,
sF24 = get(int,int,sF27,sF23),
inference(forward_subsumption_resolution,[],[f1902,f603]) ).
tff(f2488,plain,
! [X0: uni] :
( ~ sort(int,X0)
| ( sF23 = X0 )
| ( get(int,int,sF27,X0) = get(int,int,sF22,X0) )
| ~ sort(int,sF23) ),
inference(superposition,[],[f338,f756]) ).
tff(f2490,plain,
! [X0: uni] :
( ( get(int,int,sF27,X0) = get(int,int,sF22,X0) )
| ( sF23 = X0 )
| ~ sort(int,X0) ),
inference(forward_subsumption_resolution,[],[f2488,f602]) ).
tff(f2491,plain,
! [X0: uni] :
( ( get(int,int,sF27,X0) = get(int,int,sF22,X0) )
| ( sF23 = X0 ) ),
inference(forward_subsumption_resolution,[],[f2490,f637]) ).
tff(f2768,plain,
( ( t2tb(sK10) = sF28 )
| ~ spl72_15 ),
inference(superposition,[],[f506,f867]) ).
tff(f2775,plain,
( ( sF23 = sF28 )
| ~ spl72_15 ),
inference(forward_demodulation,[],[f2768,f497]) ).
tff(f2848,plain,
( ( sF29 = get(int,int,sF27,sF23) )
| ~ spl72_15 ),
inference(superposition,[],[f507,f2775]) ).
tff(f2852,plain,
( ( sF24 = sF29 )
| ~ spl72_15 ),
inference(forward_demodulation,[],[f2848,f1904]) ).
tff(f2853,plain,
( ( tb2t(sF24) = sF30 )
| ~ spl72_15 ),
inference(superposition,[],[f509,f2852]) ).
tff(f2854,plain,
( ( sK6 = sF30 )
| ~ spl72_15 ),
inference(forward_demodulation,[],[f2853,f618]) ).
tff(f2869,definition,
( spl72_72
<=> ( sK6 = sF30 ) ),
introduced(definition,[new_symbols(definition,[spl72_72])],[avatar_definition]) ).
tff(f2871,plain,
( ( sK6 = sF30 )
| ~ spl72_72 ),
inference(avatar_component_clause,[],[f2869]) ).
tff(f2880,plain,
( $less(sK6,0)
| ~ spl72_1
| ~ spl72_72 ),
inference(superposition,[],[f591,f2871]) ).
tff(f2885,plain,
( $false
| ~ spl72_1
| ~ spl72_72 ),
inference(forward_subsumption_resolution,[],[f2880,f393]) ).
tff(f2886,plain,
( ~ spl72_1
| ~ spl72_72 ),
inference(avatar_contradiction_clause,[],[f2885]) ).
tff(f2925,plain,
( spl72_72
| ~ spl72_15 ),
inference(avatar_split_clause,[],[f2854,f865,f2869]) ).
tff(f2939,plain,
( $less(sK6,sK6)
| ~ spl72_2
| ~ spl72_72 ),
inference(superposition,[],[f595,f2871]) ).
tff(f2943,plain,
( $false
| ~ spl72_2
| ~ spl72_72 ),
inference(forward_subsumption_resolution,[],[f2939,f120]) ).
tff(f2944,plain,
( ~ spl72_2
| ~ spl72_72 ),
inference(avatar_contradiction_clause,[],[f2943]) ).
tff(f3184,plain,
( ( sF23 = sF28 )
| ( sF29 = get(int,int,sF22,sF28) ) ),
inference(superposition,[],[f2491,f507]) ).
tff(f3188,definition,
( spl72_87
<=> ( sF23 = sF28 ) ),
introduced(definition,[new_symbols(definition,[spl72_87])],[avatar_definition]) ).
tff(f3190,plain,
( ( sF23 = sF28 )
| ~ spl72_87 ),
inference(avatar_component_clause,[],[f3188]) ).
tff(f3192,definition,
( spl72_88
<=> ( sF29 = get(int,int,sF22,sF28) ) ),
introduced(definition,[new_symbols(definition,[spl72_88])],[avatar_definition]) ).
tff(f3194,plain,
( ( sF29 = get(int,int,sF22,sF28) )
| ~ spl72_88 ),
inference(avatar_component_clause,[],[f3192]) ).
tff(f3196,plain,
( spl72_87
| spl72_88 ),
inference(avatar_split_clause,[],[f3184,f3192,f3188]) ).
tff(f4080,plain,
( ( sF56(sK14) = sF29 )
| ~ spl72_88 ),
inference(forward_demodulation,[],[f1202,f3194]) ).
tff(f4081,plain,
( ( tb2t(sF29) = sF57(sK14) )
| ~ spl72_88 ),
inference(superposition,[],[f553,f4080]) ).
tff(f4082,plain,
( ( sF57(sK14) = sF30 )
| ~ spl72_88 ),
inference(forward_demodulation,[],[f4081,f509]) ).
tff(f4104,plain,
( ( tb2t(sF23) = sK14 )
| ~ spl72_87 ),
inference(superposition,[],[f619,f3190]) ).
tff(f4107,plain,
( ( sK14 = sK10 )
| ~ spl72_87 ),
inference(forward_demodulation,[],[f4104,f617]) ).
tff(f4108,plain,
( $false
| spl72_15
| ~ spl72_87 ),
inference(forward_subsumption_resolution,[],[f4107,f866]) ).
tff(f4109,plain,
( spl72_15
| ~ spl72_87 ),
inference(avatar_contradiction_clause,[],[f4108]) ).
tff(f4126,plain,
( ~ $less(sF30,0)
| $less(sK14,0)
| ~ $less(sK14,sK10)
| ~ spl72_88 ),
inference(superposition,[],[f554,f4082]) ).
tff(f4127,plain,
( $less(sK14,0)
| ~ $less(sK6,sF30)
| ~ $less(sK14,sK10)
| ~ spl72_88 ),
inference(superposition,[],[f555,f4082]) ).
tff(f4148,plain,
( ~ $less(sK14,sK10)
| ~ $less(sK6,sF30)
| ~ spl72_88 ),
inference(forward_subsumption_resolution,[],[f4127,f386]) ).
tff(f4151,plain,
( ~ $less(sK14,sK10)
| ~ $less(sF30,0)
| ~ spl72_88 ),
inference(forward_subsumption_resolution,[],[f4126,f386]) ).
tff(f4155,plain,
( ~ $less(sK6,sF30)
| ~ spl72_16
| ~ spl72_88 ),
inference(forward_subsumption_resolution,[],[f4148,f871]) ).
tff(f4156,plain,
( ~ $less(sF30,0)
| ~ spl72_16
| ~ spl72_88 ),
inference(forward_subsumption_resolution,[],[f4151,f871]) ).
tff(f4157,plain,
( ~ spl72_2
| ~ spl72_16
| ~ spl72_88 ),
inference(avatar_split_clause,[],[f4155,f3192,f869,f593]) ).
tff(f4158,plain,
( ~ spl72_1
| ~ spl72_16
| ~ spl72_88 ),
inference(avatar_split_clause,[],[f4156,f3192,f869,f589]) ).
cnf(s1,plain,
( spl72_1
| spl72_2 ),
inference(sat_conversion,[],[f596]) ).
cnf(s8,plain,
( spl72_15
| spl72_16 ),
inference(sat_conversion,[],[f872]) ).
cnf(s112,plain,
( ~ spl72_1
| ~ spl72_72 ),
inference(sat_conversion,[],[f2886]) ).
cnf(s117,plain,
( ~ spl72_15
| spl72_72 ),
inference(sat_conversion,[],[f2925]) ).
cnf(s119,plain,
( ~ spl72_2
| ~ spl72_72 ),
inference(sat_conversion,[],[f2944]) ).
cnf(s134,plain,
( spl72_87
| spl72_88 ),
inference(sat_conversion,[],[f3196]) ).
cnf(s166,plain,
( spl72_15
| ~ spl72_87 ),
inference(sat_conversion,[],[f4109]) ).
cnf(s174,plain,
( ~ spl72_2
| ~ spl72_16
| ~ spl72_88 ),
inference(sat_conversion,[],[f4157]) ).
cnf(s175,plain,
( ~ spl72_1
| ~ spl72_16
| ~ spl72_88 ),
inference(sat_conversion,[],[f4158]) ).
cnf(s185,plain,
~ spl72_2,
inference(rat,[],[s174,s134,s8,s166,s117,s119]) ).
cnf(s186,plain,
spl72_1,
inference(rat,[],[s1,s185]) ).
cnf(s188,plain,
~ spl72_72,
inference(rat,[],[s112,s186]) ).
cnf(s189,plain,
~ spl72_15,
inference(rat,[],[s117,s188]) ).
cnf(s191,plain,
~ spl72_87,
inference(rat,[],[s166,s189]) ).
cnf(s192,plain,
spl72_16,
inference(rat,[],[s8,s189]) ).
cnf(s193,plain,
spl72_88,
inference(rat,[],[s134,s191]) ).
cnf(s194,plain,
$false,
inference(rat,[],[s175,s186,s193,s192]) ).
tff(f4159,plain,
$false,
inference(avatar_sat_refutation,[],[s194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW583_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n008.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 14:20:24 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.25 Running first-order theorem proving
% 0.09/0.25 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.35/1.45 % (2281877)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.35/1.45 % (2281969)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=463826238:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.35/1.45 % (2281969)Instruction limit reached!
% 4.35/1.45 % (2281969)------------------------------
% 4.35/1.45 % (2281969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.45 % (2281969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.45 % (2281969)CaDiCaL version: 2.1.3
% 4.35/1.45 % (2281969)Termination reason: Instruction limit
% 4.35/1.45 % (2281969)Termination phase: Function definition elimination
% 4.35/1.45 % (2281969)Time elapsed: 0.003 s
% 4.35/1.45 % (2281969)Peak memory usage: 87 MB
% 4.35/1.45 % (2281969)Instructions burned: 8 (million)
% 4.35/1.45 % (2281965)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=622113297:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.35/1.45 % (2281971)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2226190064:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.35/1.45 % (2281967)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=419028186:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.35/1.45 % (2281966)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3580560973:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.35/1.45 % (2281970)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1293055506:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.35/1.45 % (2281968)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2072874471:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.35/1.45 % (2281965)Instruction limit reached!
% 4.35/1.45 % (2281965)------------------------------
% 4.35/1.45 % (2281965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.45 % (2281965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.45 % (2281965)CaDiCaL version: 2.1.3
% 4.35/1.45 % (2281965)Termination reason: Instruction limit
% 4.35/1.45 % (2281965)Termination phase: Saturation
% 4.35/1.45 % (2281965)Time elapsed: 0.006 s
% 4.35/1.45 % (2281965)Peak memory usage: 87 MB
% 4.35/1.45 % (2281965)Instructions burned: 12 (million)
% 4.35/1.45 % (2281968)Instruction limit reached!
% 4.35/1.45 % (2281968)------------------------------
% 4.35/1.45 % (2281968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.45 % (2281968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.45 % (2281968)CaDiCaL version: 2.1.3
% 4.35/1.45 % (2281968)Termination reason: Instruction limit
% 4.35/1.45 % (2281968)Termination phase: Property scanning
% 4.35/1.45 % (2281968)Time elapsed: 0.006 s
% 4.35/1.45 % (2281968)Peak memory usage: 86 MB
% 4.35/1.45 % (2281968)Instructions burned: 7 (million)
% 4.35/1.45 % (2281971)Instruction limit reached!
% 4.35/1.45 % (2281971)------------------------------
% 4.35/1.45 % (2281971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.45 % (2281971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.45 % (2281971)CaDiCaL version: 2.1.3
% 4.35/1.45 % (2281971)Termination reason: Instruction limit
% 4.35/1.45 % (2281971)Termination phase: Saturation
% 4.35/1.45 % (2281971)Time elapsed: 0.042 s
% 4.35/1.45 % (2281971)Peak memory usage: 116 MB
% 4.35/1.45 % (2281971)Instructions burned: 33 (million)
% 4.35/1.45 % (2281970)Instruction limit reached!
% 4.35/1.45 % (2281970)------------------------------
% 4.35/1.45 % (2281970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.45 % (2281970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.45 % (2281970)CaDiCaL version: 2.1.3
% 4.35/1.45 % (2281970)Termination reason: Instruction limit
% 4.35/1.45 % (2281970)Termination phase: Saturation
% 4.35/1.45 % (2281970)Time elapsed: 0.052 s
% 4.35/1.45 % (2281970)Peak memory usage: 116 MB
% 4.35/1.45 % (2281970)Instructions burned: 46 (million)
% 4.35/1.45 % (2281997)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3487199116:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.35/1.45 % (2281997)Instruction limit reached!
% 4.35/1.45 % (2281997)------------------------------
% 6.24/1.73 % (2281997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.73 % (2281997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.73 % (2281997)CaDiCaL version: 2.1.3
% 6.24/1.73 % (2281997)Termination reason: Instruction limit
% 6.24/1.73 % (2281997)Termination phase: Saturation
% 6.24/1.73 % (2281997)Time elapsed: 0.008 s
% 6.24/1.73 % (2281997)Peak memory usage: 89 MB
% 6.24/1.73 % (2281997)Instructions burned: 15 (million)
% 6.24/1.73 % (2281967)Instruction limit reached!
% 6.24/1.73 % (2281967)------------------------------
% 6.24/1.73 % (2281967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.73 % (2281967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.73 % (2281967)CaDiCaL version: 2.1.3
% 6.24/1.73 % (2281967)Termination reason: Instruction limit
% 6.24/1.73 % (2281967)Termination phase: Saturation
% 6.24/1.73 % (2281967)Time elapsed: 0.215 s
% 6.24/1.73 % (2281967)Peak memory usage: 118 MB
% 6.24/1.73 % (2281967)Instructions burned: 201 (million)
% 6.24/1.73 % (2282016)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1171009374:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 6.24/1.73 % (2282015)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=1258653940:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 6.24/1.73 % (2282016)Instruction limit reached!
% 6.24/1.73 % (2282016)------------------------------
% 6.24/1.73 % (2282016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.73 % (2282016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.73 % (2282016)CaDiCaL version: 2.1.3
% 6.24/1.73 % (2282016)Termination reason: Instruction limit
% 6.24/1.73 % (2282016)Termination phase: Saturation
% 6.24/1.73 % (2282016)Time elapsed: 0.017 s
% 6.24/1.73 % (2282016)Peak memory usage: 89 MB
% 6.24/1.73 % (2282016)Instructions burned: 16 (million)
% 6.24/1.73 % (2282015)Instruction limit reached!
% 6.24/1.73 % (2282015)------------------------------
% 6.24/1.73 % (2282015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.73 % (2282015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.73 % (2282015)CaDiCaL version: 2.1.3
% 6.24/1.73 % (2282015)Termination reason: Instruction limit
% 6.24/1.73 % (2282015)Termination phase: Saturation
% 6.24/1.73 % (2282015)Time elapsed: 0.038 s
% 6.24/1.73 % (2282015)Peak memory usage: 89 MB
% 6.24/1.73 % (2282015)Instructions burned: 29 (million)
% 6.24/1.73 % (2282022)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3052511754:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.24/1.73 % (2282040)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=321180809:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 6.24/1.73 % (2282025)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=3275671232:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 6.24/1.73 % (2281966)Instruction limit reached!
% 6.24/1.73 % (2281966)------------------------------
% 6.24/1.73 % (2281966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.73 % (2281966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.73 % (2281966)CaDiCaL version: 2.1.3
% 6.24/1.73 % (2281966)Termination reason: Instruction limit
% 6.24/1.73 % (2281966)Termination phase: Saturation
% 6.24/1.73 % (2281966)Time elapsed: 0.297 s
% 6.24/1.73 % (2281966)Peak memory usage: 117 MB
% 6.24/1.73 % (2281966)Instructions burned: 307 (million)
% 6.24/1.73 % (2282022)Instruction limit reached!
% 6.24/1.73 % (2282022)------------------------------
% 6.24/1.73 % (2282022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.73 % (2282022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.73 % (2282022)CaDiCaL version: 2.1.3
% 6.24/1.73 % (2282022)Termination reason: Instruction limit
% 6.24/1.73 % (2282022)Termination phase: Saturation
% 6.24/1.73 % (2282022)Time elapsed: 0.028 s
% 6.24/1.73 % (2282022)Peak memory usage: 90 MB
% 6.24/1.73 % (2282022)Instructions burned: 24 (million)
% 6.24/1.73 % (2282025)Instruction limit reached!
% 6.24/1.73 % (2282025)------------------------------
% 7.97/2.00 % (2282025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.97/2.00 % (2282025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/2.00 % (2282025)CaDiCaL version: 2.1.3
% 7.97/2.00 % (2282025)Termination reason: Instruction limit
% 7.97/2.00 % (2282025)Termination phase: Saturation
% 7.97/2.00 % (2282025)Time elapsed: 0.029 s
% 7.97/2.00 % (2282025)Peak memory usage: 90 MB
% 7.97/2.00 % (2282025)Instructions burned: 27 (million)
% 7.97/2.00 % (2282040)Instruction limit reached!
% 7.97/2.00 % (2282040)------------------------------
% 7.97/2.00 % (2282040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.97/2.00 % (2282040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/2.00 % (2282040)CaDiCaL version: 2.1.3
% 7.97/2.00 % (2282040)Termination reason: Instruction limit
% 7.97/2.00 % (2282040)Termination phase: Saturation
% 7.97/2.00 % (2282040)Time elapsed: 0.039 s
% 7.97/2.00 % (2282040)Peak memory usage: 89 MB
% 7.97/2.00 % (2282040)Instructions burned: 86 (million)
% 7.97/2.00 % (2282054)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3563273688:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.97/2.00 % (2282054)Instruction limit reached!
% 7.97/2.00 % (2282054)------------------------------
% 7.97/2.00 % (2282054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.97/2.00 % (2282054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/2.00 % (2282054)CaDiCaL version: 2.1.3
% 7.97/2.00 % (2282054)Termination reason: Instruction limit
% 7.97/2.00 % (2282054)Termination phase: Preprocessing 1
% 7.97/2.00 % (2282054)Time elapsed: 0.002 s
% 7.97/2.00 % (2282054)Peak memory usage: 86 MB
% 7.97/2.00 % (2282054)Instructions burned: 4 (million)
% 7.97/2.00 % (2282059)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=571022069:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 7.97/2.00 % (2282063)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2387735664:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.97/2.00 % (2282073)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2355045126:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 7.97/2.00 % (2282073)Instruction limit reached!
% 7.97/2.00 % (2282073)------------------------------
% 7.97/2.00 % (2282073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.97/2.00 % (2282073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/2.00 % (2282073)CaDiCaL version: 2.1.3
% 7.97/2.00 % (2282073)Termination reason: Instruction limit
% 7.97/2.00 % (2282073)Termination phase: Preprocessing 2
% 7.97/2.00 % (2282073)Time elapsed: 0.002 s
% 7.97/2.00 % (2282073)Peak memory usage: 86 MB
% 7.97/2.00 % (2282073)Instructions burned: 3 (million)
% 7.97/2.00 % (2282063)Instruction limit reached!
% 7.97/2.00 % (2282063)------------------------------
% 7.97/2.00 % (2282063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.97/2.00 % (2282063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/2.00 % (2282063)CaDiCaL version: 2.1.3
% 7.97/2.00 % (2282063)Termination reason: Instruction limit
% 7.97/2.00 % (2282063)Termination phase: Preprocessing 3
% 7.97/2.00 % (2282063)Time elapsed: 0.005 s
% 7.97/2.00 % (2282063)Peak memory usage: 86 MB
% 7.97/2.00 % (2282063)Instructions burned: 4 (million)
% 7.97/2.00 % (2282067)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1714681191:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 7.97/2.00 % (2282069)lrs+10_1_thi=all:si=on:fd=off:random_seed=2531129441:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 7.97/2.00 % (2282072)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=1795238252:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 7.97/2.00 % (2282072)Instruction limit reached!
% 7.97/2.00 % (2282072)------------------------------
% 7.97/2.00 % (2282072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.97/2.00 % (2282072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/2.00 % (2282072)CaDiCaL version: 2.1.3
% 7.97/2.00 % (2282072)Termination reason: Instruction limit
% 10.73/2.29 % (2282072)Termination phase: Preprocessing 3
% 10.73/2.29 % (2282072)Time elapsed: 0.008 s
% 10.73/2.29 % (2282072)Peak memory usage: 86 MB
% 10.73/2.29 % (2282072)Instructions burned: 8 (million)
% 10.73/2.29 % (2282069)Instruction limit reached!
% 10.73/2.29 % (2282069)------------------------------
% 10.73/2.29 % (2282069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.29 % (2282069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.29 % (2282069)CaDiCaL version: 2.1.3
% 10.73/2.29 % (2282069)Termination reason: Instruction limit
% 10.73/2.29 % (2282069)Termination phase: Saturation
% 10.73/2.29 % (2282069)Time elapsed: 0.089 s
% 10.73/2.29 % (2282069)Peak memory usage: 116 MB
% 10.73/2.29 % (2282069)Instructions burned: 53 (million)
% 10.73/2.29 % (2282080)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2034818267:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.73/2.29 % (2282085)dis+10_1_si=on:random_seed=2866338581:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 10.73/2.29 % (2282067)Instruction limit reached!
% 10.73/2.29 % (2282067)------------------------------
% 10.73/2.29 % (2282067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.29 % (2282067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.29 % (2282067)CaDiCaL version: 2.1.3
% 10.73/2.29 % (2282067)Termination reason: Instruction limit
% 10.73/2.29 % (2282067)Termination phase: Saturation
% 10.73/2.29 % (2282067)Time elapsed: 0.131 s
% 10.73/2.29 % (2282067)Peak memory usage: 134 MB
% 10.73/2.29 % (2282067)Instructions burned: 66 (million)
% 10.73/2.29 % (2282080)Instruction limit reached!
% 10.73/2.29 % (2282080)------------------------------
% 10.73/2.29 % (2282080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.29 % (2282080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.29 % (2282080)CaDiCaL version: 2.1.3
% 10.73/2.29 % (2282080)Termination reason: Instruction limit
% 10.73/2.29 % (2282080)Termination phase: Preprocessing 1
% 10.73/2.29 % (2282080)Time elapsed: 0.003 s
% 10.73/2.29 % (2282080)Peak memory usage: 86 MB
% 10.73/2.29 % (2282080)Instructions burned: 3 (million)
% 10.73/2.29 % (2282085)Instruction limit reached!
% 10.73/2.29 % (2282085)------------------------------
% 10.73/2.29 % (2282085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.29 % (2282085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.29 % (2282085)CaDiCaL version: 2.1.3
% 10.73/2.29 % (2282085)Termination reason: Instruction limit
% 10.73/2.29 % (2282085)Termination phase: Saturation
% 10.73/2.29 % (2282085)Time elapsed: 0.006 s
% 10.73/2.29 % (2282085)Peak memory usage: 87 MB
% 10.73/2.29 % (2282085)Instructions burned: 12 (million)
% 10.73/2.29 % (2282059)Instruction limit reached!
% 10.73/2.29 % (2282059)------------------------------
% 10.73/2.29 % (2282059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.29 % (2282059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.29 % (2282059)CaDiCaL version: 2.1.3
% 10.73/2.29 % (2282059)Termination reason: Instruction limit
% 10.73/2.29 % (2282059)Termination phase: Saturation
% 10.73/2.29 % (2282059)Time elapsed: 0.216 s
% 10.73/2.29 % (2282059)Peak memory usage: 92 MB
% 10.73/2.29 % (2282059)Instructions burned: 182 (million)
% 10.73/2.29 % (2282084)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3449241231:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 10.73/2.29 % (2282089)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1927261122:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 10.73/2.29 % (2282089)Instruction limit reached!
% 10.73/2.29 % (2282089)------------------------------
% 10.73/2.29 % (2282089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.29 % (2282089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.29 % (2282089)CaDiCaL version: 2.1.3
% 10.73/2.29 % (2282089)Termination reason: Instruction limit
% 10.73/2.29 % (2282089)Termination phase: Saturation
% 10.73/2.29 % (2282089)Time elapsed: 0.026 s
% 10.73/2.29 % (2282089)Peak memory usage: 89 MB
% 10.73/2.29 % (2282089)Instructions burned: 26 (million)
% 10.73/2.29 % (2282090)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4070071277: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_2991 on theBenchmark for (2991ds/35Mi)
% 12.28/2.71 % (2282095)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4071741343:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 12.28/2.71 % (2282094)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3814284161:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 12.28/2.71 % (2282094)Instruction limit reached!
% 12.28/2.71 % (2282094)------------------------------
% 12.28/2.71 % (2282094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.28/2.71 % (2282094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.28/2.71 % (2282094)CaDiCaL version: 2.1.3
% 12.28/2.71 % (2282094)Termination reason: Instruction limit
% 12.28/2.71 % (2282094)Termination phase: Property scanning
% 12.28/2.71 % (2282094)Time elapsed: 0.009 s
% 12.28/2.71 % (2282094)Peak memory usage: 86 MB
% 12.28/2.71 % (2282094)Instructions burned: 8 (million)
% 12.28/2.71 % (2282090)Instruction limit reached!
% 12.28/2.71 % (2282090)------------------------------
% 12.28/2.71 % (2282090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.28/2.71 % (2282090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.28/2.71 % (2282090)CaDiCaL version: 2.1.3
% 12.28/2.71 % (2282090)Termination reason: Instruction limit
% 12.28/2.71 % (2282090)Termination phase: Saturation
% 12.28/2.71 % (2282090)Time elapsed: 0.041 s
% 12.28/2.71 % (2282090)Peak memory usage: 89 MB
% 12.28/2.71 % (2282090)Instructions burned: 35 (million)
% 12.28/2.71 % (2282084)Instruction limit reached!
% 12.28/2.71 % (2282084)------------------------------
% 12.28/2.71 % (2282084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.28/2.71 % (2282084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.28/2.71 % (2282084)CaDiCaL version: 2.1.3
% 12.28/2.71 % (2282084)Termination reason: Instruction limit
% 12.28/2.71 % (2282084)Termination phase: Saturation
% 12.28/2.71 % (2282084)Time elapsed: 0.182 s
% 12.28/2.71 % (2282084)Peak memory usage: 117 MB
% 12.28/2.71 % (2282084)Instructions burned: 127 (million)
% 12.28/2.71 % (2282093)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3429872598:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 12.28/2.71 % (2282093)Instruction limit reached!
% 12.28/2.71 % (2282093)------------------------------
% 12.28/2.71 % (2282093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.28/2.71 % (2282093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.28/2.71 % (2282093)CaDiCaL version: 2.1.3
% 12.28/2.71 % (2282093)Termination reason: Instruction limit
% 12.28/2.71 % (2282093)Termination phase: Property scanning
% 12.28/2.71 % (2282093)Time elapsed: 0.003 s
% 12.28/2.71 % (2282093)Peak memory usage: 85 MB
% 12.28/2.71 % (2282093)Instructions burned: 3 (million)
% 12.28/2.71 % (2282096)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=336351157:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 12.28/2.71 % (2282096)Instruction limit reached!
% 12.28/2.71 % (2282096)------------------------------
% 12.28/2.71 % (2282096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.28/2.71 % (2282096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.28/2.71 % (2282096)CaDiCaL version: 2.1.3
% 12.28/2.71 % (2282096)Termination reason: Instruction limit
% 12.28/2.71 % (2282096)Termination phase: Saturation
% 12.28/2.71 % (2282096)Time elapsed: 0.016 s
% 12.28/2.71 % (2282096)Peak memory usage: 90 MB
% 12.28/2.71 % (2282096)Instructions burned: 13 (million)
% 12.28/2.71 % (2282106)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=440567798:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 12.28/2.71 % (2282095)Instruction limit reached!
% 12.28/2.71 % (2282095)------------------------------
% 12.28/2.71 % (2282095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.28/2.71 % (2282095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.28/2.71 % (2282095)CaDiCaL version: 2.1.3
% 12.28/2.71 % (2282095)Termination reason: Instruction limit
% 12.28/2.71 % (2282095)Termination phase: Saturation
% 12.28/2.71 % (2282095)Time elapsed: 0.187 s
% 12.28/2.71 % (2282095)Peak memory usage: 92 MB
% 12.28/2.71 % (2282095)Instructions burned: 371 (million)
% 12.28/2.71 % (2282117)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=1738364347:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi)
% 17.47/3.15 % (2282114)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2825851836:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 17.47/3.15 % (2282113)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4151864735:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi)
% 17.47/3.15 % (2282113)Instruction limit reached!
% 17.47/3.15 % (2282113)------------------------------
% 17.47/3.15 % (2282113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.47/3.15 % (2282113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/3.15 % (2282113)CaDiCaL version: 2.1.3
% 17.47/3.15 % (2282113)Termination reason: Instruction limit
% 17.47/3.15 % (2282113)Termination phase: Saturation
% 17.47/3.15 % (2282113)Time elapsed: 0.011 s
% 17.47/3.15 % (2282113)Peak memory usage: 88 MB
% 17.47/3.15 % (2282113)Instructions burned: 10 (million)
% 17.47/3.15 % (2282116)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=707399605:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 17.47/3.15 % (2282119)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4266517919:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi)
% 17.47/3.15 % (2282114)Instruction limit reached!
% 17.47/3.15 % (2282114)------------------------------
% 17.47/3.15 % (2282114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.47/3.15 % (2282114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/3.15 % (2282114)CaDiCaL version: 2.1.3
% 17.47/3.15 % (2282114)Termination reason: Instruction limit
% 17.47/3.15 % (2282114)Termination phase: Saturation
% 17.47/3.15 % (2282114)Time elapsed: 0.134 s
% 17.47/3.15 % (2282114)Peak memory usage: 133 MB
% 17.47/3.15 % (2282114)Instructions burned: 72 (million)
% 17.47/3.15 % (2282116)Instruction limit reached!
% 17.47/3.15 % (2282116)------------------------------
% 17.47/3.15 % (2282116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.47/3.15 % (2282116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/3.15 % (2282116)CaDiCaL version: 2.1.3
% 17.47/3.15 % (2282116)Termination reason: Instruction limit
% 17.47/3.15 % (2282116)Termination phase: Saturation
% 17.47/3.15 % (2282116)Time elapsed: 0.087 s
% 17.47/3.15 % (2282116)Peak memory usage: 91 MB
% 17.47/3.15 % (2282116)Instructions burned: 75 (million)
% 17.47/3.15 % (2282117)Instruction limit reached!
% 17.47/3.15 % (2282117)------------------------------
% 17.47/3.15 % (2282117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.47/3.15 % (2282117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/3.15 % (2282117)CaDiCaL version: 2.1.3
% 17.47/3.15 % (2282117)Termination reason: Instruction limit
% 17.47/3.15 % (2282117)Termination phase: Saturation
% 17.47/3.15 % (2282117)Time elapsed: 0.172 s
% 17.47/3.15 % (2282117)Peak memory usage: 91 MB
% 17.47/3.15 % (2282117)Instructions burned: 296 (million)
% 17.47/3.15 % (2282121)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1741359558:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi)
% 17.47/3.15 % (2282106)Instruction limit reached!
% 17.47/3.15 % (2282106)------------------------------
% 17.47/3.15 % (2282106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.47/3.15 % (2282106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/3.15 % (2282106)CaDiCaL version: 2.1.3
% 17.47/3.15 % (2282106)Termination reason: Instruction limit
% 17.47/3.15 % (2282106)Termination phase: Saturation
% 17.47/3.15 % (2282106)Time elapsed: 0.277 s
% 17.47/3.15 % (2282106)Peak memory usage: 118 MB
% 17.47/3.15 % (2282106)Instructions burned: 226 (million)
% 17.47/3.15 % (2282119)Instruction limit reached!
% 17.47/3.15 % (2282119)------------------------------
% 17.47/3.15 % (2282119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.47/3.15 % (2282119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/3.15 % (2282119)CaDiCaL version: 2.1.3
% 17.47/3.15 % (2282119)Termination reason: Instruction limit
% 17.47/3.15 % (2282119)Termination phase: Saturation
% 17.47/3.15 % (2282119)Time elapsed: 0.175 s
% 18.70/3.63 % (2282119)Peak memory usage: 117 MB
% 18.70/3.63 % (2282119)Instructions burned: 131 (million)
% 18.70/3.63 % (2282130)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=4291241113:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi)
% 18.70/3.63 % (2282140)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=1256072812:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2985 on theBenchmark for (2985ds/259Mi)
% 18.70/3.63 % (2282130)Instruction limit reached!
% 18.70/3.63 % (2282130)------------------------------
% 18.70/3.63 % (2282130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.63 % (2282130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.63 % (2282130)CaDiCaL version: 2.1.3
% 18.70/3.63 % (2282130)Termination reason: Instruction limit
% 18.70/3.63 % (2282130)Termination phase: Saturation
% 18.70/3.63 % (2282130)Time elapsed: 0.097 s
% 18.70/3.63 % (2282130)Peak memory usage: 134 MB
% 18.70/3.63 % (2282130)Instructions burned: 40 (million)
% 18.70/3.63 % (2282121)Instruction limit reached!
% 18.70/3.63 % (2282121)------------------------------
% 18.70/3.63 % (2282121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.63 % (2282121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.63 % (2282121)CaDiCaL version: 2.1.3
% 18.70/3.63 % (2282121)Termination reason: Instruction limit
% 18.70/3.63 % (2282121)Termination phase: Saturation
% 18.70/3.63 % (2282121)Time elapsed: 0.215 s
% 18.70/3.63 % (2282121)Peak memory usage: 134 MB
% 18.70/3.63 % (2282121)Instructions burned: 131 (million)
% 18.70/3.63 % (2282137)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2622105315:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi)
% 18.70/3.63 % (2282136)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4203372821:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi)
% 18.70/3.63 % (2282139)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2277146825:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 18.70/3.63 % (2282142)dis+10_1_si=on:random_seed=3383068510:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi)
% 18.70/3.63 % (2282140)Instruction limit reached!
% 18.70/3.63 % (2282140)------------------------------
% 18.70/3.63 % (2282140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.63 % (2282140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.63 % (2282140)CaDiCaL version: 2.1.3
% 18.70/3.63 % (2282140)Termination reason: Instruction limit
% 18.70/3.63 % (2282140)Termination phase: Saturation
% 18.70/3.63 % (2282140)Time elapsed: 0.166 s
% 18.70/3.63 % (2282140)Peak memory usage: 118 MB
% 18.70/3.63 % (2282140)Instructions burned: 260 (million)
% 18.70/3.63 % (2282139)Instruction limit reached!
% 18.70/3.63 % (2282139)------------------------------
% 18.70/3.63 % (2282139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.63 % (2282139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.63 % (2282139)CaDiCaL version: 2.1.3
% 18.70/3.63 % (2282139)Termination reason: Instruction limit
% 18.70/3.63 % (2282139)Termination phase: Saturation
% 18.70/3.63 % (2282139)Time elapsed: 0.176 s
% 18.70/3.63 % (2282139)Peak memory usage: 118 MB
% 18.70/3.63 % (2282139)Instructions burned: 131 (million)
% 18.70/3.63 % (2282150)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4038339496:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 18.70/3.63 % (2282151)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2850167991:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi)
% 18.70/3.63 % (2282136)Instruction limit reached!
% 18.70/3.63 % (2282136)------------------------------
% 18.70/3.63 % (2282136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/3.63 % (2282136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/3.63 % (2282136)CaDiCaL version: 2.1.3
% 18.70/3.63 % (2282136)Termination reason: Instruction limit
% 18.70/3.63 % (2282136)Termination phase: Saturation
% 18.70/3.63 % (2282136)Time elapsed: 0.312 s
% 18.70/3.63 % (2282136)Peak memory usage: 92 MB
% 18.70/3.63 % (2282136)Instructions burned: 308 (million)
% 24.68/4.21 % (2282154)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=719977685:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 24.68/4.21 % (2282154)Instruction limit reached!
% 24.68/4.21 % (2282154)------------------------------
% 24.68/4.21 % (2282154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.68/4.21 % (2282154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.68/4.21 % (2282154)CaDiCaL version: 2.1.3
% 24.68/4.21 % (2282154)Termination reason: Instruction limit
% 24.68/4.21 % (2282154)Termination phase: Saturation
% 24.68/4.21 % (2282154)Time elapsed: 0.056 s
% 24.68/4.21 % (2282154)Peak memory usage: 117 MB
% 24.68/4.21 % (2282154)Instructions burned: 66 (million)
% 24.68/4.21 % (2282151)Instruction limit reached!
% 24.68/4.21 % (2282151)------------------------------
% 24.68/4.21 % (2282151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.68/4.21 % (2282151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.68/4.21 % (2282151)CaDiCaL version: 2.1.3
% 24.68/4.21 % (2282151)Termination reason: Instruction limit
% 24.68/4.21 % (2282151)Termination phase: Saturation
% 24.68/4.21 % (2282151)Time elapsed: 0.157 s
% 24.68/4.21 % (2282151)Peak memory usage: 91 MB
% 24.68/4.21 % (2282151)Instructions burned: 141 (million)
% 24.68/4.21 % (2282155)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3769708055:i=121:nm=16:rtra=on_2980 on theBenchmark for (2980ds/121Mi)
% 24.68/4.21 % (2282155)Instruction limit reached!
% 24.68/4.21 % (2282155)------------------------------
% 24.68/4.21 % (2282155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.68/4.21 % (2282155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.68/4.21 % (2282155)CaDiCaL version: 2.1.3
% 24.68/4.21 % (2282155)Termination reason: Instruction limit
% 24.68/4.21 % (2282155)Termination phase: Saturation
% 24.68/4.21 % (2282155)Time elapsed: 0.128 s
% 24.68/4.21 % (2282155)Peak memory usage: 90 MB
% 24.68/4.21 % (2282155)Instructions burned: 121 (million)
% 24.68/4.21 % (2282158)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=1589111278:s2a=on:i=128:s2at=5:ins=3:rtra=on_2979 on theBenchmark for (2979ds/128Mi)
% 24.68/4.21 % (2282161)dis+1010_1_to=kbo:si=on:random_seed=298485438:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2978 on theBenchmark for (2978ds/175Mi)
% 24.68/4.21 % (2282150)Instruction limit reached!
% 24.68/4.21 % (2282150)------------------------------
% 24.68/4.21 % (2282150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.68/4.21 % (2282150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.68/4.21 % (2282150)CaDiCaL version: 2.1.3
% 24.68/4.21 % (2282150)Termination reason: Instruction limit
% 24.68/4.21 % (2282150)Termination phase: Saturation
% 24.68/4.21 % (2282150)Time elapsed: 0.379 s
% 24.68/4.21 % (2282150)Peak memory usage: 93 MB
% 24.68/4.21 % (2282150)Instructions burned: 384 (million)
% 24.68/4.21 % (2282160)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=2325142133:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 24.68/4.21 % (2282137)Instruction limit reached!
% 24.68/4.21 % (2282137)------------------------------
% 24.68/4.21 % (2282137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.68/4.21 % (2282137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.68/4.21 % (2282137)CaDiCaL version: 2.1.3
% 24.68/4.21 % (2282137)Termination reason: Instruction limit
% 24.68/4.21 % (2282137)Termination phase: Saturation
% 24.68/4.21 % (2282137)Time elapsed: 0.708 s
% 24.68/4.21 % (2282137)Peak memory usage: 139 MB
% 24.68/4.21 % (2282137)Instructions burned: 598 (million)
% 24.68/4.21 % (2282161)Instruction limit reached!
% 24.68/4.21 % (2282161)------------------------------
% 24.68/4.21 % (2282161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.68/4.21 % (2282161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.68/4.21 % (2282161)CaDiCaL version: 2.1.3
% 24.68/4.21 % (2282161)Termination reason: Instruction limit
% 24.68/4.21 % (2282161)Termination phase: Saturation
% 24.68/4.21 % (2282161)Time elapsed: 0.101 s
% 24.68/4.21 % (2282161)Peak memory usage: 91 MB
% 24.68/4.21 % (2282161)Instructions burned: 177 (million)
% 24.68/4.21 % (2282158)Instruction limit reached!
% 24.68/4.21 % (2282158)------------------------------
% 24.68/4.21 % (2282158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.28/4.72 % (2282158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.28/4.72 % (2282158)CaDiCaL version: 2.1.3
% 26.28/4.72 % (2282158)Termination reason: Instruction limit
% 26.28/4.72 % (2282158)Termination phase: Saturation
% 26.28/4.72 % (2282158)Time elapsed: 0.169 s
% 26.28/4.72 % (2282158)Peak memory usage: 118 MB
% 26.28/4.72 % (2282158)Instructions burned: 128 (million)
% 26.28/4.72 % (2282160)Instruction limit reached!
% 26.28/4.72 % (2282160)------------------------------
% 26.28/4.72 % (2282160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.28/4.72 % (2282160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.28/4.72 % (2282160)CaDiCaL version: 2.1.3
% 26.28/4.72 % (2282160)Termination reason: Instruction limit
% 26.28/4.72 % (2282160)Termination phase: Saturation
% 26.28/4.72 % (2282160)Time elapsed: 0.073 s
% 26.28/4.72 % (2282160)Peak memory usage: 117 MB
% 26.28/4.72 % (2282160)Instructions burned: 39 (million)
% 26.28/4.72 % (2282166)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2124878964:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/329Mi)
% 26.28/4.72 % (2282168)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=286866881:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi)
% 26.28/4.72 % (2282173)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2952681211:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi)
% 26.28/4.72 % (2282171)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4053718168:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 26.28/4.72 % (2282176)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3225679986:i=328:kws=inv_frequency:nm=20:rtra=on_2975 on theBenchmark for (2975ds/328Mi)
% 26.28/4.72 % (2282142)Instruction limit reached!
% 26.28/4.72 % (2282142)------------------------------
% 26.28/4.72 % (2282142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.28/4.72 % (2282142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.28/4.72 % (2282142)CaDiCaL version: 2.1.3
% 26.28/4.72 % (2282142)Termination reason: Instruction limit
% 26.28/4.72 % (2282142)Termination phase: Saturation
% 26.28/4.72 % (2282142)Time elapsed: 0.927 s
% 26.28/4.72 % (2282142)Peak memory usage: 95 MB
% 26.28/4.72 % (2282142)Instructions burned: 1000 (million)
% 26.28/4.72 % (2282175)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3866285233:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi)
% 26.28/4.72 % (2282176)Instruction limit reached!
% 26.28/4.72 % (2282176)------------------------------
% 26.28/4.72 % (2282176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.28/4.72 % (2282176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.28/4.72 % (2282176)CaDiCaL version: 2.1.3
% 26.28/4.72 % (2282176)Termination reason: Instruction limit
% 26.28/4.72 % (2282176)Termination phase: Saturation
% 26.28/4.72 % (2282176)Time elapsed: 0.190 s
% 26.28/4.72 % (2282176)Peak memory usage: 118 MB
% 26.28/4.72 % (2282176)Instructions burned: 328 (million)
% 26.28/4.72 % (2282171)Instruction limit reached!
% 26.28/4.72 % (2282171)------------------------------
% 26.28/4.72 % (2282171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.28/4.72 % (2282171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.28/4.72 % (2282171)CaDiCaL version: 2.1.3
% 26.28/4.72 % (2282171)Termination reason: Instruction limit
% 26.28/4.72 % (2282171)Termination phase: Saturation
% 26.28/4.72 % (2282171)Time elapsed: 0.273 s
% 26.28/4.72 % (2282171)Peak memory usage: 136 MB
% 26.28/4.72 % (2282171)Instructions burned: 215 (million)
% 26.28/4.72 % (2282166)Instruction limit reached!
% 26.28/4.72 % (2282166)------------------------------
% 26.28/4.72 % (2282166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.28/4.72 % (2282166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.28/4.72 % (2282166)CaDiCaL version: 2.1.3
% 26.28/4.72 % (2282166)Termination reason: Instruction limit
% 26.28/4.72 % (2282166)Termination phase: Saturation
% 26.28/4.72 % (2282166)Time elapsed: 0.400 s
% 26.28/4.72 % (2282166)Peak memory usage: 119 MB
% 26.28/4.72 % (2282166)Instructions burned: 329 (million)
% 30.26/5.11 % (2282182)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1675419263:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi)
% 30.26/5.11 % (2282175)Instruction limit reached!
% 30.26/5.11 % (2282175)------------------------------
% 30.26/5.11 % (2282175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.11 % (2282175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.11 % (2282175)CaDiCaL version: 2.1.3
% 30.26/5.11 % (2282175)Termination reason: Instruction limit
% 30.26/5.11 % (2282175)Termination phase: Saturation
% 30.26/5.11 % (2282175)Time elapsed: 0.292 s
% 30.26/5.11 % (2282175)Peak memory usage: 91 MB
% 30.26/5.11 % (2282175)Instructions burned: 295 (million)
% 30.26/5.11 % (2282173)Instruction limit reached!
% 30.26/5.11 % (2282173)------------------------------
% 30.26/5.11 % (2282173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.11 % (2282173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.11 % (2282173)CaDiCaL version: 2.1.3
% 30.26/5.11 % (2282173)Termination reason: Instruction limit
% 30.26/5.11 % (2282173)Termination phase: Saturation
% 30.26/5.11 % (2282173)Time elapsed: 0.382 s
% 30.26/5.11 % (2282173)Peak memory usage: 118 MB
% 30.26/5.11 % (2282173)Instructions burned: 350 (million)
% 30.26/5.11 % (2282184)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=696997392:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi)
% 30.26/5.11 % (2282168)Instruction limit reached!
% 30.26/5.11 % (2282168)------------------------------
% 30.26/5.11 % (2282168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.11 % (2282168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.11 % (2282168)CaDiCaL version: 2.1.3
% 30.26/5.11 % (2282168)Termination reason: Instruction limit
% 30.26/5.11 % (2282168)Termination phase: Saturation
% 30.26/5.11 % (2282168)Time elapsed: 0.595 s
% 30.26/5.11 % (2282168)Peak memory usage: 136 MB
% 30.26/5.11 % (2282168)Instructions burned: 483 (million)
% 30.26/5.11 % (2282185)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2357305890:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi)
% 30.26/5.11 % (2282186)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=522642448:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi)
% 30.26/5.11 % (2282189)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=2235139995:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi)
% 30.26/5.11 % (2282188)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1412489496:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi)
% 30.26/5.11 % (2282184)Instruction limit reached!
% 30.26/5.11 % (2282184)------------------------------
% 30.26/5.11 % (2282184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.11 % (2282184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.11 % (2282184)CaDiCaL version: 2.1.3
% 30.26/5.11 % (2282184)Termination reason: Instruction limit
% 30.26/5.11 % (2282184)Termination phase: Saturation
% 30.26/5.11 % (2282184)Time elapsed: 0.245 s
% 30.26/5.11 % (2282184)Peak memory usage: 94 MB
% 30.26/5.11 % (2282184)Instructions burned: 485 (million)
% 30.26/5.11 % (2282182)Instruction limit reached!
% 30.26/5.11 % (2282182)------------------------------
% 30.26/5.11 % (2282182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.11 % (2282182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.11 % (2282182)CaDiCaL version: 2.1.3
% 30.26/5.11 % (2282182)Termination reason: Instruction limit
% 30.26/5.11 % (2282182)Termination phase: Saturation
% 30.26/5.11 % (2282182)Time elapsed: 0.335 s
% 30.26/5.11 % (2282182)Peak memory usage: 118 MB
% 30.26/5.11 % (2282182)Instructions burned: 281 (million)
% 30.26/5.11 % (2282191)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1917558401:i=375:kws=inv_arity_squared:rtra=on_2968 on theBenchmark for (2968ds/375Mi)
% 30.26/5.11 % (2282185)Instruction limit reached!
% 30.26/5.11 % (2282185)------------------------------
% 30.26/5.11 % (2282185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282185)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282185)Termination reason: Instruction limit
% 32.22/5.43 % (2282185)Termination phase: Saturation
% 32.22/5.43 % (2282185)Time elapsed: 0.326 s
% 32.22/5.43 % (2282185)Peak memory usage: 115 MB
% 32.22/5.43 % (2282185)Instructions burned: 321 (million)
% 32.22/5.43 % (2282197)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=867349007:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2966 on theBenchmark for (2966ds/513Mi)
% 32.22/5.43 % (2282196)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=143364384:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi)
% 32.22/5.43 % (2282189)Instruction limit reached!
% 32.22/5.43 % (2282189)------------------------------
% 32.22/5.43 % (2282189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282189)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282189)Termination reason: Instruction limit
% 32.22/5.43 % (2282189)Termination phase: Saturation
% 32.22/5.43 % (2282189)Time elapsed: 0.372 s
% 32.22/5.43 % (2282189)Peak memory usage: 135 MB
% 32.22/5.43 % (2282189)Instructions burned: 277 (million)
% 32.22/5.43 % (2282186)Instruction limit reached!
% 32.22/5.43 % (2282186)------------------------------
% 32.22/5.43 % (2282186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282186)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282186)Termination reason: Instruction limit
% 32.22/5.43 % (2282186)Termination phase: Saturation
% 32.22/5.43 % (2282186)Time elapsed: 0.457 s
% 32.22/5.43 % (2282186)Peak memory usage: 119 MB
% 32.22/5.43 % (2282186)Instructions burned: 416 (million)
% 32.22/5.43 % (2282199)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3612927342:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi)
% 32.22/5.43 % (2282191)Instruction limit reached!
% 32.22/5.43 % (2282191)------------------------------
% 32.22/5.43 % (2282191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282191)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282191)Termination reason: Instruction limit
% 32.22/5.43 % (2282191)Termination phase: Saturation
% 32.22/5.43 % (2282191)Time elapsed: 0.420 s
% 32.22/5.43 % (2282191)Peak memory usage: 118 MB
% 32.22/5.43 % (2282191)Instructions burned: 375 (million)
% 32.22/5.43 % (2282188)Instruction limit reached!
% 32.22/5.43 % (2282188)------------------------------
% 32.22/5.43 % (2282188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282188)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282188)Termination reason: Instruction limit
% 32.22/5.43 % (2282188)Termination phase: Saturation
% 32.22/5.43 % (2282188)Time elapsed: 0.511 s
% 32.22/5.43 % (2282188)Peak memory usage: 119 MB
% 32.22/5.43 % (2282188)Instructions burned: 472 (million)
% 32.22/5.43 % (2282197)Instruction limit reached!
% 32.22/5.43 % (2282197)------------------------------
% 32.22/5.43 % (2282197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282197)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282197)Termination reason: Instruction limit
% 32.22/5.43 % (2282197)Termination phase: Saturation
% 32.22/5.43 % (2282197)Time elapsed: 0.280 s
% 32.22/5.43 % (2282197)Peak memory usage: 93 MB
% 32.22/5.43 % (2282197)Instructions burned: 513 (million)
% 32.22/5.43 % (2282202)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2808785741:i=359:rtra=on:gtg=exists_top:ss=axioms_2963 on theBenchmark for (2963ds/359Mi)
% 32.22/5.43 % (2282203)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1790278458:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2963 on theBenchmark for (2963ds/341Mi)
% 32.22/5.43 % (2282206)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=1676330129:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi)
% 32.22/5.43 % (2282196)Instruction limit reached!
% 32.22/5.43 % (2282196)------------------------------
% 32.22/5.43 % (2282196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282196)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282196)Termination reason: Instruction limit
% 32.22/5.43 % (2282196)Termination phase: Saturation
% 32.22/5.43 % (2282196)Time elapsed: 0.449 s
% 32.22/5.43 % (2282196)Peak memory usage: 119 MB
% 32.22/5.43 % (2282196)Instructions burned: 388 (million)
% 32.22/5.43 % (2282205)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=406613589:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/261Mi)
% 32.22/5.43 % (2282207)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1427231933:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi)
% 32.22/5.43 % (2282206)Instruction limit reached!
% 32.22/5.43 % (2282206)------------------------------
% 32.22/5.43 % (2282206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282206)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282206)Termination reason: Instruction limit
% 32.22/5.43 % (2282206)Termination phase: Saturation
% 32.22/5.43 % (2282206)Time elapsed: 0.167 s
% 32.22/5.43 % (2282206)Peak memory usage: 118 MB
% 32.22/5.43 % (2282206)Instructions burned: 236 (million)
% 32.22/5.43 % (2282199)Instruction limit reached!
% 32.22/5.43 % (2282199)------------------------------
% 32.22/5.43 % (2282199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282199)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282199)Termination reason: Instruction limit
% 32.22/5.43 % (2282199)Termination phase: Saturation
% 32.22/5.43 % (2282199)Time elapsed: 0.439 s
% 32.22/5.43 % (2282199)Peak memory usage: 136 MB
% 32.22/5.43 % (2282199)Instructions burned: 334 (million)
% 32.22/5.43 % (2282202)Instruction limit reached!
% 32.22/5.43 % (2282202)------------------------------
% 32.22/5.43 % (2282202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282202)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282202)Termination reason: Instruction limit
% 32.22/5.43 % (2282202)Termination phase: Saturation
% 32.22/5.43 % (2282202)Time elapsed: 0.381 s
% 32.22/5.43 % (2282202)Peak memory usage: 92 MB
% 32.22/5.43 % (2282202)Instructions burned: 359 (million)
% 32.22/5.43 % (2282207)First to succeed.
% 32.22/5.43 % (2282207)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2281877"
% 32.22/5.43 % (2282211)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3316431039:i=146:doe=on:rtra=on_2959 on theBenchmark for (2959ds/146Mi)
% 32.22/5.43 % (2282203)Instruction limit reached!
% 32.22/5.43 % (2282203)------------------------------
% 32.22/5.43 % (2282203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282203)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282203)Termination reason: Instruction limit
% 32.22/5.43 % (2282203)Termination phase: Saturation
% 32.22/5.43 % (2282203)Time elapsed: 0.391 s
% 32.22/5.43 % (2282203)Peak memory usage: 120 MB
% 32.22/5.43 % (2282203)Instructions burned: 341 (million)
% 32.22/5.43 % (2282205)Instruction limit reached!
% 32.22/5.43 % (2282205)------------------------------
% 32.22/5.43 % (2282205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282205)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282205)Termination reason: Instruction limit
% 32.22/5.43 % (2282205)Termination phase: Saturation
% 32.22/5.43 % (2282205)Time elapsed: 0.298 s
% 32.22/5.43 % (2282205)Peak memory usage: 118 MB
% 32.22/5.43 % (2282205)Instructions burned: 262 (million)
% 32.22/5.43 % (2282215)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=866741471:avsq=on:i=276:avsqr=1,2:rtra=on_2957 on theBenchmark for (2957ds/276Mi)
% 32.22/5.43 % (2282214)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2536120184:i=4428:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/4428Mi)
% 32.22/5.43 % (2282211)Instruction limit reached!
% 32.22/5.43 % (2282211)------------------------------
% 32.22/5.43 % (2282211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282211)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282211)Termination reason: Instruction limit
% 32.22/5.43 % (2282211)Termination phase: Saturation
% 32.22/5.43 % (2282211)Time elapsed: 0.166 s
% 32.22/5.43 % (2282211)Peak memory usage: 91 MB
% 32.22/5.43 % (2282211)Instructions burned: 146 (million)
% 32.22/5.43 % (2282218)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3192581543:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi)
% 32.22/5.43 % (2282216)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1565022150:i=1052:rtra=on_2956 on theBenchmark for (2956ds/1052Mi)
% 32.22/5.43 % (2282215)Instruction limit reached!
% 32.22/5.43 % (2282215)------------------------------
% 32.22/5.43 % (2282215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.43 % (2282215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.43 % (2282215)CaDiCaL version: 2.1.3
% 32.22/5.43 % (2282215)Termination reason: Instruction limit
% 32.22/5.43 % (2282215)Termination phase: Saturation
% 32.22/5.43 % (2282215)Time elapsed: 0.195 s
% 32.22/5.43 % (2282215)Peak memory usage: 135 MB
% 32.22/5.43 % (2282215)Instructions burned: 277 (million)
% 32.22/5.43 % (2282221)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4080633759:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi)
% 32.22/5.43 % (2282207)Refutation found. Thanks to Tanya!
% 32.22/5.43 % SZS status Theorem for theBenchmark
% 32.22/5.43 % SZS output start Proof for theBenchmark
% See solution above
% 33.89/5.67 % (2282207)------------------------------
% 33.89/5.67 % (2282207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.89/5.67 % (2282207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.89/5.67 % (2282207)CaDiCaL version: 2.1.3
% 33.89/5.67 % (2282207)Termination reason: Refutation
% 33.89/5.67 % (2282207)Time elapsed: 0.222 s
% 33.89/5.67 % (2282207)Peak memory usage: 93 MB
% 33.89/5.67 % (2282207)Instructions burned: 185 (million)
% 33.89/5.67 % (2282207)------------------------------
% 33.89/5.67 % (2282207)------------------------------
% 33.89/5.67 % (2281877)Success in time 4.732 s
% 33.89/5.67 % Vampire exiting
%------------------------------------------------------------------------------