%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW608_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:56 PM UTC 2026
% Result : Theorem 34.78s 5.93s
% Output : Refutation 37.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 63
% Syntax : Number of formulae : 592 ( 114 unt; 0 typ; 47 def)
% Number of atoms : 1763 ( 317 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 2146 ( 975 ~;1018 |; 87 &)
% ( 36 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 1359 ( 516 atm; 11 fun; 791 num; 41 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 40 ( 36 usr; 33 prp; 0-5 aty)
% Number of functors : 64 ( 58 usr; 30 con; 0-5 aty)
% Number of variables : 193 ( 0 sgn 183 !; 10 ?; 193 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
map: ( ty * ty ) > ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_15,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_16,type,
array: ty > ty ).
tff(func_def_17,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_18,type,
length: ( ty * uni ) > $int ).
tff(func_def_19,type,
elts: ( ty * uni ) > uni ).
tff(func_def_20,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_21,type,
t2tb: $int > uni ).
tff(func_def_22,type,
tb2t: uni > $int ).
tff(func_def_23,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_24,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_25,type,
ref: ty > ty ).
tff(func_def_26,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_27,type,
contents: ( ty * uni ) > uni ).
tff(func_def_28,type,
prefix_tl: $int > $int ).
tff(func_def_32,type,
t2tb1: map_int_int > uni ).
tff(func_def_33,type,
tb2t1: uni > map_int_int ).
tff(func_def_34,type,
num_of: ( map_int_int * $int * $int ) > $int ).
tff(func_def_36,type,
t2tb2: array_int > uni ).
tff(func_def_37,type,
tb2t2: uni > array_int ).
tff(func_def_40,type,
sK0: ( map_int_int * $int * map_int_int * $int ) > $int ).
tff(func_def_41,type,
sK1: map_int_int ).
tff(func_def_42,type,
sK2: map_int_int ).
tff(func_def_43,type,
sK3: map_int_int ).
tff(func_def_44,type,
sK4: ( array_int * array_int ) > $int ).
tff(func_def_45,type,
sK5: array_int > $int ).
tff(func_def_46,type,
sK6: ( $int * $int * map_int_int * map_int_int ) > $int ).
tff(func_def_47,type,
sK7: ( $int * $int * map_int_int ) > $int ).
tff(func_def_48,type,
sK8: ( $int * $int * map_int_int ) > $int ).
tff(func_def_49,type,
sK9: array_int > $int ).
tff(func_def_50,type,
sK10: array_int > $int ).
tff(func_def_51,type,
sF11: uni ).
tff(func_def_52,type,
sF12: uni ).
tff(func_def_53,type,
sF13: uni ).
tff(func_def_54,type,
sF14: uni ).
tff(func_def_55,type,
sF15: map_int_int ).
tff(func_def_56,type,
sF16: uni ).
tff(func_def_57,type,
sF17: uni ).
tff(func_def_58,type,
sF18: array_int ).
tff(func_def_59,type,
sF19: uni ).
tff(func_def_60,type,
sF20: uni ).
tff(func_def_61,type,
sF21: uni ).
tff(func_def_62,type,
sF22: map_int_int ).
tff(func_def_63,type,
sF23: uni ).
tff(func_def_64,type,
sF24: uni ).
tff(func_def_65,type,
sF25: map_int_int ).
tff(func_def_71,type,
-1: $int > $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
pr: ( map_int_int * $int ) > $o ).
tff(pred_def_5,type,
is_permutation: array_int > $o ).
tff(pred_def_6,type,
loopinvariant: ( array_int * array_int * $int * $int * $int ) > $o ).
tff(f11,axiom,
! [X5: uni,X0: ty,X1: ty,X3: uni,X4: uni,X2: uni] :
( sort(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select_eq) ).
tff(f12,axiom,
! [X4: uni,X3: uni,X2: uni,X0: ty,X1: ty] :
( sort(X0,X3)
=> ( sort(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select_neq) ).
tff(f16,axiom,
! [X1: $int,X0: ty,X2: uni] : ( length(X0,mk_array(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def) ).
tff(f18,axiom,
! [X2: uni,X1: $int,X0: ty] :
( sort(map(int,X0),X2)
=> ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def) ).
tff(f21,axiom,
! [X0: $int] : sort(int,t2tb(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort) ).
tff(f22,axiom,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL) ).
tff(f23,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f24,axiom,
! [X1: uni,X2: $int,X0: ty] : ( get1(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_def) ).
tff(f34,axiom,
! [X0: map_int_int] : sort(map(int,int),t2tb1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f36,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f54,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2) ).
tff(f55,axiom,
! [X0: array_int] :
( ! [X1: $int] :
( ( $lesseq(0,X1)
& $less(X1,length(int,t2tb2(X0))) )
=> ( $lesseq(0,tb2t(get1(int,t2tb2(X0),X1)))
& $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0)))
& ! [X2: $int] :
( ( $lesseq(0,X2)
& $less(X2,length(int,t2tb2(X0))) )
=> ( ( X1 != X2 )
=> ( tb2t(get1(int,t2tb2(X0),X1)) != tb2t(get1(int,t2tb2(X0),X2)) ) ) ) ) )
<=> is_permutation(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',is_permutation_def) ).
tff(f58,conjecture,
( $lesseq(0,3)
& ( $lesseq(0,3)
=> ( $less(0,3)
& ! [X0: map_int_int] :
( ( $lesseq(0,3)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) ) )
=> ( $less(2,3)
& $lesseq(0,2)
& ! [X1: map_int_int] :
( ( $lesseq(0,3)
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(2),t2tb(0))) ) )
=> ( ! [X2: map_int_int] :
( ( ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(1),t2tb(1))) )
& $lesseq(0,3) )
=> is_permutation(tb2t2(mk_array(int,3,t2tb1(X2)))) )
& $lesseq(0,1)
& $less(1,3) ) ) ) )
& $lesseq(0,0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_test1) ).
tff(f59,negated_conjecture,
~ ( $lesseq(0,3)
& ( $lesseq(0,3)
=> ( $less(0,3)
& ! [X0: map_int_int] :
( ( $lesseq(0,3)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) ) )
=> ( $less(2,3)
& $lesseq(0,2)
& ! [X1: map_int_int] :
( ( $lesseq(0,3)
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(2),t2tb(0))) ) )
=> ( ! [X2: map_int_int] :
( ( ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(1),t2tb(1))) )
& $lesseq(0,3) )
=> is_permutation(tb2t2(mk_array(int,3,t2tb1(X2)))) )
& $lesseq(0,1)
& $less(1,3) ) ) ) )
& $lesseq(0,0) ) ) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
tff(f60,plain,
~ ( ( ~ $less(3,0)
=> ( ~ $less(0,0)
& $less(0,3)
& ! [X0: map_int_int] :
( ( ~ $less(3,0)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) ) )
=> ( $less(2,3)
& ~ $less(2,0)
& ! [X1: map_int_int] :
( ( ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(2),t2tb(0))) )
& ~ $less(3,0) )
=> ( $less(1,3)
& ~ $less(1,0)
& ! [X2: map_int_int] :
( ( ~ $less(3,0)
& ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(1),t2tb(1))) ) )
=> is_permutation(tb2t2(mk_array(int,3,t2tb1(X2)))) ) ) ) ) ) ) )
& ~ $less(3,0) ),
inference(theory_normalization,[],[f59]) ).
tff(f73,plain,
! [X0: array_int] :
( ! [X1: $int] :
( ( $less(X1,length(int,t2tb2(X0)))
& ~ $less(X1,0) )
=> ( ~ $less(tb2t(get1(int,t2tb2(X0),X1)),0)
& ! [X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,length(int,t2tb2(X0))) )
=> ( ( X1 != X2 )
=> ( tb2t(get1(int,t2tb2(X0),X1)) != tb2t(get1(int,t2tb2(X0),X2)) ) ) )
& $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0))) ) )
<=> is_permutation(X0) ),
inference(theory_normalization,[],[f55]) ).
tff(f79,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f86,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| ( X0 = X1 )
| $less(X1,X0) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f96,plain,
! [X0: $int,X1: $int] :
( ~ $less(X0,X1)
| ~ $less(X1,$sum(X0,1)) ),
introduced(definition,[],[tha_extra_integer_ordering]) ).
tff(f102,plain,
! [X1: uni,X0: uni,X4: ty,X3: ty,X2: uni] :
( sort(X3,X1)
=> ( sort(X3,X0)
=> ! [X5: uni] :
( ( X0 != X1 )
=> ( get(X4,X3,X2,X0) = get(X4,X3,set(X4,X3,X2,X1,X5),X0) ) ) ) ),
inference(rectify,[],[f12]) ).
tff(f103,plain,
! [X1: $int,X0: uni,X2: ty] :
( sort(map(int,X2),X0)
=> ( elts(X2,mk_array(X2,X1,X0)) = X0 ) ),
inference(rectify,[],[f18]) ).
tff(f118,plain,
! [X1: ty,X2: uni,X0: $int] : ( length(X1,mk_array(X1,X0,X2)) = X0 ),
inference(rectify,[],[f16]) ).
tff(f121,plain,
! [X2: ty,X1: $int,X0: uni] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get1(X2,X0,X1) ),
inference(rectify,[],[f24]) ).
tff(f132,plain,
! [X1: ty,X2: ty,X0: uni,X3: uni,X4: uni,X5: uni] :
( sort(X2,X0)
=> ( ( X3 = X4 )
=> ( get(X2,X1,set(X2,X1,X5,X3,X0),X4) = X0 ) ) ),
inference(rectify,[],[f11]) ).
tff(f145,plain,
! [X0: array_int] :
( ! [X1: $int] :
( ( ~ $less(tb2t(get1(int,t2tb2(X0),X1)),0)
& ! [X2: $int] :
( ( tb2t(get1(int,t2tb2(X0),X1)) != tb2t(get1(int,t2tb2(X0),X2)) )
| ( X1 = X2 )
| $less(X2,0)
| ~ $less(X2,length(int,t2tb2(X0))) )
& $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0))) )
| ~ $less(X1,length(int,t2tb2(X0)))
| $less(X1,0) )
<=> is_permutation(X0) ),
inference(ennf_transformation,[],[f73]) ).
tff(f146,plain,
! [X0: array_int] :
( is_permutation(X0)
<=> ! [X1: $int] :
( ( ~ $less(tb2t(get1(int,t2tb2(X0),X1)),0)
& $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0)))
& ! [X2: $int] :
( ( X1 = X2 )
| $less(X2,0)
| ~ $less(X2,length(int,t2tb2(X0)))
| ( tb2t(get1(int,t2tb2(X0),X1)) != tb2t(get1(int,t2tb2(X0),X2)) ) ) )
| $less(X1,0)
| ~ $less(X1,length(int,t2tb2(X0))) ) ),
inference(flattening,[],[f145]) ).
tff(f156,plain,
! [X1: uni,X0: uni,X4: ty,X3: ty,X2: uni] :
( ! [X5: uni] :
( ( X0 = X1 )
| ( get(X4,X3,X2,X0) = get(X4,X3,set(X4,X3,X2,X1,X5),X0) ) )
| ~ sort(X3,X0)
| ~ sort(X3,X1) ),
inference(ennf_transformation,[],[f102]) ).
tff(f157,plain,
! [X4: ty,X0: uni,X1: uni,X2: uni,X3: ty] :
( ! [X5: uni] :
( ( X0 = X1 )
| ( get(X4,X3,X2,X0) = get(X4,X3,set(X4,X3,X2,X1,X5),X0) ) )
| ~ sort(X3,X0)
| ~ sort(X3,X1) ),
inference(flattening,[],[f156]) ).
tff(f170,plain,
( ( ( $less(0,0)
| ~ $less(0,3)
| ? [X0: map_int_int] :
( ( ~ $less(2,3)
| $less(2,0)
| ? [X1: map_int_int] :
( ( ~ $less(1,3)
| $less(1,0)
| ? [X2: map_int_int] :
( ~ is_permutation(tb2t2(mk_array(int,3,t2tb1(X2))))
& ~ $less(3,0)
& ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(1),t2tb(1))) ) ) )
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(2),t2tb(0))) )
& ~ $less(3,0) ) )
& ~ $less(3,0)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) ) ) )
& ~ $less(3,0) )
| $less(3,0) ),
inference(ennf_transformation,[],[f60]) ).
tff(f171,plain,
( ( ~ $less(3,0)
& ( ~ $less(0,3)
| ? [X0: map_int_int] :
( ~ $less(3,0)
& ( ~ $less(2,3)
| $less(2,0)
| ? [X1: map_int_int] :
( ~ $less(3,0)
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(2),t2tb(0))) )
& ( $less(1,0)
| ? [X2: map_int_int] :
( ~ is_permutation(tb2t2(mk_array(int,3,t2tb1(X2))))
& ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(1),t2tb(1))) )
& ~ $less(3,0) )
| ~ $less(1,3) ) ) )
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) ) )
| $less(0,0) ) )
| $less(3,0) ),
inference(flattening,[],[f170]) ).
tff(f175,plain,
! [X2: ty,X0: uni,X1: $int] :
( ( elts(X2,mk_array(X2,X1,X0)) = X0 )
| ~ sort(map(int,X2),X0) ),
inference(ennf_transformation,[],[f103]) ).
tff(f176,plain,
! [X1: ty,X2: ty,X0: uni,X3: uni,X4: uni,X5: uni] :
( ( get(X2,X1,set(X2,X1,X5,X3,X0),X4) = X0 )
| ( X3 != X4 )
| ~ sort(X2,X0) ),
inference(ennf_transformation,[],[f132]) ).
tff(f177,plain,
! [X0: uni,X2: ty,X1: ty,X3: uni,X5: uni,X4: uni] :
( ( X3 != X4 )
| ( get(X2,X1,set(X2,X1,X5,X3,X0),X4) = X0 )
| ~ sort(X2,X0) ),
inference(flattening,[],[f176]) ).
tff(f183,plain,
! [X0: ty,X1: uni,X2: $int] :
( ( elts(X0,mk_array(X0,X2,X1)) = X1 )
| ~ sort(map(int,X0),X1) ),
inference(rectify,[],[f175]) ).
tff(f191,plain,
( ( ~ $less(3,0)
& ( ~ $less(0,3)
| ( ~ $less(3,0)
& ( ~ $less(2,3)
| $less(2,0)
| ( ~ $less(3,0)
& ( tb2t1(set(int,int,t2tb1(sK1),t2tb(2),t2tb(0))) = sK2 )
& ( $less(1,0)
| ( ~ is_permutation(tb2t2(mk_array(int,3,t2tb1(sK3))))
& ( tb2t1(set(int,int,t2tb1(sK2),t2tb(1),t2tb(1))) = sK3 )
& ~ $less(3,0) )
| ~ $less(1,3) ) ) )
& ( tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) = sK1 ) )
| $less(0,0) ) )
| $less(3,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f171]) ).
tff(f197,plain,
! [X0: ty,X1: uni,X2: $int] : ( length(X0,mk_array(X0,X2,X1)) = X2 ),
inference(rectify,[],[f118]) ).
tff(f205,plain,
! [X0: ty,X1: $int,X2: uni] : ( get1(X0,X2,X1) = get(X0,int,elts(X0,X2),t2tb(X1)) ),
inference(rectify,[],[f121]) ).
tff(f208,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni,X4: ty] :
( ! [X5: uni] :
( ( X1 = X2 )
| ( get(X0,X4,X3,X1) = get(X0,X4,set(X0,X4,X3,X2,X5),X1) ) )
| ~ sort(X4,X1)
| ~ sort(X4,X2) ),
inference(rectify,[],[f157]) ).
tff(f218,plain,
! [X0: uni,X1: ty,X2: ty,X3: uni,X4: uni,X5: uni] :
( ( X3 != X5 )
| ( get(X1,X2,set(X1,X2,X4,X3,X0),X5) = X0 )
| ~ sort(X1,X0) ),
inference(rectify,[],[f177]) ).
tff(f223,plain,
! [X0: array_int] :
( ( is_permutation(X0)
| ? [X1: $int] :
( ( $less(tb2t(get1(int,t2tb2(X0),X1)),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0)))
| ? [X2: $int] :
( ( X1 != X2 )
& ~ $less(X2,0)
& $less(X2,length(int,t2tb2(X0)))
& ( tb2t(get1(int,t2tb2(X0),X1)) = tb2t(get1(int,t2tb2(X0),X2)) ) ) )
& ~ $less(X1,0)
& $less(X1,length(int,t2tb2(X0))) ) )
& ( ! [X1: $int] :
( ( ~ $less(tb2t(get1(int,t2tb2(X0),X1)),0)
& $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0)))
& ! [X2: $int] :
( ( X1 = X2 )
| $less(X2,0)
| ~ $less(X2,length(int,t2tb2(X0)))
| ( tb2t(get1(int,t2tb2(X0),X1)) != tb2t(get1(int,t2tb2(X0),X2)) ) ) )
| $less(X1,0)
| ~ $less(X1,length(int,t2tb2(X0))) )
| ~ is_permutation(X0) ) ),
inference(nnf_transformation,[],[f146]) ).
tff(f224,plain,
! [X0: array_int] :
( ( is_permutation(X0)
| ? [X1: $int] :
( ( $less(tb2t(get1(int,t2tb2(X0),X1)),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),X1)),length(int,t2tb2(X0)))
| ? [X2: $int] :
( ( X1 != X2 )
& ~ $less(X2,0)
& $less(X2,length(int,t2tb2(X0)))
& ( tb2t(get1(int,t2tb2(X0),X1)) = tb2t(get1(int,t2tb2(X0),X2)) ) ) )
& ~ $less(X1,0)
& $less(X1,length(int,t2tb2(X0))) ) )
& ( ! [X3: $int] :
( ( ~ $less(tb2t(get1(int,t2tb2(X0),X3)),0)
& $less(tb2t(get1(int,t2tb2(X0),X3)),length(int,t2tb2(X0)))
& ! [X4: $int] :
( ( X3 = X4 )
| $less(X4,0)
| ~ $less(X4,length(int,t2tb2(X0)))
| ( tb2t(get1(int,t2tb2(X0),X3)) != tb2t(get1(int,t2tb2(X0),X4)) ) ) )
| $less(X3,0)
| ~ $less(X3,length(int,t2tb2(X0))) )
| ~ is_permutation(X0) ) ),
inference(rectify,[],[f223]) ).
tff(f225,plain,
! [X0: array_int] :
( ( is_permutation(X0)
| ( ( $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),length(int,t2tb2(X0)))
| ( ( sK10(X0) != sK9(X0) )
& ~ $less(sK10(X0),0)
& $less(sK10(X0),length(int,t2tb2(X0)))
& ( tb2t(get1(int,t2tb2(X0),sK9(X0))) = tb2t(get1(int,t2tb2(X0),sK10(X0))) ) ) )
& ~ $less(sK9(X0),0)
& $less(sK9(X0),length(int,t2tb2(X0))) ) )
& ( ! [X3: $int] :
( ( ~ $less(tb2t(get1(int,t2tb2(X0),X3)),0)
& $less(tb2t(get1(int,t2tb2(X0),X3)),length(int,t2tb2(X0)))
& ! [X4: $int] :
( ( X3 = X4 )
| $less(X4,0)
| ~ $less(X4,length(int,t2tb2(X0)))
| ( tb2t(get1(int,t2tb2(X0),X3)) != tb2t(get1(int,t2tb2(X0),X4)) ) ) )
| $less(X3,0)
| ~ $less(X3,length(int,t2tb2(X0))) )
| ~ is_permutation(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X1,sK9(X0)),skolemize(X2,sK10(X0))],[f224]) ).
tff(f230,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f36]) ).
tff(f231,plain,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f22]) ).
tff(f233,plain,
! [X2: $int,X0: ty,X1: uni] :
( ( elts(X0,mk_array(X0,X2,X1)) = X1 )
| ~ sort(map(int,X0),X1) ),
inference(cnf_transformation,[],[f183]) ).
tff(f246,plain,
( ~ $less(0,3)
| ( tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(2))) = sK1 )
| $less(0,0)
| $less(3,0) ),
inference(cnf_transformation,[],[f191]) ).
tff(f248,plain,
( ~ $less(0,3)
| ~ $less(2,3)
| $less(2,0)
| $less(1,0)
| ( tb2t1(set(int,int,t2tb1(sK2),t2tb(1),t2tb(1))) = sK3 )
| ~ $less(1,3)
| $less(0,0)
| $less(3,0) ),
inference(cnf_transformation,[],[f191]) ).
tff(f249,plain,
( ~ $less(0,3)
| ~ $less(2,3)
| $less(2,0)
| $less(1,0)
| ~ is_permutation(tb2t2(mk_array(int,3,t2tb1(sK3))))
| ~ $less(1,3)
| $less(0,0)
| $less(3,0) ),
inference(cnf_transformation,[],[f191]) ).
tff(f250,plain,
( ~ $less(0,3)
| ~ $less(2,3)
| $less(2,0)
| ( tb2t1(set(int,int,t2tb1(sK1),t2tb(2),t2tb(0))) = sK2 )
| $less(0,0)
| $less(3,0) ),
inference(cnf_transformation,[],[f191]) ).
tff(f266,plain,
! [X2: $int,X0: ty,X1: uni] : ( length(X0,mk_array(X0,X2,X1)) = X2 ),
inference(cnf_transformation,[],[f197]) ).
tff(f268,plain,
! [X0: $int] : sort(int,t2tb(X0)),
inference(cnf_transformation,[],[f21]) ).
tff(f278,plain,
! [X0: map_int_int] : sort(map(int,int),t2tb1(X0)),
inference(cnf_transformation,[],[f34]) ).
tff(f279,plain,
! [X2: uni,X0: ty,X1: $int] : ( get1(X0,X2,X1) = get(X0,int,elts(X0,X2),t2tb(X1)) ),
inference(cnf_transformation,[],[f205]) ).
tff(f284,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni,X4: ty,X5: uni] :
( ( get(X0,X4,X3,X1) = get(X0,X4,set(X0,X4,X3,X2,X5),X1) )
| ( X1 = X2 )
| ~ sort(X4,X2)
| ~ sort(X4,X1) ),
inference(cnf_transformation,[],[f208]) ).
tff(f289,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f54]) ).
tff(f300,plain,
! [X2: ty,X3: uni,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( X3 != X5 )
| ( get(X1,X2,set(X1,X2,X4,X3,X0),X5) = X0 )
| ~ sort(X1,X0) ),
inference(cnf_transformation,[],[f218]) ).
tff(f301,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f23]) ).
tff(f312,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(sK9(X0),length(int,t2tb2(X0))) ),
inference(cnf_transformation,[],[f225]) ).
tff(f313,plain,
! [X0: array_int] :
( ~ $less(sK9(X0),0)
| is_permutation(X0) ),
inference(cnf_transformation,[],[f225]) ).
tff(f314,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),length(int,t2tb2(X0)))
| ( tb2t(get1(int,t2tb2(X0),sK9(X0))) = tb2t(get1(int,t2tb2(X0),sK10(X0))) ) ),
inference(cnf_transformation,[],[f225]) ).
tff(f315,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),length(int,t2tb2(X0)))
| $less(sK10(X0),length(int,t2tb2(X0))) ),
inference(cnf_transformation,[],[f225]) ).
tff(f316,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),length(int,t2tb2(X0)))
| ~ $less(sK10(X0),0) ),
inference(cnf_transformation,[],[f225]) ).
tff(f317,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),0)
| ~ $less(tb2t(get1(int,t2tb2(X0),sK9(X0))),length(int,t2tb2(X0)))
| ( sK10(X0) != sK9(X0) ) ),
inference(cnf_transformation,[],[f225]) ).
tff(f326,plain,
! [X0: array_int] :
( ( sK10(X0) != sK9(X0) )
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),length(int,t2tb2(X0)))
| $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),0)
| is_permutation(X0) ),
inference(definition_unfolding,[],[f317,f279,f279]) ).
tff(f327,plain,
! [X0: array_int] :
( ~ $less(sK10(X0),0)
| $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),length(int,t2tb2(X0)))
| is_permutation(X0) ),
inference(definition_unfolding,[],[f316,f279,f279]) ).
tff(f328,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),0)
| $less(sK10(X0),length(int,t2tb2(X0)))
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),length(int,t2tb2(X0))) ),
inference(definition_unfolding,[],[f315,f279,f279]) ).
tff(f329,plain,
! [X0: array_int] :
( is_permutation(X0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),length(int,t2tb2(X0)))
| ( tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK10(X0)))) = tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))) )
| $less(tb2t(get(int,int,elts(int,t2tb2(X0)),t2tb(sK9(X0)))),0) ),
inference(definition_unfolding,[],[f314,f279,f279,f279,f279]) ).
tff(f334,plain,
! [X2: ty,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( get(X1,X2,set(X1,X2,X4,X5,X0),X5) = X0 )
| ~ sort(X1,X0) ),
inference(equality_resolution,[],[f300]) ).
tff(f335,definition,
sF11 = t2tb1(sK1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f336,definition,
sF12 = t2tb(2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f337,plain,
t2tb(2) = sF12,
inference(reorient_equations,[],[f336]) ).
tff(f338,definition,
sF13 = t2tb(0),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f339,plain,
t2tb(0) = sF13,
inference(reorient_equations,[],[f338]) ).
tff(f340,definition,
sF14 = set(int,int,sF11,sF12,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f341,definition,
sF15 = tb2t1(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f342,plain,
( $less(3,0)
| $less(0,0)
| ~ $less(0,3)
| ~ $less(2,3)
| ( sK2 = sF15 )
| $less(2,0) ),
inference(definition_folding,[],[f250,f341,f340,f339,f337,f335]) ).
tff(f343,definition,
sF16 = t2tb1(sK3),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f344,plain,
t2tb1(sK3) = sF16,
inference(reorient_equations,[],[f343]) ).
tff(f345,definition,
sF17 = mk_array(int,3,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f346,definition,
sF18 = tb2t2(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f347,plain,
tb2t2(sF17) = sF18,
inference(reorient_equations,[],[f346]) ).
tff(f348,plain,
( ~ $less(0,3)
| ~ $less(1,3)
| $less(3,0)
| $less(1,0)
| $less(0,0)
| ~ $less(2,3)
| ~ is_permutation(sF18)
| $less(2,0) ),
inference(definition_folding,[],[f249,f347,f345,f344]) ).
tff(f349,definition,
sF19 = t2tb1(sK2),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f350,plain,
t2tb1(sK2) = sF19,
inference(reorient_equations,[],[f349]) ).
tff(f351,definition,
sF20 = t2tb(1),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f352,plain,
t2tb(1) = sF20,
inference(reorient_equations,[],[f351]) ).
tff(f353,definition,
sF21 = set(int,int,sF19,sF20,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f354,definition,
sF22 = tb2t1(sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f355,plain,
( $less(2,0)
| ~ $less(1,3)
| ~ $less(0,3)
| $less(3,0)
| $less(1,0)
| ( sK3 = sF22 )
| ~ $less(2,3)
| $less(0,0) ),
inference(definition_folding,[],[f248,f354,f353,f352,f352,f350]) ).
tff(f356,definition,
sF23 = const(int,int,sF13),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f357,plain,
const(int,int,sF13) = sF23,
inference(reorient_equations,[],[f356]) ).
tff(f358,definition,
sF24 = set(int,int,sF23,sF13,sF12),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f359,plain,
set(int,int,sF23,sF13,sF12) = sF24,
inference(reorient_equations,[],[f358]) ).
tff(f360,definition,
sF25 = tb2t1(sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f361,plain,
( $less(3,0)
| ( sF25 = sK1 )
| ~ $less(0,3)
| $less(0,0) ),
inference(definition_folding,[],[f246,f360,f359,f337,f339,f357,f339]) ).
tff(f362,plain,
sK2 = sF15,
inference(evaluation,[],[f342]) ).
tff(f363,plain,
sK3 = sF22,
inference(evaluation,[],[f355]) ).
tff(f365,plain,
sF25 = sK1,
inference(evaluation,[],[f361]) ).
tff(f366,plain,
~ is_permutation(sF18),
inference(evaluation,[],[f348]) ).
tff(f372,plain,
sort(int,sF12),
inference(superposition,[],[f268,f337]) ).
tff(f373,plain,
sort(int,sF13),
inference(superposition,[],[f268,f339]) ).
tff(f374,plain,
sK2 = tb2t1(sF14),
inference(forward_demodulation,[],[f341,f362]) ).
tff(f375,plain,
sort(int,sF20),
inference(superposition,[],[f268,f352]) ).
tff(f376,plain,
sK3 = tb2t1(sF21),
inference(forward_demodulation,[],[f354,f363]) ).
tff(f377,plain,
tb2t1(sF24) = sK1,
inference(forward_demodulation,[],[f360,f365]) ).
tff(f381,plain,
t2tb1(sK2) = sF14,
inference(superposition,[],[f230,f374]) ).
tff(f382,plain,
sF21 = t2tb1(sK3),
inference(superposition,[],[f230,f376]) ).
tff(f383,plain,
sF24 = t2tb1(sK1),
inference(superposition,[],[f230,f377]) ).
tff(f384,plain,
sF21 = sF16,
inference(forward_demodulation,[],[f382,f344]) ).
tff(f385,plain,
sF11 = sF24,
inference(forward_demodulation,[],[f383,f335]) ).
tff(f386,plain,
2 = tb2t(sF12),
inference(superposition,[],[f231,f337]) ).
tff(f387,plain,
0 = tb2t(sF13),
inference(superposition,[],[f231,f339]) ).
tff(f388,plain,
1 = tb2t(sF20),
inference(superposition,[],[f231,f352]) ).
tff(f391,plain,
sF19 = sF14,
inference(superposition,[],[f381,f350]) ).
tff(f400,plain,
sF17 = t2tb2(sF18),
inference(superposition,[],[f289,f347]) ).
tff(f404,plain,
! [X0: uni] : sort(int,X0),
inference(superposition,[],[f268,f301]) ).
tff(f412,plain,
! [X0: uni] : sort(map(int,int),X0),
inference(superposition,[],[f278,f230]) ).
tff(f440,plain,
3 = length(int,sF17),
inference(superposition,[],[f266,f345]) ).
tff(f441,plain,
sF21 = set(int,int,sF14,sF20,sF20),
inference(forward_demodulation,[],[f353,f391]) ).
tff(f442,plain,
set(int,int,sF14,sF20,sF20) = sF16,
inference(forward_demodulation,[],[f441,f384]) ).
tff(f443,plain,
sF11 = set(int,int,sF23,sF13,sF12),
inference(forward_demodulation,[],[f359,f385]) ).
tff(f449,plain,
! [X0: array_int] :
( is_permutation(X0)
| $less(0,sK9(X0))
| ( 0 = sK9(X0) ) ),
inference(resolution,[],[f86,f313]) ).
tff(f462,definition,
( spl26_1
<=> $less(0,sK9(sF18)) ),
introduced(definition,[new_symbols(definition,[spl26_1])],[avatar_definition]) ).
tff(f464,plain,
( $less(0,sK9(sF18))
| ~ spl26_1 ),
inference(avatar_component_clause,[],[f462]) ).
tff(f466,definition,
( spl26_2
<=> ( 0 = sK9(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl26_2])],[avatar_definition]) ).
tff(f468,plain,
( ( 0 = sK9(sF18) )
| ~ spl26_2 ),
inference(avatar_component_clause,[],[f466]) ).
tff(f481,plain,
$less(sK9(sF18),length(int,t2tb2(sF18))),
inference(resolution,[],[f312,f366]) ).
tff(f482,plain,
$less(sK9(sF18),length(int,sF17)),
inference(forward_demodulation,[],[f481,f400]) ).
tff(f483,plain,
$less(sK9(sF18),3),
inference(forward_demodulation,[],[f482,f440]) ).
tff(f701,plain,
( ~ sort(map(int,int),sF16)
| ( elts(int,sF17) = sF16 ) ),
inference(superposition,[],[f233,f345]) ).
tff(f704,plain,
elts(int,sF17) = sF16,
inference(forward_subsumption_resolution,[],[f701,f412]) ).
tff(f805,plain,
( ( sF13 = get(int,int,sF14,sF12) )
| ~ sort(int,sF13) ),
inference(superposition,[],[f334,f340]) ).
tff(f806,plain,
( ~ sort(int,sF20)
| ( sF20 = get(int,int,sF16,sF20) ) ),
inference(superposition,[],[f334,f442]) ).
tff(f807,plain,
( ( get(int,int,sF11,sF13) = sF12 )
| ~ sort(int,sF12) ),
inference(superposition,[],[f334,f443]) ).
tff(f809,plain,
sF13 = get(int,int,sF14,sF12),
inference(forward_subsumption_resolution,[],[f805,f373]) ).
tff(f810,plain,
sF20 = get(int,int,sF16,sF20),
inference(forward_subsumption_resolution,[],[f806,f375]) ).
tff(f811,plain,
get(int,int,sF11,sF13) = sF12,
inference(forward_subsumption_resolution,[],[f807,f372]) ).
tff(f1151,plain,
! [X0: uni] :
( ( sF12 = X0 )
| ( get(int,int,sF14,X0) = get(int,int,sF11,X0) )
| ~ sort(int,sF12)
| ~ sort(int,X0) ),
inference(superposition,[],[f284,f340]) ).
tff(f1152,plain,
! [X0: uni] :
( ~ sort(int,X0)
| ~ sort(int,sF20)
| ( get(int,int,sF14,X0) = get(int,int,sF16,X0) )
| ( sF20 = X0 ) ),
inference(superposition,[],[f284,f442]) ).
tff(f1155,plain,
! [X0: uni] :
( ~ sort(int,X0)
| ( get(int,int,sF14,X0) = get(int,int,sF16,X0) )
| ( sF20 = X0 ) ),
inference(forward_subsumption_resolution,[],[f1152,f375]) ).
tff(f1156,plain,
! [X0: uni] :
( ~ sort(int,X0)
| ( sF12 = X0 )
| ( get(int,int,sF14,X0) = get(int,int,sF11,X0) ) ),
inference(forward_subsumption_resolution,[],[f1151,f372]) ).
tff(f1158,plain,
! [X0: uni] :
( ( get(int,int,sF14,X0) = get(int,int,sF16,X0) )
| ( sF20 = X0 ) ),
inference(forward_subsumption_resolution,[],[f1155,f404]) ).
tff(f1159,plain,
! [X0: uni] :
( ( get(int,int,sF14,X0) = get(int,int,sF11,X0) )
| ( sF12 = X0 ) ),
inference(forward_subsumption_resolution,[],[f1156,f404]) ).
tff(f1320,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| $less(sK10(sF18),length(int,t2tb2(sF18))) ),
inference(resolution,[],[f328,f366]) ).
tff(f1333,definition,
( spl26_11
<=> $less(sK10(sF18),3) ),
introduced(definition,[new_symbols(definition,[spl26_11])],[avatar_definition]) ).
tff(f1335,plain,
( $less(sK10(sF18),3)
| ~ spl26_11 ),
inference(avatar_component_clause,[],[f1333]) ).
tff(f1337,definition,
( spl26_12
<=> $less(tb2t(get(int,int,elts(int,sF17),sF13)),3) ),
introduced(definition,[new_symbols(definition,[spl26_12])],[avatar_definition]) ).
tff(f1339,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF13)),3)
| spl26_12 ),
inference(avatar_component_clause,[],[f1337]) ).
tff(f1341,definition,
( spl26_13
<=> $less(tb2t(get(int,int,elts(int,sF17),sF13)),0) ),
introduced(definition,[new_symbols(definition,[spl26_13])],[avatar_definition]) ).
tff(f1343,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_13 ),
inference(avatar_component_clause,[],[f1341]) ).
tff(f1489,plain,
( ~ $less(3,$sum(sK10(sF18),1))
| ~ spl26_11 ),
inference(resolution,[],[f1335,f96]) ).
tff(f1490,plain,
( ~ $less(3,$sum(1,sK10(sF18)))
| ~ spl26_11 ),
inference(forward_demodulation,[],[f1489,f79]) ).
tff(f1491,plain,
( ~ $less(2,sK10(sF18))
| ~ spl26_11 ),
inference(cancellation,[],[f1490]) ).
tff(f1499,definition,
( spl26_16
<=> $less(sK10(sF18),2) ),
introduced(definition,[new_symbols(definition,[spl26_16])],[avatar_definition]) ).
tff(f1500,plain,
( ~ $less(sK10(sF18),2)
| spl26_16 ),
inference(avatar_component_clause,[],[f1499]) ).
tff(f1501,plain,
( $less(sK10(sF18),2)
| ~ spl26_16 ),
inference(avatar_component_clause,[],[f1499]) ).
tff(f1503,definition,
( spl26_17
<=> ( 2 = sK10(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl26_17])],[avatar_definition]) ).
tff(f1505,plain,
( ( 2 = sK10(sF18) )
| ~ spl26_17 ),
inference(avatar_component_clause,[],[f1503]) ).
tff(f1546,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))) )
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18))) ),
inference(resolution,[],[f329,f366]) ).
tff(f1549,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))) )
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1546,f468]) ).
tff(f1550,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))) )
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1549,f468]) ).
tff(f1551,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))) )
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1550,f339]) ).
tff(f1552,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))) )
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1551,f400]) ).
tff(f1553,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1552,f339]) ).
tff(f1554,plain,
( ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1553,f400]) ).
tff(f1555,plain,
( ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1554,f440]) ).
tff(f1556,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1555,f468]) ).
tff(f1557,plain,
( ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1556,f400]) ).
tff(f1558,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF13)),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1557,f339]) ).
tff(f1560,definition,
( spl26_22
<=> ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) ) ),
introduced(definition,[new_symbols(definition,[spl26_22])],[avatar_definition]) ).
tff(f1561,plain,
( ( tb2t(get(int,int,elts(int,sF17),sF13)) != tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| spl26_22 ),
inference(avatar_component_clause,[],[f1560]) ).
tff(f1562,plain,
( ( tb2t(get(int,int,elts(int,sF17),sF13)) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| ~ spl26_22 ),
inference(avatar_component_clause,[],[f1560]) ).
tff(f1563,plain,
( spl26_22
| ~ spl26_12
| spl26_13
| ~ spl26_2 ),
inference(avatar_split_clause,[],[f1558,f466,f1341,f1337,f1560]) ).
tff(f1566,plain,
( ~ $less(2,$sum(sK10(sF18),1))
| ~ spl26_16 ),
inference(resolution,[],[f1501,f96]) ).
tff(f1567,plain,
( ~ $less(2,$sum(1,sK10(sF18)))
| ~ spl26_16 ),
inference(forward_demodulation,[],[f1566,f79]) ).
tff(f1569,plain,
( ~ $less(1,sK10(sF18))
| ~ spl26_16 ),
inference(cancellation,[],[f1567]) ).
tff(f1574,definition,
( spl26_23
<=> ( 1 = sK10(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl26_23])],[avatar_definition]) ).
tff(f1576,plain,
( ( 1 = sK10(sF18) )
| ~ spl26_23 ),
inference(avatar_component_clause,[],[f1574]) ).
tff(f1578,definition,
( spl26_24
<=> $less(sK10(sF18),1) ),
introduced(definition,[new_symbols(definition,[spl26_24])],[avatar_definition]) ).
tff(f1580,plain,
( $less(sK10(sF18),1)
| ~ spl26_24 ),
inference(avatar_component_clause,[],[f1578]) ).
tff(f1592,definition,
( spl26_25
<=> $less(0,sK10(sF18)) ),
introduced(definition,[new_symbols(definition,[spl26_25])],[avatar_definition]) ).
tff(f1593,plain,
( ~ $less(0,sK10(sF18))
| spl26_25 ),
inference(avatar_component_clause,[],[f1592]) ).
tff(f1594,plain,
( $less(0,sK10(sF18))
| ~ spl26_25 ),
inference(avatar_component_clause,[],[f1592]) ).
tff(f1596,definition,
( spl26_26
<=> ( 0 = sK10(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl26_26])],[avatar_definition]) ).
tff(f1598,plain,
( ( 0 = sK10(sF18) )
| ~ spl26_26 ),
inference(avatar_component_clause,[],[f1596]) ).
tff(f1601,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))) ) ),
inference(forward_demodulation,[],[f1546,f400]) ).
tff(f1602,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| $less(sK10(sF18),length(int,t2tb2(sF18)))
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18))) ),
inference(forward_demodulation,[],[f1320,f400]) ).
tff(f1613,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))) )
| $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0) ),
inference(forward_demodulation,[],[f1601,f400]) ).
tff(f1614,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| $less(sK10(sF18),length(int,sF17)) ),
inference(forward_demodulation,[],[f1602,f400]) ).
tff(f1615,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ( tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK10(sF18)))) = tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))) ) ),
inference(forward_demodulation,[],[f1613,f440]) ).
tff(f1616,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| $less(sK10(sF18),length(int,sF17)) ),
inference(forward_demodulation,[],[f1614,f400]) ).
tff(f1617,plain,
( ( tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3) ),
inference(forward_demodulation,[],[f1615,f400]) ).
tff(f1618,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(sK10(sF18),length(int,sF17)) ),
inference(forward_demodulation,[],[f1616,f440]) ).
tff(f1620,definition,
( spl26_29
<=> $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0) ),
introduced(definition,[new_symbols(definition,[spl26_29])],[avatar_definition]) ).
tff(f1621,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| spl26_29 ),
inference(avatar_component_clause,[],[f1620]) ).
tff(f1622,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| ~ spl26_29 ),
inference(avatar_component_clause,[],[f1620]) ).
tff(f1624,definition,
( spl26_30
<=> $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3) ),
introduced(definition,[new_symbols(definition,[spl26_30])],[avatar_definition]) ).
tff(f1625,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_30 ),
inference(avatar_component_clause,[],[f1624]) ).
tff(f1626,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| spl26_30 ),
inference(avatar_component_clause,[],[f1624]) ).
tff(f1628,definition,
( spl26_31
<=> ( tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) ) ),
introduced(definition,[new_symbols(definition,[spl26_31])],[avatar_definition]) ).
tff(f1630,plain,
( ( tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))) = tb2t(get(int,int,elts(int,sF17),t2tb(sK10(sF18)))) )
| ~ spl26_31 ),
inference(avatar_component_clause,[],[f1628]) ).
tff(f1631,plain,
( spl26_29
| ~ spl26_30
| spl26_31 ),
inference(avatar_split_clause,[],[f1617,f1628,f1624,f1620]) ).
tff(f1632,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(sK10(sF18),3)
| $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0) ),
inference(forward_demodulation,[],[f1618,f440]) ).
tff(f1673,definition,
( spl26_35
<=> ( 2 = sK9(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl26_35])],[avatar_definition]) ).
tff(f1674,plain,
( ( 2 = sK9(sF18) )
| ~ spl26_35 ),
inference(avatar_component_clause,[],[f1673]) ).
tff(f1684,plain,
( ~ $less(sK9(sF18),$sum(0,1))
| ~ spl26_1 ),
inference(resolution,[],[f464,f96]) ).
tff(f1685,plain,
( ~ $less(sK9(sF18),1)
| ~ spl26_1 ),
inference(evaluation,[],[f1684]) ).
tff(f1690,definition,
( spl26_36
<=> ( 1 = sK9(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl26_36])],[avatar_definition]) ).
tff(f1692,plain,
( ( 1 = sK9(sF18) )
| ~ spl26_36 ),
inference(avatar_component_clause,[],[f1690]) ).
tff(f1694,definition,
( spl26_37
<=> $less(1,sK9(sF18)) ),
introduced(definition,[new_symbols(definition,[spl26_37])],[avatar_definition]) ).
tff(f1696,plain,
( $less(1,sK9(sF18))
| ~ spl26_37 ),
inference(avatar_component_clause,[],[f1694]) ).
tff(f1869,plain,
( ( sF13 = get(int,int,sF16,sF12) )
| ( sF20 = sF12 ) ),
inference(superposition,[],[f1158,f809]) ).
tff(f1872,definition,
( spl26_40
<=> ( sF20 = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl26_40])],[avatar_definition]) ).
tff(f1873,plain,
( ( sF20 != sF12 )
| spl26_40 ),
inference(avatar_component_clause,[],[f1872]) ).
tff(f1874,plain,
( ( sF20 = sF12 )
| ~ spl26_40 ),
inference(avatar_component_clause,[],[f1872]) ).
tff(f1876,definition,
( spl26_41
<=> ( sF13 = get(int,int,sF16,sF12) ) ),
introduced(definition,[new_symbols(definition,[spl26_41])],[avatar_definition]) ).
tff(f1878,plain,
( ( sF13 = get(int,int,sF16,sF12) )
| ~ spl26_41 ),
inference(avatar_component_clause,[],[f1876]) ).
tff(f1880,plain,
( spl26_41
| spl26_40 ),
inference(avatar_split_clause,[],[f1869,f1872,f1876]) ).
tff(f1884,plain,
( ( 2 = tb2t(sF20) )
| ~ spl26_40 ),
inference(superposition,[],[f386,f1874]) ).
tff(f1886,plain,
( ( 1 = 2 )
| ~ spl26_40 ),
inference(forward_demodulation,[],[f1884,f388]) ).
tff(f1887,plain,
( $false
| ~ spl26_40 ),
inference(evaluation,[],[f1886]) ).
tff(f1888,plain,
~ spl26_40,
inference(avatar_contradiction_clause,[],[f1887]) ).
tff(f1933,plain,
( $less(0,sK9(sF18))
| ( 0 = sK9(sF18) ) ),
inference(resolution,[],[f449,f366]) ).
tff(f2707,definition,
( spl26_46
<=> ( 0 = tb2t(get(int,int,sF16,sF13)) ) ),
introduced(definition,[new_symbols(definition,[spl26_46])],[avatar_definition]) ).
tff(f2709,plain,
( ( 0 = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_46 ),
inference(avatar_component_clause,[],[f2707]) ).
tff(f2720,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),0)
| $less(sK10(sF18),3)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f1632,f468]) ).
tff(f2721,plain,
( $less(tb2t(get(int,int,sF16,sF13)),0)
| ~ spl26_13 ),
inference(forward_demodulation,[],[f1343,f704]) ).
tff(f2727,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(sK10(sF18),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f2720,f339]) ).
tff(f2728,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(sK10(sF18),3)
| $less(tb2t(get(int,int,sF16,sF13)),0)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f2727,f704]) ).
tff(f2729,plain,
( $less(tb2t(get(int,int,sF16,sF13)),0)
| $less(sK10(sF18),3)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f2728,f468]) ).
tff(f2730,plain,
( $less(tb2t(get(int,int,sF16,sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF13)),3)
| $less(sK10(sF18),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f2729,f339]) ).
tff(f2731,plain,
( $less(tb2t(get(int,int,sF16,sF13)),0)
| $less(sK10(sF18),3)
| ~ $less(tb2t(get(int,int,sF16,sF13)),3)
| ~ spl26_2 ),
inference(forward_demodulation,[],[f2730,f704]) ).
tff(f2733,definition,
( spl26_50
<=> $less(tb2t(get(int,int,sF16,sF13)),3) ),
introduced(definition,[new_symbols(definition,[spl26_50])],[avatar_definition]) ).
tff(f2735,plain,
( ~ $less(tb2t(get(int,int,sF16,sF13)),3)
| spl26_50 ),
inference(avatar_component_clause,[],[f2733]) ).
tff(f2737,definition,
( spl26_51
<=> $less(tb2t(get(int,int,sF16,sF13)),0) ),
introduced(definition,[new_symbols(definition,[spl26_51])],[avatar_definition]) ).
tff(f2738,plain,
( ~ $less(tb2t(get(int,int,sF16,sF13)),0)
| spl26_51 ),
inference(avatar_component_clause,[],[f2737]) ).
tff(f2739,plain,
( $less(tb2t(get(int,int,sF16,sF13)),0)
| ~ spl26_51 ),
inference(avatar_component_clause,[],[f2737]) ).
tff(f2740,plain,
( ~ spl26_50
| spl26_11
| spl26_51
| ~ spl26_2 ),
inference(avatar_split_clause,[],[f2731,f466,f2737,f1333,f2733]) ).
tff(f2753,plain,
( ( 2 = sK10(sF18) )
| $less(sK10(sF18),2)
| ~ spl26_11 ),
inference(resolution,[],[f1491,f86]) ).
tff(f2756,plain,
( spl26_16
| spl26_17
| ~ spl26_11 ),
inference(avatar_split_clause,[],[f2753,f1333,f1503,f1499]) ).
tff(f2783,plain,
( spl26_51
| ~ spl26_13 ),
inference(avatar_split_clause,[],[f2721,f1341,f2737]) ).
tff(f2871,plain,
( ( t2tb(0) = get(int,int,sF16,sF13) )
| ~ spl26_46 ),
inference(superposition,[],[f301,f2709]) ).
tff(f2874,plain,
( ( get(int,int,sF16,sF13) = sF13 )
| ~ spl26_46 ),
inference(forward_demodulation,[],[f2871,f339]) ).
tff(f3434,plain,
( ( sF13 = sF12 )
| ( get(int,int,sF14,sF13) = sF12 ) ),
inference(superposition,[],[f1159,f811]) ).
tff(f3438,definition,
( spl26_78
<=> ( get(int,int,sF14,sF13) = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl26_78])],[avatar_definition]) ).
tff(f3440,plain,
( ( get(int,int,sF14,sF13) = sF12 )
| ~ spl26_78 ),
inference(avatar_component_clause,[],[f3438]) ).
tff(f3442,definition,
( spl26_79
<=> ( sF13 = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl26_79])],[avatar_definition]) ).
tff(f3443,plain,
( ( sF13 != sF12 )
| spl26_79 ),
inference(avatar_component_clause,[],[f3442]) ).
tff(f3444,plain,
( ( sF13 = sF12 )
| ~ spl26_79 ),
inference(avatar_component_clause,[],[f3442]) ).
tff(f3446,plain,
( spl26_78
| spl26_79 ),
inference(avatar_split_clause,[],[f3434,f3442,f3438]) ).
tff(f3451,definition,
( spl26_80
<=> ( sF20 = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl26_80])],[avatar_definition]) ).
tff(f3453,plain,
( ( sF20 = sF13 )
| ~ spl26_80 ),
inference(avatar_component_clause,[],[f3451]) ).
tff(f3455,definition,
( spl26_81
<=> ( get(int,int,sF16,sF13) = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl26_81])],[avatar_definition]) ).
tff(f3457,plain,
( ( get(int,int,sF16,sF13) = sF12 )
| ~ spl26_81 ),
inference(avatar_component_clause,[],[f3455]) ).
tff(f3463,plain,
( ( 2 = tb2t(sF13) )
| ~ spl26_79 ),
inference(superposition,[],[f386,f3444]) ).
tff(f3469,plain,
( ( 0 = 2 )
| ~ spl26_79 ),
inference(forward_demodulation,[],[f3463,f387]) ).
tff(f3470,plain,
( $false
| ~ spl26_79 ),
inference(evaluation,[],[f3469]) ).
tff(f3471,plain,
~ spl26_79,
inference(avatar_contradiction_clause,[],[f3470]) ).
tff(f3491,plain,
( ( get(int,int,sF16,sF13) = sF12 )
| ( sF20 = sF13 )
| ~ spl26_78 ),
inference(superposition,[],[f1158,f3440]) ).
tff(f3494,plain,
( spl26_81
| spl26_80
| ~ spl26_78 ),
inference(avatar_split_clause,[],[f3491,f3438,f3451,f3455]) ).
tff(f3498,plain,
( $less(tb2t(sF12),0)
| ~ spl26_51
| ~ spl26_81 ),
inference(superposition,[],[f2739,f3457]) ).
tff(f3534,plain,
( $less(2,0)
| ~ spl26_51
| ~ spl26_81 ),
inference(forward_demodulation,[],[f3498,f386]) ).
tff(f3535,plain,
( $false
| ~ spl26_51
| ~ spl26_81 ),
inference(evaluation,[],[f3534]) ).
tff(f3536,plain,
( ~ spl26_51
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f3535]) ).
tff(f3574,plain,
( ( 1 = tb2t(sF13) )
| ~ spl26_80 ),
inference(superposition,[],[f388,f3453]) ).
tff(f3576,plain,
( ( 0 = 1 )
| ~ spl26_80 ),
inference(forward_demodulation,[],[f3574,f387]) ).
tff(f3577,plain,
( $false
| ~ spl26_80 ),
inference(evaluation,[],[f3576]) ).
tff(f3578,plain,
~ spl26_80,
inference(avatar_contradiction_clause,[],[f3577]) ).
tff(f3581,plain,
( ( tb2t(get(int,int,elts(int,sF17),t2tb(2))) = tb2t(get(int,int,elts(int,sF17),sF13)) )
| ~ spl26_17
| ~ spl26_22 ),
inference(forward_demodulation,[],[f1562,f1505]) ).
tff(f3584,plain,
( ( tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))) = tb2t(get(int,int,elts(int,sF17),t2tb(2))) )
| ~ spl26_17
| ~ spl26_31 ),
inference(forward_demodulation,[],[f1630,f1505]) ).
tff(f3586,plain,
( ( tb2t(get(int,int,sF16,t2tb(2))) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_17
| ~ spl26_22 ),
inference(forward_demodulation,[],[f3581,f704]) ).
tff(f3588,plain,
( ( tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))) = tb2t(get(int,int,elts(int,sF17),sF12)) )
| ~ spl26_17
| ~ spl26_31 ),
inference(forward_demodulation,[],[f3584,f337]) ).
tff(f3589,plain,
( ( tb2t(get(int,int,sF16,sF12)) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_17
| ~ spl26_22 ),
inference(forward_demodulation,[],[f3586,f337]) ).
tff(f3591,plain,
( ( tb2t(get(int,int,sF16,sF12)) = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_17
| ~ spl26_31 ),
inference(forward_demodulation,[],[f3588,f704]) ).
tff(f3592,plain,
( ( tb2t(sF13) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_17
| ~ spl26_22
| ~ spl26_41 ),
inference(forward_demodulation,[],[f3589,f1878]) ).
tff(f3595,plain,
( ( 0 = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_17
| ~ spl26_22
| ~ spl26_41 ),
inference(forward_demodulation,[],[f3592,f387]) ).
tff(f3603,plain,
( spl26_46
| ~ spl26_17
| ~ spl26_22
| ~ spl26_41 ),
inference(avatar_split_clause,[],[f3595,f1876,f1560,f1503,f2707]) ).
tff(f3624,plain,
( ( sF13 = sF12 )
| ~ spl26_46
| ~ spl26_81 ),
inference(forward_demodulation,[],[f3457,f2874]) ).
tff(f3625,plain,
( $false
| ~ spl26_46
| spl26_79
| ~ spl26_81 ),
inference(forward_subsumption_resolution,[],[f3624,f3443]) ).
tff(f3626,plain,
( ~ spl26_46
| spl26_79
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f3625]) ).
tff(f3628,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_31 ),
inference(forward_demodulation,[],[f1630,f704]) ).
tff(f3629,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_22 ),
inference(forward_demodulation,[],[f1562,f704]) ).
tff(f3651,plain,
( ( tb2t(get(int,int,sF16,t2tb(1))) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_22
| ~ spl26_23 ),
inference(superposition,[],[f3629,f1576]) ).
tff(f3652,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| is_permutation(sF18)
| ( 1 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| ~ spl26_23 ),
inference(superposition,[],[f326,f1576]) ).
tff(f3654,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),0)
| is_permutation(sF18)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),length(int,t2tb2(sF18)))
| ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(inner_rewriting,[],[f3652]) ).
tff(f3655,plain,
( ( tb2t(get(int,int,sF16,sF20)) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_22
| ~ spl26_23 ),
inference(forward_demodulation,[],[f3651,f352]) ).
tff(f3656,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),length(int,t2tb2(sF18)))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),0)
| ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(forward_subsumption_resolution,[],[f3654,f366]) ).
tff(f3657,plain,
( ( tb2t(sF20) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_22
| ~ spl26_23 ),
inference(forward_demodulation,[],[f3655,f810]) ).
tff(f3658,plain,
( ( 1 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),0)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f3656,f400]) ).
tff(f3659,plain,
( ( 1 = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_22
| ~ spl26_23 ),
inference(forward_demodulation,[],[f3657,f388]) ).
tff(f4073,plain,
( ( 1 = tb2t(sF12) )
| ~ spl26_22
| ~ spl26_23
| ~ spl26_81 ),
inference(forward_demodulation,[],[f3659,f3457]) ).
tff(f4152,plain,
( ( t2tb(1) = sF12 )
| ~ spl26_22
| ~ spl26_23
| ~ spl26_81 ),
inference(superposition,[],[f301,f4073]) ).
tff(f4157,plain,
( ( sF20 = sF12 )
| ~ spl26_22
| ~ spl26_23
| ~ spl26_81 ),
inference(forward_demodulation,[],[f4152,f352]) ).
tff(f4158,plain,
( $false
| ~ spl26_22
| ~ spl26_23
| spl26_40
| ~ spl26_81 ),
inference(forward_subsumption_resolution,[],[f4157,f1873]) ).
tff(f4159,plain,
( ~ spl26_22
| ~ spl26_23
| spl26_40
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f4158]) ).
tff(f4160,plain,
( ( tb2t(get(int,int,sF16,t2tb(1))) = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_23
| ~ spl26_31 ),
inference(forward_demodulation,[],[f3628,f1576]) ).
tff(f4165,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(forward_demodulation,[],[f3658,f440]) ).
tff(f4171,plain,
( spl26_2
| spl26_1 ),
inference(avatar_split_clause,[],[f1933,f462,f466]) ).
tff(f4172,plain,
( $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),3)
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1625,f704]) ).
tff(f4173,plain,
( ~ $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),0)
| spl26_29 ),
inference(forward_demodulation,[],[f1621,f704]) ).
tff(f4174,plain,
( ( tb2t(get(int,int,sF16,sF20)) = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_23
| ~ spl26_31 ),
inference(forward_demodulation,[],[f4160,f352]) ).
tff(f4175,plain,
( ( 1 != sK9(sF18) )
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF20)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4165,f352]) ).
tff(f4177,plain,
( ( tb2t(sF20) = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_23
| ~ spl26_31 ),
inference(forward_demodulation,[],[f4174,f810]) ).
tff(f4178,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF20)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4175,f400]) ).
tff(f4180,plain,
( ( 1 = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_23
| ~ spl26_31 ),
inference(forward_demodulation,[],[f4177,f388]) ).
tff(f4181,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| ( 1 != sK9(sF18) )
| $less(tb2t(get(int,int,sF16,sF20)),0)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4178,f704]) ).
tff(f4183,plain,
( ( 1 != sK9(sF18) )
| $less(tb2t(get(int,int,sF16,sF20)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4181,f352]) ).
tff(f4185,plain,
( ( 1 != sK9(sF18) )
| $less(tb2t(sF20),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4183,f810]) ).
tff(f4187,plain,
( $less(1,0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4185,f388]) ).
tff(f4188,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(evaluation,[],[f4187]) ).
tff(f4190,plain,
( ( 1 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,sF16,sF20)),3)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4188,f704]) ).
tff(f4191,plain,
( ( 1 != sK9(sF18) )
| ~ $less(tb2t(sF20),3)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4190,f810]) ).
tff(f4192,plain,
( ( 1 != sK9(sF18) )
| ~ $less(1,3)
| ~ spl26_23 ),
inference(forward_demodulation,[],[f4191,f388]) ).
tff(f4193,plain,
( ( 1 != sK9(sF18) )
| ~ spl26_23 ),
inference(evaluation,[],[f4192]) ).
tff(f4194,plain,
( ~ spl26_36
| ~ spl26_23 ),
inference(avatar_split_clause,[],[f4193,f1574,f1690]) ).
tff(f4338,plain,
( ~ $less(sK9(sF18),$sum(1,1))
| ~ spl26_37 ),
inference(resolution,[],[f1696,f96]) ).
tff(f4339,plain,
( ~ $less(sK9(sF18),2)
| ~ spl26_37 ),
inference(evaluation,[],[f4338]) ).
tff(f4347,plain,
( ( 2 = sK9(sF18) )
| $less(2,sK9(sF18))
| ~ spl26_37 ),
inference(resolution,[],[f4339,f86]) ).
tff(f4350,definition,
( spl26_90
<=> $less(2,sK9(sF18)) ),
introduced(definition,[new_symbols(definition,[spl26_90])],[avatar_definition]) ).
tff(f4352,plain,
( $less(2,sK9(sF18))
| ~ spl26_90 ),
inference(avatar_component_clause,[],[f4350]) ).
tff(f4361,plain,
( spl26_90
| spl26_35
| ~ spl26_37 ),
inference(avatar_split_clause,[],[f4347,f1694,f1673,f4350]) ).
tff(f4379,plain,
( ~ $less(sK9(sF18),$sum(2,1))
| ~ spl26_90 ),
inference(resolution,[],[f4352,f96]) ).
tff(f4380,plain,
( ~ $less(sK9(sF18),3)
| ~ spl26_90 ),
inference(evaluation,[],[f4379]) ).
tff(f4381,plain,
( $false
| ~ spl26_90 ),
inference(forward_subsumption_resolution,[],[f4380,f483]) ).
tff(f4382,plain,
~ spl26_90,
inference(avatar_contradiction_clause,[],[f4381]) ).
tff(f4434,plain,
( ( 1 = tb2t(get(int,int,sF16,t2tb(2))) )
| ~ spl26_23
| ~ spl26_31
| ~ spl26_35 ),
inference(superposition,[],[f4180,f1674]) ).
tff(f4438,plain,
( ( 1 = tb2t(get(int,int,sF16,sF12)) )
| ~ spl26_23
| ~ spl26_31
| ~ spl26_35 ),
inference(forward_demodulation,[],[f4434,f337]) ).
tff(f4441,plain,
( ( 1 = tb2t(sF13) )
| ~ spl26_23
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4438,f1878]) ).
tff(f4444,plain,
( ( 0 = 1 )
| ~ spl26_23
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4441,f387]) ).
tff(f4445,plain,
( $false
| ~ spl26_23
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41 ),
inference(evaluation,[],[f4444]) ).
tff(f4446,plain,
( ~ spl26_23
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41 ),
inference(avatar_contradiction_clause,[],[f4445]) ).
tff(f4448,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),3)
| spl26_30
| ~ spl26_35 ),
inference(forward_demodulation,[],[f1626,f1674]) ).
tff(f4451,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| spl26_30
| ~ spl26_35 ),
inference(forward_demodulation,[],[f4448,f337]) ).
tff(f4454,plain,
( ~ $less(tb2t(get(int,int,sF16,sF12)),3)
| spl26_30
| ~ spl26_35 ),
inference(forward_demodulation,[],[f4451,f704]) ).
tff(f4457,plain,
( ~ $less(tb2t(sF13),3)
| spl26_30
| ~ spl26_35
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4454,f1878]) ).
tff(f4460,plain,
( ~ $less(0,3)
| spl26_30
| ~ spl26_35
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4457,f387]) ).
tff(f4461,plain,
( $false
| spl26_30
| ~ spl26_35
| ~ spl26_41 ),
inference(evaluation,[],[f4460]) ).
tff(f4462,plain,
( spl26_30
| ~ spl26_35
| ~ spl26_41 ),
inference(avatar_contradiction_clause,[],[f4461]) ).
tff(f4472,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),0)
| ~ spl26_29
| ~ spl26_35 ),
inference(forward_demodulation,[],[f1622,f1674]) ).
tff(f4477,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF12)),0)
| ~ spl26_29
| ~ spl26_35 ),
inference(forward_demodulation,[],[f4472,f337]) ).
tff(f4481,plain,
( $less(tb2t(get(int,int,sF16,sF12)),0)
| ~ spl26_29
| ~ spl26_35 ),
inference(forward_demodulation,[],[f4477,f704]) ).
tff(f4485,plain,
( $less(tb2t(sF13),0)
| ~ spl26_29
| ~ spl26_35
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4481,f1878]) ).
tff(f4488,plain,
( $less(0,0)
| ~ spl26_29
| ~ spl26_35
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4485,f387]) ).
tff(f4489,plain,
( $false
| ~ spl26_29
| ~ spl26_35
| ~ spl26_41 ),
inference(evaluation,[],[f4488]) ).
tff(f4490,plain,
( ~ spl26_29
| ~ spl26_35
| ~ spl26_41 ),
inference(avatar_contradiction_clause,[],[f4489]) ).
tff(f4493,plain,
( ~ $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),3)
| spl26_30 ),
inference(forward_demodulation,[],[f1626,f704]) ).
tff(f4495,plain,
( ~ $less(tb2t(sF12),3)
| spl26_50
| ~ spl26_81 ),
inference(forward_demodulation,[],[f2735,f3457]) ).
tff(f4497,plain,
( ~ $less(tb2t(get(int,int,sF16,sF13)),3)
| spl26_12 ),
inference(forward_demodulation,[],[f1339,f704]) ).
tff(f4506,plain,
( ~ $less(2,3)
| spl26_50
| ~ spl26_81 ),
inference(forward_demodulation,[],[f4495,f386]) ).
tff(f4507,plain,
( $false
| spl26_50
| ~ spl26_81 ),
inference(evaluation,[],[f4506]) ).
tff(f4508,plain,
( spl26_50
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f4507]) ).
tff(f4509,plain,
( ~ $less(tb2t(sF12),3)
| spl26_12
| ~ spl26_81 ),
inference(forward_demodulation,[],[f4497,f3457]) ).
tff(f4520,plain,
( ~ $less(2,3)
| spl26_12
| ~ spl26_81 ),
inference(forward_demodulation,[],[f4509,f386]) ).
tff(f4521,plain,
( $false
| spl26_12
| ~ spl26_81 ),
inference(evaluation,[],[f4520]) ).
tff(f4522,plain,
( spl26_12
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f4521]) ).
tff(f4527,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) != tb2t(get(int,int,sF16,sF13)) )
| spl26_22 ),
inference(forward_demodulation,[],[f1561,f704]) ).
tff(f4540,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) != tb2t(sF12) )
| spl26_22
| ~ spl26_81 ),
inference(forward_demodulation,[],[f4527,f3457]) ).
tff(f4547,plain,
( ( 2 != tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) )
| spl26_22
| ~ spl26_81 ),
inference(forward_demodulation,[],[f4540,f386]) ).
tff(f4550,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),0)
| $less(sK10(sF18),3)
| ~ $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),3) ),
inference(forward_demodulation,[],[f1632,f704]) ).
tff(f4551,plain,
( $less(sK10(sF18),3)
| $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),3) ),
inference(forward_demodulation,[],[f4550,f704]) ).
tff(f4553,definition,
( spl26_94
<=> $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),3) ),
introduced(definition,[new_symbols(definition,[spl26_94])],[avatar_definition]) ).
tff(f4555,plain,
( ~ $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),3)
| spl26_94 ),
inference(avatar_component_clause,[],[f4553]) ).
tff(f4557,definition,
( spl26_95
<=> $less(tb2t(get(int,int,sF16,t2tb(sK9(sF18)))),0) ),
introduced(definition,[new_symbols(definition,[spl26_95])],[avatar_definition]) ).
tff(f4560,plain,
( ~ spl26_94
| spl26_11
| spl26_95 ),
inference(avatar_split_clause,[],[f4551,f4557,f1333,f4553]) ).
tff(f4576,plain,
( ~ spl26_95
| spl26_29 ),
inference(avatar_split_clause,[],[f4173,f1620,f4557]) ).
tff(f4585,plain,
( $less(2,sK10(sF18))
| ( 2 = sK10(sF18) )
| spl26_16 ),
inference(resolution,[],[f1500,f86]) ).
tff(f4589,definition,
( spl26_97
<=> $less(2,sK10(sF18)) ),
introduced(definition,[new_symbols(definition,[spl26_97])],[avatar_definition]) ).
tff(f4592,plain,
( spl26_97
| spl26_17
| spl26_16 ),
inference(avatar_split_clause,[],[f4585,f1499,f1503,f4589]) ).
tff(f4603,plain,
( ( 2 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| is_permutation(sF18)
| ~ spl26_17 ),
inference(superposition,[],[f326,f1505]) ).
tff(f4609,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),0)
| ( 2 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),length(int,t2tb2(sF18)))
| is_permutation(sF18)
| ~ spl26_17 ),
inference(inner_rewriting,[],[f4603]) ).
tff(f4610,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),length(int,t2tb2(sF18)))
| ( 2 != sK9(sF18) )
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),0)
| ~ spl26_17 ),
inference(forward_subsumption_resolution,[],[f4609,f366]) ).
tff(f4611,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),0)
| ( 2 != sK9(sF18) )
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4610,f400]) ).
tff(f4612,plain,
( ( 2 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),3)
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),0)
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4611,f440]) ).
tff(f4613,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ( 2 != sK9(sF18) )
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4612,f337]) ).
tff(f4614,plain,
( ( 2 != sK9(sF18) )
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF12)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4613,f337]) ).
tff(f4615,plain,
( ( 2 != sK9(sF18) )
| $less(tb2t(get(int,int,elts(int,sF17),sF12)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4614,f400]) ).
tff(f4616,plain,
( ( 2 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| $less(tb2t(get(int,int,sF16,sF12)),0)
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4615,f704]) ).
tff(f4617,plain,
( ( 2 != sK9(sF18) )
| $less(tb2t(get(int,int,sF16,sF12)),0)
| ~ $less(tb2t(get(int,int,sF16,sF12)),3)
| ~ spl26_17 ),
inference(forward_demodulation,[],[f4616,f704]) ).
tff(f4618,plain,
( ( 2 != sK9(sF18) )
| $less(tb2t(sF13),0)
| ~ $less(tb2t(get(int,int,sF16,sF12)),3)
| ~ spl26_17
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4617,f1878]) ).
tff(f4619,plain,
( $less(0,0)
| ( 2 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,sF16,sF12)),3)
| ~ spl26_17
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4618,f387]) ).
tff(f4620,plain,
( ( 2 != sK9(sF18) )
| ~ $less(tb2t(get(int,int,sF16,sF12)),3)
| ~ spl26_17
| ~ spl26_41 ),
inference(evaluation,[],[f4619]) ).
tff(f4621,plain,
( ~ $less(tb2t(sF13),3)
| ( 2 != sK9(sF18) )
| ~ spl26_17
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4620,f1878]) ).
tff(f4622,plain,
( ~ $less(0,3)
| ( 2 != sK9(sF18) )
| ~ spl26_17
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4621,f387]) ).
tff(f4623,plain,
( ( 2 != sK9(sF18) )
| ~ spl26_17
| ~ spl26_41 ),
inference(evaluation,[],[f4622]) ).
tff(f4624,plain,
( ~ spl26_35
| ~ spl26_17
| ~ spl26_41 ),
inference(avatar_split_clause,[],[f4623,f1876,f1503,f1673]) ).
tff(f4650,plain,
( ~ spl26_94
| spl26_30 ),
inference(avatar_split_clause,[],[f4493,f1624,f4553]) ).
tff(f4764,plain,
( ( 1 = sK9(sF18) )
| $less(1,sK9(sF18))
| ~ spl26_1 ),
inference(resolution,[],[f1685,f86]) ).
tff(f4766,plain,
( spl26_37
| spl26_36
| ~ spl26_1 ),
inference(avatar_split_clause,[],[f4764,f462,f1690,f1694]) ).
tff(f4796,plain,
( ~ $less(tb2t(get(int,int,sF16,t2tb(1))),3)
| ~ spl26_36
| spl26_94 ),
inference(superposition,[],[f4555,f1692]) ).
tff(f4799,plain,
( ~ $less(tb2t(get(int,int,sF16,sF20)),3)
| ~ spl26_36
| spl26_94 ),
inference(forward_demodulation,[],[f4796,f352]) ).
tff(f4801,plain,
( ~ $less(tb2t(sF20),3)
| ~ spl26_36
| spl26_94 ),
inference(forward_demodulation,[],[f4799,f810]) ).
tff(f4803,plain,
( ~ $less(1,3)
| ~ spl26_36
| spl26_94 ),
inference(forward_demodulation,[],[f4801,f388]) ).
tff(f4804,plain,
( $false
| ~ spl26_36
| spl26_94 ),
inference(evaluation,[],[f4803]) ).
tff(f4805,plain,
( ~ spl26_36
| spl26_94 ),
inference(avatar_contradiction_clause,[],[f4804]) ).
tff(f4811,plain,
( $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),0)
| ~ spl26_29
| ~ spl26_36 ),
inference(forward_demodulation,[],[f1622,f1692]) ).
tff(f4823,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF20)),0)
| ~ spl26_29
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4811,f352]) ).
tff(f4828,plain,
( $less(tb2t(get(int,int,sF16,sF20)),0)
| ~ spl26_29
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4823,f704]) ).
tff(f4833,plain,
( $less(tb2t(sF20),0)
| ~ spl26_29
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4828,f810]) ).
tff(f4838,plain,
( $less(1,0)
| ~ spl26_29
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4833,f388]) ).
tff(f4839,plain,
( $false
| ~ spl26_29
| ~ spl26_36 ),
inference(evaluation,[],[f4838]) ).
tff(f4840,plain,
( ~ spl26_29
| ~ spl26_36 ),
inference(avatar_contradiction_clause,[],[f4839]) ).
tff(f4842,plain,
( ~ spl26_97
| ~ spl26_11 ),
inference(avatar_split_clause,[],[f1491,f1333,f4589]) ).
tff(f4846,plain,
( ( tb2t(get(int,int,sF16,sF12)) = tb2t(get(int,int,sF16,t2tb(1))) )
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f3591,f1692]) ).
tff(f4847,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(get(int,int,sF16,t2tb(1))) )
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f3628,f1692]) ).
tff(f4851,plain,
( ( tb2t(get(int,int,sF16,sF12)) = tb2t(get(int,int,sF16,sF20)) )
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4846,f352]) ).
tff(f4852,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(get(int,int,sF16,sF20)) )
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4847,f352]) ).
tff(f4856,plain,
( ( tb2t(get(int,int,sF16,sF12)) = tb2t(sF20) )
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4851,f810]) ).
tff(f4857,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(sF20) )
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4852,f810]) ).
tff(f4861,plain,
( ( 1 = tb2t(get(int,int,sF16,sF12)) )
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4856,f388]) ).
tff(f4862,plain,
( ( 1 = tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) )
| ~ spl26_31
| ~ spl26_36 ),
inference(forward_demodulation,[],[f4857,f388]) ).
tff(f4865,plain,
( ( 1 = tb2t(sF13) )
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4861,f1878]) ).
tff(f4866,plain,
( ( 0 = 1 )
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36
| ~ spl26_41 ),
inference(forward_demodulation,[],[f4865,f387]) ).
tff(f4867,plain,
( $false
| ~ spl26_17
| ~ spl26_31
| ~ spl26_36
| ~ spl26_41 ),
inference(evaluation,[],[f4866]) ).
tff(f4868,plain,
( ~ spl26_17
| ~ spl26_31
| ~ spl26_36
| ~ spl26_41 ),
inference(avatar_contradiction_clause,[],[f4867]) ).
tff(f4917,plain,
( ( 1 = sK10(sF18) )
| $less(sK10(sF18),1)
| ~ spl26_16 ),
inference(resolution,[],[f1569,f86]) ).
tff(f4925,plain,
( spl26_23
| spl26_24
| ~ spl26_16 ),
inference(avatar_split_clause,[],[f4917,f1499,f1578,f1574]) ).
tff(f5033,plain,
( ~ $less(sK10(sF18),$sum(0,1))
| ~ spl26_25 ),
inference(resolution,[],[f1594,f96]) ).
tff(f5034,plain,
( ~ $less(sK10(sF18),1)
| ~ spl26_25 ),
inference(evaluation,[],[f5033]) ).
tff(f5036,plain,
( $false
| ~ spl26_24
| ~ spl26_25 ),
inference(forward_subsumption_resolution,[],[f5034,f1580]) ).
tff(f5037,plain,
( ~ spl26_24
| ~ spl26_25 ),
inference(avatar_contradiction_clause,[],[f5036]) ).
tff(f5041,plain,
( ( 0 = sK10(sF18) )
| $less(sK10(sF18),0)
| spl26_25 ),
inference(resolution,[],[f1593,f86]) ).
tff(f5045,definition,
( spl26_111
<=> $less(sK10(sF18),0) ),
introduced(definition,[new_symbols(definition,[spl26_111])],[avatar_definition]) ).
tff(f5047,plain,
( $less(sK10(sF18),0)
| ~ spl26_111 ),
inference(avatar_component_clause,[],[f5045]) ).
tff(f5048,plain,
( spl26_111
| spl26_26
| spl26_25 ),
inference(avatar_split_clause,[],[f5041,f1592,f1596,f5045]) ).
tff(f5082,plain,
( ( 2 != tb2t(get(int,int,sF16,t2tb(0))) )
| spl26_22
| ~ spl26_26
| ~ spl26_81 ),
inference(superposition,[],[f4547,f1598]) ).
tff(f5090,plain,
( ( 2 != tb2t(get(int,int,sF16,sF13)) )
| spl26_22
| ~ spl26_26
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5082,f339]) ).
tff(f5092,plain,
( ( 2 != tb2t(sF12) )
| spl26_22
| ~ spl26_26
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5090,f3457]) ).
tff(f5094,plain,
( $false
| spl26_22
| ~ spl26_26
| ~ spl26_81 ),
inference(forward_subsumption_resolution,[],[f5092,f386]) ).
tff(f5095,plain,
( spl26_22
| ~ spl26_26
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f5094]) ).
tff(f5151,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| is_permutation(sF18)
| ~ spl26_111 ),
inference(resolution,[],[f5047,f327]) ).
tff(f5158,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ spl26_111 ),
inference(forward_subsumption_resolution,[],[f5151,f366]) ).
tff(f5160,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5158,f400]) ).
tff(f5161,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),0)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5160,f1692]) ).
tff(f5162,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(1))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5161,f440]) ).
tff(f5163,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF20)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5162,f352]) ).
tff(f5164,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(tb2t(get(int,int,elts(int,sF17),sF20)),0)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5163,f400]) ).
tff(f5165,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF20)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5164,f1692]) ).
tff(f5166,plain,
( $less(tb2t(get(int,int,sF16,sF20)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5165,f704]) ).
tff(f5167,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(1))),3)
| $less(tb2t(sF20),0)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5166,f810]) ).
tff(f5168,plain,
( $less(tb2t(sF20),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5167,f352]) ).
tff(f5169,plain,
( $less(1,0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5168,f388]) ).
tff(f5170,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF20)),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(evaluation,[],[f5169]) ).
tff(f5171,plain,
( ~ $less(tb2t(get(int,int,sF16,sF20)),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5170,f704]) ).
tff(f5172,plain,
( ~ $less(tb2t(sF20),3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5171,f810]) ).
tff(f5173,plain,
( ~ $less(1,3)
| ~ spl26_36
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5172,f388]) ).
tff(f5174,plain,
( $false
| ~ spl26_36
| ~ spl26_111 ),
inference(evaluation,[],[f5173]) ).
tff(f5175,plain,
( ~ spl26_36
| ~ spl26_111 ),
inference(avatar_contradiction_clause,[],[f5174]) ).
tff(f5177,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_22 ),
inference(forward_demodulation,[],[f1562,f704]) ).
tff(f5180,plain,
( ( tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) = tb2t(sF12) )
| ~ spl26_22
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5177,f3457]) ).
tff(f5182,plain,
( ( 2 = tb2t(get(int,int,sF16,t2tb(sK10(sF18)))) )
| ~ spl26_22
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5180,f386]) ).
tff(f5186,plain,
( ( 1 = 2 )
| ~ spl26_22
| ~ spl26_31
| ~ spl26_36
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5182,f4862]) ).
tff(f5187,plain,
( $false
| ~ spl26_22
| ~ spl26_31
| ~ spl26_36
| ~ spl26_81 ),
inference(evaluation,[],[f5186]) ).
tff(f5188,plain,
( ~ spl26_22
| ~ spl26_31
| ~ spl26_36
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f5187]) ).
tff(f5196,plain,
( spl26_94
| ~ spl26_30 ),
inference(avatar_split_clause,[],[f4172,f1624,f4553]) ).
tff(f5228,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| is_permutation(sF18)
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ spl26_111 ),
inference(resolution,[],[f5047,f327]) ).
tff(f5234,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ spl26_111 ),
inference(forward_subsumption_resolution,[],[f5228,f366]) ).
tff(f5236,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5234,f400]) ).
tff(f5237,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5236,f440]) ).
tff(f5238,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(2))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_35
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5237,f1674]) ).
tff(f5239,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF12)),0)
| ~ spl26_35
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5238,f337]) ).
tff(f5240,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF12)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),3)
| ~ spl26_35
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5239,f1674]) ).
tff(f5241,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF12)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),3)
| ~ spl26_35
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5240,f400]) ).
tff(f5242,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(2))),3)
| $less(tb2t(get(int,int,sF16,sF12)),0)
| ~ spl26_35
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5241,f704]) ).
tff(f5243,plain,
( $less(tb2t(get(int,int,sF16,sF12)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ~ spl26_35
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5242,f337]) ).
tff(f5244,plain,
( $less(tb2t(sF13),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5243,f1878]) ).
tff(f5245,plain,
( $less(0,0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5244,f387]) ).
tff(f5246,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF12)),3)
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(evaluation,[],[f5245]) ).
tff(f5247,plain,
( ~ $less(tb2t(get(int,int,sF16,sF12)),3)
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5246,f704]) ).
tff(f5248,plain,
( ~ $less(tb2t(sF13),3)
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5247,f1878]) ).
tff(f5249,plain,
( ~ $less(0,3)
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5248,f387]) ).
tff(f5250,plain,
( $false
| ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(evaluation,[],[f5249]) ).
tff(f5251,plain,
( ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(avatar_contradiction_clause,[],[f5250]) ).
tff(f5269,plain,
( ( tb2t(get(int,int,sF16,t2tb(0))) = tb2t(get(int,int,sF16,t2tb(sK9(sF18)))) )
| ~ spl26_26
| ~ spl26_31 ),
inference(superposition,[],[f3628,f1598]) ).
tff(f5276,plain,
( ( tb2t(get(int,int,sF16,t2tb(2))) = tb2t(get(int,int,sF16,t2tb(0))) )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35 ),
inference(forward_demodulation,[],[f5269,f1674]) ).
tff(f5277,plain,
( ( tb2t(get(int,int,sF16,t2tb(2))) = tb2t(get(int,int,sF16,sF13)) )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35 ),
inference(forward_demodulation,[],[f5276,f339]) ).
tff(f5278,plain,
( ( tb2t(get(int,int,sF16,t2tb(2))) = tb2t(sF12) )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5277,f3457]) ).
tff(f5279,plain,
( ( 2 = tb2t(get(int,int,sF16,t2tb(2))) )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5278,f386]) ).
tff(f5280,plain,
( ( 2 = tb2t(get(int,int,sF16,sF12)) )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5279,f337]) ).
tff(f5281,plain,
( ( 2 = tb2t(sF13) )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5280,f1878]) ).
tff(f5282,plain,
( ( 0 = 2 )
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5281,f387]) ).
tff(f5283,plain,
( $false
| ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41
| ~ spl26_81 ),
inference(evaluation,[],[f5282]) ).
tff(f5284,plain,
( ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f5283]) ).
tff(f5327,plain,
( is_permutation(sF18)
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| ~ spl26_111 ),
inference(resolution,[],[f5047,f327]) ).
tff(f5333,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ spl26_111 ),
inference(forward_subsumption_resolution,[],[f5327,f366]) ).
tff(f5335,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5333,f400]) ).
tff(f5336,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),length(int,sF17))
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),0)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5335,f468]) ).
tff(f5337,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5336,f440]) ).
tff(f5338,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5337,f339]) ).
tff(f5339,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(sK9(sF18)))),3)
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5338,f400]) ).
tff(f5340,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),3)
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5339,f468]) ).
tff(f5341,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF13)),3)
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5340,f339]) ).
tff(f5342,plain,
( ~ $less(tb2t(get(int,int,sF16,sF13)),3)
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5341,f704]) ).
tff(f5343,plain,
( ~ $less(tb2t(sF12),3)
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_81
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5342,f3457]) ).
tff(f5344,plain,
( ~ $less(2,3)
| $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_81
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5343,f386]) ).
tff(f5345,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ spl26_2
| ~ spl26_81
| ~ spl26_111 ),
inference(evaluation,[],[f5344]) ).
tff(f5346,plain,
( $less(tb2t(get(int,int,sF16,sF13)),0)
| ~ spl26_2
| ~ spl26_81
| ~ spl26_111 ),
inference(forward_demodulation,[],[f5345,f704]) ).
tff(f5347,plain,
( $false
| ~ spl26_2
| spl26_51
| ~ spl26_81
| ~ spl26_111 ),
inference(forward_subsumption_resolution,[],[f5346,f2738]) ).
tff(f5348,plain,
( ~ spl26_2
| spl26_51
| ~ spl26_81
| ~ spl26_111 ),
inference(avatar_contradiction_clause,[],[f5347]) ).
tff(f5373,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),length(int,t2tb2(sF18)))
| is_permutation(sF18)
| $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(sK9(sF18)))),0)
| ( 0 != sK9(sF18) )
| ~ spl26_26 ),
inference(superposition,[],[f326,f1598]) ).
tff(f5375,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),0)
| ( 0 != sK9(sF18) )
| is_permutation(sF18)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| ~ spl26_26 ),
inference(inner_rewriting,[],[f5373]) ).
tff(f5377,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),0)
| is_permutation(sF18)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| ~ spl26_2
| ~ spl26_26 ),
inference(forward_subsumption_resolution,[],[f5375,f468]) ).
tff(f5379,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| ~ spl26_2
| ~ spl26_26 ),
inference(forward_subsumption_resolution,[],[f5377,f366]) ).
tff(f5380,plain,
( $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| ~ spl26_2
| ~ spl26_26 ),
inference(forward_demodulation,[],[f5379,f339]) ).
tff(f5381,plain,
( $less(tb2t(get(int,int,elts(int,sF17),sF13)),0)
| ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| ~ spl26_2
| ~ spl26_26 ),
inference(forward_demodulation,[],[f5380,f400]) ).
tff(f5382,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| $less(tb2t(get(int,int,sF16,sF13)),0)
| ~ spl26_2
| ~ spl26_26 ),
inference(forward_demodulation,[],[f5381,f704]) ).
tff(f5383,plain,
( ~ $less(tb2t(get(int,int,elts(int,t2tb2(sF18)),t2tb(0))),length(int,t2tb2(sF18)))
| ~ spl26_2
| ~ spl26_26
| spl26_51 ),
inference(forward_subsumption_resolution,[],[f5382,f2738]) ).
tff(f5384,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),length(int,sF17))
| ~ spl26_2
| ~ spl26_26
| spl26_51 ),
inference(forward_demodulation,[],[f5383,f400]) ).
tff(f5385,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),t2tb(0))),3)
| ~ spl26_2
| ~ spl26_26
| spl26_51 ),
inference(forward_demodulation,[],[f5384,f440]) ).
tff(f5386,plain,
( ~ $less(tb2t(get(int,int,elts(int,sF17),sF13)),3)
| ~ spl26_2
| ~ spl26_26
| spl26_51 ),
inference(forward_demodulation,[],[f5385,f339]) ).
tff(f5387,plain,
( ~ $less(tb2t(get(int,int,sF16,sF13)),3)
| ~ spl26_2
| ~ spl26_26
| spl26_51 ),
inference(forward_demodulation,[],[f5386,f704]) ).
tff(f5388,plain,
( ~ $less(tb2t(sF12),3)
| ~ spl26_2
| ~ spl26_26
| spl26_51
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5387,f3457]) ).
tff(f5389,plain,
( ~ $less(2,3)
| ~ spl26_2
| ~ spl26_26
| spl26_51
| ~ spl26_81 ),
inference(forward_demodulation,[],[f5388,f386]) ).
tff(f5390,plain,
( $false
| ~ spl26_2
| ~ spl26_26
| spl26_51
| ~ spl26_81 ),
inference(evaluation,[],[f5389]) ).
tff(f5391,plain,
( ~ spl26_2
| ~ spl26_26
| spl26_51
| ~ spl26_81 ),
inference(avatar_contradiction_clause,[],[f5390]) ).
cnf(s13,plain,
( ~ spl26_2
| ~ spl26_12
| spl26_13
| spl26_22 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s18,plain,
( spl26_29
| ~ spl26_30
| spl26_31 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s32,plain,
( spl26_40
| spl26_41 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s33,plain,
~ spl26_40,
inference(sat_conversion,[],[f1888]) ).
cnf(s41,plain,
( ~ spl26_2
| spl26_11
| ~ spl26_50
| spl26_51 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s47,plain,
( ~ spl26_11
| spl26_16
| spl26_17 ),
inference(sat_conversion,[],[f2756]) ).
cnf(s52,plain,
( ~ spl26_13
| spl26_51 ),
inference(sat_conversion,[],[f2783]) ).
cnf(s117,plain,
( spl26_78
| spl26_79 ),
inference(sat_conversion,[],[f3446]) ).
cnf(s121,plain,
~ spl26_79,
inference(sat_conversion,[],[f3471]) ).
cnf(s123,plain,
( ~ spl26_78
| spl26_80
| spl26_81 ),
inference(sat_conversion,[],[f3494]) ).
cnf(s128,plain,
( ~ spl26_51
| ~ spl26_81 ),
inference(sat_conversion,[],[f3536]) ).
cnf(s140,plain,
~ spl26_80,
inference(sat_conversion,[],[f3578]) ).
cnf(s147,plain,
( ~ spl26_17
| ~ spl26_22
| ~ spl26_41
| spl26_46 ),
inference(sat_conversion,[],[f3603]) ).
cnf(s151,plain,
( ~ spl26_46
| spl26_79
| ~ spl26_81 ),
inference(sat_conversion,[],[f3626]) ).
cnf(s157,plain,
( ~ spl26_22
| ~ spl26_23
| spl26_40
| ~ spl26_81 ),
inference(sat_conversion,[],[f4159]) ).
cnf(s160,plain,
( spl26_1
| spl26_2 ),
inference(sat_conversion,[],[f4171]) ).
cnf(s161,plain,
( ~ spl26_23
| ~ spl26_36 ),
inference(sat_conversion,[],[f4194]) ).
cnf(s172,plain,
( spl26_35
| ~ spl26_37
| spl26_90 ),
inference(sat_conversion,[],[f4361]) ).
cnf(s173,plain,
~ spl26_90,
inference(sat_conversion,[],[f4382]) ).
cnf(s175,plain,
( ~ spl26_23
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41 ),
inference(sat_conversion,[],[f4446]) ).
cnf(s176,plain,
( spl26_30
| ~ spl26_35
| ~ spl26_41 ),
inference(sat_conversion,[],[f4462]) ).
cnf(s177,plain,
( ~ spl26_29
| ~ spl26_35
| ~ spl26_41 ),
inference(sat_conversion,[],[f4490]) ).
cnf(s180,plain,
( spl26_50
| ~ spl26_81 ),
inference(sat_conversion,[],[f4508]) ).
cnf(s184,plain,
( spl26_12
| ~ spl26_81 ),
inference(sat_conversion,[],[f4522]) ).
cnf(s189,plain,
( spl26_11
| ~ spl26_94
| spl26_95 ),
inference(sat_conversion,[],[f4560]) ).
cnf(s192,plain,
( spl26_29
| ~ spl26_95 ),
inference(sat_conversion,[],[f4576]) ).
cnf(s193,plain,
( spl26_16
| spl26_17
| spl26_97 ),
inference(sat_conversion,[],[f4592]) ).
cnf(s198,plain,
( ~ spl26_17
| ~ spl26_35
| ~ spl26_41 ),
inference(sat_conversion,[],[f4624]) ).
cnf(s202,plain,
( spl26_30
| ~ spl26_94 ),
inference(sat_conversion,[],[f4650]) ).
cnf(s213,plain,
( ~ spl26_1
| spl26_36
| spl26_37 ),
inference(sat_conversion,[],[f4766]) ).
cnf(s216,plain,
( ~ spl26_36
| spl26_94 ),
inference(sat_conversion,[],[f4805]) ).
cnf(s222,plain,
( ~ spl26_29
| ~ spl26_36 ),
inference(sat_conversion,[],[f4840]) ).
cnf(s223,plain,
( ~ spl26_11
| ~ spl26_97 ),
inference(sat_conversion,[],[f4842]) ).
cnf(s224,plain,
( ~ spl26_17
| ~ spl26_31
| ~ spl26_36
| ~ spl26_41 ),
inference(sat_conversion,[],[f4868]) ).
cnf(s228,plain,
( ~ spl26_16
| spl26_23
| spl26_24 ),
inference(sat_conversion,[],[f4925]) ).
cnf(s231,plain,
( ~ spl26_24
| ~ spl26_25 ),
inference(sat_conversion,[],[f5037]) ).
cnf(s232,plain,
( spl26_25
| spl26_26
| spl26_111 ),
inference(sat_conversion,[],[f5048]) ).
cnf(s235,plain,
( spl26_22
| ~ spl26_26
| ~ spl26_81 ),
inference(sat_conversion,[],[f5095]) ).
cnf(s237,plain,
( ~ spl26_36
| ~ spl26_111 ),
inference(sat_conversion,[],[f5175]) ).
cnf(s239,plain,
( ~ spl26_22
| ~ spl26_31
| ~ spl26_36
| ~ spl26_81 ),
inference(sat_conversion,[],[f5188]) ).
cnf(s240,plain,
( ~ spl26_30
| spl26_94 ),
inference(sat_conversion,[],[f5196]) ).
cnf(s243,plain,
( ~ spl26_35
| ~ spl26_41
| ~ spl26_111 ),
inference(sat_conversion,[],[f5251]) ).
cnf(s244,plain,
( ~ spl26_26
| ~ spl26_31
| ~ spl26_35
| ~ spl26_41
| ~ spl26_81 ),
inference(sat_conversion,[],[f5284]) ).
cnf(s249,plain,
( ~ spl26_2
| spl26_51
| ~ spl26_81
| ~ spl26_111 ),
inference(sat_conversion,[],[f5348]) ).
cnf(s250,plain,
( ~ spl26_2
| ~ spl26_26
| spl26_51
| ~ spl26_81 ),
inference(sat_conversion,[],[f5391]) ).
cnf(s251,plain,
( spl26_35
| ~ spl26_37 ),
inference(rat,[],[s172,s173]) ).
cnf(s253,plain,
( ~ spl26_78
| spl26_81 ),
inference(rat,[],[s123,s140]) ).
cnf(s257,plain,
spl26_78,
inference(rat,[],[s117,s121]) ).
cnf(s258,plain,
spl26_81,
inference(rat,[],[s253,s257]) ).
cnf(s260,plain,
spl26_12,
inference(rat,[],[s184,s258]) ).
cnf(s261,plain,
spl26_50,
inference(rat,[],[s180,s258]) ).
cnf(s269,plain,
~ spl26_51,
inference(rat,[],[s128,s258]) ).
cnf(s271,plain,
~ spl26_46,
inference(rat,[],[s151,s121,s258]) ).
cnf(s282,plain,
~ spl26_13,
inference(rat,[],[s52,s269]) ).
cnf(s285,plain,
( ~ spl26_2
| spl26_11 ),
inference(rat,[],[s41,s269,s261]) ).
cnf(s286,plain,
spl26_41,
inference(rat,[],[s32,s33]) ).
cnf(s288,plain,
( ~ spl26_2
| spl26_22 ),
inference(rat,[],[s13,s282,s260]) ).
cnf(s290,plain,
~ spl26_2,
inference(rat,[],[s228,s193,s231,s147,s157,s223,s232,s288,s285,s249,s250,s286,s271,s33,s258,s269]) ).
cnf(s291,plain,
spl26_1,
inference(rat,[],[s160,s290]) ).
cnf(s293,plain,
~ spl26_111,
inference(rat,[],[s251,s213,s243,s237,s291,s286]) ).
cnf(s294,plain,
spl26_94,
inference(rat,[],[s251,s213,s176,s216,s240,s291,s286]) ).
cnf(s295,plain,
spl26_30,
inference(rat,[],[s202,s294]) ).
cnf(s296,plain,
~ spl26_29,
inference(rat,[],[s251,s213,s177,s222,s291,s286]) ).
cnf(s297,plain,
~ spl26_95,
inference(rat,[],[s192,s296]) ).
cnf(s298,plain,
spl26_31,
inference(rat,[],[s18,s295,s296]) ).
cnf(s299,plain,
spl26_11,
inference(rat,[],[s189,s294,s297]) ).
cnf(s302,plain,
~ spl26_17,
inference(rat,[],[s251,s213,s198,s224,s291,s286,s298]) ).
cnf(s304,plain,
spl26_16,
inference(rat,[],[s47,s299,s302]) ).
cnf(s305,plain,
~ spl26_23,
inference(rat,[],[s213,s251,s161,s175,s291,s298,s286]) ).
cnf(s306,plain,
spl26_24,
inference(rat,[],[s228,s304,s305]) ).
cnf(s308,plain,
~ spl26_25,
inference(rat,[],[s231,s306]) ).
cnf(s309,plain,
spl26_26,
inference(rat,[],[s232,s293,s308]) ).
cnf(s311,plain,
~ spl26_35,
inference(rat,[],[s244,s258,s286,s298,s309]) ).
cnf(s312,plain,
spl26_22,
inference(rat,[],[s235,s258,s309]) ).
cnf(s313,plain,
~ spl26_37,
inference(rat,[],[s251,s311]) ).
cnf(s314,plain,
~ spl26_36,
inference(rat,[],[s239,s258,s298,s312]) ).
cnf(s316,plain,
$false,
inference(rat,[],[s213,s291,s314,s313]) ).
tff(f5392,plain,
$false,
inference(avatar_sat_refutation,[],[s316]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW608_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n009.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 14:22:47 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.20/1.19 % (3059426)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.20/1.19 % (3059434)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=26161507:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.20/1.19 % (3059434)Instruction limit reached!
% 3.20/1.19 % (3059434)------------------------------
% 3.20/1.19 % (3059434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.19 % (3059434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.19 % (3059434)CaDiCaL version: 2.1.3
% 3.20/1.19 % (3059434)Termination reason: Instruction limit
% 3.20/1.19 % (3059434)Termination phase: Saturation
% 3.20/1.19 % (3059434)Time elapsed: 0.003 s
% 3.20/1.19 % (3059434)Peak memory usage: 88 MB
% 3.20/1.19 % (3059434)Instructions burned: 8 (million)
% 3.20/1.19 % (3059431)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=173236262:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.20/1.19 % (3059433)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3753161174:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.20/1.19 % (3059432)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4242120369:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.20/1.19 % (3059437)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=64596512:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.20/1.19 % (3059436)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3787034459:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.20/1.19 % (3059435)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=44374353:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.20/1.19 % (3059435)Instruction limit reached!
% 3.20/1.19 % (3059435)------------------------------
% 3.20/1.19 % (3059435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.19 % (3059435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.19 % (3059435)CaDiCaL version: 2.1.3
% 3.20/1.19 % (3059435)Termination reason: Instruction limit
% 3.20/1.19 % (3059435)Termination phase: Property scanning
% 3.20/1.19 % (3059435)Time elapsed: 0.003 s
% 3.20/1.19 % (3059435)Peak memory usage: 86 MB
% 3.20/1.19 % (3059435)Instructions burned: 4 (million)
% 3.20/1.19 % (3059431)Instruction limit reached!
% 3.20/1.19 % (3059431)------------------------------
% 3.20/1.19 % (3059431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.19 % (3059431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.19 % (3059431)CaDiCaL version: 2.1.3
% 3.20/1.19 % (3059431)Termination reason: Instruction limit
% 3.20/1.19 % (3059431)Termination phase: Saturation
% 3.20/1.19 % (3059431)Time elapsed: 0.029 s
% 3.20/1.19 % (3059431)Peak memory usage: 111 MB
% 3.20/1.19 % (3059431)Instructions burned: 12 (million)
% 3.20/1.19 % (3059437)Instruction limit reached!
% 3.20/1.19 % (3059437)------------------------------
% 3.20/1.19 % (3059437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.19 % (3059437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.19 % (3059437)CaDiCaL version: 2.1.3
% 3.20/1.19 % (3059437)Termination reason: Instruction limit
% 3.20/1.19 % (3059437)Termination phase: Saturation
% 3.20/1.19 % (3059437)Time elapsed: 0.044 s
% 3.20/1.19 % (3059437)Peak memory usage: 116 MB
% 3.20/1.19 % (3059437)Instructions burned: 34 (million)
% 3.20/1.19 % (3059436)Instruction limit reached!
% 3.20/1.19 % (3059436)------------------------------
% 3.20/1.19 % (3059436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.19 % (3059436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.19 % (3059436)CaDiCaL version: 2.1.3
% 3.20/1.19 % (3059436)Termination reason: Instruction limit
% 3.20/1.19 % (3059436)Termination phase: Saturation
% 3.20/1.19 % (3059436)Time elapsed: 0.054 s
% 3.20/1.19 % (3059436)Peak memory usage: 116 MB
% 3.20/1.19 % (3059436)Instructions burned: 46 (million)
% 3.20/1.19 % (3059439)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3312084689:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.20/1.19 % (3059439)Instruction limit reached!
% 3.20/1.19 % (3059439)------------------------------
% 4.33/1.35 % (3059439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.35 % (3059439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.35 % (3059439)CaDiCaL version: 2.1.3
% 4.33/1.35 % (3059439)Termination reason: Instruction limit
% 4.33/1.35 % (3059439)Termination phase: Saturation
% 4.33/1.35 % (3059439)Time elapsed: 0.006 s
% 4.33/1.35 % (3059439)Peak memory usage: 88 MB
% 4.33/1.35 % (3059439)Instructions burned: 15 (million)
% 4.33/1.35 % (3059433)Instruction limit reached!
% 4.33/1.35 % (3059433)------------------------------
% 4.33/1.35 % (3059433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.35 % (3059433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.35 % (3059433)CaDiCaL version: 2.1.3
% 4.33/1.35 % (3059433)Termination reason: Instruction limit
% 4.33/1.35 % (3059433)Termination phase: Saturation
% 4.33/1.35 % (3059433)Time elapsed: 0.155 s
% 4.33/1.35 % (3059433)Peak memory usage: 118 MB
% 4.33/1.35 % (3059433)Instructions burned: 201 (million)
% 4.33/1.35 % (3059446)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=3808471833:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.33/1.35 % (3059446)Instruction limit reached!
% 4.33/1.35 % (3059446)------------------------------
% 4.33/1.35 % (3059446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.35 % (3059446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.35 % (3059446)CaDiCaL version: 2.1.3
% 4.33/1.35 % (3059446)Termination reason: Instruction limit
% 4.33/1.35 % (3059446)Termination phase: Saturation
% 4.33/1.35 % (3059446)Time elapsed: 0.023 s
% 4.33/1.35 % (3059446)Peak memory usage: 89 MB
% 4.33/1.35 % (3059446)Instructions burned: 30 (million)
% 4.33/1.35 % (3059447)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=461484420:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.33/1.35 % (3059451)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2810488146:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.33/1.35 % (3059448)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1843683936:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.33/1.35 % (3059449)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=4132330230:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.33/1.35 % (3059447)Instruction limit reached!
% 4.33/1.35 % (3059447)------------------------------
% 4.33/1.35 % (3059447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.35 % (3059447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.35 % (3059447)CaDiCaL version: 2.1.3
% 4.33/1.35 % (3059447)Termination reason: Instruction limit
% 4.33/1.35 % (3059447)Termination phase: Saturation
% 4.33/1.35 % (3059447)Time elapsed: 0.010 s
% 4.33/1.35 % (3059447)Peak memory usage: 89 MB
% 4.33/1.35 % (3059447)Instructions burned: 17 (million)
% 4.33/1.35 % (3059448)Instruction limit reached!
% 4.33/1.35 % (3059448)------------------------------
% 4.33/1.35 % (3059448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.35 % (3059448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.35 % (3059448)CaDiCaL version: 2.1.3
% 4.33/1.35 % (3059448)Termination reason: Instruction limit
% 4.33/1.35 % (3059448)Termination phase: Saturation
% 4.33/1.35 % (3059448)Time elapsed: 0.018 s
% 4.33/1.35 % (3059448)Peak memory usage: 89 MB
% 4.33/1.35 % (3059448)Instructions burned: 25 (million)
% 4.33/1.35 % (3059449)Instruction limit reached!
% 4.33/1.35 % (3059449)------------------------------
% 4.33/1.35 % (3059449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.33/1.35 % (3059449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.35 % (3059449)CaDiCaL version: 2.1.3
% 4.33/1.35 % (3059449)Termination reason: Instruction limit
% 4.33/1.35 % (3059449)Termination phase: Saturation
% 4.33/1.35 % (3059449)Time elapsed: 0.018 s
% 4.33/1.35 % (3059449)Peak memory usage: 89 MB
% 4.33/1.35 % (3059449)Instructions burned: 28 (million)
% 4.33/1.35 % (3059432)Instruction limit reached!
% 4.33/1.35 % (3059432)------------------------------
% 4.33/1.35 % (3059432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.56 % (3059432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.56 % (3059432)CaDiCaL version: 2.1.3
% 5.44/1.56 % (3059432)Termination reason: Instruction limit
% 5.44/1.56 % (3059432)Termination phase: Saturation
% 5.44/1.56 % (3059432)Time elapsed: 0.218 s
% 5.44/1.56 % (3059432)Peak memory usage: 117 MB
% 5.44/1.56 % (3059432)Instructions burned: 308 (million)
% 5.44/1.56 % (3059451)Instruction limit reached!
% 5.44/1.56 % (3059451)------------------------------
% 5.44/1.56 % (3059451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.56 % (3059451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.56 % (3059451)CaDiCaL version: 2.1.3
% 5.44/1.56 % (3059451)Termination reason: Instruction limit
% 5.44/1.56 % (3059451)Termination phase: Saturation
% 5.44/1.56 % (3059451)Time elapsed: 0.025 s
% 5.44/1.56 % (3059451)Peak memory usage: 89 MB
% 5.44/1.56 % (3059451)Instructions burned: 88 (million)
% 5.44/1.56 % (3059453)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2988986321:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.44/1.56 % (3059453)Instruction limit reached!
% 5.44/1.56 % (3059453)------------------------------
% 5.44/1.56 % (3059453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.56 % (3059453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.56 % (3059453)CaDiCaL version: 2.1.3
% 5.44/1.56 % (3059453)Termination reason: Instruction limit
% 5.44/1.56 % (3059453)Termination phase: Naming
% 5.44/1.56 % (3059453)Time elapsed: 0.002 s
% 5.44/1.56 % (3059453)Peak memory usage: 85 MB
% 5.44/1.56 % (3059453)Instructions burned: 3 (million)
% 5.44/1.56 % (3059455)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=260581801:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.44/1.56 % (3059462)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=2515092972:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.44/1.56 % (3059462)Instruction limit reached!
% 5.44/1.56 % (3059462)------------------------------
% 5.44/1.56 % (3059462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.56 % (3059462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.56 % (3059462)CaDiCaL version: 2.1.3
% 5.44/1.56 % (3059462)Termination reason: Instruction limit
% 5.44/1.56 % (3059462)Termination phase: Saturation
% 5.44/1.56 % (3059462)Time elapsed: 0.003 s
% 5.44/1.56 % (3059462)Peak memory usage: 88 MB
% 5.44/1.56 % (3059462)Instructions burned: 10 (million)
% 5.44/1.56 % (3059459)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=847036877:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.44/1.56 % (3059459)Instruction limit reached!
% 5.44/1.56 % (3059459)------------------------------
% 5.44/1.56 % (3059459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.56 % (3059459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.56 % (3059459)CaDiCaL version: 2.1.3
% 5.44/1.56 % (3059459)Termination reason: Instruction limit
% 5.44/1.56 % (3059459)Termination phase: Property scanning
% 5.44/1.56 % (3059459)Time elapsed: 0.003 s
% 5.44/1.56 % (3059459)Peak memory usage: 86 MB
% 5.44/1.56 % (3059459)Instructions burned: 5 (million)
% 5.44/1.56 % (3059460)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1755706526:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.44/1.56 % (3059461)lrs+10_1_thi=all:si=on:fd=off:random_seed=432053241:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.44/1.56 % (3059463)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2783577437:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 5.44/1.56 % (3059463)Instruction limit reached!
% 5.44/1.56 % (3059463)------------------------------
% 5.44/1.56 % (3059463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.44/1.56 % (3059463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.56 % (3059463)CaDiCaL version: 2.1.3
% 5.44/1.56 % (3059463)Termination reason: Instruction limit
% 5.44/1.56 % (3059463)Termination phase: Naming
% 7.23/1.81 % (3059463)Time elapsed: 0.002 s
% 7.23/1.81 % (3059463)Peak memory usage: 86 MB
% 7.23/1.81 % (3059463)Instructions burned: 2 (million)
% 7.23/1.81 % (3059461)Instruction limit reached!
% 7.23/1.81 % (3059461)------------------------------
% 7.23/1.81 % (3059461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.81 % (3059461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.81 % (3059461)CaDiCaL version: 2.1.3
% 7.23/1.81 % (3059461)Termination reason: Instruction limit
% 7.23/1.81 % (3059461)Termination phase: Saturation
% 7.23/1.81 % (3059461)Time elapsed: 0.062 s
% 7.23/1.81 % (3059461)Peak memory usage: 117 MB
% 7.23/1.81 % (3059461)Instructions burned: 54 (million)
% 7.23/1.81 % (3059469)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1695628316:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 7.23/1.81 % (3059455)Instruction limit reached!
% 7.23/1.81 % (3059455)------------------------------
% 7.23/1.81 % (3059455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.81 % (3059455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.81 % (3059455)CaDiCaL version: 2.1.3
% 7.23/1.81 % (3059455)Termination reason: Instruction limit
% 7.23/1.81 % (3059455)Termination phase: Saturation
% 7.23/1.81 % (3059455)Time elapsed: 0.128 s
% 7.23/1.81 % (3059455)Peak memory usage: 91 MB
% 7.23/1.81 % (3059455)Instructions burned: 182 (million)
% 7.23/1.81 % (3059460)Instruction limit reached!
% 7.23/1.81 % (3059460)------------------------------
% 7.23/1.81 % (3059460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.81 % (3059460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.81 % (3059460)CaDiCaL version: 2.1.3
% 7.23/1.81 % (3059460)Termination reason: Instruction limit
% 7.23/1.81 % (3059460)Termination phase: Saturation
% 7.23/1.81 % (3059460)Time elapsed: 0.094 s
% 7.23/1.81 % (3059460)Peak memory usage: 134 MB
% 7.23/1.81 % (3059460)Instructions burned: 67 (million)
% 7.23/1.81 % (3059470)dis+10_1_si=on:random_seed=2129704328:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 7.23/1.81 % (3059466)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2994589673:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.23/1.81 % (3059466)Instruction limit reached!
% 7.23/1.81 % (3059466)------------------------------
% 7.23/1.81 % (3059466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.81 % (3059466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.81 % (3059466)CaDiCaL version: 2.1.3
% 7.23/1.81 % (3059466)Termination reason: Instruction limit
% 7.23/1.81 % (3059466)Termination phase: Naming
% 7.23/1.81 % (3059466)Time elapsed: 0.002 s
% 7.23/1.81 % (3059466)Peak memory usage: 86 MB
% 7.23/1.81 % (3059466)Instructions burned: 3 (million)
% 7.23/1.81 % (3059470)Instruction limit reached!
% 7.23/1.81 % (3059470)------------------------------
% 7.23/1.81 % (3059470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.81 % (3059470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.81 % (3059470)CaDiCaL version: 2.1.3
% 7.23/1.81 % (3059470)Termination reason: Instruction limit
% 7.23/1.81 % (3059470)Termination phase: Saturation
% 7.23/1.81 % (3059470)Time elapsed: 0.007 s
% 7.23/1.81 % (3059470)Peak memory usage: 88 MB
% 7.23/1.82 % (3059470)Instructions burned: 10 (million)
% 7.23/1.82 % (3059469)Instruction limit reached!
% 7.23/1.82 % (3059469)------------------------------
% 7.23/1.82 % (3059469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.82 % (3059469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.82 % (3059469)CaDiCaL version: 2.1.3
% 7.23/1.82 % (3059469)Termination reason: Instruction limit
% 7.23/1.82 % (3059469)Termination phase: Saturation
% 7.23/1.82 % (3059469)Time elapsed: 0.062 s
% 7.23/1.82 % (3059469)Peak memory usage: 117 MB
% 7.23/1.82 % (3059469)Instructions burned: 129 (million)
% 7.23/1.82 % (3059474)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=976099088:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.23/1.82 % (3059474)Refutation not found, incomplete strategy
% 7.23/1.82 % (3059474)------------------------------
% 7.23/1.82 % (3059474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/1.82 % (3059474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.10/2.01 % (3059474)CaDiCaL version: 2.1.3
% 8.10/2.01 % (3059474)Termination reason: Refutation not found, incomplete strategy
% 8.10/2.01 % (3059474)Time elapsed: 0.010 s
% 8.10/2.01 % (3059474)Peak memory usage: 89 MB
% 8.10/2.01 % (3059474)Instructions burned: 14 (million)
% 8.10/2.01 % (3059477)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2205081257:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 8.10/2.01 % (3059475)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1221986482:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 8.10/2.01 % (3059477)Instruction limit reached!
% 8.10/2.01 % (3059477)------------------------------
% 8.10/2.01 % (3059477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.10/2.01 % (3059477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.10/2.01 % (3059477)CaDiCaL version: 2.1.3
% 8.10/2.01 % (3059477)Termination reason: Instruction limit
% 8.10/2.01 % (3059477)Termination phase: Naming
% 8.10/2.01 % (3059477)Time elapsed: 0.002 s
% 8.10/2.01 % (3059477)Peak memory usage: 86 MB
% 8.10/2.01 % (3059477)Instructions burned: 3 (million)
% 8.10/2.01 % (3059478)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3422773772:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 8.10/2.01 % (3059478)Instruction limit reached!
% 8.10/2.01 % (3059478)------------------------------
% 8.10/2.01 % (3059478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.10/2.01 % (3059478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.10/2.01 % (3059478)CaDiCaL version: 2.1.3
% 8.10/2.01 % (3059478)Termination reason: Instruction limit
% 8.10/2.01 % (3059478)Termination phase: Saturation
% 8.10/2.01 % (3059478)Time elapsed: 0.005 s
% 8.10/2.01 % (3059478)Peak memory usage: 88 MB
% 8.10/2.01 % (3059478)Instructions burned: 8 (million)
% 8.10/2.01 % (3059475)Instruction limit reached!
% 8.10/2.01 % (3059475)------------------------------
% 8.10/2.01 % (3059475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.10/2.01 % (3059475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.10/2.01 % (3059475)CaDiCaL version: 2.1.3
% 8.10/2.01 % (3059475)Termination reason: Instruction limit
% 8.10/2.01 % (3059475)Termination phase: Saturation
% 8.10/2.01 % (3059475)Time elapsed: 0.027 s
% 8.10/2.01 % (3059475)Peak memory usage: 89 MB
% 8.10/2.01 % (3059475)Instructions burned: 35 (million)
% 8.10/2.01 % (3059483)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3435982754:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 8.10/2.01 % (3059482)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3661360852:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 8.10/2.01 % (3059481)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1804991769:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 8.10/2.01 % (3059482)Instruction limit reached!
% 8.10/2.01 % (3059482)------------------------------
% 8.10/2.01 % (3059482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.10/2.01 % (3059482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.10/2.01 % (3059482)CaDiCaL version: 2.1.3
% 8.10/2.01 % (3059482)Termination reason: Instruction limit
% 8.10/2.01 % (3059482)Termination phase: Saturation
% 8.10/2.01 % (3059482)Time elapsed: 0.028 s
% 8.10/2.01 % (3059482)Peak memory usage: 111 MB
% 8.10/2.01 % (3059482)Instructions burned: 13 (million)
% 8.10/2.01 % (3059483)Instruction limit reached!
% 8.10/2.01 % (3059483)------------------------------
% 8.10/2.01 % (3059483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.10/2.01 % (3059483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.10/2.01 % (3059483)CaDiCaL version: 2.1.3
% 8.10/2.01 % (3059483)Termination reason: Instruction limit
% 8.10/2.01 % (3059483)Termination phase: Saturation
% 8.10/2.01 % (3059483)Time elapsed: 0.086 s
% 8.10/2.01 % (3059483)Peak memory usage: 117 MB
% 8.10/2.01 % (3059483)Instructions burned: 228 (million)
% 8.10/2.01 % (3059487)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3375925236:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.80/2.31 % (3059487)Instruction limit reached!
% 10.80/2.31 % (3059487)------------------------------
% 10.80/2.31 % (3059487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.31 % (3059487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.31 % (3059487)CaDiCaL version: 2.1.3
% 10.80/2.31 % (3059487)Termination reason: Instruction limit
% 10.80/2.31 % (3059487)Termination phase: Saturation
% 10.80/2.31 % (3059487)Time elapsed: 0.008 s
% 10.80/2.31 % (3059487)Peak memory usage: 88 MB
% 10.80/2.31 % (3059487)Instructions burned: 11 (million)
% 10.80/2.31 % (3059493)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=2030880776:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.80/2.31 % (3059492)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=573690388:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.80/2.31 % (3059474)------------------------------
% 10.80/2.31 % (3059474)------------------------------
% 10.80/2.31 % (3059494)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=1186483234:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 10.80/2.31 % (3059493)Instruction limit reached!
% 10.80/2.31 % (3059493)------------------------------
% 10.80/2.31 % (3059493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.31 % (3059493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.31 % (3059493)CaDiCaL version: 2.1.3
% 10.80/2.31 % (3059493)Termination reason: Instruction limit
% 10.80/2.31 % (3059493)Termination phase: Saturation
% 10.80/2.31 % (3059493)Time elapsed: 0.051 s
% 10.80/2.31 % (3059493)Peak memory usage: 90 MB
% 10.80/2.31 % (3059493)Instructions burned: 76 (million)
% 10.80/2.31 % (3059495)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=389186745:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 10.80/2.31 % (3059492)Instruction limit reached!
% 10.80/2.31 % (3059492)------------------------------
% 10.80/2.31 % (3059492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.31 % (3059492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.31 % (3059492)CaDiCaL version: 2.1.3
% 10.80/2.31 % (3059492)Termination reason: Instruction limit
% 10.80/2.31 % (3059492)Termination phase: Saturation
% 10.80/2.31 % (3059492)Time elapsed: 0.093 s
% 10.80/2.31 % (3059492)Peak memory usage: 133 MB
% 10.80/2.31 % (3059492)Instructions burned: 71 (million)
% 10.80/2.31 % (3059481)Instruction limit reached!
% 10.80/2.31 % (3059481)------------------------------
% 10.80/2.31 % (3059481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.31 % (3059481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.31 % (3059481)CaDiCaL version: 2.1.3
% 10.80/2.31 % (3059481)Termination reason: Instruction limit
% 10.80/2.31 % (3059481)Termination phase: Saturation
% 10.80/2.31 % (3059481)Time elapsed: 0.247 s
% 10.80/2.31 % (3059481)Peak memory usage: 92 MB
% 10.80/2.31 % (3059481)Instructions burned: 371 (million)
% 10.80/2.31 % (3059495)Instruction limit reached!
% 10.80/2.31 % (3059495)------------------------------
% 10.80/2.31 % (3059495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.31 % (3059495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.31 % (3059495)CaDiCaL version: 2.1.3
% 10.80/2.31 % (3059495)Termination reason: Instruction limit
% 10.80/2.31 % (3059495)Termination phase: Saturation
% 10.80/2.31 % (3059495)Time elapsed: 0.062 s
% 10.80/2.31 % (3059495)Peak memory usage: 117 MB
% 10.80/2.31 % (3059495)Instructions burned: 133 (million)
% 10.80/2.31 % (3059497)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3258171119:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.80/2.31 % (3059500)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=190559821:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 10.80/2.31 % (3059502)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1510036913:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.80/2.31 % (3059506)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=948434815:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 13.23/2.60 % (3059500)Instruction limit reached!
% 13.23/2.60 % (3059500)------------------------------
% 13.23/2.60 % (3059500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/2.60 % (3059500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/2.60 % (3059500)CaDiCaL version: 2.1.3
% 13.23/2.60 % (3059500)Termination reason: Instruction limit
% 13.23/2.60 % (3059500)Termination phase: Saturation
% 13.23/2.60 % (3059500)Time elapsed: 0.069 s
% 13.23/2.60 % (3059500)Peak memory usage: 133 MB
% 13.23/2.60 % (3059500)Instructions burned: 42 (million)
% 13.23/2.60 % (3059505)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2890365545:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 13.23/2.60 % (3059504)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3997117675:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 13.23/2.60 % (3059494)Instruction limit reached!
% 13.23/2.60 % (3059494)------------------------------
% 13.23/2.60 % (3059494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/2.60 % (3059494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/2.60 % (3059494)CaDiCaL version: 2.1.3
% 13.23/2.60 % (3059494)Termination reason: Instruction limit
% 13.23/2.60 % (3059494)Termination phase: Saturation
% 13.23/2.60 % (3059494)Time elapsed: 0.206 s
% 13.23/2.60 % (3059494)Peak memory usage: 91 MB
% 13.23/2.60 % (3059494)Instructions burned: 295 (million)
% 13.23/2.60 % (3059497)Instruction limit reached!
% 13.23/2.60 % (3059497)------------------------------
% 13.23/2.60 % (3059497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/2.60 % (3059497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/2.60 % (3059497)CaDiCaL version: 2.1.3
% 13.23/2.60 % (3059497)Termination reason: Instruction limit
% 13.23/2.60 % (3059497)Termination phase: Saturation
% 13.23/2.60 % (3059497)Time elapsed: 0.140 s
% 13.23/2.60 % (3059497)Peak memory usage: 134 MB
% 13.23/2.60 % (3059497)Instructions burned: 131 (million)
% 13.23/2.60 % (3059506)Instruction limit reached!
% 13.23/2.60 % (3059506)------------------------------
% 13.23/2.60 % (3059506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/2.60 % (3059506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/2.60 % (3059506)CaDiCaL version: 2.1.3
% 13.23/2.60 % (3059506)Termination reason: Instruction limit
% 13.23/2.60 % (3059506)Termination phase: Saturation
% 13.23/2.60 % (3059506)Time elapsed: 0.105 s
% 13.23/2.60 % (3059506)Peak memory usage: 117 MB
% 13.23/2.60 % (3059506)Instructions burned: 261 (million)
% 13.23/2.60 % (3059505)Instruction limit reached!
% 13.23/2.60 % (3059505)------------------------------
% 13.23/2.60 % (3059505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/2.60 % (3059505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/2.60 % (3059505)CaDiCaL version: 2.1.3
% 13.23/2.60 % (3059505)Termination reason: Instruction limit
% 13.23/2.60 % (3059505)Termination phase: Saturation
% 13.23/2.60 % (3059505)Time elapsed: 0.113 s
% 13.23/2.60 % (3059505)Peak memory usage: 118 MB
% 13.23/2.60 % (3059505)Instructions burned: 131 (million)
% 13.23/2.60 % (3059514)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2351406469:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 13.23/2.60 % (3059513)dis+10_1_si=on:random_seed=3385570765:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 13.23/2.60 % (3059502)Instruction limit reached!
% 13.23/2.60 % (3059502)------------------------------
% 13.23/2.60 % (3059502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/2.60 % (3059502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/2.60 % (3059502)CaDiCaL version: 2.1.3
% 13.23/2.60 % (3059502)Termination reason: Instruction limit
% 13.23/2.60 % (3059502)Termination phase: Saturation
% 13.23/2.60 % (3059502)Time elapsed: 0.189 s
% 13.23/2.60 % (3059502)Peak memory usage: 91 MB
% 13.23/2.60 % (3059502)Instructions burned: 308 (million)
% 13.23/2.60 % (3059515)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=921168598:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 14.84/2.98 % (3059516)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1066712780:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 14.84/2.98 % (3059516)Refutation not found, incomplete strategy
% 14.84/2.98 % (3059516)------------------------------
% 14.84/2.98 % (3059516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.84/2.98 % (3059516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.84/2.98 % (3059516)CaDiCaL version: 2.1.3
% 14.84/2.98 % (3059516)Termination reason: Refutation not found, incomplete strategy
% 14.84/2.98 % (3059516)Time elapsed: 0.025 s
% 14.84/2.98 % (3059516)Peak memory usage: 116 MB
% 14.84/2.98 % (3059516)Instructions burned: 27 (million)
% 14.84/2.98 % (3059517)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2653487354:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 14.84/2.98 % (3059515)Instruction limit reached!
% 14.84/2.98 % (3059515)------------------------------
% 14.84/2.98 % (3059515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.84/2.98 % (3059515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.84/2.98 % (3059515)CaDiCaL version: 2.1.3
% 14.84/2.98 % (3059515)Termination reason: Instruction limit
% 14.84/2.98 % (3059515)Termination phase: Saturation
% 14.84/2.98 % (3059515)Time elapsed: 0.098 s
% 14.84/2.98 % (3059515)Peak memory usage: 90 MB
% 14.84/2.98 % (3059515)Instructions burned: 141 (million)
% 14.84/2.98 % (3059520)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=1815025970:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 14.84/2.98 % (3059514)Instruction limit reached!
% 14.84/2.98 % (3059514)------------------------------
% 14.84/2.98 % (3059514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.84/2.98 % (3059514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.84/2.98 % (3059514)CaDiCaL version: 2.1.3
% 14.84/2.98 % (3059514)Termination reason: Instruction limit
% 14.84/2.98 % (3059514)Termination phase: Saturation
% 14.84/2.98 % (3059514)Time elapsed: 0.201 s
% 14.84/2.98 % (3059514)Peak memory usage: 91 MB
% 14.84/2.98 % (3059514)Instructions burned: 383 (million)
% 14.84/2.98 % (3059517)Instruction limit reached!
% 14.84/2.98 % (3059517)------------------------------
% 14.84/2.98 % (3059517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.84/2.98 % (3059517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.84/2.98 % (3059517)CaDiCaL version: 2.1.3
% 14.84/2.98 % (3059517)Termination reason: Instruction limit
% 14.84/2.98 % (3059517)Termination phase: Saturation
% 14.84/2.98 % (3059517)Time elapsed: 0.079 s
% 14.84/2.98 % (3059517)Peak memory usage: 89 MB
% 14.84/2.98 % (3059517)Instructions burned: 122 (million)
% 14.84/2.98 % (3059516)------------------------------
% 14.84/2.98 % (3059516)------------------------------
% 14.84/2.98 % (3059520)Instruction limit reached!
% 14.84/2.98 % (3059520)------------------------------
% 14.84/2.98 % (3059520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.84/2.98 % (3059520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.84/2.98 % (3059520)CaDiCaL version: 2.1.3
% 14.84/2.98 % (3059520)Termination reason: Instruction limit
% 14.84/2.98 % (3059520)Termination phase: Saturation
% 14.84/2.98 % (3059520)Time elapsed: 0.107 s
% 14.84/2.98 % (3059520)Peak memory usage: 117 MB
% 14.84/2.98 % (3059520)Instructions burned: 128 (million)
% 14.84/2.98 % (3059524)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=502893178:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 14.84/2.98 % (3059504)Instruction limit reached!
% 14.84/2.98 % (3059504)------------------------------
% 14.84/2.98 % (3059504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.84/2.98 % (3059504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.84/2.98 % (3059504)CaDiCaL version: 2.1.3
% 14.84/2.98 % (3059504)Termination reason: Instruction limit
% 14.84/2.98 % (3059504)Termination phase: Saturation
% 14.84/2.98 % (3059504)Time elapsed: 0.474 s
% 14.84/2.98 % (3059504)Peak memory usage: 137 MB
% 14.84/2.98 % (3059504)Instructions burned: 598 (million)
% 14.84/2.98 % (3059524)Instruction limit reached!
% 14.84/2.98 % (3059524)------------------------------
% 14.84/2.98 % (3059524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/3.26 % (3059524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/3.26 % (3059524)CaDiCaL version: 2.1.3
% 17.90/3.26 % (3059524)Termination reason: Instruction limit
% 17.90/3.26 % (3059524)Termination phase: Saturation
% 17.90/3.26 % (3059524)Time elapsed: 0.051 s
% 17.90/3.26 % (3059524)Peak memory usage: 116 MB
% 17.90/3.26 % (3059524)Instructions burned: 40 (million)
% 17.90/3.26 % (3059526)dis+1010_1_to=kbo:si=on:random_seed=2057058597:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi)
% 17.90/3.26 % (3059527)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=984004737:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 17.90/3.26 % (3059528)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=776149112:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 17.90/3.26 % (3059530)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2626575178:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 17.90/3.26 % (3059526)Instruction limit reached!
% 17.90/3.26 % (3059526)------------------------------
% 17.90/3.26 % (3059526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/3.26 % (3059526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/3.26 % (3059526)CaDiCaL version: 2.1.3
% 17.90/3.26 % (3059526)Termination reason: Instruction limit
% 17.90/3.26 % (3059526)Termination phase: Saturation
% 17.90/3.26 % (3059526)Time elapsed: 0.130 s
% 17.90/3.26 % (3059526)Peak memory usage: 91 MB
% 17.90/3.26 % (3059526)Instructions burned: 176 (million)
% 17.90/3.26 % (3059531)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3520313402:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 17.90/3.26 % (3059534)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=216981527:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 17.90/3.26 % (3059528)Instruction limit reached!
% 17.90/3.26 % (3059528)------------------------------
% 17.90/3.26 % (3059528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/3.26 % (3059528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/3.26 % (3059528)CaDiCaL version: 2.1.3
% 17.90/3.26 % (3059528)Termination reason: Instruction limit
% 17.90/3.26 % (3059528)Termination phase: Saturation
% 17.90/3.26 % (3059528)Time elapsed: 0.199 s
% 17.90/3.26 % (3059528)Peak memory usage: 135 MB
% 17.90/3.26 % (3059528)Instructions burned: 484 (million)
% 17.90/3.26 % (3059527)Instruction limit reached!
% 17.90/3.26 % (3059527)------------------------------
% 17.90/3.26 % (3059527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/3.26 % (3059527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/3.26 % (3059527)CaDiCaL version: 2.1.3
% 17.90/3.26 % (3059527)Termination reason: Instruction limit
% 17.90/3.26 % (3059527)Termination phase: Saturation
% 17.90/3.26 % (3059527)Time elapsed: 0.237 s
% 17.90/3.26 % (3059527)Peak memory usage: 119 MB
% 17.90/3.26 % (3059527)Instructions burned: 329 (million)
% 17.90/3.26 % (3059513)Instruction limit reached!
% 17.90/3.26 % (3059513)------------------------------
% 17.90/3.26 % (3059513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/3.26 % (3059513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/3.26 % (3059513)CaDiCaL version: 2.1.3
% 17.90/3.26 % (3059513)Termination reason: Instruction limit
% 17.90/3.26 % (3059513)Termination phase: Saturation
% 17.90/3.26 % (3059513)Time elapsed: 0.590 s
% 17.90/3.26 % (3059513)Peak memory usage: 93 MB
% 17.90/3.26 % (3059513)Instructions burned: 1001 (million)
% 17.90/3.26 % (3059530)Instruction limit reached!
% 17.90/3.26 % (3059530)------------------------------
% 17.90/3.26 % (3059530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/3.26 % (3059530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/3.26 % (3059530)CaDiCaL version: 2.1.3
% 17.90/3.26 % (3059530)Termination reason: Instruction limit
% 17.90/3.26 % (3059530)Termination phase: Saturation
% 17.90/3.26 % (3059530)Time elapsed: 0.162 s
% 17.90/3.26 % (3059530)Peak memory usage: 135 MB
% 17.90/3.26 % (3059530)Instructions burned: 215 (million)
% 17.90/3.26 % (3059537)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1491876478:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 18.80/3.49 % (3059534)Instruction limit reached!
% 18.80/3.49 % (3059534)------------------------------
% 18.80/3.49 % (3059534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.80/3.49 % (3059534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.80/3.49 % (3059534)CaDiCaL version: 2.1.3
% 18.80/3.49 % (3059534)Termination reason: Instruction limit
% 18.80/3.49 % (3059534)Termination phase: Saturation
% 18.80/3.49 % (3059534)Time elapsed: 0.167 s
% 18.80/3.49 % (3059534)Peak memory usage: 90 MB
% 18.80/3.49 % (3059534)Instructions burned: 297 (million)
% 18.80/3.49 % (3059540)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=26825050:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi)
% 18.80/3.49 % (3059531)Instruction limit reached!
% 18.80/3.49 % (3059531)------------------------------
% 18.80/3.49 % (3059531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.80/3.49 % (3059531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.80/3.49 % (3059531)CaDiCaL version: 2.1.3
% 18.80/3.49 % (3059531)Termination reason: Instruction limit
% 18.80/3.49 % (3059531)Termination phase: Saturation
% 18.80/3.49 % (3059531)Time elapsed: 0.182 s
% 18.80/3.49 % (3059531)Peak memory usage: 116 MB
% 18.80/3.49 % (3059531)Instructions burned: 351 (million)
% 18.80/3.49 % (3059541)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1375970168:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 18.80/3.49 % (3059542)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2567994333:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi)
% 18.80/3.49 % (3059543)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4105082470:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 18.80/3.49 % (3059540)Instruction limit reached!
% 18.80/3.49 % (3059540)------------------------------
% 18.80/3.49 % (3059540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.80/3.49 % (3059540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.80/3.49 % (3059540)CaDiCaL version: 2.1.3
% 18.80/3.49 % (3059540)Termination reason: Instruction limit
% 18.80/3.49 % (3059540)Termination phase: Saturation
% 18.80/3.49 % (3059540)Time elapsed: 0.111 s
% 18.80/3.49 % (3059540)Peak memory usage: 117 MB
% 18.80/3.49 % (3059540)Instructions burned: 284 (million)
% 18.80/3.49 % (3059546)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3737766598:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi)
% 18.80/3.49 % (3059547)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=1682917297:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi)
% 18.80/3.49 % (3059537)Instruction limit reached!
% 18.80/3.49 % (3059537)------------------------------
% 18.80/3.49 % (3059537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.80/3.49 % (3059537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.80/3.49 % (3059537)CaDiCaL version: 2.1.3
% 18.80/3.49 % (3059537)Termination reason: Instruction limit
% 18.80/3.49 % (3059537)Termination phase: Saturation
% 18.80/3.49 % (3059537)Time elapsed: 0.236 s
% 18.80/3.49 % (3059537)Peak memory usage: 118 MB
% 18.80/3.49 % (3059537)Instructions burned: 329 (million)
% 18.80/3.49 % (3059551)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2605439244:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 18.80/3.49 % (3059542)Instruction limit reached!
% 18.80/3.49 % (3059542)------------------------------
% 18.80/3.49 % (3059542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.80/3.49 % (3059542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.80/3.49 % (3059542)CaDiCaL version: 2.1.3
% 18.80/3.49 % (3059542)Termination reason: Instruction limit
% 18.80/3.49 % (3059542)Termination phase: Saturation
% 18.80/3.49 % (3059542)Time elapsed: 0.165 s
% 18.80/3.49 % (3059542)Peak memory usage: 114 MB
% 18.80/3.49 % (3059542)Instructions burned: 322 (million)
% 18.80/3.49 % (3059541)Instruction limit reached!
% 18.80/3.49 % (3059541)------------------------------
% 20.57/4.01 % (3059541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/4.01 % (3059541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/4.01 % (3059541)CaDiCaL version: 2.1.3
% 20.57/4.01 % (3059541)Termination reason: Instruction limit
% 20.57/4.01 % (3059541)Termination phase: Saturation
% 20.57/4.01 % (3059541)Time elapsed: 0.286 s
% 20.57/4.01 % (3059541)Peak memory usage: 93 MB
% 20.57/4.01 % (3059541)Instructions burned: 486 (million)
% 20.57/4.01 % (3059543)Instruction limit reached!
% 20.57/4.01 % (3059543)------------------------------
% 20.57/4.01 % (3059543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/4.01 % (3059543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/4.01 % (3059543)CaDiCaL version: 2.1.3
% 20.57/4.01 % (3059543)Termination reason: Instruction limit
% 20.57/4.01 % (3059543)Termination phase: Saturation
% 20.57/4.01 % (3059543)Time elapsed: 0.260 s
% 20.57/4.01 % (3059543)Peak memory usage: 118 MB
% 20.57/4.01 % (3059543)Instructions burned: 417 (million)
% 20.57/4.01 % (3059554)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=549126053:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 20.57/4.01 % (3059551)Instruction limit reached!
% 20.57/4.01 % (3059551)------------------------------
% 20.57/4.01 % (3059551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/4.01 % (3059551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/4.01 % (3059551)CaDiCaL version: 2.1.3
% 20.57/4.01 % (3059551)Termination reason: Instruction limit
% 20.57/4.01 % (3059551)Termination phase: Saturation
% 20.57/4.01 % (3059551)Time elapsed: 0.143 s
% 20.57/4.01 % (3059551)Peak memory usage: 118 MB
% 20.57/4.01 % (3059551)Instructions burned: 376 (million)
% 20.57/4.01 % (3059556)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1742279904:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 20.57/4.01 % (3059547)Instruction limit reached!
% 20.57/4.01 % (3059547)------------------------------
% 20.57/4.01 % (3059547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/4.01 % (3059547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/4.01 % (3059547)CaDiCaL version: 2.1.3
% 20.57/4.01 % (3059547)Termination reason: Instruction limit
% 20.57/4.01 % (3059547)Termination phase: Saturation
% 20.57/4.01 % (3059547)Time elapsed: 0.241 s
% 20.57/4.01 % (3059547)Peak memory usage: 135 MB
% 20.57/4.01 % (3059547)Instructions burned: 277 (million)
% 20.57/4.01 % (3059546)Instruction limit reached!
% 20.57/4.01 % (3059546)------------------------------
% 20.57/4.01 % (3059546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/4.01 % (3059546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/4.01 % (3059546)CaDiCaL version: 2.1.3
% 20.57/4.01 % (3059546)Termination reason: Instruction limit
% 20.57/4.01 % (3059546)Termination phase: Saturation
% 20.57/4.01 % (3059546)Time elapsed: 0.323 s
% 20.57/4.01 % (3059546)Peak memory usage: 119 MB
% 20.57/4.01 % (3059546)Instructions burned: 471 (million)
% 20.57/4.01 % (3059560)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2783701947:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi)
% 20.57/4.01 % (3059559)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=4283642288:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi)
% 20.57/4.01 % (3059557)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=979371500:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi)
% 20.57/4.01 % (3059562)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3672958463:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 20.57/4.01 % (3059563)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=130783425:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 20.57/4.01 % (3059560)Instruction limit reached!
% 20.57/4.01 % (3059560)------------------------------
% 20.57/4.01 % (3059560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/4.01 % (3059560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.32 % (3059560)CaDiCaL version: 2.1.3
% 24.98/4.32 % (3059560)Termination reason: Instruction limit
% 24.98/4.32 % (3059560)Termination phase: Saturation
% 24.98/4.32 % (3059560)Time elapsed: 0.135 s
% 24.98/4.32 % (3059560)Peak memory usage: 121 MB
% 24.98/4.32 % (3059560)Instructions burned: 345 (million)
% 24.98/4.32 % (3059554)Instruction limit reached!
% 24.98/4.32 % (3059554)------------------------------
% 24.98/4.32 % (3059554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.32 % (3059554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.32 % (3059554)CaDiCaL version: 2.1.3
% 24.98/4.32 % (3059554)Termination reason: Instruction limit
% 24.98/4.32 % (3059554)Termination phase: Saturation
% 24.98/4.32 % (3059554)Time elapsed: 0.291 s
% 24.98/4.32 % (3059554)Peak memory usage: 118 MB
% 24.98/4.32 % (3059554)Instructions burned: 388 (million)
% 24.98/4.32 % (3059559)Instruction limit reached!
% 24.98/4.32 % (3059559)------------------------------
% 24.98/4.32 % (3059559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.32 % (3059559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.32 % (3059559)CaDiCaL version: 2.1.3
% 24.98/4.32 % (3059559)Termination reason: Instruction limit
% 24.98/4.32 % (3059559)Termination phase: Saturation
% 24.98/4.32 % (3059559)Time elapsed: 0.212 s
% 24.98/4.32 % (3059559)Peak memory usage: 91 MB
% 24.98/4.32 % (3059559)Instructions burned: 360 (million)
% 24.98/4.32 % (3059556)Instruction limit reached!
% 24.98/4.32 % (3059556)------------------------------
% 24.98/4.32 % (3059556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.32 % (3059556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.32 % (3059556)CaDiCaL version: 2.1.3
% 24.98/4.32 % (3059556)Termination reason: Instruction limit
% 24.98/4.32 % (3059556)Termination phase: Saturation
% 24.98/4.32 % (3059556)Time elapsed: 0.327 s
% 24.98/4.32 % (3059556)Peak memory usage: 93 MB
% 24.98/4.32 % (3059556)Instructions burned: 513 (million)
% 24.98/4.32 % (3059569)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3696352876:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2973 on theBenchmark for (2973ds/273Mi)
% 24.98/4.32 % (3059562)Instruction limit reached!
% 24.98/4.32 % (3059562)------------------------------
% 24.98/4.32 % (3059562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.32 % (3059562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.32 % (3059562)CaDiCaL version: 2.1.3
% 24.98/4.32 % (3059562)Termination reason: Instruction limit
% 24.98/4.32 % (3059562)Termination phase: Saturation
% 24.98/4.32 % (3059562)Time elapsed: 0.193 s
% 24.98/4.32 % (3059562)Peak memory usage: 118 MB
% 24.98/4.32 % (3059562)Instructions burned: 262 (million)
% 24.98/4.32 % (3059557)Instruction limit reached!
% 24.98/4.32 % (3059557)------------------------------
% 24.98/4.32 % (3059557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.32 % (3059557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.32 % (3059557)CaDiCaL version: 2.1.3
% 24.98/4.32 % (3059557)Termination reason: Instruction limit
% 24.98/4.32 % (3059557)Termination phase: Saturation
% 24.98/4.32 % (3059557)Time elapsed: 0.284 s
% 24.98/4.32 % (3059557)Peak memory usage: 135 MB
% 24.98/4.33 % (3059557)Instructions burned: 335 (million)
% 24.98/4.33 % (3059570)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=260928680:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi)
% 24.98/4.33 % (3059563)Instruction limit reached!
% 24.98/4.33 % (3059563)------------------------------
% 24.98/4.33 % (3059563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.33 % (3059563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.33 % (3059563)CaDiCaL version: 2.1.3
% 24.98/4.33 % (3059563)Termination reason: Instruction limit
% 24.98/4.33 % (3059563)Termination phase: Saturation
% 24.98/4.33 % (3059563)Time elapsed: 0.176 s
% 24.98/4.33 % (3059563)Peak memory usage: 117 MB
% 24.98/4.33 % (3059563)Instructions burned: 235 (million)
% 24.98/4.33 % (3059569)Instruction limit reached!
% 24.98/4.33 % (3059569)------------------------------
% 24.98/4.33 % (3059569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.33 % (3059569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.99/4.89 % (3059569)CaDiCaL version: 2.1.3
% 27.99/4.89 % (3059569)Termination reason: Instruction limit
% 27.99/4.89 % (3059569)Termination phase: Saturation
% 27.99/4.89 % (3059569)Time elapsed: 0.107 s
% 27.99/4.89 % (3059569)Peak memory usage: 91 MB
% 27.99/4.89 % (3059569)Instructions burned: 273 (million)
% 27.99/4.89 % (3059571)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3646648909:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 27.99/4.89 % (3059572)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=2270572689:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi)
% 27.99/4.89 % (3059570)Instruction limit reached!
% 27.99/4.89 % (3059570)------------------------------
% 27.99/4.89 % (3059570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.99/4.89 % (3059570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.99/4.89 % (3059570)CaDiCaL version: 2.1.3
% 27.99/4.89 % (3059570)Termination reason: Instruction limit
% 27.99/4.89 % (3059570)Termination phase: Saturation
% 27.99/4.89 % (3059570)Time elapsed: 0.100 s
% 27.99/4.89 % (3059570)Peak memory usage: 90 MB
% 27.99/4.89 % (3059570)Instructions burned: 146 (million)
% 27.99/4.89 % (3059574)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1036090773:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi)
% 27.99/4.89 % (3059575)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=966439575:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi)
% 27.99/4.89 % (3059577)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2514337771:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi)
% 27.99/4.89 % (3059578)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1446856853:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 27.99/4.89 % (3059578)Instruction limit reached!
% 27.99/4.89 % (3059578)------------------------------
% 27.99/4.89 % (3059578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.99/4.89 % (3059578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.99/4.89 % (3059578)CaDiCaL version: 2.1.3
% 27.99/4.89 % (3059578)Termination reason: Instruction limit
% 27.99/4.89 % (3059578)Termination phase: Saturation
% 27.99/4.89 % (3059578)Time elapsed: 0.049 s
% 27.99/4.89 % (3059578)Peak memory usage: 116 MB
% 27.99/4.89 % (3059578)Instructions burned: 109 (million)
% 27.99/4.89 % (3059581)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4119849646:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 27.99/4.89 % (3059572)Instruction limit reached!
% 27.99/4.89 % (3059572)------------------------------
% 27.99/4.89 % (3059572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.99/4.89 % (3059572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.99/4.89 % (3059572)CaDiCaL version: 2.1.3
% 27.99/4.89 % (3059572)Termination reason: Instruction limit
% 27.99/4.89 % (3059572)Termination phase: Saturation
% 27.99/4.89 % (3059572)Time elapsed: 0.232 s
% 27.99/4.89 % (3059572)Peak memory usage: 135 MB
% 27.99/4.89 % (3059572)Instructions burned: 276 (million)
% 27.99/4.89 % (3059586)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
% 27.99/4.89 % (3059586)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2781457768:i=1090:aac=none:nm=0:rtra=on:rawr=on_2970 on theBenchmark for (2970ds/1090Mi)
% 27.99/4.89 % (3059588)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1698632503:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi)
% 27.99/4.89 % (3059588)Instruction limit reached!
% 27.99/4.89 % (3059588)------------------------------
% 27.99/4.89 % (3059588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.99/4.89 % (3059588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.99/4.89 % (3059588)CaDiCaL version: 2.1.3
% 27.99/4.89 % (3059588)Termination reason: Instruction limit
% 27.99/4.89 % (3059588)Termination phase: Saturation
% 32.51/5.32 % (3059588)Time elapsed: 0.105 s
% 32.51/5.32 % (3059588)Peak memory usage: 117 MB
% 32.51/5.32 % (3059588)Instructions burned: 130 (million)
% 32.51/5.32 % (3059575)Instruction limit reached!
% 32.51/5.32 % (3059575)------------------------------
% 32.51/5.32 % (3059575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.32 % (3059575)CaDiCaL version: 2.1.3
% 32.51/5.32 % (3059575)Termination reason: Instruction limit
% 32.51/5.32 % (3059575)Termination phase: Saturation
% 32.51/5.32 % (3059575)Time elapsed: 0.448 s
% 32.51/5.32 % (3059575)Peak memory usage: 95 MB
% 32.51/5.32 % (3059575)Instructions burned: 656 (million)
% 32.51/5.32 % (3059581)Instruction limit reached!
% 32.51/5.32 % (3059581)------------------------------
% 32.51/5.32 % (3059581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.32 % (3059581)CaDiCaL version: 2.1.3
% 32.51/5.32 % (3059581)Termination reason: Instruction limit
% 32.51/5.32 % (3059581)Termination phase: Saturation
% 32.51/5.32 % (3059581)Time elapsed: 0.338 s
% 32.51/5.32 % (3059581)Peak memory usage: 135 MB
% 32.51/5.32 % (3059581)Instructions burned: 451 (million)
% 32.51/5.32 % (3059586)Instruction limit reached!
% 32.51/5.32 % (3059586)------------------------------
% 32.51/5.32 % (3059586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.32 % (3059586)CaDiCaL version: 2.1.3
% 32.51/5.32 % (3059586)Termination reason: Instruction limit
% 32.51/5.32 % (3059586)Termination phase: Saturation
% 32.51/5.32 % (3059586)Time elapsed: 0.332 s
% 32.51/5.32 % (3059586)Peak memory usage: 120 MB
% 32.51/5.32 % (3059586)Instructions burned: 1093 (million)
% 32.51/5.32 % (3059592)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2636931103:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi)
% 32.51/5.32 % (3059593)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=802721690:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi)
% 32.51/5.32 % (3059593)Refutation not found, incomplete strategy
% 32.51/5.32 % (3059593)------------------------------
% 32.51/5.32 % (3059593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.32 % (3059593)CaDiCaL version: 2.1.3
% 32.51/5.32 % (3059593)Termination reason: Refutation not found, incomplete strategy
% 32.51/5.32 % (3059593)Time elapsed: 0.008 s
% 32.51/5.32 % (3059593)Peak memory usage: 89 MB
% 32.51/5.32 % (3059593)Instructions burned: 12 (million)
% 32.51/5.32 % (3059594)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=919656894:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi)
% 32.51/5.32 % (3059577)Instruction limit reached!
% 32.51/5.32 % (3059577)------------------------------
% 32.51/5.32 % (3059577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.32 % (3059577)CaDiCaL version: 2.1.3
% 32.51/5.32 % (3059577)Termination reason: Instruction limit
% 32.51/5.32 % (3059577)Termination phase: Saturation
% 32.51/5.32 % (3059577)Time elapsed: 0.621 s
% 32.51/5.32 % (3059577)Peak memory usage: 97 MB
% 32.51/5.32 % (3059577)Instructions burned: 1054 (million)
% 32.51/5.32 % (3059595)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3985851011:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi)
% 32.51/5.32 % (3059574)Instruction limit reached!
% 32.51/5.32 % (3059574)------------------------------
% 32.51/5.32 % (3059574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.32 % (3059574)CaDiCaL version: 2.1.3
% 32.51/5.32 % (3059574)Termination reason: Instruction limit
% 32.51/5.32 % (3059574)Termination phase: Saturation
% 32.51/5.32 % (3059574)Time elapsed: 0.674 s
% 32.51/5.32 % (3059574)Peak memory usage: 93 MB
% 32.51/5.32 % (3059574)Instructions burned: 1052 (million)
% 32.51/5.32 % (3059595)Instruction limit reached!
% 32.51/5.32 % (3059595)------------------------------
% 32.51/5.32 % (3059595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.32 % (3059595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059595)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059595)Termination reason: Instruction limit
% 34.78/5.92 % (3059595)Termination phase: Saturation
% 34.78/5.92 % (3059595)Time elapsed: 0.104 s
% 34.78/5.92 % (3059595)Peak memory usage: 92 MB
% 34.78/5.92 % (3059595)Instructions burned: 309 (million)
% 34.78/5.92 % (3059599)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=340614328:i=776:doe=on:rtra=on_2964 on theBenchmark for (2964ds/776Mi)
% 34.78/5.92 % (3059592)Instruction limit reached!
% 34.78/5.92 % (3059592)------------------------------
% 34.78/5.92 % (3059592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059592)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059592)Termination reason: Instruction limit
% 34.78/5.92 % (3059592)Termination phase: Saturation
% 34.78/5.92 % (3059592)Time elapsed: 0.222 s
% 34.78/5.92 % (3059592)Peak memory usage: 118 MB
% 34.78/5.92 % (3059592)Instructions burned: 312 (million)
% 34.78/5.92 % (3059601)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1454674092:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/646Mi)
% 34.78/5.92 % (3059593)------------------------------
% 34.78/5.92 % (3059593)------------------------------
% 34.78/5.92 % (3059602)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=2434514092:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2963 on theBenchmark for (2963ds/784Mi)
% 34.78/5.92 % (3059604)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=1997768205:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi)
% 34.78/5.92 % (3059606)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=2546216747:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2962 on theBenchmark for (2962ds/246Mi)
% 34.78/5.92 % (3059602)Instruction limit reached!
% 34.78/5.92 % (3059602)------------------------------
% 34.78/5.92 % (3059602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059602)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059602)Termination reason: Instruction limit
% 34.78/5.92 % (3059602)Termination phase: Saturation
% 34.78/5.92 % (3059602)Time elapsed: 0.283 s
% 34.78/5.92 % (3059602)Peak memory usage: 121 MB
% 34.78/5.92 % (3059602)Instructions burned: 784 (million)
% 34.78/5.92 % (3059594)Instruction limit reached!
% 34.78/5.92 % (3059594)------------------------------
% 34.78/5.92 % (3059594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059594)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059594)Termination reason: Instruction limit
% 34.78/5.92 % (3059594)Termination phase: Saturation
% 34.78/5.92 % (3059594)Time elapsed: 0.559 s
% 34.78/5.92 % (3059594)Peak memory usage: 94 MB
% 34.78/5.92 % (3059594)Instructions burned: 836 (million)
% 34.78/5.92 % (3059606)Instruction limit reached!
% 34.78/5.92 % (3059606)------------------------------
% 34.78/5.92 % (3059606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059606)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059606)Termination reason: Instruction limit
% 34.78/5.92 % (3059606)Termination phase: Saturation
% 34.78/5.92 % (3059606)Time elapsed: 0.169 s
% 34.78/5.92 % (3059606)Peak memory usage: 117 MB
% 34.78/5.92 % (3059606)Instructions burned: 247 (million)
% 34.78/5.92 % (3059610)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2331933346:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/775Mi)
% 34.78/5.92 % (3059599)Instruction limit reached!
% 34.78/5.92 % (3059599)------------------------------
% 34.78/5.92 % (3059599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059599)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059599)Termination reason: Instruction limit
% 34.78/5.92 % (3059599)Termination phase: Saturation
% 34.78/5.92 % (3059599)Time elapsed: 0.524 s
% 34.78/5.92 % (3059599)Peak memory usage: 123 MB
% 34.78/5.92 % (3059599)Instructions burned: 777 (million)
% 34.78/5.92 % (3059601)Instruction limit reached!
% 34.78/5.92 % (3059601)------------------------------
% 34.78/5.92 % (3059601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059601)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059601)Termination reason: Instruction limit
% 34.78/5.92 % (3059601)Termination phase: Saturation
% 34.78/5.92 % (3059601)Time elapsed: 0.489 s
% 34.78/5.92 % (3059601)Peak memory usage: 139 MB
% 34.78/5.92 % (3059601)Instructions burned: 646 (million)
% 34.78/5.92 % (3059611)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1890902909:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi)
% 34.78/5.92 % (3059612)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=188659582:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi)
% 34.78/5.92 % (3059612)Instruction limit reached!
% 34.78/5.92 % (3059612)------------------------------
% 34.78/5.92 % (3059612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.92 % (3059612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.92 % (3059612)CaDiCaL version: 2.1.3
% 34.78/5.92 % (3059612)Termination reason: Instruction limit
% 34.78/5.92 % (3059612)Termination phase: Saturation
% 34.78/5.92 % (3059612)Time elapsed: 0.066 s
% 34.78/5.92 % (3059612)Peak memory usage: 89 MB
% 34.78/5.92 % (3059612)Instructions burned: 102 (million)
% 34.78/5.92 % (3059614)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2138390427:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi)
% 34.78/5.92 % (3059616)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3315908821:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi)
% 34.78/5.92 % (3059611)Instruction limit reached!
% 34.78/5.92 % (3059611)------------------------------
% 34.78/5.93 % (3059611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.93 % (3059611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.93 % (3059611)CaDiCaL version: 2.1.3
% 34.78/5.93 % (3059611)Termination reason: Instruction limit
% 34.78/5.93 % (3059611)Termination phase: Saturation
% 34.78/5.93 % (3059611)Time elapsed: 0.189 s
% 34.78/5.93 % (3059611)Peak memory usage: 92 MB
% 34.78/5.93 % (3059611)Instructions burned: 273 (million)
% 34.78/5.93 % (3059610)Instruction limit reached!
% 34.78/5.93 % (3059610)------------------------------
% 34.78/5.93 % (3059610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.93 % (3059610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.93 % (3059610)CaDiCaL version: 2.1.3
% 34.78/5.93 % (3059610)Termination reason: Instruction limit
% 34.78/5.93 % (3059610)Termination phase: Saturation
% 34.78/5.93 % (3059610)Time elapsed: 0.268 s
% 34.78/5.93 % (3059610)Peak memory usage: 95 MB
% 34.78/5.93 % (3059610)Instructions burned: 777 (million)
% 34.78/5.93 % (3059618)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=641850710:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/868Mi)
% 34.78/5.93 % (3059622)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2712965215:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi)
% 34.78/5.93 % (3059621)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=1957620836:i=1846:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/1846Mi)
% 34.78/5.93 % (3059604)Instruction limit reached!
% 34.78/5.93 % (3059604)------------------------------
% 34.78/5.93 % (3059604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.93 % (3059604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.93 % (3059604)CaDiCaL version: 2.1.3
% 34.78/5.93 % (3059604)Termination reason: Instruction limit
% 34.78/5.93 % (3059604)Termination phase: Saturation
% 34.78/5.93 % (3059604)Time elapsed: 0.786 s
% 34.78/5.93 % (3059604)Peak memory usage: 127 MB
% 34.78/5.93 % (3059604)Instructions burned: 1131 (million)
% 34.78/5.93 % (3059626)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=39006988:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2953 on theBenchmark for (2953ds/273Mi)
% 34.78/5.93 % (3059614)Instruction limit reached!
% 34.78/5.93 % (3059614)------------------------------
% 34.78/5.93 % (3059614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.93 % (3059614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.93 % (3059614)CaDiCaL version: 2.1.3
% 34.78/5.93 % (3059614)Termination reason: Instruction limit
% 34.78/5.93 % (3059614)Termination phase: Saturation
% 34.78/5.93 % (3059614)Time elapsed: 0.517 s
% 34.78/5.93 % (3059614)Peak memory usage: 94 MB
% 34.78/5.93 % (3059614)Instructions burned: 1095 (million)
% 34.78/5.93 % (3059626)First to succeed.
% 34.78/5.93 % (3059626)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3059426"
% 34.78/5.93 % (3059618)Instruction limit reached!
% 34.78/5.93 % (3059618)------------------------------
% 34.78/5.93 % (3059618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.78/5.93 % (3059618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.78/5.93 % (3059618)CaDiCaL version: 2.1.3
% 34.78/5.93 % (3059618)Termination reason: Instruction limit
% 34.78/5.93 % (3059618)Termination phase: Saturation
% 34.78/5.93 % (3059618)Time elapsed: 0.557 s
% 34.78/5.93 % (3059618)Peak memory usage: 121 MB
% 34.78/5.93 % (3059618)Instructions burned: 868 (million)
% 34.78/5.93 % (3059628)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=2808421885:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/863Mi)
% 34.78/5.93 % (3059629)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1342442302:i=5811:kws=precedence:nm=0:rtra=on_2949 on theBenchmark for (2949ds/5811Mi)
% 34.78/5.93 % (3059626)Refutation found. Thanks to Tanya!
% 34.78/5.93 % SZS status Theorem for theBenchmark
% 34.78/5.93 % SZS output start Proof for theBenchmark
% See solution above
% 37.85/6.13 % (3059626)------------------------------
% 37.85/6.13 % (3059626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.85/6.13 % (3059626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/6.13 % (3059626)CaDiCaL version: 2.1.3
% 37.85/6.13 % (3059626)Termination reason: Refutation
% 37.85/6.13 % (3059626)Time elapsed: 0.188 s
% 37.85/6.13 % (3059626)Peak memory usage: 92 MB
% 37.85/6.13 % (3059626)Instructions burned: 266 (million)
% 37.85/6.13 % (3059626)------------------------------
% 37.85/6.13 % (3059626)------------------------------
% 37.85/6.13 % (3059426)Success in time 5.265 s
% 37.85/6.13 % Vampire exiting
%------------------------------------------------------------------------------