%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW611_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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:56 PM UTC 2026
% Result : Theorem 24.81s 4.60s
% Output : Refutation 26.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 48
% Syntax : Number of formulae : 244 ( 31 unt; 0 typ; 37 def)
% Number of atoms : 1379 ( 258 equ)
% Maximal formula atoms : 68 ( 5 avg)
% Number of connectives : 1652 ( 517 ~; 597 |; 385 &)
% ( 47 <=>; 106 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 2377 ( 686 atm; 728 fun; 740 num; 223 var)
% Number of types : 10 ( 8 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 44 ( 40 usr; 38 prp; 0-5 aty)
% Number of functors : 54 ( 49 usr; 22 con; 0-5 aty)
% Number of variables : 387 ( 345 !; 42 ?; 387 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
char1: $tType ).
tff(type_def_10,type,
array_char: $tType ).
tff(type_def_11,type,
map_int_int: $tType ).
tff(type_def_12,type,
map_int_char: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length1: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
char: ty ).
tff(func_def_29,type,
t2tb1: array_char > uni ).
tff(func_def_30,type,
tb2t1: uni > array_char ).
tff(func_def_31,type,
t2tb2: char1 > uni ).
tff(func_def_32,type,
tb2t2: uni > char1 ).
tff(func_def_36,type,
t2tb3: map_int_int > uni ).
tff(func_def_37,type,
tb2t3: uni > map_int_int ).
tff(func_def_38,type,
t2tb4: map_int_char > uni ).
tff(func_def_39,type,
tb2t4: uni > map_int_char ).
tff(func_def_41,type,
sK0: ( array_char * $int * $int * array_char * $int ) > $int ).
tff(func_def_42,type,
sK1: ( $int * $int * array_char ) > $int ).
tff(func_def_43,type,
sK2: map_int_char ).
tff(func_def_44,type,
sK3: $int ).
tff(func_def_45,type,
sK4: map_int_int ).
tff(func_def_46,type,
sK5: $int ).
tff(func_def_47,type,
sK6: $int ).
tff(func_def_48,type,
sK7: map_int_int ).
tff(func_def_49,type,
sK8: $int > $int ).
tff(func_def_50,type,
sK9: $int ).
tff(func_def_51,type,
sK10: $int ).
tff(func_def_52,type,
sK11: map_int_int ).
tff(func_def_53,type,
sK12: $int ).
tff(func_def_54,type,
sK13: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
matches1: ( array_char * $int * array_char * $int * $int ) > $o ).
tff(pred_def_5,type,
is_next1: ( array_char * $int * $int ) > $o ).
tff(f15,axiom,
! [X5: uni,X1: ty,X2: uni,X4: uni,X3: uni,X0: ty] :
( sort1(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(f16,axiom,
! [X3: uni,X1: ty,X0: ty,X4: uni,X2: uni] :
( sort1(X0,X3)
=> ( sort1(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(f20,axiom,
! [X1: $int,X0: ty,X2: uni] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def2) ).
tff(f25,axiom,
! [X0: $int] : sort1(int,t2tb(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort3) ).
tff(f26,axiom,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL) ).
tff(f35,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f39,axiom,
! [X2: array_char,X4: $int,X0: array_char,X3: $int,X1: $int] :
( matches1(X0,X1,X2,X3,X4)
<=> ( $lesseq(X1,$difference(length1(char,t2tb1(X0)),X4))
& $lesseq(0,X3)
& $lesseq(X3,$difference(length1(char,t2tb1(X2)),X4))
& $lesseq(0,X1)
& ! [X5: $int] :
( ( $lesseq(0,X5)
& $less(X5,X4) )
=> ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matches_def) ).
tff(f46,axiom,
! [X4: $int,X2: $int,X1: array_char,X3: $int,X0: array_char] :
( matches1(X0,X2,X1,X3,X4)
=> matches1(X1,X3,X0,X2,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matches_sym) ).
tff(f48,axiom,
! [X1: $int,X2: $int,X0: array_char] :
( is_next1(X0,X1,X2)
<=> ( ! [X3: $int] :
( ( $less(X3,X1)
& $less(X2,X3) )
=> ~ matches1(X0,$difference(X1,X3),X0,0,X3) )
& $less(X2,X1)
& matches1(X0,$difference(X1,X2),X0,0,X2)
& $lesseq(0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',is_next_def) ).
tff(f54,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f58,conjecture,
! [X0: $int,X1: map_int_char] :
( ( ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ( $lesseq(0,X0)
=> ( ( ( 0 = X0 )
| $less(0,X0) )
=> ( $less(1,X0)
=> ( ( ( ( 0 = 1 )
| $less(0,1) )
& $less(1,X0) )
=> ! [X2: map_int_int] :
( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) ) )
=> ! [X5: map_int_int,X3: $int,X4: $int] :
( ( ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X3) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($difference(X4,X3),X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) ) )
& ( ( 0 = X3 )
| $less(0,X3) )
& $lesseq(0,$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X3))
& $lesseq(0,0)
& ( ( X4 = X0 )
| $less(X4,X0) )
& $less(X3,X4)
& $lesseq($difference(X4,X3),$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X3))
& ! [X8: $int] :
( ( $less(0,X8)
& ( $less(X8,X4)
| ( X8 = X4 ) ) )
=> ( matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$difference(X8,tb2t(get(int,int,t2tb3(X5),t2tb(X8)))),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,tb2t(get(int,int,t2tb3(X5),t2tb(X8))))
& ! [X7: $int] :
( ( $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),X7)
& $less(X7,X8) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$difference(X8,X7),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X7) )
& $lesseq(0,tb2t(get(int,int,t2tb3(X5),t2tb(X8))))
& $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),X8) ) )
& $lesseq(0,$difference(X4,X3))
& ! [X7: $int] :
( ( $less(X7,$sum(X4,1))
& $less($sum(X3,1),X7) )
=> ~ ( $lesseq(0,$difference($sum(X4,1),X7))
& ! [X6: $int] :
( ( $less(X6,X7)
& $lesseq(0,X6) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($difference($sum(X4,1),X7),X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) ) )
& $lesseq(0,$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X7))
& $lesseq(0,0)
& $lesseq($difference($sum(X4,1),X7),$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X7)) ) ) )
=> ( $less(X4,$difference(X0,1))
=> ( ( $less(X3,X0)
& ( ( 0 = X3 )
| $less(0,X3) ) )
=> ( ( ( ( 0 = X4 )
| $less(0,X4) )
& $less(X4,X0) )
=> ( ( tb2t2(get(char,int,t2tb4(X1),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X1),t2tb(X3))) )
=> ! [X6: $int] :
( ( X6 = $sum(X4,1) )
=> ! [X9: $int] :
( ( X9 = $sum(X3,1) )
=> ( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( $less(0,X6)
| ( 0 = X6 ) )
& $less(X6,X0) )
=> ! [X10: map_int_int] :
( ( ( X10 = tb2t3(set(int,int,t2tb3(X5),t2tb(X6),t2tb(X9))) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ! [X8: $int] :
( ( $less(0,X8)
& ( ( X8 = X6 )
| $less(X8,X6) ) )
=> ! [X7: $int] :
( ( $less(X7,X8)
& $less(tb2t(get(int,int,t2tb3(X10),t2tb(X8))),X7) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$difference(X8,X7),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X7) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_initnext) ).
tff(f59,negated_conjecture,
~ ! [X0: $int,X1: map_int_char] :
( ( ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ( $lesseq(0,X0)
=> ( ( ( 0 = X0 )
| $less(0,X0) )
=> ( $less(1,X0)
=> ( ( ( ( 0 = 1 )
| $less(0,1) )
& $less(1,X0) )
=> ! [X2: map_int_int] :
( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) ) )
=> ! [X5: map_int_int,X3: $int,X4: $int] :
( ( ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X3) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($difference(X4,X3),X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) ) )
& ( ( 0 = X3 )
| $less(0,X3) )
& $lesseq(0,$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X3))
& $lesseq(0,0)
& ( ( X4 = X0 )
| $less(X4,X0) )
& $less(X3,X4)
& $lesseq($difference(X4,X3),$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X3))
& ! [X8: $int] :
( ( $less(0,X8)
& ( $less(X8,X4)
| ( X8 = X4 ) ) )
=> ( matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$difference(X8,tb2t(get(int,int,t2tb3(X5),t2tb(X8)))),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,tb2t(get(int,int,t2tb3(X5),t2tb(X8))))
& ! [X7: $int] :
( ( $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),X7)
& $less(X7,X8) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$difference(X8,X7),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X7) )
& $lesseq(0,tb2t(get(int,int,t2tb3(X5),t2tb(X8))))
& $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),X8) ) )
& $lesseq(0,$difference(X4,X3))
& ! [X7: $int] :
( ( $less(X7,$sum(X4,1))
& $less($sum(X3,1),X7) )
=> ~ ( $lesseq(0,$difference($sum(X4,1),X7))
& ! [X6: $int] :
( ( $less(X6,X7)
& $lesseq(0,X6) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($difference($sum(X4,1),X7),X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) ) )
& $lesseq(0,$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X7))
& $lesseq(0,0)
& $lesseq($difference($sum(X4,1),X7),$difference(length1(char,mk_array1(char,X0,t2tb4(X1))),X7)) ) ) )
=> ( $less(X4,$difference(X0,1))
=> ( ( $less(X3,X0)
& ( ( 0 = X3 )
| $less(0,X3) ) )
=> ( ( ( ( 0 = X4 )
| $less(0,X4) )
& $less(X4,X0) )
=> ( ( tb2t2(get(char,int,t2tb4(X1),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X1),t2tb(X3))) )
=> ! [X6: $int] :
( ( X6 = $sum(X4,1) )
=> ! [X9: $int] :
( ( X9 = $sum(X3,1) )
=> ( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( $less(0,X6)
| ( 0 = X6 ) )
& $less(X6,X0) )
=> ! [X10: map_int_int] :
( ( ( X10 = tb2t3(set(int,int,t2tb3(X5),t2tb(X6),t2tb(X9))) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ! [X8: $int] :
( ( $less(0,X8)
& ( ( X8 = X6 )
| $less(X8,X6) ) )
=> ! [X7: $int] :
( ( $less(X7,X8)
& $less(tb2t(get(int,int,t2tb3(X10),t2tb(X8))),X7) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$difference(X8,X7),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X7) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
tff(f62,plain,
! [X1: $int,X2: $int,X0: array_char] :
( is_next1(X0,X1,X2)
<=> ( ! [X3: $int] :
( ( $less(X3,X1)
& $less(X2,X3) )
=> ~ matches1(X0,$sum(X1,$uminus(X3)),X0,0,X3) )
& $less(X2,X1)
& matches1(X0,$sum(X1,$uminus(X2)),X0,0,X2)
& ~ $less(X2,0) ) ),
inference(theory_normalization,[],[f48]) ).
tff(f63,plain,
~ ! [X0: $int,X1: map_int_char] :
( ( ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ( ~ $less(X0,0)
=> ( ( ( 0 = X0 )
| $less(0,X0) )
=> ( $less(1,X0)
=> ( ( ( ( 0 = 1 )
| $less(0,1) )
& $less(1,X0) )
=> ! [X2: map_int_int] :
( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) ) )
=> ! [X5: map_int_int,X3: $int,X4: $int] :
( ( ! [X6: $int] :
( ( ~ $less(X6,0)
& $less(X6,X3) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum(X4,$uminus(X3)),X6))) ) )
& ( ( 0 = X3 )
| $less(0,X3) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X3)),0)
& ~ $less(0,0)
& ( ( X4 = X0 )
| $less(X4,X0) )
& $less(X3,X4)
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X3)),$sum(X4,$uminus(X3)))
& ! [X8: $int] :
( ( $less(0,X8)
& ( $less(X8,X4)
| ( X8 = X4 ) ) )
=> ( matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X8,$uminus(tb2t(get(int,int,t2tb3(X5),t2tb(X8))))),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,tb2t(get(int,int,t2tb3(X5),t2tb(X8))))
& ! [X7: $int] :
( ( $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),X7)
& $less(X7,X8) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X8,$uminus(X7)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X7) )
& ~ $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),0)
& $less(tb2t(get(int,int,t2tb3(X5),t2tb(X8))),X8) ) )
& ~ $less($sum(X4,$uminus(X3)),0)
& ! [X7: $int] :
( ( $less(X7,$sum(X4,1))
& $less($sum(X3,1),X7) )
=> ~ ( ~ $less($sum($sum(X4,1),$uminus(X7)),0)
& ! [X6: $int] :
( ( $less(X6,X7)
& ~ $less(X6,0) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum($sum(X4,1),$uminus(X7)),X6))) ) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X7)),0)
& ~ $less(0,0)
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X7)),$sum($sum(X4,1),$uminus(X7))) ) ) )
=> ( $less(X4,$sum(X0,$uminus(1)))
=> ( ( $less(X3,X0)
& ( ( 0 = X3 )
| $less(0,X3) ) )
=> ( ( ( ( 0 = X4 )
| $less(0,X4) )
& $less(X4,X0) )
=> ( ( tb2t2(get(char,int,t2tb4(X1),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X1),t2tb(X3))) )
=> ! [X6: $int] :
( ( X6 = $sum(X4,1) )
=> ! [X9: $int] :
( ( X9 = $sum(X3,1) )
=> ( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( $less(0,X6)
| ( 0 = X6 ) )
& $less(X6,X0) )
=> ! [X10: map_int_int] :
( ( ( X10 = tb2t3(set(int,int,t2tb3(X5),t2tb(X6),t2tb(X9))) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ! [X8: $int] :
( ( $less(0,X8)
& ( ( X8 = X6 )
| $less(X8,X6) ) )
=> ! [X7: $int] :
( ( $less(X7,X8)
& $less(tb2t(get(int,int,t2tb3(X10),t2tb(X8))),X7) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X8,$uminus(X7)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X7) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f59]) ).
tff(f67,plain,
! [X2: array_char,X4: $int,X0: array_char,X3: $int,X1: $int] :
( matches1(X0,X1,X2,X3,X4)
<=> ( ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1)
& ~ $less(X3,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3)
& ~ $less(X1,0)
& ! [X5: $int] :
( ( ~ $less(X5,0)
& $less(X5,X4) )
=> ( tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5))) ) ) ) ),
inference(theory_normalization,[],[f39]) ).
tff(f71,plain,
~ ! [X1: map_int_char,X0: $int] :
( ( ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ( ~ $less(X0,0)
=> ( ( ( 0 = X0 )
| $less(0,X0) )
=> ( $less(1,X0)
=> ( ( ( ( 0 = 1 )
| $less(0,1) )
& $less(1,X0) )
=> ! [X2: map_int_int] :
( ( ( ( 0 = X0 )
| $less(0,X0) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) ) )
=> ! [X5: $int,X3: map_int_int,X4: $int] :
( ( $less(X4,X5)
& ( ( X0 = X5 )
| $less(X5,X0) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X4)),0)
& ! [X6: $int] :
( ( $less(X6,X4)
& ~ $less(X6,0) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum(X5,$uminus(X4)),X6))) ) )
& ! [X7: $int] :
( ( $less(0,X7)
& ( $less(X7,X5)
| ( X5 = X7 ) ) )
=> ( ~ $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),0)
& ! [X8: $int] :
( ( $less(X8,X7)
& $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),X8) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X8) )
& matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X7,$uminus(tb2t(get(int,int,t2tb3(X3),t2tb(X7))))),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,tb2t(get(int,int,t2tb3(X3),t2tb(X7))))
& $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),X7) ) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X4)),$sum(X5,$uminus(X4)))
& ! [X9: $int] :
( ( $less($sum(X4,1),X9)
& $less(X9,$sum(X5,1)) )
=> ~ ( ! [X10: $int] :
( ( $less(X10,X9)
& ~ $less(X10,0) )
=> ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum($sum(X5,1),$uminus(X9)),X10))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X10))) ) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X9)),$sum($sum(X5,1),$uminus(X9)))
& ~ $less($sum($sum(X5,1),$uminus(X9)),0)
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X9)),0)
& ~ $less(0,0) ) )
& ~ $less($sum(X5,$uminus(X4)),0)
& ~ $less(0,0)
& ( ( 0 = X4 )
| $less(0,X4) ) )
=> ( $less(X5,$sum(X0,$uminus(1)))
=> ( ( $less(X4,X0)
& ( ( 0 = X4 )
| $less(0,X4) ) )
=> ( ( ( $less(0,X5)
| ( 0 = X5 ) )
& $less(X5,X0) )
=> ( ( tb2t2(get(char,int,t2tb4(X1),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X1),t2tb(X5))) )
=> ! [X11: $int] :
( ( $sum(X5,1) = X11 )
=> ! [X12: $int] :
( ( $sum(X4,1) = X12 )
=> ( ( ( ( 0 = X0 )
| $less(0,X0) )
& $less(X11,X0)
& ( $less(0,X11)
| ( 0 = X11 ) ) )
=> ! [X13: map_int_int] :
( ( ( tb2t3(set(int,int,t2tb3(X3),t2tb(X11),t2tb(X12))) = X13 )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
=> ! [X14: $int] :
( ( ( $less(X14,X11)
| ( X11 = X14 ) )
& $less(0,X14) )
=> ! [X15: $int] :
( ( $less(X15,X14)
& $less(tb2t(get(int,int,t2tb3(X13),t2tb(X14))),X15) )
=> ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X14,$uminus(X15)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X15) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f63]) ).
tff(f72,plain,
! [X2: array_char,X3: $int,X0: $int,X1: $int,X4: array_char] :
( matches1(X4,X1,X2,X3,X0)
=> matches1(X2,X3,X4,X1,X0) ),
inference(rectify,[],[f46]) ).
tff(f77,plain,
! [X2: ty,X4: uni,X3: uni,X1: ty,X0: uni] :
( sort1(X2,X0)
=> ( sort1(X2,X3)
=> ! [X5: uni] :
( ( X0 != X3 )
=> ( get(X1,X2,set(X1,X2,X4,X0,X5),X3) = get(X1,X2,X4,X3) ) ) ) ),
inference(rectify,[],[f16]) ).
tff(f79,plain,
! [X5: ty,X1: ty,X4: uni,X3: uni,X2: uni,X0: uni] :
( sort1(X1,X0)
=> ( ( X3 = X4 )
=> ( get(X1,X5,set(X1,X5,X2,X4,X0),X3) = X0 ) ) ),
inference(rectify,[],[f15]) ).
tff(f82,plain,
! [X2: uni,X1: ty,X0: $int] : ( length1(X1,mk_array1(X1,X0,X2)) = X0 ),
inference(rectify,[],[f20]) ).
tff(f83,plain,
! [X3: $int,X4: $int,X0: array_char,X1: $int,X2: array_char] :
( matches1(X2,X4,X0,X3,X1)
<=> ( ~ $less(X4,0)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3)
& ~ $less(X3,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
& ! [X5: $int] :
( ( $less(X5,X1)
& ~ $less(X5,0) )
=> ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) ) ) ) ),
inference(rectify,[],[f67]) ).
tff(f91,plain,
! [X2: array_char,X1: $int,X0: $int] :
( is_next1(X2,X0,X1)
<=> ( $less(X1,X0)
& ~ $less(X1,0)
& ! [X3: $int] :
( ( $less(X1,X3)
& $less(X3,X0) )
=> ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) )
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1) ) ),
inference(rectify,[],[f62]) ).
tff(f98,plain,
! [X3: $int,X4: $int,X0: array_char,X1: $int,X2: array_char] :
( matches1(X2,X4,X0,X3,X1)
<=> ( ~ $less(X4,0)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3)
& ~ $less(X3,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
& ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) )
| ~ $less(X5,X1)
| $less(X5,0) ) ) ),
inference(ennf_transformation,[],[f83]) ).
tff(f99,plain,
! [X0: array_char,X1: $int,X4: $int,X2: array_char,X3: $int] :
( ( ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) )
| ~ $less(X5,X1)
| $less(X5,0) )
& ~ $less(X4,0)
& ~ $less(X3,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3) )
<=> matches1(X2,X4,X0,X3,X1) ),
inference(flattening,[],[f98]) ).
tff(f104,plain,
! [X5: ty,X1: ty,X4: uni,X3: uni,X2: uni,X0: uni] :
( ( get(X1,X5,set(X1,X5,X2,X4,X0),X3) = X0 )
| ( X3 != X4 )
| ~ sort1(X1,X0) ),
inference(ennf_transformation,[],[f79]) ).
tff(f105,plain,
! [X2: uni,X1: ty,X0: uni,X5: ty,X3: uni,X4: uni] :
( ( get(X1,X5,set(X1,X5,X2,X4,X0),X3) = X0 )
| ~ sort1(X1,X0)
| ( X3 != X4 ) ),
inference(flattening,[],[f104]) ).
tff(f107,plain,
? [X1: map_int_char,X0: $int] :
( ? [X2: map_int_int] :
( ? [X5: $int,X3: map_int_int,X4: $int] :
( ? [X11: $int] :
( ? [X12: $int] :
( ? [X13: map_int_int] :
( ? [X14: $int] :
( ? [X15: $int] :
( matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X14,$uminus(X15)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X15)
& $less(X15,X14)
& $less(tb2t(get(int,int,t2tb3(X13),t2tb(X14))),X15) )
& ( $less(X14,X11)
| ( X11 = X14 ) )
& $less(0,X14) )
& ( tb2t3(set(int,int,t2tb3(X3),t2tb(X11),t2tb(X12))) = X13 )
& ( $less(0,X0)
| ( 0 = X0 ) ) )
& ( ( 0 = X0 )
| $less(0,X0) )
& $less(X11,X0)
& ( $less(0,X11)
| ( 0 = X11 ) )
& ( $sum(X4,1) = X12 ) )
& ( $sum(X5,1) = X11 ) )
& ( tb2t2(get(char,int,t2tb4(X1),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X1),t2tb(X5))) )
& ( $less(0,X5)
| ( 0 = X5 ) )
& $less(X5,X0)
& $less(X4,X0)
& ( ( 0 = X4 )
| $less(0,X4) )
& $less(X5,$sum(X0,$uminus(1)))
& $less(X4,X5)
& ( ( X0 = X5 )
| $less(X5,X0) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X4)),0)
& ! [X6: $int] :
( ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum(X5,$uminus(X4)),X6))) )
| ~ $less(X6,X4)
| $less(X6,0) )
& ! [X7: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),0)
& ! [X8: $int] :
( ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X8)
| ~ $less(X8,X7)
| ~ $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),X8) )
& matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X7,$uminus(tb2t(get(int,int,t2tb3(X3),t2tb(X7))))),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,tb2t(get(int,int,t2tb3(X3),t2tb(X7))))
& $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),X7) )
| ~ $less(0,X7)
| ( ( X5 != X7 )
& ~ $less(X7,X5) ) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X4)),$sum(X5,$uminus(X4)))
& ! [X9: $int] :
( ? [X10: $int] :
( ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum($sum(X5,1),$uminus(X9)),X10))) != tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X10))) )
& $less(X10,X9)
& ~ $less(X10,0) )
| $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X9)),$sum($sum(X5,1),$uminus(X9)))
| $less($sum($sum(X5,1),$uminus(X9)),0)
| $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X9)),0)
| $less(0,0)
| ~ $less($sum(X4,1),X9)
| ~ $less(X9,$sum(X5,1)) )
& ~ $less($sum(X5,$uminus(X4)),0)
& ~ $less(0,0)
& ( ( 0 = X4 )
| $less(0,X4) ) )
& ( ( 0 = X0 )
| $less(0,X0) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) ) )
& ( ( 0 = 1 )
| $less(0,1) )
& $less(1,X0)
& $less(1,X0)
& ( ( 0 = X0 )
| $less(0,X0) )
& ~ $less(X0,0)
& ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(0,X0)
| ( 0 = X0 ) ) ),
inference(ennf_transformation,[],[f71]) ).
tff(f108,plain,
? [X1: map_int_char,X0: $int] :
( ~ $less(X0,0)
& $less(1,X0)
& ( ( 1 = X0 )
| $less(1,X0) )
& ? [X2: map_int_int] :
( ( ( 0 = X0 )
| $less(0,X0) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) )
& ? [X5: $int,X4: $int,X3: map_int_int] :
( ! [X6: $int] :
( ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X6))) = tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum(X5,$uminus(X4)),X6))) )
| ~ $less(X6,X4)
| $less(X6,0) )
& $less(X4,X0)
& ~ $less(0,0)
& $less(X5,X0)
& ! [X7: $int] :
( ~ $less(0,X7)
| ( ( X5 != X7 )
& ~ $less(X7,X5) )
| ( matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X7,$uminus(tb2t(get(int,int,t2tb3(X3),t2tb(X7))))),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,tb2t(get(int,int,t2tb3(X3),t2tb(X7))))
& ~ $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),0)
& $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),X7)
& ! [X8: $int] :
( ~ $less(tb2t(get(int,int,t2tb3(X3),t2tb(X7))),X8)
| ~ $less(X8,X7)
| ~ matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X8) ) ) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X4)),$sum(X5,$uminus(X4)))
& ! [X9: $int] :
( $less($sum($sum(X5,1),$uminus(X9)),0)
| ~ $less(X9,$sum(X5,1))
| $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X9)),0)
| $less(0,0)
| $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X9)),$sum($sum(X5,1),$uminus(X9)))
| ? [X10: $int] :
( ~ $less(X10,0)
& $less(X10,X9)
& ( tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum($sum($sum(X5,1),$uminus(X9)),X10))) != tb2t2(get2(char,mk_array1(char,X0,t2tb4(X1)),$sum(0,X10))) ) )
| ~ $less($sum(X4,1),X9) )
& $less(X4,X5)
& ? [X11: $int] :
( ? [X12: $int] :
( ( ( 0 = X0 )
| $less(0,X0) )
& ( $less(0,X11)
| ( 0 = X11 ) )
& $less(X11,X0)
& ? [X13: map_int_int] :
( ( tb2t3(set(int,int,t2tb3(X3),t2tb(X11),t2tb(X12))) = X13 )
& ( $less(0,X0)
| ( 0 = X0 ) )
& ? [X14: $int] :
( $less(0,X14)
& ( $less(X14,X11)
| ( X11 = X14 ) )
& ? [X15: $int] :
( matches1(tb2t1(mk_array1(char,X0,t2tb4(X1))),$sum(X14,$uminus(X15)),tb2t1(mk_array1(char,X0,t2tb4(X1))),0,X15)
& $less(X15,X14)
& $less(tb2t(get(int,int,t2tb3(X13),t2tb(X14))),X15) ) ) )
& ( $sum(X4,1) = X12 ) )
& ( $sum(X5,1) = X11 ) )
& ( ( 0 = X4 )
| $less(0,X4) )
& ~ $less($sum(X5,$uminus(X4)),0)
& ( ( X0 = X5 )
| $less(X5,X0) )
& ( ( 0 = X4 )
| $less(0,X4) )
& $less(X5,$sum(X0,$uminus(1)))
& ( tb2t2(get(char,int,t2tb4(X1),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X1),t2tb(X5))) )
& ( $less(0,X5)
| ( 0 = X5 ) )
& ~ $less($sum(length1(char,mk_array1(char,X0,t2tb4(X1))),$uminus(X4)),0) ) )
& ( $less(0,X0)
| ( 0 = X0 ) )
& ( ( 0 = 1 )
| $less(0,1) )
& ( ( 0 = X0 )
| $less(0,X0) )
& $less(1,X0) ),
inference(flattening,[],[f107]) ).
tff(f114,plain,
! [X2: array_char,X1: $int,X0: $int] :
( is_next1(X2,X0,X1)
<=> ( $less(X1,X0)
& ~ $less(X1,0)
& ! [X3: $int] :
( ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3)
| ~ $less(X1,X3)
| ~ $less(X3,X0) )
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1) ) ),
inference(ennf_transformation,[],[f91]) ).
tff(f115,plain,
! [X0: $int,X1: $int,X2: array_char] :
( ( $less(X1,X0)
& ~ $less(X1,0)
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
& ! [X3: $int] :
( ~ $less(X1,X3)
| ~ $less(X3,X0)
| ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) )
<=> is_next1(X2,X0,X1) ),
inference(flattening,[],[f114]) ).
tff(f118,plain,
! [X2: ty,X4: uni,X3: uni,X1: ty,X0: uni] :
( ! [X5: uni] :
( ( X0 = X3 )
| ( get(X1,X2,set(X1,X2,X4,X0,X5),X3) = get(X1,X2,X4,X3) ) )
| ~ sort1(X2,X3)
| ~ sort1(X2,X0) ),
inference(ennf_transformation,[],[f77]) ).
tff(f119,plain,
! [X0: uni,X2: ty,X1: ty,X4: uni,X3: uni] :
( ~ sort1(X2,X0)
| ! [X5: uni] :
( ( X0 = X3 )
| ( get(X1,X2,set(X1,X2,X4,X0,X5),X3) = get(X1,X2,X4,X3) ) )
| ~ sort1(X2,X3) ),
inference(flattening,[],[f118]) ).
tff(f120,plain,
! [X2: array_char,X1: $int,X3: $int,X0: $int,X4: array_char] :
( matches1(X2,X3,X4,X1,X0)
| ~ matches1(X4,X1,X2,X3,X0) ),
inference(ennf_transformation,[],[f72]) ).
tff(f123,plain,
! [X0: array_char,X1: $int,X4: $int,X2: array_char,X3: $int] :
( ( ( ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) )
| ~ $less(X5,X1)
| $less(X5,0) )
& ~ $less(X4,0)
& ~ $less(X3,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3) )
| ~ matches1(X2,X4,X0,X3,X1) )
& ( matches1(X2,X4,X0,X3,X1)
| ? [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) != tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) )
& $less(X5,X1)
& ~ $less(X5,0) )
| $less(X4,0)
| $less(X3,0)
| $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3) ) ),
inference(nnf_transformation,[],[f99]) ).
tff(f124,plain,
! [X0: array_char,X1: $int,X4: $int,X2: array_char,X3: $int] :
( ( ( ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) )
| ~ $less(X5,X1)
| $less(X5,0) )
& ~ $less(X4,0)
& ~ $less(X3,0)
& ~ $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3) )
| ~ matches1(X2,X4,X0,X3,X1) )
& ( matches1(X2,X4,X0,X3,X1)
| ? [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X3,X5))) != tb2t2(get2(char,t2tb1(X2),$sum(X4,X5))) )
& $less(X5,X1)
& ~ $less(X5,0) )
| $less(X4,0)
| $less(X3,0)
| $less($sum(length1(char,t2tb1(X2)),$uminus(X1)),X4)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X3) ) ),
inference(flattening,[],[f123]) ).
tff(f125,plain,
! [X0: array_char,X1: $int,X2: $int,X3: array_char,X4: $int] :
( ( ( ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X3),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X0),$sum(X4,X5))) )
| ~ $less(X5,X1)
| $less(X5,0) )
& ~ $less(X2,0)
& ~ $less(X4,0)
& ~ $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X2)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X4) )
| ~ matches1(X3,X2,X0,X4,X1) )
& ( matches1(X3,X2,X0,X4,X1)
| ? [X6: $int] :
( ( tb2t2(get2(char,t2tb1(X0),$sum(X4,X6))) != tb2t2(get2(char,t2tb1(X3),$sum(X2,X6))) )
& $less(X6,X1)
& ~ $less(X6,0) )
| $less(X2,0)
| $less(X4,0)
| $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X2)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X4) ) ),
inference(rectify,[],[f124]) ).
tff(f126,plain,
! [X0: array_char,X1: $int,X2: $int,X3: array_char,X4: $int] :
( ( ( ! [X5: $int] :
( ( tb2t2(get2(char,t2tb1(X3),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X0),$sum(X4,X5))) )
| ~ $less(X5,X1)
| $less(X5,0) )
& ~ $less(X2,0)
& ~ $less(X4,0)
& ~ $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X2)
& ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X4) )
| ~ matches1(X3,X2,X0,X4,X1) )
& ( matches1(X3,X2,X0,X4,X1)
| ( ( tb2t2(get2(char,t2tb1(X0),$sum(X4,sK0(X0,X1,X2,X3,X4)))) != tb2t2(get2(char,t2tb1(X3),$sum(X2,sK0(X0,X1,X2,X3,X4)))) )
& $less(sK0(X0,X1,X2,X3,X4),X1)
& ~ $less(sK0(X0,X1,X2,X3,X4),0) )
| $less(X2,0)
| $less(X4,0)
| $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X2)
| $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X6,sK0(X0,X1,X2,X3,X4))],[f125]) ).
tff(f131,plain,
! [X0: $int,X1: $int,X2: array_char] :
( ( ( $less(X1,X0)
& ~ $less(X1,0)
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
& ! [X3: $int] :
( ~ $less(X1,X3)
| ~ $less(X3,X0)
| ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) )
| ~ is_next1(X2,X0,X1) )
& ( is_next1(X2,X0,X1)
| ~ $less(X1,X0)
| $less(X1,0)
| ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| ? [X3: $int] :
( $less(X1,X3)
& $less(X3,X0)
& matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) ) ),
inference(nnf_transformation,[],[f115]) ).
tff(f132,plain,
! [X0: $int,X1: $int,X2: array_char] :
( ( ( $less(X1,X0)
& ~ $less(X1,0)
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
& ! [X3: $int] :
( ~ $less(X1,X3)
| ~ $less(X3,X0)
| ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) )
| ~ is_next1(X2,X0,X1) )
& ( is_next1(X2,X0,X1)
| ~ $less(X1,X0)
| $less(X1,0)
| ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| ? [X3: $int] :
( $less(X1,X3)
& $less(X3,X0)
& matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) ) ),
inference(flattening,[],[f131]) ).
tff(f133,plain,
! [X0: $int,X1: $int,X2: array_char] :
( ( ( $less(X1,X0)
& ~ $less(X1,0)
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
& ! [X3: $int] :
( ~ $less(X1,X3)
| ~ $less(X3,X0)
| ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) )
| ~ is_next1(X2,X0,X1) )
& ( is_next1(X2,X0,X1)
| ~ $less(X1,X0)
| $less(X1,0)
| ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| ? [X4: $int] :
( $less(X1,X4)
& $less(X4,X0)
& matches1(X2,$sum(X0,$uminus(X4)),X2,0,X4) ) ) ),
inference(rectify,[],[f132]) ).
tff(f134,plain,
! [X0: $int,X1: $int,X2: array_char] :
( ( ( $less(X1,X0)
& ~ $less(X1,0)
& matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
& ! [X3: $int] :
( ~ $less(X1,X3)
| ~ $less(X3,X0)
| ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3) ) )
| ~ is_next1(X2,X0,X1) )
& ( is_next1(X2,X0,X1)
| ~ $less(X1,X0)
| $less(X1,0)
| ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| ( $less(X1,sK1(X0,X1,X2))
& $less(sK1(X0,X1,X2),X0)
& matches1(X2,$sum(X0,$uminus(sK1(X0,X1,X2))),X2,0,sK1(X0,X1,X2)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X4,sK1(X0,X1,X2))],[f133]) ).
tff(f137,plain,
! [X0: array_char,X1: $int,X2: $int,X3: $int,X4: array_char] :
( matches1(X0,X2,X4,X1,X3)
| ~ matches1(X4,X1,X0,X2,X3) ),
inference(rectify,[],[f120]) ).
tff(f138,plain,
! [X0: uni,X1: ty,X2: $int] : ( length1(X1,mk_array1(X1,X2,X0)) = X2 ),
inference(rectify,[],[f82]) ).
tff(f143,plain,
! [X0: uni,X1: ty,X2: ty,X3: uni,X4: uni] :
( ~ sort1(X1,X0)
| ! [X5: uni] :
( ( X0 = X4 )
| ( get(X2,X1,X3,X4) = get(X2,X1,set(X2,X1,X3,X0,X5),X4) ) )
| ~ sort1(X1,X4) ),
inference(rectify,[],[f119]) ).
tff(f144,plain,
? [X0: map_int_char,X1: $int] :
( ~ $less(X1,0)
& $less(1,X1)
& ( ( 1 = X1 )
| $less(1,X1) )
& ? [X2: map_int_int] :
( ( ( 0 = X1 )
| $less(0,X1) )
& ( X2 = tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) )
& ? [X3: $int,X4: $int,X5: map_int_int] :
( ! [X6: $int] :
( ( tb2t2(get2(char,mk_array1(char,X1,t2tb4(X0)),$sum($sum(X3,$uminus(X4)),X6))) = tb2t2(get2(char,mk_array1(char,X1,t2tb4(X0)),$sum(0,X6))) )
| ~ $less(X6,X4)
| $less(X6,0) )
& $less(X4,X1)
& ~ $less(0,0)
& $less(X3,X1)
& ! [X7: $int] :
( ~ $less(0,X7)
| ( ( X3 != X7 )
& ~ $less(X7,X3) )
| ( matches1(tb2t1(mk_array1(char,X1,t2tb4(X0))),$sum(X7,$uminus(tb2t(get(int,int,t2tb3(X5),t2tb(X7))))),tb2t1(mk_array1(char,X1,t2tb4(X0))),0,tb2t(get(int,int,t2tb3(X5),t2tb(X7))))
& ~ $less(tb2t(get(int,int,t2tb3(X5),t2tb(X7))),0)
& $less(tb2t(get(int,int,t2tb3(X5),t2tb(X7))),X7)
& ! [X8: $int] :
( ~ $less(tb2t(get(int,int,t2tb3(X5),t2tb(X7))),X8)
| ~ $less(X8,X7)
| ~ matches1(tb2t1(mk_array1(char,X1,t2tb4(X0))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,X1,t2tb4(X0))),0,X8) ) ) )
& ~ $less($sum(length1(char,mk_array1(char,X1,t2tb4(X0))),$uminus(X4)),$sum(X3,$uminus(X4)))
& ! [X9: $int] :
( $less($sum($sum(X3,1),$uminus(X9)),0)
| ~ $less(X9,$sum(X3,1))
| $less($sum(length1(char,mk_array1(char,X1,t2tb4(X0))),$uminus(X9)),0)
| $less(0,0)
| $less($sum(length1(char,mk_array1(char,X1,t2tb4(X0))),$uminus(X9)),$sum($sum(X3,1),$uminus(X9)))
| ? [X10: $int] :
( ~ $less(X10,0)
& $less(X10,X9)
& ( tb2t2(get2(char,mk_array1(char,X1,t2tb4(X0)),$sum(0,X10))) != tb2t2(get2(char,mk_array1(char,X1,t2tb4(X0)),$sum($sum($sum(X3,1),$uminus(X9)),X10))) ) )
| ~ $less($sum(X4,1),X9) )
& $less(X4,X3)
& ? [X11: $int] :
( ? [X12: $int] :
( ( ( 0 = X1 )
| $less(0,X1) )
& ( $less(0,X11)
| ( 0 = X11 ) )
& $less(X11,X1)
& ? [X13: map_int_int] :
( ( tb2t3(set(int,int,t2tb3(X5),t2tb(X11),t2tb(X12))) = X13 )
& ( $less(0,X1)
| ( 0 = X1 ) )
& ? [X14: $int] :
( $less(0,X14)
& ( $less(X14,X11)
| ( X11 = X14 ) )
& ? [X15: $int] :
( matches1(tb2t1(mk_array1(char,X1,t2tb4(X0))),$sum(X14,$uminus(X15)),tb2t1(mk_array1(char,X1,t2tb4(X0))),0,X15)
& $less(X15,X14)
& $less(tb2t(get(int,int,t2tb3(X13),t2tb(X14))),X15) ) ) )
& ( $sum(X4,1) = X12 ) )
& ( $sum(X3,1) = X11 ) )
& ( ( 0 = X4 )
| $less(0,X4) )
& ~ $less($sum(X3,$uminus(X4)),0)
& ( ( X1 = X3 )
| $less(X3,X1) )
& ( ( 0 = X4 )
| $less(0,X4) )
& $less(X3,$sum(X1,$uminus(1)))
& ( tb2t2(get(char,int,t2tb4(X0),t2tb(X4))) = tb2t2(get(char,int,t2tb4(X0),t2tb(X3))) )
& ( $less(0,X3)
| ( 0 = X3 ) )
& ~ $less($sum(length1(char,mk_array1(char,X1,t2tb4(X0))),$uminus(X4)),0) ) )
& ( $less(0,X1)
| ( 0 = X1 ) )
& ( ( 0 = 1 )
| $less(0,1) )
& ( ( 0 = X1 )
| $less(0,X1) )
& $less(1,X1) ),
inference(rectify,[],[f108]) ).
tff(f145,plain,
( ~ $less(sK3,0)
& $less(1,sK3)
& ( ( 1 = sK3 )
| $less(1,sK3) )
& ( ( 0 = sK3 )
| $less(0,sK3) )
& ( tb2t3(set(int,int,const(int,int,t2tb(0)),t2tb(1),t2tb(0))) = sK4 )
& ! [X6: $int] :
( ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum(sK5,$uminus(sK6)),X6))) = tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum(0,X6))) )
| ~ $less(X6,sK6)
| $less(X6,0) )
& $less(sK6,sK3)
& ~ $less(0,0)
& $less(sK5,sK3)
& ! [X7: $int] :
( ~ $less(0,X7)
| ( ( sK5 != X7 )
& ~ $less(X7,sK5) )
| ( matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(X7,$uminus(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))))),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t(get(int,int,t2tb3(sK7),t2tb(X7))))
& ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),0)
& $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),X7)
& ! [X8: $int] :
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),X8)
| ~ $less(X8,X7)
| ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X8) ) ) )
& ~ $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(sK6)),$sum(sK5,$uminus(sK6)))
& ! [X9: $int] :
( $less($sum($sum(sK5,1),$uminus(X9)),0)
| ~ $less(X9,$sum(sK5,1))
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| $less(0,0)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ( ~ $less(sK8(X9),0)
& $less(sK8(X9),X9)
& ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum(0,sK8(X9)))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(X9)),sK8(X9)))) ) )
| ~ $less($sum(sK6,1),X9) )
& $less(sK6,sK5)
& ( ( 0 = sK3 )
| $less(0,sK3) )
& ( $less(0,sK9)
| ( 0 = sK9 ) )
& $less(sK9,sK3)
& ( sK11 = tb2t3(set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10))) )
& ( $less(0,sK3)
| ( 0 = sK3 ) )
& $less(0,sK12)
& ( $less(sK12,sK9)
| ( sK12 = sK9 ) )
& matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,sK13)
& $less(sK13,sK12)
& $less(tb2t(get(int,int,t2tb3(sK11),t2tb(sK12))),sK13)
& ( $sum(sK6,1) = sK10 )
& ( sK9 = $sum(sK5,1) )
& ( ( 0 = sK6 )
| $less(0,sK6) )
& ~ $less($sum(sK5,$uminus(sK6)),0)
& ( ( sK3 = sK5 )
| $less(sK5,sK3) )
& ( ( 0 = sK6 )
| $less(0,sK6) )
& $less(sK5,$sum(sK3,$uminus(1)))
& ( tb2t2(get(char,int,t2tb4(sK2),t2tb(sK5))) = tb2t2(get(char,int,t2tb4(sK2),t2tb(sK6))) )
& ( $less(0,sK5)
| ( 0 = sK5 ) )
& ~ $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(sK6)),0)
& ( $less(0,sK3)
| ( 0 = sK3 ) )
& ( ( 0 = 1 )
| $less(0,1) )
& ( ( 0 = sK3 )
| $less(0,sK3) )
& $less(1,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X10,sK8(X9)),skolemize(X11,sK9),skolemize(X12,sK10),skolemize(X13,sK11),skolemize(X14,sK12),skolemize(X15,sK13)],[f144]) ).
tff(f146,plain,
! [X0: uni,X1: ty,X2: uni,X3: ty,X4: uni,X5: uni] :
( ( get(X1,X3,set(X1,X3,X0,X5,X2),X4) = X2 )
| ~ sort1(X1,X2)
| ( X4 != X5 ) ),
inference(rectify,[],[f105]) ).
tff(f154,plain,
! [X2: $int,X3: array_char,X0: array_char,X1: $int,X4: $int] :
( ~ $less($sum(length1(char,t2tb1(X0)),$uminus(X1)),X4)
| ~ matches1(X3,X2,X0,X4,X1) ),
inference(cnf_transformation,[],[f126]) ).
tff(f157,plain,
! [X2: $int,X3: array_char,X0: array_char,X1: $int,X4: $int] :
( ~ matches1(X3,X2,X0,X4,X1)
| ~ $less(X2,0) ),
inference(cnf_transformation,[],[f126]) ).
tff(f158,plain,
! [X2: $int,X3: array_char,X0: array_char,X1: $int,X4: $int,X5: $int] :
( ( tb2t2(get2(char,t2tb1(X3),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X0),$sum(X4,X5))) )
| ~ matches1(X3,X2,X0,X4,X1)
| $less(X5,0)
| ~ $less(X5,X1) ),
inference(cnf_transformation,[],[f126]) ).
tff(f159,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f35]) ).
tff(f160,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f54]) ).
tff(f161,plain,
! [X0: $int] : sort1(int,t2tb(X0)),
inference(cnf_transformation,[],[f25]) ).
tff(f167,plain,
! [X2: array_char,X0: $int,X1: $int] :
( matches1(X2,$sum(X0,$uminus(sK1(X0,X1,X2))),X2,0,sK1(X0,X1,X2))
| ~ $less(X1,X0)
| ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| $less(X1,0)
| is_next1(X2,X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
tff(f168,plain,
! [X2: array_char,X0: $int,X1: $int] :
( ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| ~ $less(X1,X0)
| is_next1(X2,X0,X1)
| $less(sK1(X0,X1,X2),X0)
| $less(X1,0) ),
inference(cnf_transformation,[],[f134]) ).
tff(f169,plain,
! [X2: array_char,X0: $int,X1: $int] :
( ~ matches1(X2,$sum(X0,$uminus(X1)),X2,0,X1)
| is_next1(X2,X0,X1)
| $less(X1,sK1(X0,X1,X2))
| $less(X1,0)
| ~ $less(X1,X0) ),
inference(cnf_transformation,[],[f134]) ).
tff(f170,plain,
! [X2: array_char,X3: $int,X0: $int,X1: $int] :
( ~ matches1(X2,$sum(X0,$uminus(X3)),X2,0,X3)
| ~ is_next1(X2,X0,X1)
| ~ $less(X1,X3)
| ~ $less(X3,X0) ),
inference(cnf_transformation,[],[f134]) ).
tff(f178,plain,
! [X2: $int,X3: $int,X0: array_char,X1: $int,X4: array_char] :
( matches1(X0,X2,X4,X1,X3)
| ~ matches1(X4,X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f137]) ).
tff(f179,plain,
! [X2: $int,X0: uni,X1: ty] : ( length1(X1,mk_array1(X1,X2,X0)) = X2 ),
inference(cnf_transformation,[],[f138]) ).
tff(f184,plain,
! [X2: ty,X3: uni,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( get(X2,X1,X3,X4) = get(X2,X1,set(X2,X1,X3,X0,X5),X4) )
| ~ sort1(X1,X0)
| ( X0 = X4 )
| ~ sort1(X1,X4) ),
inference(cnf_transformation,[],[f143]) ).
tff(f198,plain,
( $less(0,sK6)
| ( 0 = sK6 ) ),
inference(cnf_transformation,[],[f145]) ).
tff(f199,plain,
sK9 = $sum(sK5,1),
inference(cnf_transformation,[],[f145]) ).
tff(f200,plain,
$sum(sK6,1) = sK10,
inference(cnf_transformation,[],[f145]) ).
tff(f201,plain,
$less(tb2t(get(int,int,t2tb3(sK11),t2tb(sK12))),sK13),
inference(cnf_transformation,[],[f145]) ).
tff(f202,plain,
$less(sK13,sK12),
inference(cnf_transformation,[],[f145]) ).
tff(f203,plain,
matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,sK13),
inference(cnf_transformation,[],[f145]) ).
tff(f204,plain,
( $less(sK12,sK9)
| ( sK12 = sK9 ) ),
inference(cnf_transformation,[],[f145]) ).
tff(f205,plain,
$less(0,sK12),
inference(cnf_transformation,[],[f145]) ).
tff(f207,plain,
sK11 = tb2t3(set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10))),
inference(cnf_transformation,[],[f145]) ).
tff(f211,plain,
$less(sK6,sK5),
inference(cnf_transformation,[],[f145]) ).
tff(f212,plain,
! [X9: $int] :
( $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| $less(0,0)
| ~ $less($sum(sK6,1),X9)
| ~ $less(X9,$sum(sK5,1))
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum(0,sK8(X9)))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(X9)),sK8(X9)))) )
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9))) ),
inference(cnf_transformation,[],[f145]) ).
tff(f213,plain,
! [X9: $int] :
( $less($sum($sum(sK5,1),$uminus(X9)),0)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ~ $less(X9,$sum(sK5,1))
| $less(sK8(X9),X9)
| $less(0,0)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| ~ $less($sum(sK6,1),X9) ),
inference(cnf_transformation,[],[f145]) ).
tff(f214,plain,
! [X9: $int] :
( ~ $less(sK8(X9),0)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| $less(0,0)
| ~ $less(X9,$sum(sK5,1))
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| ~ $less($sum(sK6,1),X9)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9))) ),
inference(cnf_transformation,[],[f145]) ).
tff(f216,plain,
! [X8: $int,X7: $int] :
( ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X8)
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),X8)
| ~ $less(X7,sK5)
| ~ $less(0,X7)
| ~ $less(X8,X7) ),
inference(cnf_transformation,[],[f145]) ).
tff(f220,plain,
! [X8: $int,X7: $int] :
( ~ $less(0,X7)
| ( sK5 != X7 )
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),X8)
| ~ $less(X8,X7)
| ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(X7,$uminus(X8)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X8) ),
inference(cnf_transformation,[],[f145]) ).
tff(f221,plain,
! [X7: $int] :
( ~ $less(0,X7)
| ( sK5 != X7 )
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),X7) ),
inference(cnf_transformation,[],[f145]) ).
tff(f222,plain,
! [X7: $int] :
( ~ $less(0,X7)
| ( sK5 != X7 )
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))),0) ),
inference(cnf_transformation,[],[f145]) ).
tff(f223,plain,
! [X7: $int] :
( ~ $less(0,X7)
| ( sK5 != X7 )
| matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(X7,$uminus(tb2t(get(int,int,t2tb3(sK7),t2tb(X7))))),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t(get(int,int,t2tb3(sK7),t2tb(X7)))) ),
inference(cnf_transformation,[],[f145]) ).
tff(f224,plain,
$less(sK5,sK3),
inference(cnf_transformation,[],[f145]) ).
tff(f233,plain,
! [X2: uni,X3: ty,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( get(X1,X3,set(X1,X3,X0,X5,X2),X4) = X2 )
| ~ sort1(X1,X2)
| ( X4 != X5 ) ),
inference(cnf_transformation,[],[f146]) ).
tff(f235,plain,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f26]) ).
tff(f240,plain,
( ~ $less(0,sK5)
| matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5)))) ),
inference(equality_resolution,[],[f223]) ).
tff(f241,plain,
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),0)
| ~ $less(0,sK5) ),
inference(equality_resolution,[],[f222]) ).
tff(f242,plain,
( ~ $less(0,sK5)
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK5) ),
inference(equality_resolution,[],[f221]) ).
tff(f243,plain,
! [X8: $int] :
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),X8)
| ~ $less(0,sK5)
| ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(X8)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X8)
| ~ $less(X8,sK5) ),
inference(equality_resolution,[],[f220]) ).
tff(f244,plain,
! [X2: uni,X3: ty,X0: uni,X1: ty,X5: uni] :
( ( get(X1,X3,set(X1,X3,X0,X5,X2),X5) = X2 )
| ~ sort1(X1,X2) ),
inference(equality_resolution,[],[f233]) ).
tff(f247,plain,
! [X9: $int] :
( $less($sum($sum(sK5,1),$uminus(X9)),0)
| ~ $less(sK8(X9),0)
| ~ $less(X9,$sum(sK5,1))
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ~ $less($sum(sK6,1),X9)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0) ),
inference(evaluation,[],[f214]) ).
tff(f248,plain,
! [X9: $int] :
( ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(X9))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(X9)),sK8(X9)))) )
| ~ $less(X9,$sum(sK5,1))
| ~ $less($sum(sK6,1),X9)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0) ),
inference(evaluation,[],[f212]) ).
tff(f250,plain,
! [X9: $int] :
( $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ~ $less(X9,$sum(sK5,1))
| $less(sK8(X9),X9)
| ~ $less($sum(sK6,1),X9)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| $less($sum($sum(sK5,1),$uminus(X9)),0) ),
inference(evaluation,[],[f213]) ).
tff(f252,definition,
( spl14_1
<=> ( sK9 = $sum(sK5,1) ) ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
tff(f254,plain,
( ( sK9 = $sum(sK5,1) )
| ~ spl14_1 ),
inference(avatar_component_clause,[],[f252]) ).
tff(f255,plain,
spl14_1,
inference(avatar_split_clause,[],[f199,f252]) ).
tff(f271,definition,
( spl14_5
<=> $less(0,sK5) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
tff(f291,definition,
( spl14_9
<=> $less(0,sK6) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
tff(f295,definition,
( spl14_10
<=> ( 0 = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
tff(f300,definition,
( spl14_11
<=> $less(0,sK12) ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
tff(f302,plain,
( $less(0,sK12)
| ~ spl14_11 ),
inference(avatar_component_clause,[],[f300]) ).
tff(f303,plain,
spl14_11,
inference(avatar_split_clause,[],[f205,f300]) ).
tff(f305,definition,
( spl14_12
<=> matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5)))) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
tff(f307,plain,
( matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f305]) ).
tff(f308,plain,
( ~ spl14_5
| spl14_12 ),
inference(avatar_split_clause,[],[f240,f305,f271]) ).
tff(f315,plain,
! [X9: $int] :
( $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| ~ $less(sK8(X9),0)
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| $less($sum(sK3,$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ~ $less($sum(sK6,1),X9)
| ~ $less(X9,$sum(sK5,1)) ),
inference(forward_demodulation,[],[f247,f179]) ).
tff(f317,definition,
( spl14_14
<=> $less(sK13,sK12) ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
tff(f319,plain,
( $less(sK13,sK12)
| ~ spl14_14 ),
inference(avatar_component_clause,[],[f317]) ).
tff(f320,plain,
spl14_14,
inference(avatar_split_clause,[],[f202,f317]) ).
tff(f322,definition,
( spl14_15
<=> ( sK11 = tb2t3(set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10))) ) ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
tff(f324,plain,
( ( sK11 = tb2t3(set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10))) )
| ~ spl14_15 ),
inference(avatar_component_clause,[],[f322]) ).
tff(f325,plain,
spl14_15,
inference(avatar_split_clause,[],[f207,f322]) ).
tff(f331,plain,
! [X9: $int] :
( $less($sum($sum(sK5,1),$uminus(X9)),0)
| ~ $less($sum(sK6,1),X9)
| ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(X9))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(X9)),sK8(X9)))) )
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| ~ $less(X9,$sum(sK5,1))
| $less($sum(sK3,$uminus(X9)),$sum($sum(sK5,1),$uminus(X9))) ),
inference(forward_demodulation,[],[f248,f179]) ).
tff(f339,definition,
( spl14_18
<=> $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),0) ),
introduced(definition,[new_symbols(definition,[spl14_18])],[avatar_definition]) ).
tff(f341,plain,
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),0)
| spl14_18 ),
inference(avatar_component_clause,[],[f339]) ).
tff(f342,plain,
( ~ spl14_18
| ~ spl14_5 ),
inference(avatar_split_clause,[],[f241,f271,f339]) ).
tff(f359,definition,
( spl14_22
<=> $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK5) ),
introduced(definition,[new_symbols(definition,[spl14_22])],[avatar_definition]) ).
tff(f361,plain,
( $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK5)
| ~ spl14_22 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f362,plain,
( ~ spl14_5
| spl14_22 ),
inference(avatar_split_clause,[],[f242,f359,f271]) ).
tff(f368,plain,
! [X9: $int] :
( $less($sum(sK3,$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(X9)),0)
| $less(sK8(X9),X9)
| ~ $less($sum(sK6,1),X9)
| ~ $less(X9,$sum(sK5,1)) ),
inference(forward_demodulation,[],[f250,f179]) ).
tff(f370,definition,
( spl14_24
<=> $less(sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl14_24])],[avatar_definition]) ).
tff(f373,plain,
spl14_24,
inference(avatar_split_clause,[],[f211,f370]) ).
tff(f381,definition,
( spl14_26
<=> matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,sK13) ),
introduced(definition,[new_symbols(definition,[spl14_26])],[avatar_definition]) ).
tff(f383,plain,
( matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,sK13)
| ~ spl14_26 ),
inference(avatar_component_clause,[],[f381]) ).
tff(f384,plain,
spl14_26,
inference(avatar_split_clause,[],[f203,f381]) ).
tff(f390,definition,
( spl14_28
<=> $less(sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl14_28])],[avatar_definition]) ).
tff(f395,definition,
( spl14_29
<=> $less(tb2t(get(int,int,t2tb3(sK11),t2tb(sK12))),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_29])],[avatar_definition]) ).
tff(f397,plain,
( $less(tb2t(get(int,int,t2tb3(sK11),t2tb(sK12))),sK13)
| ~ spl14_29 ),
inference(avatar_component_clause,[],[f395]) ).
tff(f398,plain,
spl14_29,
inference(avatar_split_clause,[],[f201,f395]) ).
tff(f400,definition,
( spl14_30
<=> ( sK12 = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl14_30])],[avatar_definition]) ).
tff(f401,plain,
( ( sK12 != sK9 )
| spl14_30 ),
inference(avatar_component_clause,[],[f400]) ).
tff(f402,plain,
( ( sK12 = sK9 )
| ~ spl14_30 ),
inference(avatar_component_clause,[],[f400]) ).
tff(f404,definition,
( spl14_31
<=> $less(sK12,sK9) ),
introduced(definition,[new_symbols(definition,[spl14_31])],[avatar_definition]) ).
tff(f406,plain,
( $less(sK12,sK9)
| ~ spl14_31 ),
inference(avatar_component_clause,[],[f404]) ).
tff(f407,plain,
( spl14_30
| spl14_31 ),
inference(avatar_split_clause,[],[f204,f404,f400]) ).
tff(f409,definition,
( spl14_32
<=> ( $sum(sK6,1) = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl14_32])],[avatar_definition]) ).
tff(f411,plain,
( ( $sum(sK6,1) = sK10 )
| ~ spl14_32 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
spl14_32,
inference(avatar_split_clause,[],[f200,f409]) ).
tff(f413,plain,
spl14_28,
inference(avatar_split_clause,[],[f224,f390]) ).
tff(f415,plain,
( spl14_10
| spl14_9 ),
inference(avatar_split_clause,[],[f198,f291,f295]) ).
tff(f417,definition,
( spl14_33
<=> ! [X8: $int] :
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),X8)
| ~ $less(X8,sK5)
| ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(X8)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X8) ) ),
introduced(definition,[new_symbols(definition,[spl14_33])],[avatar_definition]) ).
tff(f418,plain,
( ! [X8: $int] :
( ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(X8)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X8)
| ~ $less(X8,sK5)
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),X8) )
| ~ spl14_33 ),
inference(avatar_component_clause,[],[f417]) ).
tff(f419,plain,
( ~ spl14_5
| spl14_33 ),
inference(avatar_split_clause,[],[f243,f417,f271]) ).
tff(f420,plain,
! [X9: $int] :
( $less($sum(sK3,$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ~ $less(sK8(X9),0)
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| $less($sum(sK3,$uminus(X9)),0)
| ~ $less($sum(sK6,1),X9)
| ~ $less(X9,$sum(sK5,1)) ),
inference(forward_demodulation,[],[f315,f179]) ).
tff(f421,plain,
! [X9: $int] :
( ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(X9))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(X9)),sK8(X9)))) )
| ~ $less($sum(sK6,1),X9)
| $less($sum(sK3,$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| $less($sum(sK3,$uminus(X9)),0)
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| ~ $less(X9,$sum(sK5,1)) ),
inference(forward_demodulation,[],[f331,f179]) ).
tff(f427,plain,
! [X9: $int] :
( $less($sum(sK3,$uminus(X9)),$sum($sum(sK5,1),$uminus(X9)))
| ~ $less($sum(sK6,1),X9)
| $less($sum($sum(sK5,1),$uminus(X9)),0)
| $less($sum(sK3,$uminus(X9)),0)
| $less(sK8(X9),X9)
| ~ $less(X9,$sum(sK5,1)) ),
inference(forward_demodulation,[],[f368,f179]) ).
tff(f433,plain,
( $less(tb2t(get(int,int,t2tb3(tb2t3(set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10)))),t2tb(sK12))),sK13)
| ~ spl14_15
| ~ spl14_29 ),
inference(forward_demodulation,[],[f397,f324]) ).
tff(f434,plain,
( $less(sK13,sK9)
| ~ spl14_14
| ~ spl14_30 ),
inference(forward_demodulation,[],[f319,f402]) ).
tff(f435,plain,
( $less(tb2t(get(int,int,t2tb3(tb2t3(set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10)))),t2tb(sK9))),sK13)
| ~ spl14_15
| ~ spl14_29
| ~ spl14_30 ),
inference(forward_demodulation,[],[f433,f402]) ).
tff(f436,plain,
( $less(sK13,$sum(sK5,1))
| ~ spl14_1
| ~ spl14_14
| ~ spl14_30 ),
inference(forward_demodulation,[],[f434,f254]) ).
tff(f437,plain,
( $less(tb2t(get(int,int,t2tb3(tb2t3(set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb(sK10)))),t2tb($sum(sK5,1)))),sK13)
| ~ spl14_1
| ~ spl14_15
| ~ spl14_29
| ~ spl14_30 ),
inference(forward_demodulation,[],[f435,f254]) ).
tff(f439,definition,
( spl14_36
<=> $less(sK13,$sum(sK5,1)) ),
introduced(definition,[new_symbols(definition,[spl14_36])],[avatar_definition]) ).
tff(f441,plain,
( $less(sK13,$sum(sK5,1))
| ~ spl14_36 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,plain,
( spl14_36
| ~ spl14_1
| ~ spl14_14
| ~ spl14_30 ),
inference(avatar_split_clause,[],[f436,f400,f317,f252,f439]) ).
tff(f443,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb(sK10)),t2tb($sum(sK5,1)))),sK13)
| ~ spl14_1
| ~ spl14_15
| ~ spl14_29
| ~ spl14_30 ),
inference(forward_demodulation,[],[f437,f160]) ).
tff(f444,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb($sum(sK6,1))),t2tb($sum(sK5,1)))),sK13)
| ~ spl14_1
| ~ spl14_15
| ~ spl14_29
| ~ spl14_30
| ~ spl14_32 ),
inference(forward_demodulation,[],[f443,f411]) ).
tff(f446,definition,
( spl14_37
<=> $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb($sum(sK6,1))),t2tb($sum(sK5,1)))),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_37])],[avatar_definition]) ).
tff(f448,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb($sum(sK6,1))),t2tb($sum(sK5,1)))),sK13)
| ~ spl14_37 ),
inference(avatar_component_clause,[],[f446]) ).
tff(f449,plain,
( spl14_37
| ~ spl14_1
| ~ spl14_15
| ~ spl14_29
| ~ spl14_30
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f444,f409,f400,f395,f322,f252,f446]) ).
tff(f485,plain,
( ~ $less($sum(length1(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))))),$uminus(sK13)),0)
| ~ spl14_26 ),
inference(unit_resulting_resolution,[],[f154,f383]) ).
tff(f489,plain,
( matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),sK13)
| ~ spl14_26 ),
inference(unit_resulting_resolution,[],[f178,f383]) ).
tff(f495,plain,
( ~ $less($sum(sK12,$uminus(sK13)),0)
| ~ spl14_26 ),
inference(resolution,[],[f383,f157]) ).
tff(f498,plain,
( ~ $less($sum(sK9,$uminus(sK13)),0)
| ~ spl14_26
| ~ spl14_30 ),
inference(forward_demodulation,[],[f495,f402]) ).
tff(f504,plain,
( ~ $less($sum(length1(char,mk_array1(char,sK3,t2tb4(sK2))),$uminus(sK13)),0)
| ~ spl14_26 ),
inference(forward_demodulation,[],[f485,f159]) ).
tff(f508,plain,
( ~ $less($sum($sum(sK5,1),$uminus(sK13)),0)
| ~ spl14_1
| ~ spl14_26
| ~ spl14_30 ),
inference(forward_demodulation,[],[f498,f254]) ).
tff(f518,plain,
( ~ $less($sum(sK3,$uminus(sK13)),0)
| ~ spl14_26 ),
inference(forward_demodulation,[],[f504,f179]) ).
tff(f523,definition,
( spl14_43
<=> $less($sum($sum(sK5,1),$uminus(sK13)),0) ),
introduced(definition,[new_symbols(definition,[spl14_43])],[avatar_definition]) ).
tff(f525,plain,
( ~ $less($sum($sum(sK5,1),$uminus(sK13)),0)
| spl14_43 ),
inference(avatar_component_clause,[],[f523]) ).
tff(f526,plain,
( ~ spl14_43
| ~ spl14_1
| ~ spl14_26
| ~ spl14_30 ),
inference(avatar_split_clause,[],[f508,f400,f381,f252,f523]) ).
tff(f535,definition,
( spl14_45
<=> $less($sum(sK3,$uminus(sK13)),0) ),
introduced(definition,[new_symbols(definition,[spl14_45])],[avatar_definition]) ).
tff(f537,plain,
( ~ $less($sum(sK3,$uminus(sK13)),0)
| spl14_45 ),
inference(avatar_component_clause,[],[f535]) ).
tff(f538,plain,
( ~ spl14_45
| ~ spl14_26 ),
inference(avatar_split_clause,[],[f518,f381,f535]) ).
tff(f548,definition,
( spl14_46
<=> $less($sum(sK3,$uminus(sK13)),$sum($sum(sK5,1),$uminus(sK13))) ),
introduced(definition,[new_symbols(definition,[spl14_46])],[avatar_definition]) ).
tff(f550,plain,
( ~ $less($sum(sK3,$uminus(sK13)),$sum($sum(sK5,1),$uminus(sK13)))
| spl14_46 ),
inference(avatar_component_clause,[],[f548]) ).
tff(f606,plain,
( ( sK12 != $sum(sK5,1) )
| ~ spl14_1
| spl14_30 ),
inference(forward_demodulation,[],[f401,f254]) ).
tff(f612,plain,
( $less(sK12,$sum(sK5,1))
| ~ spl14_1
| ~ spl14_31 ),
inference(forward_demodulation,[],[f406,f254]) ).
tff(f623,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb(sK9),t2tb(sK10)),t2tb(sK12))),sK13)
| ~ spl14_15
| ~ spl14_29 ),
inference(forward_demodulation,[],[f433,f160]) ).
tff(f625,definition,
( spl14_59
<=> matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_59])],[avatar_definition]) ).
tff(f627,plain,
( matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK12,$uminus(sK13)),sK13)
| ~ spl14_59 ),
inference(avatar_component_clause,[],[f625]) ).
tff(f628,plain,
( spl14_59
| ~ spl14_26 ),
inference(avatar_split_clause,[],[f489,f381,f625]) ).
tff(f633,definition,
( spl14_60
<=> ( sK12 = $sum(sK5,1) ) ),
introduced(definition,[new_symbols(definition,[spl14_60])],[avatar_definition]) ).
tff(f634,plain,
( ( sK12 = $sum(sK5,1) )
| ~ spl14_60 ),
inference(avatar_component_clause,[],[f633]) ).
tff(f635,plain,
( ( sK12 != $sum(sK5,1) )
| spl14_60 ),
inference(avatar_component_clause,[],[f633]) ).
tff(f636,plain,
( ~ spl14_60
| ~ spl14_1
| spl14_30 ),
inference(avatar_split_clause,[],[f606,f400,f252,f633]) ).
tff(f638,definition,
( spl14_61
<=> $less(sK12,$sum(sK5,1)) ),
introduced(definition,[new_symbols(definition,[spl14_61])],[avatar_definition]) ).
tff(f641,plain,
( spl14_61
| ~ spl14_1
| ~ spl14_31 ),
inference(avatar_split_clause,[],[f612,f404,f252,f638]) ).
tff(f643,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb(sK9),t2tb($sum(sK6,1))),t2tb(sK12))),sK13)
| ~ spl14_15
| ~ spl14_29
| ~ spl14_32 ),
inference(forward_demodulation,[],[f623,f411]) ).
tff(f655,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb($sum(sK6,1))),t2tb(sK12))),sK13)
| ~ spl14_1
| ~ spl14_15
| ~ spl14_29
| ~ spl14_32 ),
inference(forward_demodulation,[],[f643,f254]) ).
tff(f658,definition,
( spl14_64
<=> $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb($sum(sK6,1))),t2tb(sK12))),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_64])],[avatar_definition]) ).
tff(f660,plain,
( $less(tb2t(get(int,int,set(int,int,t2tb3(sK7),t2tb($sum(sK5,1)),t2tb($sum(sK6,1))),t2tb(sK12))),sK13)
| ~ spl14_64 ),
inference(avatar_component_clause,[],[f658]) ).
tff(f661,plain,
( spl14_64
| ~ spl14_1
| ~ spl14_15
| ~ spl14_29
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f655,f409,f395,f322,f252,f658]) ).
tff(f681,plain,
( ~ sort1(int,t2tb($sum(sK5,1)))
| ~ sort1(int,t2tb(sK12))
| ( t2tb(sK12) = t2tb($sum(sK5,1)) )
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ spl14_64 ),
inference(superposition,[],[f660,f184]) ).
tff(f692,plain,
( ( t2tb(sK12) = t2tb($sum(sK5,1)) )
| ~ sort1(int,t2tb(sK12))
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ spl14_64 ),
inference(forward_subsumption_resolution,[],[f681,f161]) ).
tff(f693,plain,
( ( t2tb(sK12) = t2tb($sum(sK5,1)) )
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ spl14_64 ),
inference(forward_subsumption_resolution,[],[f692,f161]) ).
tff(f695,definition,
( spl14_70
<=> ( t2tb(sK12) = t2tb($sum(sK5,1)) ) ),
introduced(definition,[new_symbols(definition,[spl14_70])],[avatar_definition]) ).
tff(f697,plain,
( ( t2tb(sK12) = t2tb($sum(sK5,1)) )
| ~ spl14_70 ),
inference(avatar_component_clause,[],[f695]) ).
tff(f699,definition,
( spl14_71
<=> $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_71])],[avatar_definition]) ).
tff(f701,plain,
( $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ spl14_71 ),
inference(avatar_component_clause,[],[f699]) ).
tff(f702,plain,
( spl14_70
| spl14_71
| ~ spl14_64 ),
inference(avatar_split_clause,[],[f693,f658,f699,f695]) ).
tff(f711,plain,
( ~ sort1(int,t2tb($sum(sK6,1)))
| $less(tb2t(t2tb($sum(sK6,1))),sK13)
| ~ spl14_37 ),
inference(superposition,[],[f448,f244]) ).
tff(f717,plain,
( $less(tb2t(t2tb($sum(sK6,1))),sK13)
| ~ spl14_37 ),
inference(forward_subsumption_resolution,[],[f711,f161]) ).
tff(f718,plain,
( $less($sum(sK6,1),sK13)
| ~ spl14_37 ),
inference(forward_demodulation,[],[f717,f235]) ).
tff(f720,definition,
( spl14_74
<=> $less($sum(sK6,1),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_74])],[avatar_definition]) ).
tff(f722,plain,
( $less($sum(sK6,1),sK13)
| ~ spl14_74 ),
inference(avatar_component_clause,[],[f720]) ).
tff(f723,plain,
( spl14_74
| ~ spl14_37 ),
inference(avatar_split_clause,[],[f718,f446,f720]) ).
tff(f737,plain,
( ! [X0: $int] :
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,X0,tb2t1(mk_array1(char,sK3,t2tb4(sK2)))))
| ~ $less(X0,sK5)
| ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(X0)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X0)
| $less(X0,0)
| ~ $less(sK1(sK5,X0,tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),sK5)
| is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,X0) )
| ~ spl14_33 ),
inference(resolution,[],[f418,f167]) ).
tff(f743,plain,
( ! [X0: $int] :
( ~ matches1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),$sum(sK5,$uminus(X0)),tb2t1(mk_array1(char,sK3,t2tb4(sK2))),0,X0)
| $less(X0,0)
| is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,X0)
| ~ $less(X0,sK5)
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,X0,tb2t1(mk_array1(char,sK3,t2tb4(sK2))))) )
| ~ spl14_33 ),
inference(forward_subsumption_resolution,[],[f737,f168]) ).
tff(f765,plain,
( is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK5)
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),tb2t1(mk_array1(char,sK3,t2tb4(sK2)))))
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),0)
| ~ spl14_12 ),
inference(resolution,[],[f307,f169]) ).
tff(f771,plain,
( $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),tb2t1(mk_array1(char,sK3,t2tb4(sK2)))))
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),0)
| is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))
| ~ spl14_12
| ~ spl14_22 ),
inference(forward_subsumption_resolution,[],[f765,f361]) ).
tff(f793,plain,
( is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))
| $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),tb2t1(mk_array1(char,sK3,t2tb4(sK2)))))
| ~ spl14_12
| spl14_18
| ~ spl14_22 ),
inference(forward_subsumption_resolution,[],[f771,f341]) ).
tff(f799,definition,
( spl14_81
<=> $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),tb2t1(mk_array1(char,sK3,t2tb4(sK2))))) ),
introduced(definition,[new_symbols(definition,[spl14_81])],[avatar_definition]) ).
tff(f801,plain,
( $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),sK1(sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))),tb2t1(mk_array1(char,sK3,t2tb4(sK2)))))
| ~ spl14_81 ),
inference(avatar_component_clause,[],[f799]) ).
tff(f803,definition,
( spl14_82
<=> is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5)))) ),
introduced(definition,[new_symbols(definition,[spl14_82])],[avatar_definition]) ).
tff(f806,plain,
( spl14_81
| spl14_82
| ~ spl14_12
| spl14_18
| ~ spl14_22 ),
inference(avatar_split_clause,[],[f793,f359,f339,f305,f803,f799]) ).
tff(f898,plain,
( ~ $less(sK13,sK12)
| ~ $less(0,sK12)
| ~ $less(sK12,sK5)
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ spl14_26 ),
inference(resolution,[],[f216,f383]) ).
tff(f909,plain,
( ~ $less(sK12,sK5)
| ~ $less(0,sK12)
| ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ spl14_14
| ~ spl14_26 ),
inference(forward_subsumption_resolution,[],[f898,f319]) ).
tff(f911,plain,
( ~ $less(tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))),sK13)
| ~ $less(sK12,sK5)
| ~ spl14_11
| ~ spl14_14
| ~ spl14_26 ),
inference(forward_subsumption_resolution,[],[f909,f302]) ).
tff(f913,plain,
( ~ $less(sK12,sK5)
| ~ spl14_11
| ~ spl14_14
| ~ spl14_26
| ~ spl14_71 ),
inference(forward_subsumption_resolution,[],[f911,f701]) ).
tff(f916,definition,
( spl14_90
<=> $less(sK12,sK5) ),
introduced(definition,[new_symbols(definition,[spl14_90])],[avatar_definition]) ).
tff(f919,plain,
( ~ spl14_90
| ~ spl14_11
| ~ spl14_14
| ~ spl14_26
| ~ spl14_71 ),
inference(avatar_split_clause,[],[f913,f699,f381,f317,f300,f916]) ).
tff(f965,plain,
( ~ is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK12,tb2t(get(int,int,t2tb3(sK7),t2tb(sK12))))
| ~ spl14_14
| ~ spl14_26
| ~ spl14_71 ),
inference(unit_resulting_resolution,[],[f170,f319,f383,f701]) ).
tff(f973,definition,
( spl14_94
<=> is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK12,tb2t(get(int,int,t2tb3(sK7),t2tb(sK12)))) ),
introduced(definition,[new_symbols(definition,[spl14_94])],[avatar_definition]) ).
tff(f976,plain,
( ~ spl14_94
| ~ spl14_14
| ~ spl14_26
| ~ spl14_71 ),
inference(avatar_split_clause,[],[f965,f699,f381,f317,f973]) ).
tff(f1510,plain,
( is_next1(tb2t1(mk_array1(char,sK3,t2tb4(sK2))),sK5,tb2t(get(int,int,t2tb3(sK7),t2tb(sK5))))
| ~ spl14_12
| spl14_18
| ~ spl14_22
| ~ spl14_33
| ~ spl14_81 ),
inference(unit_resulting_resolution,[],[f743,f341,f361,f801,f307]) ).
tff(f1523,plain,
( spl14_82
| ~ spl14_12
| spl14_18
| ~ spl14_22
| ~ spl14_33
| ~ spl14_81 ),
inference(avatar_split_clause,[],[f1510,f799,f417,f359,f339,f305,f803]) ).
tff(f1629,plain,
( ( sK12 = tb2t(t2tb($sum(sK5,1))) )
| ~ spl14_70 ),
inference(superposition,[],[f235,f697]) ).
tff(f1653,plain,
( ( sK12 = $sum(sK5,1) )
| ~ spl14_70 ),
inference(forward_demodulation,[],[f1629,f235]) ).
tff(f1689,plain,
( $false
| spl14_60
| ~ spl14_70 ),
inference(forward_subsumption_resolution,[],[f1653,f635]) ).
tff(f1690,plain,
( spl14_60
| ~ spl14_70 ),
inference(avatar_contradiction_clause,[],[f1689]) ).
tff(f1773,plain,
( ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(sK13))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(sK13)),sK8(sK13)))) )
| ~ spl14_36
| spl14_43
| spl14_45
| spl14_46
| ~ spl14_74 ),
inference(unit_resulting_resolution,[],[f421,f441,f722,f537,f525,f550]) ).
tff(f1774,plain,
( $less(sK8(sK13),sK13)
| ~ spl14_36
| spl14_43
| spl14_45
| spl14_46
| ~ spl14_74 ),
inference(unit_resulting_resolution,[],[f427,f441,f722,f537,f525,f550]) ).
tff(f1775,plain,
( ~ $less(sK8(sK13),0)
| ~ spl14_36
| spl14_43
| spl14_45
| spl14_46
| ~ spl14_74 ),
inference(unit_resulting_resolution,[],[f420,f441,f722,f537,f525,f550]) ).
tff(f1780,definition,
( spl14_159
<=> $less(sK8(sK13),0) ),
introduced(definition,[new_symbols(definition,[spl14_159])],[avatar_definition]) ).
tff(f1782,plain,
( ~ $less(sK8(sK13),0)
| spl14_159 ),
inference(avatar_component_clause,[],[f1780]) ).
tff(f1783,plain,
( ~ spl14_159
| ~ spl14_36
| spl14_43
| spl14_45
| spl14_46
| ~ spl14_74 ),
inference(avatar_split_clause,[],[f1775,f720,f548,f535,f523,f439,f1780]) ).
tff(f1787,definition,
( spl14_160
<=> ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(sK13))) = tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(sK13)),sK8(sK13)))) ) ),
introduced(definition,[new_symbols(definition,[spl14_160])],[avatar_definition]) ).
tff(f1789,plain,
( ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(sK13))) != tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(sK13)),sK8(sK13)))) )
| spl14_160 ),
inference(avatar_component_clause,[],[f1787]) ).
tff(f1790,plain,
( ~ spl14_160
| ~ spl14_36
| spl14_43
| spl14_45
| spl14_46
| ~ spl14_74 ),
inference(avatar_split_clause,[],[f1773,f720,f548,f535,f523,f439,f1787]) ).
tff(f1792,definition,
( spl14_161
<=> $less(sK8(sK13),sK13) ),
introduced(definition,[new_symbols(definition,[spl14_161])],[avatar_definition]) ).
tff(f1794,plain,
( $less(sK8(sK13),sK13)
| ~ spl14_161 ),
inference(avatar_component_clause,[],[f1792]) ).
tff(f1795,plain,
( spl14_161
| ~ spl14_36
| spl14_43
| spl14_45
| spl14_46
| ~ spl14_74 ),
inference(avatar_split_clause,[],[f1774,f720,f548,f535,f523,f439,f1792]) ).
tff(f1807,plain,
( ( tb2t2(get2(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),$sum(0,sK8(sK13)))) = tb2t2(get2(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),$sum($sum(sK12,$uminus(sK13)),sK8(sK13)))) )
| ~ spl14_59
| spl14_159
| ~ spl14_161 ),
inference(unit_resulting_resolution,[],[f158,f627,f1782,f1794]) ).
tff(f1814,plain,
( ( tb2t2(get2(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),sK8(sK13))) = tb2t2(get2(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),$sum($sum(sK12,$uminus(sK13)),sK8(sK13)))) )
| ~ spl14_59
| spl14_159
| ~ spl14_161 ),
inference(evaluation,[],[f1807]) ).
tff(f1817,plain,
( ( tb2t2(get2(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),sK8(sK13))) = tb2t2(get2(char,t2tb1(tb2t1(mk_array1(char,sK3,t2tb4(sK2)))),$sum($sum($sum(sK5,1),$uminus(sK13)),sK8(sK13)))) )
| ~ spl14_59
| ~ spl14_60
| spl14_159
| ~ spl14_161 ),
inference(forward_demodulation,[],[f1814,f634]) ).
tff(f1833,plain,
( ( tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),sK8(sK13))) = tb2t2(get2(char,mk_array1(char,sK3,t2tb4(sK2)),$sum($sum($sum(sK5,1),$uminus(sK13)),sK8(sK13)))) )
| ~ spl14_59
| ~ spl14_60
| spl14_159
| ~ spl14_161 ),
inference(forward_demodulation,[],[f1817,f159]) ).
tff(f1850,plain,
( $false
| ~ spl14_59
| ~ spl14_60
| spl14_159
| spl14_160
| ~ spl14_161 ),
inference(forward_subsumption_resolution,[],[f1833,f1789]) ).
tff(f1851,plain,
( ~ spl14_59
| ~ spl14_60
| spl14_159
| spl14_160
| ~ spl14_161 ),
inference(avatar_contradiction_clause,[],[f1850]) ).
tff(f1854,plain,
$false,
inference(avatar_smt_refutation,[],[f1851,f1795,f1790,f1783,f1690,f1523,f976,f919,f806,f723,f702,f661,f641,f636,f628,f538,f526,f449,f442,f419,f415,f413,f412,f407,f398,f384,f373,f362,f342,f325,f320,f308,f303,f255]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW611_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n006.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 14:22:27 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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.94/1.37 % (3998266)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.94/1.37 % (3998310)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2636808190:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.94/1.37 % (3998310)Instruction limit reached!
% 3.94/1.37 % (3998310)------------------------------
% 3.94/1.37 % (3998310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.37 % (3998310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.37 % (3998310)CaDiCaL version: 2.1.3
% 3.94/1.37 % (3998310)Termination reason: Instruction limit
% 3.94/1.37 % (3998310)Termination phase: Saturation
% 3.94/1.37 % (3998310)Time elapsed: 0.003 s
% 3.94/1.37 % (3998310)Peak memory usage: 87 MB
% 3.94/1.37 % (3998310)Instructions burned: 10 (million)
% 3.94/1.37 % (3998311)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3512488419:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.94/1.37 % (3998308)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3709826847:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.94/1.37 % (3998309)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3989300230:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.94/1.37 % (3998307)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1873815939:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.94/1.37 % (3998311)Instruction limit reached!
% 3.94/1.37 % (3998311)------------------------------
% 3.94/1.37 % (3998311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.37 % (3998311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.37 % (3998311)CaDiCaL version: 2.1.3
% 3.94/1.37 % (3998311)Termination reason: Instruction limit
% 3.94/1.37 % (3998311)Termination phase: Preprocessing 3
% 3.94/1.37 % (3998311)Time elapsed: 0.003 s
% 3.94/1.37 % (3998311)Peak memory usage: 86 MB
% 3.94/1.37 % (3998311)Instructions burned: 5 (million)
% 3.94/1.37 % (3998307)Instruction limit reached!
% 3.94/1.37 % (3998307)------------------------------
% 3.94/1.37 % (3998307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.37 % (3998307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.37 % (3998307)CaDiCaL version: 2.1.3
% 3.94/1.37 % (3998307)Termination reason: Instruction limit
% 3.94/1.37 % (3998307)Termination phase: Saturation
% 3.94/1.37 % (3998307)Time elapsed: 0.022 s
% 3.94/1.37 % (3998307)Peak memory usage: 101 MB
% 3.94/1.37 % (3998307)Instructions burned: 12 (million)
% 3.94/1.37 % (3998312)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2702564314:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.94/1.37 % (3998313)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=495309760:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.94/1.37 % (3998312)Instruction limit reached!
% 3.94/1.37 % (3998312)------------------------------
% 3.94/1.37 % (3998312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.37 % (3998312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.37 % (3998312)CaDiCaL version: 2.1.3
% 3.94/1.37 % (3998312)Termination reason: Instruction limit
% 3.94/1.37 % (3998312)Termination phase: Saturation
% 3.94/1.37 % (3998312)Time elapsed: 0.071 s
% 3.94/1.37 % (3998312)Peak memory usage: 116 MB
% 3.94/1.37 % (3998312)Instructions burned: 46 (million)
% 3.94/1.37 % (3998315)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=122558195:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.94/1.37 % (3998313)Instruction limit reached!
% 3.94/1.37 % (3998313)------------------------------
% 3.94/1.37 % (3998313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.37 % (3998313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.37 % (3998313)CaDiCaL version: 2.1.3
% 3.94/1.37 % (3998313)Termination reason: Instruction limit
% 3.94/1.37 % (3998313)Termination phase: Saturation
% 3.94/1.37 % (3998313)Time elapsed: 0.044 s
% 3.94/1.37 % (3998313)Peak memory usage: 116 MB
% 3.94/1.37 % (3998313)Instructions burned: 33 (million)
% 3.94/1.37 % (3998315)Instruction limit reached!
% 3.94/1.37 % (3998315)------------------------------
% 6.80/1.76 % (3998315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/1.76 % (3998315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.76 % (3998315)CaDiCaL version: 2.1.3
% 6.80/1.76 % (3998315)Termination reason: Instruction limit
% 6.80/1.76 % (3998315)Termination phase: Saturation
% 6.80/1.76 % (3998315)Time elapsed: 0.007 s
% 6.80/1.76 % (3998315)Peak memory usage: 88 MB
% 6.80/1.76 % (3998315)Instructions burned: 14 (million)
% 6.80/1.76 % (3998309)Instruction limit reached!
% 6.80/1.76 % (3998309)------------------------------
% 6.80/1.76 % (3998309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/1.76 % (3998309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.76 % (3998309)CaDiCaL version: 2.1.3
% 6.80/1.76 % (3998309)Termination reason: Instruction limit
% 6.80/1.76 % (3998309)Termination phase: Saturation
% 6.80/1.76 % (3998309)Time elapsed: 0.240 s
% 6.80/1.76 % (3998309)Peak memory usage: 118 MB
% 6.80/1.76 % (3998309)Instructions burned: 201 (million)
% 6.80/1.76 % (3998320)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=3087448706:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 6.80/1.76 % (3998323)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1806502590:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 6.80/1.76 % (3998320)Instruction limit reached!
% 6.80/1.76 % (3998320)------------------------------
% 6.80/1.76 % (3998320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/1.76 % (3998320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.76 % (3998320)CaDiCaL version: 2.1.3
% 6.80/1.76 % (3998320)Termination reason: Instruction limit
% 6.80/1.76 % (3998320)Termination phase: Saturation
% 6.80/1.76 % (3998320)Time elapsed: 0.034 s
% 6.80/1.76 % (3998320)Peak memory usage: 89 MB
% 6.80/1.76 % (3998320)Instructions burned: 29 (million)
% 6.80/1.76 % (3998323)Instruction limit reached!
% 6.80/1.76 % (3998323)------------------------------
% 6.80/1.76 % (3998323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/1.77 % (3998323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.77 % (3998323)CaDiCaL version: 2.1.3
% 6.80/1.77 % (3998323)Termination reason: Instruction limit
% 6.80/1.77 % (3998323)Termination phase: Saturation
% 6.80/1.77 % (3998323)Time elapsed: 0.017 s
% 6.80/1.77 % (3998323)Peak memory usage: 88 MB
% 6.80/1.77 % (3998323)Instructions burned: 16 (million)
% 6.80/1.77 % (3998308)Instruction limit reached!
% 6.80/1.77 % (3998308)------------------------------
% 6.80/1.77 % (3998308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/1.77 % (3998308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.77 % (3998308)CaDiCaL version: 2.1.3
% 6.80/1.77 % (3998308)Termination reason: Instruction limit
% 6.80/1.77 % (3998308)Termination phase: Saturation
% 6.80/1.77 % (3998308)Time elapsed: 0.319 s
% 6.80/1.77 % (3998308)Peak memory usage: 117 MB
% 6.80/1.77 % (3998308)Instructions burned: 307 (million)
% 6.80/1.77 % (3998335)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1240026091:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.80/1.77 % (3998334)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=4225659996:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.80/1.77 % (3998332)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2578826086:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.80/1.77 % (3998334)Instruction limit reached!
% 6.80/1.77 % (3998334)------------------------------
% 6.80/1.77 % (3998334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/1.77 % (3998334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/1.77 % (3998334)CaDiCaL version: 2.1.3
% 6.80/1.77 % (3998334)Termination reason: Instruction limit
% 6.80/1.77 % (3998334)Termination phase: Saturation
% 6.80/1.77 % (3998334)Time elapsed: 0.025 s
% 6.80/1.77 % (3998334)Peak memory usage: 89 MB
% 6.80/1.77 % (3998334)Instructions burned: 28 (million)
% 6.80/1.77 % (3998332)Instruction limit reached!
% 6.80/1.77 % (3998332)------------------------------
% 6.80/1.77 % (3998332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/2.03 % (3998332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/2.03 % (3998332)CaDiCaL version: 2.1.3
% 8.09/2.03 % (3998332)Termination reason: Instruction limit
% 8.09/2.03 % (3998332)Termination phase: Saturation
% 8.09/2.03 % (3998332)Time elapsed: 0.025 s
% 8.09/2.03 % (3998332)Peak memory usage: 89 MB
% 8.09/2.03 % (3998332)Instructions burned: 25 (million)
% 8.09/2.03 % (3998335)Instruction limit reached!
% 8.09/2.03 % (3998335)------------------------------
% 8.09/2.03 % (3998335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/2.03 % (3998335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/2.03 % (3998335)CaDiCaL version: 2.1.3
% 8.09/2.03 % (3998335)Termination reason: Instruction limit
% 8.09/2.03 % (3998335)Termination phase: Saturation
% 8.09/2.03 % (3998335)Time elapsed: 0.039 s
% 8.09/2.03 % (3998335)Peak memory usage: 89 MB
% 8.09/2.03 % (3998335)Instructions burned: 86 (million)
% 8.09/2.03 % (3998342)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=601227340:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 8.09/2.03 % (3998342)Instruction limit reached!
% 8.09/2.03 % (3998342)------------------------------
% 8.09/2.03 % (3998342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/2.03 % (3998342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/2.03 % (3998342)CaDiCaL version: 2.1.3
% 8.09/2.03 % (3998342)Termination reason: Instruction limit
% 8.09/2.03 % (3998342)Termination phase: Preprocessing 1
% 8.09/2.03 % (3998342)Time elapsed: 0.003 s
% 8.09/2.03 % (3998342)Peak memory usage: 85 MB
% 8.09/2.03 % (3998342)Instructions burned: 3 (million)
% 8.09/2.03 % (3998361)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4143985286:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 8.09/2.03 % (3998361)Instruction limit reached!
% 8.09/2.03 % (3998361)------------------------------
% 8.09/2.03 % (3998361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/2.03 % (3998361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/2.03 % (3998361)CaDiCaL version: 2.1.3
% 8.09/2.03 % (3998361)Termination reason: Instruction limit
% 8.09/2.03 % (3998361)Termination phase: Preprocessing 1
% 8.09/2.03 % (3998361)Time elapsed: 0.001 s
% 8.09/2.03 % (3998361)Peak memory usage: 85 MB
% 8.09/2.03 % (3998361)Instructions burned: 2 (million)
% 8.09/2.03 % (3998360)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=2711927963:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 8.09/2.03 % (3998350)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=453853070:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 8.09/2.03 % (3998357)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3544987518:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 8.09/2.03 % (3998351)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2016913474:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 8.09/2.03 % (3998351)Instruction limit reached!
% 8.09/2.03 % (3998351)------------------------------
% 8.09/2.03 % (3998351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/2.03 % (3998351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/2.03 % (3998351)CaDiCaL version: 2.1.3
% 8.09/2.03 % (3998351)Termination reason: Instruction limit
% 8.09/2.03 % (3998351)Termination phase: Preprocessing 3
% 8.09/2.03 % (3998351)Time elapsed: 0.004 s
% 8.09/2.03 % (3998351)Peak memory usage: 86 MB
% 8.09/2.03 % (3998351)Instructions burned: 4 (million)
% 8.09/2.03 % (3998360)Instruction limit reached!
% 8.09/2.03 % (3998360)------------------------------
% 8.09/2.03 % (3998360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/2.03 % (3998360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/2.03 % (3998360)CaDiCaL version: 2.1.3
% 8.09/2.03 % (3998360)Termination reason: Instruction limit
% 8.09/2.03 % (3998360)Termination phase: Property scanning
% 8.09/2.03 % (3998360)Time elapsed: 0.008 s
% 8.09/2.03 % (3998360)Peak memory usage: 86 MB
% 8.09/2.03 % (3998360)Instructions burned: 9 (million)
% 11.03/2.36 % (3998359)lrs+10_1_thi=all:si=on:fd=off:random_seed=3376914534:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 11.03/2.36 % (3998357)Instruction limit reached!
% 11.03/2.36 % (3998357)------------------------------
% 11.03/2.36 % (3998357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.36 % (3998357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.36 % (3998357)CaDiCaL version: 2.1.3
% 11.03/2.36 % (3998357)Termination reason: Instruction limit
% 11.03/2.36 % (3998357)Termination phase: Saturation
% 11.03/2.36 % (3998357)Time elapsed: 0.127 s
% 11.03/2.36 % (3998357)Peak memory usage: 134 MB
% 11.03/2.36 % (3998357)Instructions burned: 66 (million)
% 11.03/2.36 % (3998381)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1276350572:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 11.03/2.36 % (3998381)Refutation not found, incomplete strategy
% 11.03/2.36 % (3998381)------------------------------
% 11.03/2.36 % (3998381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.36 % (3998381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.36 % (3998381)CaDiCaL version: 2.1.3
% 11.03/2.36 % (3998381)Termination reason: Refutation not found, incomplete strategy
% 11.03/2.36 % (3998381)Time elapsed: 0.007 s
% 11.03/2.36 % (3998381)Peak memory usage: 89 MB
% 11.03/2.36 % (3998381)Instructions burned: 21 (million)
% 11.03/2.36 % (3998359)Instruction limit reached!
% 11.03/2.36 % (3998359)------------------------------
% 11.03/2.36 % (3998359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.36 % (3998359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.36 % (3998359)CaDiCaL version: 2.1.3
% 11.03/2.36 % (3998359)Termination reason: Instruction limit
% 11.03/2.36 % (3998359)Termination phase: Saturation
% 11.03/2.36 % (3998359)Time elapsed: 0.083 s
% 11.03/2.36 % (3998359)Peak memory usage: 116 MB
% 11.03/2.36 % (3998359)Instructions burned: 53 (million)
% 11.03/2.36 % (3998350)Instruction limit reached!
% 11.03/2.36 % (3998350)------------------------------
% 11.03/2.36 % (3998350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.36 % (3998350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.37 % (3998350)CaDiCaL version: 2.1.3
% 11.03/2.37 % (3998350)Termination reason: Instruction limit
% 11.03/2.37 % (3998350)Termination phase: Saturation
% 11.03/2.37 % (3998350)Time elapsed: 0.181 s
% 11.03/2.37 % (3998350)Peak memory usage: 91 MB
% 11.03/2.37 % (3998350)Instructions burned: 182 (million)
% 11.03/2.37 % (3998371)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1774279433:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 11.03/2.37 % (3998371)Instruction limit reached!
% 11.03/2.37 % (3998371)------------------------------
% 11.03/2.37 % (3998371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.37 % (3998371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.37 % (3998371)CaDiCaL version: 2.1.3
% 11.03/2.37 % (3998371)Termination reason: Instruction limit
% 11.03/2.37 % (3998371)Termination phase: Preprocessing 1
% 11.03/2.37 % (3998371)Time elapsed: 0.003 s
% 11.03/2.37 % (3998371)Peak memory usage: 85 MB
% 11.03/2.37 % (3998371)Instructions burned: 2 (million)
% 11.03/2.37 % (3998379)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2701029829:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.03/2.37 % (3998380)dis+10_1_si=on:random_seed=3394242743:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 11.03/2.37 % (3998380)Instruction limit reached!
% 11.03/2.37 % (3998380)------------------------------
% 11.03/2.37 % (3998380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.37 % (3998380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.37 % (3998380)CaDiCaL version: 2.1.3
% 11.03/2.37 % (3998380)Termination reason: Instruction limit
% 11.03/2.37 % (3998380)Termination phase: Saturation
% 11.03/2.37 % (3998380)Time elapsed: 0.011 s
% 11.03/2.37 % (3998380)Peak memory usage: 87 MB
% 11.03/2.37 % (3998380)Instructions burned: 11 (million)
% 11.03/2.37 % (3998381)------------------------------
% 11.03/2.37 % (3998381)------------------------------
% 11.03/2.37 % (3998391)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3482368229: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_2991 on theBenchmark for (2991ds/35Mi)
% 13.66/2.79 % (3998400)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2511052231:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 13.66/2.79 % (3998379)Instruction limit reached!
% 13.66/2.79 % (3998379)------------------------------
% 13.66/2.79 % (3998379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.79 % (3998379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.79 % (3998379)CaDiCaL version: 2.1.3
% 13.66/2.79 % (3998379)Termination reason: Instruction limit
% 13.66/2.79 % (3998379)Termination phase: Saturation
% 13.66/2.79 % (3998379)Time elapsed: 0.175 s
% 13.66/2.79 % (3998379)Peak memory usage: 117 MB
% 13.66/2.79 % (3998379)Instructions burned: 127 (million)
% 13.66/2.79 % (3998394)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3851899974:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 13.66/2.79 % (3998391)Instruction limit reached!
% 13.66/2.79 % (3998391)------------------------------
% 13.66/2.79 % (3998391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.79 % (3998391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.79 % (3998391)CaDiCaL version: 2.1.3
% 13.66/2.79 % (3998391)Termination reason: Instruction limit
% 13.66/2.79 % (3998391)Termination phase: Saturation
% 13.66/2.79 % (3998391)Time elapsed: 0.029 s
% 13.66/2.79 % (3998391)Peak memory usage: 89 MB
% 13.66/2.79 % (3998391)Instructions burned: 35 (million)
% 13.66/2.79 % (3998394)Instruction limit reached!
% 13.66/2.79 % (3998394)------------------------------
% 13.66/2.79 % (3998394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.79 % (3998394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.79 % (3998394)CaDiCaL version: 2.1.3
% 13.66/2.79 % (3998394)Termination reason: Instruction limit
% 13.66/2.79 % (3998394)Termination phase: Unused predicate definition removal
% 13.66/2.79 % (3998394)Time elapsed: 0.003 s
% 13.66/2.79 % (3998394)Peak memory usage: 86 MB
% 13.66/2.79 % (3998394)Instructions burned: 3 (million)
% 13.66/2.79 % (3998395)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3149487332:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 13.66/2.79 % (3998395)Instruction limit reached!
% 13.66/2.79 % (3998395)------------------------------
% 13.66/2.79 % (3998395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.79 % (3998395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.79 % (3998395)CaDiCaL version: 2.1.3
% 13.66/2.79 % (3998395)Termination reason: Instruction limit
% 13.66/2.79 % (3998395)Termination phase: Property scanning
% 13.66/2.79 % (3998395)Time elapsed: 0.009 s
% 13.66/2.79 % (3998395)Peak memory usage: 87 MB
% 13.66/2.79 % (3998395)Instructions burned: 9 (million)
% 13.66/2.79 % (3998410)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2243035793:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 13.66/2.79 % (3998407)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4171105287:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 13.66/2.79 % (3998407)Instruction limit reached!
% 13.66/2.79 % (3998407)------------------------------
% 13.66/2.79 % (3998407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.79 % (3998407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.79 % (3998407)CaDiCaL version: 2.1.3
% 13.66/2.79 % (3998407)Termination reason: Instruction limit
% 13.66/2.79 % (3998407)Termination phase: Saturation
% 13.66/2.79 % (3998407)Time elapsed: 0.029 s
% 13.66/2.79 % (3998407)Peak memory usage: 100 MB
% 13.66/2.79 % (3998407)Instructions burned: 13 (million)
% 13.66/2.79 % (3998423)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1535060780:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 13.66/2.79 % (3998410)Instruction limit reached!
% 13.66/2.79 % (3998410)------------------------------
% 13.66/2.79 % (3998410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.79 % (3998410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.79 % (3998410)CaDiCaL version: 2.1.3
% 17.26/3.14 % (3998410)Termination reason: Instruction limit
% 17.26/3.14 % (3998410)Termination phase: Saturation
% 17.26/3.14 % (3998410)Time elapsed: 0.158 s
% 17.26/3.14 % (3998410)Peak memory usage: 117 MB
% 17.26/3.14 % (3998410)Instructions burned: 228 (million)
% 17.26/3.14 % (3998419)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2527354730:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 17.26/3.14 % (3998419)Instruction limit reached!
% 17.26/3.14 % (3998419)------------------------------
% 17.26/3.14 % (3998419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.26/3.14 % (3998419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.26/3.14 % (3998419)CaDiCaL version: 2.1.3
% 17.26/3.14 % (3998419)Termination reason: Instruction limit
% 17.26/3.14 % (3998419)Termination phase: Saturation
% 17.26/3.14 % (3998419)Time elapsed: 0.005 s
% 17.26/3.14 % (3998419)Peak memory usage: 88 MB
% 17.26/3.14 % (3998419)Instructions burned: 11 (million)
% 17.26/3.14 % (3998423)Instruction limit reached!
% 17.26/3.14 % (3998423)------------------------------
% 17.26/3.14 % (3998423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.26/3.15 % (3998423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.26/3.15 % (3998423)CaDiCaL version: 2.1.3
% 17.26/3.15 % (3998423)Termination reason: Instruction limit
% 17.26/3.15 % (3998423)Termination phase: Saturation
% 17.26/3.15 % (3998423)Time elapsed: 0.101 s
% 17.26/3.15 % (3998423)Peak memory usage: 133 MB
% 17.26/3.15 % (3998423)Instructions burned: 71 (million)
% 17.26/3.15 % (3998425)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=285551867:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 17.26/3.15 % (3998428)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=1609483430:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi)
% 17.26/3.15 % (3998400)Instruction limit reached!
% 17.26/3.15 % (3998400)------------------------------
% 17.26/3.15 % (3998400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.26/3.15 % (3998400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.26/3.15 % (3998400)CaDiCaL version: 2.1.3
% 17.26/3.15 % (3998400)Termination reason: Instruction limit
% 17.26/3.15 % (3998400)Termination phase: Saturation
% 17.26/3.15 % (3998400)Time elapsed: 0.351 s
% 17.26/3.15 % (3998400)Peak memory usage: 93 MB
% 17.26/3.15 % (3998400)Instructions burned: 371 (million)
% 17.26/3.15 % (3998425)Instruction limit reached!
% 17.26/3.15 % (3998425)------------------------------
% 17.26/3.15 % (3998425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.26/3.15 % (3998425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.26/3.15 % (3998425)CaDiCaL version: 2.1.3
% 17.26/3.15 % (3998425)Termination reason: Instruction limit
% 17.26/3.15 % (3998425)Termination phase: Saturation
% 17.26/3.15 % (3998425)Time elapsed: 0.085 s
% 17.26/3.15 % (3998425)Peak memory usage: 90 MB
% 17.26/3.15 % (3998425)Instructions burned: 75 (million)
% 17.26/3.15 % (3998433)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1925722853:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 17.26/3.15 % (3998441)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1079578134:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 17.26/3.15 % (3998445)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2693267653:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi)
% 17.26/3.15 % (3998444)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2579411465:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 17.26/3.15 % (3998451)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4228127144:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi)
% 17.26/3.15 % (3998433)Instruction limit reached!
% 17.26/3.15 % (3998433)------------------------------
% 17.26/3.15 % (3998433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.26/3.15 % (3998433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.26/3.15 % (3998433)CaDiCaL version: 2.1.3
% 17.26/3.15 % (3998433)Termination reason: Instruction limit
% 19.54/3.58 % (3998433)Termination phase: Saturation
% 19.54/3.58 % (3998433)Time elapsed: 0.177 s
% 19.54/3.58 % (3998433)Peak memory usage: 117 MB
% 19.54/3.58 % (3998433)Instructions burned: 130 (million)
% 19.54/3.58 % (3998428)Instruction limit reached!
% 19.54/3.58 % (3998428)------------------------------
% 19.54/3.58 % (3998428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.58 % (3998428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.58 % (3998428)CaDiCaL version: 2.1.3
% 19.54/3.58 % (3998428)Termination reason: Instruction limit
% 19.54/3.58 % (3998428)Termination phase: Saturation
% 19.54/3.58 % (3998428)Time elapsed: 0.303 s
% 19.54/3.58 % (3998428)Peak memory usage: 91 MB
% 19.54/3.58 % (3998428)Instructions burned: 294 (million)
% 19.54/3.58 % (3998444)Instruction limit reached!
% 19.54/3.58 % (3998444)------------------------------
% 19.54/3.58 % (3998444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.58 % (3998444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.58 % (3998444)CaDiCaL version: 2.1.3
% 19.54/3.58 % (3998444)Termination reason: Instruction limit
% 19.54/3.58 % (3998444)Termination phase: Saturation
% 19.54/3.58 % (3998444)Time elapsed: 0.098 s
% 19.54/3.58 % (3998444)Peak memory usage: 133 MB
% 19.54/3.58 % (3998444)Instructions burned: 40 (million)
% 19.54/3.58 % (3998454)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4060480045:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi)
% 19.54/3.58 % (3998441)Instruction limit reached!
% 19.54/3.58 % (3998441)------------------------------
% 19.54/3.58 % (3998441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.58 % (3998441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.58 % (3998441)CaDiCaL version: 2.1.3
% 19.54/3.58 % (3998441)Termination reason: Instruction limit
% 19.54/3.58 % (3998441)Termination phase: Saturation
% 19.54/3.58 % (3998441)Time elapsed: 0.205 s
% 19.54/3.58 % (3998441)Peak memory usage: 134 MB
% 19.54/3.58 % (3998441)Instructions burned: 131 (million)
% 19.54/3.58 % (3998468)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=551253390:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 19.54/3.58 % (3998454)Instruction limit reached!
% 19.54/3.58 % (3998454)------------------------------
% 19.54/3.58 % (3998454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.58 % (3998454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.58 % (3998454)CaDiCaL version: 2.1.3
% 19.54/3.58 % (3998454)Termination reason: Instruction limit
% 19.54/3.58 % (3998454)Termination phase: Saturation
% 19.54/3.58 % (3998454)Time elapsed: 0.175 s
% 19.54/3.58 % (3998454)Peak memory usage: 117 MB
% 19.54/3.58 % (3998454)Instructions burned: 131 (million)
% 19.54/3.58 % (3998445)Instruction limit reached!
% 19.54/3.58 % (3998445)------------------------------
% 19.54/3.58 % (3998445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.58 % (3998445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.58 % (3998445)CaDiCaL version: 2.1.3
% 19.54/3.58 % (3998445)Termination reason: Instruction limit
% 19.54/3.58 % (3998445)Termination phase: Saturation
% 19.54/3.58 % (3998445)Time elapsed: 0.300 s
% 19.54/3.58 % (3998445)Peak memory usage: 92 MB
% 19.54/3.58 % (3998445)Instructions burned: 307 (million)
% 19.54/3.58 % (3998469)dis+10_1_si=on:random_seed=3012650499:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 19.54/3.58 % (3998451)Instruction limit reached!
% 19.54/3.58 % (3998451)------------------------------
% 19.54/3.58 % (3998451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.58 % (3998451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.58 % (3998451)CaDiCaL version: 2.1.3
% 19.54/3.58 % (3998451)Termination reason: Instruction limit
% 19.54/3.58 % (3998451)Termination phase: Saturation
% 19.54/3.58 % (3998451)Time elapsed: 0.311 s
% 19.54/3.58 % (3998451)Peak memory usage: 140 MB
% 19.54/3.58 % (3998451)Instructions burned: 598 (million)
% 19.54/3.58 % (3998472)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3754393991:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 19.54/3.58 % (3998477)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3166409023:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi)
% 24.36/4.15 % (3998468)Instruction limit reached!
% 24.36/4.15 % (3998468)------------------------------
% 24.36/4.15 % (3998468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.36/4.15 % (3998468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.36/4.15 % (3998468)CaDiCaL version: 2.1.3
% 24.36/4.15 % (3998468)Termination reason: Instruction limit
% 24.36/4.15 % (3998468)Termination phase: Saturation
% 24.36/4.15 % (3998468)Time elapsed: 0.268 s
% 24.36/4.15 % (3998468)Peak memory usage: 117 MB
% 24.36/4.15 % (3998468)Instructions burned: 259 (million)
% 24.36/4.15 % (3998487)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=4141449931:s2a=on:i=128:s2at=5:ins=3:rtra=on_2979 on theBenchmark for (2979ds/128Mi)
% 24.36/4.15 % (3998484)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1029376994:i=121:nm=16:rtra=on_2980 on theBenchmark for (2980ds/121Mi)
% 24.36/4.15 % (3998483)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1289836320:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 24.36/4.15 % (3998477)Instruction limit reached!
% 24.36/4.15 % (3998477)------------------------------
% 24.36/4.15 % (3998477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.36/4.15 % (3998477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.36/4.15 % (3998477)CaDiCaL version: 2.1.3
% 24.36/4.15 % (3998477)Termination reason: Instruction limit
% 24.36/4.15 % (3998477)Termination phase: Saturation
% 24.36/4.15 % (3998477)Time elapsed: 0.149 s
% 24.36/4.15 % (3998477)Peak memory usage: 91 MB
% 24.36/4.15 % (3998477)Instructions burned: 141 (million)
% 24.36/4.15 % (3998487)Instruction limit reached!
% 24.36/4.15 % (3998487)------------------------------
% 24.36/4.15 % (3998487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.36/4.15 % (3998487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.36/4.15 % (3998487)CaDiCaL version: 2.1.3
% 24.36/4.15 % (3998487)Termination reason: Instruction limit
% 24.36/4.15 % (3998487)Termination phase: Saturation
% 24.36/4.15 % (3998487)Time elapsed: 0.076 s
% 24.36/4.15 % (3998487)Peak memory usage: 117 MB
% 24.36/4.15 % (3998487)Instructions burned: 130 (million)
% 24.36/4.15 % (3998483)Instruction limit reached!
% 24.36/4.15 % (3998483)------------------------------
% 24.36/4.15 % (3998483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.36/4.15 % (3998483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.36/4.15 % (3998483)CaDiCaL version: 2.1.3
% 24.36/4.15 % (3998483)Termination reason: Instruction limit
% 24.36/4.15 % (3998483)Termination phase: Saturation
% 24.36/4.15 % (3998483)Time elapsed: 0.096 s
% 24.36/4.15 % (3998483)Peak memory usage: 116 MB
% 24.36/4.15 % (3998483)Instructions burned: 66 (million)
% 24.36/4.15 % (3998484)Instruction limit reached!
% 24.36/4.15 % (3998484)------------------------------
% 24.36/4.15 % (3998484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.36/4.15 % (3998484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.36/4.15 % (3998484)CaDiCaL version: 2.1.3
% 24.36/4.15 % (3998484)Termination reason: Instruction limit
% 24.36/4.15 % (3998484)Termination phase: Saturation
% 24.36/4.15 % (3998484)Time elapsed: 0.115 s
% 24.36/4.15 % (3998484)Peak memory usage: 90 MB
% 24.36/4.15 % (3998484)Instructions burned: 121 (million)
% 24.36/4.15 % (3998472)Instruction limit reached!
% 24.36/4.15 % (3998472)------------------------------
% 24.36/4.15 % (3998472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.36/4.15 % (3998472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.36/4.15 % (3998472)CaDiCaL version: 2.1.3
% 24.36/4.15 % (3998472)Termination reason: Instruction limit
% 24.36/4.15 % (3998472)Termination phase: Saturation
% 24.36/4.15 % (3998472)Time elapsed: 0.368 s
% 24.36/4.15 % (3998472)Peak memory usage: 93 MB
% 24.36/4.15 % (3998472)Instructions burned: 383 (million)
% 24.36/4.15 % (3998495)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=250661987:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 24.36/4.15 % (3998503)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2131861600:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 24.81/4.60 % (3998502)dis+1010_1_to=kbo:si=on:random_seed=3203848132:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 24.81/4.60 % (3998505)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1595486282:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi)
% 24.81/4.60 % (3998495)Instruction limit reached!
% 24.81/4.60 % (3998495)------------------------------
% 24.81/4.60 % (3998495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998495)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998495)Termination reason: Instruction limit
% 24.81/4.60 % (3998495)Termination phase: Saturation
% 24.81/4.60 % (3998495)Time elapsed: 0.073 s
% 24.81/4.60 % (3998495)Peak memory usage: 116 MB
% 24.81/4.60 % (3998495)Instructions burned: 39 (million)
% 24.81/4.60 % (3998507)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=762914010:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi)
% 24.81/4.60 % (3998503)Instruction limit reached!
% 24.81/4.60 % (3998503)------------------------------
% 24.81/4.60 % (3998503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998503)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998503)Termination reason: Instruction limit
% 24.81/4.60 % (3998503)Termination phase: Saturation
% 24.81/4.60 % (3998503)Time elapsed: 0.213 s
% 24.81/4.60 % (3998503)Peak memory usage: 120 MB
% 24.81/4.60 % (3998503)Instructions burned: 330 (million)
% 24.81/4.60 % (3998511)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3095964957:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi)
% 24.81/4.60 % (3998502)Instruction limit reached!
% 24.81/4.60 % (3998502)------------------------------
% 24.81/4.60 % (3998502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998502)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998502)Termination reason: Instruction limit
% 24.81/4.60 % (3998502)Termination phase: Saturation
% 24.81/4.60 % (3998502)Time elapsed: 0.200 s
% 24.81/4.60 % (3998502)Peak memory usage: 91 MB
% 24.81/4.60 % (3998502)Instructions burned: 175 (million)
% 24.81/4.60 % (3998519)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1022839914:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi)
% 24.81/4.60 % (3998469)Instruction limit reached!
% 24.81/4.60 % (3998469)------------------------------
% 24.81/4.60 % (3998469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998469)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998469)Termination reason: Instruction limit
% 24.81/4.60 % (3998469)Termination phase: Saturation
% 24.81/4.60 % (3998469)Time elapsed: 0.859 s
% 24.81/4.60 % (3998469)Peak memory usage: 96 MB
% 24.81/4.60 % (3998469)Instructions burned: 1000 (million)
% 24.81/4.60 % (3998507)Instruction limit reached!
% 24.81/4.60 % (3998507)------------------------------
% 24.81/4.60 % (3998507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998507)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998507)Termination reason: Instruction limit
% 24.81/4.60 % (3998507)Termination phase: Saturation
% 24.81/4.60 % (3998507)Time elapsed: 0.284 s
% 24.81/4.60 % (3998507)Peak memory usage: 136 MB
% 24.81/4.60 % (3998507)Instructions burned: 215 (million)
% 24.81/4.60 % (3998525)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2527828550:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi)
% 24.81/4.60 % (3998511)Refutation not found, incomplete strategy
% 24.81/4.60 % (3998511)------------------------------
% 24.81/4.60 % (3998511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998511)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998511)Termination reason: Refutation not found, incomplete strategy
% 24.81/4.60 % (3998511)Time elapsed: 0.201 s
% 24.81/4.60 % (3998511)Peak memory usage: 117 MB
% 24.81/4.60 % (3998511)Instructions burned: 202 (million)
% 24.81/4.60 % (3998527)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3714277912:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi)
% 24.81/4.60 % (3998525)Instruction limit reached!
% 24.81/4.60 % (3998525)------------------------------
% 24.81/4.60 % (3998525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998525)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998525)Termination reason: Instruction limit
% 24.81/4.60 % (3998525)Termination phase: Saturation
% 24.81/4.60 % (3998525)Time elapsed: 0.128 s
% 24.81/4.60 % (3998525)Peak memory usage: 118 MB
% 24.81/4.60 % (3998525)Instructions burned: 329 (million)
% 24.81/4.60 % (3998505)Instruction limit reached!
% 24.81/4.60 % (3998505)------------------------------
% 24.81/4.60 % (3998505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998505)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998505)Termination reason: Instruction limit
% 24.81/4.60 % (3998505)Termination phase: Saturation
% 24.81/4.60 % (3998505)Time elapsed: 0.591 s
% 24.81/4.60 % (3998505)Peak memory usage: 135 MB
% 24.81/4.60 % (3998505)Instructions burned: 484 (million)
% 24.81/4.60 % (3998532)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=629024219:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi)
% 24.81/4.60 % (3998519)Instruction limit reached!
% 24.81/4.60 % (3998519)------------------------------
% 24.81/4.60 % (3998519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998519)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998519)Termination reason: Instruction limit
% 24.81/4.60 % (3998519)Termination phase: Saturation
% 24.81/4.60 % (3998519)Time elapsed: 0.283 s
% 24.81/4.60 % (3998519)Peak memory usage: 91 MB
% 24.81/4.60 % (3998519)Instructions burned: 295 (million)
% 24.81/4.60 % (3998542)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1311244536:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 24.81/4.60 % (3998537)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=978697468:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi)
% 24.81/4.60 % (3998511)------------------------------
% 24.81/4.60 % (3998511)------------------------------
% 24.81/4.60 % (3998527)Instruction limit reached!
% 24.81/4.60 % (3998527)------------------------------
% 24.81/4.60 % (3998527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998527)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998527)Termination reason: Instruction limit
% 24.81/4.60 % (3998527)Termination phase: Saturation
% 24.81/4.60 % (3998527)Time elapsed: 0.333 s
% 24.81/4.60 % (3998527)Peak memory usage: 117 MB
% 24.81/4.60 % (3998527)Instructions burned: 281 (million)
% 24.81/4.60 % (3998542)First to succeed.
% 24.81/4.60 % (3998542)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3998266"
% 24.81/4.60 % (3998549)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=531016338:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi)
% 24.81/4.60 % (3998547)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3191999215:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 24.81/4.60 % (3998537)Instruction limit reached!
% 24.81/4.60 % (3998537)------------------------------
% 24.81/4.60 % (3998537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998537)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998537)Termination reason: Instruction limit
% 24.81/4.60 % (3998537)Termination phase: Saturation
% 24.81/4.60 % (3998537)Time elapsed: 0.287 s
% 24.81/4.60 % (3998537)Peak memory usage: 113 MB
% 24.81/4.60 % (3998537)Instructions burned: 322 (million)
% 24.81/4.60 % (3998554)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=906434623:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 24.81/4.60 % (3998532)Instruction limit reached!
% 24.81/4.60 % (3998532)------------------------------
% 24.81/4.60 % (3998532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998532)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998532)Termination reason: Instruction limit
% 24.81/4.60 % (3998532)Termination phase: Saturation
% 24.81/4.60 % (3998532)Time elapsed: 0.427 s
% 24.81/4.60 % (3998532)Peak memory usage: 94 MB
% 24.81/4.60 % (3998532)Instructions burned: 485 (million)
% 24.81/4.60 % (3998549)Refutation not found, SMT solver inside AVATAR returned Unknown
% 24.81/4.60 % (3998549)------------------------------
% 24.81/4.60 % (3998549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.81/4.60 % (3998549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.60 % (3998549)CaDiCaL version: 2.1.3
% 24.81/4.60 % (3998549)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 24.81/4.60 % (3998549)Time elapsed: 0.217 s
% 24.81/4.60 % (3998549)Peak memory usage: 134 MB
% 24.81/4.60 % (3998549)Instructions burned: 129 (million)
% 24.81/4.60 % (3998549)------------------------------
% 24.81/4.60 % (3998549)------------------------------
% 24.81/4.60 % (3998542)Refutation found. Thanks to Tanya!
% 24.81/4.60 % SZS status Theorem for theBenchmark
% 24.81/4.60 % SZS output start Proof for theBenchmark
% See solution above
% 26.48/4.84 % (3998542)------------------------------
% 26.48/4.84 % (3998542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/4.84 % (3998542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/4.84 % (3998542)CaDiCaL version: 2.1.3
% 26.48/4.84 % (3998542)Termination reason: Refutation
% 26.48/4.84 % (3998542)Time elapsed: 0.197 s
% 26.48/4.84 % (3998542)Peak memory usage: 119 MB
% 26.48/4.84 % (3998542)Instructions burned: 348 (million)
% 26.48/4.84 % (3998542)------------------------------
% 26.48/4.84 % (3998542)------------------------------
% 26.48/4.84 % (3998266)Success in time 3.952 s
% 26.48/4.84 % Vampire exiting
%------------------------------------------------------------------------------