%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW606_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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:55 PM UTC 2026
% Result : Theorem 68.36s 10.47s
% Output : Refutation 69.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 64
% Syntax : Number of formulae : 296 ( 50 unt; 0 typ; 47 def)
% Number of atoms : 1198 ( 199 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 1321 ( 419 ~; 424 |; 321 &)
% ( 60 <=>; 97 =>; 0 <=; 0 <~>)
% Maximal formula depth : 45 ( 6 avg)
% Maximal term depth : 9 ( 2 avg)
% Number arithmetic : 1786 ( 424 atm; 555 fun; 571 num; 236 var)
% Number of types : 10 ( 8 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 64 ( 60 usr; 47 prp; 0-7 aty)
% Number of functors : 60 ( 54 usr; 23 con; 0-7 aty)
% Number of variables : 532 ( 495 !; 37 ?; 532 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
param: $tType ).
tff(type_def_10,type,
elt: $tType ).
tff(type_def_11,type,
array_elt: $tType ).
tff(type_def_12,type,
map_int_elt: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
occ: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_32,type,
param1: ty ).
tff(func_def_33,type,
elt1: ty ).
tff(func_def_34,type,
t2tb3: array_elt > uni ).
tff(func_def_35,type,
tb2t3: uni > array_elt ).
tff(func_def_36,type,
t2tb4: elt > uni ).
tff(func_def_37,type,
tb2t4: uni > elt ).
tff(func_def_38,type,
t2tb5: map_int_elt > uni ).
tff(func_def_39,type,
tb2t5: uni > map_int_elt ).
tff(func_def_41,type,
sK1: ( uni * ty * $int * uni * $int ) > $int ).
tff(func_def_42,type,
sK2: ( $int * $int * $int * uni * ty * $int * uni ) > $int ).
tff(func_def_43,type,
sK3: ( uni * ty * uni * $int * $int ) > $int ).
tff(func_def_44,type,
sK4: ( $int * ty * uni * $int * uni * $int ) > $int ).
tff(func_def_45,type,
sK5: ( $int * uni * ty * uni * $int ) > $int ).
tff(func_def_46,type,
sK6: ( $int * ty * $int * uni * uni ) > uni ).
tff(func_def_47,type,
sK7: ( $int * array_elt * param * $int ) > $int ).
tff(func_def_48,type,
sK8: ( $int * array_elt * param * $int ) > $int ).
tff(func_def_49,type,
sK9: ( $int * uni * ty * uni * $int ) > $int ).
tff(func_def_50,type,
sK10: $int ).
tff(func_def_51,type,
sK11: param ).
tff(func_def_52,type,
sK12: map_int_elt ).
tff(func_def_53,type,
sK13: map_int_elt ).
tff(func_def_54,type,
sK14: $int ).
tff(func_def_55,type,
sK15: map_int_elt ).
tff(func_def_56,type,
sK16: $int ).
tff(func_def_57,type,
sK17: map_int_elt ).
tff(func_def_58,type,
sK18: map_int_elt ).
tff(func_def_59,type,
sK19: $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_4,type,
permut: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_5,type,
map_eq_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_6,type,
array_eq_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_7,type,
array_eq: ( ty * uni * uni ) > $o ).
tff(pred_def_8,type,
exchange: ( ty * uni * uni * $int * $int * $int * $int ) > $o ).
tff(pred_def_9,type,
exchange1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_10,type,
permut1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_11,type,
permut_sub: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_12,type,
permut_all: ( ty * uni * uni ) > $o ).
tff(pred_def_13,type,
le: ( param * elt * elt ) > $o ).
tff(pred_def_14,type,
sorted_sub2: ( param * array_elt * $int * $int ) > $o ).
tff(pred_def_15,type,
sorted1: ( param * array_elt ) > $o ).
tff(pred_def_16,type,
sP0: ( $int * $int * $int * uni * ty * $int * uni ) > $o ).
tff(f14,axiom,
! [X2: uni,X4: uni,X3: uni,X1: ty,X0: ty] : sort(map(X0,X1),set(X1,X0,X2,X3,X4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',set_sort2) ).
tff(f16,axiom,
! [X2: uni,X3: uni,X1: ty,X0: ty,X4: uni] :
( sort(X0,X3)
=> ( sort(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_neq) ).
tff(f20,axiom,
! [X2: uni,X0: ty,X1: $int] : ( length(X0,mk_array(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_def) ).
tff(f22,axiom,
! [X2: uni,X0: ty,X1: $int] :
( sort(map(int,X0),X2)
=> ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',elts_def) ).
tff(f25,axiom,
! [X0: $int] : sort(int,t2tb(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort3) ).
tff(f26,axiom,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(f27,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f28,axiom,
! [X1: uni,X2: $int,X0: ty] : ( get1(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def) ).
tff(f48,axiom,
! [X6: $int,X0: ty,X3: $int,X4: $int,X2: uni,X1: uni,X5: $int] :
( ( ( get(X0,int,X1,t2tb(X6)) = get(X0,int,X2,t2tb(X5)) )
& $lesseq(X3,X6)
& ( get(X0,int,X1,t2tb(X5)) = get(X0,int,X2,t2tb(X6)) )
& $less(X5,X4)
& $less(X6,X4)
& $lesseq(X3,X5)
& ! [X7: $int] :
( ( $lesseq(X3,X7)
& $less(X7,X4) )
=> ( ( X7 != X5 )
=> ( ( X7 != X6 )
=> ( get(X0,int,X1,t2tb(X7)) = get(X0,int,X2,t2tb(X7)) ) ) ) ) )
<=> exchange(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exchange_def) ).
tff(f50,axiom,
! [X3: $int,X2: uni,X1: uni,X0: ty,X4: $int] :
( exchange1(X0,X1,X2,X3,X4)
<=> ( ( length(X0,X1) = length(X0,X2) )
& exchange(X0,elts(X0,X1),elts(X0,X2),0,length(X0,X1),X3,X4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exchange_def1) ).
tff(f58,axiom,
! [X0: param,X2: elt,X1: elt] :
( ~ le(X0,X1,X2)
=> le(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',le_asym) ).
tff(f59,axiom,
! [X1: elt,X3: elt,X0: param,X2: elt] :
( ( le(X0,X2,X3)
& le(X0,X1,X2) )
=> le(X0,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',le_trans) ).
tff(f62,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR3) ).
tff(f66,axiom,
! [X1: array_elt,X3: $int,X2: $int,X0: param] :
( sorted_sub2(X0,X1,X2,X3)
<=> ! [X4: $int,X5: $int] :
( ( $less(X5,X3)
& $lesseq(X2,X4)
& $lesseq(X4,X5) )
=> le(X0,tb2t4(get1(elt1,t2tb3(X1),X4)),tb2t4(get1(elt1,t2tb3(X1),X5))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_sub_def2) ).
tff(f68,axiom,
! [X0: map_int_elt] : sort(map(int,elt1),t2tb5(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort6) ).
tff(f70,axiom,
! [X0: uni] :
( sort(map(int,elt1),X0)
=> ( t2tb5(tb2t5(X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR5) ).
tff(f71,conjecture,
! [X1: $int,X0: param,X2: map_int_elt] :
( $lesseq(0,X1)
=> ( $lesseq(0,$difference(X1,1))
=> ! [X4: $int,X3: map_int_elt] :
( ( $lesseq(X4,$difference(X1,1))
& $lesseq(0,X4) )
=> ( ( sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X3))),0,X4)
& permut_all(elt1,mk_array(elt1,X1,t2tb5(X2)),mk_array(elt1,X1,t2tb5(X3))) )
=> ! [X5: $int,X6: map_int_elt] :
( ( ! [X7: $int,X8: $int] :
( ( $lesseq(X8,X4)
& $less(X7,X5)
& $lesseq(0,X7)
& $lesseq($sum(X5,1),X8) )
=> le(X0,tb2t4(get(elt1,int,t2tb5(X6),t2tb(X7))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X8)))) )
& sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X6))),X5,$sum(X4,1))
& sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X6))),0,X5)
& permut_all(elt1,mk_array(elt1,X1,t2tb5(X2)),mk_array(elt1,X1,t2tb5(X6)))
& $lesseq(0,X5)
& $lesseq(X5,X4) )
=> ( $less(0,X5)
=> ( ( $lesseq(0,X1)
& $lesseq(0,X5)
& $less(X5,X1) )
=> ( ( $lesseq(0,$difference(X5,1))
& $less($difference(X5,1),X1) )
=> ( ~ le(X0,tb2t4(get(elt1,int,t2tb5(X6),t2tb($difference(X5,1)))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X5))))
=> ( ( $lesseq(0,X5)
& $less(X5,X1) )
=> ( ( $lesseq(0,$difference(X5,1))
& $less($difference(X5,1),X1) )
=> ( ( $lesseq(0,X5)
& $less(X5,X1) )
=> ! [X9: map_int_elt] :
( ( $lesseq(0,X1)
& ( X9 = tb2t5(set(elt1,int,t2tb5(X6),t2tb(X5),get(elt1,int,t2tb5(X6),t2tb($difference(X5,1))))) ) )
=> ( ( $less($difference(X5,1),X1)
& $lesseq(0,$difference(X5,1)) )
=> ! [X10: map_int_elt] :
( ( $lesseq(0,X1)
& ( X10 = tb2t5(set(elt1,int,t2tb5(X9),t2tb($difference(X5,1)),get(elt1,int,t2tb5(X6),t2tb(X5)))) ) )
=> ( exchange1(elt1,mk_array(elt1,X1,t2tb5(X6)),mk_array(elt1,X1,t2tb5(X10)),$difference(X5,1),X5)
=> ! [X11: $int] :
( ( X11 = $difference(X5,1) )
=> sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X10))),X11,$sum(X4,1)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_sort1) ).
tff(f72,negated_conjecture,
~ ! [X1: $int,X0: param,X2: map_int_elt] :
( $lesseq(0,X1)
=> ( $lesseq(0,$difference(X1,1))
=> ! [X4: $int,X3: map_int_elt] :
( ( $lesseq(X4,$difference(X1,1))
& $lesseq(0,X4) )
=> ( ( sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X3))),0,X4)
& permut_all(elt1,mk_array(elt1,X1,t2tb5(X2)),mk_array(elt1,X1,t2tb5(X3))) )
=> ! [X5: $int,X6: map_int_elt] :
( ( ! [X7: $int,X8: $int] :
( ( $lesseq(X8,X4)
& $less(X7,X5)
& $lesseq(0,X7)
& $lesseq($sum(X5,1),X8) )
=> le(X0,tb2t4(get(elt1,int,t2tb5(X6),t2tb(X7))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X8)))) )
& sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X6))),X5,$sum(X4,1))
& sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X6))),0,X5)
& permut_all(elt1,mk_array(elt1,X1,t2tb5(X2)),mk_array(elt1,X1,t2tb5(X6)))
& $lesseq(0,X5)
& $lesseq(X5,X4) )
=> ( $less(0,X5)
=> ( ( $lesseq(0,X1)
& $lesseq(0,X5)
& $less(X5,X1) )
=> ( ( $lesseq(0,$difference(X5,1))
& $less($difference(X5,1),X1) )
=> ( ~ le(X0,tb2t4(get(elt1,int,t2tb5(X6),t2tb($difference(X5,1)))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X5))))
=> ( ( $lesseq(0,X5)
& $less(X5,X1) )
=> ( ( $lesseq(0,$difference(X5,1))
& $less($difference(X5,1),X1) )
=> ( ( $lesseq(0,X5)
& $less(X5,X1) )
=> ! [X9: map_int_elt] :
( ( $lesseq(0,X1)
& ( X9 = tb2t5(set(elt1,int,t2tb5(X6),t2tb(X5),get(elt1,int,t2tb5(X6),t2tb($difference(X5,1))))) ) )
=> ( ( $less($difference(X5,1),X1)
& $lesseq(0,$difference(X5,1)) )
=> ! [X10: map_int_elt] :
( ( $lesseq(0,X1)
& ( X10 = tb2t5(set(elt1,int,t2tb5(X9),t2tb($difference(X5,1)),get(elt1,int,t2tb5(X6),t2tb(X5)))) ) )
=> ( exchange1(elt1,mk_array(elt1,X1,t2tb5(X6)),mk_array(elt1,X1,t2tb5(X10)),$difference(X5,1),X5)
=> ! [X11: $int] :
( ( X11 = $difference(X5,1) )
=> sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X10))),X11,$sum(X4,1)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f71]) ).
tff(f80,plain,
! [X6: $int,X0: ty,X3: $int,X4: $int,X2: uni,X1: uni,X5: $int] :
( ( ( get(X0,int,X1,t2tb(X6)) = get(X0,int,X2,t2tb(X5)) )
& ~ $less(X6,X3)
& ( get(X0,int,X1,t2tb(X5)) = get(X0,int,X2,t2tb(X6)) )
& $less(X5,X4)
& $less(X6,X4)
& ~ $less(X5,X3)
& ! [X7: $int] :
( ( ~ $less(X7,X3)
& $less(X7,X4) )
=> ( ( X7 != X5 )
=> ( ( X7 != X6 )
=> ( get(X0,int,X1,t2tb(X7)) = get(X0,int,X2,t2tb(X7)) ) ) ) ) )
<=> exchange(X0,X1,X2,X3,X4,X5,X6) ),
inference(theory_normalization,[],[f48]) ).
tff(f84,plain,
~ ! [X1: $int,X0: param,X2: map_int_elt] :
( ~ $less(X1,0)
=> ( ~ $less($sum(X1,$uminus(1)),0)
=> ! [X4: $int,X3: map_int_elt] :
( ( ~ $less($sum(X1,$uminus(1)),X4)
& ~ $less(X4,0) )
=> ( ( sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X3))),0,X4)
& permut_all(elt1,mk_array(elt1,X1,t2tb5(X2)),mk_array(elt1,X1,t2tb5(X3))) )
=> ! [X5: $int,X6: map_int_elt] :
( ( ! [X7: $int,X8: $int] :
( ( ~ $less(X4,X8)
& $less(X7,X5)
& ~ $less(X7,0)
& ~ $less(X8,$sum(X5,1)) )
=> le(X0,tb2t4(get(elt1,int,t2tb5(X6),t2tb(X7))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X8)))) )
& sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X6))),X5,$sum(X4,1))
& sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X6))),0,X5)
& permut_all(elt1,mk_array(elt1,X1,t2tb5(X2)),mk_array(elt1,X1,t2tb5(X6)))
& ~ $less(X5,0)
& ~ $less(X4,X5) )
=> ( $less(0,X5)
=> ( ( ~ $less(X1,0)
& ~ $less(X5,0)
& $less(X5,X1) )
=> ( ( ~ $less($sum(X5,$uminus(1)),0)
& $less($sum(X5,$uminus(1)),X1) )
=> ( ~ le(X0,tb2t4(get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X5))))
=> ( ( ~ $less(X5,0)
& $less(X5,X1) )
=> ( ( ~ $less($sum(X5,$uminus(1)),0)
& $less($sum(X5,$uminus(1)),X1) )
=> ( ( ~ $less(X5,0)
& $less(X5,X1) )
=> ! [X9: map_int_elt] :
( ( ~ $less(X1,0)
& ( tb2t5(set(elt1,int,t2tb5(X6),t2tb(X5),get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1)))))) = X9 ) )
=> ( ( $less($sum(X5,$uminus(1)),X1)
& ~ $less($sum(X5,$uminus(1)),0) )
=> ! [X10: map_int_elt] :
( ( ~ $less(X1,0)
& ( tb2t5(set(elt1,int,t2tb5(X9),t2tb($sum(X5,$uminus(1))),get(elt1,int,t2tb5(X6),t2tb(X5)))) = X10 ) )
=> ( exchange1(elt1,mk_array(elt1,X1,t2tb5(X6)),mk_array(elt1,X1,t2tb5(X10)),$sum(X5,$uminus(1)),X5)
=> ! [X11: $int] :
( ( $sum(X5,$uminus(1)) = X11 )
=> sorted_sub2(X0,tb2t3(mk_array(elt1,X1,t2tb5(X10))),X11,$sum(X4,1)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f72]) ).
tff(f85,plain,
! [X1: array_elt,X3: $int,X2: $int,X0: param] :
( sorted_sub2(X0,X1,X2,X3)
<=> ! [X4: $int,X5: $int] :
( ( $less(X5,X3)
& ~ $less(X4,X2)
& ~ $less(X5,X4) )
=> le(X0,tb2t4(get1(elt1,t2tb3(X1),X4)),tb2t4(get1(elt1,t2tb3(X1),X5))) ) ),
inference(theory_normalization,[],[f66]) ).
tff(f95,plain,
! [X4: $int,X0: $int,X1: uni,X3: ty,X2: uni] :
( ( ( length(X3,X2) = length(X3,X1) )
& exchange(X3,elts(X3,X2),elts(X3,X1),0,length(X3,X2),X0,X4) )
<=> exchange1(X3,X2,X1,X0,X4) ),
inference(rectify,[],[f50]) ).
tff(f97,plain,
! [X0: uni,X2: $int,X1: ty] : ( length(X1,mk_array(X1,X2,X0)) = X2 ),
inference(rectify,[],[f20]) ).
tff(f99,plain,
! [X1: $int,X0: uni,X2: ty] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get1(X2,X0,X1) ),
inference(rectify,[],[f28]) ).
tff(f107,plain,
! [X1: elt,X2: elt,X0: param] :
( ~ le(X0,X2,X1)
=> le(X0,X1,X2) ),
inference(rectify,[],[f58]) ).
tff(f111,plain,
! [X6: $int,X1: ty,X2: $int,X5: uni,X0: $int,X4: uni,X3: $int] :
( ( ~ $less(X0,X2)
& $less(X6,X3)
& ( get(X1,int,X5,t2tb(X0)) = get(X1,int,X4,t2tb(X6)) )
& ( get(X1,int,X4,t2tb(X0)) = get(X1,int,X5,t2tb(X6)) )
& ~ $less(X6,X2)
& $less(X0,X3)
& ! [X7: $int] :
( ( ~ $less(X7,X2)
& $less(X7,X3) )
=> ( ( X6 != X7 )
=> ( ( X0 != X7 )
=> ( get(X1,int,X4,t2tb(X7)) = get(X1,int,X5,t2tb(X7)) ) ) ) ) )
<=> exchange(X1,X5,X4,X2,X3,X6,X0) ),
inference(rectify,[],[f80]) ).
tff(f114,plain,
! [X2: uni,X0: uni,X3: ty,X1: uni,X4: ty] : sort(map(X4,X3),set(X3,X4,X0,X2,X1)),
inference(rectify,[],[f14]) ).
tff(f115,plain,
! [X1: elt,X2: param,X0: elt,X3: elt] :
( ( le(X2,X0,X3)
& le(X2,X3,X1) )
=> le(X2,X0,X1) ),
inference(rectify,[],[f59]) ).
tff(f124,plain,
! [X3: ty,X4: uni,X1: uni,X2: ty,X0: uni] :
( sort(X3,X1)
=> ( sort(X3,X4)
=> ! [X5: uni] :
( ( X1 != X4 )
=> ( get(X2,X3,X0,X4) = get(X2,X3,set(X2,X3,X0,X1,X5),X4) ) ) ) ),
inference(rectify,[],[f16]) ).
tff(f126,plain,
! [X1: ty,X2: $int,X0: uni] :
( sort(map(int,X1),X0)
=> ( elts(X1,mk_array(X1,X2,X0)) = X0 ) ),
inference(rectify,[],[f22]) ).
tff(f127,plain,
~ ! [X2: map_int_elt,X1: param,X0: $int] :
( ~ $less(X0,0)
=> ( ~ $less($sum(X0,$uminus(1)),0)
=> ! [X4: map_int_elt,X3: $int] :
( ( ~ $less($sum(X0,$uminus(1)),X3)
& ~ $less(X3,0) )
=> ( ( permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X4)))
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X4))),0,X3) )
=> ! [X6: map_int_elt,X5: $int] :
( ( sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X6))),X5,$sum(X3,1))
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X6)))
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X6))),0,X5)
& ! [X8: $int,X7: $int] :
( ( ~ $less(X3,X8)
& ~ $less(X7,0)
& $less(X7,X5)
& ~ $less(X8,$sum(X5,1)) )
=> le(X1,tb2t4(get(elt1,int,t2tb5(X6),t2tb(X7))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X8)))) )
& ~ $less(X5,0)
& ~ $less(X3,X5) )
=> ( $less(0,X5)
=> ( ( ~ $less(X0,0)
& ~ $less(X5,0)
& $less(X5,X0) )
=> ( ( $less($sum(X5,$uminus(1)),X0)
& ~ $less($sum(X5,$uminus(1)),0) )
=> ( ~ le(X1,tb2t4(get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X5))))
=> ( ( ~ $less(X5,0)
& $less(X5,X0) )
=> ( ( ~ $less($sum(X5,$uminus(1)),0)
& $less($sum(X5,$uminus(1)),X0) )
=> ( ( ~ $less(X5,0)
& $less(X5,X0) )
=> ! [X9: map_int_elt] :
( ( ( tb2t5(set(elt1,int,t2tb5(X6),t2tb(X5),get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1)))))) = X9 )
& ~ $less(X0,0) )
=> ( ( $less($sum(X5,$uminus(1)),X0)
& ~ $less($sum(X5,$uminus(1)),0) )
=> ! [X10: map_int_elt] :
( ( ( tb2t5(set(elt1,int,t2tb5(X9),t2tb($sum(X5,$uminus(1))),get(elt1,int,t2tb5(X6),t2tb(X5)))) = X10 )
& ~ $less(X0,0) )
=> ( exchange1(elt1,mk_array(elt1,X0,t2tb5(X6)),mk_array(elt1,X0,t2tb5(X10)),$sum(X5,$uminus(1)),X5)
=> ! [X11: $int] :
( ( $sum(X5,$uminus(1)) = X11 )
=> sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X10))),X11,$sum(X3,1)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f84]) ).
tff(f128,plain,
! [X3: param,X1: $int,X2: $int,X0: array_elt] :
( sorted_sub2(X3,X0,X2,X1)
<=> ! [X4: $int,X5: $int] :
( ( ~ $less(X4,X2)
& ~ $less(X5,X4)
& $less(X5,X1) )
=> le(X3,tb2t4(get1(elt1,t2tb3(X0),X4)),tb2t4(get1(elt1,t2tb3(X0),X5))) ) ),
inference(rectify,[],[f85]) ).
tff(f146,plain,
? [X2: map_int_elt,X1: param,X0: $int] :
( ? [X4: map_int_elt,X3: $int] :
( ? [X6: map_int_elt,X5: $int] :
( ? [X9: map_int_elt] :
( ? [X10: map_int_elt] :
( ? [X11: $int] :
( ( $sum(X5,$uminus(1)) = X11 )
& ~ sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X10))),X11,$sum(X3,1)) )
& exchange1(elt1,mk_array(elt1,X0,t2tb5(X6)),mk_array(elt1,X0,t2tb5(X10)),$sum(X5,$uminus(1)),X5)
& ( tb2t5(set(elt1,int,t2tb5(X9),t2tb($sum(X5,$uminus(1))),get(elt1,int,t2tb5(X6),t2tb(X5)))) = X10 )
& ~ $less(X0,0) )
& $less($sum(X5,$uminus(1)),X0)
& ~ $less($sum(X5,$uminus(1)),0)
& ( tb2t5(set(elt1,int,t2tb5(X6),t2tb(X5),get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1)))))) = X9 )
& ~ $less(X0,0) )
& ~ $less(X5,0)
& $less(X5,X0)
& ~ $less($sum(X5,$uminus(1)),0)
& $less($sum(X5,$uminus(1)),X0)
& ~ $less(X5,0)
& $less(X5,X0)
& ~ le(X1,tb2t4(get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X5))))
& $less($sum(X5,$uminus(1)),X0)
& ~ $less($sum(X5,$uminus(1)),0)
& ~ $less(X0,0)
& ~ $less(X5,0)
& $less(X5,X0)
& $less(0,X5)
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X6))),X5,$sum(X3,1))
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X6)))
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X6))),0,X5)
& ! [X8: $int,X7: $int] :
( le(X1,tb2t4(get(elt1,int,t2tb5(X6),t2tb(X7))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X8))))
| $less(X3,X8)
| $less(X7,0)
| ~ $less(X7,X5)
| $less(X8,$sum(X5,1)) )
& ~ $less(X5,0)
& ~ $less(X3,X5) )
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X4)))
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X4))),0,X3)
& ~ $less($sum(X0,$uminus(1)),X3)
& ~ $less(X3,0) )
& ~ $less($sum(X0,$uminus(1)),0)
& ~ $less(X0,0) ),
inference(ennf_transformation,[],[f127]) ).
tff(f147,plain,
? [X0: $int,X1: param,X2: map_int_elt] :
( ~ $less(X0,0)
& ~ $less($sum(X0,$uminus(1)),0)
& ? [X4: map_int_elt,X3: $int] :
( ? [X6: map_int_elt,X5: $int] :
( ~ $less(X3,X5)
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X6)))
& $less(X5,X0)
& ~ $less($sum(X5,$uminus(1)),0)
& ~ $less(X0,0)
& $less($sum(X5,$uminus(1)),X0)
& ? [X9: map_int_elt] :
( ? [X10: map_int_elt] :
( exchange1(elt1,mk_array(elt1,X0,t2tb5(X6)),mk_array(elt1,X0,t2tb5(X10)),$sum(X5,$uminus(1)),X5)
& ? [X11: $int] :
( ( $sum(X5,$uminus(1)) = X11 )
& ~ sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X10))),X11,$sum(X3,1)) )
& ~ $less(X0,0)
& ( tb2t5(set(elt1,int,t2tb5(X9),t2tb($sum(X5,$uminus(1))),get(elt1,int,t2tb5(X6),t2tb(X5)))) = X10 ) )
& ( tb2t5(set(elt1,int,t2tb5(X6),t2tb(X5),get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1)))))) = X9 )
& ~ $less($sum(X5,$uminus(1)),0)
& $less($sum(X5,$uminus(1)),X0)
& ~ $less(X0,0) )
& ~ $less(X5,0)
& ~ $less(X5,0)
& ~ $less(X5,0)
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X6))),0,X5)
& ! [X7: $int,X8: $int] :
( $less(X3,X8)
| ~ $less(X7,X5)
| $less(X8,$sum(X5,1))
| le(X1,tb2t4(get(elt1,int,t2tb5(X6),t2tb(X7))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X8))))
| $less(X7,0) )
& $less(X5,X0)
& ~ le(X1,tb2t4(get(elt1,int,t2tb5(X6),t2tb($sum(X5,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(X6),t2tb(X5))))
& $less($sum(X5,$uminus(1)),X0)
& ~ $less($sum(X5,$uminus(1)),0)
& ~ $less(X5,0)
& $less(0,X5)
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X6))),X5,$sum(X3,1))
& $less(X5,X0) )
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X4))),0,X3)
& ~ $less(X3,0)
& ~ $less($sum(X0,$uminus(1)),X3)
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X4))) ) ),
inference(flattening,[],[f146]) ).
tff(f151,plain,
! [X1: elt,X2: elt,X0: param] :
( le(X0,X2,X1)
| le(X0,X1,X2) ),
inference(ennf_transformation,[],[f107]) ).
tff(f152,plain,
! [X1: ty,X2: $int,X0: uni] :
( ~ sort(map(int,X1),X0)
| ( elts(X1,mk_array(X1,X2,X0)) = X0 ) ),
inference(ennf_transformation,[],[f126]) ).
tff(f169,plain,
! [X0: uni] :
( ~ sort(map(int,elt1),X0)
| ( t2tb5(tb2t5(X0)) = X0 ) ),
inference(ennf_transformation,[],[f70]) ).
tff(f170,plain,
! [X1: elt,X2: param,X0: elt,X3: elt] :
( le(X2,X0,X1)
| ~ le(X2,X0,X3)
| ~ le(X2,X3,X1) ),
inference(ennf_transformation,[],[f115]) ).
tff(f171,plain,
! [X2: param,X0: elt,X1: elt,X3: elt] :
( ~ le(X2,X0,X3)
| le(X2,X0,X1)
| ~ le(X2,X3,X1) ),
inference(flattening,[],[f170]) ).
tff(f172,plain,
! [X3: param,X1: $int,X2: $int,X0: array_elt] :
( sorted_sub2(X3,X0,X2,X1)
<=> ! [X4: $int,X5: $int] :
( le(X3,tb2t4(get1(elt1,t2tb3(X0),X4)),tb2t4(get1(elt1,t2tb3(X0),X5)))
| $less(X4,X2)
| $less(X5,X4)
| ~ $less(X5,X1) ) ),
inference(ennf_transformation,[],[f128]) ).
tff(f173,plain,
! [X1: $int,X0: array_elt,X3: param,X2: $int] :
( sorted_sub2(X3,X0,X2,X1)
<=> ! [X4: $int,X5: $int] :
( ~ $less(X5,X1)
| le(X3,tb2t4(get1(elt1,t2tb3(X0),X4)),tb2t4(get1(elt1,t2tb3(X0),X5)))
| $less(X4,X2)
| $less(X5,X4) ) ),
inference(flattening,[],[f172]) ).
tff(f185,plain,
! [X3: ty,X4: uni,X1: uni,X2: ty,X0: uni] :
( ! [X5: uni] :
( ( get(X2,X3,X0,X4) = get(X2,X3,set(X2,X3,X0,X1,X5),X4) )
| ( X1 = X4 ) )
| ~ sort(X3,X4)
| ~ sort(X3,X1) ),
inference(ennf_transformation,[],[f124]) ).
tff(f186,plain,
! [X4: uni,X0: uni,X3: ty,X2: ty,X1: uni] :
( ~ sort(X3,X4)
| ~ sort(X3,X1)
| ! [X5: uni] :
( ( get(X2,X3,X0,X4) = get(X2,X3,set(X2,X3,X0,X1,X5),X4) )
| ( X1 = X4 ) ) ),
inference(flattening,[],[f185]) ).
tff(f191,plain,
! [X6: $int,X1: ty,X2: $int,X5: uni,X0: $int,X4: uni,X3: $int] :
( ( ~ $less(X0,X2)
& $less(X6,X3)
& ( get(X1,int,X5,t2tb(X0)) = get(X1,int,X4,t2tb(X6)) )
& ( get(X1,int,X4,t2tb(X0)) = get(X1,int,X5,t2tb(X6)) )
& ~ $less(X6,X2)
& $less(X0,X3)
& ! [X7: $int] :
( ( get(X1,int,X4,t2tb(X7)) = get(X1,int,X5,t2tb(X7)) )
| ( X0 = X7 )
| ( X6 = X7 )
| $less(X7,X2)
| ~ $less(X7,X3) ) )
<=> exchange(X1,X5,X4,X2,X3,X6,X0) ),
inference(ennf_transformation,[],[f111]) ).
tff(f192,plain,
! [X5: uni,X3: $int,X0: $int,X6: $int,X1: ty,X2: $int,X4: uni] :
( ( $less(X6,X3)
& ~ $less(X6,X2)
& ( get(X1,int,X5,t2tb(X0)) = get(X1,int,X4,t2tb(X6)) )
& ~ $less(X0,X2)
& ( get(X1,int,X4,t2tb(X0)) = get(X1,int,X5,t2tb(X6)) )
& $less(X0,X3)
& ! [X7: $int] :
( $less(X7,X2)
| ( X0 = X7 )
| ( X6 = X7 )
| ~ $less(X7,X3)
| ( get(X1,int,X4,t2tb(X7)) = get(X1,int,X5,t2tb(X7)) ) ) )
<=> exchange(X1,X5,X4,X2,X3,X6,X0) ),
inference(flattening,[],[f191]) ).
tff(f198,definition,
! [X3: $int,X6: $int,X2: $int,X4: uni,X1: ty,X0: $int,X5: uni] :
( sP0(X3,X6,X2,X4,X1,X0,X5)
<=> ( $less(X6,X3)
& ~ $less(X6,X2)
& ( get(X1,int,X5,t2tb(X0)) = get(X1,int,X4,t2tb(X6)) )
& ~ $less(X0,X2)
& ( get(X1,int,X4,t2tb(X0)) = get(X1,int,X5,t2tb(X6)) )
& $less(X0,X3)
& ! [X7: $int] :
( $less(X7,X2)
| ( X0 = X7 )
| ( X6 = X7 )
| ~ $less(X7,X3)
| ( get(X1,int,X4,t2tb(X7)) = get(X1,int,X5,t2tb(X7)) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f199,plain,
! [X5: uni,X3: $int,X0: $int,X6: $int,X1: ty,X2: $int,X4: uni] :
( sP0(X3,X6,X2,X4,X1,X0,X5)
<=> exchange(X1,X5,X4,X2,X3,X6,X0) ),
inference(definition_folding,[],[f192,f198]) ).
tff(f203,plain,
! [X0: uni,X1: $int,X2: ty] : ( length(X2,mk_array(X2,X1,X0)) = X1 ),
inference(rectify,[],[f97]) ).
tff(f220,plain,
! [X0: param,X1: elt,X2: elt,X3: elt] :
( ~ le(X0,X1,X3)
| le(X0,X1,X2)
| ~ le(X0,X3,X2) ),
inference(rectify,[],[f171]) ).
tff(f221,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni,X4: ty] : sort(map(X4,X2),set(X2,X4,X1,X0,X3)),
inference(rectify,[],[f114]) ).
tff(f222,plain,
! [X4: $int,X0: $int,X1: uni,X3: ty,X2: uni] :
( ( ( ( length(X3,X2) = length(X3,X1) )
& exchange(X3,elts(X3,X2),elts(X3,X1),0,length(X3,X2),X0,X4) )
| ~ exchange1(X3,X2,X1,X0,X4) )
& ( exchange1(X3,X2,X1,X0,X4)
| ( length(X3,X2) != length(X3,X1) )
| ~ exchange(X3,elts(X3,X2),elts(X3,X1),0,length(X3,X2),X0,X4) ) ),
inference(nnf_transformation,[],[f95]) ).
tff(f223,plain,
! [X4: $int,X0: $int,X1: uni,X3: ty,X2: uni] :
( ( ( ( length(X3,X2) = length(X3,X1) )
& exchange(X3,elts(X3,X2),elts(X3,X1),0,length(X3,X2),X0,X4) )
| ~ exchange1(X3,X2,X1,X0,X4) )
& ( exchange1(X3,X2,X1,X0,X4)
| ( length(X3,X2) != length(X3,X1) )
| ~ exchange(X3,elts(X3,X2),elts(X3,X1),0,length(X3,X2),X0,X4) ) ),
inference(flattening,[],[f222]) ).
tff(f224,plain,
! [X0: $int,X1: $int,X2: uni,X3: ty,X4: uni] :
( ( ( ( length(X3,X2) = length(X3,X4) )
& exchange(X3,elts(X3,X4),elts(X3,X2),0,length(X3,X4),X1,X0) )
| ~ exchange1(X3,X4,X2,X1,X0) )
& ( exchange1(X3,X4,X2,X1,X0)
| ( length(X3,X2) != length(X3,X4) )
| ~ exchange(X3,elts(X3,X4),elts(X3,X2),0,length(X3,X4),X1,X0) ) ),
inference(rectify,[],[f223]) ).
tff(f226,plain,
! [X0: elt,X1: elt,X2: param] :
( le(X2,X1,X0)
| le(X2,X0,X1) ),
inference(rectify,[],[f151]) ).
tff(f228,plain,
! [X3: $int,X6: $int,X2: $int,X4: uni,X1: ty,X0: $int,X5: uni] :
( ( sP0(X3,X6,X2,X4,X1,X0,X5)
| ~ $less(X6,X3)
| $less(X6,X2)
| ( get(X1,int,X5,t2tb(X0)) != get(X1,int,X4,t2tb(X6)) )
| $less(X0,X2)
| ( get(X1,int,X4,t2tb(X0)) != get(X1,int,X5,t2tb(X6)) )
| ~ $less(X0,X3)
| ? [X7: $int] :
( ~ $less(X7,X2)
& ( X0 != X7 )
& ( X6 != X7 )
& $less(X7,X3)
& ( get(X1,int,X4,t2tb(X7)) != get(X1,int,X5,t2tb(X7)) ) ) )
& ( ( $less(X6,X3)
& ~ $less(X6,X2)
& ( get(X1,int,X5,t2tb(X0)) = get(X1,int,X4,t2tb(X6)) )
& ~ $less(X0,X2)
& ( get(X1,int,X4,t2tb(X0)) = get(X1,int,X5,t2tb(X6)) )
& $less(X0,X3)
& ! [X7: $int] :
( $less(X7,X2)
| ( X0 = X7 )
| ( X6 = X7 )
| ~ $less(X7,X3)
| ( get(X1,int,X4,t2tb(X7)) = get(X1,int,X5,t2tb(X7)) ) ) )
| ~ sP0(X3,X6,X2,X4,X1,X0,X5) ) ),
inference(nnf_transformation,[],[f198]) ).
tff(f229,plain,
! [X3: $int,X6: $int,X2: $int,X4: uni,X1: ty,X0: $int,X5: uni] :
( ( sP0(X3,X6,X2,X4,X1,X0,X5)
| ~ $less(X6,X3)
| $less(X6,X2)
| ( get(X1,int,X5,t2tb(X0)) != get(X1,int,X4,t2tb(X6)) )
| $less(X0,X2)
| ( get(X1,int,X4,t2tb(X0)) != get(X1,int,X5,t2tb(X6)) )
| ~ $less(X0,X3)
| ? [X7: $int] :
( ~ $less(X7,X2)
& ( X0 != X7 )
& ( X6 != X7 )
& $less(X7,X3)
& ( get(X1,int,X4,t2tb(X7)) != get(X1,int,X5,t2tb(X7)) ) ) )
& ( ( $less(X6,X3)
& ~ $less(X6,X2)
& ( get(X1,int,X5,t2tb(X0)) = get(X1,int,X4,t2tb(X6)) )
& ~ $less(X0,X2)
& ( get(X1,int,X4,t2tb(X0)) = get(X1,int,X5,t2tb(X6)) )
& $less(X0,X3)
& ! [X7: $int] :
( $less(X7,X2)
| ( X0 = X7 )
| ( X6 = X7 )
| ~ $less(X7,X3)
| ( get(X1,int,X4,t2tb(X7)) = get(X1,int,X5,t2tb(X7)) ) ) )
| ~ sP0(X3,X6,X2,X4,X1,X0,X5) ) ),
inference(flattening,[],[f228]) ).
tff(f230,plain,
! [X0: $int,X1: $int,X2: $int,X3: uni,X4: ty,X5: $int,X6: uni] :
( ( sP0(X0,X1,X2,X3,X4,X5,X6)
| ~ $less(X1,X0)
| $less(X1,X2)
| ( get(X4,int,X3,t2tb(X1)) != get(X4,int,X6,t2tb(X5)) )
| $less(X5,X2)
| ( get(X4,int,X6,t2tb(X1)) != get(X4,int,X3,t2tb(X5)) )
| ~ $less(X5,X0)
| ? [X7: $int] :
( ~ $less(X7,X2)
& ( X5 != X7 )
& ( X1 != X7 )
& $less(X7,X0)
& ( get(X4,int,X3,t2tb(X7)) != get(X4,int,X6,t2tb(X7)) ) ) )
& ( ( $less(X1,X0)
& ~ $less(X1,X2)
& ( get(X4,int,X3,t2tb(X1)) = get(X4,int,X6,t2tb(X5)) )
& ~ $less(X5,X2)
& ( get(X4,int,X6,t2tb(X1)) = get(X4,int,X3,t2tb(X5)) )
& $less(X5,X0)
& ! [X8: $int] :
( $less(X8,X2)
| ( X5 = X8 )
| ( X1 = X8 )
| ~ $less(X8,X0)
| ( get(X4,int,X6,t2tb(X8)) = get(X4,int,X3,t2tb(X8)) ) ) )
| ~ sP0(X0,X1,X2,X3,X4,X5,X6) ) ),
inference(rectify,[],[f229]) ).
tff(f231,plain,
! [X0: $int,X1: $int,X2: $int,X3: uni,X4: ty,X5: $int,X6: uni] :
( ( sP0(X0,X1,X2,X3,X4,X5,X6)
| ~ $less(X1,X0)
| $less(X1,X2)
| ( get(X4,int,X3,t2tb(X1)) != get(X4,int,X6,t2tb(X5)) )
| $less(X5,X2)
| ( get(X4,int,X6,t2tb(X1)) != get(X4,int,X3,t2tb(X5)) )
| ~ $less(X5,X0)
| ( ~ $less(sK2(X0,X1,X2,X3,X4,X5,X6),X2)
& ( sK2(X0,X1,X2,X3,X4,X5,X6) != X5 )
& ( sK2(X0,X1,X2,X3,X4,X5,X6) != X1 )
& $less(sK2(X0,X1,X2,X3,X4,X5,X6),X0)
& ( get(X4,int,X6,t2tb(sK2(X0,X1,X2,X3,X4,X5,X6))) != get(X4,int,X3,t2tb(sK2(X0,X1,X2,X3,X4,X5,X6))) ) ) )
& ( ( $less(X1,X0)
& ~ $less(X1,X2)
& ( get(X4,int,X3,t2tb(X1)) = get(X4,int,X6,t2tb(X5)) )
& ~ $less(X5,X2)
& ( get(X4,int,X6,t2tb(X1)) = get(X4,int,X3,t2tb(X5)) )
& $less(X5,X0)
& ! [X8: $int] :
( $less(X8,X2)
| ( X5 = X8 )
| ( X1 = X8 )
| ~ $less(X8,X0)
| ( get(X4,int,X6,t2tb(X8)) = get(X4,int,X3,t2tb(X8)) ) ) )
| ~ sP0(X0,X1,X2,X3,X4,X5,X6) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X7,sK2(X0,X1,X2,X3,X4,X5,X6))],[f230]) ).
tff(f232,plain,
! [X5: uni,X3: $int,X0: $int,X6: $int,X1: ty,X2: $int,X4: uni] :
( ( sP0(X3,X6,X2,X4,X1,X0,X5)
| ~ exchange(X1,X5,X4,X2,X3,X6,X0) )
& ( exchange(X1,X5,X4,X2,X3,X6,X0)
| ~ sP0(X3,X6,X2,X4,X1,X0,X5) ) ),
inference(nnf_transformation,[],[f199]) ).
tff(f233,plain,
! [X0: uni,X1: $int,X2: $int,X3: $int,X4: ty,X5: $int,X6: uni] :
( ( sP0(X1,X3,X5,X6,X4,X2,X0)
| ~ exchange(X4,X0,X6,X5,X1,X3,X2) )
& ( exchange(X4,X0,X6,X5,X1,X3,X2)
| ~ sP0(X1,X3,X5,X6,X4,X2,X0) ) ),
inference(rectify,[],[f232]) ).
tff(f237,plain,
! [X0: uni,X1: uni,X2: ty,X3: ty,X4: uni] :
( ~ sort(X2,X0)
| ~ sort(X2,X4)
| ! [X5: uni] :
( ( get(X3,X2,set(X3,X2,X1,X4,X5),X0) = get(X3,X2,X1,X0) )
| ( X0 = X4 ) ) ),
inference(rectify,[],[f186]) ).
tff(f251,plain,
! [X0: ty,X1: $int,X2: uni] :
( ~ sort(map(int,X0),X2)
| ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
inference(rectify,[],[f152]) ).
tff(f253,plain,
! [X0: $int,X1: uni,X2: ty] : ( get(X2,int,elts(X2,X1),t2tb(X0)) = get1(X2,X1,X0) ),
inference(rectify,[],[f99]) ).
tff(f256,plain,
! [X1: $int,X0: array_elt,X3: param,X2: $int] :
( ( sorted_sub2(X3,X0,X2,X1)
| ? [X4: $int,X5: $int] :
( $less(X5,X1)
& ~ le(X3,tb2t4(get1(elt1,t2tb3(X0),X4)),tb2t4(get1(elt1,t2tb3(X0),X5)))
& ~ $less(X4,X2)
& ~ $less(X5,X4) ) )
& ( ! [X4: $int,X5: $int] :
( ~ $less(X5,X1)
| le(X3,tb2t4(get1(elt1,t2tb3(X0),X4)),tb2t4(get1(elt1,t2tb3(X0),X5)))
| $less(X4,X2)
| $less(X5,X4) )
| ~ sorted_sub2(X3,X0,X2,X1) ) ),
inference(nnf_transformation,[],[f173]) ).
tff(f257,plain,
! [X0: $int,X1: array_elt,X2: param,X3: $int] :
( ( sorted_sub2(X2,X1,X3,X0)
| ? [X4: $int,X5: $int] :
( $less(X5,X0)
& ~ le(X2,tb2t4(get1(elt1,t2tb3(X1),X4)),tb2t4(get1(elt1,t2tb3(X1),X5)))
& ~ $less(X4,X3)
& ~ $less(X5,X4) ) )
& ( ! [X6: $int,X7: $int] :
( ~ $less(X7,X0)
| le(X2,tb2t4(get1(elt1,t2tb3(X1),X6)),tb2t4(get1(elt1,t2tb3(X1),X7)))
| $less(X6,X3)
| $less(X7,X6) )
| ~ sorted_sub2(X2,X1,X3,X0) ) ),
inference(rectify,[],[f256]) ).
tff(f258,plain,
! [X0: $int,X1: array_elt,X2: param,X3: $int] :
( ( sorted_sub2(X2,X1,X3,X0)
| ( $less(sK8(X0,X1,X2,X3),X0)
& ~ le(X2,tb2t4(get1(elt1,t2tb3(X1),sK7(X0,X1,X2,X3))),tb2t4(get1(elt1,t2tb3(X1),sK8(X0,X1,X2,X3))))
& ~ $less(sK7(X0,X1,X2,X3),X3)
& ~ $less(sK8(X0,X1,X2,X3),sK7(X0,X1,X2,X3)) ) )
& ( ! [X6: $int,X7: $int] :
( ~ $less(X7,X0)
| le(X2,tb2t4(get1(elt1,t2tb3(X1),X6)),tb2t4(get1(elt1,t2tb3(X1),X7)))
| $less(X6,X3)
| $less(X7,X6) )
| ~ sorted_sub2(X2,X1,X3,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X4,sK7(X0,X1,X2,X3)),skolemize(X5,sK8(X0,X1,X2,X3))],[f257]) ).
tff(f265,plain,
? [X0: $int,X1: param,X2: map_int_elt] :
( ~ $less(X0,0)
& ~ $less($sum(X0,$uminus(1)),0)
& ? [X3: map_int_elt,X4: $int] :
( ? [X5: map_int_elt,X6: $int] :
( ~ $less(X4,X6)
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X5)))
& $less(X6,X0)
& ~ $less($sum(X6,$uminus(1)),0)
& ~ $less(X0,0)
& $less($sum(X6,$uminus(1)),X0)
& ? [X7: map_int_elt] :
( ? [X8: map_int_elt] :
( exchange1(elt1,mk_array(elt1,X0,t2tb5(X5)),mk_array(elt1,X0,t2tb5(X8)),$sum(X6,$uminus(1)),X6)
& ? [X9: $int] :
( ( $sum(X6,$uminus(1)) = X9 )
& ~ sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X8))),X9,$sum(X4,1)) )
& ~ $less(X0,0)
& ( tb2t5(set(elt1,int,t2tb5(X7),t2tb($sum(X6,$uminus(1))),get(elt1,int,t2tb5(X5),t2tb(X6)))) = X8 ) )
& ( tb2t5(set(elt1,int,t2tb5(X5),t2tb(X6),get(elt1,int,t2tb5(X5),t2tb($sum(X6,$uminus(1)))))) = X7 )
& ~ $less($sum(X6,$uminus(1)),0)
& $less($sum(X6,$uminus(1)),X0)
& ~ $less(X0,0) )
& ~ $less(X6,0)
& ~ $less(X6,0)
& ~ $less(X6,0)
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X5))),0,X6)
& ! [X10: $int,X11: $int] :
( $less(X4,X11)
| ~ $less(X10,X6)
| $less(X11,$sum(X6,1))
| le(X1,tb2t4(get(elt1,int,t2tb5(X5),t2tb(X10))),tb2t4(get(elt1,int,t2tb5(X5),t2tb(X11))))
| $less(X10,0) )
& $less(X6,X0)
& ~ le(X1,tb2t4(get(elt1,int,t2tb5(X5),t2tb($sum(X6,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(X5),t2tb(X6))))
& $less($sum(X6,$uminus(1)),X0)
& ~ $less($sum(X6,$uminus(1)),0)
& ~ $less(X6,0)
& $less(0,X6)
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X5))),X6,$sum(X4,1))
& $less(X6,X0) )
& sorted_sub2(X1,tb2t3(mk_array(elt1,X0,t2tb5(X3))),0,X4)
& ~ $less(X4,0)
& ~ $less($sum(X0,$uminus(1)),X4)
& permut_all(elt1,mk_array(elt1,X0,t2tb5(X2)),mk_array(elt1,X0,t2tb5(X3))) ) ),
inference(rectify,[],[f147]) ).
tff(f266,plain,
( ~ $less(sK10,0)
& ~ $less($sum(sK10,$uminus(1)),0)
& ~ $less(sK14,sK16)
& permut_all(elt1,mk_array(elt1,sK10,t2tb5(sK12)),mk_array(elt1,sK10,t2tb5(sK15)))
& $less(sK16,sK10)
& ~ $less($sum(sK16,$uminus(1)),0)
& ~ $less(sK10,0)
& $less($sum(sK16,$uminus(1)),sK10)
& exchange1(elt1,mk_array(elt1,sK10,t2tb5(sK15)),mk_array(elt1,sK10,t2tb5(sK18)),$sum(sK16,$uminus(1)),sK16)
& ( sK19 = $sum(sK16,$uminus(1)) )
& ~ sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK19,$sum(sK14,1))
& ~ $less(sK10,0)
& ( sK18 = tb2t5(set(elt1,int,t2tb5(sK17),t2tb($sum(sK16,$uminus(1))),get(elt1,int,t2tb5(sK15),t2tb(sK16)))) )
& ( sK17 = tb2t5(set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,$uminus(1)))))) )
& ~ $less($sum(sK16,$uminus(1)),0)
& $less($sum(sK16,$uminus(1)),sK10)
& ~ $less(sK10,0)
& ~ $less(sK16,0)
& ~ $less(sK16,0)
& ~ $less(sK16,0)
& sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),0,sK16)
& ! [X10: $int,X11: $int] :
( $less(sK14,X11)
| ~ $less(X10,sK16)
| $less(X11,$sum(sK16,1))
| le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X10))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X11))))
| $less(X10,0) )
& $less(sK16,sK10)
& ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))))
& $less($sum(sK16,$uminus(1)),sK10)
& ~ $less($sum(sK16,$uminus(1)),0)
& ~ $less(sK16,0)
& $less(0,sK16)
& sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),sK16,$sum(sK14,1))
& $less(sK16,sK10)
& sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK13))),0,sK14)
& ~ $less(sK14,0)
& ~ $less($sum(sK10,$uminus(1)),sK14)
& permut_all(elt1,mk_array(elt1,sK10,t2tb5(sK12)),mk_array(elt1,sK10,t2tb5(sK13))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12),skolemize(X3,sK13),skolemize(X4,sK14),skolemize(X5,sK15),skolemize(X6,sK16),skolemize(X7,sK17),skolemize(X8,sK18),skolemize(X9,sK19)],[f265]) ).
tff(f271,plain,
! [X2: ty,X0: uni,X1: $int] : ( length(X2,mk_array(X2,X1,X0)) = X1 ),
inference(cnf_transformation,[],[f203]) ).
tff(f294,plain,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f26]) ).
tff(f299,plain,
! [X0: $int] : sort(int,t2tb(X0)),
inference(cnf_transformation,[],[f25]) ).
tff(f300,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f62]) ).
tff(f302,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f27]) ).
tff(f303,plain,
! [X2: elt,X3: elt,X0: param,X1: elt] :
( ~ le(X0,X1,X3)
| ~ le(X0,X3,X2)
| le(X0,X1,X2) ),
inference(cnf_transformation,[],[f220]) ).
tff(f305,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni,X4: ty] : sort(map(X4,X2),set(X2,X4,X1,X0,X3)),
inference(cnf_transformation,[],[f221]) ).
tff(f307,plain,
! [X2: uni,X3: ty,X0: $int,X1: $int,X4: uni] :
( exchange(X3,elts(X3,X4),elts(X3,X2),0,length(X3,X4),X1,X0)
| ~ exchange1(X3,X4,X2,X1,X0) ),
inference(cnf_transformation,[],[f224]) ).
tff(f311,plain,
! [X2: param,X0: elt,X1: elt] :
( le(X2,X1,X0)
| le(X2,X0,X1) ),
inference(cnf_transformation,[],[f226]) ).
tff(f315,plain,
! [X2: $int,X3: uni,X0: $int,X1: $int,X6: uni,X4: ty,X5: $int] :
( ~ sP0(X0,X1,X2,X3,X4,X5,X6)
| ( get(X4,int,X6,t2tb(X1)) = get(X4,int,X3,t2tb(X5)) ) ),
inference(cnf_transformation,[],[f231]) ).
tff(f317,plain,
! [X2: $int,X3: uni,X0: $int,X1: $int,X6: uni,X4: ty,X5: $int] :
( ~ sP0(X0,X1,X2,X3,X4,X5,X6)
| ( get(X4,int,X3,t2tb(X1)) = get(X4,int,X6,t2tb(X5)) ) ),
inference(cnf_transformation,[],[f231]) ).
tff(f326,plain,
! [X2: $int,X3: $int,X0: uni,X1: $int,X6: uni,X4: ty,X5: $int] :
( ~ exchange(X4,X0,X6,X5,X1,X3,X2)
| sP0(X1,X3,X5,X6,X4,X2,X0) ),
inference(cnf_transformation,[],[f233]) ).
tff(f332,plain,
! [X2: ty,X3: ty,X0: uni,X1: uni,X4: uni,X5: uni] :
( ~ sort(X2,X4)
| ~ sort(X2,X0)
| ( get(X3,X2,set(X3,X2,X1,X4,X5),X0) = get(X3,X2,X1,X0) )
| ( X0 = X4 ) ),
inference(cnf_transformation,[],[f237]) ).
tff(f352,plain,
! [X2: uni,X0: ty,X1: $int] :
( ~ sort(map(int,X0),X2)
| ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
inference(cnf_transformation,[],[f251]) ).
tff(f355,plain,
! [X0: map_int_elt] : sort(map(int,elt1),t2tb5(X0)),
inference(cnf_transformation,[],[f68]) ).
tff(f356,plain,
! [X0: uni] :
( ~ sort(map(int,elt1),X0)
| ( t2tb5(tb2t5(X0)) = X0 ) ),
inference(cnf_transformation,[],[f169]) ).
tff(f357,plain,
! [X2: ty,X0: $int,X1: uni] : ( get(X2,int,elts(X2,X1),t2tb(X0)) = get1(X2,X1,X0) ),
inference(cnf_transformation,[],[f253]) ).
tff(f360,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt,X6: $int,X7: $int] :
( ~ $less(X7,X0)
| le(X2,tb2t4(get1(elt1,t2tb3(X1),X6)),tb2t4(get1(elt1,t2tb3(X1),X7)))
| $less(X6,X3)
| $less(X7,X6)
| ~ sorted_sub2(X2,X1,X3,X0) ),
inference(cnf_transformation,[],[f258]) ).
tff(f361,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( ~ $less(sK8(X0,X1,X2,X3),sK7(X0,X1,X2,X3))
| sorted_sub2(X2,X1,X3,X0) ),
inference(cnf_transformation,[],[f258]) ).
tff(f362,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( sorted_sub2(X2,X1,X3,X0)
| ~ $less(sK7(X0,X1,X2,X3),X3) ),
inference(cnf_transformation,[],[f258]) ).
tff(f363,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( sorted_sub2(X2,X1,X3,X0)
| ~ le(X2,tb2t4(get1(elt1,t2tb3(X1),sK7(X0,X1,X2,X3))),tb2t4(get1(elt1,t2tb3(X1),sK8(X0,X1,X2,X3)))) ),
inference(cnf_transformation,[],[f258]) ).
tff(f364,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( $less(sK8(X0,X1,X2,X3),X0)
| sorted_sub2(X2,X1,X3,X0) ),
inference(cnf_transformation,[],[f258]) ).
tff(f382,plain,
sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),sK16,$sum(sK14,1)),
inference(cnf_transformation,[],[f266]) ).
tff(f385,plain,
~ $less($sum(sK16,$uminus(1)),0),
inference(cnf_transformation,[],[f266]) ).
tff(f387,plain,
~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,$uminus(1))))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16)))),
inference(cnf_transformation,[],[f266]) ).
tff(f389,plain,
! [X10: $int,X11: $int] :
( ~ $less(X10,sK16)
| $less(sK14,X11)
| $less(X11,$sum(sK16,1))
| $less(X10,0)
| le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X10))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X11)))) ),
inference(cnf_transformation,[],[f266]) ).
tff(f390,plain,
sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),0,sK16),
inference(cnf_transformation,[],[f266]) ).
tff(f397,plain,
sK17 = tb2t5(set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,$uminus(1)))))),
inference(cnf_transformation,[],[f266]) ).
tff(f398,plain,
sK18 = tb2t5(set(elt1,int,t2tb5(sK17),t2tb($sum(sK16,$uminus(1))),get(elt1,int,t2tb5(sK15),t2tb(sK16)))),
inference(cnf_transformation,[],[f266]) ).
tff(f400,plain,
~ sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK19,$sum(sK14,1)),
inference(cnf_transformation,[],[f266]) ).
tff(f401,plain,
sK19 = $sum(sK16,$uminus(1)),
inference(cnf_transformation,[],[f266]) ).
tff(f402,plain,
exchange1(elt1,mk_array(elt1,sK10,t2tb5(sK15)),mk_array(elt1,sK10,t2tb5(sK18)),$sum(sK16,$uminus(1)),sK16),
inference(cnf_transformation,[],[f266]) ).
tff(f415,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( ~ le(X2,tb2t4(get(elt1,int,elts(elt1,t2tb3(X1)),t2tb(sK7(X0,X1,X2,X3)))),tb2t4(get(elt1,int,elts(elt1,t2tb3(X1)),t2tb(sK8(X0,X1,X2,X3)))))
| sorted_sub2(X2,X1,X3,X0) ),
inference(definition_unfolding,[],[f363,f357,f357]) ).
tff(f416,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt,X6: $int,X7: $int] :
( ~ sorted_sub2(X2,X1,X3,X0)
| ~ $less(X7,X0)
| le(X2,tb2t4(get(elt1,int,elts(elt1,t2tb3(X1)),t2tb(X6))),tb2t4(get(elt1,int,elts(elt1,t2tb3(X1)),t2tb(X7))))
| $less(X6,X3)
| $less(X7,X6) ),
inference(definition_unfolding,[],[f360,f357,f357]) ).
tff(f420,plain,
sK17 = tb2t5(set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1))))),
inference(evaluation,[],[f397]) ).
tff(f428,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt,X6: $int,X7: $int] :
( ~ sorted_sub2(X2,X1,X3,X0)
| $less(0,$sum(X6,$uminus(X7)))
| le(X2,tb2t4(get(elt1,int,elts(elt1,t2tb3(X1)),t2tb(X6))),tb2t4(get(elt1,int,elts(elt1,t2tb3(X1)),t2tb(X7))))
| $less(0,$sum($sum(X7,1),$uminus(X0)))
| $less(0,$sum(X3,$uminus(X6))) ),
inference(evaluation,[],[f416]) ).
tff(f433,plain,
sK18 = tb2t5(set(elt1,int,t2tb5(sK17),t2tb($sum(sK16,-1)),get(elt1,int,t2tb5(sK15),t2tb(sK16)))),
inference(evaluation,[],[f398]) ).
tff(f442,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( sorted_sub2(X2,X1,X3,X0)
| $less(0,$sum($sum(sK8(X0,X1,X2,X3),1),$uminus(sK7(X0,X1,X2,X3)))) ),
inference(evaluation,[],[f361]) ).
tff(f448,plain,
! [X10: $int,X11: $int] :
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X10))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X11))))
| $less(0,$sum($sum(sK16,1),$uminus(X11)))
| $less(0,$sum(X11,$uminus(sK14)))
| $less(0,$uminus(X10))
| $less(0,$sum($sum(X10,1),$uminus(sK16))) ),
inference(evaluation,[],[f389]) ).
tff(f454,plain,
$less(0,$sum($sum(sK16,-1),1)),
inference(evaluation,[],[f385]) ).
tff(f462,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( sorted_sub2(X2,X1,X3,X0)
| $less(0,$sum($sum(sK7(X0,X1,X2,X3),1),$uminus(X3))) ),
inference(evaluation,[],[f362]) ).
tff(f465,plain,
~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16)))),
inference(evaluation,[],[f387]) ).
tff(f467,plain,
! [X2: param,X3: $int,X0: $int,X1: array_elt] :
( sorted_sub2(X2,X1,X3,X0)
| $less(0,$sum(X0,$uminus(sK8(X0,X1,X2,X3)))) ),
inference(evaluation,[],[f364]) ).
tff(f479,plain,
$sum(sK16,-1) = sK19,
inference(evaluation,[],[f401]) ).
tff(f482,plain,
exchange1(elt1,mk_array(elt1,sK10,t2tb5(sK15)),mk_array(elt1,sK10,t2tb5(sK18)),$sum(sK16,-1),sK16),
inference(evaluation,[],[f402]) ).
tff(f490,definition,
( spl20_1
<=> ( sK17 = tb2t5(set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1))))) ) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
tff(f492,plain,
( ( sK17 = tb2t5(set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1))))) )
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f490]) ).
tff(f493,plain,
spl20_1,
inference(avatar_split_clause,[],[f420,f490]) ).
tff(f510,definition,
( spl20_5
<=> ( sK18 = tb2t5(set(elt1,int,t2tb5(sK17),t2tb($sum(sK16,-1)),get(elt1,int,t2tb5(sK15),t2tb(sK16)))) ) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
tff(f512,plain,
( ( sK18 = tb2t5(set(elt1,int,t2tb5(sK17),t2tb($sum(sK16,-1)),get(elt1,int,t2tb5(sK15),t2tb(sK16)))) )
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f510]) ).
tff(f513,plain,
spl20_5,
inference(avatar_split_clause,[],[f433,f510]) ).
tff(f525,definition,
( spl20_8
<=> sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK19,$sum(sK14,1)) ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
tff(f527,plain,
( ~ sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK19,$sum(sK14,1))
| spl20_8 ),
inference(avatar_component_clause,[],[f525]) ).
tff(f528,plain,
~ spl20_8,
inference(avatar_split_clause,[],[f400,f525]) ).
tff(f540,definition,
( spl20_11
<=> sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),0,sK16) ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
tff(f542,plain,
( sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),0,sK16)
| ~ spl20_11 ),
inference(avatar_component_clause,[],[f540]) ).
tff(f543,plain,
spl20_11,
inference(avatar_split_clause,[],[f390,f540]) ).
tff(f545,definition,
( spl20_12
<=> $less(0,$sum($sum(sK16,-1),1)) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
tff(f547,plain,
( $less(0,$sum($sum(sK16,-1),1))
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f545]) ).
tff(f548,plain,
spl20_12,
inference(avatar_split_clause,[],[f454,f545]) ).
tff(f555,definition,
( spl20_14
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
tff(f557,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))))
| spl20_14 ),
inference(avatar_component_clause,[],[f555]) ).
tff(f558,plain,
~ spl20_14,
inference(avatar_split_clause,[],[f465,f555]) ).
tff(f580,definition,
( spl20_19
<=> sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),sK16,$sum(sK14,1)) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
tff(f582,plain,
( sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK15))),sK16,$sum(sK14,1))
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f580]) ).
tff(f583,plain,
spl20_19,
inference(avatar_split_clause,[],[f382,f580]) ).
tff(f585,definition,
( spl20_20
<=> ( $sum(sK16,-1) = sK19 ) ),
introduced(definition,[new_symbols(definition,[spl20_20])],[avatar_definition]) ).
tff(f587,plain,
( ( $sum(sK16,-1) = sK19 )
| ~ spl20_20 ),
inference(avatar_component_clause,[],[f585]) ).
tff(f588,plain,
spl20_20,
inference(avatar_split_clause,[],[f479,f585]) ).
tff(f590,definition,
( spl20_21
<=> exchange1(elt1,mk_array(elt1,sK10,t2tb5(sK15)),mk_array(elt1,sK10,t2tb5(sK18)),$sum(sK16,-1),sK16) ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
tff(f592,plain,
( exchange1(elt1,mk_array(elt1,sK10,t2tb5(sK15)),mk_array(elt1,sK10,t2tb5(sK18)),$sum(sK16,-1),sK16)
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f590]) ).
tff(f593,plain,
spl20_21,
inference(avatar_split_clause,[],[f482,f590]) ).
tff(f599,plain,
( $less(0,$sum(sK19,1))
| ~ spl20_12
| ~ spl20_20 ),
inference(forward_demodulation,[],[f547,f587]) ).
tff(f600,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))))
| spl20_14
| ~ spl20_20 ),
inference(forward_demodulation,[],[f557,f587]) ).
tff(f602,definition,
( spl20_23
<=> $less(0,$sum(sK19,1)) ),
introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition]) ).
tff(f605,plain,
( spl20_23
| ~ spl20_12
| ~ spl20_20 ),
inference(avatar_split_clause,[],[f599,f585,f545,f602]) ).
tff(f607,definition,
( spl20_24
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
tff(f609,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))))
| spl20_24 ),
inference(avatar_component_clause,[],[f607]) ).
tff(f610,plain,
( ~ spl20_24
| spl20_14
| ~ spl20_20 ),
inference(avatar_split_clause,[],[f600,f585,f555,f607]) ).
tff(f642,definition,
( spl20_30
<=> $less(0,$sum($sum(sK19,1),$uminus(sK16))) ),
introduced(definition,[new_symbols(definition,[spl20_30])],[avatar_definition]) ).
tff(f650,definition,
( spl20_32
<=> $less(0,$uminus(sK19)) ),
introduced(definition,[new_symbols(definition,[spl20_32])],[avatar_definition]) ).
tff(f656,plain,
! [X0: uni,X1: $int] :
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X1))),tb2t4(get(elt1,int,t2tb5(sK15),X0)))
| $less(0,$sum($sum(X1,1),$uminus(sK16)))
| $less(0,$sum($sum(sK16,1),$uminus(tb2t(X0))))
| $less(0,$sum(tb2t(X0),$uminus(sK14)))
| $less(0,$uminus(X1)) ),
inference(superposition,[],[f448,f302]) ).
tff(f658,plain,
! [X0: uni] : sort(int,X0),
inference(superposition,[],[f299,f302]) ).
tff(f661,plain,
! [X0: uni,X1: uni] :
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),X0)),tb2t4(get(elt1,int,t2tb5(sK15),X1)))
| $less(0,$uminus(tb2t(X0)))
| $less(0,$sum(tb2t(X1),$uminus(sK14)))
| $less(0,$sum($sum(tb2t(X0),1),$uminus(sK16)))
| $less(0,$sum($sum(sK16,1),$uminus(tb2t(X1)))) ),
inference(superposition,[],[f656,f302]) ).
tff(f675,plain,
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))))
| spl20_24 ),
inference(resolution,[],[f311,f609]) ).
tff(f678,definition,
( spl20_33
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19)))) ),
introduced(definition,[new_symbols(definition,[spl20_33])],[avatar_definition]) ).
tff(f680,plain,
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))))
| ~ spl20_33 ),
inference(avatar_component_clause,[],[f678]) ).
tff(f681,plain,
( spl20_33
| spl20_24 ),
inference(avatar_split_clause,[],[f675,f607,f678]) ).
tff(f832,plain,
! [X2: uni,X0: uni,X1: uni] : ( set(elt1,int,X0,X1,X2) = t2tb5(tb2t5(set(elt1,int,X0,X1,X2))) ),
inference(resolution,[],[f356,f305]) ).
tff(f980,plain,
( ! [X0: elt] :
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),X0)
| le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),X0) )
| ~ spl20_33 ),
inference(resolution,[],[f303,f680]) ).
tff(f1102,plain,
! [X0: map_int_elt,X1: $int] : ( t2tb5(X0) = elts(elt1,mk_array(elt1,X1,t2tb5(X0))) ),
inference(unit_resulting_resolution,[],[f352,f355]) ).
tff(f1201,plain,
( $less(0,$sum($sum(sK14,1),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| spl20_8 ),
inference(unit_resulting_resolution,[],[f467,f527]) ).
tff(f1204,definition,
( spl20_43
<=> $less(0,$sum($sum(sK14,1),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))) ),
introduced(definition,[new_symbols(definition,[spl20_43])],[avatar_definition]) ).
tff(f1207,plain,
( spl20_43
| spl20_8 ),
inference(avatar_split_clause,[],[f1201,f525,f1204]) ).
tff(f1277,plain,
( $less(0,$sum($sum(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus(sK19)))
| spl20_8 ),
inference(resolution,[],[f462,f527]) ).
tff(f1279,definition,
( spl20_47
<=> $less(0,$sum($sum(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus(sK19))) ),
introduced(definition,[new_symbols(definition,[spl20_47])],[avatar_definition]) ).
tff(f1282,plain,
( spl20_47
| spl20_8 ),
inference(avatar_split_clause,[],[f1277,f525,f1279]) ).
tff(f1356,plain,
( exchange(elt1,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),0,length(elt1,mk_array(elt1,sK10,t2tb5(sK15))),$sum(sK16,-1),sK16)
| ~ spl20_21 ),
inference(unit_resulting_resolution,[],[f307,f592]) ).
tff(f1361,plain,
( exchange(elt1,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),0,length(elt1,mk_array(elt1,sK10,t2tb5(sK15))),sK19,sK16)
| ~ spl20_20
| ~ spl20_21 ),
inference(forward_demodulation,[],[f1356,f587]) ).
tff(f1363,plain,
( exchange(elt1,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),0,sK10,sK19,sK16)
| ~ spl20_20
| ~ spl20_21 ),
inference(forward_demodulation,[],[f1361,f271]) ).
tff(f1365,plain,
( exchange(elt1,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),t2tb5(sK18),0,sK10,sK19,sK16)
| ~ spl20_20
| ~ spl20_21 ),
inference(forward_demodulation,[],[f1363,f1102]) ).
tff(f1367,definition,
( spl20_49
<=> exchange(elt1,t2tb5(sK15),t2tb5(sK18),0,sK10,sK19,sK16) ),
introduced(definition,[new_symbols(definition,[spl20_49])],[avatar_definition]) ).
tff(f1369,plain,
( exchange(elt1,t2tb5(sK15),t2tb5(sK18),0,sK10,sK19,sK16)
| ~ spl20_49 ),
inference(avatar_component_clause,[],[f1367]) ).
tff(f1371,plain,
( exchange(elt1,t2tb5(sK15),t2tb5(sK18),0,sK10,sK19,sK16)
| ~ spl20_20
| ~ spl20_21 ),
inference(forward_demodulation,[],[f1365,f1102]) ).
tff(f1372,plain,
( spl20_49
| ~ spl20_20
| ~ spl20_21 ),
inference(avatar_split_clause,[],[f1371,f590,f585,f1367]) ).
tff(f1374,plain,
( sP0(sK10,sK19,0,t2tb5(sK18),elt1,sK16,t2tb5(sK15))
| ~ spl20_49 ),
inference(resolution,[],[f1369,f326]) ).
tff(f1376,definition,
( spl20_50
<=> sP0(sK10,sK19,0,t2tb5(sK18),elt1,sK16,t2tb5(sK15)) ),
introduced(definition,[new_symbols(definition,[spl20_50])],[avatar_definition]) ).
tff(f1378,plain,
( sP0(sK10,sK19,0,t2tb5(sK18),elt1,sK16,t2tb5(sK15))
| ~ spl20_50 ),
inference(avatar_component_clause,[],[f1376]) ).
tff(f1379,plain,
( spl20_50
| ~ spl20_49 ),
inference(avatar_split_clause,[],[f1374,f1367,f1376]) ).
tff(f1386,plain,
( ( get(elt1,int,t2tb5(sK18),t2tb(sK16)) = get(elt1,int,t2tb5(sK15),t2tb(sK19)) )
| ~ spl20_50 ),
inference(resolution,[],[f1378,f315]) ).
tff(f1397,definition,
( spl20_51
<=> ( get(elt1,int,t2tb5(sK18),t2tb(sK16)) = get(elt1,int,t2tb5(sK15),t2tb(sK19)) ) ),
introduced(definition,[new_symbols(definition,[spl20_51])],[avatar_definition]) ).
tff(f1399,plain,
( ( get(elt1,int,t2tb5(sK18),t2tb(sK16)) = get(elt1,int,t2tb5(sK15),t2tb(sK19)) )
| ~ spl20_51 ),
inference(avatar_component_clause,[],[f1397]) ).
tff(f1400,plain,
( spl20_51
| ~ spl20_50 ),
inference(avatar_split_clause,[],[f1386,f1376,f1397]) ).
tff(f1401,plain,
( ( get(elt1,int,t2tb5(sK18),t2tb(sK19)) = get(elt1,int,t2tb5(sK15),t2tb(sK16)) )
| ~ spl20_50 ),
inference(unit_resulting_resolution,[],[f317,f1378]) ).
tff(f1404,definition,
( spl20_52
<=> ( get(elt1,int,t2tb5(sK18),t2tb(sK19)) = get(elt1,int,t2tb5(sK15),t2tb(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl20_52])],[avatar_definition]) ).
tff(f1406,plain,
( ( get(elt1,int,t2tb5(sK18),t2tb(sK19)) = get(elt1,int,t2tb5(sK15),t2tb(sK16)) )
| ~ spl20_52 ),
inference(avatar_component_clause,[],[f1404]) ).
tff(f1407,plain,
( spl20_52
| ~ spl20_50 ),
inference(avatar_split_clause,[],[f1401,f1376,f1404]) ).
tff(f1409,plain,
( $less(0,$sum($sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| spl20_8 ),
inference(resolution,[],[f442,f527]) ).
tff(f1411,definition,
( spl20_53
<=> $less(0,$sum($sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))) ),
introduced(definition,[new_symbols(definition,[spl20_53])],[avatar_definition]) ).
tff(f1414,plain,
( spl20_53
| spl20_8 ),
inference(avatar_split_clause,[],[f1409,f525,f1411]) ).
tff(f1494,plain,
! [X2: uni,X3: $int,X0: uni,X1: ty,X4: uni] :
( ( t2tb(X3) = X0 )
| ( get(X1,int,X2,X0) = get(X1,int,set(X1,int,X2,t2tb(X3),X4),X0) )
| ~ sort(int,X0) ),
inference(resolution,[],[f332,f299]) ).
tff(f1510,plain,
! [X2: uni,X3: $int,X0: uni,X1: ty,X4: uni] :
( ( get(X1,int,X2,X0) = get(X1,int,set(X1,int,X2,t2tb(X3),X4),X0) )
| ( t2tb(X3) = X0 ) ),
inference(forward_subsumption_resolution,[],[f1494,f658]) ).
tff(f1720,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8 ),
inference(unit_resulting_resolution,[],[f415,f527]) ).
tff(f1727,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8 ),
inference(forward_demodulation,[],[f1720,f300]) ).
tff(f1728,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8 ),
inference(forward_demodulation,[],[f1727,f1102]) ).
tff(f1730,definition,
( spl20_68
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_68])],[avatar_definition]) ).
tff(f1732,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_68 ),
inference(avatar_component_clause,[],[f1730]) ).
tff(f1733,plain,
( ~ spl20_68
| spl20_8 ),
inference(avatar_split_clause,[],[f1728,f525,f1730]) ).
tff(f1852,plain,
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_68 ),
inference(resolution,[],[f1732,f311]) ).
tff(f1854,definition,
( spl20_75
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_75])],[avatar_definition]) ).
tff(f1857,plain,
( spl20_75
| spl20_68 ),
inference(avatar_split_clause,[],[f1852,f1730,f1854]) ).
tff(f1863,definition,
( spl20_77
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_77])],[avatar_definition]) ).
tff(f1864,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_77 ),
inference(avatar_component_clause,[],[f1863]) ).
tff(f2102,plain,
( ! [X0: $int,X1: $int] :
( $less(0,$sum($sum(X1,1),$uminus(sK16)))
| le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK15))))),t2tb(X0))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK15))))),t2tb(X1))))
| $less(0,$sum(X0,$uminus(X1)))
| $less(0,$sum(0,$uminus(X0))) )
| ~ spl20_11 ),
inference(resolution,[],[f428,f542]) ).
tff(f2103,plain,
( ! [X0: $int,X1: $int] :
( le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK15))))),t2tb(X0))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK15))))),t2tb(X1))))
| $less(0,$sum(sK16,$uminus(X0)))
| $less(0,$sum(X0,$uminus(X1)))
| $less(0,$sum($sum(X1,1),$uminus($sum(sK14,1)))) )
| ~ spl20_19 ),
inference(resolution,[],[f428,f582]) ).
tff(f2108,plain,
( ! [X0: $int,X1: $int] :
( $less(0,$sum(X0,$uminus(X1)))
| $less(0,$sum($sum(X1,1),$uminus(sK16)))
| $less(0,$uminus(X0))
| le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK15))))),t2tb(X0))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK15))))),t2tb(X1)))) )
| ~ spl20_11 ),
inference(evaluation,[],[f2102]) ).
tff(f2110,plain,
( ! [X0: $int,X1: $int] :
( le(sK11,tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),t2tb(X0))),tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),t2tb(X1))))
| $less(0,$sum(X0,$uminus(X1)))
| $less(0,$uminus(X0))
| $less(0,$sum($sum(X1,1),$uminus(sK16))) )
| ~ spl20_11 ),
inference(forward_demodulation,[],[f2108,f300]) ).
tff(f2111,plain,
( ! [X0: $int,X1: $int] :
( le(sK11,tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),t2tb(X0))),tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK15))),t2tb(X1))))
| $less(0,$sum($sum(X1,1),$uminus($sum(sK14,1))))
| $less(0,$sum(X0,$uminus(X1)))
| $less(0,$sum(sK16,$uminus(X0))) )
| ~ spl20_19 ),
inference(forward_demodulation,[],[f2103,f300]) ).
tff(f2113,plain,
( ! [X0: $int,X1: $int] :
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X0))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X1))))
| $less(0,$uminus(X0))
| $less(0,$sum($sum(X1,1),$uminus(sK16)))
| $less(0,$sum(X0,$uminus(X1))) )
| ~ spl20_11 ),
inference(forward_demodulation,[],[f2110,f1102]) ).
tff(f2114,plain,
( ! [X0: $int,X1: $int] :
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X0))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(X1))))
| $less(0,$sum($sum(X1,1),$uminus($sum(sK14,1))))
| $less(0,$sum(X0,$uminus(X1)))
| $less(0,$sum(sK16,$uminus(X0))) )
| ~ spl20_19 ),
inference(forward_demodulation,[],[f2111,f1102]) ).
tff(f2830,plain,
( ( t2tb5(sK17) = set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb($sum(sK16,-1)))) )
| ~ spl20_1 ),
inference(superposition,[],[f832,f492]) ).
tff(f2832,plain,
( ( t2tb5(sK18) = set(elt1,int,t2tb5(sK17),t2tb($sum(sK16,-1)),get(elt1,int,t2tb5(sK15),t2tb(sK16))) )
| ~ spl20_5 ),
inference(superposition,[],[f832,f512]) ).
tff(f2839,plain,
( ( set(elt1,int,t2tb5(sK17),t2tb(sK19),get(elt1,int,t2tb5(sK15),t2tb(sK16))) = t2tb5(sK18) )
| ~ spl20_5
| ~ spl20_20 ),
inference(forward_demodulation,[],[f2832,f587]) ).
tff(f2841,definition,
( spl20_91
<=> ( t2tb5(sK17) = set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb(sK19))) ) ),
introduced(definition,[new_symbols(definition,[spl20_91])],[avatar_definition]) ).
tff(f2843,plain,
( ( t2tb5(sK17) = set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb(sK19))) )
| ~ spl20_91 ),
inference(avatar_component_clause,[],[f2841]) ).
tff(f2846,definition,
( spl20_92
<=> ( set(elt1,int,t2tb5(sK17),t2tb(sK19),get(elt1,int,t2tb5(sK15),t2tb(sK16))) = t2tb5(sK18) ) ),
introduced(definition,[new_symbols(definition,[spl20_92])],[avatar_definition]) ).
tff(f2848,plain,
( ( set(elt1,int,t2tb5(sK17),t2tb(sK19),get(elt1,int,t2tb5(sK15),t2tb(sK16))) = t2tb5(sK18) )
| ~ spl20_92 ),
inference(avatar_component_clause,[],[f2846]) ).
tff(f2850,plain,
( ( t2tb5(sK17) = set(elt1,int,t2tb5(sK15),t2tb(sK16),get(elt1,int,t2tb5(sK15),t2tb(sK19))) )
| ~ spl20_1
| ~ spl20_20 ),
inference(forward_demodulation,[],[f2830,f587]) ).
tff(f2851,plain,
( spl20_92
| ~ spl20_5
| ~ spl20_20 ),
inference(avatar_split_clause,[],[f2839,f585,f510,f2846]) ).
tff(f2852,plain,
( spl20_91
| ~ spl20_1
| ~ spl20_20 ),
inference(avatar_split_clause,[],[f2850,f585,f490,f2841]) ).
tff(f3908,plain,
( ! [X0: uni] :
( ( get(elt1,int,t2tb5(sK15),X0) = get(elt1,int,t2tb5(sK17),X0) )
| ( t2tb(sK16) = X0 ) )
| ~ spl20_91 ),
inference(superposition,[],[f1510,f2843]) ).
tff(f3909,plain,
( ! [X0: uni] :
( ( get(elt1,int,t2tb5(sK18),X0) = get(elt1,int,t2tb5(sK17),X0) )
| ( t2tb(sK19) = X0 ) )
| ~ spl20_92 ),
inference(superposition,[],[f1510,f2848]) ).
tff(f4019,plain,
( ! [X0: uni] :
( ( get(elt1,int,t2tb5(sK18),X0) = get(elt1,int,t2tb5(sK15),X0) )
| ( t2tb(sK19) = X0 )
| ( t2tb(sK16) = X0 ) )
| ~ spl20_91
| ~ spl20_92 ),
inference(superposition,[],[f3908,f3909]) ).
tff(f4057,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ( t2tb(sK19) = t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ( t2tb(sK16) = t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| spl20_68
| ~ spl20_91
| ~ spl20_92 ),
inference(superposition,[],[f1732,f4019]) ).
tff(f4059,plain,
( ( t2tb(sK19) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ( t2tb(sK16) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| spl20_68
| ~ spl20_91
| ~ spl20_92 ),
inference(superposition,[],[f1732,f4019]) ).
tff(f4080,definition,
( spl20_96
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_96])],[avatar_definition]) ).
tff(f4082,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_96 ),
inference(avatar_component_clause,[],[f4080]) ).
tff(f4084,definition,
( spl20_97
<=> ( t2tb(sK19) = t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) ) ),
introduced(definition,[new_symbols(definition,[spl20_97])],[avatar_definition]) ).
tff(f4086,plain,
( ( t2tb(sK19) = t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ~ spl20_97 ),
inference(avatar_component_clause,[],[f4084]) ).
tff(f4088,definition,
( spl20_98
<=> ( t2tb(sK16) = t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) ) ),
introduced(definition,[new_symbols(definition,[spl20_98])],[avatar_definition]) ).
tff(f4090,plain,
( ( t2tb(sK16) = t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ~ spl20_98 ),
inference(avatar_component_clause,[],[f4088]) ).
tff(f4091,plain,
( ~ spl20_96
| spl20_97
| spl20_98
| spl20_68
| ~ spl20_91
| ~ spl20_92 ),
inference(avatar_split_clause,[],[f4057,f2846,f2841,f1730,f4088,f4084,f4080]) ).
tff(f4093,definition,
( spl20_99
<=> ( t2tb(sK16) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) ) ),
introduced(definition,[new_symbols(definition,[spl20_99])],[avatar_definition]) ).
tff(f4097,definition,
( spl20_100
<=> ( t2tb(sK19) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) ) ),
introduced(definition,[new_symbols(definition,[spl20_100])],[avatar_definition]) ).
tff(f4098,plain,
( ( t2tb(sK19) != t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| spl20_100 ),
inference(avatar_component_clause,[],[f4097]) ).
tff(f4099,plain,
( ( t2tb(sK19) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ~ spl20_100 ),
inference(avatar_component_clause,[],[f4097]) ).
tff(f4101,definition,
( spl20_101
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_101])],[avatar_definition]) ).
tff(f4103,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_101 ),
inference(avatar_component_clause,[],[f4101]) ).
tff(f4104,plain,
( spl20_99
| spl20_100
| ~ spl20_101
| spl20_68
| ~ spl20_91
| ~ spl20_92 ),
inference(avatar_split_clause,[],[f4059,f2846,f2841,f1730,f4101,f4097,f4093]) ).
tff(f4194,plain,
( ( sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) = tb2t(t2tb(sK16)) )
| ~ spl20_98 ),
inference(superposition,[],[f294,f4090]) ).
tff(f4236,plain,
( ( sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) = sK16 )
| ~ spl20_98 ),
inference(forward_demodulation,[],[f4194,f294]) ).
tff(f4263,definition,
( spl20_111
<=> $less(0,$uminus(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))) ),
introduced(definition,[new_symbols(definition,[spl20_111])],[avatar_definition]) ).
tff(f4297,definition,
( spl20_119
<=> $less(0,$sum(sK16,$uminus(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))) ),
introduced(definition,[new_symbols(definition,[spl20_119])],[avatar_definition]) ).
tff(f4340,definition,
( spl20_129
<=> ( sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) = sK16 ) ),
introduced(definition,[new_symbols(definition,[spl20_129])],[avatar_definition]) ).
tff(f4342,plain,
( ( sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) = sK16 )
| ~ spl20_129 ),
inference(avatar_component_clause,[],[f4340]) ).
tff(f4343,plain,
( spl20_129
| ~ spl20_98 ),
inference(avatar_split_clause,[],[f4236,f4088,f4340]) ).
tff(f4375,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK19))))
| sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK19,$sum(sK14,1))
| ~ spl20_100 ),
inference(superposition,[],[f415,f4099]) ).
tff(f4376,plain,
( ( tb2t(t2tb(sK19)) = sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) )
| ~ spl20_100 ),
inference(superposition,[],[f294,f4099]) ).
tff(f4418,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK19))))
| spl20_8
| ~ spl20_100 ),
inference(forward_subsumption_resolution,[],[f4375,f527]) ).
tff(f4427,definition,
( spl20_133
<=> $less(0,$sum($sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus(sK16))) ),
introduced(definition,[new_symbols(definition,[spl20_133])],[avatar_definition]) ).
tff(f4458,definition,
( spl20_140
<=> $less(0,$sum($sum(sK16,1),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))) ),
introduced(definition,[new_symbols(definition,[spl20_140])],[avatar_definition]) ).
tff(f4465,definition,
( spl20_142
<=> $less(0,$sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK14))) ),
introduced(definition,[new_symbols(definition,[spl20_142])],[avatar_definition]) ).
tff(f4478,definition,
( spl20_145
<=> $less(0,$sum($sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus($sum(sK14,1)))) ),
introduced(definition,[new_symbols(definition,[spl20_145])],[avatar_definition]) ).
tff(f4490,plain,
( ( sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) = sK19 )
| ~ spl20_100 ),
inference(forward_demodulation,[],[f4376,f294]) ).
tff(f4517,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),t2tb(sK19))))
| spl20_8
| ~ spl20_100 ),
inference(forward_demodulation,[],[f4418,f300]) ).
tff(f4519,definition,
( spl20_154
<=> ( sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19) = sK19 ) ),
introduced(definition,[new_symbols(definition,[spl20_154])],[avatar_definition]) ).
tff(f4522,plain,
( spl20_154
| ~ spl20_100 ),
inference(avatar_split_clause,[],[f4490,f4097,f4519]) ).
tff(f4524,definition,
( spl20_155
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl20_155])],[avatar_definition]) ).
tff(f4528,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK19))))
| spl20_8
| ~ spl20_100 ),
inference(forward_demodulation,[],[f4517,f1102]) ).
tff(f4529,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))))
| spl20_8
| ~ spl20_52
| ~ spl20_100 ),
inference(forward_demodulation,[],[f4528,f1406]) ).
tff(f4530,plain,
( ~ spl20_155
| spl20_8
| ~ spl20_52
| ~ spl20_100 ),
inference(avatar_split_clause,[],[f4529,f4097,f1404,f525,f4524]) ).
tff(f4984,plain,
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))))
| spl20_77 ),
inference(unit_resulting_resolution,[],[f311,f1864]) ).
tff(f4993,plain,
( spl20_155
| spl20_77 ),
inference(avatar_split_clause,[],[f4984,f1863,f4524]) ).
tff(f5000,definition,
( spl20_182
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_182])],[avatar_definition]) ).
tff(f5002,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_182 ),
inference(avatar_component_clause,[],[f5000]) ).
tff(f5012,definition,
( spl20_184
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_184])],[avatar_definition]) ).
tff(f5013,plain,
( le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ~ spl20_184 ),
inference(avatar_component_clause,[],[f5012]) ).
tff(f5303,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ( t2tb(sK16) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ( t2tb(sK19) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ~ spl20_91
| ~ spl20_92
| spl20_96 ),
inference(superposition,[],[f4082,f4019]) ).
tff(f5317,plain,
( ( t2tb(sK16) = t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)) )
| ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ~ spl20_91
| ~ spl20_92
| spl20_96
| spl20_100 ),
inference(forward_subsumption_resolution,[],[f5303,f4098]) ).
tff(f5320,definition,
( spl20_193
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_193])],[avatar_definition]) ).
tff(f5322,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_193 ),
inference(avatar_component_clause,[],[f5320]) ).
tff(f5323,plain,
( ~ spl20_193
| spl20_99
| ~ spl20_91
| ~ spl20_92
| spl20_96
| spl20_100 ),
inference(avatar_split_clause,[],[f5317,f4097,f4080,f2846,f2841,f4093,f5320]) ).
tff(f5326,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ~ spl20_33
| spl20_182 ),
inference(unit_resulting_resolution,[],[f980,f5002]) ).
tff(f5476,plain,
( $less(0,$sum(sK16,$uminus(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| $less(0,$sum($sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus($sum(sK14,1))))
| $less(0,$sum(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| ~ spl20_19
| spl20_193 ),
inference(resolution,[],[f5322,f2114]) ).
tff(f5477,plain,
( $less(0,$uminus(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))
| $less(0,$sum(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| $less(0,$sum($sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),1),$uminus(sK16)))
| ~ spl20_11
| spl20_193 ),
inference(resolution,[],[f5322,f2113]) ).
tff(f5505,definition,
( spl20_202
<=> $less(0,$sum(sK7($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))) ),
introduced(definition,[new_symbols(definition,[spl20_202])],[avatar_definition]) ).
tff(f5508,plain,
( spl20_133
| spl20_111
| spl20_202
| ~ spl20_11
| spl20_193 ),
inference(avatar_split_clause,[],[f5477,f5320,f540,f5505,f4263,f4427]) ).
tff(f5517,plain,
( spl20_119
| spl20_202
| spl20_145
| ~ spl20_19
| spl20_193 ),
inference(avatar_split_clause,[],[f5476,f5320,f580,f4478,f5505,f4297]) ).
tff(f5596,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_101
| ~ spl20_129 ),
inference(superposition,[],[f4103,f4342]) ).
tff(f5605,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| ~ spl20_51
| spl20_101
| ~ spl20_129 ),
inference(forward_demodulation,[],[f5596,f1399]) ).
tff(f5609,definition,
( spl20_206
<=> le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))) ),
introduced(definition,[new_symbols(definition,[spl20_206])],[avatar_definition]) ).
tff(f5611,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_206 ),
inference(avatar_component_clause,[],[f5609]) ).
tff(f5612,plain,
( ~ spl20_206
| ~ spl20_51
| spl20_101
| ~ spl20_129 ),
inference(avatar_split_clause,[],[f5605,f4340,f4101,f1397,f5609]) ).
tff(f5746,plain,
( $less(0,$sum(tb2t(t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))),$uminus(sK14)))
| $less(0,$uminus(tb2t(t2tb(sK19))))
| $less(0,$sum($sum(sK16,1),$uminus(tb2t(t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))))
| $less(0,$sum($sum(tb2t(t2tb(sK19)),1),$uminus(sK16)))
| spl20_206 ),
inference(resolution,[],[f5611,f661]) ).
tff(f5776,plain,
( $less(0,$sum($sum(sK16,1),$uminus(tb2t(t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))))
| $less(0,$sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK14)))
| $less(0,$uminus(tb2t(t2tb(sK19))))
| $less(0,$sum($sum(tb2t(t2tb(sK19)),1),$uminus(sK16)))
| spl20_206 ),
inference(forward_demodulation,[],[f5746,f294]) ).
tff(f5781,plain,
( $less(0,$sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK14)))
| $less(0,$sum($sum(tb2t(t2tb(sK19)),1),$uminus(sK16)))
| $less(0,$sum($sum(sK16,1),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| $less(0,$uminus(tb2t(t2tb(sK19))))
| spl20_206 ),
inference(forward_demodulation,[],[f5776,f294]) ).
tff(f5786,plain,
( $less(0,$uminus(tb2t(t2tb(sK19))))
| $less(0,$sum($sum(sK16,1),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| $less(0,$sum($sum(sK19,1),$uminus(sK16)))
| $less(0,$sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK14)))
| spl20_206 ),
inference(forward_demodulation,[],[f5781,f294]) ).
tff(f5788,plain,
( $less(0,$sum($sum(sK19,1),$uminus(sK16)))
| $less(0,$sum($sum(sK16,1),$uminus(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19))))
| $less(0,$uminus(sK19))
| $less(0,$sum(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19),$uminus(sK14)))
| spl20_206 ),
inference(forward_demodulation,[],[f5786,f294]) ).
tff(f5789,plain,
( spl20_30
| spl20_32
| spl20_142
| spl20_140
| spl20_206 ),
inference(avatar_split_clause,[],[f5788,f5609,f4458,f4465,f650,f642]) ).
tff(f5872,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK19))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| sorted_sub2(sK11,tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK19,$sum(sK14,1))
| ~ spl20_97 ),
inference(superposition,[],[f415,f4086]) ).
tff(f5922,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK19))),tb2t4(get(elt1,int,elts(elt1,t2tb3(tb2t3(mk_array(elt1,sK10,t2tb5(sK18))))),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8
| ~ spl20_97 ),
inference(forward_subsumption_resolution,[],[f5872,f527]) ).
tff(f5970,plain,
( ~ le(sK11,tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),t2tb(sK19))),tb2t4(get(elt1,int,elts(elt1,mk_array(elt1,sK10,t2tb5(sK18))),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8
| ~ spl20_97 ),
inference(forward_demodulation,[],[f5922,f300]) ).
tff(f5977,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK19))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8
| ~ spl20_97 ),
inference(forward_demodulation,[],[f5970,f1102]) ).
tff(f5978,plain,
( ~ le(sK11,tb2t4(get(elt1,int,t2tb5(sK15),t2tb(sK16))),tb2t4(get(elt1,int,t2tb5(sK18),t2tb(sK8($sum(sK14,1),tb2t3(mk_array(elt1,sK10,t2tb5(sK18))),sK11,sK19)))))
| spl20_8
| ~ spl20_52
| ~ spl20_97 ),
inference(forward_demodulation,[],[f5977,f1406]) ).
tff(f5979,plain,
( ~ spl20_182
| spl20_8
| ~ spl20_52
| ~ spl20_97 ),
inference(avatar_split_clause,[],[f5978,f4084,f1404,f525,f5000]) ).
tff(f5987,plain,
( $false
| ~ spl20_33
| spl20_182
| ~ spl20_184 ),
inference(forward_subsumption_resolution,[],[f5326,f5013]) ).
tff(f5988,plain,
( ~ spl20_33
| spl20_182
| ~ spl20_184 ),
inference(avatar_contradiction_clause,[],[f5987]) ).
tff(f6005,plain,
$false,
inference(avatar_smt_refutation,[],[f5988,f5979,f5789,f5612,f5517,f5508,f5323,f4993,f4530,f4522,f4343,f4104,f4091,f2852,f2851,f1857,f1733,f1414,f1407,f1400,f1379,f1372,f1282,f1207,f681,f610,f605,f593,f588,f583,f558,f548,f543,f528,f513,f493]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW606_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n006.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 14:22:27 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.33/1.47 % (3998302)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.33/1.47 % (3998327)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=931176664:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.33/1.47 % (3998327)Instruction limit reached!
% 4.33/1.47 % (3998327)------------------------------
% 4.33/1.47 % (3998327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.47 % (3998327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.47 % (3998327)CaDiCaL version: 2.1.3
% 4.33/1.47 % (3998327)Termination reason: Instruction limit
% 4.33/1.47 % (3998327)Termination phase: Property scanning
% 4.33/1.47 % (3998327)Time elapsed: 0.004 s
% 4.33/1.47 % (3998327)Peak memory usage: 86 MB
% 4.33/1.47 % (3998327)Instructions burned: 8 (million)
% 4.33/1.47 % (3998330)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=868441644:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.33/1.47 % (3998326)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1108480583:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.33/1.47 % (3998324)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2701245040:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.33/1.47 % (3998325)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1697606891:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.33/1.47 % (3998330)Instruction limit reached!
% 4.33/1.47 % (3998330)------------------------------
% 4.33/1.47 % (3998330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.47 % (3998330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.47 % (3998330)CaDiCaL version: 2.1.3
% 4.33/1.47 % (3998330)Termination reason: Instruction limit
% 4.33/1.47 % (3998330)Termination phase: Saturation
% 4.33/1.47 % (3998330)Time elapsed: 0.066 s
% 4.33/1.47 % (3998330)Peak memory usage: 116 MB
% 4.33/1.47 % (3998330)Instructions burned: 33 (million)
% 4.33/1.47 % (3998329)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3952835276:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.33/1.47 % (3998328)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2349098150:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.33/1.47 % (3998328)Instruction limit reached!
% 4.33/1.47 % (3998328)------------------------------
% 4.33/1.47 % (3998328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.47 % (3998328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.47 % (3998328)CaDiCaL version: 2.1.3
% 4.33/1.47 % (3998328)Termination reason: Instruction limit
% 4.33/1.47 % (3998328)Termination phase: Clausification
% 4.33/1.47 % (3998328)Time elapsed: 0.005 s
% 4.33/1.47 % (3998328)Peak memory usage: 86 MB
% 4.33/1.47 % (3998328)Instructions burned: 6 (million)
% 4.33/1.47 % (3998324)Instruction limit reached!
% 4.33/1.47 % (3998324)------------------------------
% 4.33/1.47 % (3998324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.47 % (3998324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.47 % (3998324)CaDiCaL version: 2.1.3
% 4.33/1.47 % (3998324)Termination reason: Instruction limit
% 4.33/1.47 % (3998324)Termination phase: Saturation
% 4.33/1.47 % (3998324)Time elapsed: 0.036 s
% 4.33/1.47 % (3998324)Peak memory usage: 104 MB
% 4.33/1.47 % (3998324)Instructions burned: 12 (million)
% 4.33/1.47 % (3998329)Instruction limit reached!
% 4.33/1.47 % (3998329)------------------------------
% 4.33/1.47 % (3998329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.47 % (3998329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.47 % (3998329)CaDiCaL version: 2.1.3
% 4.33/1.47 % (3998329)Termination reason: Instruction limit
% 4.33/1.47 % (3998329)Termination phase: Saturation
% 4.33/1.47 % (3998329)Time elapsed: 0.056 s
% 4.33/1.47 % (3998329)Peak memory usage: 116 MB
% 4.33/1.47 % (3998329)Instructions burned: 47 (million)
% 4.33/1.47 % (3998337)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2229082775:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.33/1.47 % (3998337)Instruction limit reached!
% 4.33/1.47 % (3998337)------------------------------
% 5.89/1.68 % (3998337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.68 % (3998337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.68 % (3998337)CaDiCaL version: 2.1.3
% 5.89/1.68 % (3998337)Termination reason: Instruction limit
% 5.89/1.68 % (3998337)Termination phase: Saturation
% 5.89/1.68 % (3998337)Time elapsed: 0.008 s
% 5.89/1.68 % (3998337)Peak memory usage: 89 MB
% 5.89/1.68 % (3998337)Instructions burned: 15 (million)
% 5.89/1.68 % (3998326)Instruction limit reached!
% 5.89/1.68 % (3998326)------------------------------
% 5.89/1.68 % (3998326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.68 % (3998326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.68 % (3998326)CaDiCaL version: 2.1.3
% 5.89/1.68 % (3998326)Termination reason: Instruction limit
% 5.89/1.68 % (3998326)Termination phase: Saturation
% 5.89/1.68 % (3998326)Time elapsed: 0.172 s
% 5.89/1.68 % (3998326)Peak memory usage: 117 MB
% 5.89/1.68 % (3998326)Instructions burned: 203 (million)
% 5.89/1.68 % (3998346)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=4174621326:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 5.89/1.68 % (3998346)Instruction limit reached!
% 5.89/1.68 % (3998346)------------------------------
% 5.89/1.68 % (3998346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.68 % (3998346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.68 % (3998346)CaDiCaL version: 2.1.3
% 5.89/1.68 % (3998346)Termination reason: Instruction limit
% 5.89/1.68 % (3998346)Termination phase: Saturation
% 5.89/1.68 % (3998346)Time elapsed: 0.022 s
% 5.89/1.68 % (3998346)Peak memory usage: 89 MB
% 5.89/1.68 % (3998346)Instructions burned: 29 (million)
% 5.89/1.68 % (3998348)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2537089054:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 5.89/1.68 % (3998347)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2121416692:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.89/1.68 % (3998358)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2732876859:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 5.89/1.68 % (3998347)Instruction limit reached!
% 5.89/1.68 % (3998347)------------------------------
% 5.89/1.68 % (3998347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.68 % (3998347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.68 % (3998347)CaDiCaL version: 2.1.3
% 5.89/1.68 % (3998347)Termination reason: Instruction limit
% 5.89/1.68 % (3998347)Termination phase: Saturation
% 5.89/1.68 % (3998347)Time elapsed: 0.014 s
% 5.89/1.68 % (3998347)Peak memory usage: 89 MB
% 5.89/1.68 % (3998347)Instructions burned: 17 (million)
% 5.89/1.68 % (3998348)Instruction limit reached!
% 5.89/1.68 % (3998348)------------------------------
% 5.89/1.68 % (3998348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.68 % (3998348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.68 % (3998348)CaDiCaL version: 2.1.3
% 5.89/1.68 % (3998348)Termination reason: Instruction limit
% 5.89/1.68 % (3998348)Termination phase: Saturation
% 5.89/1.68 % (3998348)Time elapsed: 0.026 s
% 5.89/1.68 % (3998348)Peak memory usage: 89 MB
% 5.89/1.68 % (3998348)Instructions burned: 25 (million)
% 5.89/1.68 % (3998358)Instruction limit reached!
% 5.89/1.68 % (3998358)------------------------------
% 5.89/1.68 % (3998358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.89/1.68 % (3998358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.68 % (3998358)CaDiCaL version: 2.1.3
% 5.89/1.68 % (3998358)Termination reason: Instruction limit
% 5.89/1.68 % (3998358)Termination phase: Saturation
% 5.89/1.68 % (3998358)Time elapsed: 0.034 s
% 5.89/1.68 % (3998358)Peak memory usage: 89 MB
% 5.89/1.68 % (3998358)Instructions burned: 88 (million)
% 5.89/1.68 % (3998353)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=4217948747:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 5.89/1.68 % (3998325)Instruction limit reached!
% 5.89/1.68 % (3998325)------------------------------
% 5.89/1.68 % (3998325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/1.90 % (3998325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.90 % (3998325)CaDiCaL version: 2.1.3
% 7.37/1.90 % (3998325)Termination reason: Instruction limit
% 7.37/1.90 % (3998325)Termination phase: Saturation
% 7.37/1.90 % (3998325)Time elapsed: 0.313 s
% 7.37/1.90 % (3998325)Peak memory usage: 117 MB
% 7.37/1.90 % (3998325)Instructions burned: 309 (million)
% 7.37/1.90 % (3998353)Instruction limit reached!
% 7.37/1.90 % (3998353)------------------------------
% 7.37/1.90 % (3998353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/1.90 % (3998353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.90 % (3998353)CaDiCaL version: 2.1.3
% 7.37/1.90 % (3998353)Termination reason: Instruction limit
% 7.37/1.90 % (3998353)Termination phase: Saturation
% 7.37/1.90 % (3998353)Time elapsed: 0.028 s
% 7.37/1.90 % (3998353)Peak memory usage: 89 MB
% 7.37/1.90 % (3998353)Instructions burned: 27 (million)
% 7.37/1.90 % (3998362)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1069377557:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.37/1.90 % (3998362)Instruction limit reached!
% 7.37/1.90 % (3998362)------------------------------
% 7.37/1.90 % (3998362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/1.90 % (3998362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.90 % (3998362)CaDiCaL version: 2.1.3
% 7.37/1.90 % (3998362)Termination reason: Instruction limit
% 7.37/1.90 % (3998362)Termination phase: Preprocessing 1
% 7.37/1.90 % (3998362)Time elapsed: 0.003 s
% 7.37/1.90 % (3998362)Peak memory usage: 85 MB
% 7.37/1.90 % (3998362)Instructions burned: 3 (million)
% 7.37/1.90 % (3998364)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3955149547:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 7.37/1.90 % (3998372)lrs+10_1_thi=all:si=on:fd=off:random_seed=85400863:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 7.37/1.90 % (3998368)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=711997244:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.37/1.90 % (3998368)Instruction limit reached!
% 7.37/1.90 % (3998368)------------------------------
% 7.37/1.90 % (3998368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/1.90 % (3998368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.90 % (3998368)CaDiCaL version: 2.1.3
% 7.37/1.90 % (3998368)Termination reason: Instruction limit
% 7.37/1.90 % (3998368)Termination phase: Naming
% 7.37/1.90 % (3998368)Time elapsed: 0.004 s
% 7.37/1.90 % (3998368)Peak memory usage: 86 MB
% 7.37/1.90 % (3998368)Instructions burned: 4 (million)
% 7.37/1.90 % (3998370)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4178070546:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 7.37/1.90 % (3998372)Instruction limit reached!
% 7.37/1.90 % (3998372)------------------------------
% 7.37/1.90 % (3998372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/1.90 % (3998372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.90 % (3998372)CaDiCaL version: 2.1.3
% 7.37/1.90 % (3998372)Termination reason: Instruction limit
% 7.37/1.90 % (3998372)Termination phase: Saturation
% 7.37/1.90 % (3998372)Time elapsed: 0.078 s
% 7.37/1.90 % (3998372)Peak memory usage: 117 MB
% 7.37/1.90 % (3998372)Instructions burned: 53 (million)
% 7.37/1.90 % (3998383)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=159028471:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 7.37/1.90 % (3998383)Instruction limit reached!
% 7.37/1.90 % (3998383)------------------------------
% 7.37/1.90 % (3998383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/1.90 % (3998383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/1.90 % (3998383)CaDiCaL version: 2.1.3
% 7.37/1.90 % (3998383)Termination reason: Instruction limit
% 7.37/1.90 % (3998383)Termination phase: Preprocessing 2
% 7.37/1.90 % (3998383)Time elapsed: 0.002 s
% 7.37/1.90 % (3998383)Peak memory usage: 86 MB
% 7.37/1.90 % (3998383)Instructions burned: 3 (million)
% 7.37/1.90 % (3998382)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=50384930:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 10.19/2.25 % (3998382)Instruction limit reached!
% 10.19/2.25 % (3998382)------------------------------
% 10.19/2.25 % (3998382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.25 % (3998382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.25 % (3998382)CaDiCaL version: 2.1.3
% 10.19/2.25 % (3998382)Termination reason: Instruction limit
% 10.19/2.25 % (3998382)Termination phase: Property scanning
% 10.19/2.25 % (3998382)Time elapsed: 0.008 s
% 10.19/2.25 % (3998382)Peak memory usage: 86 MB
% 10.19/2.25 % (3998382)Instructions burned: 9 (million)
% 10.19/2.25 % (3998364)Instruction limit reached!
% 10.19/2.25 % (3998364)------------------------------
% 10.19/2.25 % (3998364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.25 % (3998364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.25 % (3998364)CaDiCaL version: 2.1.3
% 10.19/2.25 % (3998364)Termination reason: Instruction limit
% 10.19/2.25 % (3998364)Termination phase: Saturation
% 10.19/2.25 % (3998364)Time elapsed: 0.165 s
% 10.19/2.25 % (3998364)Peak memory usage: 90 MB
% 10.19/2.25 % (3998364)Instructions burned: 181 (million)
% 10.19/2.25 % (3998386)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3157141243:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 10.19/2.25 % (3998370)Instruction limit reached!
% 10.19/2.25 % (3998370)------------------------------
% 10.19/2.25 % (3998370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.25 % (3998370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.25 % (3998370)CaDiCaL version: 2.1.3
% 10.19/2.25 % (3998370)Termination reason: Instruction limit
% 10.19/2.25 % (3998370)Termination phase: Saturation
% 10.19/2.25 % (3998370)Time elapsed: 0.124 s
% 10.19/2.25 % (3998370)Peak memory usage: 134 MB
% 10.19/2.25 % (3998370)Instructions burned: 66 (million)
% 10.19/2.25 % (3998386)Instruction limit reached!
% 10.19/2.25 % (3998386)------------------------------
% 10.19/2.25 % (3998386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.25 % (3998386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.25 % (3998386)CaDiCaL version: 2.1.3
% 10.19/2.25 % (3998386)Termination reason: Instruction limit
% 10.19/2.25 % (3998386)Termination phase: Property scanning
% 10.19/2.25 % (3998386)Time elapsed: 0.002 s
% 10.19/2.25 % (3998386)Peak memory usage: 85 MB
% 10.19/2.25 % (3998386)Instructions burned: 2 (million)
% 10.19/2.25 % (3998392)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=41605407:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 10.19/2.25 % (3998398)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=396513327:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 10.19/2.25 % (3998398)Refutation not found, incomplete strategy
% 10.19/2.25 % (3998398)------------------------------
% 10.19/2.25 % (3998398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.25 % (3998398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.25 % (3998398)CaDiCaL version: 2.1.3
% 10.19/2.25 % (3998398)Termination reason: Refutation not found, incomplete strategy
% 10.19/2.25 % (3998398)Time elapsed: 0.017 s
% 10.19/2.25 % (3998398)Peak memory usage: 89 MB
% 10.19/2.25 % (3998398)Instructions burned: 17 (million)
% 10.19/2.25 % (3998396)dis+10_1_si=on:random_seed=3771129174:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.19/2.25 % (3998396)Instruction limit reached!
% 10.19/2.25 % (3998396)------------------------------
% 10.19/2.25 % (3998396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.25 % (3998396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.25 % (3998396)CaDiCaL version: 2.1.3
% 10.19/2.25 % (3998396)Termination reason: Instruction limit
% 10.19/2.25 % (3998396)Termination phase: Property scanning
% 10.19/2.25 % (3998396)Time elapsed: 0.010 s
% 10.19/2.25 % (3998396)Peak memory usage: 87 MB
% 10.19/2.25 % (3998396)Instructions burned: 10 (million)
% 10.19/2.25 % (3998408)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3094547990:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 10.19/2.25 % (3998408)Instruction limit reached!
% 10.19/2.25 % (3998408)------------------------------
% 11.51/2.56 % (3998408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.51/2.56 % (3998408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.51/2.56 % (3998408)CaDiCaL version: 2.1.3
% 11.51/2.56 % (3998408)Termination reason: Instruction limit
% 11.51/2.56 % (3998408)Termination phase: Function definition elimination
% 11.51/2.56 % (3998408)Time elapsed: 0.005 s
% 11.51/2.56 % (3998408)Peak memory usage: 86 MB
% 11.51/2.56 % (3998408)Instructions burned: 8 (million)
% 11.51/2.56 % (3998402)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1259892437: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_2992 on theBenchmark for (2992ds/35Mi)
% 11.51/2.56 % (3998409)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1444423604:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 11.51/2.56 % (3998404)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1280039856:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.51/2.56 % (3998404)Instruction limit reached!
% 11.51/2.56 % (3998404)------------------------------
% 11.51/2.56 % (3998404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.51/2.56 % (3998404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.51/2.56 % (3998404)CaDiCaL version: 2.1.3
% 11.51/2.56 % (3998404)Termination reason: Instruction limit
% 11.51/2.56 % (3998404)Termination phase: Property scanning
% 11.51/2.56 % (3998404)Time elapsed: 0.002 s
% 11.51/2.56 % (3998404)Peak memory usage: 85 MB
% 11.51/2.56 % (3998404)Instructions burned: 2 (million)
% 11.51/2.56 % (3998402)Instruction limit reached!
% 11.51/2.56 % (3998402)------------------------------
% 11.51/2.56 % (3998402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.51/2.56 % (3998402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.51/2.56 % (3998402)CaDiCaL version: 2.1.3
% 11.51/2.56 % (3998402)Termination reason: Instruction limit
% 11.51/2.56 % (3998402)Termination phase: Saturation
% 11.51/2.56 % (3998402)Time elapsed: 0.035 s
% 11.51/2.56 % (3998402)Peak memory usage: 89 MB
% 11.51/2.56 % (3998402)Instructions burned: 36 (million)
% 11.51/2.56 % (3998392)Instruction limit reached!
% 11.51/2.56 % (3998392)------------------------------
% 11.51/2.56 % (3998392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.51/2.56 % (3998392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.51/2.56 % (3998392)CaDiCaL version: 2.1.3
% 11.51/2.56 % (3998392)Termination reason: Instruction limit
% 11.51/2.56 % (3998392)Termination phase: Saturation
% 11.51/2.56 % (3998392)Time elapsed: 0.158 s
% 11.51/2.56 % (3998392)Peak memory usage: 119 MB
% 11.51/2.56 % (3998392)Instructions burned: 127 (million)
% 11.51/2.56 % (3998409)Instruction limit reached!
% 11.51/2.56 % (3998409)------------------------------
% 11.51/2.56 % (3998409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.51/2.56 % (3998409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.51/2.56 % (3998409)CaDiCaL version: 2.1.3
% 11.51/2.56 % (3998409)Termination reason: Instruction limit
% 11.51/2.56 % (3998409)Termination phase: Saturation
% 11.51/2.56 % (3998409)Time elapsed: 0.156 s
% 11.51/2.56 % (3998409)Peak memory usage: 92 MB
% 11.51/2.56 % (3998409)Instructions burned: 372 (million)
% 11.51/2.56 % (3998429)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1586292179:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi)
% 11.51/2.56 % (3998416)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1612267532:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 11.51/2.56 % (3998421)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=235079045:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 11.51/2.56 % (3998416)Instruction limit reached!
% 11.51/2.56 % (3998416)------------------------------
% 11.51/2.56 % (3998416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.51/2.56 % (3998416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.51/2.56 % (3998416)CaDiCaL version: 2.1.3
% 11.51/2.56 % (3998416)Termination reason: Instruction limit
% 11.51/2.56 % (3998416)Termination phase: Saturation
% 14.41/2.96 % (3998416)Time elapsed: 0.023 s
% 14.41/2.96 % (3998416)Peak memory usage: 94 MB
% 14.41/2.96 % (3998416)Instructions burned: 13 (million)
% 14.41/2.96 % (3998427)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3675769645:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 14.41/2.96 % (3998427)Instruction limit reached!
% 14.41/2.96 % (3998427)------------------------------
% 14.41/2.96 % (3998427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.41/2.96 % (3998427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.41/2.96 % (3998427)CaDiCaL version: 2.1.3
% 14.41/2.96 % (3998427)Termination reason: Instruction limit
% 14.41/2.96 % (3998427)Termination phase: Saturation
% 14.41/2.96 % (3998427)Time elapsed: 0.010 s
% 14.41/2.96 % (3998427)Peak memory usage: 88 MB
% 14.41/2.96 % (3998427)Instructions burned: 11 (million)
% 14.41/2.96 % (3998432)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=77480119:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 14.41/2.96 % (3998435)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=779171269:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi)
% 14.41/2.96 % (3998398)------------------------------
% 14.41/2.96 % (3998398)------------------------------
% 14.41/2.96 % (3998429)Instruction limit reached!
% 14.41/2.96 % (3998429)------------------------------
% 14.41/2.96 % (3998429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.41/2.96 % (3998429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.41/2.96 % (3998429)CaDiCaL version: 2.1.3
% 14.41/2.96 % (3998429)Termination reason: Instruction limit
% 14.41/2.96 % (3998429)Termination phase: Saturation
% 14.41/2.96 % (3998429)Time elapsed: 0.124 s
% 14.41/2.96 % (3998429)Peak memory usage: 133 MB
% 14.41/2.96 % (3998429)Instructions burned: 71 (million)
% 14.41/2.96 % (3998432)Instruction limit reached!
% 14.41/2.96 % (3998432)------------------------------
% 14.41/2.96 % (3998432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.41/2.96 % (3998432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.41/2.96 % (3998432)CaDiCaL version: 2.1.3
% 14.41/2.96 % (3998432)Termination reason: Instruction limit
% 14.41/2.96 % (3998432)Termination phase: Saturation
% 14.41/2.96 % (3998432)Time elapsed: 0.083 s
% 14.41/2.96 % (3998432)Peak memory usage: 90 MB
% 14.41/2.96 % (3998432)Instructions burned: 75 (million)
% 14.41/2.96 % (3998435)Instruction limit reached!
% 14.41/2.96 % (3998435)------------------------------
% 14.41/2.96 % (3998435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.41/2.96 % (3998435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.41/2.96 % (3998435)CaDiCaL version: 2.1.3
% 14.41/2.96 % (3998435)Termination reason: Instruction limit
% 14.41/2.96 % (3998435)Termination phase: Saturation
% 14.41/2.96 % (3998435)Time elapsed: 0.133 s
% 14.41/2.96 % (3998435)Peak memory usage: 91 MB
% 14.41/2.96 % (3998435)Instructions burned: 295 (million)
% 14.41/2.96 % (3998442)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=939057736:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi)
% 14.41/2.96 % (3998439)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2691194015:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi)
% 14.41/2.96 % (3998421)Instruction limit reached!
% 14.41/2.96 % (3998421)------------------------------
% 14.41/2.96 % (3998421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.41/2.96 % (3998421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.41/2.96 % (3998421)CaDiCaL version: 2.1.3
% 14.41/2.96 % (3998421)Termination reason: Instruction limit
% 14.41/2.96 % (3998421)Termination phase: Saturation
% 14.41/2.96 % (3998421)Time elapsed: 0.275 s
% 14.41/2.96 % (3998421)Peak memory usage: 118 MB
% 14.41/2.96 % (3998421)Instructions burned: 227 (million)
% 14.41/2.96 % (3998452)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1503062426:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi)
% 14.41/2.96 % (3998450)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1881058211:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi)
% 14.41/2.96 % (3998453)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2772596926:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/598Mi)
% 18.39/3.43 % (3998456)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1226978626:i=131:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 18.39/3.43 % (3998439)Instruction limit reached!
% 18.39/3.43 % (3998439)------------------------------
% 18.39/3.43 % (3998439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/3.43 % (3998439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.43 % (3998439)CaDiCaL version: 2.1.3
% 18.39/3.43 % (3998439)Termination reason: Instruction limit
% 18.39/3.43 % (3998439)Termination phase: Saturation
% 18.39/3.43 % (3998439)Time elapsed: 0.170 s
% 18.39/3.43 % (3998439)Peak memory usage: 117 MB
% 18.39/3.43 % (3998439)Instructions burned: 130 (million)
% 18.39/3.43 % (3998450)Instruction limit reached!
% 18.39/3.43 % (3998450)------------------------------
% 18.39/3.43 % (3998450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/3.43 % (3998450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.43 % (3998450)CaDiCaL version: 2.1.3
% 18.39/3.43 % (3998450)Termination reason: Instruction limit
% 18.39/3.43 % (3998450)Termination phase: Saturation
% 18.39/3.43 % (3998450)Time elapsed: 0.100 s
% 18.39/3.43 % (3998450)Peak memory usage: 134 MB
% 18.39/3.43 % (3998450)Instructions burned: 40 (million)
% 18.39/3.43 % (3998442)Instruction limit reached!
% 18.39/3.43 % (3998442)------------------------------
% 18.39/3.43 % (3998442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/3.43 % (3998442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.43 % (3998442)CaDiCaL version: 2.1.3
% 18.39/3.43 % (3998442)Termination reason: Instruction limit
% 18.39/3.43 % (3998442)Termination phase: Saturation
% 18.39/3.43 % (3998442)Time elapsed: 0.200 s
% 18.39/3.43 % (3998442)Peak memory usage: 134 MB
% 18.39/3.43 % (3998442)Instructions burned: 131 (million)
% 18.39/3.43 % (3998456)Instruction limit reached!
% 18.39/3.43 % (3998456)------------------------------
% 18.39/3.43 % (3998456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/3.43 % (3998456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.43 % (3998456)CaDiCaL version: 2.1.3
% 18.39/3.43 % (3998456)Termination reason: Instruction limit
% 18.39/3.43 % (3998456)Termination phase: Saturation
% 18.39/3.43 % (3998456)Time elapsed: 0.095 s
% 18.39/3.43 % (3998456)Peak memory usage: 117 MB
% 18.39/3.43 % (3998456)Instructions burned: 131 (million)
% 18.39/3.43 % (3998459)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=1260945969:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2985 on theBenchmark for (2985ds/259Mi)
% 18.39/3.43 % (3998470)dis+10_1_si=on:random_seed=2884020366:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi)
% 18.39/3.43 % (3998471)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2909980211:i=383:fsr=off:rtra=on:ev=force_2984 on theBenchmark for (2984ds/383Mi)
% 18.39/3.43 % (3998452)Instruction limit reached!
% 18.39/3.43 % (3998452)------------------------------
% 18.39/3.43 % (3998452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/3.43 % (3998452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.43 % (3998452)CaDiCaL version: 2.1.3
% 18.39/3.43 % (3998452)Termination reason: Instruction limit
% 18.39/3.43 % (3998452)Termination phase: Saturation
% 18.39/3.43 % (3998452)Time elapsed: 0.283 s
% 18.39/3.43 % (3998452)Peak memory usage: 92 MB
% 18.39/3.43 % (3998452)Instructions burned: 308 (million)
% 18.39/3.43 % (3998475)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2772371447:i=65:nm=16:rtra=on_2983 on theBenchmark for (2983ds/65Mi)
% 18.39/3.43 % (3998474)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1778471977:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi)
% 18.39/3.43 % (3998475)Instruction limit reached!
% 18.39/3.43 % (3998475)------------------------------
% 18.39/3.43 % (3998475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/3.43 % (3998475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998475)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998475)Termination reason: Instruction limit
% 19.91/3.83 % (3998475)Termination phase: Saturation
% 19.91/3.83 % (3998475)Time elapsed: 0.048 s
% 19.91/3.83 % (3998475)Peak memory usage: 116 MB
% 19.91/3.83 % (3998475)Instructions burned: 65 (million)
% 19.91/3.83 % (3998459)Instruction limit reached!
% 19.91/3.83 % (3998459)------------------------------
% 19.91/3.83 % (3998459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.83 % (3998459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998459)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998459)Termination reason: Instruction limit
% 19.91/3.83 % (3998459)Termination phase: Saturation
% 19.91/3.83 % (3998459)Time elapsed: 0.289 s
% 19.91/3.83 % (3998459)Peak memory usage: 117 MB
% 19.91/3.83 % (3998459)Instructions burned: 259 (million)
% 19.91/3.83 % (3998474)Instruction limit reached!
% 19.91/3.83 % (3998474)------------------------------
% 19.91/3.83 % (3998474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.83 % (3998474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998474)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998474)Termination reason: Instruction limit
% 19.91/3.83 % (3998474)Termination phase: Saturation
% 19.91/3.83 % (3998474)Time elapsed: 0.150 s
% 19.91/3.83 % (3998474)Peak memory usage: 91 MB
% 19.91/3.83 % (3998474)Instructions burned: 141 (million)
% 19.91/3.83 % (3998488)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=658935150:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi)
% 19.91/3.83 % (3998481)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1414234970:i=121:nm=16:rtra=on_2982 on theBenchmark for (2982ds/121Mi)
% 19.91/3.83 % (3998453)Instruction limit reached!
% 19.91/3.83 % (3998453)------------------------------
% 19.91/3.83 % (3998453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.83 % (3998453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998453)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998453)Termination reason: Instruction limit
% 19.91/3.83 % (3998453)Termination phase: Saturation
% 19.91/3.83 % (3998453)Time elapsed: 0.524 s
% 19.91/3.83 % (3998453)Peak memory usage: 139 MB
% 19.91/3.83 % (3998453)Instructions burned: 598 (million)
% 19.91/3.83 % (3998471)Instruction limit reached!
% 19.91/3.83 % (3998471)------------------------------
% 19.91/3.83 % (3998471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.83 % (3998471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998471)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998471)Termination reason: Instruction limit
% 19.91/3.83 % (3998471)Termination phase: Saturation
% 19.91/3.83 % (3998471)Time elapsed: 0.310 s
% 19.91/3.83 % (3998471)Peak memory usage: 92 MB
% 19.91/3.83 % (3998471)Instructions burned: 383 (million)
% 19.91/3.83 % (3998488)Instruction limit reached!
% 19.91/3.83 % (3998488)------------------------------
% 19.91/3.83 % (3998488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.83 % (3998488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998488)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998488)Termination reason: Instruction limit
% 19.91/3.83 % (3998488)Termination phase: Saturation
% 19.91/3.83 % (3998488)Time elapsed: 0.088 s
% 19.91/3.83 % (3998488)Peak memory usage: 119 MB
% 19.91/3.83 % (3998488)Instructions burned: 130 (million)
% 19.91/3.83 % (3998481)Instruction limit reached!
% 19.91/3.83 % (3998481)------------------------------
% 19.91/3.83 % (3998481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.83 % (3998481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.83 % (3998481)CaDiCaL version: 2.1.3
% 19.91/3.83 % (3998481)Termination reason: Instruction limit
% 19.91/3.83 % (3998481)Termination phase: Saturation
% 19.91/3.83 % (3998481)Time elapsed: 0.121 s
% 19.91/3.83 % (3998481)Peak memory usage: 90 MB
% 19.91/3.83 % (3998481)Instructions burned: 121 (million)
% 19.91/3.83 % (3998491)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=3472040669:i=39:ins=3:rtra=on_2980 on theBenchmark for (2980ds/39Mi)
% 19.91/3.83 % (3998492)dis+1010_1_to=kbo:si=on:random_seed=3808060603:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2980 on theBenchmark for (2980ds/175Mi)
% 19.91/3.83 % (3998491)Instruction limit reached!
% 24.11/4.20 % (3998491)------------------------------
% 24.11/4.20 % (3998491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.11/4.20 % (3998491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.11/4.20 % (3998491)CaDiCaL version: 2.1.3
% 24.11/4.20 % (3998491)Termination reason: Instruction limit
% 24.11/4.20 % (3998491)Termination phase: Saturation
% 24.11/4.20 % (3998491)Time elapsed: 0.071 s
% 24.11/4.20 % (3998491)Peak memory usage: 116 MB
% 24.11/4.20 % (3998491)Instructions burned: 39 (million)
% 24.11/4.20 % (3998500)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=578512917:s2a=on:i=483:doe=on:nm=32:rtra=on_2979 on theBenchmark for (2979ds/483Mi)
% 24.11/4.20 % (3998499)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3190323764:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/329Mi)
% 24.11/4.20 % (3998504)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3327893443:i=349:rtra=on_2978 on theBenchmark for (2978ds/349Mi)
% 24.11/4.20 % (3998501)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1032463490:thitd=on:i=215:nm=0:rtra=on:ev=force_2979 on theBenchmark for (2979ds/215Mi)
% 24.11/4.20 % (3998492)Instruction limit reached!
% 24.11/4.20 % (3998492)------------------------------
% 24.11/4.20 % (3998492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.11/4.20 % (3998492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.11/4.20 % (3998492)CaDiCaL version: 2.1.3
% 24.11/4.20 % (3998492)Termination reason: Instruction limit
% 24.11/4.20 % (3998492)Termination phase: Saturation
% 24.11/4.20 % (3998492)Time elapsed: 0.191 s
% 24.11/4.20 % (3998492)Peak memory usage: 91 MB
% 24.11/4.20 % (3998492)Instructions burned: 175 (million)
% 24.11/4.20 % (3998504)Instruction limit reached!
% 24.11/4.20 % (3998504)------------------------------
% 24.11/4.20 % (3998504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.11/4.20 % (3998504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.11/4.20 % (3998504)CaDiCaL version: 2.1.3
% 24.11/4.20 % (3998504)Termination reason: Instruction limit
% 24.11/4.20 % (3998504)Termination phase: Saturation
% 24.11/4.20 % (3998504)Time elapsed: 0.142 s
% 24.11/4.20 % (3998504)Peak memory usage: 116 MB
% 24.11/4.20 % (3998504)Instructions burned: 351 (million)
% 24.11/4.20 % (3998510)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=807649977:st=2:i=295:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/295Mi)
% 24.11/4.20 % (3998499)Instruction limit reached!
% 24.11/4.20 % (3998499)------------------------------
% 24.11/4.20 % (3998499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.11/4.20 % (3998499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.11/4.20 % (3998499)CaDiCaL version: 2.1.3
% 24.11/4.20 % (3998499)Termination reason: Instruction limit
% 24.11/4.20 % (3998499)Termination phase: Saturation
% 24.11/4.20 % (3998499)Time elapsed: 0.239 s
% 24.11/4.20 % (3998499)Peak memory usage: 117 MB
% 24.11/4.20 % (3998499)Instructions burned: 331 (million)
% 24.11/4.20 % (3998501)Instruction limit reached!
% 24.11/4.20 % (3998501)------------------------------
% 24.11/4.20 % (3998501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.11/4.20 % (3998501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.11/4.20 % (3998501)CaDiCaL version: 2.1.3
% 24.11/4.20 % (3998501)Termination reason: Instruction limit
% 24.11/4.20 % (3998501)Termination phase: Saturation
% 24.11/4.20 % (3998501)Time elapsed: 0.274 s
% 24.11/4.20 % (3998501)Peak memory usage: 136 MB
% 24.11/4.20 % (3998501)Instructions burned: 215 (million)
% 24.11/4.20 % (3998521)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2900663713:i=281:gtgl=2:rtra=on:gtg=all_2975 on theBenchmark for (2975ds/281Mi)
% 24.11/4.20 % (3998520)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1391357857:i=328:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/328Mi)
% 24.11/4.20 % (3998470)Instruction limit reached!
% 24.11/4.20 % (3998470)------------------------------
% 24.11/4.20 % (3998470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.11/4.20 % (3998470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.85/4.44 % (3998470)CaDiCaL version: 2.1.3
% 24.85/4.44 % (3998470)Termination reason: Instruction limit
% 24.85/4.44 % (3998470)Termination phase: Saturation
% 24.85/4.44 % (3998470)Time elapsed: 0.970 s
% 24.85/4.44 % (3998470)Peak memory usage: 96 MB
% 24.85/4.44 % (3998470)Instructions burned: 1000 (million)
% 24.85/4.44 % (3998524)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1125835292:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/484Mi)
% 24.85/4.44 % (3998521)Instruction limit reached!
% 24.85/4.44 % (3998521)------------------------------
% 24.85/4.44 % (3998521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.85/4.44 % (3998521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.85/4.44 % (3998521)CaDiCaL version: 2.1.3
% 24.85/4.44 % (3998521)Termination reason: Instruction limit
% 24.85/4.44 % (3998521)Termination phase: Saturation
% 24.85/4.44 % (3998521)Time elapsed: 0.142 s
% 24.85/4.44 % (3998521)Peak memory usage: 118 MB
% 24.85/4.44 % (3998521)Instructions burned: 282 (million)
% 24.85/4.44 % (3998510)Instruction limit reached!
% 24.85/4.44 % (3998510)------------------------------
% 24.85/4.44 % (3998510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.85/4.44 % (3998510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.85/4.44 % (3998510)CaDiCaL version: 2.1.3
% 24.85/4.44 % (3998510)Termination reason: Instruction limit
% 24.85/4.44 % (3998510)Termination phase: Saturation
% 24.85/4.44 % (3998510)Time elapsed: 0.288 s
% 24.85/4.44 % (3998510)Peak memory usage: 91 MB
% 24.85/4.44 % (3998510)Instructions burned: 296 (million)
% 24.85/4.44 % (3998529)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=140588590:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2974 on theBenchmark for (2974ds/321Mi)
% 24.85/4.44 % (3998500)Instruction limit reached!
% 24.85/4.44 % (3998500)------------------------------
% 24.85/4.44 % (3998500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.85/4.44 % (3998500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.85/4.44 % (3998500)CaDiCaL version: 2.1.3
% 24.85/4.44 % (3998500)Termination reason: Instruction limit
% 24.85/4.44 % (3998500)Termination phase: Saturation
% 24.85/4.44 % (3998500)Time elapsed: 0.559 s
% 24.85/4.44 % (3998500)Peak memory usage: 136 MB
% 24.85/4.44 % (3998500)Instructions burned: 483 (million)
% 24.85/4.44 % (3998534)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2781580543:i=416:rtra=on:gtg=position:ss=axioms_2972 on theBenchmark for (2972ds/416Mi)
% 24.85/4.44 % (3998535)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4179047990:i=471:thf=on:kws=precedence:rtra=on_2972 on theBenchmark for (2972ds/471Mi)
% 24.85/4.44 % (3998529)Instruction limit reached!
% 24.85/4.44 % (3998529)------------------------------
% 24.85/4.44 % (3998529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.85/4.44 % (3998529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.85/4.44 % (3998529)CaDiCaL version: 2.1.3
% 24.85/4.44 % (3998529)Termination reason: Instruction limit
% 24.85/4.44 % (3998529)Termination phase: Saturation
% 24.85/4.44 % (3998529)Time elapsed: 0.177 s
% 24.85/4.44 % (3998529)Peak memory usage: 113 MB
% 24.85/4.44 % (3998529)Instructions burned: 322 (million)
% 24.85/4.44 % (3998520)Instruction limit reached!
% 24.85/4.44 % (3998520)------------------------------
% 24.85/4.44 % (3998520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.85/4.44 % (3998520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.85/4.44 % (3998520)CaDiCaL version: 2.1.3
% 24.85/4.44 % (3998520)Termination reason: Instruction limit
% 24.85/4.44 % (3998520)Termination phase: Saturation
% 24.85/4.44 % (3998520)Time elapsed: 0.355 s
% 24.85/4.44 % (3998520)Peak memory usage: 118 MB
% 24.85/4.44 % (3998520)Instructions burned: 328 (million)
% 24.85/4.44 % (3998538)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=2611748002:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi)
% 24.85/4.44 % (3998540)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3132174451:i=375:kws=inv_arity_squared:rtra=on_2971 on theBenchmark for (2971ds/375Mi)
% 24.85/4.44 % (3998545)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1341262719:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/387Mi)
% 27.01/4.89 % (3998550)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3221239860:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2970 on theBenchmark for (2970ds/513Mi)
% 27.01/4.89 % (3998524)Instruction limit reached!
% 27.01/4.89 % (3998524)------------------------------
% 27.01/4.89 % (3998524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.01/4.89 % (3998524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.01/4.89 % (3998524)CaDiCaL version: 2.1.3
% 27.01/4.89 % (3998524)Termination reason: Instruction limit
% 27.01/4.89 % (3998524)Termination phase: Saturation
% 27.01/4.89 % (3998524)Time elapsed: 0.472 s
% 27.01/4.89 % (3998524)Peak memory usage: 95 MB
% 27.01/4.89 % (3998524)Instructions burned: 485 (million)
% 27.01/4.89 % (3998535)Instruction limit reached!
% 27.01/4.89 % (3998535)------------------------------
% 27.01/4.89 % (3998535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.01/4.89 % (3998535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.01/4.89 % (3998535)CaDiCaL version: 2.1.3
% 27.01/4.89 % (3998535)Termination reason: Instruction limit
% 27.01/4.89 % (3998535)Termination phase: Saturation
% 27.01/4.89 % (3998535)Time elapsed: 0.376 s
% 27.01/4.89 % (3998535)Peak memory usage: 119 MB
% 27.01/4.89 % (3998535)Instructions burned: 471 (million)
% 27.01/4.89 % (3998538)Instruction limit reached!
% 27.01/4.89 % (3998538)------------------------------
% 27.01/4.89 % (3998538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.01/4.89 % (3998538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.01/4.89 % (3998538)CaDiCaL version: 2.1.3
% 27.01/4.89 % (3998538)Termination reason: Instruction limit
% 27.01/4.89 % (3998538)Termination phase: Saturation
% 27.01/4.89 % (3998538)Time elapsed: 0.354 s
% 27.01/4.89 % (3998538)Peak memory usage: 135 MB
% 27.01/4.89 % (3998538)Instructions burned: 276 (million)
% 27.01/4.89 % (3998534)Instruction limit reached!
% 27.01/4.89 % (3998534)------------------------------
% 27.01/4.89 % (3998534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.01/4.89 % (3998534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.01/4.89 % (3998534)CaDiCaL version: 2.1.3
% 27.01/4.89 % (3998534)Termination reason: Instruction limit
% 27.01/4.89 % (3998534)Termination phase: Saturation
% 27.01/4.89 % (3998534)Time elapsed: 0.432 s
% 27.01/4.89 % (3998534)Peak memory usage: 119 MB
% 27.01/4.89 % (3998534)Instructions burned: 416 (million)
% 27.01/4.89 % (3998545)Instruction limit reached!
% 27.01/4.89 % (3998545)------------------------------
% 27.01/4.89 % (3998545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.01/4.89 % (3998545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.01/4.89 % (3998545)CaDiCaL version: 2.1.3
% 27.01/4.89 % (3998545)Termination reason: Instruction limit
% 27.01/4.89 % (3998545)Termination phase: Saturation
% 27.01/4.89 % (3998545)Time elapsed: 0.238 s
% 27.01/4.89 % (3998545)Peak memory usage: 119 MB
% 27.01/4.89 % (3998545)Instructions burned: 387 (million)
% 27.01/4.89 % (3998540)Instruction limit reached!
% 27.01/4.89 % (3998540)------------------------------
% 27.01/4.89 % (3998540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.01/4.89 % (3998540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.01/4.89 % (3998540)CaDiCaL version: 2.1.3
% 27.01/4.89 % (3998540)Termination reason: Instruction limit
% 27.01/4.89 % (3998540)Termination phase: Saturation
% 27.01/4.89 % (3998540)Time elapsed: 0.372 s
% 27.01/4.89 % (3998540)Peak memory usage: 119 MB
% 27.01/4.89 % (3998540)Instructions burned: 375 (million)
% 27.01/4.89 % (3998558)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4264514116:i=334:rtra=on_2968 on theBenchmark for (2968ds/334Mi)
% 27.01/4.89 % (3998562)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2040038914:i=359:rtra=on:gtg=exists_top:ss=axioms_2966 on theBenchmark for (2966ds/359Mi)
% 27.01/4.89 % (3998566)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=2250070553:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2966 on theBenchmark for (2966ds/235Mi)
% 27.01/4.89 % (3998564)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2651667294:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2966 on theBenchmark for (2966ds/341Mi)
% 31.49/5.28 % (3998565)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1500612971:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2966 on theBenchmark for (2966ds/261Mi)
% 31.49/5.28 % (3998568)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3392286018:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2965 on theBenchmark for (2965ds/273Mi)
% 31.49/5.28 % (3998566)Instruction limit reached!
% 31.49/5.28 % (3998566)------------------------------
% 31.49/5.28 % (3998566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.28 % (3998566)CaDiCaL version: 2.1.3
% 31.49/5.28 % (3998566)Termination reason: Instruction limit
% 31.49/5.28 % (3998566)Termination phase: Saturation
% 31.49/5.28 % (3998566)Time elapsed: 0.099 s
% 31.49/5.28 % (3998566)Peak memory usage: 117 MB
% 31.49/5.28 % (3998566)Instructions burned: 237 (million)
% 31.49/5.28 % (3998575)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4241087297:i=146:doe=on:rtra=on_2964 on theBenchmark for (2964ds/146Mi)
% 31.49/5.28 % (3998550)Instruction limit reached!
% 31.49/5.28 % (3998550)------------------------------
% 31.49/5.28 % (3998550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.28 % (3998550)CaDiCaL version: 2.1.3
% 31.49/5.28 % (3998550)Termination reason: Instruction limit
% 31.49/5.28 % (3998550)Termination phase: Saturation
% 31.49/5.28 % (3998550)Time elapsed: 0.497 s
% 31.49/5.28 % (3998550)Peak memory usage: 93 MB
% 31.49/5.28 % (3998550)Instructions burned: 514 (million)
% 31.49/5.28 % (3998565)Instruction limit reached!
% 31.49/5.28 % (3998565)------------------------------
% 31.49/5.28 % (3998565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.28 % (3998565)CaDiCaL version: 2.1.3
% 31.49/5.28 % (3998565)Termination reason: Instruction limit
% 31.49/5.28 % (3998565)Termination phase: Saturation
% 31.49/5.28 % (3998565)Time elapsed: 0.184 s
% 31.49/5.28 % (3998565)Peak memory usage: 118 MB
% 31.49/5.28 % (3998565)Instructions burned: 262 (million)
% 31.49/5.28 % (3998558)Instruction limit reached!
% 31.49/5.28 % (3998558)------------------------------
% 31.49/5.28 % (3998558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.28 % (3998558)CaDiCaL version: 2.1.3
% 31.49/5.28 % (3998558)Termination reason: Instruction limit
% 31.49/5.28 % (3998558)Termination phase: Saturation
% 31.49/5.28 % (3998558)Time elapsed: 0.280 s
% 31.49/5.28 % (3998558)Peak memory usage: 135 MB
% 31.49/5.28 % (3998558)Instructions burned: 334 (million)
% 31.49/5.28 % (3998562)Instruction limit reached!
% 31.49/5.28 % (3998562)------------------------------
% 31.49/5.28 % (3998562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.28 % (3998562)CaDiCaL version: 2.1.3
% 31.49/5.28 % (3998562)Termination reason: Instruction limit
% 31.49/5.28 % (3998562)Termination phase: Saturation
% 31.49/5.28 % (3998562)Time elapsed: 0.243 s
% 31.49/5.28 % (3998562)Peak memory usage: 92 MB
% 31.49/5.28 % (3998562)Instructions burned: 359 (million)
% 31.49/5.28 % (3998564)Instruction limit reached!
% 31.49/5.28 % (3998564)------------------------------
% 31.49/5.28 % (3998564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.49/5.28 % (3998564)CaDiCaL version: 2.1.3
% 31.49/5.28 % (3998564)Termination reason: Instruction limit
% 31.49/5.28 % (3998564)Termination phase: Saturation
% 31.49/5.28 % (3998564)Time elapsed: 0.231 s
% 31.49/5.28 % (3998564)Peak memory usage: 120 MB
% 31.49/5.28 % (3998564)Instructions burned: 341 (million)
% 31.49/5.28 % (3998575)Instruction limit reached!
% 31.49/5.28 % (3998575)------------------------------
% 31.49/5.28 % (3998575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.49/5.28 % (3998575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.64/5.70 % (3998575)CaDiCaL version: 2.1.3
% 33.64/5.70 % (3998575)Termination reason: Instruction limit
% 33.64/5.70 % (3998575)Termination phase: Saturation
% 33.64/5.70 % (3998575)Time elapsed: 0.053 s
% 33.64/5.70 % (3998575)Peak memory usage: 91 MB
% 33.64/5.70 % (3998575)Instructions burned: 148 (million)
% 33.64/5.70 % (3998568)Instruction limit reached!
% 33.64/5.70 % (3998568)------------------------------
% 33.64/5.70 % (3998568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.64/5.70 % (3998568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.64/5.70 % (3998568)CaDiCaL version: 2.1.3
% 33.64/5.70 % (3998568)Termination reason: Instruction limit
% 33.64/5.70 % (3998568)Termination phase: Saturation
% 33.64/5.70 % (3998568)Time elapsed: 0.190 s
% 33.64/5.70 % (3998568)Peak memory usage: 92 MB
% 33.64/5.70 % (3998568)Instructions burned: 274 (million)
% 33.64/5.70 % (3998582)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=735858983:i=107:rtra=on_2962 on theBenchmark for (2962ds/107Mi)
% 33.64/5.70 % (3998578)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=490835277:avsq=on:i=276:avsqr=1,2:rtra=on_2963 on theBenchmark for (2963ds/276Mi)
% 33.64/5.70 % (3998577)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=270234965:i=4428:doe=on:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/4428Mi)
% 33.64/5.70 % (3998580)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2800870195:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2962 on theBenchmark for (2962ds/655Mi)
% 33.64/5.70 % (3998581)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3288251011:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2962 on theBenchmark for (2962ds/1054Mi)
% 33.64/5.70 % (3998579)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4115615216:i=1052:rtra=on_2963 on theBenchmark for (2963ds/1052Mi)
% 33.64/5.70 % (3998582)Instruction limit reached!
% 33.64/5.70 % (3998582)------------------------------
% 33.64/5.70 % (3998582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.64/5.70 % (3998582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.64/5.70 % (3998582)CaDiCaL version: 2.1.3
% 33.64/5.70 % (3998582)Termination reason: Instruction limit
% 33.64/5.70 % (3998582)Termination phase: Saturation
% 33.64/5.70 % (3998582)Time elapsed: 0.049 s
% 33.64/5.70 % (3998582)Peak memory usage: 116 MB
% 33.64/5.70 % (3998582)Instructions burned: 108 (million)
% 33.64/5.70 % (3998583)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3419885817:s2a=on:i=450:doe=on:nm=32:rtra=on_2962 on theBenchmark for (2962ds/450Mi)
% 33.64/5.70 % (3998590)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
% 33.64/5.70 % (3998590)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3443292553:i=1090:aac=none:nm=0:rtra=on:rawr=on_2961 on theBenchmark for (2961ds/1090Mi)
% 33.64/5.70 % (3998578)Instruction limit reached!
% 33.64/5.70 % (3998578)------------------------------
% 33.64/5.70 % (3998578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.64/5.70 % (3998578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.64/5.70 % (3998578)CaDiCaL version: 2.1.3
% 33.64/5.70 % (3998578)Termination reason: Instruction limit
% 33.64/5.70 % (3998578)Termination phase: Saturation
% 33.64/5.70 % (3998578)Time elapsed: 0.230 s
% 33.64/5.70 % (3998578)Peak memory usage: 135 MB
% 33.64/5.70 % (3998578)Instructions burned: 278 (million)
% 33.64/5.70 % (3998580)Instruction limit reached!
% 33.64/5.70 % (3998580)------------------------------
% 33.64/5.70 % (3998580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.64/5.70 % (3998580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.64/5.70 % (3998580)CaDiCaL version: 2.1.3
% 33.64/5.70 % (3998580)Termination reason: Instruction limit
% 33.64/5.70 % (3998580)Termination phase: Saturation
% 33.64/5.70 % (3998580)Time elapsed: 0.255 s
% 33.64/5.70 % (3998580)Peak memory usage: 90 MB
% 33.64/5.70 % (3998580)Instructions burned: 655 (million)
% 33.64/5.70 % (3998594)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2675732905:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2959 on theBenchmark for (2959ds/130Mi)
% 38.42/6.18 % (3998583)Instruction limit reached!
% 38.42/6.18 % (3998583)------------------------------
% 38.42/6.18 % (3998583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.18 % (3998583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.18 % (3998583)CaDiCaL version: 2.1.3
% 38.42/6.18 % (3998583)Termination reason: Instruction limit
% 38.42/6.18 % (3998583)Termination phase: Saturation
% 38.42/6.18 % (3998583)Time elapsed: 0.323 s
% 38.42/6.18 % (3998583)Peak memory usage: 135 MB
% 38.42/6.18 % (3998583)Instructions burned: 451 (million)
% 38.42/6.18 % (3998581)Instruction limit reached!
% 38.42/6.18 % (3998581)------------------------------
% 38.42/6.18 % (3998581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.18 % (3998581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.18 % (3998581)CaDiCaL version: 2.1.3
% 38.42/6.18 % (3998581)Termination reason: Instruction limit
% 38.42/6.18 % (3998581)Termination phase: Saturation
% 38.42/6.18 % (3998581)Time elapsed: 0.362 s
% 38.42/6.18 % (3998581)Peak memory usage: 89 MB
% 38.42/6.18 % (3998581)Instructions burned: 1056 (million)
% 38.42/6.18 % (3998595)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4009248524:i=312:kws=inv_frequency:nm=20:rtra=on_2959 on theBenchmark for (2959ds/312Mi)
% 38.42/6.18 % (3998594)Instruction limit reached!
% 38.42/6.18 % (3998594)------------------------------
% 38.42/6.18 % (3998594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.18 % (3998594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.18 % (3998594)CaDiCaL version: 2.1.3
% 38.42/6.18 % (3998594)Termination reason: Instruction limit
% 38.42/6.18 % (3998594)Termination phase: Saturation
% 38.42/6.18 % (3998594)Time elapsed: 0.103 s
% 38.42/6.18 % (3998594)Peak memory usage: 117 MB
% 38.42/6.18 % (3998594)Instructions burned: 130 (million)
% 38.42/6.18 % (3998590)Instruction limit reached!
% 38.42/6.18 % (3998590)------------------------------
% 38.42/6.18 % (3998590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.18 % (3998590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.18 % (3998590)CaDiCaL version: 2.1.3
% 38.42/6.18 % (3998590)Termination reason: Instruction limit
% 38.42/6.18 % (3998590)Termination phase: Saturation
% 38.42/6.18 % (3998590)Time elapsed: 0.363 s
% 38.42/6.18 % (3998590)Peak memory usage: 122 MB
% 38.42/6.18 % (3998590)Instructions burned: 1093 (million)
% 38.42/6.18 % (3998613)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1084214852:i=491:doe=on:rtra=on:gtg=position_2958 on theBenchmark for (2958ds/491Mi)
% 38.42/6.18 % (3998615)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2849393600:s2a=on:i=835:s2at=2:rtra=on_2958 on theBenchmark for (2958ds/835Mi)
% 38.42/6.18 % (3998647)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2163260808:i=776:doe=on:rtra=on_2956 on theBenchmark for (2956ds/776Mi)
% 38.42/6.18 % (3998640)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2980251325:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2957 on theBenchmark for (2957ds/307Mi)
% 38.42/6.18 % (3998595)Instruction limit reached!
% 38.42/6.18 % (3998595)------------------------------
% 38.42/6.18 % (3998595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.18 % (3998595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.18 % (3998595)CaDiCaL version: 2.1.3
% 38.42/6.18 % (3998595)Termination reason: Instruction limit
% 38.42/6.18 % (3998595)Termination phase: Saturation
% 38.42/6.18 % (3998595)Time elapsed: 0.214 s
% 38.42/6.18 % (3998595)Peak memory usage: 118 MB
% 38.42/6.18 % (3998595)Instructions burned: 313 (million)
% 38.42/6.18 % (3998579)Instruction limit reached!
% 38.42/6.18 % (3998579)------------------------------
% 38.42/6.18 % (3998579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.18 % (3998579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.18 % (3998579)CaDiCaL version: 2.1.3
% 38.42/6.18 % (3998579)Termination reason: Instruction limit
% 38.42/6.18 % (3998579)Termination phase: Saturation
% 38.42/6.18 % (3998579)Time elapsed: 0.672 s
% 38.42/6.18 % (3998579)Peak memory usage: 94 MB
% 38.42/6.18 % (3998579)Instructions burned: 1053 (million)
% 38.42/6.18 % (3998682)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2433645604:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/646Mi)
% 45.57/7.16 % (3998640)Instruction limit reached!
% 45.57/7.16 % (3998640)------------------------------
% 45.57/7.16 % (3998640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.57/7.16 % (3998640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.57/7.16 % (3998640)CaDiCaL version: 2.1.3
% 45.57/7.16 % (3998640)Termination reason: Instruction limit
% 45.57/7.16 % (3998640)Termination phase: Saturation
% 45.57/7.16 % (3998640)Time elapsed: 0.212 s
% 45.57/7.16 % (3998640)Peak memory usage: 93 MB
% 45.57/7.16 % (3998640)Instructions burned: 308 (million)
% 45.57/7.16 % (3998613)Instruction limit reached!
% 45.57/7.16 % (3998613)------------------------------
% 45.57/7.16 % (3998613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.57/7.16 % (3998613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.57/7.16 % (3998613)CaDiCaL version: 2.1.3
% 45.57/7.16 % (3998613)Termination reason: Instruction limit
% 45.57/7.16 % (3998613)Termination phase: Saturation
% 45.57/7.16 % (3998613)Time elapsed: 0.319 s
% 45.57/7.16 % (3998613)Peak memory usage: 93 MB
% 45.57/7.16 % (3998613)Instructions burned: 492 (million)
% 45.57/7.16 % (3998647)Instruction limit reached!
% 45.57/7.16 % (3998647)------------------------------
% 45.57/7.16 % (3998647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.57/7.16 % (3998647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.57/7.16 % (3998647)CaDiCaL version: 2.1.3
% 45.57/7.16 % (3998647)Termination reason: Instruction limit
% 45.57/7.16 % (3998647)Termination phase: Saturation
% 45.57/7.16 % (3998647)Time elapsed: 0.251 s
% 45.57/7.16 % (3998647)Peak memory usage: 122 MB
% 45.57/7.16 % (3998647)Instructions burned: 777 (million)
% 45.57/7.16 % (3998698)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=4111264998:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2954 on theBenchmark for (2954ds/784Mi)
% 45.57/7.16 % (3998717)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3372501577:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2953 on theBenchmark for (2953ds/775Mi)
% 45.57/7.16 % (3998714)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=3753912355:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2953 on theBenchmark for (2953ds/1131Mi)
% 45.57/7.16 % (3998715)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=2343716243:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2953 on theBenchmark for (2953ds/246Mi)
% 45.57/7.16 % (3998615)Instruction limit reached!
% 45.57/7.16 % (3998615)------------------------------
% 45.57/7.16 % (3998615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.57/7.16 % (3998615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.57/7.16 % (3998615)CaDiCaL version: 2.1.3
% 45.57/7.16 % (3998615)Termination reason: Instruction limit
% 45.57/7.16 % (3998615)Termination phase: Saturation
% 45.57/7.16 % (3998615)Time elapsed: 0.551 s
% 45.57/7.16 % (3998615)Peak memory usage: 95 MB
% 45.57/7.16 % (3998615)Instructions burned: 835 (million)
% 45.57/7.16 % (3998715)Instruction limit reached!
% 45.57/7.16 % (3998715)------------------------------
% 45.57/7.16 % (3998715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.57/7.16 % (3998715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.57/7.16 % (3998715)CaDiCaL version: 2.1.3
% 45.57/7.16 % (3998715)Termination reason: Instruction limit
% 45.57/7.16 % (3998715)Termination phase: Saturation
% 45.57/7.16 % (3998715)Time elapsed: 0.186 s
% 45.57/7.16 % (3998715)Peak memory usage: 117 MB
% 45.57/7.16 % (3998715)Instructions burned: 246 (million)
% 45.57/7.16 % (3998717)Instruction limit reached!
% 45.57/7.16 % (3998717)------------------------------
% 45.57/7.16 % (3998717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.57/7.16 % (3998717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.57/7.16 % (3998717)CaDiCaL version: 2.1.3
% 45.57/7.16 % (3998717)Termination reason: Instruction limit
% 45.57/7.16 % (3998717)Termination phase: Saturation
% 45.57/7.16 % (3998717)Time elapsed: 0.244 s
% 56.03/8.93 % (3998717)Peak memory usage: 93 MB
% 56.03/8.93 % (3998717)Instructions burned: 778 (million)
% 56.03/8.93 % (3998682)Instruction limit reached!
% 56.03/8.93 % (3998682)------------------------------
% 56.03/8.93 % (3998682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.03/8.93 % (3998682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.03/8.93 % (3998682)CaDiCaL version: 2.1.3
% 56.03/8.93 % (3998682)Termination reason: Instruction limit
% 56.03/8.93 % (3998682)Termination phase: Saturation
% 56.03/8.93 % (3998682)Time elapsed: 0.427 s
% 56.03/8.93 % (3998682)Peak memory usage: 140 MB
% 56.03/8.93 % (3998682)Instructions burned: 646 (million)
% 56.03/8.93 % (3998768)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=951308710:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2951 on theBenchmark for (2951ds/273Mi)
% 56.03/8.93 % (3998770)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3459305041:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2950 on theBenchmark for (2950ds/1094Mi)
% 56.03/8.93 % (3998769)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1468319662:i=102:nm=16:rtra=on_2950 on theBenchmark for (2950ds/102Mi)
% 56.03/8.93 % (3998771)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=404895628:i=6400:doe=on:fsr=off:rtra=on_2950 on theBenchmark for (2950ds/6400Mi)
% 56.03/8.93 % (3998769)Instruction limit reached!
% 56.03/8.93 % (3998769)------------------------------
% 56.03/8.93 % (3998769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.03/8.93 % (3998769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.03/8.93 % (3998769)CaDiCaL version: 2.1.3
% 56.03/8.93 % (3998769)Termination reason: Instruction limit
% 56.03/8.93 % (3998769)Termination phase: Saturation
% 56.03/8.93 % (3998769)Time elapsed: 0.066 s
% 56.03/8.93 % (3998769)Peak memory usage: 89 MB
% 56.03/8.93 % (3998769)Instructions burned: 102 (million)
% 56.03/8.93 % (3998768)Instruction limit reached!
% 56.03/8.93 % (3998768)------------------------------
% 56.03/8.93 % (3998768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.03/8.93 % (3998768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.03/8.93 % (3998768)CaDiCaL version: 2.1.3
% 56.03/8.93 % (3998768)Termination reason: Instruction limit
% 56.03/8.93 % (3998768)Termination phase: Saturation
% 56.03/8.93 % (3998768)Time elapsed: 0.194 s
% 56.03/8.93 % (3998768)Peak memory usage: 92 MB
% 56.03/8.93 % (3998768)Instructions burned: 274 (million)
% 56.03/8.93 % (3998698)Instruction limit reached!
% 56.03/8.93 % (3998698)------------------------------
% 56.03/8.93 % (3998698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.03/8.93 % (3998698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.03/8.93 % (3998698)CaDiCaL version: 2.1.3
% 56.03/8.93 % (3998698)Termination reason: Instruction limit
% 56.03/8.93 % (3998698)Termination phase: Saturation
% 56.03/8.93 % (3998698)Time elapsed: 0.597 s
% 56.03/8.93 % (3998698)Peak memory usage: 121 MB
% 56.03/8.93 % (3998698)Instructions burned: 784 (million)
% 56.03/8.93 % (3998776)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=1623917391:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/868Mi)
% 56.03/8.93 % (3998770)Instruction limit reached!
% 56.03/8.93 % (3998770)------------------------------
% 56.03/8.93 % (3998770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.03/8.93 % (3998770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.03/8.93 % (3998770)CaDiCaL version: 2.1.3
% 56.03/8.93 % (3998770)Termination reason: Instruction limit
% 56.03/8.93 % (3998770)Termination phase: Saturation
% 56.03/8.93 % (3998770)Time elapsed: 0.271 s
% 56.03/8.93 % (3998770)Peak memory usage: 90 MB
% 56.03/8.93 % (3998770)Instructions burned: 1094 (million)
% 56.03/8.93 % (3998777)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=1917718722:i=1846:canc=cautious:fsr=off:rtra=on_2947 on theBenchmark for (2947ds/1846Mi)
% 56.03/8.93 % (3998778)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1277972497:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2947 on theBenchmark for (2947ds/36816Mi)
% 56.03/8.93 % (3998780)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2388202958:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2946 on theBenchmark for (2946ds/273Mi)
% 67.28/10.20 % (3998714)Instruction limit reached!
% 67.28/10.20 % (3998714)------------------------------
% 67.28/10.20 % (3998714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.28/10.20 % (3998714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.20 % (3998714)CaDiCaL version: 2.1.3
% 67.28/10.20 % (3998714)Termination reason: Instruction limit
% 67.28/10.20 % (3998714)Termination phase: Saturation
% 67.28/10.20 % (3998714)Time elapsed: 0.786 s
% 67.28/10.20 % (3998714)Peak memory usage: 129 MB
% 67.28/10.20 % (3998714)Instructions burned: 1131 (million)
% 67.28/10.20 % (3998780)Instruction limit reached!
% 67.28/10.20 % (3998780)------------------------------
% 67.28/10.20 % (3998780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.28/10.20 % (3998780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.20 % (3998780)CaDiCaL version: 2.1.3
% 67.28/10.20 % (3998780)Termination reason: Instruction limit
% 67.28/10.20 % (3998780)Termination phase: Saturation
% 67.28/10.20 % (3998780)Time elapsed: 0.102 s
% 67.28/10.20 % (3998780)Peak memory usage: 92 MB
% 67.28/10.20 % (3998780)Instructions burned: 275 (million)
% 67.28/10.20 % (3998785)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=115763960:i=5811:kws=precedence:nm=0:rtra=on_2944 on theBenchmark for (2944ds/5811Mi)
% 67.28/10.20 % (3998784)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=2966521556:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2944 on theBenchmark for (2944ds/863Mi)
% 67.28/10.20 % (3998776)Instruction limit reached!
% 67.28/10.20 % (3998776)------------------------------
% 67.28/10.20 % (3998776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.28/10.20 % (3998776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.20 % (3998776)CaDiCaL version: 2.1.3
% 67.28/10.20 % (3998776)Termination reason: Instruction limit
% 67.28/10.20 % (3998776)Termination phase: Saturation
% 67.28/10.20 % (3998776)Time elapsed: 0.533 s
% 67.28/10.20 % (3998776)Peak memory usage: 120 MB
% 67.28/10.20 % (3998776)Instructions burned: 869 (million)
% 67.28/10.20 % (3998788)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=615389182:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2942 on theBenchmark for (2942ds/2216Mi)
% 67.28/10.20 % (3998784)Instruction limit reached!
% 67.28/10.20 % (3998784)------------------------------
% 67.28/10.20 % (3998784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.28/10.20 % (3998784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.20 % (3998784)CaDiCaL version: 2.1.3
% 67.28/10.20 % (3998784)Termination reason: Instruction limit
% 67.28/10.20 % (3998784)Termination phase: Saturation
% 67.28/10.20 % (3998784)Time elapsed: 0.533 s
% 67.28/10.20 % (3998784)Peak memory usage: 120 MB
% 67.28/10.20 % (3998784)Instructions burned: 863 (million)
% 67.28/10.20 % (3998790)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3611034131:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2937 on theBenchmark for (2937ds/801Mi)
% 67.28/10.20 % (3998777)Instruction limit reached!
% 67.28/10.20 % (3998777)------------------------------
% 67.28/10.20 % (3998777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.28/10.20 % (3998777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.20 % (3998777)CaDiCaL version: 2.1.3
% 67.28/10.20 % (3998777)Termination reason: Instruction limit
% 67.28/10.20 % (3998777)Termination phase: Saturation
% 67.28/10.20 % (3998777)Time elapsed: 1.048 s
% 67.28/10.20 % (3998777)Peak memory usage: 97 MB
% 67.28/10.20 % (3998777)Instructions burned: 1847 (million)
% 67.28/10.20 % (3998577)Instruction limit reached!
% 67.28/10.20 % (3998577)------------------------------
% 67.28/10.20 % (3998577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.28/10.20 % (3998577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.20 % (3998577)CaDiCaL version: 2.1.3
% 67.28/10.20 % (3998577)Termination reason: Instruction limit
% 67.28/10.20 % (3998577)Termination phase: Saturation
% 67.28/10.20 % (3998577)Time elapsed: 2.624 s
% 67.28/10.20 % (3998577)Peak memory usage: 114 MB
% 68.36/10.47 % (3998577)Instructions burned: 4428 (million)
% 68.36/10.47 % (3998792)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4102672661:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2936 on theBenchmark for (2936ds/1026Mi)
% 68.36/10.47 % (3998793)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3688119236:i=3509:rtra=on_2935 on theBenchmark for (2935ds/3509Mi)
% 68.36/10.47 % (3998790)Instruction limit reached!
% 68.36/10.47 % (3998790)------------------------------
% 68.36/10.47 % (3998790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998790)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998790)Termination reason: Instruction limit
% 68.36/10.47 % (3998790)Termination phase: Saturation
% 68.36/10.47 % (3998790)Time elapsed: 0.279 s
% 68.36/10.47 % (3998790)Peak memory usage: 90 MB
% 68.36/10.47 % (3998790)Instructions burned: 804 (million)
% 68.36/10.47 % (3998796)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=951504812:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2933 on theBenchmark for (2933ds/2127Mi)
% 68.36/10.47 % (3998792)Instruction limit reached!
% 68.36/10.47 % (3998792)------------------------------
% 68.36/10.47 % (3998792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998792)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998792)Termination reason: Instruction limit
% 68.36/10.47 % (3998792)Termination phase: Saturation
% 68.36/10.47 % (3998792)Time elapsed: 0.352 s
% 68.36/10.47 % (3998792)Peak memory usage: 89 MB
% 68.36/10.47 % (3998792)Instructions burned: 1027 (million)
% 68.36/10.47 % (3998798)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3171068259:i=1959:rtra=on:fsd=on:proc=on_2931 on theBenchmark for (2931ds/1959Mi)
% 68.36/10.47 % (3998788)Instruction limit reached!
% 68.36/10.47 % (3998788)------------------------------
% 68.36/10.47 % (3998788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998788)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998788)Termination reason: Instruction limit
% 68.36/10.47 % (3998788)Termination phase: Saturation
% 68.36/10.47 % (3998788)Time elapsed: 1.359 s
% 68.36/10.47 % (3998788)Peak memory usage: 130 MB
% 68.36/10.47 % (3998788)Instructions burned: 2216 (million)
% 68.36/10.47 % (3998785)Instruction limit reached!
% 68.36/10.47 % (3998785)------------------------------
% 68.36/10.47 % (3998785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998785)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998785)Termination reason: Instruction limit
% 68.36/10.47 % (3998785)Termination phase: Saturation
% 68.36/10.47 % (3998785)Time elapsed: 1.738 s
% 68.36/10.47 % (3998785)Peak memory usage: 132 MB
% 68.36/10.47 % (3998785)Instructions burned: 5812 (million)
% 68.36/10.47 % (3998800)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1658253844:s2a=on:i=3553:nm=0:rtra=on_2927 on theBenchmark for (2927ds/3553Mi)
% 68.36/10.47 % (3998801)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3637715663:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2926 on theBenchmark for (2926ds/3201Mi)
% 68.36/10.47 % (3998796)Instruction limit reached!
% 68.36/10.47 % (3998796)------------------------------
% 68.36/10.47 % (3998796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998796)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998796)Termination reason: Instruction limit
% 68.36/10.47 % (3998796)Termination phase: Saturation
% 68.36/10.47 % (3998796)Time elapsed: 1.002 s
% 68.36/10.47 % (3998796)Peak memory usage: 92 MB
% 68.36/10.47 % (3998796)Instructions burned: 2127 (million)
% 68.36/10.47 % (3998804)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=684194818:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2922 on theBenchmark for (2922ds/4093Mi)
% 68.36/10.47 % (3998801)Instruction limit reached!
% 68.36/10.47 % (3998801)------------------------------
% 68.36/10.47 % (3998801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998801)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998801)Termination reason: Instruction limit
% 68.36/10.47 % (3998801)Termination phase: Saturation
% 68.36/10.47 % (3998801)Time elapsed: 0.742 s
% 68.36/10.47 % (3998801)Peak memory usage: 95 MB
% 68.36/10.47 % (3998801)Instructions burned: 3206 (million)
% 68.36/10.47 % (3998798)Instruction limit reached!
% 68.36/10.47 % (3998798)------------------------------
% 68.36/10.47 % (3998798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998798)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998798)Termination reason: Instruction limit
% 68.36/10.47 % (3998798)Termination phase: Saturation
% 68.36/10.47 % (3998798)Time elapsed: 1.280 s
% 68.36/10.47 % (3998798)Peak memory usage: 126 MB
% 68.36/10.47 % (3998798)Instructions burned: 1959 (million)
% 68.36/10.47 % (3998806)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=4032830923:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2917 on theBenchmark for (2917ds/21173Mi)
% 68.36/10.47 % (3998809)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=348723214:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2917 on theBenchmark for (2917ds/10544Mi)
% 68.36/10.47 % (3998771)Instruction limit reached!
% 68.36/10.47 % (3998771)------------------------------
% 68.36/10.47 % (3998771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998771)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998771)Termination reason: Instruction limit
% 68.36/10.47 % (3998771)Termination phase: Saturation
% 68.36/10.47 % (3998771)Time elapsed: 3.684 s
% 68.36/10.47 % (3998771)Peak memory usage: 123 MB
% 68.36/10.47 % (3998771)Instructions burned: 6400 (million)
% 68.36/10.47 % (3998793)Instruction limit reached!
% 68.36/10.47 % (3998793)------------------------------
% 68.36/10.47 % (3998793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998793)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998793)Termination reason: Instruction limit
% 68.36/10.47 % (3998793)Termination phase: Saturation
% 68.36/10.47 % (3998793)Time elapsed: 2.249 s
% 68.36/10.47 % (3998793)Peak memory usage: 114 MB
% 68.36/10.47 % (3998793)Instructions burned: 3511 (million)
% 68.36/10.47 % (3998811)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2242318133:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2911 on theBenchmark for (2911ds/1262Mi)
% 68.36/10.47 % (3998812)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4063853030:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/775Mi)
% 68.36/10.47 % (3998804)Instruction limit reached!
% 68.36/10.47 % (3998804)------------------------------
% 68.36/10.47 % (3998804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998804)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998804)Termination reason: Instruction limit
% 68.36/10.47 % (3998804)Termination phase: Saturation
% 68.36/10.47 % (3998804)Time elapsed: 1.322 s
% 68.36/10.47 % (3998804)Peak memory usage: 135 MB
% 68.36/10.47 % (3998804)Instructions burned: 4095 (million)
% 68.36/10.47 % (3998815)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=920843685:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2907 on theBenchmark for (2907ds/270Mi)
% 68.36/10.47 % (3998812)Instruction limit reached!
% 68.36/10.47 % (3998812)------------------------------
% 68.36/10.47 % (3998812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998812)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998812)Termination reason: Instruction limit
% 68.36/10.47 % (3998812)Termination phase: Saturation
% 68.36/10.47 % (3998812)Time elapsed: 0.456 s
% 68.36/10.47 % (3998812)Peak memory usage: 93 MB
% 68.36/10.47 % (3998812)Instructions burned: 776 (million)
% 68.36/10.47 % (3998811)First to succeed.
% 68.36/10.47 % (3998811)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3998302"
% 68.36/10.47 % (3998815)Instruction limit reached!
% 68.36/10.47 % (3998815)------------------------------
% 68.36/10.47 % (3998815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.36/10.47 % (3998815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.36/10.47 % (3998815)CaDiCaL version: 2.1.3
% 68.36/10.47 % (3998815)Termination reason: Instruction limit
% 68.36/10.47 % (3998815)Termination phase: Saturation
% 68.36/10.47 % (3998815)Time elapsed: 0.189 s
% 68.36/10.47 % (3998815)Peak memory usage: 91 MB
% 68.36/10.47 % (3998815)Instructions burned: 270 (million)
% 68.36/10.47 % (3998817)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=133766030:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2905 on theBenchmark for (2905ds/17165Mi)
% 68.36/10.47 % (3998818)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=858167486:s2a=on:i=13094:s2at=-1:rtra=on_2904 on theBenchmark for (2904ds/13094Mi)
% 68.36/10.47 % (3998811)Refutation found. Thanks to Tanya!
% 68.36/10.47 % SZS status Theorem for theBenchmark
% 68.36/10.47 % SZS output start Proof for theBenchmark
% See solution above
% 69.41/10.66 % (3998811)------------------------------
% 69.41/10.66 % (3998811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/10.66 % (3998811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/10.66 % (3998811)CaDiCaL version: 2.1.3
% 69.41/10.66 % (3998811)Termination reason: Refutation
% 69.41/10.66 % (3998811)Time elapsed: 0.539 s
% 69.41/10.66 % (3998811)Peak memory usage: 123 MB
% 69.41/10.66 % (3998811)Instructions burned: 863 (million)
% 69.41/10.66 % (3998811)------------------------------
% 69.41/10.66 % (3998811)------------------------------
% 69.41/10.66 % (3998302)Success in time 9.739 s
% 69.41/10.66 % Vampire exiting
%------------------------------------------------------------------------------