%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM800^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 : Wed Sep 30 08:18:56 AM UTC 2026
% Result : Theorem 41.57s 6.33s
% Output : Refutation 41.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 12
% Syntax : Number of formulae : 74 ( 31 unt; 0 typ; 6 def)
% Number of atoms : 169 ( 70 equ; 0 cnn)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 623 ( 104 ~; 87 |; 2 &; 424 @)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 417 ( 417 >; 0 *; 0 +; 0 <<)
% Number of symbols : 52 ( 50 usr; 7 con; 0-4 aty)
% Number of variables : 285 ( 12 sgn 26 !; 2 ?; 285 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
zero: ( $i > $i ) > $i > $i ).
thf(func_def_1,type,
one: ( $i > $i ) > $i > $i ).
thf(func_def_2,type,
two: ( $i > $i ) > $i > $i ).
thf(func_def_3,type,
three: ( $i > $i ) > $i > $i ).
thf(func_def_4,type,
four: ( $i > $i ) > $i > $i ).
thf(func_def_5,type,
five: ( $i > $i ) > $i > $i ).
thf(func_def_6,type,
six: ( $i > $i ) > $i > $i ).
thf(func_def_7,type,
seven: ( $i > $i ) > $i > $i ).
thf(func_def_8,type,
eight: ( $i > $i ) > $i > $i ).
thf(func_def_9,type,
nine: ( $i > $i ) > $i > $i ).
thf(func_def_10,type,
ten: ( $i > $i ) > $i > $i ).
thf(func_def_11,type,
succ: ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ).
thf(func_def_12,type,
plus: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ).
thf(func_def_13,type,
mult: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ).
thf(func_def_15,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_16,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_17,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_18,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_19,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_23,type,
sK1: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i > $i ).
thf(func_def_24,type,
sK2: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i ).
thf(func_def_25,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_26,type,
sK3: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > $i > $i ).
thf(func_def_27,type,
sK4: $i > $i ).
thf(func_def_29,type,
sK6: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i > $i ).
thf(func_def_30,type,
sK7: $i > $i ).
thf(func_def_31,type,
sK8: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > $i > $i ).
thf(func_def_33,type,
sK10: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > $i > $i ).
thf(func_def_34,type,
sK11: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i ).
thf(func_def_35,type,
sK12: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i > $i ).
thf(func_def_36,type,
sK13: $i > $i ).
thf(func_def_37,type,
sK14: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > $i ).
thf(func_def_38,type,
sK15: $i > $i ).
thf(func_def_39,type,
sK16: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i ).
thf(func_def_40,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_41,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_42,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_44,type,
sK18: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > $i ).
thf(func_def_45,type,
sK19: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i ).
thf(func_def_46,type,
sK20: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > $i ).
thf(func_def_47,type,
sK21: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i > $i ) > $i > $i ).
thf(func_def_49,type,
sK23: ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i > $i ) > ( ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i ) > $i > $i ).
thf(func_def_50,type,
sK24: $i > $i ).
thf(f2,axiom,
( ( ^ [X0: $i > $i,X1: $i] : ( X0 @ X1 ) )
= one ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM006^0.ax',one_ax) ).
thf(f3,axiom,
( ( ^ [X0: $i > $i,X1: $i] : ( X0 @ ( X0 @ X1 ) ) )
= two ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM006^0.ax',two_ax) ).
thf(f4,axiom,
( ( ^ [X0: $i > $i,X1: $i] : ( X0 @ ( X0 @ ( X0 @ X1 ) ) ) )
= three ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM006^0.ax',three_ax) ).
thf(f7,axiom,
( ( ^ [X0: $i > $i,X1: $i] : ( X0 @ ( X0 @ ( X0 @ ( X0 @ ( X0 @ ( X0 @ X1 ) ) ) ) ) ) )
= six ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM006^0.ax',six_ax) ).
thf(f14,axiom,
( ( ^ [X0: ( $i > $i ) > $i > $i,X1: ( $i > $i ) > $i > $i,X2: $i > $i,X3: $i] : ( X0 @ ( X1 @ X2 ) @ X3 ) )
= mult ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM006^0.ax',mult_ax) ).
thf(f15,conjecture,
? [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( ( X0 @ two @ three )
= six )
& ( ( X0 @ one @ two )
= two ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm) ).
thf(f16,negated_conjecture,
~ ? [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( ( X0 @ two @ three )
= six )
& ( ( X0 @ one @ two )
= two ) ),
inference(negated_conjecture,[status(cth)],[f15]) ).
thf(f19,plain,
( mult
= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i,Y3: $i] : ( Y0 @ ( Y1 @ Y2 ) @ Y3 ) ) ),
inference(fool_elimination,[],[f14]) ).
thf(f20,plain,
( six
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f7]) ).
thf(f23,plain,
( three
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ),
inference(fool_elimination,[],[f4]) ).
thf(f28,plain,
( one
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ Y1 ) ) ),
inference(fool_elimination,[],[f2]) ).
thf(f29,plain,
( two
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f31,plain,
! [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( six
!= ( X0 @ two @ three ) )
| ( two
!= ( X0 @ one @ two ) ) ),
inference(ennf_transformation,[],[f16]) ).
thf(f37,plain,
! [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( two
!= ( X0 @ one @ two ) )
| ( six
!= ( X0 @ two @ three ) ) ),
inference(cnf_transformation,[],[f31]) ).
thf(f38,plain,
( one
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ Y1 ) ) ),
inference(cnf_transformation,[],[f28]) ).
thf(f41,plain,
( three
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[],[f23]) ).
thf(f42,plain,
( six
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f20]) ).
thf(f45,plain,
( mult
= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i,Y3: $i] : ( Y0 @ ( Y1 @ Y2 ) @ Y3 ) ) ),
inference(cnf_transformation,[],[f19]) ).
thf(f46,plain,
( two
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f29]) ).
thf(f47,plain,
( one
= ( ^ [Y0: $i > $i] : Y0 ) ),
inference(beta-eta_normalization,[],[f38]) ).
thf(f48,plain,
( mult
= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i] : ( Y0 @ ( Y1 @ Y2 ) ) ) ),
inference(beta-eta_normalization,[],[f45]) ).
thf(f55,definition,
( spl0_2
<=> ( one
= ( ^ [Y0: $i > $i] : Y0 ) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
thf(f57,plain,
( ( one
= ( ^ [Y0: $i > $i] : Y0 ) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f55]) ).
thf(f58,plain,
spl0_2,
inference(avatar_split_clause,[],[f47,f55]) ).
thf(f65,definition,
( spl0_4
<=> ( three
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
thf(f67,plain,
( ( three
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f65]) ).
thf(f68,plain,
spl0_4,
inference(avatar_split_clause,[],[f41,f65]) ).
thf(f80,definition,
( spl0_7
<=> ( six
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
thf(f82,plain,
( ( six
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f80]) ).
thf(f83,plain,
spl0_7,
inference(avatar_split_clause,[],[f42,f80]) ).
thf(f85,definition,
( spl0_8
<=> ( two
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
thf(f87,plain,
( ( two
= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f85]) ).
thf(f88,plain,
spl0_8,
inference(avatar_split_clause,[],[f46,f85]) ).
thf(f105,definition,
( spl0_12
<=> ( mult
= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i] : ( Y0 @ ( Y1 @ Y2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
thf(f107,plain,
( ( mult
= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i] : ( Y0 @ ( Y1 @ Y2 ) ) ) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f105]) ).
thf(f108,plain,
spl0_12,
inference(avatar_split_clause,[],[f48,f105]) ).
thf(f132,plain,
( ! [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( six
!= ( X0 @ two @ three ) )
| ( two
!= ( X0
@ ^ [Y0: $i > $i] : Y0
@ two ) ) )
| ~ spl0_2 ),
inference(forward_demodulation,[],[f37,f57]) ).
thf(f133,plain,
( ! [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( six
!= ( X0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ three ) )
| ( two
!= ( X0
@ ^ [Y0: $i > $i] : Y0
@ two ) ) )
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f132,f87]) ).
thf(f134,plain,
( ! [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( six
!= ( X0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) )
| ( two
!= ( X0
@ ^ [Y0: $i > $i] : Y0
@ two ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f133,f67]) ).
thf(f135,plain,
( ! [X0: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( ( X0
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) )
| ( six
!= ( X0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f134,f87]) ).
thf(f137,plain,
( ! [X3: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i,X4: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i] :
( ( six
!= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i,Y3: $i] : ( Y0 @ ( X4 @ Y0 @ Y1 @ Y2 @ Y3 ) @ ( X3 @ Y0 @ Y1 @ Y2 @ Y3 ) )
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) )
| ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i,Y3: $i] : ( Y0 @ ( X4 @ Y0 @ Y1 @ Y2 @ Y3 ) @ ( X3 @ Y0 @ Y1 @ Y2 @ Y3 ) )
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_8 ),
inference(projection,[],[f135]) ).
thf(f141,plain,
( ! [X3: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i,X4: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i] :
( ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] :
( X4
@ ^ [Y2: $i > $i] : Y2
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ Y0
@ Y1
@ ( X3
@ ^ [Y2: $i > $i] : Y2
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ Y0
@ Y1 ) ) ) )
| ( six
!= ( ^ [Y0: $i > $i,Y1: $i] :
( X4
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1
@ ( X4
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1
@ ( X3
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1 ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_8 ),
inference(beta-eta_normalization,[],[f137]) ).
thf(f167,plain,
( ! [X1: ( $i > $i ) > $i > $i] :
( ( mult @ X1 )
= ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: ( $i > $i ) > $i > $i,Y2: $i > $i] : ( Y0 @ ( Y1 @ Y2 ) )
@ X1 ) )
| ~ spl0_12 ),
inference(argument_congruence,[],[f107]) ).
thf(f168,plain,
( ! [X1: ( $i > $i ) > $i > $i] :
( ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: $i > $i] : ( X1 @ ( Y0 @ Y1 ) ) )
= ( mult @ X1 ) )
| ~ spl0_12 ),
inference(beta-eta_normalization,[],[f167]) ).
thf(f169,plain,
( ! [X3: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i,X4: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i > $i] :
( ( ( ^ [Y0: $i > $i,Y1: $i] :
( X4
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1
@ ( X4
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1
@ ( X3
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1 ) ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) )
| ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] :
( X4
@ ^ [Y2: $i > $i] : Y2
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ Y0
@ Y1
@ ( X3
@ ^ [Y2: $i > $i] : Y2
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ Y0
@ Y1 ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f141,f82]) ).
thf(f176,plain,
( ! [X3: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] :
( ^ [Y2: ( $i > $i ) > $i > $i,Y3: ( $i > $i ) > $i > $i,Y4: $i > $i,Y5: $i,Y6: $i] : Y6
@ ^ [Y2: $i > $i] : Y2
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ Y0
@ Y1
@ ( X3
@ ^ [Y2: $i > $i] : Y2
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ Y0
@ Y1 ) ) ) )
| ( ( ^ [Y0: $i > $i,Y1: $i] :
( ^ [Y2: ( $i > $i ) > $i > $i,Y3: ( $i > $i ) > $i > $i,Y4: $i > $i,Y5: $i,Y6: $i] : Y6
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1
@ ( ^ [Y2: ( $i > $i ) > $i > $i,Y3: ( $i > $i ) > $i > $i,Y4: $i > $i,Y5: $i,Y6: $i] : Y6
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1
@ ( X3
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ Y3 ) )
@ ^ [Y2: $i > $i,Y3: $i] : ( Y2 @ ( Y2 @ ( Y2 @ Y3 ) ) )
@ Y0
@ Y1 ) ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8 ),
inference(projection,[],[f169]) ).
thf(f185,plain,
( ! [X3: ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i] :
( ( ( X3
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) )
| ( ( X3
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8 ),
inference(beta-eta_normalization,[],[f176]) ).
thf(f228,plain,
( ! [X2: ( $i > $i ) > $i > $i,X1: ( $i > $i ) > $i > $i] :
( ( ^ [Y0: ( $i > $i ) > $i > $i,Y1: $i > $i] : ( X1 @ ( Y0 @ Y1 ) )
@ X2 )
= ( mult @ X1 @ X2 ) )
| ~ spl0_12 ),
inference(argument_congruence,[],[f168]) ).
thf(f229,plain,
( ! [X2: ( $i > $i ) > $i > $i,X1: ( $i > $i ) > $i > $i] :
( ( mult @ X1 @ X2 )
= ( ^ [Y0: $i > $i] : ( X1 @ ( X2 @ Y0 ) ) ) )
| ~ spl0_12 ),
inference(beta-eta_normalization,[],[f228]) ).
thf(f248,plain,
( ! [X2: ( $i > $i ) > $i > $i,X3: $i > $i,X1: ( $i > $i ) > $i > $i] :
( ( ^ [Y0: $i > $i] : ( X1 @ ( X2 @ Y0 ) )
@ X3 )
= ( mult @ X1 @ X2 @ X3 ) )
| ~ spl0_12 ),
inference(argument_congruence,[],[f229]) ).
thf(f250,plain,
( ( ( ^ [Y0: $i > $i] :
( ^ [Y1: $i > $i,Y2: $i] : ( Y1 @ ( Y1 @ Y2 ) )
@ ( ^ [Y1: $i > $i,Y2: $i] : ( Y1 @ ( Y1 @ ( Y1 @ Y2 ) ) )
@ Y0 ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) )
| ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8
| ~ spl0_12 ),
inference(superposition,[],[f185,f229]) ).
thf(f251,plain,
( ! [X2: ( $i > $i ) > $i > $i,X3: $i > $i,X1: ( $i > $i ) > $i > $i] :
( ( X1 @ ( X2 @ X3 ) )
= ( mult @ X1 @ X2 @ X3 ) )
| ~ spl0_12 ),
inference(beta-eta_normalization,[],[f248]) ).
thf(f254,plain,
( ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) )
| ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8
| ~ spl0_12 ),
inference(beta-eta_normalization,[],[f250]) ).
thf(f255,plain,
( ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f254]) ).
thf(f258,definition,
( spl0_19
<=> ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
= ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
thf(f260,plain,
( ( ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) )
!= ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) ) ) )
| spl0_19 ),
inference(avatar_component_clause,[],[f258]) ).
thf(f261,plain,
( ~ spl0_19
| ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f255,f105,f85,f80,f65,f55,f258]) ).
thf(f456,plain,
( ( ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ sK24 )
!= ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ sK24 ) )
| spl0_19 ),
inference(negative_extensionality,[],[f260]) ).
thf(f461,plain,
( ( ( mult
@ ^ [Y0: $i > $i] : Y0
@ ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ sK24 )
!= ( ^ [Y0: $i] : ( sK24 @ ( sK24 @ Y0 ) ) ) )
| spl0_19 ),
inference(beta-eta_normalization,[],[f456]) ).
thf(f462,plain,
( ( ( ^ [Y0: $i] : ( sK24 @ ( sK24 @ Y0 ) ) )
!= ( ^ [Y0: $i > $i] : Y0
@ ( ^ [Y0: $i > $i,Y1: $i] : ( Y0 @ ( Y0 @ Y1 ) )
@ sK24 ) ) )
| ~ spl0_12
| spl0_19 ),
inference(forward_demodulation,[],[f461,f251]) ).
thf(f463,plain,
( ( ( ^ [Y0: $i] : ( sK24 @ ( sK24 @ Y0 ) ) )
!= ( ^ [Y0: $i] : ( sK24 @ ( sK24 @ Y0 ) ) ) )
| ~ spl0_12
| spl0_19 ),
inference(beta-eta_normalization,[],[f462]) ).
thf(f464,plain,
( $false
| ~ spl0_12
| spl0_19 ),
inference(trivial_inequality_removal,[],[f463]) ).
thf(f465,plain,
( ~ spl0_12
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f464]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f58]) ).
cnf(s4,plain,
spl0_4,
inference(sat_conversion,[],[f68]) ).
cnf(s7,plain,
spl0_7,
inference(sat_conversion,[],[f83]) ).
cnf(s8,plain,
spl0_8,
inference(sat_conversion,[],[f88]) ).
cnf(s12,plain,
spl0_12,
inference(sat_conversion,[],[f108]) ).
cnf(s18,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_7
| ~ spl0_8
| ~ spl0_12
| ~ spl0_19 ),
inference(sat_conversion,[],[f261]) ).
cnf(s32,plain,
( ~ spl0_12
| spl0_19 ),
inference(sat_conversion,[],[f465]) ).
cnf(s33,plain,
spl0_19,
inference(rat,[],[s32,s12]) ).
cnf(s34,plain,
~ spl0_2,
inference(rat,[],[s18,s33,s12,s8,s7,s4]) ).
cnf(s35,plain,
$false,
inference(rat,[],[s2,s34]) ).
thf(f466,plain,
$false,
inference(avatar_sat_refutation,[],[s35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM800^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.28 % Computer : n020.cluster.edu
% 0.11/0.28 % Model : x86_64 x86_64
% 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.28 % Memory : 8046.5625MB
% 0.11/0.28 % OS : Linux 6.8.0-71-generic
% 0.11/0.28 % CPULimit : 300
% 0.11/0.28 % WCLimit : 300
% 0.11/0.28 % DateTime : Tue Sep 29 13:01:19 UTC 2026
% 0.11/0.28 % CPUTime :
% 0.11/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.33 Running higher-order theorem proving
% 0.28/0.36 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.07/0.57 % (1011458)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.07/0.57 % (1011468)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2392244817:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.07/0.57 % (1011469)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.07/0.57 % (1011469)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.07/0.57 % (1011464)lrs+10_16_si=on:nwc=1.5:random_seed=1119971260:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.07/0.57 % (1011463)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1160002379:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.07/0.57 % (1011465)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=726598040:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.07/0.57 % (1011467)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3436166634:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.07/0.57 % (1011466)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=4201593616:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 1.07/0.57 % (1011469)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=1093518484:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.07/0.57 % (1011465)Instruction limit reached!
% 1.07/0.57 % (1011465)------------------------------
% 1.07/0.57 % (1011465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.57 % (1011465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.57 % (1011465)CaDiCaL version: 2.1.3
% 1.07/0.57 % (1011465)Termination reason: Instruction limit
% 1.07/0.57 % (1011465)Termination phase: Saturation
% 1.07/0.57 % (1011465)Time elapsed: 0.003 s
% 1.07/0.57 % (1011465)Peak memory usage: 11 MB
% 1.07/0.57 % (1011465)Instructions burned: 3 (million)
% 1.07/0.57 % (1011464)Instruction limit reached!
% 1.07/0.57 % (1011464)------------------------------
% 1.07/0.57 % (1011464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.57 % (1011464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.57 % (1011464)CaDiCaL version: 2.1.3
% 1.07/0.57 % (1011464)Termination reason: Instruction limit
% 1.07/0.57 % (1011464)Termination phase: Saturation
% 1.07/0.57 % (1011464)Time elapsed: 0.014 s
% 1.07/0.57 % (1011464)Peak memory usage: 11 MB
% 1.07/0.57 % (1011464)Instructions burned: 18 (million)
% 1.07/0.57 % (1011468)Instruction limit reached!
% 1.07/0.57 % (1011468)------------------------------
% 1.07/0.57 % (1011468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.57 % (1011468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.57 % (1011468)CaDiCaL version: 2.1.3
% 1.07/0.57 % (1011468)Termination reason: Instruction limit
% 1.07/0.57 % (1011468)Termination phase: Saturation
% 1.07/0.57 % (1011468)Time elapsed: 0.030 s
% 1.07/0.57 % (1011468)Peak memory usage: 12 MB
% 1.07/0.57 % (1011468)Instructions burned: 77 (million)
% 1.07/0.57 % (1011467)Instruction limit reached!
% 1.07/0.57 % (1011467)------------------------------
% 1.07/0.57 % (1011467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.57 % (1011467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.57 % (1011467)CaDiCaL version: 2.1.3
% 1.07/0.57 % (1011467)Termination reason: Instruction limit
% 1.07/0.57 % (1011467)Termination phase: Saturation
% 1.07/0.57 % (1011467)Time elapsed: 0.022 s
% 1.07/0.57 % (1011467)Peak memory usage: 12 MB
% 1.07/0.57 % (1011467)Instructions burned: 25 (million)
% 1.07/0.57 % (1011477)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2309667919:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.07/0.57 % (1011479)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.83/0.64 % (1011478)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3741813898:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.83/0.64 % (1011477)Instruction limit reached!
% 1.83/0.64 % (1011477)------------------------------
% 1.83/0.64 % (1011477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.64 % (1011477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.64 % (1011477)CaDiCaL version: 2.1.3
% 1.83/0.64 % (1011477)Termination reason: Instruction limit
% 1.83/0.64 % (1011477)Termination phase: Function definition elimination
% 1.83/0.64 % (1011477)Time elapsed: 0.006 s
% 1.83/0.64 % (1011477)Peak memory usage: 10 MB
% 1.83/0.64 % (1011477)Instructions burned: 2 (million)
% 1.83/0.64 % (1011479)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4019443376:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.83/0.64 % (1011478)Instruction limit reached!
% 1.83/0.64 % (1011478)------------------------------
% 1.83/0.64 % (1011478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.64 % (1011478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.64 % (1011478)CaDiCaL version: 2.1.3
% 1.83/0.64 % (1011478)Termination reason: Instruction limit
% 1.83/0.64 % (1011478)Termination phase: Saturation
% 1.83/0.64 % (1011478)Time elapsed: 0.005 s
% 1.83/0.64 % (1011478)Peak memory usage: 11 MB
% 1.83/0.64 % (1011478)Instructions burned: 5 (million)
% 1.83/0.64 % (1011480)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=4292354511:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.83/0.64 % (1011479)Instruction limit reached!
% 1.83/0.64 % (1011479)------------------------------
% 1.83/0.64 % (1011479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.64 % (1011479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.64 % (1011479)CaDiCaL version: 2.1.3
% 1.83/0.64 % (1011479)Termination reason: Instruction limit
% 1.83/0.64 % (1011479)Termination phase: Saturation
% 1.83/0.64 % (1011479)Time elapsed: 0.007 s
% 1.83/0.64 % (1011479)Peak memory usage: 12 MB
% 1.83/0.64 % (1011479)Instructions burned: 7 (million)
% 1.83/0.64 % (1011480)Instruction limit reached!
% 1.83/0.64 % (1011480)------------------------------
% 1.83/0.64 % (1011480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.64 % (1011480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.64 % (1011480)CaDiCaL version: 2.1.3
% 1.83/0.64 % (1011480)Termination reason: Instruction limit
% 1.83/0.64 % (1011480)Termination phase: Saturation
% 1.83/0.64 % (1011480)Time elapsed: 0.011 s
% 1.83/0.64 % (1011480)Peak memory usage: 12 MB
% 1.83/0.64 % (1011480)Instructions burned: 13 (million)
% 1.83/0.64 % (1011484)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.83/0.64 % (1011484)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.83/0.64 % (1011484)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3531304386:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 1.83/0.64 % (1011463)Instruction limit reached!
% 1.83/0.64 % (1011463)------------------------------
% 1.83/0.64 % (1011463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.64 % (1011463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.64 % (1011463)CaDiCaL version: 2.1.3
% 1.83/0.64 % (1011463)Termination reason: Instruction limit
% 1.83/0.64 % (1011463)Termination phase: Saturation
% 1.83/0.64 % (1011463)Time elapsed: 0.077 s
% 1.83/0.64 % (1011463)Peak memory usage: 16 MB
% 1.83/0.64 % (1011463)Instructions burned: 88 (million)
% 1.83/0.64 % (1011484)Instruction limit reached!
% 1.83/0.64 % (1011484)------------------------------
% 1.83/0.64 % (1011484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.64 % (1011484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.64 % (1011484)CaDiCaL version: 2.1.3
% 1.83/0.64 % (1011484)Termination reason: Instruction limit
% 2.09/0.69 % (1011484)Termination phase: Saturation
% 2.09/0.69 % (1011484)Time elapsed: 0.012 s
% 2.09/0.69 % (1011484)Peak memory usage: 12 MB
% 2.09/0.69 % (1011484)Instructions burned: 30 (million)
% 2.09/0.69 % (1011486)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=222774782:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 2.09/0.69 % (1011487)lrs+10_1_si=on:cs=on:random_seed=3772769624:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.09/0.69 % (1011488)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.09/0.69 % (1011487)Instruction limit reached!
% 2.09/0.69 % (1011487)------------------------------
% 2.09/0.69 % (1011487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.69 % (1011487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.69 % (1011487)CaDiCaL version: 2.1.3
% 2.09/0.69 % (1011487)Termination reason: Instruction limit
% 2.09/0.69 % (1011487)Termination phase: Saturation
% 2.09/0.69 % (1011487)Time elapsed: 0.007 s
% 2.09/0.69 % (1011487)Peak memory usage: 12 MB
% 2.09/0.69 % (1011487)Instructions burned: 8 (million)
% 2.09/0.69 % (1011491)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=338843615:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.09/0.69 % (1011488)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1223404008:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.09/0.69 % (1011488)Instruction limit reached!
% 2.09/0.69 % (1011488)------------------------------
% 2.09/0.69 % (1011488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.69 % (1011488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.69 % (1011488)CaDiCaL version: 2.1.3
% 2.09/0.69 % (1011488)Termination reason: Instruction limit
% 2.09/0.69 % (1011488)Termination phase: Property scanning
% 2.09/0.69 % (1011488)Time elapsed: 0.002 s
% 2.09/0.69 % (1011488)Peak memory usage: 10 MB
% 2.09/0.69 % (1011488)Instructions burned: 2 (million)
% 2.09/0.69 % (1011490)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1880202445:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.09/0.69 % (1011494)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2656487540:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.09/0.69 % (1011497)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1317332424:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.09/0.69 % (1011490)Instruction limit reached!
% 2.09/0.69 % (1011490)------------------------------
% 2.09/0.69 % (1011490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.69 % (1011490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.69 % (1011490)CaDiCaL version: 2.1.3
% 2.09/0.69 % (1011490)Termination reason: Instruction limit
% 2.09/0.69 % (1011490)Termination phase: Saturation
% 2.09/0.69 % (1011490)Time elapsed: 0.031 s
% 2.09/0.69 % (1011490)Peak memory usage: 13 MB
% 2.09/0.69 % (1011490)Instructions burned: 38 (million)
% 2.09/0.69 % (1011469)Instruction limit reached!
% 2.09/0.69 % (1011469)------------------------------
% 2.09/0.69 % (1011469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.69 % (1011469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.69 % (1011469)CaDiCaL version: 2.1.3
% 2.09/0.69 % (1011469)Termination reason: Instruction limit
% 2.09/0.69 % (1011469)Termination phase: Saturation
% 2.09/0.69 % (1011469)Time elapsed: 0.146 s
% 2.09/0.69 % (1011469)Peak memory usage: 20 MB
% 2.09/0.69 % (1011469)Instructions burned: 157 (million)
% 2.09/0.69 % (1011497)Instruction limit reached!
% 2.09/0.69 % (1011497)------------------------------
% 2.09/0.69 % (1011497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.09/0.69 % (1011497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.09/0.69 % (1011497)CaDiCaL version: 2.1.3
% 2.09/0.69 % (1011497)Termination reason: Instruction limit
% 2.09/0.69 % (1011497)Termination phase: Saturation
% 2.35/0.76 % (1011497)Time elapsed: 0.013 s
% 2.35/0.76 % (1011497)Peak memory usage: 12 MB
% 2.35/0.76 % (1011497)Instructions burned: 15 (million)
% 2.35/0.76 % (1011486)Instruction limit reached!
% 2.35/0.76 % (1011486)------------------------------
% 2.35/0.76 % (1011486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.76 % (1011486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.76 % (1011486)CaDiCaL version: 2.1.3
% 2.35/0.76 % (1011486)Termination reason: Instruction limit
% 2.35/0.76 % (1011486)Termination phase: Saturation
% 2.35/0.76 % (1011486)Time elapsed: 0.068 s
% 2.35/0.76 % (1011486)Peak memory usage: 14 MB
% 2.35/0.76 % (1011486)Instructions burned: 86 (million)
% 2.35/0.76 % (1011494)Instruction limit reached!
% 2.35/0.76 % (1011494)------------------------------
% 2.35/0.76 % (1011494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.76 % (1011494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.76 % (1011494)CaDiCaL version: 2.1.3
% 2.35/0.76 % (1011494)Termination reason: Instruction limit
% 2.35/0.76 % (1011494)Termination phase: Saturation
% 2.35/0.77 % (1011494)Time elapsed: 0.034 s
% 2.35/0.77 % (1011494)Peak memory usage: 12 MB
% 2.35/0.77 % (1011494)Instructions burned: 25 (million)
% 2.35/0.77 % (1011501)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1386801333:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.35/0.77 % (1011502)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=683022453:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.35/0.77 % (1011503)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2712354059:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2997 on theBenchmark for (2997ds/2Mi)
% 2.35/0.77 % (1011503)Instruction limit reached!
% 2.35/0.77 % (1011503)------------------------------
% 2.35/0.77 % (1011503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.77 % (1011503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.77 % (1011503)CaDiCaL version: 2.1.3
% 2.35/0.77 % (1011503)Termination reason: Instruction limit
% 2.35/0.77 % (1011503)Termination phase: Saturation
% 2.35/0.77 % (1011503)Time elapsed: 0.003 s
% 2.35/0.77 % (1011503)Peak memory usage: 11 MB
% 2.35/0.77 % (1011503)Instructions burned: 3 (million)
% 2.35/0.77 % (1011502)Instruction limit reached!
% 2.35/0.77 % (1011502)------------------------------
% 2.35/0.77 % (1011502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.77 % (1011502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.77 % (1011502)CaDiCaL version: 2.1.3
% 2.35/0.77 % (1011502)Termination reason: Instruction limit
% 2.35/0.77 % (1011502)Termination phase: Saturation
% 2.35/0.77 % (1011502)Time elapsed: 0.012 s
% 2.35/0.77 % (1011502)Peak memory usage: 12 MB
% 2.35/0.77 % (1011502)Instructions burned: 14 (million)
% 2.35/0.77 % (1011504)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2796785480:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 2.35/0.77 % (1011505)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1787592650:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.35/0.77 % (1011510)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.35/0.77 % (1011510)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.35/0.77 % (1011504)Instruction limit reached!
% 2.35/0.77 % (1011504)------------------------------
% 2.35/0.77 % (1011504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.77 % (1011504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.77 % (1011504)CaDiCaL version: 2.1.3
% 2.35/0.77 % (1011504)Termination reason: Instruction limit
% 2.35/0.77 % (1011504)Termination phase: Saturation
% 2.35/0.77 % (1011504)Time elapsed: 0.024 s
% 2.35/0.77 % (1011504)Peak memory usage: 13 MB
% 2.35/0.77 % (1011504)Instructions burned: 26 (million)
% 2.35/0.77 % (1011505)Instruction limit reached!
% 2.35/0.77 % (1011505)------------------------------
% 2.35/0.77 % (1011505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.90 % (1011505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.90 % (1011505)CaDiCaL version: 2.1.3
% 2.83/0.90 % (1011505)Termination reason: Instruction limit
% 2.83/0.90 % (1011505)Termination phase: Saturation
% 2.83/0.90 % (1011505)Time elapsed: 0.020 s
% 2.83/0.90 % (1011505)Peak memory usage: 12 MB
% 2.83/0.90 % (1011505)Instructions burned: 23 (million)
% 2.83/0.90 % (1011509)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3642143794:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.83/0.90 % (1011491)Instruction limit reached!
% 2.83/0.90 % (1011491)------------------------------
% 2.83/0.90 % (1011491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.90 % (1011491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.90 % (1011491)CaDiCaL version: 2.1.3
% 2.83/0.90 % (1011491)Termination reason: Instruction limit
% 2.83/0.90 % (1011491)Termination phase: Saturation
% 2.83/0.90 % (1011491)Time elapsed: 0.122 s
% 2.83/0.90 % (1011491)Peak memory usage: 22 MB
% 2.83/0.90 % (1011491)Instructions burned: 251 (million)
% 2.83/0.90 % (1011510)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3758090850:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.83/0.90 % (1011510)Instruction limit reached!
% 2.83/0.90 % (1011510)------------------------------
% 2.83/0.90 % (1011510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.90 % (1011510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.90 % (1011510)CaDiCaL version: 2.1.3
% 2.83/0.90 % (1011510)Termination reason: Instruction limit
% 2.83/0.90 % (1011510)Termination phase: Saturation
% 2.83/0.90 % (1011510)Time elapsed: 0.013 s
% 2.83/0.90 % (1011510)Peak memory usage: 12 MB
% 2.83/0.90 % (1011510)Instructions burned: 14 (million)
% 2.83/0.90 % (1011517)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1912435070:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.83/0.90 % (1011517)Instruction limit reached!
% 2.83/0.90 % (1011517)------------------------------
% 2.83/0.90 % (1011517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.90 % (1011517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.90 % (1011517)CaDiCaL version: 2.1.3
% 2.83/0.90 % (1011517)Termination reason: Instruction limit
% 2.83/0.90 % (1011517)Termination phase: Saturation
% 2.83/0.90 % (1011517)Time elapsed: 0.003 s
% 2.83/0.90 % (1011517)Peak memory usage: 12 MB
% 2.83/0.90 % (1011517)Instructions burned: 7 (million)
% 2.83/0.90 % (1011513)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.83/0.90 % (1011513)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=1719466644:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.83/0.90 % (1011516)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=1627749599:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.83/0.90 % (1011513)Instruction limit reached!
% 2.83/0.90 % (1011513)------------------------------
% 2.83/0.90 % (1011513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.90 % (1011513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.90 % (1011513)CaDiCaL version: 2.1.3
% 2.83/0.90 % (1011513)Termination reason: Instruction limit
% 2.83/0.90 % (1011513)Termination phase: Saturation
% 2.83/0.90 % (1011513)Time elapsed: 0.007 s
% 2.83/0.90 % (1011513)Peak memory usage: 12 MB
% 2.83/0.90 % (1011513)Instructions burned: 8 (million)
% 2.83/0.90 % (1011520)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3342822418:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.83/0.90 % (1011518)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=856717512:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.83/0.90 % (1011520)Instruction limit reached!
% 2.83/0.90 % (1011520)------------------------------
% 2.83/0.90 % (1011520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.98 % (1011520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.98 % (1011520)CaDiCaL version: 2.1.3
% 3.24/0.98 % (1011520)Termination reason: Instruction limit
% 3.24/0.98 % (1011520)Termination phase: Saturation
% 3.24/0.98 % (1011520)Time elapsed: 0.011 s
% 3.24/0.98 % (1011520)Peak memory usage: 12 MB
% 3.24/0.98 % (1011520)Instructions burned: 21 (million)
% 3.24/0.98 % (1011509)Instruction limit reached!
% 3.24/0.98 % (1011509)------------------------------
% 3.24/0.98 % (1011509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.98 % (1011509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.98 % (1011509)CaDiCaL version: 2.1.3
% 3.24/0.98 % (1011509)Termination reason: Instruction limit
% 3.24/0.98 % (1011509)Termination phase: Saturation
% 3.24/0.98 % (1011509)Time elapsed: 0.051 s
% 3.24/0.98 % (1011509)Peak memory usage: 12 MB
% 3.24/0.98 % (1011509)Instructions burned: 60 (million)
% 3.24/0.98 % (1011516)Instruction limit reached!
% 3.24/0.98 % (1011516)------------------------------
% 3.24/0.98 % (1011516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.98 % (1011516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.98 % (1011516)CaDiCaL version: 2.1.3
% 3.24/0.98 % (1011516)Termination reason: Instruction limit
% 3.24/0.98 % (1011516)Termination phase: Saturation
% 3.24/0.98 % (1011516)Time elapsed: 0.027 s
% 3.24/0.98 % (1011516)Peak memory usage: 12 MB
% 3.24/0.98 % (1011516)Instructions burned: 32 (million)
% 3.24/0.98 % (1011518)Instruction limit reached!
% 3.24/0.98 % (1011518)------------------------------
% 3.24/0.98 % (1011518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.98 % (1011518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.98 % (1011518)CaDiCaL version: 2.1.3
% 3.24/0.98 % (1011518)Termination reason: Instruction limit
% 3.24/0.98 % (1011518)Termination phase: Saturation
% 3.24/0.98 % (1011518)Time elapsed: 0.018 s
% 3.24/0.98 % (1011518)Peak memory usage: 12 MB
% 3.24/0.98 % (1011518)Instructions burned: 23 (million)
% 3.24/0.98 % (1011526)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3376015248:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.24/0.98 % (1011523)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3780462550:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.24/0.98 % (1011527)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3778167679:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.24/0.98 % (1011529)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.24/0.98 % (1011528)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=474184981:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.24/0.98 % (1011529)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=524114280:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.24/0.98 % (1011529)Instruction limit reached!
% 3.24/0.98 % (1011529)------------------------------
% 3.24/0.98 % (1011529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.98 % (1011529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.98 % (1011529)CaDiCaL version: 2.1.3
% 3.24/0.98 % (1011529)Termination reason: Instruction limit
% 3.24/0.98 % (1011529)Termination phase: Saturation
% 3.24/0.98 % (1011529)Time elapsed: 0.007 s
% 3.24/0.98 % (1011529)Peak memory usage: 12 MB
% 3.24/0.98 % (1011529)Instructions burned: 8 (million)
% 3.24/0.98 % (1011526)Instruction limit reached!
% 3.24/0.98 % (1011526)------------------------------
% 3.24/0.98 % (1011526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.98 % (1011526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.98 % (1011526)CaDiCaL version: 2.1.3
% 3.24/0.98 % (1011526)Termination reason: Instruction limit
% 3.24/0.98 % (1011526)Termination phase: Saturation
% 3.24/0.98 % (1011526)Time elapsed: 0.054 s
% 3.24/0.98 % (1011526)Peak memory usage: 12 MB
% 3.24/0.98 % (1011526)Instructions burned: 144 (million)
% 3.24/0.98 % (1011528)Instruction limit reached!
% 3.24/0.98 % (1011528)------------------------------
% 4.91/1.11 % (1011528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.91/1.11 % (1011528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.11 % (1011528)CaDiCaL version: 2.1.3
% 4.91/1.11 % (1011528)Termination reason: Instruction limit
% 4.91/1.11 % (1011528)Termination phase: Saturation
% 4.91/1.11 % (1011528)Time elapsed: 0.032 s
% 4.91/1.11 % (1011528)Peak memory usage: 12 MB
% 4.91/1.11 % (1011528)Instructions burned: 43 (million)
% 4.91/1.11 % (1011535)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2182233771:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 4.91/1.11 % (1011536)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1656654513:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 4.91/1.11 % (1011537)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.91/1.11 % (1011537)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=4161736841:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 4.91/1.11 % (1011537)Instruction limit reached!
% 4.91/1.11 % (1011537)------------------------------
% 4.91/1.11 % (1011537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.91/1.11 % (1011537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.11 % (1011537)CaDiCaL version: 2.1.3
% 4.91/1.11 % (1011537)Termination reason: Instruction limit
% 4.91/1.11 % (1011537)Termination phase: Saturation
% 4.91/1.11 % (1011537)Time elapsed: 0.007 s
% 4.91/1.11 % (1011537)Peak memory usage: 12 MB
% 4.91/1.11 % (1011537)Instructions burned: 7 (million)
% 4.91/1.11 % (1011541)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2095813885:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 4.91/1.11 % (1011541)Instruction limit reached!
% 4.91/1.11 % (1011541)------------------------------
% 4.91/1.11 % (1011541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.91/1.11 % (1011541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.11 % (1011541)CaDiCaL version: 2.1.3
% 4.91/1.11 % (1011541)Termination reason: Instruction limit
% 4.91/1.11 % (1011541)Termination phase: Saturation
% 4.91/1.11 % (1011541)Time elapsed: 0.018 s
% 4.91/1.11 % (1011541)Peak memory usage: 12 MB
% 4.91/1.11 % (1011541)Instructions burned: 22 (million)
% 4.91/1.11 % (1011501)Instruction limit reached!
% 4.91/1.11 % (1011501)------------------------------
% 4.91/1.11 % (1011501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.91/1.11 % (1011501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.11 % (1011501)CaDiCaL version: 2.1.3
% 4.91/1.11 % (1011501)Termination reason: Instruction limit
% 4.91/1.11 % (1011501)Termination phase: Saturation
% 4.91/1.11 % (1011501)Time elapsed: 0.270 s
% 4.91/1.11 % (1011501)Peak memory usage: 20 MB
% 4.91/1.11 % (1011501)Instructions burned: 327 (million)
% 4.91/1.11 % (1011536)Instruction limit reached!
% 4.91/1.11 % (1011536)------------------------------
% 4.91/1.11 % (1011536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.91/1.11 % (1011536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.91/1.11 % (1011536)CaDiCaL version: 2.1.3
% 4.91/1.11 % (1011536)Termination reason: Instruction limit
% 4.91/1.11 % (1011536)Termination phase: Saturation
% 4.91/1.11 % (1011536)Time elapsed: 0.095 s
% 4.91/1.11 % (1011536)Peak memory usage: 19 MB
% 4.91/1.11 % (1011536)Instructions burned: 171 (million)
% 4.91/1.11 % (1011543)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2555934657:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 4.91/1.11 % (1011545)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=3832920778:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2994 on theBenchmark for (2994ds/853Mi)
% 4.91/1.11 % (1011544)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3203962898:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 5.68/1.29 % (1011543)Instruction limit reached!
% 5.68/1.29 % (1011543)------------------------------
% 5.68/1.29 % (1011543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.68/1.29 % (1011543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.29 % (1011543)CaDiCaL version: 2.1.3
% 5.68/1.29 % (1011543)Termination reason: Instruction limit
% 5.68/1.29 % (1011543)Termination phase: Saturation
% 5.68/1.29 % (1011543)Time elapsed: 0.018 s
% 5.68/1.29 % (1011543)Peak memory usage: 13 MB
% 5.68/1.29 % (1011543)Instructions burned: 20 (million)
% 5.68/1.29 % (1011527)Instruction limit reached!
% 5.68/1.29 % (1011527)------------------------------
% 5.68/1.29 % (1011527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.68/1.29 % (1011527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.29 % (1011527)CaDiCaL version: 2.1.3
% 5.68/1.29 % (1011527)Termination reason: Instruction limit
% 5.68/1.29 % (1011527)Termination phase: Saturation
% 5.68/1.29 % (1011527)Time elapsed: 0.190 s
% 5.68/1.29 % (1011527)Peak memory usage: 24 MB
% 5.68/1.29 % (1011527)Instructions burned: 194 (million)
% 5.68/1.29 % (1011535)Instruction limit reached!
% 5.68/1.29 % (1011535)------------------------------
% 5.68/1.29 % (1011535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.68/1.29 % (1011535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.29 % (1011535)CaDiCaL version: 2.1.3
% 5.68/1.29 % (1011535)Termination reason: Instruction limit
% 5.68/1.29 % (1011535)Termination phase: Saturation
% 5.68/1.29 % (1011535)Time elapsed: 0.136 s
% 5.68/1.29 % (1011535)Peak memory usage: 15 MB
% 5.68/1.29 % (1011535)Instructions burned: 181 (million)
% 5.68/1.29 % (1011549)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=76407833:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 5.68/1.29 % (1011550)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1997067602:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 5.68/1.29 % (1011551)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3877921773:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.68/1.29 % (1011550)Refutation not found, incomplete strategy
% 5.68/1.29 % (1011550)------------------------------
% 5.68/1.29 % (1011550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.68/1.29 % (1011550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.29 % (1011550)CaDiCaL version: 2.1.3
% 5.68/1.29 % (1011550)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.29 % (1011550)Time elapsed: 0.007 s
% 5.68/1.29 % (1011550)Peak memory usage: 12 MB
% 5.68/1.29 % (1011550)Instructions burned: 7 (million)
% 5.68/1.29 % (1011550)------------------------------
% 5.68/1.29 % (1011550)------------------------------
% 5.68/1.29 % (1011551)Instruction limit reached!
% 5.68/1.29 % (1011551)------------------------------
% 5.68/1.29 % (1011551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.68/1.29 % (1011551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.29 % (1011551)CaDiCaL version: 2.1.3
% 5.68/1.29 % (1011551)Termination reason: Instruction limit
% 5.68/1.29 % (1011551)Termination phase: Saturation
% 5.68/1.29 % (1011551)Time elapsed: 0.018 s
% 5.68/1.29 % (1011551)Peak memory usage: 12 MB
% 5.68/1.29 % (1011551)Instructions burned: 21 (million)
% 5.68/1.29 % (1011466)Instruction limit reached!
% 5.68/1.29 % (1011466)------------------------------
% 5.68/1.29 % (1011466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.68/1.29 % (1011466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.29 % (1011466)CaDiCaL version: 2.1.3
% 5.68/1.29 % (1011466)Termination reason: Instruction limit
% 5.68/1.29 % (1011466)Termination phase: Saturation
% 5.68/1.29 % (1011466)Time elapsed: 0.558 s
% 5.68/1.29 % (1011466)Peak memory usage: 46 MB
% 5.68/1.29 % (1011466)Instructions burned: 635 (million)
% 5.68/1.29 % (1011555)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.74/1.44 % (1011549)Instruction limit reached!
% 6.74/1.44 % (1011549)------------------------------
% 6.74/1.44 % (1011549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1011549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1011549)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1011549)Termination reason: Instruction limit
% 6.74/1.44 % (1011549)Termination phase: Saturation
% 6.74/1.44 % (1011549)Time elapsed: 0.040 s
% 6.74/1.44 % (1011549)Peak memory usage: 14 MB
% 6.74/1.44 % (1011549)Instructions burned: 46 (million)
% 6.74/1.44 % (1011555)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=573210621:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 6.74/1.44 % (1011556)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=317865038:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 6.74/1.44 % (1011557)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=3280068401:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 6.74/1.44 % (1011556)Instruction limit reached!
% 6.74/1.44 % (1011556)------------------------------
% 6.74/1.44 % (1011556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1011556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1011556)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1011556)Termination reason: Instruction limit
% 6.74/1.44 % (1011556)Termination phase: Saturation
% 6.74/1.44 % (1011556)Time elapsed: 0.014 s
% 6.74/1.44 % (1011556)Peak memory usage: 12 MB
% 6.74/1.44 % (1011556)Instructions burned: 13 (million)
% 6.74/1.44 % (1011558)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1705015681:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 6.74/1.44 % (1011562)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=448803589:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 6.74/1.44 % (1011558)Instruction limit reached!
% 6.74/1.44 % (1011558)------------------------------
% 6.74/1.44 % (1011558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1011558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1011558)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1011558)Termination reason: Instruction limit
% 6.74/1.44 % (1011558)Termination phase: Saturation
% 6.74/1.44 % (1011558)Time elapsed: 0.040 s
% 6.74/1.44 % (1011558)Peak memory usage: 13 MB
% 6.74/1.44 % (1011558)Instructions burned: 51 (million)
% 6.74/1.44 % (1011557)Instruction limit reached!
% 6.74/1.44 % (1011557)------------------------------
% 6.74/1.44 % (1011557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1011557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1011557)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1011557)Termination reason: Instruction limit
% 6.74/1.44 % (1011557)Termination phase: Saturation
% 6.74/1.44 % (1011557)Time elapsed: 0.055 s
% 6.74/1.44 % (1011557)Peak memory usage: 15 MB
% 6.74/1.44 % (1011557)Instructions burned: 66 (million)
% 6.74/1.44 % (1011562)Instruction limit reached!
% 6.74/1.44 % (1011562)------------------------------
% 6.74/1.44 % (1011562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.44 % (1011562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.44 % (1011562)CaDiCaL version: 2.1.3
% 6.74/1.44 % (1011562)Termination reason: Instruction limit
% 6.74/1.44 % (1011562)Termination phase: Saturation
% 6.74/1.44 % (1011562)Time elapsed: 0.028 s
% 6.74/1.44 % (1011562)Peak memory usage: 12 MB
% 6.74/1.44 % (1011562)Instructions burned: 31 (million)
% 6.74/1.44 % (1011565)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=401147685:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.74/1.44 % (1011566)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=3052043879:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.74/1.44 % (1011567)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2442233566:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 7.04/1.58 % (1011566)Instruction limit reached!
% 7.04/1.58 % (1011566)------------------------------
% 7.04/1.58 % (1011566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.04/1.58 % (1011566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.58 % (1011566)CaDiCaL version: 2.1.3
% 7.04/1.58 % (1011566)Termination reason: Instruction limit
% 7.04/1.58 % (1011566)Termination phase: Saturation
% 7.04/1.58 % (1011566)Time elapsed: 0.026 s
% 7.04/1.58 % (1011566)Peak memory usage: 12 MB
% 7.04/1.58 % (1011566)Instructions burned: 35 (million)
% 7.04/1.58 % (1011555)Instruction limit reached!
% 7.04/1.58 % (1011555)------------------------------
% 7.04/1.58 % (1011555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.04/1.58 % (1011555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.58 % (1011555)CaDiCaL version: 2.1.3
% 7.04/1.58 % (1011555)Termination reason: Instruction limit
% 7.04/1.58 % (1011555)Termination phase: Saturation
% 7.04/1.58 % (1011555)Time elapsed: 0.146 s
% 7.04/1.58 % (1011555)Peak memory usage: 13 MB
% 7.04/1.58 % (1011555)Instructions burned: 201 (million)
% 7.04/1.58 % (1011571)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 7.04/1.58 % (1011567)Instruction limit reached!
% 7.04/1.58 % (1011567)------------------------------
% 7.04/1.58 % (1011567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.04/1.58 % (1011567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.58 % (1011567)CaDiCaL version: 2.1.3
% 7.04/1.58 % (1011567)Termination reason: Instruction limit
% 7.04/1.58 % (1011567)Termination phase: Saturation
% 7.04/1.58 % (1011567)Time elapsed: 0.050 s
% 7.04/1.58 % (1011567)Peak memory usage: 11 MB
% 7.04/1.58 % (1011567)Instructions burned: 69 (million)
% 7.04/1.58 % (1011571)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1308233469:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 7.04/1.58 % (1011544)Instruction limit reached!
% 7.04/1.58 % (1011544)------------------------------
% 7.04/1.58 % (1011544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.04/1.58 % (1011544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.58 % (1011544)CaDiCaL version: 2.1.3
% 7.04/1.58 % (1011544)Termination reason: Instruction limit
% 7.04/1.58 % (1011544)Termination phase: Saturation
% 7.04/1.58 % (1011544)Time elapsed: 0.267 s
% 7.04/1.58 % (1011544)Peak memory usage: 19 MB
% 7.04/1.58 % (1011544)Instructions burned: 317 (million)
% 7.04/1.58 % (1011572)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2980036735:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 7.04/1.58 % (1011573)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3197158079:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 7.04/1.58 % (1011575)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2481945807:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 7.04/1.58 % (1011565)Instruction limit reached!
% 7.04/1.58 % (1011565)------------------------------
% 7.04/1.58 % (1011565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.04/1.58 % (1011565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.58 % (1011565)CaDiCaL version: 2.1.3
% 7.04/1.58 % (1011565)Termination reason: Instruction limit
% 7.04/1.58 % (1011565)Termination phase: Saturation
% 7.04/1.58 % (1011565)Time elapsed: 0.114 s
% 7.04/1.58 % (1011565)Peak memory usage: 12 MB
% 7.04/1.58 % (1011565)Instructions burned: 137 (million)
% 7.04/1.58 % (1011579)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=615574665:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 7.04/1.58 % (1011545)Instruction limit reached!
% 7.04/1.58 % (1011545)------------------------------
% 7.04/1.58 % (1011545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.04/1.58 % (1011545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.58 % (1011545)CaDiCaL version: 2.1.3
% 7.04/1.58 % (1011545)Termination reason: Instruction limit
% 7.04/1.58 % (1011545)Termination phase: Saturation
% 7.04/1.58 % (1011545)Time elapsed: 0.381 s
% 7.04/1.58 % (1011545)Peak memory usage: 44 MB
% 7.04/1.58 % (1011545)Instructions burned: 855 (million)
% 7.04/1.58 % (1011573)Instruction limit reached!
% 7.04/1.58 % (1011573)------------------------------
% 8.19/1.78 % (1011573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.19/1.78 % (1011573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.78 % (1011573)CaDiCaL version: 2.1.3
% 8.19/1.78 % (1011573)Termination reason: Instruction limit
% 8.19/1.78 % (1011573)Termination phase: Saturation
% 8.19/1.78 % (1011573)Time elapsed: 0.094 s
% 8.19/1.78 % (1011573)Peak memory usage: 16 MB
% 8.19/1.78 % (1011573)Instructions burned: 96 (million)
% 8.19/1.78 % (1011571)Instruction limit reached!
% 8.19/1.78 % (1011571)------------------------------
% 8.19/1.78 % (1011571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.19/1.78 % (1011571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.78 % (1011571)CaDiCaL version: 2.1.3
% 8.19/1.78 % (1011571)Termination reason: Instruction limit
% 8.19/1.78 % (1011571)Termination phase: Saturation
% 8.19/1.78 % (1011571)Time elapsed: 0.129 s
% 8.19/1.78 % (1011571)Peak memory usage: 12 MB
% 8.19/1.78 % (1011571)Instructions burned: 180 (million)
% 8.19/1.78 % (1011581)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1727415289:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/515Mi)
% 8.19/1.78 % (1011582)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=207573081:st=1.5:i=130:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 8.19/1.78 % (1011583)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2213692611:i=44:ep=R:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/44Mi)
% 8.19/1.78 % (1011583)Instruction limit reached!
% 8.19/1.78 % (1011583)------------------------------
% 8.19/1.78 % (1011583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.19/1.78 % (1011583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.78 % (1011583)CaDiCaL version: 2.1.3
% 8.19/1.78 % (1011583)Termination reason: Instruction limit
% 8.19/1.78 % (1011583)Termination phase: Saturation
% 8.19/1.78 % (1011583)Time elapsed: 0.034 s
% 8.19/1.78 % (1011583)Peak memory usage: 12 MB
% 8.19/1.78 % (1011583)Instructions burned: 44 (million)
% 8.19/1.78 % (1011572)Instruction limit reached!
% 8.19/1.78 % (1011572)------------------------------
% 8.19/1.78 % (1011572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.19/1.78 % (1011572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.78 % (1011572)CaDiCaL version: 2.1.3
% 8.19/1.78 % (1011572)Termination reason: Instruction limit
% 8.19/1.78 % (1011572)Termination phase: Saturation
% 8.19/1.78 % (1011572)Time elapsed: 0.224 s
% 8.19/1.78 % (1011572)Peak memory usage: 22 MB
% 8.19/1.78 % (1011572)Instructions burned: 247 (million)
% 8.19/1.78 % (1011587)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3122913007:s2a=on:i=571:nm=16:rtra=on_2990 on theBenchmark for (2990ds/571Mi)
% 8.19/1.78 % (1011587)Refutation not found, incomplete strategy
% 8.19/1.78 % (1011587)------------------------------
% 8.19/1.78 % (1011587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.19/1.78 % (1011587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.78 % (1011587)CaDiCaL version: 2.1.3
% 8.19/1.78 % (1011587)Termination reason: Refutation not found, incomplete strategy
% 8.19/1.78 % (1011587)Time elapsed: 0.009 s
% 8.19/1.78 % (1011587)Peak memory usage: 12 MB
% 8.19/1.78 % (1011587)Instructions burned: 8 (million)
% 8.19/1.78 % (1011587)------------------------------
% 8.19/1.78 % (1011587)------------------------------
% 8.19/1.78 % (1011589)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=928006703:i=450:rtra=on:ixr=off:ntd=on_2989 on theBenchmark for (2989ds/450Mi)
% 8.19/1.78 % (1011582)Instruction limit reached!
% 8.19/1.78 % (1011582)------------------------------
% 8.19/1.78 % (1011582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.19/1.78 % (1011582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.78 % (1011582)CaDiCaL version: 2.1.3
% 8.19/1.78 % (1011582)Termination reason: Instruction limit
% 8.19/1.78 % (1011582)Termination phase: Saturation
% 8.19/1.78 % (1011582)Time elapsed: 0.108 s
% 8.19/1.78 % (1011582)Peak memory usage: 16 MB
% 8.19/1.78 % (1011582)Instructions burned: 130 (million)
% 8.19/1.78 % (1011590)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2048104877:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/95Mi)
% 9.10/2.00 % (1011592)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=1189801049:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2989 on theBenchmark for (2989ds/65Mi)
% 9.10/2.00 % (1011581)Instruction limit reached!
% 9.10/2.00 % (1011581)------------------------------
% 9.10/2.00 % (1011581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.10/2.00 % (1011581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.00 % (1011581)CaDiCaL version: 2.1.3
% 9.10/2.00 % (1011581)Termination reason: Instruction limit
% 9.10/2.00 % (1011581)Termination phase: Saturation
% 9.10/2.00 % (1011581)Time elapsed: 0.203 s
% 9.10/2.00 % (1011581)Peak memory usage: 20 MB
% 9.10/2.00 % (1011581)Instructions burned: 515 (million)
% 9.10/2.00 % (1011590)Instruction limit reached!
% 9.10/2.00 % (1011590)------------------------------
% 9.10/2.00 % (1011590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.10/2.00 % (1011590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.00 % (1011590)CaDiCaL version: 2.1.3
% 9.10/2.00 % (1011590)Termination reason: Instruction limit
% 9.10/2.00 % (1011590)Termination phase: Saturation
% 9.10/2.00 % (1011590)Time elapsed: 0.069 s
% 9.10/2.00 % (1011590)Peak memory usage: 13 MB
% 9.10/2.00 % (1011590)Instructions burned: 96 (million)
% 9.10/2.00 % (1011592)Instruction limit reached!
% 9.10/2.00 % (1011592)------------------------------
% 9.10/2.00 % (1011592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.10/2.00 % (1011592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.00 % (1011592)CaDiCaL version: 2.1.3
% 9.10/2.00 % (1011592)Termination reason: Instruction limit
% 9.10/2.00 % (1011592)Termination phase: Saturation
% 9.10/2.00 % (1011592)Time elapsed: 0.054 s
% 9.10/2.00 % (1011592)Peak memory usage: 15 MB
% 9.10/2.00 % (1011592)Instructions burned: 66 (million)
% 9.10/2.00 % (1011595)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=1299106851:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2988 on theBenchmark for (2988ds/105Mi)
% 9.10/2.00 % (1011575)Instruction limit reached!
% 9.10/2.00 % (1011575)------------------------------
% 9.10/2.00 % (1011575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.10/2.00 % (1011575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.00 % (1011575)CaDiCaL version: 2.1.3
% 9.10/2.00 % (1011575)Termination reason: Instruction limit
% 9.10/2.00 % (1011575)Termination phase: Saturation
% 9.10/2.00 % (1011575)Time elapsed: 0.331 s
% 9.10/2.00 % (1011575)Peak memory usage: 21 MB
% 9.10/2.00 % (1011575)Instructions burned: 427 (million)
% 9.10/2.00 % (1011596)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=278246608:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2988 on theBenchmark for (2988ds/5755Mi)
% 9.10/2.00 % (1011597)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4022829230:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/375Mi)
% 9.10/2.00 % (1011595)Instruction limit reached!
% 9.10/2.00 % (1011595)------------------------------
% 9.10/2.00 % (1011595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.10/2.00 % (1011595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.10/2.00 % (1011595)CaDiCaL version: 2.1.3
% 9.10/2.00 % (1011595)Termination reason: Instruction limit
% 9.10/2.00 % (1011595)Termination phase: Saturation
% 9.10/2.00 % (1011595)Time elapsed: 0.042 s
% 9.10/2.00 % (1011595)Peak memory usage: 12 MB
% 9.10/2.00 % (1011595)Instructions burned: 108 (million)
% 9.10/2.00 % (1011599)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2667742583:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2988 on theBenchmark for (2988ds/495Mi)
% 9.10/2.00 % (1011602)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=241078115:cond=on:i=34:hud=10:nm=10:rtra=on_2988 on theBenchmark for (2988ds/34Mi)
% 12.15/2.14 % (1011602)Instruction limit reached!
% 12.15/2.14 % (1011602)------------------------------
% 12.15/2.14 % (1011602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.15/2.14 % (1011602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.15/2.14 % (1011602)CaDiCaL version: 2.1.3
% 12.15/2.14 % (1011602)Termination reason: Instruction limit
% 12.15/2.14 % (1011602)Termination phase: Saturation
% 12.15/2.14 % (1011602)Time elapsed: 0.014 s
% 12.15/2.14 % (1011602)Peak memory usage: 12 MB
% 12.15/2.14 % (1011602)Instructions burned: 34 (million)
% 12.15/2.14 % (1011605)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3210174926:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/91Mi)
% 12.15/2.14 % (1011605)Instruction limit reached!
% 12.15/2.14 % (1011605)------------------------------
% 12.15/2.14 % (1011605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.15/2.14 % (1011605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.15/2.14 % (1011605)CaDiCaL version: 2.1.3
% 12.15/2.14 % (1011605)Termination reason: Instruction limit
% 12.15/2.14 % (1011605)Termination phase: Saturation
% 12.15/2.14 % (1011605)Time elapsed: 0.039 s
% 12.15/2.14 % (1011605)Peak memory usage: 12 MB
% 12.15/2.14 % (1011605)Instructions burned: 92 (million)
% 12.15/2.14 % (1011607)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2553123162:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2987 on theBenchmark for (2987ds/66Mi)
% 12.15/2.14 % (1011607)Instruction limit reached!
% 12.15/2.14 % (1011607)------------------------------
% 12.15/2.14 % (1011607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.15/2.14 % (1011607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.15/2.14 % (1011607)CaDiCaL version: 2.1.3
% 12.15/2.14 % (1011607)Termination reason: Instruction limit
% 12.15/2.14 % (1011607)Termination phase: Saturation
% 12.15/2.14 % (1011607)Time elapsed: 0.034 s
% 12.15/2.14 % (1011607)Peak memory usage: 14 MB
% 12.15/2.14 % (1011607)Instructions burned: 68 (million)
% 12.15/2.14 % (1011523)Instruction limit reached!
% 12.15/2.14 % (1011523)------------------------------
% 12.15/2.14 % (1011523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.15/2.14 % (1011523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.15/2.14 % (1011523)CaDiCaL version: 2.1.3
% 12.15/2.14 % (1011523)Termination reason: Instruction limit
% 12.15/2.14 % (1011523)Termination phase: Saturation
% 12.15/2.14 % (1011523)Time elapsed: 0.995 s
% 12.15/2.14 % (1011523)Peak memory usage: 46 MB
% 12.15/2.14 % (1011523)Instructions burned: 1241 (million)
% 12.15/2.14 % (1011609)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2397075113:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2986 on theBenchmark for (2986ds/22Mi)
% 12.15/2.14 % (1011609)Instruction limit reached!
% 12.15/2.14 % (1011609)------------------------------
% 12.15/2.14 % (1011609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.15/2.14 % (1011609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.15/2.14 % (1011609)CaDiCaL version: 2.1.3
% 12.15/2.14 % (1011609)Termination reason: Instruction limit
% 12.15/2.14 % (1011609)Termination phase: Saturation
% 12.15/2.14 % (1011609)Time elapsed: 0.009 s
% 12.15/2.14 % (1011609)Peak memory usage: 12 MB
% 12.15/2.14 % (1011609)Instructions burned: 23 (million)
% 12.15/2.14 % (1011610)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=598322939:i=338:bd=all:ins=4:rtra=on_2986 on theBenchmark for (2986ds/338Mi)
% 12.15/2.14 % (1011612)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1361657108:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/28Mi)
% 12.15/2.14 % (1011612)Instruction limit reached!
% 12.15/2.14 % (1011612)------------------------------
% 12.15/2.14 % (1011612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.15/2.14 % (1011612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.15/2.14 % (1011612)CaDiCaL version: 2.1.3
% 12.15/2.14 % (1011612)Termination reason: Instruction limit
% 12.15/2.14 % (1011612)Termination phase: Saturation
% 12.15/2.14 % (1011612)Time elapsed: 0.012 s
% 12.15/2.14 % (1011612)Peak memory usage: 12 MB
% 12.15/2.14 % (1011612)Instructions burned: 29 (million)
% 12.15/2.14 % (1011615)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 13.93/2.55 % (1011615)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2579997669:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2986 on theBenchmark for (2986ds/137Mi)
% 13.93/2.55 % (1011589)Instruction limit reached!
% 13.93/2.55 % (1011589)------------------------------
% 13.93/2.55 % (1011589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.93/2.55 % (1011589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.55 % (1011589)CaDiCaL version: 2.1.3
% 13.93/2.55 % (1011589)Termination reason: Instruction limit
% 13.93/2.55 % (1011589)Termination phase: Saturation
% 13.93/2.55 % (1011589)Time elapsed: 0.372 s
% 13.93/2.55 % (1011589)Peak memory usage: 22 MB
% 13.93/2.55 % (1011589)Instructions burned: 450 (million)
% 13.93/2.55 % (1011597)Instruction limit reached!
% 13.93/2.55 % (1011597)------------------------------
% 13.93/2.55 % (1011597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.93/2.55 % (1011597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.55 % (1011597)CaDiCaL version: 2.1.3
% 13.93/2.55 % (1011597)Termination reason: Instruction limit
% 13.93/2.55 % (1011597)Termination phase: Saturation
% 13.93/2.55 % (1011597)Time elapsed: 0.259 s
% 13.93/2.55 % (1011597)Peak memory usage: 13 MB
% 13.93/2.55 % (1011597)Instructions burned: 375 (million)
% 13.93/2.55 % (1011617)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=4222463939:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/340Mi)
% 13.93/2.55 % (1011618)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1126120093:i=227:sd=1:bd=all:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/227Mi)
% 13.93/2.55 % (1011615)Instruction limit reached!
% 13.93/2.55 % (1011615)------------------------------
% 13.93/2.55 % (1011615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.93/2.55 % (1011615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.55 % (1011615)CaDiCaL version: 2.1.3
% 13.93/2.55 % (1011615)Termination reason: Instruction limit
% 13.93/2.55 % (1011615)Termination phase: Saturation
% 13.93/2.55 % (1011615)Time elapsed: 0.061 s
% 13.93/2.55 % (1011615)Peak memory usage: 16 MB
% 13.93/2.55 % (1011615)Instructions burned: 140 (million)
% 13.93/2.55 % (1011621)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.93/2.55 % (1011621)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=272672668:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/373Mi)
% 13.93/2.55 % (1011599)Instruction limit reached!
% 13.93/2.55 % (1011599)------------------------------
% 13.93/2.55 % (1011599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.93/2.55 % (1011599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.55 % (1011599)CaDiCaL version: 2.1.3
% 13.93/2.55 % (1011599)Termination reason: Instruction limit
% 13.93/2.55 % (1011599)Termination phase: Saturation
% 13.93/2.55 % (1011599)Time elapsed: 0.378 s
% 13.93/2.55 % (1011599)Peak memory usage: 24 MB
% 13.93/2.55 % (1011599)Instructions burned: 495 (million)
% 13.93/2.55 % (1011579)Instruction limit reached!
% 13.93/2.55 % (1011579)------------------------------
% 13.93/2.55 % (1011579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.93/2.55 % (1011579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.55 % (1011579)CaDiCaL version: 2.1.3
% 13.93/2.55 % (1011579)Termination reason: Instruction limit
% 13.93/2.55 % (1011579)Termination phase: Saturation
% 13.93/2.55 % (1011579)Time elapsed: 0.738 s
% 13.93/2.55 % (1011579)Peak memory usage: 44 MB
% 13.93/2.55 % (1011579)Instructions burned: 875 (million)
% 13.93/2.55 % (1011623)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=613303553:i=116:ep=RSTC:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/116Mi)
% 13.93/2.55 % (1011621)Instruction limit reached!
% 13.93/2.55 % (1011621)------------------------------
% 13.93/2.55 % (1011621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.93/2.55 % (1011621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/2.81 % (1011621)CaDiCaL version: 2.1.3
% 15.95/2.81 % (1011621)Termination reason: Instruction limit
% 15.95/2.81 % (1011621)Termination phase: Saturation
% 15.95/2.81 % (1011621)Time elapsed: 0.135 s
% 15.95/2.81 % (1011621)Peak memory usage: 11 MB
% 15.95/2.81 % (1011621)Instructions burned: 374 (million)
% 15.95/2.81 % (1011618)Instruction limit reached!
% 15.95/2.81 % (1011618)------------------------------
% 15.95/2.81 % (1011618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.95/2.81 % (1011618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/2.81 % (1011618)CaDiCaL version: 2.1.3
% 15.95/2.81 % (1011618)Termination reason: Instruction limit
% 15.95/2.81 % (1011618)Termination phase: Saturation
% 15.95/2.81 % (1011618)Time elapsed: 0.168 s
% 15.95/2.81 % (1011618)Peak memory usage: 15 MB
% 15.95/2.81 % (1011618)Instructions burned: 227 (million)
% 15.95/2.81 % (1011626)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1211195431:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2983 on theBenchmark for (2983ds/270Mi)
% 15.95/2.81 % (1011625)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=504351701:i=575:rtra=on_2983 on theBenchmark for (2983ds/575Mi)
% 15.95/2.81 % (1011610)Instruction limit reached!
% 15.95/2.81 % (1011610)------------------------------
% 15.95/2.81 % (1011610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.95/2.81 % (1011610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/2.81 % (1011610)CaDiCaL version: 2.1.3
% 15.95/2.81 % (1011610)Termination reason: Instruction limit
% 15.95/2.81 % (1011610)Termination phase: Saturation
% 15.95/2.81 % (1011610)Time elapsed: 0.319 s
% 15.95/2.81 % (1011610)Peak memory usage: 27 MB
% 15.95/2.81 % (1011610)Instructions burned: 338 (million)
% 15.95/2.81 % (1011627)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=2775170211:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2983 on theBenchmark for (2983ds/9840Mi)
% 15.95/2.81 % (1011623)Instruction limit reached!
% 15.95/2.81 % (1011623)------------------------------
% 15.95/2.81 % (1011623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.95/2.81 % (1011623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/2.81 % (1011623)CaDiCaL version: 2.1.3
% 15.95/2.81 % (1011623)Termination reason: Instruction limit
% 15.95/2.81 % (1011623)Termination phase: Saturation
% 15.95/2.81 % (1011623)Time elapsed: 0.102 s
% 15.95/2.81 % (1011623)Peak memory usage: 16 MB
% 15.95/2.81 % (1011623)Instructions burned: 116 (million)
% 15.95/2.81 % (1011630)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=791123086:i=421:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/421Mi)
% 15.95/2.81 % (1011632)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 15.95/2.81 % (1011626)Instruction limit reached!
% 15.95/2.81 % (1011626)------------------------------
% 15.95/2.81 % (1011626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.95/2.81 % (1011626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/2.81 % (1011626)CaDiCaL version: 2.1.3
% 15.95/2.81 % (1011626)Termination reason: Instruction limit
% 15.95/2.81 % (1011626)Termination phase: Saturation
% 15.95/2.81 % (1011626)Time elapsed: 0.098 s
% 15.95/2.81 % (1011626)Peak memory usage: 12 MB
% 15.95/2.81 % (1011626)Instructions burned: 271 (million)
% 15.95/2.81 % (1011632)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=2553718927:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/270Mi)
% 15.95/2.81 % (1011634)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2992471386:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/31Mi)
% 15.95/2.81 % (1011634)Instruction limit reached!
% 15.95/2.81 % (1011634)------------------------------
% 15.95/2.81 % (1011634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.95/2.81 % (1011634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.28 % (1011634)CaDiCaL version: 2.1.3
% 20.04/3.28 % (1011634)Termination reason: Instruction limit
% 20.04/3.28 % (1011634)Termination phase: Saturation
% 20.04/3.28 % (1011634)Time elapsed: 0.014 s
% 20.04/3.28 % (1011634)Peak memory usage: 12 MB
% 20.04/3.28 % (1011634)Instructions burned: 31 (million)
% 20.04/3.28 % (1011637)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 20.04/3.28 % (1011637)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 20.04/3.28 % (1011637)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=4262603693:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2982 on theBenchmark for (2982ds/1440Mi)
% 20.04/3.28 % (1011617)Instruction limit reached!
% 20.04/3.28 % (1011617)------------------------------
% 20.04/3.28 % (1011617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.28 % (1011617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.28 % (1011617)CaDiCaL version: 2.1.3
% 20.04/3.28 % (1011617)Termination reason: Instruction limit
% 20.04/3.28 % (1011617)Termination phase: Saturation
% 20.04/3.28 % (1011617)Time elapsed: 0.358 s
% 20.04/3.28 % (1011617)Peak memory usage: 21 MB
% 20.04/3.28 % (1011617)Instructions burned: 341 (million)
% 20.04/3.28 % (1011639)dis+10_2_sil=128000:si=on:random_seed=3137682832:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2981 on theBenchmark for (2981ds/339Mi)
% 20.04/3.28 % (1011632)Instruction limit reached!
% 20.04/3.28 % (1011632)------------------------------
% 20.04/3.28 % (1011632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.28 % (1011632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.28 % (1011632)CaDiCaL version: 2.1.3
% 20.04/3.28 % (1011632)Termination reason: Instruction limit
% 20.04/3.28 % (1011632)Termination phase: Saturation
% 20.04/3.28 % (1011632)Time elapsed: 0.265 s
% 20.04/3.28 % (1011632)Peak memory usage: 27 MB
% 20.04/3.28 % (1011632)Instructions burned: 271 (million)
% 20.04/3.28 % (1011641)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1720377211:i=111:add=on:fgj=on:rtra=on:fdi=1024_2979 on theBenchmark for (2979ds/111Mi)
% 20.04/3.28 % (1011630)Instruction limit reached!
% 20.04/3.28 % (1011630)------------------------------
% 20.04/3.28 % (1011630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.28 % (1011630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.28 % (1011630)CaDiCaL version: 2.1.3
% 20.04/3.28 % (1011630)Termination reason: Instruction limit
% 20.04/3.28 % (1011630)Termination phase: Saturation
% 20.04/3.28 % (1011630)Time elapsed: 0.351 s
% 20.04/3.28 % (1011630)Peak memory usage: 25 MB
% 20.04/3.28 % (1011630)Instructions burned: 422 (million)
% 20.04/3.28 % (1011643)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=889707890:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2979 on theBenchmark for (2979ds/122Mi)
% 20.04/3.28 % (1011639)Instruction limit reached!
% 20.04/3.28 % (1011639)------------------------------
% 20.04/3.28 % (1011639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.28 % (1011639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.28 % (1011639)CaDiCaL version: 2.1.3
% 20.04/3.28 % (1011639)Termination reason: Instruction limit
% 20.04/3.28 % (1011639)Termination phase: Saturation
% 20.04/3.28 % (1011639)Time elapsed: 0.286 s
% 20.04/3.28 % (1011639)Peak memory usage: 23 MB
% 20.04/3.28 % (1011639)Instructions burned: 340 (million)
% 20.04/3.28 % (1011641)Instruction limit reached!
% 20.04/3.28 % (1011641)------------------------------
% 20.04/3.28 % (1011641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.04/3.28 % (1011641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.28 % (1011641)CaDiCaL version: 2.1.3
% 20.04/3.28 % (1011641)Termination reason: Instruction limit
% 20.04/3.28 % (1011641)Termination phase: Saturation
% 20.04/3.28 % (1011641)Time elapsed: 0.111 s
% 20.04/3.28 % (1011641)Peak memory usage: 15 MB
% 20.04/3.28 % (1011641)Instructions burned: 112 (million)
% 20.04/3.28 % (1011645)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=3733064234:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/136Mi)
% 21.05/3.48 % (1011646)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2757740540:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/232Mi)
% 21.05/3.48 % (1011625)Instruction limit reached!
% 21.05/3.48 % (1011625)------------------------------
% 21.05/3.48 % (1011625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.05/3.48 % (1011625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.48 % (1011625)CaDiCaL version: 2.1.3
% 21.05/3.48 % (1011625)Termination reason: Instruction limit
% 21.05/3.48 % (1011625)Termination phase: Saturation
% 21.05/3.48 % (1011625)Time elapsed: 0.556 s
% 21.05/3.48 % (1011625)Peak memory usage: 52 MB
% 21.05/3.48 % (1011625)Instructions burned: 575 (million)
% 21.05/3.48 % (1011643)Instruction limit reached!
% 21.05/3.48 % (1011643)------------------------------
% 21.05/3.48 % (1011643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.05/3.48 % (1011643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.48 % (1011643)CaDiCaL version: 2.1.3
% 21.05/3.48 % (1011643)Termination reason: Instruction limit
% 21.05/3.48 % (1011643)Termination phase: Saturation
% 21.05/3.48 % (1011643)Time elapsed: 0.121 s
% 21.05/3.48 % (1011643)Peak memory usage: 16 MB
% 21.05/3.48 % (1011643)Instructions burned: 122 (million)
% 21.05/3.48 % (1011649)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=220060600:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2977 on theBenchmark for (2977ds/1254Mi)
% 21.05/3.48 % (1011650)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 21.05/3.48 % (1011650)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=794591669:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2977 on theBenchmark for (2977ds/281Mi)
% 21.05/3.48 % (1011645)Instruction limit reached!
% 21.05/3.48 % (1011645)------------------------------
% 21.05/3.48 % (1011645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.05/3.48 % (1011645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.48 % (1011645)CaDiCaL version: 2.1.3
% 21.05/3.48 % (1011645)Termination reason: Instruction limit
% 21.05/3.48 % (1011645)Termination phase: Saturation
% 21.05/3.48 % (1011645)Time elapsed: 0.095 s
% 21.05/3.48 % (1011645)Peak memory usage: 11 MB
% 21.05/3.48 % (1011645)Instructions burned: 136 (million)
% 21.05/3.48 % (1011653)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3189964679:i=619:add=on:rtra=on_2977 on theBenchmark for (2977ds/619Mi)
% 21.05/3.48 % (1011637)Instruction limit reached!
% 21.05/3.48 % (1011637)------------------------------
% 21.05/3.48 % (1011637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.05/3.48 % (1011637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.48 % (1011637)CaDiCaL version: 2.1.3
% 21.05/3.48 % (1011637)Termination reason: Instruction limit
% 21.05/3.48 % (1011637)Termination phase: Saturation
% 21.05/3.48 % (1011637)Time elapsed: 0.612 s
% 21.05/3.48 % (1011637)Peak memory usage: 44 MB
% 21.05/3.48 % (1011637)Instructions burned: 1442 (million)
% 21.05/3.48 % (1011646)Instruction limit reached!
% 21.05/3.48 % (1011646)------------------------------
% 21.05/3.48 % (1011646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.05/3.48 % (1011646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.48 % (1011646)CaDiCaL version: 2.1.3
% 21.05/3.48 % (1011646)Termination reason: Instruction limit
% 21.05/3.48 % (1011646)Termination phase: Saturation
% 21.05/3.48 % (1011646)Time elapsed: 0.207 s
% 21.05/3.48 % (1011646)Peak memory usage: 13 MB
% 21.05/3.48 % (1011646)Instructions burned: 232 (million)
% 21.05/3.48 % (1011656)lrs+10_1_sil=128000:si=on:urr=on:random_seed=877293800:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/212Mi)
% 21.05/3.48 % (1011655)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=4014652715:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/865Mi)
% 26.09/4.07 % (1011650)Instruction limit reached!
% 26.09/4.07 % (1011650)------------------------------
% 26.09/4.07 % (1011650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.09/4.07 % (1011650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.09/4.07 % (1011650)CaDiCaL version: 2.1.3
% 26.09/4.07 % (1011650)Termination reason: Instruction limit
% 26.09/4.07 % (1011650)Termination phase: Saturation
% 26.09/4.07 % (1011650)Time elapsed: 0.238 s
% 26.09/4.07 % (1011650)Peak memory usage: 15 MB
% 26.09/4.07 % (1011650)Instructions burned: 282 (million)
% 26.09/4.07 % (1011659)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2733267060:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/130Mi)
% 26.09/4.07 % (1011656)Instruction limit reached!
% 26.09/4.07 % (1011656)------------------------------
% 26.09/4.07 % (1011656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.09/4.07 % (1011656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.09/4.07 % (1011656)CaDiCaL version: 2.1.3
% 26.09/4.07 % (1011656)Termination reason: Instruction limit
% 26.09/4.07 % (1011656)Termination phase: Saturation
% 26.09/4.07 % (1011656)Time elapsed: 0.162 s
% 26.09/4.07 % (1011656)Peak memory usage: 15 MB
% 26.09/4.07 % (1011656)Instructions burned: 212 (million)
% 26.09/4.07 % (1011659)Instruction limit reached!
% 26.09/4.07 % (1011659)------------------------------
% 26.09/4.07 % (1011659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.09/4.07 % (1011659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.09/4.07 % (1011659)CaDiCaL version: 2.1.3
% 26.09/4.07 % (1011659)Termination reason: Instruction limit
% 26.09/4.07 % (1011659)Termination phase: Saturation
% 26.09/4.07 % (1011659)Time elapsed: 0.107 s
% 26.09/4.07 % (1011659)Peak memory usage: 17 MB
% 26.09/4.07 % (1011659)Instructions burned: 131 (million)
% 26.09/4.07 % (1011661)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=644673074:st=1.5:i=346:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/346Mi)
% 26.09/4.07 % (1011662)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=794502917:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/152Mi)
% 26.09/4.07 % (1011662)Instruction limit reached!
% 26.09/4.07 % (1011662)------------------------------
% 26.09/4.07 % (1011662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.09/4.07 % (1011662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.09/4.07 % (1011662)CaDiCaL version: 2.1.3
% 26.09/4.07 % (1011662)Termination reason: Instruction limit
% 26.09/4.07 % (1011662)Termination phase: Saturation
% 26.09/4.07 % (1011662)Time elapsed: 0.107 s
% 26.09/4.07 % (1011662)Peak memory usage: 12 MB
% 26.09/4.07 % (1011662)Instructions burned: 152 (million)
% 26.09/4.07 % (1011665)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1624621332:i=75:ep=R:rtra=on:ntd=on_2972 on theBenchmark for (2972ds/75Mi)
% 26.09/4.07 % (1011655)Instruction limit reached!
% 26.09/4.07 % (1011655)------------------------------
% 26.09/4.07 % (1011655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.09/4.07 % (1011655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.09/4.07 % (1011655)CaDiCaL version: 2.1.3
% 26.09/4.07 % (1011655)Termination reason: Instruction limit
% 26.09/4.07 % (1011655)Termination phase: Saturation
% 26.09/4.07 % (1011655)Time elapsed: 0.436 s
% 26.09/4.07 % (1011655)Peak memory usage: 34 MB
% 26.09/4.07 % (1011655)Instructions burned: 868 (million)
% 26.09/4.07 % (1011667)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=391733753:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/387Mi)
% 26.09/4.07 % (1011653)Instruction limit reached!
% 26.09/4.07 % (1011653)------------------------------
% 26.09/4.07 % (1011653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.09/4.07 % (1011653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.09/4.07 % (1011653)CaDiCaL version: 2.1.3
% 26.09/4.07 % (1011653)Termination reason: Instruction limit
% 26.09/4.07 % (1011653)Termination phase: Saturation
% 26.09/4.07 % (1011653)Time elapsed: 0.583 s
% 26.09/4.07 % (1011653)Peak memory usage: 46 MB
% 26.09/4.07 % (1011653)Instructions burned: 620 (million)
% 26.09/4.07 % (1011665)Instruction limit reached!
% 26.09/4.07 % (1011665)------------------------------
% 28.13/4.45 % (1011665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.13/4.45 % (1011665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.13/4.45 % (1011665)CaDiCaL version: 2.1.3
% 28.13/4.45 % (1011665)Termination reason: Instruction limit
% 28.13/4.45 % (1011665)Termination phase: Saturation
% 28.13/4.45 % (1011665)Time elapsed: 0.069 s
% 28.13/4.45 % (1011665)Peak memory usage: 15 MB
% 28.13/4.45 % (1011665)Instructions burned: 75 (million)
% 28.13/4.45 % (1011670)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=801491367:i=161:piset=and:rtra=on:ntd=on_2970 on theBenchmark for (2970ds/161Mi)
% 28.13/4.45 % (1011669)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=4198126361:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2970 on theBenchmark for (2970ds/148Mi)
% 28.13/4.45 % (1011661)Instruction limit reached!
% 28.13/4.45 % (1011661)------------------------------
% 28.13/4.45 % (1011661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.13/4.45 % (1011661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.13/4.45 % (1011661)CaDiCaL version: 2.1.3
% 28.13/4.45 % (1011661)Termination reason: Instruction limit
% 28.13/4.45 % (1011661)Termination phase: Saturation
% 28.13/4.45 % (1011661)Time elapsed: 0.312 s
% 28.13/4.45 % (1011661)Peak memory usage: 23 MB
% 28.13/4.45 % (1011661)Instructions burned: 346 (million)
% 28.13/4.45 % (1011673)lrs+10_1_sil=128000:si=on:random_seed=319591875:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/888Mi)
% 28.13/4.45 % (1011667)Instruction limit reached!
% 28.13/4.45 % (1011667)------------------------------
% 28.13/4.45 % (1011667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.13/4.45 % (1011667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.13/4.45 % (1011667)CaDiCaL version: 2.1.3
% 28.13/4.45 % (1011667)Termination reason: Instruction limit
% 28.13/4.45 % (1011667)Termination phase: Saturation
% 28.13/4.45 % (1011667)Time elapsed: 0.172 s
% 28.13/4.45 % (1011667)Peak memory usage: 21 MB
% 28.13/4.45 % (1011667)Instructions burned: 387 (million)
% 28.13/4.45 % (1011669)Instruction limit reached!
% 28.13/4.45 % (1011669)------------------------------
% 28.13/4.45 % (1011669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.13/4.45 % (1011669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.13/4.45 % (1011669)CaDiCaL version: 2.1.3
% 28.13/4.45 % (1011669)Termination reason: Instruction limit
% 28.13/4.45 % (1011669)Termination phase: Saturation
% 28.13/4.45 % (1011669)Time elapsed: 0.125 s
% 28.13/4.45 % (1011669)Peak memory usage: 13 MB
% 28.13/4.45 % (1011669)Instructions burned: 148 (million)
% 28.13/4.45 % (1011670)Instruction limit reached!
% 28.13/4.45 % (1011670)------------------------------
% 28.13/4.45 % (1011670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.13/4.45 % (1011670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.13/4.45 % (1011670)CaDiCaL version: 2.1.3
% 28.13/4.45 % (1011670)Termination reason: Instruction limit
% 28.13/4.45 % (1011670)Termination phase: Saturation
% 28.13/4.45 % (1011670)Time elapsed: 0.152 s
% 28.13/4.45 % (1011670)Peak memory usage: 20 MB
% 28.13/4.45 % (1011670)Instructions burned: 162 (million)
% 28.13/4.45 % (1011676)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=1985614961:i=88:s2at=3:nm=2:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/88Mi)
% 28.13/4.45 % (1011675)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=3333901429:i=136:add=on:ins=4:rtra=on:sup=off_2969 on theBenchmark for (2969ds/136Mi)
% 28.13/4.45 % (1011675)Refutation not found, incomplete strategy
% 28.13/4.45 % (1011675)------------------------------
% 28.13/4.45 % (1011675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.13/4.45 % (1011675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.13/4.45 % (1011675)CaDiCaL version: 2.1.3
% 28.13/4.45 % (1011675)Termination reason: Refutation not found, incomplete strategy
% 28.13/4.45 % (1011675)Time elapsed: 0.004 s
% 28.13/4.45 % (1011675)Peak memory usage: 12 MB
% 28.13/4.45 % (1011675)Instructions burned: 3 (million)
% 28.13/4.45 % (1011675)------------------------------
% 28.13/4.45 % (1011675)------------------------------
% 29.09/4.69 % (1011677)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=2483705891:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2969 on theBenchmark for (2969ds/93Mi)
% 29.09/4.69 % (1011680)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2416665738:i=2186:rtra=on:ixr=off_2968 on theBenchmark for (2968ds/2186Mi)
% 29.09/4.69 % (1011676)Instruction limit reached!
% 29.09/4.69 % (1011676)------------------------------
% 29.09/4.69 % (1011676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.09/4.69 % (1011676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.09/4.69 % (1011676)CaDiCaL version: 2.1.3
% 29.09/4.69 % (1011676)Termination reason: Instruction limit
% 29.09/4.69 % (1011676)Termination phase: Saturation
% 29.09/4.69 % (1011676)Time elapsed: 0.083 s
% 29.09/4.69 % (1011676)Peak memory usage: 16 MB
% 29.09/4.69 % (1011676)Instructions burned: 89 (million)
% 29.09/4.69 % (1011677)Instruction limit reached!
% 29.09/4.69 % (1011677)------------------------------
% 29.09/4.69 % (1011677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.09/4.69 % (1011677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.09/4.69 % (1011677)CaDiCaL version: 2.1.3
% 29.09/4.69 % (1011677)Termination reason: Instruction limit
% 29.09/4.69 % (1011677)Termination phase: Saturation
% 29.09/4.69 % (1011677)Time elapsed: 0.072 s
% 29.09/4.69 % (1011677)Peak memory usage: 14 MB
% 29.09/4.69 % (1011677)Instructions burned: 93 (million)
% 29.09/4.69 % (1011683)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3081717849:s2a=on:i=240:rtra=on:ntd=on_2968 on theBenchmark for (2968ds/240Mi)
% 29.09/4.69 % (1011684)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=3380478820:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2967 on theBenchmark for (2967ds/805Mi)
% 29.09/4.69 % (1011649)Instruction limit reached!
% 29.09/4.69 % (1011649)------------------------------
% 29.09/4.69 % (1011649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.09/4.69 % (1011649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.09/4.69 % (1011649)CaDiCaL version: 2.1.3
% 29.09/4.69 % (1011649)Termination reason: Instruction limit
% 29.09/4.69 % (1011649)Termination phase: Saturation
% 29.09/4.69 % (1011649)Time elapsed: 1.106 s
% 29.09/4.69 % (1011649)Peak memory usage: 61 MB
% 29.09/4.69 % (1011649)Instructions burned: 1255 (million)
% 29.09/4.69 % (1011687)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 29.09/4.69 % (1011687)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=2108064251:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2966 on theBenchmark for (2966ds/391Mi)
% 29.09/4.69 % (1011683)Instruction limit reached!
% 29.09/4.69 % (1011683)------------------------------
% 29.09/4.69 % (1011683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.09/4.69 % (1011683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.09/4.69 % (1011683)CaDiCaL version: 2.1.3
% 29.09/4.69 % (1011683)Termination reason: Instruction limit
% 29.09/4.69 % (1011683)Termination phase: Saturation
% 29.09/4.69 % (1011683)Time elapsed: 0.230 s
% 29.09/4.69 % (1011683)Peak memory usage: 26 MB
% 29.09/4.69 % (1011683)Instructions burned: 240 (million)
% 29.09/4.69 % (1011689)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=3407236780:i=355:av=off:fsr=off:rtra=on:ixr=off_2965 on theBenchmark for (2965ds/355Mi)
% 29.09/4.69 % (1011673)Instruction limit reached!
% 29.09/4.69 % (1011673)------------------------------
% 29.09/4.69 % (1011673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.09/4.69 % (1011673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.09/4.69 % (1011673)CaDiCaL version: 2.1.3
% 29.09/4.69 % (1011673)Termination reason: Instruction limit
% 29.09/4.69 % (1011673)Termination phase: Saturation
% 29.09/4.69 % (1011673)Time elapsed: 0.654 s
% 29.09/4.69 % (1011673)Peak memory usage: 23 MB
% 29.09/4.69 % (1011673)Instructions burned: 889 (million)
% 29.09/4.69 % (1011691)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=3100357525:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/314Mi)
% 33.12/5.15 % (1011687)Instruction limit reached!
% 33.12/5.15 % (1011687)------------------------------
% 33.12/5.15 % (1011687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/5.15 % (1011687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/5.15 % (1011687)CaDiCaL version: 2.1.3
% 33.12/5.15 % (1011687)Termination reason: Instruction limit
% 33.12/5.15 % (1011687)Termination phase: Saturation
% 33.12/5.15 % (1011687)Time elapsed: 0.315 s
% 33.12/5.15 % (1011687)Peak memory usage: 21 MB
% 33.12/5.15 % (1011687)Instructions burned: 392 (million)
% 33.12/5.15 % (1011693)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=2875599136:s2a=on:i=251:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/251Mi)
% 33.12/5.15 % (1011689)Instruction limit reached!
% 33.12/5.15 % (1011689)------------------------------
% 33.12/5.15 % (1011689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/5.15 % (1011689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/5.15 % (1011689)CaDiCaL version: 2.1.3
% 33.12/5.15 % (1011689)Termination reason: Instruction limit
% 33.12/5.15 % (1011689)Termination phase: Saturation
% 33.12/5.15 % (1011689)Time elapsed: 0.331 s
% 33.12/5.15 % (1011689)Peak memory usage: 34 MB
% 33.12/5.15 % (1011689)Instructions burned: 355 (million)
% 33.12/5.15 % (1011695)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=2574724527:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2961 on theBenchmark for (2961ds/2470Mi)
% 33.12/5.15 % (1011684)Instruction limit reached!
% 33.12/5.15 % (1011684)------------------------------
% 33.12/5.15 % (1011684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/5.15 % (1011684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/5.15 % (1011684)CaDiCaL version: 2.1.3
% 33.12/5.15 % (1011684)Termination reason: Instruction limit
% 33.12/5.15 % (1011684)Termination phase: Saturation
% 33.12/5.15 % (1011684)Time elapsed: 0.701 s
% 33.12/5.15 % (1011684)Peak memory usage: 45 MB
% 33.12/5.15 % (1011684)Instructions burned: 806 (million)
% 33.12/5.15 % (1011693)Instruction limit reached!
% 33.12/5.15 % (1011693)------------------------------
% 33.12/5.15 % (1011693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/5.15 % (1011693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/5.15 % (1011693)CaDiCaL version: 2.1.3
% 33.12/5.15 % (1011693)Termination reason: Instruction limit
% 33.12/5.15 % (1011693)Termination phase: Saturation
% 33.12/5.15 % (1011693)Time elapsed: 0.200 s
% 33.12/5.15 % (1011693)Peak memory usage: 21 MB
% 33.12/5.15 % (1011693)Instructions burned: 251 (million)
% 33.12/5.15 % (1011691)Instruction limit reached!
% 33.12/5.15 % (1011691)------------------------------
% 33.12/5.15 % (1011691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/5.15 % (1011691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/5.15 % (1011691)CaDiCaL version: 2.1.3
% 33.12/5.15 % (1011691)Termination reason: Instruction limit
% 33.12/5.15 % (1011691)Termination phase: Saturation
% 33.12/5.15 % (1011691)Time elapsed: 0.273 s
% 33.12/5.15 % (1011691)Peak memory usage: 23 MB
% 33.12/5.15 % (1011691)Instructions burned: 314 (million)
% 33.12/5.15 % (1011697)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=577903379:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2960 on theBenchmark for (2960ds/673Mi)
% 33.12/5.15 % (1011698)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3074089310:i=116:ep=RSTC:rtra=on:ntd=on_2960 on theBenchmark for (2960ds/116Mi)
% 33.12/5.15 % (1011700)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1992850791:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2960 on theBenchmark for (2960ds/270Mi)
% 33.12/5.15 % (1011698)Instruction limit reached!
% 33.12/5.15 % (1011698)------------------------------
% 33.12/5.15 % (1011698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/5.15 % (1011698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/5.15 % (1011698)CaDiCaL version: 2.1.3
% 33.12/5.15 % (1011698)Termination reason: Instruction limit
% 35.75/5.61 % (1011698)Termination phase: Saturation
% 35.75/5.61 % (1011698)Time elapsed: 0.095 s
% 35.75/5.61 % (1011698)Peak memory usage: 16 MB
% 35.75/5.61 % (1011698)Instructions burned: 118 (million)
% 35.75/5.61 % (1011680)Instruction limit reached!
% 35.75/5.61 % (1011680)------------------------------
% 35.75/5.61 % (1011680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.75/5.61 % (1011680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/5.61 % (1011680)CaDiCaL version: 2.1.3
% 35.75/5.61 % (1011680)Termination reason: Instruction limit
% 35.75/5.61 % (1011680)Termination phase: Saturation
% 35.75/5.61 % (1011680)Time elapsed: 0.954 s
% 35.75/5.61 % (1011680)Peak memory usage: 44 MB
% 35.75/5.61 % (1011680)Instructions burned: 2188 (million)
% 35.75/5.61 % (1011703)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=1784483077:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2959 on theBenchmark for (2959ds/30Mi)
% 35.75/5.61 % (1011704)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 35.75/5.61 % (1011704)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=1917581723:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2958 on theBenchmark for (2958ds/39Mi)
% 35.75/5.61 % (1011704)Instruction limit reached!
% 35.75/5.61 % (1011704)------------------------------
% 35.75/5.61 % (1011704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.75/5.61 % (1011704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/5.61 % (1011704)CaDiCaL version: 2.1.3
% 35.75/5.61 % (1011704)Termination reason: Instruction limit
% 35.75/5.61 % (1011704)Termination phase: Saturation
% 35.75/5.61 % (1011704)Time elapsed: 0.016 s
% 35.75/5.61 % (1011704)Peak memory usage: 12 MB
% 35.75/5.61 % (1011704)Instructions burned: 41 (million)
% 35.75/5.61 % (1011703)Instruction limit reached!
% 35.75/5.61 % (1011703)------------------------------
% 35.75/5.61 % (1011703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.75/5.61 % (1011703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/5.61 % (1011703)CaDiCaL version: 2.1.3
% 35.75/5.61 % (1011703)Termination reason: Instruction limit
% 35.75/5.61 % (1011703)Termination phase: Saturation
% 35.75/5.61 % (1011703)Time elapsed: 0.032 s
% 35.75/5.61 % (1011703)Peak memory usage: 12 MB
% 35.75/5.61 % (1011703)Instructions burned: 30 (million)
% 35.75/5.61 % (1011707)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2305623076:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2958 on theBenchmark for (2958ds/365Mi)
% 35.75/5.61 % (1011708)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3598332212:i=158:av=off:rtra=on_2958 on theBenchmark for (2958ds/158Mi)
% 35.75/5.61 % (1011700)Instruction limit reached!
% 35.75/5.61 % (1011700)------------------------------
% 35.75/5.61 % (1011700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.75/5.61 % (1011700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/5.61 % (1011700)CaDiCaL version: 2.1.3
% 35.75/5.61 % (1011700)Termination reason: Instruction limit
% 35.75/5.61 % (1011700)Termination phase: Saturation
% 35.75/5.61 % (1011700)Time elapsed: 0.195 s
% 35.75/5.61 % (1011700)Peak memory usage: 12 MB
% 35.75/5.61 % (1011700)Instructions burned: 270 (million)
% 35.75/5.61 % (1011711)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 35.75/5.61 % (1011711)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=4219458972:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2957 on theBenchmark for (2957ds/252Mi)
% 35.75/5.61 % (1011708)Instruction limit reached!
% 35.75/5.61 % (1011708)------------------------------
% 35.75/5.61 % (1011708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.75/5.61 % (1011708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/5.61 % (1011708)CaDiCaL version: 2.1.3
% 35.75/5.61 % (1011708)Termination reason: Instruction limit
% 35.75/5.61 % (1011708)Termination phase: Saturation
% 35.75/5.61 % (1011708)Time elapsed: 0.136 s
% 35.75/5.61 % (1011708)Peak memory usage: 13 MB
% 38.07/5.87 % (1011708)Instructions burned: 160 (million)
% 38.07/5.87 % (1011707)Instruction limit reached!
% 38.07/5.87 % (1011707)------------------------------
% 38.07/5.87 % (1011707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.07/5.87 % (1011707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/5.87 % (1011707)CaDiCaL version: 2.1.3
% 38.07/5.87 % (1011707)Termination reason: Instruction limit
% 38.07/5.87 % (1011707)Termination phase: Saturation
% 38.07/5.87 % (1011707)Time elapsed: 0.164 s
% 38.07/5.87 % (1011707)Peak memory usage: 26 MB
% 38.07/5.87 % (1011707)Instructions burned: 367 (million)
% 38.07/5.87 % (1011714)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=1214241657:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2956 on theBenchmark for (2956ds/160Mi)
% 38.07/5.87 % (1011713)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2417334872:i=213:rtra=on:ss=axioms_2956 on theBenchmark for (2956ds/213Mi)
% 38.07/5.87 % (1011714)Instruction limit reached!
% 38.07/5.87 % (1011714)------------------------------
% 38.07/5.87 % (1011714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.07/5.87 % (1011714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/5.87 % (1011714)CaDiCaL version: 2.1.3
% 38.07/5.87 % (1011714)Termination reason: Instruction limit
% 38.07/5.87 % (1011714)Termination phase: Saturation
% 38.07/5.87 % (1011714)Time elapsed: 0.098 s
% 38.07/5.87 % (1011714)Peak memory usage: 20 MB
% 38.07/5.87 % (1011714)Instructions burned: 163 (million)
% 38.07/5.87 % (1011717)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=2770633702:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2955 on theBenchmark for (2955ds/763Mi)
% 38.07/5.87 % (1011711)Instruction limit reached!
% 38.07/5.87 % (1011711)------------------------------
% 38.07/5.87 % (1011711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.07/5.87 % (1011711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/5.87 % (1011711)CaDiCaL version: 2.1.3
% 38.07/5.87 % (1011711)Termination reason: Instruction limit
% 38.07/5.87 % (1011711)Termination phase: Saturation
% 38.07/5.87 % (1011711)Time elapsed: 0.256 s
% 38.07/5.87 % (1011711)Peak memory usage: 26 MB
% 38.07/5.87 % (1011711)Instructions burned: 252 (million)
% 38.07/5.87 % (1011719)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 38.07/5.87 % (1011719)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2725908501:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2955 on theBenchmark for (2955ds/237Mi)
% 38.07/5.87 % (1011713)Instruction limit reached!
% 38.07/5.87 % (1011713)------------------------------
% 38.07/5.87 % (1011713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.07/5.87 % (1011713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/5.87 % (1011713)CaDiCaL version: 2.1.3
% 38.07/5.87 % (1011713)Termination reason: Instruction limit
% 38.07/5.87 % (1011713)Termination phase: Saturation
% 38.07/5.87 % (1011713)Time elapsed: 0.195 s
% 38.07/5.87 % (1011713)Peak memory usage: 24 MB
% 38.07/5.87 % (1011713)Instructions burned: 214 (million)
% 38.07/5.87 % (1011697)Instruction limit reached!
% 38.07/5.87 % (1011697)------------------------------
% 38.07/5.87 % (1011697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.07/5.87 % (1011697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/5.87 % (1011697)CaDiCaL version: 2.1.3
% 38.07/5.87 % (1011697)Termination reason: Instruction limit
% 38.07/5.87 % (1011697)Termination phase: Saturation
% 38.07/5.87 % (1011697)Time elapsed: 0.591 s
% 38.07/5.87 % (1011697)Peak memory usage: 59 MB
% 38.07/5.87 % (1011697)Instructions burned: 673 (million)
% 38.07/5.87 % (1011721)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=822022473:s2a=on:i=386:rtra=on:ntd=on_2954 on theBenchmark for (2954ds/386Mi)
% 38.07/5.87 % (1011722)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=215303330:i=300:piset=and:nm=32:rtra=on_2954 on theBenchmark for (2954ds/300Mi)
% 38.07/5.87 % (1011719)Instruction limit reached!
% 38.07/5.87 % (1011719)------------------------------
% 38.74/6.01 % (1011719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.01 % (1011719)CaDiCaL version: 2.1.3
% 38.74/6.01 % (1011719)Termination reason: Instruction limit
% 38.74/6.01 % (1011719)Termination phase: Saturation
% 38.74/6.01 % (1011719)Time elapsed: 0.244 s
% 38.74/6.01 % (1011719)Peak memory usage: 27 MB
% 38.74/6.01 % (1011719)Instructions burned: 237 (million)
% 38.74/6.01 % (1011725)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=1835891240:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2952 on theBenchmark for (2952ds/567Mi)
% 38.74/6.01 % (1011717)Instruction limit reached!
% 38.74/6.01 % (1011717)------------------------------
% 38.74/6.01 % (1011717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.01 % (1011717)CaDiCaL version: 2.1.3
% 38.74/6.01 % (1011717)Termination reason: Instruction limit
% 38.74/6.01 % (1011717)Termination phase: Saturation
% 38.74/6.01 % (1011717)Time elapsed: 0.373 s
% 38.74/6.01 % (1011717)Peak memory usage: 54 MB
% 38.74/6.01 % (1011717)Instructions burned: 766 (million)
% 38.74/6.01 % (1011727)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=3155495364:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2951 on theBenchmark for (2951ds/379Mi)
% 38.74/6.01 % (1011722)Instruction limit reached!
% 38.74/6.01 % (1011722)------------------------------
% 38.74/6.01 % (1011722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.01 % (1011722)CaDiCaL version: 2.1.3
% 38.74/6.01 % (1011722)Termination reason: Instruction limit
% 38.74/6.01 % (1011722)Termination phase: Saturation
% 38.74/6.01 % (1011722)Time elapsed: 0.316 s
% 38.74/6.01 % (1011722)Peak memory usage: 26 MB
% 38.74/6.01 % (1011722)Instructions burned: 300 (million)
% 38.74/6.01 % (1011721)Instruction limit reached!
% 38.74/6.01 % (1011721)------------------------------
% 38.74/6.01 % (1011721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.01 % (1011721)CaDiCaL version: 2.1.3
% 38.74/6.01 % (1011721)Termination reason: Instruction limit
% 38.74/6.01 % (1011721)Termination phase: Saturation
% 38.74/6.01 % (1011721)Time elapsed: 0.336 s
% 38.74/6.01 % (1011721)Peak memory usage: 20 MB
% 38.74/6.01 % (1011721)Instructions burned: 386 (million)
% 38.74/6.01 % (1011729)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=1811400033:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2950 on theBenchmark for (2950ds/429Mi)
% 38.74/6.01 % (1011730)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=1241108368:i=478:bd=all:rtra=on_2950 on theBenchmark for (2950ds/478Mi)
% 38.74/6.01 % (1011727)Instruction limit reached!
% 38.74/6.01 % (1011727)------------------------------
% 38.74/6.01 % (1011727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.01 % (1011727)CaDiCaL version: 2.1.3
% 38.74/6.01 % (1011727)Termination reason: Instruction limit
% 38.74/6.01 % (1011727)Termination phase: Saturation
% 38.74/6.01 % (1011727)Time elapsed: 0.167 s
% 38.74/6.01 % (1011727)Peak memory usage: 22 MB
% 38.74/6.01 % (1011727)Instructions burned: 381 (million)
% 38.74/6.01 % (1011733)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2036239285:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2949 on theBenchmark for (2949ds/445Mi)
% 38.74/6.01 % (1011733)Instruction limit reached!
% 38.74/6.01 % (1011733)------------------------------
% 38.74/6.01 % (1011733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.74/6.01 % (1011733)CaDiCaL version: 2.1.3
% 38.74/6.01 % (1011733)Termination reason: Instruction limit
% 38.74/6.01 % (1011733)Termination phase: Saturation
% 38.74/6.01 % (1011733)Time elapsed: 0.191 s
% 38.74/6.01 % (1011733)Peak memory usage: 15 MB
% 38.74/6.01 % (1011733)Instructions burned: 445 (million)
% 38.74/6.01 % (1011725)Instruction limit reached!
% 38.74/6.01 % (1011725)------------------------------
% 38.74/6.01 % (1011725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.74/6.01 % (1011725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011725)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011725)Termination reason: Instruction limit
% 41.57/6.33 % (1011725)Termination phase: Saturation
% 41.57/6.33 % (1011725)Time elapsed: 0.424 s
% 41.57/6.33 % (1011725)Peak memory usage: 20 MB
% 41.57/6.33 % (1011725)Instructions burned: 568 (million)
% 41.57/6.33 % (1011735)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=593869624:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2947 on theBenchmark for (2947ds/71Mi)
% 41.57/6.33 % (1011736)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=809454468:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2947 on theBenchmark for (2947ds/302Mi)
% 41.57/6.33 % (1011729)Instruction limit reached!
% 41.57/6.33 % (1011729)------------------------------
% 41.57/6.33 % (1011729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011729)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011729)Termination reason: Instruction limit
% 41.57/6.33 % (1011729)Termination phase: Saturation
% 41.57/6.33 % (1011729)Time elapsed: 0.324 s
% 41.57/6.33 % (1011729)Peak memory usage: 16 MB
% 41.57/6.33 % (1011729)Instructions burned: 429 (million)
% 41.57/6.33 % (1011735)Instruction limit reached!
% 41.57/6.33 % (1011735)------------------------------
% 41.57/6.33 % (1011735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011735)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011735)Termination reason: Instruction limit
% 41.57/6.33 % (1011735)Termination phase: Saturation
% 41.57/6.33 % (1011735)Time elapsed: 0.027 s
% 41.57/6.33 % (1011735)Peak memory usage: 12 MB
% 41.57/6.33 % (1011735)Instructions burned: 72 (million)
% 41.57/6.33 % (1011740)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 41.57/6.33 % (1011740)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 41.57/6.33 % (1011739)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=1092436319:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2947 on theBenchmark for (2947ds/4980Mi)
% 41.57/6.33 % (1011740)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=591433524:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2947 on theBenchmark for (2947ds/100Mi)
% 41.57/6.33 % (1011730)Instruction limit reached!
% 41.57/6.33 % (1011730)------------------------------
% 41.57/6.33 % (1011730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011730)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011730)Termination reason: Instruction limit
% 41.57/6.33 % (1011730)Termination phase: Saturation
% 41.57/6.33 % (1011730)Time elapsed: 0.450 s
% 41.57/6.33 % (1011730)Peak memory usage: 50 MB
% 41.57/6.33 % (1011730)Instructions burned: 478 (million)
% 41.57/6.33 % (1011740)Instruction limit reached!
% 41.57/6.33 % (1011740)------------------------------
% 41.57/6.33 % (1011740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011740)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011740)Termination reason: Instruction limit
% 41.57/6.33 % (1011740)Termination phase: Saturation
% 41.57/6.33 % (1011740)Time elapsed: 0.070 s
% 41.57/6.33 % (1011740)Peak memory usage: 11 MB
% 41.57/6.33 % (1011740)Instructions burned: 100 (million)
% 41.57/6.33 % (1011743)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3282101462:i=76:piset=equals:rtra=on:ntd=on_2945 on theBenchmark for (2945ds/76Mi)
% 41.57/6.33 % (1011744)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=2986747051:i=289:rtra=on_2945 on theBenchmark for (2945ds/289Mi)
% 41.57/6.33 % (1011743)Instruction limit reached!
% 41.57/6.33 % (1011743)------------------------------
% 41.57/6.33 % (1011743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011743)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011743)Termination reason: Instruction limit
% 41.57/6.33 % (1011743)Termination phase: Saturation
% 41.57/6.33 % (1011743)Time elapsed: 0.060 s
% 41.57/6.33 % (1011743)Peak memory usage: 14 MB
% 41.57/6.33 % (1011743)Instructions burned: 77 (million)
% 41.57/6.33 % (1011736)Instruction limit reached!
% 41.57/6.33 % (1011736)------------------------------
% 41.57/6.33 % (1011736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011736)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011736)Termination reason: Instruction limit
% 41.57/6.33 % (1011736)Termination phase: Saturation
% 41.57/6.33 % (1011736)Time elapsed: 0.250 s
% 41.57/6.33 % (1011736)Peak memory usage: 22 MB
% 41.57/6.33 % (1011736)Instructions burned: 303 (million)
% 41.57/6.33 % (1011747)lrs+2_64_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_first:bsr=unit_only:cbe=off:uwa=interpreted_only:nwc=0.5:slsqc=5:sac=on:slsq=on:random_seed=399795402:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2944 on theBenchmark for (2944ds/493Mi)
% 41.57/6.33 % (1011695)Instruction limit reached!
% 41.57/6.33 % (1011695)------------------------------
% 41.57/6.33 % (1011695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011695)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011695)Termination reason: Instruction limit
% 41.57/6.33 % (1011695)Termination phase: Saturation
% 41.57/6.33 % (1011695)Time elapsed: 1.688 s
% 41.57/6.33 % (1011695)Peak memory usage: 12 MB
% 41.57/6.33 % (1011695)Instructions burned: 2471 (million)
% 41.57/6.33 % (1011748)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=3497339678:cond=on:i=34:hud=10:nm=10:rtra=on_2944 on theBenchmark for (2944ds/34Mi)
% 41.57/6.33 % (1011750)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 41.57/6.33 % (1011750)dis+1010_1_to=lpo:irw=on:plsq=on:drc=ordering:plsqc=4:cnfonf=lazy_simp:si=on:sp=reverse_frequency:sos=on:plsqr=32,1:cbe=off:uwa=off:rp=on:lwlo=on:random_seed=316605147:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2944 on theBenchmark for (2944ds/372Mi)
% 41.57/6.33 % (1011748)Instruction limit reached!
% 41.57/6.33 % (1011748)------------------------------
% 41.57/6.33 % (1011748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011748)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011748)Termination reason: Instruction limit
% 41.57/6.33 % (1011748)Termination phase: Saturation
% 41.57/6.33 % (1011748)Time elapsed: 0.027 s
% 41.57/6.33 % (1011748)Peak memory usage: 12 MB
% 41.57/6.33 % (1011748)Instructions burned: 35 (million)
% 41.57/6.33 % (1011753)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=55941811:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2944 on theBenchmark for (2944ds/670Mi)
% 41.57/6.33 % (1011596)Instruction limit reached!
% 41.57/6.33 % (1011596)------------------------------
% 41.57/6.33 % (1011596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011596)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011596)Termination reason: Instruction limit
% 41.57/6.33 % (1011596)Termination phase: Saturation
% 41.57/6.33 % (1011596)Time elapsed: 4.455 s
% 41.57/6.33 % (1011596)Peak memory usage: 40 MB
% 41.57/6.33 % (1011596)Instructions burned: 5755 (million)
% 41.57/6.33 % (1011744)Instruction limit reached!
% 41.57/6.33 % (1011744)------------------------------
% 41.57/6.33 % (1011744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011744)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011744)Termination reason: Instruction limit
% 41.57/6.33 % (1011744)Termination phase: Saturation
% 41.57/6.33 % (1011744)Time elapsed: 0.176 s
% 41.57/6.33 % (1011744)Peak memory usage: 23 MB
% 41.57/6.33 % (1011744)Instructions burned: 291 (million)
% 41.57/6.33 % (1011755)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=4127180578:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2943 on theBenchmark for (2943ds/647Mi)
% 41.57/6.33 % (1011756)dis+10_128_sil=128000:tgt=full:plsq=on:plsqc=3:cnfonf=off:si=on:sp=arity:spb=goal_then_units:uwa=one_side_interpreted:nwc=1.5:random_seed=435117157:i=857:add=off:kws=frequency:rtra=on:ntd=on_2943 on theBenchmark for (2943ds/857Mi)
% 41.57/6.33 % (1011750)Instruction limit reached!
% 41.57/6.33 % (1011750)------------------------------
% 41.57/6.33 % (1011750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011750)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011750)Termination reason: Instruction limit
% 41.57/6.33 % (1011750)Termination phase: Saturation
% 41.57/6.33 % (1011750)Time elapsed: 0.329 s
% 41.57/6.33 % (1011750)Peak memory usage: 17 MB
% 41.57/6.33 % (1011750)Instructions burned: 373 (million)
% 41.57/6.33 % (1011627) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1011458-1011627"...
% 41.57/6.33 % (1011755)Instruction limit reached!
% 41.57/6.33 % (1011755)------------------------------
% 41.57/6.33 % (1011755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.33 % (1011755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.33 % (1011755)CaDiCaL version: 2.1.3
% 41.57/6.33 % (1011755)Termination reason: Instruction limit
% 41.57/6.33 % (1011755)Termination phase: Saturation
% 41.57/6.33 % (1011755)Time elapsed: 0.274 s
% 41.57/6.33 % (1011755)Peak memory usage: 14 MB
% 41.57/6.33 % (1011755)Instructions burned: 647 (million)
% 41.57/6.33 % (1011760)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=1704228349:i=285:hud=10:bd=all:rtra=on:ss=axioms_2940 on theBenchmark for (2940ds/285Mi)
% 41.57/6.33 % (1011759)dis+1010_4_anc=all_dependent:to=lpo:sil=128000:fde=unused:cnfonf=conj_eager:si=on:sp=reverse_frequency:lma=off:spb=intro:cbe=off:uwa=off:random_seed=3090431660:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2940 on theBenchmark for (2940ds/693Mi)
% 41.57/6.33 % (1011627)...printing done.
% 41.57/6.33 % (1011627)Refutation found. Thanks to Tanya!
% 41.57/6.33 % SZS status Theorem for theBenchmark
% 41.57/6.33 % SZS output start Proof for theBenchmark
% See solution above
% 41.57/6.34 % (1011627)------------------------------
% 41.57/6.34 % (1011627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.34 % (1011627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.34 % (1011627)CaDiCaL version: 2.1.3
% 41.57/6.34 % (1011627)Termination reason: Refutation
% 41.57/6.34 % (1011627)Time elapsed: 4.216 s
% 41.57/6.34 % (1011627)Peak memory usage: 522 MB
% 41.57/6.34 % (1011627)Instructions burned: 4247 (million)
% 41.57/6.34 % (1011458)Success in time 5.965 s
% 41.57/6.34 % Vampire exiting
%------------------------------------------------------------------------------