%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW615_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:57 PM UTC 2026
% Result : Theorem 5.33s 1.53s
% Output : Refutation 6.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 20
% Syntax : Number of formulae : 107 ( 46 unt; 0 typ; 14 def)
% Number of atoms : 337 ( 208 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 315 ( 85 ~; 69 |; 125 &)
% ( 4 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 5 prp; 0-4 aty)
% Number of functors : 86 ( 86 usr; 51 con; 0-5 aty)
% Number of variables : 244 ( 0 sgn 159 !; 85 ?; 244 :)
% 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,
loc: $tType ).
tff(type_def_10,type,
list_loc: $tType ).
tff(type_def_11,type,
map_loc_loc: $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,
list: ty > ty ).
tff(func_def_13,type,
nil: ty > uni ).
tff(func_def_14,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_18,type,
head: ( ty * uni ) > uni ).
tff(func_def_19,type,
tail: ( ty * uni ) > uni ).
tff(func_def_20,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_21,type,
length: ( ty * uni ) > $int ).
tff(func_def_24,type,
reverse: ( ty * uni ) > uni ).
tff(func_def_25,type,
map: ( ty * ty ) > ty ).
tff(func_def_26,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_27,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_28,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_29,type,
loc1: ty ).
tff(func_def_30,type,
null: loc ).
tff(func_def_31,type,
t2tb: list_loc > uni ).
tff(func_def_32,type,
tb2t: uni > list_loc ).
tff(func_def_33,type,
t2tb1: map_loc_loc > uni ).
tff(func_def_34,type,
tb2t1: uni > map_loc_loc ).
tff(func_def_35,type,
t2tb2: loc > uni ).
tff(func_def_36,type,
tb2t2: uni > loc ).
tff(func_def_37,type,
ref: ty > ty ).
tff(func_def_38,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_39,type,
contents: ( ty * uni ) > uni ).
tff(func_def_40,type,
sK1: ( uni * ty * uni ) > uni ).
tff(func_def_41,type,
sK2: list_loc ).
tff(func_def_42,type,
sK3: map_loc_loc ).
tff(func_def_43,type,
sK4: loc ).
tff(func_def_44,type,
sK5: loc ).
tff(func_def_45,type,
sK6: loc ).
tff(func_def_46,type,
sK7: list_loc ).
tff(func_def_47,type,
sK8: map_loc_loc ).
tff(func_def_48,type,
sK9: list_loc ).
tff(func_def_49,type,
sK10: map_loc_loc ).
tff(func_def_50,type,
sK11: loc ).
tff(func_def_51,type,
sK12: loc ).
tff(func_def_52,type,
sK13: list_loc ).
tff(func_def_53,type,
sK14: list_loc ).
tff(func_def_54,type,
sK15: list_loc ).
tff(func_def_55,type,
sK16: loc ).
tff(func_def_56,type,
sK17: ( ty * uni * uni ) > uni ).
tff(func_def_57,type,
sK18: ( ty * uni * uni ) > uni ).
tff(func_def_58,type,
sK19: ( list_loc * map_loc_loc * loc * loc ) > list_loc ).
tff(func_def_59,type,
sK20: ( list_loc * map_loc_loc * loc * loc ) > loc ).
tff(func_def_60,type,
sK21: ( list_loc * map_loc_loc * loc * loc ) > map_loc_loc ).
tff(func_def_61,type,
sK22: ( list_loc * map_loc_loc * loc * loc ) > loc ).
tff(func_def_62,type,
sK23: ( loc * loc * map_loc_loc * list_loc ) > map_loc_loc ).
tff(func_def_63,type,
sK24: ( loc * loc * map_loc_loc * list_loc ) > loc ).
tff(func_def_64,type,
sF25: uni ).
tff(func_def_65,type,
sF26: uni ).
tff(func_def_66,type,
sF27: uni ).
tff(func_def_67,type,
sF28: loc ).
tff(func_def_68,type,
sF29: uni ).
tff(func_def_69,type,
sF30: uni ).
tff(func_def_70,type,
sF31: uni ).
tff(func_def_71,type,
sF32: uni ).
tff(func_def_72,type,
sF33: list_loc ).
tff(func_def_73,type,
sF34: uni ).
tff(func_def_74,type,
sF35: list_loc ).
tff(func_def_75,type,
sF36: uni ).
tff(func_def_76,type,
sF37: list_loc ).
tff(func_def_77,type,
sF38: uni ).
tff(func_def_78,type,
sF39: uni ).
tff(func_def_79,type,
sF40: uni ).
tff(func_def_80,type,
sF41: list_loc ).
tff(func_def_81,type,
sF42: uni ).
tff(func_def_82,type,
sF43: uni ).
tff(func_def_83,type,
sF44: map_loc_loc ).
tff(func_def_84,type,
sF45: uni ).
tff(func_def_85,type,
sF46: uni ).
tff(func_def_86,type,
sF47: list_loc ).
tff(func_def_87,type,
sF48: uni ).
tff(func_def_88,type,
sF49: uni ).
tff(func_def_89,type,
sF50: list_loc ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
disjoint: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
no_repet: ( ty * uni ) > $o ).
tff(pred_def_6,type,
list_seg: ( loc * map_loc_loc * list_loc * loc ) > $o ).
tff(pred_def_8,type,
sP0: ( list_loc * map_loc_loc * loc * loc ) > $o ).
tff(f14,axiom,
! [X1: uni,X0: ty,X2: uni] : ( nil(X0) != cons(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nil_Cons) ).
tff(f23,axiom,
! [X2: uni,X0: ty,X1: uni] : ( tail(X0,cons(X0,X1,X2)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tail_cons) ).
tff(f51,axiom,
! [X0: list_loc] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(f52,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f61,axiom,
! [X0: loc,X1: map_loc_loc,X2: list_loc,X3: loc] :
( list_seg(X0,X1,X2,X3)
=> ( ? [X4: loc,X7: list_loc,X6: loc,X5: map_loc_loc] :
( list_seg(tb2t2(get(loc1,loc1,t2tb1(X5),t2tb2(X4))),X5,X7,X6)
& ( X0 = X4 )
& ( X3 = X6 )
& ( X1 = X5 )
& ( X4 != null )
& ( X2 = tb2t(cons(loc1,t2tb2(X4),t2tb(X7))) ) )
| ? [X4: loc,X5: map_loc_loc] :
( ( X2 = tb2t(nil(loc1)) )
& ( X1 = X5 )
& ( X0 = X4 )
& ( X3 = X4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',list_seg_inversion) ).
tff(f70,conjecture,
! [X1: list_loc,X2: map_loc_loc,X0: loc] :
( list_seg(X0,X2,X1,null)
=> ! [X4: loc,X6: loc,X3: list_loc,X5: list_loc,X7: map_loc_loc] :
( ( list_seg(X6,X7,X5,null)
& disjoint(loc1,t2tb(X5),t2tb(X3))
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(X5)),t2tb(X3))) = tb2t(reverse(loc1,t2tb(X1))) )
& list_seg(X4,X7,X3,null) )
=> ( ( X6 != null )
=> ! [X8: map_loc_loc] :
( ( X8 = tb2t1(set(loc1,loc1,t2tb1(X7),t2tb2(X6),t2tb2(X4))) )
=> ( list_seg(X4,X8,X3,null)
=> ! [X9: loc] :
( ( X9 = X6 )
=> ! [X10: loc] :
( ( X10 = tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X6))) )
=> ! [X11: list_loc] :
( ( X11 = tb2t(cons(loc1,head(loc1,t2tb(X5)),t2tb(X3))) )
=> ! [X12: list_loc] :
( ( X12 = tb2t(tail(loc1,t2tb(X5))) )
=> ( ( X5 != tb2t(nil(loc1)) )
& ! [X13: loc,X14: list_loc] :
( ( X5 = tb2t(cons(loc1,t2tb2(X13),t2tb(X14))) )
=> ( X14 = X12 ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_in_place_reverse) ).
tff(f71,negated_conjecture,
~ ! [X1: list_loc,X2: map_loc_loc,X0: loc] :
( list_seg(X0,X2,X1,null)
=> ! [X4: loc,X6: loc,X3: list_loc,X5: list_loc,X7: map_loc_loc] :
( ( list_seg(X6,X7,X5,null)
& disjoint(loc1,t2tb(X5),t2tb(X3))
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(X5)),t2tb(X3))) = tb2t(reverse(loc1,t2tb(X1))) )
& list_seg(X4,X7,X3,null) )
=> ( ( X6 != null )
=> ! [X8: map_loc_loc] :
( ( X8 = tb2t1(set(loc1,loc1,t2tb1(X7),t2tb2(X6),t2tb2(X4))) )
=> ( list_seg(X4,X8,X3,null)
=> ! [X9: loc] :
( ( X9 = X6 )
=> ! [X10: loc] :
( ( X10 = tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X6))) )
=> ! [X11: list_loc] :
( ( X11 = tb2t(cons(loc1,head(loc1,t2tb(X5)),t2tb(X3))) )
=> ! [X12: list_loc] :
( ( X12 = tb2t(tail(loc1,t2tb(X5))) )
=> ( ( X5 != tb2t(nil(loc1)) )
& ! [X13: loc,X14: list_loc] :
( ( X5 = tb2t(cons(loc1,t2tb2(X13),t2tb(X14))) )
=> ( X14 = X12 ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f70]) ).
tff(f74,plain,
~ ! [X1: map_loc_loc,X0: list_loc,X2: loc] :
( list_seg(X2,X1,X0,null)
=> ! [X3: loc,X5: list_loc,X7: map_loc_loc,X6: list_loc,X4: loc] :
( ( disjoint(loc1,t2tb(X6),t2tb(X5))
& list_seg(X4,X7,X6,null)
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(X6)),t2tb(X5))) = tb2t(reverse(loc1,t2tb(X0))) )
& list_seg(X3,X7,X5,null) )
=> ( ( null != X4 )
=> ! [X8: map_loc_loc] :
( ( tb2t1(set(loc1,loc1,t2tb1(X7),t2tb2(X4),t2tb2(X3))) = X8 )
=> ( list_seg(X3,X8,X5,null)
=> ! [X9: loc] :
( ( X4 = X9 )
=> ! [X10: loc] :
( ( tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))) = X10 )
=> ! [X11: list_loc] :
( ( tb2t(cons(loc1,head(loc1,t2tb(X6)),t2tb(X5))) = X11 )
=> ! [X12: list_loc] :
( ( tb2t(tail(loc1,t2tb(X6))) = X12 )
=> ( ( tb2t(nil(loc1)) != X6 )
& ! [X13: loc,X14: list_loc] :
( ( tb2t(cons(loc1,t2tb2(X13),t2tb(X14))) = X6 )
=> ( X14 = X12 ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f71]) ).
tff(f76,plain,
! [X2: uni,X1: ty,X0: uni] : ( nil(X1) != cons(X1,X0,X2) ),
inference(rectify,[],[f14]) ).
tff(f78,plain,
! [X1: ty,X0: uni,X2: uni] : ( tail(X1,cons(X1,X2,X0)) = X0 ),
inference(rectify,[],[f23]) ).
tff(f92,plain,
! [X2: list_loc,X3: loc,X0: loc,X1: map_loc_loc] :
( list_seg(X0,X1,X2,X3)
=> ( ? [X9: map_loc_loc,X8: loc] :
( ( X2 = tb2t(nil(loc1)) )
& ( X1 = X9 )
& ( X3 = X8 )
& ( X0 = X8 ) )
| ? [X5: list_loc,X6: loc,X7: map_loc_loc,X4: loc] :
( ( X4 != null )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))),X7,X5,X6)
& ( tb2t(cons(loc1,t2tb2(X4),t2tb(X5))) = X2 )
& ( X1 = X7 )
& ( X3 = X6 )
& ( X0 = X4 ) ) ) ),
inference(rectify,[],[f61]) ).
tff(f106,plain,
? [X1: map_loc_loc,X0: list_loc,X2: loc] :
( ? [X3: loc,X5: list_loc,X7: map_loc_loc,X6: list_loc,X4: loc] :
( ? [X8: map_loc_loc] :
( ? [X9: loc] :
( ? [X10: loc] :
( ( tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))) = X10 )
& ? [X11: list_loc] :
( ( tb2t(cons(loc1,head(loc1,t2tb(X6)),t2tb(X5))) = X11 )
& ? [X12: list_loc] :
( ( tb2t(tail(loc1,t2tb(X6))) = X12 )
& ( ? [X14: list_loc,X13: loc] :
( ( X12 != X14 )
& ( tb2t(cons(loc1,t2tb2(X13),t2tb(X14))) = X6 ) )
| ( tb2t(nil(loc1)) = X6 ) ) ) ) )
& ( X4 = X9 ) )
& list_seg(X3,X8,X5,null)
& ( tb2t1(set(loc1,loc1,t2tb1(X7),t2tb2(X4),t2tb2(X3))) = X8 ) )
& ( null != X4 )
& disjoint(loc1,t2tb(X6),t2tb(X5))
& list_seg(X4,X7,X6,null)
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(X6)),t2tb(X5))) = tb2t(reverse(loc1,t2tb(X0))) )
& list_seg(X3,X7,X5,null) )
& list_seg(X2,X1,X0,null) ),
inference(ennf_transformation,[],[f74]) ).
tff(f107,plain,
? [X0: list_loc,X1: map_loc_loc,X2: loc] :
( list_seg(X2,X1,X0,null)
& ? [X3: loc,X4: loc,X6: list_loc,X7: map_loc_loc,X5: list_loc] :
( list_seg(X3,X7,X5,null)
& ? [X8: map_loc_loc] :
( ? [X9: loc] :
( ? [X10: loc] :
( ( tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))) = X10 )
& ? [X11: list_loc] :
( ( tb2t(cons(loc1,head(loc1,t2tb(X6)),t2tb(X5))) = X11 )
& ? [X12: list_loc] :
( ( tb2t(tail(loc1,t2tb(X6))) = X12 )
& ( ? [X14: list_loc,X13: loc] :
( ( X12 != X14 )
& ( tb2t(cons(loc1,t2tb2(X13),t2tb(X14))) = X6 ) )
| ( tb2t(nil(loc1)) = X6 ) ) ) ) )
& ( X4 = X9 ) )
& list_seg(X3,X8,X5,null)
& ( tb2t1(set(loc1,loc1,t2tb1(X7),t2tb2(X4),t2tb2(X3))) = X8 ) )
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(X6)),t2tb(X5))) = tb2t(reverse(loc1,t2tb(X0))) )
& disjoint(loc1,t2tb(X6),t2tb(X5))
& ( null != X4 )
& list_seg(X4,X7,X6,null) ) ),
inference(flattening,[],[f106]) ).
tff(f108,plain,
! [X2: list_loc,X3: loc,X0: loc,X1: map_loc_loc] :
( ? [X9: map_loc_loc,X8: loc] :
( ( X2 = tb2t(nil(loc1)) )
& ( X1 = X9 )
& ( X3 = X8 )
& ( X0 = X8 ) )
| ? [X5: list_loc,X6: loc,X7: map_loc_loc,X4: loc] :
( ( X4 != null )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))),X7,X5,X6)
& ( tb2t(cons(loc1,t2tb2(X4),t2tb(X5))) = X2 )
& ( X1 = X7 )
& ( X3 = X6 )
& ( X0 = X4 ) )
| ~ list_seg(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f92]) ).
tff(f109,plain,
! [X0: loc,X3: loc,X1: map_loc_loc,X2: list_loc] :
( ~ list_seg(X0,X1,X2,X3)
| ? [X5: list_loc,X6: loc,X7: map_loc_loc,X4: loc] :
( ( X4 != null )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))),X7,X5,X6)
& ( tb2t(cons(loc1,t2tb2(X4),t2tb(X5))) = X2 )
& ( X1 = X7 )
& ( X3 = X6 )
& ( X0 = X4 ) )
| ? [X9: map_loc_loc,X8: loc] :
( ( X2 = tb2t(nil(loc1)) )
& ( X1 = X9 )
& ( X3 = X8 )
& ( X0 = X8 ) ) ),
inference(flattening,[],[f108]) ).
tff(f120,definition,
! [X2: list_loc,X1: map_loc_loc,X3: loc,X0: loc] :
( ? [X5: list_loc,X6: loc,X7: map_loc_loc,X4: loc] :
( ( X4 != null )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))),X7,X5,X6)
& ( tb2t(cons(loc1,t2tb2(X4),t2tb(X5))) = X2 )
& ( X1 = X7 )
& ( X3 = X6 )
& ( X0 = X4 ) )
| ~ sP0(X2,X1,X3,X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f121,plain,
! [X0: loc,X3: loc,X1: map_loc_loc,X2: list_loc] :
( ~ list_seg(X0,X1,X2,X3)
| sP0(X2,X1,X3,X0)
| ? [X9: map_loc_loc,X8: loc] :
( ( X2 = tb2t(nil(loc1)) )
& ( X1 = X9 )
& ( X3 = X8 )
& ( X0 = X8 ) ) ),
inference(definition_folding,[],[f109,f120]) ).
tff(f137,plain,
! [X0: ty,X1: uni,X2: uni] : ( tail(X0,cons(X0,X2,X1)) = X1 ),
inference(rectify,[],[f78]) ).
tff(f140,plain,
? [X0: list_loc,X1: map_loc_loc,X2: loc] :
( list_seg(X2,X1,X0,null)
& ? [X3: loc,X4: loc,X5: list_loc,X6: map_loc_loc,X7: list_loc] :
( list_seg(X3,X6,X7,null)
& ? [X8: map_loc_loc] :
( ? [X9: loc] :
( ? [X10: loc] :
( ( tb2t2(get(loc1,loc1,t2tb1(X6),t2tb2(X4))) = X10 )
& ? [X11: list_loc] :
( ( tb2t(cons(loc1,head(loc1,t2tb(X5)),t2tb(X7))) = X11 )
& ? [X12: list_loc] :
( ( tb2t(tail(loc1,t2tb(X5))) = X12 )
& ( ? [X13: list_loc,X14: loc] :
( ( X12 != X13 )
& ( tb2t(cons(loc1,t2tb2(X14),t2tb(X13))) = X5 ) )
| ( tb2t(nil(loc1)) = X5 ) ) ) ) )
& ( X4 = X9 ) )
& list_seg(X3,X8,X7,null)
& ( tb2t1(set(loc1,loc1,t2tb1(X6),t2tb2(X4),t2tb2(X3))) = X8 ) )
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(X5)),t2tb(X7))) = tb2t(reverse(loc1,t2tb(X0))) )
& disjoint(loc1,t2tb(X5),t2tb(X7))
& ( null != X4 )
& list_seg(X4,X6,X5,null) ) ),
inference(rectify,[],[f107]) ).
tff(f141,plain,
( list_seg(sK4,sK3,sK2,null)
& list_seg(sK5,sK8,sK9,null)
& ( sK12 = tb2t2(get(loc1,loc1,t2tb1(sK8),t2tb2(sK6))) )
& ( tb2t(cons(loc1,head(loc1,t2tb(sK7)),t2tb(sK9))) = sK13 )
& ( sK14 = tb2t(tail(loc1,t2tb(sK7))) )
& ( ( ( sK15 != sK14 )
& ( sK7 = tb2t(cons(loc1,t2tb2(sK16),t2tb(sK15))) ) )
| ( tb2t(nil(loc1)) = sK7 ) )
& ( sK6 = sK11 )
& list_seg(sK5,sK10,sK9,null)
& ( tb2t1(set(loc1,loc1,t2tb1(sK8),t2tb2(sK6),t2tb2(sK5))) = sK10 )
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(sK7)),t2tb(sK9))) = tb2t(reverse(loc1,t2tb(sK2))) )
& disjoint(loc1,t2tb(sK7),t2tb(sK9))
& ( null != sK6 )
& list_seg(sK6,sK8,sK7,null) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10),skolemize(X9,sK11),skolemize(X10,sK12),skolemize(X11,sK13),skolemize(X12,sK14),skolemize(X13,sK15),skolemize(X14,sK16)],[f140]) ).
tff(f149,plain,
! [X0: uni,X1: ty,X2: uni] : ( nil(X1) != cons(X1,X2,X0) ),
inference(rectify,[],[f76]) ).
tff(f154,plain,
! [X2: list_loc,X1: map_loc_loc,X3: loc,X0: loc] :
( ? [X5: list_loc,X6: loc,X7: map_loc_loc,X4: loc] :
( ( X4 != null )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(X7),t2tb2(X4))),X7,X5,X6)
& ( tb2t(cons(loc1,t2tb2(X4),t2tb(X5))) = X2 )
& ( X1 = X7 )
& ( X3 = X6 )
& ( X0 = X4 ) )
| ~ sP0(X2,X1,X3,X0) ),
inference(nnf_transformation,[],[f120]) ).
tff(f155,plain,
! [X0: list_loc,X1: map_loc_loc,X2: loc,X3: loc] :
( ? [X4: list_loc,X5: loc,X6: map_loc_loc,X7: loc] :
( ( null != X7 )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(X6),t2tb2(X7))),X6,X4,X5)
& ( tb2t(cons(loc1,t2tb2(X7),t2tb(X4))) = X0 )
& ( X1 = X6 )
& ( X2 = X5 )
& ( X3 = X7 ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(rectify,[],[f154]) ).
tff(f156,plain,
! [X0: list_loc,X1: map_loc_loc,X2: loc,X3: loc] :
( ( ( null != sK22(X0,X1,X2,X3) )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(sK21(X0,X1,X2,X3)),t2tb2(sK22(X0,X1,X2,X3)))),sK21(X0,X1,X2,X3),sK19(X0,X1,X2,X3),sK20(X0,X1,X2,X3))
& ( tb2t(cons(loc1,t2tb2(sK22(X0,X1,X2,X3)),t2tb(sK19(X0,X1,X2,X3)))) = X0 )
& ( sK21(X0,X1,X2,X3) = X1 )
& ( sK20(X0,X1,X2,X3) = X2 )
& ( sK22(X0,X1,X2,X3) = X3 ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20,sK21,sK22]),skolemize(X4,sK19(X0,X1,X2,X3)),skolemize(X5,sK20(X0,X1,X2,X3)),skolemize(X6,sK21(X0,X1,X2,X3)),skolemize(X7,sK22(X0,X1,X2,X3))],[f155]) ).
tff(f157,plain,
! [X0: loc,X1: loc,X2: map_loc_loc,X3: list_loc] :
( ~ list_seg(X0,X2,X3,X1)
| sP0(X3,X2,X1,X0)
| ? [X4: map_loc_loc,X5: loc] :
( ( tb2t(nil(loc1)) = X3 )
& ( X2 = X4 )
& ( X1 = X5 )
& ( X0 = X5 ) ) ),
inference(rectify,[],[f121]) ).
tff(f158,plain,
! [X0: loc,X1: loc,X2: map_loc_loc,X3: list_loc] :
( ~ list_seg(X0,X2,X3,X1)
| sP0(X3,X2,X1,X0)
| ( ( tb2t(nil(loc1)) = X3 )
& ( sK23(X0,X1,X2,X3) = X2 )
& ( sK24(X0,X1,X2,X3) = X1 )
& ( sK24(X0,X1,X2,X3) = X0 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24]),skolemize(X4,sK23(X0,X1,X2,X3)),skolemize(X5,sK24(X0,X1,X2,X3))],[f157]) ).
tff(f182,plain,
! [X2: uni,X0: ty,X1: uni] : ( tail(X0,cons(X0,X2,X1)) = X1 ),
inference(cnf_transformation,[],[f137]) ).
tff(f188,plain,
list_seg(sK6,sK8,sK7,null),
inference(cnf_transformation,[],[f141]) ).
tff(f189,plain,
null != sK6,
inference(cnf_transformation,[],[f141]) ).
tff(f194,plain,
sK6 = sK11,
inference(cnf_transformation,[],[f141]) ).
tff(f195,plain,
( ( sK7 = tb2t(cons(loc1,t2tb2(sK16),t2tb(sK15))) )
| ( tb2t(nil(loc1)) = sK7 ) ),
inference(cnf_transformation,[],[f141]) ).
tff(f196,plain,
( ( sK15 != sK14 )
| ( tb2t(nil(loc1)) = sK7 ) ),
inference(cnf_transformation,[],[f141]) ).
tff(f197,plain,
sK14 = tb2t(tail(loc1,t2tb(sK7))),
inference(cnf_transformation,[],[f141]) ).
tff(f212,plain,
! [X2: uni,X0: uni,X1: ty] : ( nil(X1) != cons(X1,X2,X0) ),
inference(cnf_transformation,[],[f149]) ).
tff(f218,plain,
! [X0: list_loc] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f51]) ).
tff(f221,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f52]) ).
tff(f226,plain,
! [X2: loc,X3: loc,X0: list_loc,X1: map_loc_loc] :
( ( tb2t(cons(loc1,t2tb2(sK22(X0,X1,X2,X3)),t2tb(sK19(X0,X1,X2,X3)))) = X0 )
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f156]) ).
tff(f229,plain,
! [X2: map_loc_loc,X3: list_loc,X0: loc,X1: loc] :
( ( sK24(X0,X1,X2,X3) = X0 )
| sP0(X3,X2,X1,X0)
| ~ list_seg(X0,X2,X3,X1) ),
inference(cnf_transformation,[],[f158]) ).
tff(f230,plain,
! [X2: map_loc_loc,X3: list_loc,X0: loc,X1: loc] :
( ( sK24(X0,X1,X2,X3) = X1 )
| sP0(X3,X2,X1,X0)
| ~ list_seg(X0,X2,X3,X1) ),
inference(cnf_transformation,[],[f158]) ).
tff(f238,plain,
null != sK11,
inference(definition_unfolding,[],[f189,f194]) ).
tff(f239,plain,
list_seg(sK11,sK8,sK7,null),
inference(definition_unfolding,[],[f188,f194]) ).
tff(f248,definition,
sF29 = t2tb(sK7),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f249,plain,
t2tb(sK7) = sF29,
inference(reorient_equations,[],[f248]) ).
tff(f257,definition,
sF34 = tail(loc1,sF29),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f258,definition,
sF35 = tb2t(sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f259,plain,
tb2t(sF34) = sF35,
inference(reorient_equations,[],[f258]) ).
tff(f260,plain,
sK14 = sF35,
inference(definition_folding,[],[f197,f259,f257,f249]) ).
tff(f261,definition,
sF36 = nil(loc1),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
tff(f262,plain,
nil(loc1) = sF36,
inference(reorient_equations,[],[f261]) ).
tff(f263,definition,
sF37 = tb2t(sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
tff(f264,plain,
( ( sK7 = sF37 )
| ( sK15 != sK14 ) ),
inference(definition_folding,[],[f196,f263,f262]) ).
tff(f265,definition,
sF38 = t2tb2(sK16),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
tff(f266,plain,
t2tb2(sK16) = sF38,
inference(reorient_equations,[],[f265]) ).
tff(f267,definition,
sF39 = t2tb(sK15),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
tff(f268,plain,
t2tb(sK15) = sF39,
inference(reorient_equations,[],[f267]) ).
tff(f269,definition,
sF40 = cons(loc1,sF38,sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
tff(f270,plain,
cons(loc1,sF38,sF39) = sF40,
inference(reorient_equations,[],[f269]) ).
tff(f271,definition,
sF41 = tb2t(sF40),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
tff(f272,plain,
( ( sF41 = sK7 )
| ( sK7 = sF37 ) ),
inference(definition_folding,[],[f195,f263,f262,f271,f270,f268,f266]) ).
tff(f292,definition,
( spl51_1
<=> ( sK15 = sK14 ) ),
introduced(definition,[new_symbols(definition,[spl51_1])],[avatar_definition]) ).
tff(f294,plain,
( ( sK15 != sK14 )
| spl51_1 ),
inference(avatar_component_clause,[],[f292]) ).
tff(f296,definition,
( spl51_2
<=> ( sK7 = sF37 ) ),
introduced(definition,[new_symbols(definition,[spl51_2])],[avatar_definition]) ).
tff(f298,plain,
( ( sK7 = sF37 )
| ~ spl51_2 ),
inference(avatar_component_clause,[],[f296]) ).
tff(f299,plain,
( ~ spl51_1
| spl51_2 ),
inference(avatar_split_clause,[],[f264,f296,f292]) ).
tff(f301,definition,
( spl51_3
<=> ( sF41 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl51_3])],[avatar_definition]) ).
tff(f303,plain,
( ( sF41 = sK7 )
| ~ spl51_3 ),
inference(avatar_component_clause,[],[f301]) ).
tff(f304,plain,
( spl51_2
| spl51_3 ),
inference(avatar_split_clause,[],[f272,f301,f296]) ).
tff(f307,plain,
tb2t(sF34) = sK14,
inference(forward_demodulation,[],[f259,f260]) ).
tff(f308,plain,
( ( sK7 = tb2t(sF36) )
| ~ spl51_2 ),
inference(forward_demodulation,[],[f263,f298]) ).
tff(f323,plain,
sK15 = tb2t(sF39),
inference(superposition,[],[f218,f268]) ).
tff(f326,plain,
( ( t2tb(sK7) = sF36 )
| ~ spl51_2 ),
inference(superposition,[],[f221,f308]) ).
tff(f327,plain,
t2tb(sF41) = sF40,
inference(superposition,[],[f221,f271]) ).
tff(f331,plain,
( ( sF36 = sF29 )
| ~ spl51_2 ),
inference(forward_demodulation,[],[f326,f249]) ).
tff(f405,plain,
tail(loc1,sF40) = sF39,
inference(superposition,[],[f182,f270]) ).
tff(f632,plain,
! [X2: map_loc_loc,X3: list_loc,X0: loc,X1: loc] :
( sP0(X3,X2,X1,X0)
| ~ list_seg(X0,X2,X3,X1)
| ~ list_seg(X0,X2,X3,X1)
| sP0(X3,X2,X1,X0)
| ( X0 = X1 ) ),
inference(superposition,[],[f230,f229]) ).
tff(f634,plain,
! [X2: map_loc_loc,X3: list_loc,X0: loc,X1: loc] :
( ~ list_seg(X0,X2,X3,X1)
| ( X0 = X1 )
| sP0(X3,X2,X1,X0) ),
inference(duplicate_literal_removal,[],[f632]) ).
tff(f702,plain,
! [X2: loc,X3: loc,X0: list_loc,X1: map_loc_loc] :
( ( t2tb(X0) = cons(loc1,t2tb2(sK22(X0,X1,X2,X3)),t2tb(sK19(X0,X1,X2,X3))) )
| ~ sP0(X0,X1,X2,X3) ),
inference(superposition,[],[f221,f226]) ).
tff(f1162,plain,
( ( t2tb(sK7) = sF40 )
| ~ spl51_3 ),
inference(forward_demodulation,[],[f327,f303]) ).
tff(f1163,plain,
( ( sF29 = sF40 )
| ~ spl51_3 ),
inference(forward_demodulation,[],[f1162,f249]) ).
tff(f1364,plain,
( ( tail(loc1,sF29) = sF39 )
| ~ spl51_3 ),
inference(forward_demodulation,[],[f405,f1163]) ).
tff(f1365,plain,
( ( sF34 = sF39 )
| ~ spl51_3 ),
inference(superposition,[],[f1364,f257]) ).
tff(f1371,plain,
( ( sK14 = tb2t(sF39) )
| ~ spl51_3 ),
inference(superposition,[],[f307,f1365]) ).
tff(f1372,plain,
( ( sK15 = sK14 )
| ~ spl51_3 ),
inference(forward_demodulation,[],[f1371,f323]) ).
tff(f1373,plain,
( $false
| spl51_1
| ~ spl51_3 ),
inference(forward_subsumption_resolution,[],[f1372,f294]) ).
tff(f1374,plain,
( spl51_1
| ~ spl51_3 ),
inference(avatar_contradiction_clause,[],[f1373]) ).
tff(f1376,definition,
( spl51_37
<=> sP0(sK7,sK8,null,sK11) ),
introduced(definition,[new_symbols(definition,[spl51_37])],[avatar_definition]) ).
tff(f1378,plain,
( sP0(sK7,sK8,null,sK11)
| ~ spl51_37 ),
inference(avatar_component_clause,[],[f1376]) ).
tff(f1642,plain,
( ( null = sK11 )
| sP0(sK7,sK8,null,sK11) ),
inference(resolution,[],[f634,f239]) ).
tff(f1644,plain,
sP0(sK7,sK8,null,sK11),
inference(forward_subsumption_resolution,[],[f1642,f238]) ).
tff(f1645,plain,
spl51_37,
inference(avatar_split_clause,[],[f1644,f1376]) ).
tff(f2447,plain,
! [X2: loc,X3: loc,X0: list_loc,X1: map_loc_loc] :
( ~ sP0(X0,X1,X2,X3)
| ( t2tb(X0) != nil(loc1) ) ),
inference(superposition,[],[f212,f702]) ).
tff(f2456,plain,
! [X2: loc,X3: loc,X0: list_loc,X1: map_loc_loc] :
( ( t2tb(X0) != sF36 )
| ~ sP0(X0,X1,X2,X3) ),
inference(forward_demodulation,[],[f2447,f262]) ).
tff(f2462,plain,
( ! [X2: loc,X3: loc,X0: list_loc,X1: map_loc_loc] :
( ( t2tb(X0) != sF29 )
| ~ sP0(X0,X1,X2,X3) )
| ~ spl51_2 ),
inference(forward_demodulation,[],[f2456,f331]) ).
tff(f2466,plain,
( ! [X2: loc,X0: map_loc_loc,X1: loc] :
( ( sF29 != sF29 )
| ~ sP0(sK7,X0,X1,X2) )
| ~ spl51_2 ),
inference(superposition,[],[f2462,f249]) ).
tff(f2475,plain,
( ! [X2: loc,X0: map_loc_loc,X1: loc] : ~ sP0(sK7,X0,X1,X2)
| ~ spl51_2 ),
inference(trivial_inequality_removal,[],[f2466]) ).
tff(f2615,plain,
( $false
| ~ spl51_2
| ~ spl51_37 ),
inference(resolution,[],[f2475,f1378]) ).
tff(f2616,plain,
( ~ spl51_2
| ~ spl51_37 ),
inference(avatar_contradiction_clause,[],[f2615]) ).
cnf(s1,plain,
( ~ spl51_1
| spl51_2 ),
inference(sat_conversion,[],[f299]) ).
cnf(s2,plain,
( spl51_2
| spl51_3 ),
inference(sat_conversion,[],[f304]) ).
cnf(s38,plain,
( spl51_1
| ~ spl51_3 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s44,plain,
spl51_37,
inference(sat_conversion,[],[f1645]) ).
cnf(s51,plain,
( ~ spl51_2
| ~ spl51_37 ),
inference(sat_conversion,[],[f2616]) ).
cnf(s55,plain,
~ spl51_2,
inference(rat,[],[s51,s44]) ).
cnf(s57,plain,
spl51_3,
inference(rat,[],[s2,s55]) ).
cnf(s58,plain,
spl51_1,
inference(rat,[],[s38,s57]) ).
cnf(s60,plain,
$false,
inference(rat,[],[s1,s55,s58]) ).
tff(f2620,plain,
$false,
inference(avatar_sat_refutation,[],[s60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW615_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n013.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 14:21:05 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.25 Running first-order theorem proving
% 0.09/0.25 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.43/1.25 % (1212768)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.43/1.25 % (1212777)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2580081102:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.43/1.25 % (1212777)Instruction limit reached!
% 3.43/1.25 % (1212777)------------------------------
% 3.43/1.25 % (1212777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.25 % (1212777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.25 % (1212777)CaDiCaL version: 2.1.3
% 3.43/1.25 % (1212777)Termination reason: Instruction limit
% 3.43/1.25 % (1212777)Termination phase: Property scanning
% 3.43/1.25 % (1212777)Time elapsed: 0.002 s
% 3.43/1.25 % (1212777)Peak memory usage: 86 MB
% 3.43/1.25 % (1212777)Instructions burned: 5 (million)
% 3.43/1.25 % (1212774)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2396895974:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.43/1.25 % (1212775)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1555659644:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.43/1.25 % (1212776)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2669200392:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.43/1.25 % (1212773)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3318849409:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.43/1.25 % (1212778)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2258423223:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.43/1.25 % (1212779)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=322988908:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.43/1.25 % (1212776)Instruction limit reached!
% 3.43/1.25 % (1212776)------------------------------
% 3.43/1.25 % (1212776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.25 % (1212776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.25 % (1212776)CaDiCaL version: 2.1.3
% 3.43/1.25 % (1212776)Termination reason: Instruction limit
% 3.43/1.25 % (1212776)Termination phase: Saturation
% 3.43/1.25 % (1212776)Time elapsed: 0.005 s
% 3.43/1.25 % (1212776)Peak memory usage: 88 MB
% 3.43/1.25 % (1212776)Instructions burned: 7 (million)
% 3.43/1.25 % (1212773)Instruction limit reached!
% 3.43/1.25 % (1212773)------------------------------
% 3.43/1.25 % (1212773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.25 % (1212773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.25 % (1212773)CaDiCaL version: 2.1.3
% 3.43/1.25 % (1212773)Termination reason: Instruction limit
% 3.43/1.25 % (1212773)Termination phase: Saturation
% 3.43/1.25 % (1212773)Time elapsed: 0.030 s
% 3.43/1.25 % (1212773)Peak memory usage: 111 MB
% 3.43/1.25 % (1212773)Instructions burned: 13 (million)
% 3.43/1.25 % (1212779)Instruction limit reached!
% 3.43/1.25 % (1212779)------------------------------
% 3.43/1.25 % (1212779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.25 % (1212779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.25 % (1212779)CaDiCaL version: 2.1.3
% 3.43/1.25 % (1212779)Termination reason: Instruction limit
% 3.43/1.25 % (1212779)Termination phase: Saturation
% 3.43/1.25 % (1212779)Time elapsed: 0.043 s
% 3.43/1.25 % (1212779)Peak memory usage: 115 MB
% 3.43/1.25 % (1212779)Instructions burned: 34 (million)
% 3.43/1.25 % (1212778)Instruction limit reached!
% 3.43/1.25 % (1212778)------------------------------
% 3.43/1.25 % (1212778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.25 % (1212778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.25 % (1212778)CaDiCaL version: 2.1.3
% 3.43/1.25 % (1212778)Termination reason: Instruction limit
% 3.43/1.25 % (1212778)Termination phase: Saturation
% 3.43/1.25 % (1212778)Time elapsed: 0.053 s
% 3.43/1.25 % (1212778)Peak memory usage: 115 MB
% 3.43/1.25 % (1212778)Instructions burned: 46 (million)
% 3.43/1.25 % (1212781)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=149926319:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.43/1.25 % (1212781)Instruction limit reached!
% 3.43/1.25 % (1212781)------------------------------
% 4.66/1.44 % (1212781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.44 % (1212781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.44 % (1212781)CaDiCaL version: 2.1.3
% 4.66/1.44 % (1212781)Termination reason: Instruction limit
% 4.66/1.44 % (1212781)Termination phase: Saturation
% 4.66/1.44 % (1212781)Time elapsed: 0.006 s
% 4.66/1.44 % (1212781)Peak memory usage: 89 MB
% 4.66/1.44 % (1212781)Instructions burned: 15 (million)
% 4.66/1.44 % (1212775)Instruction limit reached!
% 4.66/1.44 % (1212775)------------------------------
% 4.66/1.44 % (1212775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.44 % (1212775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.44 % (1212775)CaDiCaL version: 2.1.3
% 4.66/1.44 % (1212775)Termination reason: Instruction limit
% 4.66/1.44 % (1212775)Termination phase: Saturation
% 4.66/1.44 % (1212775)Time elapsed: 0.147 s
% 4.66/1.44 % (1212775)Peak memory usage: 118 MB
% 4.66/1.44 % (1212775)Instructions burned: 202 (million)
% 4.66/1.44 % (1212788)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=1997107533:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.66/1.44 % (1212788)Instruction limit reached!
% 4.66/1.44 % (1212788)------------------------------
% 4.66/1.44 % (1212788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.44 % (1212788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.44 % (1212788)CaDiCaL version: 2.1.3
% 4.66/1.44 % (1212788)Termination reason: Instruction limit
% 4.66/1.44 % (1212788)Termination phase: Saturation
% 4.66/1.44 % (1212788)Time elapsed: 0.023 s
% 4.66/1.44 % (1212788)Peak memory usage: 89 MB
% 4.66/1.44 % (1212788)Instructions burned: 30 (million)
% 4.66/1.44 % (1212790)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4045165513:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.66/1.44 % (1212789)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=310201892:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.66/1.44 % (1212793)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2110009019:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.66/1.44 % (1212789)Instruction limit reached!
% 4.66/1.44 % (1212789)------------------------------
% 4.66/1.44 % (1212789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.44 % (1212789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.44 % (1212789)CaDiCaL version: 2.1.3
% 4.66/1.44 % (1212789)Termination reason: Instruction limit
% 4.66/1.44 % (1212789)Termination phase: Saturation
% 4.66/1.44 % (1212789)Time elapsed: 0.011 s
% 4.66/1.44 % (1212789)Peak memory usage: 89 MB
% 4.66/1.44 % (1212789)Instructions burned: 17 (million)
% 4.66/1.44 % (1212791)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=3900700909:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.66/1.44 % (1212790)Instruction limit reached!
% 4.66/1.44 % (1212790)------------------------------
% 4.66/1.44 % (1212790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.44 % (1212790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.44 % (1212790)CaDiCaL version: 2.1.3
% 4.66/1.44 % (1212790)Termination reason: Instruction limit
% 4.66/1.44 % (1212790)Termination phase: Saturation
% 4.66/1.44 % (1212790)Time elapsed: 0.019 s
% 4.66/1.44 % (1212790)Peak memory usage: 89 MB
% 4.66/1.44 % (1212790)Instructions burned: 24 (million)
% 4.66/1.44 % (1212774)Instruction limit reached!
% 4.66/1.44 % (1212774)------------------------------
% 4.66/1.44 % (1212774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.66/1.44 % (1212774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.66/1.44 % (1212774)CaDiCaL version: 2.1.3
% 4.66/1.44 % (1212774)Termination reason: Instruction limit
% 4.66/1.44 % (1212774)Termination phase: Saturation
% 4.66/1.44 % (1212774)Time elapsed: 0.212 s
% 4.66/1.44 % (1212774)Peak memory usage: 117 MB
% 4.66/1.44 % (1212774)Instructions burned: 307 (million)
% 4.66/1.44 % (1212793)Instruction limit reached!
% 4.66/1.44 % (1212793)------------------------------
% 4.66/1.44 % (1212793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212793)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212793)Termination reason: Instruction limit
% 5.33/1.52 % (1212793)Termination phase: Saturation
% 5.33/1.52 % (1212793)Time elapsed: 0.025 s
% 5.33/1.52 % (1212793)Peak memory usage: 89 MB
% 5.33/1.52 % (1212793)Instructions burned: 89 (million)
% 5.33/1.52 % (1212791)Instruction limit reached!
% 5.33/1.52 % (1212791)------------------------------
% 5.33/1.52 % (1212791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212791)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212791)Termination reason: Instruction limit
% 5.33/1.52 % (1212791)Termination phase: Saturation
% 5.33/1.52 % (1212791)Time elapsed: 0.021 s
% 5.33/1.52 % (1212791)Peak memory usage: 90 MB
% 5.33/1.52 % (1212791)Instructions burned: 28 (million)
% 5.33/1.52 % (1212795)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4289941958:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.33/1.52 % (1212795)Instruction limit reached!
% 5.33/1.52 % (1212795)------------------------------
% 5.33/1.52 % (1212795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212795)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212795)Termination reason: Instruction limit
% 5.33/1.52 % (1212795)Termination phase: Naming
% 5.33/1.52 % (1212795)Time elapsed: 0.002 s
% 5.33/1.52 % (1212795)Peak memory usage: 86 MB
% 5.33/1.52 % (1212795)Instructions burned: 2 (million)
% 5.33/1.52 % (1212804)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=118274453:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.33/1.52 % (1212796)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1072494815:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.33/1.52 % (1212804)Instruction limit reached!
% 5.33/1.52 % (1212804)------------------------------
% 5.33/1.52 % (1212804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212804)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212804)Termination reason: Instruction limit
% 5.33/1.52 % (1212804)Termination phase: Saturation
% 5.33/1.52 % (1212804)Time elapsed: 0.003 s
% 5.33/1.52 % (1212804)Peak memory usage: 88 MB
% 5.33/1.52 % (1212804)Instructions burned: 9 (million)
% 5.33/1.52 % (1212801)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=548956845:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.33/1.52 % (1212801)Instruction limit reached!
% 5.33/1.52 % (1212801)------------------------------
% 5.33/1.52 % (1212801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212801)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212801)Termination reason: Instruction limit
% 5.33/1.52 % (1212801)Termination phase: Property scanning
% 5.33/1.52 % (1212801)Time elapsed: 0.003 s
% 5.33/1.52 % (1212801)Peak memory usage: 86 MB
% 5.33/1.52 % (1212801)Instructions burned: 4 (million)
% 5.33/1.52 % (1212802)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1470387156:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.33/1.52 % (1212803)lrs+10_1_thi=all:si=on:fd=off:random_seed=4222260054:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.33/1.52 % (1212805)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2100944926:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.33/1.52 % (1212805)Instruction limit reached!
% 5.33/1.52 % (1212805)------------------------------
% 5.33/1.52 % (1212805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212805)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212805)Termination reason: Instruction limit
% 5.33/1.52 % (1212805)Termination phase: Preprocessing 3
% 5.33/1.52 % (1212805)Time elapsed: 0.002 s
% 5.33/1.52 % (1212805)Peak memory usage: 86 MB
% 5.33/1.52 % (1212805)Instructions burned: 2 (million)
% 5.33/1.52 % (1212796)First to succeed.
% 5.33/1.52 % (1212796)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1212768"
% 5.33/1.52 % (1212803)Instruction limit reached!
% 5.33/1.52 % (1212803)------------------------------
% 5.33/1.52 % (1212803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212803)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212803)Termination reason: Instruction limit
% 5.33/1.52 % (1212803)Termination phase: Saturation
% 5.33/1.52 % (1212803)Time elapsed: 0.059 s
% 5.33/1.52 % (1212803)Peak memory usage: 116 MB
% 5.33/1.52 % (1212803)Instructions burned: 53 (million)
% 5.33/1.52 % (1212802)Instruction limit reached!
% 5.33/1.52 % (1212802)------------------------------
% 5.33/1.52 % (1212802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212802)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212802)Termination reason: Instruction limit
% 5.33/1.52 % (1212802)Termination phase: Saturation
% 5.33/1.52 % (1212802)Time elapsed: 0.088 s
% 5.33/1.52 % (1212802)Peak memory usage: 133 MB
% 5.33/1.52 % (1212802)Instructions burned: 66 (million)
% 5.33/1.52 % (1212810)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1814507270:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 5.33/1.52 % (1212807)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1188642961:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.33/1.52 % (1212807)Instruction limit reached!
% 5.33/1.52 % (1212807)------------------------------
% 5.33/1.52 % (1212807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212807)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212807)Termination reason: Instruction limit
% 5.33/1.52 % (1212807)Termination phase: Preprocessing 3
% 5.33/1.52 % (1212807)Time elapsed: 0.002 s
% 5.33/1.52 % (1212807)Peak memory usage: 86 MB
% 5.33/1.52 % (1212807)Instructions burned: 3 (million)
% 5.33/1.52 % (1212812)dis+10_1_si=on:random_seed=2954793815:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 5.33/1.52 % (1212812)Instruction limit reached!
% 5.33/1.52 % (1212812)------------------------------
% 5.33/1.52 % (1212812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212812)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212812)Termination reason: Instruction limit
% 5.33/1.52 % (1212812)Termination phase: Saturation
% 5.33/1.52 % (1212812)Time elapsed: 0.008 s
% 5.33/1.52 % (1212812)Peak memory usage: 88 MB
% 5.33/1.52 % (1212812)Instructions burned: 11 (million)
% 5.33/1.52 % (1212810)Instruction limit reached!
% 5.33/1.52 % (1212810)------------------------------
% 5.33/1.52 % (1212810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.52 % (1212810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.52 % (1212810)CaDiCaL version: 2.1.3
% 5.33/1.52 % (1212810)Termination reason: Instruction limit
% 5.33/1.53 % (1212810)Termination phase: Saturation
% 5.33/1.53 % (1212810)Time elapsed: 0.059 s
% 5.33/1.53 % (1212810)Peak memory usage: 117 MB
% 5.33/1.53 % (1212810)Instructions burned: 128 (million)
% 5.33/1.53 % (1212816)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3663958539:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 5.33/1.53 % (1212816)Instruction limit reached!
% 5.33/1.53 % (1212816)------------------------------
% 5.33/1.53 % (1212816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.53 % (1212816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.53 % (1212816)CaDiCaL version: 2.1.3
% 5.33/1.53 % (1212816)Termination reason: Instruction limit
% 5.33/1.53 % (1212816)Termination phase: Saturation
% 5.33/1.53 % (1212816)Time elapsed: 0.018 s
% 5.33/1.53 % (1212816)Peak memory usage: 89 MB
% 5.33/1.53 % (1212816)Instructions burned: 27 (million)
% 5.33/1.53 % (1212817)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=590587553: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_2993 on theBenchmark for (2993ds/35Mi)
% 5.33/1.53 % (1212820)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2093473894:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 5.33/1.53 % (1212820)Instruction limit reached!
% 5.33/1.53 % (1212820)------------------------------
% 5.33/1.53 % (1212820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.53 % (1212820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.53 % (1212820)CaDiCaL version: 2.1.3
% 5.33/1.53 % (1212820)Termination reason: Instruction limit
% 5.33/1.53 % (1212820)Termination phase: Preprocessing 3
% 5.33/1.53 % (1212820)Time elapsed: 0.002 s
% 5.33/1.53 % (1212820)Peak memory usage: 86 MB
% 5.33/1.53 % (1212820)Instructions burned: 2 (million)
% 5.33/1.53 % (1212821)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1848518399:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 5.33/1.53 % (1212817)Instruction limit reached!
% 5.33/1.53 % (1212817)------------------------------
% 5.33/1.53 % (1212817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.53 % (1212817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.53 % (1212817)CaDiCaL version: 2.1.3
% 5.33/1.53 % (1212817)Termination reason: Instruction limit
% 5.33/1.53 % (1212817)Termination phase: Saturation
% 5.33/1.53 % (1212817)Time elapsed: 0.027 s
% 5.33/1.53 % (1212817)Peak memory usage: 89 MB
% 5.33/1.53 % (1212817)Instructions burned: 35 (million)
% 5.33/1.53 % (1212821)Instruction limit reached!
% 5.33/1.53 % (1212821)------------------------------
% 5.33/1.53 % (1212821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.53 % (1212821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.53 % (1212821)CaDiCaL version: 2.1.3
% 5.33/1.53 % (1212821)Termination reason: Instruction limit
% 5.33/1.53 % (1212821)Termination phase: Saturation
% 5.33/1.53 % (1212821)Time elapsed: 0.006 s
% 5.33/1.53 % (1212821)Peak memory usage: 88 MB
% 5.33/1.53 % (1212821)Instructions burned: 8 (million)
% 5.33/1.53 % (1212824)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1488496248:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 5.33/1.53 % (1212824)Instruction limit reached!
% 5.33/1.53 % (1212824)------------------------------
% 5.33/1.53 % (1212824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.53 % (1212824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.53 % (1212824)CaDiCaL version: 2.1.3
% 5.33/1.53 % (1212824)Termination reason: Instruction limit
% 5.33/1.53 % (1212824)Termination phase: Saturation
% 5.33/1.53 % (1212824)Time elapsed: 0.018 s
% 5.33/1.53 % (1212824)Peak memory usage: 112 MB
% 5.33/1.53 % (1212824)Instructions burned: 14 (million)
% 5.33/1.53 % (1212823)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=692221327:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 5.33/1.53 % (1212796)Refutation found. Thanks to Tanya!
% 5.33/1.53 % SZS status Theorem for theBenchmark
% 5.33/1.53 % SZS output start Proof for theBenchmark
% See solution above
% 6.55/1.72 % (1212796)------------------------------
% 6.55/1.72 % (1212796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.55/1.72 % (1212796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.55/1.72 % (1212796)CaDiCaL version: 2.1.3
% 6.55/1.72 % (1212796)Termination reason: Refutation
% 6.55/1.72 % (1212796)Time elapsed: 0.073 s
% 6.55/1.72 % (1212796)Peak memory usage: 91 MB
% 6.55/1.72 % (1212796)Instructions burned: 98 (million)
% 6.55/1.72 % (1212796)------------------------------
% 6.55/1.72 % (1212796)------------------------------
% 6.55/1.72 % (1212768)Success in time 0.834 s
% 6.55/1.72 % Vampire exiting
%------------------------------------------------------------------------------