%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW618_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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:57 PM UTC 2026
% Result : Theorem 3.23s 1.19s
% Output : Refutation 4.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 51
% Syntax : Number of formulae : 169 ( 66 unt; 0 typ; 38 def)
% Number of atoms : 323 ( 136 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 278 ( 124 ~; 115 |; 6 &)
% ( 23 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 8 ( 0 atm; 0 fun; 0 num; 8 var)
% Number of types : 14 ( 12 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 31 ( 29 usr; 24 prp; 0-2 aty)
% Number of functors : 86 ( 86 usr; 30 con; 0-5 aty)
% Number of variables : 120 ( 114 !; 6 ?; 120 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
set1: $tType ).
tff(type_def_10,type,
map_int_lpmap_int_intrp: $tType ).
tff(type_def_11,type,
map_int_int: $tType ).
tff(type_def_12,type,
lpintcm_setrp: $tType ).
tff(type_def_13,type,
lpintcm_map_int_intrp: $tType ).
tff(type_def_14,type,
t18_lpintcm_setrp_lpintcm_map_int_intrp: $tType ).
tff(type_def_15,type,
option_lpintcm_map_int_intrp: $tType ).
tff(type_def_16,type,
map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
min: ( $int * $int ) > $int ).
tff(func_def_13,type,
max: ( $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,
ref: ty > ty ).
tff(func_def_19,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_20,type,
contents: ( ty * uni ) > uni ).
tff(func_def_21,type,
n: $int ).
tff(func_def_22,type,
size: $int ).
tff(func_def_23,type,
set2: ty ).
tff(func_def_24,type,
remove: ( $int * set1 ) > set1 ).
tff(func_def_25,type,
below: $int > set1 ).
tff(func_def_26,type,
cardinal: set1 > $int ).
tff(func_def_29,type,
m: map_int_lpmap_int_intrp ).
tff(func_def_30,type,
t2tb: map_int_int > uni ).
tff(func_def_31,type,
tb2t: uni > map_int_int ).
tff(func_def_32,type,
t2tb1: map_int_lpmap_int_intrp > uni ).
tff(func_def_33,type,
tb2t1: uni > map_int_lpmap_int_intrp ).
tff(func_def_34,type,
t2tb2: $int > uni ).
tff(func_def_35,type,
tb2t2: uni > $int ).
tff(func_def_36,type,
f: ( map_int_int * $int ) > $int ).
tff(func_def_37,type,
sum: ( map_int_int * $int * $int ) > $int ).
tff(func_def_39,type,
option: ty > ty ).
tff(func_def_40,type,
none: ty > uni ).
tff(func_def_41,type,
some: ( ty * uni ) > uni ).
tff(func_def_42,type,
match_option: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_43,type,
some_proj_1: ( ty * uni ) > uni ).
tff(func_def_44,type,
t: ( ty * ty ) > ty ).
tff(func_def_45,type,
mk_t: ( ty * ty * uni ) > uni ).
tff(func_def_46,type,
contents1: ( ty * ty * uni ) > uni ).
tff(func_def_47,type,
mixfix_lbrb: ( ty * ty * uni * uni ) > uni ).
tff(func_def_48,type,
tuple2: ( ty * ty ) > ty ).
tff(func_def_49,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(func_def_50,type,
tuple2_proj_1: ( ty * ty * uni ) > uni ).
tff(func_def_51,type,
tuple2_proj_2: ( ty * ty * uni ) > uni ).
tff(func_def_52,type,
t2tb3: lpintcm_setrp > uni ).
tff(func_def_53,type,
tb2t3: uni > lpintcm_setrp ).
tff(func_def_54,type,
t2tb4: set1 > uni ).
tff(func_def_55,type,
tb2t4: uni > set1 ).
tff(func_def_56,type,
t2tb5: lpintcm_map_int_intrp > uni ).
tff(func_def_57,type,
tb2t5: uni > lpintcm_map_int_intrp ).
tff(func_def_58,type,
t2tb6: option_lpintcm_map_int_intrp > uni ).
tff(func_def_59,type,
tb2t6: uni > option_lpintcm_map_int_intrp ).
tff(func_def_60,type,
t2tb7: t18_lpintcm_setrp_lpintcm_map_int_intrp > uni ).
tff(func_def_61,type,
tb2t7: uni > t18_lpintcm_setrp_lpintcm_map_int_intrp ).
tff(func_def_62,type,
t2tb8: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp > uni ).
tff(func_def_63,type,
tb2t8: uni > map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp ).
tff(func_def_65,type,
sK0: set1 > $int ).
tff(func_def_66,type,
sK1: set1 > $int ).
tff(func_def_67,type,
sK2: ( $int * $int * map_int_int * map_int_int ) > $int ).
tff(func_def_68,type,
sK3: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp ).
tff(func_def_69,type,
sK4: lpintcm_setrp ).
tff(func_def_70,type,
sK5: lpintcm_map_int_intrp ).
tff(func_def_71,type,
sK6: ( $int * map_int_int ) > $int ).
tff(func_def_72,type,
sK7: ( $int * map_int_int ) > $int ).
tff(func_def_73,type,
sK8: ( $int * map_int_int ) > $int ).
tff(func_def_74,type,
sK9: ( set1 * $int * $int ) > map_int_int ).
tff(func_def_75,type,
sK10: ( set1 * $int * map_int_int ) > $int ).
tff(func_def_76,type,
sK11: ( set1 * $int * map_int_int ) > $int ).
tff(func_def_77,type,
sF12: ty ).
tff(func_def_78,type,
sF13: ty ).
tff(func_def_79,type,
sF14: ty ).
tff(func_def_80,type,
sF15: ty ).
tff(func_def_81,type,
sF16: uni ).
tff(func_def_82,type,
sF17: uni ).
tff(func_def_83,type,
sF18: uni ).
tff(func_def_84,type,
sF19: uni ).
tff(func_def_85,type,
sF20: uni ).
tff(func_def_86,type,
sF21: option_lpintcm_map_int_intrp ).
tff(func_def_87,type,
sF22: uni ).
tff(func_def_88,type,
sF23: uni ).
tff(func_def_89,type,
sF24: option_lpintcm_map_int_intrp ).
tff(func_def_90,type,
sF25: uni ).
tff(func_def_91,type,
sF26: option_lpintcm_map_int_intrp ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( $int * set1 ) > $o ).
tff(pred_def_5,type,
solution: ( map_int_int * $int ) > $o ).
tff(pred_def_6,type,
pre: lpintcm_setrp > $o ).
tff(pred_def_7,type,
post: ( lpintcm_setrp * lpintcm_map_int_intrp ) > $o ).
tff(pred_def_8,type,
inv: t18_lpintcm_setrp_lpintcm_map_int_intrp > $o ).
tff(f44,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2) ).
tff(f59,axiom,
! [X0: ty,X1: uni] : ( none(X0) != some(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',none_Some) ).
tff(f65,axiom,
! [X0: ty,X2: uni,X1: ty] :
( sort(map(X0,option(X1)),X2)
=> ( contents1(X1,X0,mk_t(X1,X0,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',contents_def1) ).
tff(f68,axiom,
! [X3: uni,X2: uni,X0: ty,X1: ty] : ( mixfix_lbrb(X1,X0,X2,X3) = get(option(X1),X0,contents1(X1,X0,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mixfix_lbrb_def) ).
tff(f72,axiom,
! [X1: ty,X2: uni,X0: ty] : sort(X0,tuple2_proj_2(X1,X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuple2_proj_2_sort) ).
tff(f74,axiom,
! [X1: ty,X0: ty,X2: uni] :
( sort(tuple2(X1,X0),X2)
=> ( X2 = tuple21(X1,X0,tuple2_proj_1(X1,X0,X2),tuple2_proj_2(X1,X0,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuple2_inversion) ).
tff(f75,axiom,
! [X0: lpintcm_setrp] : sort(tuple2(int,set2),t2tb3(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort3) ).
tff(f77,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f80,axiom,
! [X0: uni] :
( sort(set2,X0)
=> ( t2tb4(tb2t4(X0)) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR4) ).
tff(f88,axiom,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR6) ).
tff(f93,axiom,
! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] : sort(map(tuple2(int,set2),option(tuple2(int,map(int,int)))),t2tb8(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort8) ).
tff(f95,axiom,
! [X0: uni] : ( t2tb8(tb2t8(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR8) ).
tff(f96,conjecture,
! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ! [X2: set1,X1: $int] : ( tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(X0),tuple21(int,set2,t2tb2(X1),t2tb4(X2)))) = tb2t6(none(tuple2(int,map(int,int)))) )
=> ! [X3: lpintcm_map_int_intrp,X1: lpintcm_setrp] :
( ( tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X1))) = tb2t6(some(tuple2(int,map(int,int)),t2tb5(X3))) )
=> post(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_maxmat) ).
tff(f97,negated_conjecture,
~ ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ! [X2: set1,X1: $int] : ( tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(X0),tuple21(int,set2,t2tb2(X1),t2tb4(X2)))) = tb2t6(none(tuple2(int,map(int,int)))) )
=> ! [X3: lpintcm_map_int_intrp,X1: lpintcm_setrp] :
( ( tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X1))) = tb2t6(some(tuple2(int,map(int,int)),t2tb5(X3))) )
=> post(X1,X3) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
tff(f132,plain,
! [X2: ty,X0: uni,X3: ty,X1: uni] : ( mixfix_lbrb(X3,X2,X1,X0) = get(option(X3),X2,contents1(X3,X2,X1),X0) ),
inference(rectify,[],[f68]) ).
tff(f137,plain,
! [X0: ty,X1: uni,X2: ty] : sort(X2,tuple2_proj_2(X0,X2,X1)),
inference(rectify,[],[f72]) ).
tff(f144,plain,
~ ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ! [X2: $int,X1: set1] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(X0),tuple21(int,set2,t2tb2(X2),t2tb4(X1)))) )
=> ! [X4: lpintcm_setrp,X3: lpintcm_map_int_intrp] :
( ( tb2t6(some(tuple2(int,map(int,int)),t2tb5(X3))) = tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X4))) )
=> post(X4,X3) ) ),
inference(rectify,[],[f97]) ).
tff(f150,plain,
! [X2: ty,X1: uni,X0: ty] :
( sort(map(X0,option(X2)),X1)
=> ( contents1(X2,X0,mk_t(X2,X0,X1)) = X1 ) ),
inference(rectify,[],[f65]) ).
tff(f167,plain,
? [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ? [X4: lpintcm_setrp,X3: lpintcm_map_int_intrp] :
( ~ post(X4,X3)
& ( tb2t6(some(tuple2(int,map(int,int)),t2tb5(X3))) = tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X4))) ) )
& ! [X2: $int,X1: set1] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(X0),tuple21(int,set2,t2tb2(X2),t2tb4(X1)))) ) ),
inference(ennf_transformation,[],[f144]) ).
tff(f168,plain,
! [X1: ty,X2: uni,X0: ty] :
( ~ sort(tuple2(X1,X0),X2)
| ( X2 = tuple21(X1,X0,tuple2_proj_1(X1,X0,X2),tuple2_proj_2(X1,X0,X2)) ) ),
inference(ennf_transformation,[],[f74]) ).
tff(f169,plain,
! [X2: ty,X0: ty,X1: uni] :
( ( contents1(X2,X0,mk_t(X2,X0,X1)) = X1 )
| ~ sort(map(X0,option(X2)),X1) ),
inference(ennf_transformation,[],[f150]) ).
tff(f172,plain,
! [X0: uni] :
( ( t2tb4(tb2t4(X0)) = X0 )
| ~ sort(set2,X0) ),
inference(ennf_transformation,[],[f80]) ).
tff(f219,plain,
! [X0: ty,X1: uni,X2: ty,X3: uni] : ( get(option(X2),X0,contents1(X2,X0,X3),X1) = mixfix_lbrb(X2,X0,X3,X1) ),
inference(rectify,[],[f132]) ).
tff(f229,plain,
! [X0: ty,X1: uni,X2: ty] :
( ~ sort(tuple2(X0,X2),X1)
| ( tuple21(X0,X2,tuple2_proj_1(X0,X2,X1),tuple2_proj_2(X0,X2,X1)) = X1 ) ),
inference(rectify,[],[f168]) ).
tff(f230,plain,
? [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ? [X1: lpintcm_setrp,X2: lpintcm_map_int_intrp] :
( ~ post(X1,X2)
& ( tb2t6(some(tuple2(int,map(int,int)),t2tb5(X2))) = tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X1))) ) )
& ! [X3: $int,X4: set1] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(X0),tuple21(int,set2,t2tb2(X3),t2tb4(X4)))) ) ),
inference(rectify,[],[f167]) ).
tff(f231,plain,
( ~ post(sK4,sK5)
& ( tb2t6(some(tuple2(int,map(int,int)),t2tb5(sK5))) = tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(sK3)),t2tb3(sK4))) )
& ! [X3: $int,X4: set1] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK3),tuple21(int,set2,t2tb2(X3),t2tb4(X4)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f230]) ).
tff(f234,plain,
! [X0: ty,X1: ty,X2: uni] :
( ( contents1(X0,X1,mk_t(X0,X1,X2)) = X2 )
| ~ sort(map(X1,option(X0)),X2) ),
inference(rectify,[],[f169]) ).
tff(f289,plain,
! [X2: ty,X3: uni,X0: ty,X1: uni] : ( get(option(X2),X0,contents1(X2,X0,X3),X1) = mixfix_lbrb(X2,X0,X3,X1) ),
inference(cnf_transformation,[],[f219]) ).
tff(f304,plain,
! [X2: ty,X0: ty,X1: uni] :
( ( tuple21(X0,X2,tuple2_proj_1(X0,X2,X1),tuple2_proj_2(X0,X2,X1)) = X1 )
| ~ sort(tuple2(X0,X2),X1) ),
inference(cnf_transformation,[],[f229]) ).
tff(f309,plain,
! [X3: $int,X4: set1] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK3),tuple21(int,set2,t2tb2(X3),t2tb4(X4)))) ),
inference(cnf_transformation,[],[f231]) ).
tff(f310,plain,
tb2t6(some(tuple2(int,map(int,int)),t2tb5(sK5))) = tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(sK3)),t2tb3(sK4))),
inference(cnf_transformation,[],[f231]) ).
tff(f314,plain,
! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] : sort(map(tuple2(int,set2),option(tuple2(int,map(int,int)))),t2tb8(X0)),
inference(cnf_transformation,[],[f93]) ).
tff(f317,plain,
! [X2: uni,X0: ty,X1: ty] :
( ( contents1(X0,X1,mk_t(X0,X1,X2)) = X2 )
| ~ sort(map(X1,option(X0)),X2) ),
inference(cnf_transformation,[],[f234]) ).
tff(f318,plain,
! [X0: ty,X1: uni] : ( none(X0) != some(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tff(f334,plain,
! [X0: uni] : ( t2tb8(tb2t8(X0)) = X0 ),
inference(cnf_transformation,[],[f95]) ).
tff(f347,plain,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
inference(cnf_transformation,[],[f88]) ).
tff(f348,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f44]) ).
tff(f372,plain,
! [X2: ty,X0: ty,X1: uni] : sort(X2,tuple2_proj_2(X0,X2,X1)),
inference(cnf_transformation,[],[f137]) ).
tff(f376,plain,
! [X0: uni] :
( ( t2tb4(tb2t4(X0)) = X0 )
| ~ sort(set2,X0) ),
inference(cnf_transformation,[],[f172]) ).
tff(f385,plain,
! [X0: lpintcm_setrp] : sort(tuple2(int,set2),t2tb3(X0)),
inference(cnf_transformation,[],[f75]) ).
tff(f413,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f77]) ).
tff(f422,plain,
tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),contents1(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(sK3))),t2tb3(sK4))) = tb2t6(some(tuple2(int,map(int,int)),t2tb5(sK5))),
inference(definition_unfolding,[],[f310,f289]) ).
tff(f436,definition,
sF12 = map(int,int),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f437,plain,
map(int,int) = sF12,
inference(reorient_equations,[],[f436]) ).
tff(f438,definition,
sF13 = tuple2(int,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f439,definition,
sF14 = option(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f440,definition,
sF15 = tuple2(int,set2),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f441,plain,
tuple2(int,set2) = sF15,
inference(reorient_equations,[],[f440]) ).
tff(f442,definition,
sF16 = t2tb8(sK3),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f443,definition,
sF17 = mk_t(sF13,sF15,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f444,plain,
mk_t(sF13,sF15,sF16) = sF17,
inference(reorient_equations,[],[f443]) ).
tff(f445,definition,
sF18 = contents1(sF13,sF15,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f446,plain,
contents1(sF13,sF15,sF17) = sF18,
inference(reorient_equations,[],[f445]) ).
tff(f447,definition,
sF19 = t2tb3(sK4),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f448,plain,
t2tb3(sK4) = sF19,
inference(reorient_equations,[],[f447]) ).
tff(f449,definition,
sF20 = get(sF14,sF15,sF18,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f450,definition,
sF21 = tb2t6(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f451,plain,
tb2t6(sF20) = sF21,
inference(reorient_equations,[],[f450]) ).
tff(f452,definition,
sF22 = t2tb5(sK5),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f453,plain,
t2tb5(sK5) = sF22,
inference(reorient_equations,[],[f452]) ).
tff(f454,definition,
sF23 = some(sF13,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f455,plain,
some(sF13,sF22) = sF23,
inference(reorient_equations,[],[f454]) ).
tff(f456,definition,
sF24 = tb2t6(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f457,plain,
tb2t6(sF23) = sF24,
inference(reorient_equations,[],[f456]) ).
tff(f458,plain,
sF24 = sF21,
inference(definition_folding,[],[f422,f457,f455,f453,f438,f437,f451,f449,f448,f446,f444,f442,f441,f438,f437,f441,f438,f437,f441,f439,f438,f437]) ).
tff(f459,definition,
sF25 = none(sF13),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f460,definition,
sF26 = tb2t6(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f461,plain,
! [X3: $int,X4: set1] : ( sF26 = tb2t6(get(sF14,sF15,sF16,tuple21(int,set2,t2tb2(X3),t2tb4(X4)))) ),
inference(definition_folding,[],[f309,f442,f441,f439,f438,f437,f460,f459,f438,f437]) ).
tff(f480,definition,
( spl27_4
<=> ( sF26 = tb2t6(sF25) ) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
tff(f482,plain,
( ( sF26 = tb2t6(sF25) )
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f480]) ).
tff(f483,plain,
spl27_4,
inference(avatar_split_clause,[],[f460,f480]) ).
tff(f485,definition,
( spl27_5
<=> ( tb2t6(sF20) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
tff(f487,plain,
( ( tb2t6(sF20) = sF21 )
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f485]) ).
tff(f488,plain,
spl27_5,
inference(avatar_split_clause,[],[f451,f485]) ).
tff(f490,definition,
( spl27_6
<=> ( mk_t(sF13,sF15,sF16) = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition]) ).
tff(f492,plain,
( ( mk_t(sF13,sF15,sF16) = sF17 )
| ~ spl27_6 ),
inference(avatar_component_clause,[],[f490]) ).
tff(f493,plain,
spl27_6,
inference(avatar_split_clause,[],[f444,f490]) ).
tff(f495,definition,
( spl27_7
<=> ( sF24 = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
tff(f497,plain,
( ( sF24 = sF21 )
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f495]) ).
tff(f498,plain,
spl27_7,
inference(avatar_split_clause,[],[f458,f495]) ).
tff(f500,definition,
( spl27_8
<=> ( map(int,int) = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition]) ).
tff(f502,plain,
( ( map(int,int) = sF12 )
| ~ spl27_8 ),
inference(avatar_component_clause,[],[f500]) ).
tff(f503,plain,
spl27_8,
inference(avatar_split_clause,[],[f437,f500]) ).
tff(f515,definition,
( spl27_11
<=> ( sF25 = none(sF13) ) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
tff(f517,plain,
( ( sF25 = none(sF13) )
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f515]) ).
tff(f518,plain,
spl27_11,
inference(avatar_split_clause,[],[f459,f515]) ).
tff(f520,definition,
( spl27_12
<=> ( sF14 = option(sF13) ) ),
introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition]) ).
tff(f522,plain,
( ( sF14 = option(sF13) )
| ~ spl27_12 ),
inference(avatar_component_clause,[],[f520]) ).
tff(f523,plain,
spl27_12,
inference(avatar_split_clause,[],[f439,f520]) ).
tff(f525,definition,
( spl27_13
<=> ( sF20 = get(sF14,sF15,sF18,sF19) ) ),
introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition]) ).
tff(f527,plain,
( ( sF20 = get(sF14,sF15,sF18,sF19) )
| ~ spl27_13 ),
inference(avatar_component_clause,[],[f525]) ).
tff(f528,plain,
spl27_13,
inference(avatar_split_clause,[],[f449,f525]) ).
tff(f530,definition,
( spl27_14
<=> ( tuple2(int,set2) = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition]) ).
tff(f532,plain,
( ( tuple2(int,set2) = sF15 )
| ~ spl27_14 ),
inference(avatar_component_clause,[],[f530]) ).
tff(f533,plain,
spl27_14,
inference(avatar_split_clause,[],[f441,f530]) ).
tff(f545,definition,
( spl27_17
<=> ( some(sF13,sF22) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl27_17])],[avatar_definition]) ).
tff(f547,plain,
( ( some(sF13,sF22) = sF23 )
| ~ spl27_17 ),
inference(avatar_component_clause,[],[f545]) ).
tff(f548,plain,
spl27_17,
inference(avatar_split_clause,[],[f455,f545]) ).
tff(f550,definition,
( spl27_18
<=> ( sF13 = tuple2(int,sF12) ) ),
introduced(definition,[new_symbols(definition,[spl27_18])],[avatar_definition]) ).
tff(f552,plain,
( ( sF13 = tuple2(int,sF12) )
| ~ spl27_18 ),
inference(avatar_component_clause,[],[f550]) ).
tff(f553,plain,
spl27_18,
inference(avatar_split_clause,[],[f438,f550]) ).
tff(f555,definition,
( spl27_19
<=> ( contents1(sF13,sF15,sF17) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl27_19])],[avatar_definition]) ).
tff(f557,plain,
( ( contents1(sF13,sF15,sF17) = sF18 )
| ~ spl27_19 ),
inference(avatar_component_clause,[],[f555]) ).
tff(f558,plain,
spl27_19,
inference(avatar_split_clause,[],[f446,f555]) ).
tff(f560,definition,
( spl27_20
<=> ( tb2t6(sF23) = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl27_20])],[avatar_definition]) ).
tff(f562,plain,
( ( tb2t6(sF23) = sF24 )
| ~ spl27_20 ),
inference(avatar_component_clause,[],[f560]) ).
tff(f563,plain,
spl27_20,
inference(avatar_split_clause,[],[f457,f560]) ).
tff(f567,plain,
( ( tb2t6(sF20) = sF24 )
| ~ spl27_5
| ~ spl27_7 ),
inference(forward_demodulation,[],[f487,f497]) ).
tff(f569,definition,
( spl27_21
<=> ( tb2t6(sF20) = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl27_21])],[avatar_definition]) ).
tff(f571,plain,
( ( tb2t6(sF20) = sF24 )
| ~ spl27_21 ),
inference(avatar_component_clause,[],[f569]) ).
tff(f572,plain,
( spl27_21
| ~ spl27_5
| ~ spl27_7 ),
inference(avatar_split_clause,[],[f567,f495,f485,f569]) ).
tff(f593,plain,
( ( t2tb6(sF24) = sF20 )
| ~ spl27_21 ),
inference(superposition,[],[f347,f571]) ).
tff(f594,plain,
( ( t2tb6(sF24) = sF23 )
| ~ spl27_20 ),
inference(superposition,[],[f347,f562]) ).
tff(f595,plain,
( ( t2tb6(sF26) = sF25 )
| ~ spl27_4 ),
inference(superposition,[],[f347,f482]) ).
tff(f597,definition,
( spl27_25
<=> ( t2tb6(sF24) = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl27_25])],[avatar_definition]) ).
tff(f599,plain,
( ( t2tb6(sF24) = sF20 )
| ~ spl27_25 ),
inference(avatar_component_clause,[],[f597]) ).
tff(f600,plain,
( spl27_25
| ~ spl27_21 ),
inference(avatar_split_clause,[],[f593,f569,f597]) ).
tff(f602,definition,
( spl27_26
<=> ( t2tb6(sF24) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl27_26])],[avatar_definition]) ).
tff(f604,plain,
( ( t2tb6(sF24) = sF23 )
| ~ spl27_26 ),
inference(avatar_component_clause,[],[f602]) ).
tff(f605,plain,
( spl27_26
| ~ spl27_20 ),
inference(avatar_split_clause,[],[f594,f560,f602]) ).
tff(f607,definition,
( spl27_27
<=> ( t2tb6(sF26) = sF25 ) ),
introduced(definition,[new_symbols(definition,[spl27_27])],[avatar_definition]) ).
tff(f609,plain,
( ( t2tb6(sF26) = sF25 )
| ~ spl27_27 ),
inference(avatar_component_clause,[],[f607]) ).
tff(f610,plain,
( spl27_27
| ~ spl27_4 ),
inference(avatar_split_clause,[],[f595,f480,f607]) ).
tff(f613,plain,
! [X0: uni,X1: set1] : ( sF26 = tb2t6(get(sF14,sF15,sF16,tuple21(int,set2,X0,t2tb4(X1)))) ),
inference(superposition,[],[f461,f348]) ).
tff(f614,plain,
! [X0: uni,X1: set1] : ( t2tb6(sF26) = get(sF14,sF15,sF16,tuple21(int,set2,X0,t2tb4(X1))) ),
inference(superposition,[],[f347,f613]) ).
tff(f627,plain,
( ( sF20 = sF23 )
| ~ spl27_25
| ~ spl27_26 ),
inference(forward_demodulation,[],[f604,f599]) ).
tff(f629,definition,
( spl27_29
<=> ( sF20 = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl27_29])],[avatar_definition]) ).
tff(f631,plain,
( ( sF20 = sF23 )
| ~ spl27_29 ),
inference(avatar_component_clause,[],[f629]) ).
tff(f632,plain,
( spl27_29
| ~ spl27_25
| ~ spl27_26 ),
inference(avatar_split_clause,[],[f627,f602,f597,f629]) ).
tff(f636,plain,
( ( some(sF13,sF22) = sF20 )
| ~ spl27_17
| ~ spl27_29 ),
inference(forward_demodulation,[],[f547,f631]) ).
tff(f638,definition,
( spl27_30
<=> ( some(sF13,sF22) = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl27_30])],[avatar_definition]) ).
tff(f640,plain,
( ( some(sF13,sF22) = sF20 )
| ~ spl27_30 ),
inference(avatar_component_clause,[],[f638]) ).
tff(f641,plain,
( spl27_30
| ~ spl27_17
| ~ spl27_29 ),
inference(avatar_split_clause,[],[f636,f629,f545,f638]) ).
tff(f642,plain,
( ( tuple2(int,map(int,int)) = sF13 )
| ~ spl27_8
| ~ spl27_18 ),
inference(forward_demodulation,[],[f552,f502]) ).
tff(f644,definition,
( spl27_31
<=> ( tuple2(int,map(int,int)) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl27_31])],[avatar_definition]) ).
tff(f646,plain,
( ( tuple2(int,map(int,int)) = sF13 )
| ~ spl27_31 ),
inference(avatar_component_clause,[],[f644]) ).
tff(f647,plain,
( spl27_31
| ~ spl27_8
| ~ spl27_18 ),
inference(avatar_split_clause,[],[f642,f550,f500,f644]) ).
tff(f651,plain,
( ( sF20 != none(sF13) )
| ~ spl27_30 ),
inference(superposition,[],[f318,f640]) ).
tff(f652,plain,
( ( sF25 != sF20 )
| ~ spl27_11
| ~ spl27_30 ),
inference(forward_demodulation,[],[f651,f517]) ).
tff(f654,definition,
( spl27_32
<=> ( sF25 = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl27_32])],[avatar_definition]) ).
tff(f656,plain,
( ( sF25 != sF20 )
| spl27_32 ),
inference(avatar_component_clause,[],[f654]) ).
tff(f657,plain,
( ~ spl27_32
| ~ spl27_11
| ~ spl27_30 ),
inference(avatar_split_clause,[],[f652,f638,f515,f654]) ).
tff(f668,plain,
( ! [X0: lpintcm_setrp] : sort(sF15,t2tb3(X0))
| ~ spl27_14 ),
inference(forward_demodulation,[],[f385,f532]) ).
tff(f670,plain,
( ! [X0: uni] : sort(sF15,X0)
| ~ spl27_14 ),
inference(superposition,[],[f668,f413]) ).
tff(f718,plain,
! [X0: uni,X1: uni] :
( ( t2tb6(sF26) = get(sF14,sF15,sF16,tuple21(int,set2,X1,X0)) )
| ~ sort(set2,X0) ),
inference(superposition,[],[f614,f376]) ).
tff(f722,plain,
( ! [X0: uni,X1: uni] :
( ( sF25 = get(sF14,sF15,sF16,tuple21(int,set2,X1,X0)) )
| ~ sort(set2,X0) )
| ~ spl27_27 ),
inference(forward_demodulation,[],[f718,f609]) ).
tff(f935,plain,
( ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] : sort(map(tuple2(int,set2),option(sF13)),t2tb8(X0))
| ~ spl27_31 ),
inference(forward_demodulation,[],[f314,f646]) ).
tff(f936,plain,
( ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] : sort(map(tuple2(int,set2),sF14),t2tb8(X0))
| ~ spl27_12
| ~ spl27_31 ),
inference(forward_demodulation,[],[f935,f522]) ).
tff(f937,plain,
( ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] : sort(map(sF15,sF14),t2tb8(X0))
| ~ spl27_12
| ~ spl27_14
| ~ spl27_31 ),
inference(forward_demodulation,[],[f936,f532]) ).
tff(f939,plain,
( ! [X0: uni] : sort(map(sF15,sF14),X0)
| ~ spl27_12
| ~ spl27_14
| ~ spl27_31 ),
inference(superposition,[],[f937,f334]) ).
tff(f1061,plain,
( ( contents1(sF13,sF15,sF17) = sF16 )
| ~ sort(map(sF15,option(sF13)),sF16)
| ~ spl27_6 ),
inference(superposition,[],[f317,f492]) ).
tff(f1065,plain,
( ~ sort(map(sF15,option(sF13)),sF16)
| ( sF18 = sF16 )
| ~ spl27_6
| ~ spl27_19 ),
inference(forward_demodulation,[],[f1061,f557]) ).
tff(f1067,plain,
( ~ sort(map(sF15,sF14),sF16)
| ( sF18 = sF16 )
| ~ spl27_6
| ~ spl27_12
| ~ spl27_19 ),
inference(forward_demodulation,[],[f1065,f522]) ).
tff(f1068,plain,
( ( sF18 = sF16 )
| ~ spl27_6
| ~ spl27_12
| ~ spl27_14
| ~ spl27_19
| ~ spl27_31 ),
inference(forward_subsumption_resolution,[],[f1067,f939]) ).
tff(f1070,definition,
( spl27_46
<=> ( sF18 = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl27_46])],[avatar_definition]) ).
tff(f1072,plain,
( ( sF18 = sF16 )
| ~ spl27_46 ),
inference(avatar_component_clause,[],[f1070]) ).
tff(f1073,plain,
( spl27_46
| ~ spl27_6
| ~ spl27_12
| ~ spl27_14
| ~ spl27_19
| ~ spl27_31 ),
inference(avatar_split_clause,[],[f1068,f644,f555,f530,f520,f490,f1070]) ).
tff(f1076,plain,
( ( sF20 = get(sF14,sF15,sF16,sF19) )
| ~ spl27_13
| ~ spl27_46 ),
inference(superposition,[],[f527,f1072]) ).
tff(f1078,definition,
( spl27_47
<=> ( sF20 = get(sF14,sF15,sF16,sF19) ) ),
introduced(definition,[new_symbols(definition,[spl27_47])],[avatar_definition]) ).
tff(f1080,plain,
( ( sF20 = get(sF14,sF15,sF16,sF19) )
| ~ spl27_47 ),
inference(avatar_component_clause,[],[f1078]) ).
tff(f1081,plain,
( spl27_47
| ~ spl27_13
| ~ spl27_46 ),
inference(avatar_split_clause,[],[f1076,f1070,f525,f1078]) ).
tff(f1157,plain,
( ! [X0: uni] :
( ( sF25 = get(sF14,sF15,sF16,X0) )
| ~ sort(set2,tuple2_proj_2(int,set2,X0))
| ~ sort(tuple2(int,set2),X0) )
| ~ spl27_27 ),
inference(superposition,[],[f722,f304]) ).
tff(f1159,plain,
( ! [X0: uni] :
( ( sF25 = get(sF14,sF15,sF16,X0) )
| ~ sort(tuple2(int,set2),X0) )
| ~ spl27_27 ),
inference(forward_subsumption_resolution,[],[f1157,f372]) ).
tff(f1163,plain,
( ! [X0: uni] :
( ~ sort(sF15,X0)
| ( sF25 = get(sF14,sF15,sF16,X0) ) )
| ~ spl27_14
| ~ spl27_27 ),
inference(forward_demodulation,[],[f1159,f532]) ).
tff(f1165,plain,
( ! [X0: uni] : ( sF25 = get(sF14,sF15,sF16,X0) )
| ~ spl27_14
| ~ spl27_27 ),
inference(forward_subsumption_resolution,[],[f1163,f670]) ).
tff(f1174,plain,
( ( sF25 = sF20 )
| ~ spl27_14
| ~ spl27_27
| ~ spl27_47 ),
inference(superposition,[],[f1080,f1165]) ).
tff(f1177,plain,
( $false
| ~ spl27_14
| ~ spl27_27
| spl27_32
| ~ spl27_47 ),
inference(forward_subsumption_resolution,[],[f1174,f656]) ).
tff(f1178,plain,
( ~ spl27_14
| ~ spl27_27
| spl27_32
| ~ spl27_47 ),
inference(avatar_contradiction_clause,[],[f1177]) ).
tff(f1179,plain,
$false,
inference(avatar_smt_refutation,[],[f1178,f1081,f1073,f657,f647,f641,f632,f610,f605,f600,f572,f563,f558,f553,f548,f533,f528,f523,f518,f503,f498,f493,f488,f483]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW618_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:27:49 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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.23/1.19 % (3658011)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.23/1.19 % (3658046)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1777129390:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.23/1.19 % (3658046)Instruction limit reached!
% 3.23/1.19 % (3658046)------------------------------
% 3.23/1.19 % (3658046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658046)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658046)Termination reason: Instruction limit
% 3.23/1.19 % (3658046)Termination phase: Saturation
% 3.23/1.19 % (3658046)Time elapsed: 0.027 s
% 3.23/1.19 % (3658046)Peak memory usage: 116 MB
% 3.23/1.19 % (3658046)Instructions burned: 33 (million)
% 3.23/1.19 % (3658045)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1843786588:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.23/1.19 % (3658042)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=847652461:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.23/1.19 % (3658044)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1827789395:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.23/1.19 % (3658040)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=139015303:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.23/1.19 % (3658043)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2615106707:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.23/1.19 % (3658041)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3814902253:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.23/1.19 % (3658044)Instruction limit reached!
% 3.23/1.19 % (3658044)------------------------------
% 3.23/1.19 % (3658044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658044)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658044)Termination reason: Instruction limit
% 3.23/1.19 % (3658044)Termination phase: Preprocessing 3
% 3.23/1.19 % (3658044)Time elapsed: 0.003 s
% 3.23/1.19 % (3658044)Peak memory usage: 86 MB
% 3.23/1.19 % (3658044)Instructions burned: 4 (million)
% 3.23/1.19 % (3658043)Instruction limit reached!
% 3.23/1.19 % (3658043)------------------------------
% 3.23/1.19 % (3658043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658043)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658043)Termination reason: Instruction limit
% 3.23/1.19 % (3658043)Termination phase: Saturation
% 3.23/1.19 % (3658043)Time elapsed: 0.005 s
% 3.23/1.19 % (3658043)Peak memory usage: 87 MB
% 3.23/1.19 % (3658043)Instructions burned: 9 (million)
% 3.23/1.19 % (3658040)Instruction limit reached!
% 3.23/1.19 % (3658040)------------------------------
% 3.23/1.19 % (3658040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658040)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658040)Termination reason: Instruction limit
% 3.23/1.19 % (3658040)Termination phase: Saturation
% 3.23/1.19 % (3658040)Time elapsed: 0.030 s
% 3.23/1.19 % (3658040)Peak memory usage: 115 MB
% 3.23/1.19 % (3658040)Instructions burned: 12 (million)
% 3.23/1.19 % (3658045)Instruction limit reached!
% 3.23/1.19 % (3658045)------------------------------
% 3.23/1.19 % (3658045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658045)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658045)Termination reason: Instruction limit
% 3.23/1.19 % (3658045)Termination phase: Saturation
% 3.23/1.19 % (3658045)Time elapsed: 0.054 s
% 3.23/1.19 % (3658045)Peak memory usage: 116 MB
% 3.23/1.19 % (3658045)Instructions burned: 46 (million)
% 3.23/1.19 % (3658041)First to succeed.
% 3.23/1.19 % (3658041)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3658011"
% 3.23/1.19 % (3658048)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3518087316:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.23/1.19 % (3658048)Instruction limit reached!
% 3.23/1.19 % (3658048)------------------------------
% 3.23/1.19 % (3658048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658048)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658048)Termination reason: Instruction limit
% 3.23/1.19 % (3658048)Termination phase: Saturation
% 3.23/1.19 % (3658048)Time elapsed: 0.006 s
% 3.23/1.19 % (3658048)Peak memory usage: 88 MB
% 3.23/1.19 % (3658048)Instructions burned: 16 (million)
% 3.23/1.19 % (3658055)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=3530569408:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.23/1.19 % (3658056)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=664258904:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.23/1.19 % (3658056)Instruction limit reached!
% 3.23/1.19 % (3658056)------------------------------
% 3.23/1.19 % (3658056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658056)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658056)Termination reason: Instruction limit
% 3.23/1.19 % (3658056)Termination phase: Saturation
% 3.23/1.19 % (3658056)Time elapsed: 0.011 s
% 3.23/1.19 % (3658056)Peak memory usage: 89 MB
% 3.23/1.19 % (3658056)Instructions burned: 18 (million)
% 3.23/1.19 % (3658042)Instruction limit reached!
% 3.23/1.19 % (3658042)------------------------------
% 3.23/1.19 % (3658042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658042)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658042)Termination reason: Instruction limit
% 3.23/1.19 % (3658042)Termination phase: Saturation
% 3.23/1.19 % (3658042)Time elapsed: 0.170 s
% 3.23/1.19 % (3658042)Peak memory usage: 119 MB
% 3.23/1.19 % (3658042)Instructions burned: 202 (million)
% 3.23/1.19 % (3658055)Instruction limit reached!
% 3.23/1.19 % (3658055)------------------------------
% 3.23/1.19 % (3658055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658055)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658055)Termination reason: Instruction limit
% 3.23/1.19 % (3658055)Termination phase: Saturation
% 3.23/1.19 % (3658055)Time elapsed: 0.021 s
% 3.23/1.19 % (3658055)Peak memory usage: 89 MB
% 3.23/1.19 % (3658055)Instructions burned: 29 (million)
% 3.23/1.19 % (3658057)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2733793016:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.23/1.19 % (3658057)Instruction limit reached!
% 3.23/1.19 % (3658057)------------------------------
% 3.23/1.19 % (3658057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658057)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658057)Termination reason: Instruction limit
% 3.23/1.19 % (3658057)Termination phase: Saturation
% 3.23/1.19 % (3658057)Time elapsed: 0.018 s
% 3.23/1.19 % (3658057)Peak memory usage: 89 MB
% 3.23/1.19 % (3658057)Instructions burned: 24 (million)
% 3.23/1.19 % (3658058)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=456359927:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.23/1.19 % (3658060)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1021113037:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.23/1.19 % (3658058)Instruction limit reached!
% 3.23/1.19 % (3658058)------------------------------
% 3.23/1.19 % (3658058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658058)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658058)Termination reason: Instruction limit
% 3.23/1.19 % (3658058)Termination phase: Saturation
% 3.23/1.19 % (3658058)Time elapsed: 0.017 s
% 3.23/1.19 % (3658058)Peak memory usage: 90 MB
% 3.23/1.19 % (3658058)Instructions burned: 27 (million)
% 3.23/1.19 % (3658060)Instruction limit reached!
% 3.23/1.19 % (3658060)------------------------------
% 3.23/1.19 % (3658060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658060)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658060)Termination reason: Instruction limit
% 3.23/1.19 % (3658060)Termination phase: Saturation
% 3.23/1.19 % (3658060)Time elapsed: 0.025 s
% 3.23/1.19 % (3658060)Peak memory usage: 89 MB
% 3.23/1.19 % (3658060)Instructions burned: 87 (million)
% 3.23/1.19 % (3658063)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2979165902:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 3.23/1.19 % (3658063)Instruction limit reached!
% 3.23/1.19 % (3658063)------------------------------
% 3.23/1.19 % (3658063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658063)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658063)Termination reason: Instruction limit
% 3.23/1.19 % (3658063)Termination phase: Unused predicate definition removal
% 3.23/1.19 % (3658063)Time elapsed: 0.002 s
% 3.23/1.19 % (3658063)Peak memory usage: 86 MB
% 3.23/1.19 % (3658063)Instructions burned: 3 (million)
% 3.23/1.19 % (3658064)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3338796230:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 3.23/1.19 % (3658065)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=204451929:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 3.23/1.19 % (3658065)Instruction limit reached!
% 3.23/1.19 % (3658065)------------------------------
% 3.23/1.19 % (3658065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658065)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658065)Termination reason: Instruction limit
% 3.23/1.19 % (3658065)Termination phase: Preprocessing 3
% 3.23/1.19 % (3658065)Time elapsed: 0.003 s
% 3.23/1.19 % (3658065)Peak memory usage: 86 MB
% 3.23/1.19 % (3658065)Instructions burned: 4 (million)
% 3.23/1.19 % (3658064)Refutation not found, incomplete strategy
% 3.23/1.19 % (3658064)------------------------------
% 3.23/1.19 % (3658064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.19 % (3658064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.19 % (3658064)CaDiCaL version: 2.1.3
% 3.23/1.19 % (3658064)Termination reason: Refutation not found, incomplete strategy
% 3.23/1.19 % (3658064)Time elapsed: 0.006 s
% 3.23/1.19 % (3658064)Peak memory usage: 89 MB
% 3.23/1.19 % (3658064)Instructions burned: 7 (million)
% 3.23/1.19 % (3658041)Refutation found. Thanks to Tanya!
% 3.23/1.19 % SZS status Theorem for theBenchmark
% 3.23/1.19 % SZS output start Proof for theBenchmark
% See solution above
% 4.26/1.39 % (3658041)------------------------------
% 4.26/1.39 % (3658041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.39 % (3658041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.39 % (3658041)CaDiCaL version: 2.1.3
% 4.26/1.39 % (3658041)Termination reason: Refutation
% 4.26/1.39 % (3658041)Time elapsed: 0.087 s
% 4.26/1.39 % (3658041)Peak memory usage: 117 MB
% 4.26/1.39 % (3658041)Instructions burned: 93 (million)
% 4.26/1.39 % (3658041)------------------------------
% 4.26/1.39 % (3658041)------------------------------
% 4.26/1.39 % (3658011)Success in time 0.519 s
% 4.26/1.39 % Vampire exiting
%------------------------------------------------------------------------------