%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:00 PM UTC 2026
% Result : Theorem 19.61s 3.77s
% Output : Refutation 21.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 26
% Syntax : Number of formulae : 158 ( 51 unt; 0 typ; 13 def)
% Number of atoms : 551 ( 229 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 561 ( 168 ~; 205 |; 149 &)
% ( 21 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 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 : 15 ( 13 usr; 7 prp; 0-3 aty)
% Number of functors : 61 ( 61 usr; 19 con; 0-8 aty)
% Number of variables : 321 ( 0 sgn 201 !; 120 ?; 321 :)
% 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: ( uni * uni * ty ) > uni ).
tff(func_def_43,type,
sK5: ( uni * uni * ty ) > uni ).
tff(func_def_44,type,
sK6: bool1 ).
tff(func_def_45,type,
sK7: regexp1 ).
tff(func_def_46,type,
sK8: regexp1 ).
tff(func_def_47,type,
sK9: bool1 ).
tff(func_def_48,type,
sK10: ( list_char * regexp1 ) > list_char ).
tff(func_def_49,type,
sK11: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_50,type,
sK12: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_51,type,
sK13: ( regexp1 * list_char ) > regexp1 ).
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 ) > list_char ).
tff(func_def_55,type,
sK17: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_56,type,
sK18: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_57,type,
sK19: ( regexp1 * list_char ) > list_char ).
tff(func_def_58,type,
sK20: ( regexp1 * list_char ) > list_char ).
tff(func_def_59,type,
sK21: ( regexp1 * list_char ) > regexp1 ).
tff(func_def_60,type,
sK22: ( regexp1 * list_char ) > list_char ).
tff(func_def_61,type,
sK23: ( list_char * regexp1 ) > char2 ).
tff(func_def_62,type,
sK24: ( list_char * regexp1 ) > regexp1 ).
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: ( regexp1 * list_char ) > $o ).
tff(pred_def_8,type,
sP2: ( regexp1 * list_char ) > $o ).
tff(pred_def_9,type,
sP3: ( list_char * regexp1 ) > $o ).
tff(f22,axiom,
! [X1: regexp1,X0: regexp1] : ( epsilon1 != concat1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',epsilon_Concat) ).
tff(f25,axiom,
! [X2: regexp1,X1: regexp1,X0: char2] : ( char3(X0) != concat1(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',char_Concat) ).
tff(f27,axiom,
! [X1: regexp1,X0: regexp1,X2: regexp1,X3: regexp1] : ( alt1(X0,X1) != concat1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt_Concat) ).
tff(f29,axiom,
! [X2: regexp1,X1: regexp1,X0: 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,
! [X0: ty,X1: uni] : sort1(X0,cons_proj_1(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cons_proj_1_sort1) ).
tff(f47,axiom,
! [X0: ty,X1: uni] :
( ( 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(f57,axiom,
! [X1: uni,X0: ty] :
( 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,nil(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_def) ).
tff(f58,axiom,
! [X2: uni,X1: uni,X0: ty,X3: 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] :
( ( X1 = alt1(X4,X5) )
& ( X0 = X3 )
& mem2(X3,X5) )
| ? [X8: regexp1] :
( ( X1 = star1(X8) )
& ( X0 = tb2t(nil(char1)) ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char1,t2tb1(X2),nil(char1))) )
& ( X1 = char3(X2) ) )
| ? [X8: regexp1,X6: list_char,X7: list_char] :
( mem2(X7,star1(X8))
& ( X0 = tb2t(infix_plpl(char1,t2tb(X6),t2tb(X7))) )
& mem2(X6,X8)
& ( X1 = star1(X8) ) )
| ? [X5: regexp1,X4: regexp1,X3: list_char] :
( ( X1 = alt1(X4,X5) )
& mem2(X3,X4)
& ( X0 = X3 ) )
| ( ( X1 = epsilon1 )
& ( X0 = tb2t(nil(char1)) ) )
| ? [X5: regexp1,X6: list_char,X7: list_char,X4: regexp1] :
( ( X1 = concat1(X4,X5) )
& ( X0 = tb2t(infix_plpl(char1,t2tb(X6),t2tb(X7))) )
& mem2(X7,X5)
& mem2(X6,X4) ) ) ),
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] :
( ( mem2(tb2t(nil(char1)),X1)
<=> ( X3 = true1 ) )
=> ( 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] :
( ( mem2(tb2t(nil(char1)),X1)
<=> ( X3 = true1 ) )
=> ( mem2(tb2t(nil(char1)),concat1(X0,X1))
=> ( X3 = true1 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f74]) ).
tff(f98,plain,
! [X0: uni,X1: ty] :
( sort1(X1,X0)
=> ( ~ mem(X1,X0,nil(X1))
& ! [X2: uni,X3: uni] :
( sort1(X1,X2)
=> ( mem(X1,X0,cons(X1,X2,X3))
<=> ( mem(X1,X0,X3)
| ( X0 = X2 ) ) ) ) ) ),
inference(rectify,[],[f57]) ).
tff(f103,plain,
! [X3: regexp1,X1: regexp1,X0: regexp1,X2: regexp1] : ( concat1(X2,X3) != alt1(X1,X0) ),
inference(rectify,[],[f27]) ).
tff(f105,plain,
! [X0: regexp1,X2: char2,X1: regexp1] : ( char3(X2) != concat1(X1,X0) ),
inference(rectify,[],[f25]) ).
tff(f121,plain,
~ ! [X0: bool1,X1: regexp1,X2: regexp1] :
( ( 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(f125,plain,
! [X0: regexp1,X1: list_char] :
( mem2(X1,X0)
=> ( ? [X12: list_char,X11: regexp1,X10: regexp1] :
( mem2(X12,X11)
& ( X1 = X12 )
& ( alt1(X11,X10) = X0 ) )
| ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( alt1(X2,X4) = X0 )
& mem2(X3,X4)
& ( X1 = X3 ) )
| ? [X6: char2] :
( ( tb2t(cons(char1,t2tb1(X6),nil(char1))) = X1 )
& ( char3(X6) = X0 ) )
| ? [X5: regexp1] :
( ( star1(X5) = X0 )
& ( tb2t(nil(char1)) = X1 ) )
| ? [X8: list_char,X7: regexp1,X9: list_char] :
( mem2(X9,star1(X7))
& ( star1(X7) = X0 )
& mem2(X8,X7)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ? [X15: list_char,X16: regexp1,X13: regexp1,X14: list_char] :
( mem2(X14,X16)
& ( concat1(X16,X13) = X0 )
& mem2(X15,X13)
& ( tb2t(infix_plpl(char1,t2tb(X14),t2tb(X15))) = X1 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) ) ) ),
inference(rectify,[],[f73]) ).
tff(f127,plain,
! [X3: uni,X0: uni,X1: uni,X2: ty] :
( mem(X2,X1,infix_plpl(X2,X0,X3))
<=> ( mem(X2,X1,X3)
| mem(X2,X1,X0) ) ),
inference(rectify,[],[f58]) ).
tff(f128,plain,
! [X0: regexp1,X1: regexp1,X2: regexp1] : ( star1(X0) != concat1(X2,X1) ),
inference(rectify,[],[f29]) ).
tff(f133,plain,
! [X0: regexp1,X1: list_char] :
( ? [X12: list_char,X11: regexp1,X10: regexp1] :
( mem2(X12,X11)
& ( X1 = X12 )
& ( alt1(X11,X10) = X0 ) )
| ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( alt1(X2,X4) = X0 )
& mem2(X3,X4)
& ( X1 = X3 ) )
| ? [X6: char2] :
( ( tb2t(cons(char1,t2tb1(X6),nil(char1))) = X1 )
& ( char3(X6) = X0 ) )
| ? [X5: regexp1] :
( ( star1(X5) = X0 )
& ( tb2t(nil(char1)) = X1 ) )
| ? [X8: list_char,X7: regexp1,X9: list_char] :
( mem2(X9,star1(X7))
& ( star1(X7) = X0 )
& mem2(X8,X7)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ? [X15: list_char,X16: regexp1,X13: regexp1,X14: list_char] :
( mem2(X14,X16)
& ( concat1(X16,X13) = X0 )
& mem2(X15,X13)
& ( tb2t(infix_plpl(char1,t2tb(X14),t2tb(X15))) = X1 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| ~ mem2(X1,X0) ),
inference(ennf_transformation,[],[f125]) ).
tff(f134,plain,
! [X1: list_char,X0: regexp1] :
( ? [X15: list_char,X16: regexp1,X13: regexp1,X14: list_char] :
( mem2(X14,X16)
& ( concat1(X16,X13) = X0 )
& mem2(X15,X13)
& ( tb2t(infix_plpl(char1,t2tb(X14),t2tb(X15))) = X1 ) )
| ? [X12: list_char,X11: regexp1,X10: regexp1] :
( mem2(X12,X11)
& ( X1 = X12 )
& ( alt1(X11,X10) = X0 ) )
| ? [X6: char2] :
( ( tb2t(cons(char1,t2tb1(X6),nil(char1))) = X1 )
& ( char3(X6) = X0 ) )
| ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( alt1(X2,X4) = X0 )
& mem2(X3,X4)
& ( X1 = X3 ) )
| ? [X8: list_char,X7: regexp1,X9: list_char] :
( mem2(X9,star1(X7))
& ( star1(X7) = X0 )
& mem2(X8,X7)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| ~ mem2(X1,X0)
| ? [X5: regexp1] :
( ( star1(X5) = X0 )
& ( tb2t(nil(char1)) = X1 ) ) ),
inference(flattening,[],[f133]) ).
tff(f139,plain,
? [X0: bool1,X1: regexp1,X2: regexp1] :
( ? [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,[],[f121]) ).
tff(f140,plain,
? [X0: bool1,X2: regexp1,X1: regexp1] :
( ? [X3: bool1] :
( ( mem2(tb2t(nil(char1)),X2)
<=> ( X3 = true1 ) )
& ( true1 != X3 )
& mem2(tb2t(nil(char1)),concat1(X1,X2)) )
& ( true1 = X0 )
& ( mem2(tb2t(nil(char1)),X1)
<=> ( true1 = X0 ) ) ),
inference(flattening,[],[f139]) ).
tff(f154,plain,
! [X0: uni,X1: ty] :
( ~ sort1(X1,X0)
| ( ~ mem(X1,X0,nil(X1))
& ! [X3: uni,X2: uni] :
( ( mem(X1,X0,cons(X1,X2,X3))
<=> ( mem(X1,X0,X3)
| ( X0 = X2 ) ) )
| ~ sort1(X1,X2) ) ) ),
inference(ennf_transformation,[],[f98]) ).
tff(f159,definition,
! [X0: regexp1,X1: list_char] :
( ? [X8: list_char,X7: regexp1,X9: list_char] :
( mem2(X9,star1(X7))
& ( star1(X7) = X0 )
& mem2(X8,X7)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f160,definition,
! [X0: regexp1,X1: list_char] :
( ? [X15: list_char,X16: regexp1,X13: regexp1,X14: list_char] :
( mem2(X14,X16)
& ( concat1(X16,X13) = X0 )
& mem2(X15,X13)
& ( tb2t(infix_plpl(char1,t2tb(X14),t2tb(X15))) = X1 ) )
| ~ sP1(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f161,definition,
! [X0: regexp1,X1: list_char] :
( ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( alt1(X2,X4) = X0 )
& mem2(X3,X4)
& ( X1 = X3 ) )
| ~ sP2(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f162,definition,
! [X1: list_char,X0: regexp1] :
( ? [X12: list_char,X11: regexp1,X10: regexp1] :
( mem2(X12,X11)
& ( X1 = X12 )
& ( alt1(X11,X10) = X0 ) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
tff(f163,plain,
! [X1: list_char,X0: regexp1] :
( sP1(X0,X1)
| sP3(X1,X0)
| ? [X6: char2] :
( ( tb2t(cons(char1,t2tb1(X6),nil(char1))) = X1 )
& ( char3(X6) = X0 ) )
| sP2(X0,X1)
| sP0(X0,X1)
| ( ( tb2t(nil(char1)) = X1 )
& ( epsilon1 = X0 ) )
| ~ mem2(X1,X0)
| ? [X5: regexp1] :
( ( star1(X5) = X0 )
& ( tb2t(nil(char1)) = X1 ) ) ),
inference(definition_folding,[],[f134,f162,f161,f160,f159]) ).
tff(f171,plain,
? [X0: bool1,X2: regexp1,X1: regexp1] :
( ? [X3: bool1] :
( ( mem2(tb2t(nil(char1)),X2)
| ( true1 != X3 ) )
& ( ( X3 = true1 )
| ~ mem2(tb2t(nil(char1)),X2) )
& ( true1 != X3 )
& mem2(tb2t(nil(char1)),concat1(X1,X2)) )
& ( true1 = X0 )
& ( mem2(tb2t(nil(char1)),X1)
| ( true1 != X0 ) )
& ( ( true1 = X0 )
| ~ mem2(tb2t(nil(char1)),X1) ) ),
inference(nnf_transformation,[],[f140]) ).
tff(f172,plain,
? [X0: bool1,X2: regexp1,X1: regexp1] :
( ? [X3: bool1] :
( ( mem2(tb2t(nil(char1)),X2)
| ( true1 != X3 ) )
& ( ( X3 = true1 )
| ~ mem2(tb2t(nil(char1)),X2) )
& ( true1 != X3 )
& mem2(tb2t(nil(char1)),concat1(X1,X2)) )
& ( true1 = X0 )
& ( mem2(tb2t(nil(char1)),X1)
| ( true1 != X0 ) )
& ( ( true1 = X0 )
| ~ mem2(tb2t(nil(char1)),X1) ) ),
inference(flattening,[],[f171]) ).
tff(f173,plain,
? [X0: bool1,X1: regexp1,X2: regexp1] :
( ? [X3: bool1] :
( ( mem2(tb2t(nil(char1)),X1)
| ( true1 != X3 ) )
& ( ( X3 = true1 )
| ~ mem2(tb2t(nil(char1)),X1) )
& ( true1 != X3 )
& mem2(tb2t(nil(char1)),concat1(X2,X1)) )
& ( true1 = X0 )
& ( mem2(tb2t(nil(char1)),X2)
| ( true1 != X0 ) )
& ( ( true1 = X0 )
| ~ mem2(tb2t(nil(char1)),X2) ) ),
inference(rectify,[],[f172]) ).
tff(f174,plain,
( ( mem2(tb2t(nil(char1)),sK7)
| ( true1 != sK9 ) )
& ( ( true1 = sK9 )
| ~ mem2(tb2t(nil(char1)),sK7) )
& ( true1 != sK9 )
& mem2(tb2t(nil(char1)),concat1(sK8,sK7))
& ( true1 = sK6 )
& ( mem2(tb2t(nil(char1)),sK8)
| ( true1 != sK6 ) )
& ( ( true1 = sK6 )
| ~ mem2(tb2t(nil(char1)),sK8) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9)],[f173]) ).
tff(f175,plain,
! [X3: uni,X0: uni,X1: uni,X2: ty] :
( ( mem(X2,X1,infix_plpl(X2,X0,X3))
| ( ~ mem(X2,X1,X3)
& ~ mem(X2,X1,X0) ) )
& ( mem(X2,X1,X3)
| mem(X2,X1,X0)
| ~ mem(X2,X1,infix_plpl(X2,X0,X3)) ) ),
inference(nnf_transformation,[],[f127]) ).
tff(f176,plain,
! [X3: uni,X0: uni,X1: uni,X2: ty] :
( ( mem(X2,X1,infix_plpl(X2,X0,X3))
| ( ~ mem(X2,X1,X3)
& ~ mem(X2,X1,X0) ) )
& ( mem(X2,X1,X3)
| mem(X2,X1,X0)
| ~ mem(X2,X1,infix_plpl(X2,X0,X3)) ) ),
inference(flattening,[],[f175]) ).
tff(f177,plain,
! [X0: uni,X1: uni,X2: uni,X3: ty] :
( ( mem(X3,X2,infix_plpl(X3,X1,X0))
| ( ~ mem(X3,X2,X0)
& ~ mem(X3,X2,X1) ) )
& ( mem(X3,X2,X0)
| mem(X3,X2,X1)
| ~ mem(X3,X2,infix_plpl(X3,X1,X0)) ) ),
inference(rectify,[],[f176]) ).
tff(f186,plain,
! [X1: list_char,X0: regexp1] :
( ? [X12: list_char,X11: regexp1,X10: regexp1] :
( mem2(X12,X11)
& ( X1 = X12 )
& ( alt1(X11,X10) = X0 ) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f162]) ).
tff(f187,plain,
! [X0: list_char,X1: regexp1] :
( ? [X2: list_char,X3: regexp1,X4: regexp1] :
( mem2(X2,X3)
& ( X0 = X2 )
& ( alt1(X3,X4) = X1 ) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f186]) ).
tff(f188,plain,
! [X0: list_char,X1: regexp1] :
( ( mem2(sK10(X0,X1),sK11(X0,X1))
& ( sK10(X0,X1) = X0 )
& ( alt1(sK11(X0,X1),sK12(X0,X1)) = X1 ) )
| ~ sP3(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))],[f187]) ).
tff(f189,plain,
! [X0: regexp1,X1: list_char] :
( ? [X2: regexp1,X3: list_char,X4: regexp1] :
( ( alt1(X2,X4) = X0 )
& mem2(X3,X4)
& ( X1 = X3 ) )
| ~ sP2(X0,X1) ),
inference(nnf_transformation,[],[f161]) ).
tff(f190,plain,
! [X0: regexp1,X1: list_char] :
( ( ( alt1(sK13(X0,X1),sK15(X0,X1)) = X0 )
& mem2(sK14(X0,X1),sK15(X0,X1))
& ( sK14(X0,X1) = X1 ) )
| ~ sP2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X2,sK13(X0,X1)),skolemize(X3,sK14(X0,X1)),skolemize(X4,sK15(X0,X1))],[f189]) ).
tff(f191,plain,
! [X0: regexp1,X1: list_char] :
( ? [X15: list_char,X16: regexp1,X13: regexp1,X14: list_char] :
( mem2(X14,X16)
& ( concat1(X16,X13) = X0 )
& mem2(X15,X13)
& ( tb2t(infix_plpl(char1,t2tb(X14),t2tb(X15))) = X1 ) )
| ~ sP1(X0,X1) ),
inference(nnf_transformation,[],[f160]) ).
tff(f192,plain,
! [X0: regexp1,X1: list_char] :
( ? [X2: list_char,X3: regexp1,X4: regexp1,X5: list_char] :
( mem2(X5,X3)
& ( concat1(X3,X4) = X0 )
& mem2(X2,X4)
& ( tb2t(infix_plpl(char1,t2tb(X5),t2tb(X2))) = X1 ) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f191]) ).
tff(f193,plain,
! [X0: regexp1,X1: list_char] :
( ( mem2(sK19(X0,X1),sK17(X0,X1))
& ( concat1(sK17(X0,X1),sK18(X0,X1)) = X0 )
& mem2(sK16(X0,X1),sK18(X0,X1))
& ( tb2t(infix_plpl(char1,t2tb(sK19(X0,X1)),t2tb(sK16(X0,X1)))) = X1 ) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19]),skolemize(X2,sK16(X0,X1)),skolemize(X3,sK17(X0,X1)),skolemize(X4,sK18(X0,X1)),skolemize(X5,sK19(X0,X1))],[f192]) ).
tff(f194,plain,
! [X0: regexp1,X1: list_char] :
( ? [X8: list_char,X7: regexp1,X9: list_char] :
( mem2(X9,star1(X7))
& ( star1(X7) = X0 )
& mem2(X8,X7)
& ( tb2t(infix_plpl(char1,t2tb(X8),t2tb(X9))) = X1 ) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f159]) ).
tff(f195,plain,
! [X0: regexp1,X1: list_char] :
( ? [X2: list_char,X3: regexp1,X4: list_char] :
( mem2(X4,star1(X3))
& ( star1(X3) = X0 )
& mem2(X2,X3)
& ( tb2t(infix_plpl(char1,t2tb(X2),t2tb(X4))) = X1 ) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f194]) ).
tff(f196,plain,
! [X0: regexp1,X1: list_char] :
( ( mem2(sK22(X0,X1),star1(sK21(X0,X1)))
& ( star1(sK21(X0,X1)) = X0 )
& mem2(sK20(X0,X1),sK21(X0,X1))
& ( tb2t(infix_plpl(char1,t2tb(sK20(X0,X1)),t2tb(sK22(X0,X1)))) = X1 ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22]),skolemize(X2,sK20(X0,X1)),skolemize(X3,sK21(X0,X1)),skolemize(X4,sK22(X0,X1))],[f195]) ).
tff(f197,plain,
! [X0: list_char,X1: regexp1] :
( sP1(X1,X0)
| sP3(X0,X1)
| ? [X2: char2] :
( ( tb2t(cons(char1,t2tb1(X2),nil(char1))) = X0 )
& ( char3(X2) = X1 ) )
| sP2(X1,X0)
| sP0(X1,X0)
| ( ( tb2t(nil(char1)) = X0 )
& ( epsilon1 = X1 ) )
| ~ mem2(X0,X1)
| ? [X3: regexp1] :
( ( star1(X3) = X1 )
& ( tb2t(nil(char1)) = X0 ) ) ),
inference(rectify,[],[f163]) ).
tff(f198,plain,
! [X0: list_char,X1: regexp1] :
( sP1(X1,X0)
| sP3(X0,X1)
| ( ( tb2t(cons(char1,t2tb1(sK23(X0,X1)),nil(char1))) = X0 )
& ( char3(sK23(X0,X1)) = X1 ) )
| sP2(X1,X0)
| sP0(X1,X0)
| ( ( tb2t(nil(char1)) = X0 )
& ( epsilon1 = X1 ) )
| ~ mem2(X0,X1)
| ( ( star1(sK24(X0,X1)) = X1 )
& ( tb2t(nil(char1)) = X0 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24]),skolemize(X2,sK23(X0,X1)),skolemize(X3,sK24(X0,X1))],[f197]) ).
tff(f200,plain,
! [X0: regexp1,X1: char2,X2: regexp1] : ( concat1(X2,X0) != char3(X1) ),
inference(rectify,[],[f105]) ).
tff(f210,plain,
! [X0: uni,X1: ty] :
( ~ sort1(X1,X0)
| ( ~ mem(X1,X0,nil(X1))
& ! [X3: uni,X2: uni] :
( ( ( mem(X1,X0,cons(X1,X2,X3))
| ( ~ mem(X1,X0,X3)
& ( X0 != X2 ) ) )
& ( mem(X1,X0,X3)
| ( X0 = X2 )
| ~ mem(X1,X0,cons(X1,X2,X3)) ) )
| ~ sort1(X1,X2) ) ) ),
inference(nnf_transformation,[],[f154]) ).
tff(f211,plain,
! [X0: uni,X1: ty] :
( ~ sort1(X1,X0)
| ( ~ mem(X1,X0,nil(X1))
& ! [X3: uni,X2: uni] :
( ( ( mem(X1,X0,cons(X1,X2,X3))
| ( ~ mem(X1,X0,X3)
& ( X0 != X2 ) ) )
& ( mem(X1,X0,X3)
| ( X0 = X2 )
| ~ mem(X1,X0,cons(X1,X2,X3)) ) )
| ~ sort1(X1,X2) ) ) ),
inference(flattening,[],[f210]) ).
tff(f212,plain,
! [X0: uni,X1: ty] :
( ~ sort1(X1,X0)
| ( ~ mem(X1,X0,nil(X1))
& ! [X2: uni,X3: uni] :
( ( ( mem(X1,X0,cons(X1,X3,X2))
| ( ~ mem(X1,X0,X2)
& ( X0 != X3 ) ) )
& ( mem(X1,X0,X2)
| ( X0 = X3 )
| ~ mem(X1,X0,cons(X1,X3,X2)) ) )
| ~ sort1(X1,X3) ) ) ),
inference(rectify,[],[f211]) ).
tff(f213,plain,
! [X0: regexp1,X1: regexp1,X2: regexp1,X3: regexp1] : ( alt1(X1,X2) != concat1(X3,X0) ),
inference(rectify,[],[f103]) ).
tff(f219,plain,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != concat1(X1,X0) ),
inference(rectify,[],[f22]) ).
tff(f222,plain,
! [X0: regexp1,X1: regexp1] : ( concat_proj_21(concat1(X1,X0)) = X0 ),
inference(rectify,[],[f34]) ).
tff(f240,plain,
mem2(tb2t(nil(char1)),concat1(sK8,sK7)),
inference(cnf_transformation,[],[f174]) ).
tff(f241,plain,
true1 != sK9,
inference(cnf_transformation,[],[f174]) ).
tff(f242,plain,
( ( true1 = sK9 )
| ~ mem2(tb2t(nil(char1)),sK7) ),
inference(cnf_transformation,[],[f174]) ).
tff(f248,plain,
! [X2: uni,X3: ty,X0: uni,X1: uni] :
( mem(X3,X2,infix_plpl(X3,X1,X0))
| ~ mem(X3,X2,X0) ),
inference(cnf_transformation,[],[f177]) ).
tff(f261,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f62]) ).
tff(f264,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP3(X0,X1)
| ( alt1(sK11(X0,X1),sK12(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f188]) ).
tff(f269,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP2(X0,X1)
| ( alt1(sK13(X0,X1),sK15(X0,X1)) = X0 ) ),
inference(cnf_transformation,[],[f190]) ).
tff(f270,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP1(X0,X1)
| ( tb2t(infix_plpl(char1,t2tb(sK19(X0,X1)),t2tb(sK16(X0,X1)))) = X1 ) ),
inference(cnf_transformation,[],[f193]) ).
tff(f271,plain,
! [X0: regexp1,X1: list_char] :
( mem2(sK16(X0,X1),sK18(X0,X1))
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
tff(f272,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP1(X0,X1)
| ( concat1(sK17(X0,X1),sK18(X0,X1)) = X0 ) ),
inference(cnf_transformation,[],[f193]) ).
tff(f276,plain,
! [X0: regexp1,X1: list_char] :
( ~ sP0(X0,X1)
| ( star1(sK21(X0,X1)) = X0 ) ),
inference(cnf_transformation,[],[f196]) ).
tff(f279,plain,
! [X0: list_char,X1: regexp1] :
( ~ mem2(X0,X1)
| sP3(X0,X1)
| sP1(X1,X0)
| sP0(X1,X0)
| ( epsilon1 = X1 )
| ( char3(sK23(X0,X1)) = X1 )
| sP2(X1,X0)
| ( star1(sK24(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f198]) ).
tff(f289,plain,
! [X0: list_char] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f61]) ).
tff(f290,plain,
! [X2: regexp1,X0: regexp1,X1: char2] : ( concat1(X2,X0) != char3(X1) ),
inference(cnf_transformation,[],[f200]) ).
tff(f296,plain,
! [X2: regexp1,X0: regexp1,X1: regexp1] : ( star1(X0) != concat1(X2,X1) ),
inference(cnf_transformation,[],[f128]) ).
tff(f302,plain,
! [X0: ty,X1: uni] : sort1(X0,cons_proj_1(X0,X1)),
inference(cnf_transformation,[],[f43]) ).
tff(f304,plain,
! [X0: ty,X1: uni] :
( ( cons(X0,cons_proj_1(X0,X1),cons_proj_2(X0,X1)) = X1 )
| ( nil(X0) = X1 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f313,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] :
( ~ sort1(X1,X0)
| mem(X1,X0,cons(X1,X3,X2))
| ( X0 != X3 )
| ~ sort1(X1,X3) ),
inference(cnf_transformation,[],[f212]) ).
tff(f315,plain,
! [X0: uni,X1: ty] :
( ~ mem(X1,X0,nil(X1))
| ~ sort1(X1,X0) ),
inference(cnf_transformation,[],[f212]) ).
tff(f316,plain,
! [X2: regexp1,X3: regexp1,X0: regexp1,X1: regexp1] : ( alt1(X1,X2) != concat1(X3,X0) ),
inference(cnf_transformation,[],[f213]) ).
tff(f323,plain,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != concat1(X1,X0) ),
inference(cnf_transformation,[],[f219]) ).
tff(f329,plain,
! [X0: regexp1,X1: regexp1] : ( concat_proj_21(concat1(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f222]) ).
tff(f337,plain,
! [X2: uni,X3: uni,X1: ty] :
( ~ sort1(X1,X3)
| mem(X1,X3,cons(X1,X3,X2))
| ~ sort1(X1,X3) ),
inference(equality_resolution,[],[f313]) ).
tff(f338,definition,
sF25 = nil(char1),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f339,plain,
nil(char1) = sF25,
inference(reorient_equations,[],[f338]) ).
tff(f340,definition,
sF26 = tb2t(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f341,plain,
tb2t(sF25) = sF26,
inference(reorient_equations,[],[f340]) ).
tff(f343,plain,
( ( true1 = sK9 )
| ~ mem2(sF26,sK7) ),
inference(definition_folding,[],[f242,f341,f339]) ).
tff(f344,definition,
sF27 = concat1(sK8,sK7),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f345,plain,
concat1(sK8,sK7) = sF27,
inference(reorient_equations,[],[f344]) ).
tff(f346,plain,
mem2(sF26,sF27),
inference(definition_folding,[],[f240,f345,f341,f339]) ).
tff(f349,plain,
! [X2: uni,X3: uni,X1: ty] :
( mem(X1,X3,cons(X1,X3,X2))
| ~ sort1(X1,X3) ),
inference(duplicate_literal_removal,[],[f337]) ).
tff(f352,plain,
~ mem2(sF26,sK7),
inference(forward_subsumption_resolution,[],[f343,f241]) ).
tff(f358,plain,
sF25 = t2tb(sF26),
inference(superposition,[],[f261,f341]) ).
tff(f364,plain,
epsilon1 != sF27,
inference(superposition,[],[f323,f345]) ).
tff(f367,plain,
! [X0: char2] : ( char3(X0) != sF27 ),
inference(superposition,[],[f290,f345]) ).
tff(f370,plain,
! [X0: regexp1] : ( star1(X0) != sF27 ),
inference(superposition,[],[f296,f345]) ).
tff(f379,plain,
sK7 = concat_proj_21(sF27),
inference(superposition,[],[f329,f345]) ).
tff(f384,plain,
! [X0: regexp1,X1: regexp1] : ( alt1(X0,X1) != sF27 ),
inference(superposition,[],[f316,f345]) ).
tff(f391,plain,
! [X0: uni] :
( ~ mem(char1,X0,sF25)
| ~ sort1(char1,X0) ),
inference(superposition,[],[f315,f339]) ).
tff(f616,plain,
! [X0: uni,X1: ty] :
( ~ sort1(X1,cons_proj_1(X1,X0))
| ( nil(X1) = X0 )
| mem(X1,cons_proj_1(X1,X0),X0) ),
inference(superposition,[],[f349,f304]) ).
tff(f619,plain,
! [X0: uni,X1: ty] :
( mem(X1,cons_proj_1(X1,X0),X0)
| ( nil(X1) = X0 ) ),
inference(forward_subsumption_resolution,[],[f616,f302]) ).
tff(f876,plain,
( ( star1(sK24(sF26,sF27)) = sF27 )
| sP0(sF27,sF26)
| sP3(sF26,sF27)
| ( epsilon1 = sF27 )
| sP2(sF27,sF26)
| sP1(sF27,sF26)
| ( char3(sK23(sF26,sF27)) = sF27 ) ),
inference(resolution,[],[f279,f346]) ).
tff(f879,plain,
( sP2(sF27,sF26)
| ( epsilon1 = sF27 )
| sP3(sF26,sF27)
| sP0(sF27,sF26)
| ( char3(sK23(sF26,sF27)) = sF27 )
| sP1(sF27,sF26) ),
inference(forward_subsumption_resolution,[],[f876,f370]) ).
tff(f888,plain,
( sP3(sF26,sF27)
| sP0(sF27,sF26)
| ( char3(sK23(sF26,sF27)) = sF27 )
| sP1(sF27,sF26)
| sP2(sF27,sF26) ),
inference(forward_subsumption_resolution,[],[f879,f364]) ).
tff(f896,plain,
( sP0(sF27,sF26)
| sP2(sF27,sF26)
| sP1(sF27,sF26)
| sP3(sF26,sF27) ),
inference(forward_subsumption_resolution,[],[f888,f367]) ).
tff(f900,definition,
( spl28_1
<=> sP1(sF27,sF26) ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
tff(f902,plain,
( sP1(sF27,sF26)
| ~ spl28_1 ),
inference(avatar_component_clause,[],[f900]) ).
tff(f904,definition,
( spl28_2
<=> sP0(sF27,sF26) ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
tff(f906,plain,
( sP0(sF27,sF26)
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f904]) ).
tff(f908,definition,
( spl28_3
<=> sP2(sF27,sF26) ),
introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition]) ).
tff(f910,plain,
( sP2(sF27,sF26)
| ~ spl28_3 ),
inference(avatar_component_clause,[],[f908]) ).
tff(f912,definition,
( spl28_4
<=> sP3(sF26,sF27) ),
introduced(definition,[new_symbols(definition,[spl28_4])],[avatar_definition]) ).
tff(f914,plain,
( sP3(sF26,sF27)
| ~ spl28_4 ),
inference(avatar_component_clause,[],[f912]) ).
tff(f915,plain,
( spl28_1
| spl28_2
| spl28_3
| spl28_4 ),
inference(avatar_split_clause,[],[f896,f912,f908,f904,f900]) ).
tff(f949,plain,
( ( star1(sK21(sF27,sF26)) = sF27 )
| ~ spl28_2 ),
inference(resolution,[],[f906,f276]) ).
tff(f950,plain,
( $false
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f949,f370]) ).
tff(f951,plain,
~ spl28_2,
inference(avatar_contradiction_clause,[],[f950]) ).
tff(f971,plain,
( ( alt1(sK13(sF27,sF26),sK15(sF27,sF26)) = sF27 )
| ~ spl28_3 ),
inference(resolution,[],[f910,f269]) ).
tff(f973,plain,
( $false
| ~ spl28_3 ),
inference(forward_subsumption_resolution,[],[f971,f384]) ).
tff(f974,plain,
~ spl28_3,
inference(avatar_contradiction_clause,[],[f973]) ).
tff(f980,plain,
( ( alt1(sK11(sF26,sF27),sK12(sF26,sF27)) = sF27 )
| ~ spl28_4 ),
inference(resolution,[],[f914,f264]) ).
tff(f982,plain,
( $false
| ~ spl28_4 ),
inference(forward_subsumption_resolution,[],[f980,f384]) ).
tff(f983,plain,
~ spl28_4,
inference(avatar_contradiction_clause,[],[f982]) ).
tff(f985,plain,
( ( sF26 = tb2t(infix_plpl(char1,t2tb(sK19(sF27,sF26)),t2tb(sK16(sF27,sF26)))) )
| ~ spl28_1 ),
inference(resolution,[],[f902,f270]) ).
tff(f986,plain,
( ( concat1(sK17(sF27,sF26),sK18(sF27,sF26)) = sF27 )
| ~ spl28_1 ),
inference(resolution,[],[f902,f272]) ).
tff(f1025,plain,
( ( concat_proj_21(sF27) = sK18(sF27,sF26) )
| ~ spl28_1 ),
inference(superposition,[],[f329,f986]) ).
tff(f1027,plain,
( ( sK7 = sK18(sF27,sF26) )
| ~ spl28_1 ),
inference(forward_demodulation,[],[f1025,f379]) ).
tff(f1214,plain,
( ( t2tb(sF26) = infix_plpl(char1,t2tb(sK19(sF27,sF26)),t2tb(sK16(sF27,sF26))) )
| ~ spl28_1 ),
inference(superposition,[],[f261,f985]) ).
tff(f1215,plain,
( ( sF25 = infix_plpl(char1,t2tb(sK19(sF27,sF26)),t2tb(sK16(sF27,sF26))) )
| ~ spl28_1 ),
inference(forward_demodulation,[],[f1214,f358]) ).
tff(f1222,plain,
( ! [X0: uni] :
( ~ mem(char1,X0,t2tb(sK16(sF27,sF26)))
| mem(char1,X0,sF25) )
| ~ spl28_1 ),
inference(superposition,[],[f248,f1215]) ).
tff(f1228,plain,
( mem(char1,cons_proj_1(char1,t2tb(sK16(sF27,sF26))),sF25)
| ( nil(char1) = t2tb(sK16(sF27,sF26)) )
| ~ spl28_1 ),
inference(resolution,[],[f1222,f619]) ).
tff(f1229,plain,
( ( t2tb(sK16(sF27,sF26)) = sF25 )
| mem(char1,cons_proj_1(char1,t2tb(sK16(sF27,sF26))),sF25)
| ~ spl28_1 ),
inference(forward_demodulation,[],[f1228,f339]) ).
tff(f1479,definition,
( spl28_15
<=> mem(char1,cons_proj_1(char1,t2tb(sK16(sF27,sF26))),sF25) ),
introduced(definition,[new_symbols(definition,[spl28_15])],[avatar_definition]) ).
tff(f1481,plain,
( mem(char1,cons_proj_1(char1,t2tb(sK16(sF27,sF26))),sF25)
| ~ spl28_15 ),
inference(avatar_component_clause,[],[f1479]) ).
tff(f1483,definition,
( spl28_16
<=> ( t2tb(sK16(sF27,sF26)) = sF25 ) ),
introduced(definition,[new_symbols(definition,[spl28_16])],[avatar_definition]) ).
tff(f1485,plain,
( ( t2tb(sK16(sF27,sF26)) = sF25 )
| ~ spl28_16 ),
inference(avatar_component_clause,[],[f1483]) ).
tff(f1486,plain,
( spl28_15
| spl28_16
| ~ spl28_1 ),
inference(avatar_split_clause,[],[f1229,f900,f1483,f1479]) ).
tff(f1494,plain,
( ~ sort1(char1,cons_proj_1(char1,t2tb(sK16(sF27,sF26))))
| ~ spl28_15 ),
inference(resolution,[],[f1481,f391]) ).
tff(f1496,plain,
( $false
| ~ spl28_15 ),
inference(forward_subsumption_resolution,[],[f1494,f302]) ).
tff(f1497,plain,
~ spl28_15,
inference(avatar_contradiction_clause,[],[f1496]) ).
tff(f1513,plain,
( ( tb2t(sF25) = sK16(sF27,sF26) )
| ~ spl28_16 ),
inference(superposition,[],[f289,f1485]) ).
tff(f1520,plain,
( ( sF26 = sK16(sF27,sF26) )
| ~ spl28_16 ),
inference(forward_demodulation,[],[f1513,f341]) ).
tff(f1546,plain,
( mem2(sF26,sK18(sF27,sF26))
| ~ sP1(sF27,sF26)
| ~ spl28_16 ),
inference(superposition,[],[f271,f1520]) ).
tff(f1557,plain,
( mem2(sF26,sK18(sF27,sF26))
| ~ spl28_1
| ~ spl28_16 ),
inference(forward_subsumption_resolution,[],[f1546,f902]) ).
tff(f1562,plain,
( mem2(sF26,sK7)
| ~ spl28_1
| ~ spl28_16 ),
inference(forward_demodulation,[],[f1557,f1027]) ).
tff(f1564,plain,
( $false
| ~ spl28_1
| ~ spl28_16 ),
inference(forward_subsumption_resolution,[],[f1562,f352]) ).
tff(f1565,plain,
( ~ spl28_1
| ~ spl28_16 ),
inference(avatar_contradiction_clause,[],[f1564]) ).
cnf(s1,plain,
( spl28_1
| spl28_2
| spl28_3
| spl28_4 ),
inference(sat_conversion,[],[f915]) ).
cnf(s2,plain,
~ spl28_2,
inference(sat_conversion,[],[f951]) ).
cnf(s3,plain,
~ spl28_3,
inference(sat_conversion,[],[f974]) ).
cnf(s4,plain,
~ spl28_4,
inference(sat_conversion,[],[f983]) ).
cnf(s9,plain,
( ~ spl28_1
| spl28_15
| spl28_16 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s10,plain,
~ spl28_15,
inference(sat_conversion,[],[f1497]) ).
cnf(s13,plain,
( ~ spl28_1
| ~ spl28_16 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s14,plain,
( ~ spl28_1
| spl28_16 ),
inference(rat,[],[s9,s10]) ).
cnf(s15,plain,
spl28_1,
inference(rat,[],[s1,s4,s3,s2]) ).
cnf(s16,plain,
~ spl28_16,
inference(rat,[],[s13,s15]) ).
cnf(s17,plain,
$false,
inference(rat,[],[s14,s16,s15]) ).
tff(f1566,plain,
$false,
inference(avatar_sat_refutation,[],[s17]) ).
%------------------------------------------------------------------------------
%----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 THM
% 0.10/0.23 % Computer : n018.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Mon Sep 28 14:25:24 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.29 Running first-order theorem proving
% 0.26/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.56/1.73 % (3421162)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.56/1.73 % (3421171)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4262231304:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.56/1.73 % (3421173)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2291295709:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.56/1.73 % (3421171)Instruction limit reached!
% 5.56/1.73 % (3421171)------------------------------
% 5.56/1.73 % (3421171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.73 % (3421171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.73 % (3421171)CaDiCaL version: 2.1.3
% 5.56/1.73 % (3421171)Termination reason: Instruction limit
% 5.56/1.73 % (3421171)Termination phase: Property scanning
% 5.56/1.73 % (3421171)Time elapsed: 0.003 s
% 5.56/1.73 % (3421171)Peak memory usage: 86 MB
% 5.56/1.73 % (3421171)Instructions burned: 5 (million)
% 5.56/1.73 % (3421173)Instruction limit reached!
% 5.56/1.73 % (3421173)------------------------------
% 5.56/1.73 % (3421173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.73 % (3421173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.73 % (3421173)CaDiCaL version: 2.1.3
% 5.56/1.73 % (3421173)Termination reason: Instruction limit
% 5.56/1.73 % (3421173)Termination phase: Saturation
% 5.56/1.73 % (3421173)Time elapsed: 0.037 s
% 5.56/1.73 % (3421173)Peak memory usage: 115 MB
% 5.56/1.73 % (3421173)Instructions burned: 34 (million)
% 5.56/1.73 % (3421168)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4066448:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.56/1.73 % (3421167)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2202664134:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.56/1.73 % (3421170)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=521859647:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.56/1.73 % (3421169)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1161849984:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.56/1.73 % (3421172)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2458364759:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.56/1.73 % (3421170)Instruction limit reached!
% 5.56/1.73 % (3421170)------------------------------
% 5.56/1.73 % (3421170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.73 % (3421170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.73 % (3421170)CaDiCaL version: 2.1.3
% 5.56/1.73 % (3421170)Termination reason: Instruction limit
% 5.56/1.73 % (3421170)Termination phase: Saturation
% 5.56/1.73 % (3421170)Time elapsed: 0.008 s
% 5.56/1.73 % (3421170)Peak memory usage: 88 MB
% 5.56/1.73 % (3421170)Instructions burned: 7 (million)
% 5.56/1.73 % (3421167)Refutation not found, incomplete strategy
% 5.56/1.73 % (3421167)------------------------------
% 5.56/1.73 % (3421167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.73 % (3421167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.73 % (3421167)CaDiCaL version: 2.1.3
% 5.56/1.73 % (3421167)Termination reason: Refutation not found, incomplete strategy
% 5.56/1.73 % (3421167)Time elapsed: 0.044 s
% 5.56/1.73 % (3421167)Peak memory usage: 116 MB
% 5.56/1.73 % (3421167)Instructions burned: 10 (million)
% 5.56/1.73 % (3421172)Instruction limit reached!
% 5.56/1.73 % (3421172)------------------------------
% 5.56/1.73 % (3421172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.73 % (3421172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.73 % (3421172)CaDiCaL version: 2.1.3
% 5.56/1.73 % (3421172)Termination reason: Instruction limit
% 5.56/1.73 % (3421172)Termination phase: Saturation
% 5.56/1.73 % (3421172)Time elapsed: 0.069 s
% 5.56/1.73 % (3421172)Peak memory usage: 115 MB
% 5.56/1.73 % (3421172)Instructions burned: 47 (million)
% 5.56/1.73 % (3421176)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=322374440:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.56/1.73 % (3421176)Instruction limit reached!
% 5.56/1.73 % (3421176)------------------------------
% 6.75/1.97 % (3421176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.97 % (3421176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.97 % (3421176)CaDiCaL version: 2.1.3
% 6.75/1.97 % (3421176)Termination reason: Instruction limit
% 6.75/1.97 % (3421176)Termination phase: Saturation
% 6.75/1.97 % (3421176)Time elapsed: 0.015 s
% 6.75/1.97 % (3421176)Peak memory usage: 89 MB
% 6.75/1.97 % (3421176)Instructions burned: 15 (million)
% 6.75/1.97 % (3421177)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=280248384:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.75/1.97 % (3421177)Instruction limit reached!
% 6.75/1.97 % (3421177)------------------------------
% 6.75/1.97 % (3421177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.97 % (3421177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.97 % (3421177)CaDiCaL version: 2.1.3
% 6.75/1.97 % (3421177)Termination reason: Instruction limit
% 6.75/1.97 % (3421177)Termination phase: Property scanning
% 6.75/1.97 % (3421177)Time elapsed: 0.013 s
% 6.75/1.97 % (3421177)Peak memory usage: 86 MB
% 6.75/1.97 % (3421177)Instructions burned: 30 (million)
% 6.75/1.97 % (3421169)Instruction limit reached!
% 6.75/1.97 % (3421169)------------------------------
% 6.75/1.97 % (3421169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.97 % (3421169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.97 % (3421169)CaDiCaL version: 2.1.3
% 6.75/1.97 % (3421169)Termination reason: Instruction limit
% 6.75/1.97 % (3421169)Termination phase: Saturation
% 6.75/1.97 % (3421169)Time elapsed: 0.221 s
% 6.75/1.97 % (3421169)Peak memory usage: 117 MB
% 6.75/1.97 % (3421169)Instructions burned: 201 (million)
% 6.75/1.97 % (3421168)Instruction limit reached!
% 6.75/1.97 % (3421168)------------------------------
% 6.75/1.97 % (3421168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.97 % (3421168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.97 % (3421168)CaDiCaL version: 2.1.3
% 6.75/1.97 % (3421168)Termination reason: Instruction limit
% 6.75/1.97 % (3421168)Termination phase: Saturation
% 6.75/1.97 % (3421168)Time elapsed: 0.278 s
% 6.75/1.97 % (3421168)Peak memory usage: 116 MB
% 6.75/1.97 % (3421168)Instructions burned: 307 (million)
% 6.75/1.97 % (3421183)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1729969601:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.75/1.97 % (3421183)Instruction limit reached!
% 6.75/1.97 % (3421183)------------------------------
% 6.75/1.97 % (3421183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.97 % (3421183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.97 % (3421183)CaDiCaL version: 2.1.3
% 6.75/1.97 % (3421183)Termination reason: Instruction limit
% 6.75/1.97 % (3421183)Termination phase: Saturation
% 6.75/1.97 % (3421183)Time elapsed: 0.017 s
% 6.75/1.97 % (3421183)Peak memory usage: 89 MB
% 6.75/1.97 % (3421183)Instructions burned: 16 (million)
% 6.75/1.97 % (3421184)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3923363909:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.75/1.97 % (3421186)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=2409969755:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.75/1.97 % (3421184)Instruction limit reached!
% 6.75/1.97 % (3421184)------------------------------
% 6.75/1.97 % (3421184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.97 % (3421184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.97 % (3421184)CaDiCaL version: 2.1.3
% 6.75/1.97 % (3421184)Termination reason: Instruction limit
% 6.75/1.97 % (3421184)Termination phase: Saturation
% 6.75/1.97 % (3421184)Time elapsed: 0.025 s
% 6.75/1.97 % (3421184)Peak memory usage: 89 MB
% 6.75/1.97 % (3421184)Instructions burned: 24 (million)
% 6.75/1.97 % (3421188)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1640553028:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 6.75/1.97 % (3421186)Instruction limit reached!
% 6.75/1.97 % (3421186)------------------------------
% 6.75/1.97 % (3421186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.27 % (3421186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.27 % (3421186)CaDiCaL version: 2.1.3
% 9.58/2.27 % (3421186)Termination reason: Instruction limit
% 9.58/2.27 % (3421186)Termination phase: Saturation
% 9.58/2.27 % (3421186)Time elapsed: 0.026 s
% 9.58/2.27 % (3421186)Peak memory usage: 89 MB
% 9.58/2.27 % (3421186)Instructions burned: 27 (million)
% 9.58/2.27 % (3421188)Instruction limit reached!
% 9.58/2.27 % (3421188)------------------------------
% 9.58/2.27 % (3421188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.27 % (3421188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.27 % (3421188)CaDiCaL version: 2.1.3
% 9.58/2.27 % (3421188)Termination reason: Instruction limit
% 9.58/2.27 % (3421188)Termination phase: Saturation
% 9.58/2.27 % (3421188)Time elapsed: 0.041 s
% 9.58/2.27 % (3421188)Peak memory usage: 89 MB
% 9.58/2.27 % (3421188)Instructions burned: 86 (million)
% 9.58/2.27 % (3421167)------------------------------
% 9.58/2.27 % (3421167)------------------------------
% 9.58/2.27 % (3421192)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=383900837:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.58/2.27 % (3421192)Instruction limit reached!
% 9.58/2.27 % (3421192)------------------------------
% 9.58/2.27 % (3421192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.27 % (3421192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.27 % (3421192)CaDiCaL version: 2.1.3
% 9.58/2.27 % (3421192)Termination reason: Instruction limit
% 9.58/2.27 % (3421192)Termination phase: Function definition elimination
% 9.58/2.27 % (3421192)Time elapsed: 0.003 s
% 9.58/2.27 % (3421192)Peak memory usage: 86 MB
% 9.58/2.27 % (3421192)Instructions burned: 4 (million)
% 9.58/2.27 % (3421189)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1053252639:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.58/2.27 % (3421189)Instruction limit reached!
% 9.58/2.27 % (3421189)------------------------------
% 9.58/2.27 % (3421189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.27 % (3421189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.27 % (3421189)CaDiCaL version: 2.1.3
% 9.58/2.27 % (3421189)Termination reason: Instruction limit
% 9.58/2.27 % (3421189)Termination phase: Naming
% 9.58/2.27 % (3421189)Time elapsed: 0.003 s
% 9.58/2.27 % (3421189)Peak memory usage: 86 MB
% 9.58/2.27 % (3421189)Instructions burned: 2 (million)
% 9.58/2.27 % (3421191)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3377505798:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.58/2.27 % (3421191)Refutation not found, incomplete strategy
% 9.58/2.27 % (3421191)------------------------------
% 9.58/2.27 % (3421191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.27 % (3421191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.27 % (3421191)CaDiCaL version: 2.1.3
% 9.58/2.27 % (3421191)Termination reason: Refutation not found, incomplete strategy
% 9.58/2.27 % (3421191)Time elapsed: 0.005 s
% 9.58/2.27 % (3421191)Peak memory usage: 89 MB
% 9.58/2.27 % (3421191)Instructions burned: 3 (million)
% 9.58/2.27 % (3421195)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4188442911:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi)
% 9.58/2.27 % (3421198)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2528577727:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.58/2.27 % (3421198)Instruction limit reached!
% 9.58/2.27 % (3421198)------------------------------
% 9.58/2.27 % (3421198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.27 % (3421198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.27 % (3421198)CaDiCaL version: 2.1.3
% 9.58/2.27 % (3421198)Termination reason: Instruction limit
% 9.58/2.27 % (3421198)Termination phase: Saturation
% 9.58/2.27 % (3421198)Time elapsed: 0.005 s
% 9.58/2.27 % (3421198)Peak memory usage: 88 MB
% 9.58/2.27 % (3421198)Instructions burned: 9 (million)
% 9.58/2.27 % (3421197)lrs+10_1_thi=all:si=on:fd=off:random_seed=44893458:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 11.09/2.59 % (3421199)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=881855559:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 11.09/2.59 % (3421195)Instruction limit reached!
% 11.09/2.59 % (3421195)------------------------------
% 11.09/2.59 % (3421195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.09/2.59 % (3421195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.09/2.59 % (3421195)CaDiCaL version: 2.1.3
% 11.09/2.59 % (3421195)Termination reason: Instruction limit
% 11.09/2.59 % (3421195)Termination phase: Saturation
% 11.09/2.59 % (3421195)Time elapsed: 0.111 s
% 11.09/2.59 % (3421195)Peak memory usage: 133 MB
% 11.09/2.59 % (3421195)Instructions burned: 67 (million)
% 11.09/2.59 % (3421199)Instruction limit reached!
% 11.09/2.59 % (3421199)------------------------------
% 11.09/2.59 % (3421199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.09/2.59 % (3421199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.09/2.59 % (3421199)CaDiCaL version: 2.1.3
% 11.09/2.59 % (3421199)Termination reason: Instruction limit
% 11.09/2.59 % (3421199)Termination phase: Naming
% 11.09/2.59 % (3421199)Time elapsed: 0.002 s
% 11.09/2.59 % (3421199)Peak memory usage: 86 MB
% 11.09/2.59 % (3421199)Instructions burned: 2 (million)
% 11.09/2.59 % (3421201)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2217408243:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.09/2.59 % (3421197)Instruction limit reached!
% 11.09/2.59 % (3421197)------------------------------
% 11.09/2.59 % (3421197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.09/2.59 % (3421197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.09/2.59 % (3421197)CaDiCaL version: 2.1.3
% 11.09/2.59 % (3421197)Termination reason: Instruction limit
% 11.09/2.59 % (3421197)Termination phase: Saturation
% 11.09/2.59 % (3421197)Time elapsed: 0.075 s
% 11.09/2.59 % (3421197)Peak memory usage: 115 MB
% 11.09/2.59 % (3421197)Instructions burned: 53 (million)
% 11.09/2.59 % (3421201)Instruction limit reached!
% 11.09/2.59 % (3421201)------------------------------
% 11.09/2.59 % (3421201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.09/2.59 % (3421201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.09/2.59 % (3421201)CaDiCaL version: 2.1.3
% 11.09/2.59 % (3421201)Termination reason: Instruction limit
% 11.09/2.59 % (3421201)Termination phase: Preprocessing 3
% 11.09/2.59 % (3421201)Time elapsed: 0.003 s
% 11.09/2.59 % (3421201)Peak memory usage: 86 MB
% 11.09/2.59 % (3421201)Instructions burned: 2 (million)
% 11.09/2.59 % (3421203)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3459461277:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.09/2.59 % (3421207)dis+10_1_si=on:random_seed=1797684584:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.09/2.59 % (3421207)Instruction limit reached!
% 11.09/2.59 % (3421207)------------------------------
% 11.09/2.59 % (3421207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.09/2.59 % (3421207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.09/2.59 % (3421207)CaDiCaL version: 2.1.3
% 11.09/2.59 % (3421207)Termination reason: Instruction limit
% 11.09/2.59 % (3421207)Termination phase: Saturation
% 11.09/2.59 % (3421207)Time elapsed: 0.011 s
% 11.09/2.59 % (3421207)Peak memory usage: 88 MB
% 11.09/2.59 % (3421207)Instructions burned: 10 (million)
% 11.09/2.59 % (3421211)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4021282457:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi)
% 11.09/2.59 % (3421213)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3261051135:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 11.09/2.59 % (3421213)Instruction limit reached!
% 11.09/2.59 % (3421213)------------------------------
% 11.09/2.59 % (3421213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.09/2.59 % (3421213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.09/2.59 % (3421213)CaDiCaL version: 2.1.3
% 11.09/2.59 % (3421213)Termination reason: Instruction limit
% 11.09/2.59 % (3421213)Termination phase: Preprocessing 3
% 11.09/2.59 % (3421213)Time elapsed: 0.002 s
% 13.30/2.97 % (3421213)Peak memory usage: 86 MB
% 13.30/2.97 % (3421213)Instructions burned: 2 (million)
% 13.30/2.97 % (3421211)Instruction limit reached!
% 13.30/2.97 % (3421211)------------------------------
% 13.30/2.97 % (3421211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.30/2.97 % (3421211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.30/2.97 % (3421211)CaDiCaL version: 2.1.3
% 13.30/2.97 % (3421211)Termination reason: Instruction limit
% 13.30/2.97 % (3421211)Termination phase: Saturation
% 13.30/2.97 % (3421211)Time elapsed: 0.020 s
% 13.30/2.97 % (3421211)Peak memory usage: 89 MB
% 13.30/2.97 % (3421211)Instructions burned: 35 (million)
% 13.30/2.97 % (3421210)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1315072227:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi)
% 13.30/2.97 % (3421191)------------------------------
% 13.30/2.97 % (3421191)------------------------------
% 13.30/2.97 % (3421203)Instruction limit reached!
% 13.30/2.97 % (3421203)------------------------------
% 13.30/2.97 % (3421203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.30/2.97 % (3421203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.30/2.97 % (3421203)CaDiCaL version: 2.1.3
% 13.30/2.97 % (3421203)Termination reason: Instruction limit
% 13.30/2.97 % (3421203)Termination phase: Saturation
% 13.30/2.97 % (3421203)Time elapsed: 0.163 s
% 13.30/2.97 % (3421203)Peak memory usage: 117 MB
% 13.30/2.97 % (3421203)Instructions burned: 127 (million)
% 13.30/2.97 % (3421210)Instruction limit reached!
% 13.30/2.97 % (3421210)------------------------------
% 13.30/2.97 % (3421210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.30/2.97 % (3421210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.30/2.97 % (3421210)CaDiCaL version: 2.1.3
% 13.30/2.97 % (3421210)Termination reason: Instruction limit
% 13.30/2.97 % (3421210)Termination phase: Saturation
% 13.30/2.97 % (3421210)Time elapsed: 0.024 s
% 13.30/2.97 % (3421210)Peak memory usage: 88 MB
% 13.30/2.97 % (3421210)Instructions burned: 26 (million)
% 13.30/2.97 % (3421214)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1807804589:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 13.30/2.97 % (3421214)Instruction limit reached!
% 13.30/2.97 % (3421214)------------------------------
% 13.30/2.97 % (3421214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.30/2.97 % (3421214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.30/2.97 % (3421214)CaDiCaL version: 2.1.3
% 13.30/2.97 % (3421214)Termination reason: Instruction limit
% 13.30/2.97 % (3421214)Termination phase: Saturation
% 13.30/2.97 % (3421214)Time elapsed: 0.011 s
% 13.30/2.97 % (3421214)Peak memory usage: 89 MB
% 13.30/2.97 % (3421214)Instructions burned: 9 (million)
% 13.30/2.97 % (3421221)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=140339131:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 13.30/2.97 % (3421217)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3566766618:i=370:ep=RS:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/370Mi)
% 13.30/2.97 % (3421220)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2564979834:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi)
% 13.30/2.97 % (3421220)Instruction limit reached!
% 13.30/2.97 % (3421220)------------------------------
% 13.30/2.97 % (3421220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.30/2.97 % (3421220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.30/2.97 % (3421220)CaDiCaL version: 2.1.3
% 13.30/2.97 % (3421220)Termination reason: Instruction limit
% 13.30/2.97 % (3421220)Termination phase: Saturation
% 13.30/2.97 % (3421220)Time elapsed: 0.041 s
% 13.30/2.97 % (3421220)Peak memory usage: 112 MB
% 13.30/2.97 % (3421220)Instructions burned: 13 (million)
% 13.30/2.97 % (3421223)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2098151269:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 13.30/2.97 % (3421225)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=1124888962:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 13.30/2.97 % (3421224)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2492212664:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 17.46/3.35 % (3421223)Instruction limit reached!
% 17.46/3.35 % (3421223)------------------------------
% 17.46/3.35 % (3421223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.46/3.35 % (3421223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/3.35 % (3421223)CaDiCaL version: 2.1.3
% 17.46/3.35 % (3421223)Termination reason: Instruction limit
% 17.46/3.35 % (3421223)Termination phase: Saturation
% 17.46/3.35 % (3421223)Time elapsed: 0.011 s
% 17.46/3.35 % (3421223)Peak memory usage: 88 MB
% 17.46/3.35 % (3421223)Instructions burned: 10 (million)
% 17.46/3.35 % (3421221)Instruction limit reached!
% 17.46/3.35 % (3421221)------------------------------
% 17.46/3.35 % (3421221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.46/3.35 % (3421221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/3.35 % (3421221)CaDiCaL version: 2.1.3
% 17.46/3.35 % (3421221)Termination reason: Instruction limit
% 17.46/3.35 % (3421221)Termination phase: Saturation
% 17.46/3.35 % (3421221)Time elapsed: 0.147 s
% 17.46/3.35 % (3421221)Peak memory usage: 117 MB
% 17.46/3.35 % (3421221)Instructions burned: 228 (million)
% 17.46/3.35 % (3421225)Instruction limit reached!
% 17.46/3.35 % (3421225)------------------------------
% 17.46/3.35 % (3421225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.46/3.35 % (3421225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/3.35 % (3421225)CaDiCaL version: 2.1.3
% 17.46/3.35 % (3421225)Termination reason: Instruction limit
% 17.46/3.35 % (3421225)Termination phase: Saturation
% 17.46/3.35 % (3421225)Time elapsed: 0.058 s
% 17.46/3.35 % (3421225)Peak memory usage: 89 MB
% 17.46/3.35 % (3421225)Instructions burned: 76 (million)
% 17.46/3.35 % (3421227)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3599300376:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 17.46/3.35 % (3421224)Instruction limit reached!
% 17.46/3.35 % (3421224)------------------------------
% 17.46/3.35 % (3421224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.46/3.35 % (3421224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/3.35 % (3421224)CaDiCaL version: 2.1.3
% 17.46/3.35 % (3421224)Termination reason: Instruction limit
% 17.46/3.35 % (3421224)Termination phase: Saturation
% 17.46/3.35 % (3421224)Time elapsed: 0.120 s
% 17.46/3.35 % (3421224)Peak memory usage: 133 MB
% 17.46/3.35 % (3421224)Instructions burned: 72 (million)
% 17.46/3.35 % (3421231)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1541914466:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi)
% 17.46/3.35 % (3421236)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=140889205:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 17.46/3.35 % (3421235)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=674099423:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.46/3.35 % (3421217)Instruction limit reached!
% 17.46/3.35 % (3421217)------------------------------
% 17.46/3.35 % (3421217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.46/3.35 % (3421217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/3.35 % (3421217)CaDiCaL version: 2.1.3
% 17.46/3.35 % (3421217)Termination reason: Instruction limit
% 17.46/3.35 % (3421217)Termination phase: Saturation
% 17.46/3.35 % (3421217)Time elapsed: 0.365 s
% 17.46/3.35 % (3421217)Peak memory usage: 91 MB
% 17.46/3.35 % (3421217)Instructions burned: 371 (million)
% 17.46/3.35 % (3421236)Instruction limit reached!
% 17.46/3.35 % (3421236)------------------------------
% 17.46/3.35 % (3421236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.46/3.35 % (3421236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/3.35 % (3421236)CaDiCaL version: 2.1.3
% 17.46/3.35 % (3421236)Termination reason: Instruction limit
% 17.46/3.35 % (3421236)Termination phase: Saturation
% 17.46/3.35 % (3421236)Time elapsed: 0.055 s
% 17.46/3.35 % (3421236)Peak memory usage: 133 MB
% 17.46/3.35 % (3421236)Instructions burned: 40 (million)
% 17.46/3.35 % (3421237)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3710084725:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi)
% 19.61/3.76 % (3421231)Instruction limit reached!
% 19.61/3.76 % (3421231)------------------------------
% 19.61/3.76 % (3421231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421231)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421231)Termination reason: Instruction limit
% 19.61/3.76 % (3421231)Termination phase: Saturation
% 19.61/3.76 % (3421231)Time elapsed: 0.129 s
% 19.61/3.76 % (3421231)Peak memory usage: 112 MB
% 19.61/3.76 % (3421231)Instructions burned: 131 (million)
% 19.61/3.76 % (3421227)Instruction limit reached!
% 19.61/3.76 % (3421227)------------------------------
% 19.61/3.76 % (3421227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421227)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421227)Termination reason: Instruction limit
% 19.61/3.76 % (3421227)Termination phase: Saturation
% 19.61/3.76 % (3421227)Time elapsed: 0.284 s
% 19.61/3.76 % (3421227)Peak memory usage: 90 MB
% 19.61/3.76 % (3421227)Instructions burned: 294 (million)
% 19.61/3.76 % (3421239)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3983077739:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 19.61/3.76 % (3421235)Instruction limit reached!
% 19.61/3.76 % (3421235)------------------------------
% 19.61/3.76 % (3421235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421235)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421235)Termination reason: Instruction limit
% 19.61/3.76 % (3421235)Termination phase: Saturation
% 19.61/3.76 % (3421235)Time elapsed: 0.162 s
% 19.61/3.76 % (3421235)Peak memory usage: 132 MB
% 19.61/3.76 % (3421235)Instructions burned: 131 (million)
% 19.61/3.76 % (3421244)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2044478960:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 19.61/3.76 % (3421243)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3826116410:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi)
% 19.61/3.76 % (3421244)Refutation not found, incomplete strategy
% 19.61/3.76 % (3421244)------------------------------
% 19.61/3.76 % (3421244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421244)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421244)Termination reason: Refutation not found, incomplete strategy
% 19.61/3.76 % (3421244)Time elapsed: 0.026 s
% 19.61/3.76 % (3421244)Peak memory usage: 115 MB
% 19.61/3.76 % (3421244)Instructions burned: 10 (million)
% 19.61/3.76 % (3421237)Instruction limit reached!
% 19.61/3.76 % (3421237)------------------------------
% 19.61/3.76 % (3421237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421237)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421237)Termination reason: Instruction limit
% 19.61/3.76 % (3421237)Termination phase: Saturation
% 19.61/3.76 % (3421237)Time elapsed: 0.268 s
% 19.61/3.76 % (3421237)Peak memory usage: 92 MB
% 19.61/3.76 % (3421237)Instructions burned: 307 (million)
% 19.61/3.76 % (3421246)dis+10_1_si=on:random_seed=1166493086:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi)
% 19.61/3.76 % (3421247)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=149299121:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 19.61/3.76 % (3421243)Instruction limit reached!
% 19.61/3.76 % (3421243)------------------------------
% 19.61/3.76 % (3421243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421243)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421243)Termination reason: Instruction limit
% 19.61/3.76 % (3421243)Termination phase: Saturation
% 19.61/3.76 % (3421243)Time elapsed: 0.170 s
% 19.61/3.76 % (3421243)Peak memory usage: 117 MB
% 19.61/3.76 % (3421243)Instructions burned: 131 (million)
% 19.61/3.76 % (3421249)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4208203802:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi)
% 19.61/3.76 % (3421244)------------------------------
% 19.61/3.76 % (3421244)------------------------------
% 19.61/3.76 % (3421249)Instruction limit reached!
% 19.61/3.76 % (3421249)------------------------------
% 19.61/3.76 % (3421249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421249)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421249)Termination reason: Instruction limit
% 19.61/3.76 % (3421249)Termination phase: Saturation
% 19.61/3.76 % (3421249)Time elapsed: 0.100 s
% 19.61/3.76 % (3421249)Peak memory usage: 89 MB
% 19.61/3.76 % (3421249)Instructions burned: 142 (million)
% 19.61/3.76 % (3421252)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=221822373:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi)
% 19.61/3.76 % (3421257)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=1585586459:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi)
% 19.61/3.76 % (3421255)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2386246316:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi)
% 19.61/3.76 % (3421252)Instruction limit reached!
% 19.61/3.76 % (3421252)------------------------------
% 19.61/3.76 % (3421252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421252)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421252)Termination reason: Instruction limit
% 19.61/3.76 % (3421252)Termination phase: Saturation
% 19.61/3.76 % (3421252)Time elapsed: 0.096 s
% 19.61/3.76 % (3421252)Peak memory usage: 115 MB
% 19.61/3.76 % (3421252)Instructions burned: 65 (million)
% 19.61/3.76 % (3421258)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=1562214006:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi)
% 19.61/3.76 % (3421255)First to succeed.
% 19.61/3.76 % (3421239)Instruction limit reached!
% 19.61/3.76 % (3421239)------------------------------
% 19.61/3.76 % (3421239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421239)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421239)Termination reason: Instruction limit
% 19.61/3.76 % (3421239)Termination phase: Saturation
% 19.61/3.76 % (3421239)Time elapsed: 0.629 s
% 19.61/3.76 % (3421239)Peak memory usage: 139 MB
% 19.61/3.76 % (3421239)Instructions burned: 598 (million)
% 19.61/3.76 % (3421255)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3421162"
% 19.61/3.76 % (3421257)Instruction limit reached!
% 19.61/3.76 % (3421257)------------------------------
% 19.61/3.76 % (3421257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421257)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421257)Termination reason: Instruction limit
% 19.61/3.76 % (3421257)Termination phase: Saturation
% 19.61/3.76 % (3421257)Time elapsed: 0.113 s
% 19.61/3.76 % (3421257)Peak memory usage: 117 MB
% 19.61/3.76 % (3421257)Instructions burned: 128 (million)
% 19.61/3.76 % (3421258)Instruction limit reached!
% 19.61/3.76 % (3421258)------------------------------
% 19.61/3.76 % (3421258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421258)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421258)Termination reason: Instruction limit
% 19.61/3.76 % (3421258)Termination phase: Saturation
% 19.61/3.76 % (3421258)Time elapsed: 0.038 s
% 19.61/3.76 % (3421258)Peak memory usage: 115 MB
% 19.61/3.76 % (3421258)Instructions burned: 41 (million)
% 19.61/3.76 % (3421247)Instruction limit reached!
% 19.61/3.76 % (3421247)------------------------------
% 19.61/3.76 % (3421247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (3421247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (3421247)CaDiCaL version: 2.1.3
% 19.61/3.76 % (3421247)Termination reason: Instruction limit
% 19.61/3.76 % (3421247)Termination phase: Saturation
% 19.61/3.76 % (3421247)Time elapsed: 0.423 s
% 19.61/3.76 % (3421247)Peak memory usage: 95 MB
% 19.61/3.77 % (3421247)Instructions burned: 383 (million)
% 19.61/3.77 % (3421262)dis+1010_1_to=kbo:si=on:random_seed=3461758366:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi)
% 19.61/3.77 % (3421266)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=844673073:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi)
% 19.61/3.77 % (3421265)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3617349109:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 19.61/3.77 % (3421264)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3132986080:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi)
% 19.61/3.77 % (3421266)Instruction limit reached!
% 19.61/3.77 % (3421266)------------------------------
% 19.61/3.77 % (3421266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.77 % (3421266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.77 % (3421266)CaDiCaL version: 2.1.3
% 19.61/3.77 % (3421266)Termination reason: Instruction limit
% 19.61/3.77 % (3421266)Termination phase: Saturation
% 19.61/3.77 % (3421266)Time elapsed: 0.125 s
% 19.61/3.77 % (3421266)Peak memory usage: 131 MB
% 19.61/3.77 % (3421266)Instructions burned: 215 (million)
% 19.61/3.77 % (3421267)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1927540541:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 19.61/3.77 % (3421262)Instruction limit reached!
% 19.61/3.77 % (3421262)------------------------------
% 19.61/3.77 % (3421262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.77 % (3421262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.77 % (3421262)CaDiCaL version: 2.1.3
% 19.61/3.77 % (3421262)Termination reason: Instruction limit
% 19.61/3.77 % (3421262)Termination phase: Saturation
% 19.61/3.77 % (3421262)Time elapsed: 0.186 s
% 19.61/3.77 % (3421262)Peak memory usage: 91 MB
% 19.61/3.77 % (3421262)Instructions burned: 176 (million)
% 19.61/3.77 % (3421255)Refutation found. Thanks to Tanya!
% 19.61/3.77 % SZS status Theorem for theBenchmark
% 19.61/3.77 % SZS output start Proof for theBenchmark
% See solution above
% 21.33/3.92 % (3421255)------------------------------
% 21.33/3.92 % (3421255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.92 % (3421255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/3.92 % (3421255)CaDiCaL version: 2.1.3
% 21.33/3.92 % (3421255)Termination reason: Refutation
% 21.33/3.92 % (3421255)Time elapsed: 0.084 s
% 21.33/3.92 % (3421255)Peak memory usage: 91 MB
% 21.33/3.92 % (3421255)Instructions burned: 74 (million)
% 21.33/3.92 % (3421255)------------------------------
% 21.33/3.92 % (3421255)------------------------------
% 21.33/3.92 % (3421162)Success in time 2.926 s
% 21.33/3.92 % Vampire exiting
%------------------------------------------------------------------------------