%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW672_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 : n015.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:06 PM UTC 2026
% Result : Theorem 12.10s 2.78s
% Output : Refutation 0.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 64 ( 9 unt; 0 typ; 6 def)
% Number of atoms : 460 ( 112 equ)
% Maximal formula atoms : 30 ( 7 avg)
% Number of connectives : 543 ( 147 ~; 106 |; 194 &)
% ( 22 <=>; 74 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 58 ( 10 atm; 10 fun; 20 num; 18 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 17 usr; 7 prp; 0-6 aty)
% Number of functors : 60 ( 57 usr; 27 con; 0-4 aty)
% Number of variables : 263 ( 178 !; 85 ?; 263 :)
% 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,
vertex1: $tType ).
tff(type_def_10,type,
set_vertex: $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,
set: ty > ty ).
tff(func_def_13,type,
empty: ty > uni ).
tff(func_def_14,type,
add: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
remove: ( ty * uni * uni ) > uni ).
tff(func_def_16,type,
union: ( ty * uni * uni ) > uni ).
tff(func_def_17,type,
inter: ( ty * uni * uni ) > uni ).
tff(func_def_18,type,
diff: ( ty * uni * uni ) > uni ).
tff(func_def_19,type,
choose: ( ty * uni ) > uni ).
tff(func_def_20,type,
cardinal1: ( ty * uni ) > $int ).
tff(func_def_23,type,
vertex: ty ).
tff(func_def_24,type,
succ1: vertex1 > set_vertex ).
tff(func_def_25,type,
t2tb: set_vertex > uni ).
tff(func_def_26,type,
tb2t: uni > set_vertex ).
tff(func_def_27,type,
t2tb1: vertex1 > uni ).
tff(func_def_28,type,
tb2t1: uni > vertex1 ).
tff(func_def_29,type,
ref: ty > ty ).
tff(func_def_30,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_31,type,
contents: ( ty * uni ) > uni ).
tff(func_def_32,type,
sK2: ( $int * vertex1 * vertex1 ) > $int ).
tff(func_def_33,type,
sK3: ( $int * vertex1 * vertex1 ) > vertex1 ).
tff(func_def_34,type,
sK4: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_35,type,
sK5: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_36,type,
sK6: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_37,type,
sK7: ( vertex1 * vertex1 * $int ) > $int ).
tff(func_def_38,type,
sK8: ( $int * vertex1 * vertex1 ) > vertex1 ).
tff(func_def_39,type,
sK9: ( set_vertex * vertex1 ) > vertex1 ).
tff(func_def_40,type,
sK10: vertex1 ).
tff(func_def_41,type,
sK11: set_vertex ).
tff(func_def_42,type,
sK12: vertex1 ).
tff(func_def_43,type,
sK13: $int ).
tff(func_def_44,type,
sK14: set_vertex ).
tff(func_def_45,type,
sK15: set_vertex ).
tff(func_def_46,type,
sK16: bool1 ).
tff(func_def_47,type,
sK17: set_vertex ).
tff(func_def_48,type,
sK18: vertex1 ).
tff(func_def_49,type,
sK19: set_vertex ).
tff(func_def_50,type,
sK20: set_vertex ).
tff(func_def_51,type,
sK21: bool1 ).
tff(func_def_52,type,
sK22: set_vertex ).
tff(func_def_53,type,
sK23: set_vertex ).
tff(func_def_54,type,
sK24: $int ).
tff(func_def_55,type,
sK25: vertex1 ).
tff(func_def_56,type,
sK26: ( $int * vertex1 * vertex1 ) > $int ).
tff(func_def_57,type,
sK27: ( ty * uni * uni ) > uni ).
tff(func_def_58,type,
sK28: set_vertex > vertex1 ).
tff(func_def_59,type,
sK29: set_vertex > vertex1 ).
tff(func_def_60,type,
sK30: ( ty * uni ) > uni ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
infix_eqeq: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
subset: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
is_empty: ( ty * uni ) > $o ).
tff(pred_def_7,type,
path1: ( vertex1 * vertex1 * $int ) > $o ).
tff(pred_def_8,type,
shortest_path1: ( vertex1 * vertex1 * $int ) > $o ).
tff(pred_def_10,type,
inv1: ( vertex1 * vertex1 * set_vertex * set_vertex * set_vertex * $int ) > $o ).
tff(pred_def_11,type,
closure1: ( set_vertex * set_vertex * set_vertex * vertex1 ) > $o ).
tff(pred_def_12,type,
sP0: ( $int * vertex1 * set_vertex ) > $o ).
tff(pred_def_13,type,
sP1: ( vertex1 * vertex1 * $int ) > $o ).
tff(f15,axiom,
! [X1: uni,X0: ty] :
( ( is_empty(X0,X1)
=> ! [X2: uni] : ~ mem(X0,X2,X1) )
& ( ! [X2: uni] :
( sort1(X0,X2)
=> ~ mem(X0,X2,X1) )
=> is_empty(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',is_empty_def) ).
tff(f58,axiom,
! [X2: set_vertex,X0: set_vertex,X1: set_vertex,X3: vertex1] :
( ( mem(vertex,t2tb1(X3),t2tb(X0))
=> ( ~ mem(vertex,t2tb1(X3),t2tb(X1))
=> ( ~ mem(vertex,t2tb1(X3),t2tb(X2))
=> ! [X4: vertex1] :
( mem(vertex,t2tb1(X4),t2tb(succ1(X3)))
=> mem(vertex,t2tb1(X4),t2tb(X0)) ) ) ) )
<=> closure1(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_def) ).
tff(f59,conjecture,
! [X1: vertex1,X5: set_vertex,X0: vertex1,X4: set_vertex,X3: set_vertex,X2: $int] :
( ( $lesseq(0,X2)
& ( is_empty(vertex,t2tb(X4))
=> is_empty(vertex,t2tb(X3)) )
& inv1(X0,X1,X5,X4,X3,X2)
& ! [X6: vertex1] : closure1(X5,X4,X3,X6) )
=> ! [X7: bool1] :
( ( is_empty(vertex,t2tb(X4))
<=> ( X7 = true1 ) )
=> ( ( X7 != true1 )
=> ( ~ is_empty(vertex,t2tb(X4))
=> ! [X9: vertex1,X8: set_vertex] :
( ( ( X8 = tb2t(remove(vertex,t2tb1(X9),t2tb(X4))) )
& mem(vertex,t2tb1(X9),t2tb(X4)) )
=> ( ( X9 != X1 )
=> ( ( shortest_path1(X0,X9,X2)
& ! [X6: vertex1] :
( ( X6 != X9 )
=> closure1(X5,X8,X3,X6) )
& inv1(X0,X1,X5,X8,X3,X2) )
=> ! [X10: set_vertex,X11: set_vertex] :
( ( subset(vertex,t2tb(succ1(X9)),t2tb(X11))
& ! [X6: vertex1] : closure1(X11,X8,X10,X6)
& inv1(X0,X1,X11,X8,X10,X2) )
=> ! [X12: bool1] :
( ( is_empty(vertex,t2tb(X8))
<=> ( X12 = true1 ) )
=> ( ( X12 = true1 )
=> ! [X13: set_vertex] :
( ( X13 = X10 )
=> ! [X14: set_vertex] :
( ( X14 = tb2t(empty(vertex)) )
=> ! [X15: $int] :
( ( X15 = $sum(X2,1) )
=> ! [X6: vertex1] : closure1(X11,X13,X14,X6) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_bfs) ).
tff(f60,negated_conjecture,
~ ! [X1: vertex1,X5: set_vertex,X0: vertex1,X4: set_vertex,X3: set_vertex,X2: $int] :
( ( $lesseq(0,X2)
& ( is_empty(vertex,t2tb(X4))
=> is_empty(vertex,t2tb(X3)) )
& inv1(X0,X1,X5,X4,X3,X2)
& ! [X6: vertex1] : closure1(X5,X4,X3,X6) )
=> ! [X7: bool1] :
( ( is_empty(vertex,t2tb(X4))
<=> ( X7 = true1 ) )
=> ( ( X7 != true1 )
=> ( ~ is_empty(vertex,t2tb(X4))
=> ! [X9: vertex1,X8: set_vertex] :
( ( ( X8 = tb2t(remove(vertex,t2tb1(X9),t2tb(X4))) )
& mem(vertex,t2tb1(X9),t2tb(X4)) )
=> ( ( X9 != X1 )
=> ( ( shortest_path1(X0,X9,X2)
& ! [X6: vertex1] :
( ( X6 != X9 )
=> closure1(X5,X8,X3,X6) )
& inv1(X0,X1,X5,X8,X3,X2) )
=> ! [X10: set_vertex,X11: set_vertex] :
( ( subset(vertex,t2tb(succ1(X9)),t2tb(X11))
& ! [X6: vertex1] : closure1(X11,X8,X10,X6)
& inv1(X0,X1,X11,X8,X10,X2) )
=> ! [X12: bool1] :
( ( is_empty(vertex,t2tb(X8))
<=> ( X12 = true1 ) )
=> ( ( X12 = true1 )
=> ! [X13: set_vertex] :
( ( X13 = X10 )
=> ! [X14: set_vertex] :
( ( X14 = tb2t(empty(vertex)) )
=> ! [X15: $int] :
( ( X15 = $sum(X2,1) )
=> ! [X6: vertex1] : closure1(X11,X13,X14,X6) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
tff(f67,plain,
~ ! [X1: vertex1,X5: set_vertex,X0: vertex1,X4: set_vertex,X3: set_vertex,X2: $int] :
( ( ~ $less(X2,0)
& ( is_empty(vertex,t2tb(X4))
=> is_empty(vertex,t2tb(X3)) )
& inv1(X0,X1,X5,X4,X3,X2)
& ! [X6: vertex1] : closure1(X5,X4,X3,X6) )
=> ! [X7: bool1] :
( ( is_empty(vertex,t2tb(X4))
<=> ( X7 = true1 ) )
=> ( ( X7 != true1 )
=> ( ~ is_empty(vertex,t2tb(X4))
=> ! [X9: vertex1,X8: set_vertex] :
( ( ( X8 = tb2t(remove(vertex,t2tb1(X9),t2tb(X4))) )
& mem(vertex,t2tb1(X9),t2tb(X4)) )
=> ( ( X9 != X1 )
=> ( ( shortest_path1(X0,X9,X2)
& ! [X6: vertex1] :
( ( X6 != X9 )
=> closure1(X5,X8,X3,X6) )
& inv1(X0,X1,X5,X8,X3,X2) )
=> ! [X10: set_vertex,X11: set_vertex] :
( ( subset(vertex,t2tb(succ1(X9)),t2tb(X11))
& ! [X6: vertex1] : closure1(X11,X8,X10,X6)
& inv1(X0,X1,X11,X8,X10,X2) )
=> ! [X12: bool1] :
( ( is_empty(vertex,t2tb(X8))
<=> ( X12 = true1 ) )
=> ( ( X12 = true1 )
=> ! [X13: set_vertex] :
( ( X13 = X10 )
=> ! [X14: set_vertex] :
( ( X14 = tb2t(empty(vertex)) )
=> ! [X15: $int] :
( ( X15 = $sum(X2,1) )
=> ! [X6: vertex1] : closure1(X11,X13,X14,X6) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f60]) ).
tff(f68,plain,
~ ! [X2: vertex1,X3: set_vertex,X1: set_vertex,X5: $int,X4: set_vertex,X0: vertex1] :
( ( inv1(X2,X0,X1,X3,X4,X5)
& ~ $less(X5,0)
& ! [X6: vertex1] : closure1(X1,X3,X4,X6)
& ( is_empty(vertex,t2tb(X3))
=> is_empty(vertex,t2tb(X4)) ) )
=> ! [X7: bool1] :
( ( is_empty(vertex,t2tb(X3))
<=> ( X7 = true1 ) )
=> ( ( X7 != true1 )
=> ( ~ is_empty(vertex,t2tb(X3))
=> ! [X8: vertex1,X9: set_vertex] :
( ( ( tb2t(remove(vertex,t2tb1(X8),t2tb(X3))) = X9 )
& mem(vertex,t2tb1(X8),t2tb(X3)) )
=> ( ( X0 != X8 )
=> ( ( inv1(X2,X0,X1,X9,X4,X5)
& shortest_path1(X2,X8,X5)
& ! [X10: vertex1] :
( ( X8 != X10 )
=> closure1(X1,X9,X4,X10) ) )
=> ! [X11: set_vertex,X12: set_vertex] :
( ( subset(vertex,t2tb(succ1(X8)),t2tb(X12))
& ! [X13: vertex1] : closure1(X12,X9,X11,X13)
& inv1(X2,X0,X12,X9,X11,X5) )
=> ! [X14: bool1] :
( ( is_empty(vertex,t2tb(X9))
<=> ( true1 = X14 ) )
=> ( ( true1 = X14 )
=> ! [X15: set_vertex] :
( ( X11 = X15 )
=> ! [X16: set_vertex] :
( ( tb2t(empty(vertex)) = X16 )
=> ! [X17: $int] :
( ( $sum(X5,1) = X17 )
=> ! [X18: vertex1] : closure1(X12,X15,X16,X18) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f67]) ).
tff(f72,plain,
! [X1: ty,X0: uni] :
( ( ! [X3: uni] :
( sort1(X1,X3)
=> ~ mem(X1,X3,X0) )
=> is_empty(X1,X0) )
& ( is_empty(X1,X0)
=> ! [X2: uni] : ~ mem(X1,X2,X0) ) ),
inference(rectify,[],[f15]) ).
tff(f76,plain,
! [X3: vertex1,X0: set_vertex,X2: set_vertex,X1: set_vertex] :
( closure1(X1,X2,X0,X3)
<=> ( mem(vertex,t2tb1(X3),t2tb(X1))
=> ( ~ mem(vertex,t2tb1(X3),t2tb(X2))
=> ( ~ mem(vertex,t2tb1(X3),t2tb(X0))
=> ! [X4: vertex1] :
( mem(vertex,t2tb1(X4),t2tb(succ1(X3)))
=> mem(vertex,t2tb1(X4),t2tb(X1)) ) ) ) ) ),
inference(rectify,[],[f58]) ).
tff(f93,plain,
! [X1: ty,X0: uni] :
( ( is_empty(X1,X0)
| ? [X3: uni] :
( sort1(X1,X3)
& mem(X1,X3,X0) ) )
& ( ~ is_empty(X1,X0)
| ! [X2: uni] : ~ mem(X1,X2,X0) ) ),
inference(ennf_transformation,[],[f72]) ).
tff(f94,plain,
! [X3: vertex1,X0: set_vertex,X2: set_vertex,X1: set_vertex] :
( closure1(X1,X2,X0,X3)
<=> ( ! [X4: vertex1] :
( mem(vertex,t2tb1(X4),t2tb(X1))
| ~ mem(vertex,t2tb1(X4),t2tb(succ1(X3))) )
| mem(vertex,t2tb1(X3),t2tb(X0))
| mem(vertex,t2tb1(X3),t2tb(X2))
| ~ mem(vertex,t2tb1(X3),t2tb(X1)) ) ),
inference(ennf_transformation,[],[f76]) ).
tff(f95,plain,
! [X1: set_vertex,X0: set_vertex,X3: vertex1,X2: set_vertex] :
( closure1(X1,X2,X0,X3)
<=> ( mem(vertex,t2tb1(X3),t2tb(X2))
| ! [X4: vertex1] :
( mem(vertex,t2tb1(X4),t2tb(X1))
| ~ mem(vertex,t2tb1(X4),t2tb(succ1(X3))) )
| ~ mem(vertex,t2tb1(X3),t2tb(X1))
| mem(vertex,t2tb1(X3),t2tb(X0)) ) ),
inference(flattening,[],[f94]) ).
tff(f98,plain,
? [X2: vertex1,X3: set_vertex,X1: set_vertex,X5: $int,X4: set_vertex,X0: vertex1] :
( ? [X7: bool1] :
( ? [X8: vertex1,X9: set_vertex] :
( ? [X11: set_vertex,X12: set_vertex] :
( ? [X14: bool1] :
( ? [X15: set_vertex] :
( ? [X16: set_vertex] :
( ( tb2t(empty(vertex)) = X16 )
& ? [X17: $int] :
( ( $sum(X5,1) = X17 )
& ? [X18: vertex1] : ~ closure1(X12,X15,X16,X18) ) )
& ( X11 = X15 ) )
& ( true1 = X14 )
& ( is_empty(vertex,t2tb(X9))
<=> ( true1 = X14 ) ) )
& subset(vertex,t2tb(succ1(X8)),t2tb(X12))
& ! [X13: vertex1] : closure1(X12,X9,X11,X13)
& inv1(X2,X0,X12,X9,X11,X5) )
& inv1(X2,X0,X1,X9,X4,X5)
& shortest_path1(X2,X8,X5)
& ! [X10: vertex1] :
( closure1(X1,X9,X4,X10)
| ( X8 = X10 ) )
& ( X0 != X8 )
& ( tb2t(remove(vertex,t2tb1(X8),t2tb(X3))) = X9 )
& mem(vertex,t2tb1(X8),t2tb(X3)) )
& ~ is_empty(vertex,t2tb(X3))
& ( X7 != true1 )
& ( is_empty(vertex,t2tb(X3))
<=> ( X7 = true1 ) ) )
& inv1(X2,X0,X1,X3,X4,X5)
& ~ $less(X5,0)
& ! [X6: vertex1] : closure1(X1,X3,X4,X6)
& ( is_empty(vertex,t2tb(X4))
| ~ is_empty(vertex,t2tb(X3)) ) ),
inference(ennf_transformation,[],[f68]) ).
tff(f99,plain,
? [X0: vertex1,X3: set_vertex,X2: vertex1,X5: $int,X4: set_vertex,X1: set_vertex] :
( ? [X7: bool1] :
( ? [X9: set_vertex,X8: vertex1] :
( shortest_path1(X2,X8,X5)
& inv1(X2,X0,X1,X9,X4,X5)
& ! [X10: vertex1] :
( closure1(X1,X9,X4,X10)
| ( X8 = X10 ) )
& ( tb2t(remove(vertex,t2tb1(X8),t2tb(X3))) = X9 )
& ( X0 != X8 )
& mem(vertex,t2tb1(X8),t2tb(X3))
& ? [X12: set_vertex,X11: set_vertex] :
( inv1(X2,X0,X12,X9,X11,X5)
& ? [X14: bool1] :
( ? [X15: set_vertex] :
( ? [X16: set_vertex] :
( ( tb2t(empty(vertex)) = X16 )
& ? [X17: $int] :
( ( $sum(X5,1) = X17 )
& ? [X18: vertex1] : ~ closure1(X12,X15,X16,X18) ) )
& ( X11 = X15 ) )
& ( true1 = X14 )
& ( is_empty(vertex,t2tb(X9))
<=> ( true1 = X14 ) ) )
& ! [X13: vertex1] : closure1(X12,X9,X11,X13)
& subset(vertex,t2tb(succ1(X8)),t2tb(X12)) ) )
& ~ is_empty(vertex,t2tb(X3))
& ( is_empty(vertex,t2tb(X3))
<=> ( X7 = true1 ) )
& ( X7 != true1 ) )
& inv1(X2,X0,X1,X3,X4,X5)
& ( is_empty(vertex,t2tb(X4))
| ~ is_empty(vertex,t2tb(X3)) )
& ~ $less(X5,0)
& ! [X6: vertex1] : closure1(X1,X3,X4,X6) ),
inference(flattening,[],[f98]) ).
tff(f133,plain,
! [X1: set_vertex,X0: set_vertex,X3: vertex1,X2: set_vertex] :
( ( closure1(X1,X2,X0,X3)
| ( ~ mem(vertex,t2tb1(X3),t2tb(X2))
& ? [X4: vertex1] :
( ~ mem(vertex,t2tb1(X4),t2tb(X1))
& mem(vertex,t2tb1(X4),t2tb(succ1(X3))) )
& mem(vertex,t2tb1(X3),t2tb(X1))
& ~ mem(vertex,t2tb1(X3),t2tb(X0)) ) )
& ( mem(vertex,t2tb1(X3),t2tb(X2))
| ! [X4: vertex1] :
( mem(vertex,t2tb1(X4),t2tb(X1))
| ~ mem(vertex,t2tb1(X4),t2tb(succ1(X3))) )
| ~ mem(vertex,t2tb1(X3),t2tb(X1))
| mem(vertex,t2tb1(X3),t2tb(X0))
| ~ closure1(X1,X2,X0,X3) ) ),
inference(nnf_transformation,[],[f95]) ).
tff(f134,plain,
! [X1: set_vertex,X0: set_vertex,X3: vertex1,X2: set_vertex] :
( ( closure1(X1,X2,X0,X3)
| ( ~ mem(vertex,t2tb1(X3),t2tb(X2))
& ? [X4: vertex1] :
( ~ mem(vertex,t2tb1(X4),t2tb(X1))
& mem(vertex,t2tb1(X4),t2tb(succ1(X3))) )
& mem(vertex,t2tb1(X3),t2tb(X1))
& ~ mem(vertex,t2tb1(X3),t2tb(X0)) ) )
& ( mem(vertex,t2tb1(X3),t2tb(X2))
| ! [X4: vertex1] :
( mem(vertex,t2tb1(X4),t2tb(X1))
| ~ mem(vertex,t2tb1(X4),t2tb(succ1(X3))) )
| ~ mem(vertex,t2tb1(X3),t2tb(X1))
| mem(vertex,t2tb1(X3),t2tb(X0))
| ~ closure1(X1,X2,X0,X3) ) ),
inference(flattening,[],[f133]) ).
tff(f135,plain,
! [X0: set_vertex,X1: set_vertex,X2: vertex1,X3: set_vertex] :
( ( closure1(X0,X3,X1,X2)
| ( ~ mem(vertex,t2tb1(X2),t2tb(X3))
& ? [X4: vertex1] :
( ~ mem(vertex,t2tb1(X4),t2tb(X0))
& mem(vertex,t2tb1(X4),t2tb(succ1(X2))) )
& mem(vertex,t2tb1(X2),t2tb(X0))
& ~ mem(vertex,t2tb1(X2),t2tb(X1)) ) )
& ( mem(vertex,t2tb1(X2),t2tb(X3))
| ! [X5: vertex1] :
( mem(vertex,t2tb1(X5),t2tb(X0))
| ~ mem(vertex,t2tb1(X5),t2tb(succ1(X2))) )
| ~ mem(vertex,t2tb1(X2),t2tb(X0))
| mem(vertex,t2tb1(X2),t2tb(X1))
| ~ closure1(X0,X3,X1,X2) ) ),
inference(rectify,[],[f134]) ).
tff(f136,plain,
! [X0: set_vertex,X1: set_vertex,X2: vertex1,X3: set_vertex] :
( ( closure1(X0,X3,X1,X2)
| ( ~ mem(vertex,t2tb1(X2),t2tb(X3))
& ~ mem(vertex,t2tb1(sK9(X0,X2)),t2tb(X0))
& mem(vertex,t2tb1(sK9(X0,X2)),t2tb(succ1(X2)))
& mem(vertex,t2tb1(X2),t2tb(X0))
& ~ mem(vertex,t2tb1(X2),t2tb(X1)) ) )
& ( mem(vertex,t2tb1(X2),t2tb(X3))
| ! [X5: vertex1] :
( mem(vertex,t2tb1(X5),t2tb(X0))
| ~ mem(vertex,t2tb1(X5),t2tb(succ1(X2))) )
| ~ mem(vertex,t2tb1(X2),t2tb(X0))
| mem(vertex,t2tb1(X2),t2tb(X1))
| ~ closure1(X0,X3,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X4,sK9(X0,X2))],[f135]) ).
tff(f140,plain,
? [X0: vertex1,X3: set_vertex,X2: vertex1,X5: $int,X4: set_vertex,X1: set_vertex] :
( ? [X7: bool1] :
( ? [X9: set_vertex,X8: vertex1] :
( shortest_path1(X2,X8,X5)
& inv1(X2,X0,X1,X9,X4,X5)
& ! [X10: vertex1] :
( closure1(X1,X9,X4,X10)
| ( X8 = X10 ) )
& ( tb2t(remove(vertex,t2tb1(X8),t2tb(X3))) = X9 )
& ( X0 != X8 )
& mem(vertex,t2tb1(X8),t2tb(X3))
& ? [X12: set_vertex,X11: set_vertex] :
( inv1(X2,X0,X12,X9,X11,X5)
& ? [X14: bool1] :
( ? [X15: set_vertex] :
( ? [X16: set_vertex] :
( ( tb2t(empty(vertex)) = X16 )
& ? [X17: $int] :
( ( $sum(X5,1) = X17 )
& ? [X18: vertex1] : ~ closure1(X12,X15,X16,X18) ) )
& ( X11 = X15 ) )
& ( true1 = X14 )
& ( is_empty(vertex,t2tb(X9))
| ( true1 != X14 ) )
& ( ( true1 = X14 )
| ~ is_empty(vertex,t2tb(X9)) ) )
& ! [X13: vertex1] : closure1(X12,X9,X11,X13)
& subset(vertex,t2tb(succ1(X8)),t2tb(X12)) ) )
& ~ is_empty(vertex,t2tb(X3))
& ( is_empty(vertex,t2tb(X3))
| ( true1 != X7 ) )
& ( ( X7 = true1 )
| ~ is_empty(vertex,t2tb(X3)) )
& ( X7 != true1 ) )
& inv1(X2,X0,X1,X3,X4,X5)
& ( is_empty(vertex,t2tb(X4))
| ~ is_empty(vertex,t2tb(X3)) )
& ~ $less(X5,0)
& ! [X6: vertex1] : closure1(X1,X3,X4,X6) ),
inference(nnf_transformation,[],[f99]) ).
tff(f141,plain,
? [X0: vertex1,X3: set_vertex,X2: vertex1,X5: $int,X4: set_vertex,X1: set_vertex] :
( ? [X7: bool1] :
( ? [X9: set_vertex,X8: vertex1] :
( shortest_path1(X2,X8,X5)
& inv1(X2,X0,X1,X9,X4,X5)
& ! [X10: vertex1] :
( closure1(X1,X9,X4,X10)
| ( X8 = X10 ) )
& ( tb2t(remove(vertex,t2tb1(X8),t2tb(X3))) = X9 )
& ( X0 != X8 )
& mem(vertex,t2tb1(X8),t2tb(X3))
& ? [X12: set_vertex,X11: set_vertex] :
( inv1(X2,X0,X12,X9,X11,X5)
& ? [X14: bool1] :
( ? [X15: set_vertex] :
( ? [X16: set_vertex] :
( ( tb2t(empty(vertex)) = X16 )
& ? [X17: $int] :
( ( $sum(X5,1) = X17 )
& ? [X18: vertex1] : ~ closure1(X12,X15,X16,X18) ) )
& ( X11 = X15 ) )
& ( true1 = X14 )
& ( is_empty(vertex,t2tb(X9))
| ( true1 != X14 ) )
& ( ( true1 = X14 )
| ~ is_empty(vertex,t2tb(X9)) ) )
& ! [X13: vertex1] : closure1(X12,X9,X11,X13)
& subset(vertex,t2tb(succ1(X8)),t2tb(X12)) ) )
& ~ is_empty(vertex,t2tb(X3))
& ( is_empty(vertex,t2tb(X3))
| ( true1 != X7 ) )
& ( ( X7 = true1 )
| ~ is_empty(vertex,t2tb(X3)) )
& ( X7 != true1 ) )
& inv1(X2,X0,X1,X3,X4,X5)
& ( is_empty(vertex,t2tb(X4))
| ~ is_empty(vertex,t2tb(X3)) )
& ~ $less(X5,0)
& ! [X6: vertex1] : closure1(X1,X3,X4,X6) ),
inference(flattening,[],[f140]) ).
tff(f142,plain,
? [X0: vertex1,X1: set_vertex,X2: vertex1,X3: $int,X4: set_vertex,X5: set_vertex] :
( ? [X6: bool1] :
( ? [X7: set_vertex,X8: vertex1] :
( shortest_path1(X2,X8,X3)
& inv1(X2,X0,X5,X7,X4,X3)
& ! [X9: vertex1] :
( closure1(X5,X7,X4,X9)
| ( X8 = X9 ) )
& ( tb2t(remove(vertex,t2tb1(X8),t2tb(X1))) = X7 )
& ( X0 != X8 )
& mem(vertex,t2tb1(X8),t2tb(X1))
& ? [X10: set_vertex,X11: set_vertex] :
( inv1(X2,X0,X10,X7,X11,X3)
& ? [X12: bool1] :
( ? [X13: set_vertex] :
( ? [X14: set_vertex] :
( ( tb2t(empty(vertex)) = X14 )
& ? [X15: $int] :
( ( $sum(X3,1) = X15 )
& ? [X16: vertex1] : ~ closure1(X10,X13,X14,X16) ) )
& ( X11 = X13 ) )
& ( true1 = X12 )
& ( is_empty(vertex,t2tb(X7))
| ( true1 != X12 ) )
& ( ( true1 = X12 )
| ~ is_empty(vertex,t2tb(X7)) ) )
& ! [X17: vertex1] : closure1(X10,X7,X11,X17)
& subset(vertex,t2tb(succ1(X8)),t2tb(X10)) ) )
& ~ is_empty(vertex,t2tb(X1))
& ( is_empty(vertex,t2tb(X1))
| ( true1 != X6 ) )
& ( ( true1 = X6 )
| ~ is_empty(vertex,t2tb(X1)) )
& ( true1 != X6 ) )
& inv1(X2,X0,X5,X1,X4,X3)
& ( is_empty(vertex,t2tb(X4))
| ~ is_empty(vertex,t2tb(X1)) )
& ~ $less(X3,0)
& ! [X18: vertex1] : closure1(X5,X1,X4,X18) ),
inference(rectify,[],[f141]) ).
tff(f143,plain,
( shortest_path1(sK12,sK18,sK13)
& inv1(sK12,sK10,sK15,sK17,sK14,sK13)
& ! [X9: vertex1] :
( closure1(sK15,sK17,sK14,X9)
| ( sK18 = X9 ) )
& ( sK17 = tb2t(remove(vertex,t2tb1(sK18),t2tb(sK11))) )
& ( sK10 != sK18 )
& mem(vertex,t2tb1(sK18),t2tb(sK11))
& inv1(sK12,sK10,sK19,sK17,sK20,sK13)
& ( tb2t(empty(vertex)) = sK23 )
& ( $sum(sK13,1) = sK24 )
& ~ closure1(sK19,sK22,sK23,sK25)
& ( sK20 = sK22 )
& ( true1 = sK21 )
& ( is_empty(vertex,t2tb(sK17))
| ( true1 != sK21 ) )
& ( ( true1 = sK21 )
| ~ is_empty(vertex,t2tb(sK17)) )
& ! [X17: vertex1] : closure1(sK19,sK17,sK20,X17)
& subset(vertex,t2tb(succ1(sK18)),t2tb(sK19))
& ~ is_empty(vertex,t2tb(sK11))
& ( is_empty(vertex,t2tb(sK11))
| ( true1 != sK16 ) )
& ( ( true1 = sK16 )
| ~ is_empty(vertex,t2tb(sK11)) )
& ( true1 != sK16 )
& inv1(sK12,sK10,sK15,sK11,sK14,sK13)
& ( is_empty(vertex,t2tb(sK14))
| ~ is_empty(vertex,t2tb(sK11)) )
& ~ $less(sK13,0)
& ! [X18: vertex1] : closure1(sK15,sK11,sK14,X18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12),skolemize(X3,sK13),skolemize(X4,sK14),skolemize(X5,sK15),skolemize(X6,sK16),skolemize(X7,sK17),skolemize(X8,sK18),skolemize(X10,sK19),skolemize(X11,sK20),skolemize(X12,sK21),skolemize(X13,sK22),skolemize(X14,sK23),skolemize(X15,sK24),skolemize(X16,sK25)],[f142]) ).
tff(f160,plain,
! [X0: ty,X1: uni] :
( ( is_empty(X0,X1)
| ? [X2: uni] :
( sort1(X0,X2)
& mem(X0,X2,X1) ) )
& ( ~ is_empty(X0,X1)
| ! [X3: uni] : ~ mem(X0,X3,X1) ) ),
inference(rectify,[],[f93]) ).
tff(f161,plain,
! [X0: ty,X1: uni] :
( ( is_empty(X0,X1)
| ( sort1(X0,sK30(X0,X1))
& mem(X0,sK30(X0,X1),X1) ) )
& ( ~ is_empty(X0,X1)
| ! [X3: uni] : ~ mem(X0,X3,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(X2,sK30(X0,X1))],[f160]) ).
tff(f184,plain,
! [X2: vertex1,X3: set_vertex,X0: set_vertex,X1: set_vertex,X5: vertex1] :
( ~ mem(vertex,t2tb1(X5),t2tb(succ1(X2)))
| mem(vertex,t2tb1(X2),t2tb(X1))
| mem(vertex,t2tb1(X2),t2tb(X3))
| ~ closure1(X0,X3,X1,X2)
| mem(vertex,t2tb1(X5),t2tb(X0))
| ~ mem(vertex,t2tb1(X2),t2tb(X0)) ),
inference(cnf_transformation,[],[f136]) ).
tff(f186,plain,
! [X2: vertex1,X3: set_vertex,X0: set_vertex,X1: set_vertex] :
( mem(vertex,t2tb1(X2),t2tb(X0))
| closure1(X0,X3,X1,X2) ),
inference(cnf_transformation,[],[f136]) ).
tff(f187,plain,
! [X2: vertex1,X3: set_vertex,X0: set_vertex,X1: set_vertex] :
( mem(vertex,t2tb1(sK9(X0,X2)),t2tb(succ1(X2)))
| closure1(X0,X3,X1,X2) ),
inference(cnf_transformation,[],[f136]) ).
tff(f188,plain,
! [X2: vertex1,X3: set_vertex,X0: set_vertex,X1: set_vertex] :
( ~ mem(vertex,t2tb1(sK9(X0,X2)),t2tb(X0))
| closure1(X0,X3,X1,X2) ),
inference(cnf_transformation,[],[f136]) ).
tff(f189,plain,
! [X2: vertex1,X3: set_vertex,X0: set_vertex,X1: set_vertex] :
( ~ mem(vertex,t2tb1(X2),t2tb(X3))
| closure1(X0,X3,X1,X2) ),
inference(cnf_transformation,[],[f136]) ).
tff(f204,plain,
! [X17: vertex1] : closure1(sK19,sK17,sK20,X17),
inference(cnf_transformation,[],[f143]) ).
tff(f206,plain,
( is_empty(vertex,t2tb(sK17))
| ( true1 != sK21 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f207,plain,
true1 = sK21,
inference(cnf_transformation,[],[f143]) ).
tff(f208,plain,
sK20 = sK22,
inference(cnf_transformation,[],[f143]) ).
tff(f209,plain,
~ closure1(sK19,sK22,sK23,sK25),
inference(cnf_transformation,[],[f143]) ).
tff(f244,plain,
! [X3: uni,X0: ty,X1: uni] :
( ~ mem(X0,X3,X1)
| ~ is_empty(X0,X1) ),
inference(cnf_transformation,[],[f161]) ).
tff(f249,plain,
( ( sK21 != sK21 )
| is_empty(vertex,t2tb(sK17)) ),
inference(definition_unfolding,[],[f206,f207]) ).
tff(f251,plain,
! [X17: vertex1] : closure1(sK19,sK17,sK22,X17),
inference(definition_unfolding,[],[f204,f208]) ).
tff(f257,plain,
is_empty(vertex,t2tb(sK17)),
inference(trivial_inequality_removal,[],[f249]) ).
tff(f321,definition,
( spl31_13
<=> is_empty(vertex,t2tb(sK17)) ),
introduced(definition,[new_symbols(definition,[spl31_13])],[avatar_definition]) ).
tff(f323,plain,
( is_empty(vertex,t2tb(sK17))
| ~ spl31_13 ),
inference(avatar_component_clause,[],[f321]) ).
tff(f324,plain,
spl31_13,
inference(avatar_split_clause,[],[f257,f321]) ).
tff(f331,definition,
( spl31_15
<=> closure1(sK19,sK22,sK23,sK25) ),
introduced(definition,[new_symbols(definition,[spl31_15])],[avatar_definition]) ).
tff(f333,plain,
( ~ closure1(sK19,sK22,sK23,sK25)
| spl31_15 ),
inference(avatar_component_clause,[],[f331]) ).
tff(f334,plain,
~ spl31_15,
inference(avatar_split_clause,[],[f209,f331]) ).
tff(f366,plain,
( ! [X0: uni] : ~ mem(vertex,X0,t2tb(sK17))
| ~ spl31_13 ),
inference(unit_resulting_resolution,[],[f244,f323]) ).
tff(f381,plain,
( ~ mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(sK19))
| spl31_15 ),
inference(unit_resulting_resolution,[],[f188,f333]) ).
tff(f382,plain,
( mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(succ1(sK25)))
| spl31_15 ),
inference(unit_resulting_resolution,[],[f187,f333]) ).
tff(f384,plain,
( ~ mem(vertex,t2tb1(sK25),t2tb(sK22))
| spl31_15 ),
inference(unit_resulting_resolution,[],[f189,f333]) ).
tff(f385,plain,
( mem(vertex,t2tb1(sK25),t2tb(sK19))
| spl31_15 ),
inference(unit_resulting_resolution,[],[f186,f333]) ).
tff(f388,definition,
( spl31_23
<=> mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(succ1(sK25))) ),
introduced(definition,[new_symbols(definition,[spl31_23])],[avatar_definition]) ).
tff(f390,plain,
( mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(succ1(sK25)))
| ~ spl31_23 ),
inference(avatar_component_clause,[],[f388]) ).
tff(f391,plain,
( spl31_23
| spl31_15 ),
inference(avatar_split_clause,[],[f382,f331,f388]) ).
tff(f393,definition,
( spl31_24
<=> mem(vertex,t2tb1(sK25),t2tb(sK19)) ),
introduced(definition,[new_symbols(definition,[spl31_24])],[avatar_definition]) ).
tff(f395,plain,
( mem(vertex,t2tb1(sK25),t2tb(sK19))
| ~ spl31_24 ),
inference(avatar_component_clause,[],[f393]) ).
tff(f396,plain,
( spl31_24
| spl31_15 ),
inference(avatar_split_clause,[],[f385,f331,f393]) ).
tff(f403,definition,
( spl31_26
<=> mem(vertex,t2tb1(sK25),t2tb(sK22)) ),
introduced(definition,[new_symbols(definition,[spl31_26])],[avatar_definition]) ).
tff(f405,plain,
( ~ mem(vertex,t2tb1(sK25),t2tb(sK22))
| spl31_26 ),
inference(avatar_component_clause,[],[f403]) ).
tff(f406,plain,
( ~ spl31_26
| spl31_15 ),
inference(avatar_split_clause,[],[f384,f331,f403]) ).
tff(f409,definition,
( spl31_27
<=> mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(sK19)) ),
introduced(definition,[new_symbols(definition,[spl31_27])],[avatar_definition]) ).
tff(f411,plain,
( ~ mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(sK19))
| spl31_27 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
( ~ spl31_27
| spl31_15 ),
inference(avatar_split_clause,[],[f381,f331,f409]) ).
tff(f985,plain,
( ~ mem(vertex,t2tb1(sK9(sK19,sK25)),t2tb(succ1(sK25)))
| ~ spl31_13
| ~ spl31_24
| spl31_26
| spl31_27 ),
inference(unit_resulting_resolution,[],[f184,f251,f366,f405,f395,f411]) ).
tff(f1015,plain,
( $false
| ~ spl31_13
| ~ spl31_23
| ~ spl31_24
| spl31_26
| spl31_27 ),
inference(forward_subsumption_resolution,[],[f985,f390]) ).
tff(f1016,plain,
( ~ spl31_13
| ~ spl31_23
| ~ spl31_24
| spl31_26
| spl31_27 ),
inference(avatar_contradiction_clause,[],[f1015]) ).
tff(f1017,plain,
$false,
inference(avatar_smt_refutation,[],[f1016,f412,f406,f396,f391,f334,f324]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW672_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 % Computer : n015.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 14:27:47 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.28 Running first-order theorem proving
% 0.25/0.28 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
% 5.23/1.76 % (2666514)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.23/1.76 % (2666522)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=688072314:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.23/1.76 % (2666522)Instruction limit reached!
% 5.23/1.76 % (2666522)------------------------------
% 5.23/1.76 % (2666522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.76 % (2666522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.76 % (2666522)CaDiCaL version: 2.1.3
% 5.23/1.76 % (2666522)Termination reason: Instruction limit
% 5.23/1.76 % (2666522)Termination phase: Saturation
% 5.23/1.76 % (2666522)Time elapsed: 0.005 s
% 5.23/1.76 % (2666522)Peak memory usage: 88 MB
% 5.23/1.76 % (2666522)Instructions burned: 8 (million)
% 5.23/1.76 % (2666519)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3719750896:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.23/1.76 % (2666520)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3296610778:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.23/1.76 % (2666519)Instruction limit reached!
% 5.23/1.76 % (2666519)------------------------------
% 5.23/1.76 % (2666519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.76 % (2666519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.76 % (2666519)CaDiCaL version: 2.1.3
% 5.23/1.76 % (2666519)Termination reason: Instruction limit
% 5.23/1.76 % (2666519)Termination phase: Saturation
% 5.23/1.76 % (2666519)Time elapsed: 0.039 s
% 5.23/1.76 % (2666519)Peak memory usage: 112 MB
% 5.23/1.76 % (2666519)Instructions burned: 12 (million)
% 5.23/1.76 % (2666525)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2389696782:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.23/1.76 % (2666521)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=353630966:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.23/1.76 % (2666523)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1091987663:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.23/1.76 % (2666523)Instruction limit reached!
% 5.23/1.76 % (2666523)------------------------------
% 5.23/1.76 % (2666523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.76 % (2666523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.76 % (2666523)CaDiCaL version: 2.1.3
% 5.23/1.76 % (2666523)Termination reason: Instruction limit
% 5.23/1.76 % (2666523)Termination phase: Property scanning
% 5.23/1.76 % (2666523)Time elapsed: 0.005 s
% 5.23/1.76 % (2666523)Peak memory usage: 86 MB
% 5.23/1.76 % (2666523)Instructions burned: 4 (million)
% 5.23/1.76 % (2666524)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3939339854:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.23/1.76 % (2666525)Instruction limit reached!
% 5.23/1.76 % (2666525)------------------------------
% 5.23/1.76 % (2666525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.76 % (2666525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.76 % (2666525)CaDiCaL version: 2.1.3
% 5.23/1.76 % (2666525)Termination reason: Instruction limit
% 5.23/1.76 % (2666525)Termination phase: Saturation
% 5.23/1.76 % (2666525)Time elapsed: 0.065 s
% 5.23/1.76 % (2666525)Peak memory usage: 116 MB
% 5.23/1.76 % (2666525)Instructions burned: 34 (million)
% 5.23/1.76 % (2666524)Instruction limit reached!
% 5.23/1.76 % (2666524)------------------------------
% 5.23/1.76 % (2666524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.76 % (2666524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.76 % (2666524)CaDiCaL version: 2.1.3
% 5.23/1.76 % (2666524)Termination reason: Instruction limit
% 5.23/1.76 % (2666524)Termination phase: Saturation
% 5.23/1.76 % (2666524)Time elapsed: 0.071 s
% 5.23/1.76 % (2666524)Peak memory usage: 116 MB
% 5.23/1.76 % (2666524)Instructions burned: 46 (million)
% 5.23/1.76 % (2666527)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1594025503:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.23/1.76 % (2666527)Instruction limit reached!
% 5.23/1.76 % (2666527)------------------------------
% 6.98/1.98 % (2666527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.98/1.98 % (2666527)CaDiCaL version: 2.1.3
% 6.98/1.98 % (2666527)Termination reason: Instruction limit
% 6.98/1.98 % (2666527)Termination phase: Saturation
% 6.98/1.98 % (2666527)Time elapsed: 0.008 s
% 6.98/1.98 % (2666527)Peak memory usage: 88 MB
% 6.98/1.98 % (2666527)Instructions burned: 15 (million)
% 6.98/1.98 % (2666521)Instruction limit reached!
% 6.98/1.98 % (2666521)------------------------------
% 6.98/1.98 % (2666521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.98/1.98 % (2666521)CaDiCaL version: 2.1.3
% 6.98/1.98 % (2666521)Termination reason: Instruction limit
% 6.98/1.98 % (2666521)Termination phase: Saturation
% 6.98/1.98 % (2666521)Time elapsed: 0.224 s
% 6.98/1.98 % (2666521)Peak memory usage: 117 MB
% 6.98/1.98 % (2666521)Instructions burned: 202 (million)
% 6.98/1.98 % (2666530)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=588157535:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.98/1.98 % (2666520)Instruction limit reached!
% 6.98/1.98 % (2666520)------------------------------
% 6.98/1.98 % (2666520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.98/1.98 % (2666520)CaDiCaL version: 2.1.3
% 6.98/1.98 % (2666520)Termination reason: Instruction limit
% 6.98/1.98 % (2666520)Termination phase: Saturation
% 6.98/1.98 % (2666520)Time elapsed: 0.322 s
% 6.98/1.98 % (2666520)Peak memory usage: 117 MB
% 6.98/1.98 % (2666520)Instructions burned: 307 (million)
% 6.98/1.98 % (2666530)Instruction limit reached!
% 6.98/1.98 % (2666530)------------------------------
% 6.98/1.98 % (2666530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.98/1.98 % (2666530)CaDiCaL version: 2.1.3
% 6.98/1.98 % (2666530)Termination reason: Instruction limit
% 6.98/1.98 % (2666530)Termination phase: Saturation
% 6.98/1.98 % (2666530)Time elapsed: 0.036 s
% 6.98/1.98 % (2666530)Peak memory usage: 89 MB
% 6.98/1.98 % (2666530)Instructions burned: 29 (million)
% 6.98/1.98 % (2666534)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=521558498:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.98/1.98 % (2666537)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=1344058085:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.98/1.98 % (2666534)Instruction limit reached!
% 6.98/1.98 % (2666534)------------------------------
% 6.98/1.98 % (2666534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.98/1.98 % (2666534)CaDiCaL version: 2.1.3
% 6.98/1.98 % (2666534)Termination reason: Instruction limit
% 6.98/1.98 % (2666534)Termination phase: Saturation
% 6.98/1.98 % (2666534)Time elapsed: 0.017 s
% 6.98/1.98 % (2666534)Peak memory usage: 88 MB
% 6.98/1.98 % (2666534)Instructions burned: 17 (million)
% 6.98/1.98 % (2666536)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2485031134:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.98/1.98 % (2666537)Instruction limit reached!
% 6.98/1.98 % (2666537)------------------------------
% 6.98/1.98 % (2666537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.98/1.98 % (2666537)CaDiCaL version: 2.1.3
% 6.98/1.98 % (2666537)Termination reason: Instruction limit
% 6.98/1.98 % (2666537)Termination phase: Saturation
% 6.98/1.98 % (2666537)Time elapsed: 0.023 s
% 6.98/1.98 % (2666537)Peak memory usage: 90 MB
% 6.98/1.98 % (2666537)Instructions burned: 27 (million)
% 6.98/1.98 % (2666536)Instruction limit reached!
% 6.98/1.98 % (2666536)------------------------------
% 6.98/1.98 % (2666536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.98/1.98 % (2666536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.21 % (2666536)CaDiCaL version: 2.1.3
% 9.56/2.21 % (2666536)Termination reason: Instruction limit
% 9.56/2.21 % (2666536)Termination phase: Saturation
% 9.56/2.21 % (2666536)Time elapsed: 0.026 s
% 9.56/2.21 % (2666536)Peak memory usage: 89 MB
% 9.56/2.21 % (2666536)Instructions burned: 25 (million)
% 9.56/2.21 % (2666539)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3857472820:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 9.56/2.21 % (2666541)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2935076934:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 9.56/2.21 % (2666541)Instruction limit reached!
% 9.56/2.21 % (2666541)------------------------------
% 9.56/2.21 % (2666541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/2.21 % (2666541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.21 % (2666541)CaDiCaL version: 2.1.3
% 9.56/2.21 % (2666541)Termination reason: Instruction limit
% 9.56/2.21 % (2666541)Termination phase: Preprocessing 3
% 9.56/2.21 % (2666541)Time elapsed: 0.002 s
% 9.56/2.21 % (2666541)Peak memory usage: 86 MB
% 9.56/2.21 % (2666541)Instructions burned: 3 (million)
% 9.56/2.21 % (2666547)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1733983629:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.56/2.21 % (2666539)Instruction limit reached!
% 9.56/2.21 % (2666539)------------------------------
% 9.56/2.21 % (2666539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/2.21 % (2666539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.21 % (2666539)CaDiCaL version: 2.1.3
% 9.56/2.21 % (2666539)Termination reason: Instruction limit
% 9.56/2.21 % (2666539)Termination phase: Saturation
% 9.56/2.21 % (2666539)Time elapsed: 0.081 s
% 9.56/2.21 % (2666539)Peak memory usage: 89 MB
% 9.56/2.21 % (2666539)Instructions burned: 86 (million)
% 9.56/2.21 % (2666545)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3415918250:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.56/2.21 % (2666544)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3428904835:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.56/2.21 % (2666545)Instruction limit reached!
% 9.56/2.21 % (2666545)------------------------------
% 9.56/2.21 % (2666545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/2.21 % (2666545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.21 % (2666545)CaDiCaL version: 2.1.3
% 9.56/2.21 % (2666545)Termination reason: Instruction limit
% 9.56/2.21 % (2666545)Termination phase: Property scanning
% 9.56/2.21 % (2666545)Time elapsed: 0.005 s
% 9.56/2.21 % (2666545)Peak memory usage: 86 MB
% 9.56/2.21 % (2666545)Instructions burned: 4 (million)
% 9.56/2.21 % (2666548)lrs+10_1_thi=all:si=on:fd=off:random_seed=4180606779:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 9.56/2.21 % (2666547)Instruction limit reached!
% 9.56/2.21 % (2666547)------------------------------
% 9.56/2.21 % (2666547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/2.21 % (2666547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.21 % (2666547)CaDiCaL version: 2.1.3
% 9.56/2.21 % (2666547)Termination reason: Instruction limit
% 9.56/2.21 % (2666547)Termination phase: Saturation
% 9.56/2.21 % (2666547)Time elapsed: 0.110 s
% 9.56/2.21 % (2666547)Peak memory usage: 133 MB
% 9.56/2.21 % (2666547)Instructions burned: 67 (million)
% 9.56/2.21 % (2666549)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=1564091062:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 9.56/2.21 % (2666549)Instruction limit reached!
% 9.56/2.21 % (2666549)------------------------------
% 9.56/2.21 % (2666549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/2.21 % (2666549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.21 % (2666549)CaDiCaL version: 2.1.3
% 9.56/2.21 % (2666549)Termination reason: Instruction limit
% 9.56/2.21 % (2666549)Termination phase: Property scanning
% 9.56/2.21 % (2666549)Time elapsed: 0.008 s
% 9.56/2.21 % (2666549)Peak memory usage: 87 MB
% 9.56/2.21 % (2666549)Instructions burned: 8 (million)
% 9.56/2.21 % (2666548)Instruction limit reached!
% 10.81/2.60 % (2666548)------------------------------
% 10.81/2.60 % (2666548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.60 % (2666548)CaDiCaL version: 2.1.3
% 10.81/2.60 % (2666548)Termination reason: Instruction limit
% 10.81/2.60 % (2666548)Termination phase: Saturation
% 10.81/2.60 % (2666548)Time elapsed: 0.078 s
% 10.81/2.60 % (2666548)Peak memory usage: 115 MB
% 10.81/2.60 % (2666548)Instructions burned: 54 (million)
% 10.81/2.60 % (2666555)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3412199760:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.81/2.60 % (2666552)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4292356727:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 10.81/2.60 % (2666555)Instruction limit reached!
% 10.81/2.60 % (2666555)------------------------------
% 10.81/2.60 % (2666555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.60 % (2666555)CaDiCaL version: 2.1.3
% 10.81/2.60 % (2666555)Termination reason: Instruction limit
% 10.81/2.60 % (2666555)Termination phase: shuffling
% 10.81/2.60 % (2666555)Time elapsed: 0.002 s
% 10.81/2.60 % (2666555)Peak memory usage: 85 MB
% 10.81/2.60 % (2666555)Instructions burned: 2 (million)
% 10.81/2.60 % (2666552)Instruction limit reached!
% 10.81/2.60 % (2666552)------------------------------
% 10.81/2.60 % (2666552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.60 % (2666552)CaDiCaL version: 2.1.3
% 10.81/2.60 % (2666552)Termination reason: Instruction limit
% 10.81/2.60 % (2666552)Termination phase: Naming
% 10.81/2.60 % (2666552)Time elapsed: 0.003 s
% 10.81/2.60 % (2666552)Peak memory usage: 85 MB
% 10.81/2.60 % (2666552)Instructions burned: 2 (million)
% 10.81/2.60 % (2666544)Instruction limit reached!
% 10.81/2.60 % (2666544)------------------------------
% 10.81/2.60 % (2666544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.60 % (2666544)CaDiCaL version: 2.1.3
% 10.81/2.60 % (2666544)Termination reason: Instruction limit
% 10.81/2.60 % (2666544)Termination phase: Saturation
% 10.81/2.60 % (2666544)Time elapsed: 0.199 s
% 10.81/2.60 % (2666544)Peak memory usage: 91 MB
% 10.81/2.60 % (2666544)Instructions burned: 181 (million)
% 10.81/2.60 % (2666557)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3664801532:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 10.81/2.60 % (2666557)Instruction limit reached!
% 10.81/2.60 % (2666557)------------------------------
% 10.81/2.60 % (2666557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.60 % (2666557)CaDiCaL version: 2.1.3
% 10.81/2.60 % (2666557)Termination reason: Instruction limit
% 10.81/2.60 % (2666557)Termination phase: Saturation
% 10.81/2.60 % (2666557)Time elapsed: 0.095 s
% 10.81/2.60 % (2666557)Peak memory usage: 117 MB
% 10.81/2.60 % (2666557)Instructions burned: 128 (million)
% 10.81/2.60 % (2666561)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1531068393:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 10.81/2.60 % (2666561)Instruction limit reached!
% 10.81/2.60 % (2666561)------------------------------
% 10.81/2.60 % (2666561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.60 % (2666561)CaDiCaL version: 2.1.3
% 10.81/2.60 % (2666561)Termination reason: Instruction limit
% 10.81/2.60 % (2666561)Termination phase: Saturation
% 10.81/2.60 % (2666561)Time elapsed: 0.025 s
% 10.81/2.60 % (2666561)Peak memory usage: 89 MB
% 10.81/2.60 % (2666561)Instructions burned: 26 (million)
% 10.81/2.60 % (2666560)dis+10_1_si=on:random_seed=2868095882:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 10.81/2.60 % (2666560)Instruction limit reached!
% 10.81/2.60 % (2666560)------------------------------
% 10.81/2.60 % (2666560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.60 % (2666560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666560)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666560)Termination reason: Instruction limit
% 12.10/2.78 % (2666560)Termination phase: Saturation
% 12.10/2.78 % (2666560)Time elapsed: 0.013 s
% 12.10/2.78 % (2666560)Peak memory usage: 89 MB
% 12.10/2.78 % (2666560)Instructions burned: 10 (million)
% 12.10/2.78 % (2666566)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3668778686:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 12.10/2.78 % (2666562)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=734062854: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_2990 on theBenchmark for (2990ds/35Mi)
% 12.10/2.78 % (2666566)Instruction limit reached!
% 12.10/2.78 % (2666566)------------------------------
% 12.10/2.78 % (2666566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666566)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666566)Termination reason: Instruction limit
% 12.10/2.78 % (2666566)Termination phase: Saturation
% 12.10/2.78 % (2666566)Time elapsed: 0.013 s
% 12.10/2.78 % (2666566)Peak memory usage: 88 MB
% 12.10/2.78 % (2666566)Instructions burned: 8 (million)
% 12.10/2.78 % (2666562)Instruction limit reached!
% 12.10/2.78 % (2666562)------------------------------
% 12.10/2.78 % (2666562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666562)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666562)Termination reason: Instruction limit
% 12.10/2.78 % (2666562)Termination phase: Saturation
% 12.10/2.78 % (2666562)Time elapsed: 0.039 s
% 12.10/2.78 % (2666562)Peak memory usage: 89 MB
% 12.10/2.78 % (2666562)Instructions burned: 35 (million)
% 12.10/2.78 % (2666565)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2747783889:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 12.10/2.78 % (2666565)Instruction limit reached!
% 12.10/2.78 % (2666565)------------------------------
% 12.10/2.78 % (2666565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666565)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666565)Termination reason: Instruction limit
% 12.10/2.78 % (2666565)Termination phase: Preprocessing 3
% 12.10/2.78 % (2666565)Time elapsed: 0.003 s
% 12.10/2.78 % (2666565)Peak memory usage: 86 MB
% 12.10/2.78 % (2666565)Instructions burned: 2 (million)
% 12.10/2.78 % (2666568)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3260631903:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 12.10/2.78 % (2666569)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2307442563:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 12.10/2.78 % (2666576)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1224580509:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 12.10/2.78 % (2666573)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1348275208:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 12.10/2.78 % (2666572)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2591935367:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 12.10/2.78 % (2666569)Instruction limit reached!
% 12.10/2.78 % (2666569)------------------------------
% 12.10/2.78 % (2666569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666569)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666569)Termination reason: Instruction limit
% 12.10/2.78 % (2666569)Termination phase: Saturation
% 12.10/2.78 % (2666569)Time elapsed: 0.042 s
% 12.10/2.78 % (2666569)Peak memory usage: 112 MB
% 12.10/2.78 % (2666569)Instructions burned: 13 (million)
% 12.10/2.78 % (2666577)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=3456340300:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 12.10/2.78 % (2666573)Instruction limit reached!
% 12.10/2.78 % (2666573)------------------------------
% 12.10/2.78 % (2666573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666573)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666573)Termination reason: Instruction limit
% 12.10/2.78 % (2666573)Termination phase: Saturation
% 12.10/2.78 % (2666573)Time elapsed: 0.012 s
% 12.10/2.78 % (2666573)Peak memory usage: 88 MB
% 12.10/2.78 % (2666573)Instructions burned: 10 (million)
% 12.10/2.78 % (2666576)Instruction limit reached!
% 12.10/2.78 % (2666576)------------------------------
% 12.10/2.78 % (2666576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666576)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666576)Termination reason: Instruction limit
% 12.10/2.78 % (2666576)Termination phase: Saturation
% 12.10/2.78 % (2666576)Time elapsed: 0.069 s
% 12.10/2.78 % (2666576)Peak memory usage: 133 MB
% 12.10/2.78 % (2666576)Instructions burned: 74 (million)
% 12.10/2.78 % (2666577)Instruction limit reached!
% 12.10/2.78 % (2666577)------------------------------
% 12.10/2.78 % (2666577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666577)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666577)Termination reason: Instruction limit
% 12.10/2.78 % (2666577)Termination phase: Saturation
% 12.10/2.78 % (2666577)Time elapsed: 0.065 s
% 12.10/2.78 % (2666577)Peak memory usage: 89 MB
% 12.10/2.78 % (2666577)Instructions burned: 80 (million)
% 12.10/2.78 % (2666580)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=1018042949:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 12.10/2.78 % (2666572)First to succeed.
% 12.10/2.78 % (2666572)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2666514"
% 12.10/2.78 % (2666568)Instruction limit reached!
% 12.10/2.78 % (2666568)------------------------------
% 12.10/2.78 % (2666568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666568)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666568)Termination reason: Instruction limit
% 12.10/2.78 % (2666568)Termination phase: Saturation
% 12.10/2.78 % (2666568)Time elapsed: 0.367 s
% 12.10/2.78 % (2666568)Peak memory usage: 93 MB
% 12.10/2.78 % (2666568)Instructions burned: 370 (million)
% 12.10/2.78 % (2666587)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2875242055:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 12.10/2.78 % (2666580)Also succeeded, but the first one will report.
% 12.10/2.78 % (2666586)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1498179859:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi)
% 12.10/2.78 % (2666589)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=410513948:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi)
% 12.10/2.78 % (2666589)Also succeeded, but the first one will report.
% 12.10/2.78 % (2666588)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2466559617:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 12.10/2.78 % (2666586)Instruction limit reached!
% 12.10/2.78 % (2666586)------------------------------
% 12.10/2.78 % (2666586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666586)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666586)Termination reason: Instruction limit
% 12.10/2.78 % (2666586)Termination phase: Saturation
% 12.10/2.78 % (2666586)Time elapsed: 0.140 s
% 12.10/2.78 % (2666586)Peak memory usage: 116 MB
% 12.10/2.78 % (2666586)Instructions burned: 131 (million)
% 12.10/2.78 % (2666587)Instruction limit reached!
% 12.10/2.78 % (2666587)------------------------------
% 12.10/2.78 % (2666587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666587)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666587)Termination reason: Instruction limit
% 12.10/2.78 % (2666587)Termination phase: Saturation
% 12.10/2.78 % (2666587)Time elapsed: 0.163 s
% 12.10/2.78 % (2666587)Peak memory usage: 133 MB
% 12.10/2.78 % (2666587)Instructions burned: 131 (million)
% 12.10/2.78 % (2666588)Instruction limit reached!
% 12.10/2.78 % (2666588)------------------------------
% 12.10/2.78 % (2666588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.78 % (2666588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.78 % (2666588)CaDiCaL version: 2.1.3
% 12.10/2.78 % (2666588)Termination reason: Instruction limit
% 12.10/2.78 % (2666588)Termination phase: Saturation
% 12.10/2.78 % (2666588)Time elapsed: 0.099 s
% 12.10/2.78 % (2666588)Peak memory usage: 134 MB
% 12.10/2.78 % (2666588)Instructions burned: 40 (million)
% 12.10/2.78 % (2666592)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3724106827:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 12.10/2.78 % (2666572)Refutation found. Thanks to Tanya!
% 12.10/2.78 % SZS status Theorem for theBenchmark
% 12.10/2.78 % SZS output start Proof for theBenchmark
% See solution above
% 0.27/3.04 % (2666572)------------------------------
% 0.27/3.04 % (2666572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.27/3.04 % (2666572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.27/3.04 % (2666572)CaDiCaL version: 2.1.3
% 0.27/3.04 % (2666572)Termination reason: Refutation
% 0.27/3.04 % (2666572)Time elapsed: 0.163 s
% 0.27/3.04 % (2666572)Peak memory usage: 118 MB
% 0.27/3.04 % (2666572)Instructions burned: 125 (million)
% 0.27/3.04 % (2666572)------------------------------
% 0.27/3.04 % (2666572)------------------------------
% 0.27/3.04 % (2666514)Success in time 1.916 s
% 0.27/3.04 % Vampire exiting
%------------------------------------------------------------------------------