%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW649_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 : n019.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:03 PM UTC 2026
% Result : Theorem 89.61s 13.78s
% Output : Refutation 91.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 73
% Syntax : Number of formulae : 246 ( 90 unt; 0 typ; 65 def)
% Number of atoms : 578 ( 293 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 564 ( 232 ~; 195 |; 60 &)
% ( 41 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 132 ( 16 atm; 64 fun; 44 num; 8 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 48 ( 44 usr; 42 prp; 0-3 aty)
% Number of functors : 85 ( 80 usr; 58 con; 0-5 aty)
% Number of variables : 190 ( 146 !; 44 ?; 190 :)
% 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,
option_a1: $tType ).
tff(type_def_11,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,
option: ty > ty ).
tff(func_def_23,type,
none: ty > uni ).
tff(func_def_24,type,
some: ( ty * uni ) > uni ).
tff(func_def_25,type,
match_option: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_26,type,
some_proj_1: ( ty * uni ) > uni ).
tff(func_def_27,type,
nth: ( ty * $int * uni ) > uni ).
tff(func_def_29,type,
a1: ty ).
tff(func_def_30,type,
t2tb: a > uni ).
tff(func_def_31,type,
tb2t: uni > a ).
tff(func_def_32,type,
t2tb4: option_a1 > uni ).
tff(func_def_33,type,
tb2t4: uni > option_a1 ).
tff(func_def_34,type,
t2tb3: list_a1 > uni ).
tff(func_def_35,type,
tb2t3: uni > list_a1 ).
tff(func_def_37,type,
sK0: list_a1 ).
tff(func_def_38,type,
sK1: list_a1 ).
tff(func_def_39,type,
sK2: a ).
tff(func_def_40,type,
sK3: list_a1 ).
tff(func_def_41,type,
sK4: a ).
tff(func_def_42,type,
sK5: list_a1 ).
tff(func_def_43,type,
sK6: a ).
tff(func_def_44,type,
sK7: list_a1 ).
tff(func_def_45,type,
sK8: list_a1 ).
tff(func_def_46,type,
sK9: list_a1 ).
tff(func_def_47,type,
sK10: a ).
tff(func_def_48,type,
sK11: list_a1 ).
tff(func_def_49,type,
sK12: ( uni * uni * ty ) > uni ).
tff(func_def_50,type,
sK13: ( uni * uni * ty ) > uni ).
tff(func_def_51,type,
sF14: uni ).
tff(func_def_52,type,
sF15: $int ).
tff(func_def_53,type,
sF16: uni ).
tff(func_def_54,type,
sF17: $int ).
tff(func_def_55,type,
sF18: uni ).
tff(func_def_56,type,
sF19: uni ).
tff(func_def_57,type,
sF20: uni ).
tff(func_def_58,type,
sF21: list_a1 ).
tff(func_def_59,type,
sF22: uni ).
tff(func_def_60,type,
sF23: $int ).
tff(func_def_61,type,
sF24: uni ).
tff(func_def_62,type,
sF25: $int ).
tff(func_def_63,type,
sF26: uni ).
tff(func_def_64,type,
sF27: uni ).
tff(func_def_65,type,
sF28: list_a1 ).
tff(func_def_66,type,
sF29: uni ).
tff(func_def_67,type,
sF30: uni ).
tff(func_def_68,type,
sF31: uni ).
tff(func_def_69,type,
sF32: list_a1 ).
tff(func_def_70,type,
sF33: $int ).
tff(func_def_71,type,
sF34: uni ).
tff(func_def_72,type,
sF35: uni ).
tff(func_def_73,type,
sF36: list_a1 ).
tff(func_def_74,type,
sF37: $int ).
tff(func_def_75,type,
sF38: $int ).
tff(func_def_76,type,
sF39: uni ).
tff(func_def_77,type,
sF40: option_a1 ).
tff(func_def_78,type,
sF41: uni ).
tff(func_def_79,type,
sF42: option_a1 ).
tff(func_def_80,type,
sF43: uni ).
tff(func_def_81,type,
sF44: uni ).
tff(func_def_82,type,
sF45: list_a1 ).
tff(func_def_85,type,
'$inst47': $int ).
tff(func_def_86,type,
'$inst48': $int ).
tff(func_def_87,type,
'$inst49': $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
pal: ( ty * uni * $int ) > $o ).
tff(f20,axiom,
! [X0: ty] :
( ( length(X0,nil(X0)) = 0 )
& ! [X2: uni,X1: 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] :
( ! [X3: uni,X2: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) )
& ( infix_plpl(X0,nil(X0),X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(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(f27,axiom,
! [X1: uni,X2: uni,X0: ty] : ( length(X0,infix_plpl(X0,X1,X2)) = $sum(length(X0,X1),length(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',append_length) ).
tff(f56,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f57,conjecture,
! [X1: list_a1,X0: list_a1] :
( $lesseq(length(a1,t2tb3(X1)),length(a1,t2tb3(X0)))
=> ! [X3: list_a1,X2: a] :
( ( X1 = tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) )
=> ! [X4: a,X5: list_a1] :
( ( X3 = tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) )
=> ! [X6: a,X7: list_a1] :
( ( X0 = tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) )
=> ( $lesseq(length(a1,t2tb3(X5)),length(a1,t2tb3(X7)))
=> ! [X8: list_a1] :
( ( ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5))) )
=> ! [X11: list_a1,X10: a] :
( ( X8 = tb2t3(cons(a1,t2tb(X10),t2tb3(X11))) )
=> ( ( tb2t4(nth(a1,$difference(length(a1,t2tb3(X1)),1),t2tb3(X0))) = tb2t4(some(a1,t2tb(X10))) )
=> ( ( X6 = X10 )
=> ? [X9: list_a1] :
( ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X1)) )
& ( X0 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X11))) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_palindrome_rec) ).
tff(f58,negated_conjecture,
~ ! [X1: list_a1,X0: list_a1] :
( $lesseq(length(a1,t2tb3(X1)),length(a1,t2tb3(X0)))
=> ! [X3: list_a1,X2: a] :
( ( X1 = tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) )
=> ! [X4: a,X5: list_a1] :
( ( X3 = tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) )
=> ! [X6: a,X7: list_a1] :
( ( X0 = tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) )
=> ( $lesseq(length(a1,t2tb3(X5)),length(a1,t2tb3(X7)))
=> ! [X8: list_a1] :
( ( ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5))) )
=> ! [X11: list_a1,X10: a] :
( ( X8 = tb2t3(cons(a1,t2tb(X10),t2tb3(X11))) )
=> ( ( tb2t4(nth(a1,$difference(length(a1,t2tb3(X1)),1),t2tb3(X0))) = tb2t4(some(a1,t2tb(X10))) )
=> ( ( X6 = X10 )
=> ? [X9: list_a1] :
( ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X1)) )
& ( X0 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X11))) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
tff(f62,plain,
~ ! [X1: list_a1,X0: list_a1] :
( ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X1)))
=> ! [X3: list_a1,X2: a] :
( ( X1 = tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) )
=> ! [X4: a,X5: list_a1] :
( ( X3 = tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) )
=> ! [X6: a,X7: list_a1] :
( ( X0 = tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) )
=> ( ~ $less(length(a1,t2tb3(X7)),length(a1,t2tb3(X5)))
=> ! [X8: list_a1] :
( ( ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5))) )
=> ! [X11: list_a1,X10: a] :
( ( X8 = tb2t3(cons(a1,t2tb(X10),t2tb3(X11))) )
=> ( ( tb2t4(some(a1,t2tb(X10))) = tb2t4(nth(a1,$sum(length(a1,t2tb3(X1)),$uminus(1)),t2tb3(X0))) )
=> ( ( X6 = X10 )
=> ? [X9: list_a1] :
( ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X1)) )
& ( X0 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X11))) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f58]) ).
tff(f67,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f68,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2) ),
introduced(definition,[],[tha_associativity]) ).
tff(f91,plain,
! [X2: ty,X0: uni,X1: uni] : ( $sum(length(X2,X0),length(X2,X1)) = length(X2,infix_plpl(X2,X0,X1)) ),
inference(rectify,[],[f27]) ).
tff(f102,plain,
! [X0: ty] :
( ! [X1: uni,X2: uni] : ( $sum(1,length(X0,X1)) = length(X0,cons(X0,X2,X1)) )
& ( length(X0,nil(X0)) = 0 ) ),
inference(rectify,[],[f20]) ).
tff(f106,plain,
~ ! [X1: list_a1,X0: list_a1] :
( ~ $less(length(a1,t2tb3(X1)),length(a1,t2tb3(X0)))
=> ! [X3: a,X2: list_a1] :
( ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X0 )
=> ! [X4: a,X5: list_a1] :
( ( tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) = X2 )
=> ! [X7: list_a1,X6: a] :
( ( tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) = X1 )
=> ( ~ $less(length(a1,t2tb3(X7)),length(a1,t2tb3(X5)))
=> ! [X8: list_a1] :
( ( ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5))) )
=> ! [X10: list_a1,X11: a] :
( ( tb2t3(cons(a1,t2tb(X11),t2tb3(X10))) = X8 )
=> ( ( tb2t4(some(a1,t2tb(X11))) = tb2t4(nth(a1,$sum(length(a1,t2tb3(X0)),$uminus(1)),t2tb3(X1))) )
=> ( ( X6 = X11 )
=> ? [X12: list_a1] :
( ( tb2t3(infix_plpl(a1,t2tb3(X12),t2tb3(X10))) = X1 )
& ( length(a1,t2tb3(X0)) = length(a1,t2tb3(X12)) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f62]) ).
tff(f110,plain,
! [X3: uni,X0: uni,X2: ty,X1: uni] : ( infix_plpl(X2,infix_plpl(X2,X1,X3),X0) = infix_plpl(X2,X1,infix_plpl(X2,X3,X0)) ),
inference(rectify,[],[f25]) ).
tff(f136,plain,
? [X1: list_a1,X0: list_a1] :
( ? [X3: a,X2: list_a1] :
( ? [X4: a,X5: list_a1] :
( ? [X7: list_a1,X6: a] :
( ? [X8: list_a1] :
( ? [X10: list_a1,X11: a] :
( ! [X12: list_a1] :
( ( length(a1,t2tb3(X0)) != length(a1,t2tb3(X12)) )
| ( tb2t3(infix_plpl(a1,t2tb3(X12),t2tb3(X10))) != X1 ) )
& ( X6 = X11 )
& ( tb2t4(some(a1,t2tb(X11))) = tb2t4(nth(a1,$sum(length(a1,t2tb3(X0)),$uminus(1)),t2tb3(X1))) )
& ( tb2t3(cons(a1,t2tb(X11),t2tb3(X10))) = X8 ) )
& ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5))) )
& ~ $less(length(a1,t2tb3(X7)),length(a1,t2tb3(X5)))
& ( tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) = X1 ) )
& ( tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) = X2 ) )
& ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X0 ) )
& ~ $less(length(a1,t2tb3(X1)),length(a1,t2tb3(X0))) ),
inference(ennf_transformation,[],[f106]) ).
tff(f137,plain,
? [X1: list_a1,X0: list_a1] :
( ~ $less(length(a1,t2tb3(X1)),length(a1,t2tb3(X0)))
& ? [X3: a,X2: list_a1] :
( ( tb2t3(cons(a1,t2tb(X3),t2tb3(X2))) = X0 )
& ? [X4: a,X5: list_a1] :
( ? [X6: a,X7: list_a1] :
( ~ $less(length(a1,t2tb3(X7)),length(a1,t2tb3(X5)))
& ( tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) = X1 )
& ? [X8: list_a1] :
( ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5)))
& ? [X11: a,X10: list_a1] :
( ! [X12: list_a1] :
( ( length(a1,t2tb3(X0)) != length(a1,t2tb3(X12)) )
| ( tb2t3(infix_plpl(a1,t2tb3(X12),t2tb3(X10))) != X1 ) )
& ( tb2t3(cons(a1,t2tb(X11),t2tb3(X10))) = X8 )
& ( tb2t4(some(a1,t2tb(X11))) = tb2t4(nth(a1,$sum(length(a1,t2tb3(X0)),$uminus(1)),t2tb3(X1))) )
& ( X6 = X11 ) ) ) )
& ( tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) = X2 ) ) ) ),
inference(flattening,[],[f136]) ).
tff(f145,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni] : ( infix_plpl(X2,X3,infix_plpl(X2,X0,X1)) = infix_plpl(X2,infix_plpl(X2,X3,X0),X1) ),
inference(rectify,[],[f110]) ).
tff(f158,plain,
? [X0: list_a1,X1: list_a1] :
( ~ $less(length(a1,t2tb3(X0)),length(a1,t2tb3(X1)))
& ? [X2: a,X3: list_a1] :
( ( tb2t3(cons(a1,t2tb(X2),t2tb3(X3))) = X1 )
& ? [X4: a,X5: list_a1] :
( ? [X6: a,X7: list_a1] :
( ~ $less(length(a1,t2tb3(X7)),length(a1,t2tb3(X5)))
& ( tb2t3(cons(a1,t2tb(X6),t2tb3(X7))) = X0 )
& ? [X8: list_a1] :
( ? [X9: list_a1] :
( ( X7 = tb2t3(infix_plpl(a1,t2tb3(X9),t2tb3(X8))) )
& ( length(a1,t2tb3(X9)) = length(a1,t2tb3(X5)) ) )
& pal(a1,t2tb3(X7),length(a1,t2tb3(X5)))
& ? [X10: a,X11: list_a1] :
( ! [X12: list_a1] :
( ( length(a1,t2tb3(X1)) != length(a1,t2tb3(X12)) )
| ( tb2t3(infix_plpl(a1,t2tb3(X12),t2tb3(X11))) != X0 ) )
& ( tb2t3(cons(a1,t2tb(X10),t2tb3(X11))) = X8 )
& ( tb2t4(some(a1,t2tb(X10))) = tb2t4(nth(a1,$sum(length(a1,t2tb3(X1)),$uminus(1)),t2tb3(X0))) )
& ( X6 = X10 ) ) ) )
& ( tb2t3(cons(a1,t2tb(X4),t2tb3(X5))) = X3 ) ) ) ),
inference(rectify,[],[f137]) ).
tff(f159,plain,
( ~ $less(length(a1,t2tb3(sK0)),length(a1,t2tb3(sK1)))
& ( tb2t3(cons(a1,t2tb(sK2),t2tb3(sK3))) = sK1 )
& ~ $less(length(a1,t2tb3(sK7)),length(a1,t2tb3(sK5)))
& ( sK0 = tb2t3(cons(a1,t2tb(sK6),t2tb3(sK7))) )
& ( sK7 = tb2t3(infix_plpl(a1,t2tb3(sK9),t2tb3(sK8))) )
& ( length(a1,t2tb3(sK9)) = length(a1,t2tb3(sK5)) )
& pal(a1,t2tb3(sK7),length(a1,t2tb3(sK5)))
& ! [X12: list_a1] :
( ( length(a1,t2tb3(sK1)) != length(a1,t2tb3(X12)) )
| ( sK0 != tb2t3(infix_plpl(a1,t2tb3(X12),t2tb3(sK11))) ) )
& ( sK8 = tb2t3(cons(a1,t2tb(sK10),t2tb3(sK11))) )
& ( tb2t4(nth(a1,$sum(length(a1,t2tb3(sK1)),$uminus(1)),t2tb3(sK0))) = tb2t4(some(a1,t2tb(sK10))) )
& ( sK6 = sK10 )
& ( tb2t3(cons(a1,t2tb(sK4),t2tb3(sK5))) = sK3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X9,sK9),skolemize(X10,sK10),skolemize(X11,sK11)],[f158]) ).
tff(f168,plain,
! [X0: ty,X1: uni,X2: uni] : ( length(X0,infix_plpl(X0,X1,X2)) = $sum(length(X0,X1),length(X0,X2)) ),
inference(rectify,[],[f91]) ).
tff(f172,plain,
! [X0: uni,X1: ty] :
( ! [X2: uni,X3: uni] : ( cons(X1,X3,infix_plpl(X1,X2,X0)) = infix_plpl(X1,cons(X1,X3,X2),X0) )
& ( infix_plpl(X1,nil(X1),X0) = X0 ) ),
inference(rectify,[],[f24]) ).
tff(f186,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] : ( infix_plpl(X2,X3,infix_plpl(X2,X0,X1)) = infix_plpl(X2,infix_plpl(X2,X3,X0),X1) ),
inference(cnf_transformation,[],[f145]) ).
tff(f187,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f56]) ).
tff(f204,plain,
! [X2: uni,X0: ty,X1: uni] : ( $sum(1,length(X0,X1)) = length(X0,cons(X0,X2,X1)) ),
inference(cnf_transformation,[],[f102]) ).
tff(f208,plain,
tb2t3(cons(a1,t2tb(sK4),t2tb3(sK5))) = sK3,
inference(cnf_transformation,[],[f159]) ).
tff(f209,plain,
sK6 = sK10,
inference(cnf_transformation,[],[f159]) ).
tff(f211,plain,
sK8 = tb2t3(cons(a1,t2tb(sK10),t2tb3(sK11))),
inference(cnf_transformation,[],[f159]) ).
tff(f212,plain,
! [X12: list_a1] :
( ( length(a1,t2tb3(sK1)) != length(a1,t2tb3(X12)) )
| ( sK0 != tb2t3(infix_plpl(a1,t2tb3(X12),t2tb3(sK11))) ) ),
inference(cnf_transformation,[],[f159]) ).
tff(f214,plain,
length(a1,t2tb3(sK9)) = length(a1,t2tb3(sK5)),
inference(cnf_transformation,[],[f159]) ).
tff(f215,plain,
sK7 = tb2t3(infix_plpl(a1,t2tb3(sK9),t2tb3(sK8))),
inference(cnf_transformation,[],[f159]) ).
tff(f216,plain,
sK0 = tb2t3(cons(a1,t2tb(sK6),t2tb3(sK7))),
inference(cnf_transformation,[],[f159]) ).
tff(f218,plain,
tb2t3(cons(a1,t2tb(sK2),t2tb3(sK3))) = sK1,
inference(cnf_transformation,[],[f159]) ).
tff(f240,plain,
! [X2: uni,X0: ty,X1: uni] : ( length(X0,infix_plpl(X0,X1,X2)) = $sum(length(X0,X1),length(X0,X2)) ),
inference(cnf_transformation,[],[f168]) ).
tff(f246,plain,
! [X0: uni,X1: ty] : ( infix_plpl(X1,nil(X1),X0) = X0 ),
inference(cnf_transformation,[],[f172]) ).
tff(f247,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] : ( cons(X1,X3,infix_plpl(X1,X2,X0)) = infix_plpl(X1,cons(X1,X3,X2),X0) ),
inference(cnf_transformation,[],[f172]) ).
tff(f263,plain,
sK0 = tb2t3(cons(a1,t2tb(sK10),t2tb3(sK7))),
inference(definition_unfolding,[],[f216,f209]) ).
tff(f268,definition,
sF14 = t2tb3(sK0),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f269,plain,
t2tb3(sK0) = sF14,
inference(reorient_equations,[],[f268]) ).
tff(f272,definition,
sF16 = t2tb3(sK1),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f273,definition,
sF17 = length(a1,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f275,definition,
sF18 = t2tb(sK2),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f276,definition,
sF19 = t2tb3(sK3),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f277,definition,
sF20 = cons(a1,sF18,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f278,plain,
cons(a1,sF18,sF19) = sF20,
inference(reorient_equations,[],[f277]) ).
tff(f279,definition,
sF21 = tb2t3(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f280,plain,
sK1 = sF21,
inference(definition_folding,[],[f218,f279,f278,f276,f275]) ).
tff(f281,definition,
sF22 = t2tb3(sK7),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f283,definition,
sF24 = t2tb3(sK5),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f284,definition,
sF25 = length(a1,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f286,definition,
sF26 = t2tb(sK10),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f287,plain,
t2tb(sK10) = sF26,
inference(reorient_equations,[],[f286]) ).
tff(f288,definition,
sF27 = cons(a1,sF26,sF22),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f289,plain,
cons(a1,sF26,sF22) = sF27,
inference(reorient_equations,[],[f288]) ).
tff(f290,definition,
sF28 = tb2t3(sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f291,plain,
sF28 = sK0,
inference(definition_folding,[],[f263,f290,f289,f281,f287]) ).
tff(f292,definition,
sF29 = t2tb3(sK9),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f293,plain,
t2tb3(sK9) = sF29,
inference(reorient_equations,[],[f292]) ).
tff(f294,definition,
sF30 = t2tb3(sK8),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f295,definition,
sF31 = infix_plpl(a1,sF29,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f296,definition,
sF32 = tb2t3(sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f297,plain,
tb2t3(sF31) = sF32,
inference(reorient_equations,[],[f296]) ).
tff(f298,plain,
sF32 = sK7,
inference(definition_folding,[],[f215,f297,f295,f294,f293]) ).
tff(f299,definition,
sF33 = length(a1,sF29),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f300,plain,
sF25 = sF33,
inference(definition_folding,[],[f214,f284,f283,f299,f293]) ).
tff(f302,definition,
sF34 = t2tb3(sK11),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f303,plain,
t2tb3(sK11) = sF34,
inference(reorient_equations,[],[f302]) ).
tff(f304,plain,
! [X12: list_a1] :
( ( sF17 != length(a1,t2tb3(X12)) )
| ( sK0 != tb2t3(infix_plpl(a1,t2tb3(X12),sF34)) ) ),
inference(definition_folding,[],[f212,f303,f273,f272]) ).
tff(f305,definition,
sF35 = cons(a1,sF26,sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f306,plain,
cons(a1,sF26,sF34) = sF35,
inference(reorient_equations,[],[f305]) ).
tff(f307,definition,
sF36 = tb2t3(sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
tff(f308,plain,
sK8 = sF36,
inference(definition_folding,[],[f211,f307,f306,f303,f287]) ).
tff(f320,definition,
sF43 = t2tb(sK4),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
tff(f321,definition,
sF44 = cons(a1,sF43,sF24),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
tff(f322,definition,
sF45 = tb2t3(sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
tff(f323,plain,
sK3 = sF45,
inference(definition_folding,[],[f208,f322,f321,f283,f320]) ).
tff(f344,definition,
( spl46_4
<=> ( sF28 = tb2t3(sF27) ) ),
introduced(definition,[new_symbols(definition,[spl46_4])],[avatar_definition]) ).
tff(f346,plain,
( ( sF28 = tb2t3(sF27) )
| ~ spl46_4 ),
inference(avatar_component_clause,[],[f344]) ).
tff(f347,plain,
spl46_4,
inference(avatar_split_clause,[],[f290,f344]) ).
tff(f354,definition,
( spl46_6
<=> ( sF22 = t2tb3(sK7) ) ),
introduced(definition,[new_symbols(definition,[spl46_6])],[avatar_definition]) ).
tff(f356,plain,
( ( sF22 = t2tb3(sK7) )
| ~ spl46_6 ),
inference(avatar_component_clause,[],[f354]) ).
tff(f357,plain,
spl46_6,
inference(avatar_split_clause,[],[f281,f354]) ).
tff(f359,definition,
( spl46_7
<=> ( sF36 = tb2t3(sF35) ) ),
introduced(definition,[new_symbols(definition,[spl46_7])],[avatar_definition]) ).
tff(f361,plain,
( ( sF36 = tb2t3(sF35) )
| ~ spl46_7 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f362,plain,
spl46_7,
inference(avatar_split_clause,[],[f307,f359]) ).
tff(f364,definition,
( spl46_8
<=> ( tb2t3(sF31) = sF32 ) ),
introduced(definition,[new_symbols(definition,[spl46_8])],[avatar_definition]) ).
tff(f366,plain,
( ( tb2t3(sF31) = sF32 )
| ~ spl46_8 ),
inference(avatar_component_clause,[],[f364]) ).
tff(f367,plain,
spl46_8,
inference(avatar_split_clause,[],[f297,f364]) ).
tff(f369,definition,
( spl46_9
<=> ( sK8 = sF36 ) ),
introduced(definition,[new_symbols(definition,[spl46_9])],[avatar_definition]) ).
tff(f371,plain,
( ( sK8 = sF36 )
| ~ spl46_9 ),
inference(avatar_component_clause,[],[f369]) ).
tff(f372,plain,
spl46_9,
inference(avatar_split_clause,[],[f308,f369]) ).
tff(f384,definition,
( spl46_12
<=> ( sF45 = tb2t3(sF44) ) ),
introduced(definition,[new_symbols(definition,[spl46_12])],[avatar_definition]) ).
tff(f386,plain,
( ( sF45 = tb2t3(sF44) )
| ~ spl46_12 ),
inference(avatar_component_clause,[],[f384]) ).
tff(f387,plain,
spl46_12,
inference(avatar_split_clause,[],[f322,f384]) ).
tff(f389,definition,
( spl46_13
<=> ( sF19 = t2tb3(sK3) ) ),
introduced(definition,[new_symbols(definition,[spl46_13])],[avatar_definition]) ).
tff(f391,plain,
( ( sF19 = t2tb3(sK3) )
| ~ spl46_13 ),
inference(avatar_component_clause,[],[f389]) ).
tff(f392,plain,
spl46_13,
inference(avatar_split_clause,[],[f276,f389]) ).
tff(f399,definition,
( spl46_15
<=> ( sF30 = t2tb3(sK8) ) ),
introduced(definition,[new_symbols(definition,[spl46_15])],[avatar_definition]) ).
tff(f401,plain,
( ( sF30 = t2tb3(sK8) )
| ~ spl46_15 ),
inference(avatar_component_clause,[],[f399]) ).
tff(f402,plain,
spl46_15,
inference(avatar_split_clause,[],[f294,f399]) ).
tff(f404,definition,
( spl46_16
<=> ( sF16 = t2tb3(sK1) ) ),
introduced(definition,[new_symbols(definition,[spl46_16])],[avatar_definition]) ).
tff(f406,plain,
( ( sF16 = t2tb3(sK1) )
| ~ spl46_16 ),
inference(avatar_component_clause,[],[f404]) ).
tff(f407,plain,
spl46_16,
inference(avatar_split_clause,[],[f272,f404]) ).
tff(f409,definition,
( spl46_17
<=> ( sF21 = tb2t3(sF20) ) ),
introduced(definition,[new_symbols(definition,[spl46_17])],[avatar_definition]) ).
tff(f411,plain,
( ( sF21 = tb2t3(sF20) )
| ~ spl46_17 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
spl46_17,
inference(avatar_split_clause,[],[f279,f409]) ).
tff(f414,definition,
( spl46_18
<=> ( sF33 = length(a1,sF29) ) ),
introduced(definition,[new_symbols(definition,[spl46_18])],[avatar_definition]) ).
tff(f416,plain,
( ( sF33 = length(a1,sF29) )
| ~ spl46_18 ),
inference(avatar_component_clause,[],[f414]) ).
tff(f417,plain,
spl46_18,
inference(avatar_split_clause,[],[f299,f414]) ).
tff(f429,definition,
( spl46_21
<=> ( sK3 = sF45 ) ),
introduced(definition,[new_symbols(definition,[spl46_21])],[avatar_definition]) ).
tff(f431,plain,
( ( sK3 = sF45 )
| ~ spl46_21 ),
inference(avatar_component_clause,[],[f429]) ).
tff(f432,plain,
spl46_21,
inference(avatar_split_clause,[],[f323,f429]) ).
tff(f434,definition,
( spl46_22
<=> ( sF31 = infix_plpl(a1,sF29,sF30) ) ),
introduced(definition,[new_symbols(definition,[spl46_22])],[avatar_definition]) ).
tff(f436,plain,
( ( sF31 = infix_plpl(a1,sF29,sF30) )
| ~ spl46_22 ),
inference(avatar_component_clause,[],[f434]) ).
tff(f437,plain,
spl46_22,
inference(avatar_split_clause,[],[f295,f434]) ).
tff(f439,definition,
( spl46_23
<=> ( sF32 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl46_23])],[avatar_definition]) ).
tff(f441,plain,
( ( sF32 = sK7 )
| ~ spl46_23 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,plain,
spl46_23,
inference(avatar_split_clause,[],[f298,f439]) ).
tff(f444,definition,
( spl46_24
<=> ( sF17 = length(a1,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl46_24])],[avatar_definition]) ).
tff(f446,plain,
( ( sF17 = length(a1,sF16) )
| ~ spl46_24 ),
inference(avatar_component_clause,[],[f444]) ).
tff(f447,plain,
spl46_24,
inference(avatar_split_clause,[],[f273,f444]) ).
tff(f455,definition,
( spl46_26
<=> ( t2tb3(sK0) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl46_26])],[avatar_definition]) ).
tff(f457,plain,
( ( t2tb3(sK0) = sF14 )
| ~ spl46_26 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f458,plain,
spl46_26,
inference(avatar_split_clause,[],[f269,f455]) ).
tff(f465,definition,
( spl46_28
<=> ( sK1 = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl46_28])],[avatar_definition]) ).
tff(f467,plain,
( ( sK1 = sF21 )
| ~ spl46_28 ),
inference(avatar_component_clause,[],[f465]) ).
tff(f468,plain,
spl46_28,
inference(avatar_split_clause,[],[f280,f465]) ).
tff(f480,definition,
( spl46_31
<=> ( cons(a1,sF26,sF22) = sF27 ) ),
introduced(definition,[new_symbols(definition,[spl46_31])],[avatar_definition]) ).
tff(f482,plain,
( ( cons(a1,sF26,sF22) = sF27 )
| ~ spl46_31 ),
inference(avatar_component_clause,[],[f480]) ).
tff(f483,plain,
spl46_31,
inference(avatar_split_clause,[],[f289,f480]) ).
tff(f490,definition,
( spl46_33
<=> ( cons(a1,sF18,sF19) = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl46_33])],[avatar_definition]) ).
tff(f492,plain,
( ( cons(a1,sF18,sF19) = sF20 )
| ~ spl46_33 ),
inference(avatar_component_clause,[],[f490]) ).
tff(f493,plain,
spl46_33,
inference(avatar_split_clause,[],[f278,f490]) ).
tff(f495,definition,
( spl46_34
<=> ( sF44 = cons(a1,sF43,sF24) ) ),
introduced(definition,[new_symbols(definition,[spl46_34])],[avatar_definition]) ).
tff(f497,plain,
( ( sF44 = cons(a1,sF43,sF24) )
| ~ spl46_34 ),
inference(avatar_component_clause,[],[f495]) ).
tff(f498,plain,
spl46_34,
inference(avatar_split_clause,[],[f321,f495]) ).
tff(f510,definition,
( spl46_37
<=> ( cons(a1,sF26,sF34) = sF35 ) ),
introduced(definition,[new_symbols(definition,[spl46_37])],[avatar_definition]) ).
tff(f512,plain,
( ( cons(a1,sF26,sF34) = sF35 )
| ~ spl46_37 ),
inference(avatar_component_clause,[],[f510]) ).
tff(f513,plain,
spl46_37,
inference(avatar_split_clause,[],[f306,f510]) ).
tff(f515,definition,
( spl46_38
<=> ( sF25 = length(a1,sF24) ) ),
introduced(definition,[new_symbols(definition,[spl46_38])],[avatar_definition]) ).
tff(f517,plain,
( ( sF25 = length(a1,sF24) )
| ~ spl46_38 ),
inference(avatar_component_clause,[],[f515]) ).
tff(f518,plain,
spl46_38,
inference(avatar_split_clause,[],[f284,f515]) ).
tff(f520,definition,
( spl46_39
<=> ( sF28 = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl46_39])],[avatar_definition]) ).
tff(f522,plain,
( ( sF28 = sK0 )
| ~ spl46_39 ),
inference(avatar_component_clause,[],[f520]) ).
tff(f523,plain,
spl46_39,
inference(avatar_split_clause,[],[f291,f520]) ).
tff(f540,definition,
( spl46_43
<=> ( sF25 = sF33 ) ),
introduced(definition,[new_symbols(definition,[spl46_43])],[avatar_definition]) ).
tff(f542,plain,
( ( sF25 = sF33 )
| ~ spl46_43 ),
inference(avatar_component_clause,[],[f540]) ).
tff(f543,plain,
spl46_43,
inference(avatar_split_clause,[],[f300,f540]) ).
tff(f544,plain,
( ( sK3 = tb2t3(sF44) )
| ~ spl46_12
| ~ spl46_21 ),
inference(forward_demodulation,[],[f386,f431]) ).
tff(f545,plain,
( ( t2tb3(sF28) = sF14 )
| ~ spl46_26
| ~ spl46_39 ),
inference(forward_demodulation,[],[f457,f522]) ).
tff(f548,definition,
( spl46_44
<=> ( sK3 = tb2t3(sF44) ) ),
introduced(definition,[new_symbols(definition,[spl46_44])],[avatar_definition]) ).
tff(f550,plain,
( ( sK3 = tb2t3(sF44) )
| ~ spl46_44 ),
inference(avatar_component_clause,[],[f548]) ).
tff(f551,plain,
( spl46_44
| ~ spl46_12
| ~ spl46_21 ),
inference(avatar_split_clause,[],[f544,f429,f384,f548]) ).
tff(f553,definition,
( spl46_45
<=> ( t2tb3(sF28) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl46_45])],[avatar_definition]) ).
tff(f555,plain,
( ( t2tb3(sF28) = sF14 )
| ~ spl46_45 ),
inference(avatar_component_clause,[],[f553]) ).
tff(f556,plain,
( spl46_45
| ~ spl46_26
| ~ spl46_39 ),
inference(avatar_split_clause,[],[f545,f520,f455,f553]) ).
tff(f669,plain,
( ( sF20 = t2tb3(sF21) )
| ~ spl46_17 ),
inference(superposition,[],[f187,f411]) ).
tff(f670,plain,
( ( t2tb3(sF28) = sF27 )
| ~ spl46_4 ),
inference(superposition,[],[f187,f346]) ).
tff(f671,plain,
( ( t2tb3(sF32) = sF31 )
| ~ spl46_8 ),
inference(superposition,[],[f187,f366]) ).
tff(f672,plain,
( ( t2tb3(sF36) = sF35 )
| ~ spl46_7 ),
inference(superposition,[],[f187,f361]) ).
tff(f673,plain,
( ( sF44 = t2tb3(sK3) )
| ~ spl46_44 ),
inference(superposition,[],[f187,f550]) ).
tff(f674,plain,
! [X0: uni] :
( ( sK0 != tb2t3(infix_plpl(a1,X0,sF34)) )
| ( sF17 != length(a1,X0) ) ),
inference(superposition,[],[f304,f187]) ).
tff(f675,plain,
( ( t2tb3(sK8) = sF35 )
| ~ spl46_7
| ~ spl46_9 ),
inference(forward_demodulation,[],[f672,f371]) ).
tff(f676,plain,
( ( t2tb3(sK1) = sF20 )
| ~ spl46_17
| ~ spl46_28 ),
inference(forward_demodulation,[],[f669,f467]) ).
tff(f677,plain,
( ( sF19 = sF44 )
| ~ spl46_13
| ~ spl46_44 ),
inference(forward_demodulation,[],[f673,f391]) ).
tff(f678,plain,
( ( t2tb3(sK7) = sF31 )
| ~ spl46_8
| ~ spl46_23 ),
inference(forward_demodulation,[],[f671,f441]) ).
tff(f679,plain,
( ( sF14 = sF27 )
| ~ spl46_4
| ~ spl46_45 ),
inference(forward_demodulation,[],[f670,f555]) ).
tff(f680,plain,
( ! [X0: uni] :
( ( sF28 != tb2t3(infix_plpl(a1,X0,sF34)) )
| ( sF17 != length(a1,X0) ) )
| ~ spl46_39 ),
inference(forward_demodulation,[],[f674,f522]) ).
tff(f682,definition,
( spl46_64
<=> ( t2tb3(sK8) = sF35 ) ),
introduced(definition,[new_symbols(definition,[spl46_64])],[avatar_definition]) ).
tff(f684,plain,
( ( t2tb3(sK8) = sF35 )
| ~ spl46_64 ),
inference(avatar_component_clause,[],[f682]) ).
tff(f685,plain,
( spl46_64
| ~ spl46_7
| ~ spl46_9 ),
inference(avatar_split_clause,[],[f675,f369,f359,f682]) ).
tff(f687,definition,
( spl46_65
<=> ( t2tb3(sK1) = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl46_65])],[avatar_definition]) ).
tff(f689,plain,
( ( t2tb3(sK1) = sF20 )
| ~ spl46_65 ),
inference(avatar_component_clause,[],[f687]) ).
tff(f690,plain,
( spl46_65
| ~ spl46_17
| ~ spl46_28 ),
inference(avatar_split_clause,[],[f676,f465,f409,f687]) ).
tff(f692,definition,
( spl46_66
<=> ( sF19 = sF44 ) ),
introduced(definition,[new_symbols(definition,[spl46_66])],[avatar_definition]) ).
tff(f694,plain,
( ( sF19 = sF44 )
| ~ spl46_66 ),
inference(avatar_component_clause,[],[f692]) ).
tff(f695,plain,
( spl46_66
| ~ spl46_13
| ~ spl46_44 ),
inference(avatar_split_clause,[],[f677,f548,f389,f692]) ).
tff(f697,definition,
( spl46_67
<=> ( t2tb3(sK7) = sF31 ) ),
introduced(definition,[new_symbols(definition,[spl46_67])],[avatar_definition]) ).
tff(f699,plain,
( ( t2tb3(sK7) = sF31 )
| ~ spl46_67 ),
inference(avatar_component_clause,[],[f697]) ).
tff(f700,plain,
( spl46_67
| ~ spl46_8
| ~ spl46_23 ),
inference(avatar_split_clause,[],[f678,f439,f364,f697]) ).
tff(f702,definition,
( spl46_68
<=> ( sF14 = sF27 ) ),
introduced(definition,[new_symbols(definition,[spl46_68])],[avatar_definition]) ).
tff(f704,plain,
( ( sF14 = sF27 )
| ~ spl46_68 ),
inference(avatar_component_clause,[],[f702]) ).
tff(f705,plain,
( spl46_68
| ~ spl46_4
| ~ spl46_45 ),
inference(avatar_split_clause,[],[f679,f553,f344,f702]) ).
tff(f712,plain,
( ( sF28 = tb2t3(sF14) )
| ~ spl46_4
| ~ spl46_68 ),
inference(superposition,[],[f346,f704]) ).
tff(f714,definition,
( spl46_70
<=> ( sF28 = tb2t3(sF14) ) ),
introduced(definition,[new_symbols(definition,[spl46_70])],[avatar_definition]) ).
tff(f716,plain,
( ( sF28 = tb2t3(sF14) )
| ~ spl46_70 ),
inference(avatar_component_clause,[],[f714]) ).
tff(f717,plain,
( spl46_70
| ~ spl46_4
| ~ spl46_68 ),
inference(avatar_split_clause,[],[f712,f702,f344,f714]) ).
tff(f737,plain,
( ( sF30 = sF35 )
| ~ spl46_15
| ~ spl46_64 ),
inference(superposition,[],[f401,f684]) ).
tff(f741,definition,
( spl46_74
<=> ( sF30 = sF35 ) ),
introduced(definition,[new_symbols(definition,[spl46_74])],[avatar_definition]) ).
tff(f743,plain,
( ( sF30 = sF35 )
| ~ spl46_74 ),
inference(avatar_component_clause,[],[f741]) ).
tff(f744,plain,
( spl46_74
| ~ spl46_15
| ~ spl46_64 ),
inference(avatar_split_clause,[],[f737,f682,f399,f741]) ).
tff(f752,plain,
( ( sF16 = sF20 )
| ~ spl46_16
| ~ spl46_65 ),
inference(superposition,[],[f406,f689]) ).
tff(f756,definition,
( spl46_76
<=> ( sF16 = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl46_76])],[avatar_definition]) ).
tff(f758,plain,
( ( sF16 = sF20 )
| ~ spl46_76 ),
inference(avatar_component_clause,[],[f756]) ).
tff(f759,plain,
( spl46_76
| ~ spl46_16
| ~ spl46_65 ),
inference(avatar_split_clause,[],[f752,f687,f404,f756]) ).
tff(f810,plain,
( ( sF22 = sF31 )
| ~ spl46_6
| ~ spl46_67 ),
inference(superposition,[],[f699,f356]) ).
tff(f816,definition,
( spl46_84
<=> ( sF22 = sF31 ) ),
introduced(definition,[new_symbols(definition,[spl46_84])],[avatar_definition]) ).
tff(f818,plain,
( ( sF22 = sF31 )
| ~ spl46_84 ),
inference(avatar_component_clause,[],[f816]) ).
tff(f819,plain,
( spl46_84
| ~ spl46_6
| ~ spl46_67 ),
inference(avatar_split_clause,[],[f810,f697,f354,f816]) ).
tff(f907,plain,
( ( sF17 = length(a1,sF20) )
| ~ spl46_24
| ~ spl46_76 ),
inference(superposition,[],[f446,f758]) ).
tff(f910,definition,
( spl46_97
<=> ( sF17 = length(a1,sF20) ) ),
introduced(definition,[new_symbols(definition,[spl46_97])],[avatar_definition]) ).
tff(f912,plain,
( ( sF17 = length(a1,sF20) )
| ~ spl46_97 ),
inference(avatar_component_clause,[],[f910]) ).
tff(f913,plain,
( spl46_97
| ~ spl46_24
| ~ spl46_76 ),
inference(avatar_split_clause,[],[f907,f756,f444,f910]) ).
tff(f952,plain,
( ( sF31 = infix_plpl(a1,sF29,sF35) )
| ~ spl46_22
| ~ spl46_74 ),
inference(superposition,[],[f436,f743]) ).
tff(f954,definition,
( spl46_102
<=> ( sF31 = infix_plpl(a1,sF29,sF35) ) ),
introduced(definition,[new_symbols(definition,[spl46_102])],[avatar_definition]) ).
tff(f956,plain,
( ( sF31 = infix_plpl(a1,sF29,sF35) )
| ~ spl46_102 ),
inference(avatar_component_clause,[],[f954]) ).
tff(f957,plain,
( spl46_102
| ~ spl46_22
| ~ spl46_74 ),
inference(avatar_split_clause,[],[f952,f741,f434,f954]) ).
tff(f960,plain,
( ( cons(a1,sF26,sF31) = sF27 )
| ~ spl46_31
| ~ spl46_84 ),
inference(superposition,[],[f482,f818]) ).
tff(f963,plain,
( ( cons(a1,sF26,sF31) = sF14 )
| ~ spl46_31
| ~ spl46_68
| ~ spl46_84 ),
inference(forward_demodulation,[],[f960,f704]) ).
tff(f970,definition,
( spl46_104
<=> ( cons(a1,sF26,sF31) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl46_104])],[avatar_definition]) ).
tff(f972,plain,
( ( cons(a1,sF26,sF31) = sF14 )
| ~ spl46_104 ),
inference(avatar_component_clause,[],[f970]) ).
tff(f973,plain,
( spl46_104
| ~ spl46_31
| ~ spl46_68
| ~ spl46_84 ),
inference(avatar_split_clause,[],[f963,f816,f702,f480,f970]) ).
tff(f1383,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum(X1,$sum(X2,X0)) = $sum(X0,$sum(X1,X2)) ),
inference(superposition,[],[f68,f67]) ).
tff(f1513,plain,
( ( $sum(1,length(a1,sF19)) = length(a1,sF20) )
| ~ spl46_33 ),
inference(superposition,[],[f204,f492]) ).
tff(f1514,plain,
( ( length(a1,sF44) = $sum(1,length(a1,sF24)) )
| ~ spl46_34 ),
inference(superposition,[],[f204,f497]) ).
tff(f1518,plain,
( ( $sum(1,length(a1,sF19)) = sF17 )
| ~ spl46_33
| ~ spl46_97 ),
inference(forward_demodulation,[],[f1513,f912]) ).
tff(f1526,plain,
( ( $sum(1,sF25) = length(a1,sF44) )
| ~ spl46_34
| ~ spl46_38 ),
inference(forward_demodulation,[],[f1514,f517]) ).
tff(f1529,definition,
( spl46_159
<=> ( $sum(1,length(a1,sF19)) = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl46_159])],[avatar_definition]) ).
tff(f1531,plain,
( ( $sum(1,length(a1,sF19)) = sF17 )
| ~ spl46_159 ),
inference(avatar_component_clause,[],[f1529]) ).
tff(f1532,plain,
( spl46_159
| ~ spl46_33
| ~ spl46_97 ),
inference(avatar_split_clause,[],[f1518,f910,f490,f1529]) ).
tff(f1534,plain,
( ( $sum(1,sF25) = length(a1,sF19) )
| ~ spl46_34
| ~ spl46_38
| ~ spl46_66 ),
inference(forward_demodulation,[],[f1526,f694]) ).
tff(f1570,definition,
( spl46_165
<=> ( $sum(1,sF25) = length(a1,sF19) ) ),
introduced(definition,[new_symbols(definition,[spl46_165])],[avatar_definition]) ).
tff(f1572,plain,
( ( $sum(1,sF25) = length(a1,sF19) )
| ~ spl46_165 ),
inference(avatar_component_clause,[],[f1570]) ).
tff(f1573,plain,
( spl46_165
| ~ spl46_34
| ~ spl46_38
| ~ spl46_66 ),
inference(avatar_split_clause,[],[f1534,f692,f515,f495,f1570]) ).
tff(f1771,plain,
( ( sF17 = $sum(1,$sum(1,sF25)) )
| ~ spl46_159
| ~ spl46_165 ),
inference(superposition,[],[f1531,f1572]) ).
tff(f1800,definition,
( spl46_183
<=> ( sF17 = $sum(1,$sum(1,sF25)) ) ),
introduced(definition,[new_symbols(definition,[spl46_183])],[avatar_definition]) ).
tff(f1802,plain,
( ( sF17 = $sum(1,$sum(1,sF25)) )
| ~ spl46_183 ),
inference(avatar_component_clause,[],[f1800]) ).
tff(f1803,plain,
( spl46_183
| ~ spl46_159
| ~ spl46_165 ),
inference(avatar_split_clause,[],[f1771,f1570,f1529,f1800]) ).
tff(f1862,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( length(X0,infix_plpl(X0,X2,cons(X0,X3,X1))) = $sum(length(X0,X2),$sum(1,length(X0,X1))) ),
inference(superposition,[],[f240,f204]) ).
tff(f1871,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( length(X0,infix_plpl(X0,X2,cons(X0,X3,X1))) = $sum(1,$sum(length(X0,X1),length(X0,X2))) ),
inference(forward_demodulation,[],[f1862,f1383]) ).
tff(f1884,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( length(X0,infix_plpl(X0,X2,cons(X0,X3,X1))) = $sum(1,length(X0,infix_plpl(X0,X1,X2))) ),
inference(forward_demodulation,[],[f1871,f240]) ).
tff(f1997,plain,
( ! [X0: uni,X1: uni] :
( ( sF28 != tb2t3(infix_plpl(a1,X0,infix_plpl(a1,X1,sF34))) )
| ( sF17 != length(a1,infix_plpl(a1,X0,X1)) ) )
| ~ spl46_39 ),
inference(superposition,[],[f680,f186]) ).
tff(f2085,plain,
( ! [X2: uni,X0: uni,X1: uni] :
( ( sF28 != tb2t3(infix_plpl(a1,X2,cons(a1,X0,infix_plpl(a1,X1,sF34)))) )
| ( length(a1,infix_plpl(a1,X2,cons(a1,X0,X1))) != sF17 ) )
| ~ spl46_39 ),
inference(superposition,[],[f1997,f247]) ).
tff(f2091,plain,
( ! [X2: uni,X0: uni,X1: uni] :
( ( sF28 != tb2t3(infix_plpl(a1,X2,cons(a1,X0,infix_plpl(a1,X1,sF34)))) )
| ( sF17 != $sum(1,length(a1,infix_plpl(a1,X1,X2))) ) )
| ~ spl46_39 ),
inference(forward_demodulation,[],[f2085,f1884]) ).
tff(f2180,plain,
( ! [X0: uni,X1: uni] :
( ( $sum(1,length(a1,infix_plpl(a1,nil(a1),X0))) != sF17 )
| ( sF28 != tb2t3(infix_plpl(a1,X0,cons(a1,X1,sF34))) ) )
| ~ spl46_39 ),
inference(superposition,[],[f2091,f246]) ).
tff(f2188,plain,
( ! [X0: uni,X1: uni] :
( ( sF28 != tb2t3(infix_plpl(a1,X0,cons(a1,X1,sF34))) )
| ( sF17 != $sum(1,length(a1,X0)) ) )
| ~ spl46_39 ),
inference(forward_demodulation,[],[f2180,f246]) ).
tff(f2211,plain,
( ! [X0: uni] :
( ( sF28 != tb2t3(infix_plpl(a1,X0,sF35)) )
| ( sF17 != $sum(1,length(a1,X0)) ) )
| ~ spl46_37
| ~ spl46_39 ),
inference(superposition,[],[f2188,f512]) ).
tff(f2254,plain,
( ! [X0: uni,X1: uni] :
( ( sF28 != tb2t3(cons(a1,X0,infix_plpl(a1,X1,sF35))) )
| ( sF17 != $sum(1,length(a1,cons(a1,X0,X1))) ) )
| ~ spl46_37
| ~ spl46_39 ),
inference(superposition,[],[f2211,f247]) ).
tff(f2255,plain,
( ! [X0: uni,X1: uni] :
( ( sF28 != tb2t3(cons(a1,X0,infix_plpl(a1,X1,sF35))) )
| ( $sum(1,$sum(1,length(a1,X1))) != sF17 ) )
| ~ spl46_37
| ~ spl46_39 ),
inference(forward_demodulation,[],[f2254,f204]) ).
tff(f2310,plain,
( ! [X0: uni] :
( ( sF28 != tb2t3(cons(a1,X0,sF31)) )
| ( sF17 != $sum(1,$sum(1,length(a1,sF29))) ) )
| ~ spl46_37
| ~ spl46_39
| ~ spl46_102 ),
inference(superposition,[],[f2255,f956]) ).
tff(f2314,plain,
( ! [X0: uni] :
( ( sF17 != $sum(1,$sum(1,sF33)) )
| ( sF28 != tb2t3(cons(a1,X0,sF31)) ) )
| ~ spl46_18
| ~ spl46_37
| ~ spl46_39
| ~ spl46_102 ),
inference(forward_demodulation,[],[f2310,f416]) ).
tff(f2318,plain,
( ! [X0: uni] :
( ( sF17 != $sum(1,$sum(1,sF25)) )
| ( sF28 != tb2t3(cons(a1,X0,sF31)) ) )
| ~ spl46_18
| ~ spl46_37
| ~ spl46_39
| ~ spl46_43
| ~ spl46_102 ),
inference(forward_demodulation,[],[f2314,f542]) ).
tff(f2319,plain,
( ! [X0: uni] : ( sF28 != tb2t3(cons(a1,X0,sF31)) )
| ~ spl46_18
| ~ spl46_37
| ~ spl46_39
| ~ spl46_43
| ~ spl46_102
| ~ spl46_183 ),
inference(forward_subsumption_resolution,[],[f2318,f1802]) ).
tff(f2382,plain,
( ( sF28 != tb2t3(sF14) )
| ~ spl46_18
| ~ spl46_37
| ~ spl46_39
| ~ spl46_43
| ~ spl46_102
| ~ spl46_104
| ~ spl46_183 ),
inference(superposition,[],[f2319,f972]) ).
tff(f2383,plain,
( $false
| ~ spl46_18
| ~ spl46_37
| ~ spl46_39
| ~ spl46_43
| ~ spl46_70
| ~ spl46_102
| ~ spl46_104
| ~ spl46_183 ),
inference(forward_subsumption_resolution,[],[f2382,f716]) ).
tff(f2384,plain,
( ~ spl46_18
| ~ spl46_37
| ~ spl46_39
| ~ spl46_43
| ~ spl46_70
| ~ spl46_102
| ~ spl46_104
| ~ spl46_183 ),
inference(avatar_contradiction_clause,[],[f2383]) ).
tff(f2385,plain,
$false,
inference(avatar_smt_refutation,[],[f2384,f1803,f1573,f1532,f973,f957,f913,f819,f759,f744,f717,f705,f700,f695,f690,f685,f556,f551,f543,f523,f518,f513,f498,f493,f483,f468,f458,f447,f442,f437,f432,f417,f412,f407,f402,f392,f387,f372,f367,f362,f357,f347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW649_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.22 % Computer : n019.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 14:23:33 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.28 Running first-order theorem proving
% 0.25/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.50/1.79 % (4031597)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.50/1.79 % (4031606)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=466761145:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.50/1.79 % (4031606)Instruction limit reached!
% 5.50/1.79 % (4031606)------------------------------
% 5.50/1.79 % (4031606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.50/1.79 % (4031606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.50/1.79 % (4031606)CaDiCaL version: 2.1.3
% 5.50/1.79 % (4031606)Termination reason: Instruction limit
% 5.50/1.79 % (4031606)Termination phase: Saturation
% 5.50/1.79 % (4031606)Time elapsed: 0.003 s
% 5.50/1.79 % (4031606)Peak memory usage: 88 MB
% 5.50/1.79 % (4031606)Instructions burned: 5 (million)
% 5.50/1.79 % (4031608)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2375907972:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.50/1.79 % (4031602)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=805167325:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.50/1.79 % (4031603)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=322424350:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.50/1.79 % (4031605)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3857301867:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.50/1.79 % (4031604)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2395843092:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.50/1.79 % (4031605)Instruction limit reached!
% 5.50/1.79 % (4031605)------------------------------
% 5.50/1.79 % (4031605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.50/1.79 % (4031605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.50/1.79 % (4031605)CaDiCaL version: 2.1.3
% 5.50/1.79 % (4031605)Termination reason: Instruction limit
% 5.50/1.79 % (4031605)Termination phase: Saturation
% 5.50/1.79 % (4031605)Time elapsed: 0.008 s
% 5.50/1.79 % (4031605)Peak memory usage: 88 MB
% 5.50/1.79 % (4031605)Instructions burned: 7 (million)
% 5.50/1.79 % (4031608)Instruction limit reached!
% 5.50/1.79 % (4031608)------------------------------
% 5.50/1.79 % (4031608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.50/1.79 % (4031608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.50/1.79 % (4031608)CaDiCaL version: 2.1.3
% 5.50/1.79 % (4031608)Termination reason: Instruction limit
% 5.50/1.79 % (4031608)Termination phase: Saturation
% 5.50/1.79 % (4031608)Time elapsed: 0.066 s
% 5.50/1.79 % (4031608)Peak memory usage: 116 MB
% 5.50/1.79 % (4031608)Instructions burned: 33 (million)
% 5.50/1.79 % (4031607)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4064976576:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.50/1.79 % (4031602)Instruction limit reached!
% 5.50/1.79 % (4031602)------------------------------
% 5.50/1.79 % (4031602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.50/1.79 % (4031602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.50/1.79 % (4031602)CaDiCaL version: 2.1.3
% 5.50/1.79 % (4031602)Termination reason: Instruction limit
% 5.50/1.79 % (4031602)Termination phase: Saturation
% 5.50/1.79 % (4031602)Time elapsed: 0.042 s
% 5.50/1.79 % (4031602)Peak memory usage: 115 MB
% 5.50/1.79 % (4031602)Instructions burned: 12 (million)
% 5.50/1.79 % (4031607)Instruction limit reached!
% 5.50/1.79 % (4031607)------------------------------
% 5.50/1.79 % (4031607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.50/1.79 % (4031607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.50/1.79 % (4031607)CaDiCaL version: 2.1.3
% 5.50/1.79 % (4031607)Termination reason: Instruction limit
% 5.50/1.79 % (4031607)Termination phase: Saturation
% 5.50/1.79 % (4031607)Time elapsed: 0.071 s
% 5.50/1.79 % (4031607)Peak memory usage: 116 MB
% 5.50/1.79 % (4031607)Instructions burned: 47 (million)
% 5.50/1.79 % (4031611)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3899224432:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 5.50/1.79 % (4031611)Instruction limit reached!
% 5.50/1.79 % (4031611)------------------------------
% 5.50/1.79 % (4031611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.06 % (4031611)CaDiCaL version: 2.1.3
% 8.71/2.06 % (4031611)Termination reason: Instruction limit
% 8.71/2.06 % (4031611)Termination phase: Saturation
% 8.71/2.06 % (4031611)Time elapsed: 0.009 s
% 8.71/2.06 % (4031611)Peak memory usage: 88 MB
% 8.71/2.06 % (4031611)Instructions burned: 15 (million)
% 8.71/2.06 % (4031616)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=682609531:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 8.71/2.06 % (4031619)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3096163401:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 8.71/2.06 % (4031619)Instruction limit reached!
% 8.71/2.06 % (4031619)------------------------------
% 8.71/2.06 % (4031619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.06 % (4031619)CaDiCaL version: 2.1.3
% 8.71/2.06 % (4031619)Termination reason: Instruction limit
% 8.71/2.06 % (4031619)Termination phase: Saturation
% 8.71/2.06 % (4031619)Time elapsed: 0.018 s
% 8.71/2.06 % (4031619)Peak memory usage: 90 MB
% 8.71/2.06 % (4031619)Instructions burned: 16 (million)
% 8.71/2.06 % (4031616)Instruction limit reached!
% 8.71/2.06 % (4031616)------------------------------
% 8.71/2.06 % (4031616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.06 % (4031616)CaDiCaL version: 2.1.3
% 8.71/2.06 % (4031616)Termination reason: Instruction limit
% 8.71/2.06 % (4031616)Termination phase: Saturation
% 8.71/2.06 % (4031616)Time elapsed: 0.032 s
% 8.71/2.06 % (4031616)Peak memory usage: 88 MB
% 8.71/2.06 % (4031616)Instructions burned: 29 (million)
% 8.71/2.06 % (4031604)Instruction limit reached!
% 8.71/2.06 % (4031604)------------------------------
% 8.71/2.06 % (4031604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.06 % (4031604)CaDiCaL version: 2.1.3
% 8.71/2.06 % (4031604)Termination reason: Instruction limit
% 8.71/2.06 % (4031604)Termination phase: Saturation
% 8.71/2.06 % (4031604)Time elapsed: 0.277 s
% 8.71/2.06 % (4031604)Peak memory usage: 119 MB
% 8.71/2.06 % (4031604)Instructions burned: 201 (million)
% 8.71/2.06 % (4031620)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2409285739:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 8.71/2.06 % (4031623)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3847038781:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 8.71/2.06 % (4031620)Instruction limit reached!
% 8.71/2.06 % (4031620)------------------------------
% 8.71/2.06 % (4031620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.06 % (4031620)CaDiCaL version: 2.1.3
% 8.71/2.06 % (4031620)Termination reason: Instruction limit
% 8.71/2.06 % (4031620)Termination phase: Saturation
% 8.71/2.06 % (4031620)Time elapsed: 0.019 s
% 8.71/2.06 % (4031620)Peak memory usage: 89 MB
% 8.71/2.06 % (4031620)Instructions burned: 25 (million)
% 8.71/2.06 % (4031603)Instruction limit reached!
% 8.71/2.06 % (4031603)------------------------------
% 8.71/2.06 % (4031603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.06 % (4031603)CaDiCaL version: 2.1.3
% 8.71/2.06 % (4031603)Termination reason: Instruction limit
% 8.71/2.06 % (4031603)Termination phase: Saturation
% 8.71/2.06 % (4031603)Time elapsed: 0.346 s
% 8.71/2.06 % (4031603)Peak memory usage: 117 MB
% 8.71/2.06 % (4031603)Instructions burned: 307 (million)
% 8.71/2.06 % (4031623)Instruction limit reached!
% 8.71/2.06 % (4031623)------------------------------
% 8.71/2.06 % (4031623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.06 % (4031623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.39 % (4031623)CaDiCaL version: 2.1.3
% 9.94/2.39 % (4031623)Termination reason: Instruction limit
% 9.94/2.39 % (4031623)Termination phase: Saturation
% 9.94/2.39 % (4031623)Time elapsed: 0.034 s
% 9.94/2.39 % (4031623)Peak memory usage: 90 MB
% 9.94/2.39 % (4031623)Instructions burned: 27 (million)
% 9.94/2.39 % (4031627)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=530371308:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 9.94/2.39 % (4031638)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=400706073:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.94/2.39 % (4031633)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1086808064:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 9.94/2.39 % (4031633)Instruction limit reached!
% 9.94/2.39 % (4031633)------------------------------
% 9.94/2.39 % (4031633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.39 % (4031633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.39 % (4031633)CaDiCaL version: 2.1.3
% 9.94/2.39 % (4031633)Termination reason: Instruction limit
% 9.94/2.39 % (4031633)Termination phase: Preprocessing 3
% 9.94/2.39 % (4031633)Time elapsed: 0.003 s
% 9.94/2.39 % (4031633)Peak memory usage: 86 MB
% 9.94/2.39 % (4031633)Instructions burned: 2 (million)
% 9.94/2.39 % (4031635)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3187601581:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.94/2.39 % (4031634)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3797020304:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.94/2.39 % (4031627)Instruction limit reached!
% 9.94/2.39 % (4031627)------------------------------
% 9.94/2.39 % (4031627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.39 % (4031627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.39 % (4031627)CaDiCaL version: 2.1.3
% 9.94/2.39 % (4031627)Termination reason: Instruction limit
% 9.94/2.39 % (4031627)Termination phase: Saturation
% 9.94/2.39 % (4031627)Time elapsed: 0.083 s
% 9.94/2.39 % (4031627)Peak memory usage: 89 MB
% 9.94/2.39 % (4031627)Instructions burned: 85 (million)
% 9.94/2.39 % (4031635)Instruction limit reached!
% 9.94/2.39 % (4031635)------------------------------
% 9.94/2.39 % (4031635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.39 % (4031635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.39 % (4031635)CaDiCaL version: 2.1.3
% 9.94/2.39 % (4031635)Termination reason: Instruction limit
% 9.94/2.39 % (4031635)Termination phase: Equality proxy
% 9.94/2.39 % (4031635)Time elapsed: 0.005 s
% 9.94/2.39 % (4031635)Peak memory usage: 86 MB
% 9.94/2.39 % (4031635)Instructions burned: 4 (million)
% 9.94/2.39 % (4031639)lrs+10_1_thi=all:si=on:fd=off:random_seed=225316916:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 9.94/2.39 % (4031639)Instruction limit reached!
% 9.94/2.39 % (4031639)------------------------------
% 9.94/2.39 % (4031639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.39 % (4031639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.39 % (4031639)CaDiCaL version: 2.1.3
% 9.94/2.39 % (4031639)Termination reason: Instruction limit
% 9.94/2.39 % (4031639)Termination phase: Saturation
% 9.94/2.39 % (4031639)Time elapsed: 0.048 s
% 9.94/2.39 % (4031639)Peak memory usage: 116 MB
% 9.94/2.39 % (4031639)Instructions burned: 55 (million)
% 9.94/2.39 % (4031638)Instruction limit reached!
% 9.94/2.39 % (4031638)------------------------------
% 9.94/2.39 % (4031638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.39 % (4031638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.39 % (4031638)CaDiCaL version: 2.1.3
% 9.94/2.39 % (4031638)Termination reason: Instruction limit
% 9.94/2.39 % (4031638)Termination phase: Saturation
% 9.94/2.39 % (4031638)Time elapsed: 0.117 s
% 9.94/2.39 % (4031638)Peak memory usage: 134 MB
% 9.94/2.39 % (4031638)Instructions burned: 66 (million)
% 9.94/2.39 % (4031640)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=1700218981:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.94/2.39 % (4031640)Instruction limit reached!
% 11.32/2.66 % (4031640)------------------------------
% 11.32/2.66 % (4031640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.66 % (4031640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.66 % (4031640)CaDiCaL version: 2.1.3
% 11.32/2.66 % (4031640)Termination reason: Instruction limit
% 11.32/2.66 % (4031640)Termination phase: Saturation
% 11.32/2.66 % (4031640)Time elapsed: 0.010 s
% 11.32/2.66 % (4031640)Peak memory usage: 88 MB
% 11.32/2.66 % (4031640)Instructions burned: 8 (million)
% 11.32/2.66 % (4031634)Instruction limit reached!
% 11.32/2.66 % (4031634)------------------------------
% 11.32/2.66 % (4031634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.66 % (4031634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.66 % (4031634)CaDiCaL version: 2.1.3
% 11.32/2.66 % (4031634)Termination reason: Instruction limit
% 11.32/2.66 % (4031634)Termination phase: Saturation
% 11.32/2.66 % (4031634)Time elapsed: 0.193 s
% 11.32/2.66 % (4031634)Peak memory usage: 91 MB
% 11.32/2.66 % (4031634)Instructions burned: 181 (million)
% 11.32/2.66 % (4031644)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1531136403:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 11.32/2.66 % (4031644)Instruction limit reached!
% 11.32/2.66 % (4031644)------------------------------
% 11.32/2.66 % (4031644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.66 % (4031644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.66 % (4031644)CaDiCaL version: 2.1.3
% 11.32/2.66 % (4031644)Termination reason: Instruction limit
% 11.32/2.66 % (4031644)Termination phase: Preprocessing 3
% 11.32/2.66 % (4031644)Time elapsed: 0.003 s
% 11.32/2.66 % (4031644)Peak memory usage: 86 MB
% 11.32/2.66 % (4031644)Instructions burned: 2 (million)
% 11.32/2.66 % (4031650)dis+10_1_si=on:random_seed=116635948:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.32/2.66 % (4031650)Instruction limit reached!
% 11.32/2.66 % (4031650)------------------------------
% 11.32/2.66 % (4031650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.66 % (4031650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.66 % (4031650)CaDiCaL version: 2.1.3
% 11.32/2.66 % (4031650)Termination reason: Instruction limit
% 11.32/2.66 % (4031650)Termination phase: Saturation
% 11.32/2.66 % (4031650)Time elapsed: 0.008 s
% 11.32/2.66 % (4031650)Peak memory usage: 88 MB
% 11.32/2.66 % (4031650)Instructions burned: 10 (million)
% 11.32/2.66 % (4031647)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1830838429:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.32/2.66 % (4031647)Instruction limit reached!
% 11.32/2.66 % (4031647)------------------------------
% 11.32/2.66 % (4031647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.66 % (4031647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.66 % (4031647)CaDiCaL version: 2.1.3
% 11.32/2.66 % (4031647)Termination reason: Instruction limit
% 11.32/2.66 % (4031647)Termination phase: Preprocessing 3
% 11.32/2.66 % (4031647)Time elapsed: 0.003 s
% 11.32/2.66 % (4031647)Peak memory usage: 86 MB
% 11.32/2.66 % (4031647)Instructions burned: 2 (million)
% 11.32/2.66 % (4031648)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1941517510:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.32/2.66 % (4031651)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=708939668:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.32/2.66 % (4031651)Instruction limit reached!
% 11.32/2.66 % (4031651)------------------------------
% 11.32/2.66 % (4031651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.66 % (4031651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.66 % (4031651)CaDiCaL version: 2.1.3
% 11.32/2.66 % (4031651)Termination reason: Instruction limit
% 11.32/2.66 % (4031651)Termination phase: Saturation
% 11.32/2.66 % (4031651)Time elapsed: 0.016 s
% 11.32/2.66 % (4031651)Peak memory usage: 89 MB
% 11.32/2.66 % (4031651)Instructions burned: 28 (million)
% 11.32/2.66 % (4031653)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=122378406:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi)
% 16.80/3.23 % (4031653)Instruction limit reached!
% 16.80/3.23 % (4031653)------------------------------
% 16.80/3.23 % (4031653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/3.23 % (4031653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/3.23 % (4031653)CaDiCaL version: 2.1.3
% 16.80/3.23 % (4031653)Termination reason: Instruction limit
% 16.80/3.23 % (4031653)Termination phase: Saturation
% 16.80/3.23 % (4031653)Time elapsed: 0.044 s
% 16.80/3.23 % (4031653)Peak memory usage: 89 MB
% 16.80/3.23 % (4031653)Instructions burned: 35 (million)
% 16.80/3.23 % (4031648)Instruction limit reached!
% 16.80/3.23 % (4031648)------------------------------
% 16.80/3.23 % (4031648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/3.23 % (4031648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/3.23 % (4031648)CaDiCaL version: 2.1.3
% 16.80/3.23 % (4031648)Termination reason: Instruction limit
% 16.80/3.23 % (4031648)Termination phase: Saturation
% 16.80/3.23 % (4031648)Time elapsed: 0.183 s
% 16.80/3.23 % (4031648)Peak memory usage: 119 MB
% 16.80/3.23 % (4031648)Instructions burned: 127 (million)
% 16.80/3.23 % (4031654)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=774430420:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 16.80/3.23 % (4031654)Instruction limit reached!
% 16.80/3.23 % (4031654)------------------------------
% 16.80/3.23 % (4031654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/3.23 % (4031654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/3.23 % (4031654)CaDiCaL version: 2.1.3
% 16.80/3.23 % (4031654)Termination reason: Instruction limit
% 16.80/3.23 % (4031654)Termination phase: Preprocessing 3
% 16.80/3.23 % (4031654)Time elapsed: 0.003 s
% 16.80/3.23 % (4031654)Peak memory usage: 86 MB
% 16.80/3.23 % (4031654)Instructions burned: 2 (million)
% 16.80/3.23 % (4031660)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2958161386:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 16.80/3.23 % (4031659)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3413073847:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 16.80/3.23 % (4031657)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2058460965:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi)
% 16.80/3.23 % (4031657)Instruction limit reached!
% 16.80/3.23 % (4031657)------------------------------
% 16.80/3.23 % (4031657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/3.23 % (4031657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/3.23 % (4031657)CaDiCaL version: 2.1.3
% 16.80/3.23 % (4031657)Termination reason: Instruction limit
% 16.80/3.23 % (4031657)Termination phase: Saturation
% 16.80/3.23 % (4031657)Time elapsed: 0.010 s
% 16.80/3.23 % (4031657)Peak memory usage: 88 MB
% 16.80/3.23 % (4031657)Instructions burned: 8 (million)
% 16.80/3.23 % (4031663)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2832462769:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 16.80/3.23 % (4031660)Instruction limit reached!
% 16.80/3.23 % (4031660)------------------------------
% 16.80/3.23 % (4031660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/3.23 % (4031660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/3.23 % (4031660)CaDiCaL version: 2.1.3
% 16.80/3.23 % (4031660)Termination reason: Instruction limit
% 16.80/3.23 % (4031660)Termination phase: Saturation
% 16.80/3.23 % (4031660)Time elapsed: 0.042 s
% 16.80/3.23 % (4031660)Peak memory usage: 112 MB
% 16.80/3.23 % (4031660)Instructions burned: 13 (million)
% 16.80/3.23 % (4031663)Instruction limit reached!
% 16.80/3.23 % (4031663)------------------------------
% 16.80/3.23 % (4031663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/3.23 % (4031663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/3.23 % (4031663)CaDiCaL version: 2.1.3
% 16.80/3.23 % (4031663)Termination reason: Instruction limit
% 16.80/3.23 % (4031663)Termination phase: Saturation
% 16.80/3.23 % (4031663)Time elapsed: 0.138 s
% 16.80/3.23 % (4031663)Peak memory usage: 117 MB
% 16.80/3.23 % (4031663)Instructions burned: 228 (million)
% 16.80/3.23 % (4031665)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2828549435:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 18.06/3.58 % (4031665)Instruction limit reached!
% 18.06/3.58 % (4031665)------------------------------
% 18.06/3.58 % (4031665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.06/3.58 % (4031665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.06/3.58 % (4031665)CaDiCaL version: 2.1.3
% 18.06/3.58 % (4031665)Termination reason: Instruction limit
% 18.06/3.58 % (4031665)Termination phase: Saturation
% 18.06/3.58 % (4031665)Time elapsed: 0.013 s
% 18.06/3.58 % (4031665)Peak memory usage: 88 MB
% 18.06/3.58 % (4031665)Instructions burned: 10 (million)
% 18.06/3.58 % (4031668)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=851545414:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 18.06/3.58 % (4031667)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2174458754:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 18.06/3.58 % (4031672)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=3930153830:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 18.06/3.58 % (4031668)Instruction limit reached!
% 18.06/3.58 % (4031668)------------------------------
% 18.06/3.58 % (4031668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.06/3.58 % (4031668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.06/3.58 % (4031668)CaDiCaL version: 2.1.3
% 18.06/3.58 % (4031668)Termination reason: Instruction limit
% 18.06/3.58 % (4031668)Termination phase: Saturation
% 18.06/3.58 % (4031668)Time elapsed: 0.083 s
% 18.06/3.58 % (4031668)Peak memory usage: 90 MB
% 18.06/3.58 % (4031668)Instructions burned: 75 (million)
% 18.06/3.58 % (4031674)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3696614438:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi)
% 18.06/3.58 % (4031659)Instruction limit reached!
% 18.06/3.58 % (4031659)------------------------------
% 18.06/3.58 % (4031659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.06/3.58 % (4031659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.06/3.58 % (4031659)CaDiCaL version: 2.1.3
% 18.06/3.58 % (4031659)Termination reason: Instruction limit
% 18.06/3.58 % (4031659)Termination phase: Saturation
% 18.06/3.58 % (4031659)Time elapsed: 0.363 s
% 18.06/3.58 % (4031659)Peak memory usage: 91 MB
% 18.06/3.58 % (4031659)Instructions burned: 370 (million)
% 18.06/3.58 % (4031667)Instruction limit reached!
% 18.06/3.58 % (4031667)------------------------------
% 18.06/3.58 % (4031667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.06/3.58 % (4031667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.06/3.58 % (4031667)CaDiCaL version: 2.1.3
% 18.06/3.58 % (4031667)Termination reason: Instruction limit
% 18.06/3.58 % (4031667)Termination phase: Saturation
% 18.06/3.58 % (4031667)Time elapsed: 0.138 s
% 18.06/3.58 % (4031667)Peak memory usage: 133 MB
% 18.06/3.58 % (4031667)Instructions burned: 71 (million)
% 18.06/3.58 % (4031675)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1984790713:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 18.06/3.58 % (4031675)Instruction limit reached!
% 18.06/3.58 % (4031675)------------------------------
% 18.06/3.58 % (4031675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.06/3.58 % (4031675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.06/3.58 % (4031675)CaDiCaL version: 2.1.3
% 18.06/3.58 % (4031675)Termination reason: Instruction limit
% 18.06/3.58 % (4031675)Termination phase: Saturation
% 18.06/3.58 % (4031675)Time elapsed: 0.102 s
% 18.06/3.58 % (4031675)Peak memory usage: 134 MB
% 18.06/3.58 % (4031675)Instructions burned: 132 (million)
% 18.06/3.58 % (4031674)Instruction limit reached!
% 18.06/3.58 % (4031674)------------------------------
% 18.06/3.58 % (4031674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.06/3.58 % (4031674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.06/3.58 % (4031674)CaDiCaL version: 2.1.3
% 18.06/3.58 % (4031674)Termination reason: Instruction limit
% 18.06/3.58 % (4031674)Termination phase: Saturation
% 18.06/3.58 % (4031674)Time elapsed: 0.164 s
% 18.06/3.58 % (4031674)Peak memory usage: 117 MB
% 22.81/4.08 % (4031674)Instructions burned: 130 (million)
% 22.81/4.08 % (4031679)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2158389953:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 22.81/4.08 % (4031685)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=885474648:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 22.81/4.08 % (4031672)Instruction limit reached!
% 22.81/4.08 % (4031672)------------------------------
% 22.81/4.08 % (4031672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.81/4.08 % (4031672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.81/4.08 % (4031672)CaDiCaL version: 2.1.3
% 22.81/4.08 % (4031672)Termination reason: Instruction limit
% 22.81/4.08 % (4031672)Termination phase: Saturation
% 22.81/4.08 % (4031672)Time elapsed: 0.289 s
% 22.81/4.08 % (4031672)Peak memory usage: 92 MB
% 22.81/4.08 % (4031672)Instructions burned: 295 (million)
% 22.81/4.08 % (4031682)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3346144430:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 22.81/4.08 % (4031679)Instruction limit reached!
% 22.81/4.08 % (4031679)------------------------------
% 22.81/4.08 % (4031679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.81/4.08 % (4031679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.81/4.08 % (4031679)CaDiCaL version: 2.1.3
% 22.81/4.08 % (4031679)Termination reason: Instruction limit
% 22.81/4.08 % (4031679)Termination phase: Saturation
% 22.81/4.08 % (4031679)Time elapsed: 0.101 s
% 22.81/4.08 % (4031679)Peak memory usage: 133 MB
% 22.81/4.08 % (4031679)Instructions burned: 40 (million)
% 22.81/4.08 % (4031683)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1803677899:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi)
% 22.81/4.08 % (4031685)Instruction limit reached!
% 22.81/4.08 % (4031685)------------------------------
% 22.81/4.08 % (4031685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.81/4.08 % (4031685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.81/4.08 % (4031685)CaDiCaL version: 2.1.3
% 22.81/4.08 % (4031685)Termination reason: Instruction limit
% 22.81/4.08 % (4031685)Termination phase: Saturation
% 22.81/4.08 % (4031685)Time elapsed: 0.123 s
% 22.81/4.08 % (4031685)Peak memory usage: 117 MB
% 22.81/4.08 % (4031685)Instructions burned: 131 (million)
% 22.81/4.08 % (4031687)dis+10_1_si=on:random_seed=925716406:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 22.81/4.08 % (4031686)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=4188615593:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 22.81/4.08 % (4031690)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4066560241:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 22.81/4.08 % (4031682)Instruction limit reached!
% 22.81/4.08 % (4031682)------------------------------
% 22.81/4.08 % (4031682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.81/4.08 % (4031682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.81/4.08 % (4031682)CaDiCaL version: 2.1.3
% 22.81/4.08 % (4031682)Termination reason: Instruction limit
% 22.81/4.08 % (4031682)Termination phase: Saturation
% 22.81/4.08 % (4031682)Time elapsed: 0.310 s
% 22.81/4.08 % (4031682)Peak memory usage: 91 MB
% 22.81/4.08 % (4031682)Instructions burned: 307 (million)
% 22.81/4.08 % (4031692)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=421453044:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 22.81/4.08 % (4031695)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3324750211:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 22.81/4.08 % (4031695)Instruction limit reached!
% 22.81/4.08 % (4031695)------------------------------
% 22.81/4.08 % (4031695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.81/4.08 % (4031695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.81/4.08 % (4031695)CaDiCaL version: 2.1.3
% 22.81/4.08 % (4031695)Termination reason: Instruction limit
% 22.81/4.08 % (4031695)Termination phase: Saturation
% 24.02/4.57 % (4031695)Time elapsed: 0.096 s
% 24.02/4.57 % (4031695)Peak memory usage: 116 MB
% 24.02/4.57 % (4031695)Instructions burned: 66 (million)
% 24.02/4.57 % (4031686)Instruction limit reached!
% 24.02/4.57 % (4031686)------------------------------
% 24.02/4.57 % (4031686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.57 % (4031686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.57 % (4031686)CaDiCaL version: 2.1.3
% 24.02/4.57 % (4031686)Termination reason: Instruction limit
% 24.02/4.57 % (4031686)Termination phase: Saturation
% 24.02/4.57 % (4031686)Time elapsed: 0.303 s
% 24.02/4.57 % (4031686)Peak memory usage: 117 MB
% 24.02/4.57 % (4031686)Instructions burned: 260 (million)
% 24.02/4.57 % (4031692)Instruction limit reached!
% 24.02/4.57 % (4031692)------------------------------
% 24.02/4.57 % (4031692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.57 % (4031692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.57 % (4031692)CaDiCaL version: 2.1.3
% 24.02/4.57 % (4031692)Termination reason: Instruction limit
% 24.02/4.57 % (4031692)Termination phase: Saturation
% 24.02/4.57 % (4031692)Time elapsed: 0.159 s
% 24.02/4.57 % (4031692)Peak memory usage: 90 MB
% 24.02/4.57 % (4031692)Instructions burned: 141 (million)
% 24.02/4.57 % (4031698)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1031278593:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi)
% 24.02/4.57 % (4031687)Instruction limit reached!
% 24.02/4.57 % (4031687)------------------------------
% 24.02/4.57 % (4031687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.57 % (4031687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.57 % (4031687)CaDiCaL version: 2.1.3
% 24.02/4.57 % (4031687)Termination reason: Instruction limit
% 24.02/4.57 % (4031687)Termination phase: Saturation
% 24.02/4.57 % (4031687)Time elapsed: 0.520 s
% 24.02/4.57 % (4031687)Peak memory usage: 94 MB
% 24.02/4.57 % (4031687)Instructions burned: 1001 (million)
% 24.02/4.57 % (4031690)Instruction limit reached!
% 24.02/4.57 % (4031690)------------------------------
% 24.02/4.57 % (4031690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.57 % (4031690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.57 % (4031690)CaDiCaL version: 2.1.3
% 24.02/4.57 % (4031690)Termination reason: Instruction limit
% 24.02/4.57 % (4031690)Termination phase: Saturation
% 24.02/4.57 % (4031690)Time elapsed: 0.387 s
% 24.02/4.57 % (4031690)Peak memory usage: 93 MB
% 24.02/4.57 % (4031690)Instructions burned: 383 (million)
% 24.02/4.57 % (4031698)Instruction limit reached!
% 24.02/4.57 % (4031698)------------------------------
% 24.02/4.57 % (4031698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.57 % (4031698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.57 % (4031698)CaDiCaL version: 2.1.3
% 24.02/4.57 % (4031698)Termination reason: Instruction limit
% 24.02/4.57 % (4031698)Termination phase: Saturation
% 24.02/4.57 % (4031698)Time elapsed: 0.130 s
% 24.02/4.57 % (4031698)Peak memory usage: 90 MB
% 24.02/4.57 % (4031698)Instructions burned: 121 (million)
% 24.02/4.57 % (4031701)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=2858860187:s2a=on:i=128:s2at=5:ins=3:rtra=on_2976 on theBenchmark for (2976ds/128Mi)
% 24.02/4.57 % (4031703)dis+1010_1_to=kbo:si=on:random_seed=4288993124:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi)
% 24.02/4.57 % (4031702)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=616056527:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi)
% 24.02/4.57 % (4031683)Instruction limit reached!
% 24.02/4.57 % (4031683)------------------------------
% 24.02/4.57 % (4031683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.57 % (4031683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.57 % (4031683)CaDiCaL version: 2.1.3
% 24.02/4.57 % (4031683)Termination reason: Instruction limit
% 24.02/4.57 % (4031683)Termination phase: Saturation
% 24.02/4.57 % (4031683)Time elapsed: 0.715 s
% 24.02/4.57 % (4031683)Peak memory usage: 139 MB
% 24.02/4.57 % (4031683)Instructions burned: 598 (million)
% 24.02/4.57 % (4031702)Instruction limit reached!
% 24.02/4.57 % (4031702)------------------------------
% 24.02/4.57 % (4031702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.80/5.12 % (4031702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.80/5.12 % (4031702)CaDiCaL version: 2.1.3
% 29.80/5.12 % (4031702)Termination reason: Instruction limit
% 29.80/5.12 % (4031702)Termination phase: Saturation
% 29.80/5.12 % (4031702)Time elapsed: 0.074 s
% 29.80/5.12 % (4031702)Peak memory usage: 116 MB
% 29.80/5.12 % (4031702)Instructions burned: 39 (million)
% 29.80/5.12 % (4031705)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1684480543:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi)
% 29.80/5.12 % (4031706)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3056881714:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi)
% 29.80/5.12 % (4031701)Instruction limit reached!
% 29.80/5.12 % (4031701)------------------------------
% 29.80/5.12 % (4031701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.80/5.12 % (4031701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.80/5.12 % (4031701)CaDiCaL version: 2.1.3
% 29.80/5.12 % (4031701)Termination reason: Instruction limit
% 29.80/5.12 % (4031701)Termination phase: Saturation
% 29.80/5.12 % (4031701)Time elapsed: 0.170 s
% 29.80/5.12 % (4031701)Peak memory usage: 117 MB
% 29.80/5.12 % (4031701)Instructions burned: 129 (million)
% 29.80/5.12 % (4031703)Instruction limit reached!
% 29.80/5.12 % (4031703)------------------------------
% 29.80/5.12 % (4031703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.80/5.12 % (4031703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.80/5.12 % (4031703)CaDiCaL version: 2.1.3
% 29.80/5.12 % (4031703)Termination reason: Instruction limit
% 29.80/5.12 % (4031703)Termination phase: Saturation
% 29.80/5.12 % (4031703)Time elapsed: 0.184 s
% 29.80/5.12 % (4031703)Peak memory usage: 91 MB
% 29.80/5.12 % (4031703)Instructions burned: 175 (million)
% 29.80/5.12 % (4031707)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=831751844:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi)
% 29.80/5.12 % (4031705)Instruction limit reached!
% 29.80/5.12 % (4031705)------------------------------
% 29.80/5.12 % (4031705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.80/5.12 % (4031705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.80/5.12 % (4031705)CaDiCaL version: 2.1.3
% 29.80/5.12 % (4031705)Termination reason: Instruction limit
% 29.80/5.12 % (4031705)Termination phase: Saturation
% 29.80/5.12 % (4031705)Time elapsed: 0.204 s
% 29.80/5.12 % (4031705)Peak memory usage: 119 MB
% 29.80/5.12 % (4031705)Instructions burned: 333 (million)
% 29.80/5.12 % (4031711)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4260839393:i=349:rtra=on_2973 on theBenchmark for (2973ds/349Mi)
% 29.80/5.12 % (4031713)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2077130381:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi)
% 29.80/5.12 % (4031715)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2886736174:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi)
% 29.80/5.12 % (4031716)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3661711420:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi)
% 29.80/5.12 % (4031707)Instruction limit reached!
% 29.80/5.12 % (4031707)------------------------------
% 29.80/5.12 % (4031707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.80/5.12 % (4031707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.80/5.12 % (4031707)CaDiCaL version: 2.1.3
% 29.80/5.12 % (4031707)Termination reason: Instruction limit
% 29.80/5.12 % (4031707)Termination phase: Saturation
% 29.80/5.12 % (4031707)Time elapsed: 0.263 s
% 29.80/5.12 % (4031707)Peak memory usage: 135 MB
% 29.80/5.12 % (4031707)Instructions burned: 215 (million)
% 29.80/5.12 % (4031720)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2417737754:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi)
% 29.80/5.12 % (4031713)Instruction limit reached!
% 29.80/5.12 % (4031713)------------------------------
% 29.80/5.12 % (4031713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.80/5.12 % (4031713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.53 % (4031713)CaDiCaL version: 2.1.3
% 31.93/5.53 % (4031713)Termination reason: Instruction limit
% 31.93/5.53 % (4031713)Termination phase: Saturation
% 31.93/5.53 % (4031713)Time elapsed: 0.271 s
% 31.93/5.53 % (4031713)Peak memory usage: 91 MB
% 31.93/5.53 % (4031713)Instructions burned: 296 (million)
% 31.93/5.53 % (4031706)Instruction limit reached!
% 31.93/5.53 % (4031706)------------------------------
% 31.93/5.53 % (4031706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.53 % (4031706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.53 % (4031706)CaDiCaL version: 2.1.3
% 31.93/5.53 % (4031706)Termination reason: Instruction limit
% 31.93/5.53 % (4031706)Termination phase: Saturation
% 31.93/5.53 % (4031706)Time elapsed: 0.556 s
% 31.93/5.53 % (4031706)Peak memory usage: 136 MB
% 31.93/5.53 % (4031706)Instructions burned: 483 (million)
% 31.93/5.53 % (4031711)Instruction limit reached!
% 31.93/5.53 % (4031711)------------------------------
% 31.93/5.53 % (4031711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.53 % (4031711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.53 % (4031711)CaDiCaL version: 2.1.3
% 31.93/5.53 % (4031711)Termination reason: Instruction limit
% 31.93/5.53 % (4031711)Termination phase: Saturation
% 31.93/5.53 % (4031711)Time elapsed: 0.405 s
% 31.93/5.53 % (4031711)Peak memory usage: 119 MB
% 31.93/5.53 % (4031711)Instructions burned: 350 (million)
% 31.93/5.53 % (4031720)Instruction limit reached!
% 31.93/5.53 % (4031720)------------------------------
% 31.93/5.53 % (4031720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.53 % (4031720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.53 % (4031720)CaDiCaL version: 2.1.3
% 31.93/5.53 % (4031720)Termination reason: Instruction limit
% 31.93/5.53 % (4031720)Termination phase: Saturation
% 31.93/5.53 % (4031720)Time elapsed: 0.259 s
% 31.93/5.53 % (4031720)Peak memory usage: 93 MB
% 31.93/5.53 % (4031720)Instructions burned: 485 (million)
% 31.93/5.53 % (4031725)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1318568788:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi)
% 31.93/5.53 % (4031716)Instruction limit reached!
% 31.93/5.53 % (4031716)------------------------------
% 31.93/5.53 % (4031716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.53 % (4031716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.53 % (4031716)CaDiCaL version: 2.1.3
% 31.93/5.53 % (4031716)Termination reason: Instruction limit
% 31.93/5.53 % (4031716)Termination phase: Saturation
% 31.93/5.53 % (4031716)Time elapsed: 0.326 s
% 31.93/5.53 % (4031716)Peak memory usage: 118 MB
% 31.93/5.53 % (4031716)Instructions burned: 281 (million)
% 31.93/5.53 % (4031715)Instruction limit reached!
% 31.93/5.53 % (4031715)------------------------------
% 31.93/5.53 % (4031715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.53 % (4031715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.53 % (4031715)CaDiCaL version: 2.1.3
% 31.93/5.53 % (4031715)Termination reason: Instruction limit
% 31.93/5.53 % (4031715)Termination phase: Saturation
% 31.93/5.53 % (4031715)Time elapsed: 0.366 s
% 31.93/5.53 % (4031715)Peak memory usage: 117 MB
% 31.93/5.53 % (4031715)Instructions burned: 328 (million)
% 31.93/5.53 % (4031727)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1457481851:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi)
% 31.93/5.53 % (4031728)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2370129531:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi)
% 31.93/5.53 % (4031731)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2267751196:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi)
% 31.93/5.53 % (4031729)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=2264582386:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi)
% 31.93/5.53 % (4031732)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3979161812:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi)
% 31.93/5.53 % (4031725)Instruction limit reached!
% 38.74/6.32 % (4031725)------------------------------
% 38.74/6.32 % (4031725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.32 % (4031725)CaDiCaL version: 2.1.3
% 38.74/6.32 % (4031725)Termination reason: Instruction limit
% 38.74/6.32 % (4031725)Termination phase: Saturation
% 38.74/6.32 % (4031725)Time elapsed: 0.299 s
% 38.74/6.32 % (4031725)Peak memory usage: 115 MB
% 38.74/6.32 % (4031725)Instructions burned: 322 (million)
% 38.74/6.32 % (4031733)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3605451507:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi)
% 38.74/6.32 % (4031731)Instruction limit reached!
% 38.74/6.32 % (4031731)------------------------------
% 38.74/6.32 % (4031731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.32 % (4031731)CaDiCaL version: 2.1.3
% 38.74/6.32 % (4031731)Termination reason: Instruction limit
% 38.74/6.32 % (4031731)Termination phase: Saturation
% 38.74/6.32 % (4031731)Time elapsed: 0.218 s
% 38.74/6.32 % (4031731)Peak memory usage: 118 MB
% 38.74/6.32 % (4031731)Instructions burned: 378 (million)
% 38.74/6.32 % (4031727)Instruction limit reached!
% 38.74/6.32 % (4031727)------------------------------
% 38.74/6.32 % (4031727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.32 % (4031727)CaDiCaL version: 2.1.3
% 38.74/6.32 % (4031727)Termination reason: Instruction limit
% 38.74/6.32 % (4031727)Termination phase: Saturation
% 38.74/6.32 % (4031727)Time elapsed: 0.434 s
% 38.74/6.32 % (4031727)Peak memory usage: 118 MB
% 38.74/6.32 % (4031727)Instructions burned: 417 (million)
% 38.74/6.32 % (4031729)Instruction limit reached!
% 38.74/6.32 % (4031729)------------------------------
% 38.74/6.32 % (4031729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.32 % (4031729)CaDiCaL version: 2.1.3
% 38.74/6.32 % (4031729)Termination reason: Instruction limit
% 38.74/6.32 % (4031729)Termination phase: Saturation
% 38.74/6.32 % (4031729)Time elapsed: 0.348 s
% 38.74/6.32 % (4031729)Peak memory usage: 135 MB
% 38.74/6.32 % (4031729)Instructions burned: 276 (million)
% 38.74/6.32 % (4031739)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=140037647:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi)
% 38.74/6.32 % (4031728)Instruction limit reached!
% 38.74/6.32 % (4031728)------------------------------
% 38.74/6.32 % (4031728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.32 % (4031728)CaDiCaL version: 2.1.3
% 38.74/6.32 % (4031728)Termination reason: Instruction limit
% 38.74/6.32 % (4031728)Termination phase: Saturation
% 38.74/6.32 % (4031728)Time elapsed: 0.498 s
% 38.74/6.32 % (4031728)Peak memory usage: 118 MB
% 38.74/6.32 % (4031728)Instructions burned: 471 (million)
% 38.74/6.32 % (4031741)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2939308009:i=359:rtra=on:gtg=exists_top:ss=axioms_2961 on theBenchmark for (2961ds/359Mi)
% 38.74/6.32 % (4031732)Instruction limit reached!
% 38.74/6.32 % (4031732)------------------------------
% 38.74/6.32 % (4031732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.32 % (4031732)CaDiCaL version: 2.1.3
% 38.74/6.32 % (4031732)Termination reason: Instruction limit
% 38.74/6.32 % (4031732)Termination phase: Saturation
% 38.74/6.32 % (4031732)Time elapsed: 0.429 s
% 38.74/6.32 % (4031732)Peak memory usage: 118 MB
% 38.74/6.32 % (4031732)Instructions burned: 387 (million)
% 38.74/6.32 % (4031742)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=526165439:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2961 on theBenchmark for (2961ds/341Mi)
% 38.74/6.32 % (4031733)Instruction limit reached!
% 38.74/6.32 % (4031733)------------------------------
% 38.74/6.32 % (4031733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.74/6.32 % (4031733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/6.93 % (4031733)CaDiCaL version: 2.1.3
% 40.72/6.93 % (4031733)Termination reason: Instruction limit
% 40.72/6.93 % (4031733)Termination phase: Saturation
% 40.72/6.93 % (4031733)Time elapsed: 0.532 s
% 40.72/6.93 % (4031733)Peak memory usage: 93 MB
% 40.72/6.93 % (4031733)Instructions burned: 514 (million)
% 40.72/6.93 % (4031743)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1931631581:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi)
% 40.72/6.93 % (4031746)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2689280834:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/235Mi)
% 40.72/6.93 % (4031741)Instruction limit reached!
% 40.72/6.93 % (4031741)------------------------------
% 40.72/6.93 % (4031741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/6.93 % (4031741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/6.93 % (4031741)CaDiCaL version: 2.1.3
% 40.72/6.93 % (4031741)Termination reason: Instruction limit
% 40.72/6.93 % (4031741)Termination phase: Saturation
% 40.72/6.93 % (4031741)Time elapsed: 0.320 s
% 40.72/6.93 % (4031741)Peak memory usage: 92 MB
% 40.72/6.93 % (4031741)Instructions burned: 359 (million)
% 40.72/6.93 % (4031742)Instruction limit reached!
% 40.72/6.93 % (4031742)------------------------------
% 40.72/6.93 % (4031742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/6.93 % (4031742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/6.93 % (4031742)CaDiCaL version: 2.1.3
% 40.72/6.93 % (4031742)Termination reason: Instruction limit
% 40.72/6.93 % (4031742)Termination phase: Saturation
% 40.72/6.93 % (4031742)Time elapsed: 0.212 s
% 40.72/6.93 % (4031742)Peak memory usage: 120 MB
% 40.72/6.93 % (4031742)Instructions burned: 342 (million)
% 40.72/6.93 % (4031739)Instruction limit reached!
% 40.72/6.93 % (4031739)------------------------------
% 40.72/6.93 % (4031739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/6.93 % (4031739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/6.93 % (4031739)CaDiCaL version: 2.1.3
% 40.72/6.93 % (4031739)Termination reason: Instruction limit
% 40.72/6.93 % (4031739)Termination phase: Saturation
% 40.72/6.93 % (4031739)Time elapsed: 0.403 s
% 40.72/6.93 % (4031739)Peak memory usage: 135 MB
% 40.72/6.93 % (4031739)Instructions burned: 334 (million)
% 40.72/6.93 % (4031747)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4013376833:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi)
% 40.72/6.93 % (4031750)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2537484474:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi)
% 40.72/6.93 % (4031754)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=3068240761:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi)
% 40.72/6.93 % (4031743)Instruction limit reached!
% 40.72/6.93 % (4031743)------------------------------
% 40.72/6.93 % (4031743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/6.93 % (4031743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/6.93 % (4031743)CaDiCaL version: 2.1.3
% 40.72/6.93 % (4031743)Termination reason: Instruction limit
% 40.72/6.93 % (4031743)Termination phase: Saturation
% 40.72/6.93 % (4031743)Time elapsed: 0.284 s
% 40.72/6.93 % (4031743)Peak memory usage: 117 MB
% 40.72/6.93 % (4031743)Instructions burned: 261 (million)
% 40.72/6.93 % (4031746)Instruction limit reached!
% 40.72/6.93 % (4031746)------------------------------
% 40.72/6.93 % (4031746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.72/6.93 % (4031746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.72/6.93 % (4031746)CaDiCaL version: 2.1.3
% 40.72/6.93 % (4031746)Termination reason: Instruction limit
% 40.72/6.93 % (4031746)Termination phase: Saturation
% 40.72/6.93 % (4031746)Time elapsed: 0.286 s
% 40.72/6.93 % (4031746)Peak memory usage: 117 MB
% 40.72/6.93 % (4031746)Instructions burned: 236 (million)
% 40.72/6.93 % (4031753)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=524449650:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi)
% 40.72/6.93 % (4031750)Instruction limit reached!
% 47.14/7.70 % (4031750)------------------------------
% 47.14/7.70 % (4031750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.14/7.70 % (4031750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.14/7.70 % (4031750)CaDiCaL version: 2.1.3
% 47.14/7.70 % (4031750)Termination reason: Instruction limit
% 47.14/7.70 % (4031750)Termination phase: Saturation
% 47.14/7.70 % (4031750)Time elapsed: 0.158 s
% 47.14/7.70 % (4031750)Peak memory usage: 90 MB
% 47.14/7.70 % (4031750)Instructions burned: 146 (million)
% 47.14/7.70 % (4031760)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=122861934:i=1052:rtra=on_2956 on theBenchmark for (2956ds/1052Mi)
% 47.14/7.70 % (4031754)Instruction limit reached!
% 47.14/7.70 % (4031754)------------------------------
% 47.14/7.70 % (4031754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.14/7.70 % (4031754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.14/7.70 % (4031754)CaDiCaL version: 2.1.3
% 47.14/7.70 % (4031754)Termination reason: Instruction limit
% 47.14/7.70 % (4031754)Termination phase: Saturation
% 47.14/7.70 % (4031754)Time elapsed: 0.179 s
% 47.14/7.70 % (4031754)Peak memory usage: 135 MB
% 47.14/7.70 % (4031754)Instructions burned: 277 (million)
% 47.14/7.70 % (4031747)Instruction limit reached!
% 47.14/7.70 % (4031747)------------------------------
% 47.14/7.70 % (4031747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.14/7.70 % (4031747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.14/7.70 % (4031747)CaDiCaL version: 2.1.3
% 47.14/7.70 % (4031747)Termination reason: Instruction limit
% 47.14/7.70 % (4031747)Termination phase: Saturation
% 47.14/7.70 % (4031747)Time elapsed: 0.319 s
% 47.14/7.70 % (4031747)Peak memory usage: 92 MB
% 47.14/7.70 % (4031747)Instructions burned: 273 (million)
% 47.14/7.70 % (4031765)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1234833511:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1054Mi)
% 47.14/7.70 % (4031764)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2278106432:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/655Mi)
% 47.14/7.70 % (4031767)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=274823606:i=107:rtra=on_2953 on theBenchmark for (2953ds/107Mi)
% 47.14/7.70 % (4031770)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 47.14/7.70 % (4031770)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1461702558:i=1090:aac=none:nm=0:rtra=on:rawr=on_2952 on theBenchmark for (2952ds/1090Mi)
% 47.14/7.70 % (4031769)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4159127807:s2a=on:i=450:doe=on:nm=32:rtra=on_2953 on theBenchmark for (2953ds/450Mi)
% 47.14/7.70 % (4031767)Instruction limit reached!
% 47.14/7.70 % (4031767)------------------------------
% 47.14/7.70 % (4031767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.14/7.70 % (4031767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.14/7.70 % (4031767)CaDiCaL version: 2.1.3
% 47.14/7.70 % (4031767)Termination reason: Instruction limit
% 47.14/7.70 % (4031767)Termination phase: Saturation
% 47.14/7.70 % (4031767)Time elapsed: 0.146 s
% 47.14/7.70 % (4031767)Peak memory usage: 117 MB
% 47.14/7.70 % (4031767)Instructions burned: 108 (million)
% 47.14/7.70 % (4031776)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1995536855:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2949 on theBenchmark for (2949ds/130Mi)
% 47.14/7.70 % (4031764)Instruction limit reached!
% 47.14/7.70 % (4031764)------------------------------
% 47.14/7.70 % (4031764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.14/7.70 % (4031764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.14/7.70 % (4031764)CaDiCaL version: 2.1.3
% 47.14/7.70 % (4031764)Termination reason: Instruction limit
% 47.14/7.70 % (4031764)Termination phase: Saturation
% 47.14/7.70 % (4031764)Time elapsed: 0.635 s
% 47.14/7.70 % (4031764)Peak memory usage: 98 MB
% 47.14/7.70 % (4031764)Instructions burned: 655 (million)
% 47.14/7.70 % (4031769)Instruction limit reached!
% 55.75/8.85 % (4031769)------------------------------
% 55.75/8.85 % (4031769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.75/8.85 % (4031769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.75/8.85 % (4031769)CaDiCaL version: 2.1.3
% 55.75/8.85 % (4031769)Termination reason: Instruction limit
% 55.75/8.85 % (4031769)Termination phase: Saturation
% 55.75/8.85 % (4031769)Time elapsed: 0.514 s
% 55.75/8.85 % (4031769)Peak memory usage: 136 MB
% 55.75/8.85 % (4031769)Instructions burned: 451 (million)
% 55.75/8.85 % (4031770)Instruction limit reached!
% 55.75/8.85 % (4031770)------------------------------
% 55.75/8.85 % (4031770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.75/8.85 % (4031770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.75/8.85 % (4031770)CaDiCaL version: 2.1.3
% 55.75/8.85 % (4031770)Termination reason: Instruction limit
% 55.75/8.85 % (4031770)Termination phase: Saturation
% 55.75/8.85 % (4031770)Time elapsed: 0.560 s
% 55.75/8.85 % (4031770)Peak memory usage: 122 MB
% 55.75/8.85 % (4031770)Instructions burned: 1090 (million)
% 55.75/8.85 % (4031776)Instruction limit reached!
% 55.75/8.85 % (4031776)------------------------------
% 55.75/8.85 % (4031776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.75/8.85 % (4031776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.75/8.85 % (4031776)CaDiCaL version: 2.1.3
% 55.75/8.85 % (4031776)Termination reason: Instruction limit
% 55.75/8.85 % (4031776)Termination phase: Saturation
% 55.75/8.85 % (4031776)Time elapsed: 0.162 s
% 55.75/8.85 % (4031776)Peak memory usage: 117 MB
% 55.75/8.85 % (4031776)Instructions burned: 131 (million)
% 55.75/8.85 % (4031780)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=256614583:i=312:kws=inv_frequency:nm=20:rtra=on_2945 on theBenchmark for (2945ds/312Mi)
% 55.75/8.85 % (4031781)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1684296592:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi)
% 55.75/8.85 % (4031783)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2035423442:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2944 on theBenchmark for (2944ds/307Mi)
% 55.75/8.85 % (4031782)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2887354906:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi)
% 55.75/8.85 % (4031760)Instruction limit reached!
% 55.75/8.85 % (4031760)------------------------------
% 55.75/8.85 % (4031760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.75/8.85 % (4031760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.75/8.85 % (4031760)CaDiCaL version: 2.1.3
% 55.75/8.85 % (4031760)Termination reason: Instruction limit
% 55.75/8.85 % (4031760)Termination phase: Saturation
% 55.75/8.85 % (4031760)Time elapsed: 1.056 s
% 55.75/8.85 % (4031760)Peak memory usage: 97 MB
% 55.75/8.85 % (4031760)Instructions burned: 1052 (million)
% 55.75/8.85 % (4031765)Instruction limit reached!
% 55.75/8.85 % (4031765)------------------------------
% 55.75/8.85 % (4031765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.75/8.85 % (4031765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.75/8.85 % (4031765)CaDiCaL version: 2.1.3
% 55.75/8.85 % (4031765)Termination reason: Instruction limit
% 55.75/8.85 % (4031765)Termination phase: Saturation
% 55.75/8.85 % (4031765)Time elapsed: 0.999 s
% 55.75/8.85 % (4031765)Peak memory usage: 98 MB
% 55.75/8.85 % (4031765)Instructions burned: 1055 (million)
% 55.75/8.85 % (4031783)Instruction limit reached!
% 55.75/8.85 % (4031783)------------------------------
% 55.75/8.85 % (4031783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.75/8.85 % (4031783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.75/8.85 % (4031783)CaDiCaL version: 2.1.3
% 55.75/8.85 % (4031783)Termination reason: Instruction limit
% 55.75/8.85 % (4031783)Termination phase: Saturation
% 55.75/8.85 % (4031783)Time elapsed: 0.178 s
% 55.75/8.85 % (4031783)Peak memory usage: 92 MB
% 55.75/8.85 % (4031783)Instructions burned: 307 (million)
% 55.75/8.85 % (4031788)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1876354454:i=776:doe=on:rtra=on_2942 on theBenchmark for (2942ds/776Mi)
% 55.75/8.85 % (4031780)Instruction limit reached!
% 55.75/8.85 % (4031780)------------------------------
% 55.75/8.85 % (4031780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.20/10.25 % (4031780)CaDiCaL version: 2.1.3
% 66.20/10.25 % (4031780)Termination reason: Instruction limit
% 66.20/10.25 % (4031780)Termination phase: Saturation
% 66.20/10.25 % (4031780)Time elapsed: 0.348 s
% 66.20/10.25 % (4031780)Peak memory usage: 117 MB
% 66.20/10.25 % (4031780)Instructions burned: 312 (million)
% 66.20/10.25 % (4031789)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3072709213:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2942 on theBenchmark for (2942ds/646Mi)
% 66.20/10.25 % (4031790)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=3836112126:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2941 on theBenchmark for (2941ds/784Mi)
% 66.20/10.25 % (4031781)Instruction limit reached!
% 66.20/10.25 % (4031781)------------------------------
% 66.20/10.25 % (4031781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.20/10.25 % (4031781)CaDiCaL version: 2.1.3
% 66.20/10.25 % (4031781)Termination reason: Instruction limit
% 66.20/10.25 % (4031781)Termination phase: Saturation
% 66.20/10.25 % (4031781)Time elapsed: 0.447 s
% 66.20/10.25 % (4031781)Peak memory usage: 92 MB
% 66.20/10.25 % (4031781)Instructions burned: 491 (million)
% 66.20/10.25 % (4031793)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=2646687833:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2939 on theBenchmark for (2939ds/1131Mi)
% 66.20/10.25 % (4031798)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3271231236:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2938 on theBenchmark for (2938ds/246Mi)
% 66.20/10.25 % (4031782)Instruction limit reached!
% 66.20/10.25 % (4031782)------------------------------
% 66.20/10.25 % (4031782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.20/10.25 % (4031782)CaDiCaL version: 2.1.3
% 66.20/10.25 % (4031782)Termination reason: Instruction limit
% 66.20/10.25 % (4031782)Termination phase: Saturation
% 66.20/10.25 % (4031782)Time elapsed: 0.865 s
% 66.20/10.25 % (4031782)Peak memory usage: 94 MB
% 66.20/10.25 % (4031782)Instructions burned: 835 (million)
% 66.20/10.25 % (4031790)Instruction limit reached!
% 66.20/10.25 % (4031790)------------------------------
% 66.20/10.25 % (4031790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.20/10.25 % (4031790)CaDiCaL version: 2.1.3
% 66.20/10.25 % (4031790)Termination reason: Instruction limit
% 66.20/10.25 % (4031790)Termination phase: Saturation
% 66.20/10.25 % (4031790)Time elapsed: 0.482 s
% 66.20/10.25 % (4031790)Peak memory usage: 122 MB
% 66.20/10.25 % (4031790)Instructions burned: 785 (million)
% 66.20/10.25 % (4031788)Instruction limit reached!
% 66.20/10.25 % (4031788)------------------------------
% 66.20/10.25 % (4031788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.20/10.25 % (4031788)CaDiCaL version: 2.1.3
% 66.20/10.25 % (4031788)Termination reason: Instruction limit
% 66.20/10.25 % (4031788)Termination phase: Saturation
% 66.20/10.25 % (4031788)Time elapsed: 0.759 s
% 66.20/10.25 % (4031788)Peak memory usage: 124 MB
% 66.20/10.25 % (4031788)Instructions burned: 777 (million)
% 66.20/10.25 % (4031798)Instruction limit reached!
% 66.20/10.25 % (4031798)------------------------------
% 66.20/10.25 % (4031798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.20/10.25 % (4031798)CaDiCaL version: 2.1.3
% 66.20/10.25 % (4031798)Termination reason: Instruction limit
% 66.20/10.25 % (4031798)Termination phase: Saturation
% 66.20/10.25 % (4031798)Time elapsed: 0.295 s
% 66.20/10.25 % (4031798)Peak memory usage: 117 MB
% 66.20/10.25 % (4031798)Instructions burned: 247 (million)
% 66.20/10.25 % (4031789)Instruction limit reached!
% 66.20/10.25 % (4031789)------------------------------
% 66.20/10.25 % (4031789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.20/10.25 % (4031789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.38/13.28 % (4031789)CaDiCaL version: 2.1.3
% 87.38/13.28 % (4031789)Termination reason: Instruction limit
% 87.38/13.28 % (4031789)Termination phase: Saturation
% 87.38/13.28 % (4031789)Time elapsed: 0.757 s
% 87.38/13.28 % (4031789)Peak memory usage: 139 MB
% 87.38/13.28 % (4031789)Instructions burned: 647 (million)
% 87.38/13.28 % (4031802)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1017596095:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/775Mi)
% 87.38/13.28 % (4031803)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3272363130:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2933 on theBenchmark for (2933ds/273Mi)
% 87.38/13.28 % (4031804)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2336132042:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi)
% 87.38/13.28 % (4031803)Instruction limit reached!
% 87.38/13.28 % (4031803)------------------------------
% 87.38/13.28 % (4031803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.38/13.28 % (4031803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.38/13.28 % (4031803)CaDiCaL version: 2.1.3
% 87.38/13.28 % (4031803)Termination reason: Instruction limit
% 87.38/13.28 % (4031803)Termination phase: Saturation
% 87.38/13.28 % (4031803)Time elapsed: 0.167 s
% 87.38/13.28 % (4031803)Peak memory usage: 92 MB
% 87.38/13.28 % (4031803)Instructions burned: 274 (million)
% 87.38/13.28 % (4031805)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=76559428:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2932 on theBenchmark for (2932ds/1094Mi)
% 87.38/13.28 % (4031808)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=655020908:i=6400:doe=on:fsr=off:rtra=on_2931 on theBenchmark for (2931ds/6400Mi)
% 87.38/13.28 % (4031804)Instruction limit reached!
% 87.38/13.28 % (4031804)------------------------------
% 87.38/13.28 % (4031804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.38/13.28 % (4031804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.38/13.28 % (4031804)CaDiCaL version: 2.1.3
% 87.38/13.28 % (4031804)Termination reason: Instruction limit
% 87.38/13.28 % (4031804)Termination phase: Saturation
% 87.38/13.28 % (4031804)Time elapsed: 0.112 s
% 87.38/13.28 % (4031804)Peak memory usage: 89 MB
% 87.38/13.28 % (4031804)Instructions burned: 102 (million)
% 87.38/13.28 % (4031810)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3480450724:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/868Mi)
% 87.38/13.28 % (4031813)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=75747140:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi)
% 87.38/13.28 % (4031793)Instruction limit reached!
% 87.38/13.28 % (4031793)------------------------------
% 87.38/13.28 % (4031793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.38/13.28 % (4031793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.38/13.28 % (4031793)CaDiCaL version: 2.1.3
% 87.38/13.28 % (4031793)Termination reason: Instruction limit
% 87.38/13.28 % (4031793)Termination phase: Saturation
% 87.38/13.28 % (4031793)Time elapsed: 1.164 s
% 87.38/13.28 % (4031793)Peak memory usage: 126 MB
% 87.38/13.28 % (4031793)Instructions burned: 1132 (million)
% 87.38/13.28 % (4031802)Instruction limit reached!
% 87.38/13.28 % (4031802)------------------------------
% 87.38/13.28 % (4031802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.38/13.28 % (4031802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.38/13.28 % (4031802)CaDiCaL version: 2.1.3
% 87.38/13.28 % (4031802)Termination reason: Instruction limit
% 87.38/13.28 % (4031802)Termination phase: Saturation
% 87.38/13.28 % (4031802)Time elapsed: 0.846 s
% 87.38/13.28 % (4031802)Peak memory usage: 95 MB
% 87.38/13.28 % (4031802)Instructions burned: 775 (million)
% 87.38/13.28 % (4031816)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3744477304:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2925 on theBenchmark for (2925ds/36816Mi)
% 87.38/13.28 % (4031817)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1250250252:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/273Mi)
% 89.61/13.78 % (4031805)Instruction limit reached!
% 89.61/13.78 % (4031805)------------------------------
% 89.61/13.78 % (4031805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031805)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031805)Termination reason: Instruction limit
% 89.61/13.78 % (4031805)Termination phase: Saturation
% 89.61/13.78 % (4031805)Time elapsed: 1.059 s
% 89.61/13.78 % (4031805)Peak memory usage: 94 MB
% 89.61/13.78 % (4031805)Instructions burned: 1094 (million)
% 89.61/13.78 % (4031810)Instruction limit reached!
% 89.61/13.78 % (4031810)------------------------------
% 89.61/13.78 % (4031810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031810)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031810)Termination reason: Instruction limit
% 89.61/13.78 % (4031810)Termination phase: Saturation
% 89.61/13.78 % (4031810)Time elapsed: 0.891 s
% 89.61/13.78 % (4031810)Peak memory usage: 120 MB
% 89.61/13.78 % (4031810)Instructions burned: 869 (million)
% 89.61/13.78 % (4031817)Instruction limit reached!
% 89.61/13.78 % (4031817)------------------------------
% 89.61/13.78 % (4031817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031817)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031817)Termination reason: Instruction limit
% 89.61/13.78 % (4031817)Termination phase: Saturation
% 89.61/13.78 % (4031817)Time elapsed: 0.317 s
% 89.61/13.78 % (4031817)Peak memory usage: 92 MB
% 89.61/13.78 % (4031817)Instructions burned: 273 (million)
% 89.61/13.78 % (4031820)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1676686050:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2919 on theBenchmark for (2919ds/863Mi)
% 89.61/13.78 % (4031821)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2623602676:i=5811:kws=precedence:nm=0:rtra=on_2918 on theBenchmark for (2918ds/5811Mi)
% 89.61/13.78 % (4031823)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=2958238228:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2917 on theBenchmark for (2917ds/2216Mi)
% 89.61/13.78 % (4031753)Instruction limit reached!
% 89.61/13.78 % (4031753)------------------------------
% 89.61/13.78 % (4031753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031753)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031753)Termination reason: Instruction limit
% 89.61/13.78 % (4031753)Termination phase: Saturation
% 89.61/13.78 % (4031753)Time elapsed: 4.381 s
% 89.61/13.78 % (4031753)Peak memory usage: 112 MB
% 89.61/13.78 % (4031753)Instructions burned: 4429 (million)
% 89.61/13.78 % (4031813)Instruction limit reached!
% 89.61/13.78 % (4031813)------------------------------
% 89.61/13.78 % (4031813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031813)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031813)Termination reason: Instruction limit
% 89.61/13.78 % (4031813)Termination phase: Saturation
% 89.61/13.78 % (4031813)Time elapsed: 1.706 s
% 89.61/13.78 % (4031813)Peak memory usage: 102 MB
% 89.61/13.78 % (4031813)Instructions burned: 1846 (million)
% 89.61/13.78 % (4031820)Instruction limit reached!
% 89.61/13.78 % (4031820)------------------------------
% 89.61/13.78 % (4031820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031820)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031820)Termination reason: Instruction limit
% 89.61/13.78 % (4031820)Termination phase: Saturation
% 89.61/13.78 % (4031820)Time elapsed: 0.868 s
% 89.61/13.78 % (4031820)Peak memory usage: 120 MB
% 89.61/13.78 % (4031820)Instructions burned: 864 (million)
% 89.61/13.78 % (4031828)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4227704447:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2910 on theBenchmark for (2910ds/801Mi)
% 89.61/13.78 % (4031829)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=272717323:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2909 on theBenchmark for (2909ds/1026Mi)
% 89.61/13.78 % (4031830)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3397070855:i=3509:rtra=on_2907 on theBenchmark for (2907ds/3509Mi)
% 89.61/13.78 % (4031828)Instruction limit reached!
% 89.61/13.78 % (4031828)------------------------------
% 89.61/13.78 % (4031828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031828)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031828)Termination reason: Instruction limit
% 89.61/13.78 % (4031828)Termination phase: Saturation
% 89.61/13.78 % (4031828)Time elapsed: 0.798 s
% 89.61/13.78 % (4031828)Peak memory usage: 100 MB
% 89.61/13.78 % (4031828)Instructions burned: 801 (million)
% 89.61/13.78 % (4031834)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4009406315:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2899 on theBenchmark for (2899ds/2127Mi)
% 89.61/13.78 % (4031808)Instruction limit reached!
% 89.61/13.78 % (4031808)------------------------------
% 89.61/13.78 % (4031808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031808)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031808)Termination reason: Instruction limit
% 89.61/13.78 % (4031808)Termination phase: Saturation
% 89.61/13.78 % (4031808)Time elapsed: 3.308 s
% 89.61/13.78 % (4031808)Peak memory usage: 123 MB
% 89.61/13.78 % (4031808)Instructions burned: 6401 (million)
% 89.61/13.78 % (4031829)Instruction limit reached!
% 89.61/13.78 % (4031829)------------------------------
% 89.61/13.78 % (4031829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031829)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031829)Termination reason: Instruction limit
% 89.61/13.78 % (4031829)Termination phase: Saturation
% 89.61/13.78 % (4031829)Time elapsed: 1.042 s
% 89.61/13.78 % (4031829)Peak memory usage: 98 MB
% 89.61/13.78 % (4031829)Instructions burned: 1026 (million)
% 89.61/13.78 % (4031837)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3999224911:s2a=on:i=3553:nm=0:rtra=on_2895 on theBenchmark for (2895ds/3553Mi)
% 89.61/13.78 % (4031836)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4129363775:i=1959:rtra=on:fsd=on:proc=on_2896 on theBenchmark for (2896ds/1959Mi)
% 89.61/13.78 % (4031823)Instruction limit reached!
% 89.61/13.78 % (4031823)------------------------------
% 89.61/13.78 % (4031823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031823)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031823)Termination reason: Instruction limit
% 89.61/13.78 % (4031823)Termination phase: Saturation
% 89.61/13.78 % (4031823)Time elapsed: 2.148 s
% 89.61/13.78 % (4031823)Peak memory usage: 135 MB
% 89.61/13.78 % (4031823)Instructions burned: 2217 (million)
% 89.61/13.78 % (4031840)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3049251535:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/3201Mi)
% 89.61/13.78 % (4031834)Instruction limit reached!
% 89.61/13.78 % (4031834)------------------------------
% 89.61/13.78 % (4031834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031834)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031834)Termination reason: Instruction limit
% 89.61/13.78 % (4031834)Termination phase: Saturation
% 89.61/13.78 % (4031834)Time elapsed: 1.789 s
% 89.61/13.78 % (4031834)Peak memory usage: 107 MB
% 89.61/13.78 % (4031834)Instructions burned: 2128 (million)
% 89.61/13.78 % (4031843)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=1420699966:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2878 on theBenchmark for (2878ds/4093Mi)
% 89.61/13.78 % (4031837)Instruction limit reached!
% 89.61/13.78 % (4031837)------------------------------
% 89.61/13.78 % (4031837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031837)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031837)Termination reason: Instruction limit
% 89.61/13.78 % (4031837)Termination phase: Saturation
% 89.61/13.78 % (4031837)Time elapsed: 1.777 s
% 89.61/13.78 % (4031837)Peak memory usage: 102 MB
% 89.61/13.78 % (4031837)Instructions burned: 3554 (million)
% 89.61/13.78 % (4031836)Instruction limit reached!
% 89.61/13.78 % (4031836)------------------------------
% 89.61/13.78 % (4031836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031836)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031836)Termination reason: Instruction limit
% 89.61/13.78 % (4031836)Termination phase: Saturation
% 89.61/13.78 % (4031836)Time elapsed: 1.827 s
% 89.61/13.78 % (4031836)Peak memory usage: 127 MB
% 89.61/13.78 % (4031836)Instructions burned: 1960 (million)
% 89.61/13.78 % (4031910)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=829712371:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2876 on theBenchmark for (2876ds/21173Mi)
% 89.61/13.78 % (4031921)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4097847959:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2875 on theBenchmark for (2875ds/10544Mi)
% 89.61/13.78 % (4031843)First to succeed.
% 89.61/13.78 % (4031843)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4031597"
% 89.61/13.78 % (4031830)Instruction limit reached!
% 89.61/13.78 % (4031830)------------------------------
% 89.61/13.78 % (4031830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.61/13.78 % (4031830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.61/13.78 % (4031830)CaDiCaL version: 2.1.3
% 89.61/13.78 % (4031830)Termination reason: Instruction limit
% 89.61/13.78 % (4031830)Termination phase: Saturation
% 89.61/13.78 % (4031830)Time elapsed: 3.164 s
% 89.61/13.78 % (4031830)Peak memory usage: 108 MB
% 89.61/13.78 % (4031830)Instructions burned: 3510 (million)
% 89.61/13.78 % (4031969)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3199228987:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2872 on theBenchmark for (2872ds/1262Mi)
% 89.61/13.78 % (4031843)Refutation found. Thanks to Tanya!
% 89.61/13.78 % SZS status Theorem for theBenchmark
% 89.61/13.78 % SZS output start Proof for theBenchmark
% See solution above
% 91.82/14.01 % (4031843)------------------------------
% 91.82/14.01 % (4031843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.82/14.01 % (4031843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.82/14.01 % (4031843)CaDiCaL version: 2.1.3
% 91.82/14.01 % (4031843)Termination reason: Refutation
% 91.82/14.01 % (4031843)Time elapsed: 0.316 s
% 91.82/14.01 % (4031843)Peak memory usage: 137 MB
% 91.82/14.01 % (4031843)Instructions burned: 453 (million)
% 91.82/14.01 % (4031843)------------------------------
% 91.82/14.01 % (4031843)------------------------------
% 91.82/14.01 % (4031597)Success in time 12.883 s
% 91.82/14.01 % Vampire exiting
%------------------------------------------------------------------------------