%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW618_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:40:32 PM UTC 2026
% Result : Theorem 7.42s 1.36s
% Output : Refutation 7.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 11
% Syntax : Number of formulae : 43 ( 30 unt; 0 typ; 0 def)
% Number of atoms : 60 ( 40 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 28 ( 11 ~; 6 |; 2 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 5 ( 0 atm; 0 fun; 0 num; 5 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 : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 71 ( 71 usr; 15 con; 0-5 aty)
% Number of variables : 83 ( 80 !; 3 ?; 83 :)
% 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: ( map_int_int * $int ) > $int ).
tff(func_def_67,type,
sK2: ( map_int_int * $int ) > $int ).
tff(func_def_68,type,
sK3: ( map_int_int * $int ) > $int ).
tff(func_def_69,type,
sK4: ( map_int_int * map_int_int * $int * $int ) > $int ).
tff(func_def_70,type,
sK5: set1 > $int ).
tff(func_def_71,type,
sK6: ( $int * set1 * $int ) > map_int_int ).
tff(func_def_72,type,
sK7: ( $int * set1 * map_int_int ) > $int ).
tff(func_def_73,type,
sK8: ( $int * set1 * map_int_int ) > $int ).
tff(func_def_74,type,
sK9: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp ).
tff(func_def_75,type,
sK10: lpintcm_setrp ).
tff(func_def_76,type,
sK11: 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/sandbox/benchmark/theBenchmark.p',bridgeR2) ).
tff(f59,axiom,
! [X0: ty,X1: uni] : ( none(X0) != some(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',none_Some) ).
tff(f65,axiom,
! [X0: ty,X1: ty,X2: uni] :
( sort(map(X0,option(X1)),X2)
=> ( contents1(X1,X0,mk_t(X1,X0,X2)) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',contents_def1) ).
tff(f68,axiom,
! [X0: ty,X1: ty,X2: uni,X3: uni] : ( mixfix_lbrb(X1,X0,X2,X3) = get(option(X1),X0,contents1(X1,X0,X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mixfix_lbrb_def) ).
tff(f72,axiom,
! [X0: ty,X1: ty,X2: uni] : sort(X0,tuple2_proj_2(X1,X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tuple2_proj_2_sort) ).
tff(f74,axiom,
! [X0: ty,X1: 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/sandbox/benchmark/theBenchmark.p',tuple2_inversion) ).
tff(f75,axiom,
! [X0: lpintcm_setrp] : sort(tuple2(int,set2),t2tb3(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort3) ).
tff(f80,axiom,
! [X0: uni] :
( sort(set2,X0)
=> ( t2tb4(tb2t4(X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR4) ).
tff(f88,axiom,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',t2tb_sort8) ).
tff(f96,conjecture,
! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ! [X1: $int,X2: set1] : ( 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)))) )
=> ! [X1: lpintcm_setrp,X3: lpintcm_map_int_intrp] :
( ( 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/sandbox/benchmark/theBenchmark.p',wP_parameter_maxmat) ).
tff(f97,negated_conjecture,
~ ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ! [X1: $int,X2: set1] : ( 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)))) )
=> ! [X1: lpintcm_setrp,X3: lpintcm_map_int_intrp] :
( ( 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(f138,plain,
~ ! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ! [X1: $int,X2: set1] : ( 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_setrp,X4: lpintcm_map_int_intrp] :
( ( tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X3))) = tb2t6(some(tuple2(int,map(int,int)),t2tb5(X4))) )
=> post(X3,X4) ) ),
inference(rectify,[],[f97]) ).
tff(f178,plain,
! [X0: ty,X1: ty,X2: uni] :
( ( contents1(X1,X0,mk_t(X1,X0,X2)) = X2 )
| ~ sort(map(X0,option(X1)),X2) ),
inference(ennf_transformation,[],[f65]) ).
tff(f182,plain,
! [X0: ty,X1: ty,X2: uni] :
( ( X2 = tuple21(X1,X0,tuple2_proj_1(X1,X0,X2),tuple2_proj_2(X1,X0,X2)) )
| ~ sort(tuple2(X1,X0),X2) ),
inference(ennf_transformation,[],[f74]) ).
tff(f183,plain,
! [X0: uni] :
( ( t2tb4(tb2t4(X0)) = X0 )
| ~ sort(set2,X0) ),
inference(ennf_transformation,[],[f80]) ).
tff(f187,plain,
? [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] :
( ? [X3: lpintcm_setrp,X4: lpintcm_map_int_intrp] :
( ~ post(X3,X4)
& ( tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0)),t2tb3(X3))) = tb2t6(some(tuple2(int,map(int,int)),t2tb5(X4))) ) )
& ! [X1: $int,X2: set1] : ( 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)))) ) ),
inference(ennf_transformation,[],[f138]) ).
tff(f238,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f44]) ).
tff(f269,plain,
! [X0: ty,X1: uni] : ( none(X0) != some(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tff(f275,plain,
! [X2: uni,X0: ty,X1: ty] :
( ~ sort(map(X0,option(X1)),X2)
| ( contents1(X1,X0,mk_t(X1,X0,X2)) = X2 ) ),
inference(cnf_transformation,[],[f178]) ).
tff(f278,plain,
! [X2: uni,X3: uni,X0: ty,X1: ty] : ( mixfix_lbrb(X1,X0,X2,X3) = get(option(X1),X0,contents1(X1,X0,X2),X3) ),
inference(cnf_transformation,[],[f68]) ).
tff(f282,plain,
! [X2: uni,X0: ty,X1: ty] : sort(X0,tuple2_proj_2(X1,X0,X2)),
inference(cnf_transformation,[],[f72]) ).
tff(f284,plain,
! [X2: uni,X0: ty,X1: ty] :
( ~ sort(tuple2(X1,X0),X2)
| ( tuple21(X1,X0,tuple2_proj_1(X1,X0,X2),tuple2_proj_2(X1,X0,X2)) = X2 ) ),
inference(cnf_transformation,[],[f182]) ).
tff(f285,plain,
! [X0: lpintcm_setrp] : sort(tuple2(int,set2),t2tb3(X0)),
inference(cnf_transformation,[],[f75]) ).
tff(f290,plain,
! [X0: uni] :
( ~ sort(set2,X0)
| ( t2tb4(tb2t4(X0)) = X0 ) ),
inference(cnf_transformation,[],[f183]) ).
tff(f319,plain,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
inference(cnf_transformation,[],[f88]) ).
tff(f323,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(f326,plain,
tb2t6(mixfix_lbrb(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(sK9)),t2tb3(sK10))) = tb2t6(some(tuple2(int,map(int,int)),t2tb5(sK11))),
inference(cnf_transformation,[],[f187]) ).
tff(f328,plain,
! [X2: set1,X1: $int] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),tuple21(int,set2,t2tb2(X1),t2tb4(X2)))) ),
inference(cnf_transformation,[],[f187]) ).
tff(f333,plain,
tb2t6(some(tuple2(int,map(int,int)),t2tb5(sK11))) = 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(sK9))),t2tb3(sK10))),
inference(definition_unfolding,[],[f326,f278]) ).
tff(f370,plain,
! [X0: uni,X1: set1] : ( tb2t6(none(tuple2(int,map(int,int)))) = tb2t6(get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),tuple21(int,set2,X0,t2tb4(X1)))) ),
inference(superposition,[],[f328,f238]) ).
tff(f372,plain,
! [X0: uni,X1: set1] : ( get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),tuple21(int,set2,X0,t2tb4(X1))) = t2tb6(tb2t6(none(tuple2(int,map(int,int))))) ),
inference(superposition,[],[f319,f370]) ).
tff(f373,plain,
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(sK9))),t2tb3(sK10)) = t2tb6(tb2t6(some(tuple2(int,map(int,int)),t2tb5(sK11)))),
inference(superposition,[],[f319,f333]) ).
tff(f374,plain,
some(tuple2(int,map(int,int)),t2tb5(sK11)) = 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(sK9))),t2tb3(sK10)),
inference(forward_demodulation,[],[f373,f319]) ).
tff(f375,plain,
! [X0: uni,X1: set1] : ( none(tuple2(int,map(int,int))) = get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),tuple21(int,set2,X0,t2tb4(X1))) ),
inference(forward_demodulation,[],[f372,f319]) ).
tff(f467,plain,
! [X0: ty,X1: uni] : ( tuple2_proj_2(X0,set2,X1) = t2tb4(tb2t4(tuple2_proj_2(X0,set2,X1))) ),
inference(resolution,[],[f290,f282]) ).
tff(f1069,plain,
! [X0: map_lpintcm_setrp_lpoption_lpintcm_map_int_intrprp] : ( t2tb8(X0) = contents1(tuple2(int,map(int,int)),tuple2(int,set2),mk_t(tuple2(int,map(int,int)),tuple2(int,set2),t2tb8(X0))) ),
inference(resolution,[],[f275,f323]) ).
tff(f1139,plain,
! [X0: lpintcm_setrp] : ( t2tb3(X0) = tuple21(int,set2,tuple2_proj_1(int,set2,t2tb3(X0)),tuple2_proj_2(int,set2,t2tb3(X0))) ),
inference(resolution,[],[f284,f285]) ).
tff(f2848,plain,
! [X2: uni,X0: ty,X1: uni] : ( none(tuple2(int,map(int,int))) = get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),tuple21(int,set2,X2,tuple2_proj_2(X0,set2,X1))) ),
inference(superposition,[],[f375,f467]) ).
tff(f9171,plain,
! [X0: lpintcm_setrp] : ( none(tuple2(int,map(int,int))) = get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),t2tb3(X0)) ),
inference(superposition,[],[f2848,f1139]) ).
tff(f19196,plain,
some(tuple2(int,map(int,int)),t2tb5(sK11)) = get(option(tuple2(int,map(int,int))),tuple2(int,set2),t2tb8(sK9),t2tb3(sK10)),
inference(superposition,[],[f374,f1069]) ).
tff(f19210,plain,
none(tuple2(int,map(int,int))) = some(tuple2(int,map(int,int)),t2tb5(sK11)),
inference(forward_demodulation,[],[f19196,f9171]) ).
tff(f19211,plain,
$false,
inference(forward_subsumption_resolution,[],[f19210,f269]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW618_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n004.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:22:52 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.76/1.20 % (380829)Will run a generic schedule for satisfiability detection.
% 6.76/1.20 % (380836)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=369426512:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.76/1.20 % (380834)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1952548194_2999 on theBenchmark for (2999ds/0Mi)
% 6.76/1.20 % (380837)dis+10_1_sil=32000:sp=arity:random_seed=2530063227:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.76/1.20 % (380838)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=192957403:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.76/1.20 % (380840)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=168071210:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.76/1.20 % (380835)% WARNING: option uhcvi not known.
% 6.76/1.20 % (380834)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.76/1.20 % (380834)Terminated due to inappropriate strategy.
% 6.76/1.20 % (380834)------------------------------
% 6.76/1.20 % (380834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.20 % (380834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.20 % (380834)CaDiCaL version: 2.1.3
% 6.76/1.20 % (380834)Termination reason: Inappropriate
% 6.76/1.20 % (380834)Time elapsed: 0.005 s
% 6.76/1.20 % (380834)Peak memory usage: 11 MB
% 6.76/1.20 % (380834)Instructions burned: 9 (million)
% 6.76/1.20 % (380834)------------------------------
% 6.76/1.20 % (380834)------------------------------
% 6.76/1.20 % (380835)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3317824722:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.76/1.20 % (380839)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3654437341:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.76/1.20 % (380846)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=513911764:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.76/1.20 % (380846)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.76/1.20 % (380846)Terminated due to inappropriate strategy.
% 6.76/1.20 % (380846)------------------------------
% 6.76/1.20 % (380846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.20 % (380846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.20 % (380846)CaDiCaL version: 2.1.3
% 6.76/1.20 % (380846)Termination reason: Inappropriate
% 6.76/1.20 % (380846)Time elapsed: 0.004 s
% 6.76/1.20 % (380846)Peak memory usage: 10 MB
% 6.76/1.20 % (380846)Instructions burned: 8 (million)
% 6.76/1.20 % (380846)------------------------------
% 6.76/1.20 % (380846)------------------------------
% 6.76/1.20 % (380850)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=937600927:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.76/1.20 % (380837)Instruction limit reached!
% 6.76/1.20 % (380837)------------------------------
% 6.76/1.20 % (380837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.20 % (380837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.20 % (380837)CaDiCaL version: 2.1.3
% 6.76/1.20 % (380837)Termination reason: Instruction limit
% 6.76/1.20 % (380837)Termination phase: Saturation
% 6.76/1.20 % (380837)Time elapsed: 0.064 s
% 6.76/1.20 % (380837)Peak memory usage: 13 MB
% 6.76/1.20 % (380837)Instructions burned: 103 (million)
% 6.76/1.20 % (380838)Instruction limit reached!
% 6.76/1.20 % (380838)------------------------------
% 6.76/1.20 % (380838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.20 % (380838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.20 % (380838)CaDiCaL version: 2.1.3
% 6.76/1.20 % (380838)Termination reason: Instruction limit
% 6.76/1.20 % (380838)Termination phase: Saturation
% 6.76/1.20 % (380838)Time elapsed: 0.073 s
% 6.76/1.20 % (380838)Peak memory usage: 13 MB
% 6.76/1.20 % (380838)Instructions burned: 117 (million)
% 6.76/1.20 % (380852)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4210001754:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.76/1.20 % (380840)Instruction limit reached!
% 6.76/1.20 % (380840)------------------------------
% 6.76/1.20 % (380840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380840)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380840)Termination reason: Instruction limit
% 7.42/1.35 % (380840)Termination phase: Saturation
% 7.42/1.35 % (380840)Time elapsed: 0.103 s
% 7.42/1.35 % (380840)Peak memory usage: 14 MB
% 7.42/1.35 % (380840)Instructions burned: 159 (million)
% 7.42/1.35 % (380853)ott-21_1_sil=16000:fs=off:random_seed=3651798190:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.42/1.35 % (380855)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2465406269:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.42/1.35 % (380850)Instruction limit reached!
% 7.42/1.35 % (380850)------------------------------
% 7.42/1.35 % (380850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380850)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380850)Termination reason: Instruction limit
% 7.42/1.35 % (380850)Termination phase: Saturation
% 7.42/1.35 % (380850)Time elapsed: 0.085 s
% 7.42/1.35 % (380850)Peak memory usage: 13 MB
% 7.42/1.35 % (380850)Instructions burned: 132 (million)
% 7.42/1.35 % (380858)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=241696888:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.42/1.35 % (380839)Instruction limit reached!
% 7.42/1.35 % (380839)------------------------------
% 7.42/1.35 % (380839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380839)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380839)Termination reason: Instruction limit
% 7.42/1.35 % (380839)Termination phase: Saturation
% 7.42/1.35 % (380839)Time elapsed: 0.137 s
% 7.42/1.35 % (380839)Peak memory usage: 13 MB
% 7.42/1.35 % (380839)Instructions burned: 131 (million)
% 7.42/1.35 % (380858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380858)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380858)------------------------------
% 7.42/1.35 % (380858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380858)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380858)Termination reason: Inappropriate
% 7.42/1.35 % (380858)Time elapsed: 0.004 s
% 7.42/1.35 % (380858)Peak memory usage: 11 MB
% 7.42/1.35 % (380858)Instructions burned: 8 (million)
% 7.42/1.35 % (380858)------------------------------
% 7.42/1.35 % (380858)------------------------------
% 7.42/1.35 % (380860)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=206779369:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.42/1.35 % (380861)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1020069412:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.42/1.35 % (380861)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380861)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380861)------------------------------
% 7.42/1.35 % (380861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380861)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380861)Termination reason: Inappropriate
% 7.42/1.35 % (380861)Time elapsed: 0.016 s
% 7.42/1.35 % (380861)Peak memory usage: 10 MB
% 7.42/1.35 % (380861)Instructions burned: 8 (million)
% 7.42/1.35 % (380861)------------------------------
% 7.42/1.35 % (380861)------------------------------
% 7.42/1.35 % (380853)Instruction limit reached!
% 7.42/1.35 % (380853)------------------------------
% 7.42/1.35 % (380853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380853)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380853)Termination reason: Instruction limit
% 7.42/1.35 % (380853)Termination phase: Saturation
% 7.42/1.35 % (380853)Time elapsed: 0.115 s
% 7.42/1.35 % (380853)Peak memory usage: 13 MB
% 7.42/1.35 % (380853)Instructions burned: 180 (million)
% 7.42/1.35 % (380872)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2725371616:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 7.42/1.35 % (380873)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4286091067:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 7.42/1.35 % (380855)Instruction limit reached!
% 7.42/1.35 % (380855)------------------------------
% 7.42/1.35 % (380855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380855)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380855)Termination reason: Instruction limit
% 7.42/1.35 % (380855)Termination phase: Saturation
% 7.42/1.35 % (380855)Time elapsed: 0.471 s
% 7.42/1.35 % (380855)Peak memory usage: 14 MB
% 7.42/1.35 % (380855)Instructions burned: 477 (million)
% 7.42/1.35 % (380888)fmb+10_1_sil=64000:random_seed=3864388039:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 7.42/1.35 % (380888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380888)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380888)------------------------------
% 7.42/1.35 % (380888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380888)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380888)Termination reason: Inappropriate
% 7.42/1.35 % (380888)Time elapsed: 0.009 s
% 7.42/1.35 % (380888)Peak memory usage: 10 MB
% 7.42/1.35 % (380888)Instructions burned: 8 (million)
% 7.42/1.35 % (380888)------------------------------
% 7.42/1.35 % (380888)------------------------------
% 7.42/1.35 % (380852)Instruction limit reached!
% 7.42/1.35 % (380852)------------------------------
% 7.42/1.35 % (380852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380852)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380852)Termination reason: Instruction limit
% 7.42/1.35 % (380852)Termination phase: Saturation
% 7.42/1.35 % (380852)Time elapsed: 0.595 s
% 7.42/1.35 % (380852)Peak memory usage: 18 MB
% 7.42/1.35 % (380852)Instructions burned: 684 (million)
% 7.42/1.35 % (380892)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2613090387:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 7.42/1.35 % (380892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380892)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380892)------------------------------
% 7.42/1.35 % (380892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380892)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380892)Termination reason: Inappropriate
% 7.42/1.35 % (380892)Time elapsed: 0.008 s
% 7.42/1.35 % (380892)Peak memory usage: 10 MB
% 7.42/1.35 % (380892)Instructions burned: 8 (million)
% 7.42/1.35 % (380892)------------------------------
% 7.42/1.35 % (380892)------------------------------
% 7.42/1.35 % (380893)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2853048806:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 7.42/1.35 % (380893)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380893)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380893)------------------------------
% 7.42/1.35 % (380893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380893)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380893)Termination reason: Inappropriate
% 7.42/1.35 % (380893)Time elapsed: 0.007 s
% 7.42/1.35 % (380893)Peak memory usage: 11 MB
% 7.42/1.35 % (380893)Instructions burned: 8 (million)
% 7.42/1.35 % (380893)------------------------------
% 7.42/1.35 % (380893)------------------------------
% 7.42/1.35 % (380895)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3028705517:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 7.42/1.35 % (380902)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3861451310:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 7.42/1.35 % (380872)Instruction limit reached!
% 7.42/1.35 % (380872)------------------------------
% 7.42/1.35 % (380872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380872)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380872)Termination reason: Instruction limit
% 7.42/1.35 % (380872)Termination phase: Saturation
% 7.42/1.35 % (380872)Time elapsed: 0.702 s
% 7.42/1.35 % (380872)Peak memory usage: 19 MB
% 7.42/1.35 % (380872)Instructions burned: 693 (million)
% 7.42/1.35 % (380914)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2024520038:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 7.42/1.35 % (380914)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380914)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380914)------------------------------
% 7.42/1.35 % (380914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380914)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380914)Termination reason: Inappropriate
% 7.42/1.35 % (380914)Time elapsed: 0.012 s
% 7.42/1.35 % (380914)Peak memory usage: 11 MB
% 7.42/1.35 % (380914)Instructions burned: 9 (million)
% 7.42/1.35 % (380914)------------------------------
% 7.42/1.35 % (380914)------------------------------
% 7.42/1.35 % (380919)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1054682061:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 7.42/1.35 % (380919)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.42/1.35 % (380919)Terminated due to inappropriate strategy.
% 7.42/1.35 % (380919)------------------------------
% 7.42/1.35 % (380919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.35 % (380919)CaDiCaL version: 2.1.3
% 7.42/1.35 % (380919)Termination reason: Inappropriate
% 7.42/1.35 % (380919)Time elapsed: 0.009 s
% 7.42/1.35 % (380919)Peak memory usage: 11 MB
% 7.42/1.35 % (380919)Instructions burned: 8 (million)
% 7.42/1.35 % (380873)Instruction limit reached!
% 7.42/1.35 % (380873)------------------------------
% 7.42/1.35 % (380873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.35 % (380873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.36 % (380873)CaDiCaL version: 2.1.3
% 7.42/1.36 % (380873)Termination reason: Instruction limit
% 7.42/1.36 % (380873)Termination phase: Saturation
% 7.42/1.36 % (380873)Time elapsed: 0.775 s
% 7.42/1.36 % (380873)Peak memory usage: 18 MB
% 7.42/1.36 % (380873)Instructions burned: 879 (million)
% 7.42/1.36 % (380919)------------------------------
% 7.42/1.36 % (380919)------------------------------
% 7.42/1.36 % (380924)ott-2_1_sil=16000:newcnf=on:random_seed=3029436569:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi)
% 7.42/1.36 % (380835) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-380829-380835"...
% 7.42/1.36 % (380925)ott+10_1_sil=32000:tgt=ground:random_seed=1236819345:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi)
% 7.42/1.36 % (380835)...printing done.
% 7.42/1.36 % (380835)Refutation found. Thanks to Tanya!
% 7.42/1.36 % SZS status Theorem for theBenchmark
% 7.42/1.36 % SZS output start Proof for theBenchmark
% See solution above
% 7.42/1.36 % (380835)------------------------------
% 7.42/1.36 % (380835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.42/1.36 % (380835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.36 % (380835)CaDiCaL version: 2.1.3
% 7.42/1.36 % (380835)Termination reason: Refutation
% 7.42/1.36 % (380835)Time elapsed: 1.065 s
% 7.42/1.36 % (380835)Peak memory usage: 19 MB
% 7.42/1.36 % (380835)Instructions burned: 1314 (million)
% 7.42/1.36 % (380829)Success in time 1.123 s
% 7.42/1.36 % Vampire exiting
%------------------------------------------------------------------------------