%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW586_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 : n016.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:29 PM UTC 2026
% Result : Theorem 8.38s 1.55s
% Output : Refutation 8.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 95
% Number of leaves : 30
% Syntax : Number of formulae : 310 ( 55 unt; 0 typ; 14 def)
% Number of atoms : 1095 ( 539 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 929 ( 144 ~; 673 |; 104 &)
% ( 3 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 10 ( 8 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 : 77 ( 77 usr; 26 con; 0-8 aty)
% Number of variables : 267 ( 162 !; 105 ?; 267 :)
% 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(type_def_12,type,
stream1: $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,
char: ty ).
tff(func_def_11,type,
zero1: char2 ).
tff(func_def_12,type,
one1: char2 ).
tff(func_def_13,type,
match_char1: ( ty * char2 * uni * uni ) > uni ).
tff(func_def_14,type,
regexp: ty ).
tff(func_def_15,type,
empty1: regexp1 ).
tff(func_def_16,type,
epsilon1: regexp1 ).
tff(func_def_17,type,
char3: char2 > regexp1 ).
tff(func_def_18,type,
alt1: ( regexp1 * regexp1 ) > regexp1 ).
tff(func_def_19,type,
concat1: ( regexp1 * regexp1 ) > regexp1 ).
tff(func_def_20,type,
star1: regexp1 > regexp1 ).
tff(func_def_21,type,
match_regexp1: ( ty * regexp1 * uni * uni * uni * uni * uni * uni ) > uni ).
tff(func_def_22,type,
char_proj_11: regexp1 > char2 ).
tff(func_def_23,type,
alt_proj_11: regexp1 > regexp1 ).
tff(func_def_24,type,
alt_proj_21: regexp1 > regexp1 ).
tff(func_def_25,type,
concat_proj_11: regexp1 > regexp1 ).
tff(func_def_26,type,
concat_proj_21: regexp1 > regexp1 ).
tff(func_def_27,type,
star_proj_11: regexp1 > regexp1 ).
tff(func_def_28,type,
list: ty > ty ).
tff(func_def_29,type,
nil: ty > uni ).
tff(func_def_30,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_31,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_32,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_33,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_34,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_37,type,
length1: ( ty * uni ) > $int ).
tff(func_def_40,type,
t2tb: list_char > uni ).
tff(func_def_41,type,
tb2t: uni > list_char ).
tff(func_def_42,type,
t2tb1: char2 > uni ).
tff(func_def_43,type,
tb2t1: uni > char2 ).
tff(func_def_44,type,
option: ty > ty ).
tff(func_def_45,type,
none: ty > uni ).
tff(func_def_46,type,
some: ( ty * uni ) > uni ).
tff(func_def_47,type,
match_option1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_48,type,
some_proj_11: ( ty * uni ) > uni ).
tff(func_def_49,type,
stream: ty ).
tff(func_def_50,type,
mk_stream1: list_char > stream1 ).
tff(func_def_51,type,
state1: stream1 > list_char ).
tff(func_def_53,type,
sK4: ( ty * uni * uni ) > uni ).
tff(func_def_54,type,
sK5: ( ty * uni * uni ) > uni ).
tff(func_def_55,type,
sK6: ( list_char * regexp1 ) > list_char ).
tff(func_def_56,type,
sK7: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_57,type,
sK8: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_58,type,
sK9: ( list_char * regexp1 ) > list_char ).
tff(func_def_59,type,
sK10: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_60,type,
sK11: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_61,type,
sK12: ( list_char * regexp1 ) > list_char ).
tff(func_def_62,type,
sK13: ( list_char * regexp1 ) > list_char ).
tff(func_def_63,type,
sK14: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_64,type,
sK15: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_65,type,
sK16: ( list_char * regexp1 ) > list_char ).
tff(func_def_66,type,
sK17: ( list_char * regexp1 ) > list_char ).
tff(func_def_67,type,
sK18: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_68,type,
sK19: ( list_char * regexp1 ) > char2 ).
tff(func_def_69,type,
sK20: ( list_char * regexp1 ) > regexp1 ).
tff(func_def_70,type,
sK21: list_char > list_char ).
tff(func_def_71,type,
sK22: list_char ).
tff(func_def_72,type,
sF23: uni ).
tff(func_def_73,type,
sF24: uni ).
tff(func_def_74,type,
sF25: uni ).
tff(func_def_75,type,
sF26: list_char ).
tff(func_def_76,type,
sF27: regexp1 ).
tff(func_def_77,type,
sF28: regexp1 ).
tff(func_def_78,type,
sF29: regexp1 ).
tff(func_def_79,type,
sF30: regexp1 ).
tff(func_def_80,type,
sF31: regexp1 ).
tff(func_def_81,type,
sF32: 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: ( list_char * regexp1 ) > $o ).
tff(pred_def_7,type,
sP1: ( list_char * regexp1 ) > $o ).
tff(pred_def_8,type,
sP2: ( list_char * regexp1 ) > $o ).
tff(pred_def_9,type,
sP3: ( list_char * regexp1 ) > $o ).
tff(f25,axiom,
! [X0: char2] : ( epsilon1 != char3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',epsilon_Char) ).
tff(f26,axiom,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != alt1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',epsilon_Alt) ).
tff(f27,axiom,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != concat1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',epsilon_Concat) ).
tff(f28,axiom,
! [X0: regexp1] : ( epsilon1 != star1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',epsilon_Star) ).
tff(f29,axiom,
! [X0: char2,X1: regexp1,X2: regexp1] : ( char3(X0) != alt1(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',char_Alt) ).
tff(f32,axiom,
! [X0: regexp1,X1: regexp1,X2: regexp1,X3: regexp1] : ( alt1(X0,X1) != concat1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt_Concat) ).
tff(f33,axiom,
! [X0: regexp1,X1: regexp1,X2: regexp1] : ( alt1(X0,X1) != star1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt_Star) ).
tff(f36,axiom,
! [X0: regexp1,X1: regexp1] : ( alt_proj_11(alt1(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt_proj_1_def) ).
tff(f37,axiom,
! [X0: regexp1,X1: regexp1] : ( alt_proj_21(alt1(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alt_proj_2_def) ).
tff(f47,axiom,
! [X0: ty,X1: uni,X2: uni] : ( nil(X0) != cons(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nil_Cons) ).
tff(f67,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f73,axiom,
! [X0: list_char,X1: regexp1,X2: regexp1] :
( mem2(X0,X1)
=> mem2(X0,alt1(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_altl) ).
tff(f74,axiom,
! [X0: list_char,X1: regexp1,X2: regexp1] :
( mem2(X0,X2)
=> mem2(X0,alt1(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_altr) ).
tff(f78,axiom,
! [X0: list_char,X1: regexp1] :
( mem2(X0,X1)
=> ( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char,t2tb1(X2),nil(char))) )
& ( X1 = char3(X2) ) )
| ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X4)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X5)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ? [X6: list_char,X7: list_char,X4: regexp1,X5: regexp1] :
( mem2(X6,X4)
& mem2(X7,X5)
& ( X0 = tb2t(infix_plpl(char,t2tb(X6),t2tb(X7))) )
& ( X1 = concat1(X4,X5) ) )
| ? [X8: regexp1] :
( ( X0 = tb2t(nil(char)) )
& ( X1 = star1(X8) ) )
| ? [X6: list_char,X7: list_char,X8: regexp1] :
( mem2(X6,X8)
& mem2(X7,star1(X8))
& ( X0 = tb2t(infix_plpl(char,t2tb(X6),t2tb(X7))) )
& ( X1 = star1(X8) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_inversion) ).
tff(f94,axiom,
! [X0: list_char] :
( mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
<=> mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',one_w_in_r1) ).
tff(f96,conjecture,
! [X0: list_char] :
( mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
<=> mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',one_w_in_r2) ).
tff(f97,negated_conjecture,
~ ! [X0: list_char] :
( mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
<=> mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
tff(f118,plain,
! [X0: list_char,X1: regexp1] :
( mem2(X0,X1)
=> ( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char,t2tb1(X2),nil(char))) )
& ( X1 = char3(X2) ) )
| ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X4)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ? [X6: list_char,X7: regexp1,X8: regexp1] :
( mem2(X6,X8)
& ( X0 = X6 )
& ( alt1(X7,X8) = X1 ) )
| ? [X9: list_char,X10: list_char,X11: regexp1,X12: regexp1] :
( mem2(X9,X11)
& mem2(X10,X12)
& ( tb2t(infix_plpl(char,t2tb(X9),t2tb(X10))) = X0 )
& ( concat1(X11,X12) = X1 ) )
| ? [X13: regexp1] :
( ( X0 = tb2t(nil(char)) )
& ( star1(X13) = X1 ) )
| ? [X14: list_char,X15: list_char,X16: regexp1] :
( mem2(X14,X16)
& mem2(X15,star1(X16))
& ( tb2t(infix_plpl(char,t2tb(X14),t2tb(X15))) = X0 )
& ( star1(X16) = X1 ) ) ) ),
inference(rectify,[],[f78]) ).
tff(f137,plain,
! [X0: list_char,X1: regexp1,X2: regexp1] :
( mem2(X0,alt1(X1,X2))
| ~ mem2(X0,X1) ),
inference(ennf_transformation,[],[f73]) ).
tff(f138,plain,
! [X0: list_char,X1: regexp1,X2: regexp1] :
( mem2(X0,alt1(X1,X2))
| ~ mem2(X0,X2) ),
inference(ennf_transformation,[],[f74]) ).
tff(f143,plain,
! [X0: list_char,X1: regexp1] :
( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char,t2tb1(X2),nil(char))) )
& ( X1 = char3(X2) ) )
| ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X4)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ? [X6: list_char,X7: regexp1,X8: regexp1] :
( mem2(X6,X8)
& ( X0 = X6 )
& ( alt1(X7,X8) = X1 ) )
| ? [X9: list_char,X10: list_char,X11: regexp1,X12: regexp1] :
( mem2(X9,X11)
& mem2(X10,X12)
& ( tb2t(infix_plpl(char,t2tb(X9),t2tb(X10))) = X0 )
& ( concat1(X11,X12) = X1 ) )
| ? [X13: regexp1] :
( ( X0 = tb2t(nil(char)) )
& ( star1(X13) = X1 ) )
| ? [X14: list_char,X15: list_char,X16: regexp1] :
( mem2(X14,X16)
& mem2(X15,star1(X16))
& ( tb2t(infix_plpl(char,t2tb(X14),t2tb(X15))) = X0 )
& ( star1(X16) = X1 ) )
| ~ mem2(X0,X1) ),
inference(ennf_transformation,[],[f118]) ).
tff(f144,plain,
! [X0: list_char,X1: regexp1] :
( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char,t2tb1(X2),nil(char))) )
& ( X1 = char3(X2) ) )
| ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X4)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ? [X6: list_char,X7: regexp1,X8: regexp1] :
( mem2(X6,X8)
& ( X0 = X6 )
& ( alt1(X7,X8) = X1 ) )
| ? [X9: list_char,X10: list_char,X11: regexp1,X12: regexp1] :
( mem2(X9,X11)
& mem2(X10,X12)
& ( tb2t(infix_plpl(char,t2tb(X9),t2tb(X10))) = X0 )
& ( concat1(X11,X12) = X1 ) )
| ? [X13: regexp1] :
( ( X0 = tb2t(nil(char)) )
& ( star1(X13) = X1 ) )
| ? [X14: list_char,X15: list_char,X16: regexp1] :
( mem2(X14,X16)
& mem2(X15,star1(X16))
& ( tb2t(infix_plpl(char,t2tb(X14),t2tb(X15))) = X0 )
& ( star1(X16) = X1 ) )
| ~ mem2(X0,X1) ),
inference(flattening,[],[f143]) ).
tff(f150,plain,
? [X0: list_char] :
( mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
<~> mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(ennf_transformation,[],[f97]) ).
tff(f151,definition,
! [X0: list_char,X1: regexp1] :
( ? [X14: list_char,X15: list_char,X16: regexp1] :
( mem2(X14,X16)
& mem2(X15,star1(X16))
& ( tb2t(infix_plpl(char,t2tb(X14),t2tb(X15))) = X0 )
& ( star1(X16) = X1 ) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f152,definition,
! [X0: list_char,X1: regexp1] :
( ? [X9: list_char,X10: list_char,X11: regexp1,X12: regexp1] :
( mem2(X9,X11)
& mem2(X10,X12)
& ( tb2t(infix_plpl(char,t2tb(X9),t2tb(X10))) = X0 )
& ( concat1(X11,X12) = X1 ) )
| ~ sP1(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f153,definition,
! [X0: list_char,X1: regexp1] :
( ? [X6: list_char,X7: regexp1,X8: regexp1] :
( mem2(X6,X8)
& ( X0 = X6 )
& ( alt1(X7,X8) = X1 ) )
| ~ sP2(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f154,definition,
! [X0: list_char,X1: regexp1] :
( ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X4)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ~ sP3(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
tff(f155,plain,
! [X0: list_char,X1: regexp1] :
( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char,t2tb1(X2),nil(char))) )
& ( X1 = char3(X2) ) )
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| ? [X13: regexp1] :
( ( X0 = tb2t(nil(char)) )
& ( star1(X13) = X1 ) )
| sP0(X0,X1)
| ~ mem2(X0,X1) ),
inference(definition_folding,[],[f144,f154,f153,f152,f151]) ).
tff(f162,plain,
! [X0: list_char,X1: regexp1] :
( ? [X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X3,X4)
& ( X0 = X3 )
& ( X1 = alt1(X4,X5) ) )
| ~ sP3(X0,X1) ),
inference(nnf_transformation,[],[f154]) ).
tff(f163,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,[],[f162]) ).
tff(f164,plain,
! [X0: list_char,X1: regexp1] :
( ( mem2(sK6(X0,X1),sK7(X0,X1))
& ( sK6(X0,X1) = X0 )
& ( alt1(sK7(X0,X1),sK8(X0,X1)) = X1 ) )
| ~ sP3(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X2,sK6(X0,X1)),skolemize(X3,sK7(X0,X1)),skolemize(X4,sK8(X0,X1))],[f163]) ).
tff(f165,plain,
! [X0: list_char,X1: regexp1] :
( ? [X6: list_char,X7: regexp1,X8: regexp1] :
( mem2(X6,X8)
& ( X0 = X6 )
& ( alt1(X7,X8) = X1 ) )
| ~ sP2(X0,X1) ),
inference(nnf_transformation,[],[f153]) ).
tff(f166,plain,
! [X0: list_char,X1: regexp1] :
( ? [X2: list_char,X3: regexp1,X4: regexp1] :
( mem2(X2,X4)
& ( X0 = X2 )
& ( alt1(X3,X4) = X1 ) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f165]) ).
tff(f167,plain,
! [X0: list_char,X1: regexp1] :
( ( mem2(sK9(X0,X1),sK11(X0,X1))
& ( sK9(X0,X1) = X0 )
& ( alt1(sK10(X0,X1),sK11(X0,X1)) = X1 ) )
| ~ sP2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X2,sK9(X0,X1)),skolemize(X3,sK10(X0,X1)),skolemize(X4,sK11(X0,X1))],[f166]) ).
tff(f168,plain,
! [X0: list_char,X1: regexp1] :
( ? [X9: list_char,X10: list_char,X11: regexp1,X12: regexp1] :
( mem2(X9,X11)
& mem2(X10,X12)
& ( tb2t(infix_plpl(char,t2tb(X9),t2tb(X10))) = X0 )
& ( concat1(X11,X12) = X1 ) )
| ~ sP1(X0,X1) ),
inference(nnf_transformation,[],[f152]) ).
tff(f169,plain,
! [X0: list_char,X1: regexp1] :
( ? [X2: list_char,X3: list_char,X4: regexp1,X5: regexp1] :
( mem2(X2,X4)
& mem2(X3,X5)
& ( tb2t(infix_plpl(char,t2tb(X2),t2tb(X3))) = X0 )
& ( concat1(X4,X5) = X1 ) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f168]) ).
tff(f170,plain,
! [X0: list_char,X1: regexp1] :
( ( mem2(sK12(X0,X1),sK14(X0,X1))
& mem2(sK13(X0,X1),sK15(X0,X1))
& ( tb2t(infix_plpl(char,t2tb(sK12(X0,X1)),t2tb(sK13(X0,X1)))) = X0 )
& ( concat1(sK14(X0,X1),sK15(X0,X1)) = X1 ) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15]),skolemize(X2,sK12(X0,X1)),skolemize(X3,sK13(X0,X1)),skolemize(X4,sK14(X0,X1)),skolemize(X5,sK15(X0,X1))],[f169]) ).
tff(f171,plain,
! [X0: list_char,X1: regexp1] :
( ? [X14: list_char,X15: list_char,X16: regexp1] :
( mem2(X14,X16)
& mem2(X15,star1(X16))
& ( tb2t(infix_plpl(char,t2tb(X14),t2tb(X15))) = X0 )
& ( star1(X16) = X1 ) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f151]) ).
tff(f172,plain,
! [X0: list_char,X1: regexp1] :
( ? [X2: list_char,X3: list_char,X4: regexp1] :
( mem2(X2,X4)
& mem2(X3,star1(X4))
& ( tb2t(infix_plpl(char,t2tb(X2),t2tb(X3))) = X0 )
& ( star1(X4) = X1 ) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f171]) ).
tff(f173,plain,
! [X0: list_char,X1: regexp1] :
( ( mem2(sK16(X0,X1),sK18(X0,X1))
& mem2(sK17(X0,X1),star1(sK18(X0,X1)))
& ( tb2t(infix_plpl(char,t2tb(sK16(X0,X1)),t2tb(sK17(X0,X1)))) = X0 )
& ( star1(sK18(X0,X1)) = X1 ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X2,sK16(X0,X1)),skolemize(X3,sK17(X0,X1)),skolemize(X4,sK18(X0,X1))],[f172]) ).
tff(f174,plain,
! [X0: list_char,X1: regexp1] :
( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ? [X2: char2] :
( ( X0 = tb2t(cons(char,t2tb1(X2),nil(char))) )
& ( X1 = char3(X2) ) )
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| ? [X3: regexp1] :
( ( X0 = tb2t(nil(char)) )
& ( star1(X3) = X1 ) )
| sP0(X0,X1)
| ~ mem2(X0,X1) ),
inference(rectify,[],[f155]) ).
tff(f175,plain,
! [X0: list_char,X1: regexp1] :
( ( ( X0 = tb2t(nil(char)) )
& ( X1 = epsilon1 ) )
| ( ( tb2t(cons(char,t2tb1(sK19(X0,X1)),nil(char))) = X0 )
& ( char3(sK19(X0,X1)) = X1 ) )
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| ( ( X0 = tb2t(nil(char)) )
& ( star1(sK20(X0,X1)) = X1 ) )
| sP0(X0,X1)
| ~ mem2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X2,sK19(X0,X1)),skolemize(X3,sK20(X0,X1))],[f174]) ).
tff(f180,plain,
! [X0: list_char] :
( ( mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| ~ mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))) )
& ( mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))
| ~ mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ) ),
inference(nnf_transformation,[],[f94]) ).
tff(f182,plain,
? [X0: list_char] :
( ( ~ mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| ~ mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) )
& ( mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ) ),
inference(nnf_transformation,[],[f150]) ).
tff(f183,plain,
( ( ~ mem2(tb2t(cons(char,t2tb1(one1),t2tb(sK22))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) )
& ( mem2(tb2t(cons(char,t2tb1(one1),t2tb(sK22))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X0,sK22)],[f182]) ).
tff(f208,plain,
! [X0: char2] : ( epsilon1 != char3(X0) ),
inference(cnf_transformation,[],[f25]) ).
tff(f209,plain,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != alt1(X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
tff(f210,plain,
! [X0: regexp1,X1: regexp1] : ( epsilon1 != concat1(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
tff(f211,plain,
! [X0: regexp1] : ( epsilon1 != star1(X0) ),
inference(cnf_transformation,[],[f28]) ).
tff(f212,plain,
! [X2: regexp1,X0: char2,X1: regexp1] : ( char3(X0) != alt1(X1,X2) ),
inference(cnf_transformation,[],[f29]) ).
tff(f215,plain,
! [X2: regexp1,X3: regexp1,X0: regexp1,X1: regexp1] : ( alt1(X0,X1) != concat1(X2,X3) ),
inference(cnf_transformation,[],[f32]) ).
tff(f216,plain,
! [X2: regexp1,X0: regexp1,X1: regexp1] : ( alt1(X0,X1) != star1(X2) ),
inference(cnf_transformation,[],[f33]) ).
tff(f219,plain,
! [X0: regexp1,X1: regexp1] : ( alt_proj_11(alt1(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f36]) ).
tff(f220,plain,
! [X0: regexp1,X1: regexp1] : ( alt_proj_21(alt1(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f37]) ).
tff(f230,plain,
! [X2: uni,X0: ty,X1: uni] : ( nil(X0) != cons(X0,X1,X2) ),
inference(cnf_transformation,[],[f47]) ).
tff(f260,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f67]) ).
tff(f266,plain,
! [X2: regexp1,X0: list_char,X1: regexp1] :
( mem2(X0,alt1(X1,X2))
| ~ mem2(X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
tff(f267,plain,
! [X2: regexp1,X0: list_char,X1: regexp1] :
( mem2(X0,alt1(X1,X2))
| ~ mem2(X0,X2) ),
inference(cnf_transformation,[],[f138]) ).
tff(f271,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP3(X0,X1)
| ( alt1(sK7(X0,X1),sK8(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f164]) ).
tff(f272,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP3(X0,X1)
| ( sK6(X0,X1) = X0 ) ),
inference(cnf_transformation,[],[f164]) ).
tff(f273,plain,
! [X0: list_char,X1: regexp1] :
( mem2(sK6(X0,X1),sK7(X0,X1))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tff(f274,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP2(X0,X1)
| ( alt1(sK10(X0,X1),sK11(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f167]) ).
tff(f275,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP2(X0,X1)
| ( sK9(X0,X1) = X0 ) ),
inference(cnf_transformation,[],[f167]) ).
tff(f276,plain,
! [X0: list_char,X1: regexp1] :
( mem2(sK9(X0,X1),sK11(X0,X1))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
tff(f277,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP1(X0,X1)
| ( concat1(sK14(X0,X1),sK15(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f170]) ).
tff(f281,plain,
! [X0: list_char,X1: regexp1] :
( ~ sP0(X0,X1)
| ( star1(sK18(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f173]) ).
tff(f285,plain,
! [X0: list_char,X1: regexp1] :
( ~ mem2(X0,X1)
| ( char3(sK19(X0,X1)) = X1 )
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| ( star1(sK20(X0,X1)) = X1 )
| sP0(X0,X1)
| ( epsilon1 = X1 ) ),
inference(cnf_transformation,[],[f175]) ).
tff(f290,plain,
! [X0: list_char,X1: regexp1] :
( ( tb2t(nil(char)) = X0 )
| ( char3(sK19(X0,X1)) = X1 )
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| ( tb2t(nil(char)) = X0 )
| sP0(X0,X1)
| ~ mem2(X0,X1) ),
inference(cnf_transformation,[],[f175]) ).
tff(f310,plain,
! [X0: list_char] :
( mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))
| ~ mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(cnf_transformation,[],[f180]) ).
tff(f311,plain,
! [X0: list_char] :
( ~ mem2(tb2t(cons(char,t2tb1(one1),t2tb(X0))),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))
| mem2(X0,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(cnf_transformation,[],[f180]) ).
tff(f314,plain,
( mem2(tb2t(cons(char,t2tb1(one1),t2tb(sK22))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(cnf_transformation,[],[f183]) ).
tff(f315,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),t2tb(sK22))),alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1))))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(cnf_transformation,[],[f183]) ).
tff(f320,definition,
sF23 = t2tb1(one1),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f321,plain,
t2tb1(one1) = sF23,
inference(reorient_equations,[],[f320]) ).
tff(f322,definition,
sF24 = t2tb(sK22),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f323,plain,
t2tb(sK22) = sF24,
inference(reorient_equations,[],[f322]) ).
tff(f324,definition,
sF25 = cons(char,sF23,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f325,plain,
cons(char,sF23,sF24) = sF25,
inference(reorient_equations,[],[f324]) ).
tff(f326,definition,
sF26 = tb2t(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f327,plain,
tb2t(sF25) = sF26,
inference(reorient_equations,[],[f326]) ).
tff(f328,definition,
sF27 = char3(zero1),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f329,plain,
char3(zero1) = sF27,
inference(reorient_equations,[],[f328]) ).
tff(f330,definition,
sF28 = char3(one1),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f331,plain,
char3(one1) = sF28,
inference(reorient_equations,[],[f330]) ).
tff(f332,definition,
sF29 = alt1(sF27,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f333,plain,
alt1(sF27,sF28) = sF29,
inference(reorient_equations,[],[f332]) ).
tff(f334,definition,
sF30 = star1(sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f335,plain,
star1(sF29) = sF30,
inference(reorient_equations,[],[f334]) ).
tff(f336,definition,
sF31 = concat1(sF30,sF28),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f337,plain,
concat1(sF30,sF28) = sF31,
inference(reorient_equations,[],[f336]) ).
tff(f338,definition,
sF32 = alt1(epsilon1,sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f339,plain,
alt1(epsilon1,sF31) = sF32,
inference(reorient_equations,[],[f338]) ).
tff(f340,plain,
( ~ mem2(sF26,sF32)
| ~ mem2(sK22,sF32) ),
inference(definition_folding,[],[f315,f339,f337,f331,f335,f333,f331,f329,f339,f337,f331,f335,f333,f331,f329,f327,f325,f323,f321]) ).
tff(f341,plain,
( mem2(sF26,sF32)
| mem2(sK22,sF32) ),
inference(definition_folding,[],[f314,f339,f337,f331,f335,f333,f331,f329,f339,f337,f331,f335,f333,f331,f329,f327,f325,f323,f321]) ).
tff(f342,plain,
! [X0: list_char,X1: regexp1] :
( ~ mem2(X0,X1)
| ( char3(sK19(X0,X1)) = X1 )
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| sP0(X0,X1)
| ( tb2t(nil(char)) = X0 ) ),
inference(duplicate_literal_removal,[],[f290]) ).
tff(f364,plain,
sF25 = t2tb(sF26),
inference(superposition,[],[f260,f327]) ).
tff(f374,plain,
epsilon1 != sF32,
inference(superposition,[],[f209,f339]) ).
tff(f392,plain,
! [X0: char2] : ( char3(X0) != sF32 ),
inference(superposition,[],[f212,f339]) ).
tff(f397,plain,
! [X0: regexp1] : ( star1(X0) != sF32 ),
inference(superposition,[],[f216,f339]) ).
tff(f402,plain,
epsilon1 = alt_proj_11(sF32),
inference(superposition,[],[f219,f339]) ).
tff(f404,plain,
sF31 = alt_proj_21(sF32),
inference(superposition,[],[f220,f339]) ).
tff(f428,plain,
nil(char) != sF25,
inference(superposition,[],[f230,f325]) ).
tff(f460,plain,
! [X0: list_char] :
( ~ mem2(X0,epsilon1)
| mem2(X0,sF32) ),
inference(superposition,[],[f266,f339]) ).
tff(f462,plain,
! [X0: list_char] :
( ~ mem2(X0,sF31)
| mem2(X0,sF32) ),
inference(superposition,[],[f267,f339]) ).
tff(f1684,plain,
( ( sF32 = char3(sK19(sF26,sF32)) )
| sP3(sF26,sF32)
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32) ),
inference(resolution,[],[f342,f341]) ).
tff(f1685,plain,
( sP3(sF26,sF32)
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32) ),
inference(forward_subsumption_resolution,[],[f1684,f392]) ).
tff(f2053,plain,
( ( sF32 = char3(sK19(sF26,sF32)) )
| sP3(sF26,sF32)
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| ( sF32 = star1(sK20(sF26,sF32)) )
| sP0(sF26,sF32)
| ( epsilon1 = sF32 )
| mem2(sK22,sF32) ),
inference(resolution,[],[f285,f341]) ).
tff(f2054,plain,
( sP3(sF26,sF32)
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| ( sF32 = star1(sK20(sF26,sF32)) )
| sP0(sF26,sF32)
| ( epsilon1 = sF32 )
| mem2(sK22,sF32) ),
inference(forward_subsumption_resolution,[],[f2053,f392]) ).
tff(f2069,plain,
( sP3(sF26,sF32)
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| ( epsilon1 = sF32 )
| mem2(sK22,sF32) ),
inference(forward_subsumption_resolution,[],[f2054,f397]) ).
tff(f2083,plain,
( sP3(sF26,sF32)
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32) ),
inference(forward_subsumption_resolution,[],[f2069,f374]) ).
tff(f2159,plain,
( sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(resolution,[],[f2083,f271]) ).
tff(f2160,plain,
( sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(resolution,[],[f2083,f272]) ).
tff(f2166,plain,
( mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(superposition,[],[f310,f323]) ).
tff(f2179,plain,
( mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(alt1(char3(zero1),sF28)),sF28))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2166,f331]) ).
tff(f2191,plain,
( mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(alt1(sF27,sF28)),sF28))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2179,f329]) ).
tff(f2203,plain,
( mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(sF29),sF28))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2191,f333]) ).
tff(f2214,plain,
( mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(sF30,sF28))
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2203,f335]) ).
tff(f2225,plain,
( mem2(tb2t(cons(char,t2tb1(one1),sF24)),sF31)
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2214,f337]) ).
tff(f2236,plain,
( mem2(tb2t(cons(char,sF23,sF24)),sF31)
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2225,f321]) ).
tff(f2247,plain,
( mem2(tb2t(sF25),sF31)
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2236,f325]) ).
tff(f2258,plain,
( mem2(sF26,sF31)
| ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2247,f327]) ).
tff(f2268,plain,
( ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),sF28)),sF28)))
| mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2258,f331]) ).
tff(f2278,plain,
( ~ mem2(sK22,alt1(epsilon1,concat1(star1(alt1(sF27,sF28)),sF28)))
| mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2268,f329]) ).
tff(f2286,plain,
( ~ mem2(sK22,alt1(epsilon1,concat1(star1(sF29),sF28)))
| mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2278,f333]) ).
tff(f2293,plain,
( ~ mem2(sK22,alt1(epsilon1,concat1(sF30,sF28)))
| mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2286,f335]) ).
tff(f2297,plain,
( ~ mem2(sK22,alt1(epsilon1,sF31))
| mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2293,f337]) ).
tff(f2301,plain,
( ~ mem2(sK22,sF32)
| mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2297,f339]) ).
tff(f2361,plain,
( sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(resolution,[],[f2160,f274]) ).
tff(f2362,plain,
( sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(resolution,[],[f2160,f275]) ).
tff(f2365,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(superposition,[],[f311,f323]) ).
tff(f2378,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(alt1(char3(zero1),sF28)),sF28))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2365,f331]) ).
tff(f2386,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(alt1(sF27,sF28)),sF28))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2378,f329]) ).
tff(f2394,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(star1(sF29),sF28))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2386,f333]) ).
tff(f2401,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),sF24)),concat1(sF30,sF28))
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2394,f335]) ).
tff(f2408,plain,
( ~ mem2(tb2t(cons(char,t2tb1(one1),sF24)),sF31)
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2401,f337]) ).
tff(f2415,plain,
( ~ mem2(tb2t(cons(char,sF23,sF24)),sF31)
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2408,f321]) ).
tff(f2422,plain,
( ~ mem2(tb2t(sF25),sF31)
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2415,f325]) ).
tff(f2429,plain,
( ~ mem2(sF26,sF31)
| mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),char3(one1))),char3(one1)))) ),
inference(forward_demodulation,[],[f2422,f327]) ).
tff(f2436,plain,
( mem2(sK22,alt1(epsilon1,concat1(star1(alt1(char3(zero1),sF28)),sF28)))
| ~ mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2429,f331]) ).
tff(f2443,plain,
( mem2(sK22,alt1(epsilon1,concat1(star1(alt1(sF27,sF28)),sF28)))
| ~ mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2436,f329]) ).
tff(f2448,plain,
( mem2(sK22,alt1(epsilon1,concat1(star1(sF29),sF28)))
| ~ mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2443,f333]) ).
tff(f2452,plain,
( mem2(sK22,alt1(epsilon1,concat1(sF30,sF28)))
| ~ mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2448,f335]) ).
tff(f2453,plain,
( mem2(sK22,alt1(epsilon1,sF31))
| ~ mem2(sF26,sF31) ),
inference(forward_demodulation,[],[f2452,f337]) ).
tff(f2454,plain,
( ~ mem2(sF26,sF31)
| mem2(sK22,sF32) ),
inference(forward_demodulation,[],[f2453,f339]) ).
tff(f2456,plain,
( sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f2362,f277]) ).
tff(f2623,plain,
( sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(resolution,[],[f2159,f274]) ).
tff(f2624,plain,
( sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(resolution,[],[f2159,f275]) ).
tff(f2704,plain,
( sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f2361,f277]) ).
tff(f2881,plain,
( sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f2624,f277]) ).
tff(f3044,plain,
( mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f2456,f281]) ).
tff(f3045,plain,
( mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f3044,f397]) ).
tff(f3431,plain,
( sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f2623,f277]) ).
tff(f3618,plain,
( mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f2301,f3045]) ).
tff(f3619,plain,
( mem2(sF26,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(resolution,[],[f3618,f462]) ).
tff(f3637,plain,
( ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f3619,f340]) ).
tff(f3654,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f3637,f3045]) ).
tff(f3700,plain,
! [X0: regexp1,X1: regexp1] :
( ( alt1(X0,X1) != sF32 )
| ( sF26 = sK9(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(superposition,[],[f215,f3654]) ).
tff(f3938,plain,
( ( sF32 != sF32 )
| ( sF26 = sK9(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(superposition,[],[f3700,f339]) ).
tff(f3939,plain,
( ( sF26 = sK9(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(trivial_inequality_removal,[],[f3938]) ).
tff(f3949,plain,
( mem2(sF26,sK11(sF26,sF32))
| ~ sP2(sF26,sF32)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(superposition,[],[f276,f3939]) ).
tff(f4010,plain,
( mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f2704,f281]) ).
tff(f4011,plain,
( mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f4010,f397]) ).
tff(f4020,plain,
( mem2(sF26,sF31)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(resolution,[],[f4011,f2301]) ).
tff(f4050,plain,
( mem2(sF26,sF32)
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(resolution,[],[f4020,f462]) ).
tff(f4075,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f4050,f340]) ).
tff(f4092,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f4075,f4011]) ).
tff(f4118,plain,
! [X0: regexp1,X1: regexp1] :
( ( alt1(X0,X1) != sF32 )
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(superposition,[],[f215,f4092]) ).
tff(f4129,plain,
( ( sF32 != sF32 )
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(superposition,[],[f4118,f339]) ).
tff(f4130,plain,
( ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(trivial_inequality_removal,[],[f4129]) ).
tff(f4141,plain,
! [X0: regexp1,X1: regexp1] :
( ( concat1(X0,X1) != sF32 )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(superposition,[],[f215,f4130]) ).
tff(f4144,plain,
( ( alt_proj_21(sF32) = sK11(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(superposition,[],[f220,f4130]) ).
tff(f4151,plain,
( ( sF31 = sK11(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(forward_demodulation,[],[f4144,f404]) ).
tff(f4180,plain,
( mem2(sF26,sF31)
| ~ sP2(sF26,sF32)
| ( sF26 = sK6(sF26,sF32) )
| ( sF26 = sK6(sF26,sF32) ) ),
inference(superposition,[],[f3949,f4151]) ).
tff(f4182,plain,
( ~ sP2(sF26,sF32)
| mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(duplicate_literal_removal,[],[f4180]) ).
tff(f4193,plain,
( mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) )
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(resolution,[],[f4182,f2160]) ).
tff(f4197,plain,
( mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) )
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32) ),
inference(duplicate_literal_removal,[],[f4193]) ).
tff(f4200,plain,
( sP1(sF26,sF32)
| ( sF26 = sK6(sF26,sF32) )
| mem2(sF26,sF31)
| sP0(sF26,sF32) ),
inference(forward_subsumption_resolution,[],[f4197,f2301]) ).
tff(f4517,plain,
( ( sF26 = sK6(sF26,sF32) )
| mem2(sF26,sF31)
| sP0(sF26,sF32)
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f4200,f277]) ).
tff(f4518,plain,
( sP0(sF26,sF32)
| mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f4517,f4141]) ).
tff(f4523,plain,
( mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f4518,f281]) ).
tff(f4524,plain,
( mem2(sF26,sF31)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f4523,f397]) ).
tff(f4531,plain,
( mem2(sK22,sF32)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(resolution,[],[f4524,f2454]) ).
tff(f4532,plain,
( mem2(sF26,sF32)
| ( sF26 = sK6(sF26,sF32) ) ),
inference(resolution,[],[f4524,f462]) ).
tff(f4577,plain,
( ( sF26 = sK6(sF26,sF32) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f4532,f340]) ).
tff(f4594,plain,
sF26 = sK6(sF26,sF32),
inference(forward_subsumption_resolution,[],[f4577,f4531]) ).
tff(f4611,plain,
( mem2(sF26,sK7(sF26,sF32))
| ~ sP3(sF26,sF32) ),
inference(superposition,[],[f273,f4594]) ).
tff(f4626,plain,
( sP3(sF26,sK7(sF26,sF32))
| ( sK7(sF26,sF32) = char3(sK19(sF26,sK7(sF26,sF32))) )
| ~ sP3(sF26,sF32)
| sP2(sF26,sK7(sF26,sF32))
| sP1(sF26,sK7(sF26,sF32))
| sP0(sF26,sK7(sF26,sF32))
| ( tb2t(nil(char)) = sF26 ) ),
inference(resolution,[],[f4611,f342]) ).
tff(f4943,plain,
( mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f2881,f281]) ).
tff(f4944,plain,
( mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f4943,f397]) ).
tff(f4956,plain,
( mem2(sF26,sF31)
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(resolution,[],[f4944,f2301]) ).
tff(f4984,plain,
( mem2(sF26,sF32)
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(resolution,[],[f4956,f462]) ).
tff(f5012,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f4984,f340]) ).
tff(f5029,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f5012,f4944]) ).
tff(f5048,plain,
! [X0: regexp1,X1: regexp1] :
( ( alt1(X0,X1) != sF32 )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(superposition,[],[f215,f5029]) ).
tff(f5064,plain,
( ( sF32 != sF32 )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(superposition,[],[f5048,f339]) ).
tff(f5075,plain,
( ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(trivial_inequality_removal,[],[f5064]) ).
tff(f5087,plain,
! [X0: regexp1,X1: regexp1] :
( ( concat1(X0,X1) != sF32 )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(superposition,[],[f215,f5075]) ).
tff(f5089,plain,
( ( alt_proj_11(sF32) = sK7(sF26,sF32) )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(superposition,[],[f219,f5075]) ).
tff(f5100,plain,
( ( sF26 = sK9(sF26,sF32) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(forward_demodulation,[],[f5089,f402]) ).
tff(f5143,plain,
( mem2(sF26,sK11(sF26,sF32))
| ~ sP2(sF26,sF32)
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(superposition,[],[f276,f5100]) ).
tff(f5905,plain,
( mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f3431,f281]) ).
tff(f5906,plain,
( mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f5905,f397]) ).
tff(f5921,plain,
( mem2(sF26,sF31)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(resolution,[],[f5906,f2301]) ).
tff(f5959,plain,
( mem2(sF26,sF32)
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(resolution,[],[f5921,f462]) ).
tff(f5984,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f5959,f340]) ).
tff(f6001,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f5984,f5906]) ).
tff(f6021,plain,
! [X0: regexp1,X1: regexp1] :
( ( alt1(X0,X1) != sF32 )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(superposition,[],[f215,f6001]) ).
tff(f6053,plain,
( ( sF32 != sF32 )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(superposition,[],[f6021,f339]) ).
tff(f6061,plain,
( ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(trivial_inequality_removal,[],[f6053]) ).
tff(f6075,plain,
! [X0: regexp1,X1: regexp1] :
( ( concat1(X0,X1) != sF32 )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(superposition,[],[f215,f6061]) ).
tff(f6078,plain,
( ( alt_proj_21(sF32) = sK11(sF26,sF32) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(superposition,[],[f220,f6061]) ).
tff(f6087,plain,
( ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF31 = sK11(sF26,sF32) ) ),
inference(forward_demodulation,[],[f6078,f404]) ).
tff(f6144,plain,
( ( alt_proj_11(sF32) = sK7(sF26,sF32) )
| ( sF31 = sK11(sF26,sF32) ) ),
inference(superposition,[],[f219,f6087]) ).
tff(f6154,plain,
( ( sF31 = sK11(sF26,sF32) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(forward_demodulation,[],[f6144,f402]) ).
tff(f6200,plain,
( mem2(sF26,sF31)
| ~ sP2(sF26,sF32)
| ( epsilon1 = sK7(sF26,sF32) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(superposition,[],[f5143,f6154]) ).
tff(f6203,plain,
( ~ sP2(sF26,sF32)
| mem2(sF26,sF31)
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(duplicate_literal_removal,[],[f6200]) ).
tff(f6215,plain,
( mem2(sF26,sF31)
| ( epsilon1 = sK7(sF26,sF32) )
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(resolution,[],[f6203,f2159]) ).
tff(f6222,plain,
( sP1(sF26,sF32)
| ( epsilon1 = sK7(sF26,sF32) )
| mem2(sF26,sF31)
| sP0(sF26,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f6215,f2301]) ).
tff(f7286,plain,
( ( epsilon1 = sK7(sF26,sF32) )
| mem2(sF26,sF31)
| sP0(sF26,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f6222,f277]) ).
tff(f7287,plain,
( sP0(sF26,sF32)
| mem2(sF26,sF31)
| ( epsilon1 = sK7(sF26,sF32) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f7286,f6075]) ).
tff(f7297,plain,
( mem2(sF26,sF31)
| ( epsilon1 = sK7(sF26,sF32) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f7287,f281]) ).
tff(f7298,plain,
( mem2(sF26,sF31)
| ( epsilon1 = sK7(sF26,sF32) )
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f7297,f397]) ).
tff(f7310,plain,
( mem2(sK22,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(resolution,[],[f7298,f2454]) ).
tff(f7311,plain,
( mem2(sF26,sF32)
| ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(resolution,[],[f7298,f462]) ).
tff(f7453,plain,
( ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( epsilon1 = sK7(sF26,sF32) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f7311,f340]) ).
tff(f7470,plain,
( ( sF32 = alt1(sK7(sF26,sF32),sK8(sF26,sF32)) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f7453,f7310]) ).
tff(f7541,plain,
( ( alt_proj_11(sF32) = sK7(sF26,sF32) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(superposition,[],[f219,f7470]) ).
tff(f7551,plain,
( ( epsilon1 = sK7(sF26,sF32) )
| ( epsilon1 = sK7(sF26,sF32) ) ),
inference(forward_demodulation,[],[f7541,f402]) ).
tff(f7552,plain,
epsilon1 = sK7(sF26,sF32),
inference(duplicate_literal_removal,[],[f7551]) ).
tff(f7574,plain,
( ~ sP3(sF26,sF32)
| mem2(sF26,epsilon1) ),
inference(superposition,[],[f4611,f7552]) ).
tff(f7610,plain,
( sP2(sF26,sF32)
| mem2(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32) ),
inference(resolution,[],[f7574,f2083]) ).
tff(f7611,plain,
( sP2(sF26,sF32)
| mem2(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32) ),
inference(resolution,[],[f7574,f1685]) ).
tff(f7748,plain,
( sP1(sF26,sF32)
| mem2(sF26,epsilon1)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) ) ),
inference(resolution,[],[f7610,f275]) ).
tff(f7761,plain,
( mem2(sF26,epsilon1)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f7748,f277]) ).
tff(f7762,plain,
( sP0(sF26,sF32)
| mem2(sF26,epsilon1)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f7761,f5087]) ).
tff(f7768,plain,
( mem2(sF26,epsilon1)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f7762,f281]) ).
tff(f7769,plain,
( mem2(sF26,epsilon1)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) ) ),
inference(forward_subsumption_resolution,[],[f7768,f397]) ).
tff(f7787,plain,
( mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( epsilon1 = char3(sK19(sF26,epsilon1)) )
| sP3(sF26,epsilon1)
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(resolution,[],[f7769,f342]) ).
tff(f7789,plain,
( sP3(sF26,epsilon1)
| ( sF26 = sK9(sF26,sF32) )
| mem2(sK22,sF32)
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f7787,f208]) ).
tff(f7914,plain,
( ( sF26 = sK9(sF26,sF32) )
| mem2(sK22,sF32)
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| ( epsilon1 = alt1(sK7(sF26,epsilon1),sK8(sF26,epsilon1)) ) ),
inference(resolution,[],[f7789,f271]) ).
tff(f7916,plain,
( sP2(sF26,epsilon1)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f7914,f209]) ).
tff(f7923,plain,
( mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| ( epsilon1 = alt1(sK10(sF26,epsilon1),sK11(sF26,epsilon1)) ) ),
inference(resolution,[],[f7916,f274]) ).
tff(f7925,plain,
( sP1(sF26,epsilon1)
| ( sF26 = sK9(sF26,sF32) )
| mem2(sK22,sF32)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f7923,f209]) ).
tff(f7934,plain,
( ( sF26 = sK9(sF26,sF32) )
| mem2(sK22,sF32)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| ( epsilon1 = concat1(sK14(sF26,epsilon1),sK15(sF26,epsilon1)) ) ),
inference(resolution,[],[f7925,f277]) ).
tff(f7935,plain,
( sP0(sF26,epsilon1)
| mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f7934,f210]) ).
tff(f8068,plain,
( mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 )
| ( epsilon1 = star1(sK18(sF26,epsilon1)) ) ),
inference(resolution,[],[f7935,f281]) ).
tff(f8069,plain,
( mem2(sK22,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f8068,f211]) ).
tff(f8145,plain,
( mem2(sF26,sF31)
| ( tb2t(nil(char)) = sF26 )
| ( sF26 = sK9(sF26,sF32) ) ),
inference(resolution,[],[f8069,f2301]) ).
tff(f8238,plain,
( mem2(sF26,sF32)
| ( sF26 = sK9(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(resolution,[],[f8145,f462]) ).
tff(f8272,plain,
( ( sF26 = sK9(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f8238,f340]) ).
tff(f8295,plain,
( ( sF26 = sK9(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f8272,f8069]) ).
tff(f8322,plain,
( mem2(sF26,sK11(sF26,sF32))
| ~ sP2(sF26,sF32)
| ( tb2t(nil(char)) = sF26 ) ),
inference(superposition,[],[f276,f8295]) ).
tff(f13793,plain,
( ( sK7(sF26,sF32) = char3(sK19(sF26,sK7(sF26,sF32))) )
| ~ sP3(sF26,sF32)
| sP2(sF26,sK7(sF26,sF32))
| sP1(sF26,sK7(sF26,sF32))
| sP0(sF26,sK7(sF26,sF32))
| ( tb2t(nil(char)) = sF26 )
| ( sK7(sF26,sF32) = alt1(sK7(sF26,sK7(sF26,sF32)),sK8(sF26,sK7(sF26,sF32))) ) ),
inference(resolution,[],[f4626,f271]) ).
tff(f13798,plain,
( ( epsilon1 = char3(sK19(sF26,epsilon1)) )
| ~ sP3(sF26,sF32)
| sP2(sF26,sK7(sF26,sF32))
| sP1(sF26,sK7(sF26,sF32))
| sP0(sF26,sK7(sF26,sF32))
| ( tb2t(nil(char)) = sF26 )
| ( sK7(sF26,sF32) = alt1(sK7(sF26,sK7(sF26,sF32)),sK8(sF26,sK7(sF26,sF32))) ) ),
inference(forward_demodulation,[],[f13793,f7552]) ).
tff(f13800,plain,
( ~ sP3(sF26,sF32)
| sP2(sF26,sK7(sF26,sF32))
| sP1(sF26,sK7(sF26,sF32))
| sP0(sF26,sK7(sF26,sF32))
| ( tb2t(nil(char)) = sF26 )
| ( sK7(sF26,sF32) = alt1(sK7(sF26,sK7(sF26,sF32)),sK8(sF26,sK7(sF26,sF32))) ) ),
inference(forward_subsumption_resolution,[],[f13798,f208]) ).
tff(f13802,plain,
( sP2(sF26,epsilon1)
| ~ sP3(sF26,sF32)
| sP1(sF26,sK7(sF26,sF32))
| sP0(sF26,sK7(sF26,sF32))
| ( tb2t(nil(char)) = sF26 )
| ( sK7(sF26,sF32) = alt1(sK7(sF26,sK7(sF26,sF32)),sK8(sF26,sK7(sF26,sF32))) ) ),
inference(forward_demodulation,[],[f13800,f7552]) ).
tff(f13804,plain,
( sP1(sF26,epsilon1)
| sP2(sF26,epsilon1)
| ~ sP3(sF26,sF32)
| sP0(sF26,sK7(sF26,sF32))
| ( tb2t(nil(char)) = sF26 )
| ( sK7(sF26,sF32) = alt1(sK7(sF26,sK7(sF26,sF32)),sK8(sF26,sK7(sF26,sF32))) ) ),
inference(forward_demodulation,[],[f13802,f7552]) ).
tff(f13806,plain,
( sP0(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP2(sF26,epsilon1)
| ~ sP3(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| ( sK7(sF26,sF32) = alt1(sK7(sF26,sK7(sF26,sF32)),sK8(sF26,sK7(sF26,sF32))) ) ),
inference(forward_demodulation,[],[f13804,f7552]) ).
tff(f13808,plain,
( ( epsilon1 = alt1(sK7(sF26,epsilon1),sK8(sF26,epsilon1)) )
| sP0(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP2(sF26,epsilon1)
| ~ sP3(sF26,sF32)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_demodulation,[],[f13806,f7552]) ).
tff(f13809,plain,
( ~ sP3(sF26,sF32)
| sP1(sF26,epsilon1)
| sP2(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f13808,f209]) ).
tff(f13849,plain,
( sP1(sF26,epsilon1)
| sP2(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP2(sF26,sF32)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32) ),
inference(resolution,[],[f13809,f1685]) ).
tff(f13850,plain,
( sP2(sF26,sF32)
| sP2(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP1(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32) ),
inference(duplicate_literal_removal,[],[f13849]) ).
tff(f13928,plain,
( sP2(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP1(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(resolution,[],[f13850,f274]) ).
tff(f14604,plain,
( sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP1(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( epsilon1 = alt1(sK10(sF26,epsilon1),sK11(sF26,epsilon1)) ) ),
inference(resolution,[],[f13928,f274]) ).
tff(f14606,plain,
( sP1(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f14604,f209]) ).
tff(f14642,plain,
( sP1(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP0(sF26,epsilon1)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f14606,f277]) ).
tff(f14737,plain,
( ( tb2t(nil(char)) = sF26 )
| sP0(sF26,epsilon1)
| sP0(sF26,sF32)
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( epsilon1 = concat1(sK14(sF26,epsilon1),sK15(sF26,epsilon1)) ) ),
inference(resolution,[],[f14642,f277]) ).
tff(f14738,plain,
( sP0(sF26,sF32)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f14737,f210]) ).
tff(f14797,plain,
( sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f14738,f281]) ).
tff(f14798,plain,
( sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f14797,f397]) ).
tff(f14814,plain,
( ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( epsilon1 = star1(sK18(sF26,epsilon1)) ) ),
inference(resolution,[],[f14798,f281]) ).
tff(f14815,plain,
( mem2(sK22,sF32)
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f14814,f211]) ).
tff(f14832,plain,
( mem2(sF26,sF31)
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(resolution,[],[f14815,f2301]) ).
tff(f14920,plain,
( mem2(sF26,sF32)
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(resolution,[],[f14832,f462]) ).
tff(f15008,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ~ mem2(sK22,sF32) ),
inference(resolution,[],[f14920,f340]) ).
tff(f15031,plain,
( ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) )
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(forward_subsumption_resolution,[],[f15008,f14815]) ).
tff(f15089,plain,
! [X0: regexp1,X1: regexp1] :
( ( alt1(X0,X1) != sF32 )
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(superposition,[],[f215,f15031]) ).
tff(f15173,plain,
( ( sF32 != sF32 )
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) ) ),
inference(superposition,[],[f15089,f339]) ).
tff(f15215,plain,
( ( sF32 = alt1(sK10(sF26,sF32),sK11(sF26,sF32)) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(trivial_inequality_removal,[],[f15173]) ).
tff(f15256,plain,
! [X0: regexp1,X1: regexp1] :
( ( concat1(X0,X1) != sF32 )
| ( tb2t(nil(char)) = sF26 ) ),
inference(superposition,[],[f215,f15215]) ).
tff(f15259,plain,
( ( alt_proj_21(sF32) = sK11(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(superposition,[],[f220,f15215]) ).
tff(f15280,plain,
( ( sF31 = sK11(sF26,sF32) )
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_demodulation,[],[f15259,f404]) ).
tff(f15330,plain,
( mem2(sF26,sF31)
| ~ sP2(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| ( tb2t(nil(char)) = sF26 ) ),
inference(superposition,[],[f8322,f15280]) ).
tff(f15334,plain,
( ~ sP2(sF26,sF32)
| mem2(sF26,sF31)
| ( tb2t(nil(char)) = sF26 ) ),
inference(duplicate_literal_removal,[],[f15330]) ).
tff(f15375,plain,
( mem2(sF26,sF31)
| ( tb2t(nil(char)) = sF26 )
| mem2(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32) ),
inference(resolution,[],[f15334,f7611]) ).
tff(f15378,plain,
( mem2(sF26,sF31)
| ( tb2t(nil(char)) = sF26 )
| mem2(sF26,epsilon1)
| sP1(sF26,sF32)
| sP0(sF26,sF32)
| mem2(sK22,sF32) ),
inference(duplicate_literal_removal,[],[f15375]) ).
tff(f15383,plain,
( sP1(sF26,sF32)
| ( tb2t(nil(char)) = sF26 )
| mem2(sF26,epsilon1)
| mem2(sF26,sF31)
| sP0(sF26,sF32) ),
inference(forward_subsumption_resolution,[],[f15378,f2301]) ).
tff(f16165,plain,
( ( tb2t(nil(char)) = sF26 )
| mem2(sF26,epsilon1)
| mem2(sF26,sF31)
| sP0(sF26,sF32)
| ( sF32 = concat1(sK14(sF26,sF32),sK15(sF26,sF32)) ) ),
inference(resolution,[],[f15383,f277]) ).
tff(f16166,plain,
( sP0(sF26,sF32)
| mem2(sF26,epsilon1)
| mem2(sF26,sF31)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f16165,f15256]) ).
tff(f16391,plain,
( mem2(sF26,epsilon1)
| mem2(sF26,sF31)
| ( tb2t(nil(char)) = sF26 )
| ( sF32 = star1(sK18(sF26,sF32)) ) ),
inference(resolution,[],[f16166,f281]) ).
tff(f16392,plain,
( mem2(sF26,sF31)
| mem2(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f16391,f397]) ).
tff(f16616,plain,
( mem2(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32) ),
inference(resolution,[],[f16392,f2454]) ).
tff(f16618,plain,
( mem2(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| mem2(sF26,sF32) ),
inference(resolution,[],[f16392,f462]) ).
tff(f16637,plain,
( mem2(sF26,sF32)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f16618,f460]) ).
tff(f16856,plain,
( ~ mem2(sK22,sF32)
| ( tb2t(nil(char)) = sF26 ) ),
inference(resolution,[],[f16637,f340]) ).
tff(f16917,plain,
( ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32)
| ( epsilon1 = char3(sK19(sF26,epsilon1)) )
| sP3(sF26,epsilon1)
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(resolution,[],[f16616,f342]) ).
tff(f16920,plain,
( ( tb2t(nil(char)) = sF26 )
| mem2(sK22,sF32)
| ( epsilon1 = char3(sK19(sF26,epsilon1)) )
| sP3(sF26,epsilon1)
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1) ),
inference(duplicate_literal_removal,[],[f16917]) ).
tff(f16926,plain,
( ( tb2t(nil(char)) = sF26 )
| ( epsilon1 = char3(sK19(sF26,epsilon1)) )
| sP3(sF26,epsilon1)
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1) ),
inference(forward_subsumption_resolution,[],[f16920,f16856]) ).
tff(f16929,plain,
( sP3(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1) ),
inference(forward_subsumption_resolution,[],[f16926,f208]) ).
tff(f16966,plain,
( ( tb2t(nil(char)) = sF26 )
| sP2(sF26,epsilon1)
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( epsilon1 = alt1(sK7(sF26,epsilon1),sK8(sF26,epsilon1)) ) ),
inference(resolution,[],[f16929,f271]) ).
tff(f16968,plain,
( sP2(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1) ),
inference(forward_subsumption_resolution,[],[f16966,f209]) ).
tff(f17044,plain,
( ( tb2t(nil(char)) = sF26 )
| sP1(sF26,epsilon1)
| sP0(sF26,epsilon1)
| ( epsilon1 = alt1(sK10(sF26,epsilon1),sK11(sF26,epsilon1)) ) ),
inference(resolution,[],[f16968,f274]) ).
tff(f17046,plain,
( sP1(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 )
| sP0(sF26,epsilon1) ),
inference(forward_subsumption_resolution,[],[f17044,f209]) ).
tff(f17123,plain,
( ( tb2t(nil(char)) = sF26 )
| sP0(sF26,epsilon1)
| ( epsilon1 = concat1(sK14(sF26,epsilon1),sK15(sF26,epsilon1)) ) ),
inference(resolution,[],[f17046,f277]) ).
tff(f17124,plain,
( sP0(sF26,epsilon1)
| ( tb2t(nil(char)) = sF26 ) ),
inference(forward_subsumption_resolution,[],[f17123,f210]) ).
tff(f17174,plain,
( ( tb2t(nil(char)) = sF26 )
| ( epsilon1 = star1(sK18(sF26,epsilon1)) ) ),
inference(resolution,[],[f17124,f281]) ).
tff(f17175,plain,
tb2t(nil(char)) = sF26,
inference(forward_subsumption_resolution,[],[f17174,f211]) ).
tff(f17231,plain,
nil(char) = t2tb(sF26),
inference(superposition,[],[f260,f17175]) ).
tff(f17232,plain,
nil(char) = sF25,
inference(forward_demodulation,[],[f17231,f364]) ).
tff(f17234,plain,
$false,
inference(forward_subsumption_resolution,[],[f17232,f428]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW586_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:25:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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.84/0.80 % (3656046)Will run a generic schedule for satisfiability detection.
% 3.84/0.80 % (3656053)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3116389437:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.84/0.80 % (3656052)% WARNING: option uhcvi not known.
% 3.84/0.80 % (3656051)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2853023472_2999 on theBenchmark for (2999ds/0Mi)
% 3.84/0.80 % (3656052)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2071722825:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.84/0.80 % (3656054)dis+10_1_sil=32000:sp=arity:random_seed=3819459432:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.84/0.80 % (3656055)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1721717292:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.84/0.80 % (3656056)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3533802254:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.84/0.80 % (3656057)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=337372184:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.84/0.80 % (3656051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.84/0.80 % (3656051)Terminated due to inappropriate strategy.
% 3.84/0.80 % (3656051)------------------------------
% 3.84/0.80 % (3656051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.80 % (3656051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.80 % (3656051)CaDiCaL version: 2.1.3
% 3.84/0.80 % (3656051)Termination reason: Inappropriate
% 3.84/0.80 % (3656051)Time elapsed: 0.004 s
% 3.84/0.80 % (3656051)Peak memory usage: 11 MB
% 3.84/0.80 % (3656051)Instructions burned: 8 (million)
% 3.84/0.80 % (3656051)------------------------------
% 3.84/0.80 % (3656051)------------------------------
% 3.84/0.80 % (3656065)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=712116892:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.84/0.80 % (3656065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.84/0.80 % (3656065)Terminated due to inappropriate strategy.
% 3.84/0.80 % (3656065)------------------------------
% 3.84/0.80 % (3656065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.80 % (3656065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.80 % (3656065)CaDiCaL version: 2.1.3
% 3.84/0.80 % (3656065)Termination reason: Inappropriate
% 3.84/0.80 % (3656065)Time elapsed: 0.003 s
% 3.84/0.80 % (3656065)Peak memory usage: 10 MB
% 3.84/0.80 % (3656065)Instructions burned: 7 (million)
% 3.84/0.80 % (3656065)------------------------------
% 3.84/0.80 % (3656065)------------------------------
% 3.84/0.80 % (3656067)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=322846365:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.84/0.80 % (3656054)Instruction limit reached!
% 3.84/0.80 % (3656054)------------------------------
% 3.84/0.80 % (3656054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.80 % (3656054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.80 % (3656054)CaDiCaL version: 2.1.3
% 3.84/0.80 % (3656054)Termination reason: Instruction limit
% 3.84/0.80 % (3656054)Termination phase: Saturation
% 3.84/0.80 % (3656054)Time elapsed: 0.061 s
% 3.84/0.80 % (3656054)Peak memory usage: 12 MB
% 3.84/0.80 % (3656054)Instructions burned: 104 (million)
% 3.84/0.80 % (3656056)Instruction limit reached!
% 3.84/0.80 % (3656056)------------------------------
% 3.84/0.80 % (3656056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.80 % (3656056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.80 % (3656056)CaDiCaL version: 2.1.3
% 3.84/0.80 % (3656056)Termination reason: Instruction limit
% 3.84/0.80 % (3656056)Termination phase: Saturation
% 3.84/0.80 % (3656056)Time elapsed: 0.071 s
% 3.84/0.80 % (3656056)Peak memory usage: 13 MB
% 3.84/0.80 % (3656056)Instructions burned: 132 (million)
% 3.84/0.80 % (3656055)Instruction limit reached!
% 3.84/0.80 % (3656055)------------------------------
% 3.84/0.80 % (3656055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.80 % (3656055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.80 % (3656055)CaDiCaL version: 2.1.3
% 3.84/0.80 % (3656055)Termination reason: Instruction limit
% 5.70/1.08 % (3656055)Termination phase: Saturation
% 5.70/1.08 % (3656055)Time elapsed: 0.072 s
% 5.70/1.08 % (3656055)Peak memory usage: 13 MB
% 5.70/1.08 % (3656055)Instructions burned: 118 (million)
% 5.70/1.08 % (3656069)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=1505569498:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.70/1.08 % (3656057)Instruction limit reached!
% 5.70/1.08 % (3656057)------------------------------
% 5.70/1.08 % (3656057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.08 % (3656057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.08 % (3656057)CaDiCaL version: 2.1.3
% 5.70/1.08 % (3656057)Termination reason: Instruction limit
% 5.70/1.08 % (3656057)Termination phase: Saturation
% 5.70/1.08 % (3656057)Time elapsed: 0.088 s
% 5.70/1.08 % (3656057)Peak memory usage: 13 MB
% 5.70/1.08 % (3656057)Instructions burned: 160 (million)
% 5.70/1.08 % (3656070)ott-21_1_sil=16000:fs=off:random_seed=666139565:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.70/1.08 % (3656071)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1704031482:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.70/1.08 % (3656073)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1656511553:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.70/1.08 % (3656073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.70/1.08 % (3656073)Terminated due to inappropriate strategy.
% 5.70/1.08 % (3656073)------------------------------
% 5.70/1.08 % (3656073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.08 % (3656073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.08 % (3656073)CaDiCaL version: 2.1.3
% 5.70/1.08 % (3656073)Termination reason: Inappropriate
% 5.70/1.08 % (3656073)Time elapsed: 0.003 s
% 5.70/1.08 % (3656073)Peak memory usage: 10 MB
% 5.70/1.08 % (3656073)Instructions burned: 5 (million)
% 5.70/1.08 % (3656073)------------------------------
% 5.70/1.08 % (3656073)------------------------------
% 5.70/1.08 % (3656077)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2741677448:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.70/1.08 % (3656067)Instruction limit reached!
% 5.70/1.08 % (3656067)------------------------------
% 5.70/1.08 % (3656067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.08 % (3656067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.08 % (3656067)CaDiCaL version: 2.1.3
% 5.70/1.08 % (3656067)Termination reason: Instruction limit
% 5.70/1.08 % (3656067)Termination phase: Saturation
% 5.70/1.08 % (3656067)Time elapsed: 0.085 s
% 5.70/1.08 % (3656067)Peak memory usage: 13 MB
% 5.70/1.08 % (3656067)Instructions burned: 133 (million)
% 5.70/1.08 % (3656079)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2493545299:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.70/1.08 % (3656079)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.70/1.08 % (3656079)Terminated due to inappropriate strategy.
% 5.70/1.08 % (3656079)------------------------------
% 5.70/1.08 % (3656079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.08 % (3656079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.08 % (3656079)CaDiCaL version: 2.1.3
% 5.70/1.08 % (3656079)Termination reason: Inappropriate
% 5.70/1.08 % (3656079)Time elapsed: 0.004 s
% 5.70/1.08 % (3656079)Peak memory usage: 10 MB
% 5.70/1.08 % (3656079)Instructions burned: 7 (million)
% 5.70/1.08 % (3656079)------------------------------
% 5.70/1.08 % (3656079)------------------------------
% 5.70/1.08 % (3656081)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=1050060880: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)
% 5.70/1.08 % (3656070)Instruction limit reached!
% 5.70/1.08 % (3656070)------------------------------
% 5.70/1.08 % (3656070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.08 % (3656070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.08 % (3656070)CaDiCaL version: 2.1.3
% 5.70/1.08 % (3656070)Termination reason: Instruction limit
% 5.70/1.08 % (3656070)Termination phase: Saturation
% 8.38/1.55 % (3656070)Time elapsed: 0.093 s
% 8.38/1.55 % (3656070)Peak memory usage: 13 MB
% 8.38/1.55 % (3656070)Instructions burned: 182 (million)
% 8.38/1.55 % (3656083)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=308913065:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 8.38/1.55 % (3656069)Instruction limit reached!
% 8.38/1.55 % (3656069)------------------------------
% 8.38/1.55 % (3656069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656071)Instruction limit reached!
% 8.38/1.55 % (3656071)------------------------------
% 8.38/1.55 % (3656071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656069)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656071)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656069)Termination reason: Instruction limit
% 8.38/1.55 % (3656069)Termination phase: Saturation
% 8.38/1.55 % (3656069)Time elapsed: 0.317 s
% 8.38/1.55 % (3656071)Termination reason: Instruction limit
% 8.38/1.55 % (3656071)Termination phase: Saturation
% 8.38/1.55 % (3656069)Peak memory usage: 14 MB
% 8.38/1.55 % (3656071)Time elapsed: 0.307 s
% 8.38/1.55 % (3656069)Instructions burned: 685 (million)
% 8.38/1.55 % (3656071)Peak memory usage: 14 MB
% 8.38/1.55 % (3656071)Instructions burned: 478 (million)
% 8.38/1.55 % (3656085)fmb+10_1_sil=64000:random_seed=525259020:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 8.38/1.55 % (3656086)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3713022340:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 8.38/1.55 % (3656086)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/1.55 % (3656086)Terminated due to inappropriate strategy.
% 8.38/1.55 % (3656086)------------------------------
% 8.38/1.55 % (3656086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656086)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656086)Termination reason: Inappropriate
% 8.38/1.55 % (3656086)Time elapsed: 0.003 s
% 8.38/1.55 % (3656086)Peak memory usage: 10 MB
% 8.38/1.55 % (3656086)Instructions burned: 7 (million)
% 8.38/1.55 % (3656085)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/1.55 % (3656085)Terminated due to inappropriate strategy.
% 8.38/1.55 % (3656085)------------------------------
% 8.38/1.55 % (3656085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656085)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656085)Termination reason: Inappropriate
% 8.38/1.55 % (3656085)Time elapsed: 0.004 s
% 8.38/1.55 % (3656085)Peak memory usage: 10 MB
% 8.38/1.55 % (3656085)Instructions burned: 7 (million)
% 8.38/1.55 % (3656086)------------------------------
% 8.38/1.55 % (3656086)------------------------------
% 8.38/1.55 % (3656085)------------------------------
% 8.38/1.55 % (3656085)------------------------------
% 8.38/1.55 % (3656089)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=868651452:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 8.38/1.55 % (3656090)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=700496209:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 8.38/1.55 % (3656089)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/1.55 % (3656089)Terminated due to inappropriate strategy.
% 8.38/1.55 % (3656089)------------------------------
% 8.38/1.55 % (3656089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656089)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656089)Termination reason: Inappropriate
% 8.38/1.55 % (3656089)Time elapsed: 0.003 s
% 8.38/1.55 % (3656089)Peak memory usage: 10 MB
% 8.38/1.55 % (3656089)Instructions burned: 7 (million)
% 8.38/1.55 % (3656089)------------------------------
% 8.38/1.55 % (3656089)------------------------------
% 8.38/1.55 % (3656093)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2814524546:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 8.38/1.55 % (3656081)Instruction limit reached!
% 8.38/1.55 % (3656081)------------------------------
% 8.38/1.55 % (3656081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656081)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656081)Termination reason: Instruction limit
% 8.38/1.55 % (3656081)Termination phase: Saturation
% 8.38/1.55 % (3656081)Time elapsed: 0.363 s
% 8.38/1.55 % (3656081)Peak memory usage: 15 MB
% 8.38/1.55 % (3656081)Instructions burned: 693 (million)
% 8.38/1.55 % (3656095)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1694940291:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 8.38/1.55 % (3656095)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/1.55 % (3656095)Terminated due to inappropriate strategy.
% 8.38/1.55 % (3656095)------------------------------
% 8.38/1.55 % (3656095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656095)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656095)Termination reason: Inappropriate
% 8.38/1.55 % (3656095)Time elapsed: 0.004 s
% 8.38/1.55 % (3656095)Peak memory usage: 11 MB
% 8.38/1.55 % (3656095)Instructions burned: 8 (million)
% 8.38/1.55 % (3656095)------------------------------
% 8.38/1.55 % (3656095)------------------------------
% 8.38/1.55 % (3656097)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2162188556:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 8.38/1.55 % (3656097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/1.55 % (3656097)Terminated due to inappropriate strategy.
% 8.38/1.55 % (3656097)------------------------------
% 8.38/1.55 % (3656097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656097)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656097)Termination reason: Inappropriate
% 8.38/1.55 % (3656097)Time elapsed: 0.004 s
% 8.38/1.55 % (3656097)Peak memory usage: 10 MB
% 8.38/1.55 % (3656097)Instructions burned: 7 (million)
% 8.38/1.55 % (3656097)------------------------------
% 8.38/1.55 % (3656097)------------------------------
% 8.38/1.55 % (3656099)ott-2_1_sil=16000:newcnf=on:random_seed=1566648023:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 8.38/1.55 % (3656083)Instruction limit reached!
% 8.38/1.55 % (3656083)------------------------------
% 8.38/1.55 % (3656083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656083)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656083)Termination reason: Instruction limit
% 8.38/1.55 % (3656083)Termination phase: Saturation
% 8.38/1.55 % (3656083)Time elapsed: 0.505 s
% 8.38/1.55 % (3656083)Peak memory usage: 18 MB
% 8.38/1.55 % (3656083)Instructions burned: 880 (million)
% 8.38/1.55 % (3656101)ott+10_1_sil=32000:tgt=ground:random_seed=2264419111:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 8.38/1.55 % (3656077)Instruction limit reached!
% 8.38/1.55 % (3656077)------------------------------
% 8.38/1.55 % (3656077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656077)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656077)Termination reason: Instruction limit
% 8.38/1.55 % (3656077)Termination phase: Saturation
% 8.38/1.55 % (3656077)Time elapsed: 0.658 s
% 8.38/1.55 % (3656077)Peak memory usage: 21 MB
% 8.38/1.55 % (3656077)Instructions burned: 1180 (million)
% 8.38/1.55 % (3656103)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1422748216:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 8.38/1.55 % (3656103)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/1.55 % (3656103)Terminated due to inappropriate strategy.
% 8.38/1.55 % (3656103)------------------------------
% 8.38/1.55 % (3656103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656103)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656103)Termination reason: Inappropriate
% 8.38/1.55 % (3656103)Time elapsed: 0.004 s
% 8.38/1.55 % (3656103)Peak memory usage: 11 MB
% 8.38/1.55 % (3656103)Instructions burned: 8 (million)
% 8.38/1.55 % (3656103)------------------------------
% 8.38/1.55 % (3656103)------------------------------
% 8.38/1.55 % (3656105)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2067242492:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 8.38/1.55 % (3656099)Instruction limit reached!
% 8.38/1.55 % (3656099)------------------------------
% 8.38/1.55 % (3656099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656099)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656099)Termination reason: Instruction limit
% 8.38/1.55 % (3656099)Termination phase: Saturation
% 8.38/1.55 % (3656099)Time elapsed: 0.462 s
% 8.38/1.55 % (3656099)Peak memory usage: 16 MB
% 8.38/1.55 % (3656099)Instructions burned: 870 (million)
% 8.38/1.55 % (3656107)dis+21_1_sil=32000:sas=cadical:random_seed=4070061741:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 8.38/1.55 % (3656093)Instruction limit reached!
% 8.38/1.55 % (3656093)------------------------------
% 8.38/1.55 % (3656093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656093)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656093)Termination reason: Instruction limit
% 8.38/1.55 % (3656093)Termination phase: Saturation
% 8.38/1.55 % (3656093)Time elapsed: 0.731 s
% 8.38/1.55 % (3656093)Peak memory usage: 26 MB
% 8.38/1.55 % (3656093)Instructions burned: 1473 (million)
% 8.38/1.55 % (3656109)ott+11_1_sil=16000:gs=on:random_seed=211968131:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 8.38/1.55 % (3656101) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3656046-3656101"...
% 8.38/1.55 % (3656101)...printing done.
% 8.38/1.55 % (3656101)Refutation found. Thanks to Tanya!
% 8.38/1.55 % SZS status Theorem for theBenchmark
% 8.38/1.55 % SZS output start Proof for theBenchmark
% See solution above
% 8.38/1.55 % (3656101)------------------------------
% 8.38/1.55 % (3656101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/1.55 % (3656101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/1.55 % (3656101)CaDiCaL version: 2.1.3
% 8.38/1.55 % (3656101)Termination reason: Refutation
% 8.38/1.55 % (3656101)Time elapsed: 0.547 s
% 8.38/1.55 % (3656101)Peak memory usage: 17 MB
% 8.38/1.55 % (3656101)Instructions burned: 998 (million)
% 8.38/1.55 % (3656046)Success in time 1.323 s
% 8.38/1.55 % Vampire exiting
%------------------------------------------------------------------------------