%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW638_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:40:34 PM UTC 2026
% Result : Theorem 162.48s 40.94s
% Output : Refutation 162.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 21
% Syntax : Number of formulae : 139 ( 58 unt; 0 typ; 7 def)
% Number of atoms : 499 ( 244 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 483 ( 123 ~; 173 |; 154 &)
% ( 15 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 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 : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 61 ( 61 usr; 19 con; 0-8 aty)
% Number of variables : 348 ( 225 !; 123 ?; 348 :)
% 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,
char2: $tType ).
tff(type_def_10,type,
regexp1: $tType ).
tff(type_def_11,type,
list_char: $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_10,type,
char1: ty ).
tff(func_def_11,type,
regexp: ty ).
tff(func_def_12,type,
empty1: regexp1 ).
tff(func_def_13,type,
epsilon1: regexp1 ).
tff(func_def_14,type,
char3: char2 > regexp1 ).
tff(func_def_15,type,
alt1: ( regexp1 * regexp1 ) > regexp1 ).
tff(func_def_16,type,
concat1: ( regexp1 * regexp1 ) > regexp1 ).
tff(func_def_17,type,
star1: regexp1 > regexp1 ).
tff(func_def_18,type,
match_regexp1: ( ty * regexp1 * uni * uni * uni * uni * uni * uni ) > uni ).
tff(func_def_19,type,
char_proj_11: regexp1 > char2 ).
tff(func_def_20,type,
alt_proj_11: regexp1 > regexp1 ).
tff(func_def_21,type,
alt_proj_21: regexp1 > regexp1 ).
tff(func_def_22,type,
concat_proj_11: regexp1 > regexp1 ).
tff(func_def_23,type,
concat_proj_21: regexp1 > regexp1 ).
tff(func_def_24,type,
star_proj_11: regexp1 > regexp1 ).
tff(func_def_25,type,
list: ty > ty ).
tff(func_def_26,type,
nil: ty > uni ).
tff(func_def_27,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_28,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_29,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_30,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_31,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_34,type,
length1: ( ty * uni ) > $int ).
tff(func_def_37,type,
t2tb: list_char > uni ).
tff(func_def_38,type,
tb2t: uni > list_char ).
tff(func_def_39,type,
t2tb1: char2 > uni ).
tff(func_def_40,type,
tb2t1: uni > char2 ).
tff(func_def_42,type,
sK4: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_43,type,
sK5: ( list_char * regexp1 ) > list_char ).
tff(func_def_44,type,
sK6: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_45,type,
sK7: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_46,type,
sK8: ( regexp1 * list_char ) > list_char ).
tff(func_def_47,type,
sK9: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_48,type,
sK10: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_49,type,
sK11: ( list_char * regexp1 ) > list_char ).
tff(func_def_50,type,
sK12: ( list_char * regexp1 ) > list_char ).
tff(func_def_51,type,
sK13: ( regexp1 * list_char ) > list_char ).
tff(func_def_52,type,
sK14: ( regexp1 * list_char ) > list_char ).
tff(func_def_53,type,
sK15: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_54,type,
sK16: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_55,type,
sK17: ( regexp1 * list_char ) > char2 ).
tff(func_def_56,type,
sK18: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_57,type,
sK19: regexp1 ).
tff(func_def_58,type,
sK20: bool1 ).
tff(func_def_59,type,
sK21: regexp1 ).
tff(func_def_60,type,
sK22: bool1 ).
tff(func_def_61,type,
sK23: ( ty * uni * uni ) > uni ).
tff(func_def_62,type,
sK24: ( ty * uni * uni ) > uni ).
tff(func_def_63,type,
sF25: uni ).
tff(func_def_64,type,
sF26: list_char ).
tff(func_def_65,type,
sF27: regexp1 ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
mem2: ( list_char * regexp1 ) > $o ).
tff(pred_def_6,type,
sP0: ( regexp1 * list_char ) > $o ).
tff(pred_def_7,type,
sP1: ( list_char * regexp1 ) > $o ).
tff(pred_def_8,type,
sP2: ( regexp1 * list_char ) > $o ).
tff(pred_def_9,type,
sP3: ( list_char * regexp1 ) > $o ).
tff(f22,axiom,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != concat1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',epsilon_Concat) ).
tff(f25,axiom,
! [X0: char2,X2: regexp1,X1: regexp1] : ( char3(X0) != concat1(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',char_Concat) ).
tff(f27,axiom,
! [X2: regexp1,X3: regexp1,X0: regexp1,X1: regexp1] : ( alt1(X0,X1) != concat1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt_Concat) ).
tff(f29,axiom,
! [X0: regexp1,X2: regexp1,X1: regexp1] : ( concat1(X0,X1) != star1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',concat_Star) ).
tff(f34,axiom,
! [X1: regexp1,X0: regexp1] : ( concat_proj_21(concat1(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',concat_proj_2_def) ).
tff(f43,axiom,
! [X1: uni,X0: ty] : sort1(X0,cons_proj_1(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cons_proj_1_sort1) ).
tff(f47,axiom,
! [X1: uni,X0: ty] :
( ( X1 = cons(X0,cons_proj_1(X0,X1),cons_proj_2(X0,X1)) )
| ( X1 = nil(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',list_inversion) ).
tff(f49,axiom,
! [X1: uni,X0: ty] :
( ! [X3: uni,X2: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) )
& ( infix_plpl(X0,nil(X0),X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(f57,axiom,
! [X0: ty,X1: uni] :
( sort1(X0,X1)
=> ( ~ mem(X0,X1,nil(X0))
& ! [X3: uni,X2: uni] :
( sort1(X0,X2)
=> ( mem(X0,X1,cons(X0,X2,X3))
<=> ( ( X1 = X2 )
| mem(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_def) ).
tff(f58,axiom,
! [X1: uni,X3: uni,X0: ty,X2: uni] :
( mem(X0,X1,infix_plpl(X0,X2,X3))
<=> ( mem(X0,X1,X2)
| mem(X0,X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_append) ).
tff(f61,axiom,
! [X0: list_char] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL) ).
tff(f62,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f73,axiom,
! [X1: regexp1,X0: list_char] :
( mem2(X0,X1)
=> ( ? [X4: regexp1,X3: list_char,X5: regexp1] :
( mem2(X3,X5)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ? [X4: regexp1,X3: list_char,X5: regexp1] :
( ( X1 = alt1(X4,X5) )
& mem2(X3,X4)
& ( X0 = X3 ) )
| ( ( X0 = tb2t(nil(char1)) )
& ( X1 = epsilon1 ) )
| ? [X6: list_char,X7: list_char,X5: regexp1,X4: regexp1] :
( ( X1 = concat1(X4,X5) )
& ( X0 = tb2t(infix_plpl(char1,t2tb(X6),t2tb(X7))) )
& mem2(X7,X5)
& mem2(X6,X4) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char1,t2tb1(X2),nil(char1))) )
& ( X1 = char3(X2) ) )
| ? [X8: regexp1,X7: list_char,X6: list_char] :
( ( X1 = star1(X8) )
& mem2(X7,star1(X8))
& ( X0 = tb2t(infix_plpl(char1,t2tb(X6),t2tb(X7))) )
& mem2(X6,X8) )
| ? [X8: regexp1] :
( ( X1 = star1(X8) )
& ( X0 = tb2t(nil(char1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_inversion) ).
tff(f74,conjecture,
! [X2: bool1,X0: regexp1,X1: regexp1] :
( ( ( X2 = true1 )
<=> mem2(tb2t(nil(char1)),X0) )
=> ( ( X2 = true1 )
=> ! [X3: bool1] :
( ( ( X3 = true1 )
<=> mem2(tb2t(nil(char1)),X1) )
=> ( mem2(tb2t(nil(char1)),concat1(X0,X1))
=> ( X3 = true1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_accepts_epsilon) ).
tff(f75,negated_conjecture,
~ ! [X2: bool1,X0: regexp1,X1: regexp1] :
( ( ( X2 = true1 )
<=> mem2(tb2t(nil(char1)),X0) )
=> ( ( X2 = true1 )
=> ! [X3: bool1] :
( ( ( X3 = true1 )
<=> mem2(tb2t(nil(char1)),X1) )
=> ( mem2(tb2t(nil(char1)),concat1(X0,X1))
=> ( X3 = true1 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f74]) ).
tff(f98,plain,
! [X2: regexp1,X1: regexp1,X3: regexp1,X0: regexp1] : ( concat1(X0,X1) != alt1(X2,X3) ),
inference(rectify,[],[f27]) ).
tff(f102,plain,
! [X1: ty,X0: uni] : sort1(X1,cons_proj_1(X1,X0)),
inference(rectify,[],[f43]) ).
tff(f103,plain,
! [X1: ty,X0: uni] :
( ! [X2: uni,X3: uni] : ( cons(X1,X3,infix_plpl(X1,X2,X0)) = infix_plpl(X1,cons(X1,X3,X2),X0) )
& ( infix_plpl(X1,nil(X1),X0) = X0 ) ),
inference(rectify,[],[f49]) ).
tff(f113,plain,
! [X0: uni,X1: ty] :
( ( nil(X1) = X0 )
| ( cons(X1,cons_proj_1(X1,X0),cons_proj_2(X1,X0)) = X0 ) ),
inference(rectify,[],[f47]) ).
tff(f114,plain,
~ ! [X1: regexp1,X2: regexp1,X0: bool1] :
( ( mem2(tb2t(nil(char1)),X1)
<=> ( true1 = X0 ) )
=> ( ( true1 = X0 )
=> ! [X3: bool1] :
( ( mem2(tb2t(nil(char1)),X2)
<=> ( X3 = true1 ) )
=> ( mem2(tb2t(nil(char1)),concat1(X1,X2))
=> ( X3 = true1 ) ) ) ) ),
inference(rectify,[],[f75]) ).
tff(f119,plain,
! [X0: regexp1,X1: list_char] :
( mem2(X1,X0)
=> ( ? [X16: regexp1] :
( ( tb2t(nil(char1)) = X1 )
& ( star1(X16) = X0 ) )
| ? [X13: regexp1,X15: list_char,X14: list_char] :
( mem2(X14,star1(X13))
& ( tb2t(infix_plpl(char1,t2tb(X15),t2tb(X14))) = X1 )
& ( star1(X13) = X0 )
& mem2(X15,X13) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| ? [X12: char2] :
( ( tb2t(cons(char1,t2tb1(X12),nil(char1))) = X1 )
& ( char3(X12) = X0 ) )
| ? [X8: list_char,X9: list_char,X11: regexp1,X10: regexp1] :
( mem2(X9,X10)
& ( concat1(X11,X10) = X0 )
& mem2(X8,X11)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ? [X4: regexp1,X3: list_char,X2: regexp1] :
( ( alt1(X2,X4) = X0 )
& ( X1 = X3 )
& mem2(X3,X4) )
| ? [X7: regexp1,X6: list_char,X5: regexp1] :
( ( X1 = X6 )
& mem2(X6,X5)
& ( alt1(X5,X7) = X0 ) ) ) ),
inference(rectify,[],[f73]) ).
tff(f120,plain,
! [X1: regexp1,X0: char2,X2: regexp1] : ( char3(X0) != concat1(X2,X1) ),
inference(rectify,[],[f25]) ).
tff(f123,plain,
! [X1: regexp1,X0: regexp1,X2: regexp1] : ( star1(X1) != concat1(X0,X2) ),
inference(rectify,[],[f29]) ).
tff(f134,plain,
! [X0: ty,X1: uni] :
( sort1(X0,X1)
=> ( ! [X3: uni,X2: uni] :
( sort1(X0,X3)
=> ( ( mem(X0,X1,X2)
| ( X1 = X3 ) )
<=> mem(X0,X1,cons(X0,X3,X2)) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(rectify,[],[f57]) ).
tff(f135,plain,
! [X2: ty,X1: uni,X0: uni,X3: uni] :
( ( mem(X2,X0,X3)
| mem(X2,X0,X1) )
<=> mem(X2,X0,infix_plpl(X2,X3,X1)) ),
inference(rectify,[],[f58]) ).
tff(f149,plain,
? [X1: regexp1,X2: regexp1,X0: bool1] :
( ? [X3: bool1] :
( ( true1 != X3 )
& mem2(tb2t(nil(char1)),concat1(X1,X2))
& ( mem2(tb2t(nil(char1)),X2)
<=> ( X3 = true1 ) ) )
& ( true1 = X0 )
& ( mem2(tb2t(nil(char1)),X1)
<=> ( true1 = X0 ) ) ),
inference(ennf_transformation,[],[f114]) ).
tff(f150,plain,
? [X2: regexp1,X0: bool1,X1: regexp1] :
( ( mem2(tb2t(nil(char1)),X1)
<=> ( true1 = X0 ) )
& ( true1 = X0 )
& ? [X3: bool1] :
( mem2(tb2t(nil(char1)),concat1(X1,X2))
& ( true1 != X3 )
& ( mem2(tb2t(nil(char1)),X2)
<=> ( X3 = true1 ) ) ) ),
inference(flattening,[],[f149]) ).
tff(f155,plain,
! [X0: regexp1,X1: list_char] :
( ? [X16: regexp1] :
( ( tb2t(nil(char1)) = X1 )
& ( star1(X16) = X0 ) )
| ? [X13: regexp1,X15: list_char,X14: list_char] :
( mem2(X14,star1(X13))
& ( tb2t(infix_plpl(char1,t2tb(X15),t2tb(X14))) = X1 )
& ( star1(X13) = X0 )
& mem2(X15,X13) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| ? [X12: char2] :
( ( tb2t(cons(char1,t2tb1(X12),nil(char1))) = X1 )
& ( char3(X12) = X0 ) )
| ? [X8: list_char,X9: list_char,X11: regexp1,X10: regexp1] :
( mem2(X9,X10)
& ( concat1(X11,X10) = X0 )
& mem2(X8,X11)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ? [X4: regexp1,X3: list_char,X2: regexp1] :
( ( alt1(X2,X4) = X0 )
& ( X1 = X3 )
& mem2(X3,X4) )
| ? [X7: regexp1,X6: list_char,X5: regexp1] :
( ( X1 = X6 )
& mem2(X6,X5)
& ( alt1(X5,X7) = X0 ) )
| ~ mem2(X1,X0) ),
inference(ennf_transformation,[],[f119]) ).
tff(f156,plain,
! [X0: regexp1,X1: list_char] :
( ? [X12: char2] :
( ( tb2t(cons(char1,t2tb1(X12),nil(char1))) = X1 )
& ( char3(X12) = X0 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| ? [X7: regexp1,X6: list_char,X5: regexp1] :
( ( X1 = X6 )
& mem2(X6,X5)
& ( alt1(X5,X7) = X0 ) )
| ? [X16: regexp1] :
( ( tb2t(nil(char1)) = X1 )
& ( star1(X16) = X0 ) )
| ? [X4: regexp1,X3: list_char,X2: regexp1] :
( ( alt1(X2,X4) = X0 )
& ( X1 = X3 )
& mem2(X3,X4) )
| ~ mem2(X1,X0)
| ? [X13: regexp1,X15: list_char,X14: list_char] :
( mem2(X14,star1(X13))
& ( tb2t(infix_plpl(char1,t2tb(X15),t2tb(X14))) = X1 )
& ( star1(X13) = X0 )
& mem2(X15,X13) )
| ? [X8: list_char,X9: list_char,X11: regexp1,X10: regexp1] :
( mem2(X9,X10)
& ( concat1(X11,X10) = X0 )
& mem2(X8,X11)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) ) ),
inference(flattening,[],[f155]) ).
tff(f161,plain,
! [X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ( ! [X3: uni,X2: uni] :
( ~ sort1(X0,X3)
| ( ( mem(X0,X1,X2)
| ( X1 = X3 ) )
<=> mem(X0,X1,cons(X0,X3,X2)) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(ennf_transformation,[],[f134]) ).
tff(f162,definition,
! [X0: regexp1,X1: list_char] :
( ? [X8: list_char,X9: list_char,X11: regexp1,X10: regexp1] :
( mem2(X9,X10)
& ( concat1(X11,X10) = X0 )
& mem2(X8,X11)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f163,definition,
! [X1: list_char,X0: regexp1] :
( ? [X13: regexp1,X15: list_char,X14: list_char] :
( mem2(X14,star1(X13))
& ( tb2t(infix_plpl(char1,t2tb(X15),t2tb(X14))) = X1 )
& ( star1(X13) = X0 )
& mem2(X15,X13) )
| ~ sP1(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f164,definition,
! [X0: regexp1,X1: list_char] :
( ? [X4: regexp1,X3: list_char,X2: regexp1] :
( ( alt1(X2,X4) = X0 )
& ( X1 = X3 )
& mem2(X3,X4) )
| ~ sP2(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f165,definition,
! [X1: list_char,X0: regexp1] :
( ? [X7: regexp1,X6: list_char,X5: regexp1] :
( ( X1 = X6 )
& mem2(X6,X5)
& ( alt1(X5,X7) = X0 ) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
tff(f166,plain,
! [X0: regexp1,X1: list_char] :
( ? [X12: char2] :
( ( tb2t(cons(char1,t2tb1(X12),nil(char1))) = X1 )
& ( char3(X12) = X0 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| sP3(X1,X0)
| ? [X16: regexp1] :
( ( tb2t(nil(char1)) = X1 )
& ( star1(X16) = X0 ) )
| sP2(X0,X1)
| ~ mem2(X1,X0)
| sP1(X1,X0)
| sP0(X0,X1) ),
inference(definition_folding,[],[f156,f165,f164,f163,f162]) ).
tff(f170,plain,
! [X0: regexp1,X1: regexp1] : ( concat_proj_21(concat1(X1,X0)) = X0 ),
inference(rectify,[],[f34]) ).
tff(f173,plain,
! [X0: ty,X1: uni] : sort1(X0,cons_proj_1(X0,X1)),
inference(rectify,[],[f102]) ).
tff(f175,plain,
! [X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ( ! [X3: uni,X2: uni] :
( ~ sort1(X0,X3)
| ( ( mem(X0,X1,X2)
| ( X1 = X3 )
| ~ mem(X0,X1,cons(X0,X3,X2)) )
& ( mem(X0,X1,cons(X0,X3,X2))
| ( ~ mem(X0,X1,X2)
& ( X1 != X3 ) ) ) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(nnf_transformation,[],[f161]) ).
tff(f176,plain,
! [X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ( ! [X3: uni,X2: uni] :
( ~ sort1(X0,X3)
| ( ( mem(X0,X1,X2)
| ( X1 = X3 )
| ~ mem(X0,X1,cons(X0,X3,X2)) )
& ( mem(X0,X1,cons(X0,X3,X2))
| ( ~ mem(X0,X1,X2)
& ( X1 != X3 ) ) ) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(flattening,[],[f175]) ).
tff(f177,plain,
! [X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ( ! [X2: uni,X3: uni] :
( ~ sort1(X0,X2)
| ( ( mem(X0,X1,X3)
| ( X1 = X2 )
| ~ mem(X0,X1,cons(X0,X2,X3)) )
& ( mem(X0,X1,cons(X0,X2,X3))
| ( ~ mem(X0,X1,X3)
& ( X1 != X2 ) ) ) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(rectify,[],[f176]) ).
tff(f178,plain,
! [X0: ty,X1: uni] :
( ! [X2: uni,X3: uni] : ( infix_plpl(X0,cons(X0,X3,X2),X1) = cons(X0,X3,infix_plpl(X0,X2,X1)) )
& ( infix_plpl(X0,nil(X0),X1) = X1 ) ),
inference(rectify,[],[f103]) ).
tff(f181,plain,
! [X1: list_char,X0: regexp1] :
( ? [X7: regexp1,X6: list_char,X5: regexp1] :
( ( X1 = X6 )
& mem2(X6,X5)
& ( alt1(X5,X7) = X0 ) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f165]) ).
tff(f182,plain,
! [X0: list_char,X1: regexp1] :
( ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( X0 = X3 )
& mem2(X3,X4)
& ( alt1(X4,X2) = X1 ) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f181]) ).
tff(f183,plain,
! [X0: list_char,X1: regexp1] :
( ( ( sK5(X0,X1) = X0 )
& mem2(sK5(X0,X1),sK6(X0,X1))
& ( alt1(sK6(X0,X1),sK4(X0,X1)) = X1 ) )
| ~ sP3(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X2,sK4(X0,X1)),skolemize(X3,sK5(X0,X1)),skolemize(X4,sK6(X0,X1))],[f182]) ).
tff(f184,plain,
! [X0: regexp1,X1: list_char] :
( ? [X4: regexp1,X3: list_char,X2: regexp1] :
( ( alt1(X2,X4) = X0 )
& ( X1 = X3 )
& mem2(X3,X4) )
| ~ sP2(X0,X1) ),
inference(nnf_transformation,[],[f164]) ).
tff(f185,plain,
! [X0: regexp1,X1: list_char] :
( ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( alt1(X4,X2) = X0 )
& ( X1 = X3 )
& mem2(X3,X2) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f184]) ).
tff(f186,plain,
! [X0: regexp1,X1: list_char] :
( ( ( alt1(sK9(X0,X1),sK7(X0,X1)) = X0 )
& ( sK8(X0,X1) = X1 )
& mem2(sK8(X0,X1),sK7(X0,X1)) )
| ~ sP2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X2,sK7(X0,X1)),skolemize(X3,sK8(X0,X1)),skolemize(X4,sK9(X0,X1))],[f185]) ).
tff(f187,plain,
! [X1: list_char,X0: regexp1] :
( ? [X13: regexp1,X15: list_char,X14: list_char] :
( mem2(X14,star1(X13))
& ( tb2t(infix_plpl(char1,t2tb(X15),t2tb(X14))) = X1 )
& ( star1(X13) = X0 )
& mem2(X15,X13) )
| ~ sP1(X1,X0) ),
inference(nnf_transformation,[],[f163]) ).
tff(f188,plain,
! [X0: list_char,X1: regexp1] :
( ? [X2: regexp1,X3: list_char,X4: list_char] :
( mem2(X4,star1(X2))
& ( tb2t(infix_plpl(char1,t2tb(X3),t2tb(X4))) = X0 )
& ( star1(X2) = X1 )
& mem2(X3,X2) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f187]) ).
tff(f189,plain,
! [X0: list_char,X1: regexp1] :
( ( mem2(sK12(X0,X1),star1(sK10(X0,X1)))
& ( tb2t(infix_plpl(char1,t2tb(sK11(X0,X1)),t2tb(sK12(X0,X1)))) = X0 )
& ( star1(sK10(X0,X1)) = X1 )
& mem2(sK11(X0,X1),sK10(X0,X1)) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X2,sK10(X0,X1)),skolemize(X3,sK11(X0,X1)),skolemize(X4,sK12(X0,X1))],[f188]) ).
tff(f190,plain,
! [X0: regexp1,X1: list_char] :
( ? [X8: list_char,X9: list_char,X11: regexp1,X10: regexp1] :
( mem2(X9,X10)
& ( concat1(X11,X10) = X0 )
& mem2(X8,X11)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f162]) ).
tff(f191,plain,
! [X0: regexp1,X1: list_char] :
( ? [X2: list_char,X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X5)
& ( concat1(X4,X5) = X0 )
& mem2(X2,X4)
& ( tb2t(infix_plpl(char1,t2tb(X2),t2tb(X3))) = X1 ) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f190]) ).
tff(f192,plain,
! [X0: regexp1,X1: list_char] :
( ( mem2(sK14(X0,X1),sK16(X0,X1))
& ( concat1(sK15(X0,X1),sK16(X0,X1)) = X0 )
& mem2(sK13(X0,X1),sK15(X0,X1))
& ( tb2t(infix_plpl(char1,t2tb(sK13(X0,X1)),t2tb(sK14(X0,X1)))) = X1 ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16]),skolemize(X2,sK13(X0,X1)),skolemize(X3,sK14(X0,X1)),skolemize(X4,sK15(X0,X1)),skolemize(X5,sK16(X0,X1))],[f191]) ).
tff(f193,plain,
! [X0: regexp1,X1: list_char] :
( ? [X2: char2] :
( ( tb2t(cons(char1,t2tb1(X2),nil(char1))) = X1 )
& ( char3(X2) = X0 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| sP3(X1,X0)
| ? [X3: regexp1] :
( ( tb2t(nil(char1)) = X1 )
& ( star1(X3) = X0 ) )
| sP2(X0,X1)
| ~ mem2(X1,X0)
| sP1(X1,X0)
| sP0(X0,X1) ),
inference(rectify,[],[f166]) ).
tff(f194,plain,
! [X0: regexp1,X1: list_char] :
( ( ( tb2t(cons(char1,t2tb1(sK17(X0,X1)),nil(char1))) = X1 )
& ( char3(sK17(X0,X1)) = X0 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| sP3(X1,X0)
| ( ( tb2t(nil(char1)) = X1 )
& ( star1(sK18(X0,X1)) = X0 ) )
| sP2(X0,X1)
| ~ mem2(X1,X0)
| sP1(X1,X0)
| sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18]),skolemize(X2,sK17(X0,X1)),skolemize(X3,sK18(X0,X1))],[f193]) ).
tff(f205,plain,
! [X0: regexp1,X1: regexp1,X2: regexp1] : ( star1(X0) != concat1(X1,X2) ),
inference(rectify,[],[f123]) ).
tff(f208,plain,
! [X0: regexp1,X1: regexp1,X2: regexp1,X3: regexp1] : ( alt1(X0,X2) != concat1(X3,X1) ),
inference(rectify,[],[f98]) ).
tff(f209,plain,
! [X2: ty,X1: uni,X0: uni,X3: uni] :
( ( mem(X2,X0,X3)
| mem(X2,X0,X1)
| ~ mem(X2,X0,infix_plpl(X2,X3,X1)) )
& ( mem(X2,X0,infix_plpl(X2,X3,X1))
| ( ~ mem(X2,X0,X3)
& ~ mem(X2,X0,X1) ) ) ),
inference(nnf_transformation,[],[f135]) ).
tff(f210,plain,
! [X2: ty,X1: uni,X0: uni,X3: uni] :
( ( mem(X2,X0,X3)
| mem(X2,X0,X1)
| ~ mem(X2,X0,infix_plpl(X2,X3,X1)) )
& ( mem(X2,X0,infix_plpl(X2,X3,X1))
| ( ~ mem(X2,X0,X3)
& ~ mem(X2,X0,X1) ) ) ),
inference(flattening,[],[f209]) ).
tff(f211,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( ( mem(X0,X2,X3)
| mem(X0,X2,X1)
| ~ mem(X0,X2,infix_plpl(X0,X3,X1)) )
& ( mem(X0,X2,infix_plpl(X0,X3,X1))
| ( ~ mem(X0,X2,X3)
& ~ mem(X0,X2,X1) ) ) ),
inference(rectify,[],[f210]) ).
tff(f212,plain,
! [X0: regexp1,X1: char2,X2: regexp1] : ( concat1(X2,X0) != char3(X1) ),
inference(rectify,[],[f120]) ).
tff(f218,plain,
? [X2: regexp1,X0: bool1,X1: regexp1] :
( ( mem2(tb2t(nil(char1)),X1)
| ( true1 != X0 ) )
& ( ( true1 = X0 )
| ~ mem2(tb2t(nil(char1)),X1) )
& ( true1 = X0 )
& ? [X3: bool1] :
( mem2(tb2t(nil(char1)),concat1(X1,X2))
& ( true1 != X3 )
& ( mem2(tb2t(nil(char1)),X2)
| ( true1 != X3 ) )
& ( ( X3 = true1 )
| ~ mem2(tb2t(nil(char1)),X2) ) ) ),
inference(nnf_transformation,[],[f150]) ).
tff(f219,plain,
? [X2: regexp1,X0: bool1,X1: regexp1] :
( ( mem2(tb2t(nil(char1)),X1)
| ( true1 != X0 ) )
& ( ( true1 = X0 )
| ~ mem2(tb2t(nil(char1)),X1) )
& ( true1 = X0 )
& ? [X3: bool1] :
( mem2(tb2t(nil(char1)),concat1(X1,X2))
& ( true1 != X3 )
& ( mem2(tb2t(nil(char1)),X2)
| ( true1 != X3 ) )
& ( ( X3 = true1 )
| ~ mem2(tb2t(nil(char1)),X2) ) ) ),
inference(flattening,[],[f218]) ).
tff(f220,plain,
? [X0: regexp1,X1: bool1,X2: regexp1] :
( ( mem2(tb2t(nil(char1)),X2)
| ( true1 != X1 ) )
& ( ( true1 = X1 )
| ~ mem2(tb2t(nil(char1)),X2) )
& ( true1 = X1 )
& ? [X3: bool1] :
( mem2(tb2t(nil(char1)),concat1(X2,X0))
& ( true1 != X3 )
& ( mem2(tb2t(nil(char1)),X0)
| ( true1 != X3 ) )
& ( ( X3 = true1 )
| ~ mem2(tb2t(nil(char1)),X0) ) ) ),
inference(rectify,[],[f219]) ).
tff(f221,plain,
( ( mem2(tb2t(nil(char1)),sK21)
| ( true1 != sK20 ) )
& ( ( true1 = sK20 )
| ~ mem2(tb2t(nil(char1)),sK21) )
& ( true1 = sK20 )
& mem2(tb2t(nil(char1)),concat1(sK21,sK19))
& ( true1 != sK22 )
& ( mem2(tb2t(nil(char1)),sK19)
| ( true1 != sK22 ) )
& ( ( true1 = sK22 )
| ~ mem2(tb2t(nil(char1)),sK19) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20,sK21,sK22]),skolemize(X0,sK19),skolemize(X1,sK20),skolemize(X2,sK21),skolemize(X3,sK22)],[f220]) ).
tff(f234,plain,
! [X0: list_char] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f61]) ).
tff(f235,plain,
! [X0: regexp1,X1: regexp1] : ( concat_proj_21(concat1(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f170]) ).
tff(f238,plain,
! [X0: ty,X1: uni] : sort1(X0,cons_proj_1(X0,X1)),
inference(cnf_transformation,[],[f173]) ).
tff(f240,plain,
! [X0: ty,X1: uni] :
( ~ mem(X0,X1,nil(X0))
| ~ sort1(X0,X1) ),
inference(cnf_transformation,[],[f177]) ).
tff(f241,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ~ sort1(X0,X2)
| mem(X0,X1,cons(X0,X2,X3))
| ( X1 != X2 ) ),
inference(cnf_transformation,[],[f177]) ).
tff(f244,plain,
! [X0: ty,X1: uni] : ( infix_plpl(X0,nil(X0),X1) = X1 ),
inference(cnf_transformation,[],[f178]) ).
tff(f253,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP3(X0,X1)
| ( alt1(sK6(X0,X1),sK4(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f183]) ).
tff(f258,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP2(X0,X1)
| ( alt1(sK9(X0,X1),sK7(X0,X1)) = X0 ) ),
inference(cnf_transformation,[],[f186]) ).
tff(f260,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP1(X0,X1)
| ( star1(sK10(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f189]) ).
tff(f263,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP0(X0,X1)
| ( tb2t(infix_plpl(char1,t2tb(sK13(X0,X1)),t2tb(sK14(X0,X1)))) = X1 ) ),
inference(cnf_transformation,[],[f192]) ).
tff(f265,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP0(X0,X1)
| ( concat1(sK15(X0,X1),sK16(X0,X1)) = X0 ) ),
inference(cnf_transformation,[],[f192]) ).
tff(f266,plain,
! [X0: regexp1,X1: list_char] :
( mem2(sK14(X0,X1),sK16(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f192]) ).
tff(f267,plain,
! [X0: regexp1,X1: list_char] :
( ~ mem2(X1,X0)
| ( star1(sK18(X0,X1)) = X0 )
| sP0(X0,X1)
| sP3(X1,X0)
| ( char3(sK17(X0,X1)) = X0 )
| sP2(X0,X1)
| sP1(X1,X0)
| ( epsilon1 = X0 ) ),
inference(cnf_transformation,[],[f194]) ).
tff(f293,plain,
! [X2: regexp1,X0: regexp1,X1: regexp1] : ( star1(X0) != concat1(X1,X2) ),
inference(cnf_transformation,[],[f205]) ).
tff(f299,plain,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != concat1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
tff(f301,plain,
! [X2: regexp1,X3: regexp1,X0: regexp1,X1: regexp1] : ( alt1(X0,X2) != concat1(X3,X1) ),
inference(cnf_transformation,[],[f208]) ).
tff(f305,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( mem(X0,X2,infix_plpl(X0,X3,X1))
| ~ mem(X0,X2,X3) ),
inference(cnf_transformation,[],[f211]) ).
tff(f307,plain,
! [X2: regexp1,X0: regexp1,X1: char2] : ( concat1(X2,X0) != char3(X1) ),
inference(cnf_transformation,[],[f212]) ).
tff(f318,plain,
( ( true1 = sK22 )
| ~ mem2(tb2t(nil(char1)),sK19) ),
inference(cnf_transformation,[],[f221]) ).
tff(f320,plain,
true1 != sK22,
inference(cnf_transformation,[],[f221]) ).
tff(f321,plain,
mem2(tb2t(nil(char1)),concat1(sK21,sK19)),
inference(cnf_transformation,[],[f221]) ).
tff(f322,plain,
true1 = sK20,
inference(cnf_transformation,[],[f221]) ).
tff(f326,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f62]) ).
tff(f331,plain,
! [X0: uni,X1: ty] :
( ( cons(X1,cons_proj_1(X1,X0),cons_proj_2(X1,X0)) = X0 )
| ( nil(X1) = X0 ) ),
inference(cnf_transformation,[],[f113]) ).
tff(f344,plain,
sK20 != sK22,
inference(definition_unfolding,[],[f320,f322]) ).
tff(f346,plain,
( ( sK20 = sK22 )
| ~ mem2(tb2t(nil(char1)),sK19) ),
inference(definition_unfolding,[],[f318,f322]) ).
tff(f347,plain,
! [X2: uni,X3: uni,X0: ty] :
( ~ sort1(X0,X2)
| ~ sort1(X0,X2)
| mem(X0,X2,cons(X0,X2,X3)) ),
inference(equality_resolution,[],[f241]) ).
tff(f350,definition,
sF25 = nil(char1),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f351,plain,
nil(char1) = sF25,
inference(reorient_equations,[],[f350]) ).
tff(f352,definition,
sF26 = tb2t(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f353,plain,
tb2t(sF25) = sF26,
inference(reorient_equations,[],[f352]) ).
tff(f356,definition,
sF27 = concat1(sK21,sK19),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f357,plain,
mem2(sF26,sF27),
inference(definition_folding,[],[f321,f356,f353,f351]) ).
tff(f359,plain,
( ~ mem2(sF26,sK19)
| ( sK20 = sK22 ) ),
inference(definition_folding,[],[f346,f353,f351]) ).
tff(f363,plain,
! [X2: uni,X3: uni,X0: ty] :
( mem(X0,X2,cons(X0,X2,X3))
| ~ sort1(X0,X2) ),
inference(duplicate_literal_removal,[],[f347]) ).
tff(f367,plain,
~ mem2(sF26,sK19),
inference(forward_subsumption_resolution,[],[f359,f344]) ).
tff(f2953,plain,
sF25 = t2tb(sF26),
inference(superposition,[],[f326,f353]) ).
tff(f3105,plain,
epsilon1 != sF27,
inference(superposition,[],[f299,f356]) ).
tff(f3111,plain,
sK19 = concat_proj_21(sF27),
inference(superposition,[],[f235,f356]) ).
tff(f3355,plain,
! [X0: regexp1] : ( star1(X0) != sF27 ),
inference(superposition,[],[f293,f356]) ).
tff(f3404,plain,
! [X0: char2] : ( char3(X0) != sF27 ),
inference(superposition,[],[f307,f356]) ).
tff(f4884,plain,
! [X0: uni] : ( infix_plpl(char1,sF25,X0) = X0 ),
inference(superposition,[],[f244,f351]) ).
tff(f5089,plain,
! [X0: regexp1,X1: regexp1] : ( alt1(X0,X1) != sF27 ),
inference(superposition,[],[f301,f356]) ).
tff(f5386,plain,
! [X0: uni] :
( ~ mem(char1,X0,sF25)
| ~ sort1(char1,X0) ),
inference(superposition,[],[f240,f351]) ).
tff(f10316,plain,
! [X0: uni,X1: ty] :
( mem(X1,cons_proj_1(X1,X0),X0)
| ~ sort1(X1,cons_proj_1(X1,X0))
| ( nil(X1) = X0 ) ),
inference(superposition,[],[f363,f331]) ).
tff(f10319,plain,
! [X0: uni,X1: ty] :
( mem(X1,cons_proj_1(X1,X0),X0)
| ( nil(X1) = X0 ) ),
inference(forward_subsumption_resolution,[],[f10316,f238]) ).
tff(f12133,plain,
( ( sF27 = star1(sK18(sF27,sF26)) )
| sP0(sF27,sF26)
| sP1(sF26,sF27)
| ( sF27 = char3(sK17(sF27,sF26)) )
| sP3(sF26,sF27)
| sP2(sF27,sF26)
| ( epsilon1 = sF27 ) ),
inference(resolution,[],[f267,f357]) ).
tff(f12138,plain,
( sP0(sF27,sF26)
| sP3(sF26,sF27)
| sP1(sF26,sF27)
| sP2(sF27,sF26)
| ( sF27 = char3(sK17(sF27,sF26)) )
| ( epsilon1 = sF27 ) ),
inference(forward_subsumption_resolution,[],[f12133,f3355]) ).
tff(f12146,plain,
( sP0(sF27,sF26)
| sP1(sF26,sF27)
| ( epsilon1 = sF27 )
| sP2(sF27,sF26)
| sP3(sF26,sF27) ),
inference(forward_subsumption_resolution,[],[f12138,f3404]) ).
tff(f12152,plain,
( sP2(sF27,sF26)
| sP0(sF27,sF26)
| sP1(sF26,sF27)
| sP3(sF26,sF27) ),
inference(forward_subsumption_resolution,[],[f12146,f3105]) ).
tff(f12154,plain,
( sP1(sF26,sF27)
| sP0(sF27,sF26)
| ( sF27 = alt1(sK9(sF27,sF26),sK7(sF27,sF26)) )
| sP3(sF26,sF27) ),
inference(resolution,[],[f12152,f258]) ).
tff(f12156,plain,
( sP3(sF26,sF27)
| sP0(sF27,sF26)
| sP1(sF26,sF27) ),
inference(forward_subsumption_resolution,[],[f12154,f5089]) ).
tff(f12175,plain,
( sP0(sF27,sF26)
| sP1(sF26,sF27)
| ( alt1(sK6(sF26,sF27),sK4(sF26,sF27)) = sF27 ) ),
inference(resolution,[],[f12156,f253]) ).
tff(f12177,plain,
( sP1(sF26,sF27)
| sP0(sF27,sF26) ),
inference(forward_subsumption_resolution,[],[f12175,f5089]) ).
tff(f12221,plain,
( ( sF27 = star1(sK10(sF26,sF27)) )
| sP0(sF27,sF26) ),
inference(resolution,[],[f12177,f260]) ).
tff(f12222,plain,
sP0(sF27,sF26),
inference(forward_subsumption_resolution,[],[f12221,f3355]) ).
tff(f12252,plain,
tb2t(infix_plpl(char1,t2tb(sK13(sF27,sF26)),t2tb(sK14(sF27,sF26)))) = sF26,
inference(resolution,[],[f12222,f263]) ).
tff(f12253,plain,
sF27 = concat1(sK15(sF27,sF26),sK16(sF27,sF26)),
inference(resolution,[],[f12222,f265]) ).
tff(f12271,plain,
sK16(sF27,sF26) = concat_proj_21(sF27),
inference(superposition,[],[f235,f12253]) ).
tff(f12279,plain,
sK16(sF27,sF26) = sK19,
inference(forward_demodulation,[],[f12271,f3111]) ).
tff(f12402,plain,
( ~ sP0(sF27,sF26)
| mem2(sK14(sF27,sF26),sK19) ),
inference(superposition,[],[f266,f12279]) ).
tff(f12404,plain,
mem2(sK14(sF27,sF26),sK19),
inference(forward_subsumption_resolution,[],[f12402,f12222]) ).
tff(f12635,plain,
infix_plpl(char1,t2tb(sK13(sF27,sF26)),t2tb(sK14(sF27,sF26))) = t2tb(sF26),
inference(superposition,[],[f326,f12252]) ).
tff(f12636,plain,
sF25 = infix_plpl(char1,t2tb(sK13(sF27,sF26)),t2tb(sK14(sF27,sF26))),
inference(forward_demodulation,[],[f12635,f2953]) ).
tff(f12645,plain,
! [X0: uni] :
( ~ mem(char1,X0,t2tb(sK13(sF27,sF26)))
| mem(char1,X0,sF25) ),
inference(superposition,[],[f305,f12636]) ).
tff(f18016,plain,
( mem(char1,cons_proj_1(char1,t2tb(sK13(sF27,sF26))),sF25)
| ( nil(char1) = t2tb(sK13(sF27,sF26)) ) ),
inference(resolution,[],[f10319,f12645]) ).
tff(f18021,plain,
( mem(char1,cons_proj_1(char1,t2tb(sK13(sF27,sF26))),sF25)
| ( sF25 = t2tb(sK13(sF27,sF26)) ) ),
inference(forward_demodulation,[],[f18016,f351]) ).
tff(f18028,plain,
( ~ sort1(char1,cons_proj_1(char1,t2tb(sK13(sF27,sF26))))
| ( sF25 = t2tb(sK13(sF27,sF26)) ) ),
inference(resolution,[],[f18021,f5386]) ).
tff(f18032,plain,
sF25 = t2tb(sK13(sF27,sF26)),
inference(forward_subsumption_resolution,[],[f18028,f238]) ).
tff(f18044,plain,
tb2t(infix_plpl(char1,sF25,t2tb(sK14(sF27,sF26)))) = sF26,
inference(superposition,[],[f12252,f18032]) ).
tff(f18067,plain,
tb2t(t2tb(sK14(sF27,sF26))) = sF26,
inference(forward_demodulation,[],[f18044,f4884]) ).
tff(f18073,plain,
sK14(sF27,sF26) = sF26,
inference(forward_demodulation,[],[f18067,f234]) ).
tff(f18290,plain,
mem2(sF26,sK19),
inference(superposition,[],[f12404,f18073]) ).
tff(f18301,plain,
$false,
inference(forward_subsumption_resolution,[],[f18290,f367]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW638_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n017.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:19:06 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.62/0.82 % (3586966)Will run a generic schedule for satisfiability detection.
% 3.62/0.82 % (3586978)% WARNING: option uhcvi not known.
% 3.62/0.82 % (3586978)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2526428257:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.62/0.82 % (3586977)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1459158437_2999 on theBenchmark for (2999ds/0Mi)
% 3.62/0.82 % (3586980)dis+10_1_sil=32000:sp=arity:random_seed=2821001469:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.62/0.82 % (3586981)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2941207893:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.62/0.82 % (3586979)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2510027812:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.62/0.82 % (3586982)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1592834457:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.62/0.82 % (3586983)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1291442531:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.62/0.82 % (3586977)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.62/0.82 % (3586977)Terminated due to inappropriate strategy.
% 3.62/0.82 % (3586977)------------------------------
% 3.62/0.82 % (3586977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.82 % (3586977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.82 % (3586977)CaDiCaL version: 2.1.3
% 3.62/0.82 % (3586977)Termination reason: Inappropriate
% 3.62/0.82 % (3586977)Time elapsed: 0.004 s
% 3.62/0.82 % (3586977)Peak memory usage: 10 MB
% 3.62/0.82 % (3586977)Instructions burned: 6 (million)
% 3.62/0.82 % (3586977)------------------------------
% 3.62/0.82 % (3586977)------------------------------
% 3.62/0.82 % (3586997)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4114178073:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.62/0.82 % (3586997)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.62/0.82 % (3586997)Terminated due to inappropriate strategy.
% 3.62/0.82 % (3586997)------------------------------
% 3.62/0.82 % (3586997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.82 % (3586997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.82 % (3586997)CaDiCaL version: 2.1.3
% 3.62/0.82 % (3586997)Termination reason: Inappropriate
% 3.62/0.82 % (3586997)Time elapsed: 0.003 s
% 3.62/0.82 % (3586997)Peak memory usage: 10 MB
% 3.62/0.82 % (3586997)Instructions burned: 5 (million)
% 3.62/0.82 % (3586997)------------------------------
% 3.62/0.82 % (3586997)------------------------------
% 3.62/0.82 % (3587007)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=150778774:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.62/0.82 % (3586980)Instruction limit reached!
% 3.62/0.82 % (3586980)------------------------------
% 3.62/0.82 % (3586980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.82 % (3586980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.82 % (3586980)CaDiCaL version: 2.1.3
% 3.62/0.82 % (3586980)Termination reason: Instruction limit
% 3.62/0.82 % (3586980)Termination phase: Saturation
% 3.62/0.82 % (3586980)Time elapsed: 0.058 s
% 3.62/0.82 % (3586980)Peak memory usage: 12 MB
% 3.62/0.82 % (3586980)Instructions burned: 111 (million)
% 3.62/0.82 % (3586982)Instruction limit reached!
% 3.62/0.82 % (3586982)------------------------------
% 3.62/0.82 % (3586982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.82 % (3586982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.82 % (3586982)CaDiCaL version: 2.1.3
% 3.62/0.82 % (3586982)Termination reason: Instruction limit
% 3.62/0.82 % (3586982)Termination phase: Saturation
% 3.62/0.82 % (3586982)Time elapsed: 0.057 s
% 3.62/0.82 % (3586982)Peak memory usage: 12 MB
% 3.62/0.82 % (3586982)Instructions burned: 136 (million)
% 3.62/0.82 % (3586981)Instruction limit reached!
% 3.62/0.82 % (3586981)------------------------------
% 3.62/0.82 % (3586981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.82 % (3586981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.82 % (3586981)CaDiCaL version: 2.1.3
% 3.62/0.82 % (3586981)Termination reason: Instruction limit
% 4.08/0.93 % (3586981)Termination phase: Saturation
% 4.08/0.93 % (3586981)Time elapsed: 0.063 s
% 4.08/0.93 % (3586981)Peak memory usage: 12 MB
% 4.08/0.93 % (3586981)Instructions burned: 116 (million)
% 4.08/0.93 % (3587013)ott-21_1_sil=16000:fs=off:random_seed=3219661150:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.08/0.93 % (3587012)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3308263132:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.08/0.93 % (3586983)Instruction limit reached!
% 4.08/0.93 % (3586983)------------------------------
% 4.08/0.93 % (3586983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/0.93 % (3586983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/0.93 % (3586983)CaDiCaL version: 2.1.3
% 4.08/0.93 % (3586983)Termination reason: Instruction limit
% 4.08/0.93 % (3586983)Termination phase: Saturation
% 4.08/0.93 % (3586983)Time elapsed: 0.078 s
% 4.08/0.93 % (3586983)Peak memory usage: 12 MB
% 4.08/0.93 % (3586983)Instructions burned: 159 (million)
% 4.08/0.93 % (3587014)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3292029643:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 4.08/0.93 % (3587019)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2149207154:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.08/0.93 % (3587019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.08/0.93 % (3587019)Terminated due to inappropriate strategy.
% 4.08/0.93 % (3587019)------------------------------
% 4.08/0.93 % (3587019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/0.93 % (3587019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/0.93 % (3587019)CaDiCaL version: 2.1.3
% 4.08/0.93 % (3587019)Termination reason: Inappropriate
% 4.08/0.93 % (3587019)Time elapsed: 0.003 s
% 4.08/0.93 % (3587019)Peak memory usage: 10 MB
% 4.08/0.93 % (3587019)Instructions burned: 5 (million)
% 4.08/0.93 % (3587019)------------------------------
% 4.08/0.93 % (3587019)------------------------------
% 4.08/0.93 % (3587007)Instruction limit reached!
% 4.08/0.93 % (3587007)------------------------------
% 4.08/0.93 % (3587007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/0.93 % (3587007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/0.93 % (3587007)CaDiCaL version: 2.1.3
% 4.08/0.93 % (3587007)Termination reason: Instruction limit
% 4.08/0.93 % (3587007)Termination phase: Saturation
% 4.08/0.93 % (3587007)Time elapsed: 0.074 s
% 4.08/0.93 % (3587007)Peak memory usage: 12 MB
% 4.08/0.93 % (3587007)Instructions burned: 131 (million)
% 4.08/0.93 % (3587036)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1290018181:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.08/0.93 % (3587037)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4157222810:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.08/0.93 % (3587037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.08/0.93 % (3587037)Terminated due to inappropriate strategy.
% 4.08/0.93 % (3587037)------------------------------
% 4.08/0.93 % (3587037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/0.93 % (3587037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/0.93 % (3587037)CaDiCaL version: 2.1.3
% 4.08/0.93 % (3587037)Termination reason: Inappropriate
% 4.08/0.93 % (3587037)Time elapsed: 0.003 s
% 4.08/0.93 % (3587037)Peak memory usage: 10 MB
% 4.08/0.93 % (3587037)Instructions burned: 5 (million)
% 4.08/0.93 % (3587037)------------------------------
% 4.08/0.93 % (3587037)------------------------------
% 4.08/0.93 % (3587044)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=928565953:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 4.08/0.93 % (3587013)Instruction limit reached!
% 4.08/0.93 % (3587013)------------------------------
% 4.08/0.93 % (3587013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/0.93 % (3587013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/0.93 % (3587013)CaDiCaL version: 2.1.3
% 4.08/0.93 % (3587013)Termination reason: Instruction limit
% 4.08/0.93 % (3587013)Termination phase: Saturation
% 23.59/3.78 % (3587013)Time elapsed: 0.092 s
% 23.59/3.78 % (3587013)Peak memory usage: 12 MB
% 23.59/3.78 % (3587013)Instructions burned: 181 (million)
% 23.59/3.78 % (3587052)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3863807971:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 23.59/3.78 % (3587014)Instruction limit reached!
% 23.59/3.78 % (3587014)------------------------------
% 23.59/3.78 % (3587014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.59/3.78 % (3587014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.59/3.78 % (3587014)CaDiCaL version: 2.1.3
% 23.59/3.78 % (3587014)Termination reason: Instruction limit
% 23.59/3.78 % (3587014)Termination phase: Saturation
% 23.59/3.78 % (3587014)Time elapsed: 0.199 s
% 23.59/3.78 % (3587014)Peak memory usage: 12 MB
% 23.59/3.78 % (3587014)Instructions burned: 479 (million)
% 23.59/3.78 % (3587075)fmb+10_1_sil=64000:random_seed=2274061438:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 23.59/3.78 % (3587075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 23.59/3.78 % (3587075)Terminated due to inappropriate strategy.
% 23.59/3.78 % (3587075)------------------------------
% 23.59/3.78 % (3587075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.59/3.78 % (3587075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.59/3.78 % (3587075)CaDiCaL version: 2.1.3
% 23.59/3.78 % (3587075)Termination reason: Inappropriate
% 23.59/3.78 % (3587075)Time elapsed: 0.004 s
% 23.59/3.78 % (3587075)Peak memory usage: 10 MB
% 23.59/3.78 % (3587075)Instructions burned: 5 (million)
% 23.59/3.78 % (3587075)------------------------------
% 23.59/3.78 % (3587075)------------------------------
% 23.59/3.78 % (3587077)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3885616901:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 23.59/3.78 % (3587077)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 23.59/3.78 % (3587077)Terminated due to inappropriate strategy.
% 23.59/3.78 % (3587077)------------------------------
% 23.59/3.78 % (3587077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.59/3.78 % (3587077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.59/3.78 % (3587077)CaDiCaL version: 2.1.3
% 23.59/3.78 % (3587077)Termination reason: Inappropriate
% 23.59/3.78 % (3587077)Time elapsed: 0.003 s
% 23.59/3.78 % (3587077)Peak memory usage: 10 MB
% 23.59/3.78 % (3587077)Instructions burned: 5 (million)
% 23.59/3.78 % (3587077)------------------------------
% 23.59/3.78 % (3587077)------------------------------
% 23.59/3.78 % (3587079)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4187278714:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 23.59/3.78 % (3587079)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 23.59/3.78 % (3587079)Terminated due to inappropriate strategy.
% 23.59/3.78 % (3587079)------------------------------
% 23.59/3.78 % (3587079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.59/3.78 % (3587079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.59/3.78 % (3587079)CaDiCaL version: 2.1.3
% 23.59/3.78 % (3587079)Termination reason: Inappropriate
% 23.59/3.78 % (3587079)Time elapsed: 0.003 s
% 23.59/3.78 % (3587079)Peak memory usage: 10 MB
% 23.59/3.78 % (3587079)Instructions burned: 5 (million)
% 23.59/3.78 % (3587079)------------------------------
% 23.59/3.78 % (3587079)------------------------------
% 23.59/3.78 % (3587012)Instruction limit reached!
% 23.59/3.78 % (3587012)------------------------------
% 23.59/3.78 % (3587012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.59/3.78 % (3587012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.59/3.78 % (3587012)CaDiCaL version: 2.1.3
% 23.59/3.78 % (3587012)Termination reason: Instruction limit
% 23.59/3.78 % (3587012)Termination phase: Saturation
% 23.59/3.78 % (3587012)Time elapsed: 0.307 s
% 23.59/3.78 % (3587012)Peak memory usage: 13 MB
% 23.59/3.78 % (3587012)Instructions burned: 686 (million)
% 23.59/3.78 % (3587081)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3644303630:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 23.59/3.78 % (3587082)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3375534026:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 23.59/3.78 % (3587052)Instruction limit reached!
% 23.59/3.78 % (3587052)------------------------------
% 37.99/5.66 % (3587052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.99/5.66 % (3587052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.99/5.66 % (3587052)CaDiCaL version: 2.1.3
% 37.99/5.66 % (3587052)Termination reason: Instruction limit
% 37.99/5.66 % (3587052)Termination phase: Saturation
% 37.99/5.66 % (3587052)Time elapsed: 0.349 s
% 37.99/5.66 % (3587052)Peak memory usage: 13 MB
% 37.99/5.66 % (3587052)Instructions burned: 879 (million)
% 37.99/5.66 % (3587044)Instruction limit reached!
% 37.99/5.66 % (3587044)------------------------------
% 37.99/5.66 % (3587044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.99/5.66 % (3587044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.99/5.66 % (3587044)CaDiCaL version: 2.1.3
% 37.99/5.66 % (3587044)Termination reason: Instruction limit
% 37.99/5.66 % (3587044)Termination phase: Saturation
% 37.99/5.66 % (3587044)Time elapsed: 0.378 s
% 37.99/5.66 % (3587044)Peak memory usage: 16 MB
% 37.99/5.66 % (3587044)Instructions burned: 693 (million)
% 37.99/5.66 % (3587085)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3294167984:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 37.99/5.66 % (3587086)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1749269989:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 37.99/5.66 % (3587085)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 37.99/5.66 % (3587085)Terminated due to inappropriate strategy.
% 37.99/5.66 % (3587085)------------------------------
% 37.99/5.66 % (3587085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.99/5.66 % (3587085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.99/5.66 % (3587085)CaDiCaL version: 2.1.3
% 37.99/5.66 % (3587085)Termination reason: Inappropriate
% 37.99/5.66 % (3587085)Time elapsed: 0.004 s
% 37.99/5.66 % (3587085)Peak memory usage: 11 MB
% 37.99/5.66 % (3587085)Instructions burned: 6 (million)
% 37.99/5.66 % (3587085)------------------------------
% 37.99/5.66 % (3587085)------------------------------
% 37.99/5.66 % (3587086)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 37.99/5.66 % (3587086)Terminated due to inappropriate strategy.
% 37.99/5.66 % (3587086)------------------------------
% 37.99/5.66 % (3587086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.99/5.66 % (3587086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.99/5.66 % (3587086)CaDiCaL version: 2.1.3
% 37.99/5.66 % (3587086)Termination reason: Inappropriate
% 37.99/5.66 % (3587086)Time elapsed: 0.003 s
% 37.99/5.66 % (3587086)Peak memory usage: 10 MB
% 37.99/5.66 % (3587086)Instructions burned: 5 (million)
% 37.99/5.66 % (3587086)------------------------------
% 37.99/5.66 % (3587086)------------------------------
% 37.99/5.66 % (3587089)ott-2_1_sil=16000:newcnf=on:random_seed=3369060364:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 37.99/5.66 % (3587090)ott+10_1_sil=32000:tgt=ground:random_seed=2848438713:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 37.99/5.66 % (3587036)Instruction limit reached!
% 37.99/5.66 % (3587036)------------------------------
% 37.99/5.66 % (3587036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.99/5.66 % (3587036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.99/5.66 % (3587036)CaDiCaL version: 2.1.3
% 37.99/5.66 % (3587036)Termination reason: Instruction limit
% 37.99/5.66 % (3587036)Termination phase: Saturation
% 37.99/5.66 % (3587036)Time elapsed: 0.504 s
% 37.99/5.66 % (3587036)Peak memory usage: 13 MB
% 37.99/5.66 % (3587036)Instructions burned: 1179 (million)
% 37.99/5.66 % (3587093)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=371256201:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 37.99/5.66 % (3587093)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 37.99/5.66 % (3587093)Terminated due to inappropriate strategy.
% 37.99/5.66 % (3587093)------------------------------
% 37.99/5.66 % (3587093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.99/5.66 % (3587093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.99/5.66 % (3587093)CaDiCaL version: 2.1.3
% 37.99/5.66 % (3587093)Termination reason: Inappropriate
% 37.99/5.66 % (3587093)Time elapsed: 0.004 s
% 37.99/5.66 % (3587093)Peak memory usage: 11 MB
% 37.99/5.66 % (3587093)Instructions burned: 6 (million)
% 96.19/13.88 % (3587093)------------------------------
% 96.19/13.88 % (3587093)------------------------------
% 96.19/13.88 % (3587095)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4041601867:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 96.19/13.88 % (3587089)Instruction limit reached!
% 96.19/13.88 % (3587089)------------------------------
% 96.19/13.88 % (3587089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.19/13.88 % (3587089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.19/13.88 % (3587089)CaDiCaL version: 2.1.3
% 96.19/13.88 % (3587089)Termination reason: Instruction limit
% 96.19/13.88 % (3587089)Termination phase: Saturation
% 96.19/13.88 % (3587089)Time elapsed: 0.316 s
% 96.19/13.88 % (3587089)Peak memory usage: 12 MB
% 96.19/13.88 % (3587089)Instructions burned: 871 (million)
% 96.19/13.88 % (3587097)dis+21_1_sil=32000:sas=cadical:random_seed=3272753136:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 96.19/13.88 % (3587082)Instruction limit reached!
% 96.19/13.88 % (3587082)------------------------------
% 96.19/13.88 % (3587082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.19/13.88 % (3587082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.19/13.88 % (3587082)CaDiCaL version: 2.1.3
% 96.19/13.88 % (3587082)Termination reason: Instruction limit
% 96.19/13.88 % (3587082)Termination phase: Saturation
% 96.19/13.88 % (3587082)Time elapsed: 0.920 s
% 96.19/13.88 % (3587082)Peak memory usage: 24 MB
% 96.19/13.88 % (3587082)Instructions burned: 1473 (million)
% 96.19/13.88 % (3587121)ott+11_1_sil=16000:gs=on:random_seed=1033181792:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 96.19/13.88 % (3587121)Instruction limit reached!
% 96.19/13.88 % (3587121)------------------------------
% 96.19/13.88 % (3587121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.19/13.88 % (3587121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.19/13.88 % (3587121)CaDiCaL version: 2.1.3
% 96.19/13.88 % (3587121)Termination reason: Instruction limit
% 96.19/13.88 % (3587121)Termination phase: Saturation
% 96.19/13.88 % (3587121)Time elapsed: 1.382 s
% 96.19/13.88 % (3587121)Peak memory usage: 14 MB
% 96.19/13.88 % (3587121)Instructions burned: 2253 (million)
% 96.19/13.88 % (3587189)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=847284414:fmbsr=1.6:i=67534_2972 on theBenchmark for (2972ds/67534Mi)
% 96.19/13.88 % (3587189)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 96.19/13.88 % (3587189)Terminated due to inappropriate strategy.
% 96.19/13.88 % (3587189)------------------------------
% 96.19/13.88 % (3587189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.19/13.88 % (3587189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.19/13.88 % (3587189)CaDiCaL version: 2.1.3
% 96.19/13.88 % (3587189)Termination reason: Inappropriate
% 96.19/13.88 % (3587189)Time elapsed: 0.006 s
% 96.19/13.88 % (3587189)Peak memory usage: 10 MB
% 96.19/13.88 % (3587189)Instructions burned: 5 (million)
% 96.19/13.88 % (3587189)------------------------------
% 96.19/13.88 % (3587189)------------------------------
% 96.19/13.88 % (3587191)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3929051396:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi)
% 96.19/13.88 % (3587095)Instruction limit reached!
% 96.19/13.88 % (3587095)------------------------------
% 96.19/13.88 % (3587095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.19/13.88 % (3587095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.19/13.88 % (3587095)CaDiCaL version: 2.1.3
% 96.19/13.88 % (3587095)Termination reason: Instruction limit
% 96.19/13.88 % (3587095)Termination phase: Saturation
% 96.19/13.88 % (3587095)Time elapsed: 2.436 s
% 96.19/13.88 % (3587095)Peak memory usage: 19 MB
% 96.19/13.88 % (3587095)Instructions burned: 3513 (million)
% 96.19/13.88 % (3587204)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3895792263:i=29340_2968 on theBenchmark for (2968ds/29340Mi)
% 96.19/13.88 % (3587090)Instruction limit reached!
% 96.19/13.88 % (3587090)------------------------------
% 96.19/13.88 % (3587090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.19/13.88 % (3587090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.19/13.88 % (3587090)CaDiCaL version: 2.1.3
% 96.19/13.88 % (3587090)Termination reason: Instruction limit
% 112.29/16.14 % (3587090)Termination phase: Saturation
% 112.29/16.14 % (3587090)Time elapsed: 2.917 s
% 112.29/16.14 % (3587090)Peak memory usage: 12 MB
% 112.29/16.14 % (3587090)Instructions burned: 5115 (million)
% 112.29/16.14 % (3587218)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1870639455:i=5211_2964 on theBenchmark for (2964ds/5211Mi)
% 112.29/16.14 % (3587081)Instruction limit reached!
% 112.29/16.14 % (3587081)------------------------------
% 112.29/16.14 % (3587081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.29/16.14 % (3587081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.29/16.14 % (3587081)CaDiCaL version: 2.1.3
% 112.29/16.14 % (3587081)Termination reason: Instruction limit
% 112.29/16.14 % (3587081)Termination phase: Saturation
% 112.29/16.14 % (3587081)Time elapsed: 3.256 s
% 112.29/16.14 % (3587081)Peak memory usage: 23 MB
% 112.29/16.14 % (3587081)Instructions burned: 5132 (million)
% 112.29/16.14 % (3587097)Instruction limit reached!
% 112.29/16.14 % (3587097)------------------------------
% 112.29/16.14 % (3587097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.29/16.14 % (3587097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.29/16.14 % (3587097)CaDiCaL version: 2.1.3
% 112.29/16.14 % (3587097)Termination reason: Instruction limit
% 112.29/16.14 % (3587097)Termination phase: Saturation
% 112.29/16.14 % (3587097)Time elapsed: 2.748 s
% 112.29/16.14 % (3587097)Peak memory usage: 19 MB
% 112.29/16.14 % (3587097)Instructions burned: 3774 (million)
% 112.29/16.14 % (3587224)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1891046636:i=5497:nm=2_2963 on theBenchmark for (2963ds/5497Mi)
% 112.29/16.14 % (3587224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.29/16.14 % (3587224)Terminated due to inappropriate strategy.
% 112.29/16.14 % (3587224)------------------------------
% 112.29/16.14 % (3587224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.29/16.14 % (3587224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.29/16.14 % (3587224)CaDiCaL version: 2.1.3
% 112.29/16.14 % (3587224)Termination reason: Inappropriate
% 112.29/16.14 % (3587224)Time elapsed: 0.004 s
% 112.29/16.14 % (3587224)Peak memory usage: 11 MB
% 112.29/16.14 % (3587224)Instructions burned: 6 (million)
% 112.29/16.14 % (3587224)------------------------------
% 112.29/16.14 % (3587224)------------------------------
% 112.29/16.14 % (3587228)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2423071791:i=14071_2962 on theBenchmark for (2962ds/14071Mi)
% 112.29/16.14 % (3587228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.29/16.14 % (3587228)Terminated due to inappropriate strategy.
% 112.29/16.14 % (3587228)------------------------------
% 112.29/16.14 % (3587228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.29/16.14 % (3587228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.29/16.14 % (3587228)CaDiCaL version: 2.1.3
% 112.29/16.14 % (3587228)Termination reason: Inappropriate
% 112.29/16.14 % (3587228)Time elapsed: 0.003 s
% 112.29/16.14 % (3587228)Peak memory usage: 11 MB
% 112.29/16.14 % (3587228)Instructions burned: 5 (million)
% 112.29/16.14 % (3587228)------------------------------
% 112.29/16.14 % (3587228)------------------------------
% 112.29/16.14 % (3587227)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3249194555:fmbsr=2:i=46332_2962 on theBenchmark for (2962ds/46332Mi)
% 112.29/16.14 % (3587227)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 112.29/16.14 % (3587227)Terminated due to inappropriate strategy.
% 112.29/16.14 % (3587227)------------------------------
% 112.29/16.14 % (3587227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.29/16.14 % (3587227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.29/16.14 % (3587227)CaDiCaL version: 2.1.3
% 112.29/16.14 % (3587227)Termination reason: Inappropriate
% 112.29/16.14 % (3587227)Time elapsed: 0.006 s
% 112.29/16.14 % (3587227)Peak memory usage: 11 MB
% 112.29/16.14 % (3587227)Instructions burned: 5 (million)
% 112.29/16.14 % (3587227)------------------------------
% 112.29/16.14 % (3587227)------------------------------
% 112.29/16.14 % (3587230)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=655283879:i=22565:add=on:rawr=on_2962 on theBenchmark for (2962ds/22565Mi)
% 112.29/16.14 % (3587232)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3869626660:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi)
% 112.29/16.14 % (3587191)Instruction limit reached!
% 113.97/16.34 % (3587191)------------------------------
% 113.97/16.34 % (3587191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.97/16.34 % (3587191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.97/16.34 % (3587191)CaDiCaL version: 2.1.3
% 113.97/16.34 % (3587191)Termination reason: Instruction limit
% 113.97/16.34 % (3587191)Termination phase: Saturation
% 113.97/16.34 % (3587191)Time elapsed: 2.544 s
% 113.97/16.34 % (3587191)Peak memory usage: 13 MB
% 113.97/16.34 % (3587191)Instructions burned: 4594 (million)
% 113.97/16.34 % (3587274)dis+10_16:1_sil=16000:random_seed=1719936231:i=9155:fsr=off_2945 on theBenchmark for (2945ds/9155Mi)
% 113.97/16.34 % (3587218)Instruction limit reached!
% 113.97/16.34 % (3587218)------------------------------
% 113.97/16.34 % (3587218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.97/16.34 % (3587218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.97/16.34 % (3587218)CaDiCaL version: 2.1.3
% 113.97/16.34 % (3587218)Termination reason: Instruction limit
% 113.97/16.34 % (3587218)Termination phase: Saturation
% 113.97/16.34 % (3587218)Time elapsed: 3.246 s
% 113.97/16.34 % (3587218)Peak memory usage: 37 MB
% 113.97/16.34 % (3587218)Instructions burned: 5213 (million)
% 113.97/16.34 % (3587429)ott-3_8_sil=64000:random_seed=3292721153:i=20139:bs=on_2931 on theBenchmark for (2931ds/20139Mi)
% 113.97/16.34 % (3587232)Instruction limit reached!
% 113.97/16.34 % (3587232)------------------------------
% 113.97/16.34 % (3587232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.97/16.34 % (3587232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.97/16.34 % (3587232)CaDiCaL version: 2.1.3
% 113.97/16.34 % (3587232)Termination reason: Instruction limit
% 113.97/16.34 % (3587232)Termination phase: Saturation
% 113.97/16.34 % (3587232)Time elapsed: 3.662 s
% 113.97/16.34 % (3587232)Peak memory usage: 13 MB
% 113.97/16.34 % (3587232)Instructions burned: 8177 (million)
% 113.97/16.34 % (3587431)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4120975977:fmbsr=2:i=32576_2925 on theBenchmark for (2925ds/32576Mi)
% 113.97/16.34 % (3587431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 113.97/16.34 % (3587431)Terminated due to inappropriate strategy.
% 113.97/16.34 % (3587431)------------------------------
% 113.97/16.34 % (3587431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.97/16.34 % (3587431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.97/16.34 % (3587431)CaDiCaL version: 2.1.3
% 113.97/16.34 % (3587431)Termination reason: Inappropriate
% 113.97/16.34 % (3587431)Time elapsed: 0.004 s
% 113.97/16.34 % (3587431)Peak memory usage: 11 MB
% 113.97/16.34 % (3587431)Instructions burned: 6 (million)
% 113.97/16.34 % (3587431)------------------------------
% 113.97/16.34 % (3587431)------------------------------
% 113.97/16.34 % (3587433)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=904575209:i=11404_2925 on theBenchmark for (2925ds/11404Mi)
% 113.97/16.34 % (3587274)Instruction limit reached!
% 113.97/16.34 % (3587274)------------------------------
% 113.97/16.34 % (3587274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.97/16.34 % (3587274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.97/16.34 % (3587274)CaDiCaL version: 2.1.3
% 113.97/16.34 % (3587274)Termination reason: Instruction limit
% 113.97/16.34 % (3587274)Termination phase: Saturation
% 113.97/16.34 % (3587274)Time elapsed: 4.637 s
% 113.97/16.34 % (3587274)Peak memory usage: 52 MB
% 113.97/16.34 % (3587274)Instructions burned: 9157 (million)
% 113.97/16.34 % (3587435)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4022905904:i=14134_2899 on theBenchmark for (2899ds/14134Mi)
% 113.97/16.34 % (3587230)Instruction limit reached!
% 113.97/16.34 % (3587230)------------------------------
% 113.97/16.34 % (3587230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.97/16.34 % (3587230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.97/16.34 % (3587230)CaDiCaL version: 2.1.3
% 113.97/16.34 % (3587230)Termination reason: Instruction limit
% 113.97/16.34 % (3587230)Termination phase: Saturation
% 113.97/16.34 % (3587230)Time elapsed: 8.064 s
% 113.97/16.34 % (3587230)Peak memory usage: 17 MB
% 113.97/16.34 % (3587230)Instructions burned: 22565 (million)
% 113.97/16.34 % (3587437)dis+33_16_sil=32000:sac=on:random_seed=2705595931:i=15851:nm=0_2881 on theBenchmark for (2881ds/15851Mi)
% 113.97/16.34 % (3587429)Instruction limit reached!
% 113.97/16.34 % (3587429)------------------------------
% 113.97/16.34 % (3587429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.70/24.36 % (3587429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.70/24.36 % (3587429)CaDiCaL version: 2.1.3
% 170.70/24.36 % (3587429)Termination reason: Instruction limit
% 170.70/24.36 % (3587429)Termination phase: Saturation
% 170.70/24.36 % (3587429)Time elapsed: 6.801 s
% 170.70/24.36 % (3587429)Peak memory usage: 15 MB
% 170.70/24.36 % (3587429)Instructions burned: 20141 (million)
% 170.70/24.36 % (3587440)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2531746862:avsq=on:i=17627:add=on:amm=off_2863 on theBenchmark for (2863ds/17627Mi)
% 170.70/24.36 % (3587204)Instruction limit reached!
% 170.70/24.36 % (3587204)------------------------------
% 170.70/24.36 % (3587204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.70/24.36 % (3587204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.70/24.36 % (3587204)CaDiCaL version: 2.1.3
% 170.70/24.36 % (3587204)Termination reason: Instruction limit
% 170.70/24.36 % (3587204)Termination phase: Saturation
% 170.70/24.36 % (3587204)Time elapsed: 10.725 s
% 170.70/24.36 % (3587204)Peak memory usage: 14 MB
% 170.70/24.36 % (3587204)Instructions burned: 29341 (million)
% 170.70/24.36 % (3587537)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3248441719:s2a=on:i=53295_2860 on theBenchmark for (2860ds/53295Mi)
% 170.70/24.36 % (3587433)Instruction limit reached!
% 170.70/24.36 % (3587433)------------------------------
% 170.70/24.36 % (3587433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.70/24.36 % (3587433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.70/24.36 % (3587433)CaDiCaL version: 2.1.3
% 170.70/24.36 % (3587433)Termination reason: Instruction limit
% 170.70/24.36 % (3587433)Termination phase: Saturation
% 170.70/24.36 % (3587433)Time elapsed: 7.073 s
% 170.70/24.36 % (3587433)Peak memory usage: 62 MB
% 170.70/24.36 % (3587433)Instructions burned: 11404 (million)
% 170.70/24.36 % (3587642)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3678968932:i=26857:ins=20_2854 on theBenchmark for (2854ds/26857Mi)
% 170.70/24.36 % (3587642)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 170.70/24.36 % (3587642)Terminated due to inappropriate strategy.
% 170.70/24.36 % (3587642)------------------------------
% 170.70/24.36 % (3587642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.70/24.36 % (3587642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.70/24.36 % (3587642)CaDiCaL version: 2.1.3
% 170.70/24.36 % (3587642)Termination reason: Inappropriate
% 170.70/24.36 % (3587642)Time elapsed: 0.003 s
% 170.70/24.36 % (3587642)Peak memory usage: 10 MB
% 170.70/24.36 % (3587642)Instructions burned: 5 (million)
% 170.70/24.36 % (3587642)------------------------------
% 170.70/24.36 % (3587642)------------------------------
% 170.70/24.36 % (3587653)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2648937557:i=28120:bs=on:fsr=off_2853 on theBenchmark for (2853ds/28120Mi)
% 170.70/24.36 % (3587435)Instruction limit reached!
% 170.70/24.36 % (3587435)------------------------------
% 170.70/24.36 % (3587435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.70/24.36 % (3587435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.70/24.36 % (3587435)CaDiCaL version: 2.1.3
% 170.70/24.36 % (3587435)Termination reason: Instruction limit
% 170.70/24.36 % (3587435)Termination phase: Saturation
% 170.70/24.36 % (3587435)Time elapsed: 5.701 s
% 170.70/24.36 % (3587435)Peak memory usage: 17 MB
% 170.70/24.36 % (3587435)Instructions burned: 14134 (million)
% 170.70/24.36 % (3587744)fmb+10_1_sil=256000:fmbss=7:random_seed=1135688467:fmbsr=1.6:i=182295_2841 on theBenchmark for (2841ds/182295Mi)
% 170.70/24.36 % (3587744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 170.70/24.36 % (3587744)Terminated due to inappropriate strategy.
% 170.70/24.36 % (3587744)------------------------------
% 170.70/24.36 % (3587744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.70/24.36 % (3587744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.70/24.36 % (3587744)CaDiCaL version: 2.1.3
% 170.70/24.36 % (3587744)Termination reason: Inappropriate
% 170.70/24.36 % (3587744)Time elapsed: 0.006 s
% 170.70/24.36 % (3587744)Peak memory usage: 10 MB
% 170.70/24.36 % (3587744)Instructions burned: 5 (million)
% 170.70/24.36 % (3587744)------------------------------
% 170.70/24.36 % (3587744)------------------------------
% 170.70/24.36 % (3587747)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1520786797:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi)
% 187.79/26.76 % (3587747)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 187.79/26.76 % (3587747)Terminated due to inappropriate strategy.
% 187.79/26.76 % (3587747)------------------------------
% 187.79/26.76 % (3587747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.79/26.76 % (3587747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.79/26.76 % (3587747)CaDiCaL version: 2.1.3
% 187.79/26.76 % (3587747)Termination reason: Inappropriate
% 187.79/26.76 % (3587747)Time elapsed: 0.008 s
% 187.79/26.76 % (3587747)Peak memory usage: 11 MB
% 187.79/26.76 % (3587747)Instructions burned: 7 (million)
% 187.79/26.76 % (3587747)------------------------------
% 187.79/26.76 % (3587747)------------------------------
% 187.79/26.76 % (3587749)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4157500506:i=160505_2840 on theBenchmark for (2840ds/160505Mi)
% 187.79/26.76 % (3587749)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 187.79/26.76 % (3587749)Terminated due to inappropriate strategy.
% 187.79/26.76 % (3587749)------------------------------
% 187.79/26.76 % (3587749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.79/26.76 % (3587749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.79/26.76 % (3587749)CaDiCaL version: 2.1.3
% 187.79/26.76 % (3587749)Termination reason: Inappropriate
% 187.79/26.76 % (3587749)Time elapsed: 0.006 s
% 187.79/26.76 % (3587749)Peak memory usage: 10 MB
% 187.79/26.76 % (3587749)Instructions burned: 5 (million)
% 187.79/26.76 % (3587749)------------------------------
% 187.79/26.76 % (3587749)------------------------------
% 187.79/26.76 % (3587751)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=232951252:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi)
% 187.79/26.76 % (3587751)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 187.79/26.76 % (3587751)Terminated due to inappropriate strategy.
% 187.79/26.76 % (3587751)------------------------------
% 187.79/26.76 % (3587751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.79/26.76 % (3587751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.79/26.76 % (3587751)CaDiCaL version: 2.1.3
% 187.79/26.76 % (3587751)Termination reason: Inappropriate
% 187.79/26.76 % (3587751)Time elapsed: 0.007 s
% 187.79/26.76 % (3587751)Peak memory usage: 11 MB
% 187.79/26.76 % (3587751)Instructions burned: 5 (million)
% 187.79/26.76 % (3587751)------------------------------
% 187.79/26.76 % (3587751)------------------------------
% 187.79/26.76 % (3587755)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2342530320:fmbsr=2:i=185024:ins=7_2840 on theBenchmark for (2840ds/185024Mi)
% 187.79/26.76 % (3587755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 187.79/26.76 % (3587755)Terminated due to inappropriate strategy.
% 187.79/26.76 % (3587755)------------------------------
% 187.79/26.76 % (3587755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.79/26.76 % (3587755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.79/26.76 % (3587755)CaDiCaL version: 2.1.3
% 187.79/26.76 % (3587755)Termination reason: Inappropriate
% 187.79/26.76 % (3587755)Time elapsed: 0.006 s
% 187.79/26.76 % (3587755)Peak memory usage: 11 MB
% 187.79/26.76 % (3587755)Instructions burned: 5 (million)
% 187.79/26.76 % (3587755)------------------------------
% 187.79/26.76 % (3587755)------------------------------
% 187.79/26.76 % (3587757)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3212186296:rtra=on_2839 on theBenchmark for (2839ds/0Mi)
% 187.79/26.76 % (3587757)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 187.79/26.76 % (3587757)Terminated due to inappropriate strategy.
% 187.79/26.76 % (3587757)------------------------------
% 187.79/26.76 % (3587757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 187.79/26.76 % (3587757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.79/26.76 % (3587757)CaDiCaL version: 2.1.3
% 187.79/26.76 % (3587757)Termination reason: Inappropriate
% 187.79/26.76 % (3587757)Time elapsed: 0.008 s
% 187.79/26.76 % (3587757)Peak memory usage: 10 MB
% 187.79/26.76 % (3587757)Instructions burned: 7 (million)
% 187.79/26.76 % (3587757)------------------------------
% 187.79/26.76 % (3587757)------------------------------
% 187.79/26.76 % (3587759)% WARNING: option uhcvi not known.
% 187.79/26.76 % (3587759)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2969249275:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi)
% 212.51/30.27 % (3587437)Instruction limit reached!
% 212.51/30.27 % (3587437)------------------------------
% 212.51/30.27 % (3587437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.51/30.27 % (3587437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.51/30.27 % (3587437)CaDiCaL version: 2.1.3
% 212.51/30.27 % (3587437)Termination reason: Instruction limit
% 212.51/30.27 % (3587437)Termination phase: Saturation
% 212.51/30.27 % (3587437)Time elapsed: 10.178 s
% 212.51/30.27 % (3587437)Peak memory usage: 71 MB
% 212.51/30.27 % (3587437)Instructions burned: 15852 (million)
% 212.51/30.27 % (3587789)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4219572539:i=176048:add=on:rtra=on:rawr=on_2779 on theBenchmark for (2779ds/176048Mi)
% 212.51/30.27 % (3587440)Instruction limit reached!
% 212.51/30.27 % (3587440)------------------------------
% 212.51/30.27 % (3587440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.51/30.27 % (3587440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.51/30.27 % (3587440)CaDiCaL version: 2.1.3
% 212.51/30.27 % (3587440)Termination reason: Instruction limit
% 212.51/30.27 % (3587440)Termination phase: Saturation
% 212.51/30.27 % (3587440)Time elapsed: 9.669 s
% 212.51/30.27 % (3587440)Peak memory usage: 16 MB
% 212.51/30.27 % (3587440)Instructions burned: 17627 (million)
% 212.51/30.27 % (3587791)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1796781902:i=206:fgj=on:rtra=on_2766 on theBenchmark for (2766ds/206Mi)
% 212.51/30.27 % (3587791)Instruction limit reached!
% 212.51/30.27 % (3587791)------------------------------
% 212.51/30.27 % (3587791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.51/30.27 % (3587791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.51/30.27 % (3587791)CaDiCaL version: 2.1.3
% 212.51/30.27 % (3587791)Termination reason: Instruction limit
% 212.51/30.27 % (3587791)Termination phase: Saturation
% 212.51/30.27 % (3587791)Time elapsed: 0.190 s
% 212.51/30.27 % (3587791)Peak memory usage: 13 MB
% 212.51/30.27 % (3587791)Instructions burned: 206 (million)
% 212.51/30.27 % (3587793)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1348007469:i=232:rtra=on_2764 on theBenchmark for (2764ds/232Mi)
% 212.51/30.28 % (3587793)Instruction limit reached!
% 212.51/30.28 % (3587793)------------------------------
% 212.51/30.28 % (3587793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.51/30.28 % (3587793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.51/30.28 % (3587793)CaDiCaL version: 2.1.3
% 212.51/30.28 % (3587793)Termination reason: Instruction limit
% 212.51/30.28 % (3587793)Termination phase: Saturation
% 212.51/30.28 % (3587793)Time elapsed: 0.137 s
% 212.51/30.28 % (3587793)Peak memory usage: 12 MB
% 212.51/30.28 % (3587793)Instructions burned: 232 (million)
% 212.51/30.28 % (3587795)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3046017282:i=262:rtra=on_2762 on theBenchmark for (2762ds/262Mi)
% 212.51/30.28 % (3587795)Instruction limit reached!
% 212.51/30.28 % (3587795)------------------------------
% 212.51/30.28 % (3587795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.51/30.28 % (3587795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.51/30.28 % (3587795)CaDiCaL version: 2.1.3
% 212.51/30.28 % (3587795)Termination reason: Instruction limit
% 212.51/30.28 % (3587795)Termination phase: Saturation
% 212.51/30.28 % (3587795)Time elapsed: 0.168 s
% 212.51/30.28 % (3587795)Peak memory usage: 12 MB
% 212.51/30.28 % (3587795)Instructions burned: 262 (million)
% 212.51/30.28 % (3587797)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1587413198:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2761 on theBenchmark for (2761ds/318Mi)
% 212.51/30.28 % (3587797)Instruction limit reached!
% 212.51/30.28 % (3587797)------------------------------
% 212.51/30.28 % (3587797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.51/30.28 % (3587797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.51/30.28 % (3587797)CaDiCaL version: 2.1.3
% 212.51/30.28 % (3587797)Termination reason: Instruction limit
% 212.51/30.28 % (3587797)Termination phase: Saturation
% 212.51/30.28 % (3587797)Time elapsed: 0.168 s
% 212.51/30.28 % (3587797)Peak memory usage: 12 MB
% 212.51/30.28 % (3587797)Instructions burned: 324 (million)
% 212.51/30.28 % (3587799)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4044107189:i=1428:nm=2:rtra=on_2759 on theBenchmark for (2759ds/1428Mi)
% 241.12/34.24 % (3587799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 241.12/34.24 % (3587799)Terminated due to inappropriate strategy.
% 241.12/34.24 % (3587799)------------------------------
% 241.12/34.24 % (3587799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.12/34.24 % (3587799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.12/34.24 % (3587799)CaDiCaL version: 2.1.3
% 241.12/34.24 % (3587799)Termination reason: Inappropriate
% 241.12/34.24 % (3587799)Time elapsed: 0.005 s
% 241.12/34.24 % (3587799)Peak memory usage: 11 MB
% 241.12/34.24 % (3587799)Instructions burned: 6 (million)
% 241.12/34.24 % (3587799)------------------------------
% 241.12/34.24 % (3587799)------------------------------
% 241.12/34.24 % (3587801)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=711744437:i=262:bd=preordered:rtra=on:fsd=on_2758 on theBenchmark for (2758ds/262Mi)
% 241.12/34.24 % (3587801)Instruction limit reached!
% 241.12/34.24 % (3587801)------------------------------
% 241.12/34.24 % (3587801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.12/34.24 % (3587801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.12/34.24 % (3587801)CaDiCaL version: 2.1.3
% 241.12/34.24 % (3587801)Termination reason: Instruction limit
% 241.12/34.24 % (3587801)Termination phase: Saturation
% 241.12/34.24 % (3587801)Time elapsed: 0.230 s
% 241.12/34.24 % (3587801)Peak memory usage: 12 MB
% 241.12/34.24 % (3587801)Instructions burned: 262 (million)
% 241.12/34.24 % (3587805)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3904539130:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/1368Mi)
% 241.12/34.24 % (3587805)Instruction limit reached!
% 241.12/34.24 % (3587805)------------------------------
% 241.12/34.24 % (3587805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.12/34.24 % (3587805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.12/34.24 % (3587805)CaDiCaL version: 2.1.3
% 241.12/34.24 % (3587805)Termination reason: Instruction limit
% 241.12/34.24 % (3587805)Termination phase: Saturation
% 241.12/34.24 % (3587805)Time elapsed: 0.988 s
% 241.12/34.24 % (3587805)Peak memory usage: 15 MB
% 241.12/34.24 % (3587805)Instructions burned: 1369 (million)
% 241.12/34.24 % (3587811)ott-21_1_sil=16000:si=on:fs=off:random_seed=814972430:i=360:av=off:fsr=off:rtra=on_2745 on theBenchmark for (2745ds/360Mi)
% 241.12/34.24 % (3587811)Instruction limit reached!
% 241.12/34.24 % (3587811)------------------------------
% 241.12/34.24 % (3587811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.12/34.24 % (3587811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.12/34.24 % (3587811)CaDiCaL version: 2.1.3
% 241.12/34.24 % (3587811)Termination reason: Instruction limit
% 241.12/34.24 % (3587811)Termination phase: Saturation
% 241.12/34.24 % (3587811)Time elapsed: 0.256 s
% 241.12/34.24 % (3587811)Peak memory usage: 13 MB
% 241.12/34.24 % (3587811)Instructions burned: 360 (million)
% 241.12/34.24 % (3587813)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3666934898:i=954:bd=all:rtra=on_2743 on theBenchmark for (2743ds/954Mi)
% 241.12/34.24 % (3587813)Instruction limit reached!
% 241.12/34.24 % (3587813)------------------------------
% 241.12/34.24 % (3587813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.12/34.24 % (3587813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.12/34.24 % (3587813)CaDiCaL version: 2.1.3
% 241.12/34.24 % (3587813)Termination reason: Instruction limit
% 241.12/34.24 % (3587813)Termination phase: Saturation
% 241.12/34.24 % (3587813)Time elapsed: 0.764 s
% 241.12/34.24 % (3587813)Peak memory usage: 13 MB
% 241.12/34.24 % (3587813)Instructions burned: 954 (million)
% 241.12/34.24 % (3587815)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2497987935:fmbsr=1.3:i=1730:ins=25:rtra=on_2735 on theBenchmark for (2735ds/1730Mi)
% 241.12/34.24 % (3587815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 241.12/34.24 % (3587815)Terminated due to inappropriate strategy.
% 241.12/34.24 % (3587815)------------------------------
% 241.12/34.24 % (3587815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.12/34.24 % (3587815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.12/34.24 % (3587815)CaDiCaL version: 2.1.3
% 241.12/34.24 % (3587815)Termination reason: Inappropriate
% 241.12/34.24 % (3587815)Time elapsed: 0.006 s
% 162.48/40.94 % (3587815)Peak memory usage: 10 MB
% 162.48/40.94 % (3587815)Instructions burned: 6 (million)
% 162.48/40.94 % (3587815)------------------------------
% 162.48/40.94 % (3587815)------------------------------
% 162.48/40.94 % (3587817)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3330270077:i=2358:rtra=on_2734 on theBenchmark for (2734ds/2358Mi)
% 162.48/40.94 % (3587817)Instruction limit reached!
% 162.48/40.94 % (3587817)------------------------------
% 162.48/40.94 % (3587817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587817)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587817)Termination reason: Instruction limit
% 162.48/40.94 % (3587817)Termination phase: Saturation
% 162.48/40.94 % (3587817)Time elapsed: 1.832 s
% 162.48/40.94 % (3587817)Peak memory usage: 15 MB
% 162.48/40.94 % (3587817)Instructions burned: 2359 (million)
% 162.48/40.94 % (3587819)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3719000015:i=1778:ins=1:rtra=on_2716 on theBenchmark for (2716ds/1778Mi)
% 162.48/40.94 % (3587819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587819)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587819)------------------------------
% 162.48/40.94 % (3587819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587819)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587819)Termination reason: Inappropriate
% 162.48/40.94 % (3587819)Time elapsed: 0.007 s
% 162.48/40.94 % (3587819)Peak memory usage: 10 MB
% 162.48/40.94 % (3587819)Instructions burned: 6 (million)
% 162.48/40.94 % (3587819)------------------------------
% 162.48/40.94 % (3587819)------------------------------
% 162.48/40.94 % (3587821)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3527125745:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/1384Mi)
% 162.48/40.94 % (3587653)Instruction limit reached!
% 162.48/40.94 % (3587653)------------------------------
% 162.48/40.94 % (3587653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587653)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587653)Termination reason: Instruction limit
% 162.48/40.94 % (3587653)Termination phase: Saturation
% 162.48/40.94 % (3587653)Time elapsed: 15.140 s
% 162.48/40.94 % (3587653)Peak memory usage: 16 MB
% 162.48/40.94 % (3587653)Instructions burned: 28120 (million)
% 162.48/40.94 % (3587825)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3815643037:i=1758:kws=inv_precedence:fsr=off:rtra=on_2702 on theBenchmark for (2702ds/1758Mi)
% 162.48/40.94 % (3587821)Instruction limit reached!
% 162.48/40.94 % (3587821)------------------------------
% 162.48/40.94 % (3587821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587821)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587821)Termination reason: Instruction limit
% 162.48/40.94 % (3587821)Termination phase: Saturation
% 162.48/40.94 % (3587821)Time elapsed: 1.508 s
% 162.48/40.94 % (3587821)Peak memory usage: 28 MB
% 162.48/40.94 % (3587821)Instructions burned: 1384 (million)
% 162.48/40.94 % (3587827)fmb+10_1_sil=64000:si=on:random_seed=3576338145:i=44122:nm=2:rtra=on:gsp=on_2700 on theBenchmark for (2700ds/44122Mi)
% 162.48/40.94 % (3587827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587827)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587827)------------------------------
% 162.48/40.94 % (3587827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587827)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587827)Termination reason: Inappropriate
% 162.48/40.94 % (3587827)Time elapsed: 0.005 s
% 162.48/40.94 % (3587827)Peak memory usage: 11 MB
% 162.48/40.94 % (3587827)Instructions burned: 6 (million)
% 162.48/40.94 % (3587827)------------------------------
% 162.48/40.94 % (3587827)------------------------------
% 162.48/40.94 % (3587829)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2508264029:i=19030:nm=5:rtra=on_2700 on theBenchmark for (2700ds/19030Mi)
% 162.48/40.94 % (3587829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587829)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587829)------------------------------
% 162.48/40.94 % (3587829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587829)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587829)Termination reason: Inappropriate
% 162.48/40.94 % (3587829)Time elapsed: 0.006 s
% 162.48/40.94 % (3587829)Peak memory usage: 10 MB
% 162.48/40.94 % (3587829)Instructions burned: 6 (million)
% 162.48/40.94 % (3587829)------------------------------
% 162.48/40.94 % (3587829)------------------------------
% 162.48/40.94 % (3587831)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=966092709:fmbsr=1.7:i=1840:rtra=on_2699 on theBenchmark for (2699ds/1840Mi)
% 162.48/40.94 % (3587831)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587831)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587831)------------------------------
% 162.48/40.94 % (3587831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587831)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587831)Termination reason: Inappropriate
% 162.48/40.94 % (3587831)Time elapsed: 0.008 s
% 162.48/40.94 % (3587831)Peak memory usage: 11 MB
% 162.48/40.94 % (3587831)Instructions burned: 6 (million)
% 162.48/40.94 % (3587831)------------------------------
% 162.48/40.94 % (3587831)------------------------------
% 162.48/40.94 % (3587833)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4082832021:i=10262:rtra=on_2699 on theBenchmark for (2699ds/10262Mi)
% 162.48/40.94 % (3587825)Instruction limit reached!
% 162.48/40.94 % (3587825)------------------------------
% 162.48/40.94 % (3587825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587825)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587825)Termination reason: Instruction limit
% 162.48/40.94 % (3587825)Termination phase: Saturation
% 162.48/40.94 % (3587825)Time elapsed: 1.358 s
% 162.48/40.94 % (3587825)Peak memory usage: 16 MB
% 162.48/40.94 % (3587825)Instructions burned: 1758 (million)
% 162.48/40.94 % (3587835)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3722872007:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2688 on theBenchmark for (2688ds/2944Mi)
% 162.48/40.94 % (3587835)Instruction limit reached!
% 162.48/40.94 % (3587835)------------------------------
% 162.48/40.94 % (3587835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587835)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587835)Termination reason: Instruction limit
% 162.48/40.94 % (3587835)Termination phase: Saturation
% 162.48/40.94 % (3587835)Time elapsed: 2.708 s
% 162.48/40.94 % (3587835)Peak memory usage: 32 MB
% 162.48/40.94 % (3587835)Instructions burned: 2945 (million)
% 162.48/40.94 % (3587839)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1776877147:i=12648:rtra=on_2660 on theBenchmark for (2660ds/12648Mi)
% 162.48/40.94 % (3587839)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587839)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587839)------------------------------
% 162.48/40.94 % (3587839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587839)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587839)Termination reason: Inappropriate
% 162.48/40.94 % (3587839)Time elapsed: 0.008 s
% 162.48/40.94 % (3587839)Peak memory usage: 11 MB
% 162.48/40.94 % (3587839)Instructions burned: 7 (million)
% 162.48/40.94 % (3587839)------------------------------
% 162.48/40.94 % (3587839)------------------------------
% 162.48/40.94 % (3587841)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=627586324:fmbsr=2.30978:i=4348:rtra=on_2660 on theBenchmark for (2660ds/4348Mi)
% 162.48/40.94 % (3587841)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587841)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587841)------------------------------
% 162.48/40.94 % (3587841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587841)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587841)Termination reason: Inappropriate
% 162.48/40.94 % (3587841)Time elapsed: 0.006 s
% 162.48/40.94 % (3587841)Peak memory usage: 10 MB
% 162.48/40.94 % (3587841)Instructions burned: 6 (million)
% 162.48/40.94 % (3587841)------------------------------
% 162.48/40.94 % (3587841)------------------------------
% 162.48/40.94 % (3587843)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2352776799:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2659 on theBenchmark for (2659ds/1738Mi)
% 162.48/40.94 % (3587843)Instruction limit reached!
% 162.48/40.94 % (3587843)------------------------------
% 162.48/40.94 % (3587843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587843)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587843)Termination reason: Instruction limit
% 162.48/40.94 % (3587843)Termination phase: Saturation
% 162.48/40.94 % (3587843)Time elapsed: 1.023 s
% 162.48/40.94 % (3587843)Peak memory usage: 12 MB
% 162.48/40.94 % (3587843)Instructions burned: 1739 (million)
% 162.48/40.94 % (3587845)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=113475342:i=10228:av=off:rtra=on_2649 on theBenchmark for (2649ds/10228Mi)
% 162.48/40.94 % (3587833)Instruction limit reached!
% 162.48/40.94 % (3587833)------------------------------
% 162.48/40.94 % (3587833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587833)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587833)Termination reason: Instruction limit
% 162.48/40.94 % (3587833)Termination phase: Saturation
% 162.48/40.94 % (3587833)Time elapsed: 8.773 s
% 162.48/40.94 % (3587833)Peak memory usage: 42 MB
% 162.48/40.94 % (3587833)Instructions burned: 10262 (million)
% 162.48/40.94 % (3587849)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1883828749:i=108564:rtra=on_2611 on theBenchmark for (2611ds/108564Mi)
% 162.48/40.94 % (3587849)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 162.48/40.94 % (3587849)Terminated due to inappropriate strategy.
% 162.48/40.94 % (3587849)------------------------------
% 162.48/40.94 % (3587849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587849)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587849)Termination reason: Inappropriate
% 162.48/40.94 % (3587849)Time elapsed: 0.008 s
% 162.48/40.94 % (3587849)Peak memory usage: 11 MB
% 162.48/40.94 % (3587849)Instructions burned: 7 (million)
% 162.48/40.94 % (3587849)------------------------------
% 162.48/40.94 % (3587849)------------------------------
% 162.48/40.94 % (3587851)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1388251238:i=7024:aac=none:rtra=on_2610 on theBenchmark for (2610ds/7024Mi)
% 162.48/40.94 % (3587845) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3586966-3587845"...
% 162.48/40.94 % (3587845)...printing done.
% 162.48/40.94 % (3587845)Refutation found. Thanks to Tanya!
% 162.48/40.94 % SZS status Theorem for theBenchmark
% 162.48/40.94 % SZS output start Proof for theBenchmark
% See solution above
% 162.48/40.94 % (3587845)------------------------------
% 162.48/40.94 % (3587845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.48/40.94 % (3587845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.48/40.94 % (3587845)CaDiCaL version: 2.1.3
% 162.48/40.94 % (3587845)Termination reason: Refutation
% 162.48/40.94 % (3587845)Time elapsed: 5.553 s
% 162.48/40.94 % (3587845)Peak memory usage: 15 MB
% 162.48/40.94 % (3587845)Instructions burned: 8048 (million)
% 162.48/40.94 % (3586966)Success in time 40.695 s
% 162.48/40.94 % Vampire exiting
%------------------------------------------------------------------------------