%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW641_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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:01 PM UTC 2026
% Result : Theorem 6.25s 1.64s
% Output : Refutation 8.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 39
% Syntax : Number of formulae : 179 ( 98 unt; 0 typ; 26 def)
% Number of atoms : 450 ( 115 equ)
% Maximal formula atoms : 22 ( 2 avg)
% Number of connectives : 363 ( 92 ~; 92 |; 130 &)
% ( 3 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 536 ( 157 atm; 130 fun; 198 num; 51 var)
% Number of types : 11 ( 9 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 6 usr; 4 prp; 0-2 aty)
% Number of functors : 113 ( 109 usr; 64 con; 0-5 aty)
% Number of variables : 183 ( 0 sgn 165 !; 18 ?; 183 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
char1: $tType ).
tff(type_def_10,type,
string2: $tType ).
tff(type_def_11,type,
rope1: $tType ).
tff(type_def_12,type,
array_rope: $tType ).
tff(type_def_13,type,
map_int_rope: $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,
char: ty ).
tff(func_def_13,type,
dummy_char1: char1 ).
tff(func_def_14,type,
string: ty ).
tff(func_def_15,type,
length3: string2 > $int ).
tff(func_def_16,type,
mixfix_lbrb1: ( string2 * $int ) > char1 ).
tff(func_def_17,type,
empty1: string2 ).
tff(func_def_18,type,
app2: ( string2 * string2 ) > string2 ).
tff(func_def_21,type,
sub1: ( string2 * $int * $int ) > string2 ).
tff(func_def_22,type,
rope: ty ).
tff(func_def_23,type,
emp1: rope1 ).
tff(func_def_24,type,
str1: ( string2 * $int * $int ) > rope1 ).
tff(func_def_25,type,
app3: ( rope1 * rope1 * $int ) > rope1 ).
tff(func_def_26,type,
match_rope1: ( ty * rope1 * uni * uni * uni ) > uni ).
tff(func_def_27,type,
str_proj_11: rope1 > string2 ).
tff(func_def_28,type,
str_proj_21: rope1 > $int ).
tff(func_def_29,type,
str_proj_31: rope1 > $int ).
tff(func_def_30,type,
app_proj_11: rope1 > rope1 ).
tff(func_def_31,type,
app_proj_21: rope1 > rope1 ).
tff(func_def_32,type,
app_proj_31: rope1 > $int ).
tff(func_def_33,type,
length4: rope1 > $int ).
tff(func_def_34,type,
string3: rope1 > string2 ).
tff(func_def_35,type,
fib1: $int > $int ).
tff(func_def_38,type,
min1: ( $int * $int ) > $int ).
tff(func_def_39,type,
max2: ( $int * $int ) > $int ).
tff(func_def_40,type,
map: ( ty * ty ) > ty ).
tff(func_def_41,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_42,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_43,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_44,type,
array: ty > ty ).
tff(func_def_45,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_46,type,
length5: ( ty * uni ) > $int ).
tff(func_def_47,type,
elts: ( ty * uni ) > uni ).
tff(func_def_48,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_49,type,
t2tb: $int > uni ).
tff(func_def_50,type,
tb2t: uni > $int ).
tff(func_def_51,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_52,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_53,type,
ref: ty > ty ).
tff(func_def_54,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_55,type,
contents: ( ty * uni ) > uni ).
tff(func_def_56,type,
max3: $int ).
tff(func_def_57,type,
string_of_array1: ( array_rope * $int * $int ) > string2 ).
tff(func_def_58,type,
t2tb1: array_rope > uni ).
tff(func_def_59,type,
tb2t1: uni > array_rope ).
tff(func_def_60,type,
t2tb2: rope1 > uni ).
tff(func_def_61,type,
tb2t2: uni > rope1 ).
tff(func_def_62,type,
string_of_queue1: array_rope > string2 ).
tff(func_def_63,type,
t2tb3: map_int_rope > uni ).
tff(func_def_64,type,
tb2t3: uni > map_int_rope ).
tff(func_def_66,type,
sK0: map_int_rope ).
tff(func_def_67,type,
sK1: $int ).
tff(func_def_68,type,
sK2: $int ).
tff(func_def_69,type,
sK3: rope1 ).
tff(func_def_70,type,
sK4: rope1 ).
tff(func_def_71,type,
sK5: map_int_rope ).
tff(func_def_72,type,
sK6: ( array_rope * $int * $int ) > $int ).
tff(func_def_73,type,
sK7: ( $int * $int * array_rope * array_rope ) > $int ).
tff(func_def_74,type,
sF8: uni ).
tff(func_def_75,type,
sF9: $int > uni ).
tff(func_def_76,type,
sF10: $int > rope1 ).
tff(func_def_77,type,
sF11: uni ).
tff(func_def_78,type,
sF12: uni ).
tff(func_def_79,type,
sF13: rope1 ).
tff(func_def_80,type,
sF14: uni ).
tff(func_def_81,type,
sF15: uni ).
tff(func_def_82,type,
sF16: map_int_rope ).
tff(func_def_83,type,
sF17: uni ).
tff(func_def_84,type,
sF18: uni ).
tff(func_def_85,type,
sF19: array_rope ).
tff(func_def_86,type,
sF20: $int ).
tff(func_def_87,type,
sF21: $int ).
tff(func_def_88,type,
sF22: string2 ).
tff(func_def_89,type,
sF23: uni ).
tff(func_def_90,type,
sF24: array_rope ).
tff(func_def_91,type,
sF25: string2 ).
tff(func_def_92,type,
sF26: string2 ).
tff(func_def_93,type,
sF27: string2 ).
tff(func_def_94,type,
sF28: string2 ).
tff(func_def_95,type,
sF29: string2 ).
tff(func_def_96,type,
sF30: uni ).
tff(func_def_97,type,
sF31: $int ).
tff(func_def_98,type,
sF32: uni ).
tff(func_def_99,type,
sF33: $int ).
tff(func_def_100,type,
sF34: uni ).
tff(func_def_101,type,
sF35: uni ).
tff(func_def_102,type,
sF36: $int ).
tff(func_def_103,type,
sF37: $int ).
tff(func_def_104,type,
sF38: string2 ).
tff(func_def_105,type,
sF39: string2 ).
tff(func_def_106,type,
sF40: string2 ).
tff(func_def_107,type,
sF41: $int ).
tff(func_def_108,type,
sF42: $int ).
tff(func_def_109,type,
sF43: uni ).
tff(func_def_110,type,
sF44: $int ).
tff(func_def_111,type,
sF45: uni ).
tff(func_def_112,type,
sF46: uni ).
tff(func_def_113,type,
sF47: $int ).
tff(func_def_114,type,
sF48: $int ).
tff(func_def_115,type,
sF49: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
infix_eqeq1: ( string2 * string2 ) > $o ).
tff(pred_def_5,type,
inv1: rope1 > $o ).
tff(f12,axiom,
! [X1: string2,X0: string2] :
( infix_eqeq1(X0,X1)
=> ( X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality) ).
tff(f16,axiom,
! [X0: string2,X2: string2,X1: string2] : infix_eqeq1(app2(X0,app2(X1,X2)),app2(app2(X0,X1),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',app_assoc) ).
tff(f52,axiom,
! [X1: ty,X3: uni,X5: uni,X2: uni,X4: uni,X0: ty] :
( sort1(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select_eq) ).
tff(f57,axiom,
! [X0: ty,X2: uni,X1: $int] : ( length5(X0,mk_array1(X0,X1,X2)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def2) ).
tff(f59,axiom,
! [X1: $int,X2: uni,X0: ty] :
( sort1(map(int,X0),X2)
=> ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def1) ).
tff(f65,axiom,
! [X2: $int,X1: uni,X0: ty] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_def) ).
tff(f77,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f79,axiom,
! [X0: rope1] : sort1(rope,t2tb2(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f80,axiom,
! [X0: rope1] : ( tb2t2(t2tb2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL2) ).
tff(f82,axiom,
! [X1: $int,X0: array_rope,X2: $int] :
( ( $lesseq(X2,length5(rope,t2tb1(X0)))
& $lesseq(0,X1)
& $less(X1,X2) )
=> infix_eqeq1(string_of_array1(X0,X1,X2),app2(string_of_array1(X0,$sum(X1,1),X2),string3(tb2t2(get2(rope,t2tb1(X0),X1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',string_of_array_concat_left) ).
tff(f90,axiom,
! [X0: map_int_rope] : sort1(map(int,rope),t2tb3(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort3) ).
tff(f92,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f93,conjecture,
! [X1: map_int_rope,X2: $int,X3: rope1,X0: $int] :
( ( $lesseq(2,X2)
& $less(X2,X0)
& ! [X4: $int] :
( ( $lesseq(2,X4)
& $lesseq(X4,max3) )
=> inv1(tb2t2(get(rope,int,t2tb3(X1),t2tb(X4)))) )
& ( X0 = $sum(max3,1) )
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),X2,$sum(max3,1))),tb2t(match_rope1(int,X3,t2tb(0),t2tb(str_proj_31(X3)),t2tb(app_proj_31(X3))))),fib1($sum(max3,1)))
& $lesseq(0,X0)
& inv1(X3) )
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( ( inv1(X3)
& inv1(tb2t2(get(rope,int,t2tb3(X1),t2tb(X2)))) )
=> ! [X5: rope1] :
( ( infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X1),t2tb(X2)))),string3(X3)))
& inv1(X5) )
=> ( $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X2,1)))
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ! [X6: map_int_rope] :
( ( $lesseq(0,X0)
& ( X6 = tb2t3(set(rope,int,t2tb3(X1),t2tb(X2),t2tb2(X5))) ) )
=> ( infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X6))),$sum(X2,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),$sum(X2,1),$sum(max3,1)))
=> infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X6))),X2,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),X2,$sum(max3,1)),string3(X3))) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_insert) ).
tff(f94,negated_conjecture,
~ ! [X1: map_int_rope,X2: $int,X3: rope1,X0: $int] :
( ( $lesseq(2,X2)
& $less(X2,X0)
& ! [X4: $int] :
( ( $lesseq(2,X4)
& $lesseq(X4,max3) )
=> inv1(tb2t2(get(rope,int,t2tb3(X1),t2tb(X4)))) )
& ( X0 = $sum(max3,1) )
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),X2,$sum(max3,1))),tb2t(match_rope1(int,X3,t2tb(0),t2tb(str_proj_31(X3)),t2tb(app_proj_31(X3))))),fib1($sum(max3,1)))
& $lesseq(0,X0)
& inv1(X3) )
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ( ( inv1(X3)
& inv1(tb2t2(get(rope,int,t2tb3(X1),t2tb(X2)))) )
=> ! [X5: rope1] :
( ( infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X1),t2tb(X2)))),string3(X3)))
& inv1(X5) )
=> ( $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X2,1)))
=> ( ( $lesseq(0,X2)
& $less(X2,X0) )
=> ! [X6: map_int_rope] :
( ( $lesseq(0,X0)
& ( X6 = tb2t3(set(rope,int,t2tb3(X1),t2tb(X2),t2tb2(X5))) ) )
=> ( infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X6))),$sum(X2,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),$sum(X2,1),$sum(max3,1)))
=> infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X6))),X2,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),X2,$sum(max3,1)),string3(X3))) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f93]) ).
tff(f98,plain,
~ ! [X1: map_int_rope,X2: $int,X3: rope1,X0: $int] :
( ( ~ $less(X2,2)
& $less(X2,X0)
& ! [X4: $int] :
( ( ~ $less(max3,X4)
& ~ $less(X4,2) )
=> inv1(tb2t2(get(rope,int,t2tb3(X1),t2tb(X4)))) )
& ( X0 = $sum(max3,1) )
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),X2,$sum(max3,1))),tb2t(match_rope1(int,X3,t2tb(0),t2tb(str_proj_31(X3)),t2tb(app_proj_31(X3))))),fib1($sum(max3,1)))
& ~ $less(X0,0)
& inv1(X3) )
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ( ( inv1(X3)
& inv1(tb2t2(get(rope,int,t2tb3(X1),t2tb(X2)))) )
=> ! [X5: rope1] :
( ( infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X1),t2tb(X2)))),string3(X3)))
& inv1(X5) )
=> ( $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X2,1)))
=> ( ( ~ $less(X2,0)
& $less(X2,X0) )
=> ! [X6: map_int_rope] :
( ( ~ $less(X0,0)
& ( X6 = tb2t3(set(rope,int,t2tb3(X1),t2tb(X2),t2tb2(X5))) ) )
=> ( infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X6))),$sum(X2,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),$sum(X2,1),$sum(max3,1)))
=> infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X6))),X2,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X0,t2tb3(X1))),X2,$sum(max3,1)),string3(X3))) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f94]) ).
tff(f111,plain,
! [X1: $int,X0: array_rope,X2: $int] :
( ( ~ $less(length5(rope,t2tb1(X0)),X2)
& ~ $less(X1,0)
& $less(X1,X2) )
=> infix_eqeq1(string_of_array1(X0,X1,X2),app2(string_of_array1(X0,$sum(X1,1),X2),string3(tb2t2(get2(rope,t2tb1(X0),X1))))) ),
inference(theory_normalization,[],[f82]) ).
tff(f122,plain,
~ ! [X2: rope1,X1: $int,X0: map_int_rope,X3: $int] :
( ( ~ $less(X3,0)
& ( $sum(max3,1) = X3 )
& inv1(X2)
& ~ $less(X1,2)
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),X1,$sum(max3,1))),tb2t(match_rope1(int,X2,t2tb(0),t2tb(str_proj_31(X2)),t2tb(app_proj_31(X2))))),fib1($sum(max3,1)))
& $less(X1,X3)
& ! [X4: $int] :
( ( ~ $less(max3,X4)
& ~ $less(X4,2) )
=> inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X4)))) ) )
=> ( ( ~ $less(X1,0)
& $less(X1,X3) )
=> ( ( inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X1))))
& inv1(X2) )
=> ! [X5: rope1] :
( ( inv1(X5)
& infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X0),t2tb(X1)))),string3(X2))) )
=> ( $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X1,1)))
=> ( ( $less(X1,X3)
& ~ $less(X1,0) )
=> ! [X6: map_int_rope] :
( ( ( tb2t3(set(rope,int,t2tb3(X0),t2tb(X1),t2tb2(X5))) = X6 )
& ~ $less(X3,0) )
=> ( infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X6))),$sum(X1,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),$sum(X1,1),$sum(max3,1)))
=> infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X6))),X1,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),X1,$sum(max3,1)),string3(X2))) ) ) ) ) ) ) ) ),
inference(rectify,[],[f98]) ).
tff(f125,plain,
! [X2: string2,X0: string2,X1: string2] : infix_eqeq1(app2(X0,app2(X2,X1)),app2(app2(X0,X2),X1)),
inference(rectify,[],[f16]) ).
tff(f133,plain,
! [X0: $int,X1: array_rope,X2: $int] :
( ( ~ $less(X0,0)
& $less(X0,X2)
& ~ $less(length5(rope,t2tb1(X1)),X2) )
=> infix_eqeq1(string_of_array1(X1,X0,X2),app2(string_of_array1(X1,$sum(X0,1),X2),string3(tb2t2(get2(rope,t2tb1(X1),X0))))) ),
inference(rectify,[],[f111]) ).
tff(f135,plain,
! [X1: uni,X3: uni,X0: ty,X4: uni,X2: uni,X5: ty] :
( sort1(X0,X2)
=> ( ( X1 = X4 )
=> ( get(X0,X5,set(X0,X5,X3,X1,X2),X4) = X2 ) ) ),
inference(rectify,[],[f52]) ).
tff(f138,plain,
! [X1: uni,X0: ty,X2: $int] : ( length5(X0,mk_array1(X0,X2,X1)) = X2 ),
inference(rectify,[],[f57]) ).
tff(f144,plain,
! [X1: uni,X0: $int,X2: ty] :
( sort1(map(int,X2),X1)
=> ( elts(X2,mk_array1(X2,X0,X1)) = X1 ) ),
inference(rectify,[],[f59]) ).
tff(f146,plain,
! [X2: ty,X1: uni,X0: $int] : ( get(X2,int,elts(X2,X1),t2tb(X0)) = get2(X2,X1,X0) ),
inference(rectify,[],[f65]) ).
tff(f148,plain,
! [X1: uni,X3: uni,X0: ty,X4: uni,X2: uni,X5: ty] :
( ( get(X0,X5,set(X0,X5,X3,X1,X2),X4) = X2 )
| ( X1 != X4 )
| ~ sort1(X0,X2) ),
inference(ennf_transformation,[],[f135]) ).
tff(f149,plain,
! [X3: uni,X0: ty,X1: uni,X5: ty,X2: uni,X4: uni] :
( ~ sort1(X0,X2)
| ( get(X0,X5,set(X0,X5,X3,X1,X2),X4) = X2 )
| ( X1 != X4 ) ),
inference(flattening,[],[f148]) ).
tff(f153,plain,
! [X0: string2,X1: string2] :
( ( X0 = X1 )
| ~ infix_eqeq1(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
tff(f162,plain,
! [X0: $int,X1: array_rope,X2: $int] :
( infix_eqeq1(string_of_array1(X1,X0,X2),app2(string_of_array1(X1,$sum(X0,1),X2),string3(tb2t2(get2(rope,t2tb1(X1),X0)))))
| $less(X0,0)
| ~ $less(X0,X2)
| $less(length5(rope,t2tb1(X1)),X2) ),
inference(ennf_transformation,[],[f133]) ).
tff(f163,plain,
! [X2: $int,X1: array_rope,X0: $int] :
( infix_eqeq1(string_of_array1(X1,X0,X2),app2(string_of_array1(X1,$sum(X0,1),X2),string3(tb2t2(get2(rope,t2tb1(X1),X0)))))
| $less(length5(rope,t2tb1(X1)),X2)
| ~ $less(X0,X2)
| $less(X0,0) ),
inference(flattening,[],[f162]) ).
tff(f164,plain,
! [X1: uni,X2: ty,X0: $int] :
( ~ sort1(map(int,X2),X1)
| ( elts(X2,mk_array1(X2,X0,X1)) = X1 ) ),
inference(ennf_transformation,[],[f144]) ).
tff(f165,plain,
? [X2: rope1,X1: $int,X0: map_int_rope,X3: $int] :
( ? [X5: rope1] :
( ? [X6: map_int_rope] :
( ~ infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X6))),X1,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),X1,$sum(max3,1)),string3(X2)))
& infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X6))),$sum(X1,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),$sum(X1,1),$sum(max3,1)))
& ( tb2t3(set(rope,int,t2tb3(X0),t2tb(X1),t2tb2(X5))) = X6 )
& ~ $less(X3,0) )
& $less(X1,X3)
& ~ $less(X1,0)
& $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X1,1)))
& inv1(X5)
& infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X0),t2tb(X1)))),string3(X2))) )
& inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X1))))
& inv1(X2)
& ~ $less(X1,0)
& $less(X1,X3)
& ~ $less(X3,0)
& ( $sum(max3,1) = X3 )
& inv1(X2)
& ~ $less(X1,2)
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),X1,$sum(max3,1))),tb2t(match_rope1(int,X2,t2tb(0),t2tb(str_proj_31(X2)),t2tb(app_proj_31(X2))))),fib1($sum(max3,1)))
& $less(X1,X3)
& ! [X4: $int] :
( inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X4))))
| $less(max3,X4)
| $less(X4,2) ) ),
inference(ennf_transformation,[],[f122]) ).
tff(f166,plain,
? [X0: map_int_rope,X3: $int,X1: $int,X2: rope1] :
( $less(X1,X3)
& $less(X1,X3)
& ! [X4: $int] :
( $less(X4,2)
| $less(max3,X4)
| inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X4)))) )
& ~ $less(X3,0)
& inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X1))))
& ~ $less(X1,0)
& inv1(X2)
& ? [X5: rope1] :
( ? [X6: map_int_rope] :
( ( tb2t3(set(rope,int,t2tb3(X0),t2tb(X1),t2tb2(X5))) = X6 )
& ~ $less(X3,0)
& infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X6))),$sum(X1,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),$sum(X1,1),$sum(max3,1)))
& ~ infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X6))),X1,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),X1,$sum(max3,1)),string3(X2))) )
& inv1(X5)
& $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X1,1)))
& ~ $less(X1,0)
& infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X0),t2tb(X1)))),string3(X2)))
& $less(X1,X3) )
& ~ $less(X1,2)
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X3,t2tb3(X0))),X1,$sum(max3,1))),tb2t(match_rope1(int,X2,t2tb(0),t2tb(str_proj_31(X2)),t2tb(app_proj_31(X2))))),fib1($sum(max3,1)))
& ( $sum(max3,1) = X3 )
& inv1(X2) ),
inference(flattening,[],[f165]) ).
tff(f167,plain,
! [X0: uni,X1: ty,X2: uni,X3: ty,X4: uni,X5: uni] :
( ~ sort1(X1,X4)
| ( get(X1,X3,set(X1,X3,X0,X2,X4),X5) = X4 )
| ( X2 != X5 ) ),
inference(rectify,[],[f149]) ).
tff(f169,plain,
! [X0: string2,X1: string2,X2: string2] : infix_eqeq1(app2(X1,app2(X0,X2)),app2(app2(X1,X0),X2)),
inference(rectify,[],[f125]) ).
tff(f172,plain,
? [X0: map_int_rope,X1: $int,X2: $int,X3: rope1] :
( $less(X2,X1)
& $less(X2,X1)
& ! [X4: $int] :
( $less(X4,2)
| $less(max3,X4)
| inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X4)))) )
& ~ $less(X1,0)
& inv1(tb2t2(get(rope,int,t2tb3(X0),t2tb(X2))))
& ~ $less(X2,0)
& inv1(X3)
& ? [X5: rope1] :
( ? [X6: map_int_rope] :
( ( tb2t3(set(rope,int,t2tb3(X0),t2tb(X2),t2tb2(X5))) = X6 )
& ~ $less(X1,0)
& infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X1,t2tb3(X6))),$sum(X2,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,X1,t2tb3(X0))),$sum(X2,1),$sum(max3,1)))
& ~ infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,X1,t2tb3(X6))),X2,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,X1,t2tb3(X0))),X2,$sum(max3,1)),string3(X3))) )
& inv1(X5)
& $less(tb2t(match_rope1(int,X5,t2tb(0),t2tb(str_proj_31(X5)),t2tb(app_proj_31(X5)))),fib1($sum(X2,1)))
& ~ $less(X2,0)
& infix_eqeq1(string3(X5),app2(string3(tb2t2(get(rope,int,t2tb3(X0),t2tb(X2)))),string3(X3)))
& $less(X2,X1) )
& ~ $less(X2,2)
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,X1,t2tb3(X0))),X2,$sum(max3,1))),tb2t(match_rope1(int,X3,t2tb(0),t2tb(str_proj_31(X3)),t2tb(app_proj_31(X3))))),fib1($sum(max3,1)))
& ( $sum(max3,1) = X1 )
& inv1(X3) ),
inference(rectify,[],[f166]) ).
tff(f173,plain,
( $less(sK2,sK1)
& $less(sK2,sK1)
& ! [X4: $int] :
( $less(X4,2)
| $less(max3,X4)
| inv1(tb2t2(get(rope,int,t2tb3(sK0),t2tb(X4)))) )
& ~ $less(sK1,0)
& inv1(tb2t2(get(rope,int,t2tb3(sK0),t2tb(sK2))))
& ~ $less(sK2,0)
& inv1(sK3)
& ( sK5 = tb2t3(set(rope,int,t2tb3(sK0),t2tb(sK2),t2tb2(sK4))) )
& ~ $less(sK1,0)
& infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK5))),$sum(sK2,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK0))),$sum(sK2,1),$sum(max3,1)))
& ~ infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK5))),sK2,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK0))),sK2,$sum(max3,1)),string3(sK3)))
& inv1(sK4)
& $less(tb2t(match_rope1(int,sK4,t2tb(0),t2tb(str_proj_31(sK4)),t2tb(app_proj_31(sK4)))),fib1($sum(sK2,1)))
& ~ $less(sK2,0)
& infix_eqeq1(string3(sK4),app2(string3(tb2t2(get(rope,int,t2tb3(sK0),t2tb(sK2)))),string3(sK3)))
& $less(sK2,sK1)
& ~ $less(sK2,2)
& $less($sum(length3(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK0))),sK2,$sum(max3,1))),tb2t(match_rope1(int,sK3,t2tb(0),t2tb(str_proj_31(sK3)),t2tb(app_proj_31(sK3))))),fib1($sum(max3,1)))
& ( $sum(max3,1) = sK1 )
& inv1(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X5,sK4),skolemize(X6,sK5)],[f172]) ).
tff(f174,plain,
! [X0: uni,X1: ty,X2: $int] :
( ~ sort1(map(int,X1),X0)
| ( elts(X1,mk_array1(X1,X2,X0)) = X0 ) ),
inference(rectify,[],[f164]) ).
tff(f180,plain,
! [X0: $int,X1: array_rope,X2: $int] :
( infix_eqeq1(string_of_array1(X1,X2,X0),app2(string_of_array1(X1,$sum(X2,1),X0),string3(tb2t2(get2(rope,t2tb1(X1),X2)))))
| $less(length5(rope,t2tb1(X1)),X0)
| ~ $less(X2,X0)
| $less(X2,0) ),
inference(rectify,[],[f163]) ).
tff(f187,plain,
! [X0: ty,X1: uni,X2: $int] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
inference(rectify,[],[f146]) ).
tff(f190,plain,
! [X0: uni,X1: ty,X2: $int] : ( length5(X1,mk_array1(X1,X2,X0)) = X2 ),
inference(rectify,[],[f138]) ).
tff(f192,plain,
! [X2: uni,X3: ty,X0: uni,X1: ty,X4: uni,X5: uni] :
( ~ sort1(X1,X4)
| ( get(X1,X3,set(X1,X3,X0,X2,X4),X5) = X4 )
| ( X2 != X5 ) ),
inference(cnf_transformation,[],[f167]) ).
tff(f193,plain,
! [X0: rope1] : sort1(rope,t2tb2(X0)),
inference(cnf_transformation,[],[f79]) ).
tff(f195,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f92]) ).
tff(f198,plain,
! [X2: string2,X0: string2,X1: string2] : infix_eqeq1(app2(X1,app2(X0,X2)),app2(app2(X1,X0),X2)),
inference(cnf_transformation,[],[f169]) ).
tff(f203,plain,
$sum(max3,1) = sK1,
inference(cnf_transformation,[],[f173]) ).
tff(f206,plain,
$less(sK2,sK1),
inference(cnf_transformation,[],[f173]) ).
tff(f207,plain,
infix_eqeq1(string3(sK4),app2(string3(tb2t2(get(rope,int,t2tb3(sK0),t2tb(sK2)))),string3(sK3))),
inference(cnf_transformation,[],[f173]) ).
tff(f208,plain,
~ $less(sK2,0),
inference(cnf_transformation,[],[f173]) ).
tff(f211,plain,
~ infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK5))),sK2,$sum(max3,1)),app2(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK0))),sK2,$sum(max3,1)),string3(sK3))),
inference(cnf_transformation,[],[f173]) ).
tff(f212,plain,
infix_eqeq1(string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK5))),$sum(sK2,1),$sum(max3,1)),string_of_array1(tb2t1(mk_array1(rope,sK1,t2tb3(sK0))),$sum(sK2,1),$sum(max3,1))),
inference(cnf_transformation,[],[f173]) ).
tff(f214,plain,
sK5 = tb2t3(set(rope,int,t2tb3(sK0),t2tb(sK2),t2tb2(sK4))),
inference(cnf_transformation,[],[f173]) ).
tff(f224,plain,
! [X2: $int,X0: uni,X1: ty] :
( ( elts(X1,mk_array1(X1,X2,X0)) = X0 )
| ~ sort1(map(int,X1),X0) ),
inference(cnf_transformation,[],[f174]) ).
tff(f233,plain,
! [X2: $int,X0: $int,X1: array_rope] :
( infix_eqeq1(string_of_array1(X1,X2,X0),app2(string_of_array1(X1,$sum(X2,1),X0),string3(tb2t2(get2(rope,t2tb1(X1),X2)))))
| $less(length5(rope,t2tb1(X1)),X0)
| ~ $less(X2,X0)
| $less(X2,0) ),
inference(cnf_transformation,[],[f180]) ).
tff(f234,plain,
! [X0: string2,X1: string2] :
( ~ infix_eqeq1(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f153]) ).
tff(f236,plain,
! [X0: rope1] : ( tb2t2(t2tb2(X0)) = X0 ),
inference(cnf_transformation,[],[f80]) ).
tff(f242,plain,
! [X0: map_int_rope] : sort1(map(int,rope),t2tb3(X0)),
inference(cnf_transformation,[],[f90]) ).
tff(f247,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f77]) ).
tff(f250,plain,
! [X2: $int,X0: ty,X1: uni] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
inference(cnf_transformation,[],[f187]) ).
tff(f254,plain,
! [X2: $int,X0: uni,X1: ty] : ( length5(X1,mk_array1(X1,X2,X0)) = X2 ),
inference(cnf_transformation,[],[f190]) ).
tff(f260,plain,
! [X2: $int,X0: $int,X1: array_rope] :
( infix_eqeq1(string_of_array1(X1,X2,X0),app2(string_of_array1(X1,$sum(X2,1),X0),string3(tb2t2(get(rope,int,elts(rope,t2tb1(X1)),t2tb(X2))))))
| ~ $less(X2,X0)
| $less(X2,0)
| $less(length5(rope,t2tb1(X1)),X0) ),
inference(definition_unfolding,[],[f233,f250]) ).
tff(f263,plain,
! [X3: ty,X0: uni,X1: ty,X4: uni,X5: uni] :
( ( get(X1,X3,set(X1,X3,X0,X5,X4),X5) = X4 )
| ~ sort1(X1,X4) ),
inference(equality_resolution,[],[f192]) ).
tff(f264,definition,
sF8 = t2tb3(sK0),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f265,plain,
t2tb3(sK0) = sF8,
inference(reorient_equations,[],[f264]) ).
tff(f270,definition,
sF11 = t2tb(sK2),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f271,plain,
t2tb(sK2) = sF11,
inference(reorient_equations,[],[f270]) ).
tff(f272,definition,
sF12 = get(rope,int,sF8,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f273,definition,
sF13 = tb2t2(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f274,plain,
tb2t2(sF12) = sF13,
inference(reorient_equations,[],[f273]) ).
tff(f276,definition,
sF14 = t2tb2(sK4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f277,plain,
t2tb2(sK4) = sF14,
inference(reorient_equations,[],[f276]) ).
tff(f278,definition,
sF15 = set(rope,int,sF8,sF11,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f279,definition,
sF16 = tb2t3(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f280,plain,
sF16 = sK5,
inference(definition_folding,[],[f214,f279,f278,f277,f271,f265]) ).
tff(f281,definition,
sF17 = t2tb3(sK5),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f282,plain,
t2tb3(sK5) = sF17,
inference(reorient_equations,[],[f281]) ).
tff(f283,definition,
sF18 = mk_array1(rope,sK1,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f284,definition,
sF19 = tb2t1(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f285,plain,
tb2t1(sF18) = sF19,
inference(reorient_equations,[],[f284]) ).
tff(f286,definition,
sF20 = $sum(sK2,1),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f287,plain,
$sum(sK2,1) = sF20,
inference(reorient_equations,[],[f286]) ).
tff(f288,definition,
sF21 = $sum(max3,1),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f289,plain,
$sum(max3,1) = sF21,
inference(reorient_equations,[],[f288]) ).
tff(f290,definition,
sF22 = string_of_array1(sF19,sF20,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f291,plain,
string_of_array1(sF19,sF20,sF21) = sF22,
inference(reorient_equations,[],[f290]) ).
tff(f292,definition,
sF23 = mk_array1(rope,sK1,sF8),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f293,plain,
mk_array1(rope,sK1,sF8) = sF23,
inference(reorient_equations,[],[f292]) ).
tff(f294,definition,
sF24 = tb2t1(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f295,definition,
sF25 = string_of_array1(sF24,sF20,sF21),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f296,plain,
infix_eqeq1(sF22,sF25),
inference(definition_folding,[],[f212,f295,f289,f287,f294,f293,f265,f291,f289,f287,f285,f283,f282]) ).
tff(f297,definition,
sF26 = string_of_array1(sF19,sK2,sF21),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f298,definition,
sF27 = string_of_array1(sF24,sK2,sF21),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f299,definition,
sF28 = string3(sK3),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f300,plain,
string3(sK3) = sF28,
inference(reorient_equations,[],[f299]) ).
tff(f301,definition,
sF29 = app2(sF27,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f302,plain,
app2(sF27,sF28) = sF29,
inference(reorient_equations,[],[f301]) ).
tff(f303,plain,
~ infix_eqeq1(sF26,sF29),
inference(definition_folding,[],[f211,f302,f300,f298,f289,f294,f293,f265,f297,f289,f285,f283,f282]) ).
tff(f317,definition,
sF38 = string3(sK4),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
tff(f318,definition,
sF39 = string3(sF13),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
tff(f319,definition,
sF40 = app2(sF39,sF28),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
tff(f320,plain,
app2(sF39,sF28) = sF40,
inference(reorient_equations,[],[f319]) ).
tff(f321,plain,
infix_eqeq1(sF38,sF40),
inference(definition_folding,[],[f207,f320,f300,f318,f274,f272,f271,f265,f317]) ).
tff(f335,plain,
sF21 = sK1,
inference(definition_folding,[],[f203,f289]) ).
tff(f337,plain,
sort1(rope,sF14),
inference(superposition,[],[f193,f277]) ).
tff(f338,plain,
sF17 = t2tb3(sF16),
inference(forward_demodulation,[],[f282,f280]) ).
tff(f352,plain,
sF15 = t2tb3(sF16),
inference(superposition,[],[f195,f279]) ).
tff(f353,plain,
sF15 = sF17,
inference(forward_demodulation,[],[f352,f338]) ).
tff(f358,plain,
sK4 = tb2t2(sF14),
inference(superposition,[],[f236,f277]) ).
tff(f365,plain,
t2tb1(sF19) = sF18,
inference(superposition,[],[f247,f285]) ).
tff(f366,plain,
t2tb1(sF24) = sF23,
inference(superposition,[],[f247,f294]) ).
tff(f378,plain,
sF25 = sF22,
inference(resolution,[],[f234,f296]) ).
tff(f379,plain,
sF38 = sF40,
inference(resolution,[],[f234,f321]) ).
tff(f382,plain,
sort1(map(int,rope),sF8),
inference(superposition,[],[f242,f265]) ).
tff(f383,plain,
sort1(map(int,rope),sF17),
inference(superposition,[],[f242,f338]) ).
tff(f388,plain,
string_of_array1(sF19,sF20,sK1) = sF22,
inference(forward_demodulation,[],[f291,f335]) ).
tff(f391,plain,
sF25 = string_of_array1(sF24,sF20,sK1),
inference(forward_demodulation,[],[f295,f335]) ).
tff(f392,plain,
string_of_array1(sF24,sF20,sK1) = sF22,
inference(forward_demodulation,[],[f391,f378]) ).
tff(f393,plain,
sF26 = string_of_array1(sF19,sK2,sK1),
inference(forward_demodulation,[],[f297,f335]) ).
tff(f394,plain,
sF27 = string_of_array1(sF24,sK2,sK1),
inference(forward_demodulation,[],[f298,f335]) ).
tff(f402,plain,
length5(rope,sF18) = sK1,
inference(superposition,[],[f254,f283]) ).
tff(f403,plain,
length5(rope,sF23) = sK1,
inference(superposition,[],[f254,f293]) ).
tff(f404,plain,
sF17 = set(rope,int,sF8,sF11,sF14),
inference(forward_demodulation,[],[f278,f353]) ).
tff(f446,plain,
( ~ sort1(map(int,rope),sF17)
| ( elts(rope,sF18) = sF17 ) ),
inference(superposition,[],[f224,f283]) ).
tff(f447,plain,
( ~ sort1(map(int,rope),sF8)
| ( elts(rope,sF23) = sF8 ) ),
inference(superposition,[],[f224,f293]) ).
tff(f450,plain,
elts(rope,sF18) = sF17,
inference(forward_subsumption_resolution,[],[f446,f383]) ).
tff(f451,plain,
elts(rope,sF23) = sF8,
inference(forward_subsumption_resolution,[],[f447,f382]) ).
tff(f461,plain,
( ( get(rope,int,sF17,sF11) = sF14 )
| ~ sort1(rope,sF14) ),
inference(superposition,[],[f263,f404]) ).
tff(f463,plain,
get(rope,int,sF17,sF11) = sF14,
inference(forward_subsumption_resolution,[],[f461,f337]) ).
tff(f547,definition,
( spl50_2
<=> $less(sK1,sK1) ),
introduced(definition,[new_symbols(definition,[spl50_2])],[avatar_definition]) ).
tff(f549,plain,
( $less(sK1,sK1)
| ~ spl50_2 ),
inference(avatar_component_clause,[],[f547]) ).
tff(f611,plain,
( $false
| ~ spl50_2 ),
inference(evaluation,[],[f549]) ).
tff(f612,plain,
~ spl50_2,
inference(avatar_contradiction_clause,[],[f611]) ).
tff(f617,plain,
( infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF19)),t2tb(sK2))))))
| ~ $less(sK2,sK1)
| $less(sK2,0)
| $less(length5(rope,t2tb1(sF19)),sK1) ),
inference(superposition,[],[f260,f393]) ).
tff(f618,plain,
( $less(length5(rope,t2tb1(sF24)),sK1)
| $less(sK2,0)
| ~ $less(sK2,sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF24)),t2tb(sK2)))))) ),
inference(superposition,[],[f260,f394]) ).
tff(f658,plain,
( $less(length5(rope,t2tb1(sF24)),sK1)
| ~ $less(sK2,sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF24)),t2tb(sK2)))))) ),
inference(forward_subsumption_resolution,[],[f618,f208]) ).
tff(f669,plain,
( infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF19)),t2tb(sK2))))))
| $less(sK2,0)
| $less(length5(rope,t2tb1(sF19)),sK1) ),
inference(forward_subsumption_resolution,[],[f617,f206]) ).
tff(f698,plain,
( infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF24)),t2tb(sK2))))))
| $less(length5(rope,t2tb1(sF24)),sK1) ),
inference(forward_subsumption_resolution,[],[f658,f206]) ).
tff(f701,plain,
( $less(length5(rope,t2tb1(sF19)),sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF19)),t2tb(sK2)))))) ),
inference(forward_subsumption_resolution,[],[f669,f208]) ).
tff(f705,plain,
( $less(length5(rope,t2tb1(sF24)),sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF24)),sF11))))) ),
inference(forward_demodulation,[],[f698,f271]) ).
tff(f708,plain,
( $less(length5(rope,sF18),sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF19)),t2tb(sK2)))))) ),
inference(forward_demodulation,[],[f701,f365]) ).
tff(f710,plain,
( $less(length5(rope,sF23),sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF24)),sF11))))) ),
inference(forward_demodulation,[],[f705,f366]) ).
tff(f713,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF19)),t2tb(sK2)))))) ),
inference(forward_demodulation,[],[f708,f402]) ).
tff(f723,plain,
( infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF24)),sF11)))))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f710,f403]) ).
tff(f725,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,t2tb1(sF19)),sF11))))) ),
inference(forward_demodulation,[],[f713,f271]) ).
tff(f726,plain,
( infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,sF23),sF11)))))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f723,f366]) ).
tff(f728,plain,
( infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,elts(rope,sF18),sF11)))))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f725,f365]) ).
tff(f729,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,sF8,sF11))))) ),
inference(forward_demodulation,[],[f726,f451]) ).
tff(f735,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(get(rope,int,sF17,sF11))))) ),
inference(forward_demodulation,[],[f728,f450]) ).
tff(f736,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(tb2t2(sF12)))) ),
inference(forward_demodulation,[],[f729,f272]) ).
tff(f737,plain,
( infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(tb2t2(sF14))))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f735,f463]) ).
tff(f738,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),string3(sF13))) ),
inference(forward_demodulation,[],[f736,f274]) ).
tff(f739,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),string3(sK4))) ),
inference(forward_demodulation,[],[f737,f358]) ).
tff(f740,plain,
( infix_eqeq1(sF27,app2(string_of_array1(sF24,$sum(sK2,1),sK1),sF39))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f738,f318]) ).
tff(f741,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),sF38)) ),
inference(forward_demodulation,[],[f739,f317]) ).
tff(f742,plain,
( infix_eqeq1(sF27,app2(string_of_array1(sF24,sF20,sK1),sF39))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f740,f287]) ).
tff(f743,plain,
( $less(sK1,sK1)
| infix_eqeq1(sF26,app2(string_of_array1(sF19,$sum(sK2,1),sK1),sF40)) ),
inference(forward_demodulation,[],[f741,f379]) ).
tff(f744,plain,
( infix_eqeq1(sF27,app2(sF22,sF39))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f742,f392]) ).
tff(f745,plain,
( infix_eqeq1(sF26,app2(string_of_array1(sF19,sF20,sK1),sF40))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f743,f287]) ).
tff(f747,definition,
( spl50_34
<=> infix_eqeq1(sF27,app2(sF22,sF39)) ),
introduced(definition,[new_symbols(definition,[spl50_34])],[avatar_definition]) ).
tff(f749,plain,
( infix_eqeq1(sF27,app2(sF22,sF39))
| ~ spl50_34 ),
inference(avatar_component_clause,[],[f747]) ).
tff(f750,plain,
( spl50_34
| spl50_2 ),
inference(avatar_split_clause,[],[f744,f547,f747]) ).
tff(f751,plain,
( infix_eqeq1(sF26,app2(sF22,sF40))
| $less(sK1,sK1) ),
inference(forward_demodulation,[],[f745,f388]) ).
tff(f753,definition,
( spl50_35
<=> infix_eqeq1(sF26,app2(sF22,sF40)) ),
introduced(definition,[new_symbols(definition,[spl50_35])],[avatar_definition]) ).
tff(f755,plain,
( infix_eqeq1(sF26,app2(sF22,sF40))
| ~ spl50_35 ),
inference(avatar_component_clause,[],[f753]) ).
tff(f756,plain,
( spl50_2
| spl50_35 ),
inference(avatar_split_clause,[],[f751,f753,f547]) ).
tff(f1007,plain,
( ( app2(sF22,sF39) = sF27 )
| ~ spl50_34 ),
inference(resolution,[],[f749,f234]) ).
tff(f1030,plain,
( ( sF26 = app2(sF22,sF40) )
| ~ spl50_35 ),
inference(resolution,[],[f755,f234]) ).
tff(f1097,plain,
( ! [X0: string2] : infix_eqeq1(app2(sF22,app2(sF39,X0)),app2(sF27,X0))
| ~ spl50_34 ),
inference(superposition,[],[f198,f1007]) ).
tff(f1140,plain,
( infix_eqeq1(app2(sF22,sF40),app2(sF27,sF28))
| ~ spl50_34 ),
inference(superposition,[],[f1097,f320]) ).
tff(f1142,plain,
( infix_eqeq1(app2(sF22,sF40),sF29)
| ~ spl50_34 ),
inference(forward_demodulation,[],[f1140,f302]) ).
tff(f1144,plain,
( infix_eqeq1(sF26,sF29)
| ~ spl50_34
| ~ spl50_35 ),
inference(forward_demodulation,[],[f1142,f1030]) ).
tff(f1146,plain,
( $false
| ~ spl50_34
| ~ spl50_35 ),
inference(forward_subsumption_resolution,[],[f1144,f303]) ).
tff(f1147,plain,
( ~ spl50_34
| ~ spl50_35 ),
inference(avatar_contradiction_clause,[],[f1146]) ).
cnf(s13,plain,
~ spl50_2,
inference(sat_conversion,[],[f612]) ).
cnf(s23,plain,
( spl50_2
| spl50_34 ),
inference(sat_conversion,[],[f750]) ).
cnf(s24,plain,
( spl50_2
| spl50_35 ),
inference(sat_conversion,[],[f756]) ).
cnf(s43,plain,
( ~ spl50_34
| ~ spl50_35 ),
inference(sat_conversion,[],[f1147]) ).
cnf(s47,plain,
spl50_35,
inference(rat,[],[s24,s13]) ).
cnf(s48,plain,
spl50_34,
inference(rat,[],[s23,s13]) ).
cnf(s49,plain,
$false,
inference(rat,[],[s43,s47,s48]) ).
tff(f1150,plain,
$false,
inference(avatar_sat_refutation,[],[s49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW641_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.22 % Computer : n018.cluster.edu
% 0.11/0.22 % Model : x86_64 x86_64
% 0.11/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.22 % Memory : 8046.5625MB
% 0.11/0.22 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Mon Sep 28 14:25:55 UTC 2026
% 0.11/0.23 % CPUTime :
% 0.11/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.27 Running first-order theorem proving
% 0.11/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
% 3.96/1.24 % (3422504)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.96/1.24 % (3422535)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=946727323:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.96/1.24 % (3422534)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=953777868:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.96/1.24 % (3422534)Instruction limit reached!
% 3.96/1.24 % (3422534)------------------------------
% 3.96/1.24 % (3422534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.24 % (3422534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.24 % (3422534)CaDiCaL version: 2.1.3
% 3.96/1.24 % (3422534)Termination reason: Instruction limit
% 3.96/1.24 % (3422534)Termination phase: Preprocessing 3
% 3.96/1.24 % (3422534)Time elapsed: 0.002 s
% 3.96/1.24 % (3422534)Peak memory usage: 86 MB
% 3.96/1.24 % (3422534)Instructions burned: 4 (million)
% 3.96/1.24 % (3422530)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2787211605:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.96/1.24 % (3422532)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=178507410:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.96/1.24 % (3422531)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1160989409:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.96/1.24 % (3422535)Instruction limit reached!
% 3.96/1.24 % (3422535)------------------------------
% 3.96/1.24 % (3422535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.24 % (3422535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.24 % (3422535)CaDiCaL version: 2.1.3
% 3.96/1.24 % (3422535)Termination reason: Instruction limit
% 3.96/1.24 % (3422535)Termination phase: Saturation
% 3.96/1.24 % (3422535)Time elapsed: 0.055 s
% 3.96/1.24 % (3422535)Peak memory usage: 116 MB
% 3.96/1.24 % (3422535)Instructions burned: 46 (million)
% 3.96/1.24 % (3422530)Instruction limit reached!
% 3.96/1.24 % (3422530)------------------------------
% 3.96/1.24 % (3422530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.24 % (3422530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.24 % (3422530)CaDiCaL version: 2.1.3
% 3.96/1.24 % (3422530)Termination reason: Instruction limit
% 3.96/1.24 % (3422530)Termination phase: Saturation
% 3.96/1.24 % (3422530)Time elapsed: 0.034 s
% 3.96/1.24 % (3422530)Peak memory usage: 105 MB
% 3.96/1.24 % (3422530)Instructions burned: 12 (million)
% 3.96/1.24 % (3422536)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1078542492:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.96/1.24 % (3422533)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3794392490:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.96/1.24 % (3422533)Instruction limit reached!
% 3.96/1.24 % (3422533)------------------------------
% 3.96/1.24 % (3422533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.24 % (3422533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.24 % (3422533)CaDiCaL version: 2.1.3
% 3.96/1.24 % (3422533)Termination reason: Instruction limit
% 3.96/1.24 % (3422533)Termination phase: Saturation
% 3.96/1.24 % (3422533)Time elapsed: 0.007 s
% 3.96/1.24 % (3422533)Peak memory usage: 87 MB
% 3.96/1.24 % (3422533)Instructions burned: 8 (million)
% 3.96/1.24 % (3422536)Instruction limit reached!
% 3.96/1.24 % (3422536)------------------------------
% 3.96/1.24 % (3422536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.24 % (3422536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.24 % (3422536)CaDiCaL version: 2.1.3
% 3.96/1.24 % (3422536)Termination reason: Instruction limit
% 3.96/1.24 % (3422536)Termination phase: Saturation
% 3.96/1.24 % (3422536)Time elapsed: 0.045 s
% 3.96/1.24 % (3422536)Peak memory usage: 116 MB
% 3.96/1.24 % (3422536)Instructions burned: 33 (million)
% 3.96/1.24 % (3422548)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=87999002:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.96/1.24 % (3422548)Instruction limit reached!
% 3.96/1.24 % (3422548)------------------------------
% 5.27/1.46 % (3422548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.27/1.46 % (3422548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.46 % (3422548)CaDiCaL version: 2.1.3
% 5.27/1.46 % (3422548)Termination reason: Instruction limit
% 5.27/1.46 % (3422548)Termination phase: Saturation
% 5.27/1.46 % (3422548)Time elapsed: 0.009 s
% 5.27/1.46 % (3422548)Peak memory usage: 88 MB
% 5.27/1.46 % (3422548)Instructions burned: 14 (million)
% 5.27/1.46 % (3422553)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=1584357124:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 5.27/1.46 % (3422532)Instruction limit reached!
% 5.27/1.46 % (3422532)------------------------------
% 5.27/1.46 % (3422532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.27/1.46 % (3422532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.46 % (3422532)CaDiCaL version: 2.1.3
% 5.27/1.46 % (3422532)Termination reason: Instruction limit
% 5.27/1.46 % (3422532)Termination phase: Saturation
% 5.27/1.46 % (3422532)Time elapsed: 0.231 s
% 5.27/1.46 % (3422532)Peak memory usage: 118 MB
% 5.27/1.46 % (3422532)Instructions burned: 202 (million)
% 5.27/1.46 % (3422554)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2440802275:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.27/1.46 % (3422553)Instruction limit reached!
% 5.27/1.46 % (3422553)------------------------------
% 5.27/1.46 % (3422553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.27/1.46 % (3422553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.46 % (3422553)CaDiCaL version: 2.1.3
% 5.27/1.46 % (3422553)Termination reason: Instruction limit
% 5.27/1.46 % (3422553)Termination phase: Saturation
% 5.27/1.46 % (3422553)Time elapsed: 0.034 s
% 5.27/1.46 % (3422553)Peak memory usage: 89 MB
% 5.27/1.46 % (3422553)Instructions burned: 29 (million)
% 5.27/1.46 % (3422554)Instruction limit reached!
% 5.27/1.46 % (3422554)------------------------------
% 5.27/1.46 % (3422554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.27/1.46 % (3422554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.46 % (3422554)CaDiCaL version: 2.1.3
% 5.27/1.46 % (3422554)Termination reason: Instruction limit
% 5.27/1.46 % (3422554)Termination phase: Saturation
% 5.27/1.46 % (3422554)Time elapsed: 0.014 s
% 5.27/1.46 % (3422554)Peak memory usage: 89 MB
% 5.27/1.46 % (3422554)Instructions burned: 17 (million)
% 5.27/1.46 % (3422562)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1672881434:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 5.27/1.46 % (3422558)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1386954166:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 5.27/1.46 % (3422561)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=2873910717:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 5.27/1.46 % (3422562)Instruction limit reached!
% 5.27/1.46 % (3422562)------------------------------
% 5.27/1.46 % (3422562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.27/1.46 % (3422562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.46 % (3422562)CaDiCaL version: 2.1.3
% 5.27/1.46 % (3422562)Termination reason: Instruction limit
% 5.27/1.46 % (3422562)Termination phase: Saturation
% 5.27/1.46 % (3422562)Time elapsed: 0.028 s
% 5.27/1.46 % (3422562)Peak memory usage: 89 MB
% 5.27/1.46 % (3422562)Instructions burned: 86 (million)
% 5.27/1.46 % (3422558)Instruction limit reached!
% 5.27/1.46 % (3422558)------------------------------
% 5.27/1.46 % (3422558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.27/1.46 % (3422558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.46 % (3422558)CaDiCaL version: 2.1.3
% 5.27/1.46 % (3422558)Termination reason: Instruction limit
% 5.27/1.46 % (3422558)Termination phase: Saturation
% 5.27/1.46 % (3422558)Time elapsed: 0.028 s
% 5.27/1.46 % (3422558)Peak memory usage: 89 MB
% 5.27/1.46 % (3422558)Instructions burned: 24 (million)
% 5.27/1.46 % (3422561)Instruction limit reached!
% 5.27/1.46 % (3422561)------------------------------
% 5.27/1.46 % (3422561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422561)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422561)Termination reason: Instruction limit
% 6.25/1.63 % (3422561)Termination phase: Saturation
% 6.25/1.63 % (3422561)Time elapsed: 0.023 s
% 6.25/1.63 % (3422561)Peak memory usage: 90 MB
% 6.25/1.63 % (3422561)Instructions burned: 27 (million)
% 6.25/1.63 % (3422531)Instruction limit reached!
% 6.25/1.63 % (3422531)------------------------------
% 6.25/1.63 % (3422531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422531)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422531)Termination reason: Instruction limit
% 6.25/1.63 % (3422531)Termination phase: Saturation
% 6.25/1.63 % (3422531)Time elapsed: 0.339 s
% 6.25/1.63 % (3422531)Peak memory usage: 117 MB
% 6.25/1.63 % (3422531)Instructions burned: 307 (million)
% 6.25/1.63 % (3422569)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1699479393:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 6.25/1.63 % (3422569)Instruction limit reached!
% 6.25/1.63 % (3422569)------------------------------
% 6.25/1.63 % (3422569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422569)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422569)Termination reason: Instruction limit
% 6.25/1.63 % (3422569)Termination phase: Property scanning
% 6.25/1.63 % (3422569)Time elapsed: 0.002 s
% 6.25/1.63 % (3422569)Peak memory usage: 85 MB
% 6.25/1.63 % (3422569)Instructions burned: 2 (million)
% 6.25/1.63 % (3422578)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4260266952:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 6.25/1.63 % (3422573)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2737134488:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 6.25/1.63 % (3422580)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=427185071:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 6.25/1.63 % (3422574)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4252036360:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 6.25/1.63 % (3422580)Instruction limit reached!
% 6.25/1.63 % (3422580)------------------------------
% 6.25/1.63 % (3422580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422580)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422580)Termination reason: Instruction limit
% 6.25/1.63 % (3422580)Termination phase: Property scanning
% 6.25/1.63 % (3422580)Time elapsed: 0.009 s
% 6.25/1.63 % (3422580)Peak memory usage: 86 MB
% 6.25/1.63 % (3422580)Instructions burned: 9 (million)
% 6.25/1.63 % (3422574)Instruction limit reached!
% 6.25/1.63 % (3422574)------------------------------
% 6.25/1.63 % (3422574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422574)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422574)Termination reason: Instruction limit
% 6.25/1.63 % (3422574)Termination phase: Preprocessing 3
% 6.25/1.63 % (3422574)Time elapsed: 0.004 s
% 6.25/1.63 % (3422574)Peak memory usage: 86 MB
% 6.25/1.63 % (3422574)Instructions burned: 4 (million)
% 6.25/1.63 % (3422578)Instruction limit reached!
% 6.25/1.63 % (3422578)------------------------------
% 6.25/1.63 % (3422578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422578)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422578)Termination reason: Instruction limit
% 6.25/1.63 % (3422578)Termination phase: Saturation
% 6.25/1.63 % (3422578)Time elapsed: 0.066 s
% 6.25/1.63 % (3422578)Peak memory usage: 134 MB
% 6.25/1.63 % (3422578)Instructions burned: 66 (million)
% 6.25/1.63 % (3422579)lrs+10_1_thi=all:si=on:fd=off:random_seed=3076118315:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 6.25/1.63 % (3422573)First to succeed.
% 6.25/1.63 % (3422573)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3422504"
% 6.25/1.63 % (3422584)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2843465360:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 6.25/1.63 % (3422584)Instruction limit reached!
% 6.25/1.63 % (3422584)------------------------------
% 6.25/1.63 % (3422584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422584)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422584)Termination reason: Instruction limit
% 6.25/1.63 % (3422584)Termination phase: SInE selection
% 6.25/1.63 % (3422584)Time elapsed: 0.002 s
% 6.25/1.63 % (3422584)Peak memory usage: 85 MB
% 6.25/1.63 % (3422584)Instructions burned: 2 (million)
% 6.25/1.63 % (3422579)Instruction limit reached!
% 6.25/1.63 % (3422579)------------------------------
% 6.25/1.63 % (3422579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422579)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422579)Termination reason: Instruction limit
% 6.25/1.63 % (3422579)Termination phase: Saturation
% 6.25/1.63 % (3422579)Time elapsed: 0.091 s
% 6.25/1.63 % (3422579)Peak memory usage: 116 MB
% 6.25/1.63 % (3422579)Instructions burned: 53 (million)
% 6.25/1.63 % (3422588)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3533464856:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 6.25/1.63 % (3422588)Instruction limit reached!
% 6.25/1.63 % (3422588)------------------------------
% 6.25/1.63 % (3422588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.63 % (3422588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.63 % (3422588)CaDiCaL version: 2.1.3
% 6.25/1.63 % (3422588)Termination reason: Instruction limit
% 6.25/1.63 % (3422588)Termination phase: Preprocessing 1
% 6.25/1.63 % (3422588)Time elapsed: 0.002 s
% 6.25/1.63 % (3422588)Peak memory usage: 86 MB
% 6.25/1.63 % (3422588)Instructions burned: 3 (million)
% 6.25/1.63 % (3422599)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2112294953:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 6.25/1.64 % (3422593)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3269462646:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 6.25/1.64 % (3422594)dis+10_1_si=on:random_seed=2097914665:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 6.25/1.64 % (3422599)Refutation not found, incomplete strategy
% 6.25/1.64 % (3422599)------------------------------
% 6.25/1.64 % (3422599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422599)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422599)Termination reason: Refutation not found, incomplete strategy
% 6.25/1.64 % (3422599)Time elapsed: 0.021 s
% 6.25/1.64 % (3422599)Peak memory usage: 89 MB
% 6.25/1.64 % (3422599)Instructions burned: 18 (million)
% 6.25/1.64 % (3422594)Instruction limit reached!
% 6.25/1.64 % (3422594)------------------------------
% 6.25/1.64 % (3422594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422594)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422594)Termination reason: Instruction limit
% 6.25/1.64 % (3422594)Termination phase: Property scanning
% 6.25/1.64 % (3422594)Time elapsed: 0.011 s
% 6.25/1.64 % (3422594)Peak memory usage: 87 MB
% 6.25/1.64 % (3422594)Instructions burned: 11 (million)
% 6.25/1.64 % (3422601)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2955002539:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2992 on theBenchmark for (2992ds/35Mi)
% 6.25/1.64 % (3422601)Instruction limit reached!
% 6.25/1.64 % (3422601)------------------------------
% 6.25/1.64 % (3422601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422601)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422601)Termination reason: Instruction limit
% 6.25/1.64 % (3422601)Termination phase: Saturation
% 6.25/1.64 % (3422601)Time elapsed: 0.019 s
% 6.25/1.64 % (3422601)Peak memory usage: 89 MB
% 6.25/1.64 % (3422601)Instructions burned: 37 (million)
% 6.25/1.64 % (3422605)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1179374305:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 6.25/1.64 % (3422605)Instruction limit reached!
% 6.25/1.64 % (3422605)------------------------------
% 6.25/1.64 % (3422605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422605)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422605)Termination reason: Instruction limit
% 6.25/1.64 % (3422605)Termination phase: Preprocessing 1
% 6.25/1.64 % (3422605)Time elapsed: 0.003 s
% 6.25/1.64 % (3422605)Peak memory usage: 86 MB
% 6.25/1.64 % (3422605)Instructions burned: 3 (million)
% 6.25/1.64 % (3422607)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2536782087:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 6.25/1.64 % (3422593)Instruction limit reached!
% 6.25/1.64 % (3422593)------------------------------
% 6.25/1.64 % (3422593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422593)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422593)Termination reason: Instruction limit
% 6.25/1.64 % (3422593)Termination phase: Saturation
% 6.25/1.64 % (3422593)Time elapsed: 0.163 s
% 6.25/1.64 % (3422593)Peak memory usage: 117 MB
% 6.25/1.64 % (3422593)Instructions burned: 127 (million)
% 6.25/1.64 % (3422607)Instruction limit reached!
% 6.25/1.64 % (3422607)------------------------------
% 6.25/1.64 % (3422607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422607)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422607)Termination reason: Instruction limit
% 6.25/1.64 % (3422607)Termination phase: Property scanning
% 6.25/1.64 % (3422607)Time elapsed: 0.009 s
% 6.25/1.64 % (3422607)Peak memory usage: 87 MB
% 6.25/1.64 % (3422607)Instructions burned: 8 (million)
% 6.25/1.64 % (3422616)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=381685761:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 6.25/1.64 % (3422616)Instruction limit reached!
% 6.25/1.64 % (3422616)------------------------------
% 6.25/1.64 % (3422616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.64 % (3422616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.64 % (3422616)CaDiCaL version: 2.1.3
% 6.25/1.64 % (3422616)Termination reason: Instruction limit
% 6.25/1.64 % (3422616)Termination phase: Saturation
% 6.25/1.64 % (3422616)Time elapsed: 0.015 s
% 6.25/1.64 % (3422616)Peak memory usage: 97 MB
% 6.25/1.64 % (3422616)Instructions burned: 13 (million)
% 6.25/1.64 % (3422573)Refutation found. Thanks to Tanya!
% 6.25/1.64 % SZS status Theorem for theBenchmark
% 6.25/1.64 % SZS output start Proof for theBenchmark
% See solution above
% 8.12/1.89 % (3422573)------------------------------
% 8.12/1.89 % (3422573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.12/1.89 % (3422573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.12/1.89 % (3422573)CaDiCaL version: 2.1.3
% 8.12/1.89 % (3422573)Termination reason: Refutation
% 8.12/1.89 % (3422573)Time elapsed: 0.056 s
% 8.12/1.89 % (3422573)Peak memory usage: 91 MB
% 8.12/1.89 % (3422573)Instructions burned: 49 (million)
% 8.12/1.89 % (3422573)------------------------------
% 8.12/1.89 % (3422573)------------------------------
% 8.12/1.89 % (3422504)Success in time 1.091 s
% 8.12/1.89 % Vampire exiting
%------------------------------------------------------------------------------