%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW605_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 9.95s 2.29s
% Output : Refutation 10.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 38
% Syntax : Number of formulae : 204 ( 67 unt; 0 typ; 26 def)
% Number of atoms : 865 ( 160 equ)
% Maximal formula atoms : 41 ( 4 avg)
% Number of connectives : 991 ( 330 ~; 335 |; 255 &)
% ( 20 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 957 ( 271 atm; 227 fun; 391 num; 68 var)
% Number of types : 14 ( 12 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 12 usr; 8 prp; 0-5 aty)
% Number of functors : 108 ( 103 usr; 42 con; 0-5 aty)
% Number of variables : 374 ( 0 sgn 319 !; 55 ?; 374 :)
% 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(type_def_16,type,
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,
t2tb8: lpkeycm_a1rp > uni ).
tff(func_def_68,type,
tb2t8: uni > lpkeycm_a1rp ).
tff(func_def_69,type,
t2tb7: a1 > uni ).
tff(func_def_70,type,
tb2t7: uni > a1 ).
tff(func_def_72,type,
sK0: ( $int * ty * uni ) > key1 ).
tff(func_def_73,type,
sK1: ( $int * ty * uni ) > uni ).
tff(func_def_74,type,
sK2: $int ).
tff(func_def_75,type,
sK3: map_key_lpoption_a1rp ).
tff(func_def_76,type,
sK4: map_int_lplist_lpkeycm_a1rprp ).
tff(func_def_77,type,
sK5: list_lpkeycm_a1rp ).
tff(func_def_78,type,
sK6: map_int_lplist_lpkeycm_a1rprp ).
tff(func_def_79,type,
sK7: $int ).
tff(func_def_80,type,
sK8: map_key_lpoption_a1rp ).
tff(func_def_81,type,
sK9: $int ).
tff(func_def_82,type,
sK10: map_int_lplist_lpkeycm_a1rprp ).
tff(func_def_83,type,
sK11: a1 ).
tff(func_def_84,type,
sK12: key1 ).
tff(func_def_85,type,
sF13: uni ).
tff(func_def_86,type,
sF14: ty ).
tff(func_def_87,type,
sF15: ty ).
tff(func_def_88,type,
sF16: uni ).
tff(func_def_89,type,
sF17: uni ).
tff(func_def_90,type,
sF18: $int ).
tff(func_def_91,type,
sF19: $int ).
tff(func_def_92,type,
sF20: ( key1 * a1 ) > uni ).
tff(func_def_93,type,
sF21: uni ).
tff(func_def_94,type,
sF22: key1 > $int ).
tff(func_def_95,type,
sF23: uni ).
tff(func_def_96,type,
sF24: uni ).
tff(func_def_97,type,
sF25: a1 > uni ).
tff(func_def_98,type,
sF26: a1 > option_a1 ).
tff(func_def_99,type,
sF27: ty ).
tff(func_def_100,type,
sF28: uni ).
tff(func_def_101,type,
sF29: key1 > uni ).
tff(func_def_102,type,
sF30: key1 > option_a1 ).
tff(func_def_103,type,
sF31: uni ).
tff(func_def_104,type,
sF32: uni ).
tff(func_def_105,type,
sF33: $int ).
tff(func_def_106,type,
sF34: uni ).
tff(func_def_107,type,
sF35: uni ).
tff(func_def_108,type,
sF36: list_lpkeycm_a1rp ).
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(f27,axiom,
! [X1: uni,X0: ty] : sort1(option(X0),some(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',some_sort2) ).
tff(f46,axiom,
! [X1: uni,X0: ty] :
( sort1(X0,X1)
=> ( ! [X2: uni,X3: uni] :
( sort1(X0,X2)
=> ( ( ( X1 = X2 )
| mem(X0,X1,X3) )
<=> mem(X0,X1,cons(X0,X2,X3)) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_def) ).
tff(f47,axiom,
! [X3: uni,X0: ty,X1: ty,X2: uni] : sort1(X1,get(X1,X0,X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_sort4) ).
tff(f69,axiom,
! [X0: $int] :
( $less(0,X0)
=> ! [X1: key1] :
( $lesseq(0,bucket1(X1,X0))
& $less(bucket1(X1,X0),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bucket_bounds) ).
tff(f70,axiom,
! [X1: ty,X2: uni,X0: ty,X3: uni] : sort1(tuple2(X1,X0),tuple21(X1,X0,X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuple2_sort2) ).
tff(f80,axiom,
! [X2: uni,X3: uni,X0: ty,X4: 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/sandbox2/benchmark/theBenchmark.p',good_data_def) ).
tff(f97,axiom,
! [X0: uni] :
( sort1(option(a),X0)
=> ( t2tb4(tb2t4(X0)) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR4) ).
tff(f103,axiom,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR6) ).
tff(f110,conjecture,
! [X2: map_key_lpoption_a1rp,X0: $int,X1: map_int_lplist_lpkeycm_a1rprp] :
( ( ! [X3: $int] :
( ( $less(X3,X0)
& $lesseq(0,X3) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) )
& $less(0,X0)
& ! [X4: key1,X5: a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))
& $lesseq(0,X0) )
=> ( $lesseq(0,$sum($product(2,X0),1))
=> ( $lesseq(0,$sum($product(2,X0),1))
=> ! [X9: $int,X3: $int,X6: list_lpkeycm_a1rp,X10: map_int_lplist_lpkeycm_a1rprp,X8: map_key_lpoption_a1rp,X7: map_int_lplist_lpkeycm_a1rprp] :
( ( ! [X4: key1,X5: a1] :
( mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6))
=> ( bucket1(X4,X0) = X3 ) )
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)))
& ! [X12: $int] :
( ( $lesseq(0,X12)
& $less(X12,$sum($product(2,X0),1)) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)),X12) )
& $lesseq(0,X9)
& $less(0,X9)
& $lesseq(0,$sum($product(2,X0),1))
& ! [X11: $int] :
( ( $less(X11,X9)
& $lesseq(0,X11) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)),X11) )
& ! [X5: a1,X4: key1] :
( ( ~ ( $less(bucket1(X4,X0),X3)
& $lesseq(0,bucket1(X4,X0)) )
& ( ( ( bucket1(X4,X0) != X3 )
& ~ in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) )
| ( ( ( in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))
| mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) )
<=> ( tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X4))) = tb2t4(some(a,t2tb7(X5))) ) )
& ( bucket1(X4,X0) = X3 ) ) ) )
| ( $lesseq(0,bucket1(X4,X0))
& good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))
& $less(bucket1(X4,X0),X3) ) ) )
=> ( ( X6 = tb2t6(nil(tuple2(key,a))) )
=> ! [X5: a1,X4: key1] :
( ( ( $lesseq(bucket1(X4,X0),X3)
& $lesseq(0,bucket1(X4,X0)) )
=> good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) )
& ( ~ ( $lesseq(0,bucket1(X4,X0))
& $lesseq(bucket1(X4,X0),X3) )
=> ~ in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_resize) ).
tff(f111,negated_conjecture,
~ ! [X2: map_key_lpoption_a1rp,X0: $int,X1: map_int_lplist_lpkeycm_a1rprp] :
( ( ! [X3: $int] :
( ( $less(X3,X0)
& $lesseq(0,X3) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) )
& $less(0,X0)
& ! [X4: key1,X5: a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))
& $lesseq(0,X0) )
=> ( $lesseq(0,$sum($product(2,X0),1))
=> ( $lesseq(0,$sum($product(2,X0),1))
=> ! [X9: $int,X3: $int,X6: list_lpkeycm_a1rp,X10: map_int_lplist_lpkeycm_a1rprp,X8: map_key_lpoption_a1rp,X7: map_int_lplist_lpkeycm_a1rprp] :
( ( ! [X4: key1,X5: a1] :
( mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6))
=> ( bucket1(X4,X0) = X3 ) )
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)))
& ! [X12: $int] :
( ( $lesseq(0,X12)
& $less(X12,$sum($product(2,X0),1)) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)),X12) )
& $lesseq(0,X9)
& $less(0,X9)
& $lesseq(0,$sum($product(2,X0),1))
& ! [X11: $int] :
( ( $less(X11,X9)
& $lesseq(0,X11) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)),X11) )
& ! [X5: a1,X4: key1] :
( ( ~ ( $less(bucket1(X4,X0),X3)
& $lesseq(0,bucket1(X4,X0)) )
& ( ( ( bucket1(X4,X0) != X3 )
& ~ in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) )
| ( ( ( in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))
| mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) )
<=> ( tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X4))) = tb2t4(some(a,t2tb7(X5))) ) )
& ( bucket1(X4,X0) = X3 ) ) ) )
| ( $lesseq(0,bucket1(X4,X0))
& good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))
& $less(bucket1(X4,X0),X3) ) ) )
=> ( ( X6 = tb2t6(nil(tuple2(key,a))) )
=> ! [X5: a1,X4: key1] :
( ( ( $lesseq(bucket1(X4,X0),X3)
& $lesseq(0,bucket1(X4,X0)) )
=> good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) )
& ( ~ ( $lesseq(0,bucket1(X4,X0))
& $lesseq(bucket1(X4,X0),X3) )
=> ~ in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f110]) ).
tff(f118,plain,
~ ! [X2: map_key_lpoption_a1rp,X0: $int,X1: map_int_lplist_lpkeycm_a1rprp] :
( ( ! [X3: $int] :
( ( $less(X3,X0)
& ~ $less(X3,0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3) )
& $less(0,X0)
& ! [X4: key1,X5: a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))
& ~ $less(X0,0) )
=> ( ~ $less($sum($product(2,X0),1),0)
=> ( ~ $less($sum($product(2,X0),1),0)
=> ! [X9: $int,X3: $int,X6: list_lpkeycm_a1rp,X10: map_int_lplist_lpkeycm_a1rprp,X8: map_key_lpoption_a1rp,X7: map_int_lplist_lpkeycm_a1rprp] :
( ( ! [X4: key1,X5: a1] :
( mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6))
=> ( bucket1(X4,X0) = X3 ) )
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)))
& ! [X12: $int] :
( ( ~ $less(X12,0)
& $less(X12,$sum($product(2,X0),1)) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)),X12) )
& ~ $less(X9,0)
& $less(0,X9)
& ~ $less($sum($product(2,X0),1),0)
& ! [X11: $int] :
( ( $less(X11,X9)
& ~ $less(X11,0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)),X11) )
& ! [X5: a1,X4: key1] :
( ( ~ ( $less(bucket1(X4,X0),X3)
& ~ $less(bucket1(X4,X0),0) )
& ( ( ( bucket1(X4,X0) != X3 )
& ~ in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) )
| ( ( ( in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))
| mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) )
<=> ( tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X4))) = tb2t4(some(a,t2tb7(X5))) ) )
& ( bucket1(X4,X0) = X3 ) ) ) )
| ( ~ $less(bucket1(X4,X0),0)
& good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))
& $less(bucket1(X4,X0),X3) ) ) )
=> ( ( X6 = tb2t6(nil(tuple2(key,a))) )
=> ! [X5: a1,X4: key1] :
( ( ( ~ $less(X3,bucket1(X4,X0))
& ~ $less(bucket1(X4,X0),0) )
=> good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) )
& ( ~ ( ~ $less(bucket1(X4,X0),0)
& ~ $less(X3,bucket1(X4,X0)) )
=> ~ in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f111]) ).
tff(f120,plain,
! [X0: $int] :
( $less(0,X0)
=> ! [X1: key1] :
( $less(bucket1(X1,X0),X0)
& ~ $less(bucket1(X1,X0),0) ) ),
inference(theory_normalization,[],[f69]) ).
tff(f134,plain,
! [X0: $int] : ~ $less(X0,X0),
introduced(definition,[],[tha_non-reflexivity]) ).
tff(f135,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X0,X1)
| $less(X0,X2)
| ~ $less(X1,X2) ),
introduced(definition,[],[tha_transitivity]) ).
tff(f136,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( X0 = X1 )
| $less(X0,X1) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f154,plain,
! [X0: uni,X1: ty,X2: ty,X3: uni] : sort1(X2,get(X2,X1,X3,X0)),
inference(rectify,[],[f47]) ).
tff(f158,plain,
~ ! [X2: map_int_lplist_lpkeycm_a1rprp,X1: $int,X0: map_key_lpoption_a1rp] :
( ( ! [X3: $int] :
( ( ~ $less(X3,0)
& $less(X3,X1) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)),X3) )
& ~ $less(X1,0)
& $less(0,X1)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X1,t2tb2(X2))) )
=> ( ~ $less($sum($product(2,X1),1),0)
=> ( ~ $less($sum($product(2,X1),1),0)
=> ! [X11: map_int_lplist_lpkeycm_a1rprp,X6: $int,X7: $int,X10: map_key_lpoption_a1rp,X9: map_int_lplist_lpkeycm_a1rprp,X8: list_lpkeycm_a1rp] :
( ( ! [X15: key1,X14: a1] : good_data1(a,X15,t2tb7(X14),t2tb3(X10),mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)))
& ~ $less(X6,0)
& ! [X17: $int] :
( ( $less(X17,X6)
& ~ $less(X17,0) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)),X17) )
& ~ $less($sum($product(2,X1),1),0)
& ! [X16: $int] :
( ( ~ $less(X16,0)
& $less(X16,$sum($product(2,X1),1)) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)),X16) )
& ! [X18: a1,X19: key1] :
( ( $less(bucket1(X19,X1),X7)
& good_data1(a,X19,t2tb7(X18),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ~ $less(bucket1(X19,X1),0) )
| ( ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
| in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
<=> ( tb2t4(some(a,t2tb7(X18))) = tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) ) )
& ( bucket1(X19,X1) = X7 ) )
| ( ( bucket1(X19,X1) != X7 )
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ~ ( $less(bucket1(X19,X1),X7)
& ~ $less(bucket1(X19,X1),0) ) ) )
& ! [X12: key1,X13: a1] :
( mem(tuple2(key,a),tuple21(key,a,t2tb1(X12),t2tb7(X13)),t2tb6(X8))
=> ( bucket1(X12,X1) = X7 ) )
& $less(0,X6) )
=> ( ( tb2t6(nil(tuple2(key,a))) = X8 )
=> ! [X20: a1,X21: key1] :
( ( ~ ( ~ $less(bucket1(X21,X1),0)
& ~ $less(X7,bucket1(X21,X1)) )
=> ~ in_data1(a,X21,t2tb7(X20),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
& ( ( ~ $less(X7,bucket1(X21,X1))
& ~ $less(bucket1(X21,X1),0) )
=> good_data1(a,X21,t2tb7(X20),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) ) ) ) ) ) ),
inference(rectify,[],[f118]) ).
tff(f168,plain,
! [X0: uni,X1: ty] : sort1(option(X1),some(X1,X0)),
inference(rectify,[],[f27]) ).
tff(f174,plain,
! [X1: uni,X2: ty,X3: uni,X0: ty] : sort1(tuple2(X0,X2),tuple21(X0,X2,X1,X3)),
inference(rectify,[],[f70]) ).
tff(f184,plain,
! [X3: uni,X0: uni,X1: uni,X4: key1,X2: ty] :
( ( ( some(X2,X0) = get(option(X2),key,X1,t2tb1(X4)) )
<=> in_data1(X2,X4,X0,X3) )
<=> good_data1(X2,X4,X0,X1,X3) ),
inference(rectify,[],[f80]) ).
tff(f197,plain,
! [X0: uni,X1: ty] :
( sort1(X1,X0)
=> ( ! [X3: uni,X2: uni] :
( sort1(X1,X2)
=> ( ( mem(X1,X0,X3)
| ( X0 = X2 ) )
<=> mem(X1,X0,cons(X1,X2,X3)) ) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(rectify,[],[f46]) ).
tff(f238,plain,
! [X0: $int] :
( ! [X1: key1] :
( $less(bucket1(X1,X0),X0)
& ~ $less(bucket1(X1,X0),0) )
| ~ $less(0,X0) ),
inference(ennf_transformation,[],[f120]) ).
tff(f247,plain,
? [X2: map_int_lplist_lpkeycm_a1rprp,X1: $int,X0: map_key_lpoption_a1rp] :
( ? [X11: map_int_lplist_lpkeycm_a1rprp,X6: $int,X7: $int,X10: map_key_lpoption_a1rp,X9: map_int_lplist_lpkeycm_a1rprp,X8: list_lpkeycm_a1rp] :
( ? [X20: a1,X21: key1] :
( ( in_data1(a,X21,t2tb7(X20),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ( $less(X7,bucket1(X21,X1))
| $less(bucket1(X21,X1),0) ) )
| ( ~ good_data1(a,X21,t2tb7(X20),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ~ $less(X7,bucket1(X21,X1))
& ~ $less(bucket1(X21,X1),0) ) )
& ( tb2t6(nil(tuple2(key,a))) = X8 )
& ! [X15: key1,X14: a1] : good_data1(a,X15,t2tb7(X14),t2tb3(X10),mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)))
& ~ $less(X6,0)
& ! [X17: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)),X17)
| ~ $less(X17,X6)
| $less(X17,0) )
& ~ $less($sum($product(2,X1),1),0)
& ! [X16: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)),X16)
| $less(X16,0)
| ~ $less(X16,$sum($product(2,X1),1)) )
& ! [X18: a1,X19: key1] :
( ( $less(bucket1(X19,X1),X7)
& good_data1(a,X19,t2tb7(X18),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ~ $less(bucket1(X19,X1),0) )
| ( ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
| in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
<=> ( tb2t4(some(a,t2tb7(X18))) = tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) ) )
& ( bucket1(X19,X1) = X7 ) )
| ( ( bucket1(X19,X1) != X7 )
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ( ~ $less(bucket1(X19,X1),X7)
| $less(bucket1(X19,X1),0) ) ) )
& ! [X12: key1,X13: a1] :
( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X12),t2tb7(X13)),t2tb6(X8))
| ( bucket1(X12,X1) = X7 ) )
& $less(0,X6) )
& ~ $less($sum($product(2,X1),1),0)
& ~ $less($sum($product(2,X1),1),0)
& ! [X3: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)),X3)
| $less(X3,0)
| ~ $less(X3,X1) )
& ~ $less(X1,0)
& $less(0,X1)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X1,t2tb2(X2))) ),
inference(ennf_transformation,[],[f158]) ).
tff(f248,plain,
? [X1: $int,X0: map_key_lpoption_a1rp,X2: map_int_lplist_lpkeycm_a1rprp] :
( ~ $less(X1,0)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)))
& ~ $less($sum($product(2,X1),1),0)
& ? [X8: list_lpkeycm_a1rp,X9: map_int_lplist_lpkeycm_a1rprp,X7: $int,X10: map_key_lpoption_a1rp,X6: $int,X11: map_int_lplist_lpkeycm_a1rprp] :
( ! [X12: key1,X13: a1] :
( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X12),t2tb7(X13)),t2tb6(X8))
| ( bucket1(X12,X1) = X7 ) )
& ! [X18: a1,X19: key1] :
( ( $less(bucket1(X19,X1),X7)
& good_data1(a,X19,t2tb7(X18),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ~ $less(bucket1(X19,X1),0) )
| ( ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
| in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
<=> ( tb2t4(some(a,t2tb7(X18))) = tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) ) )
& ( bucket1(X19,X1) = X7 ) )
| ( ( bucket1(X19,X1) != X7 )
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ( ~ $less(bucket1(X19,X1),X7)
| $less(bucket1(X19,X1),0) ) ) )
& ! [X15: key1,X14: a1] : good_data1(a,X15,t2tb7(X14),t2tb3(X10),mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)))
& ? [X20: a1,X21: key1] :
( ( ~ $less(X7,bucket1(X21,X1))
& ~ $less(bucket1(X21,X1),0)
& ~ good_data1(a,X21,t2tb7(X20),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
| ( in_data1(a,X21,t2tb7(X20),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ( $less(X7,bucket1(X21,X1))
| $less(bucket1(X21,X1),0) ) ) )
& ( tb2t6(nil(tuple2(key,a))) = X8 )
& ~ $less($sum($product(2,X1),1),0)
& ! [X16: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)),X16)
| $less(X16,0)
| ~ $less(X16,$sum($product(2,X1),1)) )
& $less(0,X6)
& ~ $less(X6,0)
& ! [X17: $int] :
( $less(X17,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)),X17)
| ~ $less(X17,X6) ) )
& $less(0,X1)
& ~ $less($sum($product(2,X1),1),0)
& ! [X3: $int] :
( $less(X3,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)),X3)
| ~ $less(X3,X1) ) ),
inference(flattening,[],[f247]) ).
tff(f255,plain,
! [X1: ty,X0: uni] :
( ( ! [X2: uni,X3: uni] :
( ~ sort1(X1,X2)
| ( ( mem(X1,X0,X3)
| ( X0 = X2 ) )
<=> mem(X1,X0,cons(X1,X2,X3)) ) )
& ~ mem(X1,X0,nil(X1)) )
| ~ sort1(X1,X0) ),
inference(ennf_transformation,[],[f197]) ).
tff(f256,plain,
! [X0: uni] :
( ~ sort1(option(a),X0)
| ( t2tb4(tb2t4(X0)) = X0 ) ),
inference(ennf_transformation,[],[f97]) ).
tff(f260,plain,
! [X0: uni,X1: ty,X2: uni,X3: ty] : sort1(tuple2(X3,X1),tuple21(X3,X1,X0,X2)),
inference(rectify,[],[f174]) ).
tff(f283,plain,
! [X3: uni,X0: uni,X1: uni,X4: key1,X2: ty] :
( ( ( ( ( some(X2,X0) = get(option(X2),key,X1,t2tb1(X4)) )
| ~ in_data1(X2,X4,X0,X3) )
& ( in_data1(X2,X4,X0,X3)
| ( some(X2,X0) != get(option(X2),key,X1,t2tb1(X4)) ) ) )
| ~ good_data1(X2,X4,X0,X1,X3) )
& ( good_data1(X2,X4,X0,X1,X3)
| ( ( ~ in_data1(X2,X4,X0,X3)
| ( some(X2,X0) != get(option(X2),key,X1,t2tb1(X4)) ) )
& ( in_data1(X2,X4,X0,X3)
| ( some(X2,X0) = get(option(X2),key,X1,t2tb1(X4)) ) ) ) ) ),
inference(nnf_transformation,[],[f184]) ).
tff(f284,plain,
! [X0: uni,X1: uni,X2: uni,X3: key1,X4: ty] :
( ( ( ( ( get(option(X4),key,X2,t2tb1(X3)) = some(X4,X1) )
| ~ in_data1(X4,X3,X1,X0) )
& ( in_data1(X4,X3,X1,X0)
| ( get(option(X4),key,X2,t2tb1(X3)) != some(X4,X1) ) ) )
| ~ good_data1(X4,X3,X1,X2,X0) )
& ( good_data1(X4,X3,X1,X2,X0)
| ( ( ~ in_data1(X4,X3,X1,X0)
| ( get(option(X4),key,X2,t2tb1(X3)) != some(X4,X1) ) )
& ( in_data1(X4,X3,X1,X0)
| ( get(option(X4),key,X2,t2tb1(X3)) = some(X4,X1) ) ) ) ) ),
inference(rectify,[],[f283]) ).
tff(f293,plain,
? [X1: $int,X0: map_key_lpoption_a1rp,X2: map_int_lplist_lpkeycm_a1rprp] :
( ~ $less(X1,0)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)))
& ~ $less($sum($product(2,X1),1),0)
& ? [X8: list_lpkeycm_a1rp,X9: map_int_lplist_lpkeycm_a1rprp,X7: $int,X10: map_key_lpoption_a1rp,X6: $int,X11: map_int_lplist_lpkeycm_a1rprp] :
( ! [X12: key1,X13: a1] :
( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X12),t2tb7(X13)),t2tb6(X8))
| ( bucket1(X12,X1) = X7 ) )
& ! [X18: a1,X19: key1] :
( ( $less(bucket1(X19,X1),X7)
& good_data1(a,X19,t2tb7(X18),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ~ $less(bucket1(X19,X1),0) )
| ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
| in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
| ( tb2t4(some(a,t2tb7(X18))) != tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) ) )
& ( ( tb2t4(some(a,t2tb7(X18))) = tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) )
| ( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ( bucket1(X19,X1) = X7 ) )
| ( ( bucket1(X19,X1) != X7 )
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ( ~ $less(bucket1(X19,X1),X7)
| $less(bucket1(X19,X1),0) ) ) )
& ! [X15: key1,X14: a1] : good_data1(a,X15,t2tb7(X14),t2tb3(X10),mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)))
& ? [X20: a1,X21: key1] :
( ( ~ $less(X7,bucket1(X21,X1))
& ~ $less(bucket1(X21,X1),0)
& ~ good_data1(a,X21,t2tb7(X20),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
| ( in_data1(a,X21,t2tb7(X20),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ( $less(X7,bucket1(X21,X1))
| $less(bucket1(X21,X1),0) ) ) )
& ( tb2t6(nil(tuple2(key,a))) = X8 )
& ~ $less($sum($product(2,X1),1),0)
& ! [X16: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)),X16)
| $less(X16,0)
| ~ $less(X16,$sum($product(2,X1),1)) )
& $less(0,X6)
& ~ $less(X6,0)
& ! [X17: $int] :
( $less(X17,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)),X17)
| ~ $less(X17,X6) ) )
& $less(0,X1)
& ~ $less($sum($product(2,X1),1),0)
& ! [X3: $int] :
( $less(X3,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)),X3)
| ~ $less(X3,X1) ) ),
inference(nnf_transformation,[],[f248]) ).
tff(f294,plain,
? [X1: $int,X0: map_key_lpoption_a1rp,X2: map_int_lplist_lpkeycm_a1rprp] :
( ~ $less(X1,0)
& ! [X5: a1,X4: key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)))
& ~ $less($sum($product(2,X1),1),0)
& ? [X8: list_lpkeycm_a1rp,X9: map_int_lplist_lpkeycm_a1rprp,X7: $int,X10: map_key_lpoption_a1rp,X6: $int,X11: map_int_lplist_lpkeycm_a1rprp] :
( ! [X12: key1,X13: a1] :
( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X12),t2tb7(X13)),t2tb6(X8))
| ( bucket1(X12,X1) = X7 ) )
& ! [X18: a1,X19: key1] :
( ( $less(bucket1(X19,X1),X7)
& good_data1(a,X19,t2tb7(X18),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ~ $less(bucket1(X19,X1),0) )
| ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
| in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
| ( tb2t4(some(a,t2tb7(X18))) != tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) ) )
& ( ( tb2t4(some(a,t2tb7(X18))) = tb2t4(get(option(a),key,t2tb3(X10),t2tb1(X19))) )
| ( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X8))
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ( bucket1(X19,X1) = X7 ) )
| ( ( bucket1(X19,X1) != X7 )
& ~ in_data1(a,X19,t2tb7(X18),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) ) )
& ( ~ $less(bucket1(X19,X1),X7)
| $less(bucket1(X19,X1),0) ) ) )
& ! [X15: key1,X14: a1] : good_data1(a,X15,t2tb7(X14),t2tb3(X10),mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)))
& ? [X20: a1,X21: key1] :
( ( ~ $less(X7,bucket1(X21,X1))
& ~ $less(bucket1(X21,X1),0)
& ~ good_data1(a,X21,t2tb7(X20),t2tb3(X10),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11))) )
| ( in_data1(a,X21,t2tb7(X20),mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)))
& ( $less(X7,bucket1(X21,X1))
| $less(bucket1(X21,X1),0) ) ) )
& ( tb2t6(nil(tuple2(key,a))) = X8 )
& ~ $less($sum($product(2,X1),1),0)
& ! [X16: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X1),1),t2tb2(X11)),X16)
| $less(X16,0)
| ~ $less(X16,$sum($product(2,X1),1)) )
& $less(0,X6)
& ~ $less(X6,0)
& ! [X17: $int] :
( $less(X17,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X6,t2tb2(X9)),X17)
| ~ $less(X17,X6) ) )
& $less(0,X1)
& ~ $less($sum($product(2,X1),1),0)
& ! [X3: $int] :
( $less(X3,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X1,t2tb2(X2)),X3)
| ~ $less(X3,X1) ) ),
inference(flattening,[],[f293]) ).
tff(f295,plain,
? [X0: $int,X1: map_key_lpoption_a1rp,X2: map_int_lplist_lpkeycm_a1rprp] :
( ~ $less(X0,0)
& ! [X3: a1,X4: key1] : good_data1(a,X4,t2tb7(X3),t2tb3(X1),mk_array1(list(tuple2(key,a)),X0,t2tb2(X2)))
& ~ $less($sum($product(2,X0),1),0)
& ? [X5: list_lpkeycm_a1rp,X6: map_int_lplist_lpkeycm_a1rprp,X7: $int,X8: map_key_lpoption_a1rp,X9: $int,X10: map_int_lplist_lpkeycm_a1rprp] :
( ! [X11: key1,X12: a1] :
( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X11),t2tb7(X12)),t2tb6(X5))
| ( bucket1(X11,X0) = X7 ) )
& ! [X13: a1,X14: key1] :
( ( $less(bucket1(X14,X0),X7)
& good_data1(a,X14,t2tb7(X13),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10)))
& ~ $less(bucket1(X14,X0),0) )
| ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X13)),t2tb6(X5))
| in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10)))
| ( tb2t4(some(a,t2tb7(X13))) != tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X14))) ) )
& ( ( tb2t4(some(a,t2tb7(X13))) = tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X14))) )
| ( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X13)),t2tb6(X5))
& ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10))) ) )
& ( bucket1(X14,X0) = X7 ) )
| ( ( bucket1(X14,X0) != X7 )
& ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10))) ) )
& ( ~ $less(bucket1(X14,X0),X7)
| $less(bucket1(X14,X0),0) ) ) )
& ! [X15: key1,X16: a1] : good_data1(a,X15,t2tb7(X16),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X6)))
& ? [X17: a1,X18: key1] :
( ( ~ $less(X7,bucket1(X18,X0))
& ~ $less(bucket1(X18,X0),0)
& ~ good_data1(a,X18,t2tb7(X17),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10))) )
| ( in_data1(a,X18,t2tb7(X17),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10)))
& ( $less(X7,bucket1(X18,X0))
| $less(bucket1(X18,X0),0) ) ) )
& ( tb2t6(nil(tuple2(key,a))) = X5 )
& ~ $less($sum($product(2,X0),1),0)
& ! [X19: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X10)),X19)
| $less(X19,0)
| ~ $less(X19,$sum($product(2,X0),1)) )
& $less(0,X9)
& ~ $less(X9,0)
& ! [X20: $int] :
( $less(X20,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X6)),X20)
| ~ $less(X20,X9) ) )
& $less(0,X0)
& ~ $less($sum($product(2,X0),1),0)
& ! [X21: $int] :
( $less(X21,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X2)),X21)
| ~ $less(X21,X0) ) ),
inference(rectify,[],[f294]) ).
tff(f296,plain,
( ~ $less(sK2,0)
& ! [X3: a1,X4: key1] : good_data1(a,X4,t2tb7(X3),t2tb3(sK3),mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK4)))
& ~ $less($sum($product(2,sK2),1),0)
& ! [X11: key1,X12: a1] :
( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X11),t2tb7(X12)),t2tb6(sK5))
| ( bucket1(X11,sK2) = sK7 ) )
& ! [X13: a1,X14: key1] :
( ( $less(bucket1(X14,sK2),sK7)
& good_data1(a,X14,t2tb7(X13),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
& ~ $less(bucket1(X14,sK2),0) )
| ( ( ( ( mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X13)),t2tb6(sK5))
| in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
| ( tb2t4(some(a,t2tb7(X13))) != tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) ) )
& ( ( tb2t4(some(a,t2tb7(X13))) = tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) )
| ( ~ mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X13)),t2tb6(sK5))
& ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10))) ) )
& ( bucket1(X14,sK2) = sK7 ) )
| ( ( bucket1(X14,sK2) != sK7 )
& ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10))) ) )
& ( ~ $less(bucket1(X14,sK2),sK7)
| $less(bucket1(X14,sK2),0) ) ) )
& ! [X15: key1,X16: a1] : good_data1(a,X15,t2tb7(X16),t2tb3(sK8),mk_array1(list(tuple2(key,a)),sK9,t2tb2(sK6)))
& ( ( ~ $less(sK7,bucket1(sK12,sK2))
& ~ $less(bucket1(sK12,sK2),0)
& ~ good_data1(a,sK12,t2tb7(sK11),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10))) )
| ( in_data1(a,sK12,t2tb7(sK11),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
& ( $less(sK7,bucket1(sK12,sK2))
| $less(bucket1(sK12,sK2),0) ) ) )
& ( tb2t6(nil(tuple2(key,a))) = sK5 )
& ~ $less($sum($product(2,sK2),1),0)
& ! [X19: $int] :
( good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)),X19)
| $less(X19,0)
| ~ $less(X19,$sum($product(2,sK2),1)) )
& $less(0,sK9)
& ~ $less(sK9,0)
& ! [X20: $int] :
( $less(X20,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),sK9,t2tb2(sK6)),X20)
| ~ $less(X20,sK9) )
& $less(0,sK2)
& ~ $less($sum($product(2,sK2),1),0)
& ! [X21: $int] :
( $less(X21,0)
| good_hash1(a,mk_array1(list(tuple2(key,a)),sK2,t2tb2(sK4)),X21)
| ~ $less(X21,sK2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X9,sK9),skolemize(X10,sK10),skolemize(X17,sK11),skolemize(X18,sK12)],[f295]) ).
tff(f297,plain,
! [X1: ty,X0: uni] :
( ( ! [X2: uni,X3: uni] :
( ~ sort1(X1,X2)
| ( ( mem(X1,X0,X3)
| ( X0 = X2 )
| ~ mem(X1,X0,cons(X1,X2,X3)) )
& ( mem(X1,X0,cons(X1,X2,X3))
| ( ~ mem(X1,X0,X3)
& ( X0 != X2 ) ) ) ) )
& ~ mem(X1,X0,nil(X1)) )
| ~ sort1(X1,X0) ),
inference(nnf_transformation,[],[f255]) ).
tff(f298,plain,
! [X1: ty,X0: uni] :
( ( ! [X2: uni,X3: uni] :
( ~ sort1(X1,X2)
| ( ( mem(X1,X0,X3)
| ( X0 = X2 )
| ~ mem(X1,X0,cons(X1,X2,X3)) )
& ( mem(X1,X0,cons(X1,X2,X3))
| ( ~ mem(X1,X0,X3)
& ( X0 != X2 ) ) ) ) )
& ~ mem(X1,X0,nil(X1)) )
| ~ sort1(X1,X0) ),
inference(flattening,[],[f297]) ).
tff(f299,plain,
! [X0: ty,X1: uni] :
( ( ! [X2: uni,X3: uni] :
( ~ sort1(X0,X2)
| ( ( mem(X0,X1,X3)
| ( X1 = X2 )
| ~ mem(X0,X1,cons(X0,X2,X3)) )
& ( mem(X0,X1,cons(X0,X2,X3))
| ( ~ mem(X0,X1,X3)
& ( X1 != X2 ) ) ) ) )
& ~ mem(X0,X1,nil(X0)) )
| ~ sort1(X0,X1) ),
inference(rectify,[],[f298]) ).
tff(f317,plain,
! [X2: uni,X3: ty,X0: uni,X1: ty] : sort1(tuple2(X3,X1),tuple21(X3,X1,X0,X2)),
inference(cnf_transformation,[],[f260]) ).
tff(f344,plain,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
inference(cnf_transformation,[],[f103]) ).
tff(f354,plain,
! [X0: $int,X1: key1] :
( ~ $less(bucket1(X1,X0),0)
| ~ $less(0,X0) ),
inference(cnf_transformation,[],[f238]) ).
tff(f359,plain,
! [X0: uni,X1: ty] : sort1(option(X1),some(X1,X0)),
inference(cnf_transformation,[],[f168]) ).
tff(f369,plain,
! [X2: uni,X3: key1,X0: uni,X1: uni,X4: ty] :
( in_data1(X4,X3,X1,X0)
| good_data1(X4,X3,X1,X2,X0)
| ( get(option(X4),key,X2,t2tb1(X3)) = some(X4,X1) ) ),
inference(cnf_transformation,[],[f284]) ).
tff(f370,plain,
! [X2: uni,X3: key1,X0: uni,X1: uni,X4: ty] :
( good_data1(X4,X3,X1,X2,X0)
| ~ in_data1(X4,X3,X1,X0)
| ( get(option(X4),key,X2,t2tb1(X3)) != some(X4,X1) ) ),
inference(cnf_transformation,[],[f284]) ).
tff(f376,plain,
! [X2: ty,X3: uni,X0: uni,X1: ty] : sort1(X2,get(X2,X1,X3,X0)),
inference(cnf_transformation,[],[f154]) ).
tff(f390,plain,
! [X0: uni] :
( ( t2tb4(tb2t4(X0)) = X0 )
| ~ sort1(option(a),X0) ),
inference(cnf_transformation,[],[f256]) ).
tff(f399,plain,
$less(0,sK2),
inference(cnf_transformation,[],[f296]) ).
tff(f405,plain,
tb2t6(nil(tuple2(key,a))) = sK5,
inference(cnf_transformation,[],[f296]) ).
tff(f406,plain,
( ~ good_data1(a,sK12,t2tb7(sK11),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
| $less(sK7,bucket1(sK12,sK2))
| $less(bucket1(sK12,sK2),0) ),
inference(cnf_transformation,[],[f296]) ).
tff(f411,plain,
( ~ $less(sK7,bucket1(sK12,sK2))
| in_data1(a,sK12,t2tb7(sK11),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10))) ),
inference(cnf_transformation,[],[f296]) ).
tff(f422,plain,
! [X14: key1,X13: a1] :
( good_data1(a,X14,t2tb7(X13),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
| ~ $less(bucket1(X14,sK2),sK7)
| $less(bucket1(X14,sK2),0) ),
inference(cnf_transformation,[],[f296]) ).
tff(f425,plain,
! [X14: key1,X13: a1] :
( good_data1(a,X14,t2tb7(X13),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
| ( tb2t4(some(a,t2tb7(X13))) = tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) )
| ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
| ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10))) ),
inference(cnf_transformation,[],[f296]) ).
tff(f432,plain,
! [X14: key1,X13: a1] :
( $less(bucket1(X14,sK2),sK7)
| ( bucket1(X14,sK2) = sK7 )
| ~ in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10))) ),
inference(cnf_transformation,[],[f296]) ).
tff(f439,plain,
! [X14: key1,X13: a1] :
( $less(bucket1(X14,sK2),sK7)
| mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X13)),t2tb6(sK5))
| in_data1(a,X14,t2tb7(X13),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK10)))
| ( tb2t4(some(a,t2tb7(X13))) != tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) )
| ( bucket1(X14,sK2) != sK7 ) ),
inference(cnf_transformation,[],[f296]) ).
tff(f447,plain,
! [X0: ty,X1: uni] :
( ~ mem(X0,X1,nil(X0))
| ~ sort1(X0,X1) ),
inference(cnf_transformation,[],[f299]) ).
tff(f493,definition,
sF14 = tuple2(key,a),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f494,plain,
tuple2(key,a) = sF14,
inference(reorient_equations,[],[f493]) ).
tff(f495,definition,
sF15 = list(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f499,definition,
sF18 = $product(2,sK2),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f500,plain,
$product(2,sK2) = sF18,
inference(reorient_equations,[],[f499]) ).
tff(f501,definition,
sF19 = $sum(sF18,1),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f503,definition,
! [X11: key1,X12: a1] : ( sF20(X11,X12) = tuple21(key,a,t2tb1(X11),t2tb7(X12)) ),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f504,definition,
sF21 = t2tb6(sK5),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f505,plain,
t2tb6(sK5) = sF21,
inference(reorient_equations,[],[f504]) ).
tff(f506,definition,
! [X11: key1] : ( sF22(X11) = bucket1(X11,sK2) ),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f508,definition,
sF23 = t2tb2(sK10),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f509,definition,
sF24 = mk_array1(sF15,sF19,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f510,plain,
mk_array1(sF15,sF19,sF23) = sF24,
inference(reorient_equations,[],[f509]) ).
tff(f511,definition,
! [X13: a1] : ( sF25(X13) = some(a,t2tb7(X13)) ),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f512,plain,
! [X13: a1] : ( some(a,t2tb7(X13)) = sF25(X13) ),
inference(reorient_equations,[],[f511]) ).
tff(f513,definition,
! [X13: a1] : ( sF26(X13) = tb2t4(sF25(X13)) ),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f514,definition,
sF27 = option(a),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f515,plain,
option(a) = sF27,
inference(reorient_equations,[],[f514]) ).
tff(f516,definition,
sF28 = t2tb3(sK8),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f517,plain,
t2tb3(sK8) = sF28,
inference(reorient_equations,[],[f516]) ).
tff(f518,definition,
! [X14: key1] : ( sF29(X14) = get(sF27,key,sF28,t2tb1(X14)) ),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f519,definition,
! [X14: key1] : ( sF30(X14) = tb2t4(sF29(X14)) ),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f520,plain,
! [X14: key1,X13: a1] :
( mem(sF14,sF20(X14,X13),sF21)
| ( sF30(X14) != sF26(X13) )
| ( sK7 != sF22(X14) )
| $less(sF22(X14),sK7)
| in_data1(a,X14,t2tb7(X13),sF24) ),
inference(definition_folding,[],[f439,f506,f519,f518,f517,f515,f513,f512,f510,f508,f501,f500,f495,f494,f505,f503,f494,f506]) ).
tff(f527,plain,
! [X14: key1,X13: a1] :
( $less(sF22(X14),sK7)
| ~ in_data1(a,X14,t2tb7(X13),sF24)
| ( sK7 = sF22(X14) ) ),
inference(definition_folding,[],[f432,f510,f508,f501,f500,f495,f494,f506,f506]) ).
tff(f534,plain,
! [X14: key1,X13: a1] :
( ( sF30(X14) = sF26(X13) )
| good_data1(a,X14,t2tb7(X13),sF28,sF24)
| ~ in_data1(a,X14,t2tb7(X13),sF24)
| ~ in_data1(a,X14,t2tb7(X13),sF24) ),
inference(definition_folding,[],[f425,f510,f508,f501,f500,f495,f494,f510,f508,f501,f500,f495,f494,f519,f518,f517,f515,f513,f512,f510,f508,f501,f500,f495,f494,f517]) ).
tff(f537,plain,
! [X14: key1,X13: a1] :
( good_data1(a,X14,t2tb7(X13),sF28,sF24)
| $less(sF22(X14),0)
| ~ $less(sF22(X14),sK7) ),
inference(definition_folding,[],[f422,f506,f506,f510,f508,f501,f500,f495,f494,f517]) ).
tff(f551,definition,
sF33 = bucket1(sK12,sK2),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f552,definition,
sF34 = t2tb7(sK11),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f553,plain,
( ~ $less(sK7,sF33)
| in_data1(a,sK12,sF34,sF24) ),
inference(definition_folding,[],[f411,f510,f508,f501,f500,f495,f494,f552,f551]) ).
tff(f558,plain,
( $less(sF33,0)
| ~ good_data1(a,sK12,sF34,sF28,sF24)
| $less(sK7,sF33) ),
inference(definition_folding,[],[f406,f551,f551,f510,f508,f501,f500,f495,f494,f517,f552]) ).
tff(f559,definition,
sF35 = nil(sF14),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f560,plain,
nil(sF14) = sF35,
inference(reorient_equations,[],[f559]) ).
tff(f561,definition,
sF36 = tb2t6(sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
tff(f562,plain,
tb2t6(sF35) = sF36,
inference(reorient_equations,[],[f561]) ).
tff(f563,plain,
sF36 = sK5,
inference(definition_folding,[],[f405,f562,f560,f494]) ).
tff(f569,plain,
! [X14: key1,X13: a1] :
( good_data1(a,X14,t2tb7(X13),sF28,sF24)
| ( sF30(X14) = sF26(X13) )
| ~ in_data1(a,X14,t2tb7(X13),sF24) ),
inference(duplicate_literal_removal,[],[f534]) ).
tff(f575,definition,
( spl37_1
<=> $less(sK7,sF33) ),
introduced(definition,[new_symbols(definition,[spl37_1])],[avatar_definition]) ).
tff(f576,plain,
( $less(sK7,sF33)
| ~ spl37_1 ),
inference(avatar_component_clause,[],[f575]) ).
tff(f577,plain,
( ~ $less(sK7,sF33)
| spl37_1 ),
inference(avatar_component_clause,[],[f575]) ).
tff(f579,definition,
( spl37_2
<=> in_data1(a,sK12,sF34,sF24) ),
introduced(definition,[new_symbols(definition,[spl37_2])],[avatar_definition]) ).
tff(f580,plain,
( ~ in_data1(a,sK12,sF34,sF24)
| spl37_2 ),
inference(avatar_component_clause,[],[f579]) ).
tff(f581,plain,
( in_data1(a,sK12,sF34,sF24)
| ~ spl37_2 ),
inference(avatar_component_clause,[],[f579]) ).
tff(f582,plain,
( ~ spl37_1
| spl37_2 ),
inference(avatar_split_clause,[],[f553,f579,f575]) ).
tff(f586,definition,
( spl37_3
<=> $less(sF33,0) ),
introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition]) ).
tff(f587,plain,
( $less(sF33,0)
| ~ spl37_3 ),
inference(avatar_component_clause,[],[f586]) ).
tff(f588,plain,
( ~ $less(sF33,0)
| spl37_3 ),
inference(avatar_component_clause,[],[f586]) ).
tff(f593,plain,
tb2t6(sF35) = sK5,
inference(forward_demodulation,[],[f562,f563]) ).
tff(f595,plain,
t2tb6(sK5) = sF35,
inference(superposition,[],[f344,f593]) ).
tff(f596,plain,
sF21 = sF35,
inference(superposition,[],[f595,f505]) ).
tff(f616,definition,
( spl37_4
<=> good_data1(a,sK12,sF34,sF28,sF24) ),
introduced(definition,[new_symbols(definition,[spl37_4])],[avatar_definition]) ).
tff(f617,plain,
( good_data1(a,sK12,sF34,sF28,sF24)
| ~ spl37_4 ),
inference(avatar_component_clause,[],[f616]) ).
tff(f618,plain,
( ~ good_data1(a,sK12,sF34,sF28,sF24)
| spl37_4 ),
inference(avatar_component_clause,[],[f616]) ).
tff(f627,plain,
sF33 = sF22(sK12),
inference(superposition,[],[f506,f551]) ).
tff(f629,plain,
! [X0: a1] :
( $less(sF33,sK7)
| ~ in_data1(a,sK12,t2tb7(X0),sF24)
| ( sF33 = sK7 ) ),
inference(superposition,[],[f527,f627]) ).
tff(f631,definition,
( spl37_5
<=> ( sF33 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition]) ).
tff(f633,plain,
( ( sF33 = sK7 )
| ~ spl37_5 ),
inference(avatar_component_clause,[],[f631]) ).
tff(f635,definition,
( spl37_6
<=> ! [X0: a1] : ~ in_data1(a,sK12,t2tb7(X0),sF24) ),
introduced(definition,[new_symbols(definition,[spl37_6])],[avatar_definition]) ).
tff(f636,plain,
( ! [X0: a1] : ~ in_data1(a,sK12,t2tb7(X0),sF24)
| ~ spl37_6 ),
inference(avatar_component_clause,[],[f635]) ).
tff(f638,definition,
( spl37_7
<=> $less(sF33,sK7) ),
introduced(definition,[new_symbols(definition,[spl37_7])],[avatar_definition]) ).
tff(f639,plain,
( ~ $less(sF33,sK7)
| spl37_7 ),
inference(avatar_component_clause,[],[f638]) ).
tff(f640,plain,
( $less(sF33,sK7)
| ~ spl37_7 ),
inference(avatar_component_clause,[],[f638]) ).
tff(f641,plain,
( spl37_5
| spl37_6
| spl37_7 ),
inference(avatar_split_clause,[],[f629,f638,f635,f631]) ).
tff(f661,plain,
sF25(sK11) = some(a,sF34),
inference(superposition,[],[f512,f552]) ).
tff(f664,plain,
! [X0: a1] : sort1(option(a),sF25(X0)),
inference(superposition,[],[f359,f512]) ).
tff(f665,plain,
! [X0: a1] : sort1(sF27,sF25(X0)),
inference(forward_demodulation,[],[f664,f515]) ).
tff(f666,plain,
! [X0: key1] :
( $less(sF22(X0),0)
| good_data1(a,X0,sF34,sF28,sF24)
| ~ $less(sF22(X0),sK7) ),
inference(superposition,[],[f537,f552]) ).
tff(f687,plain,
( ~ $less(0,sK2)
| ~ $less(sF33,0) ),
inference(superposition,[],[f354,f551]) ).
tff(f688,plain,
! [X0: key1] :
( ~ $less(0,sK2)
| ~ $less(sF22(X0),0) ),
inference(superposition,[],[f354,f506]) ).
tff(f689,plain,
! [X0: key1] : ~ $less(sF22(X0),0),
inference(forward_subsumption_resolution,[],[f688,f399]) ).
tff(f699,plain,
! [X0: uni] :
( ~ mem(sF14,X0,sF35)
| ~ sort1(sF14,X0) ),
inference(superposition,[],[f447,f560]) ).
tff(f705,plain,
! [X0: key1] :
( good_data1(a,X0,sF34,sF28,sF24)
| ( sF26(sK11) = sF30(X0) )
| ~ in_data1(a,X0,sF34,sF24) ),
inference(superposition,[],[f569,f552]) ).
tff(f738,plain,
! [X0: uni] :
( ( t2tb4(tb2t4(X0)) = X0 )
| ~ sort1(sF27,X0) ),
inference(forward_demodulation,[],[f390,f515]) ).
tff(f739,plain,
! [X0: a1] :
( ( t2tb4(sF26(X0)) = sF25(X0) )
| ~ sort1(sF27,sF25(X0)) ),
inference(superposition,[],[f738,f513]) ).
tff(f740,plain,
! [X0: key1] :
( ( t2tb4(sF30(X0)) = sF29(X0) )
| ~ sort1(sF27,sF29(X0)) ),
inference(superposition,[],[f738,f519]) ).
tff(f742,plain,
! [X0: a1] : ( t2tb4(sF26(X0)) = sF25(X0) ),
inference(forward_subsumption_resolution,[],[f739,f665]) ).
tff(f768,plain,
! [X0: key1] : sort1(sF27,sF29(X0)),
inference(superposition,[],[f376,f518]) ).
tff(f787,plain,
~ $less(sF33,0),
inference(forward_subsumption_resolution,[],[f687,f399]) ).
tff(f866,plain,
! [X0: key1,X1: a1] : sort1(tuple2(key,a),sF20(X0,X1)),
inference(superposition,[],[f317,f503]) ).
tff(f867,plain,
! [X0: key1,X1: a1] : sort1(sF14,sF20(X0,X1)),
inference(forward_demodulation,[],[f866,f494]) ).
tff(f884,plain,
! [X14: key1,X13: a1] :
( ( sK7 != sF22(X14) )
| $less(sF22(X14),sK7)
| in_data1(a,X14,t2tb7(X13),sF24)
| ( sF30(X14) != sF26(X13) )
| mem(sF14,sF20(X14,X13),sF35) ),
inference(forward_demodulation,[],[f520,f596]) ).
tff(f999,plain,
( ~ in_data1(a,sK12,sF34,sF24)
| ( get(option(a),key,sF28,t2tb1(sK12)) != some(a,sF34) )
| spl37_4 ),
inference(resolution,[],[f370,f618]) ).
tff(f1000,plain,
( ( get(option(a),key,sF28,t2tb1(sK12)) != some(a,sF34) )
| ~ spl37_2
| spl37_4 ),
inference(forward_subsumption_resolution,[],[f999,f581]) ).
tff(f1001,plain,
( ( get(sF27,key,sF28,t2tb1(sK12)) != some(a,sF34) )
| ~ spl37_2
| spl37_4 ),
inference(forward_demodulation,[],[f1000,f515]) ).
tff(f1002,plain,
( ( sF29(sK12) != some(a,sF34) )
| ~ spl37_2
| spl37_4 ),
inference(forward_demodulation,[],[f1001,f518]) ).
tff(f1055,plain,
! [X0: key1] :
( good_data1(a,X0,sF34,sF28,sF24)
| ~ $less(sF22(X0),sK7) ),
inference(forward_subsumption_resolution,[],[f666,f689]) ).
tff(f1096,plain,
( ~ in_data1(a,sK12,sF34,sF24)
| ( sF26(sK11) = sF30(sK12) )
| spl37_4 ),
inference(resolution,[],[f705,f618]) ).
tff(f1097,plain,
( ( sF26(sK11) = sF30(sK12) )
| ~ spl37_2
| spl37_4 ),
inference(forward_subsumption_resolution,[],[f1096,f581]) ).
tff(f1248,plain,
! [X0: a1] :
( ( sF33 != sK7 )
| mem(sF14,sF20(sK12,X0),sF35)
| ( sF26(X0) != sF30(sK12) )
| in_data1(a,sK12,t2tb7(X0),sF24)
| $less(sF33,sK7) ),
inference(superposition,[],[f884,f627]) ).
tff(f1254,plain,
( ~ $less(sF22(sK12),sK7)
| spl37_4 ),
inference(resolution,[],[f1055,f618]) ).
tff(f1257,plain,
( ~ $less(sF33,sK7)
| spl37_4 ),
inference(forward_demodulation,[],[f1254,f627]) ).
tff(f1292,plain,
( $false
| ~ spl37_3 ),
inference(forward_subsumption_resolution,[],[f787,f587]) ).
tff(f1293,plain,
~ spl37_3,
inference(avatar_contradiction_clause,[],[f1292]) ).
tff(f1330,plain,
( $false
| spl37_4
| ~ spl37_7 ),
inference(forward_subsumption_resolution,[],[f1257,f640]) ).
tff(f1331,plain,
( spl37_4
| ~ spl37_7 ),
inference(avatar_contradiction_clause,[],[f1330]) ).
tff(f1334,plain,
( $less(sF33,0)
| ~ good_data1(a,sK12,sF34,sF28,sF24)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f558,f577]) ).
tff(f1337,plain,
( ~ good_data1(a,sK12,sF34,sF28,sF24)
| spl37_1
| spl37_3 ),
inference(forward_subsumption_resolution,[],[f1334,f588]) ).
tff(f1342,plain,
( $false
| spl37_1
| spl37_3
| ~ spl37_4 ),
inference(forward_subsumption_resolution,[],[f1337,f617]) ).
tff(f1343,plain,
( spl37_1
| spl37_3
| ~ spl37_4 ),
inference(avatar_contradiction_clause,[],[f1342]) ).
tff(f1344,plain,
( ( sF29(sK12) != sF25(sK11) )
| ~ spl37_2
| spl37_4 ),
inference(forward_demodulation,[],[f1002,f661]) ).
tff(f1463,plain,
! [X0: key1] : ( t2tb4(sF30(X0)) = sF29(X0) ),
inference(forward_subsumption_resolution,[],[f740,f768]) ).
tff(f1672,plain,
( ( t2tb4(sF30(sK12)) = sF25(sK11) )
| ~ spl37_2
| spl37_4 ),
inference(superposition,[],[f742,f1097]) ).
tff(f1674,plain,
( ( sF29(sK12) = sF25(sK11) )
| ~ spl37_2
| spl37_4 ),
inference(forward_demodulation,[],[f1672,f1463]) ).
tff(f1677,plain,
( $false
| ~ spl37_2
| spl37_4 ),
inference(forward_subsumption_resolution,[],[f1674,f1344]) ).
tff(f1678,plain,
( ~ spl37_2
| spl37_4 ),
inference(avatar_contradiction_clause,[],[f1677]) ).
tff(f1679,plain,
( $less(sK7,sK7)
| ~ spl37_1
| ~ spl37_5 ),
inference(forward_demodulation,[],[f576,f633]) ).
tff(f1681,plain,
( $false
| ~ spl37_1
| ~ spl37_5 ),
inference(forward_subsumption_resolution,[],[f1679,f134]) ).
tff(f1682,plain,
( ~ spl37_1
| ~ spl37_5 ),
inference(avatar_contradiction_clause,[],[f1681]) ).
tff(f2036,plain,
( ~ in_data1(a,sK12,sF34,sF24)
| ~ spl37_6 ),
inference(superposition,[],[f636,f552]) ).
tff(f2039,plain,
( $false
| ~ spl37_2
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f2036,f581]) ).
tff(f2040,plain,
( ~ spl37_2
| ~ spl37_6 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
tff(f2049,plain,
( $less(sF33,sK7)
| ( sF33 = sK7 )
| spl37_1 ),
inference(resolution,[],[f577,f136]) ).
tff(f2050,plain,
( ( sF33 = sK7 )
| spl37_1
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f2049,f639]) ).
tff(f2054,plain,
( ! [X0: uni] :
( good_data1(a,sK12,sF34,X0,sF24)
| ( get(option(a),key,X0,t2tb1(sK12)) = some(a,sF34) ) )
| spl37_2 ),
inference(resolution,[],[f580,f369]) ).
tff(f2055,plain,
( ! [X0: uni] :
( ( get(option(a),key,X0,t2tb1(sK12)) = sF25(sK11) )
| good_data1(a,sK12,sF34,X0,sF24) )
| spl37_2 ),
inference(forward_demodulation,[],[f2054,f661]) ).
tff(f2058,plain,
( ! [X0: uni] :
( good_data1(a,sK12,sF34,X0,sF24)
| ( get(sF27,key,X0,t2tb1(sK12)) = sF25(sK11) ) )
| spl37_2 ),
inference(forward_demodulation,[],[f2055,f515]) ).
tff(f2074,plain,
( spl37_5
| spl37_1
| spl37_7 ),
inference(avatar_split_clause,[],[f2050,f638,f575,f631]) ).
tff(f2075,plain,
( ( get(sF27,key,sF28,t2tb1(sK12)) = sF25(sK11) )
| spl37_2
| spl37_4 ),
inference(resolution,[],[f2058,f618]) ).
tff(f2076,plain,
( ( sF29(sK12) = sF25(sK11) )
| spl37_2
| spl37_4 ),
inference(forward_demodulation,[],[f2075,f518]) ).
tff(f2141,plain,
( ( tb2t4(sF29(sK12)) = sF26(sK11) )
| spl37_2
| spl37_4 ),
inference(superposition,[],[f513,f2076]) ).
tff(f2143,plain,
( ( sF26(sK11) = sF30(sK12) )
| spl37_2
| spl37_4 ),
inference(forward_demodulation,[],[f2141,f519]) ).
tff(f3999,plain,
( ! [X0: a1] :
( in_data1(a,sK12,t2tb7(X0),sF24)
| ( sF33 != sK7 )
| mem(sF14,sF20(sK12,X0),sF35)
| ( sF26(X0) != sF30(sK12) ) )
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f1248,f639]) ).
tff(f4000,plain,
( ! [X0: a1] :
( ( sF26(X0) != sF30(sK12) )
| mem(sF14,sF20(sK12,X0),sF35)
| in_data1(a,sK12,t2tb7(X0),sF24) )
| ~ spl37_5
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f3999,f633]) ).
tff(f4043,plain,
( in_data1(a,sK12,t2tb7(sK11),sF24)
| ( sF30(sK12) != sF30(sK12) )
| mem(sF14,sF20(sK12,sK11),sF35)
| spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(superposition,[],[f4000,f2143]) ).
tff(f4044,plain,
( mem(sF14,sF20(sK12,sK11),sF35)
| in_data1(a,sK12,t2tb7(sK11),sF24)
| spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(trivial_inequality_removal,[],[f4043]) ).
tff(f4045,plain,
( mem(sF14,sF20(sK12,sK11),sF35)
| in_data1(a,sK12,sF34,sF24)
| spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(forward_demodulation,[],[f4044,f552]) ).
tff(f4046,plain,
( mem(sF14,sF20(sK12,sK11),sF35)
| spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f4045,f580]) ).
tff(f4108,plain,
( ~ sort1(sF14,sF20(sK12,sK11))
| spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(resolution,[],[f4046,f699]) ).
tff(f4109,plain,
( $false
| spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f4108,f867]) ).
tff(f4110,plain,
( spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(avatar_contradiction_clause,[],[f4109]) ).
tff(f4121,plain,
( ! [X0: $int] :
( ~ $less(sF33,X0)
| $less(sK7,X0) )
| ~ spl37_1 ),
inference(resolution,[],[f576,f135]) ).
tff(f4134,plain,
( $less(sK7,sK7)
| ~ spl37_1
| ~ spl37_7 ),
inference(resolution,[],[f640,f4121]) ).
tff(f4137,plain,
( $false
| ~ spl37_1
| ~ spl37_7 ),
inference(forward_subsumption_resolution,[],[f4134,f134]) ).
tff(f4138,plain,
( ~ spl37_1
| ~ spl37_7 ),
inference(avatar_contradiction_clause,[],[f4137]) ).
cnf(s1,plain,
( ~ spl37_1
| spl37_2 ),
inference(sat_conversion,[],[f582]) ).
cnf(s4,plain,
( spl37_5
| spl37_6
| spl37_7 ),
inference(sat_conversion,[],[f641]) ).
cnf(s15,plain,
~ spl37_3,
inference(sat_conversion,[],[f1293]) ).
cnf(s16,plain,
( spl37_4
| ~ spl37_7 ),
inference(sat_conversion,[],[f1331]) ).
cnf(s17,plain,
( spl37_1
| spl37_3
| ~ spl37_4 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s23,plain,
( ~ spl37_2
| spl37_4 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s24,plain,
( ~ spl37_1
| ~ spl37_5 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s25,plain,
( ~ spl37_2
| ~ spl37_6 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s26,plain,
( spl37_1
| spl37_5
| spl37_7 ),
inference(sat_conversion,[],[f2074]) ).
cnf(s37,plain,
( spl37_2
| spl37_4
| ~ spl37_5
| spl37_7 ),
inference(sat_conversion,[],[f4110]) ).
cnf(s38,plain,
( ~ spl37_1
| ~ spl37_7 ),
inference(sat_conversion,[],[f4138]) ).
cnf(s44,plain,
spl37_1,
inference(rat,[],[s26,s37,s16,s23,s17,s15]) ).
cnf(s45,plain,
~ spl37_7,
inference(rat,[],[s38,s44]) ).
cnf(s46,plain,
~ spl37_5,
inference(rat,[],[s24,s44]) ).
cnf(s47,plain,
spl37_2,
inference(rat,[],[s1,s44]) ).
cnf(s48,plain,
spl37_6,
inference(rat,[],[s4,s45,s46]) ).
cnf(s50,plain,
$false,
inference(rat,[],[s25,s48,s47]) ).
tff(f4139,plain,
$false,
inference(avatar_sat_refutation,[],[s50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW605_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n020.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:22:04 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.56/1.26 % (196066)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.56/1.26 % (196074)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3131773434:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.56/1.26 % (196074)Instruction limit reached!
% 3.56/1.26 % (196074)------------------------------
% 3.56/1.26 % (196074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.26 % (196074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.26 % (196074)CaDiCaL version: 2.1.3
% 3.56/1.26 % (196074)Termination reason: Instruction limit
% 3.56/1.26 % (196074)Termination phase: Property scanning
% 3.56/1.26 % (196074)Time elapsed: 0.003 s
% 3.56/1.26 % (196074)Peak memory usage: 87 MB
% 3.56/1.26 % (196074)Instructions burned: 9 (million)
% 3.56/1.26 % (196072)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1734014212:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.56/1.26 % (196073)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1677090882:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.56/1.26 % (196071)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=333009814:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.56/1.26 % (196076)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2125893771:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.56/1.26 % (196075)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3901369071:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.56/1.26 % (196077)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1396005679:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.56/1.26 % (196075)Instruction limit reached!
% 3.56/1.26 % (196075)------------------------------
% 3.56/1.26 % (196075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.26 % (196075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.26 % (196075)CaDiCaL version: 2.1.3
% 3.56/1.26 % (196075)Termination reason: Instruction limit
% 3.56/1.26 % (196075)Termination phase: Preprocessing 3
% 3.56/1.26 % (196075)Time elapsed: 0.003 s
% 3.56/1.26 % (196075)Peak memory usage: 86 MB
% 3.56/1.26 % (196075)Instructions burned: 5 (million)
% 3.56/1.26 % (196071)Instruction limit reached!
% 3.56/1.26 % (196071)------------------------------
% 3.56/1.26 % (196071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.26 % (196071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.26 % (196071)CaDiCaL version: 2.1.3
% 3.56/1.26 % (196071)Termination reason: Instruction limit
% 3.56/1.26 % (196071)Termination phase: Saturation
% 3.56/1.26 % (196071)Time elapsed: 0.013 s
% 3.56/1.26 % (196071)Peak memory usage: 94 MB
% 3.56/1.26 % (196071)Instructions burned: 12 (million)
% 3.56/1.26 % (196077)Instruction limit reached!
% 3.56/1.26 % (196077)------------------------------
% 3.56/1.26 % (196077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.26 % (196077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.26 % (196077)CaDiCaL version: 2.1.3
% 3.56/1.26 % (196077)Termination reason: Instruction limit
% 3.56/1.26 % (196077)Termination phase: Saturation
% 3.56/1.26 % (196077)Time elapsed: 0.043 s
% 3.56/1.26 % (196077)Peak memory usage: 116 MB
% 3.56/1.26 % (196077)Instructions burned: 33 (million)
% 3.56/1.26 % (196076)Instruction limit reached!
% 3.56/1.26 % (196076)------------------------------
% 3.56/1.26 % (196076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.26 % (196076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.26 % (196076)CaDiCaL version: 2.1.3
% 3.56/1.26 % (196076)Termination reason: Instruction limit
% 3.56/1.26 % (196076)Termination phase: Saturation
% 3.56/1.26 % (196076)Time elapsed: 0.056 s
% 3.56/1.26 % (196076)Peak memory usage: 116 MB
% 3.56/1.26 % (196076)Instructions burned: 47 (million)
% 3.56/1.26 % (196079)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1209643163:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.56/1.26 % (196079)Instruction limit reached!
% 3.56/1.26 % (196079)------------------------------
% 3.56/1.26 % (196079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.40 % (196079)CaDiCaL version: 2.1.3
% 4.69/1.40 % (196079)Termination reason: Instruction limit
% 4.69/1.40 % (196079)Termination phase: Saturation
% 4.69/1.40 % (196079)Time elapsed: 0.005 s
% 4.69/1.40 % (196079)Peak memory usage: 89 MB
% 4.69/1.40 % (196079)Instructions burned: 15 (million)
% 4.69/1.40 % (196086)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=1365076855:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.69/1.40 % (196087)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1098247878:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.69/1.40 % (196073)Instruction limit reached!
% 4.69/1.40 % (196073)------------------------------
% 4.69/1.40 % (196073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.40 % (196073)CaDiCaL version: 2.1.3
% 4.69/1.40 % (196073)Termination reason: Instruction limit
% 4.69/1.40 % (196073)Termination phase: Saturation
% 4.69/1.40 % (196073)Time elapsed: 0.161 s
% 4.69/1.40 % (196073)Peak memory usage: 118 MB
% 4.69/1.40 % (196073)Instructions burned: 201 (million)
% 4.69/1.40 % (196087)Instruction limit reached!
% 4.69/1.40 % (196087)------------------------------
% 4.69/1.40 % (196087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.40 % (196087)CaDiCaL version: 2.1.3
% 4.69/1.40 % (196087)Termination reason: Instruction limit
% 4.69/1.40 % (196087)Termination phase: Saturation
% 4.69/1.40 % (196087)Time elapsed: 0.011 s
% 4.69/1.40 % (196087)Peak memory usage: 89 MB
% 4.69/1.40 % (196087)Instructions burned: 17 (million)
% 4.69/1.40 % (196086)Instruction limit reached!
% 4.69/1.40 % (196086)------------------------------
% 4.69/1.40 % (196086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.40 % (196086)CaDiCaL version: 2.1.3
% 4.69/1.40 % (196086)Termination reason: Instruction limit
% 4.69/1.40 % (196086)Termination phase: Saturation
% 4.69/1.40 % (196086)Time elapsed: 0.020 s
% 4.69/1.40 % (196086)Peak memory usage: 89 MB
% 4.69/1.40 % (196086)Instructions burned: 29 (million)
% 4.69/1.40 % (196072)Instruction limit reached!
% 4.69/1.40 % (196072)------------------------------
% 4.69/1.40 % (196072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.40 % (196072)CaDiCaL version: 2.1.3
% 4.69/1.40 % (196072)Termination reason: Instruction limit
% 4.69/1.40 % (196072)Termination phase: Saturation
% 4.69/1.40 % (196072)Time elapsed: 0.191 s
% 4.69/1.40 % (196072)Peak memory usage: 116 MB
% 4.69/1.40 % (196072)Instructions burned: 307 (million)
% 4.69/1.40 % (196091)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=867805765:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.69/1.40 % (196088)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2491617863:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.69/1.40 % (196089)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=470803437:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.69/1.40 % (196088)Instruction limit reached!
% 4.69/1.40 % (196088)------------------------------
% 4.69/1.40 % (196088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.40 % (196088)CaDiCaL version: 2.1.3
% 4.69/1.40 % (196088)Termination reason: Instruction limit
% 4.69/1.40 % (196088)Termination phase: Saturation
% 4.69/1.40 % (196088)Time elapsed: 0.017 s
% 4.69/1.40 % (196088)Peak memory usage: 90 MB
% 4.69/1.40 % (196088)Instructions burned: 25 (million)
% 4.69/1.40 % (196091)Instruction limit reached!
% 4.69/1.40 % (196091)------------------------------
% 4.69/1.40 % (196091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.40 % (196091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (196091)CaDiCaL version: 2.1.3
% 5.60/1.58 % (196091)Termination reason: Instruction limit
% 5.60/1.58 % (196091)Termination phase: Saturation
% 5.60/1.58 % (196091)Time elapsed: 0.027 s
% 5.60/1.58 % (196091)Peak memory usage: 89 MB
% 5.60/1.58 % (196091)Instructions burned: 88 (million)
% 5.60/1.58 % (196089)Instruction limit reached!
% 5.60/1.58 % (196089)------------------------------
% 5.60/1.58 % (196089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.58 % (196089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (196089)CaDiCaL version: 2.1.3
% 5.60/1.58 % (196089)Termination reason: Instruction limit
% 5.60/1.58 % (196089)Termination phase: Saturation
% 5.60/1.58 % (196089)Time elapsed: 0.018 s
% 5.60/1.58 % (196089)Peak memory usage: 90 MB
% 5.60/1.58 % (196089)Instructions burned: 28 (million)
% 5.60/1.58 % (196094)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3499001594:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.60/1.58 % (196094)Instruction limit reached!
% 5.60/1.58 % (196094)------------------------------
% 5.60/1.58 % (196094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.58 % (196094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (196094)CaDiCaL version: 2.1.3
% 5.60/1.58 % (196094)Termination reason: Instruction limit
% 5.60/1.58 % (196094)Termination phase: Preprocessing 1
% 5.60/1.58 % (196094)Time elapsed: 0.002 s
% 5.60/1.58 % (196094)Peak memory usage: 85 MB
% 5.60/1.58 % (196094)Instructions burned: 3 (million)
% 5.60/1.58 % (196096)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3347928834:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.60/1.58 % (196095)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4084154573:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.60/1.58 % (196096)Instruction limit reached!
% 5.60/1.58 % (196096)------------------------------
% 5.60/1.58 % (196096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.58 % (196096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (196096)CaDiCaL version: 2.1.3
% 5.60/1.58 % (196096)Termination reason: Instruction limit
% 5.60/1.58 % (196096)Termination phase: Preprocessing 3
% 5.60/1.58 % (196096)Time elapsed: 0.003 s
% 5.60/1.58 % (196096)Peak memory usage: 86 MB
% 5.60/1.58 % (196096)Instructions burned: 4 (million)
% 5.60/1.58 % (196102)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=4049577894:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.60/1.58 % (196099)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=62332994:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.60/1.58 % (196102)Instruction limit reached!
% 5.60/1.58 % (196102)------------------------------
% 5.60/1.58 % (196102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.58 % (196102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (196102)CaDiCaL version: 2.1.3
% 5.60/1.58 % (196102)Termination reason: Instruction limit
% 5.60/1.58 % (196102)Termination phase: Property scanning
% 5.60/1.58 % (196102)Time elapsed: 0.003 s
% 5.60/1.58 % (196102)Peak memory usage: 87 MB
% 5.60/1.58 % (196102)Instructions burned: 10 (million)
% 5.60/1.58 % (196101)lrs+10_1_thi=all:si=on:fd=off:random_seed=2869869558:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.60/1.58 % (196103)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=677289822:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.60/1.58 % (196103)Instruction limit reached!
% 5.60/1.58 % (196103)------------------------------
% 5.60/1.58 % (196103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.58 % (196103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (196103)CaDiCaL version: 2.1.3
% 5.60/1.58 % (196103)Termination reason: Instruction limit
% 5.60/1.58 % (196103)Termination phase: Preprocessing 1
% 5.60/1.58 % (196103)Time elapsed: 0.002 s
% 5.60/1.58 % (196103)Peak memory usage: 86 MB
% 5.60/1.58 % (196103)Instructions burned: 3 (million)
% 5.60/1.58 % (196099)Instruction limit reached!
% 7.34/1.83 % (196099)------------------------------
% 7.34/1.83 % (196099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.34/1.83 % (196099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.83 % (196099)CaDiCaL version: 2.1.3
% 7.34/1.83 % (196099)Termination reason: Instruction limit
% 7.34/1.83 % (196099)Termination phase: Saturation
% 7.34/1.83 % (196099)Time elapsed: 0.089 s
% 7.34/1.83 % (196099)Peak memory usage: 134 MB
% 7.34/1.83 % (196099)Instructions burned: 66 (million)
% 7.34/1.83 % (196101)Instruction limit reached!
% 7.34/1.83 % (196101)------------------------------
% 7.34/1.83 % (196101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.34/1.83 % (196101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.83 % (196101)CaDiCaL version: 2.1.3
% 7.34/1.83 % (196101)Termination reason: Instruction limit
% 7.34/1.83 % (196101)Termination phase: Saturation
% 7.34/1.83 % (196101)Time elapsed: 0.060 s
% 7.34/1.83 % (196101)Peak memory usage: 117 MB
% 7.34/1.83 % (196101)Instructions burned: 53 (million)
% 7.34/1.83 % (196111)dis+10_1_si=on:random_seed=3173729621:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.34/1.83 % (196095)Instruction limit reached!
% 7.34/1.83 % (196095)------------------------------
% 7.34/1.83 % (196095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.34/1.83 % (196095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.83 % (196095)CaDiCaL version: 2.1.3
% 7.34/1.83 % (196095)Termination reason: Instruction limit
% 7.34/1.83 % (196095)Termination phase: Saturation
% 7.34/1.83 % (196095)Time elapsed: 0.122 s
% 7.34/1.83 % (196095)Peak memory usage: 91 MB
% 7.34/1.83 % (196095)Instructions burned: 181 (million)
% 7.34/1.83 % (196111)Instruction limit reached!
% 7.34/1.83 % (196111)------------------------------
% 7.34/1.83 % (196111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.34/1.83 % (196111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.83 % (196111)CaDiCaL version: 2.1.3
% 7.34/1.83 % (196111)Termination reason: Instruction limit
% 7.34/1.83 % (196111)Termination phase: Saturation
% 7.34/1.83 % (196111)Time elapsed: 0.004 s
% 7.34/1.83 % (196111)Peak memory usage: 88 MB
% 7.34/1.83 % (196111)Instructions burned: 13 (million)
% 7.34/1.83 % (196106)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1905039986:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.34/1.83 % (196110)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2343943720:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 7.34/1.83 % (196106)Instruction limit reached!
% 7.34/1.83 % (196106)------------------------------
% 7.34/1.83 % (196106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.34/1.83 % (196106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.83 % (196106)CaDiCaL version: 2.1.3
% 7.34/1.83 % (196106)Termination reason: Instruction limit
% 7.34/1.83 % (196106)Termination phase: Preprocessing 1
% 7.34/1.83 % (196106)Time elapsed: 0.002 s
% 7.34/1.83 % (196106)Peak memory usage: 85 MB
% 7.34/1.83 % (196106)Instructions burned: 3 (million)
% 7.34/1.83 % (196114)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1334092487:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.34/1.83 % (196119)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=384053445:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 7.34/1.83 % (196114)Refutation not found, incomplete strategy
% 7.34/1.83 % (196114)------------------------------
% 7.34/1.83 % (196114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.34/1.83 % (196114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.83 % (196114)CaDiCaL version: 2.1.3
% 7.34/1.83 % (196114)Termination reason: Refutation not found, incomplete strategy
% 7.34/1.83 % (196114)Time elapsed: 0.013 s
% 7.34/1.83 % (196114)Peak memory usage: 89 MB
% 7.34/1.83 % (196114)Instructions burned: 19 (million)
% 7.34/1.83 % (196115)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2565999731: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.34/1.83 % (196116)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=568827577:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 9.95/2.29 % (196116)Instruction limit reached!
% 9.95/2.29 % (196116)------------------------------
% 9.95/2.29 % (196116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196116)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196116)Termination reason: Instruction limit
% 9.95/2.29 % (196116)Termination phase: Preprocessing 2
% 9.95/2.29 % (196116)Time elapsed: 0.002 s
% 9.95/2.29 % (196116)Peak memory usage: 85 MB
% 9.95/2.29 % (196116)Instructions burned: 4 (million)
% 9.95/2.29 % (196110)Instruction limit reached!
% 9.95/2.29 % (196110)------------------------------
% 9.95/2.29 % (196110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196110)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196110)Termination reason: Instruction limit
% 9.95/2.29 % (196110)Termination phase: Saturation
% 9.95/2.29 % (196110)Time elapsed: 0.115 s
% 9.95/2.29 % (196110)Peak memory usage: 117 MB
% 9.95/2.29 % (196110)Instructions burned: 128 (million)
% 9.95/2.29 % (196115)Instruction limit reached!
% 9.95/2.29 % (196115)------------------------------
% 9.95/2.29 % (196115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196115)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196115)Termination reason: Instruction limit
% 9.95/2.29 % (196115)Termination phase: Saturation
% 9.95/2.29 % (196115)Time elapsed: 0.025 s
% 9.95/2.29 % (196115)Peak memory usage: 89 MB
% 9.95/2.29 % (196115)Instructions burned: 36 (million)
% 9.95/2.29 % (196118)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1444503315:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 9.95/2.29 % (196118)Instruction limit reached!
% 9.95/2.29 % (196118)------------------------------
% 9.95/2.29 % (196118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196118)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196118)Termination reason: Instruction limit
% 9.95/2.29 % (196118)Termination phase: Function definition elimination
% 9.95/2.29 % (196118)Time elapsed: 0.005 s
% 9.95/2.29 % (196118)Peak memory usage: 86 MB
% 9.95/2.29 % (196118)Instructions burned: 8 (million)
% 9.95/2.29 % (196122)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=499613267:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 9.95/2.29 % (196122)Instruction limit reached!
% 9.95/2.29 % (196122)------------------------------
% 9.95/2.29 % (196122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196122)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196122)Termination reason: Instruction limit
% 9.95/2.29 % (196122)Termination phase: Saturation
% 9.95/2.29 % (196122)Time elapsed: 0.009 s
% 9.95/2.29 % (196122)Peak memory usage: 90 MB
% 9.95/2.29 % (196122)Instructions burned: 13 (million)
% 9.95/2.29 % (196119)Instruction limit reached!
% 9.95/2.29 % (196119)------------------------------
% 9.95/2.29 % (196119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196119)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196119)Termination reason: Instruction limit
% 9.95/2.29 % (196119)Termination phase: Saturation
% 9.95/2.29 % (196119)Time elapsed: 0.110 s
% 9.95/2.29 % (196119)Peak memory usage: 92 MB
% 9.95/2.29 % (196119)Instructions burned: 371 (million)
% 9.95/2.29 % (196127)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4042389230:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 9.95/2.29 % (196128)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1795077584:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 9.95/2.29 % (196129)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=490963099:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 9.95/2.29 % (196128)Instruction limit reached!
% 9.95/2.29 % (196128)------------------------------
% 9.95/2.29 % (196128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196128)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196128)Termination reason: Instruction limit
% 9.95/2.29 % (196128)Termination phase: Saturation
% 9.95/2.29 % (196128)Time elapsed: 0.006 s
% 9.95/2.29 % (196128)Peak memory usage: 88 MB
% 9.95/2.29 % (196128)Instructions burned: 10 (million)
% 9.95/2.29 % (196131)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=570088350:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 9.95/2.29 % (196134)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=961801228:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 9.95/2.29 % (196133)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=1659786925:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 9.95/2.29 % (196114)------------------------------
% 9.95/2.29 % (196114)------------------------------
% 9.95/2.29 % (196131)Instruction limit reached!
% 9.95/2.29 % (196131)------------------------------
% 9.95/2.29 % (196131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196131)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196131)Termination reason: Instruction limit
% 9.95/2.29 % (196131)Termination phase: Saturation
% 9.95/2.29 % (196131)Time elapsed: 0.056 s
% 9.95/2.29 % (196131)Peak memory usage: 90 MB
% 9.95/2.29 % (196131)Instructions burned: 75 (million)
% 9.95/2.29 % (196129)Instruction limit reached!
% 9.95/2.29 % (196129)------------------------------
% 9.95/2.29 % (196129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196129)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196129)Termination reason: Instruction limit
% 9.95/2.29 % (196129)Termination phase: Saturation
% 9.95/2.29 % (196129)Time elapsed: 0.091 s
% 9.95/2.29 % (196129)Peak memory usage: 134 MB
% 9.95/2.29 % (196129)Instructions burned: 72 (million)
% 9.95/2.29 % (196134)Instruction limit reached!
% 9.95/2.29 % (196134)------------------------------
% 9.95/2.29 % (196134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196134)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196134)Termination reason: Instruction limit
% 9.95/2.29 % (196134)Termination phase: Saturation
% 9.95/2.29 % (196134)Time elapsed: 0.058 s
% 9.95/2.29 % (196134)Peak memory usage: 117 MB
% 9.95/2.29 % (196134)Instructions burned: 130 (million)
% 9.95/2.29 % (196127)Instruction limit reached!
% 9.95/2.29 % (196127)------------------------------
% 9.95/2.29 % (196127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196127)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196127)Termination reason: Instruction limit
% 9.95/2.29 % (196127)Termination phase: Saturation
% 9.95/2.29 % (196127)Time elapsed: 0.144 s
% 9.95/2.29 % (196127)Peak memory usage: 119 MB
% 9.95/2.29 % (196127)Instructions burned: 226 (million)
% 9.95/2.29 % (196138)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1303244302:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 9.95/2.29 % (196133)First to succeed.
% 9.95/2.29 % (196133)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-196066"
% 9.95/2.29 % (196145)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1214110422:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 9.95/2.29 % (196143)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3247369314:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 9.95/2.29 % (196142)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1377262707:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 9.95/2.29 % (196144)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3215376305:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 9.95/2.29 % (196145)Instruction limit reached!
% 9.95/2.29 % (196145)------------------------------
% 9.95/2.29 % (196145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196145)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196145)Termination reason: Instruction limit
% 9.95/2.29 % (196145)Termination phase: Saturation
% 9.95/2.29 % (196145)Time elapsed: 0.061 s
% 9.95/2.29 % (196145)Peak memory usage: 119 MB
% 9.95/2.29 % (196145)Instructions burned: 132 (million)
% 9.95/2.29 % (196142)Instruction limit reached!
% 9.95/2.29 % (196142)------------------------------
% 9.95/2.29 % (196142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196142)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196142)Termination reason: Instruction limit
% 9.95/2.29 % (196142)Termination phase: Saturation
% 9.95/2.29 % (196142)Time elapsed: 0.068 s
% 9.95/2.29 % (196142)Peak memory usage: 134 MB
% 9.95/2.29 % (196142)Instructions burned: 41 (million)
% 9.95/2.29 % (196138)Instruction limit reached!
% 9.95/2.29 % (196138)------------------------------
% 9.95/2.29 % (196138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196138)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196138)Termination reason: Instruction limit
% 9.95/2.29 % (196138)Termination phase: Saturation
% 9.95/2.29 % (196138)Time elapsed: 0.135 s
% 9.95/2.29 % (196138)Peak memory usage: 134 MB
% 9.95/2.29 % (196138)Instructions burned: 132 (million)
% 9.95/2.29 % (196146)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=2509005586:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 9.95/2.29 % (196143)Instruction limit reached!
% 9.95/2.29 % (196143)------------------------------
% 9.95/2.29 % (196143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196143)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196143)Termination reason: Instruction limit
% 9.95/2.29 % (196143)Termination phase: Saturation
% 9.95/2.29 % (196143)Time elapsed: 0.164 s
% 9.95/2.29 % (196143)Peak memory usage: 92 MB
% 9.95/2.29 % (196143)Instructions burned: 308 (million)
% 9.95/2.29 % (196152)dis+10_1_si=on:random_seed=1254793147:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 9.95/2.29 % (196153)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1369769525:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 9.95/2.29 % (196146)Refutation not found, SMT solver inside AVATAR returned Unknown
% 9.95/2.29 % (196146)------------------------------
% 9.95/2.29 % (196146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.95/2.29 % (196146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.95/2.29 % (196146)CaDiCaL version: 2.1.3
% 9.95/2.29 % (196146)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 9.95/2.29 % (196146)Time elapsed: 0.160 s
% 9.95/2.29 % (196146)Peak memory usage: 119 MB
% 9.95/2.29 % (196146)Instructions burned: 192 (million)
% 9.95/2.29 % (196146)------------------------------
% 9.95/2.29 % (196146)------------------------------
% 9.95/2.29 % (196133)Refutation found. Thanks to Tanya!
% 9.95/2.29 % SZS status Theorem for theBenchmark
% 9.95/2.29 % SZS output start Proof for theBenchmark
% See solution above
% 10.52/2.49 % (196133)------------------------------
% 10.52/2.49 % (196133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.49 % (196133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.49 % (196133)CaDiCaL version: 2.1.3
% 10.52/2.49 % (196133)Termination reason: Refutation
% 10.52/2.49 % (196133)Time elapsed: 0.163 s
% 10.52/2.49 % (196133)Peak memory usage: 92 MB
% 10.52/2.49 % (196133)Instructions burned: 223 (million)
% 10.52/2.49 % (196133)------------------------------
% 10.52/2.49 % (196133)------------------------------
% 10.52/2.49 % (196066)Success in time 1.619 s
% 10.52/2.49 % Vampire exiting
%------------------------------------------------------------------------------