%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW635_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:00 PM UTC 2026
% Result : Theorem 55.14s 8.44s
% Output : Refutation 55.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 66
% Syntax : Number of formulae : 236 ( 59 unt; 0 typ; 57 def)
% Number of atoms : 1091 ( 252 equ)
% Maximal formula atoms : 65 ( 4 avg)
% Number of connectives : 1308 ( 453 ~; 361 |; 342 &)
% ( 75 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 799 ( 285 atm; 142 fun; 157 num; 215 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 55 ( 51 usr; 43 prp; 0-4 aty)
% Number of functors : 104 ( 99 usr; 57 con; 0-5 aty)
% Number of variables : 468 ( 363 !; 105 ?; 468 :)
% 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,
set_int: $tType ).
tff(type_def_10,type,
map_int_int: $tType ).
tff(type_def_11,type,
map_int_lpmap_int_intrp: $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,
set: ty > ty ).
tff(func_def_13,type,
empty: ty > uni ).
tff(func_def_14,type,
add: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
remove: ( ty * uni * uni ) > uni ).
tff(func_def_16,type,
union: ( ty * uni * uni ) > uni ).
tff(func_def_17,type,
inter: ( ty * uni * uni ) > uni ).
tff(func_def_18,type,
diff: ( ty * uni * uni ) > uni ).
tff(func_def_19,type,
choose: ( ty * uni ) > uni ).
tff(func_def_20,type,
cardinal1: ( ty * uni ) > $int ).
tff(func_def_23,type,
min_elt1: set_int > $int ).
tff(func_def_24,type,
t2tb: set_int > uni ).
tff(func_def_25,type,
tb2t: uni > set_int ).
tff(func_def_26,type,
t2tb1: $int > uni ).
tff(func_def_27,type,
tb2t1: uni > $int ).
tff(func_def_28,type,
max_elt1: set_int > $int ).
tff(func_def_29,type,
below1: $int > set_int ).
tff(func_def_30,type,
succ1: set_int > set_int ).
tff(func_def_32,type,
pred1: set_int > set_int ).
tff(func_def_33,type,
ref: ty > ty ).
tff(func_def_34,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_35,type,
contents: ( ty * uni ) > uni ).
tff(func_def_36,type,
map: ( ty * ty ) > ty ).
tff(func_def_37,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_38,type,
set1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_39,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_40,type,
n1: $int ).
tff(func_def_41,type,
t2tb2: map_int_int > uni ).
tff(func_def_42,type,
tb2t2: uni > map_int_int ).
tff(func_def_43,type,
t2tb3: map_int_lpmap_int_intrp > uni ).
tff(func_def_44,type,
tb2t3: uni > map_int_lpmap_int_intrp ).
tff(func_def_46,type,
sK0: ( uni * uni * ty ) > uni ).
tff(func_def_47,type,
sK1: ( uni * ty * uni ) > uni ).
tff(func_def_48,type,
sK2: ( map_int_int * map_int_int ) > $int ).
tff(func_def_49,type,
sK3: ( uni * $int * ty * uni ) > $int ).
tff(func_def_50,type,
sK4: ( $int * map_int_lpmap_int_intrp * $int ) > $int ).
tff(func_def_51,type,
sK5: ( $int * map_int_lpmap_int_intrp * $int ) > $int ).
tff(func_def_52,type,
sK6: set_int ).
tff(func_def_53,type,
sK7: set_int ).
tff(func_def_54,type,
sK8: map_int_int ).
tff(func_def_55,type,
sK9: $int ).
tff(func_def_56,type,
sK10: set_int ).
tff(func_def_57,type,
sK11: $int ).
tff(func_def_58,type,
sK12: map_int_lpmap_int_intrp ).
tff(func_def_59,type,
sK13: $int > $int ).
tff(func_def_60,type,
sK14: $int > $int ).
tff(func_def_61,type,
sK15: $int ).
tff(func_def_62,type,
sK16: map_int_lpmap_int_intrp ).
tff(func_def_63,type,
sK17: map_int_int ).
tff(func_def_64,type,
sK18: set_int ).
tff(func_def_65,type,
sK19: $int ).
tff(func_def_66,type,
sK20: $int ).
tff(func_def_67,type,
sK21: map_int_int ).
tff(func_def_68,type,
sK22: $int ).
tff(func_def_69,type,
sK23: $int ).
tff(func_def_70,type,
sK24: $int ).
tff(func_def_71,type,
sK25: map_int_int > $int ).
tff(func_def_72,type,
sK26: $int > $int ).
tff(func_def_73,type,
sK27: ( uni * ty ) > uni ).
tff(func_def_74,type,
sK28: ( map_int_int * $int ) > $int ).
tff(func_def_75,type,
sK29: ( map_int_int * $int ) > $int ).
tff(func_def_76,type,
sF30: uni ).
tff(func_def_77,type,
sF31: $int ).
tff(func_def_78,type,
sF32: $int ).
tff(func_def_79,type,
sF33: uni ).
tff(func_def_80,type,
sF34: $int ).
tff(func_def_81,type,
sF35: uni ).
tff(func_def_82,type,
sF36: ty ).
tff(func_def_83,type,
sF37: uni ).
tff(func_def_84,type,
sF38: uni ).
tff(func_def_85,type,
sF39: uni ).
tff(func_def_86,type,
sF40: uni ).
tff(func_def_87,type,
sF41: uni ).
tff(func_def_88,type,
sF42: uni ).
tff(func_def_89,type,
sF43: uni ).
tff(func_def_90,type,
sF44: uni ).
tff(func_def_91,type,
sF45: uni ).
tff(func_def_92,type,
sF46: $int ).
tff(func_def_93,type,
sF47: uni ).
tff(func_def_94,type,
sF48: $int ).
tff(func_def_95,type,
sF49: uni ).
tff(func_def_96,type,
sF50: uni ).
tff(func_def_97,type,
sF51: $int ).
tff(func_def_98,type,
sF52: uni ).
tff(func_def_99,type,
sF53: uni ).
tff(func_def_100,type,
sF54: uni ).
tff(func_def_101,type,
sF55: map_int_int ).
tff(func_def_102,type,
sF56: $int ).
tff(func_def_103,type,
sF57: $int ).
tff(func_def_104,type,
sF58: uni ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
infix_eqeq: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
subset: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
is_empty: ( ty * uni ) > $o ).
tff(pred_def_8,type,
eq_prefix1: ( ty * uni * uni * $int ) > $o ).
tff(pred_def_9,type,
partial_solution1: ( $int * map_int_int ) > $o ).
tff(pred_def_10,type,
lt_sol1: ( map_int_int * map_int_int ) > $o ).
tff(pred_def_11,type,
sorted1: ( map_int_lpmap_int_intrp * $int * $int ) > $o ).
tff(f21,axiom,
! [X1: uni,X3: uni,X2: uni,X0: ty] :
( sort1(X0,X1)
=> ( sort1(X0,X2)
=> ( ( ( X1 != X2 )
& mem(X0,X1,X3) )
<=> mem(X0,X1,remove(X0,X2,X3)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',remove_def1) ).
tff(f43,axiom,
! [X0: $int] : sort1(int,t2tb1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f44,axiom,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL1) ).
tff(f45,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f60,axiom,
! [X4: uni,X1: ty,X2: uni,X3: uni,X0: ty,X5: uni] :
( sort1(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set1(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_eq) ).
tff(f61,axiom,
! [X1: ty,X3: uni,X2: uni,X4: uni,X0: ty] :
( sort1(X0,X3)
=> ( sort1(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set1(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_neq) ).
tff(f64,axiom,
! [X0: ty,X2: uni,X1: uni,X3: $int] :
( ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq(0,X4) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',eq_prefix_def) ).
tff(f67,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR2) ).
tff(f76,conjecture,
! [X3: $int,X4: map_int_lpmap_int_intrp,X6: map_int_int,X2: set_int,X5: $int,X1: set_int,X0: set_int] :
( ( ( $sum(X5,cardinal1(int,t2tb(X0))) = n1 )
& ! [X7: $int] :
( $lesseq(0,X7)
=> ( ~ mem(int,t2tb1(X7),t2tb(X1))
<=> ! [X8: $int] :
( ( $lesseq(0,X8)
& $less(X8,X5) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != $difference($sum(X7,X8),X5) ) ) ) )
& $lesseq(0,X3)
& ! [X7: $int] :
( mem(int,t2tb1(X7),t2tb(X0))
<=> ( $lesseq(0,X7)
& $less(X7,n1)
& ! [X8: $int] :
( ( $less(X8,X5)
& $lesseq(0,X8) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != X7 ) ) ) )
& ! [X7: $int] :
( $lesseq(0,X7)
=> ( ~ mem(int,t2tb1(X7),t2tb(X2))
<=> ! [X8: $int] :
( ( $less(X8,X5)
& $lesseq(0,X8) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != $difference($sum(X7,X5),X8) ) ) ) )
& $lesseq(0,X5)
& partial_solution1(X5,X6) )
=> ( ~ is_empty(int,t2tb(X0))
=> ! [X14: map_int_int,X13: $int,X9: $int,X10: set_int,X12: map_int_lpmap_int_intrp,X11: $int] :
( ( subset(int,t2tb(X10),diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)))
& ( X13 = X5 )
& $lesseq(0,$difference(X11,X3))
& sorted1(X12,X3,X11)
& ( X9 = $difference(X11,X3) )
& partial_solution1(X13,X14)
& ! [X15: map_int_int] :
( ? [X7: $int] :
( eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X7)),n1)
& $less(X7,X11)
& $lesseq(X3,X7) )
<=> ( eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13)
& mem(int,get(int,int,t2tb2(X15),t2tb1(X13)),diff(int,diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)),t2tb(X10)))
& partial_solution1(n1,X15) ) )
& eq_prefix1(map(int,int),t2tb3(X4),t2tb3(X12),X3)
& eq_prefix1(int,t2tb2(X6),t2tb2(X14),X13)
& ! [X7: $int,X8: $int] :
( mem(int,t2tb1(X7),diff(int,diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)),t2tb(X10)))
=> ( mem(int,t2tb1(X8),t2tb(X10))
=> $less(X7,X8) ) ) )
=> ( ~ is_empty(int,t2tb(X10))
=> ! [X16: map_int_int] :
( ( X16 = tb2t2(set1(int,int,t2tb2(X14),t2tb1(X13),t2tb1(min_elt1(X10)))) )
=> ! [X17: $int] :
( ( X17 = $sum(X13,1) )
=> ! [X7: $int] :
( mem(int,t2tb1(X7),remove(int,t2tb1(min_elt1(X10)),t2tb(X0)))
=> ! [X8: $int] :
( ( $lesseq(0,X8)
& $less(X8,X17) )
=> ( tb2t1(get(int,int,t2tb2(X16),t2tb1(X8))) != X7 ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_t3) ).
tff(f77,negated_conjecture,
~ ! [X3: $int,X4: map_int_lpmap_int_intrp,X6: map_int_int,X2: set_int,X5: $int,X1: set_int,X0: set_int] :
( ( ( $sum(X5,cardinal1(int,t2tb(X0))) = n1 )
& ! [X7: $int] :
( $lesseq(0,X7)
=> ( ~ mem(int,t2tb1(X7),t2tb(X1))
<=> ! [X8: $int] :
( ( $lesseq(0,X8)
& $less(X8,X5) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != $difference($sum(X7,X8),X5) ) ) ) )
& $lesseq(0,X3)
& ! [X7: $int] :
( mem(int,t2tb1(X7),t2tb(X0))
<=> ( $lesseq(0,X7)
& $less(X7,n1)
& ! [X8: $int] :
( ( $less(X8,X5)
& $lesseq(0,X8) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != X7 ) ) ) )
& ! [X7: $int] :
( $lesseq(0,X7)
=> ( ~ mem(int,t2tb1(X7),t2tb(X2))
<=> ! [X8: $int] :
( ( $less(X8,X5)
& $lesseq(0,X8) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != $difference($sum(X7,X5),X8) ) ) ) )
& $lesseq(0,X5)
& partial_solution1(X5,X6) )
=> ( ~ is_empty(int,t2tb(X0))
=> ! [X14: map_int_int,X13: $int,X9: $int,X10: set_int,X12: map_int_lpmap_int_intrp,X11: $int] :
( ( subset(int,t2tb(X10),diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)))
& ( X13 = X5 )
& $lesseq(0,$difference(X11,X3))
& sorted1(X12,X3,X11)
& ( X9 = $difference(X11,X3) )
& partial_solution1(X13,X14)
& ! [X15: map_int_int] :
( ? [X7: $int] :
( eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X7)),n1)
& $less(X7,X11)
& $lesseq(X3,X7) )
<=> ( eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13)
& mem(int,get(int,int,t2tb2(X15),t2tb1(X13)),diff(int,diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)),t2tb(X10)))
& partial_solution1(n1,X15) ) )
& eq_prefix1(map(int,int),t2tb3(X4),t2tb3(X12),X3)
& eq_prefix1(int,t2tb2(X6),t2tb2(X14),X13)
& ! [X7: $int,X8: $int] :
( mem(int,t2tb1(X7),diff(int,diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)),t2tb(X10)))
=> ( mem(int,t2tb1(X8),t2tb(X10))
=> $less(X7,X8) ) ) )
=> ( ~ is_empty(int,t2tb(X10))
=> ! [X16: map_int_int] :
( ( X16 = tb2t2(set1(int,int,t2tb2(X14),t2tb1(X13),t2tb1(min_elt1(X10)))) )
=> ! [X17: $int] :
( ( X17 = $sum(X13,1) )
=> ! [X7: $int] :
( mem(int,t2tb1(X7),remove(int,t2tb1(min_elt1(X10)),t2tb(X0)))
=> ! [X8: $int] :
( ( $lesseq(0,X8)
& $less(X8,X17) )
=> ( tb2t1(get(int,int,t2tb2(X16),t2tb1(X8))) != X7 ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f76]) ).
tff(f79,plain,
! [X0: ty,X2: uni,X1: uni,X3: $int] :
( ! [X4: $int] :
( ( $less(X4,X3)
& ~ $less(X4,0) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X0,X1,X2,X3) ),
inference(theory_normalization,[],[f64]) ).
tff(f82,plain,
~ ! [X3: $int,X4: map_int_lpmap_int_intrp,X6: map_int_int,X2: set_int,X5: $int,X1: set_int,X0: set_int] :
( ( ( $sum(X5,cardinal1(int,t2tb(X0))) = n1 )
& ! [X7: $int] :
( ~ $less(X7,0)
=> ( ~ mem(int,t2tb1(X7),t2tb(X1))
<=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,X5) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X5)) ) ) ) )
& ~ $less(X3,0)
& ! [X7: $int] :
( mem(int,t2tb1(X7),t2tb(X0))
<=> ( ~ $less(X7,0)
& $less(X7,n1)
& ! [X8: $int] :
( ( $less(X8,X5)
& ~ $less(X8,0) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != X7 ) ) ) )
& ! [X7: $int] :
( ~ $less(X7,0)
=> ( ~ mem(int,t2tb1(X7),t2tb(X2))
<=> ! [X8: $int] :
( ( $less(X8,X5)
& ~ $less(X8,0) )
=> ( tb2t1(get(int,int,t2tb2(X6),t2tb1(X8))) != $sum($sum(X7,X5),$uminus(X8)) ) ) ) )
& ~ $less(X5,0)
& partial_solution1(X5,X6) )
=> ( ~ is_empty(int,t2tb(X0))
=> ! [X14: map_int_int,X13: $int,X9: $int,X10: set_int,X12: map_int_lpmap_int_intrp,X11: $int] :
( ( subset(int,t2tb(X10),diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)))
& ( X13 = X5 )
& ~ $less($sum(X11,$uminus(X3)),0)
& sorted1(X12,X3,X11)
& ( $sum(X11,$uminus(X3)) = X9 )
& partial_solution1(X13,X14)
& ! [X15: map_int_int] :
( ? [X7: $int] :
( eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X7)),n1)
& $less(X7,X11)
& ~ $less(X7,X3) )
<=> ( eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13)
& mem(int,get(int,int,t2tb2(X15),t2tb1(X13)),diff(int,diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)),t2tb(X10)))
& partial_solution1(n1,X15) ) )
& eq_prefix1(map(int,int),t2tb3(X4),t2tb3(X12),X3)
& eq_prefix1(int,t2tb2(X6),t2tb2(X14),X13)
& ! [X7: $int,X8: $int] :
( mem(int,t2tb1(X7),diff(int,diff(int,diff(int,t2tb(X0),t2tb(X1)),t2tb(X2)),t2tb(X10)))
=> ( mem(int,t2tb1(X8),t2tb(X10))
=> $less(X7,X8) ) ) )
=> ( ~ is_empty(int,t2tb(X10))
=> ! [X16: map_int_int] :
( ( X16 = tb2t2(set1(int,int,t2tb2(X14),t2tb1(X13),t2tb1(min_elt1(X10)))) )
=> ! [X17: $int] :
( ( X17 = $sum(X13,1) )
=> ! [X7: $int] :
( mem(int,t2tb1(X7),remove(int,t2tb1(min_elt1(X10)),t2tb(X0)))
=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,X17) )
=> ( tb2t1(get(int,int,t2tb2(X16),t2tb1(X8))) != X7 ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f77]) ).
tff(f98,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( ! [X4: $int] :
( ( $less(X4,X3)
& ~ $less(X4,0) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X0,X2,X1,X3) ),
inference(rectify,[],[f79]) ).
tff(f104,plain,
~ ! [X4: $int,X3: set_int,X0: $int,X6: set_int,X1: map_int_lpmap_int_intrp,X2: map_int_int,X5: set_int] :
( ( partial_solution1(X4,X2)
& ~ $less(X0,0)
& ! [X9: $int] :
( mem(int,t2tb1(X9),t2tb(X6))
<=> ( ~ $less(X9,0)
& $less(X9,n1)
& ! [X10: $int] :
( ( ~ $less(X10,0)
& $less(X10,X4) )
=> ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) != X9 ) ) ) )
& ! [X7: $int] :
( ~ $less(X7,0)
=> ( ~ mem(int,t2tb1(X7),t2tb(X5))
<=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,X4) )
=> ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X4)) ) ) ) )
& ( n1 = $sum(X4,cardinal1(int,t2tb(X6))) )
& ! [X11: $int] :
( ~ $less(X11,0)
=> ( ~ mem(int,t2tb1(X11),t2tb(X3))
<=> ! [X12: $int] :
( ( ~ $less(X12,0)
& $less(X12,X4) )
=> ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) != $sum($sum(X11,X4),$uminus(X12)) ) ) ) )
& ~ $less(X4,0) )
=> ( ~ is_empty(int,t2tb(X6))
=> ! [X16: set_int,X18: $int,X13: map_int_int,X14: $int,X15: $int,X17: map_int_lpmap_int_intrp] :
( ( eq_prefix1(int,t2tb2(X2),t2tb2(X13),X14)
& ! [X19: map_int_int] :
( ? [X20: $int] :
( ~ $less(X20,X0)
& $less(X20,X18)
& eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) )
<=> ( eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
& partial_solution1(n1,X19)
& mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) ) )
& subset(int,t2tb(X16),diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)))
& ( X4 = X14 )
& partial_solution1(X14,X13)
& ! [X22: $int,X21: $int] :
( mem(int,t2tb1(X21),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16)))
=> ( mem(int,t2tb1(X22),t2tb(X16))
=> $less(X21,X22) ) )
& ( $sum(X18,$uminus(X0)) = X15 )
& ~ $less($sum(X18,$uminus(X0)),0)
& sorted1(X17,X0,X18)
& eq_prefix1(map(int,int),t2tb3(X1),t2tb3(X17),X0) )
=> ( ~ is_empty(int,t2tb(X16))
=> ! [X23: map_int_int] :
( ( tb2t2(set1(int,int,t2tb2(X13),t2tb1(X14),t2tb1(min_elt1(X16)))) = X23 )
=> ! [X24: $int] :
( ( $sum(X14,1) = X24 )
=> ! [X25: $int] :
( mem(int,t2tb1(X25),remove(int,t2tb1(min_elt1(X16)),t2tb(X6)))
=> ! [X26: $int] :
( ( ~ $less(X26,0)
& $less(X26,X24) )
=> ( tb2t1(get(int,int,t2tb2(X23),t2tb1(X26))) != X25 ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f82]) ).
tff(f106,plain,
! [X0: uni,X1: uni,X3: ty,X2: uni] :
( sort1(X3,X0)
=> ( sort1(X3,X2)
=> ( mem(X3,X0,remove(X3,X2,X1))
<=> ( mem(X3,X0,X1)
& ( X0 != X2 ) ) ) ) ),
inference(rectify,[],[f21]) ).
tff(f118,plain,
! [X0: uni,X5: uni,X3: uni,X1: ty,X4: ty,X2: uni] :
( sort1(X1,X5)
=> ( ( X0 = X3 )
=> ( get(X1,X4,set1(X1,X4,X2,X3,X5),X0) = X5 ) ) ),
inference(rectify,[],[f60]) ).
tff(f131,plain,
! [X4: ty,X3: uni,X0: ty,X2: uni,X1: uni] :
( sort1(X4,X1)
=> ( sort1(X4,X3)
=> ! [X5: uni] :
( ( X1 != X3 )
=> ( get(X0,X4,X2,X3) = get(X0,X4,set1(X0,X4,X2,X1,X5),X3) ) ) ) ),
inference(rectify,[],[f61]) ).
tff(f140,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( ! [X4: $int] :
( ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) )
| ~ $less(X4,X3)
| $less(X4,0) )
<=> eq_prefix1(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f98]) ).
tff(f141,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( ! [X4: $int] :
( $less(X4,0)
| ~ $less(X4,X3)
| ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X0,X2,X1,X3) ),
inference(flattening,[],[f140]) ).
tff(f159,plain,
! [X0: uni,X1: uni,X3: ty,X2: uni] :
( ( mem(X3,X0,remove(X3,X2,X1))
<=> ( mem(X3,X0,X1)
& ( X0 != X2 ) ) )
| ~ sort1(X3,X2)
| ~ sort1(X3,X0) ),
inference(ennf_transformation,[],[f106]) ).
tff(f160,plain,
! [X0: uni,X1: uni,X3: ty,X2: uni] :
( ( mem(X3,X0,remove(X3,X2,X1))
<=> ( mem(X3,X0,X1)
& ( X0 != X2 ) ) )
| ~ sort1(X3,X0)
| ~ sort1(X3,X2) ),
inference(flattening,[],[f159]) ).
tff(f161,plain,
? [X4: $int,X3: set_int,X0: $int,X6: set_int,X1: map_int_lpmap_int_intrp,X2: map_int_int,X5: set_int] :
( ? [X16: set_int,X18: $int,X13: map_int_int,X14: $int,X15: $int,X17: map_int_lpmap_int_intrp] :
( ? [X23: map_int_int] :
( ? [X24: $int] :
( ? [X25: $int] :
( ? [X26: $int] :
( ( tb2t1(get(int,int,t2tb2(X23),t2tb1(X26))) = X25 )
& ~ $less(X26,0)
& $less(X26,X24) )
& mem(int,t2tb1(X25),remove(int,t2tb1(min_elt1(X16)),t2tb(X6))) )
& ( $sum(X14,1) = X24 ) )
& ( tb2t2(set1(int,int,t2tb2(X13),t2tb1(X14),t2tb1(min_elt1(X16)))) = X23 ) )
& ~ is_empty(int,t2tb(X16))
& eq_prefix1(int,t2tb2(X2),t2tb2(X13),X14)
& ! [X19: map_int_int] :
( ? [X20: $int] :
( ~ $less(X20,X0)
& $less(X20,X18)
& eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) )
<=> ( eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
& partial_solution1(n1,X19)
& mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) ) )
& subset(int,t2tb(X16),diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)))
& ( X4 = X14 )
& partial_solution1(X14,X13)
& ! [X22: $int,X21: $int] :
( $less(X21,X22)
| ~ mem(int,t2tb1(X22),t2tb(X16))
| ~ mem(int,t2tb1(X21),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
& ( $sum(X18,$uminus(X0)) = X15 )
& ~ $less($sum(X18,$uminus(X0)),0)
& sorted1(X17,X0,X18)
& eq_prefix1(map(int,int),t2tb3(X1),t2tb3(X17),X0) )
& ~ is_empty(int,t2tb(X6))
& partial_solution1(X4,X2)
& ~ $less(X0,0)
& ! [X9: $int] :
( mem(int,t2tb1(X9),t2tb(X6))
<=> ( ~ $less(X9,0)
& $less(X9,n1)
& ! [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) != X9 )
| $less(X10,0)
| ~ $less(X10,X4) ) ) )
& ! [X7: $int] :
( ( ~ mem(int,t2tb1(X7),t2tb(X5))
<=> ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X4)) )
| $less(X8,0)
| ~ $less(X8,X4) ) )
| $less(X7,0) )
& ( n1 = $sum(X4,cardinal1(int,t2tb(X6))) )
& ! [X11: $int] :
( ( ~ mem(int,t2tb1(X11),t2tb(X3))
<=> ! [X12: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) != $sum($sum(X11,X4),$uminus(X12)) )
| $less(X12,0)
| ~ $less(X12,X4) ) )
| $less(X11,0) )
& ~ $less(X4,0) ),
inference(ennf_transformation,[],[f104]) ).
tff(f162,plain,
? [X3: set_int,X5: set_int,X2: map_int_int,X4: $int,X6: set_int,X0: $int,X1: map_int_lpmap_int_intrp] :
( partial_solution1(X4,X2)
& ~ is_empty(int,t2tb(X6))
& ~ $less(X0,0)
& ( n1 = $sum(X4,cardinal1(int,t2tb(X6))) )
& ~ $less(X4,0)
& ! [X9: $int] :
( ( ~ $less(X9,0)
& ! [X10: $int] :
( $less(X10,0)
| ~ $less(X10,X4)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) != X9 ) )
& $less(X9,n1) )
<=> mem(int,t2tb1(X9),t2tb(X6)) )
& ! [X7: $int] :
( ( ! [X8: $int] :
( $less(X8,0)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X4)) )
| ~ $less(X8,X4) )
<=> ~ mem(int,t2tb1(X7),t2tb(X5)) )
| $less(X7,0) )
& ? [X18: $int,X17: map_int_lpmap_int_intrp,X13: map_int_int,X16: set_int,X14: $int,X15: $int] :
( eq_prefix1(map(int,int),t2tb3(X1),t2tb3(X17),X0)
& subset(int,t2tb(X16),diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)))
& ? [X23: map_int_int] :
( ? [X24: $int] :
( ? [X25: $int] :
( ? [X26: $int] :
( $less(X26,X24)
& ~ $less(X26,0)
& ( tb2t1(get(int,int,t2tb2(X23),t2tb1(X26))) = X25 ) )
& mem(int,t2tb1(X25),remove(int,t2tb1(min_elt1(X16)),t2tb(X6))) )
& ( $sum(X14,1) = X24 ) )
& ( tb2t2(set1(int,int,t2tb2(X13),t2tb1(X14),t2tb1(min_elt1(X16)))) = X23 ) )
& ~ $less($sum(X18,$uminus(X0)),0)
& eq_prefix1(int,t2tb2(X2),t2tb2(X13),X14)
& ( X4 = X14 )
& ( $sum(X18,$uminus(X0)) = X15 )
& ! [X19: map_int_int] :
( ? [X20: $int] :
( ~ $less(X20,X0)
& $less(X20,X18)
& eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) )
<=> ( eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
& partial_solution1(n1,X19)
& mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) ) )
& ! [X22: $int,X21: $int] :
( ~ mem(int,t2tb1(X22),t2tb(X16))
| $less(X21,X22)
| ~ mem(int,t2tb1(X21),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
& partial_solution1(X14,X13)
& ~ is_empty(int,t2tb(X16))
& sorted1(X17,X0,X18) )
& ! [X11: $int] :
( $less(X11,0)
| ( ! [X12: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) != $sum($sum(X11,X4),$uminus(X12)) )
| ~ $less(X12,X4)
| $less(X12,0) )
<=> ~ mem(int,t2tb1(X11),t2tb(X3)) ) ) ),
inference(flattening,[],[f161]) ).
tff(f172,plain,
! [X4: ty,X3: uni,X0: ty,X2: uni,X1: uni] :
( ! [X5: uni] :
( ( get(X0,X4,X2,X3) = get(X0,X4,set1(X0,X4,X2,X1,X5),X3) )
| ( X1 = X3 ) )
| ~ sort1(X4,X3)
| ~ sort1(X4,X1) ),
inference(ennf_transformation,[],[f131]) ).
tff(f173,plain,
! [X1: uni,X0: ty,X4: ty,X3: uni,X2: uni] :
( ! [X5: uni] :
( ( get(X0,X4,X2,X3) = get(X0,X4,set1(X0,X4,X2,X1,X5),X3) )
| ( X1 = X3 ) )
| ~ sort1(X4,X1)
| ~ sort1(X4,X3) ),
inference(flattening,[],[f172]) ).
tff(f179,plain,
! [X0: uni,X5: uni,X3: uni,X1: ty,X4: ty,X2: uni] :
( ( get(X1,X4,set1(X1,X4,X2,X3,X5),X0) = X5 )
| ( X0 != X3 )
| ~ sort1(X1,X5) ),
inference(ennf_transformation,[],[f118]) ).
tff(f180,plain,
! [X2: uni,X4: ty,X5: uni,X3: uni,X0: uni,X1: ty] :
( ( get(X1,X4,set1(X1,X4,X2,X3,X5),X0) = X5 )
| ( X0 != X3 )
| ~ sort1(X1,X5) ),
inference(flattening,[],[f179]) ).
tff(f205,plain,
! [X0: uni,X1: ty,X2: uni,X3: uni,X4: uni,X5: ty] :
( ( get(X5,X1,set1(X5,X1,X0,X3,X2),X4) = X2 )
| ( X3 != X4 )
| ~ sort1(X5,X2) ),
inference(rectify,[],[f180]) ).
tff(f218,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( ( ! [X4: $int] :
( $less(X4,0)
| ~ $less(X4,X3)
| ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
| ~ eq_prefix1(X0,X2,X1,X3) )
& ( eq_prefix1(X0,X2,X1,X3)
| ? [X4: $int] :
( ~ $less(X4,0)
& $less(X4,X3)
& ( get(X0,int,X1,t2tb1(X4)) != get(X0,int,X2,t2tb1(X4)) ) ) ) ),
inference(nnf_transformation,[],[f141]) ).
tff(f219,plain,
! [X0: uni,X1: $int,X2: ty,X3: uni] :
( ( ! [X4: $int] :
( $less(X4,0)
| ~ $less(X4,X1)
| ( get(X2,int,X3,t2tb1(X4)) = get(X2,int,X0,t2tb1(X4)) ) )
| ~ eq_prefix1(X2,X0,X3,X1) )
& ( eq_prefix1(X2,X0,X3,X1)
| ? [X5: $int] :
( ~ $less(X5,0)
& $less(X5,X1)
& ( get(X2,int,X3,t2tb1(X5)) != get(X2,int,X0,t2tb1(X5)) ) ) ) ),
inference(rectify,[],[f218]) ).
tff(f220,plain,
! [X0: uni,X1: $int,X2: ty,X3: uni] :
( ( ! [X4: $int] :
( $less(X4,0)
| ~ $less(X4,X1)
| ( get(X2,int,X3,t2tb1(X4)) = get(X2,int,X0,t2tb1(X4)) ) )
| ~ eq_prefix1(X2,X0,X3,X1) )
& ( eq_prefix1(X2,X0,X3,X1)
| ( ~ $less(sK3(X0,X1,X2,X3),0)
& $less(sK3(X0,X1,X2,X3),X1)
& ( get(X2,int,X3,t2tb1(sK3(X0,X1,X2,X3))) != get(X2,int,X0,t2tb1(sK3(X0,X1,X2,X3))) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X5,sK3(X0,X1,X2,X3))],[f219]) ).
tff(f223,plain,
! [X0: uni,X1: ty,X2: ty,X3: uni,X4: uni] :
( ! [X5: uni] :
( ( get(X1,X2,set1(X1,X2,X4,X0,X5),X3) = get(X1,X2,X4,X3) )
| ( X0 = X3 ) )
| ~ sort1(X2,X0)
| ~ sort1(X2,X3) ),
inference(rectify,[],[f173]) ).
tff(f229,plain,
! [X0: uni,X1: uni,X3: ty,X2: uni] :
( ( ( mem(X3,X0,remove(X3,X2,X1))
| ~ mem(X3,X0,X1)
| ( X0 = X2 ) )
& ( ( mem(X3,X0,X1)
& ( X0 != X2 ) )
| ~ mem(X3,X0,remove(X3,X2,X1)) ) )
| ~ sort1(X3,X0)
| ~ sort1(X3,X2) ),
inference(nnf_transformation,[],[f160]) ).
tff(f230,plain,
! [X0: uni,X1: uni,X3: ty,X2: uni] :
( ( ( mem(X3,X0,remove(X3,X2,X1))
| ~ mem(X3,X0,X1)
| ( X0 = X2 ) )
& ( ( mem(X3,X0,X1)
& ( X0 != X2 ) )
| ~ mem(X3,X0,remove(X3,X2,X1)) ) )
| ~ sort1(X3,X0)
| ~ sort1(X3,X2) ),
inference(flattening,[],[f229]) ).
tff(f231,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni] :
( ( ( mem(X2,X0,remove(X2,X3,X1))
| ~ mem(X2,X0,X1)
| ( X0 = X3 ) )
& ( ( mem(X2,X0,X1)
& ( X0 != X3 ) )
| ~ mem(X2,X0,remove(X2,X3,X1)) ) )
| ~ sort1(X2,X0)
| ~ sort1(X2,X3) ),
inference(rectify,[],[f230]) ).
tff(f234,plain,
? [X3: set_int,X5: set_int,X2: map_int_int,X4: $int,X6: set_int,X0: $int,X1: map_int_lpmap_int_intrp] :
( partial_solution1(X4,X2)
& ~ is_empty(int,t2tb(X6))
& ~ $less(X0,0)
& ( n1 = $sum(X4,cardinal1(int,t2tb(X6))) )
& ~ $less(X4,0)
& ! [X9: $int] :
( ( ( ~ $less(X9,0)
& ! [X10: $int] :
( $less(X10,0)
| ~ $less(X10,X4)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) != X9 ) )
& $less(X9,n1) )
| ~ mem(int,t2tb1(X9),t2tb(X6)) )
& ( mem(int,t2tb1(X9),t2tb(X6))
| $less(X9,0)
| ? [X10: $int] :
( ~ $less(X10,0)
& $less(X10,X4)
& ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) = X9 ) )
| ~ $less(X9,n1) ) )
& ! [X7: $int] :
( ( ( ! [X8: $int] :
( $less(X8,0)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X4)) )
| ~ $less(X8,X4) )
| mem(int,t2tb1(X7),t2tb(X5)) )
& ( ~ mem(int,t2tb1(X7),t2tb(X5))
| ? [X8: $int] :
( ~ $less(X8,0)
& ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) = $sum($sum(X7,X8),$uminus(X4)) )
& $less(X8,X4) ) ) )
| $less(X7,0) )
& ? [X18: $int,X17: map_int_lpmap_int_intrp,X13: map_int_int,X16: set_int,X14: $int,X15: $int] :
( eq_prefix1(map(int,int),t2tb3(X1),t2tb3(X17),X0)
& subset(int,t2tb(X16),diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)))
& ? [X23: map_int_int] :
( ? [X24: $int] :
( ? [X25: $int] :
( ? [X26: $int] :
( $less(X26,X24)
& ~ $less(X26,0)
& ( tb2t1(get(int,int,t2tb2(X23),t2tb1(X26))) = X25 ) )
& mem(int,t2tb1(X25),remove(int,t2tb1(min_elt1(X16)),t2tb(X6))) )
& ( $sum(X14,1) = X24 ) )
& ( tb2t2(set1(int,int,t2tb2(X13),t2tb1(X14),t2tb1(min_elt1(X16)))) = X23 ) )
& ~ $less($sum(X18,$uminus(X0)),0)
& eq_prefix1(int,t2tb2(X2),t2tb2(X13),X14)
& ( X4 = X14 )
& ( $sum(X18,$uminus(X0)) = X15 )
& ! [X19: map_int_int] :
( ( ? [X20: $int] :
( ~ $less(X20,X0)
& $less(X20,X18)
& eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) )
| ~ eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
| ~ partial_solution1(n1,X19)
| ~ mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
& ( ( eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
& partial_solution1(n1,X19)
& mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
| ! [X20: $int] :
( $less(X20,X0)
| ~ $less(X20,X18)
| ~ eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) ) ) )
& ! [X22: $int,X21: $int] :
( ~ mem(int,t2tb1(X22),t2tb(X16))
| $less(X21,X22)
| ~ mem(int,t2tb1(X21),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
& partial_solution1(X14,X13)
& ~ is_empty(int,t2tb(X16))
& sorted1(X17,X0,X18) )
& ! [X11: $int] :
( $less(X11,0)
| ( ( ! [X12: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) != $sum($sum(X11,X4),$uminus(X12)) )
| ~ $less(X12,X4)
| $less(X12,0) )
| mem(int,t2tb1(X11),t2tb(X3)) )
& ( ~ mem(int,t2tb1(X11),t2tb(X3))
| ? [X12: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) = $sum($sum(X11,X4),$uminus(X12)) )
& $less(X12,X4)
& ~ $less(X12,0) ) ) ) ) ),
inference(nnf_transformation,[],[f162]) ).
tff(f235,plain,
? [X3: set_int,X5: set_int,X2: map_int_int,X4: $int,X6: set_int,X0: $int,X1: map_int_lpmap_int_intrp] :
( partial_solution1(X4,X2)
& ~ is_empty(int,t2tb(X6))
& ~ $less(X0,0)
& ( n1 = $sum(X4,cardinal1(int,t2tb(X6))) )
& ~ $less(X4,0)
& ! [X9: $int] :
( ( ( ~ $less(X9,0)
& ! [X10: $int] :
( $less(X10,0)
| ~ $less(X10,X4)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) != X9 ) )
& $less(X9,n1) )
| ~ mem(int,t2tb1(X9),t2tb(X6)) )
& ( mem(int,t2tb1(X9),t2tb(X6))
| $less(X9,0)
| ? [X10: $int] :
( ~ $less(X10,0)
& $less(X10,X4)
& ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) = X9 ) )
| ~ $less(X9,n1) ) )
& ! [X7: $int] :
( ( ( ! [X8: $int] :
( $less(X8,0)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X4)) )
| ~ $less(X8,X4) )
| mem(int,t2tb1(X7),t2tb(X5)) )
& ( ~ mem(int,t2tb1(X7),t2tb(X5))
| ? [X8: $int] :
( ~ $less(X8,0)
& ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) = $sum($sum(X7,X8),$uminus(X4)) )
& $less(X8,X4) ) ) )
| $less(X7,0) )
& ? [X18: $int,X17: map_int_lpmap_int_intrp,X13: map_int_int,X16: set_int,X14: $int,X15: $int] :
( eq_prefix1(map(int,int),t2tb3(X1),t2tb3(X17),X0)
& subset(int,t2tb(X16),diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)))
& ? [X23: map_int_int] :
( ? [X24: $int] :
( ? [X25: $int] :
( ? [X26: $int] :
( $less(X26,X24)
& ~ $less(X26,0)
& ( tb2t1(get(int,int,t2tb2(X23),t2tb1(X26))) = X25 ) )
& mem(int,t2tb1(X25),remove(int,t2tb1(min_elt1(X16)),t2tb(X6))) )
& ( $sum(X14,1) = X24 ) )
& ( tb2t2(set1(int,int,t2tb2(X13),t2tb1(X14),t2tb1(min_elt1(X16)))) = X23 ) )
& ~ $less($sum(X18,$uminus(X0)),0)
& eq_prefix1(int,t2tb2(X2),t2tb2(X13),X14)
& ( X4 = X14 )
& ( $sum(X18,$uminus(X0)) = X15 )
& ! [X19: map_int_int] :
( ( ? [X20: $int] :
( ~ $less(X20,X0)
& $less(X20,X18)
& eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) )
| ~ eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
| ~ partial_solution1(n1,X19)
| ~ mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
& ( ( eq_prefix1(int,t2tb2(X13),t2tb2(X19),X14)
& partial_solution1(n1,X19)
& mem(int,get(int,int,t2tb2(X19),t2tb1(X14)),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
| ! [X20: $int] :
( $less(X20,X0)
| ~ $less(X20,X18)
| ~ eq_prefix1(int,t2tb2(X19),get(map(int,int),int,t2tb3(X17),t2tb1(X20)),n1) ) ) )
& ! [X22: $int,X21: $int] :
( ~ mem(int,t2tb1(X22),t2tb(X16))
| $less(X21,X22)
| ~ mem(int,t2tb1(X21),diff(int,diff(int,diff(int,t2tb(X6),t2tb(X5)),t2tb(X3)),t2tb(X16))) )
& partial_solution1(X14,X13)
& ~ is_empty(int,t2tb(X16))
& sorted1(X17,X0,X18) )
& ! [X11: $int] :
( $less(X11,0)
| ( ( ! [X12: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) != $sum($sum(X11,X4),$uminus(X12)) )
| ~ $less(X12,X4)
| $less(X12,0) )
| mem(int,t2tb1(X11),t2tb(X3)) )
& ( ~ mem(int,t2tb1(X11),t2tb(X3))
| ? [X12: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) = $sum($sum(X11,X4),$uminus(X12)) )
& $less(X12,X4)
& ~ $less(X12,0) ) ) ) ) ),
inference(flattening,[],[f234]) ).
tff(f236,plain,
? [X0: set_int,X1: set_int,X2: map_int_int,X3: $int,X4: set_int,X5: $int,X6: map_int_lpmap_int_intrp] :
( partial_solution1(X3,X2)
& ~ is_empty(int,t2tb(X4))
& ~ $less(X5,0)
& ( n1 = $sum(X3,cardinal1(int,t2tb(X4))) )
& ~ $less(X3,0)
& ! [X7: $int] :
( ( ( ~ $less(X7,0)
& ! [X8: $int] :
( $less(X8,0)
| ~ $less(X8,X3)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X8))) != X7 ) )
& $less(X7,n1) )
| ~ mem(int,t2tb1(X7),t2tb(X4)) )
& ( mem(int,t2tb1(X7),t2tb(X4))
| $less(X7,0)
| ? [X9: $int] :
( ~ $less(X9,0)
& $less(X9,X3)
& ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X9))) = X7 ) )
| ~ $less(X7,n1) ) )
& ! [X10: $int] :
( ( ( ! [X11: $int] :
( $less(X11,0)
| ( $sum($sum(X10,X11),$uminus(X3)) != tb2t1(get(int,int,t2tb2(X2),t2tb1(X11))) )
| ~ $less(X11,X3) )
| mem(int,t2tb1(X10),t2tb(X1)) )
& ( ~ mem(int,t2tb1(X10),t2tb(X1))
| ? [X12: $int] :
( ~ $less(X12,0)
& ( $sum($sum(X10,X12),$uminus(X3)) = tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) )
& $less(X12,X3) ) ) )
| $less(X10,0) )
& ? [X13: $int,X14: map_int_lpmap_int_intrp,X15: map_int_int,X16: set_int,X17: $int,X18: $int] :
( eq_prefix1(map(int,int),t2tb3(X6),t2tb3(X14),X5)
& subset(int,t2tb(X16),diff(int,diff(int,t2tb(X4),t2tb(X1)),t2tb(X0)))
& ? [X19: map_int_int] :
( ? [X20: $int] :
( ? [X21: $int] :
( ? [X22: $int] :
( $less(X22,X20)
& ~ $less(X22,0)
& ( tb2t1(get(int,int,t2tb2(X19),t2tb1(X22))) = X21 ) )
& mem(int,t2tb1(X21),remove(int,t2tb1(min_elt1(X16)),t2tb(X4))) )
& ( $sum(X17,1) = X20 ) )
& ( tb2t2(set1(int,int,t2tb2(X15),t2tb1(X17),t2tb1(min_elt1(X16)))) = X19 ) )
& ~ $less($sum(X13,$uminus(X5)),0)
& eq_prefix1(int,t2tb2(X2),t2tb2(X15),X17)
& ( X3 = X17 )
& ( $sum(X13,$uminus(X5)) = X18 )
& ! [X23: map_int_int] :
( ( ? [X24: $int] :
( ~ $less(X24,X5)
& $less(X24,X13)
& eq_prefix1(int,t2tb2(X23),get(map(int,int),int,t2tb3(X14),t2tb1(X24)),n1) )
| ~ eq_prefix1(int,t2tb2(X15),t2tb2(X23),X17)
| ~ partial_solution1(n1,X23)
| ~ mem(int,get(int,int,t2tb2(X23),t2tb1(X17)),diff(int,diff(int,diff(int,t2tb(X4),t2tb(X1)),t2tb(X0)),t2tb(X16))) )
& ( ( eq_prefix1(int,t2tb2(X15),t2tb2(X23),X17)
& partial_solution1(n1,X23)
& mem(int,get(int,int,t2tb2(X23),t2tb1(X17)),diff(int,diff(int,diff(int,t2tb(X4),t2tb(X1)),t2tb(X0)),t2tb(X16))) )
| ! [X25: $int] :
( $less(X25,X5)
| ~ $less(X25,X13)
| ~ eq_prefix1(int,t2tb2(X23),get(map(int,int),int,t2tb3(X14),t2tb1(X25)),n1) ) ) )
& ! [X26: $int,X27: $int] :
( ~ mem(int,t2tb1(X26),t2tb(X16))
| $less(X27,X26)
| ~ mem(int,t2tb1(X27),diff(int,diff(int,diff(int,t2tb(X4),t2tb(X1)),t2tb(X0)),t2tb(X16))) )
& partial_solution1(X17,X15)
& ~ is_empty(int,t2tb(X16))
& sorted1(X14,X5,X13) )
& ! [X28: $int] :
( $less(X28,0)
| ( ( ! [X29: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X29))) != $sum($sum(X28,X3),$uminus(X29)) )
| ~ $less(X29,X3)
| $less(X29,0) )
| mem(int,t2tb1(X28),t2tb(X0)) )
& ( ~ mem(int,t2tb1(X28),t2tb(X0))
| ? [X30: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X30))) = $sum($sum(X28,X3),$uminus(X30)) )
& $less(X30,X3)
& ~ $less(X30,0) ) ) ) ) ),
inference(rectify,[],[f235]) ).
tff(f237,plain,
( partial_solution1(sK9,sK8)
& ~ is_empty(int,t2tb(sK10))
& ~ $less(sK11,0)
& ( n1 = $sum(sK9,cardinal1(int,t2tb(sK10))) )
& ~ $less(sK9,0)
& ! [X7: $int] :
( ( ( ~ $less(X7,0)
& ! [X8: $int] :
( $less(X8,0)
| ~ $less(X8,sK9)
| ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(X8))) != X7 ) )
& $less(X7,n1) )
| ~ mem(int,t2tb1(X7),t2tb(sK10)) )
& ( mem(int,t2tb1(X7),t2tb(sK10))
| $less(X7,0)
| ( ~ $less(sK13(X7),0)
& $less(sK13(X7),sK9)
& ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(sK13(X7)))) = X7 ) )
| ~ $less(X7,n1) ) )
& ! [X10: $int] :
( ( ( ! [X11: $int] :
( $less(X11,0)
| ( $sum($sum(X10,X11),$uminus(sK9)) != tb2t1(get(int,int,t2tb2(sK8),t2tb1(X11))) )
| ~ $less(X11,sK9) )
| mem(int,t2tb1(X10),t2tb(sK7)) )
& ( ~ mem(int,t2tb1(X10),t2tb(sK7))
| ( ~ $less(sK14(X10),0)
& ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(sK14(X10)))) = $sum($sum(X10,sK14(X10)),$uminus(sK9)) )
& $less(sK14(X10),sK9) ) ) )
| $less(X10,0) )
& eq_prefix1(map(int,int),t2tb3(sK12),t2tb3(sK16),sK11)
& subset(int,t2tb(sK18),diff(int,diff(int,t2tb(sK10),t2tb(sK7)),t2tb(sK6)))
& $less(sK24,sK22)
& ~ $less(sK24,0)
& ( tb2t1(get(int,int,t2tb2(sK21),t2tb1(sK24))) = sK23 )
& mem(int,t2tb1(sK23),remove(int,t2tb1(min_elt1(sK18)),t2tb(sK10)))
& ( sK22 = $sum(sK19,1) )
& ( sK21 = tb2t2(set1(int,int,t2tb2(sK17),t2tb1(sK19),t2tb1(min_elt1(sK18)))) )
& ~ $less($sum(sK15,$uminus(sK11)),0)
& eq_prefix1(int,t2tb2(sK8),t2tb2(sK17),sK19)
& ( sK9 = sK19 )
& ( sK20 = $sum(sK15,$uminus(sK11)) )
& ! [X23: map_int_int] :
( ( ( ~ $less(sK25(X23),sK11)
& $less(sK25(X23),sK15)
& eq_prefix1(int,t2tb2(X23),get(map(int,int),int,t2tb3(sK16),t2tb1(sK25(X23))),n1) )
| ~ eq_prefix1(int,t2tb2(sK17),t2tb2(X23),sK19)
| ~ partial_solution1(n1,X23)
| ~ mem(int,get(int,int,t2tb2(X23),t2tb1(sK19)),diff(int,diff(int,diff(int,t2tb(sK10),t2tb(sK7)),t2tb(sK6)),t2tb(sK18))) )
& ( ( eq_prefix1(int,t2tb2(sK17),t2tb2(X23),sK19)
& partial_solution1(n1,X23)
& mem(int,get(int,int,t2tb2(X23),t2tb1(sK19)),diff(int,diff(int,diff(int,t2tb(sK10),t2tb(sK7)),t2tb(sK6)),t2tb(sK18))) )
| ! [X25: $int] :
( $less(X25,sK11)
| ~ $less(X25,sK15)
| ~ eq_prefix1(int,t2tb2(X23),get(map(int,int),int,t2tb3(sK16),t2tb1(X25)),n1) ) ) )
& ! [X26: $int,X27: $int] :
( ~ mem(int,t2tb1(X26),t2tb(sK18))
| $less(X27,X26)
| ~ mem(int,t2tb1(X27),diff(int,diff(int,diff(int,t2tb(sK10),t2tb(sK7)),t2tb(sK6)),t2tb(sK18))) )
& partial_solution1(sK19,sK17)
& ~ is_empty(int,t2tb(sK18))
& sorted1(sK16,sK11,sK15)
& ! [X28: $int] :
( $less(X28,0)
| ( ( ! [X29: $int] :
( ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(X29))) != $sum($sum(X28,sK9),$uminus(X29)) )
| ~ $less(X29,sK9)
| $less(X29,0) )
| mem(int,t2tb1(X28),t2tb(sK6)) )
& ( ~ mem(int,t2tb1(X28),t2tb(sK6))
| ( ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(sK26(X28)))) = $sum($sum(X28,sK9),$uminus(sK26(X28))) )
& $less(sK26(X28),sK9)
& ~ $less(sK26(X28),0) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9),skolemize(X4,sK10),skolemize(X5,sK11),skolemize(X6,sK12),skolemize(X9,sK13(X7)),skolemize(X12,sK14(X10)),skolemize(X13,sK15),skolemize(X14,sK16),skolemize(X15,sK17),skolemize(X16,sK18),skolemize(X17,sK19),skolemize(X18,sK20),skolemize(X19,sK21),skolemize(X20,sK22),skolemize(X21,sK23),skolemize(X22,sK24),skolemize(X24,sK25(X23)),skolemize(X30,sK26(X28))],[f236]) ).
tff(f272,plain,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
inference(cnf_transformation,[],[f44]) ).
tff(f290,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty,X4: uni,X5: ty] :
( ( get(X5,X1,set1(X5,X1,X0,X3,X2),X4) = X2 )
| ( X3 != X4 )
| ~ sort1(X5,X2) ),
inference(cnf_transformation,[],[f205]) ).
tff(f295,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f67]) ).
tff(f304,plain,
! [X0: $int] : sort1(int,t2tb1(X0)),
inference(cnf_transformation,[],[f43]) ).
tff(f307,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f45]) ).
tff(f320,plain,
! [X2: ty,X3: uni,X0: uni,X1: $int,X4: $int] :
( ( get(X2,int,X3,t2tb1(X4)) = get(X2,int,X0,t2tb1(X4)) )
| ~ $less(X4,X1)
| $less(X4,0)
| ~ eq_prefix1(X2,X0,X3,X1) ),
inference(cnf_transformation,[],[f220]) ).
tff(f324,plain,
! [X2: ty,X3: uni,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( get(X1,X2,set1(X1,X2,X4,X0,X5),X3) = get(X1,X2,X4,X3) )
| ~ sort1(X2,X3)
| ( X0 = X3 )
| ~ sort1(X2,X0) ),
inference(cnf_transformation,[],[f223]) ).
tff(f337,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] :
( ( X0 != X3 )
| ~ mem(X2,X0,remove(X2,X3,X1))
| ~ sort1(X2,X0)
| ~ sort1(X2,X3) ),
inference(cnf_transformation,[],[f231]) ).
tff(f338,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] :
( ~ mem(X2,X0,remove(X2,X3,X1))
| ~ sort1(X2,X0)
| mem(X2,X0,X1)
| ~ sort1(X2,X3) ),
inference(cnf_transformation,[],[f231]) ).
tff(f359,plain,
sK9 = sK19,
inference(cnf_transformation,[],[f237]) ).
tff(f360,plain,
eq_prefix1(int,t2tb2(sK8),t2tb2(sK17),sK19),
inference(cnf_transformation,[],[f237]) ).
tff(f362,plain,
sK21 = tb2t2(set1(int,int,t2tb2(sK17),t2tb1(sK19),t2tb1(min_elt1(sK18)))),
inference(cnf_transformation,[],[f237]) ).
tff(f363,plain,
sK22 = $sum(sK19,1),
inference(cnf_transformation,[],[f237]) ).
tff(f364,plain,
mem(int,t2tb1(sK23),remove(int,t2tb1(min_elt1(sK18)),t2tb(sK10))),
inference(cnf_transformation,[],[f237]) ).
tff(f365,plain,
tb2t1(get(int,int,t2tb2(sK21),t2tb1(sK24))) = sK23,
inference(cnf_transformation,[],[f237]) ).
tff(f366,plain,
~ $less(sK24,0),
inference(cnf_transformation,[],[f237]) ).
tff(f367,plain,
$less(sK24,sK22),
inference(cnf_transformation,[],[f237]) ).
tff(f378,plain,
! [X8: $int,X7: $int] :
( $less(X8,0)
| ~ $less(X8,sK9)
| ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(X8))) != X7 )
| ~ mem(int,t2tb1(X7),t2tb(sK10)) ),
inference(cnf_transformation,[],[f237]) ).
tff(f426,plain,
! [X8: $int,X7: $int] :
( $less(X8,0)
| ~ $less(X8,sK19)
| ( tb2t1(get(int,int,t2tb2(sK8),t2tb1(X8))) != X7 )
| ~ mem(int,t2tb1(X7),t2tb(sK10)) ),
inference(definition_unfolding,[],[f378,f359]) ).
tff(f434,plain,
! [X2: uni,X0: uni,X1: ty,X4: uni,X5: ty] :
( ( get(X5,X1,set1(X5,X1,X0,X4,X2),X4) = X2 )
| ~ sort1(X5,X2) ),
inference(equality_resolution,[],[f290]) ).
tff(f435,plain,
! [X2: ty,X3: uni,X1: uni] :
( ~ mem(X2,X3,remove(X2,X3,X1))
| ~ sort1(X2,X3)
| ~ sort1(X2,X3) ),
inference(equality_resolution,[],[f337]) ).
tff(f436,plain,
! [X8: $int] :
( $less(X8,0)
| ~ $less(X8,sK19)
| ~ mem(int,t2tb1(tb2t1(get(int,int,t2tb2(sK8),t2tb1(X8)))),t2tb(sK10)) ),
inference(equality_resolution,[],[f426]) ).
tff(f438,definition,
sF30 = t2tb(sK10),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f439,plain,
t2tb(sK10) = sF30,
inference(reorient_equations,[],[f438]) ).
tff(f446,definition,
sF33 = t2tb2(sK8),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f447,plain,
! [X8: $int] :
( ~ mem(int,t2tb1(tb2t1(get(int,int,sF33,t2tb1(X8)))),sF30)
| $less(X8,0)
| ~ $less(X8,sK19) ),
inference(definition_folding,[],[f436,f439,f446]) ).
tff(f470,definition,
sF43 = t2tb2(sK21),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
tff(f471,definition,
sF44 = t2tb1(sK24),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
tff(f472,definition,
sF45 = get(int,int,sF43,sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
tff(f473,plain,
get(int,int,sF43,sF44) = sF45,
inference(reorient_equations,[],[f472]) ).
tff(f474,definition,
sF46 = tb2t1(sF45),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
tff(f475,plain,
sF46 = sK23,
inference(definition_folding,[],[f365,f474,f473,f471,f470]) ).
tff(f476,definition,
sF47 = t2tb1(sK23),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
tff(f477,definition,
sF48 = min_elt1(sK18),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
tff(f478,definition,
sF49 = t2tb1(sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
tff(f479,definition,
sF50 = remove(int,sF49,sF30),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
tff(f480,plain,
remove(int,sF49,sF30) = sF50,
inference(reorient_equations,[],[f479]) ).
tff(f481,plain,
mem(int,sF47,sF50),
inference(definition_folding,[],[f364,f480,f439,f478,f477,f476]) ).
tff(f482,definition,
sF51 = $sum(sK19,1),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
tff(f483,plain,
sK22 = sF51,
inference(definition_folding,[],[f363,f482]) ).
tff(f484,definition,
sF52 = t2tb2(sK17),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
tff(f485,definition,
sF53 = t2tb1(sK19),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
tff(f486,definition,
sF54 = set1(int,int,sF52,sF53,sF49),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
tff(f487,definition,
sF55 = tb2t2(sF54),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
tff(f488,plain,
sF55 = sK21,
inference(definition_folding,[],[f362,f487,f486,f478,f477,f485,f484]) ).
tff(f494,plain,
eq_prefix1(int,sF33,sF52,sK19),
inference(definition_folding,[],[f360,f484,f446]) ).
tff(f512,plain,
! [X2: ty,X3: uni,X1: uni] :
( ~ mem(X2,X3,remove(X2,X3,X1))
| ~ sort1(X2,X3) ),
inference(duplicate_literal_removal,[],[f435]) ).
tff(f519,definition,
( spl59_2
<=> ( sF43 = t2tb2(sK21) ) ),
introduced(definition,[new_symbols(definition,[spl59_2])],[avatar_definition]) ).
tff(f521,plain,
( ( sF43 = t2tb2(sK21) )
| ~ spl59_2 ),
inference(avatar_component_clause,[],[f519]) ).
tff(f522,plain,
spl59_2,
inference(avatar_split_clause,[],[f470,f519]) ).
tff(f549,definition,
( spl59_8
<=> $less(sK24,0) ),
introduced(definition,[new_symbols(definition,[spl59_8])],[avatar_definition]) ).
tff(f551,plain,
( ~ $less(sK24,0)
| spl59_8 ),
inference(avatar_component_clause,[],[f549]) ).
tff(f552,plain,
~ spl59_8,
inference(avatar_split_clause,[],[f366,f549]) ).
tff(f554,definition,
( spl59_9
<=> ( sF46 = tb2t1(sF45) ) ),
introduced(definition,[new_symbols(definition,[spl59_9])],[avatar_definition]) ).
tff(f556,plain,
( ( sF46 = tb2t1(sF45) )
| ~ spl59_9 ),
inference(avatar_component_clause,[],[f554]) ).
tff(f557,plain,
spl59_9,
inference(avatar_split_clause,[],[f474,f554]) ).
tff(f574,definition,
( spl59_13
<=> ( sK22 = sF51 ) ),
introduced(definition,[new_symbols(definition,[spl59_13])],[avatar_definition]) ).
tff(f576,plain,
( ( sK22 = sF51 )
| ~ spl59_13 ),
inference(avatar_component_clause,[],[f574]) ).
tff(f577,plain,
spl59_13,
inference(avatar_split_clause,[],[f483,f574]) ).
tff(f604,definition,
( spl59_19
<=> ( sF54 = set1(int,int,sF52,sF53,sF49) ) ),
introduced(definition,[new_symbols(definition,[spl59_19])],[avatar_definition]) ).
tff(f606,plain,
( ( sF54 = set1(int,int,sF52,sF53,sF49) )
| ~ spl59_19 ),
inference(avatar_component_clause,[],[f604]) ).
tff(f607,plain,
spl59_19,
inference(avatar_split_clause,[],[f486,f604]) ).
tff(f609,definition,
( spl59_20
<=> ( sF55 = tb2t2(sF54) ) ),
introduced(definition,[new_symbols(definition,[spl59_20])],[avatar_definition]) ).
tff(f611,plain,
( ( sF55 = tb2t2(sF54) )
| ~ spl59_20 ),
inference(avatar_component_clause,[],[f609]) ).
tff(f612,plain,
spl59_20,
inference(avatar_split_clause,[],[f487,f609]) ).
tff(f634,definition,
( spl59_25
<=> ( sF55 = sK21 ) ),
introduced(definition,[new_symbols(definition,[spl59_25])],[avatar_definition]) ).
tff(f636,plain,
( ( sF55 = sK21 )
| ~ spl59_25 ),
inference(avatar_component_clause,[],[f634]) ).
tff(f637,plain,
spl59_25,
inference(avatar_split_clause,[],[f488,f634]) ).
tff(f649,definition,
( spl59_28
<=> $less(sK24,sK22) ),
introduced(definition,[new_symbols(definition,[spl59_28])],[avatar_definition]) ).
tff(f651,plain,
( $less(sK24,sK22)
| ~ spl59_28 ),
inference(avatar_component_clause,[],[f649]) ).
tff(f652,plain,
spl59_28,
inference(avatar_split_clause,[],[f367,f649]) ).
tff(f654,definition,
( spl59_29
<=> mem(int,sF47,sF50) ),
introduced(definition,[new_symbols(definition,[spl59_29])],[avatar_definition]) ).
tff(f656,plain,
( mem(int,sF47,sF50)
| ~ spl59_29 ),
inference(avatar_component_clause,[],[f654]) ).
tff(f657,plain,
spl59_29,
inference(avatar_split_clause,[],[f481,f654]) ).
tff(f669,definition,
( spl59_32
<=> ( remove(int,sF49,sF30) = sF50 ) ),
introduced(definition,[new_symbols(definition,[spl59_32])],[avatar_definition]) ).
tff(f671,plain,
( ( remove(int,sF49,sF30) = sF50 )
| ~ spl59_32 ),
inference(avatar_component_clause,[],[f669]) ).
tff(f672,plain,
spl59_32,
inference(avatar_split_clause,[],[f480,f669]) ).
tff(f679,definition,
( spl59_34
<=> ( sF53 = t2tb1(sK19) ) ),
introduced(definition,[new_symbols(definition,[spl59_34])],[avatar_definition]) ).
tff(f681,plain,
( ( sF53 = t2tb1(sK19) )
| ~ spl59_34 ),
inference(avatar_component_clause,[],[f679]) ).
tff(f682,plain,
spl59_34,
inference(avatar_split_clause,[],[f485,f679]) ).
tff(f699,definition,
( spl59_38
<=> ( get(int,int,sF43,sF44) = sF45 ) ),
introduced(definition,[new_symbols(definition,[spl59_38])],[avatar_definition]) ).
tff(f701,plain,
( ( get(int,int,sF43,sF44) = sF45 )
| ~ spl59_38 ),
inference(avatar_component_clause,[],[f699]) ).
tff(f702,plain,
spl59_38,
inference(avatar_split_clause,[],[f473,f699]) ).
tff(f704,definition,
( spl59_39
<=> eq_prefix1(int,sF33,sF52,sK19) ),
introduced(definition,[new_symbols(definition,[spl59_39])],[avatar_definition]) ).
tff(f706,plain,
( eq_prefix1(int,sF33,sF52,sK19)
| ~ spl59_39 ),
inference(avatar_component_clause,[],[f704]) ).
tff(f707,plain,
spl59_39,
inference(avatar_split_clause,[],[f494,f704]) ).
tff(f709,definition,
( spl59_40
<=> ( sF51 = $sum(sK19,1) ) ),
introduced(definition,[new_symbols(definition,[spl59_40])],[avatar_definition]) ).
tff(f711,plain,
( ( sF51 = $sum(sK19,1) )
| ~ spl59_40 ),
inference(avatar_component_clause,[],[f709]) ).
tff(f712,plain,
spl59_40,
inference(avatar_split_clause,[],[f482,f709]) ).
tff(f724,definition,
( spl59_43
<=> ( sF47 = t2tb1(sK23) ) ),
introduced(definition,[new_symbols(definition,[spl59_43])],[avatar_definition]) ).
tff(f726,plain,
( ( sF47 = t2tb1(sK23) )
| ~ spl59_43 ),
inference(avatar_component_clause,[],[f724]) ).
tff(f727,plain,
spl59_43,
inference(avatar_split_clause,[],[f476,f724]) ).
tff(f744,definition,
( spl59_47
<=> ( sF49 = t2tb1(sF48) ) ),
introduced(definition,[new_symbols(definition,[spl59_47])],[avatar_definition]) ).
tff(f746,plain,
( ( sF49 = t2tb1(sF48) )
| ~ spl59_47 ),
inference(avatar_component_clause,[],[f744]) ).
tff(f747,plain,
spl59_47,
inference(avatar_split_clause,[],[f478,f744]) ).
tff(f749,definition,
( spl59_48
<=> ( sF44 = t2tb1(sK24) ) ),
introduced(definition,[new_symbols(definition,[spl59_48])],[avatar_definition]) ).
tff(f751,plain,
( ( sF44 = t2tb1(sK24) )
| ~ spl59_48 ),
inference(avatar_component_clause,[],[f749]) ).
tff(f752,plain,
spl59_48,
inference(avatar_split_clause,[],[f471,f749]) ).
tff(f754,definition,
( spl59_49
<=> ( sF46 = sK23 ) ),
introduced(definition,[new_symbols(definition,[spl59_49])],[avatar_definition]) ).
tff(f756,plain,
( ( sF46 = sK23 )
| ~ spl59_49 ),
inference(avatar_component_clause,[],[f754]) ).
tff(f757,plain,
spl59_49,
inference(avatar_split_clause,[],[f475,f754]) ).
tff(f758,plain,
( $less(sK24,sF51)
| ~ spl59_13
| ~ spl59_28 ),
inference(forward_demodulation,[],[f651,f576]) ).
tff(f760,definition,
( spl59_50
<=> $less(sK24,sF51) ),
introduced(definition,[new_symbols(definition,[spl59_50])],[avatar_definition]) ).
tff(f762,plain,
( $less(sK24,sF51)
| ~ spl59_50 ),
inference(avatar_component_clause,[],[f760]) ).
tff(f763,plain,
( spl59_50
| ~ spl59_13
| ~ spl59_28 ),
inference(avatar_split_clause,[],[f758,f649,f574,f760]) ).
tff(f872,plain,
( ( t2tb2(sF55) = sF43 )
| ~ spl59_2
| ~ spl59_25 ),
inference(forward_demodulation,[],[f521,f636]) ).
tff(f874,definition,
( spl59_56
<=> ( t2tb2(sF55) = sF43 ) ),
introduced(definition,[new_symbols(definition,[spl59_56])],[avatar_definition]) ).
tff(f876,plain,
( ( t2tb2(sF55) = sF43 )
| ~ spl59_56 ),
inference(avatar_component_clause,[],[f874]) ).
tff(f877,plain,
( spl59_56
| ~ spl59_2
| ~ spl59_25 ),
inference(avatar_split_clause,[],[f872,f634,f519,f874]) ).
tff(f917,plain,
( ( sK23 = tb2t1(sF45) )
| ~ spl59_9
| ~ spl59_49 ),
inference(forward_demodulation,[],[f556,f756]) ).
tff(f919,definition,
( spl59_64
<=> ( sK23 = tb2t1(sF45) ) ),
introduced(definition,[new_symbols(definition,[spl59_64])],[avatar_definition]) ).
tff(f921,plain,
( ( sK23 = tb2t1(sF45) )
| ~ spl59_64 ),
inference(avatar_component_clause,[],[f919]) ).
tff(f922,plain,
( spl59_64
| ~ spl59_9
| ~ spl59_49 ),
inference(avatar_split_clause,[],[f917,f754,f554,f919]) ).
tff(f1001,plain,
( sort1(int,sF53)
| ~ spl59_34 ),
inference(superposition,[],[f304,f681]) ).
tff(f1079,definition,
( spl59_91
<=> sort1(int,sF53) ),
introduced(definition,[new_symbols(definition,[spl59_91])],[avatar_definition]) ).
tff(f1082,plain,
( spl59_91
| ~ spl59_34 ),
inference(avatar_split_clause,[],[f1001,f679,f1079]) ).
tff(f1198,definition,
( spl59_112
<=> mem(int,sF47,sF30) ),
introduced(definition,[new_symbols(definition,[spl59_112])],[avatar_definition]) ).
tff(f1199,plain,
( ~ mem(int,sF47,sF30)
| spl59_112 ),
inference(avatar_component_clause,[],[f1198]) ).
tff(f1200,plain,
( mem(int,sF47,sF30)
| ~ spl59_112 ),
inference(avatar_component_clause,[],[f1198]) ).
tff(f1282,plain,
( sort1(int,sF49)
| ~ spl59_47 ),
inference(superposition,[],[f304,f746]) ).
tff(f1337,definition,
( spl59_138
<=> sort1(int,sF49) ),
introduced(definition,[new_symbols(definition,[spl59_138])],[avatar_definition]) ).
tff(f1340,plain,
( spl59_138
| ~ spl59_47 ),
inference(avatar_split_clause,[],[f1282,f744,f1337]) ).
tff(f1419,plain,
( ( sK19 = tb2t1(sF53) )
| ~ spl59_34 ),
inference(superposition,[],[f272,f681]) ).
tff(f1428,definition,
( spl59_157
<=> ( sK19 = tb2t1(sF53) ) ),
introduced(definition,[new_symbols(definition,[spl59_157])],[avatar_definition]) ).
tff(f1431,plain,
( spl59_157
| ~ spl59_34 ),
inference(avatar_split_clause,[],[f1419,f679,f1428]) ).
tff(f1455,plain,
( ( t2tb2(sF55) = sF54 )
| ~ spl59_20 ),
inference(superposition,[],[f295,f611]) ).
tff(f1463,definition,
( spl59_162
<=> ( t2tb2(sF55) = sF54 ) ),
introduced(definition,[new_symbols(definition,[spl59_162])],[avatar_definition]) ).
tff(f1465,plain,
( ( t2tb2(sF55) = sF54 )
| ~ spl59_162 ),
inference(avatar_component_clause,[],[f1463]) ).
tff(f1466,plain,
( spl59_162
| ~ spl59_20 ),
inference(avatar_split_clause,[],[f1455,f609,f1463]) ).
tff(f1495,plain,
( ( sF45 = t2tb1(sK23) )
| ~ spl59_64 ),
inference(superposition,[],[f307,f921]) ).
tff(f1499,plain,
! [X0: uni] : sort1(int,X0),
inference(superposition,[],[f304,f307]) ).
tff(f1520,definition,
( spl59_167
<=> ( sF45 = t2tb1(sK23) ) ),
introduced(definition,[new_symbols(definition,[spl59_167])],[avatar_definition]) ).
tff(f1522,plain,
( ( sF45 = t2tb1(sK23) )
| ~ spl59_167 ),
inference(avatar_component_clause,[],[f1520]) ).
tff(f1523,plain,
( spl59_167
| ~ spl59_64 ),
inference(avatar_split_clause,[],[f1495,f919,f1520]) ).
tff(f1570,plain,
( ( sF47 = sF45 )
| ~ spl59_43
| ~ spl59_167 ),
inference(superposition,[],[f726,f1522]) ).
tff(f1592,definition,
( spl59_175
<=> ( sF47 = sF45 ) ),
introduced(definition,[new_symbols(definition,[spl59_175])],[avatar_definition]) ).
tff(f1594,plain,
( ( sF47 = sF45 )
| ~ spl59_175 ),
inference(avatar_component_clause,[],[f1592]) ).
tff(f1595,plain,
( spl59_175
| ~ spl59_43
| ~ spl59_167 ),
inference(avatar_split_clause,[],[f1570,f1520,f724,f1592]) ).
tff(f1613,definition,
( spl59_179
<=> mem(int,sF45,sF30) ),
introduced(definition,[new_symbols(definition,[spl59_179])],[avatar_definition]) ).
tff(f1614,plain,
( mem(int,sF45,sF30)
| ~ spl59_179 ),
inference(avatar_component_clause,[],[f1613]) ).
tff(f1635,plain,
( mem(int,sF45,sF50)
| ~ spl59_29
| ~ spl59_175 ),
inference(superposition,[],[f656,f1594]) ).
tff(f1638,definition,
( spl59_182
<=> mem(int,sF45,sF50) ),
introduced(definition,[new_symbols(definition,[spl59_182])],[avatar_definition]) ).
tff(f1641,plain,
( spl59_182
| ~ spl59_29
| ~ spl59_175 ),
inference(avatar_split_clause,[],[f1635,f1592,f654,f1638]) ).
tff(f1645,plain,
( $less(sK24,$sum(sK19,1))
| ~ spl59_40
| ~ spl59_50 ),
inference(superposition,[],[f762,f711]) ).
tff(f1647,definition,
( spl59_183
<=> $less(sK24,$sum(sK19,1)) ),
introduced(definition,[new_symbols(definition,[spl59_183])],[avatar_definition]) ).
tff(f1650,plain,
( spl59_183
| ~ spl59_40
| ~ spl59_50 ),
inference(avatar_split_clause,[],[f1645,f760,f709,f1647]) ).
tff(f1835,plain,
( ( sF45 = get(int,int,sF43,t2tb1(sK24)) )
| ~ spl59_38
| ~ spl59_48 ),
inference(forward_demodulation,[],[f701,f751]) ).
tff(f1837,definition,
( spl59_208
<=> ( sF45 = get(int,int,sF43,t2tb1(sK24)) ) ),
introduced(definition,[new_symbols(definition,[spl59_208])],[avatar_definition]) ).
tff(f1839,plain,
( ( sF45 = get(int,int,sF43,t2tb1(sK24)) )
| ~ spl59_208 ),
inference(avatar_component_clause,[],[f1837]) ).
tff(f1840,plain,
( spl59_208
| ~ spl59_38
| ~ spl59_48 ),
inference(avatar_split_clause,[],[f1835,f749,f699,f1837]) ).
tff(f2076,plain,
( ~ mem(int,sF49,sF50)
| ~ sort1(int,sF49)
| ~ spl59_32 ),
inference(superposition,[],[f512,f671]) ).
tff(f2078,definition,
( spl59_221
<=> mem(int,sF49,sF50) ),
introduced(definition,[new_symbols(definition,[spl59_221])],[avatar_definition]) ).
tff(f2081,plain,
( ~ spl59_138
| ~ spl59_221
| ~ spl59_32 ),
inference(avatar_split_clause,[],[f2076,f669,f2078,f1337]) ).
tff(f2514,plain,
( ( get(int,int,sF54,sF53) = sF49 )
| ~ sort1(int,sF49)
| ~ spl59_19 ),
inference(superposition,[],[f434,f606]) ).
tff(f2519,definition,
( spl59_247
<=> ( get(int,int,sF54,sF53) = sF49 ) ),
introduced(definition,[new_symbols(definition,[spl59_247])],[avatar_definition]) ).
tff(f2522,plain,
( ~ spl59_138
| spl59_247
| ~ spl59_19 ),
inference(avatar_split_clause,[],[f2514,f604,f2519,f1337]) ).
tff(f2558,plain,
( ! [X0: uni] :
( ~ mem(int,X0,sF50)
| ~ sort1(int,sF49)
| ~ sort1(int,X0)
| mem(int,X0,sF30) )
| ~ spl59_32 ),
inference(superposition,[],[f338,f671]) ).
tff(f2561,definition,
( spl59_248
<=> ! [X0: uni] :
( ~ mem(int,X0,sF50)
| mem(int,X0,sF30)
| ~ sort1(int,X0) ) ),
introduced(definition,[new_symbols(definition,[spl59_248])],[avatar_definition]) ).
tff(f2562,plain,
( ! [X0: uni] :
( ~ sort1(int,X0)
| mem(int,X0,sF30)
| ~ mem(int,X0,sF50) )
| ~ spl59_248 ),
inference(avatar_component_clause,[],[f2561]) ).
tff(f2563,plain,
( spl59_248
| ~ spl59_138
| ~ spl59_32 ),
inference(avatar_split_clause,[],[f2558,f669,f1337,f2561]) ).
tff(f2791,plain,
! [X2: $int,X0: uni,X1: $int] :
( $less(X1,0)
| ~ $less(X1,sK19)
| ~ mem(int,t2tb1(tb2t1(get(int,int,X0,t2tb1(X1)))),sF30)
| $less(X1,0)
| ~ $less(X1,X2)
| ~ eq_prefix1(int,sF33,X0,X2) ),
inference(superposition,[],[f447,f320]) ).
tff(f2838,plain,
! [X2: $int,X0: uni,X1: $int] :
( ~ eq_prefix1(int,sF33,X0,X2)
| ~ mem(int,t2tb1(tb2t1(get(int,int,X0,t2tb1(X1)))),sF30)
| $less(X1,0)
| ~ $less(X1,sK19)
| ~ $less(X1,X2) ),
inference(duplicate_literal_removal,[],[f2791]) ).
tff(f2883,plain,
! [X2: $int,X0: uni,X1: $int] :
( ~ mem(int,get(int,int,X0,t2tb1(X1)),sF30)
| ~ eq_prefix1(int,sF33,X0,X2)
| ~ $less(X1,sK19)
| $less(X1,0)
| ~ $less(X1,X2) ),
inference(forward_demodulation,[],[f2838,f307]) ).
tff(f2965,plain,
( ! [X0: uni] :
( ( sF53 = X0 )
| ( get(int,int,sF52,X0) = get(int,int,sF54,X0) )
| ~ sort1(int,sF53)
| ~ sort1(int,X0) )
| ~ spl59_19 ),
inference(superposition,[],[f324,f606]) ).
tff(f2977,definition,
( spl59_264
<=> ! [X0: uni] :
( ( sF53 = X0 )
| ~ sort1(int,X0)
| ( get(int,int,sF52,X0) = get(int,int,sF54,X0) ) ) ),
introduced(definition,[new_symbols(definition,[spl59_264])],[avatar_definition]) ).
tff(f2978,plain,
( ! [X0: uni] :
( ( sF53 = X0 )
| ~ sort1(int,X0)
| ( get(int,int,sF52,X0) = get(int,int,sF54,X0) ) )
| ~ spl59_264 ),
inference(avatar_component_clause,[],[f2977]) ).
tff(f2979,plain,
( ~ spl59_91
| spl59_264
| ~ spl59_19 ),
inference(avatar_split_clause,[],[f2965,f604,f2977,f1079]) ).
tff(f3481,definition,
( spl59_296
<=> $less(sK24,sK19) ),
introduced(definition,[new_symbols(definition,[spl59_296])],[avatar_definition]) ).
tff(f6904,plain,
( ( sF43 = sF54 )
| ~ spl59_56
| ~ spl59_162 ),
inference(superposition,[],[f876,f1465]) ).
tff(f6997,definition,
( spl59_442
<=> ( sF43 = sF54 ) ),
introduced(definition,[new_symbols(definition,[spl59_442])],[avatar_definition]) ).
tff(f6999,plain,
( ( sF43 = sF54 )
| ~ spl59_442 ),
inference(avatar_component_clause,[],[f6997]) ).
tff(f7000,plain,
( spl59_442
| ~ spl59_56
| ~ spl59_162 ),
inference(avatar_split_clause,[],[f6904,f1463,f874,f6997]) ).
tff(f7050,plain,
( ( sF45 = get(int,int,sF54,t2tb1(sK24)) )
| ~ spl59_208
| ~ spl59_442 ),
inference(superposition,[],[f1839,f6999]) ).
tff(f7094,definition,
( spl59_451
<=> ( sF45 = get(int,int,sF54,t2tb1(sK24)) ) ),
introduced(definition,[new_symbols(definition,[spl59_451])],[avatar_definition]) ).
tff(f7096,plain,
( ( sF45 = get(int,int,sF54,t2tb1(sK24)) )
| ~ spl59_451 ),
inference(avatar_component_clause,[],[f7094]) ).
tff(f7097,plain,
( spl59_451
| ~ spl59_208
| ~ spl59_442 ),
inference(avatar_split_clause,[],[f7050,f6997,f1837,f7094]) ).
tff(f9025,plain,
( ! [X0: uni] :
( mem(int,X0,sF30)
| ~ mem(int,X0,sF50) )
| ~ spl59_248 ),
inference(forward_subsumption_resolution,[],[f2562,f1499]) ).
tff(f9043,plain,
( ~ mem(int,sF47,sF50)
| spl59_112
| ~ spl59_248 ),
inference(resolution,[],[f9025,f1199]) ).
tff(f9048,plain,
( $false
| ~ spl59_29
| spl59_112
| ~ spl59_248 ),
inference(forward_subsumption_resolution,[],[f9043,f656]) ).
tff(f9049,plain,
( ~ spl59_29
| spl59_112
| ~ spl59_248 ),
inference(avatar_contradiction_clause,[],[f9048]) ).
tff(f9092,plain,
( mem(int,sF45,sF30)
| ~ spl59_112
| ~ spl59_175 ),
inference(forward_demodulation,[],[f1200,f1594]) ).
tff(f9134,plain,
( spl59_179
| ~ spl59_112
| ~ spl59_175 ),
inference(avatar_split_clause,[],[f9092,f1592,f1198,f1613]) ).
tff(f11809,plain,
( ! [X0: uni] :
( ( get(int,int,sF52,X0) = get(int,int,sF54,X0) )
| ( sF53 = X0 ) )
| ~ spl59_264 ),
inference(forward_subsumption_resolution,[],[f2978,f1499]) ).
tff(f11810,plain,
( ( sF53 = t2tb1(sK24) )
| ( sF45 = get(int,int,sF52,t2tb1(sK24)) )
| ~ spl59_264
| ~ spl59_451 ),
inference(superposition,[],[f11809,f7096]) ).
tff(f11861,definition,
( spl59_769
<=> ( sF53 = t2tb1(sK24) ) ),
introduced(definition,[new_symbols(definition,[spl59_769])],[avatar_definition]) ).
tff(f11865,definition,
( spl59_770
<=> ( sF45 = get(int,int,sF52,t2tb1(sK24)) ) ),
introduced(definition,[new_symbols(definition,[spl59_770])],[avatar_definition]) ).
tff(f11867,plain,
( ( sF45 = get(int,int,sF52,t2tb1(sK24)) )
| ~ spl59_770 ),
inference(avatar_component_clause,[],[f11865]) ).
tff(f11904,plain,
( spl59_770
| spl59_769
| ~ spl59_264
| ~ spl59_451 ),
inference(avatar_split_clause,[],[f11810,f7094,f2977,f11861,f11865]) ).
tff(f15750,plain,
( ! [X0: $int] :
( ~ $less(sK24,sK19)
| ~ mem(int,sF45,sF30)
| ~ $less(sK24,X0)
| $less(sK24,0)
| ~ eq_prefix1(int,sF33,sF52,X0) )
| ~ spl59_770 ),
inference(superposition,[],[f2883,f11867]) ).
tff(f15766,plain,
( ! [X0: $int] :
( ~ $less(sK24,sK19)
| $less(sK24,0)
| ~ $less(sK24,X0)
| ~ eq_prefix1(int,sF33,sF52,X0) )
| ~ spl59_179
| ~ spl59_770 ),
inference(forward_subsumption_resolution,[],[f15750,f1614]) ).
tff(f15782,plain,
( ! [X0: $int] :
( ~ eq_prefix1(int,sF33,sF52,X0)
| ~ $less(sK24,X0)
| ~ $less(sK24,sK19) )
| spl59_8
| ~ spl59_179
| ~ spl59_770 ),
inference(forward_subsumption_resolution,[],[f15766,f551]) ).
tff(f15793,definition,
( spl59_844
<=> ! [X0: $int] :
( ~ eq_prefix1(int,sF33,sF52,X0)
| ~ $less(sK24,X0) ) ),
introduced(definition,[new_symbols(definition,[spl59_844])],[avatar_definition]) ).
tff(f15794,plain,
( ! [X0: $int] :
( ~ eq_prefix1(int,sF33,sF52,X0)
| ~ $less(sK24,X0) )
| ~ spl59_844 ),
inference(avatar_component_clause,[],[f15793]) ).
tff(f15795,plain,
( ~ spl59_296
| spl59_844
| spl59_8
| ~ spl59_179
| ~ spl59_770 ),
inference(avatar_split_clause,[],[f15782,f11865,f1613,f549,f15793,f3481]) ).
tff(f16276,plain,
( ~ $less(sK24,sK19)
| ~ spl59_39
| ~ spl59_844 ),
inference(resolution,[],[f15794,f706]) ).
tff(f16278,plain,
( ~ spl59_296
| ~ spl59_39
| ~ spl59_844 ),
inference(avatar_split_clause,[],[f16276,f15793,f704,f3481]) ).
tff(f16279,plain,
$false,
inference(avatar_smt_refutation,[],[f16278,f15795,f11904,f9134,f9049,f7097,f7000,f2979,f2563,f2522,f2081,f1840,f1650,f1641,f1595,f1523,f1466,f1431,f1340,f1082,f922,f877,f763,f757,f752,f747,f727,f712,f707,f702,f682,f672,f657,f652,f637,f612,f607,f577,f557,f552,f522]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW635_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.18 % Computer : n004.cluster.edu
% 0.12/0.18 % Model : x86_64 x86_64
% 0.12/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.18 % Memory : 8046.5625MB
% 0.12/0.18 % OS : Linux 6.8.0-71-generic
% 0.12/0.18 % CPULimit : 300
% 0.12/0.18 % WCLimit : 300
% 0.12/0.18 % DateTime : Mon Sep 28 14:23:22 UTC 2026
% 0.12/0.18 % CPUTime :
% 0.12/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.21 Running first-order theorem proving
% 0.12/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.53/1.27 % (382339)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.53/1.27 % (382404)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=513941909:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.53/1.27 % (382410)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=745185696:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.53/1.27 % (382407)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1476570182:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.53/1.27 % (382400)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2874087092:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.53/1.27 % (382403)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2727526331:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.53/1.27 % (382406)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=851942322:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.53/1.27 % (382407)Instruction limit reached!
% 3.53/1.27 % (382407)------------------------------
% 3.53/1.27 % (382407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.27 % (382407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.27 % (382407)CaDiCaL version: 2.1.3
% 3.53/1.27 % (382407)Termination reason: Instruction limit
% 3.53/1.27 % (382407)Termination phase: Preprocessing 3
% 3.53/1.27 % (382407)Time elapsed: 0.004 s
% 3.53/1.27 % (382407)Peak memory usage: 86 MB
% 3.53/1.27 % (382407)Instructions burned: 5 (million)
% 3.53/1.27 % (382406)Instruction limit reached!
% 3.53/1.27 % (382406)------------------------------
% 3.53/1.27 % (382406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.27 % (382406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.27 % (382406)CaDiCaL version: 2.1.3
% 3.53/1.27 % (382406)Termination reason: Instruction limit
% 3.53/1.27 % (382406)Termination phase: Property scanning
% 3.53/1.27 % (382406)Time elapsed: 0.008 s
% 3.53/1.27 % (382406)Peak memory usage: 86 MB
% 3.53/1.27 % (382406)Instructions burned: 8 (million)
% 3.53/1.27 % (382400)Instruction limit reached!
% 3.53/1.27 % (382400)------------------------------
% 3.53/1.27 % (382400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.27 % (382400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.27 % (382400)CaDiCaL version: 2.1.3
% 3.53/1.27 % (382400)Termination reason: Instruction limit
% 3.53/1.27 % (382400)Termination phase: Saturation
% 3.53/1.27 % (382400)Time elapsed: 0.015 s
% 3.53/1.27 % (382400)Peak memory usage: 95 MB
% 3.53/1.27 % (382400)Instructions burned: 12 (million)
% 3.53/1.27 % (382409)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2149781980:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.53/1.27 % (382410)Instruction limit reached!
% 3.53/1.27 % (382410)------------------------------
% 3.53/1.27 % (382410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.27 % (382410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.27 % (382410)CaDiCaL version: 2.1.3
% 3.53/1.27 % (382410)Termination reason: Instruction limit
% 3.53/1.27 % (382410)Termination phase: Saturation
% 3.53/1.27 % (382410)Time elapsed: 0.043 s
% 3.53/1.27 % (382410)Peak memory usage: 116 MB
% 3.53/1.27 % (382410)Instructions burned: 34 (million)
% 3.53/1.27 % (382404)Instruction limit reached!
% 3.53/1.27 % (382404)------------------------------
% 3.53/1.27 % (382404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.27 % (382404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.27 % (382404)CaDiCaL version: 2.1.3
% 3.53/1.27 % (382404)Termination reason: Instruction limit
% 3.53/1.27 % (382404)Termination phase: Saturation
% 3.53/1.27 % (382404)Time elapsed: 0.084 s
% 3.53/1.27 % (382404)Peak memory usage: 118 MB
% 3.53/1.27 % (382404)Instructions burned: 207 (million)
% 3.53/1.27 % (382409)Instruction limit reached!
% 3.53/1.27 % (382409)------------------------------
% 3.53/1.27 % (382409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.53/1.27 % (382409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/1.27 % (382409)CaDiCaL version: 2.1.3
% 3.53/1.27 % (382409)Termination reason: Instruction limit
% 4.91/1.41 % (382409)Termination phase: Saturation
% 4.91/1.41 % (382409)Time elapsed: 0.055 s
% 4.91/1.41 % (382409)Peak memory usage: 116 MB
% 4.91/1.41 % (382409)Instructions burned: 46 (million)
% 4.91/1.41 % (382456)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3293073004:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.91/1.41 % (382459)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2997482102:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.91/1.41 % (382457)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=1479596845:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.91/1.41 % (382456)Instruction limit reached!
% 4.91/1.41 % (382456)------------------------------
% 4.91/1.41 % (382456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.41 % (382456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.41 % (382456)CaDiCaL version: 2.1.3
% 4.91/1.41 % (382456)Termination reason: Instruction limit
% 4.91/1.41 % (382456)Termination phase: Saturation
% 4.91/1.41 % (382456)Time elapsed: 0.010 s
% 4.91/1.41 % (382456)Peak memory usage: 89 MB
% 4.91/1.41 % (382456)Instructions burned: 15 (million)
% 4.91/1.41 % (382471)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=1550398429:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.91/1.41 % (382459)Instruction limit reached!
% 4.91/1.41 % (382459)------------------------------
% 4.91/1.41 % (382459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.41 % (382459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.41 % (382459)CaDiCaL version: 2.1.3
% 4.91/1.41 % (382459)Termination reason: Instruction limit
% 4.91/1.41 % (382459)Termination phase: Saturation
% 4.91/1.41 % (382459)Time elapsed: 0.016 s
% 4.91/1.41 % (382459)Peak memory usage: 89 MB
% 4.91/1.41 % (382459)Instructions burned: 16 (million)
% 4.91/1.41 % (382471)Instruction limit reached!
% 4.91/1.41 % (382471)------------------------------
% 4.91/1.41 % (382471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.41 % (382471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.41 % (382471)CaDiCaL version: 2.1.3
% 4.91/1.41 % (382471)Termination reason: Instruction limit
% 4.91/1.41 % (382471)Termination phase: Saturation
% 4.91/1.41 % (382471)Time elapsed: 0.015 s
% 4.91/1.41 % (382471)Peak memory usage: 90 MB
% 4.91/1.41 % (382471)Instructions burned: 29 (million)
% 4.91/1.41 % (382457)Instruction limit reached!
% 4.91/1.41 % (382457)------------------------------
% 4.91/1.41 % (382457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.41 % (382457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.41 % (382457)CaDiCaL version: 2.1.3
% 4.91/1.41 % (382457)Termination reason: Instruction limit
% 4.91/1.41 % (382457)Termination phase: Saturation
% 4.91/1.41 % (382457)Time elapsed: 0.032 s
% 4.91/1.41 % (382457)Peak memory usage: 89 MB
% 4.91/1.41 % (382457)Instructions burned: 29 (million)
% 4.91/1.41 % (382468)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=912594310:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.91/1.41 % (382403)Instruction limit reached!
% 4.91/1.41 % (382403)------------------------------
% 4.91/1.41 % (382403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.41 % (382403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.41 % (382403)CaDiCaL version: 2.1.3
% 4.91/1.41 % (382403)Termination reason: Instruction limit
% 4.91/1.41 % (382403)Termination phase: Saturation
% 4.91/1.41 % (382403)Time elapsed: 0.243 s
% 4.91/1.41 % (382403)Peak memory usage: 117 MB
% 4.91/1.41 % (382403)Instructions burned: 308 (million)
% 4.91/1.41 % (382468)Instruction limit reached!
% 4.91/1.41 % (382468)------------------------------
% 4.91/1.41 % (382468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.41 % (382468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.41 % (382468)CaDiCaL version: 2.1.3
% 4.91/1.41 % (382468)Termination reason: Instruction limit
% 4.91/1.41 % (382468)Termination phase: Saturation
% 5.72/1.56 % (382468)Time elapsed: 0.016 s
% 5.72/1.56 % (382468)Peak memory usage: 89 MB
% 5.72/1.56 % (382468)Instructions burned: 24 (million)
% 5.72/1.56 % (382480)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2739825957:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 5.72/1.56 % (382513)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1552292800:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.72/1.56 % (382513)Instruction limit reached!
% 5.72/1.56 % (382513)------------------------------
% 5.72/1.56 % (382513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.56 % (382513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.56 % (382513)CaDiCaL version: 2.1.3
% 5.72/1.56 % (382513)Termination reason: Instruction limit
% 5.72/1.56 % (382513)Termination phase: Preprocessing 3
% 5.72/1.56 % (382513)Time elapsed: 0.002 s
% 5.72/1.56 % (382513)Peak memory usage: 86 MB
% 5.72/1.56 % (382513)Instructions burned: 5 (million)
% 5.72/1.56 % (382505)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2367289297:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.72/1.56 % (382505)Instruction limit reached!
% 5.72/1.56 % (382505)------------------------------
% 5.72/1.56 % (382505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.56 % (382505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.56 % (382505)CaDiCaL version: 2.1.3
% 5.72/1.56 % (382505)Termination reason: Instruction limit
% 5.72/1.56 % (382505)Termination phase: Preprocessing 1
% 5.72/1.56 % (382505)Time elapsed: 0.002 s
% 5.72/1.56 % (382505)Peak memory usage: 85 MB
% 5.72/1.56 % (382505)Instructions burned: 3 (million)
% 5.72/1.56 % (382508)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2828134254:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.72/1.56 % (382480)Instruction limit reached!
% 5.72/1.56 % (382480)------------------------------
% 5.72/1.56 % (382480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.56 % (382480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.56 % (382480)CaDiCaL version: 2.1.3
% 5.72/1.56 % (382480)Termination reason: Instruction limit
% 5.72/1.56 % (382480)Termination phase: Saturation
% 5.72/1.56 % (382480)Time elapsed: 0.052 s
% 5.72/1.56 % (382480)Peak memory usage: 89 MB
% 5.72/1.56 % (382480)Instructions burned: 87 (million)
% 5.72/1.56 % (382516)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2248326856:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.72/1.56 % (382519)lrs+10_1_thi=all:si=on:fd=off:random_seed=3763588485:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 5.72/1.56 % (382520)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=730601221:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.72/1.56 % (382520)Instruction limit reached!
% 5.72/1.56 % (382520)------------------------------
% 5.72/1.56 % (382520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.56 % (382520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.56 % (382520)CaDiCaL version: 2.1.3
% 5.72/1.56 % (382520)Termination reason: Instruction limit
% 5.72/1.56 % (382520)Termination phase: Property scanning
% 5.72/1.56 % (382520)Time elapsed: 0.005 s
% 5.72/1.56 % (382520)Peak memory usage: 86 MB
% 5.72/1.56 % (382520)Instructions burned: 9 (million)
% 5.72/1.56 % (382528)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2143023863:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.72/1.56 % (382528)Instruction limit reached!
% 5.72/1.56 % (382528)------------------------------
% 5.72/1.56 % (382528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.56 % (382528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.56 % (382528)CaDiCaL version: 2.1.3
% 5.72/1.56 % (382528)Termination reason: Instruction limit
% 5.72/1.56 % (382528)Termination phase: Preprocessing 1
% 5.72/1.56 % (382528)Time elapsed: 0.001 s
% 5.72/1.56 % (382528)Peak memory usage: 86 MB
% 5.72/1.56 % (382528)Instructions burned: 3 (million)
% 5.72/1.56 % (382516)Instruction limit reached!
% 7.13/1.77 % (382516)------------------------------
% 7.13/1.77 % (382516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.77 % (382516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.77 % (382516)CaDiCaL version: 2.1.3
% 7.13/1.77 % (382516)Termination reason: Instruction limit
% 7.13/1.77 % (382516)Termination phase: Saturation
% 7.13/1.77 % (382516)Time elapsed: 0.089 s
% 7.13/1.77 % (382516)Peak memory usage: 134 MB
% 7.13/1.77 % (382516)Instructions burned: 66 (million)
% 7.13/1.77 % (382527)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2917642091:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 7.13/1.77 % (382519)Instruction limit reached!
% 7.13/1.77 % (382519)------------------------------
% 7.13/1.77 % (382519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.77 % (382519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.77 % (382519)CaDiCaL version: 2.1.3
% 7.13/1.77 % (382519)Termination reason: Instruction limit
% 7.13/1.77 % (382519)Termination phase: Saturation
% 7.13/1.77 % (382519)Time elapsed: 0.060 s
% 7.13/1.77 % (382519)Peak memory usage: 116 MB
% 7.13/1.77 % (382519)Instructions burned: 54 (million)
% 7.13/1.77 % (382527)Instruction limit reached!
% 7.13/1.77 % (382527)------------------------------
% 7.13/1.77 % (382527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.77 % (382527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.77 % (382527)CaDiCaL version: 2.1.3
% 7.13/1.77 % (382527)Termination reason: Instruction limit
% 7.13/1.77 % (382527)Termination phase: Preprocessing 3
% 7.13/1.77 % (382527)Time elapsed: 0.002 s
% 7.13/1.77 % (382527)Peak memory usage: 86 MB
% 7.13/1.77 % (382527)Instructions burned: 3 (million)
% 7.13/1.77 % (382508)Instruction limit reached!
% 7.13/1.77 % (382508)------------------------------
% 7.13/1.77 % (382508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.77 % (382508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.77 % (382508)CaDiCaL version: 2.1.3
% 7.13/1.77 % (382508)Termination reason: Instruction limit
% 7.13/1.77 % (382508)Termination phase: Saturation
% 7.13/1.77 % (382508)Time elapsed: 0.127 s
% 7.13/1.78 % (382508)Peak memory usage: 92 MB
% 7.13/1.78 % (382508)Instructions burned: 182 (million)
% 7.13/1.78 % (382544)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=700401888:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.13/1.78 % (382578)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=333814474:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.13/1.78 % (382571)dis+10_1_si=on:random_seed=3350088867:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.13/1.78 % (382578)Instruction limit reached!
% 7.13/1.78 % (382578)------------------------------
% 7.13/1.78 % (382578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.78 % (382578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.78 % (382578)CaDiCaL version: 2.1.3
% 7.13/1.78 % (382578)Termination reason: Instruction limit
% 7.13/1.78 % (382578)Termination phase: Saturation
% 7.13/1.78 % (382578)Time elapsed: 0.010 s
% 7.13/1.78 % (382578)Peak memory usage: 89 MB
% 7.13/1.78 % (382578)Instructions burned: 27 (million)
% 7.13/1.78 % (382571)Instruction limit reached!
% 7.13/1.78 % (382571)------------------------------
% 7.13/1.78 % (382571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.78 % (382571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.78 % (382571)CaDiCaL version: 2.1.3
% 7.13/1.78 % (382571)Termination reason: Instruction limit
% 7.13/1.78 % (382571)Termination phase: Property scanning
% 7.13/1.78 % (382571)Time elapsed: 0.006 s
% 7.13/1.78 % (382571)Peak memory usage: 87 MB
% 7.13/1.78 % (382571)Instructions burned: 11 (million)
% 7.13/1.78 % (382597)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=631948567:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 7.13/1.78 % (382592)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=852616951: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_2993 on theBenchmark for (2993ds/35Mi)
% 7.13/1.78 % (382595)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3828465609:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.06/2.05 % (382595)Instruction limit reached!
% 10.06/2.05 % (382595)------------------------------
% 10.06/2.05 % (382595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.05 % (382595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.05 % (382595)CaDiCaL version: 2.1.3
% 10.06/2.05 % (382595)Termination reason: Instruction limit
% 10.06/2.05 % (382595)Termination phase: Property scanning
% 10.06/2.05 % (382595)Time elapsed: 0.001 s
% 10.06/2.05 % (382595)Peak memory usage: 85 MB
% 10.06/2.05 % (382595)Instructions burned: 2 (million)
% 10.06/2.05 % (382597)Instruction limit reached!
% 10.06/2.05 % (382597)------------------------------
% 10.06/2.05 % (382597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.05 % (382597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.05 % (382597)CaDiCaL version: 2.1.3
% 10.06/2.05 % (382597)Termination reason: Instruction limit
% 10.06/2.05 % (382597)Termination phase: Property scanning
% 10.06/2.05 % (382597)Time elapsed: 0.006 s
% 10.06/2.05 % (382597)Peak memory usage: 86 MB
% 10.06/2.05 % (382597)Instructions burned: 10 (million)
% 10.06/2.05 % (382544)Instruction limit reached!
% 10.06/2.05 % (382544)------------------------------
% 10.06/2.05 % (382544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.05 % (382544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.05 % (382544)CaDiCaL version: 2.1.3
% 10.06/2.05 % (382544)Termination reason: Instruction limit
% 10.06/2.05 % (382544)Termination phase: Saturation
% 10.06/2.05 % (382544)Time elapsed: 0.115 s
% 10.06/2.05 % (382544)Peak memory usage: 117 MB
% 10.06/2.05 % (382544)Instructions burned: 128 (million)
% 10.06/2.05 % (382592)Instruction limit reached!
% 10.06/2.05 % (382592)------------------------------
% 10.06/2.05 % (382592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.05 % (382592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.05 % (382592)CaDiCaL version: 2.1.3
% 10.06/2.05 % (382592)Termination reason: Instruction limit
% 10.06/2.05 % (382592)Termination phase: Saturation
% 10.06/2.05 % (382592)Time elapsed: 0.025 s
% 10.06/2.05 % (382592)Peak memory usage: 89 MB
% 10.06/2.05 % (382592)Instructions burned: 36 (million)
% 10.06/2.05 % (382604)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3502636340:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.06/2.05 % (382627)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=219070369:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 10.06/2.05 % (382627)Instruction limit reached!
% 10.06/2.05 % (382627)------------------------------
% 10.06/2.05 % (382627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.05 % (382627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.05 % (382627)CaDiCaL version: 2.1.3
% 10.06/2.05 % (382627)Termination reason: Instruction limit
% 10.06/2.05 % (382627)Termination phase: Saturation
% 10.06/2.05 % (382627)Time elapsed: 0.005 s
% 10.06/2.05 % (382627)Peak memory usage: 90 MB
% 10.06/2.05 % (382627)Instructions burned: 13 (million)
% 10.06/2.05 % (382628)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3595814269:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 10.06/2.05 % (382646)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=308412639:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.06/2.05 % (382644)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1619374701:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.06/2.05 % (382644)Instruction limit reached!
% 10.06/2.05 % (382644)------------------------------
% 10.06/2.05 % (382644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.05 % (382644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.05 % (382644)CaDiCaL version: 2.1.3
% 10.06/2.05 % (382644)Termination reason: Instruction limit
% 10.06/2.05 % (382644)Termination phase: Saturation
% 10.06/2.05 % (382644)Time elapsed: 0.006 s
% 10.06/2.05 % (382644)Peak memory usage: 87 MB
% 10.06/2.05 % (382644)Instructions burned: 10 (million)
% 10.06/2.05 % (382654)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=3043618090:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.70/2.24 % (382658)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4258333353:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 10.70/2.24 % (382656)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=1157260993:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 10.70/2.24 % (382654)Instruction limit reached!
% 10.70/2.24 % (382654)------------------------------
% 10.70/2.24 % (382654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.24 % (382654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.24 % (382654)CaDiCaL version: 2.1.3
% 10.70/2.24 % (382654)Termination reason: Instruction limit
% 10.70/2.24 % (382654)Termination phase: Saturation
% 10.70/2.24 % (382654)Time elapsed: 0.057 s
% 10.70/2.24 % (382654)Peak memory usage: 91 MB
% 10.70/2.24 % (382654)Instructions burned: 76 (million)
% 10.70/2.24 % (382658)Instruction limit reached!
% 10.70/2.24 % (382658)------------------------------
% 10.70/2.24 % (382658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.24 % (382658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.24 % (382658)CaDiCaL version: 2.1.3
% 10.70/2.24 % (382658)Termination reason: Instruction limit
% 10.70/2.24 % (382658)Termination phase: Saturation
% 10.70/2.24 % (382658)Time elapsed: 0.057 s
% 10.70/2.24 % (382658)Peak memory usage: 117 MB
% 10.70/2.24 % (382658)Instructions burned: 136 (million)
% 10.70/2.24 % (382646)Instruction limit reached!
% 10.70/2.24 % (382646)------------------------------
% 10.70/2.24 % (382646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.24 % (382646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.24 % (382646)CaDiCaL version: 2.1.3
% 10.70/2.24 % (382646)Termination reason: Instruction limit
% 10.70/2.24 % (382646)Termination phase: Saturation
% 10.70/2.24 % (382646)Time elapsed: 0.090 s
% 10.70/2.24 % (382646)Peak memory usage: 133 MB
% 10.70/2.25 % (382646)Instructions burned: 71 (million)
% 10.70/2.25 % (382604)Instruction limit reached!
% 10.70/2.25 % (382604)------------------------------
% 10.70/2.25 % (382604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.25 % (382604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.25 % (382604)CaDiCaL version: 2.1.3
% 10.70/2.25 % (382604)Termination reason: Instruction limit
% 10.70/2.25 % (382604)Termination phase: Saturation
% 10.70/2.25 % (382604)Time elapsed: 0.231 s
% 10.70/2.25 % (382604)Peak memory usage: 92 MB
% 10.70/2.25 % (382604)Instructions burned: 371 (million)
% 10.70/2.25 % (382628)Instruction limit reached!
% 10.70/2.25 % (382628)------------------------------
% 10.70/2.25 % (382628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.25 % (382628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.25 % (382628)CaDiCaL version: 2.1.3
% 10.70/2.25 % (382628)Termination reason: Instruction limit
% 10.70/2.25 % (382628)Termination phase: Saturation
% 10.70/2.25 % (382628)Time elapsed: 0.172 s
% 10.70/2.25 % (382628)Peak memory usage: 117 MB
% 10.70/2.25 % (382628)Instructions burned: 226 (million)
% 10.70/2.25 % (382662)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2757983730:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.70/2.25 % (382689)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1418363552:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.70/2.25 % (382685)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1101174343:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 10.70/2.25 % (382656)Instruction limit reached!
% 10.70/2.25 % (382656)------------------------------
% 10.70/2.25 % (382656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.25 % (382656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.25 % (382656)CaDiCaL version: 2.1.3
% 10.70/2.25 % (382656)Termination reason: Instruction limit
% 10.70/2.25 % (382656)Termination phase: Saturation
% 10.70/2.25 % (382656)Time elapsed: 0.208 s
% 10.70/2.25 % (382656)Peak memory usage: 91 MB
% 10.70/2.25 % (382656)Instructions burned: 295 (million)
% 13.04/2.60 % (382700)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1331915581:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 13.04/2.60 % (382714)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=396290118:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 13.04/2.60 % (382712)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2159611789:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 13.04/2.60 % (382685)Instruction limit reached!
% 13.04/2.60 % (382685)------------------------------
% 13.04/2.60 % (382685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.04/2.60 % (382685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.04/2.60 % (382685)CaDiCaL version: 2.1.3
% 13.04/2.60 % (382685)Termination reason: Instruction limit
% 13.04/2.60 % (382685)Termination phase: Saturation
% 13.04/2.60 % (382685)Time elapsed: 0.066 s
% 13.04/2.60 % (382685)Peak memory usage: 134 MB
% 13.04/2.60 % (382685)Instructions burned: 40 (million)
% 13.04/2.60 % (382689)Instruction limit reached!
% 13.04/2.60 % (382689)------------------------------
% 13.04/2.60 % (382689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.04/2.60 % (382689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.04/2.60 % (382689)CaDiCaL version: 2.1.3
% 13.04/2.60 % (382689)Termination reason: Instruction limit
% 13.04/2.60 % (382689)Termination phase: Saturation
% 13.04/2.60 % (382689)Time elapsed: 0.103 s
% 13.04/2.60 % (382689)Peak memory usage: 92 MB
% 13.04/2.60 % (382689)Instructions burned: 308 (million)
% 13.04/2.60 % (382662)Instruction limit reached!
% 13.04/2.60 % (382662)------------------------------
% 13.04/2.60 % (382662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.04/2.60 % (382662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.04/2.60 % (382662)CaDiCaL version: 2.1.3
% 13.04/2.60 % (382662)Termination reason: Instruction limit
% 13.04/2.60 % (382662)Termination phase: Saturation
% 13.04/2.60 % (382662)Time elapsed: 0.134 s
% 13.04/2.60 % (382662)Peak memory usage: 134 MB
% 13.04/2.60 % (382662)Instructions burned: 131 (million)
% 13.04/2.60 % (382721)dis+10_1_si=on:random_seed=1972398689:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 13.04/2.60 % (382725)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2569439502:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 13.04/2.60 % (382712)Instruction limit reached!
% 13.04/2.60 % (382712)------------------------------
% 13.04/2.60 % (382712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.04/2.60 % (382712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.04/2.60 % (382712)CaDiCaL version: 2.1.3
% 13.04/2.60 % (382712)Termination reason: Instruction limit
% 13.04/2.60 % (382712)Termination phase: Saturation
% 13.04/2.60 % (382712)Time elapsed: 0.113 s
% 13.04/2.60 % (382712)Peak memory usage: 117 MB
% 13.04/2.60 % (382712)Instructions burned: 132 (million)
% 13.04/2.60 % (382726)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2163295593:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 13.04/2.60 % (382727)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4157649687:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 13.04/2.60 % (382714)Instruction limit reached!
% 13.04/2.60 % (382714)------------------------------
% 13.04/2.60 % (382714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.04/2.60 % (382714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.04/2.60 % (382714)CaDiCaL version: 2.1.3
% 13.04/2.60 % (382714)Termination reason: Instruction limit
% 13.04/2.60 % (382714)Termination phase: Saturation
% 13.04/2.60 % (382714)Time elapsed: 0.195 s
% 13.04/2.60 % (382714)Peak memory usage: 117 MB
% 13.04/2.60 % (382714)Instructions burned: 260 (million)
% 13.04/2.60 % (382727)Instruction limit reached!
% 13.04/2.60 % (382727)------------------------------
% 13.04/2.60 % (382727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.04/2.60 % (382727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382727)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382727)Termination reason: Instruction limit
% 14.88/2.94 % (382727)Termination phase: Saturation
% 14.88/2.94 % (382727)Time elapsed: 0.065 s
% 14.88/2.94 % (382727)Peak memory usage: 116 MB
% 14.88/2.94 % (382727)Instructions burned: 66 (million)
% 14.88/2.94 % (382725)Instruction limit reached!
% 14.88/2.94 % (382725)------------------------------
% 14.88/2.94 % (382725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.94 % (382725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382725)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382725)Termination reason: Instruction limit
% 14.88/2.94 % (382725)Termination phase: Saturation
% 14.88/2.94 % (382725)Time elapsed: 0.132 s
% 14.88/2.94 % (382725)Peak memory usage: 95 MB
% 14.88/2.94 % (382725)Instructions burned: 384 (million)
% 14.88/2.94 % (382726)Instruction limit reached!
% 14.88/2.94 % (382726)------------------------------
% 14.88/2.94 % (382726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.94 % (382726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382726)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382726)Termination reason: Instruction limit
% 14.88/2.94 % (382726)Termination phase: Saturation
% 14.88/2.94 % (382726)Time elapsed: 0.096 s
% 14.88/2.94 % (382726)Peak memory usage: 91 MB
% 14.88/2.94 % (382726)Instructions burned: 142 (million)
% 14.88/2.94 % (382730)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=317115859:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 14.88/2.94 % (382733)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=2356989629:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 14.88/2.94 % (382735)dis+1010_1_to=kbo:si=on:random_seed=799884030:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 14.88/2.94 % (382730)Instruction limit reached!
% 14.88/2.94 % (382730)------------------------------
% 14.88/2.94 % (382730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.94 % (382730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382730)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382730)Termination reason: Instruction limit
% 14.88/2.94 % (382730)Termination phase: Saturation
% 14.88/2.94 % (382730)Time elapsed: 0.082 s
% 14.88/2.94 % (382730)Peak memory usage: 90 MB
% 14.88/2.94 % (382730)Instructions burned: 121 (million)
% 14.88/2.94 % (382734)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2512321830:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 14.88/2.94 % (382700)Instruction limit reached!
% 14.88/2.94 % (382700)------------------------------
% 14.88/2.94 % (382700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.94 % (382700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382700)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382700)Termination reason: Instruction limit
% 14.88/2.94 % (382700)Termination phase: Saturation
% 14.88/2.94 % (382700)Time elapsed: 0.429 s
% 14.88/2.94 % (382700)Peak memory usage: 139 MB
% 14.88/2.94 % (382700)Instructions burned: 599 (million)
% 14.88/2.94 % (382736)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3143773369:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi)
% 14.88/2.94 % (382735)Instruction limit reached!
% 14.88/2.94 % (382735)------------------------------
% 14.88/2.94 % (382735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.94 % (382735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382735)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382735)Termination reason: Instruction limit
% 14.88/2.94 % (382735)Termination phase: Saturation
% 14.88/2.94 % (382735)Time elapsed: 0.069 s
% 14.88/2.94 % (382735)Peak memory usage: 91 MB
% 14.88/2.94 % (382735)Instructions burned: 177 (million)
% 14.88/2.94 % (382734)Instruction limit reached!
% 14.88/2.94 % (382734)------------------------------
% 14.88/2.94 % (382734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.94 % (382734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.94 % (382734)CaDiCaL version: 2.1.3
% 14.88/2.94 % (382734)Termination reason: Instruction limit
% 14.88/2.94 % (382734)Termination phase: Saturation
% 17.79/3.27 % (382734)Time elapsed: 0.048 s
% 17.79/3.27 % (382734)Peak memory usage: 116 MB
% 17.79/3.27 % (382734)Instructions burned: 39 (million)
% 17.79/3.27 % (382733)Instruction limit reached!
% 17.79/3.27 % (382733)------------------------------
% 17.79/3.27 % (382733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.27 % (382733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.27 % (382733)CaDiCaL version: 2.1.3
% 17.79/3.27 % (382733)Termination reason: Instruction limit
% 17.79/3.27 % (382733)Termination phase: Saturation
% 17.79/3.27 % (382733)Time elapsed: 0.105 s
% 17.79/3.27 % (382733)Peak memory usage: 118 MB
% 17.79/3.27 % (382733)Instructions burned: 128 (million)
% 17.79/3.27 % (382740)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4077587343:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 17.79/3.27 % (382743)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3502102204:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 17.79/3.27 % (382744)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1202219447:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi)
% 17.79/3.27 % (382745)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3084084246:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi)
% 17.79/3.27 % (382746)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1088445958:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi)
% 17.79/3.27 % (382736)Instruction limit reached!
% 17.79/3.27 % (382736)------------------------------
% 17.79/3.27 % (382736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.27 % (382736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.27 % (382736)CaDiCaL version: 2.1.3
% 17.79/3.27 % (382736)Termination reason: Instruction limit
% 17.79/3.27 % (382736)Termination phase: Saturation
% 17.79/3.27 % (382736)Time elapsed: 0.217 s
% 17.79/3.27 % (382736)Peak memory usage: 119 MB
% 17.79/3.27 % (382736)Instructions burned: 330 (million)
% 17.79/3.27 % (382743)Instruction limit reached!
% 17.79/3.27 % (382743)------------------------------
% 17.79/3.27 % (382743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.27 % (382743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.27 % (382743)CaDiCaL version: 2.1.3
% 17.79/3.27 % (382743)Termination reason: Instruction limit
% 17.79/3.27 % (382743)Termination phase: Saturation
% 17.79/3.27 % (382743)Time elapsed: 0.168 s
% 17.79/3.27 % (382743)Peak memory usage: 136 MB
% 17.79/3.27 % (382743)Instructions burned: 216 (million)
% 17.79/3.27 % (382721)Instruction limit reached!
% 17.79/3.27 % (382721)------------------------------
% 17.79/3.27 % (382721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.27 % (382721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.27 % (382721)CaDiCaL version: 2.1.3
% 17.79/3.27 % (382721)Termination reason: Instruction limit
% 17.79/3.27 % (382721)Termination phase: Saturation
% 17.79/3.27 % (382721)Time elapsed: 0.619 s
% 17.79/3.27 % (382721)Peak memory usage: 96 MB
% 17.79/3.27 % (382721)Instructions burned: 1001 (million)
% 17.79/3.27 % (382744)Instruction limit reached!
% 17.79/3.27 % (382744)------------------------------
% 17.79/3.27 % (382744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.27 % (382744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.27 % (382744)CaDiCaL version: 2.1.3
% 17.79/3.27 % (382744)Termination reason: Instruction limit
% 17.79/3.27 % (382744)Termination phase: Saturation
% 17.79/3.27 % (382744)Time elapsed: 0.162 s
% 17.79/3.27 % (382744)Peak memory usage: 118 MB
% 17.79/3.27 % (382744)Instructions burned: 350 (million)
% 17.79/3.27 % (382745)Instruction limit reached!
% 17.79/3.27 % (382745)------------------------------
% 17.79/3.27 % (382745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.27 % (382745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.27 % (382745)CaDiCaL version: 2.1.3
% 17.79/3.27 % (382745)Termination reason: Instruction limit
% 17.79/3.27 % (382745)Termination phase: Saturation
% 17.79/3.27 % (382745)Time elapsed: 0.167 s
% 17.79/3.27 % (382745)Peak memory usage: 90 MB
% 17.79/3.27 % (382745)Instructions burned: 295 (million)
% 17.79/3.27 % (382752)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1124198525:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 19.46/3.50 % (382746)Instruction limit reached!
% 19.46/3.50 % (382746)------------------------------
% 19.46/3.50 % (382746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.50 % (382746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.50 % (382746)CaDiCaL version: 2.1.3
% 19.46/3.50 % (382746)Termination reason: Instruction limit
% 19.46/3.50 % (382746)Termination phase: Saturation
% 19.46/3.50 % (382746)Time elapsed: 0.217 s
% 19.46/3.50 % (382746)Peak memory usage: 118 MB
% 19.46/3.50 % (382746)Instructions burned: 329 (million)
% 19.46/3.50 % (382755)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3276922741:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi)
% 19.46/3.50 % (382753)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2880254727:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 19.46/3.50 % (382740)Instruction limit reached!
% 19.46/3.50 % (382740)------------------------------
% 19.46/3.50 % (382740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.50 % (382740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.50 % (382740)CaDiCaL version: 2.1.3
% 19.46/3.50 % (382740)Termination reason: Instruction limit
% 19.46/3.50 % (382740)Termination phase: Saturation
% 19.46/3.50 % (382740)Time elapsed: 0.363 s
% 19.46/3.50 % (382740)Peak memory usage: 135 MB
% 19.46/3.50 % (382740)Instructions burned: 484 (million)
% 19.46/3.50 % (382754)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1760040577:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi)
% 19.46/3.50 % (382756)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=521822293:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi)
% 19.46/3.50 % (382758)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=251667316:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi)
% 19.46/3.50 % (382755)Instruction limit reached!
% 19.46/3.50 % (382755)------------------------------
% 19.46/3.50 % (382755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.50 % (382755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.50 % (382755)CaDiCaL version: 2.1.3
% 19.46/3.50 % (382755)Termination reason: Instruction limit
% 19.46/3.50 % (382755)Termination phase: Saturation
% 19.46/3.50 % (382755)Time elapsed: 0.153 s
% 19.46/3.50 % (382755)Peak memory usage: 119 MB
% 19.46/3.50 % (382755)Instructions burned: 419 (million)
% 19.46/3.50 % (382752)Instruction limit reached!
% 19.46/3.50 % (382752)------------------------------
% 19.46/3.50 % (382752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.50 % (382752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.50 % (382752)CaDiCaL version: 2.1.3
% 19.46/3.50 % (382752)Termination reason: Instruction limit
% 19.46/3.50 % (382752)Termination phase: Saturation
% 19.46/3.50 % (382752)Time elapsed: 0.208 s
% 19.46/3.50 % (382752)Peak memory usage: 118 MB
% 19.46/3.50 % (382752)Instructions burned: 282 (million)
% 19.46/3.50 % (382761)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=53194253:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 19.46/3.50 % (382754)Instruction limit reached!
% 19.46/3.50 % (382754)------------------------------
% 19.46/3.50 % (382754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.50 % (382754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.50 % (382754)CaDiCaL version: 2.1.3
% 19.46/3.50 % (382754)Termination reason: Instruction limit
% 19.46/3.50 % (382754)Termination phase: Saturation
% 19.46/3.50 % (382754)Time elapsed: 0.156 s
% 19.46/3.50 % (382754)Peak memory usage: 113 MB
% 19.46/3.50 % (382754)Instructions burned: 322 (million)
% 19.46/3.50 % (382765)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1851705618:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 19.46/3.50 % (382753)Instruction limit reached!
% 19.46/3.50 % (382753)------------------------------
% 19.46/3.50 % (382753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.00 % (382753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.00 % (382753)CaDiCaL version: 2.1.3
% 20.20/4.00 % (382753)Termination reason: Instruction limit
% 20.20/4.00 % (382753)Termination phase: Saturation
% 20.20/4.00 % (382753)Time elapsed: 0.285 s
% 20.20/4.00 % (382753)Peak memory usage: 93 MB
% 20.20/4.00 % (382753)Instructions burned: 485 (million)
% 20.20/4.00 % (382766)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=4123398257:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2978 on theBenchmark for (2978ds/513Mi)
% 20.20/4.00 % (382758)Instruction limit reached!
% 20.20/4.00 % (382758)------------------------------
% 20.20/4.00 % (382758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.00 % (382758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.00 % (382758)CaDiCaL version: 2.1.3
% 20.20/4.00 % (382758)Termination reason: Instruction limit
% 20.20/4.00 % (382758)Termination phase: Saturation
% 20.20/4.00 % (382758)Time elapsed: 0.228 s
% 20.20/4.00 % (382758)Peak memory usage: 135 MB
% 20.20/4.00 % (382758)Instructions burned: 277 (million)
% 20.20/4.00 % (382756)Instruction limit reached!
% 20.20/4.00 % (382756)------------------------------
% 20.20/4.00 % (382756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.00 % (382756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.00 % (382756)CaDiCaL version: 2.1.3
% 20.20/4.00 % (382756)Termination reason: Instruction limit
% 20.20/4.00 % (382756)Termination phase: Saturation
% 20.20/4.00 % (382756)Time elapsed: 0.304 s
% 20.20/4.00 % (382756)Peak memory usage: 118 MB
% 20.20/4.00 % (382756)Instructions burned: 471 (million)
% 20.20/4.00 % (382768)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1895691380:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 20.20/4.00 % (382765)Instruction limit reached!
% 20.20/4.00 % (382765)------------------------------
% 20.20/4.00 % (382765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.00 % (382765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.00 % (382765)CaDiCaL version: 2.1.3
% 20.20/4.00 % (382765)Termination reason: Instruction limit
% 20.20/4.00 % (382765)Termination phase: Saturation
% 20.20/4.00 % (382765)Time elapsed: 0.145 s
% 20.20/4.00 % (382765)Peak memory usage: 119 MB
% 20.20/4.00 % (382765)Instructions burned: 388 (million)
% 20.20/4.00 % (382761)Instruction limit reached!
% 20.20/4.00 % (382761)------------------------------
% 20.20/4.00 % (382761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.00 % (382761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.00 % (382761)CaDiCaL version: 2.1.3
% 20.20/4.00 % (382761)Termination reason: Instruction limit
% 20.20/4.00 % (382761)Termination phase: Saturation
% 20.20/4.00 % (382761)Time elapsed: 0.249 s
% 20.20/4.00 % (382761)Peak memory usage: 118 MB
% 20.20/4.00 % (382761)Instructions burned: 376 (million)
% 20.20/4.00 % (382770)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2707618914:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi)
% 20.20/4.00 % (382773)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4096703674:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi)
% 20.20/4.00 % (382774)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=535306120:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi)
% 20.20/4.00 % (382775)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=1747466973:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 20.20/4.00 % (382777)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=8269939:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi)
% 20.20/4.00 % (382768)Instruction limit reached!
% 20.20/4.00 % (382768)------------------------------
% 20.20/4.00 % (382768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.00 % (382768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382768)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382768)Termination reason: Instruction limit
% 25.67/4.41 % (382768)Termination phase: Saturation
% 25.67/4.41 % (382768)Time elapsed: 0.261 s
% 25.67/4.41 % (382768)Peak memory usage: 135 MB
% 25.67/4.41 % (382768)Instructions burned: 334 (million)
% 25.67/4.41 % (382766)Instruction limit reached!
% 25.67/4.41 % (382766)------------------------------
% 25.67/4.41 % (382766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/4.41 % (382766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382766)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382766)Termination reason: Instruction limit
% 25.67/4.41 % (382766)Termination phase: Saturation
% 25.67/4.41 % (382766)Time elapsed: 0.324 s
% 25.67/4.41 % (382766)Peak memory usage: 93 MB
% 25.67/4.41 % (382766)Instructions burned: 513 (million)
% 25.67/4.41 % (382775)Instruction limit reached!
% 25.67/4.41 % (382775)------------------------------
% 25.67/4.41 % (382775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/4.41 % (382775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382775)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382775)Termination reason: Instruction limit
% 25.67/4.41 % (382775)Termination phase: Saturation
% 25.67/4.41 % (382775)Time elapsed: 0.097 s
% 25.67/4.41 % (382775)Peak memory usage: 117 MB
% 25.67/4.41 % (382775)Instructions burned: 237 (million)
% 25.67/4.41 % (382770)Instruction limit reached!
% 25.67/4.41 % (382770)------------------------------
% 25.67/4.41 % (382770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/4.41 % (382770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382770)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382770)Termination reason: Instruction limit
% 25.67/4.41 % (382770)Termination phase: Saturation
% 25.67/4.41 % (382770)Time elapsed: 0.231 s
% 25.67/4.41 % (382770)Peak memory usage: 91 MB
% 25.67/4.41 % (382770)Instructions burned: 360 (million)
% 25.67/4.41 % (382774)Instruction limit reached!
% 25.67/4.41 % (382774)------------------------------
% 25.67/4.41 % (382774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/4.41 % (382774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382774)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382774)Termination reason: Instruction limit
% 25.67/4.41 % (382774)Termination phase: Saturation
% 25.67/4.41 % (382774)Time elapsed: 0.178 s
% 25.67/4.41 % (382774)Peak memory usage: 117 MB
% 25.67/4.41 % (382774)Instructions burned: 262 (million)
% 25.67/4.41 % (382784)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=2715051538:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 25.67/4.41 % (382782)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3955301826:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi)
% 25.67/4.41 % (382783)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=493312988:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 25.67/4.41 % (382773)Instruction limit reached!
% 25.67/4.41 % (382773)------------------------------
% 25.67/4.41 % (382773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/4.41 % (382773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382773)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382773)Termination reason: Instruction limit
% 25.67/4.41 % (382773)Termination phase: Saturation
% 25.67/4.41 % (382773)Time elapsed: 0.272 s
% 25.67/4.41 % (382773)Peak memory usage: 121 MB
% 25.67/4.41 % (382773)Instructions burned: 342 (million)
% 25.67/4.41 % (382777)Instruction limit reached!
% 25.67/4.41 % (382777)------------------------------
% 25.67/4.41 % (382777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/4.41 % (382777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/4.41 % (382777)CaDiCaL version: 2.1.3
% 25.67/4.41 % (382777)Termination reason: Instruction limit
% 25.67/4.41 % (382777)Termination phase: Saturation
% 25.67/4.41 % (382777)Time elapsed: 0.201 s
% 25.67/4.41 % (382777)Peak memory usage: 92 MB
% 25.67/4.41 % (382777)Instructions burned: 274 (million)
% 25.67/4.41 % (382785)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2137824294:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi)
% 25.67/4.41 % (382786)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2573727219:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2973 on theBenchmark for (2973ds/655Mi)
% 28.14/5.01 % (382782)Instruction limit reached!
% 28.14/5.01 % (382782)------------------------------
% 28.14/5.01 % (382782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (382782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (382782)CaDiCaL version: 2.1.3
% 28.14/5.01 % (382782)Termination reason: Instruction limit
% 28.14/5.01 % (382782)Termination phase: Saturation
% 28.14/5.01 % (382782)Time elapsed: 0.100 s
% 28.14/5.01 % (382782)Peak memory usage: 91 MB
% 28.14/5.01 % (382782)Instructions burned: 147 (million)
% 28.14/5.01 % (382784)Instruction limit reached!
% 28.14/5.01 % (382784)------------------------------
% 28.14/5.01 % (382784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (382784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (382784)CaDiCaL version: 2.1.3
% 28.14/5.01 % (382784)Termination reason: Instruction limit
% 28.14/5.01 % (382784)Termination phase: Saturation
% 28.14/5.01 % (382784)Time elapsed: 0.124 s
% 28.14/5.01 % (382784)Peak memory usage: 134 MB
% 28.14/5.01 % (382784)Instructions burned: 277 (million)
% 28.14/5.01 % (382790)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=248823472:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi)
% 28.14/5.01 % (382791)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2437809013:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 28.14/5.01 % (382795)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 28.14/5.01 % (382795)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3933498747:i=1090:aac=none:nm=0:rtra=on:rawr=on_2971 on theBenchmark for (2971ds/1090Mi)
% 28.14/5.01 % (382794)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2563287587:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 28.14/5.01 % (382791)Instruction limit reached!
% 28.14/5.01 % (382791)------------------------------
% 28.14/5.01 % (382791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (382791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (382791)CaDiCaL version: 2.1.3
% 28.14/5.01 % (382791)Termination reason: Instruction limit
% 28.14/5.01 % (382791)Termination phase: Saturation
% 28.14/5.01 % (382791)Time elapsed: 0.091 s
% 28.14/5.01 % (382791)Peak memory usage: 117 MB
% 28.14/5.01 % (382791)Instructions burned: 108 (million)
% 28.14/5.01 % (382800)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3027079937:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi)
% 28.14/5.01 % (382786)Instruction limit reached!
% 28.14/5.01 % (382786)------------------------------
% 28.14/5.01 % (382786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (382786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (382786)CaDiCaL version: 2.1.3
% 28.14/5.01 % (382786)Termination reason: Instruction limit
% 28.14/5.01 % (382786)Termination phase: Saturation
% 28.14/5.01 % (382786)Time elapsed: 0.434 s
% 28.14/5.01 % (382786)Peak memory usage: 94 MB
% 28.14/5.01 % (382786)Instructions burned: 655 (million)
% 28.14/5.01 % (382794)Instruction limit reached!
% 28.14/5.01 % (382794)------------------------------
% 28.14/5.01 % (382794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (382794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (382794)CaDiCaL version: 2.1.3
% 28.14/5.01 % (382794)Termination reason: Instruction limit
% 28.14/5.01 % (382794)Termination phase: Saturation
% 28.14/5.01 % (382794)Time elapsed: 0.338 s
% 28.14/5.01 % (382794)Peak memory usage: 135 MB
% 28.14/5.01 % (382794)Instructions burned: 450 (million)
% 28.14/5.01 % (382795)Instruction limit reached!
% 28.14/5.01 % (382795)------------------------------
% 28.14/5.01 % (382795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (382795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (382795)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382795)Termination reason: Instruction limit
% 33.28/5.68 % (382795)Termination phase: Saturation
% 33.28/5.68 % (382795)Time elapsed: 0.358 s
% 33.28/5.68 % (382795)Peak memory usage: 121 MB
% 33.28/5.68 % (382795)Instructions burned: 1090 (million)
% 33.28/5.68 % (382800)Instruction limit reached!
% 33.28/5.68 % (382800)------------------------------
% 33.28/5.68 % (382800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.28/5.68 % (382800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.28/5.68 % (382800)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382800)Termination reason: Instruction limit
% 33.28/5.68 % (382800)Termination phase: Saturation
% 33.28/5.68 % (382800)Time elapsed: 0.155 s
% 33.28/5.68 % (382800)Peak memory usage: 117 MB
% 33.28/5.68 % (382800)Instructions burned: 131 (million)
% 33.28/5.68 % (382802)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4052769944:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi)
% 33.28/5.68 % (382804)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=342364037:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi)
% 33.28/5.68 % (382803)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3181564747:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi)
% 33.28/5.68 % (382805)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3675744339:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi)
% 33.28/5.68 % (382785)Instruction limit reached!
% 33.28/5.68 % (382785)------------------------------
% 33.28/5.68 % (382785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.28/5.68 % (382785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.28/5.68 % (382785)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382785)Termination reason: Instruction limit
% 33.28/5.68 % (382785)Termination phase: Saturation
% 33.28/5.68 % (382785)Time elapsed: 0.709 s
% 33.28/5.68 % (382785)Peak memory usage: 95 MB
% 33.28/5.68 % (382785)Instructions burned: 1053 (million)
% 33.28/5.68 % (382802)Instruction limit reached!
% 33.28/5.68 % (382802)------------------------------
% 33.28/5.68 % (382802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.28/5.68 % (382802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.28/5.68 % (382802)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382802)Termination reason: Instruction limit
% 33.28/5.68 % (382802)Termination phase: Saturation
% 33.28/5.68 % (382802)Time elapsed: 0.206 s
% 33.28/5.68 % (382802)Peak memory usage: 118 MB
% 33.28/5.68 % (382802)Instructions burned: 313 (million)
% 33.28/5.68 % (382790)Instruction limit reached!
% 33.28/5.68 % (382790)------------------------------
% 33.28/5.68 % (382790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.28/5.68 % (382790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.28/5.68 % (382790)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382790)Termination reason: Instruction limit
% 33.28/5.68 % (382790)Termination phase: Saturation
% 33.28/5.68 % (382790)Time elapsed: 0.724 s
% 33.28/5.68 % (382790)Peak memory usage: 97 MB
% 33.28/5.68 % (382790)Instructions burned: 1054 (million)
% 33.28/5.68 % (382810)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=719554744:i=776:doe=on:rtra=on_2964 on theBenchmark for (2964ds/776Mi)
% 33.28/5.68 % (382805)Instruction limit reached!
% 33.28/5.68 % (382805)------------------------------
% 33.28/5.68 % (382805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.28/5.68 % (382805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.28/5.68 % (382805)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382805)Termination reason: Instruction limit
% 33.28/5.68 % (382805)Termination phase: Saturation
% 33.28/5.68 % (382805)Time elapsed: 0.216 s
% 33.28/5.68 % (382805)Peak memory usage: 92 MB
% 33.28/5.68 % (382805)Instructions burned: 307 (million)
% 33.28/5.68 % (382804)Instruction limit reached!
% 33.28/5.68 % (382804)------------------------------
% 33.28/5.68 % (382804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.28/5.68 % (382804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.28/5.68 % (382804)CaDiCaL version: 2.1.3
% 33.28/5.68 % (382804)Termination reason: Instruction limit
% 33.28/5.68 % (382804)Termination phase: Saturation
% 33.28/5.68 % (382804)Time elapsed: 0.276 s
% 33.28/5.68 % (382804)Peak memory usage: 94 MB
% 33.28/5.68 % (382804)Instructions burned: 837 (million)
% 41.06/6.63 % (382811)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3839033428:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/646Mi)
% 41.06/6.63 % (382812)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=3563106159:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2963 on theBenchmark for (2963ds/784Mi)
% 41.06/6.63 % (382803)Instruction limit reached!
% 41.06/6.63 % (382803)------------------------------
% 41.06/6.63 % (382803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.06/6.63 % (382803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.63 % (382803)CaDiCaL version: 2.1.3
% 41.06/6.63 % (382803)Termination reason: Instruction limit
% 41.06/6.63 % (382803)Termination phase: Saturation
% 41.06/6.63 % (382803)Time elapsed: 0.334 s
% 41.06/6.63 % (382803)Peak memory usage: 94 MB
% 41.06/6.63 % (382803)Instructions burned: 491 (million)
% 41.06/6.63 % (382815)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=2387311561:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2962 on theBenchmark for (2962ds/246Mi)
% 41.06/6.63 % (382814)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=2291763413:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi)
% 41.06/6.63 % (382815)Instruction limit reached!
% 41.06/6.63 % (382815)------------------------------
% 41.06/6.63 % (382815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.06/6.63 % (382815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.63 % (382815)CaDiCaL version: 2.1.3
% 41.06/6.63 % (382815)Termination reason: Instruction limit
% 41.06/6.63 % (382815)Termination phase: Saturation
% 41.06/6.63 % (382815)Time elapsed: 0.102 s
% 41.06/6.63 % (382815)Peak memory usage: 117 MB
% 41.06/6.63 % (382815)Instructions burned: 249 (million)
% 41.06/6.63 % (382818)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3050654475:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/775Mi)
% 41.06/6.63 % (382822)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2514727346:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi)
% 41.06/6.63 % (382810)Instruction limit reached!
% 41.06/6.63 % (382810)------------------------------
% 41.06/6.63 % (382810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.06/6.63 % (382810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.63 % (382810)CaDiCaL version: 2.1.3
% 41.06/6.63 % (382810)Termination reason: Instruction limit
% 41.06/6.63 % (382810)Termination phase: Saturation
% 41.06/6.63 % (382810)Time elapsed: 0.489 s
% 41.06/6.63 % (382810)Peak memory usage: 123 MB
% 41.06/6.63 % (382810)Instructions burned: 776 (million)
% 41.06/6.63 % (382822)Instruction limit reached!
% 41.06/6.63 % (382822)------------------------------
% 41.06/6.63 % (382822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.06/6.63 % (382822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.63 % (382822)CaDiCaL version: 2.1.3
% 41.06/6.63 % (382822)Termination reason: Instruction limit
% 41.06/6.63 % (382822)Termination phase: Saturation
% 41.06/6.63 % (382822)Time elapsed: 0.107 s
% 41.06/6.63 % (382822)Peak memory usage: 92 MB
% 41.06/6.63 % (382822)Instructions burned: 275 (million)
% 41.06/6.63 % (382811)Instruction limit reached!
% 41.06/6.63 % (382811)------------------------------
% 41.06/6.63 % (382811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.06/6.63 % (382811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.63 % (382811)CaDiCaL version: 2.1.3
% 41.06/6.63 % (382811)Termination reason: Instruction limit
% 41.06/6.63 % (382811)Termination phase: Saturation
% 41.06/6.63 % (382811)Time elapsed: 0.443 s
% 41.06/6.63 % (382811)Peak memory usage: 140 MB
% 41.06/6.63 % (382811)Instructions burned: 647 (million)
% 41.06/6.63 % (382825)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=101658090:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi)
% 41.06/6.63 % (382824)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2523722090:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi)
% 55.14/8.44 % (382812)Instruction limit reached!
% 55.14/8.44 % (382812)------------------------------
% 55.14/8.44 % (382812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382812)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382812)Termination reason: Instruction limit
% 55.14/8.44 % (382812)Termination phase: Saturation
% 55.14/8.44 % (382812)Time elapsed: 0.588 s
% 55.14/8.44 % (382812)Peak memory usage: 122 MB
% 55.14/8.44 % (382812)Instructions burned: 784 (million)
% 55.14/8.44 % (382826)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=825285622:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi)
% 55.14/8.44 % (382824)Instruction limit reached!
% 55.14/8.44 % (382824)------------------------------
% 55.14/8.44 % (382824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382824)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382824)Termination reason: Instruction limit
% 55.14/8.44 % (382824)Termination phase: Saturation
% 55.14/8.44 % (382824)Time elapsed: 0.068 s
% 55.14/8.44 % (382824)Peak memory usage: 90 MB
% 55.14/8.44 % (382824)Instructions burned: 102 (million)
% 55.14/8.44 % (382818)Instruction limit reached!
% 55.14/8.44 % (382818)------------------------------
% 55.14/8.44 % (382818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382818)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382818)Termination reason: Instruction limit
% 55.14/8.44 % (382818)Termination phase: Saturation
% 55.14/8.44 % (382818)Time elapsed: 0.494 s
% 55.14/8.44 % (382818)Peak memory usage: 95 MB
% 55.14/8.44 % (382818)Instructions burned: 776 (million)
% 55.14/8.44 % (382829)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=2451731089:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/868Mi)
% 55.14/8.44 % (382831)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=1871774988:i=1846:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/1846Mi)
% 55.14/8.44 % (382832)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2355083377:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi)
% 55.14/8.44 % (382814)Instruction limit reached!
% 55.14/8.44 % (382814)------------------------------
% 55.14/8.44 % (382814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382814)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382814)Termination reason: Instruction limit
% 55.14/8.44 % (382814)Termination phase: Saturation
% 55.14/8.44 % (382814)Time elapsed: 0.789 s
% 55.14/8.44 % (382814)Peak memory usage: 125 MB
% 55.14/8.44 % (382814)Instructions burned: 1133 (million)
% 55.14/8.44 % (382825)Instruction limit reached!
% 55.14/8.44 % (382825)------------------------------
% 55.14/8.44 % (382825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382825)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382825)Termination reason: Instruction limit
% 55.14/8.44 % (382825)Termination phase: Saturation
% 55.14/8.44 % (382825)Time elapsed: 0.400 s
% 55.14/8.44 % (382825)Peak memory usage: 98 MB
% 55.14/8.44 % (382825)Instructions burned: 1097 (million)
% 55.14/8.44 % (382837)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=2674735559:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/863Mi)
% 55.14/8.44 % (382836)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=691769590:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2953 on theBenchmark for (2953ds/273Mi)
% 55.14/8.44 % (382836)Instruction limit reached!
% 55.14/8.44 % (382836)------------------------------
% 55.14/8.44 % (382836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382836)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382836)Termination reason: Instruction limit
% 55.14/8.44 % (382836)Termination phase: Saturation
% 55.14/8.44 % (382836)Time elapsed: 0.198 s
% 55.14/8.44 % (382836)Peak memory usage: 92 MB
% 55.14/8.44 % (382836)Instructions burned: 274 (million)
% 55.14/8.44 % (382829)Instruction limit reached!
% 55.14/8.44 % (382829)------------------------------
% 55.14/8.44 % (382829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382829)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382829)Termination reason: Instruction limit
% 55.14/8.44 % (382829)Termination phase: Saturation
% 55.14/8.44 % (382829)Time elapsed: 0.524 s
% 55.14/8.44 % (382829)Peak memory usage: 119 MB
% 55.14/8.44 % (382829)Instructions burned: 868 (million)
% 55.14/8.44 % (382837)Instruction limit reached!
% 55.14/8.44 % (382837)------------------------------
% 55.14/8.44 % (382837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382837)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382837)Termination reason: Instruction limit
% 55.14/8.44 % (382837)Termination phase: Saturation
% 55.14/8.44 % (382837)Time elapsed: 0.276 s
% 55.14/8.44 % (382837)Peak memory usage: 119 MB
% 55.14/8.44 % (382837)Instructions burned: 863 (million)
% 55.14/8.44 % (382840)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3356610999:i=5811:kws=precedence:nm=0:rtra=on_2949 on theBenchmark for (2949ds/5811Mi)
% 55.14/8.44 % (382842)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2404350748:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/801Mi)
% 55.14/8.44 % (382841)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3057802016:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2949 on theBenchmark for (2949ds/2216Mi)
% 55.14/8.44 % (382783)Instruction limit reached!
% 55.14/8.44 % (382783)------------------------------
% 55.14/8.44 % (382783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382783)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382783)Termination reason: Instruction limit
% 55.14/8.44 % (382783)Termination phase: Saturation
% 55.14/8.44 % (382783)Time elapsed: 2.739 s
% 55.14/8.44 % (382783)Peak memory usage: 122 MB
% 55.14/8.44 % (382783)Instructions burned: 4429 (million)
% 55.14/8.44 % (382842)Instruction limit reached!
% 55.14/8.44 % (382842)------------------------------
% 55.14/8.44 % (382842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382842)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382842)Termination reason: Instruction limit
% 55.14/8.44 % (382842)Termination phase: Saturation
% 55.14/8.44 % (382842)Time elapsed: 0.265 s
% 55.14/8.44 % (382842)Peak memory usage: 95 MB
% 55.14/8.44 % (382842)Instructions burned: 803 (million)
% 55.14/8.44 % (382831)Instruction limit reached!
% 55.14/8.44 % (382831)------------------------------
% 55.14/8.44 % (382831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382831)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382831)Termination reason: Instruction limit
% 55.14/8.44 % (382831)Termination phase: Saturation
% 55.14/8.44 % (382831)Time elapsed: 0.925 s
% 55.14/8.44 % (382831)Peak memory usage: 100 MB
% 55.14/8.44 % (382831)Instructions burned: 1848 (million)
% 55.14/8.44 % (382846)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2268132430:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2944 on theBenchmark for (2944ds/1026Mi)
% 55.14/8.44 % (382848)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=806381202:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2944 on theBenchmark for (2944ds/2127Mi)
% 55.14/8.44 % (382847)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3303470146:i=3509:rtra=on_2944 on theBenchmark for (2944ds/3509Mi)
% 55.14/8.44 % (382846)Instruction limit reached!
% 55.14/8.44 % (382846)------------------------------
% 55.14/8.44 % (382846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382846)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382846)Termination reason: Instruction limit
% 55.14/8.44 % (382846)Termination phase: Saturation
% 55.14/8.44 % (382846)Time elapsed: 0.369 s
% 55.14/8.44 % (382846)Peak memory usage: 96 MB
% 55.14/8.44 % (382846)Instructions burned: 1030 (million)
% 55.14/8.44 % (382852)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=897871888:i=1959:rtra=on:fsd=on:proc=on_2940 on theBenchmark for (2940ds/1959Mi)
% 55.14/8.44 % (382841)Instruction limit reached!
% 55.14/8.44 % (382841)------------------------------
% 55.14/8.44 % (382841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382841)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382841)Termination reason: Instruction limit
% 55.14/8.44 % (382841)Termination phase: Saturation
% 55.14/8.44 % (382841)Time elapsed: 1.277 s
% 55.14/8.44 % (382841)Peak memory usage: 132 MB
% 55.14/8.44 % (382841)Instructions burned: 2217 (million)
% 55.14/8.44 % (382854)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=988600506:s2a=on:i=3553:nm=0:rtra=on_2934 on theBenchmark for (2934ds/3553Mi)
% 55.14/8.44 % (382852)Instruction limit reached!
% 55.14/8.44 % (382852)------------------------------
% 55.14/8.44 % (382852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382852)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382852)Termination reason: Instruction limit
% 55.14/8.44 % (382852)Termination phase: Saturation
% 55.14/8.44 % (382852)Time elapsed: 0.661 s
% 55.14/8.44 % (382852)Peak memory usage: 125 MB
% 55.14/8.44 % (382852)Instructions burned: 1962 (million)
% 55.14/8.44 % (382848)Instruction limit reached!
% 55.14/8.44 % (382848)------------------------------
% 55.14/8.44 % (382848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382848)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382848)Termination reason: Instruction limit
% 55.14/8.44 % (382848)Termination phase: Saturation
% 55.14/8.44 % (382848)Time elapsed: 1.231 s
% 55.14/8.44 % (382848)Peak memory usage: 104 MB
% 55.14/8.44 % (382848)Instructions burned: 2128 (million)
% 55.14/8.44 % (382856)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1464903579:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2932 on theBenchmark for (2932ds/3201Mi)
% 55.14/8.44 % (382857)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=3416025320:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2931 on theBenchmark for (2931ds/4093Mi)
% 55.14/8.44 % (382840)First to succeed.
% 55.14/8.44 % (382840)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-382339"
% 55.14/8.44 % (382856)Instruction limit reached!
% 55.14/8.44 % (382856)------------------------------
% 55.14/8.44 % (382856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.14/8.44 % (382856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.14/8.44 % (382856)CaDiCaL version: 2.1.3
% 55.14/8.44 % (382856)Termination reason: Instruction limit
% 55.14/8.44 % (382856)Termination phase: Saturation
% 55.14/8.44 % (382856)Time elapsed: 0.813 s
% 55.14/8.44 % (382856)Peak memory usage: 104 MB
% 55.14/8.44 % (382856)Instructions burned: 3203 (million)
% 55.14/8.44 % (382840)Refutation found. Thanks to Tanya!
% 55.14/8.44 % SZS status Theorem for theBenchmark
% 55.14/8.44 % SZS output start Proof for theBenchmark
% See solution above
% 55.54/8.54 % (382840)------------------------------
% 55.54/8.54 % (382840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.54/8.54 % (382840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.54/8.54 % (382840)CaDiCaL version: 2.1.3
% 55.54/8.54 % (382840)Termination reason: Refutation
% 55.54/8.54 % (382840)Time elapsed: 2.348 s
% 55.54/8.54 % (382840)Peak memory usage: 128 MB
% 55.54/8.54 % (382840)Instructions burned: 4166 (million)
% 55.54/8.54 % (382840)------------------------------
% 55.54/8.54 % (382840)------------------------------
% 55.54/8.54 % (382339)Success in time 7.791 s
% 55.54/8.54 % Vampire exiting
%------------------------------------------------------------------------------