%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW648_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 : n011.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:02 PM UTC 2026
% Result : Theorem 2.25s 0.83s
% Output : Refutation 3.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 18
% Syntax : Number of formulae : 90 ( 30 unt; 0 typ; 8 def)
% Number of atoms : 270 ( 173 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 314 ( 134 ~; 96 |; 56 &)
% ( 8 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 47 ( 16 atm; 15 fun; 16 num; 0 var)
% Number of types : 10 ( 8 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 10 usr; 9 prp; 0-3 aty)
% Number of functors : 47 ( 44 usr; 20 con; 0-5 aty)
% Number of variables : 171 ( 136 !; 35 ?; 171 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
a: $tType ).
tff(type_def_10,type,
list_lpa1cm_a1rp: $tType ).
tff(type_def_11,type,
lpa1cm_a1rp: $tType ).
tff(type_def_12,type,
list_a1: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
list: ty > ty ).
tff(func_def_13,type,
nil: ty > uni ).
tff(func_def_14,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_18,type,
length: ( ty * uni ) > $int ).
tff(func_def_21,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_22,type,
reverse: ( ty * uni ) > uni ).
tff(func_def_23,type,
tuple2: ( ty * ty ) > ty ).
tff(func_def_24,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(func_def_25,type,
tuple2_proj_1: ( ty * ty * uni ) > uni ).
tff(func_def_26,type,
tuple2_proj_2: ( ty * ty * uni ) > uni ).
tff(func_def_27,type,
combine: ( ty * ty * uni * uni ) > uni ).
tff(func_def_28,type,
a1: ty ).
tff(func_def_29,type,
t2tb: a > uni ).
tff(func_def_30,type,
tb2t: uni > a ).
tff(func_def_31,type,
t2tb1: list_lpa1cm_a1rp > uni ).
tff(func_def_32,type,
tb2t1: uni > list_lpa1cm_a1rp ).
tff(func_def_33,type,
t2tb2: lpa1cm_a1rp > uni ).
tff(func_def_34,type,
tb2t2: uni > lpa1cm_a1rp ).
tff(func_def_35,type,
t2tb3: list_a1 > uni ).
tff(func_def_36,type,
tb2t3: uni > list_a1 ).
tff(func_def_37,type,
sK0: ( uni * uni * ty ) > uni ).
tff(func_def_38,type,
sK1: ( uni * uni * ty ) > uni ).
tff(func_def_39,type,
sK2: list_a1 ).
tff(func_def_40,type,
sK3: list_a1 ).
tff(func_def_41,type,
sK4: list_a1 ).
tff(func_def_42,type,
sK5: a ).
tff(func_def_43,type,
sK6: list_a1 ).
tff(func_def_44,type,
sK7: list_lpa1cm_a1rp ).
tff(func_def_45,type,
sK8: a ).
tff(func_def_46,type,
sK9: list_a1 ).
tff(func_def_47,type,
sK10: list_a1 ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(f20,axiom,
! [X0: ty] :
( ( length(X0,nil(X0)) = 0 )
& ! [X1: uni,X2: uni] : ( length(X0,cons(X0,X1,X2)) = $sum(1,length(X0,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_def) ).
tff(f24,axiom,
! [X1: uni,X0: ty] :
( ( infix_plpl(X0,nil(X0),X1) = X1 )
& ! [X3: uni,X2: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(f25,axiom,
! [X3: uni,X1: uni,X0: ty,X2: uni] : ( infix_plpl(X0,X1,infix_plpl(X0,X2,X3)) = infix_plpl(X0,infix_plpl(X0,X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',append_assoc) ).
tff(f32,axiom,
! [X0: ty] :
( ( reverse(X0,nil(X0)) = nil(X0) )
& ! [X2: uni,X1: uni] : ( reverse(X0,cons(X0,X1,X2)) = infix_plpl(X0,reverse(X0,X2),cons(X0,X1,nil(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reverse_def) ).
tff(f35,axiom,
! [X0: ty,X1: uni] : ( reverse(X0,reverse(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reverse_reverse) ).
tff(f37,axiom,
! [X1: uni,X0: ty] : ( length(X0,reverse(X0,X1)) = length(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reverse_length) ).
tff(f45,axiom,
! [X1: ty,X2: uni,X0: ty] :
( ( combine(X1,X0,X2,nil(X1)) = nil(tuple2(X0,X1)) )
& ! [X3: uni,X4: uni] :
( ! [X5: uni,X6: uni] : ( combine(X1,X0,cons(X0,X5,X6),cons(X1,X3,X4)) = cons(tuple2(X0,X1),tuple21(X0,X1,X5,X3),combine(X1,X0,X6,X4)) )
& ( combine(X1,X0,nil(X0),cons(X1,X3,X4)) = nil(tuple2(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',combine_def) ).
tff(f51,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f57,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f58,conjecture,
! [X1: list_a1,X0: list_a1] :
( $lesseq(length(a1,t2tb3(X0)),length(a1,t2tb3(X1)))
=> ! [X3: list_a1,X2: a] :
( ( X0 = tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) )
=> ( $lesseq(length(a1,t2tb3(X3)),length(a1,t2tb3(X1)))
=> ! [X5: list_a1,X4: list_lpa1cm_a1rp] :
( ? [X6: list_a1] :
( ( X4 = tb2t1(combine(a1,a1,t2tb3(X3),reverse(a1,t2tb3(X6)))) )
& ( X1 = tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X5))) )
& ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X3)) ) )
=> ! [X8: list_a1,X7: a] :
( ( X5 = tb2t3(cons(a1,t2tb(X7),t2tb3(X8))) )
=> ? [X6: list_a1] :
( ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X0)) )
& ( tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X2),t2tb(X7)),t2tb1(X4))) = tb2t1(combine(a1,a1,t2tb3(X0),reverse(a1,t2tb3(X6)))) )
& ( X1 = tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X8))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_convolution_rec) ).
tff(f59,negated_conjecture,
~ ! [X1: list_a1,X0: list_a1] :
( $lesseq(length(a1,t2tb3(X0)),length(a1,t2tb3(X1)))
=> ! [X3: list_a1,X2: a] :
( ( X0 = tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) )
=> ( $lesseq(length(a1,t2tb3(X3)),length(a1,t2tb3(X1)))
=> ! [X5: list_a1,X4: list_lpa1cm_a1rp] :
( ? [X6: list_a1] :
( ( X4 = tb2t1(combine(a1,a1,t2tb3(X3),reverse(a1,t2tb3(X6)))) )
& ( X1 = tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X5))) )
& ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X3)) ) )
=> ! [X8: list_a1,X7: a] :
( ( X5 = tb2t3(cons(a1,t2tb(X7),t2tb3(X8))) )
=> ? [X6: list_a1] :
( ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X0)) )
& ( tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X2),t2tb(X7)),t2tb1(X4))) = tb2t1(combine(a1,a1,t2tb3(X0),reverse(a1,t2tb3(X6)))) )
& ( X1 = tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X8))) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
tff(f60,plain,
~ ! [X1: list_a1,X0: list_a1] :
( ~ $less(length(a1,t2tb3(X1)),length(a1,t2tb3(X0)))
=> ! [X3: list_a1,X2: a] :
( ( X0 = tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) )
=> ( ~ $less(length(a1,t2tb3(X1)),length(a1,t2tb3(X3)))
=> ! [X5: list_a1,X4: list_lpa1cm_a1rp] :
( ? [X6: list_a1] :
( ( X4 = tb2t1(combine(a1,a1,t2tb3(X3),reverse(a1,t2tb3(X6)))) )
& ( X1 = tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X5))) )
& ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X3)) ) )
=> ! [X8: list_a1,X7: a] :
( ( X5 = tb2t3(cons(a1,t2tb(X7),t2tb3(X8))) )
=> ? [X6: list_a1] :
( ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X0)) )
& ( tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X2),t2tb(X7)),t2tb1(X4))) = tb2t1(combine(a1,a1,t2tb3(X0),reverse(a1,t2tb3(X6)))) )
& ( X1 = tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X8))) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f59]) ).
tff(f67,plain,
~ ! [X1: list_a1,X0: list_a1] :
( ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X1)))
=> ! [X2: list_a1,X3: a] :
( ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X1 )
=> ( ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X2)))
=> ! [X5: list_lpa1cm_a1rp,X4: list_a1] :
( ? [X6: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(X2),reverse(a1,t2tb3(X6)))) = X5 )
& ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X2)) )
& ( tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X4))) = X0 ) )
=> ! [X8: a,X7: list_a1] :
( ( tb2t3(cons(a1,t2tb(X8),t2tb3(X7))) = X4 )
=> ? [X9: list_a1] :
( ( tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X7))) = X0 )
& ( length(a1,t2tb3(X1)) = length(a1,t2tb3(X9)) )
& ( tb2t1(combine(a1,a1,t2tb3(X1),reverse(a1,t2tb3(X9)))) = tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X3),t2tb(X8)),t2tb1(X5))) ) ) ) ) ) ) ),
inference(rectify,[],[f60]) ).
tff(f68,plain,
! [X0: ty,X2: ty,X1: uni] :
( ( combine(X0,X2,X1,nil(X0)) = nil(tuple2(X2,X0)) )
& ! [X4: uni,X3: uni] :
( ! [X5: uni,X6: uni] : ( cons(tuple2(X2,X0),tuple21(X2,X0,X5,X3),combine(X0,X2,X6,X4)) = combine(X0,X2,cons(X2,X5,X6),cons(X0,X3,X4)) )
& ( combine(X0,X2,nil(X2),cons(X0,X3,X4)) = nil(tuple2(X2,X0)) ) ) ),
inference(rectify,[],[f45]) ).
tff(f79,plain,
! [X1: ty,X0: uni] :
( ( infix_plpl(X1,nil(X1),X0) = X0 )
& ! [X3: uni,X2: uni] : ( infix_plpl(X1,cons(X1,X3,X2),X0) = cons(X1,X3,infix_plpl(X1,X2,X0)) ) ),
inference(rectify,[],[f24]) ).
tff(f83,plain,
! [X1: ty,X0: uni] : ( length(X1,reverse(X1,X0)) = length(X1,X0) ),
inference(rectify,[],[f37]) ).
tff(f91,plain,
! [X2: ty,X0: uni,X3: uni,X1: uni] : ( infix_plpl(X2,X1,infix_plpl(X2,X3,X0)) = infix_plpl(X2,infix_plpl(X2,X1,X3),X0) ),
inference(rectify,[],[f25]) ).
tff(f99,plain,
? [X1: list_a1,X0: list_a1] :
( ? [X2: list_a1,X3: a] :
( ? [X4: list_a1,X5: list_lpa1cm_a1rp] :
( ? [X8: a,X7: list_a1] :
( ! [X9: list_a1] :
( ( length(a1,t2tb3(X1)) != length(a1,t2tb3(X9)) )
| ( tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X7))) != X0 )
| ( tb2t1(combine(a1,a1,t2tb3(X1),reverse(a1,t2tb3(X9)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X3),t2tb(X8)),t2tb1(X5))) ) )
& ( tb2t3(cons(a1,t2tb(X8),t2tb3(X7))) = X4 ) )
& ? [X6: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(X2),reverse(a1,t2tb3(X6)))) = X5 )
& ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X2)) )
& ( tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X4))) = X0 ) ) )
& ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X2)))
& ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X1 ) )
& ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X1))) ),
inference(ennf_transformation,[],[f67]) ).
tff(f100,plain,
? [X0: list_a1,X1: list_a1] :
( ? [X2: list_a1,X3: a] :
( ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X2)))
& ? [X4: list_a1,X5: list_lpa1cm_a1rp] :
( ? [X8: a,X7: list_a1] :
( ! [X9: list_a1] :
( ( length(a1,t2tb3(X1)) != length(a1,t2tb3(X9)) )
| ( tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X7))) != X0 )
| ( tb2t1(combine(a1,a1,t2tb3(X1),reverse(a1,t2tb3(X9)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X3),t2tb(X8)),t2tb1(X5))) ) )
& ( tb2t3(cons(a1,t2tb(X8),t2tb3(X7))) = X4 ) )
& ? [X6: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(X2),reverse(a1,t2tb3(X6)))) = X5 )
& ( length(a1,t2tb3(X6)) = length(a1,t2tb3(X2)) )
& ( tb2t3(infix_plpl(a1,t2tb3(X6),t2tb3(X4))) = X0 ) ) )
& ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X1 ) )
& ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X1))) ),
inference(flattening,[],[f99]) ).
tff(f123,plain,
! [X0: ty,X1: uni] : ( length(X0,X1) = length(X0,reverse(X0,X1)) ),
inference(rectify,[],[f83]) ).
tff(f125,plain,
! [X0: ty] :
( ( reverse(X0,nil(X0)) = nil(X0) )
& ! [X1: uni,X2: uni] : ( reverse(X0,cons(X0,X2,X1)) = infix_plpl(X0,reverse(X0,X1),cons(X0,X2,nil(X0))) ) ),
inference(rectify,[],[f32]) ).
tff(f126,plain,
! [X0: ty,X1: ty,X2: uni] :
( ( nil(tuple2(X1,X0)) = combine(X0,X1,X2,nil(X0)) )
& ! [X3: uni,X4: uni] :
( ! [X5: uni,X6: uni] : ( cons(tuple2(X1,X0),tuple21(X1,X0,X5,X4),combine(X0,X1,X6,X3)) = combine(X0,X1,cons(X1,X5,X6),cons(X0,X4,X3)) )
& ( nil(tuple2(X1,X0)) = combine(X0,X1,nil(X1),cons(X0,X4,X3)) ) ) ),
inference(rectify,[],[f68]) ).
tff(f139,plain,
? [X0: list_a1,X1: list_a1] :
( ? [X2: list_a1,X3: a] :
( ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X2)))
& ? [X4: list_a1,X5: list_lpa1cm_a1rp] :
( ? [X6: a,X7: list_a1] :
( ! [X8: list_a1] :
( ( length(a1,t2tb3(X1)) != length(a1,t2tb3(X8)) )
| ( tb2t3(infix_plpl(a1,t2tb3(X8),t2tb3(X7))) != X0 )
| ( tb2t1(combine(a1,a1,t2tb3(X1),reverse(a1,t2tb3(X8)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(X3),t2tb(X6)),t2tb1(X5))) ) )
& ( tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) = X4 ) )
& ? [X9: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(X2),reverse(a1,t2tb3(X9)))) = X5 )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X2)) )
& ( tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X4))) = X0 ) ) )
& ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X1 ) )
& ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X1))) ),
inference(rectify,[],[f100]) ).
tff(f140,plain,
( ~ $less(length(a1,t2tb3(sK2)),length(a1,t2tb3(sK4)))
& ! [X8: list_a1] :
( ( length(a1,t2tb3(sK3)) != length(a1,t2tb3(X8)) )
| ( sK2 != tb2t3(infix_plpl(a1,t2tb3(X8),t2tb3(sK9))) )
| ( tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,t2tb3(X8)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(sK5),t2tb(sK8)),t2tb1(sK7))) ) )
& ( tb2t3(cons(a1,t2tb(sK8),t2tb3(sK9))) = sK6 )
& ( tb2t1(combine(a1,a1,t2tb3(sK4),reverse(a1,t2tb3(sK10)))) = sK7 )
& ( length(a1,t2tb3(sK10)) = length(a1,t2tb3(sK4)) )
& ( sK2 = tb2t3(infix_plpl(a1,t2tb3(sK10),t2tb3(sK6))) )
& ( tb2t3(cons(a1,t2tb(sK5),t2tb3(sK4))) = sK3 )
& ~ $less(length(a1,t2tb3(sK2)),length(a1,t2tb3(sK3))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X9,sK10)],[f139]) ).
tff(f149,plain,
! [X0: ty,X1: uni] :
( ( infix_plpl(X0,nil(X0),X1) = X1 )
& ! [X2: uni,X3: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ) ),
inference(rectify,[],[f79]) ).
tff(f153,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] : ( infix_plpl(X0,X3,infix_plpl(X0,X2,X1)) = infix_plpl(X0,infix_plpl(X0,X3,X2),X1) ),
inference(rectify,[],[f91]) ).
tff(f167,plain,
! [X0: ty,X1: uni] : ( length(X0,X1) = length(X0,reverse(X0,X1)) ),
inference(cnf_transformation,[],[f123]) ).
tff(f169,plain,
! [X2: uni,X0: ty,X1: uni] : ( reverse(X0,cons(X0,X2,X1)) = infix_plpl(X0,reverse(X0,X1),cons(X0,X2,nil(X0))) ),
inference(cnf_transformation,[],[f125]) ).
tff(f174,plain,
! [X3: uni,X0: ty,X1: ty,X6: uni,X4: uni,X5: uni] : ( cons(tuple2(X1,X0),tuple21(X1,X0,X5,X4),combine(X0,X1,X6,X3)) = combine(X0,X1,cons(X1,X5,X6),cons(X0,X4,X3)) ),
inference(cnf_transformation,[],[f126]) ).
tff(f180,plain,
! [X0: ty,X1: uni] : ( reverse(X0,reverse(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f35]) ).
tff(f188,plain,
! [X2: uni,X0: ty,X1: uni] : ( length(X0,cons(X0,X1,X2)) = $sum(1,length(X0,X2)) ),
inference(cnf_transformation,[],[f20]) ).
tff(f195,plain,
tb2t3(cons(a1,t2tb(sK5),t2tb3(sK4))) = sK3,
inference(cnf_transformation,[],[f140]) ).
tff(f196,plain,
sK2 = tb2t3(infix_plpl(a1,t2tb3(sK10),t2tb3(sK6))),
inference(cnf_transformation,[],[f140]) ).
tff(f197,plain,
length(a1,t2tb3(sK10)) = length(a1,t2tb3(sK4)),
inference(cnf_transformation,[],[f140]) ).
tff(f198,plain,
tb2t1(combine(a1,a1,t2tb3(sK4),reverse(a1,t2tb3(sK10)))) = sK7,
inference(cnf_transformation,[],[f140]) ).
tff(f199,plain,
tb2t3(cons(a1,t2tb(sK8),t2tb3(sK9))) = sK6,
inference(cnf_transformation,[],[f140]) ).
tff(f200,plain,
! [X8: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,t2tb3(X8)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(sK5),t2tb(sK8)),t2tb1(sK7))) )
| ( length(a1,t2tb3(sK3)) != length(a1,t2tb3(X8)) )
| ( sK2 != tb2t3(infix_plpl(a1,t2tb3(X8),t2tb3(sK9))) ) ),
inference(cnf_transformation,[],[f140]) ).
tff(f203,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f57]) ).
tff(f215,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ),
inference(cnf_transformation,[],[f149]) ).
tff(f216,plain,
! [X0: ty,X1: uni] : ( infix_plpl(X0,nil(X0),X1) = X1 ),
inference(cnf_transformation,[],[f149]) ).
tff(f226,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( infix_plpl(X0,X3,infix_plpl(X0,X2,X1)) = infix_plpl(X0,infix_plpl(X0,X3,X2),X1) ),
inference(cnf_transformation,[],[f153]) ).
tff(f229,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f51]) ).
tff(f238,definition,
( spl11_1
<=> ( sK2 = tb2t3(infix_plpl(a1,t2tb3(sK10),t2tb3(sK6))) ) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
tff(f240,plain,
( ( sK2 = tb2t3(infix_plpl(a1,t2tb3(sK10),t2tb3(sK6))) )
| ~ spl11_1 ),
inference(avatar_component_clause,[],[f238]) ).
tff(f241,plain,
spl11_1,
inference(avatar_split_clause,[],[f196,f238]) ).
tff(f243,definition,
( spl11_2
<=> ( tb2t3(cons(a1,t2tb(sK8),t2tb3(sK9))) = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
tff(f245,plain,
( ( tb2t3(cons(a1,t2tb(sK8),t2tb3(sK9))) = sK6 )
| ~ spl11_2 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f246,plain,
spl11_2,
inference(avatar_split_clause,[],[f199,f243]) ).
tff(f254,definition,
( spl11_4
<=> ( length(a1,t2tb3(sK10)) = length(a1,t2tb3(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl11_4])],[avatar_definition]) ).
tff(f256,plain,
( ( length(a1,t2tb3(sK10)) = length(a1,t2tb3(sK4)) )
| ~ spl11_4 ),
inference(avatar_component_clause,[],[f254]) ).
tff(f257,plain,
spl11_4,
inference(avatar_split_clause,[],[f197,f254]) ).
tff(f259,definition,
( spl11_5
<=> ( tb2t1(combine(a1,a1,t2tb3(sK4),reverse(a1,t2tb3(sK10)))) = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl11_5])],[avatar_definition]) ).
tff(f261,plain,
( ( tb2t1(combine(a1,a1,t2tb3(sK4),reverse(a1,t2tb3(sK10)))) = sK7 )
| ~ spl11_5 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f262,plain,
spl11_5,
inference(avatar_split_clause,[],[f198,f259]) ).
tff(f269,definition,
( spl11_7
<=> ( tb2t3(cons(a1,t2tb(sK5),t2tb3(sK4))) = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl11_7])],[avatar_definition]) ).
tff(f271,plain,
( ( tb2t3(cons(a1,t2tb(sK5),t2tb3(sK4))) = sK3 )
| ~ spl11_7 ),
inference(avatar_component_clause,[],[f269]) ).
tff(f272,plain,
spl11_7,
inference(avatar_split_clause,[],[f195,f269]) ).
tff(f283,plain,
( ! [X0: list_a1] :
( ( length(a1,t2tb3(X0)) != length(a1,t2tb3(sK3)) )
| ( tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,t2tb3(X0)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(sK5),t2tb(sK8)),t2tb1(tb2t1(combine(a1,a1,t2tb3(sK4),reverse(a1,t2tb3(sK10))))))) )
| ( sK2 != tb2t3(infix_plpl(a1,t2tb3(X0),t2tb3(sK9))) ) )
| ~ spl11_5 ),
inference(superposition,[],[f200,f261]) ).
tff(f284,plain,
( ! [X0: list_a1] :
( ( sK2 != tb2t3(infix_plpl(a1,t2tb3(X0),t2tb3(sK9))) )
| ( tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,t2tb3(X0)))) != tb2t1(cons(tuple2(a1,a1),tuple21(a1,a1,t2tb(sK5),t2tb(sK8)),combine(a1,a1,t2tb3(sK4),reverse(a1,t2tb3(sK10))))) )
| ( length(a1,t2tb3(X0)) != length(a1,t2tb3(sK3)) ) )
| ~ spl11_5 ),
inference(forward_demodulation,[],[f283,f229]) ).
tff(f285,plain,
( ! [X0: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,t2tb3(X0)))) != tb2t1(combine(a1,a1,cons(a1,t2tb(sK5),t2tb3(sK4)),cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10))))) )
| ( length(a1,t2tb3(X0)) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,t2tb3(X0),t2tb3(sK9))) ) )
| ~ spl11_5 ),
inference(forward_demodulation,[],[f284,f174]) ).
tff(f287,plain,
( ( cons(a1,t2tb(sK8),t2tb3(sK9)) = t2tb3(sK6) )
| ~ spl11_2 ),
inference(superposition,[],[f203,f245]) ).
tff(f288,plain,
( ( t2tb3(sK3) = cons(a1,t2tb(sK5),t2tb3(sK4)) )
| ~ spl11_7 ),
inference(superposition,[],[f203,f271]) ).
tff(f293,definition,
( spl11_9
<=> ( t2tb3(sK3) = cons(a1,t2tb(sK5),t2tb3(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl11_9])],[avatar_definition]) ).
tff(f295,plain,
( ( t2tb3(sK3) = cons(a1,t2tb(sK5),t2tb3(sK4)) )
| ~ spl11_9 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f296,plain,
( spl11_9
| ~ spl11_7 ),
inference(avatar_split_clause,[],[f288,f269,f293]) ).
tff(f298,definition,
( spl11_10
<=> ( cons(a1,t2tb(sK8),t2tb3(sK9)) = t2tb3(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl11_10])],[avatar_definition]) ).
tff(f300,plain,
( ( cons(a1,t2tb(sK8),t2tb3(sK9)) = t2tb3(sK6) )
| ~ spl11_10 ),
inference(avatar_component_clause,[],[f298]) ).
tff(f301,plain,
( spl11_10
| ~ spl11_2 ),
inference(avatar_split_clause,[],[f287,f243,f298]) ).
tff(f311,plain,
( ! [X0: list_a1] :
( ( tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,t2tb3(X0)))) != tb2t1(combine(a1,a1,t2tb3(sK3),cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10))))) )
| ( length(a1,t2tb3(X0)) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,t2tb3(X0),t2tb3(sK9))) ) )
| ~ spl11_5
| ~ spl11_9 ),
inference(superposition,[],[f285,f295]) ).
tff(f315,plain,
( ! [X0: uni] :
( ( tb2t1(combine(a1,a1,t2tb3(sK3),cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10))))) != tb2t1(combine(a1,a1,t2tb3(sK3),reverse(a1,X0))) )
| ( sK2 != tb2t3(infix_plpl(a1,X0,t2tb3(sK9))) )
| ( length(a1,t2tb3(sK3)) != length(a1,X0) ) )
| ~ spl11_5
| ~ spl11_9 ),
inference(superposition,[],[f311,f203]) ).
tff(f326,plain,
( ! [X0: uni] :
( ( tb2t1(combine(a1,a1,t2tb3(sK3),cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10))))) != tb2t1(combine(a1,a1,t2tb3(sK3),X0)) )
| ( length(a1,reverse(a1,X0)) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,X0),t2tb3(sK9))) ) )
| ~ spl11_5
| ~ spl11_9 ),
inference(superposition,[],[f315,f180]) ).
tff(f329,plain,
( ! [X0: uni] :
( ( tb2t1(combine(a1,a1,t2tb3(sK3),cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10))))) != tb2t1(combine(a1,a1,t2tb3(sK3),X0)) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,X0),t2tb3(sK9))) )
| ( length(a1,t2tb3(sK3)) != length(a1,X0) ) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f326,f167]) ).
tff(f344,plain,
( ( length(a1,t2tb3(sK3)) != length(a1,cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10)))) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10)))),t2tb3(sK9))) )
| ~ spl11_5
| ~ spl11_9 ),
inference(equality_resolution,[],[f329]) ).
tff(f345,plain,
( ( $sum(1,length(a1,reverse(a1,t2tb3(sK10)))) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10)))),t2tb3(sK9))) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f344,f188]) ).
tff(f346,plain,
( ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,cons(a1,t2tb(sK8),reverse(a1,t2tb3(sK10)))),t2tb3(sK9))) )
| ( $sum(1,length(a1,t2tb3(sK10))) != length(a1,t2tb3(sK3)) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f345,f167]) ).
tff(f347,plain,
( ( sK2 != tb2t3(infix_plpl(a1,infix_plpl(a1,reverse(a1,reverse(a1,t2tb3(sK10))),cons(a1,t2tb(sK8),nil(a1))),t2tb3(sK9))) )
| ( $sum(1,length(a1,t2tb3(sK10))) != length(a1,t2tb3(sK3)) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f346,f169]) ).
tff(f348,plain,
( ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,reverse(a1,t2tb3(sK10))),infix_plpl(a1,cons(a1,t2tb(sK8),nil(a1)),t2tb3(sK9)))) )
| ( $sum(1,length(a1,t2tb3(sK10))) != length(a1,t2tb3(sK3)) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f347,f226]) ).
tff(f349,plain,
( ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,reverse(a1,t2tb3(sK10))),cons(a1,t2tb(sK8),infix_plpl(a1,nil(a1),t2tb3(sK9))))) )
| ( $sum(1,length(a1,t2tb3(sK10))) != length(a1,t2tb3(sK3)) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f348,f215]) ).
tff(f350,plain,
( ( $sum(1,length(a1,t2tb3(sK10))) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,reverse(a1,t2tb3(sK10))),cons(a1,t2tb(sK8),t2tb3(sK9)))) )
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f349,f216]) ).
tff(f351,plain,
( ( $sum(1,length(a1,t2tb3(sK4))) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,reverse(a1,t2tb3(sK10))),cons(a1,t2tb(sK8),t2tb3(sK9)))) )
| ~ spl11_4
| ~ spl11_5
| ~ spl11_9 ),
inference(forward_demodulation,[],[f350,f256]) ).
tff(f352,plain,
( ( $sum(1,length(a1,t2tb3(sK4))) != length(a1,t2tb3(sK3)) )
| ( sK2 != tb2t3(infix_plpl(a1,reverse(a1,reverse(a1,t2tb3(sK10))),t2tb3(sK6))) )
| ~ spl11_4
| ~ spl11_5
| ~ spl11_9
| ~ spl11_10 ),
inference(forward_demodulation,[],[f351,f300]) ).
tff(f353,plain,
( ( sK2 != tb2t3(infix_plpl(a1,t2tb3(sK10),t2tb3(sK6))) )
| ( $sum(1,length(a1,t2tb3(sK4))) != length(a1,t2tb3(sK3)) )
| ~ spl11_4
| ~ spl11_5
| ~ spl11_9
| ~ spl11_10 ),
inference(forward_demodulation,[],[f352,f180]) ).
tff(f354,plain,
( ( $sum(1,length(a1,t2tb3(sK4))) != length(a1,t2tb3(sK3)) )
| ~ spl11_1
| ~ spl11_4
| ~ spl11_5
| ~ spl11_9
| ~ spl11_10 ),
inference(forward_subsumption_resolution,[],[f353,f240]) ).
tff(f356,definition,
( spl11_14
<=> ( $sum(1,length(a1,t2tb3(sK4))) = length(a1,t2tb3(sK3)) ) ),
introduced(definition,[new_symbols(definition,[spl11_14])],[avatar_definition]) ).
tff(f358,plain,
( ( $sum(1,length(a1,t2tb3(sK4))) != length(a1,t2tb3(sK3)) )
| spl11_14 ),
inference(avatar_component_clause,[],[f356]) ).
tff(f359,plain,
( ~ spl11_14
| ~ spl11_1
| ~ spl11_4
| ~ spl11_5
| ~ spl11_9
| ~ spl11_10 ),
inference(avatar_split_clause,[],[f354,f298,f293,f259,f254,f238,f356]) ).
tff(f573,plain,
( ( $sum(1,length(a1,t2tb3(sK4))) = length(a1,t2tb3(sK3)) )
| ~ spl11_9 ),
inference(superposition,[],[f188,f295]) ).
tff(f582,plain,
( $false
| ~ spl11_9
| spl11_14 ),
inference(forward_subsumption_resolution,[],[f573,f358]) ).
tff(f583,plain,
( ~ spl11_9
| spl11_14 ),
inference(avatar_contradiction_clause,[],[f582]) ).
tff(f585,plain,
$false,
inference(avatar_smt_refutation,[],[f583,f359,f301,f296,f272,f262,f257,f246,f241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW648_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n011.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:23:31 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 2.25/0.83 % (3417377)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.25/0.83 % (3417448)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2789423251:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.25/0.83 % (3417448)First to succeed.
% 2.25/0.83 % (3417448)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3417377"
% 2.25/0.83 % (3417443)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=566313943:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.25/0.83 % (3417445)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3633853967:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.25/0.83 % (3417444)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4219186192:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.25/0.83 % (3417446)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3918702453:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.25/0.83 % (3417446)Instruction limit reached!
% 2.25/0.83 % (3417446)------------------------------
% 2.25/0.83 % (3417446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417446)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417446)Termination reason: Instruction limit
% 2.25/0.83 % (3417446)Termination phase: Saturation
% 2.25/0.83 % (3417446)Time elapsed: 0.005 s
% 2.25/0.83 % (3417446)Peak memory usage: 88 MB
% 2.25/0.83 % (3417446)Instructions burned: 7 (million)
% 2.25/0.83 % (3417443)Instruction limit reached!
% 2.25/0.83 % (3417443)------------------------------
% 2.25/0.83 % (3417443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417443)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417443)Termination reason: Instruction limit
% 2.25/0.83 % (3417443)Termination phase: Saturation
% 2.25/0.83 % (3417443)Time elapsed: 0.030 s
% 2.25/0.83 % (3417443)Peak memory usage: 115 MB
% 2.25/0.83 % (3417443)Instructions burned: 13 (million)
% 2.25/0.83 % (3417449)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3006767955:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.25/0.83 % (3417447)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1364333528:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.25/0.83 % (3417447)Instruction limit reached!
% 2.25/0.83 % (3417447)------------------------------
% 2.25/0.83 % (3417447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417447)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417447)Termination reason: Instruction limit
% 2.25/0.83 % (3417447)Termination phase: Saturation
% 2.25/0.83 % (3417447)Time elapsed: 0.003 s
% 2.25/0.83 % (3417447)Peak memory usage: 87 MB
% 2.25/0.83 % (3417447)Instructions burned: 5 (million)
% 2.25/0.83 % (3417449)Instruction limit reached!
% 2.25/0.83 % (3417449)------------------------------
% 2.25/0.83 % (3417449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417449)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417449)Termination reason: Instruction limit
% 2.25/0.83 % (3417449)Termination phase: Saturation
% 2.25/0.83 % (3417449)Time elapsed: 0.043 s
% 2.25/0.83 % (3417449)Peak memory usage: 116 MB
% 2.25/0.83 % (3417449)Instructions burned: 33 (million)
% 2.25/0.83 % (3417445)Instruction limit reached!
% 2.25/0.83 % (3417445)------------------------------
% 2.25/0.83 % (3417445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417445)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417445)Termination reason: Instruction limit
% 2.25/0.83 % (3417445)Termination phase: Saturation
% 2.25/0.83 % (3417445)Time elapsed: 0.126 s
% 2.25/0.83 % (3417445)Peak memory usage: 118 MB
% 2.25/0.83 % (3417445)Instructions burned: 202 (million)
% 2.25/0.83 % (3417455)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3176351250:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.25/0.83 % (3417455)Instruction limit reached!
% 2.25/0.83 % (3417455)------------------------------
% 2.25/0.83 % (3417455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417455)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417455)Termination reason: Instruction limit
% 2.25/0.83 % (3417455)Termination phase: Saturation
% 2.25/0.83 % (3417455)Time elapsed: 0.012 s
% 2.25/0.83 % (3417455)Peak memory usage: 88 MB
% 2.25/0.83 % (3417455)Instructions burned: 14 (million)
% 2.25/0.83 % (3417457)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=2883439572:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 2.25/0.83 % (3417457)Instruction limit reached!
% 2.25/0.83 % (3417457)------------------------------
% 2.25/0.83 % (3417457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417457)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417457)Termination reason: Instruction limit
% 2.25/0.83 % (3417457)Termination phase: Saturation
% 2.25/0.83 % (3417457)Time elapsed: 0.022 s
% 2.25/0.83 % (3417457)Peak memory usage: 89 MB
% 2.25/0.83 % (3417457)Instructions burned: 29 (million)
% 2.25/0.83 % (3417444)Instruction limit reached!
% 2.25/0.83 % (3417444)------------------------------
% 2.25/0.83 % (3417444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.83 % (3417444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.83 % (3417444)CaDiCaL version: 2.1.3
% 2.25/0.83 % (3417444)Termination reason: Instruction limit
% 2.25/0.83 % (3417444)Termination phase: Saturation
% 2.25/0.83 % (3417444)Time elapsed: 0.210 s
% 2.25/0.83 % (3417444)Peak memory usage: 117 MB
% 2.25/0.83 % (3417444)Instructions burned: 307 (million)
% 2.25/0.83 % (3417448)Refutation found. Thanks to Tanya!
% 2.25/0.83 % SZS status Theorem for theBenchmark
% 2.25/0.83 % SZS output start Proof for theBenchmark
% See solution above
% 3.08/1.05 % (3417448)------------------------------
% 3.08/1.05 % (3417448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.05 % (3417448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.05 % (3417448)CaDiCaL version: 2.1.3
% 3.08/1.05 % (3417448)Termination reason: Refutation
% 3.08/1.05 % (3417448)Time elapsed: 0.036 s
% 3.08/1.05 % (3417448)Peak memory usage: 117 MB
% 3.08/1.05 % (3417448)Instructions burned: 52 (million)
% 3.08/1.05 % (3417448)------------------------------
% 3.08/1.05 % (3417448)------------------------------
% 3.08/1.05 % (3417377)Success in time 0.372 s
% 3.08/1.05 % Vampire exiting
%------------------------------------------------------------------------------