%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW639_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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:01 PM UTC 2026
% Result : Theorem 22.53s 4.12s
% Output : Refutation 23.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 30
% Syntax : Number of formulae : 188 ( 48 unt; 0 typ; 17 def)
% Number of atoms : 1076 ( 338 equ)
% Maximal formula atoms : 68 ( 5 avg)
% Number of connectives : 1297 ( 409 ~; 439 |; 376 &)
% ( 17 <=>; 56 =>; 0 <=; 0 <~>)
% Maximal formula depth : 45 ( 6 avg)
% Maximal term depth : 11 ( 2 avg)
% Number arithmetic : 2444 ( 480 atm; 58 fun;1688 num; 218 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 18 usr; 18 prp; 0-2 aty)
% Number of functors : 79 ( 69 usr; 44 con; 0-5 aty)
% Number of variables : 387 ( 0 sgn 197 !; 190 ?; 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,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $tType ).
tff(type_def_11,type,
rarray_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,
min1: ( $int * $int ) > $int ).
tff(func_def_13,type,
max1: ( $int * $int ) > $int ).
tff(func_def_14,type,
map: ( ty * ty ) > ty ).
tff(func_def_15,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_16,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_17,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_18,type,
array: ty > ty ).
tff(func_def_19,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_20,type,
length2: ( ty * uni ) > $int ).
tff(func_def_21,type,
elts: ( ty * uni ) > uni ).
tff(func_def_22,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_23,type,
t2tb: $int > uni ).
tff(func_def_24,type,
tb2t: uni > $int ).
tff(func_def_25,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_26,type,
make2: ( ty * $int * uni ) > uni ).
tff(func_def_27,type,
rarray: ty > ty ).
tff(func_def_28,type,
mk_rarray1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_29,type,
dummy: ( ty * uni ) > uni ).
tff(func_def_30,type,
length3: ( ty * uni ) > $int ).
tff(func_def_31,type,
data: ( ty * uni ) > uni ).
tff(func_def_32,type,
mixfix_lbrb1: ( ty * uni * $int ) > uni ).
tff(func_def_33,type,
mixfix_lblsmnrb1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_34,type,
make3: ( ty * $int * uni ) > uni ).
tff(func_def_35,type,
t2tb1: map_int_int > uni ).
tff(func_def_36,type,
tb2t1: uni > map_int_int ).
tff(func_def_37,type,
t2tb2: array_int > uni ).
tff(func_def_38,type,
tb2t2: uni > array_int ).
tff(func_def_39,type,
t2tb3: rarray_int > uni ).
tff(func_def_40,type,
tb2t3: uni > rarray_int ).
tff(func_def_49,type,
sK0: array_int ).
tff(func_def_50,type,
sK1: $int ).
tff(func_def_51,type,
sK2: $int ).
tff(func_def_52,type,
sK3: map_int_int ).
tff(func_def_53,type,
sK4: map_int_int ).
tff(func_def_54,type,
sK5: map_int_int ).
tff(func_def_55,type,
sK6: $int ).
tff(func_def_56,type,
sK7: $int ).
tff(func_def_57,type,
sK8: $int ).
tff(func_def_58,type,
sK9: array_int ).
tff(func_def_59,type,
sK10: $int ).
tff(func_def_60,type,
sK11: array_int ).
tff(func_def_61,type,
sK12: $int ).
tff(func_def_62,type,
sK13: $int ).
tff(func_def_63,type,
sK14: map_int_int ).
tff(func_def_64,type,
sK15: $int ).
tff(func_def_65,type,
sK16: $int ).
tff(func_def_66,type,
sK17: $int ).
tff(func_def_67,type,
sK18: array_int ).
tff(func_def_68,type,
sK19: $int ).
tff(func_def_69,type,
sK20: array_int ).
tff(func_def_70,type,
sK21: $int ).
tff(func_def_71,type,
sK22: $int ).
tff(func_def_72,type,
sK23: $int ).
tff(func_def_73,type,
sK24: array_int ).
tff(func_def_74,type,
sK25: $int ).
tff(func_def_75,type,
sK26: map_int_int ).
tff(func_def_76,type,
sK27: array_int ).
tff(func_def_77,type,
sK28: $int ).
tff(func_def_78,type,
sK29: $int ).
tff(func_def_81,type,
-1: $int > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(f21,axiom,
! [X1: ty,X5: uni,X0: ty,X2: uni,X3: uni,X4: uni] :
( 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(f31,axiom,
! [X0: $int] : sort1(int,t2tb(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort) ).
tff(f32,axiom,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL) ).
tff(f38,axiom,
! [X2: uni,X1: $int,X0: ty] : ( make2(X0,X1,X2) = mk_array1(X0,X1,const(X0,int,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',make_def) ).
tff(f42,axiom,
! [X3: uni,X0: ty,X2: $int,X1: uni] : ( length3(X0,mk_rarray1(X0,X1,X2,X3)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def3) ).
tff(f44,axiom,
! [X2: $int,X1: uni,X0: ty,X3: uni] : ( data(X0,mk_rarray1(X0,X1,X2,X3)) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',data_def1) ).
tff(f51,axiom,
! [X1: $int,X0: ty,X2: uni] : ( make3(X0,X1,X2) = mk_rarray1(X0,X2,X1,make2(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',make_def1) ).
tff(f54,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f61,conjecture,
( ( ( $lesseq(0,length3(int,make3(int,10,t2tb(0))))
& $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& ? [X3: array_int,X1: $int,X2: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) ) )
=> ( ! [X4: map_int_int] :
( ( ? [X3: array_int,X2: $int,X1: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& $lesseq(0,length3(int,make3(int,10,t2tb(0))))
& ! [X0: $int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& ? [X3: array_int,X1: $int,X2: $int] :
( ( length3(int,make3(int,10,t2tb(0))) = X2 )
& ? [X5: $int,X6: map_int_int] :
( ( X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X5 ) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) ) )
=> ( $lesseq(0,10)
& ( ( ? [X2: $int,X3: array_int,X1: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))
& $lesseq(length3(int,make3(int,10,t2tb(0))),X0) )
=> ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& $lesseq(0,length3(int,make3(int,10,t2tb(0)))) )
=> ( $less(0,length3(int,make3(int,10,t2tb(0))))
& ! [X7: map_int_int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& $lesseq(0,length3(int,make3(int,10,t2tb(0))))
& ? [X3: array_int,X1: $int,X2: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 )
& ( length3(int,make3(int,10,t2tb(0))) = X2 )
& ? [X6: map_int_int,X5: $int] :
( ( X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X5 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X7 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,t2tb1(X7),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& ? [X3: array_int,X1: $int,X2: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) ) )
=> ! [X9: map_int_int,X8: $int,X10: $int] :
( ( $lesseq(X10,X8)
& ! [X0: $int] :
( ( $lesseq(X10,X0)
& $less(X0,X8) )
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(0,X10)
& ? [X3: array_int,X1: $int,X2: $int] :
( $lesseq(0,X8)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ( X10 = $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) )
& ! [X0: $int] :
( ( $less(X0,X10)
& $lesseq(0,X0) )
=> ( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X7),t2tb($difference(X0,length3(int,make3(int,10,t2tb(0))))))) ) )
& ( $less(X0,length3(int,make3(int,10,t2tb(0))))
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X4),t2tb(X0))) ) ) ) ) )
=> ( $lesseq(0,10)
& ( X10 = 20 )
& $lesseq(0,0)
& $less(10,X10)
& ( tb2t(get(int,int,t2tb1(X9),t2tb(10))) = 42 )
& ( tb2t(get(int,int,t2tb1(X7),t2tb(0))) = 42 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 17 )
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) ) )
& $lesseq(0,0) ) ) ) )
& $lesseq(0,0)
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(0,10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_test2) ).
tff(f62,negated_conjecture,
~ ( ( ( $lesseq(0,length3(int,make3(int,10,t2tb(0))))
& $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& ? [X3: array_int,X1: $int,X2: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) ) )
=> ( ! [X4: map_int_int] :
( ( ? [X3: array_int,X2: $int,X1: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& $lesseq(0,length3(int,make3(int,10,t2tb(0))))
& ! [X0: $int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& ? [X3: array_int,X1: $int,X2: $int] :
( ( length3(int,make3(int,10,t2tb(0))) = X2 )
& ? [X5: $int,X6: map_int_int] :
( ( X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X5 ) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) ) )
=> ( $lesseq(0,10)
& ( ( ? [X2: $int,X3: array_int,X1: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))
& $lesseq(length3(int,make3(int,10,t2tb(0))),X0) )
=> ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& $lesseq(0,length3(int,make3(int,10,t2tb(0)))) )
=> ( $less(0,length3(int,make3(int,10,t2tb(0))))
& ! [X7: map_int_int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0)))))
& $lesseq(0,length3(int,make3(int,10,t2tb(0))))
& ? [X3: array_int,X1: $int,X2: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 )
& ( length3(int,make3(int,10,t2tb(0))) = X2 )
& ? [X6: map_int_int,X5: $int] :
( ( X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X5 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X7 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,t2tb1(X7),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& ? [X3: array_int,X1: $int,X2: $int] :
( $lesseq(0,length2(int,t2tb2(X3)))
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) ) )
=> ! [X9: map_int_int,X8: $int,X10: $int] :
( ( $lesseq(X10,X8)
& ! [X0: $int] :
( ( $lesseq(X10,X0)
& $less(X0,X8) )
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(0,X10)
& ? [X3: array_int,X1: $int,X2: $int] :
( $lesseq(0,X8)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ( X10 = $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) )
& ! [X0: $int] :
( ( $less(X0,X10)
& $lesseq(0,X0) )
=> ( ( $lesseq(length3(int,make3(int,10,t2tb(0))),X0)
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X7),t2tb($difference(X0,length3(int,make3(int,10,t2tb(0))))))) ) )
& ( $less(X0,length3(int,make3(int,10,t2tb(0))))
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X4),t2tb(X0))) ) ) ) ) )
=> ( $lesseq(0,10)
& ( X10 = 20 )
& $lesseq(0,0)
& $less(10,X10)
& ( tb2t(get(int,int,t2tb1(X9),t2tb(10))) = 42 )
& ( tb2t(get(int,int,t2tb1(X7),t2tb(0))) = 42 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 17 )
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) ) )
& $lesseq(0,0) ) ) ) )
& $lesseq(0,0)
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) )
& $lesseq(0,10) ),
inference(negated_conjecture,[status(cth)],[f61]) ).
tff(f66,plain,
~ ( ( ( ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X3: array_int,X1: $int,X2: $int] :
( ~ $less(length2(int,t2tb2(X3)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( ~ $less(X0,length3(int,make3(int,10,t2tb(0))))
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) ) )
=> ( ! [X4: map_int_int] :
( ( ? [X3: array_int,X2: $int,X1: $int] :
( ~ $less(length2(int,t2tb2(X3)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ! [X0: $int] :
( ( ~ $less(X0,length3(int,make3(int,10,t2tb(0))))
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,t2tb1(X4),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X3: array_int,X1: $int,X2: $int] :
( ( length3(int,make3(int,10,t2tb(0))) = X2 )
& ? [X5: $int,X6: map_int_int] :
( ( X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X5 ) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) ) )
=> ( ~ $less(10,0)
& ( ( ? [X2: $int,X3: array_int,X1: $int] :
( ~ $less(length2(int,t2tb2(X3)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))
& ~ $less(X0,length3(int,make3(int,10,t2tb(0)))) )
=> ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) )
=> ( $less(0,length3(int,make3(int,10,t2tb(0))))
& ! [X7: map_int_int] :
( ( ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X3: array_int,X1: $int,X2: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 )
& ( length3(int,make3(int,10,t2tb(0))) = X2 )
& ? [X6: map_int_int,X5: $int] :
( ( X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X5 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X7 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ! [X0: $int] :
( ( ~ $less(X0,length3(int,make3(int,10,t2tb(0))))
& $less(X0,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(get(int,int,t2tb1(X7),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& ? [X3: array_int,X1: $int,X2: $int] :
( ~ $less(length2(int,t2tb2(X3)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) ) )
=> ! [X9: map_int_int,X8: $int,X10: $int] :
( ( ~ $less(X8,X10)
& ! [X0: $int] :
( ( ~ $less(X0,X10)
& $less(X0,X8) )
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) ) )
& ~ $less(X10,0)
& ? [X3: array_int,X1: $int,X2: $int] :
( ~ $less(X8,0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) ) )
& ( X10 = $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) )
& ! [X0: $int] :
( ( $less(X0,X10)
& ~ $less(X0,0) )
=> ( ( ~ $less(X0,length3(int,make3(int,10,t2tb(0))))
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X7),t2tb($sum(X0,$uminus(length3(int,make3(int,10,t2tb(0)))))))) ) )
& ( $less(X0,length3(int,make3(int,10,t2tb(0))))
=> ( tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X4),t2tb(X0))) ) ) ) ) )
=> ( ~ $less(10,0)
& ( X10 = 20 )
& ~ $less(0,0)
& $less(10,X10)
& ( tb2t(get(int,int,t2tb1(X9),t2tb(10))) = 42 )
& ( tb2t(get(int,int,t2tb1(X7),t2tb(0))) = 42 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 17 )
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) ) )
& ~ $less(0,0) ) ) ) )
& ~ $less(0,0)
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) )
& ~ $less(10,0) ),
inference(theory_normalization,[],[f62]) ).
tff(f73,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f77,plain,
! [X0: $int] : ( 0 = $sum(X0,$uminus(X0)) ),
introduced(definition,[],[tha_inverse_op_unit]) ).
tff(f78,plain,
! [X0: $int] : ~ $less(X0,X0),
introduced(definition,[],[tha_non-reflexivity]) ).
tff(f79,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X1,X2)
| $less(X0,X2)
| ~ $less(X0,X1) ),
introduced(definition,[],[tha_transitivity]) ).
tff(f91,plain,
~ ( ~ $less(10,0)
& ( ( ! [X3: $int] :
( ( ~ $less(X3,length3(int,make3(int,10,t2tb(0))))
& $less(X3,length2(int,data(int,make3(int,10,t2tb(0))))) )
=> ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X3))) ) )
& ? [X0: array_int,X2: $int,X1: $int] :
( ~ $less(length2(int,t2tb2(X0)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X0))) ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) )
=> ( ~ $less(0,0)
& ! [X4: map_int_int] :
( ( ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X11: $int,X10: $int,X9: array_int] :
( ? [X12: $int,X13: map_int_int] :
( ( length2(int,data(int,make3(int,10,t2tb(0)))) = X12 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( tb2t2(mk_array1(int,X12,t2tb1(X13))) = X9 ) )
& ( length3(int,make3(int,10,t2tb(0))) = X11 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X10),X11,t2tb2(X9))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X10 ) )
& ! [X8: $int] :
( ( $less(X8,length2(int,data(int,make3(int,10,t2tb(0)))))
& ~ $less(X8,length3(int,make3(int,10,t2tb(0)))) )
=> ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X8))) ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X5: array_int,X7: $int,X6: $int] :
( ~ $less(length2(int,t2tb2(X5)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X7),X6,t2tb2(X5))) ) ) )
=> ( ( ( ? [X16: $int,X15: array_int,X14: $int] :
( ~ $less(length2(int,t2tb2(X15)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X16),X14,t2tb2(X15))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ! [X17: $int] :
( ( $less(X17,length2(int,data(int,make3(int,10,t2tb(0)))))
& ~ $less(X17,length3(int,make3(int,10,t2tb(0)))) )
=> ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X17))) ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) )
=> ( $less(0,length3(int,make3(int,10,t2tb(0))))
& ! [X18: map_int_int] :
( ( ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X19: array_int,X20: $int,X21: $int] :
( ? [X22: map_int_int,X23: $int] :
( ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X18 )
& ( tb2t2(mk_array1(int,X23,t2tb1(X22))) = X19 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X23 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X20),X21,t2tb2(X19))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X20 )
& ( length3(int,make3(int,10,t2tb(0))) = X21 ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X27: $int,X26: $int,X25: array_int] :
( ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X26),X27,t2tb2(X25))) )
& ~ $less(length2(int,t2tb2(X25)),0) )
& ! [X24: $int] :
( ( $less(X24,length2(int,data(int,make3(int,10,t2tb(0)))))
& ~ $less(X24,length3(int,make3(int,10,t2tb(0)))) )
=> ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X18),t2tb(X24))) ) ) )
=> ! [X29: $int,X28: map_int_int,X30: $int] :
( ( ~ $less(X29,X30)
& ! [X35: $int] :
( ( ~ $less(X35,0)
& $less(X35,X30) )
=> ( ( $less(X35,length3(int,make3(int,10,t2tb(0))))
=> ( tb2t(get(int,int,t2tb1(X28),t2tb(X35))) = tb2t(get(int,int,t2tb1(X4),t2tb(X35))) ) )
& ( ~ $less(X35,length3(int,make3(int,10,t2tb(0))))
=> ( tb2t(get(int,int,t2tb1(X28),t2tb(X35))) = tb2t(get(int,int,t2tb1(X18),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))) ) ) ) )
& ? [X34: $int,X32: array_int,X33: $int] :
( ~ $less(X29,0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X33),X34,t2tb2(X32))) ) )
& ! [X31: $int] :
( ( ~ $less(X31,X30)
& $less(X31,X29) )
=> ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X28),t2tb(X31))) ) )
& ( $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X30 )
& ~ $less(X30,0) )
=> ( ( 42 = tb2t(get(int,int,t2tb1(X28),t2tb(10))) )
& $less(0,length3(int,make3(int,10,t2tb(0))))
& ~ $less(0,0)
& ( 17 = tb2t(get(int,int,t2tb1(X28),t2tb(0))) )
& ~ $less(10,0)
& ( 42 = tb2t(get(int,int,t2tb1(X18),t2tb(0))) )
& $less(10,X30)
& ( 20 = X30 ) ) ) )
& ~ $less(0,0) ) )
& ~ $less(10,0) ) )
& $less(0,length3(int,make3(int,10,t2tb(0)))) ) ) ),
inference(rectify,[],[f66]) ).
tff(f94,plain,
! [X5: uni,X3: uni,X1: uni,X4: uni,X2: ty,X0: ty] :
( sort1(X0,X1)
=> ( ( X4 = X5 )
=> ( get(X0,X2,set(X0,X2,X3,X4,X1),X5) = X1 ) ) ),
inference(rectify,[],[f21]) ).
tff(f99,plain,
! [X1: ty,X3: uni,X0: uni,X2: $int] : ( length3(X1,mk_rarray1(X1,X3,X2,X0)) = X2 ),
inference(rectify,[],[f42]) ).
tff(f100,plain,
! [X1: uni,X0: $int,X2: ty,X3: uni] : ( data(X2,mk_rarray1(X2,X1,X0,X3)) = X3 ),
inference(rectify,[],[f44]) ).
tff(f101,plain,
! [X2: uni,X0: $int,X1: ty] : ( make3(X1,X0,X2) = mk_rarray1(X1,X2,X0,make2(X1,X0,X2)) ),
inference(rectify,[],[f51]) ).
tff(f106,plain,
! [X2: ty,X0: uni,X1: $int] : ( mk_array1(X2,X1,const(X2,int,X0)) = make2(X2,X1,X0) ),
inference(rectify,[],[f38]) ).
tff(f111,plain,
( $less(10,0)
| ( ( $less(0,0)
| ? [X4: map_int_int] :
( ( ( ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ? [X18: map_int_int] :
( ? [X29: $int,X28: map_int_int,X30: $int] :
( ( ( 17 != tb2t(get(int,int,t2tb1(X28),t2tb(0))) )
| $less(10,0)
| ~ $less(10,X30)
| ( 42 != tb2t(get(int,int,t2tb1(X28),t2tb(10))) )
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( 42 != tb2t(get(int,int,t2tb1(X18),t2tb(0))) )
| ( 20 != X30 )
| $less(0,0) )
& ~ $less(X29,X30)
& ! [X35: $int] :
( ( ( ( tb2t(get(int,int,t2tb1(X28),t2tb(X35))) = tb2t(get(int,int,t2tb1(X18),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))) )
| $less(X35,length3(int,make3(int,10,t2tb(0)))) )
& ( ( tb2t(get(int,int,t2tb1(X28),t2tb(X35))) = tb2t(get(int,int,t2tb1(X4),t2tb(X35))) )
| ~ $less(X35,length3(int,make3(int,10,t2tb(0)))) ) )
| $less(X35,0)
| ~ $less(X35,X30) )
& ? [X34: $int,X32: array_int,X33: $int] :
( ~ $less(X29,0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X33),X34,t2tb2(X32))) ) )
& ! [X31: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X28),t2tb(X31))) )
| $less(X31,X30)
| ~ $less(X31,X29) )
& ( $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X30 )
& ~ $less(X30,0) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X19: array_int,X20: $int,X21: $int] :
( ? [X22: map_int_int,X23: $int] :
( ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X18 )
& ( tb2t2(mk_array1(int,X23,t2tb1(X22))) = X19 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X23 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X20),X21,t2tb2(X19))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X20 )
& ( length3(int,make3(int,10,t2tb(0))) = X21 ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X27: $int,X26: $int,X25: array_int] :
( ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X26),X27,t2tb2(X25))) )
& ~ $less(length2(int,t2tb2(X25)),0) )
& ! [X24: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X18),t2tb(X24))) )
| ~ $less(X24,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X24,length3(int,make3(int,10,t2tb(0)))) ) )
| $less(0,0) )
& ? [X16: $int,X15: array_int,X14: $int] :
( ~ $less(length2(int,t2tb2(X15)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X16),X14,t2tb2(X15))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ! [X17: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X17))) )
| ~ $less(X17,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X17,length3(int,make3(int,10,t2tb(0)))) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) )
| $less(10,0) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X11: $int,X10: $int,X9: array_int] :
( ? [X12: $int,X13: map_int_int] :
( ( length2(int,data(int,make3(int,10,t2tb(0)))) = X12 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( tb2t2(mk_array1(int,X12,t2tb1(X13))) = X9 ) )
& ( length3(int,make3(int,10,t2tb(0))) = X11 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X10),X11,t2tb2(X9))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X10 ) )
& ! [X8: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X8))) )
| ~ $less(X8,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X8,length3(int,make3(int,10,t2tb(0)))) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X5: array_int,X7: $int,X6: $int] :
( ~ $less(length2(int,t2tb2(X5)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X7),X6,t2tb2(X5))) ) ) )
| ~ $less(0,length3(int,make3(int,10,t2tb(0)))) )
& ! [X3: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X3))) )
| $less(X3,length3(int,make3(int,10,t2tb(0))))
| ~ $less(X3,length2(int,data(int,make3(int,10,t2tb(0))))) )
& ? [X0: array_int,X2: $int,X1: $int] :
( ~ $less(length2(int,t2tb2(X0)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X0))) ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) ) ),
inference(ennf_transformation,[],[f91]) ).
tff(f112,plain,
( $less(10,0)
| ( ! [X3: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X3))) )
| ~ $less(X3,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X3,length3(int,make3(int,10,t2tb(0)))) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X0: array_int,X2: $int,X1: $int] :
( ~ $less(length2(int,t2tb2(X0)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X0))) ) )
& ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ? [X4: map_int_int] :
( ( ( ! [X17: $int] :
( $less(X17,length3(int,make3(int,10,t2tb(0))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X17))) )
| ~ $less(X17,length2(int,data(int,make3(int,10,t2tb(0))))) )
& ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ? [X18: map_int_int] :
( ? [X28: map_int_int,X29: $int,X30: $int] :
( ? [X34: $int,X32: array_int,X33: $int] :
( ~ $less(X29,0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X33),X34,t2tb2(X32))) ) )
& ~ $less(X30,0)
& ! [X35: $int] :
( $less(X35,0)
| ( ( ( tb2t(get(int,int,t2tb1(X28),t2tb(X35))) = tb2t(get(int,int,t2tb1(X18),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))) )
| $less(X35,length3(int,make3(int,10,t2tb(0)))) )
& ( ( tb2t(get(int,int,t2tb1(X28),t2tb(X35))) = tb2t(get(int,int,t2tb1(X4),t2tb(X35))) )
| ~ $less(X35,length3(int,make3(int,10,t2tb(0)))) ) )
| ~ $less(X35,X30) )
& ( $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X30 )
& ! [X31: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X28),t2tb(X31))) )
| $less(X31,X30)
| ~ $less(X31,X29) )
& ~ $less(X29,X30)
& ( ( 17 != tb2t(get(int,int,t2tb1(X28),t2tb(0))) )
| $less(10,0)
| ~ $less(10,X30)
| ( 42 != tb2t(get(int,int,t2tb1(X28),t2tb(10))) )
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( 42 != tb2t(get(int,int,t2tb1(X18),t2tb(0))) )
| ( 20 != X30 )
| $less(0,0) ) )
& ? [X19: array_int,X20: $int,X21: $int] :
( ? [X22: map_int_int,X23: $int] :
( ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X18 )
& ( tb2t2(mk_array1(int,X23,t2tb1(X22))) = X19 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X23 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X20),X21,t2tb2(X19))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X20 )
& ( length3(int,make3(int,10,t2tb(0))) = X21 ) )
& ! [X24: $int] :
( $less(X24,length3(int,make3(int,10,t2tb(0))))
| ~ $less(X24,length2(int,data(int,make3(int,10,t2tb(0)))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X18),t2tb(X24))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X27: $int,X26: $int,X25: array_int] :
( ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X26),X27,t2tb2(X25))) )
& ~ $less(length2(int,t2tb2(X25)),0) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) )
| $less(0,0) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X16: $int,X15: array_int,X14: $int] :
( ~ $less(length2(int,t2tb2(X15)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X16),X14,t2tb2(X15))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) )
| $less(10,0) )
& ! [X8: $int] :
( ~ $less(X8,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X8,length3(int,make3(int,10,t2tb(0))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X8))) ) )
& ? [X11: $int,X10: $int,X9: array_int] :
( ? [X12: $int,X13: map_int_int] :
( ( length2(int,data(int,make3(int,10,t2tb(0)))) = X12 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( tb2t2(mk_array1(int,X12,t2tb1(X13))) = X9 ) )
& ( length3(int,make3(int,10,t2tb(0))) = X11 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X10),X11,t2tb2(X9))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X10 ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X5: array_int,X7: $int,X6: $int] :
( ~ $less(length2(int,t2tb2(X5)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X7),X6,t2tb2(X5))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) ) ) ) ),
inference(flattening,[],[f111]) ).
tff(f113,plain,
! [X5: uni,X3: uni,X1: uni,X4: uni,X2: ty,X0: ty] :
( ( get(X0,X2,set(X0,X2,X3,X4,X1),X5) = X1 )
| ( X4 != X5 )
| ~ sort1(X0,X1) ),
inference(ennf_transformation,[],[f94]) ).
tff(f114,plain,
! [X2: ty,X1: uni,X5: uni,X0: ty,X4: uni,X3: uni] :
( ~ sort1(X0,X1)
| ( get(X0,X2,set(X0,X2,X3,X4,X1),X5) = X1 )
| ( X4 != X5 ) ),
inference(flattening,[],[f113]) ).
tff(f122,plain,
! [X0: uni,X1: $int,X2: ty,X3: uni] : ( data(X2,mk_rarray1(X2,X0,X1,X3)) = X3 ),
inference(rectify,[],[f100]) ).
tff(f123,plain,
! [X0: ty,X1: uni,X2: uni,X3: $int] : ( length3(X0,mk_rarray1(X0,X1,X3,X2)) = X3 ),
inference(rectify,[],[f99]) ).
tff(f124,plain,
( $less(10,0)
| ( ! [X0: $int] :
( ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) )
| ~ $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X0,length3(int,make3(int,10,t2tb(0)))) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X1: array_int,X2: $int,X3: $int] :
( ~ $less(length2(int,t2tb2(X1)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X3),X2,t2tb2(X1))) ) )
& ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ? [X4: map_int_int] :
( ( ( ! [X5: $int] :
( $less(X5,length3(int,make3(int,10,t2tb(0))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X5))) )
| ~ $less(X5,length2(int,data(int,make3(int,10,t2tb(0))))) )
& ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ? [X6: map_int_int] :
( ? [X7: map_int_int,X8: $int,X9: $int] :
( ? [X10: $int,X11: array_int,X12: $int] :
( ~ $less(X8,0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X12),X10,t2tb2(X11))) ) )
& ~ $less(X9,0)
& ! [X13: $int] :
( $less(X13,0)
| ( ( ( tb2t(get(int,int,t2tb1(X6),t2tb($sum(X13,$uminus(length3(int,make3(int,10,t2tb(0)))))))) = tb2t(get(int,int,t2tb1(X7),t2tb(X13))) )
| $less(X13,length3(int,make3(int,10,t2tb(0)))) )
& ( ( tb2t(get(int,int,t2tb1(X7),t2tb(X13))) = tb2t(get(int,int,t2tb1(X4),t2tb(X13))) )
| ~ $less(X13,length3(int,make3(int,10,t2tb(0)))) ) )
| ~ $less(X13,X9) )
& ( $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X9 )
& ! [X14: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X7),t2tb(X14))) )
| $less(X14,X9)
| ~ $less(X14,X8) )
& ~ $less(X8,X9)
& ( ( 17 != tb2t(get(int,int,t2tb1(X7),t2tb(0))) )
| $less(10,0)
| ~ $less(10,X9)
| ( 42 != tb2t(get(int,int,t2tb1(X7),t2tb(10))) )
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( 42 != tb2t(get(int,int,t2tb1(X6),t2tb(0))) )
| ( 20 != X9 )
| $less(0,0) ) )
& ? [X15: array_int,X16: $int,X17: $int] :
( ? [X18: map_int_int,X19: $int] :
( ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X6 )
& ( tb2t2(mk_array1(int,X19,t2tb1(X18))) = X15 )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = X19 ) )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X16),X17,t2tb2(X15))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X16 )
& ( length3(int,make3(int,10,t2tb(0))) = X17 ) )
& ! [X20: $int] :
( $less(X20,length3(int,make3(int,10,t2tb(0))))
| ~ $less(X20,length2(int,data(int,make3(int,10,t2tb(0)))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X6),t2tb(X20))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ? [X21: $int,X22: $int,X23: array_int] :
( ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X22),X21,t2tb2(X23))) )
& ~ $less(length2(int,t2tb2(X23)),0) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) )
| $less(0,0) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X24: $int,X25: array_int,X26: $int] :
( ~ $less(length2(int,t2tb2(X25)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X24),X26,t2tb2(X25))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) )
| $less(10,0) )
& ! [X27: $int] :
( ~ $less(X27,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X27,length3(int,make3(int,10,t2tb(0))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X27))) ) )
& ? [X28: $int,X29: $int,X30: array_int] :
( ? [X31: $int,X32: map_int_int] :
( ( length2(int,data(int,make3(int,10,t2tb(0)))) = X31 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4 )
& ( tb2t2(mk_array1(int,X31,t2tb1(X32))) = X30 ) )
& ( length3(int,make3(int,10,t2tb(0))) = X28 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X29),X28,t2tb2(X30))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = X29 ) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ? [X33: array_int,X34: $int,X35: $int] :
( ~ $less(length2(int,t2tb2(X33)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X34),X35,t2tb2(X33))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) ) ) ) ),
inference(rectify,[],[f112]) ).
tff(f125,plain,
( $less(10,0)
| ( ! [X0: $int] :
( ( tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) )
| ~ $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X0,length3(int,make3(int,10,t2tb(0)))) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length2(int,t2tb2(sK0)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK2),sK1,t2tb2(sK0))) )
& ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ( ( ( ! [X5: $int] :
( $less(X5,length3(int,make3(int,10,t2tb(0))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X5))) )
| ~ $less(X5,length2(int,data(int,make3(int,10,t2tb(0))))) )
& ( ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( ~ $less(sK6,0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK10),sK8,t2tb2(sK9))) )
& ~ $less(sK7,0)
& ! [X13: $int] :
( $less(X13,0)
| ( ( ( tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(length3(int,make3(int,10,t2tb(0)))))))) )
| $less(X13,length3(int,make3(int,10,t2tb(0)))) )
& ( ( tb2t(get(int,int,t2tb1(sK3),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| ~ $less(X13,length3(int,make3(int,10,t2tb(0)))) ) )
| ~ $less(X13,sK7) )
& ( $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = sK7 )
& ! [X14: $int] :
( ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X14))) )
| $less(X14,sK7)
| ~ $less(X14,sK6) )
& ~ $less(sK6,sK7)
& ( ( 17 != tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| $less(10,0)
| ~ $less(10,sK7)
| ( 42 != tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( 42 != tb2t(get(int,int,t2tb1(sK4),t2tb(0))) )
| ( 20 != sK7 )
| $less(0,0) )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = sK4 )
& ( sK11 = tb2t2(mk_array1(int,sK15,t2tb1(sK14))) )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = sK15 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK12),sK13,t2tb2(sK11))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = sK12 )
& ( length3(int,make3(int,10,t2tb(0))) = sK13 )
& ! [X20: $int] :
( $less(X20,length3(int,make3(int,10,t2tb(0))))
| ~ $less(X20,length2(int,data(int,make3(int,10,t2tb(0)))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(sK4),t2tb(X20))) ) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK17),sK16,t2tb2(sK18))) )
& ~ $less(length2(int,t2tb2(sK18)),0)
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) )
| $less(0,0) )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length2(int,t2tb2(sK20)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK19),sK21,t2tb2(sK20))) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) )
| $less(10,0) )
& ! [X27: $int] :
( ~ $less(X27,length2(int,data(int,make3(int,10,t2tb(0)))))
| $less(X27,length3(int,make3(int,10,t2tb(0))))
| ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(sK3),t2tb(X27))) ) )
& ( length2(int,data(int,make3(int,10,t2tb(0)))) = sK25 )
& ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = sK3 )
& ( tb2t2(mk_array1(int,sK25,t2tb1(sK26))) = sK24 )
& ( length3(int,make3(int,10,t2tb(0))) = sK22 )
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK23),sK22,t2tb2(sK24))) )
& ( tb2t(dummy(int,make3(int,10,t2tb(0)))) = sK23 )
& ~ $less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0))))
& ~ $less(length2(int,t2tb2(sK27)),0)
& ( tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK28),sK29,t2tb2(sK27))) )
& ~ $less(length3(int,make3(int,10,t2tb(0))),0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29]),skolemize(X1,sK0),skolemize(X2,sK1),skolemize(X3,sK2),skolemize(X4,sK3),skolemize(X6,sK4),skolemize(X7,sK5),skolemize(X8,sK6),skolemize(X9,sK7),skolemize(X10,sK8),skolemize(X11,sK9),skolemize(X12,sK10),skolemize(X15,sK11),skolemize(X16,sK12),skolemize(X17,sK13),skolemize(X18,sK14),skolemize(X19,sK15),skolemize(X21,sK16),skolemize(X22,sK17),skolemize(X23,sK18),skolemize(X24,sK19),skolemize(X25,sK20),skolemize(X26,sK21),skolemize(X28,sK22),skolemize(X29,sK23),skolemize(X30,sK24),skolemize(X31,sK25),skolemize(X32,sK26),skolemize(X33,sK27),skolemize(X34,sK28),skolemize(X35,sK29)],[f124]) ).
tff(f126,plain,
! [X0: ty,X1: uni,X2: uni,X3: ty,X4: uni,X5: uni] :
( ~ sort1(X3,X1)
| ( get(X3,X0,set(X3,X0,X5,X4,X1),X2) = X1 )
| ( X2 != X4 ) ),
inference(rectify,[],[f114]) ).
tff(f134,plain,
! [X0: ty,X1: uni,X2: $int] : ( make2(X0,X2,X1) = mk_array1(X0,X2,const(X0,int,X1)) ),
inference(rectify,[],[f106]) ).
tff(f137,plain,
! [X0: uni,X1: $int,X2: ty] : ( make3(X2,X1,X0) = mk_rarray1(X2,X0,X1,make2(X2,X1,X0)) ),
inference(rectify,[],[f101]) ).
tff(f141,plain,
! [X2: ty,X3: uni,X0: uni,X1: $int] : ( data(X2,mk_rarray1(X2,X0,X1,X3)) = X3 ),
inference(cnf_transformation,[],[f122]) ).
tff(f143,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f54]) ).
tff(f144,plain,
! [X0: $int] : sort1(int,t2tb(X0)),
inference(cnf_transformation,[],[f31]) ).
tff(f147,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] : ( length3(X0,mk_rarray1(X0,X1,X3,X2)) = X3 ),
inference(cnf_transformation,[],[f123]) ).
tff(f156,plain,
( $less(10,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = sK3 ) ),
inference(cnf_transformation,[],[f125]) ).
tff(f173,plain,
( $less(10,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = sK4 )
| $less(0,0)
| $less(10,0) ),
inference(cnf_transformation,[],[f125]) ).
tff(f174,plain,
( $less(10,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( 17 != tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| $less(10,0)
| ~ $less(10,sK7)
| ( 42 != tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( 42 != tb2t(get(int,int,t2tb1(sK4),t2tb(0))) )
| ( 20 != sK7 )
| $less(0,0)
| $less(0,0)
| $less(10,0) ),
inference(cnf_transformation,[],[f125]) ).
tff(f177,plain,
( $less(10,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| ( $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = sK7 )
| $less(0,0)
| $less(10,0) ),
inference(cnf_transformation,[],[f125]) ).
tff(f178,plain,
! [X13: $int] :
( $less(10,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(X13,0)
| ( tb2t(get(int,int,t2tb1(sK3),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| ~ $less(X13,length3(int,make3(int,10,t2tb(0))))
| ~ $less(X13,sK7)
| $less(0,0)
| $less(10,0) ),
inference(cnf_transformation,[],[f125]) ).
tff(f179,plain,
! [X13: $int] :
( $less(10,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(0,0)
| ~ $less(0,length3(int,make3(int,10,t2tb(0))))
| $less(X13,0)
| ( tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(length3(int,make3(int,10,t2tb(0)))))))) )
| $less(X13,length3(int,make3(int,10,t2tb(0))))
| ~ $less(X13,sK7)
| $less(0,0)
| $less(10,0) ),
inference(cnf_transformation,[],[f125]) ).
tff(f189,plain,
! [X2: uni,X3: ty,X0: ty,X1: uni,X4: uni,X5: uni] :
( ~ sort1(X3,X1)
| ( get(X3,X0,set(X3,X0,X5,X4,X1),X2) = X1 )
| ( X2 != X4 ) ),
inference(cnf_transformation,[],[f126]) ).
tff(f208,plain,
! [X2: $int,X0: ty,X1: uni] : ( make2(X0,X2,X1) = mk_array1(X0,X2,const(X0,int,X1)) ),
inference(cnf_transformation,[],[f134]) ).
tff(f213,plain,
! [X0: $int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f32]) ).
tff(f214,plain,
! [X2: ty,X0: uni,X1: $int] : ( make3(X2,X1,X0) = mk_rarray1(X2,X0,X1,make2(X2,X1,X0)) ),
inference(cnf_transformation,[],[f137]) ).
tff(f219,plain,
! [X2: ty,X0: uni,X1: $int] : ( mk_rarray1(X2,X0,X1,mk_array1(X2,X1,const(X2,int,X0))) = make3(X2,X1,X0) ),
inference(definition_unfolding,[],[f214,f208]) ).
tff(f228,plain,
! [X13: $int] :
( ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| $less(0,0)
| ~ $less(X13,sK7)
| $less(10,0)
| $less(10,0)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(X13,0)
| $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(0,0) ),
inference(definition_unfolding,[],[f179,f219,f219,f219,f219]) ).
tff(f229,plain,
! [X13: $int] :
( $less(0,0)
| ( tb2t(get(int,int,t2tb1(sK3),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(10,0)
| $less(10,0)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(X13,sK7)
| $less(X13,0)
| $less(0,0) ),
inference(definition_unfolding,[],[f178,f219,f219,f219]) ).
tff(f230,plain,
( $less(10,0)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(0,0)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) = sK7 )
| $less(0,0)
| $less(10,0) ),
inference(definition_unfolding,[],[f177,f219,f219,f219,f219]) ).
tff(f233,plain,
( ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( 42 != tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(10,sK7)
| ( 17 != tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(0,0)
| $less(10,0)
| ( 20 != sK7 )
| $less(10,0)
| $less(0,0)
| ( 42 != tb2t(get(int,int,t2tb1(sK4),t2tb(0))) )
| $less(10,0)
| $less(0,0) ),
inference(definition_unfolding,[],[f174,f219,f219,f219]) ).
tff(f234,plain,
( $less(10,0)
| ( tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) = sK4 )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(10,0)
| $less(0,0)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(0,0) ),
inference(definition_unfolding,[],[f173,f219,f219,f219]) ).
tff(f251,plain,
( ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(0,0)
| ( sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17))) )
| $less(10,0) ),
inference(definition_unfolding,[],[f156,f219,f219]) ).
tff(f262,plain,
! [X3: ty,X0: ty,X1: uni,X4: uni,X5: uni] :
( ( get(X3,X0,set(X3,X0,X5,X4,X1),X4) = X1 )
| ~ sort1(X3,X1) ),
inference(equality_resolution,[],[f189]) ).
tff(f265,plain,
( $less(0,0)
| $less(10,0)
| ( $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) = sK7 )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) ),
inference(duplicate_literal_removal,[],[f230]) ).
tff(f270,plain,
! [X13: $int] :
( ~ $less(X13,sK7)
| $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(0,0)
| $less(X13,0)
| $less(10,0)
| ( tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) ),
inference(duplicate_literal_removal,[],[f228]) ).
tff(f272,plain,
( $less(0,0)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) = sK4 )
| $less(10,0) ),
inference(duplicate_literal_removal,[],[f234]) ).
tff(f277,plain,
( ( 42 != tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| $less(10,0)
| ( 17 != tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(10,sK7)
| $less(0,0)
| ( 42 != tb2t(get(int,int,t2tb1(sK4),t2tb(0))) )
| ( 20 != sK7 ) ),
inference(duplicate_literal_removal,[],[f233]) ).
tff(f288,plain,
! [X13: $int] :
( $less(10,0)
| ~ $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(X13,sK7)
| ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| $less(X13,0)
| $less(0,0)
| ( tb2t(get(int,int,t2tb1(sK3),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) ) ),
inference(duplicate_literal_removal,[],[f229]) ).
tff(f290,definition,
( spl30_1
<=> $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
tff(f291,plain,
( $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ spl30_1 ),
inference(avatar_component_clause,[],[f290]) ).
tff(f292,plain,
( ~ $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| spl30_1 ),
inference(avatar_component_clause,[],[f290]) ).
tff(f298,definition,
( spl30_3
<=> $less(0,0) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
tff(f300,plain,
( $less(0,0)
| ~ spl30_3 ),
inference(avatar_component_clause,[],[f298]) ).
tff(f302,definition,
( spl30_4
<=> $less(10,0) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
tff(f312,definition,
( spl30_6
<=> ( $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
tff(f314,plain,
( ( $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) = sK7 )
| ~ spl30_6 ),
inference(avatar_component_clause,[],[f312]) ).
tff(f315,plain,
( ~ spl30_1
| spl30_3
| spl30_6
| spl30_4 ),
inference(avatar_split_clause,[],[f265,f302,f312,f298,f290]) ).
tff(f347,definition,
( spl30_13
<=> ! [X13: $int] :
( ~ $less(X13,sK7)
| ( tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| $less(X13,0)
| $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) ) ),
introduced(definition,[new_symbols(definition,[spl30_13])],[avatar_definition]) ).
tff(f348,plain,
( ! [X13: $int] :
( $less(X13,0)
| ~ $less(X13,sK7)
| ( tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) )
| ~ spl30_13 ),
inference(avatar_component_clause,[],[f347]) ).
tff(f349,plain,
( ~ spl30_1
| spl30_13
| spl30_3
| spl30_4 ),
inference(avatar_split_clause,[],[f270,f302,f298,f347,f290]) ).
tff(f358,definition,
( spl30_15
<=> ( tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl30_15])],[avatar_definition]) ).
tff(f360,plain,
( ( tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) = sK4 )
| ~ spl30_15 ),
inference(avatar_component_clause,[],[f358]) ).
tff(f361,plain,
( spl30_4
| ~ spl30_1
| spl30_3
| spl30_15 ),
inference(avatar_split_clause,[],[f272,f358,f298,f290,f302]) ).
tff(f368,definition,
( spl30_17
<=> ( sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17))) ) ),
introduced(definition,[new_symbols(definition,[spl30_17])],[avatar_definition]) ).
tff(f370,plain,
( ( sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17))) )
| ~ spl30_17 ),
inference(avatar_component_clause,[],[f368]) ).
tff(f371,plain,
( spl30_3
| ~ spl30_1
| spl30_4
| spl30_17 ),
inference(avatar_split_clause,[],[f251,f368,f302,f290,f298]) ).
tff(f403,definition,
( spl30_24
<=> ( 42 = tb2t(get(int,int,t2tb1(sK5),t2tb(10))) ) ),
introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition]) ).
tff(f407,definition,
( spl30_25
<=> ( 42 = tb2t(get(int,int,t2tb1(sK4),t2tb(0))) ) ),
introduced(definition,[new_symbols(definition,[spl30_25])],[avatar_definition]) ).
tff(f409,plain,
( ( 42 != tb2t(get(int,int,t2tb1(sK4),t2tb(0))) )
| spl30_25 ),
inference(avatar_component_clause,[],[f407]) ).
tff(f411,definition,
( spl30_26
<=> ( 20 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl30_26])],[avatar_definition]) ).
tff(f412,plain,
( ( 20 = sK7 )
| ~ spl30_26 ),
inference(avatar_component_clause,[],[f411]) ).
tff(f415,definition,
( spl30_27
<=> $less(10,sK7) ),
introduced(definition,[new_symbols(definition,[spl30_27])],[avatar_definition]) ).
tff(f417,plain,
( ~ $less(10,sK7)
| spl30_27 ),
inference(avatar_component_clause,[],[f415]) ).
tff(f419,definition,
( spl30_28
<=> ( 17 = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) ) ),
introduced(definition,[new_symbols(definition,[spl30_28])],[avatar_definition]) ).
tff(f421,plain,
( ( 17 != tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| spl30_28 ),
inference(avatar_component_clause,[],[f419]) ).
tff(f422,plain,
( spl30_4
| ~ spl30_24
| spl30_3
| ~ spl30_25
| ~ spl30_1
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28 ),
inference(avatar_split_clause,[],[f277,f419,f415,f411,f290,f407,f298,f403,f302]) ).
tff(f476,definition,
( spl30_39
<=> ! [X13: $int] :
( ~ $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( tb2t(get(int,int,t2tb1(sK3),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| $less(X13,0)
| ~ $less(X13,sK7) ) ),
introduced(definition,[new_symbols(definition,[spl30_39])],[avatar_definition]) ).
tff(f477,plain,
( ! [X13: $int] :
( ~ $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( tb2t(get(int,int,t2tb1(sK3),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| $less(X13,0)
| ~ $less(X13,sK7) )
| ~ spl30_39 ),
inference(avatar_component_clause,[],[f476]) ).
tff(f478,plain,
( spl30_39
| ~ spl30_1
| spl30_4
| spl30_3 ),
inference(avatar_split_clause,[],[f288,f298,f302,f290,f476]) ).
tff(f607,plain,
( ~ $less(0,10)
| spl30_1 ),
inference(superposition,[],[f292,f147]) ).
tff(f626,plain,
( $false
| spl30_1 ),
inference(evaluation,[],[f607]) ).
tff(f628,plain,
spl30_1,
inference(avatar_contradiction_clause,[],[f626]) ).
tff(f634,plain,
( $false
| ~ spl30_3 ),
inference(forward_subsumption_resolution,[],[f300,f78]) ).
tff(f635,plain,
~ spl30_3,
inference(avatar_contradiction_clause,[],[f634]) ).
tff(f651,plain,
( ( tb2t1(set(int,int,elts(int,mk_array1(int,10,const(int,int,t2tb(0)))),t2tb(0),t2tb(42))) = sK4 )
| ~ spl30_15 ),
inference(forward_demodulation,[],[f360,f141]) ).
tff(f653,plain,
( ( $sum(10,10) = sK7 )
| ~ spl30_6 ),
inference(forward_demodulation,[],[f314,f147]) ).
tff(f656,plain,
( ! [X13: $int] :
( ( tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X13,$uminus(10))))) = tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) )
| ~ $less(X13,sK7)
| $less(X13,0)
| $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) )
| ~ spl30_13 ),
inference(forward_demodulation,[],[f348,f147]) ).
tff(f660,plain,
( ( sK3 = tb2t1(set(int,int,elts(int,mk_array1(int,10,const(int,int,t2tb(0)))),t2tb(0),t2tb(17))) )
| ~ spl30_17 ),
inference(forward_demodulation,[],[f370,f141]) ).
tff(f682,definition,
( spl30_52
<=> $less(0,sK7) ),
introduced(definition,[new_symbols(definition,[spl30_52])],[avatar_definition]) ).
tff(f683,plain,
( ~ $less(0,sK7)
| spl30_52 ),
inference(avatar_component_clause,[],[f682]) ).
tff(f684,plain,
( $less(0,sK7)
| ~ spl30_52 ),
inference(avatar_component_clause,[],[f682]) ).
tff(f701,plain,
( ( 20 = sK7 )
| ~ spl30_6 ),
inference(evaluation,[],[f653]) ).
tff(f702,plain,
( spl30_26
| ~ spl30_6 ),
inference(avatar_split_clause,[],[f701,f312,f411]) ).
tff(f756,plain,
( ~ $less(0,20)
| ~ spl30_26
| spl30_52 ),
inference(superposition,[],[f683,f412]) ).
tff(f799,plain,
( ! [X0: $int] :
( $less(X0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(X0,0) )
| ~ spl30_1 ),
inference(resolution,[],[f291,f79]) ).
tff(f816,plain,
( $false
| ~ spl30_26
| spl30_52 ),
inference(evaluation,[],[f756]) ).
tff(f818,plain,
( ~ spl30_26
| spl30_52 ),
inference(avatar_contradiction_clause,[],[f816]) ).
tff(f885,plain,
( ( set(int,int,elts(int,mk_array1(int,10,const(int,int,t2tb(0)))),t2tb(0),t2tb(42)) = t2tb1(sK4) )
| ~ spl30_15 ),
inference(superposition,[],[f143,f651]) ).
tff(f886,plain,
( ( t2tb1(sK3) = set(int,int,elts(int,mk_array1(int,10,const(int,int,t2tb(0)))),t2tb(0),t2tb(17)) )
| ~ spl30_17 ),
inference(superposition,[],[f143,f660]) ).
tff(f913,plain,
( ( tb2t(get(int,int,t2tb1(sK3),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| $less(0,0)
| ~ $less(0,sK7)
| ~ spl30_1
| ~ spl30_39 ),
inference(resolution,[],[f477,f291]) ).
tff(f917,plain,
( ( tb2t(get(int,int,t2tb1(sK3),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ $less(0,sK7)
| ~ spl30_1
| ~ spl30_39 ),
inference(forward_subsumption_resolution,[],[f913,f78]) ).
tff(f918,plain,
( ( tb2t(get(int,int,t2tb1(sK3),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ spl30_1
| ~ spl30_39
| ~ spl30_52 ),
inference(forward_subsumption_resolution,[],[f917,f684]) ).
tff(f920,plain,
( ! [X13: $int] :
( ( tb2t(get(int,int,t2tb1(sK5),t2tb(X13))) = tb2t(get(int,int,t2tb1(sK4),t2tb($sum(-10,X13)))) )
| $less(X13,0)
| $less(X13,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(X13,sK7) )
| ~ spl30_13 ),
inference(evaluation,[],[f656]) ).
tff(f923,plain,
( ! [X0: $int] :
( $less(X0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ( tb2t(get(int,int,t2tb1(sK5),t2tb(X0))) = tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X0,-10)))) )
| ~ $less(X0,sK7)
| $less(X0,0) )
| ~ spl30_13 ),
inference(superposition,[],[f920,f73]) ).
tff(f931,definition,
( spl30_72
<=> ( tb2t(get(int,int,t2tb1(sK4),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb($uminus(-10)))) ) ),
introduced(definition,[new_symbols(definition,[spl30_72])],[avatar_definition]) ).
tff(f933,plain,
( ( tb2t(get(int,int,t2tb1(sK4),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb($uminus(-10)))) )
| ~ spl30_72 ),
inference(avatar_component_clause,[],[f931]) ).
tff(f935,definition,
( spl30_73
<=> $less($uminus(-10),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) ),
introduced(definition,[new_symbols(definition,[spl30_73])],[avatar_definition]) ).
tff(f936,plain,
( ~ $less($uminus(-10),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| spl30_73 ),
inference(avatar_component_clause,[],[f935]) ).
tff(f937,plain,
( $less($uminus(-10),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ spl30_73 ),
inference(avatar_component_clause,[],[f935]) ).
tff(f939,definition,
( spl30_74
<=> $less($uminus(-10),sK7) ),
introduced(definition,[new_symbols(definition,[spl30_74])],[avatar_definition]) ).
tff(f941,plain,
( ~ $less($uminus(-10),sK7)
| spl30_74 ),
inference(avatar_component_clause,[],[f939]) ).
tff(f944,plain,
( ~ $less(10,sK7)
| spl30_74 ),
inference(evaluation,[],[f941]) ).
tff(f945,plain,
( ~ spl30_27
| spl30_74 ),
inference(avatar_split_clause,[],[f944,f939,f415]) ).
tff(f947,plain,
( ~ $less(10,20)
| ~ spl30_26
| spl30_27 ),
inference(superposition,[],[f417,f412]) ).
tff(f1423,plain,
( ( tb2t(get(int,int,t2tb1(sK4),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| ~ spl30_72 ),
inference(evaluation,[],[f933]) ).
tff(f1501,plain,
( ( t2tb(42) = get(int,int,t2tb1(sK4),t2tb(0)) )
| ~ sort1(int,t2tb(42))
| ~ spl30_15 ),
inference(superposition,[],[f262,f885]) ).
tff(f1503,plain,
( ( t2tb(42) = get(int,int,t2tb1(sK4),t2tb(0)) )
| ~ spl30_15 ),
inference(forward_subsumption_resolution,[],[f1501,f144]) ).
tff(f1510,plain,
( ( t2tb(17) = get(int,int,t2tb1(sK3),t2tb(0)) )
| ~ sort1(int,t2tb(17))
| ~ spl30_17 ),
inference(superposition,[],[f262,f886]) ).
tff(f1514,plain,
( ( t2tb(17) = get(int,int,t2tb1(sK3),t2tb(0)) )
| ~ spl30_17 ),
inference(forward_subsumption_resolution,[],[f1510,f144]) ).
tff(f1644,plain,
( $false
| ~ spl30_26
| spl30_27 ),
inference(evaluation,[],[f947]) ).
tff(f1646,plain,
( ~ spl30_26
| spl30_27 ),
inference(avatar_contradiction_clause,[],[f1644]) ).
tff(f1685,plain,
( ! [X0: $int] :
( ( tb2t(get(int,int,t2tb1(sK5),t2tb(X0))) = tb2t(get(int,int,t2tb1(sK4),t2tb($sum(X0,-10)))) )
| $less(X0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ $less(X0,sK7) )
| ~ spl30_1
| ~ spl30_13 ),
inference(forward_subsumption_resolution,[],[f923,f799]) ).
tff(f1687,plain,
( ! [X0: $int] :
( ( tb2t(get(int,int,t2tb1(sK5),t2tb(X0))) = tb2t(get(int,int,t2tb1(sK4),t2tb($sum(-10,X0)))) )
| ~ $less(X0,sK7)
| $less(X0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) )
| ~ spl30_1
| ~ spl30_13 ),
inference(evaluation,[],[f1685]) ).
tff(f1694,plain,
( ( tb2t(get(int,int,t2tb1(sK4),t2tb(0))) = tb2t(get(int,int,t2tb1(sK5),t2tb($uminus(-10)))) )
| ~ $less($uminus(-10),sK7)
| $less($uminus(-10),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ spl30_1
| ~ spl30_13 ),
inference(superposition,[],[f1687,f77]) ).
tff(f1705,plain,
( spl30_72
| ~ spl30_74
| spl30_73
| ~ spl30_1
| ~ spl30_13 ),
inference(avatar_split_clause,[],[f1694,f347,f290,f935,f939,f931]) ).
tff(f1706,plain,
( $less(10,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| ~ spl30_73 ),
inference(evaluation,[],[f937]) ).
tff(f1721,plain,
( $less(10,10)
| ~ spl30_73 ),
inference(superposition,[],[f1706,f147]) ).
tff(f1723,plain,
( $false
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1721,f78]) ).
tff(f1724,plain,
~ spl30_73,
inference(avatar_contradiction_clause,[],[f1723]) ).
tff(f1798,plain,
( ~ $less(10,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))
| spl30_73 ),
inference(evaluation,[],[f936]) ).
tff(f1803,plain,
( ~ $less(10,0)
| ~ spl30_1
| spl30_73 ),
inference(resolution,[],[f1798,f799]) ).
tff(f1807,plain,
( ~ spl30_4
| ~ spl30_1
| spl30_73 ),
inference(avatar_split_clause,[],[f1803,f935,f290,f302]) ).
tff(f3505,plain,
( ( tb2t(t2tb(42)) = tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| ~ spl30_15
| ~ spl30_72 ),
inference(superposition,[],[f1423,f1503]) ).
tff(f3507,plain,
( ( 42 = tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| ~ spl30_15
| ~ spl30_72 ),
inference(forward_demodulation,[],[f3505,f213]) ).
tff(f3510,plain,
( spl30_24
| ~ spl30_15
| ~ spl30_72 ),
inference(avatar_split_clause,[],[f3507,f931,f358,f403]) ).
tff(f3511,plain,
( ( 42 != tb2t(get(int,int,t2tb1(sK5),t2tb(10))) )
| spl30_25
| ~ spl30_72 ),
inference(forward_demodulation,[],[f409,f1423]) ).
tff(f3512,plain,
( ~ spl30_24
| spl30_25
| ~ spl30_72 ),
inference(avatar_split_clause,[],[f3511,f931,f407,f403]) ).
tff(f3627,plain,
( ( tb2t(get(int,int,t2tb1(sK5),t2tb(0))) = tb2t(t2tb(17)) )
| ~ spl30_1
| ~ spl30_17
| ~ spl30_39
| ~ spl30_52 ),
inference(superposition,[],[f918,f1514]) ).
tff(f3630,plain,
( ( 17 = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ spl30_1
| ~ spl30_17
| ~ spl30_39
| ~ spl30_52 ),
inference(forward_demodulation,[],[f3627,f213]) ).
tff(f3632,plain,
( $false
| ~ spl30_1
| ~ spl30_17
| spl30_28
| ~ spl30_39
| ~ spl30_52 ),
inference(forward_subsumption_resolution,[],[f3630,f421]) ).
tff(f3633,plain,
( ~ spl30_1
| ~ spl30_17
| spl30_28
| ~ spl30_39
| ~ spl30_52 ),
inference(avatar_contradiction_clause,[],[f3632]) ).
cnf(s3,plain,
( ~ spl30_1
| spl30_3
| spl30_4
| spl30_6 ),
inference(sat_conversion,[],[f315]) ).
cnf(s11,plain,
( ~ spl30_1
| spl30_3
| spl30_4
| spl30_13 ),
inference(sat_conversion,[],[f349]) ).
cnf(s15,plain,
( ~ spl30_1
| spl30_3
| spl30_4
| spl30_15 ),
inference(sat_conversion,[],[f361]) ).
cnf(s17,plain,
( ~ spl30_1
| spl30_3
| spl30_4
| spl30_17 ),
inference(sat_conversion,[],[f371]) ).
cnf(s25,plain,
( ~ spl30_1
| spl30_3
| spl30_4
| ~ spl30_24
| ~ spl30_25
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28 ),
inference(sat_conversion,[],[f422]) ).
cnf(s39,plain,
( ~ spl30_1
| spl30_3
| spl30_4
| spl30_39 ),
inference(sat_conversion,[],[f478]) ).
cnf(s47,plain,
spl30_1,
inference(sat_conversion,[],[f628]) ).
cnf(s49,plain,
~ spl30_3,
inference(sat_conversion,[],[f635]) ).
cnf(s55,plain,
( ~ spl30_6
| spl30_26 ),
inference(sat_conversion,[],[f702]) ).
cnf(s74,plain,
( ~ spl30_26
| spl30_52 ),
inference(sat_conversion,[],[f818]) ).
cnf(s87,plain,
( ~ spl30_27
| spl30_74 ),
inference(sat_conversion,[],[f945]) ).
cnf(s149,plain,
( ~ spl30_26
| spl30_27 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s158,plain,
( ~ spl30_1
| ~ spl30_13
| spl30_72
| spl30_73
| ~ spl30_74 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s160,plain,
~ spl30_73,
inference(sat_conversion,[],[f1724]) ).
cnf(s179,plain,
( ~ spl30_1
| ~ spl30_4
| spl30_73 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s354,plain,
( ~ spl30_15
| spl30_24
| ~ spl30_72 ),
inference(sat_conversion,[],[f3510]) ).
cnf(s355,plain,
( ~ spl30_24
| spl30_25
| ~ spl30_72 ),
inference(sat_conversion,[],[f3512]) ).
cnf(s364,plain,
( ~ spl30_1
| ~ spl30_17
| spl30_28
| ~ spl30_39
| ~ spl30_52 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s365,plain,
( ~ spl30_1
| ~ spl30_13
| spl30_72
| ~ spl30_74 ),
inference(rat,[],[s158,s160]) ).
cnf(s376,plain,
~ spl30_4,
inference(rat,[],[s179,s160,s47]) ).
cnf(s381,plain,
spl30_39,
inference(rat,[],[s39,s376,s49,s47]) ).
cnf(s396,plain,
( ~ spl30_24
| ~ spl30_25
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28 ),
inference(rat,[],[s25,s376,s49,s47]) ).
cnf(s402,plain,
spl30_17,
inference(rat,[],[s17,s376,s49,s47]) ).
cnf(s404,plain,
spl30_15,
inference(rat,[],[s15,s376,s49,s47]) ).
cnf(s406,plain,
spl30_13,
inference(rat,[],[s11,s376,s49,s47]) ).
cnf(s411,plain,
spl30_6,
inference(rat,[],[s3,s376,s49,s47]) ).
cnf(s412,plain,
spl30_26,
inference(rat,[],[s55,s411]) ).
cnf(s413,plain,
spl30_27,
inference(rat,[],[s149,s412]) ).
cnf(s414,plain,
spl30_52,
inference(rat,[],[s74,s412]) ).
cnf(s416,plain,
spl30_74,
inference(rat,[],[s87,s413]) ).
cnf(s419,plain,
spl30_28,
inference(rat,[],[s364,s402,s381,s47,s414]) ).
cnf(s420,plain,
spl30_72,
inference(rat,[],[s365,s406,s47,s416]) ).
cnf(s423,plain,
spl30_24,
inference(rat,[],[s354,s404,s420]) ).
cnf(s424,plain,
spl30_25,
inference(rat,[],[s355,s420,s423]) ).
cnf(s425,plain,
$false,
inference(rat,[],[s396,s419,s413,s412,s424,s423]) ).
tff(f3636,plain,
$false,
inference(avatar_sat_refutation,[],[s425]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW639_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n013.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 14:23:06 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.27 Running first-order theorem proving
% 0.08/0.27 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
% 4.91/1.78 % (1215432)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.91/1.78 % (1215440)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2361994567:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.91/1.78 % (1215445)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3829174179:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.91/1.78 % (1215445)Instruction limit reached!
% 4.91/1.78 % (1215445)------------------------------
% 4.91/1.78 % (1215445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.78 % (1215445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.78 % (1215445)CaDiCaL version: 2.1.3
% 4.91/1.78 % (1215445)Termination reason: Instruction limit
% 4.91/1.78 % (1215445)Termination phase: Saturation
% 4.91/1.78 % (1215445)Time elapsed: 0.045 s
% 4.91/1.78 % (1215445)Peak memory usage: 116 MB
% 4.91/1.78 % (1215445)Instructions burned: 33 (million)
% 4.91/1.78 % (1215441)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1407819491:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.91/1.78 % (1215444)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1702248367:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.91/1.78 % (1215439)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1842759947:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.91/1.78 % (1215442)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1062427060:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.91/1.78 % (1215442)Instruction limit reached!
% 4.91/1.78 % (1215442)------------------------------
% 4.91/1.78 % (1215442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.78 % (1215442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.78 % (1215442)CaDiCaL version: 2.1.3
% 4.91/1.78 % (1215442)Termination reason: Instruction limit
% 4.91/1.78 % (1215442)Termination phase: Property scanning
% 4.91/1.78 % (1215442)Time elapsed: 0.007 s
% 4.91/1.78 % (1215442)Peak memory usage: 86 MB
% 4.91/1.78 % (1215442)Instructions burned: 7 (million)
% 4.91/1.78 % (1215439)Instruction limit reached!
% 4.91/1.78 % (1215439)------------------------------
% 4.91/1.78 % (1215439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.78 % (1215439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.78 % (1215439)CaDiCaL version: 2.1.3
% 4.91/1.78 % (1215439)Termination reason: Instruction limit
% 4.91/1.78 % (1215439)Termination phase: Saturation
% 4.91/1.78 % (1215439)Time elapsed: 0.017 s
% 4.91/1.78 % (1215439)Peak memory usage: 92 MB
% 4.91/1.78 % (1215439)Instructions burned: 12 (million)
% 4.91/1.78 % (1215443)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=630277846:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.91/1.78 % (1215440)Instruction limit reached!
% 4.91/1.78 % (1215440)------------------------------
% 4.91/1.78 % (1215440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.78 % (1215440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.78 % (1215440)CaDiCaL version: 2.1.3
% 4.91/1.78 % (1215440)Termination reason: Instruction limit
% 4.91/1.78 % (1215440)Termination phase: Saturation
% 4.91/1.78 % (1215440)Time elapsed: 0.148 s
% 4.91/1.78 % (1215440)Peak memory usage: 117 MB
% 4.91/1.78 % (1215440)Instructions burned: 308 (million)
% 4.91/1.78 % (1215443)Instruction limit reached!
% 4.91/1.78 % (1215443)------------------------------
% 4.91/1.78 % (1215443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.78 % (1215443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.78 % (1215443)CaDiCaL version: 2.1.3
% 4.91/1.78 % (1215443)Termination reason: Instruction limit
% 4.91/1.78 % (1215443)Termination phase: Preprocessing 3
% 4.91/1.78 % (1215443)Time elapsed: 0.005 s
% 4.91/1.78 % (1215443)Peak memory usage: 86 MB
% 4.91/1.78 % (1215443)Instructions burned: 4 (million)
% 4.91/1.78 % (1215444)Instruction limit reached!
% 4.91/1.78 % (1215444)------------------------------
% 4.91/1.78 % (1215444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.91/1.78 % (1215444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/2.00 % (1215444)CaDiCaL version: 2.1.3
% 6.76/2.00 % (1215444)Termination reason: Instruction limit
% 6.76/2.00 % (1215444)Termination phase: Saturation
% 6.76/2.00 % (1215444)Time elapsed: 0.077 s
% 6.76/2.00 % (1215444)Peak memory usage: 116 MB
% 6.76/2.00 % (1215444)Instructions burned: 46 (million)
% 6.76/2.00 % (1215450)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3715160699:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.76/2.00 % (1215450)Instruction limit reached!
% 6.76/2.00 % (1215450)------------------------------
% 6.76/2.00 % (1215450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/2.00 % (1215450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/2.00 % (1215450)CaDiCaL version: 2.1.3
% 6.76/2.00 % (1215450)Termination reason: Instruction limit
% 6.76/2.00 % (1215450)Termination phase: Saturation
% 6.76/2.00 % (1215450)Time elapsed: 0.009 s
% 6.76/2.00 % (1215450)Peak memory usage: 88 MB
% 6.76/2.00 % (1215450)Instructions burned: 15 (million)
% 6.76/2.00 % (1215455)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=2213883876:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.76/2.00 % (1215458)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3690747728:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.76/2.00 % (1215441)Instruction limit reached!
% 6.76/2.00 % (1215441)------------------------------
% 6.76/2.00 % (1215441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/2.00 % (1215441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/2.00 % (1215441)CaDiCaL version: 2.1.3
% 6.76/2.00 % (1215441)Termination reason: Instruction limit
% 6.76/2.00 % (1215441)Termination phase: Saturation
% 6.76/2.00 % (1215441)Time elapsed: 0.242 s
% 6.76/2.00 % (1215441)Peak memory usage: 119 MB
% 6.76/2.00 % (1215441)Instructions burned: 201 (million)
% 6.76/2.00 % (1215458)Instruction limit reached!
% 6.76/2.00 % (1215458)------------------------------
% 6.76/2.00 % (1215458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/2.00 % (1215458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/2.00 % (1215458)CaDiCaL version: 2.1.3
% 6.76/2.00 % (1215458)Termination reason: Instruction limit
% 6.76/2.00 % (1215458)Termination phase: Saturation
% 6.76/2.00 % (1215458)Time elapsed: 0.014 s
% 6.76/2.00 % (1215458)Peak memory usage: 89 MB
% 6.76/2.00 % (1215458)Instructions burned: 24 (million)
% 6.76/2.00 % (1215456)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2859065469:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.76/2.00 % (1215455)Instruction limit reached!
% 6.76/2.00 % (1215455)------------------------------
% 6.76/2.00 % (1215455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/2.00 % (1215455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/2.00 % (1215455)CaDiCaL version: 2.1.3
% 6.76/2.00 % (1215455)Termination reason: Instruction limit
% 6.76/2.00 % (1215455)Termination phase: Saturation
% 6.76/2.00 % (1215455)Time elapsed: 0.031 s
% 6.76/2.00 % (1215455)Peak memory usage: 89 MB
% 6.76/2.00 % (1215455)Instructions burned: 30 (million)
% 6.76/2.00 % (1215456)Instruction limit reached!
% 6.76/2.00 % (1215456)------------------------------
% 6.76/2.00 % (1215456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/2.00 % (1215456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/2.00 % (1215456)CaDiCaL version: 2.1.3
% 6.76/2.00 % (1215456)Termination reason: Instruction limit
% 6.76/2.00 % (1215456)Termination phase: Saturation
% 6.76/2.00 % (1215456)Time elapsed: 0.016 s
% 6.76/2.00 % (1215456)Peak memory usage: 89 MB
% 6.76/2.00 % (1215456)Instructions burned: 16 (million)
% 6.76/2.00 % (1215459)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=2650104520:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.76/2.00 % (1215461)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1586318773:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.76/2.00 % (1215463)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=326268775:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.24/2.30 % (1215463)Instruction limit reached!
% 9.24/2.30 % (1215463)------------------------------
% 9.24/2.30 % (1215463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.30 % (1215463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.30 % (1215463)CaDiCaL version: 2.1.3
% 9.24/2.30 % (1215463)Termination reason: Instruction limit
% 9.24/2.30 % (1215463)Termination phase: Preprocessing 1
% 9.24/2.30 % (1215463)Time elapsed: 0.002 s
% 9.24/2.30 % (1215463)Peak memory usage: 86 MB
% 9.24/2.30 % (1215463)Instructions burned: 3 (million)
% 9.24/2.30 % (1215459)Instruction limit reached!
% 9.24/2.30 % (1215459)------------------------------
% 9.24/2.30 % (1215459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.30 % (1215459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.30 % (1215459)CaDiCaL version: 2.1.3
% 9.24/2.30 % (1215459)Termination reason: Instruction limit
% 9.24/2.30 % (1215459)Termination phase: Saturation
% 9.24/2.30 % (1215459)Time elapsed: 0.031 s
% 9.24/2.30 % (1215459)Peak memory usage: 90 MB
% 9.24/2.30 % (1215459)Instructions burned: 30 (million)
% 9.24/2.30 % (1215461)Instruction limit reached!
% 9.24/2.30 % (1215461)------------------------------
% 9.24/2.30 % (1215461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.30 % (1215461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.30 % (1215461)CaDiCaL version: 2.1.3
% 9.24/2.30 % (1215461)Termination reason: Instruction limit
% 9.24/2.30 % (1215461)Termination phase: Saturation
% 9.24/2.30 % (1215461)Time elapsed: 0.075 s
% 9.24/2.30 % (1215461)Peak memory usage: 89 MB
% 9.24/2.30 % (1215461)Instructions burned: 85 (million)
% 9.24/2.30 % (1215469)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2847747250:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.24/2.30 % (1215469)Instruction limit reached!
% 9.24/2.30 % (1215469)------------------------------
% 9.24/2.30 % (1215469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.30 % (1215469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.30 % (1215469)CaDiCaL version: 2.1.3
% 9.24/2.30 % (1215469)Termination reason: Instruction limit
% 9.24/2.30 % (1215469)Termination phase: Property scanning
% 9.24/2.30 % (1215469)Time elapsed: 0.003 s
% 9.24/2.30 % (1215469)Peak memory usage: 86 MB
% 9.24/2.30 % (1215469)Instructions burned: 5 (million)
% 9.24/2.30 % (1215470)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=135690890:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.24/2.30 % (1215468)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3609614772:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.24/2.30 % (1215471)lrs+10_1_thi=all:si=on:fd=off:random_seed=2434208221:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 9.24/2.30 % (1215475)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=3344792069:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.24/2.30 % (1215475)Instruction limit reached!
% 9.24/2.30 % (1215475)------------------------------
% 9.24/2.30 % (1215475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.30 % (1215475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.30 % (1215475)CaDiCaL version: 2.1.3
% 9.24/2.30 % (1215475)Termination reason: Instruction limit
% 9.24/2.30 % (1215475)Termination phase: Function definition elimination
% 9.24/2.30 % (1215475)Time elapsed: 0.009 s
% 9.24/2.30 % (1215475)Peak memory usage: 86 MB
% 9.24/2.30 % (1215475)Instructions burned: 9 (million)
% 9.24/2.30 % (1215471)Instruction limit reached!
% 9.24/2.30 % (1215471)------------------------------
% 9.24/2.30 % (1215471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.30 % (1215471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.30 % (1215471)CaDiCaL version: 2.1.3
% 9.24/2.30 % (1215471)Termination reason: Instruction limit
% 9.24/2.30 % (1215471)Termination phase: Saturation
% 9.24/2.30 % (1215471)Time elapsed: 0.089 s
% 9.24/2.30 % (1215471)Peak memory usage: 117 MB
% 9.24/2.30 % (1215471)Instructions burned: 54 (million)
% 10.87/2.68 % (1215470)Instruction limit reached!
% 10.87/2.68 % (1215470)------------------------------
% 10.87/2.68 % (1215470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.68 % (1215470)CaDiCaL version: 2.1.3
% 10.87/2.68 % (1215470)Termination reason: Instruction limit
% 10.87/2.68 % (1215470)Termination phase: Saturation
% 10.87/2.68 % (1215470)Time elapsed: 0.129 s
% 10.87/2.68 % (1215470)Peak memory usage: 134 MB
% 10.87/2.68 % (1215470)Instructions burned: 66 (million)
% 10.87/2.68 % (1215477)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=523224427:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.87/2.68 % (1215476)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2641892690:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 10.87/2.68 % (1215477)Instruction limit reached!
% 10.87/2.68 % (1215477)------------------------------
% 10.87/2.68 % (1215477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.68 % (1215477)CaDiCaL version: 2.1.3
% 10.87/2.68 % (1215477)Termination reason: Instruction limit
% 10.87/2.68 % (1215477)Termination phase: Preprocessing 1
% 10.87/2.68 % (1215477)Time elapsed: 0.003 s
% 10.87/2.68 % (1215477)Peak memory usage: 86 MB
% 10.87/2.68 % (1215477)Instructions burned: 3 (million)
% 10.87/2.68 % (1215476)Instruction limit reached!
% 10.87/2.68 % (1215476)------------------------------
% 10.87/2.68 % (1215476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.68 % (1215476)CaDiCaL version: 2.1.3
% 10.87/2.68 % (1215476)Termination reason: Instruction limit
% 10.87/2.68 % (1215476)Termination phase: Naming
% 10.87/2.68 % (1215476)Time elapsed: 0.003 s
% 10.87/2.68 % (1215476)Peak memory usage: 86 MB
% 10.87/2.68 % (1215476)Instructions burned: 3 (million)
% 10.87/2.68 % (1215479)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=960203628:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 10.87/2.68 % (1215468)Instruction limit reached!
% 10.87/2.68 % (1215468)------------------------------
% 10.87/2.68 % (1215468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.68 % (1215468)CaDiCaL version: 2.1.3
% 10.87/2.68 % (1215468)Termination reason: Instruction limit
% 10.87/2.68 % (1215468)Termination phase: Saturation
% 10.87/2.68 % (1215468)Time elapsed: 0.199 s
% 10.87/2.68 % (1215468)Peak memory usage: 91 MB
% 10.87/2.68 % (1215468)Instructions burned: 181 (million)
% 10.87/2.68 % (1215479)Instruction limit reached!
% 10.87/2.68 % (1215479)------------------------------
% 10.87/2.68 % (1215479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.68 % (1215479)CaDiCaL version: 2.1.3
% 10.87/2.68 % (1215479)Termination reason: Instruction limit
% 10.87/2.68 % (1215479)Termination phase: Saturation
% 10.87/2.68 % (1215479)Time elapsed: 0.091 s
% 10.87/2.68 % (1215479)Peak memory usage: 118 MB
% 10.87/2.68 % (1215479)Instructions burned: 128 (million)
% 10.87/2.68 % (1215488)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1630753954:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 10.87/2.68 % (1215485)dis+10_1_si=on:random_seed=3592145456:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 10.87/2.68 % (1215485)Instruction limit reached!
% 10.87/2.68 % (1215485)------------------------------
% 10.87/2.68 % (1215485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.68 % (1215485)CaDiCaL version: 2.1.3
% 10.87/2.68 % (1215485)Termination reason: Instruction limit
% 10.87/2.68 % (1215485)Termination phase: Property scanning
% 10.87/2.68 % (1215485)Time elapsed: 0.010 s
% 10.87/2.68 % (1215485)Peak memory usage: 86 MB
% 10.87/2.68 % (1215485)Instructions burned: 11 (million)
% 10.87/2.68 % (1215488)Refutation not found, incomplete strategy
% 10.87/2.68 % (1215488)------------------------------
% 10.87/2.68 % (1215488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.68 % (1215488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/3.11 % (1215488)CaDiCaL version: 2.1.3
% 15.49/3.11 % (1215488)Termination reason: Refutation not found, incomplete strategy
% 15.49/3.11 % (1215488)Time elapsed: 0.018 s
% 15.49/3.11 % (1215488)Peak memory usage: 89 MB
% 15.49/3.11 % (1215488)Instructions burned: 18 (million)
% 15.49/3.11 % (1215489)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2680166754: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)
% 15.49/3.11 % (1215490)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=667005407:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 15.49/3.11 % (1215491)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=91842825:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 15.49/3.11 % (1215490)Instruction limit reached!
% 15.49/3.11 % (1215490)------------------------------
% 15.49/3.11 % (1215490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/3.11 % (1215490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/3.11 % (1215490)CaDiCaL version: 2.1.3
% 15.49/3.11 % (1215490)Termination reason: Instruction limit
% 15.49/3.11 % (1215490)Termination phase: Preprocessing 1
% 15.49/3.11 % (1215490)Time elapsed: 0.003 s
% 15.49/3.11 % (1215490)Peak memory usage: 85 MB
% 15.49/3.11 % (1215490)Instructions burned: 3 (million)
% 15.49/3.11 % (1215491)Instruction limit reached!
% 15.49/3.11 % (1215491)------------------------------
% 15.49/3.11 % (1215491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/3.11 % (1215491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/3.11 % (1215491)CaDiCaL version: 2.1.3
% 15.49/3.11 % (1215491)Termination reason: Instruction limit
% 15.49/3.11 % (1215491)Termination phase: Saturation
% 15.49/3.11 % (1215491)Time elapsed: 0.008 s
% 15.49/3.11 % (1215491)Peak memory usage: 87 MB
% 15.49/3.11 % (1215491)Instructions burned: 8 (million)
% 15.49/3.11 % (1215489)Instruction limit reached!
% 15.49/3.11 % (1215489)------------------------------
% 15.49/3.11 % (1215489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/3.12 % (1215489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/3.12 % (1215489)CaDiCaL version: 2.1.3
% 15.49/3.12 % (1215489)Termination reason: Instruction limit
% 15.49/3.12 % (1215489)Termination phase: Saturation
% 15.49/3.12 % (1215489)Time elapsed: 0.039 s
% 15.49/3.12 % (1215489)Peak memory usage: 89 MB
% 15.49/3.12 % (1215489)Instructions burned: 36 (million)
% 15.49/3.12 % (1215494)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3173202065:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 15.49/3.12 % (1215493)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=316342652:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 15.49/3.12 % (1215494)Instruction limit reached!
% 15.49/3.12 % (1215494)------------------------------
% 15.49/3.12 % (1215494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/3.12 % (1215494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/3.12 % (1215494)CaDiCaL version: 2.1.3
% 15.49/3.12 % (1215494)Termination reason: Instruction limit
% 15.49/3.12 % (1215494)Termination phase: Saturation
% 15.49/3.12 % (1215494)Time elapsed: 0.008 s
% 15.49/3.12 % (1215494)Peak memory usage: 90 MB
% 15.49/3.12 % (1215494)Instructions burned: 13 (million)
% 15.49/3.12 % (1215497)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1666308478:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 15.49/3.12 % (1215502)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3944575459:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 15.49/3.12 % (1215502)Instruction limit reached!
% 15.49/3.12 % (1215502)------------------------------
% 15.49/3.12 % (1215502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/3.12 % (1215502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/3.12 % (1215502)CaDiCaL version: 2.1.3
% 15.49/3.12 % (1215502)Termination reason: Instruction limit
% 15.49/3.12 % (1215502)Termination phase: Saturation
% 15.49/3.12 % (1215502)Time elapsed: 0.009 s
% 17.84/3.51 % (1215502)Peak memory usage: 88 MB
% 17.84/3.51 % (1215502)Instructions burned: 10 (million)
% 17.84/3.51 % (1215507)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=4069205821:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 17.84/3.51 % (1215504)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=1599748339:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 17.84/3.51 % (1215503)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3460935254:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 17.84/3.51 % (1215497)Refutation not found, incomplete strategy
% 17.84/3.51 % (1215497)------------------------------
% 17.84/3.51 % (1215497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.51 % (1215497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.51 % (1215497)CaDiCaL version: 2.1.3
% 17.84/3.51 % (1215497)Termination reason: Refutation not found, incomplete strategy
% 17.84/3.51 % (1215497)Time elapsed: 0.082 s
% 17.84/3.51 % (1215497)Peak memory usage: 116 MB
% 17.84/3.51 % (1215497)Instructions burned: 44 (million)
% 17.84/3.51 % (1215488)------------------------------
% 17.84/3.51 % (1215488)------------------------------
% 17.84/3.51 % (1215504)Instruction limit reached!
% 17.84/3.51 % (1215504)------------------------------
% 17.84/3.51 % (1215504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.51 % (1215504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.51 % (1215504)CaDiCaL version: 2.1.3
% 17.84/3.51 % (1215504)Termination reason: Instruction limit
% 17.84/3.51 % (1215504)Termination phase: Saturation
% 17.84/3.51 % (1215504)Time elapsed: 0.069 s
% 17.84/3.51 % (1215504)Peak memory usage: 90 MB
% 17.84/3.51 % (1215504)Instructions burned: 76 (million)
% 17.84/3.51 % (1215493)Instruction limit reached!
% 17.84/3.51 % (1215493)------------------------------
% 17.84/3.51 % (1215493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.51 % (1215493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.51 % (1215493)CaDiCaL version: 2.1.3
% 17.84/3.51 % (1215493)Termination reason: Instruction limit
% 17.84/3.51 % (1215493)Termination phase: Saturation
% 17.84/3.51 % (1215493)Time elapsed: 0.328 s
% 17.84/3.51 % (1215493)Peak memory usage: 92 MB
% 17.84/3.51 % (1215493)Instructions burned: 370 (million)
% 17.84/3.51 % (1215503)Instruction limit reached!
% 17.84/3.51 % (1215503)------------------------------
% 17.84/3.51 % (1215503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.51 % (1215503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.51 % (1215503)CaDiCaL version: 2.1.3
% 17.84/3.51 % (1215503)Termination reason: Instruction limit
% 17.84/3.51 % (1215503)Termination phase: Saturation
% 17.84/3.51 % (1215503)Time elapsed: 0.134 s
% 17.84/3.51 % (1215503)Peak memory usage: 133 MB
% 17.84/3.51 % (1215503)Instructions burned: 71 (million)
% 17.84/3.51 % (1215507)Instruction limit reached!
% 17.84/3.51 % (1215507)------------------------------
% 17.84/3.51 % (1215507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.51 % (1215507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.51 % (1215507)CaDiCaL version: 2.1.3
% 17.84/3.51 % (1215507)Termination reason: Instruction limit
% 17.84/3.51 % (1215507)Termination phase: Saturation
% 17.84/3.51 % (1215507)Time elapsed: 0.159 s
% 17.84/3.51 % (1215507)Peak memory usage: 92 MB
% 17.84/3.51 % (1215507)Instructions burned: 295 (million)
% 17.84/3.51 % (1215511)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3991089879:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi)
% 17.84/3.51 % (1215515)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1973408802:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.84/3.51 % (1215516)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1689705851:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 17.84/3.51 % (1215519)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=52433328:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 18.88/3.95 % (1215518)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=858848466:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 18.88/3.95 % (1215511)Instruction limit reached!
% 18.88/3.95 % (1215511)------------------------------
% 18.88/3.95 % (1215511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.95 % (1215511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.95 % (1215511)CaDiCaL version: 2.1.3
% 18.88/3.95 % (1215511)Termination reason: Instruction limit
% 18.88/3.95 % (1215511)Termination phase: Saturation
% 18.88/3.95 % (1215511)Time elapsed: 0.162 s
% 18.88/3.95 % (1215511)Peak memory usage: 117 MB
% 18.88/3.95 % (1215511)Instructions burned: 130 (million)
% 18.88/3.95 % (1215497)------------------------------
% 18.88/3.95 % (1215497)------------------------------
% 18.88/3.95 % (1215520)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3870572010:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi)
% 18.88/3.95 % (1215516)Instruction limit reached!
% 18.88/3.95 % (1215516)------------------------------
% 18.88/3.95 % (1215516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.95 % (1215516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.95 % (1215516)CaDiCaL version: 2.1.3
% 18.88/3.95 % (1215516)Termination reason: Instruction limit
% 18.88/3.95 % (1215516)Termination phase: Saturation
% 18.88/3.95 % (1215516)Time elapsed: 0.097 s
% 18.88/3.95 % (1215516)Peak memory usage: 134 MB
% 18.88/3.95 % (1215516)Instructions burned: 40 (million)
% 18.88/3.95 % (1215515)Instruction limit reached!
% 18.88/3.95 % (1215515)------------------------------
% 18.88/3.95 % (1215515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.95 % (1215515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.95 % (1215515)CaDiCaL version: 2.1.3
% 18.88/3.95 % (1215515)Termination reason: Instruction limit
% 18.88/3.95 % (1215515)Termination phase: Saturation
% 18.88/3.95 % (1215515)Time elapsed: 0.196 s
% 18.88/3.95 % (1215515)Peak memory usage: 134 MB
% 18.88/3.95 % (1215515)Instructions burned: 131 (million)
% 18.88/3.95 % (1215527)dis+10_1_si=on:random_seed=4084513494:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi)
% 18.88/3.95 % (1215520)Instruction limit reached!
% 18.88/3.95 % (1215520)------------------------------
% 18.88/3.95 % (1215520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.95 % (1215520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.95 % (1215520)CaDiCaL version: 2.1.3
% 18.88/3.95 % (1215520)Termination reason: Instruction limit
% 18.88/3.95 % (1215520)Termination phase: Saturation
% 18.88/3.95 % (1215520)Time elapsed: 0.169 s
% 18.88/3.95 % (1215520)Peak memory usage: 117 MB
% 18.88/3.95 % (1215520)Instructions burned: 131 (million)
% 18.88/3.95 % (1215526)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=802017119:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 18.88/3.95 % (1215518)Instruction limit reached!
% 18.88/3.95 % (1215518)------------------------------
% 18.88/3.95 % (1215518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.95 % (1215518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.95 % (1215518)CaDiCaL version: 2.1.3
% 18.88/3.95 % (1215518)Termination reason: Instruction limit
% 18.88/3.95 % (1215518)Termination phase: Saturation
% 18.88/3.95 % (1215518)Time elapsed: 0.309 s
% 18.88/3.95 % (1215518)Peak memory usage: 93 MB
% 18.88/3.95 % (1215518)Instructions burned: 307 (million)
% 18.88/3.95 % (1215519)Instruction limit reached!
% 18.88/3.95 % (1215519)------------------------------
% 18.88/3.95 % (1215519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.95 % (1215519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.95 % (1215519)CaDiCaL version: 2.1.3
% 18.88/3.95 % (1215519)Termination reason: Instruction limit
% 18.88/3.95 % (1215519)Termination phase: Saturation
% 18.88/3.95 % (1215519)Time elapsed: 0.356 s
% 18.88/3.95 % (1215519)Peak memory usage: 138 MB
% 18.88/3.95 % (1215519)Instructions burned: 598 (million)
% 18.88/3.95 % (1215529)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1491889817:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 18.88/3.95 % (1215530)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2526469547:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 22.53/4.12 % (1215533)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=443101232:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi)
% 22.53/4.12 % (1215526)Instruction limit reached!
% 22.53/4.12 % (1215526)------------------------------
% 22.53/4.12 % (1215526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215526)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215526)Termination reason: Instruction limit
% 22.53/4.12 % (1215526)Termination phase: Saturation
% 22.53/4.12 % (1215526)Time elapsed: 0.295 s
% 22.53/4.12 % (1215526)Peak memory usage: 117 MB
% 22.53/4.12 % (1215526)Instructions burned: 259 (million)
% 22.53/4.12 % (1215536)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=1525761747:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 22.53/4.12 % (1215534)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3620880942:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 22.53/4.12 % (1215530)Instruction limit reached!
% 22.53/4.12 % (1215530)------------------------------
% 22.53/4.12 % (1215530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215530)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215530)Termination reason: Instruction limit
% 22.53/4.12 % (1215530)Termination phase: Saturation
% 22.53/4.12 % (1215530)Time elapsed: 0.154 s
% 22.53/4.12 % (1215530)Peak memory usage: 91 MB
% 22.53/4.12 % (1215530)Instructions burned: 142 (million)
% 22.53/4.12 % (1215533)Instruction limit reached!
% 22.53/4.12 % (1215533)------------------------------
% 22.53/4.12 % (1215533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215533)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215533)Termination reason: Instruction limit
% 22.53/4.12 % (1215533)Termination phase: Saturation
% 22.53/4.12 % (1215533)Time elapsed: 0.095 s
% 22.53/4.12 % (1215533)Peak memory usage: 116 MB
% 22.53/4.12 % (1215533)Instructions burned: 66 (million)
% 22.53/4.12 % (1215536)Instruction limit reached!
% 22.53/4.12 % (1215536)------------------------------
% 22.53/4.12 % (1215536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215536)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215536)Termination reason: Instruction limit
% 22.53/4.12 % (1215536)Termination phase: Saturation
% 22.53/4.12 % (1215536)Time elapsed: 0.088 s
% 22.53/4.12 % (1215536)Peak memory usage: 117 MB
% 22.53/4.12 % (1215536)Instructions burned: 129 (million)
% 22.53/4.12 % (1215534)Instruction limit reached!
% 22.53/4.12 % (1215534)------------------------------
% 22.53/4.12 % (1215534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215534)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215534)Termination reason: Instruction limit
% 22.53/4.12 % (1215534)Termination phase: Saturation
% 22.53/4.12 % (1215534)Time elapsed: 0.124 s
% 22.53/4.12 % (1215534)Peak memory usage: 90 MB
% 22.53/4.12 % (1215534)Instructions burned: 121 (million)
% 22.53/4.12 % (1215529)Instruction limit reached!
% 22.53/4.12 % (1215529)------------------------------
% 22.53/4.12 % (1215529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215529)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215529)Termination reason: Instruction limit
% 22.53/4.12 % (1215529)Termination phase: Saturation
% 22.53/4.12 % (1215529)Time elapsed: 0.382 s
% 22.53/4.12 % (1215529)Peak memory usage: 92 MB
% 22.53/4.12 % (1215529)Instructions burned: 384 (million)
% 22.53/4.12 % (1215539)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=270730941:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi)
% 22.53/4.12 % (1215539)Instruction limit reached!
% 22.53/4.12 % (1215539)------------------------------
% 22.53/4.12 % (1215539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215539)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215539)Termination reason: Instruction limit
% 22.53/4.12 % (1215539)Termination phase: Saturation
% 22.53/4.12 % (1215539)Time elapsed: 0.042 s
% 22.53/4.12 % (1215539)Peak memory usage: 116 MB
% 22.53/4.12 % (1215539)Instructions burned: 42 (million)
% 22.53/4.12 % (1215542)dis+1010_1_to=kbo:si=on:random_seed=2318227296:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi)
% 22.53/4.12 % (1215543)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1729403333:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 22.53/4.12 % (1215544)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=393452146:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 22.53/4.12 % (1215546)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1536960268:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 22.53/4.12 % (1215545)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=24190049:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 22.53/4.12 % (1215542)First to succeed.
% 22.53/4.12 % (1215542)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1215432"
% 22.53/4.12 % (1215548)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=848703624:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi)
% 22.53/4.12 % (1215546)Instruction limit reached!
% 22.53/4.12 % (1215546)------------------------------
% 22.53/4.12 % (1215546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215546)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215546)Termination reason: Instruction limit
% 22.53/4.12 % (1215546)Termination phase: Saturation
% 22.53/4.12 % (1215546)Time elapsed: 0.212 s
% 22.53/4.12 % (1215546)Peak memory usage: 117 MB
% 22.53/4.12 % (1215546)Instructions burned: 350 (million)
% 22.53/4.12 % (1215527)Instruction limit reached!
% 22.53/4.12 % (1215527)------------------------------
% 22.53/4.12 % (1215527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215527)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215527)Termination reason: Instruction limit
% 22.53/4.12 % (1215527)Termination phase: Saturation
% 22.53/4.12 % (1215527)Time elapsed: 0.951 s
% 22.53/4.12 % (1215527)Peak memory usage: 94 MB
% 22.53/4.12 % (1215527)Instructions burned: 1000 (million)
% 22.53/4.12 % (1215545)Instruction limit reached!
% 22.53/4.12 % (1215545)------------------------------
% 22.53/4.12 % (1215545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215545)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215545)Termination reason: Instruction limit
% 22.53/4.12 % (1215545)Termination phase: Saturation
% 22.53/4.12 % (1215545)Time elapsed: 0.256 s
% 22.53/4.12 % (1215545)Peak memory usage: 136 MB
% 22.53/4.12 % (1215545)Instructions burned: 215 (million)
% 22.53/4.12 % (1215543)Instruction limit reached!
% 22.53/4.12 % (1215543)------------------------------
% 22.53/4.12 % (1215543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215543)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215543)Termination reason: Instruction limit
% 22.53/4.12 % (1215543)Termination phase: Saturation
% 22.53/4.12 % (1215543)Time elapsed: 0.392 s
% 22.53/4.12 % (1215543)Peak memory usage: 121 MB
% 22.53/4.12 % (1215543)Instructions burned: 329 (million)
% 22.53/4.12 % (1215548)Instruction limit reached!
% 22.53/4.12 % (1215548)------------------------------
% 22.53/4.12 % (1215548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215548)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215548)Termination reason: Instruction limit
% 22.53/4.12 % (1215548)Termination phase: Saturation
% 22.53/4.12 % (1215548)Time elapsed: 0.154 s
% 22.53/4.12 % (1215548)Peak memory usage: 91 MB
% 22.53/4.12 % (1215548)Instructions burned: 296 (million)
% 22.53/4.12 % (1215555)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1674918982:i=328:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/328Mi)
% 22.53/4.12 % (1215544)Instruction limit reached!
% 22.53/4.12 % (1215544)------------------------------
% 22.53/4.12 % (1215544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.53/4.12 % (1215544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.53/4.12 % (1215544)CaDiCaL version: 2.1.3
% 22.53/4.12 % (1215544)Termination reason: Instruction limit
% 22.53/4.12 % (1215544)Termination phase: Saturation
% 22.53/4.12 % (1215544)Time elapsed: 0.544 s
% 22.53/4.12 % (1215544)Peak memory usage: 136 MB
% 22.53/4.12 % (1215544)Instructions burned: 483 (million)
% 22.53/4.12 % (1215556)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=829144905:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi)
% 22.53/4.12 % (1215542)Refutation found. Thanks to Tanya!
% 22.53/4.12 % SZS status Theorem for theBenchmark
% 22.53/4.12 % SZS output start Proof for theBenchmark
% See solution above
% 23.44/4.46 % (1215542)------------------------------
% 23.44/4.46 % (1215542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.44/4.46 % (1215542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.44/4.46 % (1215542)CaDiCaL version: 2.1.3
% 23.44/4.46 % (1215542)Termination reason: Refutation
% 23.44/4.46 % (1215542)Time elapsed: 0.181 s
% 23.44/4.46 % (1215542)Peak memory usage: 93 MB
% 23.44/4.46 % (1215542)Instructions burned: 167 (million)
% 23.44/4.46 % (1215542)------------------------------
% 23.44/4.46 % (1215542)------------------------------
% 23.44/4.46 % (1215432)Success in time 3.208 s
% 23.44/4.46 % Vampire exiting
%------------------------------------------------------------------------------