%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW604_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 : n014.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:55 PM UTC 2026
% Result : Theorem 14.79s 2.99s
% Output : Refutation 17.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 63
% Syntax : Number of formulae : 303 ( 67 unt; 0 typ; 45 def)
% Number of atoms : 1341 ( 346 equ)
% Maximal formula atoms : 27 ( 4 avg)
% Number of connectives : 1695 ( 657 ~; 794 |; 150 &)
% ( 41 <=>; 53 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number arithmetic : 1016 ( 426 atm; 32 fun; 346 num; 212 var)
% Number of types : 13 ( 11 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 41 ( 37 usr; 33 prp; 0-5 aty)
% Number of functors : 93 ( 91 usr; 36 con; 0-5 aty)
% Number of variables : 507 ( 474 !; 33 ?; 507 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
key1: $tType ).
tff(type_def_10,type,
a1: $tType ).
tff(type_def_11,type,
map_int_lplist_lpkeycm_a1rprp: $tType ).
tff(type_def_12,type,
map_key_lpoption_a1rp: $tType ).
tff(type_def_13,type,
option_a1: $tType ).
tff(type_def_14,type,
array_lplist_lpkeycm_a1rprp: $tType ).
tff(type_def_15,type,
list_lpkeycm_a1rp: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
abs1: $int > $int ).
tff(func_def_14,type,
div1: ( $int * $int ) > $int ).
tff(func_def_15,type,
mod1: ( $int * $int ) > $int ).
tff(func_def_18,type,
option: ty > ty ).
tff(func_def_19,type,
none: ty > uni ).
tff(func_def_20,type,
some: ( ty * uni ) > uni ).
tff(func_def_21,type,
match_option1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_22,type,
some_proj_11: ( ty * uni ) > uni ).
tff(func_def_23,type,
list: ty > ty ).
tff(func_def_24,type,
nil: ty > uni ).
tff(func_def_25,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_26,type,
match_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_27,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(func_def_28,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(func_def_29,type,
map: ( ty * ty ) > ty ).
tff(func_def_30,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_31,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_32,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_33,type,
array: ty > ty ).
tff(func_def_34,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_35,type,
length1: ( ty * uni ) > $int ).
tff(func_def_36,type,
elts: ( ty * uni ) > uni ).
tff(func_def_37,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_38,type,
t2tb: $int > uni ).
tff(func_def_39,type,
tb2t: uni > $int ).
tff(func_def_40,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_41,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_42,type,
key: ty ).
tff(func_def_43,type,
hash1: key1 > $int ).
tff(func_def_44,type,
bucket1: ( key1 * $int ) > $int ).
tff(func_def_45,type,
tuple2: ( ty * ty ) > ty ).
tff(func_def_46,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(func_def_47,type,
tuple2_proj_11: ( ty * ty * uni ) > uni ).
tff(func_def_48,type,
tuple2_proj_21: ( ty * ty * uni ) > uni ).
tff(func_def_49,type,
t2tb1: key1 > uni ).
tff(func_def_50,type,
tb2t1: uni > key1 ).
tff(func_def_51,type,
t: ty > ty ).
tff(func_def_52,type,
mk_t1: ( ty * $int * uni * uni ) > uni ).
tff(func_def_53,type,
size1: ( ty * uni ) > $int ).
tff(func_def_54,type,
data: ( ty * uni ) > uni ).
tff(func_def_55,type,
view: ( ty * uni ) > uni ).
tff(func_def_56,type,
a: ty ).
tff(func_def_57,type,
t2tb2: map_int_lplist_lpkeycm_a1rprp > uni ).
tff(func_def_58,type,
tb2t2: uni > map_int_lplist_lpkeycm_a1rprp ).
tff(func_def_59,type,
t2tb3: map_key_lpoption_a1rp > uni ).
tff(func_def_60,type,
tb2t3: uni > map_key_lpoption_a1rp ).
tff(func_def_61,type,
t2tb4: option_a1 > uni ).
tff(func_def_62,type,
tb2t4: uni > option_a1 ).
tff(func_def_63,type,
t2tb5: array_lplist_lpkeycm_a1rprp > uni ).
tff(func_def_64,type,
tb2t5: uni > array_lplist_lpkeycm_a1rprp ).
tff(func_def_65,type,
t2tb6: list_lpkeycm_a1rp > uni ).
tff(func_def_66,type,
tb2t6: uni > list_lpkeycm_a1rp ).
tff(func_def_67,type,
t2tb7: a1 > uni ).
tff(func_def_68,type,
tb2t7: uni > a1 ).
tff(func_def_69,type,
sK0: ( ty * uni * $int ) > key1 ).
tff(func_def_70,type,
sK1: ( ty * uni * $int ) > uni ).
tff(func_def_71,type,
sK2: $int ).
tff(func_def_72,type,
sK3: map_key_lpoption_a1rp ).
tff(func_def_73,type,
sK4: map_int_lplist_lpkeycm_a1rprp ).
tff(func_def_74,type,
sK5: $int ).
tff(func_def_75,type,
sK6: map_int_lplist_lpkeycm_a1rprp ).
tff(func_def_76,type,
sK7: map_key_lpoption_a1rp ).
tff(func_def_77,type,
sK8: a1 ).
tff(func_def_78,type,
sK9: key1 ).
tff(func_def_79,type,
sK10: $int ).
tff(func_def_80,type,
sF11: ty ).
tff(func_def_81,type,
sF12: uni ).
tff(func_def_82,type,
sF13: list_lpkeycm_a1rp ).
tff(func_def_83,type,
sF14: ty ).
tff(func_def_84,type,
sF15: uni ).
tff(func_def_85,type,
sF16: $int ).
tff(func_def_86,type,
sF17: uni ).
tff(func_def_87,type,
sF18: uni ).
tff(func_def_88,type,
sF19: uni ).
tff(func_def_89,type,
sF20: ty ).
tff(func_def_90,type,
sF21: uni ).
tff(func_def_91,type,
sF22: uni ).
tff(func_def_92,type,
sF23: map_key_lpoption_a1rp ).
tff(func_def_93,type,
sF24: uni ).
tff(func_def_94,type,
sF25: uni ).
tff(func_def_95,type,
sF26: uni ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_4,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
in_data1: ( ty * key1 * uni * uni ) > $o ).
tff(pred_def_6,type,
good_data1: ( ty * key1 * uni * uni * uni ) > $o ).
tff(pred_def_7,type,
good_hash1: ( ty * uni * $int ) > $o ).
tff(f26,axiom,
! [X0: ty] : sort1(option(X0),none(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',none_sort1) ).
tff(f31,axiom,
! [X0: ty,X1: uni] : ( none(X0) != some(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',none_Some1) ).
tff(f46,axiom,
! [X1: uni,X0: ty] :
( sort1(X0,X1)
=> ( ~ mem(X0,X1,nil(X0))
& ! [X2: uni,X3: uni] :
( sort1(X0,X2)
=> ( mem(X0,X1,cons(X0,X2,X3))
<=> ( mem(X0,X1,X3)
| ( X1 = X2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_def) ).
tff(f51,axiom,
! [X1: ty,X2: uni,X0: ty] : sort1(map(X0,X1),const(X1,X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',const_sort1) ).
tff(f52,axiom,
! [X2: uni,X0: ty,X3: uni,X1: ty] :
( sort1(X1,X2)
=> ( get(X1,X0,const(X1,X0,X2),X3) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',const) ).
tff(f54,axiom,
! [X2: uni,X1: $int,X0: ty] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_def1) ).
tff(f56,axiom,
! [X2: uni,X0: ty,X1: $int] :
( sort1(map(int,X0),X2)
=> ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',elts_def1) ).
tff(f62,axiom,
! [X2: $int,X1: uni,X0: ty] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def) ).
tff(f69,axiom,
! [X0: $int] :
( $less(0,X0)
=> ! [X1: key1] :
( $lesseq(0,bucket1(X1,X0))
& $less(bucket1(X1,X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bucket_bounds) ).
tff(f70,axiom,
! [X2: uni,X3: uni,X1: ty,X0: ty] : sort1(tuple2(X1,X0),tuple21(X1,X0,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tuple2_sort1) ).
tff(f79,axiom,
! [X0: ty,X2: uni,X3: uni,X1: key1] :
( mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X1),X2),get2(list(tuple2(key,X0)),X3,bucket1(X1,length1(list(tuple2(key,X0)),X3))))
<=> in_data1(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',in_data_def) ).
tff(f80,axiom,
! [X4: uni,X0: ty,X2: uni,X3: uni,X1: key1] :
( good_data1(X0,X1,X2,X3,X4)
<=> ( ( get(option(X0),key,X3,t2tb1(X1)) = some(X0,X2) )
<=> in_data1(X0,X1,X2,X4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',good_data_def) ).
tff(f81,axiom,
! [X2: $int,X1: uni,X0: ty] :
( ( good_hash1(X0,X1,X2)
=> ! [X3: key1,X4: uni] :
( mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X4),get2(list(tuple2(key,X0)),X1,X2))
=> ( bucket1(X3,length1(list(tuple2(key,X0)),X1)) = X2 ) ) )
& ( ! [X4: uni,X3: key1] :
( sort1(X0,X4)
=> ( mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X4),get2(list(tuple2(key,X0)),X1,X2))
=> ( bucket1(X3,length1(list(tuple2(key,X0)),X1)) = X2 ) ) )
=> good_hash1(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',good_hash_def) ).
tff(f89,axiom,
! [X0: map_int_lplist_lpkeycm_a1rprp] : sort1(map(int,list(tuple2(key,a))),t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f91,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR2) ).
tff(f94,axiom,
! [X0: uni] :
( sort1(map(key,option(a)),X0)
=> ( t2tb3(tb2t3(X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR3) ).
tff(f103,axiom,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR6) ).
tff(f107,conjecture,
! [X0: $int,X1: map_int_lplist_lpkeycm_a1rprp,X2: map_key_lpoption_a1rp] :
( ( ! [X3: $int] :
( ( $lesseq(0,X3)
& $less(X3,X0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) )
& $lesseq(0,X0)
& $less(0,X0)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1))) )
=> ! [X6: $int] :
( ( X6 = 0 )
=> ( $lesseq(0,X0)
& ! [X7: map_int_lplist_lpkeycm_a1rprp] :
( ( $lesseq(0,X0)
& ! [X3: $int] :
( ( $lesseq(0,X3)
& $less(X3,$sum(0,X0)) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X3))) = tb2t6(nil(tuple2(key,a))) ) )
& ! [X3: $int] :
( ( ( $less(X3,X0)
& $lesseq($sum(0,X0),X3) )
| ( $lesseq(0,X3)
& $less(X3,0) ) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X3))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X1),t2tb(X3))) ) ) )
=> ! [X8: map_key_lpoption_a1rp] :
( ( X8 = tb2t3(const(option(a),key,none(a))) )
=> ( $lesseq(0,X0)
& ( X8 = tb2t3(const(option(a),key,none(a))) )
& ! [X4: key1,X5: a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)))
& $less(0,X0)
& ! [X3: $int] :
( ( $lesseq(0,X3)
& $less(X3,X0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)),X3) ) ) ) )
& $lesseq(0,0)
& $lesseq($sum(0,X0),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_clear) ).
tff(f108,negated_conjecture,
~ ! [X0: $int,X1: map_int_lplist_lpkeycm_a1rprp,X2: map_key_lpoption_a1rp] :
( ( ! [X3: $int] :
( ( $lesseq(0,X3)
& $less(X3,X0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) )
& $lesseq(0,X0)
& $less(0,X0)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1))) )
=> ! [X6: $int] :
( ( X6 = 0 )
=> ( $lesseq(0,X0)
& ! [X7: map_int_lplist_lpkeycm_a1rprp] :
( ( $lesseq(0,X0)
& ! [X3: $int] :
( ( $lesseq(0,X3)
& $less(X3,$sum(0,X0)) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X3))) = tb2t6(nil(tuple2(key,a))) ) )
& ! [X3: $int] :
( ( ( $less(X3,X0)
& $lesseq($sum(0,X0),X3) )
| ( $lesseq(0,X3)
& $less(X3,0) ) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X3))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X1),t2tb(X3))) ) ) )
=> ! [X8: map_key_lpoption_a1rp] :
( ( X8 = tb2t3(const(option(a),key,none(a))) )
=> ( $lesseq(0,X0)
& ( X8 = tb2t3(const(option(a),key,none(a))) )
& ! [X4: key1,X5: a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)))
& $less(0,X0)
& ! [X3: $int] :
( ( $lesseq(0,X3)
& $less(X3,X0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)),X3) ) ) ) )
& $lesseq(0,0)
& $lesseq($sum(0,X0),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f107]) ).
tff(f123,plain,
~ ! [X0: $int,X1: map_int_lplist_lpkeycm_a1rprp,X2: map_key_lpoption_a1rp] :
( ( ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))
& $less(0,X0)
& ~ $less(X0,0)
& ! [X3: $int] :
( ( $less(X3,X0)
& ~ $less(X3,0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) ) )
=> ! [X6: $int] :
( ( X6 = 0 )
=> ( ~ $less(X0,0)
& ! [X7: map_int_lplist_lpkeycm_a1rprp] :
( ( ~ $less(X0,0)
& ! [X3: $int] :
( ( ~ $less(X3,0)
& $less(X3,$sum(0,X0)) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X3))) = tb2t6(nil(tuple2(key,a))) ) )
& ! [X3: $int] :
( ( ( $less(X3,X0)
& ~ $less(X3,$sum(0,X0)) )
| ( ~ $less(X3,0)
& $less(X3,0) ) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X3))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X1),t2tb(X3))) ) ) )
=> ! [X8: map_key_lpoption_a1rp] :
( ( X8 = tb2t3(const(option(a),key,none(a))) )
=> ( ~ $less(X0,0)
& ( X8 = tb2t3(const(option(a),key,none(a))) )
& ! [X4: key1,X5: a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)))
& $less(0,X0)
& ! [X3: $int] :
( ( ~ $less(X3,0)
& $less(X3,X0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)),X3) ) ) ) )
& ~ $less(0,0)
& ~ $less(X0,$sum(0,X0)) ) ) ),
inference(theory_normalization,[],[f108]) ).
tff(f125,plain,
! [X0: $int] :
( $less(0,X0)
=> ! [X1: key1] :
( $less(bucket1(X1,X0),X0)
& ~ $less(bucket1(X1,X0),0) ) ),
inference(theory_normalization,[],[f69]) ).
tff(f128,plain,
! [X2: ty,X0: $int,X1: uni] :
( ( good_hash1(X2,X1,X0)
=> ! [X4: uni,X3: key1] :
( mem(tuple2(key,X2),tuple21(key,X2,t2tb1(X3),X4),get2(list(tuple2(key,X2)),X1,X0))
=> ( bucket1(X3,length1(list(tuple2(key,X2)),X1)) = X0 ) ) )
& ( ! [X6: key1,X5: uni] :
( sort1(X2,X5)
=> ( mem(tuple2(key,X2),tuple21(key,X2,t2tb1(X6),X5),get2(list(tuple2(key,X2)),X1,X0))
=> ( bucket1(X6,length1(list(tuple2(key,X2)),X1)) = X0 ) ) )
=> good_hash1(X2,X1,X0) ) ),
inference(rectify,[],[f81]) ).
tff(f133,plain,
! [X1: $int,X2: ty,X0: uni] : ( length1(X2,mk_array1(X2,X1,X0)) = X1 ),
inference(rectify,[],[f54]) ).
tff(f135,plain,
! [X0: $int,X1: uni,X2: ty] : ( get(X2,int,elts(X2,X1),t2tb(X0)) = get2(X2,X1,X0) ),
inference(rectify,[],[f62]) ).
tff(f142,plain,
! [X1: ty,X2: uni,X4: key1,X0: uni,X3: uni] :
( ( ( some(X1,X2) = get(option(X1),key,X3,t2tb1(X4)) )
<=> in_data1(X1,X4,X2,X0) )
<=> good_data1(X1,X4,X2,X3,X0) ),
inference(rectify,[],[f80]) ).
tff(f147,plain,
! [X2: uni,X1: uni,X3: key1,X0: ty] :
( in_data1(X0,X3,X1,X2)
<=> mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X1),get2(list(tuple2(key,X0)),X2,bucket1(X3,length1(list(tuple2(key,X0)),X2)))) ),
inference(rectify,[],[f79]) ).
tff(f155,plain,
! [X0: uni,X1: ty] :
( sort1(X1,X0)
=> ( ~ mem(X1,X0,nil(X1))
& ! [X2: uni,X3: uni] :
( sort1(X1,X2)
=> ( mem(X1,X0,cons(X1,X2,X3))
<=> ( ( X0 = X2 )
| mem(X1,X0,X3) ) ) ) ) ),
inference(rectify,[],[f46]) ).
tff(f161,plain,
! [X3: ty,X1: ty,X2: uni,X0: uni] :
( sort1(X3,X0)
=> ( get(X3,X1,const(X3,X1,X0),X2) = X0 ) ),
inference(rectify,[],[f52]) ).
tff(f162,plain,
! [X2: ty,X1: uni,X0: ty] : sort1(map(X2,X0),const(X0,X2,X1)),
inference(rectify,[],[f51]) ).
tff(f165,plain,
~ ! [X1: map_int_lplist_lpkeycm_a1rprp,X2: map_key_lpoption_a1rp,X0: $int] :
( ( ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))
& $less(0,X0)
& ~ $less(X0,0)
& ! [X3: $int] :
( ( $less(X3,X0)
& ~ $less(X3,0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) ) )
=> ! [X6: $int] :
( ( X6 = 0 )
=> ( ! [X7: map_int_lplist_lpkeycm_a1rprp] :
( ( ~ $less(X0,0)
& ! [X9: $int] :
( ( ( $less(X9,X0)
& ~ $less(X9,$sum(0,X0)) )
| ( ~ $less(X9,0)
& $less(X9,0) ) )
=> ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X1),t2tb(X9))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X9))) ) )
& ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,$sum(0,X0)) )
=> ( tb2t6(nil(tuple2(key,a))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X8))) ) ) )
=> ! [X10: map_key_lpoption_a1rp] :
( ( tb2t3(const(option(a),key,none(a))) = X10 )
=> ( ! [X12: a1,X11: key1] : good_data1(a,X11,t2tb7(X12),t2tb3(X10),mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)))
& $less(0,X0)
& ! [X13: $int] :
( ( $less(X13,X0)
& ~ $less(X13,0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)),X13) )
& ( tb2t3(const(option(a),key,none(a))) = X10 )
& ~ $less(X0,0) ) ) )
& ~ $less(X0,$sum(0,X0))
& ~ $less(0,0)
& ~ $less(X0,0) ) ) ),
inference(rectify,[],[f123]) ).
tff(f167,plain,
! [X0: uni,X1: ty,X2: $int] :
( sort1(map(int,X1),X0)
=> ( elts(X1,mk_array1(X1,X2,X0)) = X0 ) ),
inference(rectify,[],[f56]) ).
tff(f174,plain,
! [X1: uni,X0: uni,X2: ty,X3: ty] : sort1(tuple2(X2,X3),tuple21(X2,X3,X0,X1)),
inference(rectify,[],[f70]) ).
tff(f184,plain,
? [X1: map_int_lplist_lpkeycm_a1rprp,X2: map_key_lpoption_a1rp,X0: $int] :
( ? [X6: $int] :
( ( ? [X7: map_int_lplist_lpkeycm_a1rprp] :
( ? [X10: map_key_lpoption_a1rp] :
( ( ? [X12: a1,X11: key1] : ~ good_data1(a,X11,t2tb7(X12),t2tb3(X10),mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)))
| ~ $less(0,X0)
| ? [X13: $int] :
( ~ good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)),X13)
& $less(X13,X0)
& ~ $less(X13,0) )
| ( tb2t3(const(option(a),key,none(a))) != X10 )
| $less(X0,0) )
& ( tb2t3(const(option(a),key,none(a))) = X10 ) )
& ~ $less(X0,0)
& ! [X9: $int] :
( ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X1),t2tb(X9))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X9))) )
| ( ( $less(X9,$sum(0,X0))
| ~ $less(X9,X0) )
& ( ~ $less(X9,0)
| $less(X9,0) ) ) )
& ! [X8: $int] :
( ( tb2t6(nil(tuple2(key,a))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X8))) )
| $less(X8,0)
| ~ $less(X8,$sum(0,X0)) ) )
| $less(X0,$sum(0,X0))
| $less(0,0)
| $less(X0,0) )
& ( X6 = 0 ) )
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))
& $less(0,X0)
& ~ $less(X0,0)
& ! [X3: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3)
| ~ $less(X3,X0)
| $less(X3,0) ) ),
inference(ennf_transformation,[],[f165]) ).
tff(f185,plain,
? [X0: $int,X2: map_key_lpoption_a1rp,X1: map_int_lplist_lpkeycm_a1rprp] :
( ? [X6: $int] :
( ( ? [X7: map_int_lplist_lpkeycm_a1rprp] :
( ! [X8: $int] :
( ( tb2t6(nil(tuple2(key,a))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X8))) )
| $less(X8,0)
| ~ $less(X8,$sum(0,X0)) )
& ~ $less(X0,0)
& ? [X10: map_key_lpoption_a1rp] :
( ( ? [X12: a1,X11: key1] : ~ good_data1(a,X11,t2tb7(X12),t2tb3(X10),mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)))
| $less(X0,0)
| ( tb2t3(const(option(a),key,none(a))) != X10 )
| ? [X13: $int] :
( $less(X13,X0)
& ~ $less(X13,0)
& ~ good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X7)),X13) )
| ~ $less(0,X0) )
& ( tb2t3(const(option(a),key,none(a))) = X10 ) )
& ! [X9: $int] :
( ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X1),t2tb(X9))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X7),t2tb(X9))) )
| ( ( $less(X9,$sum(0,X0))
| ~ $less(X9,X0) )
& ( ~ $less(X9,0)
| $less(X9,0) ) ) ) )
| $less(X0,$sum(0,X0))
| $less(0,0)
| $less(X0,0) )
& ( X6 = 0 ) )
& ~ $less(X0,0)
& $less(0,X0)
& ! [X3: $int] :
( $less(X3,0)
| ~ $less(X3,X0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) )
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1))) ),
inference(flattening,[],[f184]) ).
tff(f186,plain,
! [X1: ty,X3: ty,X0: uni,X2: uni] :
( ( get(X3,X1,const(X3,X1,X0),X2) = X0 )
| ~ sort1(X3,X0) ),
inference(ennf_transformation,[],[f161]) ).
tff(f189,plain,
! [X0: uni,X2: $int,X1: ty] :
( ( elts(X1,mk_array1(X1,X2,X0)) = X0 )
| ~ sort1(map(int,X1),X0) ),
inference(ennf_transformation,[],[f167]) ).
tff(f203,plain,
! [X0: uni,X1: ty] :
( ( ~ mem(X1,X0,nil(X1))
& ! [X2: uni,X3: uni] :
( ( mem(X1,X0,cons(X1,X2,X3))
<=> ( ( X0 = X2 )
| mem(X1,X0,X3) ) )
| ~ sort1(X1,X2) ) )
| ~ sort1(X1,X0) ),
inference(ennf_transformation,[],[f155]) ).
tff(f209,plain,
! [X2: ty,X0: $int,X1: uni] :
( ( ~ good_hash1(X2,X1,X0)
| ! [X3: key1,X4: uni] :
( ~ mem(tuple2(key,X2),tuple21(key,X2,t2tb1(X3),X4),get2(list(tuple2(key,X2)),X1,X0))
| ( bucket1(X3,length1(list(tuple2(key,X2)),X1)) = X0 ) ) )
& ( good_hash1(X2,X1,X0)
| ? [X6: key1,X5: uni] :
( ( bucket1(X6,length1(list(tuple2(key,X2)),X1)) != X0 )
& mem(tuple2(key,X2),tuple21(key,X2,t2tb1(X6),X5),get2(list(tuple2(key,X2)),X1,X0))
& sort1(X2,X5) ) ) ),
inference(ennf_transformation,[],[f128]) ).
tff(f210,plain,
! [X2: ty,X1: uni,X0: $int] :
( ( ~ good_hash1(X2,X1,X0)
| ! [X3: key1,X4: uni] :
( ~ mem(tuple2(key,X2),tuple21(key,X2,t2tb1(X3),X4),get2(list(tuple2(key,X2)),X1,X0))
| ( bucket1(X3,length1(list(tuple2(key,X2)),X1)) = X0 ) ) )
& ( ? [X6: key1,X5: uni] :
( sort1(X2,X5)
& mem(tuple2(key,X2),tuple21(key,X2,t2tb1(X6),X5),get2(list(tuple2(key,X2)),X1,X0))
& ( bucket1(X6,length1(list(tuple2(key,X2)),X1)) != X0 ) )
| good_hash1(X2,X1,X0) ) ),
inference(flattening,[],[f209]) ).
tff(f217,plain,
! [X0: uni] :
( ( t2tb3(tb2t3(X0)) = X0 )
| ~ sort1(map(key,option(a)),X0) ),
inference(ennf_transformation,[],[f94]) ).
tff(f226,plain,
! [X0: $int] :
( ~ $less(0,X0)
| ! [X1: key1] :
( $less(bucket1(X1,X0),X0)
& ~ $less(bucket1(X1,X0),0) ) ),
inference(ennf_transformation,[],[f125]) ).
tff(f237,plain,
! [X0: $int,X1: ty,X2: uni] : ( length1(X1,mk_array1(X1,X0,X2)) = X0 ),
inference(rectify,[],[f133]) ).
tff(f241,plain,
! [X1: ty,X2: uni,X4: key1,X0: uni,X3: uni] :
( ( ( ( ( some(X1,X2) = get(option(X1),key,X3,t2tb1(X4)) )
| ~ in_data1(X1,X4,X2,X0) )
& ( in_data1(X1,X4,X2,X0)
| ( some(X1,X2) != get(option(X1),key,X3,t2tb1(X4)) ) ) )
| ~ good_data1(X1,X4,X2,X3,X0) )
& ( good_data1(X1,X4,X2,X3,X0)
| ( ( ~ in_data1(X1,X4,X2,X0)
| ( some(X1,X2) != get(option(X1),key,X3,t2tb1(X4)) ) )
& ( in_data1(X1,X4,X2,X0)
| ( some(X1,X2) = get(option(X1),key,X3,t2tb1(X4)) ) ) ) ) ),
inference(nnf_transformation,[],[f142]) ).
tff(f242,plain,
! [X0: ty,X1: uni,X2: key1,X3: uni,X4: uni] :
( ( ( ( ( some(X0,X1) = get(option(X0),key,X4,t2tb1(X2)) )
| ~ in_data1(X0,X2,X1,X3) )
& ( in_data1(X0,X2,X1,X3)
| ( some(X0,X1) != get(option(X0),key,X4,t2tb1(X2)) ) ) )
| ~ good_data1(X0,X2,X1,X4,X3) )
& ( good_data1(X0,X2,X1,X4,X3)
| ( ( ~ in_data1(X0,X2,X1,X3)
| ( some(X0,X1) != get(option(X0),key,X4,t2tb1(X2)) ) )
& ( in_data1(X0,X2,X1,X3)
| ( some(X0,X1) = get(option(X0),key,X4,t2tb1(X2)) ) ) ) ) ),
inference(rectify,[],[f241]) ).
tff(f246,plain,
! [X2: uni,X1: uni,X3: key1,X0: ty] :
( ( in_data1(X0,X3,X1,X2)
| ~ mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X1),get2(list(tuple2(key,X0)),X2,bucket1(X3,length1(list(tuple2(key,X0)),X2)))) )
& ( mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X1),get2(list(tuple2(key,X0)),X2,bucket1(X3,length1(list(tuple2(key,X0)),X2))))
| ~ in_data1(X0,X3,X1,X2) ) ),
inference(nnf_transformation,[],[f147]) ).
tff(f247,plain,
! [X0: uni,X1: uni,X2: key1,X3: ty] :
( ( in_data1(X3,X2,X1,X0)
| ~ mem(tuple2(key,X3),tuple21(key,X3,t2tb1(X2),X1),get2(list(tuple2(key,X3)),X0,bucket1(X2,length1(list(tuple2(key,X3)),X0)))) )
& ( mem(tuple2(key,X3),tuple21(key,X3,t2tb1(X2),X1),get2(list(tuple2(key,X3)),X0,bucket1(X2,length1(list(tuple2(key,X3)),X0))))
| ~ in_data1(X3,X2,X1,X0) ) ),
inference(rectify,[],[f246]) ).
tff(f254,plain,
! [X0: uni,X1: $int,X2: ty] :
( ( elts(X2,mk_array1(X2,X1,X0)) = X0 )
| ~ sort1(map(int,X2),X0) ),
inference(rectify,[],[f189]) ).
tff(f262,plain,
! [X0: ty,X1: uni,X2: $int] :
( ( ~ good_hash1(X0,X1,X2)
| ! [X3: key1,X4: uni] :
( ~ mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X4),get2(list(tuple2(key,X0)),X1,X2))
| ( bucket1(X3,length1(list(tuple2(key,X0)),X1)) = X2 ) ) )
& ( ? [X5: key1,X6: uni] :
( sort1(X0,X6)
& mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X5),X6),get2(list(tuple2(key,X0)),X1,X2))
& ( bucket1(X5,length1(list(tuple2(key,X0)),X1)) != X2 ) )
| good_hash1(X0,X1,X2) ) ),
inference(rectify,[],[f210]) ).
tff(f263,plain,
! [X0: ty,X1: uni,X2: $int] :
( ( ~ good_hash1(X0,X1,X2)
| ! [X3: key1,X4: uni] :
( ~ mem(tuple2(key,X0),tuple21(key,X0,t2tb1(X3),X4),get2(list(tuple2(key,X0)),X1,X2))
| ( bucket1(X3,length1(list(tuple2(key,X0)),X1)) = X2 ) ) )
& ( ( sort1(X0,sK1(X0,X1,X2))
& mem(tuple2(key,X0),tuple21(key,X0,t2tb1(sK0(X0,X1,X2)),sK1(X0,X1,X2)),get2(list(tuple2(key,X0)),X1,X2))
& ( bucket1(sK0(X0,X1,X2),length1(list(tuple2(key,X0)),X1)) != X2 ) )
| good_hash1(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X5,sK0(X0,X1,X2)),skolemize(X6,sK1(X0,X1,X2))],[f262]) ).
tff(f269,plain,
! [X0: ty,X1: uni,X2: ty] : sort1(map(X0,X2),const(X2,X0,X1)),
inference(rectify,[],[f162]) ).
tff(f272,plain,
! [X0: uni,X1: ty] :
( ( ~ mem(X1,X0,nil(X1))
& ! [X2: uni,X3: uni] :
( ( ( mem(X1,X0,cons(X1,X2,X3))
| ( ( X0 != X2 )
& ~ mem(X1,X0,X3) ) )
& ( ( X0 = X2 )
| mem(X1,X0,X3)
| ~ mem(X1,X0,cons(X1,X2,X3)) ) )
| ~ sort1(X1,X2) ) )
| ~ sort1(X1,X0) ),
inference(nnf_transformation,[],[f203]) ).
tff(f273,plain,
! [X0: uni,X1: ty] :
( ( ~ mem(X1,X0,nil(X1))
& ! [X2: uni,X3: uni] :
( ( ( mem(X1,X0,cons(X1,X2,X3))
| ( ( X0 != X2 )
& ~ mem(X1,X0,X3) ) )
& ( ( X0 = X2 )
| mem(X1,X0,X3)
| ~ mem(X1,X0,cons(X1,X2,X3)) ) )
| ~ sort1(X1,X2) ) )
| ~ sort1(X1,X0) ),
inference(flattening,[],[f272]) ).
tff(f276,plain,
? [X0: $int,X1: map_key_lpoption_a1rp,X2: map_int_lplist_lpkeycm_a1rprp] :
( ? [X3: $int] :
( ( ? [X4: map_int_lplist_lpkeycm_a1rprp] :
( ! [X5: $int] :
( ( tb2t6(nil(tuple2(key,a))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X4),t2tb(X5))) )
| $less(X5,0)
| ~ $less(X5,$sum(0,X0)) )
& ~ $less(X0,0)
& ? [X6: map_key_lpoption_a1rp] :
( ( ? [X7: a1,X8: key1] : ~ good_data1(a,X8,t2tb7(X7),t2tb3(X6),mk_array1(list(tuple2(key,a)),X0,t2tb2(X4)))
| $less(X0,0)
| ( tb2t3(const(option(a),key,none(a))) != X6 )
| ? [X9: $int] :
( $less(X9,X0)
& ~ $less(X9,0)
& ~ good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X4)),X9) )
| ~ $less(0,X0) )
& ( tb2t3(const(option(a),key,none(a))) = X6 ) )
& ! [X10: $int] :
( ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(X2),t2tb(X10))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(X4),t2tb(X10))) )
| ( ( $less(X10,$sum(0,X0))
| ~ $less(X10,X0) )
& ( ~ $less(X10,0)
| $less(X10,0) ) ) ) )
| $less(X0,$sum(0,X0))
| $less(0,0)
| $less(X0,0) )
& ( 0 = X3 ) )
& ~ $less(X0,0)
& $less(0,X0)
& ! [X11: $int] :
( $less(X11,0)
| ~ $less(X11,X0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X2)),X11) )
& ! [X12: a1,X13: key1] : good_data1(a,X13,t2tb7(X12),t2tb3(X1),mk_array1(list(tuple2(key,a)),X0,t2tb2(X2))) ),
inference(rectify,[],[f185]) ).
tff(f277,plain,
( ( ( ! [X5: $int] :
( ( tb2t6(nil(tuple2(key,a))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(sK6),t2tb(X5))) )
| $less(X5,0)
| ~ $less(X5,$sum(0,sK2)) )
& ~ $less(sK2,0)
& ( ~ good_data1(a,sK9,t2tb7(sK8),t2tb3(sK7),mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK6)))
| $less(sK2,0)
| ( tb2t3(const(option(a),key,none(a))) != sK7 )
| ( $less(sK10,sK2)
& ~ $less(sK10,0)
& ~ good_hash1(a,mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK6)),sK10) )
| ~ $less(0,sK2) )
& ( tb2t3(const(option(a),key,none(a))) = sK7 )
& ! [X10: $int] :
( ( tb2t6(get(list(tuple2(key,a)),int,t2tb2(sK4),t2tb(X10))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(sK6),t2tb(X10))) )
| ( ( $less(X10,$sum(0,sK2))
| ~ $less(X10,sK2) )
& ( ~ $less(X10,0)
| $less(X10,0) ) ) ) )
| $less(sK2,$sum(0,sK2))
| $less(0,0)
| $less(sK2,0) )
& ( 0 = sK5 )
& ~ $less(sK2,0)
& $less(0,sK2)
& ! [X11: $int] :
( $less(X11,0)
| ~ $less(X11,sK2)
| good_hash1(a,mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK4)),X11) )
& ! [X12: a1,X13: key1] : good_data1(a,X13,t2tb7(X12),t2tb3(sK3),mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK4))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X8,sK9),skolemize(X9,sK10)],[f276]) ).
tff(f280,plain,
! [X0: uni,X1: uni,X2: ty,X3: ty] : sort1(tuple2(X2,X3),tuple21(X2,X3,X1,X0)),
inference(rectify,[],[f174]) ).
tff(f285,plain,
! [X0: ty,X1: ty,X2: uni,X3: uni] :
( ( get(X1,X0,const(X1,X0,X2),X3) = X2 )
| ~ sort1(X1,X2) ),
inference(rectify,[],[f186]) ).
tff(f294,plain,
! [X0: $int,X1: key1] :
( ~ $less(0,X0)
| ~ $less(bucket1(X1,X0),0) ),
inference(cnf_transformation,[],[f226]) ).
tff(f295,plain,
! [X0: $int,X1: key1] :
( ~ $less(0,X0)
| $less(bucket1(X1,X0),X0) ),
inference(cnf_transformation,[],[f226]) ).
tff(f309,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f91]) ).
tff(f310,plain,
! [X2: uni,X0: $int,X1: ty] : ( length1(X1,mk_array1(X1,X0,X2)) = X0 ),
inference(cnf_transformation,[],[f237]) ).
tff(f316,plain,
! [X2: ty,X0: $int,X1: uni] : ( get(X2,int,elts(X2,X1),t2tb(X0)) = get2(X2,X1,X0) ),
inference(cnf_transformation,[],[f135]) ).
tff(f320,plain,
! [X2: key1,X3: uni,X0: ty,X1: uni,X4: uni] :
( ( some(X0,X1) = get(option(X0),key,X4,t2tb1(X2)) )
| good_data1(X0,X2,X1,X4,X3)
| in_data1(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f242]) ).
tff(f329,plain,
! [X0: map_int_lplist_lpkeycm_a1rprp] : sort1(map(int,list(tuple2(key,a))),t2tb2(X0)),
inference(cnf_transformation,[],[f89]) ).
tff(f331,plain,
! [X2: key1,X3: ty,X0: uni,X1: uni] :
( mem(tuple2(key,X3),tuple21(key,X3,t2tb1(X2),X1),get2(list(tuple2(key,X3)),X0,bucket1(X2,length1(list(tuple2(key,X3)),X0))))
| ~ in_data1(X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f247]) ).
tff(f345,plain,
! [X2: ty,X0: uni,X1: $int] :
( ( elts(X2,mk_array1(X2,X1,X0)) = X0 )
| ~ sort1(map(int,X2),X0) ),
inference(cnf_transformation,[],[f254]) ).
tff(f357,plain,
! [X2: $int,X0: ty,X1: uni] :
( mem(tuple2(key,X0),tuple21(key,X0,t2tb1(sK0(X0,X1,X2)),sK1(X0,X1,X2)),get2(list(tuple2(key,X0)),X1,X2))
| good_hash1(X0,X1,X2) ),
inference(cnf_transformation,[],[f263]) ).
tff(f362,plain,
! [X0: ty] : sort1(option(X0),none(X0)),
inference(cnf_transformation,[],[f26]) ).
tff(f368,plain,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
inference(cnf_transformation,[],[f103]) ).
tff(f373,plain,
! [X2: ty,X0: ty,X1: uni] : sort1(map(X0,X2),const(X2,X0,X1)),
inference(cnf_transformation,[],[f269]) ).
tff(f379,plain,
! [X0: uni] :
( ~ sort1(map(key,option(a)),X0)
| ( t2tb3(tb2t3(X0)) = X0 ) ),
inference(cnf_transformation,[],[f217]) ).
tff(f384,plain,
! [X0: uni,X1: ty] :
( ~ mem(X1,X0,nil(X1))
| ~ sort1(X1,X0) ),
inference(cnf_transformation,[],[f273]) ).
tff(f390,plain,
$less(0,sK2),
inference(cnf_transformation,[],[f277]) ).
tff(f391,plain,
~ $less(sK2,0),
inference(cnf_transformation,[],[f277]) ).
tff(f395,plain,
( ( tb2t3(const(option(a),key,none(a))) = sK7 )
| $less(sK2,$sum(0,sK2))
| $less(0,0)
| $less(sK2,0) ),
inference(cnf_transformation,[],[f277]) ).
tff(f396,plain,
( ~ good_data1(a,sK9,t2tb7(sK8),t2tb3(sK7),mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK6)))
| $less(sK2,0)
| ( tb2t3(const(option(a),key,none(a))) != sK7 )
| ~ good_hash1(a,mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK6)),sK10)
| ~ $less(0,sK2)
| $less(sK2,$sum(0,sK2))
| $less(0,0)
| $less(sK2,0) ),
inference(cnf_transformation,[],[f277]) ).
tff(f397,plain,
( ~ good_data1(a,sK9,t2tb7(sK8),t2tb3(sK7),mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK6)))
| $less(sK2,0)
| ( tb2t3(const(option(a),key,none(a))) != sK7 )
| ~ $less(sK10,0)
| ~ $less(0,sK2)
| $less(sK2,$sum(0,sK2))
| $less(0,0)
| $less(sK2,0) ),
inference(cnf_transformation,[],[f277]) ).
tff(f398,plain,
( ~ good_data1(a,sK9,t2tb7(sK8),t2tb3(sK7),mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK6)))
| $less(sK2,0)
| ( tb2t3(const(option(a),key,none(a))) != sK7 )
| $less(sK10,sK2)
| ~ $less(0,sK2)
| $less(sK2,$sum(0,sK2))
| $less(0,0)
| $less(sK2,0) ),
inference(cnf_transformation,[],[f277]) ).
tff(f400,plain,
! [X5: $int] :
( ( tb2t6(nil(tuple2(key,a))) = tb2t6(get(list(tuple2(key,a)),int,t2tb2(sK6),t2tb(X5))) )
| $less(X5,0)
| ~ $less(X5,$sum(0,sK2))
| $less(sK2,$sum(0,sK2))
| $less(0,0)
| $less(sK2,0) ),
inference(cnf_transformation,[],[f277]) ).
tff(f407,plain,
! [X0: ty,X1: uni] : ( none(X0) != some(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tff(f408,plain,
! [X2: ty,X3: ty,X0: uni,X1: uni] : sort1(tuple2(X2,X3),tuple21(X2,X3,X1,X0)),
inference(cnf_transformation,[],[f280]) ).
tff(f416,plain,
! [X2: uni,X3: uni,X0: ty,X1: ty] :
( ( get(X1,X0,const(X1,X0,X2),X3) = X2 )
| ~ sort1(X1,X2) ),
inference(cnf_transformation,[],[f285]) ).
tff(f427,definition,
sF11 = tuple2(key,a),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f428,plain,
tuple2(key,a) = sF11,
inference(reorient_equations,[],[f427]) ).
tff(f429,definition,
sF12 = nil(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f430,definition,
sF13 = tb2t6(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f431,plain,
tb2t6(sF12) = sF13,
inference(reorient_equations,[],[f430]) ).
tff(f432,definition,
sF14 = list(sF11),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f433,plain,
list(sF11) = sF14,
inference(reorient_equations,[],[f432]) ).
tff(f434,definition,
sF15 = t2tb2(sK6),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f435,plain,
t2tb2(sK6) = sF15,
inference(reorient_equations,[],[f434]) ).
tff(f436,definition,
sF16 = $sum(0,sK2),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f437,plain,
! [X5: $int] :
( ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| $less(X5,0)
| ~ $less(X5,sF16)
| $less(sK2,sF16)
| $less(0,0)
| $less(sK2,0) ),
inference(definition_folding,[],[f400,f436,f436,f435,f433,f428,f431,f429,f428]) ).
tff(f439,definition,
sF17 = t2tb7(sK8),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f440,plain,
t2tb7(sK8) = sF17,
inference(reorient_equations,[],[f439]) ).
tff(f441,definition,
sF18 = t2tb3(sK7),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f442,plain,
t2tb3(sK7) = sF18,
inference(reorient_equations,[],[f441]) ).
tff(f443,definition,
sF19 = mk_array1(sF14,sK2,sF15),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f444,definition,
sF20 = option(a),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f445,plain,
option(a) = sF20,
inference(reorient_equations,[],[f444]) ).
tff(f446,definition,
sF21 = none(a),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f447,plain,
none(a) = sF21,
inference(reorient_equations,[],[f446]) ).
tff(f448,definition,
sF22 = const(sF20,key,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f449,plain,
const(sF20,key,sF21) = sF22,
inference(reorient_equations,[],[f448]) ).
tff(f450,definition,
sF23 = tb2t3(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f451,plain,
( ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK2,0)
| ( sK7 != sF23 )
| $less(sK10,sK2)
| ~ $less(0,sK2)
| $less(sK2,sF16)
| $less(0,0)
| $less(sK2,0) ),
inference(definition_folding,[],[f398,f436,f450,f449,f447,f445,f443,f435,f433,f428,f442,f440]) ).
tff(f452,plain,
( ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK2,0)
| ( sK7 != sF23 )
| ~ $less(sK10,0)
| ~ $less(0,sK2)
| $less(sK2,sF16)
| $less(0,0)
| $less(sK2,0) ),
inference(definition_folding,[],[f397,f436,f450,f449,f447,f445,f443,f435,f433,f428,f442,f440]) ).
tff(f453,plain,
( ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK2,0)
| ( sK7 != sF23 )
| ~ good_hash1(a,sF19,sK10)
| ~ $less(0,sK2)
| $less(sK2,sF16)
| $less(0,0)
| $less(sK2,0) ),
inference(definition_folding,[],[f396,f436,f443,f435,f433,f428,f450,f449,f447,f445,f443,f435,f433,f428,f442,f440]) ).
tff(f454,plain,
( ( sK7 = sF23 )
| $less(sK2,sF16)
| $less(0,0)
| $less(sK2,0) ),
inference(definition_folding,[],[f395,f436,f450,f449,f447,f445]) ).
tff(f463,plain,
! [X2: $int,X1: $int] :
( ( sF16 != X1 )
| ( $sum(0,X2) = X1 )
| ( sK2 != X2 ) ),
inference(theory_flattening,[],[f436]) ).
tff(f464,plain,
! [X2: $int,X0: $int,X1: key1] :
( ( bucket1(X1,X0) != X2 )
| ~ $less(0,X0)
| $less(X2,X0) ),
inference(theory_flattening,[],[f295]) ).
tff(f465,plain,
! [X2: $int,X0: $int,X1: key1] :
( ( bucket1(X1,X0) != X2 )
| ~ $less(X2,0)
| ~ $less(0,X0) ),
inference(theory_flattening,[],[f294]) ).
tff(f480,plain,
! [X8: $int,X6: $int,X9: $int,X7: $int,X5: $int] :
( ~ $less(X5,X6)
| ( sF16 != X8 )
| ( sK2 != X7 )
| $less(X7,X8)
| $less(X5,0)
| ( sK2 != X9 )
| $less(X9,0)
| $less(0,0)
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| ( sF16 != X6 ) ),
inference(theory_flattening,[],[f437]) ).
tff(f482,plain,
! [X2: $int,X3: $int,X1: $int,X6: $int,X7: $int,X4: $int,X5: $int] :
( $less(X5,X6)
| ( sF16 != X6 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK2 != X3 )
| $less(X2,X3)
| $less(X7,0)
| $less(0,0)
| ( sK7 != sF23 )
| ( sK10 != X2 )
| $less(X1,0)
| ~ $less(0,X4)
| ( sK2 != X4 )
| ( sK2 != X5 )
| ( sK2 != X7 )
| ( sK2 != X1 ) ),
inference(theory_flattening,[],[f451]) ).
tff(f483,plain,
! [X2: $int,X3: $int,X1: $int,X6: $int,X4: $int,X5: $int] :
( ~ $less(X2,0)
| ( sK2 != X6 )
| $less(X4,X5)
| ( sF16 != X5 )
| ( sK2 != X3 )
| ( sK10 != X2 )
| $less(0,0)
| ( sK2 != X1 )
| $less(X1,0)
| $less(X6,0)
| ( sK2 != X4 )
| ~ $less(0,X3)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK7 != sF23 ) ),
inference(theory_flattening,[],[f452]) ).
tff(f484,plain,
! [X2: $int,X3: $int,X1: $int,X4: $int,X5: $int] :
( ( sK2 != X5 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(X5,0)
| ~ $less(0,X2)
| $less(X3,X4)
| ( sK2 != X3 )
| $less(0,0)
| ( sF16 != X4 )
| ( sK2 != X1 )
| ( sK7 != sF23 )
| $less(X1,0)
| ~ good_hash1(a,sF19,sK10)
| ( sK2 != X2 ) ),
inference(theory_flattening,[],[f453]) ).
tff(f485,plain,
! [X2: $int,X3: $int,X1: $int] :
( $less(X1,X2)
| ( sK7 = sF23 )
| ( sF16 != X2 )
| ( sK2 != X3 )
| ( sK2 != X1 )
| $less(0,0)
| $less(X3,0) ),
inference(theory_flattening,[],[f454]) ).
tff(f488,plain,
! [X1: $int] :
( ~ $less(X1,0)
| ( sK2 != X1 ) ),
inference(theory_flattening,[],[f391]) ).
tff(f489,plain,
! [X1: $int] :
( ( sK2 != X1 )
| $less(0,X1) ),
inference(theory_flattening,[],[f390]) ).
tff(f496,plain,
~ $less(sK2,0),
inference(gaussian_variable_elimination,[],[f488]) ).
tff(f497,plain,
! [X0: $int,X1: key1] :
( ~ $less(bucket1(X1,X0),0)
| ~ $less(0,X0) ),
inference(gaussian_variable_elimination,[],[f465]) ).
tff(f499,plain,
! [X2: $int,X1: $int] :
( ( sK2 != X2 )
| ( X1 = X2 )
| ( sF16 != X1 ) ),
inference(evaluation,[],[f463]) ).
tff(f500,plain,
! [X1: $int] :
( ( sK2 = X1 )
| ( sF16 != X1 ) ),
inference(gaussian_variable_elimination,[],[f499]) ).
tff(f501,plain,
sF16 = sK2,
inference(gaussian_variable_elimination,[],[f500]) ).
tff(f505,plain,
$less(0,sK2),
inference(gaussian_variable_elimination,[],[f489]) ).
tff(f511,plain,
! [X8: $int,X6: $int,X9: $int,X7: $int,X5: $int] :
( $less(X7,X8)
| ( sF16 != X6 )
| $less(X9,0)
| $less(X5,0)
| ( sK2 != X9 )
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| ~ $less(X5,X6)
| ( sK2 != X7 )
| ( sF16 != X8 ) ),
inference(evaluation,[],[f480]) ).
tff(f512,plain,
! [X8: $int,X9: $int,X7: $int,X5: $int] :
( $less(X7,X8)
| $less(X5,0)
| $less(X9,0)
| ( sF16 != X8 )
| ( sK2 != X9 )
| ~ $less(X5,sF16)
| ( sK2 != X7 )
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 ) ),
inference(gaussian_variable_elimination,[],[f511]) ).
tff(f513,plain,
! [X9: $int,X7: $int,X5: $int] :
( $less(X7,sF16)
| ~ $less(X5,sF16)
| $less(X9,0)
| ( sK2 != X9 )
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| ( sK2 != X7 )
| $less(X5,0) ),
inference(gaussian_variable_elimination,[],[f512]) ).
tff(f514,plain,
! [X7: $int,X5: $int] :
( $less(X7,sF16)
| $less(X5,0)
| $less(sK2,0)
| ~ $less(X5,sF16)
| ( sK2 != X7 )
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 ) ),
inference(gaussian_variable_elimination,[],[f513]) ).
tff(f515,plain,
! [X5: $int] :
( $less(sK2,sF16)
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| ~ $less(X5,sF16)
| $less(sK2,0)
| $less(X5,0) ),
inference(gaussian_variable_elimination,[],[f514]) ).
tff(f524,plain,
! [X2: $int,X3: $int,X1: $int] :
( ( sK7 = sF23 )
| $less(X3,0)
| ( sK2 != X1 )
| ( sK2 != X3 )
| ( sF16 != X2 )
| $less(X1,X2) ),
inference(evaluation,[],[f485]) ).
tff(f525,plain,
! [X2: $int,X3: $int] :
( $less(sK2,X2)
| ( sK7 = sF23 )
| ( sK2 != X3 )
| ( sF16 != X2 )
| $less(X3,0) ),
inference(gaussian_variable_elimination,[],[f524]) ).
tff(f526,plain,
! [X2: $int] :
( ( sF16 != X2 )
| ( sK7 = sF23 )
| $less(sK2,X2)
| $less(sK2,0) ),
inference(gaussian_variable_elimination,[],[f525]) ).
tff(f527,plain,
( $less(sK2,sF16)
| ( sK7 = sF23 )
| $less(sK2,0) ),
inference(gaussian_variable_elimination,[],[f526]) ).
tff(f530,plain,
! [X2: $int,X3: $int,X1: $int,X6: $int,X4: $int,X5: $int] :
( $less(X4,X5)
| ( sK2 != X6 )
| $less(X6,0)
| ( sF16 != X5 )
| ( sK2 != X1 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK2 != X4 )
| ~ $less(0,X3)
| ( sK2 != X3 )
| $less(X1,0)
| ( sK7 != sF23 )
| ( sK10 != X2 )
| ~ $less(X2,0) ),
inference(evaluation,[],[f483]) ).
tff(f531,plain,
! [X2: $int,X3: $int,X1: $int,X4: $int,X5: $int] :
( ~ $less(0,X3)
| ( sK2 != X1 )
| ~ $less(X2,0)
| $less(X4,X5)
| $less(sK2,0)
| ( sF16 != X5 )
| $less(X1,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK7 != sF23 )
| ( sK10 != X2 )
| ( sK2 != X4 )
| ( sK2 != X3 ) ),
inference(gaussian_variable_elimination,[],[f530]) ).
tff(f532,plain,
! [X2: $int,X3: $int,X4: $int,X5: $int] :
( ( sK2 != X3 )
| $less(sK2,0)
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK2 != X4 )
| ~ $less(X2,0)
| ( sK10 != X2 )
| ( sF16 != X5 )
| ( sK7 != sF23 )
| ~ $less(0,X3)
| $less(X4,X5) ),
inference(gaussian_variable_elimination,[],[f531]) ).
tff(f533,plain,
! [X2: $int,X3: $int,X4: $int,X5: $int] :
( ( sK7 != sF23 )
| ( sF16 != X5 )
| $less(sK2,0)
| ( sK10 != X2 )
| $less(X4,X5)
| ( sK2 != X3 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ~ $less(X2,0)
| ( sK2 != X4 )
| ~ $less(0,X3) ),
inference(duplicate_literal_removal,[],[f532]) ).
tff(f534,plain,
! [X2: $int,X3: $int,X4: $int] :
( ( sK7 != sF23 )
| ~ $less(X2,0)
| ( sK2 != X3 )
| ~ $less(0,X3)
| ( sK2 != X4 )
| $less(X4,sF16)
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK10 != X2 ) ),
inference(gaussian_variable_elimination,[],[f533]) ).
tff(f535,plain,
! [X2: $int,X4: $int] :
( ( sK7 != sF23 )
| ( sK10 != X2 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK2 != X4 )
| $less(X4,sF16)
| ~ $less(X2,0)
| ~ $less(0,sK2)
| $less(sK2,0) ),
inference(gaussian_variable_elimination,[],[f534]) ).
tff(f536,plain,
! [X4: $int] :
( ( sK7 != sF23 )
| $less(sK2,0)
| ~ $less(sK10,0)
| ( sK2 != X4 )
| ~ $less(0,sK2)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(X4,sF16) ),
inference(gaussian_variable_elimination,[],[f535]) ).
tff(f537,plain,
( ~ $less(sK10,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK2,0)
| ~ $less(0,sK2)
| ( sK7 != sF23 )
| $less(sK2,sF16) ),
inference(gaussian_variable_elimination,[],[f536]) ).
tff(f543,plain,
! [X2: $int,X3: $int,X1: $int,X4: $int,X5: $int] :
( ( sK2 != X2 )
| ( sK2 != X5 )
| ( sF16 != X4 )
| $less(X1,0)
| ( sK7 != sF23 )
| ( sK2 != X3 )
| $less(X3,X4)
| ~ good_hash1(a,sF19,sK10)
| ( sK2 != X1 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ~ $less(0,X2)
| $less(X5,0) ),
inference(evaluation,[],[f484]) ).
tff(f544,plain,
! [X3: $int,X1: $int,X4: $int,X5: $int] :
( ( sK2 != X5 )
| ( sK2 != X1 )
| $less(X3,X4)
| $less(X1,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(X5,0)
| ~ good_hash1(a,sF19,sK10)
| ~ $less(0,sK2)
| ( sF16 != X4 )
| ( sK2 != X3 )
| ( sK7 != sF23 ) ),
inference(gaussian_variable_elimination,[],[f543]) ).
tff(f545,plain,
! [X3: $int,X1: $int,X4: $int] :
( ( sF16 != X4 )
| ( sK2 != X3 )
| ~ good_hash1(a,sF19,sK10)
| $less(X1,0)
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ~ $less(0,sK2)
| ( sK7 != sF23 )
| ( sK2 != X1 )
| $less(X3,X4) ),
inference(gaussian_variable_elimination,[],[f544]) ).
tff(f546,plain,
! [X3: $int,X1: $int] :
( $less(X3,sF16)
| ~ good_hash1(a,sF19,sK10)
| ( sK2 != X3 )
| ~ $less(0,sK2)
| ( sK7 != sF23 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(X1,0)
| ( sK2 != X1 )
| $less(sK2,0) ),
inference(gaussian_variable_elimination,[],[f545]) ).
tff(f547,plain,
! [X1: $int] :
( ~ good_hash1(a,sF19,sK10)
| ~ $less(0,sK2)
| $less(sK2,0)
| ( sK7 != sF23 )
| $less(X1,0)
| $less(sK2,sF16)
| ( sK2 != X1 )
| ~ good_data1(a,sK9,sF17,sF18,sF19) ),
inference(gaussian_variable_elimination,[],[f546]) ).
tff(f548,plain,
( $less(sK2,0)
| ~ good_hash1(a,sF19,sK10)
| ~ $less(0,sK2)
| ( sK7 != sF23 )
| $less(sK2,sF16)
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19) ),
inference(gaussian_variable_elimination,[],[f547]) ).
tff(f549,plain,
( ~ good_hash1(a,sF19,sK10)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK2,0)
| $less(sK2,sF16)
| ~ $less(0,sK2)
| ( sK7 != sF23 ) ),
inference(duplicate_literal_removal,[],[f548]) ).
tff(f550,plain,
! [X2: $int,X3: $int,X1: $int,X6: $int,X7: $int,X4: $int,X5: $int] :
( ( sK7 != sF23 )
| $less(X2,X3)
| ( sK2 != X5 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(X7,0)
| ~ $less(0,X4)
| $less(X1,0)
| ( sK10 != X2 )
| ( sK2 != X3 )
| ( sK2 != X4 )
| ( sF16 != X6 )
| ( sK2 != X1 )
| ( sK2 != X7 )
| $less(X5,X6) ),
inference(evaluation,[],[f482]) ).
tff(f551,plain,
! [X2: $int,X3: $int,X1: $int,X6: $int,X7: $int,X4: $int] :
( ( sK2 != X7 )
| $less(X1,0)
| ( sK2 != X3 )
| ( sK2 != X4 )
| $less(X2,X3)
| $less(X7,0)
| $less(sK2,X6)
| ( sK7 != sF23 )
| ~ $less(0,X4)
| ( sF16 != X6 )
| ( sK10 != X2 )
| ( sK2 != X1 )
| ~ good_data1(a,sK9,sF17,sF18,sF19) ),
inference(gaussian_variable_elimination,[],[f550]) ).
tff(f552,plain,
! [X2: $int,X3: $int,X1: $int,X6: $int,X4: $int] :
( $less(sK2,X6)
| $less(X2,X3)
| ~ $less(0,X4)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK10 != X2 )
| ( sK2 != X4 )
| ( sK7 != sF23 )
| ( sK2 != X3 )
| $less(X1,0)
| ( sF16 != X6 )
| $less(sK2,0)
| ( sK2 != X1 ) ),
inference(gaussian_variable_elimination,[],[f551]) ).
tff(f553,plain,
! [X3: $int,X1: $int,X6: $int,X4: $int] :
( ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK2 != X3 )
| ( sF16 != X6 )
| ( sK7 != sF23 )
| $less(X1,0)
| ( sK2 != X4 )
| $less(sK2,0)
| ( sK2 != X1 )
| $less(sK10,X3)
| ~ $less(0,X4)
| $less(sK2,X6) ),
inference(gaussian_variable_elimination,[],[f552]) ).
tff(f554,plain,
! [X1: $int,X6: $int,X4: $int] :
( ( sF16 != X6 )
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK2 != X1 )
| ( sK2 != X4 )
| ( sK7 != sF23 )
| $less(sK10,sK2)
| $less(X1,0)
| $less(sK2,X6)
| ~ $less(0,X4)
| $less(sK2,0) ),
inference(gaussian_variable_elimination,[],[f553]) ).
tff(f555,plain,
! [X1: $int,X4: $int] :
( ( sK2 != X1 )
| ( sK7 != sF23 )
| ( sK2 != X4 )
| $less(X1,0)
| $less(sK2,sF16)
| ~ $less(0,X4)
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK10,sK2) ),
inference(gaussian_variable_elimination,[],[f554]) ).
tff(f556,plain,
! [X4: $int] :
( $less(sK2,sF16)
| $less(sK2,0)
| ( sK7 != sF23 )
| ( sK2 != X4 )
| $less(sK2,0)
| $less(sK10,sK2)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ~ $less(0,X4) ),
inference(gaussian_variable_elimination,[],[f555]) ).
tff(f557,plain,
! [X4: $int] :
( ( sK2 != X4 )
| $less(sK10,sK2)
| ( sK7 != sF23 )
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| $less(sK2,sF16)
| ~ $less(0,X4) ),
inference(duplicate_literal_removal,[],[f556]) ).
tff(f558,plain,
( $less(sK2,sF16)
| ~ $less(0,sK2)
| $less(sK2,0)
| ~ good_data1(a,sK9,sF17,sF18,sF19)
| ( sK7 != sF23 )
| $less(sK10,sK2) ),
inference(gaussian_variable_elimination,[],[f557]) ).
tff(f572,plain,
! [X0: $int,X1: key1] :
( $less(bucket1(X1,X0),X0)
| ~ $less(0,X0) ),
inference(gaussian_variable_elimination,[],[f464]) ).
tff(f575,definition,
( spl27_1
<=> $less(sK2,0) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
tff(f578,plain,
~ spl27_1,
inference(avatar_split_clause,[],[f496,f575]) ).
tff(f585,definition,
( spl27_3
<=> ( const(sF20,key,sF21) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition]) ).
tff(f587,plain,
( ( const(sF20,key,sF21) = sF22 )
| ~ spl27_3 ),
inference(avatar_component_clause,[],[f585]) ).
tff(f588,plain,
spl27_3,
inference(avatar_split_clause,[],[f449,f585]) ).
tff(f590,definition,
( spl27_4
<=> ( none(a) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
tff(f592,plain,
( ( none(a) = sF21 )
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f590]) ).
tff(f593,plain,
spl27_4,
inference(avatar_split_clause,[],[f447,f590]) ).
tff(f595,definition,
( spl27_5
<=> ( sF16 = sK2 ) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
tff(f597,plain,
( ( sF16 = sK2 )
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f595]) ).
tff(f598,plain,
spl27_5,
inference(avatar_split_clause,[],[f501,f595]) ).
tff(f605,definition,
( spl27_7
<=> $less(0,sK2) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
tff(f607,plain,
( $less(0,sK2)
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f605]) ).
tff(f608,plain,
spl27_7,
inference(avatar_split_clause,[],[f505,f605]) ).
tff(f610,definition,
( spl27_8
<=> $less(sK2,sF16) ),
introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition]) ).
tff(f614,definition,
( spl27_9
<=> ! [X5: $int] :
( ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| $less(X5,0)
| ~ $less(X5,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
tff(f615,plain,
( ! [X5: $int] :
( $less(X5,0)
| ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| ~ $less(X5,sF16) )
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f614]) ).
tff(f616,plain,
( spl27_8
| spl27_9
| spl27_1 ),
inference(avatar_split_clause,[],[f515,f575,f614,f610]) ).
tff(f618,definition,
( spl27_10
<=> ( tuple2(key,a) = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
tff(f620,plain,
( ( tuple2(key,a) = sF11 )
| ~ spl27_10 ),
inference(avatar_component_clause,[],[f618]) ).
tff(f621,plain,
spl27_10,
inference(avatar_split_clause,[],[f428,f618]) ).
tff(f623,definition,
( spl27_11
<=> ( sF19 = mk_array1(sF14,sK2,sF15) ) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
tff(f625,plain,
( ( sF19 = mk_array1(sF14,sK2,sF15) )
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f623]) ).
tff(f626,plain,
spl27_11,
inference(avatar_split_clause,[],[f443,f623]) ).
tff(f633,definition,
( spl27_13
<=> ( sK7 = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition]) ).
tff(f635,plain,
( ( sK7 = sF23 )
| ~ spl27_13 ),
inference(avatar_component_clause,[],[f633]) ).
tff(f636,plain,
( spl27_13
| spl27_8
| spl27_1 ),
inference(avatar_split_clause,[],[f527,f575,f610,f633]) ).
tff(f638,definition,
( spl27_14
<=> good_data1(a,sK9,sF17,sF18,sF19) ),
introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition]) ).
tff(f640,plain,
( ~ good_data1(a,sK9,sF17,sF18,sF19)
| spl27_14 ),
inference(avatar_component_clause,[],[f638]) ).
tff(f642,definition,
( spl27_15
<=> $less(sK10,0) ),
introduced(definition,[new_symbols(definition,[spl27_15])],[avatar_definition]) ).
tff(f644,plain,
( ~ $less(sK10,0)
| spl27_15 ),
inference(avatar_component_clause,[],[f642]) ).
tff(f645,plain,
( spl27_8
| spl27_1
| ~ spl27_13
| ~ spl27_14
| ~ spl27_15
| ~ spl27_7 ),
inference(avatar_split_clause,[],[f537,f605,f642,f638,f633,f575,f610]) ).
tff(f652,definition,
( spl27_17
<=> good_hash1(a,sF19,sK10) ),
introduced(definition,[new_symbols(definition,[spl27_17])],[avatar_definition]) ).
tff(f654,plain,
( ~ good_hash1(a,sF19,sK10)
| spl27_17 ),
inference(avatar_component_clause,[],[f652]) ).
tff(f655,plain,
( ~ spl27_17
| ~ spl27_14
| spl27_1
| ~ spl27_7
| spl27_8
| ~ spl27_13 ),
inference(avatar_split_clause,[],[f549,f633,f610,f605,f575,f638,f652]) ).
tff(f657,definition,
( spl27_18
<=> $less(sK10,sK2) ),
introduced(definition,[new_symbols(definition,[spl27_18])],[avatar_definition]) ).
tff(f659,plain,
( $less(sK10,sK2)
| ~ spl27_18 ),
inference(avatar_component_clause,[],[f657]) ).
tff(f660,plain,
( ~ spl27_7
| spl27_18
| ~ spl27_13
| ~ spl27_14
| spl27_8
| spl27_1 ),
inference(avatar_split_clause,[],[f558,f575,f610,f638,f633,f657,f605]) ).
tff(f671,definition,
( spl27_21
<=> ( option(a) = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl27_21])],[avatar_definition]) ).
tff(f673,plain,
( ( option(a) = sF20 )
| ~ spl27_21 ),
inference(avatar_component_clause,[],[f671]) ).
tff(f674,plain,
spl27_21,
inference(avatar_split_clause,[],[f445,f671]) ).
tff(f681,definition,
( spl27_23
<=> ( list(sF11) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl27_23])],[avatar_definition]) ).
tff(f683,plain,
( ( list(sF11) = sF14 )
| ~ spl27_23 ),
inference(avatar_component_clause,[],[f681]) ).
tff(f684,plain,
spl27_23,
inference(avatar_split_clause,[],[f433,f681]) ).
tff(f686,definition,
( spl27_24
<=> ( sF12 = nil(sF11) ) ),
introduced(definition,[new_symbols(definition,[spl27_24])],[avatar_definition]) ).
tff(f688,plain,
( ( sF12 = nil(sF11) )
| ~ spl27_24 ),
inference(avatar_component_clause,[],[f686]) ).
tff(f689,plain,
spl27_24,
inference(avatar_split_clause,[],[f429,f686]) ).
tff(f691,definition,
( spl27_25
<=> ( sF23 = tb2t3(sF22) ) ),
introduced(definition,[new_symbols(definition,[spl27_25])],[avatar_definition]) ).
tff(f693,plain,
( ( sF23 = tb2t3(sF22) )
| ~ spl27_25 ),
inference(avatar_component_clause,[],[f691]) ).
tff(f694,plain,
spl27_25,
inference(avatar_split_clause,[],[f450,f691]) ).
tff(f696,definition,
( spl27_26
<=> ( tb2t6(sF12) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl27_26])],[avatar_definition]) ).
tff(f698,plain,
( ( tb2t6(sF12) = sF13 )
| ~ spl27_26 ),
inference(avatar_component_clause,[],[f696]) ).
tff(f699,plain,
spl27_26,
inference(avatar_split_clause,[],[f431,f696]) ).
tff(f701,definition,
( spl27_27
<=> ( t2tb3(sK7) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl27_27])],[avatar_definition]) ).
tff(f703,plain,
( ( t2tb3(sK7) = sF18 )
| ~ spl27_27 ),
inference(avatar_component_clause,[],[f701]) ).
tff(f704,plain,
spl27_27,
inference(avatar_split_clause,[],[f442,f701]) ).
tff(f706,plain,
( ! [X5: $int] :
( ( tb2t6(get(sF14,int,sF15,t2tb(X5))) = sF13 )
| ~ $less(X5,sK2)
| $less(X5,0) )
| ~ spl27_5
| ~ spl27_9 ),
inference(forward_demodulation,[],[f615,f597]) ).
tff(f717,plain,
( ( t2tb3(sF23) = sF18 )
| ~ spl27_13
| ~ spl27_27 ),
inference(superposition,[],[f703,f635]) ).
tff(f719,definition,
( spl27_29
<=> ( t2tb3(sF23) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl27_29])],[avatar_definition]) ).
tff(f721,plain,
( ( t2tb3(sF23) = sF18 )
| ~ spl27_29 ),
inference(avatar_component_clause,[],[f719]) ).
tff(f722,plain,
( spl27_29
| ~ spl27_13
| ~ spl27_27 ),
inference(avatar_split_clause,[],[f717,f701,f633,f719]) ).
tff(f754,plain,
( sort1(sF20,none(a))
| ~ spl27_21 ),
inference(superposition,[],[f362,f673]) ).
tff(f756,plain,
( sort1(sF20,sF21)
| ~ spl27_4
| ~ spl27_21 ),
inference(forward_demodulation,[],[f754,f592]) ).
tff(f759,definition,
( spl27_34
<=> sort1(sF20,sF21) ),
introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition]) ).
tff(f761,plain,
( sort1(sF20,sF21)
| ~ spl27_34 ),
inference(avatar_component_clause,[],[f759]) ).
tff(f762,plain,
( spl27_34
| ~ spl27_4
| ~ spl27_21 ),
inference(avatar_split_clause,[],[f756,f671,f590,f759]) ).
tff(f763,plain,
( ! [X0: $int] :
( ( t2tb6(sF13) = get(sF14,int,sF15,t2tb(X0)) )
| ~ $less(X0,sK2)
| $less(X0,0) )
| ~ spl27_5
| ~ spl27_9 ),
inference(superposition,[],[f368,f706]) ).
tff(f765,plain,
( ( sF12 = t2tb6(sF13) )
| ~ spl27_26 ),
inference(superposition,[],[f368,f698]) ).
tff(f767,definition,
( spl27_35
<=> ( sF12 = t2tb6(sF13) ) ),
introduced(definition,[new_symbols(definition,[spl27_35])],[avatar_definition]) ).
tff(f769,plain,
( ( sF12 = t2tb6(sF13) )
| ~ spl27_35 ),
inference(avatar_component_clause,[],[f767]) ).
tff(f770,plain,
( spl27_35
| ~ spl27_26 ),
inference(avatar_split_clause,[],[f765,f696,f767]) ).
tff(f797,plain,
( ! [X0: uni] : ( sF21 != some(a,X0) )
| ~ spl27_4 ),
inference(superposition,[],[f407,f592]) ).
tff(f851,plain,
( ( length1(sF14,sF19) = sK2 )
| ~ spl27_11 ),
inference(superposition,[],[f310,f625]) ).
tff(f853,definition,
( spl27_42
<=> ( length1(sF14,sF19) = sK2 ) ),
introduced(definition,[new_symbols(definition,[spl27_42])],[avatar_definition]) ).
tff(f855,plain,
( ( length1(sF14,sF19) = sK2 )
| ~ spl27_42 ),
inference(avatar_component_clause,[],[f853]) ).
tff(f856,plain,
( spl27_42
| ~ spl27_11 ),
inference(avatar_split_clause,[],[f851,f623,f853]) ).
tff(f875,plain,
( sort1(map(key,sF20),sF22)
| ~ spl27_3 ),
inference(superposition,[],[f373,f587]) ).
tff(f877,definition,
( spl27_44
<=> sort1(map(key,sF20),sF22) ),
introduced(definition,[new_symbols(definition,[spl27_44])],[avatar_definition]) ).
tff(f879,plain,
( sort1(map(key,sF20),sF22)
| ~ spl27_44 ),
inference(avatar_component_clause,[],[f877]) ).
tff(f880,plain,
( spl27_44
| ~ spl27_3 ),
inference(avatar_split_clause,[],[f875,f585,f877]) ).
tff(f884,plain,
( ! [X0: uni] :
( ~ mem(sF11,X0,sF12)
| ~ sort1(sF11,X0) )
| ~ spl27_24 ),
inference(superposition,[],[f384,f688]) ).
tff(f897,plain,
! [X0: uni] : sort1(map(int,list(tuple2(key,a))),X0),
inference(superposition,[],[f329,f309]) ).
tff(f901,plain,
( ! [X0: uni] : sort1(map(int,list(sF11)),X0)
| ~ spl27_10 ),
inference(forward_demodulation,[],[f897,f620]) ).
tff(f904,plain,
( ! [X0: uni] : sort1(map(int,sF14),X0)
| ~ spl27_10
| ~ spl27_23 ),
inference(forward_demodulation,[],[f901,f683]) ).
tff(f923,plain,
( ! [X0: uni,X1: uni] : sort1(sF11,tuple21(key,a,X0,X1))
| ~ spl27_10 ),
inference(superposition,[],[f408,f620]) ).
tff(f1021,plain,
( ! [X0: uni] :
( ~ sort1(map(key,sF20),X0)
| ( t2tb3(tb2t3(X0)) = X0 ) )
| ~ spl27_21 ),
inference(superposition,[],[f379,f673]) ).
tff(f1125,plain,
( ( t2tb3(tb2t3(sF22)) = sF22 )
| ~ spl27_21
| ~ spl27_44 ),
inference(resolution,[],[f1021,f879]) ).
tff(f1140,plain,
( ( t2tb3(sF23) = sF22 )
| ~ spl27_21
| ~ spl27_25
| ~ spl27_44 ),
inference(forward_demodulation,[],[f1125,f693]) ).
tff(f1142,definition,
( spl27_52
<=> ( t2tb3(sF23) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl27_52])],[avatar_definition]) ).
tff(f1144,plain,
( ( t2tb3(sF23) = sF22 )
| ~ spl27_52 ),
inference(avatar_component_clause,[],[f1142]) ).
tff(f1145,plain,
( spl27_52
| ~ spl27_21
| ~ spl27_25
| ~ spl27_44 ),
inference(avatar_split_clause,[],[f1140,f877,f691,f671,f1142]) ).
tff(f1147,plain,
( ( sF15 = elts(sF14,sF19) )
| ~ sort1(map(int,sF14),sF15)
| ~ spl27_11 ),
inference(superposition,[],[f345,f625]) ).
tff(f1152,plain,
( ( sF15 = elts(sF14,sF19) )
| ~ spl27_10
| ~ spl27_11
| ~ spl27_23 ),
inference(forward_subsumption_resolution,[],[f1147,f904]) ).
tff(f1156,definition,
( spl27_53
<=> ( sF15 = elts(sF14,sF19) ) ),
introduced(definition,[new_symbols(definition,[spl27_53])],[avatar_definition]) ).
tff(f1158,plain,
( ( sF15 = elts(sF14,sF19) )
| ~ spl27_53 ),
inference(avatar_component_clause,[],[f1156]) ).
tff(f1159,plain,
( spl27_53
| ~ spl27_10
| ~ spl27_11
| ~ spl27_23 ),
inference(avatar_split_clause,[],[f1152,f681,f623,f618,f1156]) ).
tff(f1166,plain,
( ( sF22 = sF18 )
| ~ spl27_29
| ~ spl27_52 ),
inference(superposition,[],[f721,f1144]) ).
tff(f1171,definition,
( spl27_55
<=> ( sF22 = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl27_55])],[avatar_definition]) ).
tff(f1173,plain,
( ( sF22 = sF18 )
| ~ spl27_55 ),
inference(avatar_component_clause,[],[f1171]) ).
tff(f1174,plain,
( spl27_55
| ~ spl27_29
| ~ spl27_52 ),
inference(avatar_split_clause,[],[f1166,f1142,f719,f1171]) ).
tff(f1179,plain,
( ~ good_data1(a,sK9,sF17,sF22,sF19)
| spl27_14
| ~ spl27_55 ),
inference(superposition,[],[f640,f1173]) ).
tff(f1181,definition,
( spl27_56
<=> good_data1(a,sK9,sF17,sF22,sF19) ),
introduced(definition,[new_symbols(definition,[spl27_56])],[avatar_definition]) ).
tff(f1183,plain,
( ~ good_data1(a,sK9,sF17,sF22,sF19)
| spl27_56 ),
inference(avatar_component_clause,[],[f1181]) ).
tff(f1184,plain,
( ~ spl27_56
| spl27_14
| ~ spl27_55 ),
inference(avatar_split_clause,[],[f1179,f1171,f638,f1181]) ).
tff(f1191,plain,
( ! [X0: uni] :
( ~ sort1(sF20,sF21)
| ( get(sF20,key,sF22,X0) = sF21 ) )
| ~ spl27_3 ),
inference(superposition,[],[f416,f587]) ).
tff(f1193,plain,
( ! [X0: uni] : ( get(sF20,key,sF22,X0) = sF21 )
| ~ spl27_3
| ~ spl27_34 ),
inference(forward_subsumption_resolution,[],[f1191,f761]) ).
tff(f1195,plain,
( ! [X0: $int] : ( get2(sF14,sF19,X0) = get(sF14,int,sF15,t2tb(X0)) )
| ~ spl27_53 ),
inference(superposition,[],[f316,f1158]) ).
tff(f1341,plain,
( ! [X2: key1,X3: uni,X0: uni,X1: uni] :
( ( some(a,X0) = get(sF20,key,X1,t2tb1(X2)) )
| good_data1(a,X2,X0,X1,X3)
| in_data1(a,X2,X0,X3) )
| ~ spl27_21 ),
inference(superposition,[],[f320,f673]) ).
tff(f1475,plain,
( ! [X0: $int] :
( $less(X0,0)
| ( get2(sF14,sF19,X0) = t2tb6(sF13) )
| ~ $less(X0,sK2) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_53 ),
inference(superposition,[],[f1195,f763]) ).
tff(f1483,plain,
( ! [X0: $int] :
( ( sF12 = get2(sF14,sF19,X0) )
| $less(X0,0)
| ~ $less(X0,sK2) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_35
| ~ spl27_53 ),
inference(forward_demodulation,[],[f1475,f769]) ).
tff(f1492,plain,
( ! [X0: uni,X1: $int] :
( good_hash1(a,X0,X1)
| mem(sF11,tuple21(key,a,t2tb1(sK0(a,X0,X1)),sK1(a,X0,X1)),get2(list(sF11),X0,X1)) )
| ~ spl27_10 ),
inference(superposition,[],[f357,f620]) ).
tff(f1493,plain,
( ! [X0: uni,X1: $int] :
( mem(sF11,tuple21(key,a,t2tb1(sK0(a,X0,X1)),sK1(a,X0,X1)),get2(sF14,X0,X1))
| good_hash1(a,X0,X1) )
| ~ spl27_10
| ~ spl27_23 ),
inference(forward_demodulation,[],[f1492,f683]) ).
tff(f1507,plain,
( ! [X2: uni,X0: key1,X1: uni] :
( ~ in_data1(a,X0,X1,X2)
| mem(sF11,tuple21(key,a,t2tb1(X0),X1),get2(list(sF11),X2,bucket1(X0,length1(list(sF11),X2)))) )
| ~ spl27_10 ),
inference(superposition,[],[f331,f620]) ).
tff(f1512,plain,
( ! [X2: uni,X0: key1,X1: uni] :
( mem(sF11,tuple21(key,a,t2tb1(X0),X1),get2(sF14,X2,bucket1(X0,length1(sF14,X2))))
| ~ in_data1(a,X0,X1,X2) )
| ~ spl27_10
| ~ spl27_23 ),
inference(forward_demodulation,[],[f1507,f683]) ).
tff(f2288,plain,
( ! [X2: uni,X0: uni,X1: key1] :
( in_data1(a,X1,X0,X2)
| ( sF21 = some(a,X0) )
| good_data1(a,X1,X0,sF22,X2) )
| ~ spl27_3
| ~ spl27_21
| ~ spl27_34 ),
inference(superposition,[],[f1341,f1193]) ).
tff(f2318,plain,
( ! [X2: uni,X0: uni,X1: key1] :
( good_data1(a,X1,X0,sF22,X2)
| in_data1(a,X1,X0,X2) )
| ~ spl27_3
| ~ spl27_4
| ~ spl27_21
| ~ spl27_34 ),
inference(forward_subsumption_resolution,[],[f2288,f797]) ).
tff(f2332,plain,
( in_data1(a,sK9,sF17,sF19)
| ~ spl27_3
| ~ spl27_4
| ~ spl27_21
| ~ spl27_34
| spl27_56 ),
inference(resolution,[],[f2318,f1183]) ).
tff(f2334,definition,
( spl27_72
<=> in_data1(a,sK9,sF17,sF19) ),
introduced(definition,[new_symbols(definition,[spl27_72])],[avatar_definition]) ).
tff(f2336,plain,
( in_data1(a,sK9,sF17,sF19)
| ~ spl27_72 ),
inference(avatar_component_clause,[],[f2334]) ).
tff(f2337,plain,
( spl27_72
| ~ spl27_3
| ~ spl27_4
| ~ spl27_21
| ~ spl27_34
| spl27_56 ),
inference(avatar_split_clause,[],[f2332,f1181,f759,f671,f590,f585,f2334]) ).
tff(f2496,plain,
( ! [X0: key1,X1: uni] :
( ~ in_data1(a,X0,X1,sF19)
| mem(sF11,tuple21(key,a,t2tb1(X0),X1),sF12)
| $less(bucket1(X0,length1(sF14,sF19)),0)
| ~ $less(bucket1(X0,length1(sF14,sF19)),sK2) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_35
| ~ spl27_53 ),
inference(superposition,[],[f1512,f1483]) ).
tff(f2505,plain,
( ! [X0: key1,X1: uni] :
( mem(sF11,tuple21(key,a,t2tb1(X0),X1),sF12)
| $less(bucket1(X0,sK2),0)
| ~ in_data1(a,X0,X1,sF19)
| ~ $less(bucket1(X0,length1(sF14,sF19)),sK2) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_35
| ~ spl27_42
| ~ spl27_53 ),
inference(forward_demodulation,[],[f2496,f855]) ).
tff(f2508,plain,
( ! [X0: key1,X1: uni] :
( mem(sF11,tuple21(key,a,t2tb1(X0),X1),sF12)
| ~ in_data1(a,X0,X1,sF19)
| $less(bucket1(X0,sK2),0)
| ~ $less(bucket1(X0,sK2),sK2) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_35
| ~ spl27_42
| ~ spl27_53 ),
inference(forward_demodulation,[],[f2505,f855]) ).
tff(f2509,plain,
( ! [X0: key1,X1: uni] :
( ~ $less(bucket1(X0,sK2),sK2)
| ~ sort1(sF11,tuple21(key,a,t2tb1(X0),X1))
| ~ in_data1(a,X0,X1,sF19)
| $less(bucket1(X0,sK2),0) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_42
| ~ spl27_53 ),
inference(resolution,[],[f2508,f884]) ).
tff(f2513,plain,
( ! [X0: key1,X1: uni] :
( ~ in_data1(a,X0,X1,sF19)
| ~ $less(bucket1(X0,sK2),sK2)
| $less(bucket1(X0,sK2),0) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_42
| ~ spl27_53 ),
inference(forward_subsumption_resolution,[],[f2509,f923]) ).
tff(f2559,plain,
( ! [X0: $int] :
( mem(sF11,tuple21(key,a,t2tb1(sK0(a,sF19,X0)),sK1(a,sF19,X0)),sF12)
| good_hash1(a,sF19,X0)
| ~ $less(X0,sK2)
| $less(X0,0) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_35
| ~ spl27_53 ),
inference(superposition,[],[f1493,f1483]) ).
tff(f2572,plain,
( ! [X0: $int] :
( $less(X0,0)
| good_hash1(a,sF19,X0)
| ~ $less(X0,sK2)
| ~ sort1(sF11,tuple21(key,a,t2tb1(sK0(a,sF19,X0)),sK1(a,sF19,X0))) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_53 ),
inference(resolution,[],[f2559,f884]) ).
tff(f2573,plain,
( ! [X0: $int] :
( good_hash1(a,sF19,X0)
| ~ $less(X0,sK2)
| $less(X0,0) )
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_53 ),
inference(forward_subsumption_resolution,[],[f2572,f923]) ).
tff(f2598,plain,
( $less(sK10,0)
| ~ $less(sK10,sK2)
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| spl27_17
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_53 ),
inference(resolution,[],[f2573,f654]) ).
tff(f2599,plain,
( $less(sK10,0)
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| spl27_17
| ~ spl27_18
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_53 ),
inference(forward_subsumption_resolution,[],[f2598,f659]) ).
tff(f2600,plain,
( $false
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| spl27_15
| spl27_17
| ~ spl27_18
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_53 ),
inference(forward_subsumption_resolution,[],[f2599,f644]) ).
tff(f2601,plain,
( ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| spl27_15
| spl27_17
| ~ spl27_18
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_53 ),
inference(avatar_contradiction_clause,[],[f2600]) ).
tff(f2604,plain,
( ~ $less(bucket1(sK9,sK2),sK2)
| $less(bucket1(sK9,sK2),0)
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_42
| ~ spl27_53
| ~ spl27_72 ),
inference(resolution,[],[f2336,f2513]) ).
tff(f2606,definition,
( spl27_73
<=> $less(bucket1(sK9,sK2),0) ),
introduced(definition,[new_symbols(definition,[spl27_73])],[avatar_definition]) ).
tff(f2608,plain,
( $less(bucket1(sK9,sK2),0)
| ~ spl27_73 ),
inference(avatar_component_clause,[],[f2606]) ).
tff(f2610,definition,
( spl27_74
<=> $less(bucket1(sK9,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl27_74])],[avatar_definition]) ).
tff(f2612,plain,
( ~ $less(bucket1(sK9,sK2),sK2)
| spl27_74 ),
inference(avatar_component_clause,[],[f2610]) ).
tff(f2613,plain,
( spl27_73
| ~ spl27_74
| ~ spl27_5
| ~ spl27_9
| ~ spl27_10
| ~ spl27_23
| ~ spl27_24
| ~ spl27_35
| ~ spl27_42
| ~ spl27_53
| ~ spl27_72 ),
inference(avatar_split_clause,[],[f2604,f2334,f1156,f853,f767,f686,f681,f618,f614,f595,f2610,f2606]) ).
tff(f2630,plain,
( ~ $less(0,sK2)
| ~ spl27_73 ),
inference(resolution,[],[f2608,f497]) ).
tff(f2634,plain,
( $false
| ~ spl27_7
| ~ spl27_73 ),
inference(forward_subsumption_resolution,[],[f2630,f607]) ).
tff(f2635,plain,
( ~ spl27_7
| ~ spl27_73 ),
inference(avatar_contradiction_clause,[],[f2634]) ).
tff(f2707,plain,
( ~ $less(0,sK2)
| spl27_74 ),
inference(resolution,[],[f2612,f572]) ).
tff(f2712,plain,
( $false
| ~ spl27_7
| spl27_74 ),
inference(forward_subsumption_resolution,[],[f2707,f607]) ).
tff(f2713,plain,
( ~ spl27_7
| spl27_74 ),
inference(avatar_contradiction_clause,[],[f2712]) ).
tff(f2716,plain,
$false,
inference(avatar_smt_refutation,[],[f2713,f2635,f2613,f2601,f2337,f1184,f1174,f1159,f1145,f880,f856,f770,f762,f722,f704,f699,f694,f689,f684,f674,f660,f655,f645,f636,f626,f621,f616,f608,f598,f593,f588,f578]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW604_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.17 % Computer : n014.cluster.edu
% 0.12/0.17 % Model : x86_64 x86_64
% 0.12/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.17 % Memory : 8046.5625MB
% 0.12/0.17 % OS : Linux 6.8.0-71-generic
% 0.12/0.17 % CPULimit : 300
% 0.12/0.17 % WCLimit : 300
% 0.12/0.17 % DateTime : Mon Sep 28 14:20:46 UTC 2026
% 0.12/0.17 % CPUTime :
% 0.12/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.20 Running first-order theorem proving
% 0.12/0.20 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
% 3.14/1.12 % (1803914)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.14/1.12 % (1803922)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3499397061:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.14/1.12 % (1803922)Instruction limit reached!
% 3.14/1.12 % (1803922)------------------------------
% 3.14/1.12 % (1803922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.12 % (1803922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.12 % (1803922)CaDiCaL version: 2.1.3
% 3.14/1.12 % (1803922)Termination reason: Instruction limit
% 3.14/1.12 % (1803922)Termination phase: Saturation
% 3.14/1.12 % (1803922)Time elapsed: 0.003 s
% 3.14/1.12 % (1803922)Peak memory usage: 88 MB
% 3.14/1.12 % (1803922)Instructions burned: 9 (million)
% 3.14/1.12 % (1803921)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1361758208:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.14/1.12 % (1803924)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2146539566:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.14/1.12 % (1803919)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=542970201:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.14/1.12 % (1803920)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=360585829:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.14/1.12 % (1803925)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1105422194:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.14/1.12 % (1803923)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2280053229:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.14/1.12 % (1803923)Instruction limit reached!
% 3.14/1.12 % (1803923)------------------------------
% 3.14/1.12 % (1803923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.12 % (1803923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.12 % (1803923)CaDiCaL version: 2.1.3
% 3.14/1.12 % (1803923)Termination reason: Instruction limit
% 3.14/1.12 % (1803923)Termination phase: Preprocessing 3
% 3.14/1.12 % (1803923)Time elapsed: 0.003 s
% 3.14/1.12 % (1803923)Peak memory usage: 86 MB
% 3.14/1.12 % (1803923)Instructions burned: 4 (million)
% 3.14/1.12 % (1803919)Instruction limit reached!
% 3.14/1.12 % (1803919)------------------------------
% 3.14/1.12 % (1803919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.12 % (1803919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.12 % (1803919)CaDiCaL version: 2.1.3
% 3.14/1.12 % (1803919)Termination reason: Instruction limit
% 3.14/1.12 % (1803919)Termination phase: Saturation
% 3.14/1.12 % (1803919)Time elapsed: 0.028 s
% 3.14/1.12 % (1803919)Peak memory usage: 111 MB
% 3.14/1.12 % (1803919)Instructions burned: 12 (million)
% 3.14/1.12 % (1803925)Instruction limit reached!
% 3.14/1.12 % (1803925)------------------------------
% 3.14/1.12 % (1803925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.12 % (1803925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.12 % (1803925)CaDiCaL version: 2.1.3
% 3.14/1.12 % (1803925)Termination reason: Instruction limit
% 3.14/1.12 % (1803925)Termination phase: Saturation
% 3.14/1.12 % (1803925)Time elapsed: 0.044 s
% 3.14/1.12 % (1803925)Peak memory usage: 116 MB
% 3.14/1.12 % (1803925)Instructions burned: 34 (million)
% 3.14/1.12 % (1803924)Instruction limit reached!
% 3.14/1.12 % (1803924)------------------------------
% 3.14/1.12 % (1803924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.12 % (1803924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.12 % (1803924)CaDiCaL version: 2.1.3
% 3.14/1.12 % (1803924)Termination reason: Instruction limit
% 3.14/1.12 % (1803924)Termination phase: Saturation
% 3.14/1.12 % (1803924)Time elapsed: 0.055 s
% 3.14/1.12 % (1803924)Peak memory usage: 116 MB
% 3.14/1.12 % (1803924)Instructions burned: 47 (million)
% 3.14/1.12 % (1803927)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=500533457:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.14/1.12 % (1803927)Instruction limit reached!
% 3.14/1.12 % (1803927)------------------------------
% 4.01/1.29 % (1803927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.29 % (1803927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.29 % (1803927)CaDiCaL version: 2.1.3
% 4.01/1.29 % (1803927)Termination reason: Instruction limit
% 4.01/1.29 % (1803927)Termination phase: Saturation
% 4.01/1.29 % (1803927)Time elapsed: 0.005 s
% 4.01/1.29 % (1803927)Peak memory usage: 89 MB
% 4.01/1.29 % (1803927)Instructions burned: 14 (million)
% 4.01/1.29 % (1803934)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=1235294654:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.01/1.29 % (1803921)Instruction limit reached!
% 4.01/1.29 % (1803921)------------------------------
% 4.01/1.29 % (1803921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.29 % (1803921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.29 % (1803921)CaDiCaL version: 2.1.3
% 4.01/1.29 % (1803921)Termination reason: Instruction limit
% 4.01/1.29 % (1803921)Termination phase: Saturation
% 4.01/1.29 % (1803921)Time elapsed: 0.169 s
% 4.01/1.29 % (1803921)Peak memory usage: 118 MB
% 4.01/1.29 % (1803921)Instructions burned: 201 (million)
% 4.01/1.29 % (1803935)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2760197268:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.01/1.29 % (1803939)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3940228831:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.01/1.29 % (1803934)Instruction limit reached!
% 4.01/1.29 % (1803934)------------------------------
% 4.01/1.29 % (1803934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.29 % (1803934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.29 % (1803934)CaDiCaL version: 2.1.3
% 4.01/1.29 % (1803934)Termination reason: Instruction limit
% 4.01/1.29 % (1803934)Termination phase: Saturation
% 4.01/1.29 % (1803934)Time elapsed: 0.023 s
% 4.01/1.29 % (1803934)Peak memory usage: 89 MB
% 4.01/1.29 % (1803934)Instructions burned: 29 (million)
% 4.01/1.29 % (1803938)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=3733326806:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.01/1.29 % (1803936)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=8502354:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.01/1.29 % (1803935)Instruction limit reached!
% 4.01/1.29 % (1803935)------------------------------
% 4.01/1.29 % (1803935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.29 % (1803935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.29 % (1803935)CaDiCaL version: 2.1.3
% 4.01/1.29 % (1803935)Termination reason: Instruction limit
% 4.01/1.29 % (1803935)Termination phase: Saturation
% 4.01/1.29 % (1803935)Time elapsed: 0.010 s
% 4.01/1.29 % (1803935)Peak memory usage: 89 MB
% 4.01/1.29 % (1803935)Instructions burned: 16 (million)
% 4.01/1.29 % (1803936)Instruction limit reached!
% 4.01/1.29 % (1803936)------------------------------
% 4.01/1.29 % (1803936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.29 % (1803936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.29 % (1803936)CaDiCaL version: 2.1.3
% 4.01/1.29 % (1803936)Termination reason: Instruction limit
% 4.01/1.29 % (1803936)Termination phase: Saturation
% 4.01/1.29 % (1803936)Time elapsed: 0.017 s
% 4.01/1.29 % (1803936)Peak memory usage: 89 MB
% 4.01/1.29 % (1803936)Instructions burned: 24 (million)
% 4.01/1.29 % (1803938)Instruction limit reached!
% 4.01/1.29 % (1803938)------------------------------
% 4.01/1.29 % (1803938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.29 % (1803938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.29 % (1803938)CaDiCaL version: 2.1.3
% 4.01/1.29 % (1803938)Termination reason: Instruction limit
% 4.01/1.29 % (1803938)Termination phase: Saturation
% 4.01/1.29 % (1803938)Time elapsed: 0.017 s
% 4.01/1.29 % (1803938)Peak memory usage: 90 MB
% 4.01/1.29 % (1803938)Instructions burned: 27 (million)
% 4.01/1.29 % (1803939)Instruction limit reached!
% 4.01/1.29 % (1803939)------------------------------
% 4.01/1.29 % (1803939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.45 % (1803939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.45 % (1803939)CaDiCaL version: 2.1.3
% 5.23/1.45 % (1803939)Termination reason: Instruction limit
% 5.23/1.45 % (1803939)Termination phase: Saturation
% 5.23/1.45 % (1803939)Time elapsed: 0.026 s
% 5.23/1.45 % (1803939)Peak memory usage: 89 MB
% 5.23/1.45 % (1803939)Instructions burned: 87 (million)
% 5.23/1.45 % (1803920)Instruction limit reached!
% 5.23/1.45 % (1803920)------------------------------
% 5.23/1.45 % (1803920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.45 % (1803920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.45 % (1803920)CaDiCaL version: 2.1.3
% 5.23/1.45 % (1803920)Termination reason: Instruction limit
% 5.23/1.45 % (1803920)Termination phase: Saturation
% 5.23/1.45 % (1803920)Time elapsed: 0.225 s
% 5.23/1.45 % (1803920)Peak memory usage: 117 MB
% 5.23/1.45 % (1803920)Instructions burned: 308 (million)
% 5.23/1.45 % (1803943)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3933450839:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.23/1.45 % (1803948)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2299723709:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.23/1.45 % (1803943)Instruction limit reached!
% 5.23/1.45 % (1803943)------------------------------
% 5.23/1.45 % (1803943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.45 % (1803943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.45 % (1803943)CaDiCaL version: 2.1.3
% 5.23/1.45 % (1803943)Termination reason: Instruction limit
% 5.23/1.45 % (1803943)Termination phase: Unused predicate definition removal
% 5.23/1.45 % (1803943)Time elapsed: 0.002 s
% 5.23/1.45 % (1803943)Peak memory usage: 86 MB
% 5.23/1.45 % (1803943)Instructions burned: 3 (million)
% 5.23/1.45 % (1803946)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1749575178:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.23/1.45 % (1803947)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=103139679:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.23/1.45 % (1803947)Instruction limit reached!
% 5.23/1.45 % (1803947)------------------------------
% 5.23/1.45 % (1803947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.45 % (1803947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.45 % (1803947)CaDiCaL version: 2.1.3
% 5.23/1.45 % (1803947)Termination reason: Instruction limit
% 5.23/1.45 % (1803947)Termination phase: Preprocessing 3
% 5.23/1.45 % (1803947)Time elapsed: 0.003 s
% 5.23/1.45 % (1803947)Peak memory usage: 86 MB
% 5.23/1.45 % (1803947)Instructions burned: 4 (million)
% 5.23/1.45 % (1803949)lrs+10_1_thi=all:si=on:fd=off:random_seed=1692501755:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.23/1.45 % (1803950)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=2752762292:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.23/1.45 % (1803950)Instruction limit reached!
% 5.23/1.45 % (1803950)------------------------------
% 5.23/1.45 % (1803950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.45 % (1803950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.45 % (1803950)CaDiCaL version: 2.1.3
% 5.23/1.45 % (1803950)Termination reason: Instruction limit
% 5.23/1.45 % (1803950)Termination phase: Property scanning
% 5.23/1.45 % (1803950)Time elapsed: 0.005 s
% 5.23/1.45 % (1803950)Peak memory usage: 86 MB
% 5.23/1.45 % (1803950)Instructions burned: 9 (million)
% 5.23/1.45 % (1803948)Instruction limit reached!
% 5.23/1.45 % (1803948)------------------------------
% 5.23/1.45 % (1803948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.45 % (1803948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.45 % (1803948)CaDiCaL version: 2.1.3
% 5.23/1.45 % (1803948)Termination reason: Instruction limit
% 5.23/1.45 % (1803948)Termination phase: Saturation
% 5.23/1.45 % (1803948)Time elapsed: 0.049 s
% 5.23/1.45 % (1803948)Peak memory usage: 134 MB
% 5.23/1.45 % (1803948)Instructions burned: 67 (million)
% 6.47/1.67 % (1803951)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1932403740:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 6.47/1.67 % (1803951)Instruction limit reached!
% 6.47/1.67 % (1803951)------------------------------
% 6.47/1.67 % (1803951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/1.67 % (1803951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.67 % (1803951)CaDiCaL version: 2.1.3
% 6.47/1.67 % (1803951)Termination reason: Instruction limit
% 6.47/1.67 % (1803951)Termination phase: Unused predicate definition removal
% 6.47/1.67 % (1803951)Time elapsed: 0.002 s
% 6.47/1.67 % (1803951)Peak memory usage: 86 MB
% 6.47/1.67 % (1803951)Instructions burned: 3 (million)
% 6.47/1.67 % (1803949)Instruction limit reached!
% 6.47/1.67 % (1803949)------------------------------
% 6.47/1.67 % (1803949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/1.67 % (1803949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.67 % (1803949)CaDiCaL version: 2.1.3
% 6.47/1.67 % (1803949)Termination reason: Instruction limit
% 6.47/1.67 % (1803949)Termination phase: Saturation
% 6.47/1.67 % (1803949)Time elapsed: 0.062 s
% 6.47/1.67 % (1803949)Peak memory usage: 116 MB
% 6.47/1.67 % (1803949)Instructions burned: 53 (million)
% 6.47/1.67 % (1803946)Instruction limit reached!
% 6.47/1.67 % (1803946)------------------------------
% 6.47/1.67 % (1803946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/1.67 % (1803946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.67 % (1803946)CaDiCaL version: 2.1.3
% 6.47/1.67 % (1803946)Termination reason: Instruction limit
% 6.47/1.67 % (1803946)Termination phase: Saturation
% 6.47/1.67 % (1803946)Time elapsed: 0.117 s
% 6.47/1.67 % (1803946)Peak memory usage: 91 MB
% 6.47/1.67 % (1803946)Instructions burned: 181 (million)
% 6.47/1.67 % (1803955)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3167652909:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.47/1.67 % (1803955)Instruction limit reached!
% 6.47/1.67 % (1803955)------------------------------
% 6.47/1.67 % (1803955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/1.67 % (1803955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.67 % (1803955)CaDiCaL version: 2.1.3
% 6.47/1.67 % (1803955)Termination reason: Instruction limit
% 6.47/1.67 % (1803955)Termination phase: Preprocessing 1
% 6.47/1.67 % (1803955)Time elapsed: 0.001 s
% 6.47/1.67 % (1803955)Peak memory usage: 85 MB
% 6.47/1.67 % (1803955)Instructions burned: 2 (million)
% 6.47/1.67 % (1803961)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1838002205:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi)
% 6.47/1.67 % (1803961)Refutation not found, incomplete strategy
% 6.47/1.67 % (1803961)------------------------------
% 6.47/1.67 % (1803961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/1.67 % (1803961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.67 % (1803961)CaDiCaL version: 2.1.3
% 6.47/1.67 % (1803961)Termination reason: Refutation not found, incomplete strategy
% 6.47/1.67 % (1803961)Time elapsed: 0.005 s
% 6.47/1.67 % (1803961)Peak memory usage: 89 MB
% 6.47/1.67 % (1803961)Instructions burned: 14 (million)
% 6.47/1.67 % (1803957)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4139446255:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.47/1.67 % (1803960)dis+10_1_si=on:random_seed=3820531618:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 6.47/1.67 % (1803960)Instruction limit reached!
% 6.47/1.67 % (1803960)------------------------------
% 6.47/1.67 % (1803960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/1.67 % (1803960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.67 % (1803960)CaDiCaL version: 2.1.3
% 6.47/1.67 % (1803960)Termination reason: Instruction limit
% 6.47/1.67 % (1803960)Termination phase: Saturation
% 6.47/1.67 % (1803960)Time elapsed: 0.006 s
% 6.47/1.67 % (1803960)Peak memory usage: 88 MB
% 6.47/1.67 % (1803960)Instructions burned: 11 (million)
% 6.47/1.67 % (1803963)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=848768112:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 7.67/1.85 % (1803964)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3094958864:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.67/1.85 % (1803963)Instruction limit reached!
% 7.67/1.85 % (1803963)------------------------------
% 7.67/1.85 % (1803963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.85 % (1803963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.85 % (1803963)CaDiCaL version: 2.1.3
% 7.67/1.85 % (1803963)Termination reason: Instruction limit
% 7.67/1.85 % (1803963)Termination phase: Saturation
% 7.67/1.85 % (1803963)Time elapsed: 0.027 s
% 7.67/1.85 % (1803963)Peak memory usage: 89 MB
% 7.67/1.85 % (1803963)Instructions burned: 35 (million)
% 7.67/1.85 % (1803964)Instruction limit reached!
% 7.67/1.85 % (1803964)------------------------------
% 7.67/1.85 % (1803964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.85 % (1803964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.85 % (1803964)CaDiCaL version: 2.1.3
% 7.67/1.85 % (1803964)Termination reason: Instruction limit
% 7.67/1.85 % (1803964)Termination phase: Unused predicate definition removal
% 7.67/1.85 % (1803964)Time elapsed: 0.002 s
% 7.67/1.85 % (1803964)Peak memory usage: 86 MB
% 7.67/1.85 % (1803964)Instructions burned: 3 (million)
% 7.67/1.85 % (1803967)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3598453145:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 7.67/1.85 % (1803966)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3966106148:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 7.67/1.85 % (1803966)Instruction limit reached!
% 7.67/1.85 % (1803966)------------------------------
% 7.67/1.85 % (1803966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.85 % (1803966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.85 % (1803966)CaDiCaL version: 2.1.3
% 7.67/1.85 % (1803966)Termination reason: Instruction limit
% 7.67/1.85 % (1803966)Termination phase: Saturation
% 7.67/1.85 % (1803966)Time elapsed: 0.005 s
% 7.67/1.85 % (1803966)Peak memory usage: 88 MB
% 7.67/1.85 % (1803966)Instructions burned: 9 (million)
% 7.67/1.85 % (1803957)Instruction limit reached!
% 7.67/1.85 % (1803957)------------------------------
% 7.67/1.85 % (1803957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.85 % (1803957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.85 % (1803957)CaDiCaL version: 2.1.3
% 7.67/1.85 % (1803957)Termination reason: Instruction limit
% 7.67/1.85 % (1803957)Termination phase: Saturation
% 7.67/1.85 % (1803957)Time elapsed: 0.113 s
% 7.67/1.85 % (1803957)Peak memory usage: 118 MB
% 7.67/1.85 % (1803957)Instructions burned: 127 (million)
% 7.67/1.85 % (1803961)------------------------------
% 7.67/1.85 % (1803961)------------------------------
% 7.67/1.85 % (1803971)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3233700869:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 7.67/1.85 % (1803971)Instruction limit reached!
% 7.67/1.85 % (1803971)------------------------------
% 7.67/1.85 % (1803971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.85 % (1803971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.85 % (1803971)CaDiCaL version: 2.1.3
% 7.67/1.85 % (1803971)Termination reason: Instruction limit
% 7.67/1.85 % (1803971)Termination phase: Saturation
% 7.67/1.85 % (1803971)Time elapsed: 0.026 s
% 7.67/1.85 % (1803971)Peak memory usage: 105 MB
% 7.67/1.85 % (1803971)Instructions burned: 13 (million)
% 7.67/1.85 % (1803976)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1797859379:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 7.67/1.85 % (1803974)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2339852128:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 7.67/1.85 % (1803976)Instruction limit reached!
% 7.67/1.85 % (1803976)------------------------------
% 7.67/1.85 % (1803976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.85 % (1803976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.85 % (1803976)CaDiCaL version: 2.1.3
% 10.17/2.12 % (1803976)Termination reason: Instruction limit
% 10.17/2.12 % (1803976)Termination phase: Saturation
% 10.17/2.12 % (1803976)Time elapsed: 0.007 s
% 10.17/2.12 % (1803976)Peak memory usage: 88 MB
% 10.17/2.12 % (1803976)Instructions burned: 11 (million)
% 10.17/2.12 % (1803978)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2904497373:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi)
% 10.17/2.12 % (1803980)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=4176960166:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 10.17/2.12 % (1803979)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=3530307800:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.17/2.12 % (1803967)Instruction limit reached!
% 10.17/2.12 % (1803967)------------------------------
% 10.17/2.12 % (1803967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.12 % (1803967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.12 % (1803967)CaDiCaL version: 2.1.3
% 10.17/2.12 % (1803967)Termination reason: Instruction limit
% 10.17/2.12 % (1803967)Termination phase: Saturation
% 10.17/2.12 % (1803967)Time elapsed: 0.206 s
% 10.17/2.12 % (1803967)Peak memory usage: 92 MB
% 10.17/2.12 % (1803967)Instructions burned: 371 (million)
% 10.17/2.12 % (1803979)Instruction limit reached!
% 10.17/2.12 % (1803979)------------------------------
% 10.17/2.12 % (1803979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.12 % (1803979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.12 % (1803979)CaDiCaL version: 2.1.3
% 10.17/2.12 % (1803979)Termination reason: Instruction limit
% 10.17/2.12 % (1803979)Termination phase: Saturation
% 10.17/2.12 % (1803979)Time elapsed: 0.055 s
% 10.17/2.12 % (1803979)Peak memory usage: 90 MB
% 10.17/2.12 % (1803979)Instructions burned: 75 (million)
% 10.17/2.12 % (1803978)Instruction limit reached!
% 10.17/2.12 % (1803978)------------------------------
% 10.17/2.12 % (1803978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.12 % (1803978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.12 % (1803978)CaDiCaL version: 2.1.3
% 10.17/2.12 % (1803978)Termination reason: Instruction limit
% 10.17/2.12 % (1803978)Termination phase: Saturation
% 10.17/2.12 % (1803978)Time elapsed: 0.087 s
% 10.17/2.12 % (1803978)Peak memory usage: 133 MB
% 10.17/2.12 % (1803978)Instructions burned: 72 (million)
% 10.17/2.12 % (1803982)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4059392543:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi)
% 10.17/2.12 % (1803980)Instruction limit reached!
% 10.17/2.12 % (1803980)------------------------------
% 10.17/2.12 % (1803980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.12 % (1803980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.12 % (1803980)CaDiCaL version: 2.1.3
% 10.17/2.12 % (1803980)Termination reason: Instruction limit
% 10.17/2.12 % (1803980)Termination phase: Saturation
% 10.17/2.12 % (1803980)Time elapsed: 0.111 s
% 10.17/2.12 % (1803980)Peak memory usage: 91 MB
% 10.17/2.12 % (1803980)Instructions burned: 294 (million)
% 10.17/2.12 % (1803985)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4213312414:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.17/2.12 % (1803974)Instruction limit reached!
% 10.17/2.12 % (1803974)------------------------------
% 10.17/2.12 % (1803974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.12 % (1803974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.12 % (1803974)CaDiCaL version: 2.1.3
% 10.17/2.12 % (1803974)Termination reason: Instruction limit
% 10.17/2.12 % (1803974)Termination phase: Saturation
% 10.17/2.12 % (1803974)Time elapsed: 0.163 s
% 10.17/2.12 % (1803974)Peak memory usage: 120 MB
% 10.17/2.12 % (1803974)Instructions burned: 226 (million)
% 10.17/2.12 % (1803989)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1781634588:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi)
% 10.17/2.12 % (1803991)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3899807905:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 11.63/2.43 % (1803990)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1115936228:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 11.63/2.43 % (1803993)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1942540144:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.63/2.43 % (1803982)Instruction limit reached!
% 11.63/2.43 % (1803982)------------------------------
% 11.63/2.43 % (1803982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.43 % (1803982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.43 % (1803982)CaDiCaL version: 2.1.3
% 11.63/2.43 % (1803982)Termination reason: Instruction limit
% 11.63/2.43 % (1803982)Termination phase: Saturation
% 11.63/2.43 % (1803982)Time elapsed: 0.111 s
% 11.63/2.43 % (1803982)Peak memory usage: 117 MB
% 11.63/2.43 % (1803982)Instructions burned: 131 (million)
% 11.63/2.43 % (1803989)Instruction limit reached!
% 11.63/2.43 % (1803989)------------------------------
% 11.63/2.43 % (1803989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.43 % (1803989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.43 % (1803989)CaDiCaL version: 2.1.3
% 11.63/2.43 % (1803989)Termination reason: Instruction limit
% 11.63/2.43 % (1803989)Termination phase: Saturation
% 11.63/2.43 % (1803989)Time elapsed: 0.068 s
% 11.63/2.43 % (1803989)Peak memory usage: 134 MB
% 11.63/2.43 % (1803989)Instructions burned: 41 (million)
% 11.63/2.43 % (1803985)Instruction limit reached!
% 11.63/2.43 % (1803985)------------------------------
% 11.63/2.43 % (1803985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.43 % (1803985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.43 % (1803985)CaDiCaL version: 2.1.3
% 11.63/2.43 % (1803985)Termination reason: Instruction limit
% 11.63/2.43 % (1803985)Termination phase: Saturation
% 11.63/2.43 % (1803985)Time elapsed: 0.137 s
% 11.63/2.43 % (1803985)Peak memory usage: 134 MB
% 11.63/2.43 % (1803985)Instructions burned: 132 (million)
% 11.63/2.43 % (1803993)Instruction limit reached!
% 11.63/2.43 % (1803993)------------------------------
% 11.63/2.43 % (1803993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.43 % (1803993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.43 % (1803993)CaDiCaL version: 2.1.3
% 11.63/2.43 % (1803993)Termination reason: Instruction limit
% 11.63/2.43 % (1803993)Termination phase: Saturation
% 11.63/2.43 % (1803993)Time elapsed: 0.061 s
% 11.63/2.43 % (1803993)Peak memory usage: 117 MB
% 11.63/2.43 % (1803993)Instructions burned: 132 (million)
% 11.63/2.43 % (1803995)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=2700342555:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi)
% 11.63/2.43 % (1804000)dis+10_1_si=on:random_seed=2346720427:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 11.63/2.43 % (1804003)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2481220649:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 11.63/2.43 % (1803990)Instruction limit reached!
% 11.63/2.43 % (1803990)------------------------------
% 11.63/2.43 % (1803990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.43 % (1803990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.43 % (1803990)CaDiCaL version: 2.1.3
% 11.63/2.43 % (1803990)Termination reason: Instruction limit
% 11.63/2.43 % (1803990)Termination phase: Saturation
% 11.63/2.43 % (1803990)Time elapsed: 0.164 s
% 11.63/2.43 % (1803990)Peak memory usage: 92 MB
% 11.63/2.43 % (1803990)Instructions burned: 307 (million)
% 11.63/2.43 % (1804003)Refutation not found, incomplete strategy
% 11.63/2.43 % (1804003)------------------------------
% 11.63/2.43 % (1804003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.63/2.43 % (1804003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.43 % (1804003)CaDiCaL version: 2.1.3
% 11.63/2.43 % (1804003)Termination reason: Refutation not found, incomplete strategy
% 11.63/2.43 % (1804003)Time elapsed: 0.023 s
% 11.63/2.43 % (1804003)Peak memory usage: 116 MB
% 11.63/2.43 % (1804003)Instructions burned: 24 (million)
% 11.63/2.43 % (1804001)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2446640300:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi)
% 13.39/2.70 % (1804002)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=856218983:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi)
% 13.39/2.70 % (1803995)Instruction limit reached!
% 13.39/2.70 % (1803995)------------------------------
% 13.39/2.70 % (1803995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.70 % (1803995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.70 % (1803995)CaDiCaL version: 2.1.3
% 13.39/2.70 % (1803995)Termination reason: Instruction limit
% 13.39/2.70 % (1803995)Termination phase: Saturation
% 13.39/2.70 % (1803995)Time elapsed: 0.205 s
% 13.39/2.70 % (1803995)Peak memory usage: 118 MB
% 13.39/2.70 % (1803995)Instructions burned: 260 (million)
% 13.39/2.70 % (1804002)Instruction limit reached!
% 13.39/2.70 % (1804002)------------------------------
% 13.39/2.70 % (1804002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.70 % (1804002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.70 % (1804002)CaDiCaL version: 2.1.3
% 13.39/2.70 % (1804002)Termination reason: Instruction limit
% 13.39/2.70 % (1804002)Termination phase: Saturation
% 13.39/2.70 % (1804002)Time elapsed: 0.097 s
% 13.39/2.70 % (1804002)Peak memory usage: 91 MB
% 13.39/2.70 % (1804002)Instructions burned: 141 (million)
% 13.39/2.70 % (1804007)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3621384528:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 13.39/2.70 % (1804003)------------------------------
% 13.39/2.70 % (1804003)------------------------------
% 13.39/2.70 % (1804007)Instruction limit reached!
% 13.39/2.70 % (1804007)------------------------------
% 13.39/2.70 % (1804007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.70 % (1804007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.70 % (1804007)CaDiCaL version: 2.1.3
% 13.39/2.70 % (1804007)Termination reason: Instruction limit
% 13.39/2.70 % (1804007)Termination phase: Saturation
% 13.39/2.70 % (1804007)Time elapsed: 0.080 s
% 13.39/2.70 % (1804007)Peak memory usage: 90 MB
% 13.39/2.70 % (1804007)Instructions burned: 121 (million)
% 13.39/2.70 % (1803991)Instruction limit reached!
% 13.39/2.70 % (1803991)------------------------------
% 13.39/2.70 % (1803991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.70 % (1803991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.70 % (1803991)CaDiCaL version: 2.1.3
% 13.39/2.70 % (1803991)Termination reason: Instruction limit
% 13.39/2.70 % (1803991)Termination phase: Saturation
% 13.39/2.70 % (1803991)Time elapsed: 0.402 s
% 13.39/2.70 % (1803991)Peak memory usage: 142 MB
% 13.39/2.70 % (1803991)Instructions burned: 598 (million)
% 13.39/2.70 % (1804001)Instruction limit reached!
% 13.39/2.70 % (1804001)------------------------------
% 13.39/2.70 % (1804001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.70 % (1804001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.70 % (1804001)CaDiCaL version: 2.1.3
% 13.39/2.70 % (1804001)Termination reason: Instruction limit
% 13.39/2.70 % (1804001)Termination phase: Saturation
% 13.39/2.70 % (1804001)Time elapsed: 0.221 s
% 13.39/2.70 % (1804001)Peak memory usage: 92 MB
% 13.39/2.70 % (1804001)Instructions burned: 384 (million)
% 13.39/2.70 % (1804013)dis+1010_1_to=kbo:si=on:random_seed=1491149030:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi)
% 13.39/2.70 % (1804011)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=1931369879:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 13.39/2.70 % (1804010)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=2521088851:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 13.39/2.70 % (1804013)Instruction limit reached!
% 13.39/2.70 % (1804013)------------------------------
% 13.39/2.70 % (1804013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.70 % (1804013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.70 % (1804013)CaDiCaL version: 2.1.3
% 13.39/2.70 % (1804013)Termination reason: Instruction limit
% 13.39/2.70 % (1804013)Termination phase: Saturation
% 13.39/2.70 % (1804013)Time elapsed: 0.047 s
% 14.79/2.99 % (1804013)Peak memory usage: 90 MB
% 14.79/2.99 % (1804013)Instructions burned: 178 (million)
% 14.79/2.99 % (1804011)Instruction limit reached!
% 14.79/2.99 % (1804011)------------------------------
% 14.79/2.99 % (1804011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804011)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804011)Termination reason: Instruction limit
% 14.79/2.99 % (1804011)Termination phase: Saturation
% 14.79/2.99 % (1804011)Time elapsed: 0.049 s
% 14.79/2.99 % (1804011)Peak memory usage: 116 MB
% 14.79/2.99 % (1804011)Instructions burned: 40 (million)
% 14.79/2.99 % (1804014)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1986299211:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi)
% 14.79/2.99 % (1804010)Instruction limit reached!
% 14.79/2.99 % (1804010)------------------------------
% 14.79/2.99 % (1804010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804010)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804010)Termination reason: Instruction limit
% 14.79/2.99 % (1804010)Termination phase: Saturation
% 14.79/2.99 % (1804010)Time elapsed: 0.110 s
% 14.79/2.99 % (1804010)Peak memory usage: 118 MB
% 14.79/2.99 % (1804010)Instructions burned: 129 (million)
% 14.79/2.99 % (1804019)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1177942596:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi)
% 14.79/2.99 % (1804018)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2231396994:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi)
% 14.79/2.99 % (1804020)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1286338195:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi)
% 14.79/2.99 % (1804021)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1741363499:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi)
% 14.79/2.99 % (1804020)Instruction limit reached!
% 14.79/2.99 % (1804020)------------------------------
% 14.79/2.99 % (1804020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804020)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804020)Termination reason: Instruction limit
% 14.79/2.99 % (1804020)Termination phase: Saturation
% 14.79/2.99 % (1804020)Time elapsed: 0.113 s
% 14.79/2.99 % (1804020)Peak memory usage: 117 MB
% 14.79/2.99 % (1804020)Instructions burned: 350 (million)
% 14.79/2.99 % (1804023)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=625643082:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi)
% 14.79/2.99 % (1804019)Instruction limit reached!
% 14.79/2.99 % (1804019)------------------------------
% 14.79/2.99 % (1804019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804019)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804019)Termination reason: Instruction limit
% 14.79/2.99 % (1804019)Termination phase: Saturation
% 14.79/2.99 % (1804019)Time elapsed: 0.162 s
% 14.79/2.99 % (1804019)Peak memory usage: 135 MB
% 14.79/2.99 % (1804019)Instructions burned: 216 (million)
% 14.79/2.99 % (1804000)Instruction limit reached!
% 14.79/2.99 % (1804000)------------------------------
% 14.79/2.99 % (1804000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804000)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804000)Termination reason: Instruction limit
% 14.79/2.99 % (1804000)Termination phase: Saturation
% 14.79/2.99 % (1804000)Time elapsed: 0.564 s
% 14.79/2.99 % (1804000)Peak memory usage: 93 MB
% 14.79/2.99 % (1804000)Instructions burned: 1000 (million)
% 14.79/2.99 % (1804028)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2824799614:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi)
% 14.79/2.99 % (1804021)Instruction limit reached!
% 14.79/2.99 % (1804021)------------------------------
% 14.79/2.99 % (1804021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804021)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804021)Termination reason: Instruction limit
% 14.79/2.99 % (1804021)Termination phase: Saturation
% 14.79/2.99 % (1804021)Time elapsed: 0.168 s
% 14.79/2.99 % (1804021)Peak memory usage: 91 MB
% 14.79/2.99 % (1804021)Instructions burned: 296 (million)
% 14.79/2.99 % (1804014)Instruction limit reached!
% 14.79/2.99 % (1804014)------------------------------
% 14.79/2.99 % (1804014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804014)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804014)Termination reason: Instruction limit
% 14.79/2.99 % (1804014)Termination phase: Saturation
% 14.79/2.99 % (1804014)Time elapsed: 0.244 s
% 14.79/2.99 % (1804014)Peak memory usage: 120 MB
% 14.79/2.99 % (1804014)Instructions burned: 330 (million)
% 14.79/2.99 % (1804030)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=799957191:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi)
% 14.79/2.99 % (1804031)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=837727699:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi)
% 14.79/2.99 % (1804028)Instruction limit reached!
% 14.79/2.99 % (1804028)------------------------------
% 14.79/2.99 % (1804028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804028)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804028)Termination reason: Instruction limit
% 14.79/2.99 % (1804028)Termination phase: Saturation
% 14.79/2.99 % (1804028)Time elapsed: 0.118 s
% 14.79/2.99 % (1804028)Peak memory usage: 118 MB
% 14.79/2.99 % (1804028)Instructions burned: 282 (million)
% 14.79/2.99 % (1804033)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1966531810:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi)
% 14.79/2.99 % (1804034)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1240132856:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi)
% 14.79/2.99 % (1804018)Instruction limit reached!
% 14.79/2.99 % (1804018)------------------------------
% 14.79/2.99 % (1804018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804018)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804018)Termination reason: Instruction limit
% 14.79/2.99 % (1804018)Termination phase: Saturation
% 14.79/2.99 % (1804018)Time elapsed: 0.363 s
% 14.79/2.99 % (1804018)Peak memory usage: 135 MB
% 14.79/2.99 % (1804018)Instructions burned: 484 (million)
% 14.79/2.99 % (1804023)Instruction limit reached!
% 14.79/2.99 % (1804023)------------------------------
% 14.79/2.99 % (1804023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804023)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804023)Termination reason: Instruction limit
% 14.79/2.99 % (1804023)Termination phase: Saturation
% 14.79/2.99 % (1804023)Time elapsed: 0.235 s
% 14.79/2.99 % (1804023)Peak memory usage: 118 MB
% 14.79/2.99 % (1804023)Instructions burned: 329 (million)
% 14.79/2.99 % (1804037)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=158479306:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi)
% 14.79/2.99 % (1804031)Instruction limit reached!
% 14.79/2.99 % (1804031)------------------------------
% 14.79/2.99 % (1804031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804031)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804031)Termination reason: Instruction limit
% 14.79/2.99 % (1804031)Termination phase: Saturation
% 14.79/2.99 % (1804031)Time elapsed: 0.196 s
% 14.79/2.99 % (1804031)Peak memory usage: 114 MB
% 14.79/2.99 % (1804031)Instructions burned: 323 (million)
% 14.79/2.99 % (1804041)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=616106292:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi)
% 14.79/2.99 % (1804040)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4294128864:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi)
% 14.79/2.99 % (1804034)First to succeed.
% 14.79/2.99 % (1804034)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1803914"
% 14.79/2.99 % (1804037)Instruction limit reached!
% 14.79/2.99 % (1804037)------------------------------
% 14.79/2.99 % (1804037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804037)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804037)Termination reason: Instruction limit
% 14.79/2.99 % (1804037)Termination phase: Saturation
% 14.79/2.99 % (1804037)Time elapsed: 0.124 s
% 14.79/2.99 % (1804037)Peak memory usage: 135 MB
% 14.79/2.99 % (1804037)Instructions burned: 277 (million)
% 14.79/2.99 % (1804030)Instruction limit reached!
% 14.79/2.99 % (1804030)------------------------------
% 14.79/2.99 % (1804030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804030)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804030)Termination reason: Instruction limit
% 14.79/2.99 % (1804030)Termination phase: Saturation
% 14.79/2.99 % (1804030)Time elapsed: 0.287 s
% 14.79/2.99 % (1804030)Peak memory usage: 93 MB
% 14.79/2.99 % (1804030)Instructions burned: 485 (million)
% 14.79/2.99 % (1804046)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1087792163:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi)
% 14.79/2.99 % (1804043)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2133691861:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi)
% 14.79/2.99 % (1804033)Instruction limit reached!
% 14.79/2.99 % (1804033)------------------------------
% 14.79/2.99 % (1804033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804033)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804033)Termination reason: Instruction limit
% 14.79/2.99 % (1804033)Termination phase: Saturation
% 14.79/2.99 % (1804033)Time elapsed: 0.276 s
% 14.79/2.99 % (1804033)Peak memory usage: 123 MB
% 14.79/2.99 % (1804033)Instructions burned: 416 (million)
% 14.79/2.99 % (1804047)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=4040833077:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi)
% 14.79/2.99 % (1804040)Instruction limit reached!
% 14.79/2.99 % (1804040)------------------------------
% 14.79/2.99 % (1804040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804040)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804040)Termination reason: Instruction limit
% 14.79/2.99 % (1804040)Termination phase: Saturation
% 14.79/2.99 % (1804040)Time elapsed: 0.265 s
% 14.79/2.99 % (1804040)Peak memory usage: 119 MB
% 14.79/2.99 % (1804040)Instructions burned: 376 (million)
% 14.79/2.99 % (1804046)Instruction limit reached!
% 14.79/2.99 % (1804046)------------------------------
% 14.79/2.99 % (1804046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/2.99 % (1804046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.99 % (1804046)CaDiCaL version: 2.1.3
% 14.79/2.99 % (1804046)Termination reason: Instruction limit
% 14.79/2.99 % (1804046)Termination phase: Saturation
% 14.79/2.99 % (1804046)Time elapsed: 0.149 s
% 14.79/2.99 % (1804046)Peak memory usage: 137 MB
% 14.79/2.99 % (1804046)Instructions burned: 336 (million)
% 14.79/2.99 % (1804034)Refutation found. Thanks to Tanya!
% 14.79/2.99 % SZS status Theorem for theBenchmark
% 14.79/2.99 % SZS output start Proof for theBenchmark
% See solution above
% 17.18/3.19 % (1804034)------------------------------
% 17.18/3.19 % (1804034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/3.19 % (1804034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.19 % (1804034)CaDiCaL version: 2.1.3
% 17.18/3.19 % (1804034)Termination reason: Refutation
% 17.18/3.19 % (1804034)Time elapsed: 0.165 s
% 17.18/3.19 % (1804034)Peak memory usage: 119 MB
% 17.18/3.19 % (1804034)Instructions burned: 202 (million)
% 17.18/3.19 % (1804034)------------------------------
% 17.18/3.19 % (1804034)------------------------------
% 17.18/3.19 % (1803914)Success in time 2.35 s
% 17.18/3.19 % Vampire exiting
%------------------------------------------------------------------------------