%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW584_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:51 PM UTC 2026
% Result : Theorem 4.53s 1.49s
% Output : Refutation 6.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 73
% Syntax : Number of formulae : 249 ( 66 unt; 0 typ; 63 def)
% Number of atoms : 908 ( 228 equ)
% Maximal formula atoms : 34 ( 3 avg)
% Number of connectives : 1086 ( 427 ~; 383 |; 172 &)
% ( 46 <=>; 58 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 770 ( 325 atm; 129 fun; 218 num; 98 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 52 ( 48 usr; 47 prp; 0-2 aty)
% Number of functors : 60 ( 54 usr; 34 con; 0-5 aty)
% Number of variables : 145 ( 127 !; 18 ?; 145 :)
% 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,
array_int: $tType ).
tff(type_def_10,type,
map_int_int: $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,
t2tb1: array_int > uni ).
tff(func_def_29,type,
tb2t1: uni > array_int ).
tff(func_def_33,type,
t2tb2: map_int_int > uni ).
tff(func_def_34,type,
tb2t2: uni > map_int_int ).
tff(func_def_36,type,
sK0: array_int > $int ).
tff(func_def_37,type,
sK1: map_int_int ).
tff(func_def_38,type,
sK2: $int ).
tff(func_def_39,type,
sK3: $int ).
tff(func_def_40,type,
sK4: $int ).
tff(func_def_41,type,
sK5: $int ).
tff(func_def_42,type,
sK6: $int ).
tff(func_def_43,type,
sF7: uni ).
tff(func_def_44,type,
sF8: uni ).
tff(func_def_45,type,
sF9: uni ).
tff(func_def_46,type,
sF10: $int ).
tff(func_def_47,type,
sF11: uni ).
tff(func_def_48,type,
sF12: array_int ).
tff(func_def_49,type,
sF13: $int ).
tff(func_def_50,type,
sF14: $int ).
tff(func_def_51,type,
sF15: uni ).
tff(func_def_52,type,
sF16: uni ).
tff(func_def_53,type,
sF17: $int ).
tff(func_def_54,type,
sF18: uni ).
tff(func_def_55,type,
sF19: uni ).
tff(func_def_56,type,
sF20: $int ).
tff(func_def_57,type,
sF21: uni ).
tff(func_def_58,type,
sF22: uni ).
tff(func_def_59,type,
sF23: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
decrease11: array_int > $o ).
tff(f20,axiom,
! [X0: ty,X2: uni,X1: $int] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_def1) ).
tff(f22,axiom,
! [X2: uni,X1: $int,X0: ty] :
( sort1(map(int,X0),X2)
=> ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',elts_def1) ).
tff(f26,axiom,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(f27,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f28,axiom,
! [X1: uni,X2: $int,X0: ty] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def) ).
tff(f35,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f37,axiom,
! [X0: array_int] :
( decrease11(X0)
=> ! [X1: $int,X2: $int] :
( ( $less(X2,length1(int,t2tb1(X0)))
& $lesseq(0,X1)
& $lesseq(X1,X2) )
=> $lesseq($difference($sum(tb2t(get2(int,t2tb1(X0),X1)),X1),X2),tb2t(get2(int,t2tb1(X0),X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',decrease1_induction) ).
tff(f38,axiom,
! [X0: map_int_int] : sort1(map(int,int),t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f40,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR2) ).
tff(f41,conjecture,
! [X0: $int,X2: $int,X1: map_int_int] :
( ( decrease11(tb2t1(mk_array1(int,X0,t2tb2(X1))))
& $lesseq(0,X2)
& $lesseq(0,X0) )
=> ( $less(X2,X0)
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( ( tb2t(get(int,int,t2tb2(X1),t2tb(X2))) != 0 )
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( $less(0,tb2t(get(int,int,t2tb2(X1),t2tb(X2))))
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( ( $lesseq(0,$sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))))
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X1)))) )
=> ! [X3: $int] :
( ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( $less(X4,X0)
& $lesseq($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) ) )
| ( $less(X3,X0)
& ( tb2t(get(int,int,t2tb2(X1),t2tb(X3))) = 0 )
& ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) )
& $lesseq($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),X3) ) )
=> ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( $less(X4,X0)
& $lesseq(X2,X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) ) )
| ( $lesseq(X2,X3)
& $less(X3,X0)
& ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq(X2,X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) )
& ( tb2t(get(int,int,t2tb2(X1),t2tb(X3))) = 0 ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_search_rec) ).
tff(f42,negated_conjecture,
~ ! [X0: $int,X2: $int,X1: map_int_int] :
( ( decrease11(tb2t1(mk_array1(int,X0,t2tb2(X1))))
& $lesseq(0,X2)
& $lesseq(0,X0) )
=> ( $less(X2,X0)
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( ( tb2t(get(int,int,t2tb2(X1),t2tb(X2))) != 0 )
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( $less(0,tb2t(get(int,int,t2tb2(X1),t2tb(X2))))
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( ( $lesseq(0,$sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))))
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X1)))) )
=> ! [X3: $int] :
( ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( $less(X4,X0)
& $lesseq($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) ) )
| ( $less(X3,X0)
& ( tb2t(get(int,int,t2tb2(X1),t2tb(X3))) = 0 )
& ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) )
& $lesseq($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),X3) ) )
=> ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( $less(X4,X0)
& $lesseq(X2,X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) ) )
| ( $lesseq(X2,X3)
& $less(X3,X0)
& ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq(X2,X4) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) )
& ( tb2t(get(int,int,t2tb2(X1),t2tb(X3))) = 0 ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
tff(f44,plain,
~ ! [X0: $int,X2: $int,X1: map_int_int] :
( ( decrease11(tb2t1(mk_array1(int,X0,t2tb2(X1))))
& ~ $less(X2,0)
& ~ $less(X0,0) )
=> ( $less(X2,X0)
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ( ( tb2t(get(int,int,t2tb2(X1),t2tb(X2))) != 0 )
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ( $less(0,tb2t(get(int,int,t2tb2(X1),t2tb(X2))))
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ( ( ~ $less($sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2)))),0)
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X1)))) )
=> ! [X3: $int] :
( ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( $less(X4,X0)
& ~ $less(X4,$sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2))))) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) ) )
| ( $less(X3,X0)
& ( tb2t(get(int,int,t2tb2(X1),t2tb(X3))) = 0 )
& ! [X4: $int] :
( ( $less(X4,X3)
& ~ $less(X4,$sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2))))) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) )
& ~ $less(X3,$sum(X2,tb2t(get(int,int,t2tb2(X1),t2tb(X2))))) ) )
=> ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( $less(X4,X0)
& ~ $less(X4,X2) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) ) )
| ( ~ $less(X3,X2)
& $less(X3,X0)
& ! [X4: $int] :
( ( $less(X4,X3)
& ~ $less(X4,X2) )
=> ( tb2t(get(int,int,t2tb2(X1),t2tb(X4))) != 0 ) )
& ( tb2t(get(int,int,t2tb2(X1),t2tb(X3))) = 0 ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f42]) ).
tff(f46,plain,
! [X0: array_int] :
( decrease11(X0)
=> ! [X1: $int,X2: $int] :
( ( ~ $less(X1,0)
& $less(X2,length1(int,t2tb1(X0)))
& ~ $less(X2,X1) )
=> ~ $less(tb2t(get2(int,t2tb1(X0),X2)),$sum($sum(tb2t(get2(int,t2tb1(X0),X1)),X1),$uminus(X2))) ) ),
inference(theory_normalization,[],[f37]) ).
tff(f48,plain,
! [X0: ty,X2: $int,X1: uni] : ( length1(X0,mk_array1(X0,X2,X1)) = X2 ),
inference(rectify,[],[f20]) ).
tff(f49,plain,
! [X1: $int,X2: ty,X0: uni] :
( sort1(map(int,X2),X0)
=> ( elts(X2,mk_array1(X2,X1,X0)) = X0 ) ),
inference(rectify,[],[f22]) ).
tff(f64,plain,
~ ! [X1: $int,X2: map_int_int,X0: $int] :
( ( decrease11(tb2t1(mk_array1(int,X0,t2tb2(X2))))
& ~ $less(X0,0)
& ~ $less(X1,0) )
=> ( $less(X1,X0)
=> ( ( ~ $less(X1,0)
& $less(X1,X0) )
=> ( ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X1))) )
=> ( ( ~ $less(X1,0)
& $less(X1,X0) )
=> ( $less(0,tb2t(get(int,int,t2tb2(X2),t2tb(X1))))
=> ( ( ~ $less(X1,0)
& $less(X1,X0) )
=> ( ( decrease11(tb2t1(mk_array1(int,X0,t2tb2(X2))))
& ~ $less($sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))),0) )
=> ! [X3: $int] :
( ( ( ! [X5: $int] :
( ( ~ $less(X5,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
& $less(X5,X3) )
=> ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X5))) ) )
& ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X3))) )
& ~ $less(X3,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
& $less(X3,X0) )
| ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( ~ $less(X4,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
& $less(X4,X0) )
=> ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X4))) ) ) ) )
=> ( ( ! [X6: $int] :
( ( $less(X6,X0)
& ~ $less(X6,X1) )
=> ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X6))) ) )
& ( X3 = $uminus(1) ) )
| ( ~ $less(X3,X1)
& ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X3))) )
& ! [X7: $int] :
( ( ~ $less(X7,X1)
& $less(X7,X3) )
=> ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X7))) ) )
& $less(X3,X0) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f44]) ).
tff(f72,plain,
! [X0: array_int] :
( ! [X1: $int,X2: $int] :
( ~ $less(tb2t(get2(int,t2tb1(X0),X2)),$sum($sum(tb2t(get2(int,t2tb1(X0),X1)),X1),$uminus(X2)))
| $less(X1,0)
| ~ $less(X2,length1(int,t2tb1(X0)))
| $less(X2,X1) )
| ~ decrease11(X0) ),
inference(ennf_transformation,[],[f46]) ).
tff(f73,plain,
! [X0: array_int] :
( ! [X2: $int,X1: $int] :
( $less(X2,X1)
| ~ $less(X2,length1(int,t2tb1(X0)))
| ~ $less(tb2t(get2(int,t2tb1(X0),X2)),$sum($sum(tb2t(get2(int,t2tb1(X0),X1)),X1),$uminus(X2)))
| $less(X1,0) )
| ~ decrease11(X0) ),
inference(flattening,[],[f72]) ).
tff(f74,plain,
! [X1: $int,X0: uni,X2: ty] :
( ~ sort1(map(int,X2),X0)
| ( elts(X2,mk_array1(X2,X1,X0)) = X0 ) ),
inference(ennf_transformation,[],[f49]) ).
tff(f83,plain,
? [X1: $int,X2: map_int_int,X0: $int] :
( ? [X3: $int] :
( ( ? [X6: $int] :
( ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X6))) )
& $less(X6,X0)
& ~ $less(X6,X1) )
| ( $uminus(1) != X3 ) )
& ( $less(X3,X1)
| ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X3))) )
| ? [X7: $int] :
( ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X7))) )
& ~ $less(X7,X1)
& $less(X7,X3) )
| ~ $less(X3,X0) )
& ( ( ! [X5: $int] :
( ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X5))) )
| $less(X5,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
| ~ $less(X5,X3) )
& ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X3))) )
& ~ $less(X3,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
& $less(X3,X0) )
| ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X4))) )
| $less(X4,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
| ~ $less(X4,X0) ) ) ) )
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X2))))
& ~ $less($sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))),0)
& ~ $less(X1,0)
& $less(X1,X0)
& $less(0,tb2t(get(int,int,t2tb2(X2),t2tb(X1))))
& ~ $less(X1,0)
& $less(X1,X0)
& ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X1))) )
& ~ $less(X1,0)
& $less(X1,X0)
& $less(X1,X0)
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X2))))
& ~ $less(X0,0)
& ~ $less(X1,0) ),
inference(ennf_transformation,[],[f64]) ).
tff(f84,plain,
? [X2: map_int_int,X0: $int,X1: $int] :
( $less(0,tb2t(get(int,int,t2tb2(X2),t2tb(X1))))
& ~ $less(X1,0)
& $less(X1,X0)
& $less(X1,X0)
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X2))))
& ~ $less(X1,0)
& ~ $less(X0,0)
& ~ $less(X1,0)
& $less(X1,X0)
& ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X1))) )
& ~ $less($sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))),0)
& ? [X3: $int] :
( ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ~ $less(X4,X0)
| ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X4))) )
| $less(X4,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1))))) ) )
| ( ~ $less(X3,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
& ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X3))) )
& ! [X5: $int] :
( $less(X5,$sum(X1,tb2t(get(int,int,t2tb2(X2),t2tb(X1)))))
| ~ $less(X5,X3)
| ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X5))) ) )
& $less(X3,X0) ) )
& ( ( $uminus(1) != X3 )
| ? [X6: $int] :
( $less(X6,X0)
& ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X6))) )
& ~ $less(X6,X1) ) )
& ( ~ $less(X3,X0)
| $less(X3,X1)
| ( 0 != tb2t(get(int,int,t2tb2(X2),t2tb(X3))) )
| ? [X7: $int] :
( $less(X7,X3)
& ( 0 = tb2t(get(int,int,t2tb2(X2),t2tb(X7))) )
& ~ $less(X7,X1) ) ) )
& $less(X1,X0)
& ~ $less(X1,0)
& decrease11(tb2t1(mk_array1(int,X0,t2tb2(X2)))) ),
inference(flattening,[],[f83]) ).
tff(f97,plain,
! [X0: ty,X1: $int,X2: uni] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
inference(rectify,[],[f48]) ).
tff(f99,plain,
! [X0: uni,X1: $int,X2: ty] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get2(X2,X0,X1) ),
inference(rectify,[],[f28]) ).
tff(f100,plain,
! [X0: array_int] :
( ! [X1: $int,X2: $int] :
( $less(X1,X2)
| ~ $less(X1,length1(int,t2tb1(X0)))
| ~ $less(tb2t(get2(int,t2tb1(X0),X1)),$sum($sum(tb2t(get2(int,t2tb1(X0),X2)),X2),$uminus(X1)))
| $less(X2,0) )
| ~ decrease11(X0) ),
inference(rectify,[],[f73]) ).
tff(f105,plain,
? [X0: map_int_int,X1: $int,X2: $int] :
( $less(0,tb2t(get(int,int,t2tb2(X0),t2tb(X2))))
& ~ $less(X2,0)
& $less(X2,X1)
& $less(X2,X1)
& decrease11(tb2t1(mk_array1(int,X1,t2tb2(X0))))
& ~ $less(X2,0)
& ~ $less(X1,0)
& ~ $less(X2,0)
& $less(X2,X1)
& ( 0 != tb2t(get(int,int,t2tb2(X0),t2tb(X2))) )
& ~ $less($sum(X2,tb2t(get(int,int,t2tb2(X0),t2tb(X2)))),0)
& ? [X3: $int] :
( ( ( ( X3 = $uminus(1) )
& ! [X4: $int] :
( ~ $less(X4,X1)
| ( 0 != tb2t(get(int,int,t2tb2(X0),t2tb(X4))) )
| $less(X4,$sum(X2,tb2t(get(int,int,t2tb2(X0),t2tb(X2))))) ) )
| ( ~ $less(X3,$sum(X2,tb2t(get(int,int,t2tb2(X0),t2tb(X2)))))
& ( 0 = tb2t(get(int,int,t2tb2(X0),t2tb(X3))) )
& ! [X5: $int] :
( $less(X5,$sum(X2,tb2t(get(int,int,t2tb2(X0),t2tb(X2)))))
| ~ $less(X5,X3)
| ( 0 != tb2t(get(int,int,t2tb2(X0),t2tb(X5))) ) )
& $less(X3,X1) ) )
& ( ( $uminus(1) != X3 )
| ? [X6: $int] :
( $less(X6,X1)
& ( 0 = tb2t(get(int,int,t2tb2(X0),t2tb(X6))) )
& ~ $less(X6,X2) ) )
& ( ~ $less(X3,X1)
| $less(X3,X2)
| ( 0 != tb2t(get(int,int,t2tb2(X0),t2tb(X3))) )
| ? [X7: $int] :
( $less(X7,X3)
& ( 0 = tb2t(get(int,int,t2tb2(X0),t2tb(X7))) )
& ~ $less(X7,X2) ) ) )
& $less(X2,X1)
& ~ $less(X2,0)
& decrease11(tb2t1(mk_array1(int,X1,t2tb2(X0)))) ),
inference(rectify,[],[f84]) ).
tff(f106,plain,
( $less(0,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3))))
& ~ $less(sK3,0)
& $less(sK3,sK2)
& $less(sK3,sK2)
& decrease11(tb2t1(mk_array1(int,sK2,t2tb2(sK1))))
& ~ $less(sK3,0)
& ~ $less(sK2,0)
& ~ $less(sK3,0)
& $less(sK3,sK2)
& ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(sK3))) )
& ~ $less($sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3)))),0)
& ( ( ( $uminus(1) = sK4 )
& ! [X4: $int] :
( ~ $less(X4,sK2)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(X4))) )
| $less(X4,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3))))) ) )
| ( ~ $less(sK4,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3)))))
& ( 0 = tb2t(get(int,int,t2tb2(sK1),t2tb(sK4))) )
& ! [X5: $int] :
( $less(X5,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3)))))
| ~ $less(X5,sK4)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(X5))) ) )
& $less(sK4,sK2) ) )
& ( ( $uminus(1) != sK4 )
| ( $less(sK5,sK2)
& ( 0 = tb2t(get(int,int,t2tb2(sK1),t2tb(sK5))) )
& ~ $less(sK5,sK3) ) )
& ( ~ $less(sK4,sK2)
| $less(sK4,sK3)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(sK4))) )
| ( $less(sK6,sK4)
& ( 0 = tb2t(get(int,int,t2tb2(sK1),t2tb(sK6))) )
& ~ $less(sK6,sK3) ) )
& $less(sK3,sK2)
& ~ $less(sK3,0)
& decrease11(tb2t1(mk_array1(int,sK2,t2tb2(sK1)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X6,sK5),skolemize(X7,sK6)],[f105]) ).
tff(f110,plain,
! [X0: $int,X1: uni,X2: ty] :
( ~ sort1(map(int,X2),X1)
| ( elts(X2,mk_array1(X2,X0,X1)) = X1 ) ),
inference(rectify,[],[f74]) ).
tff(f116,plain,
! [X0: map_int_int] : sort1(map(int,int),t2tb2(X0)),
inference(cnf_transformation,[],[f38]) ).
tff(f120,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f27]) ).
tff(f124,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f35]) ).
tff(f131,plain,
! [X2: uni,X0: ty,X1: $int] : ( length1(X0,mk_array1(X0,X1,X2)) = X1 ),
inference(cnf_transformation,[],[f97]) ).
tff(f136,plain,
! [X2: ty,X0: uni,X1: $int] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get2(X2,X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
tff(f137,plain,
! [X2: $int,X0: array_int,X1: $int] :
( $less(X1,X2)
| ~ $less(X1,length1(int,t2tb1(X0)))
| ~ $less(tb2t(get2(int,t2tb1(X0),X1)),$sum($sum(tb2t(get2(int,t2tb1(X0),X2)),X2),$uminus(X1)))
| $less(X2,0)
| ~ decrease11(X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f144,plain,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f26]) ).
tff(f151,plain,
( ~ $less(sK4,sK2)
| $less(sK4,sK3)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(sK4))) )
| ~ $less(sK6,sK3) ),
inference(cnf_transformation,[],[f106]) ).
tff(f152,plain,
( ~ $less(sK4,sK2)
| $less(sK4,sK3)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(sK4))) )
| ( 0 = tb2t(get(int,int,t2tb2(sK1),t2tb(sK6))) ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f153,plain,
( ~ $less(sK4,sK2)
| $less(sK4,sK3)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(sK4))) )
| $less(sK6,sK4) ),
inference(cnf_transformation,[],[f106]) ).
tff(f154,plain,
( ( $uminus(1) != sK4 )
| ~ $less(sK5,sK3) ),
inference(cnf_transformation,[],[f106]) ).
tff(f155,plain,
( ( $uminus(1) != sK4 )
| ( 0 = tb2t(get(int,int,t2tb2(sK1),t2tb(sK5))) ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f156,plain,
( ( $uminus(1) != sK4 )
| $less(sK5,sK2) ),
inference(cnf_transformation,[],[f106]) ).
tff(f160,plain,
! [X4: $int] :
( ~ $less(X4,sK2)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(X4))) )
| $less(X4,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3)))))
| ~ $less(sK4,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3))))) ),
inference(cnf_transformation,[],[f106]) ).
tff(f161,plain,
( ( $uminus(1) = sK4 )
| $less(sK4,sK2) ),
inference(cnf_transformation,[],[f106]) ).
tff(f162,plain,
! [X5: $int] :
( ( $uminus(1) = sK4 )
| $less(X5,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3)))))
| ~ $less(X5,sK4)
| ( 0 != tb2t(get(int,int,t2tb2(sK1),t2tb(X5))) ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f163,plain,
( ( $uminus(1) = sK4 )
| ( 0 = tb2t(get(int,int,t2tb2(sK1),t2tb(sK4))) ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f164,plain,
( ( $uminus(1) = sK4 )
| ~ $less(sK4,$sum(sK3,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3))))) ),
inference(cnf_transformation,[],[f106]) ).
tff(f170,plain,
~ $less(sK3,0),
inference(cnf_transformation,[],[f106]) ).
tff(f171,plain,
decrease11(tb2t1(mk_array1(int,sK2,t2tb2(sK1)))),
inference(cnf_transformation,[],[f106]) ).
tff(f175,plain,
$less(0,tb2t(get(int,int,t2tb2(sK1),t2tb(sK3)))),
inference(cnf_transformation,[],[f106]) ).
tff(f179,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f40]) ).
tff(f181,plain,
! [X2: ty,X0: $int,X1: uni] :
( ( elts(X2,mk_array1(X2,X0,X1)) = X1 )
| ~ sort1(map(int,X2),X1) ),
inference(cnf_transformation,[],[f110]) ).
tff(f186,plain,
! [X2: $int,X0: array_int,X1: $int] :
( ~ $less(tb2t(get(int,int,elts(int,t2tb1(X0)),t2tb(X1))),$sum($sum(tb2t(get(int,int,elts(int,t2tb1(X0)),t2tb(X2))),X2),$uminus(X1)))
| $less(X2,0)
| ~ $less(X1,length1(int,t2tb1(X0)))
| $less(X1,X2)
| ~ decrease11(X0) ),
inference(definition_unfolding,[],[f137,f136,f136]) ).
tff(f189,definition,
sF7 = t2tb2(sK1),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f190,definition,
sF8 = t2tb(sK3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f191,plain,
t2tb(sK3) = sF8,
inference(reorient_equations,[],[f190]) ).
tff(f192,definition,
sF9 = get(int,int,sF7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f193,definition,
sF10 = tb2t(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f194,plain,
tb2t(sF9) = sF10,
inference(reorient_equations,[],[f193]) ).
tff(f195,plain,
$less(0,sF10),
inference(definition_folding,[],[f175,f194,f192,f191,f189]) ).
tff(f196,definition,
sF11 = mk_array1(int,sK2,sF7),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f197,definition,
sF12 = tb2t1(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f198,plain,
decrease11(sF12),
inference(definition_folding,[],[f171,f197,f196,f189]) ).
tff(f200,definition,
sF13 = $sum(sK3,sF10),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f201,plain,
$sum(sK3,sF10) = sF13,
inference(reorient_equations,[],[f200]) ).
tff(f203,definition,
sF14 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f204,plain,
$uminus(1) = sF14,
inference(reorient_equations,[],[f203]) ).
tff(f205,plain,
( ~ $less(sK4,sF13)
| ( sK4 = sF14 ) ),
inference(definition_folding,[],[f164,f201,f194,f192,f191,f189,f204]) ).
tff(f206,definition,
sF15 = t2tb(sK4),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f207,definition,
sF16 = get(int,int,sF7,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f208,plain,
get(int,int,sF7,sF15) = sF16,
inference(reorient_equations,[],[f207]) ).
tff(f209,definition,
sF17 = tb2t(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f210,plain,
( ( sK4 = sF14 )
| ( 0 = sF17 ) ),
inference(definition_folding,[],[f163,f209,f208,f206,f189,f204]) ).
tff(f211,plain,
! [X5: $int] :
( ( 0 != tb2t(get(int,int,sF7,t2tb(X5))) )
| ( sK4 = sF14 )
| ~ $less(X5,sK4)
| $less(X5,sF13) ),
inference(definition_folding,[],[f162,f189,f201,f194,f192,f191,f189,f204]) ).
tff(f212,plain,
( ( sK4 = sF14 )
| $less(sK4,sK2) ),
inference(definition_folding,[],[f161,f204]) ).
tff(f213,plain,
! [X4: $int] :
( $less(X4,sF13)
| ~ $less(X4,sK2)
| ~ $less(sK4,sF13)
| ( 0 != tb2t(get(int,int,sF7,t2tb(X4))) ) ),
inference(definition_folding,[],[f160,f201,f194,f192,f191,f189,f201,f194,f192,f191,f189,f189]) ).
tff(f217,plain,
( ( sK4 != sF14 )
| $less(sK5,sK2) ),
inference(definition_folding,[],[f156,f204]) ).
tff(f218,definition,
sF18 = t2tb(sK5),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f219,definition,
sF19 = get(int,int,sF7,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f220,definition,
sF20 = tb2t(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f221,plain,
tb2t(sF19) = sF20,
inference(reorient_equations,[],[f220]) ).
tff(f222,plain,
( ( sK4 != sF14 )
| ( 0 = sF20 ) ),
inference(definition_folding,[],[f155,f221,f219,f218,f189,f204]) ).
tff(f223,plain,
( ~ $less(sK5,sK3)
| ( sK4 != sF14 ) ),
inference(definition_folding,[],[f154,f204]) ).
tff(f224,plain,
( $less(sK6,sK4)
| ( 0 != sF17 )
| ~ $less(sK4,sK2)
| $less(sK4,sK3) ),
inference(definition_folding,[],[f153,f209,f208,f206,f189]) ).
tff(f225,definition,
sF21 = t2tb(sK6),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f226,definition,
sF22 = get(int,int,sF7,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f227,plain,
get(int,int,sF7,sF21) = sF22,
inference(reorient_equations,[],[f226]) ).
tff(f228,definition,
sF23 = tb2t(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f229,plain,
tb2t(sF22) = sF23,
inference(reorient_equations,[],[f228]) ).
tff(f230,plain,
( ( 0 != sF17 )
| ( 0 = sF23 )
| ~ $less(sK4,sK2)
| $less(sK4,sK3) ),
inference(definition_folding,[],[f152,f229,f227,f225,f189,f209,f208,f206,f189]) ).
tff(f231,plain,
( ~ $less(sK6,sK3)
| $less(sK4,sK3)
| ( 0 != sF17 )
| ~ $less(sK4,sK2) ),
inference(definition_folding,[],[f151,f209,f208,f206,f189]) ).
tff(f235,plain,
-1 = sF14,
inference(evaluation,[],[f204]) ).
tff(f238,definition,
( spl24_1
<=> $less(sK3,0) ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
tff(f240,plain,
( ~ $less(sK3,0)
| spl24_1 ),
inference(avatar_component_clause,[],[f238]) ).
tff(f241,plain,
~ spl24_1,
inference(avatar_split_clause,[],[f170,f238]) ).
tff(f253,definition,
( spl24_4
<=> ! [X4: $int] :
( $less(X4,sF13)
| ( 0 != tb2t(get(int,int,sF7,t2tb(X4))) )
| ~ $less(X4,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition]) ).
tff(f254,plain,
( ! [X4: $int] :
( ( 0 != tb2t(get(int,int,sF7,t2tb(X4))) )
| ~ $less(X4,sK2)
| $less(X4,sF13) )
| ~ spl24_4 ),
inference(avatar_component_clause,[],[f253]) ).
tff(f256,definition,
( spl24_5
<=> ( 0 = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition]) ).
tff(f261,definition,
( spl24_6
<=> ( sF18 = t2tb(sK5) ) ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
tff(f263,plain,
( ( sF18 = t2tb(sK5) )
| ~ spl24_6 ),
inference(avatar_component_clause,[],[f261]) ).
tff(f264,plain,
spl24_6,
inference(avatar_split_clause,[],[f218,f261]) ).
tff(f266,definition,
( spl24_7
<=> $less(sK4,sF13) ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
tff(f270,definition,
( spl24_8
<=> ( sK4 = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition]) ).
tff(f272,plain,
( ( sK4 = sF14 )
| ~ spl24_8 ),
inference(avatar_component_clause,[],[f270]) ).
tff(f273,plain,
( ~ spl24_7
| spl24_8 ),
inference(avatar_split_clause,[],[f205,f270,f266]) ).
tff(f275,definition,
( spl24_9
<=> decrease11(sF12) ),
introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition]) ).
tff(f277,plain,
( decrease11(sF12)
| ~ spl24_9 ),
inference(avatar_component_clause,[],[f275]) ).
tff(f278,plain,
spl24_9,
inference(avatar_split_clause,[],[f198,f275]) ).
tff(f280,definition,
( spl24_10
<=> $less(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl24_10])],[avatar_definition]) ).
tff(f284,definition,
( spl24_11
<=> $less(sK4,sK2) ),
introduced(definition,[new_symbols(definition,[spl24_11])],[avatar_definition]) ).
tff(f288,definition,
( spl24_12
<=> $less(sK6,sK3) ),
introduced(definition,[new_symbols(definition,[spl24_12])],[avatar_definition]) ).
tff(f291,plain,
( spl24_10
| ~ spl24_5
| ~ spl24_11
| ~ spl24_12 ),
inference(avatar_split_clause,[],[f231,f288,f284,f256,f280]) ).
tff(f293,definition,
( spl24_13
<=> ( 0 = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition]) ).
tff(f296,plain,
( ~ spl24_5
| spl24_10
| ~ spl24_11
| spl24_13 ),
inference(avatar_split_clause,[],[f230,f293,f284,f280,f256]) ).
tff(f298,definition,
( spl24_14
<=> ( sF11 = mk_array1(int,sK2,sF7) ) ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
tff(f300,plain,
( ( sF11 = mk_array1(int,sK2,sF7) )
| ~ spl24_14 ),
inference(avatar_component_clause,[],[f298]) ).
tff(f301,plain,
spl24_14,
inference(avatar_split_clause,[],[f196,f298]) ).
tff(f303,definition,
( spl24_15
<=> ( get(int,int,sF7,sF21) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition]) ).
tff(f305,plain,
( ( get(int,int,sF7,sF21) = sF22 )
| ~ spl24_15 ),
inference(avatar_component_clause,[],[f303]) ).
tff(f306,plain,
spl24_15,
inference(avatar_split_clause,[],[f227,f303]) ).
tff(f308,definition,
( spl24_16
<=> ( sF19 = get(int,int,sF7,sF18) ) ),
introduced(definition,[new_symbols(definition,[spl24_16])],[avatar_definition]) ).
tff(f310,plain,
( ( sF19 = get(int,int,sF7,sF18) )
| ~ spl24_16 ),
inference(avatar_component_clause,[],[f308]) ).
tff(f311,plain,
spl24_16,
inference(avatar_split_clause,[],[f219,f308]) ).
tff(f313,definition,
( spl24_17
<=> ( sF12 = tb2t1(sF11) ) ),
introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition]) ).
tff(f315,plain,
( ( sF12 = tb2t1(sF11) )
| ~ spl24_17 ),
inference(avatar_component_clause,[],[f313]) ).
tff(f316,plain,
spl24_17,
inference(avatar_split_clause,[],[f197,f313]) ).
tff(f318,definition,
( spl24_18
<=> ( tb2t(sF19) = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition]) ).
tff(f320,plain,
( ( tb2t(sF19) = sF20 )
| ~ spl24_18 ),
inference(avatar_component_clause,[],[f318]) ).
tff(f321,plain,
spl24_18,
inference(avatar_split_clause,[],[f221,f318]) ).
tff(f323,definition,
( spl24_19
<=> ( t2tb(sK3) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl24_19])],[avatar_definition]) ).
tff(f325,plain,
( ( t2tb(sK3) = sF8 )
| ~ spl24_19 ),
inference(avatar_component_clause,[],[f323]) ).
tff(f326,plain,
spl24_19,
inference(avatar_split_clause,[],[f191,f323]) ).
tff(f328,definition,
( spl24_20
<=> ( $sum(sK3,sF10) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition]) ).
tff(f331,plain,
spl24_20,
inference(avatar_split_clause,[],[f201,f328]) ).
tff(f333,definition,
( spl24_21
<=> ( sF9 = get(int,int,sF7,sF8) ) ),
introduced(definition,[new_symbols(definition,[spl24_21])],[avatar_definition]) ).
tff(f335,plain,
( ( sF9 = get(int,int,sF7,sF8) )
| ~ spl24_21 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f336,plain,
spl24_21,
inference(avatar_split_clause,[],[f192,f333]) ).
tff(f338,definition,
( spl24_22
<=> ( tb2t(sF22) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition]) ).
tff(f340,plain,
( ( tb2t(sF22) = sF23 )
| ~ spl24_22 ),
inference(avatar_component_clause,[],[f338]) ).
tff(f341,plain,
spl24_22,
inference(avatar_split_clause,[],[f229,f338]) ).
tff(f343,definition,
( spl24_23
<=> ! [X5: $int] :
( ( 0 != tb2t(get(int,int,sF7,t2tb(X5))) )
| $less(X5,sF13)
| ~ $less(X5,sK4) ) ),
introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition]) ).
tff(f344,plain,
( ! [X5: $int] :
( ( 0 != tb2t(get(int,int,sF7,t2tb(X5))) )
| $less(X5,sF13)
| ~ $less(X5,sK4) )
| ~ spl24_23 ),
inference(avatar_component_clause,[],[f343]) ).
tff(f345,plain,
( spl24_23
| spl24_8 ),
inference(avatar_split_clause,[],[f211,f270,f343]) ).
tff(f352,definition,
( spl24_25
<=> $less(sK5,sK2) ),
introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition]) ).
tff(f354,plain,
( $less(sK5,sK2)
| ~ spl24_25 ),
inference(avatar_component_clause,[],[f352]) ).
tff(f355,plain,
( ~ spl24_8
| spl24_25 ),
inference(avatar_split_clause,[],[f217,f352,f270]) ).
tff(f357,definition,
( spl24_26
<=> ( 0 = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl24_26])],[avatar_definition]) ).
tff(f359,plain,
( ( 0 = sF20 )
| ~ spl24_26 ),
inference(avatar_component_clause,[],[f357]) ).
tff(f360,plain,
( ~ spl24_8
| spl24_26 ),
inference(avatar_split_clause,[],[f222,f357,f270]) ).
tff(f372,definition,
( spl24_29
<=> $less(sK6,sK4) ),
introduced(definition,[new_symbols(definition,[spl24_29])],[avatar_definition]) ).
tff(f374,plain,
( $less(sK6,sK4)
| ~ spl24_29 ),
inference(avatar_component_clause,[],[f372]) ).
tff(f375,plain,
( spl24_29
| ~ spl24_5
| ~ spl24_11
| spl24_10 ),
inference(avatar_split_clause,[],[f224,f280,f284,f256,f372]) ).
tff(f377,definition,
( spl24_30
<=> ( tb2t(sF9) = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
tff(f379,plain,
( ( tb2t(sF9) = sF10 )
| ~ spl24_30 ),
inference(avatar_component_clause,[],[f377]) ).
tff(f380,plain,
spl24_30,
inference(avatar_split_clause,[],[f194,f377]) ).
tff(f384,definition,
( spl24_31
<=> $less(0,sF10) ),
introduced(definition,[new_symbols(definition,[spl24_31])],[avatar_definition]) ).
tff(f387,plain,
spl24_31,
inference(avatar_split_clause,[],[f195,f384]) ).
tff(f388,plain,
( spl24_8
| spl24_5 ),
inference(avatar_split_clause,[],[f210,f256,f270]) ).
tff(f395,definition,
( spl24_33
<=> $less(sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl24_33])],[avatar_definition]) ).
tff(f398,plain,
( ~ spl24_8
| ~ spl24_33 ),
inference(avatar_split_clause,[],[f223,f395,f270]) ).
tff(f410,definition,
( spl24_36
<=> ( sF21 = t2tb(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl24_36])],[avatar_definition]) ).
tff(f412,plain,
( ( sF21 = t2tb(sK6) )
| ~ spl24_36 ),
inference(avatar_component_clause,[],[f410]) ).
tff(f413,plain,
spl24_36,
inference(avatar_split_clause,[],[f225,f410]) ).
tff(f414,plain,
( spl24_8
| spl24_11 ),
inference(avatar_split_clause,[],[f212,f284,f270]) ).
tff(f416,definition,
( spl24_37
<=> ( -1 = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl24_37])],[avatar_definition]) ).
tff(f418,plain,
( ( -1 = sF14 )
| ~ spl24_37 ),
inference(avatar_component_clause,[],[f416]) ).
tff(f419,plain,
spl24_37,
inference(avatar_split_clause,[],[f235,f416]) ).
tff(f425,plain,
( ~ spl24_7
| spl24_4 ),
inference(avatar_split_clause,[],[f213,f253,f266]) ).
tff(f427,plain,
( ( -1 = sK4 )
| ~ spl24_8
| ~ spl24_37 ),
inference(superposition,[],[f418,f272]) ).
tff(f430,definition,
( spl24_39
<=> ( -1 = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl24_39])],[avatar_definition]) ).
tff(f433,plain,
( spl24_39
| ~ spl24_8
| ~ spl24_37 ),
inference(avatar_split_clause,[],[f427,f416,f270,f430]) ).
tff(f448,plain,
( ( 0 = tb2t(sF19) )
| ~ spl24_18
| ~ spl24_26 ),
inference(forward_demodulation,[],[f320,f359]) ).
tff(f450,definition,
( spl24_42
<=> ( 0 = tb2t(sF19) ) ),
introduced(definition,[new_symbols(definition,[spl24_42])],[avatar_definition]) ).
tff(f452,plain,
( ( 0 = tb2t(sF19) )
| ~ spl24_42 ),
inference(avatar_component_clause,[],[f450]) ).
tff(f453,plain,
( spl24_42
| ~ spl24_18
| ~ spl24_26 ),
inference(avatar_split_clause,[],[f448,f357,f318,f450]) ).
tff(f462,definition,
( spl24_44
<=> $less(sK6,sK2) ),
introduced(definition,[new_symbols(definition,[spl24_44])],[avatar_definition]) ).
tff(f466,definition,
( spl24_45
<=> $less(sK6,sF13) ),
introduced(definition,[new_symbols(definition,[spl24_45])],[avatar_definition]) ).
tff(f470,definition,
( spl24_46
<=> ( 0 = tb2t(get(int,int,sF7,sF21)) ) ),
introduced(definition,[new_symbols(definition,[spl24_46])],[avatar_definition]) ).
tff(f471,plain,
( ( 0 = tb2t(get(int,int,sF7,sF21)) )
| ~ spl24_46 ),
inference(avatar_component_clause,[],[f470]) ).
tff(f472,plain,
( ( 0 != tb2t(get(int,int,sF7,sF21)) )
| spl24_46 ),
inference(avatar_component_clause,[],[f470]) ).
tff(f474,plain,
( ( sF9 = t2tb(sF10) )
| ~ spl24_30 ),
inference(superposition,[],[f120,f379]) ).
tff(f476,plain,
( ( sF19 = t2tb(0) )
| ~ spl24_42 ),
inference(superposition,[],[f120,f452]) ).
tff(f481,definition,
( spl24_47
<=> ( sF9 = t2tb(sF10) ) ),
introduced(definition,[new_symbols(definition,[spl24_47])],[avatar_definition]) ).
tff(f483,plain,
( ( sF9 = t2tb(sF10) )
| ~ spl24_47 ),
inference(avatar_component_clause,[],[f481]) ).
tff(f484,plain,
( spl24_47
| ~ spl24_30 ),
inference(avatar_split_clause,[],[f474,f377,f481]) ).
tff(f496,definition,
( spl24_50
<=> ( sF19 = t2tb(0) ) ),
introduced(definition,[new_symbols(definition,[spl24_50])],[avatar_definition]) ).
tff(f498,plain,
( ( sF19 = t2tb(0) )
| ~ spl24_50 ),
inference(avatar_component_clause,[],[f496]) ).
tff(f499,plain,
( spl24_50
| ~ spl24_42 ),
inference(avatar_split_clause,[],[f476,f450,f496]) ).
tff(f500,plain,
( ( sF11 = t2tb1(sF12) )
| ~ spl24_17 ),
inference(superposition,[],[f124,f315]) ).
tff(f503,definition,
( spl24_51
<=> ( sF11 = t2tb1(sF12) ) ),
introduced(definition,[new_symbols(definition,[spl24_51])],[avatar_definition]) ).
tff(f505,plain,
( ( sF11 = t2tb1(sF12) )
| ~ spl24_51 ),
inference(avatar_component_clause,[],[f503]) ).
tff(f506,plain,
( spl24_51
| ~ spl24_17 ),
inference(avatar_split_clause,[],[f500,f313,f503]) ).
tff(f507,plain,
( ( 0 = tb2t(t2tb(0)) )
| ~ spl24_42
| ~ spl24_50 ),
inference(superposition,[],[f452,f498]) ).
tff(f509,definition,
( spl24_52
<=> ( 0 = tb2t(t2tb(0)) ) ),
introduced(definition,[new_symbols(definition,[spl24_52])],[avatar_definition]) ).
tff(f511,plain,
( ( 0 = tb2t(t2tb(0)) )
| ~ spl24_52 ),
inference(avatar_component_clause,[],[f509]) ).
tff(f512,plain,
( spl24_52
| ~ spl24_42
| ~ spl24_50 ),
inference(avatar_split_clause,[],[f507,f496,f450,f509]) ).
tff(f543,plain,
! [X0: uni] : sort1(map(int,int),X0),
inference(superposition,[],[f116,f179]) ).
tff(f557,plain,
( ( 0 != tb2t(sF22) )
| ~ spl24_15
| spl24_46 ),
inference(superposition,[],[f472,f305]) ).
tff(f561,plain,
( ( 0 != sF23 )
| ~ spl24_15
| ~ spl24_22
| spl24_46 ),
inference(forward_demodulation,[],[f557,f340]) ).
tff(f563,plain,
( ~ spl24_13
| ~ spl24_15
| ~ spl24_22
| spl24_46 ),
inference(avatar_split_clause,[],[f561,f470,f338,f303,f293]) ).
tff(f566,plain,
( ( sF19 = get(int,int,sF7,t2tb(sK5)) )
| ~ spl24_6
| ~ spl24_16 ),
inference(forward_demodulation,[],[f310,f263]) ).
tff(f567,plain,
( ( get(int,int,sF7,t2tb(sK5)) = t2tb(0) )
| ~ spl24_6
| ~ spl24_16
| ~ spl24_50 ),
inference(forward_demodulation,[],[f566,f498]) ).
tff(f569,definition,
( spl24_59
<=> ( get(int,int,sF7,t2tb(sK5)) = t2tb(0) ) ),
introduced(definition,[new_symbols(definition,[spl24_59])],[avatar_definition]) ).
tff(f571,plain,
( ( get(int,int,sF7,t2tb(sK5)) = t2tb(0) )
| ~ spl24_59 ),
inference(avatar_component_clause,[],[f569]) ).
tff(f572,plain,
( spl24_59
| ~ spl24_6
| ~ spl24_16
| ~ spl24_50 ),
inference(avatar_split_clause,[],[f567,f496,f308,f261,f569]) ).
tff(f573,plain,
( ~ $less(sK5,sK2)
| ( 0 != tb2t(t2tb(0)) )
| $less(sK5,sF13)
| ~ spl24_4
| ~ spl24_59 ),
inference(superposition,[],[f254,f571]) ).
tff(f576,plain,
( ( 0 != tb2t(t2tb(0)) )
| $less(sK5,sF13)
| ~ spl24_4
| ~ spl24_25
| ~ spl24_59 ),
inference(forward_subsumption_resolution,[],[f573,f354]) ).
tff(f578,plain,
( $less(sK5,sF13)
| ~ spl24_4
| ~ spl24_25
| ~ spl24_52
| ~ spl24_59 ),
inference(forward_subsumption_resolution,[],[f576,f511]) ).
tff(f581,definition,
( spl24_60
<=> $less(sK5,sF13) ),
introduced(definition,[new_symbols(definition,[spl24_60])],[avatar_definition]) ).
tff(f584,plain,
( spl24_60
| ~ spl24_4
| ~ spl24_25
| ~ spl24_52
| ~ spl24_59 ),
inference(avatar_split_clause,[],[f578,f569,f509,f352,f253,f581]) ).
tff(f587,plain,
( ( sF9 = get(int,int,sF7,t2tb(sK3)) )
| ~ spl24_19
| ~ spl24_21 ),
inference(forward_demodulation,[],[f335,f325]) ).
tff(f588,plain,
( ( t2tb(sF10) = get(int,int,sF7,t2tb(sK3)) )
| ~ spl24_19
| ~ spl24_21
| ~ spl24_47 ),
inference(forward_demodulation,[],[f587,f483]) ).
tff(f590,definition,
( spl24_61
<=> ( t2tb(sF10) = get(int,int,sF7,t2tb(sK3)) ) ),
introduced(definition,[new_symbols(definition,[spl24_61])],[avatar_definition]) ).
tff(f592,plain,
( ( t2tb(sF10) = get(int,int,sF7,t2tb(sK3)) )
| ~ spl24_61 ),
inference(avatar_component_clause,[],[f590]) ).
tff(f593,plain,
( spl24_61
| ~ spl24_19
| ~ spl24_21
| ~ spl24_47 ),
inference(avatar_split_clause,[],[f588,f481,f333,f323,f590]) ).
tff(f618,plain,
( ( sK2 = length1(int,sF11) )
| ~ spl24_14 ),
inference(superposition,[],[f131,f300]) ).
tff(f620,definition,
( spl24_65
<=> ( sK2 = length1(int,sF11) ) ),
introduced(definition,[new_symbols(definition,[spl24_65])],[avatar_definition]) ).
tff(f622,plain,
( ( sK2 = length1(int,sF11) )
| ~ spl24_65 ),
inference(avatar_component_clause,[],[f620]) ).
tff(f623,plain,
( spl24_65
| ~ spl24_14 ),
inference(avatar_split_clause,[],[f618,f298,f620]) ).
tff(f740,plain,
( ( sF7 = elts(int,sF11) )
| ~ sort1(map(int,int),sF7)
| ~ spl24_14 ),
inference(superposition,[],[f181,f300]) ).
tff(f743,plain,
( ( sF7 = elts(int,sF11) )
| ~ spl24_14 ),
inference(forward_subsumption_resolution,[],[f740,f543]) ).
tff(f745,definition,
( spl24_67
<=> ( sF7 = elts(int,sF11) ) ),
introduced(definition,[new_symbols(definition,[spl24_67])],[avatar_definition]) ).
tff(f747,plain,
( ( sF7 = elts(int,sF11) )
| ~ spl24_67 ),
inference(avatar_component_clause,[],[f745]) ).
tff(f748,plain,
( spl24_67
| ~ spl24_14 ),
inference(avatar_split_clause,[],[f743,f298,f745]) ).
tff(f862,plain,
( ! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,0)
| ~ decrease11(sF12)
| ~ $less(tb2t(get(int,int,elts(int,sF11),t2tb(X0))),$sum($sum(tb2t(get(int,int,elts(int,sF11),t2tb(X1))),X1),$uminus(X0)))
| ~ $less(X0,length1(int,sF11)) )
| ~ spl24_51 ),
inference(superposition,[],[f186,f505]) ).
tff(f874,plain,
( ! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,0)
| ~ $less(tb2t(get(int,int,elts(int,sF11),t2tb(X0))),$sum($sum(tb2t(get(int,int,elts(int,sF11),t2tb(X1))),X1),$uminus(X0)))
| ~ $less(X0,length1(int,sF11)) )
| ~ spl24_9
| ~ spl24_51 ),
inference(forward_subsumption_resolution,[],[f862,f277]) ).
tff(f875,plain,
( ! [X0: $int,X1: $int] :
( $less(X1,0)
| ~ $less(tb2t(get(int,int,sF7,t2tb(X0))),$sum($sum(tb2t(get(int,int,sF7,t2tb(X1))),X1),$uminus(X0)))
| $less(X0,X1)
| ~ $less(X0,length1(int,sF11)) )
| ~ spl24_9
| ~ spl24_51
| ~ spl24_67 ),
inference(forward_demodulation,[],[f874,f747]) ).
tff(f876,plain,
( ! [X0: $int,X1: $int] :
( ~ $less(tb2t(get(int,int,sF7,t2tb(X0))),$sum($sum(tb2t(get(int,int,sF7,t2tb(X1))),X1),$uminus(X0)))
| $less(X0,X1)
| $less(X1,0)
| ~ $less(X0,sK2) )
| ~ spl24_9
| ~ spl24_51
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_demodulation,[],[f875,f622]) ).
tff(f912,plain,
( ! [X0: $int] :
( $less(sK3,0)
| ~ $less(tb2t(get(int,int,sF7,t2tb(X0))),$sum($sum(tb2t(t2tb(sF10)),sK3),$uminus(X0)))
| ~ $less(X0,sK2)
| $less(X0,sK3) )
| ~ spl24_9
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(superposition,[],[f876,f592]) ).
tff(f920,plain,
( ! [X0: $int] :
( ~ $less(X0,sK2)
| ~ $less(tb2t(get(int,int,sF7,t2tb(X0))),$sum($sum(tb2t(t2tb(sF10)),sK3),$uminus(X0)))
| $less(X0,sK3) )
| spl24_1
| ~ spl24_9
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_subsumption_resolution,[],[f912,f240]) ).
tff(f935,plain,
( ! [X0: $int] :
( ~ $less(tb2t(get(int,int,sF7,t2tb(X0))),$sum($sum(sF10,sK3),$uminus(X0)))
| ~ $less(X0,sK2)
| $less(X0,sK3) )
| spl24_1
| ~ spl24_9
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_demodulation,[],[f920,f144]) ).
tff(f1384,plain,
( $less(sK6,sK3)
| ~ $less(sK6,sK2)
| ~ $less(tb2t(get(int,int,sF7,sF21)),$sum($sum(sF10,sK3),$uminus(sK6)))
| spl24_1
| ~ spl24_9
| ~ spl24_36
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(superposition,[],[f935,f412]) ).
tff(f1387,plain,
( ~ $less(sK5,sK2)
| $less(sK5,sK3)
| ~ $less(tb2t(t2tb(0)),$sum($sum(sF10,sK3),$uminus(sK5)))
| spl24_1
| ~ spl24_9
| ~ spl24_51
| ~ spl24_59
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(superposition,[],[f935,f571]) ).
tff(f1402,plain,
( ~ $less(sK6,sK2)
| $less(sK6,sK3)
| ~ $less(tb2t(sF22),$sum($sum(sF10,sK3),$uminus(sK6)))
| spl24_1
| ~ spl24_9
| ~ spl24_15
| ~ spl24_36
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_demodulation,[],[f1384,f305]) ).
tff(f1405,plain,
( ~ $less(sF23,$sum($sum(sF10,sK3),$uminus(sK6)))
| ~ $less(sK6,sK2)
| $less(sK6,sK3)
| spl24_1
| ~ spl24_9
| ~ spl24_15
| ~ spl24_22
| ~ spl24_36
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_demodulation,[],[f1402,f340]) ).
tff(f1417,definition,
( spl24_129
<=> $less(sF23,$sum($sum(sF10,sK3),$uminus(sK6))) ),
introduced(definition,[new_symbols(definition,[spl24_129])],[avatar_definition]) ).
tff(f1420,plain,
( ~ spl24_129
| spl24_12
| ~ spl24_44
| spl24_1
| ~ spl24_9
| ~ spl24_15
| ~ spl24_22
| ~ spl24_36
| ~ spl24_51
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(avatar_split_clause,[],[f1405,f745,f620,f590,f503,f410,f338,f303,f275,f238,f462,f288,f1417]) ).
tff(f1422,definition,
( spl24_130
<=> $less(0,$sum($sum(sF10,sK3),$uminus(sK5))) ),
introduced(definition,[new_symbols(definition,[spl24_130])],[avatar_definition]) ).
tff(f1426,plain,
( ( 0 = tb2t(sF22) )
| ~ spl24_15
| ~ spl24_46 ),
inference(forward_demodulation,[],[f471,f305]) ).
tff(f1432,plain,
( ~ $less(tb2t(t2tb(0)),$sum($sum(sF10,sK3),$uminus(sK5)))
| $less(sK5,sK3)
| spl24_1
| ~ spl24_9
| ~ spl24_25
| ~ spl24_51
| ~ spl24_59
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_subsumption_resolution,[],[f1387,f354]) ).
tff(f1435,definition,
( spl24_132
<=> ( 0 = tb2t(sF22) ) ),
introduced(definition,[new_symbols(definition,[spl24_132])],[avatar_definition]) ).
tff(f1437,plain,
( ( 0 = tb2t(sF22) )
| ~ spl24_132 ),
inference(avatar_component_clause,[],[f1435]) ).
tff(f1438,plain,
( spl24_132
| ~ spl24_15
| ~ spl24_46 ),
inference(avatar_split_clause,[],[f1426,f470,f303,f1435]) ).
tff(f1439,plain,
( $less(sK5,sK3)
| ~ $less(0,$sum($sum(sF10,sK3),$uminus(sK5)))
| spl24_1
| ~ spl24_9
| ~ spl24_25
| ~ spl24_51
| ~ spl24_52
| ~ spl24_59
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(forward_demodulation,[],[f1432,f511]) ).
tff(f1441,plain,
( ~ spl24_130
| spl24_33
| spl24_1
| ~ spl24_9
| ~ spl24_25
| ~ spl24_51
| ~ spl24_52
| ~ spl24_59
| ~ spl24_61
| ~ spl24_65
| ~ spl24_67 ),
inference(avatar_split_clause,[],[f1439,f745,f620,f590,f569,f509,f503,f352,f275,f238,f395,f1422]) ).
tff(f1509,plain,
( $less(sK6,sF13)
| ( 0 != tb2t(get(int,int,sF7,sF21)) )
| ~ $less(sK6,sK4)
| ~ spl24_23
| ~ spl24_36 ),
inference(superposition,[],[f344,f412]) ).
tff(f1515,plain,
( ( 0 != tb2t(get(int,int,sF7,sF21)) )
| $less(sK6,sF13)
| ~ spl24_23
| ~ spl24_29
| ~ spl24_36 ),
inference(forward_subsumption_resolution,[],[f1509,f374]) ).
tff(f1516,plain,
( $less(sK6,sF13)
| ( 0 != tb2t(sF22) )
| ~ spl24_15
| ~ spl24_23
| ~ spl24_29
| ~ spl24_36 ),
inference(forward_demodulation,[],[f1515,f305]) ).
tff(f1517,plain,
( $less(sK6,sF13)
| ~ spl24_15
| ~ spl24_23
| ~ spl24_29
| ~ spl24_36
| ~ spl24_132 ),
inference(forward_subsumption_resolution,[],[f1516,f1437]) ).
tff(f1518,plain,
( spl24_45
| ~ spl24_15
| ~ spl24_23
| ~ spl24_29
| ~ spl24_36
| ~ spl24_132 ),
inference(avatar_split_clause,[],[f1517,f1435,f410,f372,f343,f303,f466]) ).
tff(f1519,plain,
$false,
inference(avatar_smt_refutation,[],[f1518,f1441,f1438,f1420,f748,f623,f593,f584,f572,f563,f512,f506,f499,f484,f453,f433,f425,f419,f414,f413,f398,f388,f387,f380,f375,f360,f355,f345,f341,f336,f331,f326,f321,f316,f311,f306,f301,f296,f291,f278,f273,f264,f241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW584_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n018.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 14:21:55 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.53/1.49 % (3417894)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.53/1.49 % (3417973)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1038614246:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.53/1.49 % (3417973)Instruction limit reached!
% 4.53/1.49 % (3417973)------------------------------
% 4.53/1.49 % (3417973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3417973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3417973)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3417973)Termination reason: Instruction limit
% 4.53/1.49 % (3417973)Termination phase: Saturation
% 4.53/1.49 % (3417973)Time elapsed: 0.002 s
% 4.53/1.49 % (3417973)Peak memory usage: 88 MB
% 4.53/1.49 % (3417973)Instructions burned: 5 (million)
% 4.53/1.49 % (3417970)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3907844345:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.53/1.49 % (3417972)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1044604998:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.53/1.49 % (3417969)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2042319214:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.53/1.49 % (3417968)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=958924838:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.53/1.49 % (3417972)Instruction limit reached!
% 4.53/1.49 % (3417972)------------------------------
% 4.53/1.49 % (3417972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3417972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3417972)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3417972)Termination reason: Instruction limit
% 4.53/1.49 % (3417972)Termination phase: Saturation
% 4.53/1.49 % (3417972)Time elapsed: 0.005 s
% 4.53/1.49 % (3417972)Peak memory usage: 88 MB
% 4.53/1.49 % (3417972)Instructions burned: 7 (million)
% 4.53/1.49 % (3417975)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2788412954:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.53/1.49 % (3417976)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1076045244:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.53/1.49 % (3417968)Instruction limit reached!
% 4.53/1.49 % (3417968)------------------------------
% 4.53/1.49 % (3417968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3417968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3417968)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3417968)Termination reason: Instruction limit
% 4.53/1.49 % (3417968)Termination phase: Saturation
% 4.53/1.49 % (3417968)Time elapsed: 0.028 s
% 4.53/1.49 % (3417968)Peak memory usage: 112 MB
% 4.53/1.49 % (3417968)Instructions burned: 12 (million)
% 4.53/1.49 % (3417976)Instruction limit reached!
% 4.53/1.49 % (3417976)------------------------------
% 4.53/1.49 % (3417976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3417976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3417976)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3417976)Termination reason: Instruction limit
% 4.53/1.49 % (3417976)Termination phase: Saturation
% 4.53/1.49 % (3417976)Time elapsed: 0.044 s
% 4.53/1.49 % (3417976)Peak memory usage: 116 MB
% 4.53/1.49 % (3417976)Instructions burned: 33 (million)
% 4.53/1.49 % (3417975)Instruction limit reached!
% 4.53/1.49 % (3417975)------------------------------
% 4.53/1.49 % (3417975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3417975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3417975)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3417975)Termination reason: Instruction limit
% 4.53/1.49 % (3417975)Termination phase: Saturation
% 4.53/1.49 % (3417975)Time elapsed: 0.053 s
% 4.53/1.49 % (3417975)Peak memory usage: 116 MB
% 4.53/1.49 % (3417975)Instructions burned: 46 (million)
% 4.53/1.49 % (3418000)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3187473744:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.53/1.49 % (3418016)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=245131177:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.53/1.49 % (3417970)Instruction limit reached!
% 4.53/1.49 % (3417970)------------------------------
% 4.53/1.49 % (3417970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3417970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3417970)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3417970)Termination reason: Instruction limit
% 4.53/1.49 % (3417970)Termination phase: Saturation
% 4.53/1.49 % (3417970)Time elapsed: 0.193 s
% 4.53/1.49 % (3417970)Peak memory usage: 119 MB
% 4.53/1.49 % (3417970)Instructions burned: 201 (million)
% 4.53/1.49 % (3418000)Instruction limit reached!
% 4.53/1.49 % (3418000)------------------------------
% 4.53/1.49 % (3418000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418000)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418000)Termination reason: Instruction limit
% 4.53/1.49 % (3418000)Termination phase: Saturation
% 4.53/1.49 % (3418000)Time elapsed: 0.028 s
% 4.53/1.49 % (3418000)Peak memory usage: 89 MB
% 4.53/1.49 % (3418000)Instructions burned: 14 (million)
% 4.53/1.49 % (3418016)Instruction limit reached!
% 4.53/1.49 % (3418016)------------------------------
% 4.53/1.49 % (3418016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418016)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418016)Termination reason: Instruction limit
% 4.53/1.49 % (3418016)Termination phase: Saturation
% 4.53/1.49 % (3418016)Time elapsed: 0.025 s
% 4.53/1.49 % (3418016)Peak memory usage: 89 MB
% 4.53/1.49 % (3418016)Instructions burned: 29 (million)
% 4.53/1.49 % (3418024)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1852098799:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.53/1.49 % (3417969)First to succeed.
% 4.53/1.49 % (3417969)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3417894"
% 4.53/1.49 % (3418024)Instruction limit reached!
% 4.53/1.49 % (3418024)------------------------------
% 4.53/1.49 % (3418024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418024)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418024)Termination reason: Instruction limit
% 4.53/1.49 % (3418024)Termination phase: Saturation
% 4.53/1.49 % (3418024)Time elapsed: 0.018 s
% 4.53/1.49 % (3418024)Peak memory usage: 89 MB
% 4.53/1.49 % (3418024)Instructions burned: 16 (million)
% 4.53/1.49 % (3418038)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=72014955:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.53/1.49 % (3418037)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2690209194:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.53/1.49 % (3418037)Instruction limit reached!
% 4.53/1.49 % (3418037)------------------------------
% 4.53/1.49 % (3418037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418037)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418037)Termination reason: Instruction limit
% 4.53/1.49 % (3418037)Termination phase: Saturation
% 4.53/1.49 % (3418037)Time elapsed: 0.029 s
% 4.53/1.49 % (3418037)Peak memory usage: 89 MB
% 4.53/1.49 % (3418037)Instructions burned: 24 (million)
% 4.53/1.49 % (3418038)Instruction limit reached!
% 4.53/1.49 % (3418038)------------------------------
% 4.53/1.49 % (3418038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418038)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418038)Termination reason: Instruction limit
% 4.53/1.49 % (3418038)Termination phase: Saturation
% 4.53/1.49 % (3418038)Time elapsed: 0.030 s
% 4.53/1.49 % (3418038)Peak memory usage: 89 MB
% 4.53/1.49 % (3418038)Instructions burned: 28 (million)
% 4.53/1.49 % (3418069)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1889233742:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 4.53/1.49 % (3418069)Instruction limit reached!
% 4.53/1.49 % (3418069)------------------------------
% 4.53/1.49 % (3418069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418069)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418069)Termination reason: Instruction limit
% 4.53/1.49 % (3418069)Termination phase: Property scanning
% 4.53/1.49 % (3418069)Time elapsed: 0.002 s
% 4.53/1.49 % (3418069)Peak memory usage: 86 MB
% 4.53/1.49 % (3418069)Instructions burned: 3 (million)
% 4.53/1.49 % (3418068)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3518333842:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 4.53/1.49 % (3418070)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2104545885:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 4.53/1.49 % (3418068)Instruction limit reached!
% 4.53/1.49 % (3418068)------------------------------
% 4.53/1.49 % (3418068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418068)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418068)Termination reason: Instruction limit
% 4.53/1.49 % (3418068)Termination phase: Saturation
% 4.53/1.49 % (3418068)Time elapsed: 0.076 s
% 4.53/1.49 % (3418068)Peak memory usage: 89 MB
% 4.53/1.49 % (3418068)Instructions burned: 86 (million)
% 4.53/1.49 % (3418080)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3449147290:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 4.53/1.49 % (3418080)Instruction limit reached!
% 4.53/1.49 % (3418080)------------------------------
% 4.53/1.49 % (3418080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418080)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418080)Termination reason: Instruction limit
% 4.53/1.49 % (3418080)Termination phase: Property scanning
% 4.53/1.49 % (3418080)Time elapsed: 0.005 s
% 4.53/1.49 % (3418080)Peak memory usage: 87 MB
% 4.53/1.49 % (3418080)Instructions burned: 4 (million)
% 4.53/1.49 % (3418092)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=290365992:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 4.53/1.49 % (3418087)lrs+10_1_thi=all:si=on:fd=off:random_seed=4019536135:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 4.53/1.49 % (3418086)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3518577151:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 4.53/1.49 % (3418092)Instruction limit reached!
% 4.53/1.49 % (3418092)------------------------------
% 4.53/1.49 % (3418092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418092)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418092)Termination reason: Instruction limit
% 4.53/1.49 % (3418092)Termination phase: Saturation
% 4.53/1.49 % (3418092)Time elapsed: 0.005 s
% 4.53/1.49 % (3418092)Peak memory usage: 88 MB
% 4.53/1.49 % (3418092)Instructions burned: 9 (million)
% 4.53/1.49 % (3418070)Instruction limit reached!
% 4.53/1.49 % (3418070)------------------------------
% 4.53/1.49 % (3418070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.49 % (3418070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.49 % (3418070)CaDiCaL version: 2.1.3
% 4.53/1.49 % (3418070)Termination reason: Instruction limit
% 4.53/1.49 % (3418070)Termination phase: Saturation
% 4.53/1.49 % (3418070)Time elapsed: 0.208 s
% 4.53/1.49 % (3418070)Peak memory usage: 91 MB
% 4.53/1.49 % (3418070)Instructions burned: 181 (million)
% 4.53/1.49 % (3417969)Refutation found. Thanks to Tanya!
% 4.53/1.49 % SZS status Theorem for theBenchmark
% 4.53/1.49 % SZS output start Proof for theBenchmark
% See solution above
% 6.49/1.75 % (3417969)------------------------------
% 6.49/1.75 % (3417969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.49/1.75 % (3417969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.49/1.75 % (3417969)CaDiCaL version: 2.1.3
% 6.49/1.75 % (3417969)Termination reason: Refutation
% 6.49/1.75 % (3417969)Time elapsed: 0.259 s
% 6.49/1.75 % (3417969)Peak memory usage: 118 MB
% 6.49/1.75 % (3417969)Instructions burned: 253 (million)
% 6.49/1.75 % (3417969)------------------------------
% 6.49/1.75 % (3417969)------------------------------
% 6.49/1.75 % (3417894)Success in time 0.84 s
% 6.49/1.75 % Vampire exiting
%------------------------------------------------------------------------------