%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL944^8 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:14:54 AM UTC 2026
% Result : Theorem 17.40s 3.18s
% Output : Refutation 17.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 10
% Syntax : Number of formulae : 67 ( 58 unt; 0 typ; 0 def)
% Number of atoms : 658 ( 55 equ; 0 cnn)
% Maximal formula atoms : 22 ( 9 avg)
% Number of connectives : 1451 ( 6 ~; 0 |; 8 &;1123 @)
% ( 0 <=>; 173 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 85 ( 85 >; 0 *; 0 +; 0 <<)
% Number of symbols : 78 ( 74 usr; 9 con; 0-4 aty)
% ( 141 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 321 ( 309 ^; 12 !; 0 ?; 321 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
mworld: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
mrel: mworld > mworld > $o ).
thf(func_def_1,type,
mactual: mworld ).
thf(func_def_2,type,
mlocal: ( mworld > $o ) > $o ).
thf(func_def_4,type,
mnot: ( mworld > $o ) > mworld > $o ).
thf(func_def_5,type,
mand: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_6,type,
mor: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_7,type,
mimplies: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_8,type,
mequiv: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_9,type,
mbox: ( mworld > $o ) > mworld > $o ).
thf(func_def_10,type,
mdia: ( mworld > $o ) > mworld > $o ).
thf(func_def_11,type,
eiw_di: $i > mworld > $o ).
thf(func_def_12,type,
mforall_di: ( $i > mworld > $o ) > mworld > $o ).
thf(func_def_13,type,
mexists_di: ( $i > mworld > $o ) > mworld > $o ).
thf(func_def_14,type,
r2: mworld > $o ).
thf(func_def_15,type,
r3: mworld > $o ).
thf(func_def_16,type,
r4: mworld > $o ).
thf(func_def_17,type,
r5: mworld > $o ).
thf(func_def_18,type,
equivalence_1: mworld > $o ).
thf(func_def_19,type,
equivalence_2: mworld > $o ).
thf(func_def_20,type,
cn2: mworld > $o ).
thf(func_def_21,type,
cn1: mworld > $o ).
thf(func_def_22,type,
cn3: mworld > $o ).
thf(func_def_23,type,
kn2: mworld > $o ).
thf(func_def_24,type,
kn1: mworld > $o ).
thf(func_def_25,type,
kn3: mworld > $o ).
thf(func_def_26,type,
equivalence_3: mworld > $o ).
thf(func_def_27,type,
op_implies_or: mworld > $o ).
thf(func_def_28,type,
op_and: mworld > $o ).
thf(func_def_29,type,
and_2: mworld > $o ).
thf(func_def_30,type,
and_3: mworld > $o ).
thf(func_def_31,type,
and_1: mworld > $o ).
thf(func_def_32,type,
implies_2: mworld > $o ).
thf(func_def_33,type,
implies_3: mworld > $o ).
thf(func_def_34,type,
op_implies_and: mworld > $o ).
thf(func_def_35,type,
implies_1: mworld > $o ).
thf(func_def_36,type,
substitution_of_equivalents: mworld > $o ).
thf(func_def_37,type,
op_or: mworld > $o ).
thf(func_def_38,type,
modus_tollens: mworld > $o ).
thf(func_def_39,type,
or_1: mworld > $o ).
thf(func_def_40,type,
or_2: mworld > $o ).
thf(func_def_41,type,
or_3: mworld > $o ).
thf(func_def_42,type,
op_equiv: mworld > $o ).
thf(func_def_43,type,
modus_ponens: mworld > $o ).
thf(func_def_44,type,
r1: mworld > $o ).
thf(func_def_45,type,
qmltpeq: $i > $i > mworld > $o ).
thf(func_def_46,type,
is_a_theorem: $i > mworld > $o ).
thf(func_def_47,type,
equiv: $i > $i > $i ).
thf(func_def_48,type,
not: $i > $i ).
thf(func_def_49,type,
or: $i > $i > $i ).
thf(func_def_50,type,
and: $i > $i > $i ).
thf(func_def_51,type,
implies: $i > $i > $i ).
thf(func_def_52,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_53,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_54,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_57,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_58,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_59,type,
vIMP: $o > $o > $o ).
thf(func_def_60,type,
vIFF: $o > $o > $o ).
thf(func_def_61,type,
vOR: $o > $o > $o ).
thf(func_def_62,type,
vNOT: $o > $o ).
thf(func_def_63,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_64,type,
vAND: $o > $o > $o ).
thf(func_def_65,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_66,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_67,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_68,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_69,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_70,type,
sK0: mworld ).
thf(func_def_71,type,
sK1: mworld > $i ).
thf(func_def_73,type,
sK3: mworld ).
thf(func_def_74,type,
sK4: mworld ).
thf(func_def_75,type,
sK5: mworld ).
thf(func_def_77,type,
sK7: mworld ).
thf(f1,axiom,
( ( ^ [X0: mworld > $o] : ( X0 @ mactual ) )
= mlocal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mlocal_def) ).
thf(f3,axiom,
( mand
= ( ^ [X0: mworld > $o,X1: mworld > $o,X2: mworld] :
( ( X1 @ X2 )
& ( X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mand_def) ).
thf(f5,axiom,
( ( ^ [X0: mworld > $o,X1: mworld > $o,X2: mworld] :
( ( X0 @ X2 )
=> ( X1 @ X2 ) ) )
= mimplies ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mimplies_def) ).
thf(f7,axiom,
( ( ^ [X0: mworld > $o,X1: mworld] :
! [X2: mworld] :
( ( mrel @ X1 @ X2 )
=> ( X0 @ X2 ) ) )
= mbox ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mbox_def) ).
thf(f9,axiom,
! [X0: mworld] : ( mrel @ X0 @ X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_reflexive) ).
thf(f11,axiom,
( ( ^ [X0: $i > mworld > $o,X1: mworld] :
! [X2: $i] :
( ( eiw_di @ X2 @ X1 )
=> ( X0 @ X2 @ X1 ) ) )
= mforall_di ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mforall_di_def) ).
thf(f36,axiom,
( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ or_2 )
@ ( mbox
@ ( mforall_di
@ ^ [X0: $i] :
( mbox
@ ( mforall_di
@ ^ [X1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X1 @ ( or @ X0 @ X1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [X0: $i] :
( mbox
@ ( mforall_di
@ ^ [X1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X1 @ ( or @ X0 @ X1 ) ) ) ) ) ) ) )
@ ( mbox @ or_2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_2_0) ).
thf(f48,axiom,
( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ r2 )
@ ( mbox
@ ( mforall_di
@ ^ [X0: $i] :
( mbox
@ ( mforall_di
@ ^ [X1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X1 @ ( or @ X0 @ X1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [X0: $i] :
( mbox
@ ( mforall_di
@ ^ [X1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X1 @ ( or @ X0 @ X1 ) ) ) ) ) ) ) )
@ ( mbox @ r2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r2_0) ).
thf(f69,axiom,
mlocal @ ( mbox @ or_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_2) ).
thf(f78,conjecture,
mlocal @ ( mbox @ r2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',principia_r2) ).
thf(f79,negated_conjecture,
~ ( mlocal @ ( mbox @ r2 ) ),
inference(negated_conjecture,[status(cth)],[f78]) ).
thf(f96,plain,
( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ or_2 )
@ ( mbox
@ ( mforall_di
@ ^ [X0: $i] :
( mbox
@ ( mforall_di
@ ^ [X1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X1 @ ( or @ X0 @ X1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [X2: $i] :
( mbox
@ ( mforall_di
@ ^ [X3: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X3 @ ( or @ X2 @ X3 ) ) ) ) ) ) ) )
@ ( mbox @ or_2 ) ) ) ) ),
inference(rectify,[],[f36]) ).
thf(f97,plain,
( $true
= ( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ or_2 )
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) )
@ ( mbox @ or_2 ) ) ) ) ) ),
inference(fool_elimination,[],[f96]) ).
thf(f104,plain,
( ( ^ [X0: mworld > $o,X1: mworld] :
! [X2: mworld] :
( ( mrel @ X1 @ X2 )
=> ( X0 @ X2 ) ) )
= mbox ),
inference(rectify,[],[f7]) ).
thf(f105,plain,
( mbox
= ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) ) ) ),
inference(fool_elimination,[],[f104]) ).
thf(f122,plain,
! [X0: mworld] : ( mrel @ X0 @ X0 ),
inference(rectify,[],[f9]) ).
thf(f123,plain,
( $true
= ( !! @ mworld
@ ^ [Y0: mworld] : ( mrel @ Y0 @ Y0 ) ) ),
inference(fool_elimination,[],[f122]) ).
thf(f126,plain,
( ( ^ [X0: $i > mworld > $o,X1: mworld] :
! [X2: $i] :
( ( eiw_di @ X2 @ X1 )
=> ( X0 @ X2 @ X1 ) ) )
= mforall_di ),
inference(rectify,[],[f11]) ).
thf(f127,plain,
( mforall_di
= ( ^ [Y0: $i > mworld > $o,Y1: mworld] :
( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) ) ) ),
inference(fool_elimination,[],[f126]) ).
thf(f128,plain,
~ ( mlocal @ ( mbox @ r2 ) ),
inference(rectify,[],[f79]) ).
thf(f129,plain,
( $true
= ( ~ ( mlocal @ ( mbox @ r2 ) ) ) ),
inference(fool_elimination,[],[f128]) ).
thf(f134,plain,
( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ r2 )
@ ( mbox
@ ( mforall_di
@ ^ [X0: $i] :
( mbox
@ ( mforall_di
@ ^ [X1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X1 @ ( or @ X0 @ X1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [X2: $i] :
( mbox
@ ( mforall_di
@ ^ [X3: $i] : ( mbox @ ( is_a_theorem @ ( implies @ X3 @ ( or @ X2 @ X3 ) ) ) ) ) ) ) )
@ ( mbox @ r2 ) ) ) ) ),
inference(rectify,[],[f48]) ).
thf(f135,plain,
( $true
= ( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ r2 )
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) )
@ ( mbox @ r2 ) ) ) ) ) ),
inference(fool_elimination,[],[f134]) ).
thf(f144,plain,
( ( ^ [X0: mworld > $o,X1: mworld > $o,X2: mworld] :
( ( X0 @ X2 )
=> ( X1 @ X2 ) ) )
= mimplies ),
inference(rectify,[],[f5]) ).
thf(f145,plain,
( mimplies
= ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f144]) ).
thf(f154,plain,
( mand
= ( ^ [X0: mworld > $o,X1: mworld > $o,X2: mworld] :
( ( X1 @ X2 )
& ( X0 @ X2 ) ) ) ),
inference(rectify,[],[f3]) ).
thf(f155,plain,
( mand
= ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
& ( Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f154]) ).
thf(f200,plain,
( mlocal
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual ) ) ),
inference(fool_elimination,[],[f1]) ).
thf(f211,plain,
mlocal @ ( mbox @ or_2 ),
inference(rectify,[],[f69]) ).
thf(f212,plain,
( ( mlocal @ ( mbox @ or_2 ) )
= $true ),
inference(fool_elimination,[],[f211]) ).
thf(f244,plain,
( $true
= ( !! @ mworld
@ ^ [Y0: mworld] : ( mrel @ Y0 @ Y0 ) ) ),
inference(cnf_transformation,[],[f123]) ).
thf(f263,plain,
( mforall_di
= ( ^ [Y0: $i > mworld > $o,Y1: mworld] :
( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[],[f127]) ).
thf(f267,plain,
( mlocal
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual ) ) ),
inference(cnf_transformation,[],[f200]) ).
thf(f277,plain,
( mimplies
= ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f145]) ).
thf(f282,plain,
( $true
= ( ~ ( mlocal @ ( mbox @ r2 ) ) ) ),
inference(cnf_transformation,[],[f129]) ).
thf(f284,plain,
( mbox
= ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) ) ) ),
inference(cnf_transformation,[],[f105]) ).
thf(f289,plain,
( mand
= ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
& ( Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f155]) ).
thf(f290,plain,
( ( mlocal @ ( mbox @ or_2 ) )
= $true ),
inference(cnf_transformation,[],[f212]) ).
thf(f298,plain,
( $true
= ( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ r2 )
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) )
@ ( mbox @ r2 ) ) ) ) ) ),
inference(cnf_transformation,[],[f135]) ).
thf(f301,plain,
( $true
= ( mlocal
@ ( mand
@ ( mbox
@ ( mimplies @ ( mbox @ or_2 )
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) )
@ ( mbox
@ ( mimplies
@ ( mbox
@ ( mforall_di
@ ^ [Y0: $i] :
( mbox
@ ( mforall_di
@ ^ [Y1: $i] : ( mbox @ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) )
@ ( mbox @ or_2 ) ) ) ) ) ),
inference(cnf_transformation,[],[f97]) ).
thf(f356,plain,
( $true
= ( ~ ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ r2 ) ) ) ),
inference(definition_unfolding,[],[f282,f267,f284]) ).
thf(f360,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ or_2 ) ) ),
inference(definition_unfolding,[],[f290,f267,f284]) ).
thf(f368,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
& ( Y1 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ r2 )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: $i > mworld > $o,Y1: mworld] :
( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) )
@ ^ [Y0: $i] :
( ^ [Y1: mworld > $o,Y2: mworld] :
( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ ( ^ [Y1: $i > mworld > $o,Y2: mworld] :
( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) )
@ ^ [Y1: $i] :
( ^ [Y2: mworld > $o,Y3: mworld] :
( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: $i > mworld > $o,Y1: mworld] :
( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) )
@ ^ [Y0: $i] :
( ^ [Y1: mworld > $o,Y2: mworld] :
( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ ( ^ [Y1: $i > mworld > $o,Y2: mworld] :
( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) )
@ ^ [Y1: $i] :
( ^ [Y2: mworld > $o,Y3: mworld] :
( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ r2 ) ) ) ) ) ),
inference(definition_unfolding,[],[f298,f267,f289,f284,f277,f284,f284,f263,f284,f263,f284,f284,f277,f284,f263,f284,f263,f284,f284]) ).
thf(f369,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
& ( Y1 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ or_2 )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: $i > mworld > $o,Y1: mworld] :
( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) )
@ ^ [Y0: $i] :
( ^ [Y1: mworld > $o,Y2: mworld] :
( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ ( ^ [Y1: $i > mworld > $o,Y2: mworld] :
( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) )
@ ^ [Y1: $i] :
( ^ [Y2: mworld > $o,Y3: mworld] :
( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: $i > mworld > $o,Y1: mworld] :
( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( Y0 @ Y2 @ Y1 ) ) )
@ ^ [Y0: $i] :
( ^ [Y1: mworld > $o,Y2: mworld] :
( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y2 @ Y3 )
=> ( Y1 @ Y3 ) ) )
@ ( ^ [Y1: $i > mworld > $o,Y2: mworld] :
( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( Y1 @ Y3 @ Y2 ) ) )
@ ^ [Y1: $i] :
( ^ [Y2: mworld > $o,Y3: mworld] :
( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ ( is_a_theorem @ ( implies @ Y1 @ ( or @ Y0 @ Y1 ) ) ) ) ) ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ or_2 ) ) ) ) ) ),
inference(definition_unfolding,[],[f301,f267,f289,f284,f277,f284,f284,f263,f284,f263,f284,f284,f277,f284,f263,f284,f263,f284,f284]) ).
thf(f390,plain,
( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( or_2 @ Y0 ) ) ) ),
inference(beta-eta_normalization,[],[f360]) ).
thf(f397,plain,
( $true
= ( ~ ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( r2 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f356]) ).
thf(f411,plain,
( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( or_2 @ Y1 ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( or_2 @ Y1 ) ) ) ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f369]) ).
thf(f436,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( r2 @ Y1 ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( r2 @ Y1 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f368]) ).
thf(f447,plain,
( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( r2 @ Y0 ) ) )
= $false ),
inference(not_proxy_clausification,[],[f397]) ).
thf(f454,plain,
! [X1: mworld] :
( $true
= ( ^ [Y0: mworld] : ( mrel @ Y0 @ Y0 )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f244]) ).
thf(f455,plain,
! [X1: mworld] :
( $true
= ( mrel @ X1 @ X1 ) ),
inference(beta-eta_normalization,[],[f454]) ).
thf(f1062,plain,
( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( or_2 @ Y1 ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f411]) ).
thf(f1065,plain,
( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( r2 @ Y1 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f436]) ).
thf(f1656,plain,
! [X1: mworld] :
( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( or_2 @ Y1 ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f1062]) ).
thf(f1657,plain,
! [X1: mworld] :
( ( ( mrel @ mactual @ X1 )
=> ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( or_2 @ Y0 ) ) )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f1656]) ).
thf(f1665,plain,
( $true
= ( $true
=> ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( or_2 @ Y0 ) ) )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(superposition,[],[f1657,f455]) ).
thf(f1668,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( or_2 @ Y0 ) ) )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(boolean_simplification,[],[f1665]) ).
thf(f1670,plain,
( $true
= ( $true
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(forward_demodulation,[],[f1668,f390]) ).
thf(f1671,plain,
( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) )
= $true ),
inference(boolean_simplification,[],[f1670]) ).
thf(f1674,plain,
! [X1: mworld] :
( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( eiw_di @ Y2 @ Y1 )
=> ( !! @ mworld
@ ^ [Y3: mworld] :
( ( mrel @ Y1 @ Y3 )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( eiw_di @ Y4 @ Y3 )
=> ( !! @ mworld
@ ^ [Y5: mworld] :
( ( mrel @ Y3 @ Y5 )
=> ( is_a_theorem @ ( implies @ Y4 @ ( or @ Y2 @ Y4 ) ) @ Y5 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( r2 @ Y1 ) ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f1065]) ).
thf(f1675,plain,
! [X1: mworld] :
( $true
= ( ( mrel @ mactual @ X1 )
=> ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( r2 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1674]) ).
thf(f1680,plain,
( $true
= ( $true
=> ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( r2 @ Y0 ) ) ) ) ) ),
inference(superposition,[],[f1675,f455]) ).
thf(f1683,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( eiw_di @ Y1 @ Y0 )
=> ( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y0 @ Y2 )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( eiw_di @ Y3 @ Y2 )
=> ( !! @ mworld
@ ^ [Y4: mworld] :
( ( mrel @ Y2 @ Y4 )
=> ( is_a_theorem @ ( implies @ Y3 @ ( or @ Y1 @ Y3 ) ) @ Y4 ) ) ) ) ) ) ) ) ) ) )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( r2 @ Y0 ) ) ) ) ),
inference(boolean_simplification,[],[f1680]) ).
thf(f1685,plain,
( $true
= ( $true
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( r2 @ Y0 ) ) ) ) ),
inference(forward_demodulation,[],[f1683,f1671]) ).
thf(f1686,plain,
( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( r2 @ Y0 ) ) ) ),
inference(boolean_simplification,[],[f1685]) ).
thf(f1687,plain,
$true = $false,
inference(forward_demodulation,[],[f1686,f447]) ).
thf(f1688,plain,
$false,
inference(trivial_inequality_removal,[],[f1687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL944^8 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n018.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 10:50:26 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.72/0.41 % (4118893)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.72/0.41 % (4118904)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.72/0.41 % (4118904)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
% 0.72/0.41 % (4118898)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4119558004:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.72/0.41 % (4118899)lrs+10_16_si=on:nwc=1.5:random_seed=1060919689:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.72/0.41 % (4118900)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3837300264:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.72/0.41 % (4118901)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=2561262313: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)
% 0.72/0.41 % (4118904)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=2639456084:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.72/0.41 % (4118900)Instruction limit reached!
% 0.72/0.41 % (4118900)------------------------------
% 0.72/0.41 % (4118900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (4118900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (4118900)CaDiCaL version: 2.1.3
% 0.72/0.41 % (4118900)Termination reason: Instruction limit
% 0.72/0.41 % (4118900)Termination phase: shuffling
% 0.72/0.41 % (4118900)Time elapsed: 0.002 s
% 0.72/0.41 % (4118900)Peak memory usage: 10 MB
% 0.72/0.41 % (4118900)Instructions burned: 4 (million)
% 0.72/0.41 % (4118902)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=355614107:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.72/0.41 % (4118899)Instruction limit reached!
% 0.72/0.41 % (4118899)------------------------------
% 0.72/0.41 % (4118899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (4118899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (4118899)CaDiCaL version: 2.1.3
% 0.72/0.41 % (4118899)Termination reason: Instruction limit
% 0.72/0.41 % (4118899)Termination phase: Property scanning
% 0.72/0.41 % (4118899)Time elapsed: 0.008 s
% 0.72/0.41 % (4118899)Peak memory usage: 10 MB
% 0.72/0.41 % (4118899)Instructions burned: 21 (million)
% 0.72/0.41 % (4118902)Instruction limit reached!
% 0.72/0.41 % (4118902)------------------------------
% 0.72/0.41 % (4118902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (4118902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (4118902)CaDiCaL version: 2.1.3
% 0.72/0.41 % (4118903)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=20250314:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.72/0.41 % (4118902)Termination reason: Instruction limit
% 0.72/0.41 % (4118902)Termination phase: Property scanning
% 0.72/0.41 % (4118902)Time elapsed: 0.009 s
% 0.72/0.41 % (4118902)Peak memory usage: 10 MB
% 0.72/0.41 % (4118902)Instructions burned: 24 (million)
% 0.72/0.41 % (4118911)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2739024564:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.41 % (4118911)Instruction limit reached!
% 0.72/0.41 % (4118911)------------------------------
% 0.72/0.41 % (4118911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (4118911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (4118911)CaDiCaL version: 2.1.3
% 0.72/0.41 % (4118911)Termination reason: Instruction limit
% 0.72/0.41 % (4118911)Termination phase: shuffling
% 0.72/0.41 % (4118911)Time elapsed: 0.002 s
% 0.72/0.41 % (4118911)Peak memory usage: 10 MB
% 0.72/0.41 % (4118911)Instructions burned: 5 (million)
% 0.72/0.41 % (4118912)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=828992016:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.72/0.44 % (4118912)Instruction limit reached!
% 0.72/0.44 % (4118912)------------------------------
% 0.72/0.44 % (4118912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (4118912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (4118912)CaDiCaL version: 2.1.3
% 0.72/0.44 % (4118912)Termination reason: Instruction limit
% 0.72/0.44 % (4118912)Termination phase: shuffling
% 0.72/0.44 % (4118912)Time elapsed: 0.003 s
% 0.72/0.44 % (4118912)Peak memory usage: 10 MB
% 0.72/0.44 % (4118912)Instructions burned: 7 (million)
% 0.72/0.44 % (4118914)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.44 % (4118914)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3040484665:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.72/0.44 % (4118914)Instruction limit reached!
% 0.72/0.44 % (4118914)------------------------------
% 0.72/0.44 % (4118914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (4118914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (4118914)CaDiCaL version: 2.1.3
% 0.72/0.44 % (4118914)Termination reason: Instruction limit
% 0.72/0.44 % (4118914)Termination phase: Property scanning
% 0.72/0.44 % (4118914)Time elapsed: 0.003 s
% 0.72/0.44 % (4118914)Peak memory usage: 10 MB
% 0.72/0.44 % (4118914)Instructions burned: 13 (million)
% 0.72/0.44 % (4118898)Instruction limit reached!
% 0.72/0.44 % (4118898)------------------------------
% 0.72/0.44 % (4118898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (4118898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (4118898)CaDiCaL version: 2.1.3
% 0.72/0.44 % (4118898)Termination reason: Instruction limit
% 0.72/0.44 % (4118898)Termination phase: Saturation
% 0.72/0.44 % (4118898)Time elapsed: 0.046 s
% 0.72/0.44 % (4118898)Peak memory usage: 11 MB
% 0.72/0.44 % (4118898)Instructions burned: 88 (million)
% 0.72/0.44 % (4118918)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
% 0.72/0.44 % (4118918)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.44 % (4118916)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3314088066:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.72/0.44 % (4118918)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=873391866:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.72/0.44 % (4118916)Instruction limit reached!
% 0.72/0.44 % (4118916)------------------------------
% 0.72/0.44 % (4118916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (4118916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (4118916)CaDiCaL version: 2.1.3
% 0.72/0.44 % (4118916)Termination reason: Instruction limit
% 0.72/0.44 % (4118916)Termination phase: shuffling
% 0.72/0.44 % (4118916)Time elapsed: 0.006 s
% 0.72/0.44 % (4118916)Peak memory usage: 10 MB
% 0.72/0.44 % (4118916)Instructions burned: 15 (million)
% 0.72/0.44 % (4118918)Instruction limit reached!
% 0.72/0.44 % (4118918)------------------------------
% 0.72/0.44 % (4118918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.44 % (4118918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.44 % (4118918)CaDiCaL version: 2.1.3
% 0.72/0.44 % (4118918)Termination reason: Instruction limit
% 0.72/0.44 % (4118918)Termination phase: Function definition elimination
% 0.72/0.44 % (4118918)Time elapsed: 0.011 s
% 0.72/0.44 % (4118918)Peak memory usage: 10 MB
% 0.72/0.44 % (4118918)Instructions burned: 28 (million)
% 0.72/0.44 % (4118921)lrs+10_1_si=on:cs=on:random_seed=2510161998:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.72/0.44 % (4118924)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.72/0.44 % (4118904)Instruction limit reached!
% 0.72/0.44 % (4118904)------------------------------
% 0.72/0.47 % (4118904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (4118904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (4118904)CaDiCaL version: 2.1.3
% 0.72/0.47 % (4118904)Termination reason: Instruction limit
% 0.72/0.47 % (4118904)Termination phase: Saturation
% 0.72/0.47 % (4118904)Time elapsed: 0.066 s
% 0.72/0.47 % (4118904)Peak memory usage: 13 MB
% 0.72/0.47 % (4118904)Instructions burned: 157 (million)
% 0.72/0.47 % (4118903)Instruction limit reached!
% 0.72/0.47 % (4118903)------------------------------
% 0.72/0.47 % (4118903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (4118903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (4118903)CaDiCaL version: 2.1.3
% 0.72/0.47 % (4118903)Termination reason: Instruction limit
% 0.72/0.47 % (4118903)Termination phase: Property scanning
% 0.72/0.47 % (4118903)Time elapsed: 0.055 s
% 0.72/0.47 % (4118903)Peak memory usage: 11 MB
% 0.72/0.47 % (4118903)Instructions burned: 76 (million)
% 0.72/0.47 % (4118921)Instruction limit reached!
% 0.72/0.47 % (4118921)------------------------------
% 0.72/0.47 % (4118921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (4118921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (4118921)CaDiCaL version: 2.1.3
% 0.72/0.47 % (4118921)Termination reason: Instruction limit
% 0.72/0.47 % (4118921)Termination phase: shuffling
% 0.72/0.47 % (4118921)Time elapsed: 0.003 s
% 0.72/0.47 % (4118921)Peak memory usage: 10 MB
% 0.72/0.47 % (4118921)Instructions burned: 12 (million)
% 0.72/0.47 % (4118924)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=176600816:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.47 % (4118924)Instruction limit reached!
% 0.72/0.47 % (4118924)------------------------------
% 0.72/0.47 % (4118924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (4118924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (4118924)CaDiCaL version: 2.1.3
% 0.72/0.47 % (4118924)Termination reason: Instruction limit
% 0.72/0.47 % (4118924)Termination phase: shuffling
% 0.72/0.47 % (4118924)Time elapsed: 0.002 s
% 0.72/0.47 % (4118924)Peak memory usage: 10 MB
% 0.72/0.47 % (4118924)Instructions burned: 5 (million)
% 0.72/0.47 % (4118927)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3665421495:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.72/0.47 % (4118920)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=2941924084:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.72/0.47 % (4118927)Refutation not found, incomplete strategy
% 0.72/0.47 % (4118927)------------------------------
% 0.72/0.47 % (4118927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (4118927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (4118927)CaDiCaL version: 2.1.3
% 0.72/0.47 % (4118927)Termination reason: Refutation not found, incomplete strategy
% 0.72/0.47 % (4118927)Time elapsed: 0.007 s
% 0.72/0.47 % (4118927)Peak memory usage: 12 MB
% 0.72/0.48 % (4118927)Instructions burned: 33 (million)
% 0.72/0.48 % (4118927)------------------------------
% 0.72/0.48 % (4118927)------------------------------
% 0.72/0.48 % (4118925)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=84605076:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.72/0.48 % (4118934)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1860811405:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.72/0.48 % (4118934)Instruction limit reached!
% 0.72/0.48 % (4118934)------------------------------
% 0.72/0.48 % (4118934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.48 % (4118934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.48 % (4118934)CaDiCaL version: 2.1.3
% 0.72/0.48 % (4118934)Termination reason: Instruction limit
% 0.72/0.48 % (4118934)Termination phase: shuffling
% 0.72/0.48 % (4118934)Time elapsed: 0.003 s
% 0.72/0.48 % (4118934)Peak memory usage: 10 MB
% 0.72/0.48 % (4118934)Instructions burned: 15 (million)
% 1.32/0.52 % (4118928)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2667723441:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.32/0.52 % (4118929)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=4163695139:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.32/0.52 % (4118937)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3946004244:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.32/0.52 % (4118931)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1537058752:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.32/0.52 % (4118937)Instruction limit reached!
% 1.32/0.52 % (4118937)------------------------------
% 1.32/0.52 % (4118937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.52 % (4118937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.52 % (4118937)CaDiCaL version: 2.1.3
% 1.32/0.52 % (4118937)Termination reason: Instruction limit
% 1.32/0.52 % (4118937)Termination phase: shuffling
% 1.32/0.52 % (4118937)Time elapsed: 0.003 s
% 1.32/0.52 % (4118937)Peak memory usage: 10 MB
% 1.32/0.52 % (4118937)Instructions burned: 14 (million)
% 1.32/0.52 % (4118920)Instruction limit reached!
% 1.32/0.52 % (4118920)------------------------------
% 1.32/0.52 % (4118920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.52 % (4118920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.52 % (4118920)CaDiCaL version: 2.1.3
% 1.32/0.52 % (4118920)Termination reason: Instruction limit
% 1.32/0.52 % (4118920)Termination phase: Saturation
% 1.32/0.52 % (4118920)Time elapsed: 0.036 s
% 1.32/0.52 % (4118920)Peak memory usage: 12 MB
% 1.32/0.52 % (4118920)Instructions burned: 86 (million)
% 1.32/0.52 % (4118929)Instruction limit reached!
% 1.32/0.52 % (4118929)------------------------------
% 1.32/0.52 % (4118929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.52 % (4118929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.52 % (4118929)CaDiCaL version: 2.1.3
% 1.32/0.52 % (4118929)Termination reason: Instruction limit
% 1.32/0.52 % (4118929)Termination phase: shuffling
% 1.32/0.52 % (4118929)Time elapsed: 0.011 s
% 1.32/0.52 % (4118929)Peak memory usage: 10 MB
% 1.32/0.52 % (4118929)Instructions burned: 14 (million)
% 1.32/0.52 % (4118928)Instruction limit reached!
% 1.32/0.52 % (4118928)------------------------------
% 1.32/0.52 % (4118928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.52 % (4118928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.52 % (4118928)CaDiCaL version: 2.1.3
% 1.32/0.52 % (4118928)Termination reason: Instruction limit
% 1.32/0.52 % (4118928)Termination phase: Property scanning
% 1.32/0.52 % (4118928)Time elapsed: 0.017 s
% 1.32/0.52 % (4118928)Peak memory usage: 10 MB
% 1.32/0.52 % (4118928)Instructions burned: 26 (million)
% 1.32/0.52 % (4118925)Refutation not found, incomplete strategy
% 1.32/0.52 % (4118925)------------------------------
% 1.32/0.52 % (4118925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.52 % (4118925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.52 % (4118925)CaDiCaL version: 2.1.3
% 1.32/0.52 % (4118925)Termination reason: Refutation not found, incomplete strategy
% 1.32/0.52 % (4118925)Time elapsed: 0.034 s
% 1.32/0.52 % (4118925)Peak memory usage: 12 MB
% 1.32/0.52 % (4118925)Instructions burned: 35 (million)
% 1.32/0.52 % (4118925)------------------------------
% 1.32/0.52 % (4118925)------------------------------
% 1.32/0.52 % (4118942)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2904959453:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.32/0.52 % (4118942)Instruction limit reached!
% 1.32/0.52 % (4118942)------------------------------
% 1.32/0.52 % (4118942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.52 % (4118942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.52 % (4118942)CaDiCaL version: 2.1.3
% 1.32/0.52 % (4118942)Termination reason: Instruction limit
% 1.32/0.52 % (4118942)Termination phase: Function definition elimination
% 1.32/0.52 % (4118942)Time elapsed: 0.006 s
% 1.32/0.52 % (4118942)Peak memory usage: 10 MB
% 1.32/0.57 % (4118942)Instructions burned: 31 (million)
% 1.32/0.57 % (4118947)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.32/0.57 % (4118931)Refutation not found, incomplete strategy
% 1.32/0.57 % (4118931)------------------------------
% 1.32/0.57 % (4118931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (4118931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (4118931)CaDiCaL version: 2.1.3
% 1.32/0.57 % (4118931)Termination reason: Refutation not found, incomplete strategy
% 1.32/0.57 % (4118931)Time elapsed: 0.030 s
% 1.32/0.57 % (4118948)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=826016014:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.32/0.57 % (4118947)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=2936013626:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.32/0.57 % (4118931)Peak memory usage: 12 MB
% 1.32/0.57 % (4118931)Instructions burned: 43 (million)
% 1.32/0.57 % (4118931)------------------------------
% 1.32/0.57 % (4118931)------------------------------
% 1.32/0.57 % (4118945)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
% 1.32/0.57 % (4118945)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.32/0.57 % (4118943)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3907391870:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.32/0.57 % (4118947)Instruction limit reached!
% 1.32/0.57 % (4118947)------------------------------
% 1.32/0.57 % (4118947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (4118947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (4118947)CaDiCaL version: 2.1.3
% 1.32/0.57 % (4118947)Termination reason: Instruction limit
% 1.32/0.57 % (4118947)Termination phase: shuffling
% 1.32/0.57 % (4118947)Time elapsed: 0.004 s
% 1.32/0.57 % (4118947)Peak memory usage: 10 MB
% 1.32/0.57 % (4118947)Instructions burned: 10 (million)
% 1.32/0.57 % (4118948)Instruction limit reached!
% 1.32/0.57 % (4118948)------------------------------
% 1.32/0.57 % (4118948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (4118948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (4118948)CaDiCaL version: 2.1.3
% 1.32/0.57 % (4118948)Termination reason: Instruction limit
% 1.32/0.57 % (4118948)Termination phase: Property scanning
% 1.32/0.57 % (4118948)Time elapsed: 0.007 s
% 1.32/0.57 % (4118948)Peak memory usage: 10 MB
% 1.32/0.57 % (4118948)Instructions burned: 33 (million)
% 1.32/0.57 % (4118945)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=3614403320:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.32/0.57 % (4118944)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2897244505:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.32/0.57 % (4118955)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2810693717:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.32/0.57 % (4118955)Instruction limit reached!
% 1.32/0.57 % (4118955)------------------------------
% 1.32/0.57 % (4118955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.57 % (4118955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.57 % (4118955)CaDiCaL version: 2.1.3
% 1.32/0.57 % (4118955)Termination reason: Instruction limit
% 1.32/0.57 % (4118955)Termination phase: Property scanning
% 1.32/0.57 % (4118955)Time elapsed: 0.004 s
% 1.32/0.57 % (4118955)Peak memory usage: 10 MB
% 1.32/0.57 % (4118955)Instructions burned: 22 (million)
% 1.32/0.57 % (4118943)Instruction limit reached!
% 1.32/0.57 % (4118943)------------------------------
% 1.32/0.57 % (4118943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.66 % (4118943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.66 % (4118943)CaDiCaL version: 2.1.3
% 2.06/0.66 % (4118943)Termination reason: Instruction limit
% 2.06/0.66 % (4118943)Termination phase: Property scanning
% 2.06/0.66 % (4118943)Time elapsed: 0.017 s
% 2.06/0.66 % (4118943)Peak memory usage: 10 MB
% 2.06/0.66 % (4118943)Instructions burned: 23 (million)
% 2.06/0.66 % (4118945)Instruction limit reached!
% 2.06/0.66 % (4118945)------------------------------
% 2.06/0.66 % (4118945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.66 % (4118945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.66 % (4118945)CaDiCaL version: 2.1.3
% 2.06/0.66 % (4118945)Termination reason: Instruction limit
% 2.06/0.66 % (4118945)Termination phase: Property scanning
% 2.06/0.66 % (4118945)Time elapsed: 0.010 s
% 2.06/0.66 % (4118945)Peak memory usage: 10 MB
% 2.06/0.66 % (4118945)Instructions burned: 14 (million)
% 2.06/0.66 % (4118954)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2511942834:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.06/0.66 % (4118954)Instruction limit reached!
% 2.06/0.66 % (4118954)------------------------------
% 2.06/0.66 % (4118954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.66 % (4118954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.66 % (4118954)CaDiCaL version: 2.1.3
% 2.06/0.66 % (4118954)Termination reason: Instruction limit
% 2.06/0.66 % (4118954)Termination phase: Property scanning
% 2.06/0.66 % (4118954)Time elapsed: 0.009 s
% 2.06/0.66 % (4118954)Peak memory usage: 10 MB
% 2.06/0.66 % (4118954)Instructions burned: 23 (million)
% 2.06/0.66 % (4118959)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=125771673:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.06/0.66 % (4118952)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1606424758:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.06/0.66 % (4118962)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=977236221:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.06/0.66 % (4118952)Instruction limit reached!
% 2.06/0.66 % (4118952)------------------------------
% 2.06/0.66 % (4118952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.66 % (4118952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.66 % (4118952)CaDiCaL version: 2.1.3
% 2.06/0.66 % (4118952)Termination reason: Instruction limit
% 2.06/0.66 % (4118952)Termination phase: shuffling
% 2.06/0.66 % (4118952)Time elapsed: 0.008 s
% 2.06/0.66 % (4118952)Peak memory usage: 10 MB
% 2.06/0.66 % (4118952)Instructions burned: 9 (million)
% 2.06/0.66 % (4118963)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4253385660:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.06/0.66 % (4118944)Instruction limit reached!
% 2.06/0.66 % (4118944)------------------------------
% 2.06/0.66 % (4118944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.66 % (4118944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.66 % (4118944)CaDiCaL version: 2.1.3
% 2.06/0.66 % (4118944)Termination reason: Instruction limit
% 2.06/0.66 % (4118944)Termination phase: Saturation
% 2.06/0.66 % (4118944)Time elapsed: 0.047 s
% 2.06/0.66 % (4118944)Peak memory usage: 12 MB
% 2.06/0.66 % (4118944)Instructions burned: 61 (million)
% 2.06/0.66 % (4118960)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1887650736:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.06/0.66 % (4118962)Refutation not found, incomplete strategy
% 2.06/0.66 % (4118962)------------------------------
% 2.06/0.66 % (4118962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.06/0.66 % (4118962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/0.66 % (4118962)CaDiCaL version: 2.1.3
% 2.06/0.66 % (4118962)Termination reason: Refutation not found, incomplete strategy
% 2.06/0.66 % (4118962)Time elapsed: 0.016 s
% 2.06/0.66 % (4118962)Peak memory usage: 12 MB
% 2.06/0.66 % (4118962)Instructions burned: 41 (million)
% 2.06/0.66 % (4118962)------------------------------
% 2.06/0.66 % (4118962)------------------------------
% 2.06/0.66 % (4118967)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.28/0.75 % (4118963)Instruction limit reached!
% 2.28/0.75 % (4118963)------------------------------
% 2.28/0.75 % (4118963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.75 % (4118963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.75 % (4118963)CaDiCaL version: 2.1.3
% 2.28/0.75 % (4118963)Termination reason: Instruction limit
% 2.28/0.75 % (4118963)Termination phase: Property scanning
% 2.28/0.75 % (4118963)Time elapsed: 0.019 s
% 2.28/0.75 % (4118963)Peak memory usage: 10 MB
% 2.28/0.75 % (4118963)Instructions burned: 51 (million)
% 2.28/0.75 % (4118967)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=509050479:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.28/0.75 % (4118967)Instruction limit reached!
% 2.28/0.75 % (4118967)------------------------------
% 2.28/0.75 % (4118967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.75 % (4118967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.75 % (4118967)CaDiCaL version: 2.1.3
% 2.28/0.75 % (4118967)Termination reason: Instruction limit
% 2.28/0.75 % (4118967)Termination phase: shuffling
% 2.28/0.75 % (4118967)Time elapsed: 0.003 s
% 2.28/0.75 % (4118967)Peak memory usage: 10 MB
% 2.28/0.75 % (4118967)Instructions burned: 7 (million)
% 2.28/0.75 % (4118971)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=1086705717:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.28/0.75 % (4118972)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.28/0.75 % (4118972)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1374768072:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.28/0.75 % (4118972)Instruction limit reached!
% 2.28/0.75 % (4118972)------------------------------
% 2.28/0.75 % (4118972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.75 % (4118972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.75 % (4118972)CaDiCaL version: 2.1.3
% 2.28/0.75 % (4118972)Termination reason: Instruction limit
% 2.28/0.75 % (4118972)Termination phase: shuffling
% 2.28/0.75 % (4118972)Time elapsed: 0.003 s
% 2.28/0.75 % (4118972)Peak memory usage: 10 MB
% 2.28/0.75 % (4118972)Instructions burned: 7 (million)
% 2.28/0.75 % (4118970)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=87681484:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.28/0.75 % (4118974)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=608607469:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.28/0.75 % (4118974)Instruction limit reached!
% 2.28/0.75 % (4118974)------------------------------
% 2.28/0.75 % (4118974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.75 % (4118974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.75 % (4118974)CaDiCaL version: 2.1.3
% 2.28/0.75 % (4118974)Termination reason: Instruction limit
% 2.28/0.75 % (4118974)Termination phase: Property scanning
% 2.28/0.75 % (4118974)Time elapsed: 0.008 s
% 2.28/0.75 % (4118974)Peak memory usage: 10 MB
% 2.28/0.75 % (4118974)Instructions burned: 22 (million)
% 2.28/0.75 % (4118971)Refutation not found, incomplete strategy
% 2.28/0.75 % (4118971)------------------------------
% 2.28/0.75 % (4118971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/0.75 % (4118971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/0.75 % (4118971)CaDiCaL version: 2.1.3
% 2.28/0.75 % (4118971)Termination reason: Refutation not found, incomplete strategy
% 2.28/0.75 % (4118971)Time elapsed: 0.018 s
% 2.28/0.75 % (4118971)Peak memory usage: 12 MB
% 2.28/0.75 % (4118971)Instructions burned: 36 (million)
% 2.28/0.75 % (4118971)------------------------------
% 2.28/0.75 % (4118971)------------------------------
% 2.28/0.75 % (4118978)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2961325662:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.86/0.83 % (4118978)Instruction limit reached!
% 2.86/0.83 % (4118978)------------------------------
% 2.86/0.83 % (4118978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.83 % (4118978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.83 % (4118978)CaDiCaL version: 2.1.3
% 2.86/0.83 % (4118978)Termination reason: Instruction limit
% 2.86/0.83 % (4118978)Termination phase: Property scanning
% 2.86/0.83 % (4118978)Time elapsed: 0.008 s
% 2.86/0.83 % (4118978)Peak memory usage: 10 MB
% 2.86/0.83 % (4118978)Instructions burned: 19 (million)
% 2.86/0.83 % (4118970)Refutation not found, incomplete strategy
% 2.86/0.83 % (4118970)------------------------------
% 2.86/0.83 % (4118970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.83 % (4118970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.83 % (4118970)CaDiCaL version: 2.1.3
% 2.86/0.83 % (4118970)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.83 % (4118970)Time elapsed: 0.027 s
% 2.86/0.83 % (4118970)Peak memory usage: 12 MB
% 2.86/0.83 % (4118970)Instructions burned: 34 (million)
% 2.86/0.83 % (4118970)------------------------------
% 2.86/0.83 % (4118970)------------------------------
% 2.86/0.83 % (4118980)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=1950723648:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.86/0.83 % (4118981)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=472814585:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.86/0.83 % (4118983)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=1738524734:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 2.86/0.83 % (4118984)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3785078579:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.86/0.83 % (4118960)Instruction limit reached!
% 2.86/0.83 % (4118960)------------------------------
% 2.86/0.83 % (4118960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.83 % (4118960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.83 % (4118960)CaDiCaL version: 2.1.3
% 2.86/0.83 % (4118960)Termination reason: Instruction limit
% 2.86/0.83 % (4118960)Termination phase: Saturation
% 2.86/0.83 % (4118960)Time elapsed: 0.111 s
% 2.86/0.83 % (4118960)Peak memory usage: 13 MB
% 2.86/0.83 % (4118960)Instructions burned: 144 (million)
% 2.86/0.83 % (4118901)Instruction limit reached!
% 2.86/0.83 % (4118901)------------------------------
% 2.86/0.83 % (4118901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.83 % (4118901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.83 % (4118901)CaDiCaL version: 2.1.3
% 2.86/0.83 % (4118901)Termination reason: Instruction limit
% 2.86/0.83 % (4118901)Termination phase: Saturation
% 2.86/0.83 % (4118901)Time elapsed: 0.330 s
% 2.86/0.83 % (4118901)Peak memory usage: 15 MB
% 2.86/0.83 % (4118901)Instructions burned: 635 (million)
% 2.86/0.83 % (4118989)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=773850245:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.86/0.83 % (4118983)Instruction limit reached!
% 2.86/0.83 % (4118983)------------------------------
% 2.86/0.83 % (4118983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.83 % (4118983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.83 % (4118983)CaDiCaL version: 2.1.3
% 2.86/0.83 % (4118983)Termination reason: Instruction limit
% 2.86/0.83 % (4118983)Termination phase: Property scanning
% 2.86/0.83 % (4118983)Time elapsed: 0.036 s
% 2.86/0.83 % (4118983)Peak memory usage: 11 MB
% 2.86/0.83 % (4118983)Instructions burned: 47 (million)
% 2.86/0.83 % (4118990)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.86/0.83 % (4118989)Instruction limit reached!
% 2.86/0.88 % (4118989)------------------------------
% 2.86/0.88 % (4118989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.88 % (4118989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.88 % (4118989)CaDiCaL version: 2.1.3
% 2.86/0.88 % (4118989)Termination reason: Instruction limit
% 2.86/0.88 % (4118989)Termination phase: Property scanning
% 2.86/0.88 % (4118989)Time elapsed: 0.011 s
% 2.86/0.88 % (4118989)Peak memory usage: 10 MB
% 2.86/0.88 % (4118989)Instructions burned: 22 (million)
% 2.86/0.88 % (4118984)Refutation not found, incomplete strategy
% 2.86/0.88 % (4118984)------------------------------
% 2.86/0.88 % (4118984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.88 % (4118984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.88 % (4118984)CaDiCaL version: 2.1.3
% 2.86/0.88 % (4118984)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.88 % (4118984)Time elapsed: 0.042 s
% 2.86/0.88 % (4118984)Peak memory usage: 13 MB
% 2.86/0.88 % (4118984)Instructions burned: 60 (million)
% 2.86/0.88 % (4118984)------------------------------
% 2.86/0.88 % (4118984)------------------------------
% 2.86/0.88 % (4118990)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3957622205:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 2.86/0.88 % (4118993)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=2434370917:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 2.86/0.88 % (4118992)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1669532488:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 2.86/0.88 % (4118994)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=686578190:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 2.86/0.88 % (4118992)Instruction limit reached!
% 2.86/0.88 % (4118992)------------------------------
% 2.86/0.88 % (4118992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.88 % (4118992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.88 % (4118992)CaDiCaL version: 2.1.3
% 2.86/0.88 % (4118992)Termination reason: Instruction limit
% 2.86/0.88 % (4118992)Termination phase: shuffling
% 2.86/0.88 % (4118992)Time elapsed: 0.009 s
% 2.86/0.88 % (4118992)Peak memory usage: 9 MB
% 2.86/0.88 % (4118992)Instructions burned: 13 (million)
% 2.86/0.88 % (4118993)Instruction limit reached!
% 2.86/0.88 % (4118993)------------------------------
% 2.86/0.88 % (4118993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.88 % (4118993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.88 % (4118993)CaDiCaL version: 2.1.3
% 2.86/0.88 % (4118993)Termination reason: Instruction limit
% 2.86/0.88 % (4118993)Termination phase: Property scanning
% 2.86/0.88 % (4118993)Time elapsed: 0.027 s
% 2.86/0.88 % (4118993)Peak memory usage: 11 MB
% 2.86/0.88 % (4118993)Instructions burned: 66 (million)
% 2.86/0.88 % (4118994)Instruction limit reached!
% 2.86/0.88 % (4118994)------------------------------
% 2.86/0.88 % (4118994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.88 % (4118994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.88 % (4118994)CaDiCaL version: 2.1.3
% 2.86/0.88 % (4118994)Termination reason: Instruction limit
% 2.86/0.88 % (4118994)Termination phase: Property scanning
% 2.86/0.88 % (4118994)Time elapsed: 0.025 s
% 2.86/0.88 % (4118994)Peak memory usage: 11 MB
% 2.86/0.88 % (4118994)Instructions burned: 53 (million)
% 2.86/0.88 % (4119000)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2295806009:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 2.86/0.88 % (4119001)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=2513051303:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 2.86/0.88 % (4118999)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2548766443:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 2.86/0.88 % (4119001)Instruction limit reached!
% 2.86/0.88 % (4119001)------------------------------
% 3.42/0.94 % (4119001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.94 % (4119001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.94 % (4119001)CaDiCaL version: 2.1.3
% 3.42/0.94 % (4119001)Termination reason: Instruction limit
% 3.42/0.94 % (4119001)Termination phase: Function definition elimination
% 3.42/0.94 % (4119001)Time elapsed: 0.014 s
% 3.42/0.94 % (4119001)Peak memory usage: 10 MB
% 3.42/0.94 % (4119001)Instructions burned: 35 (million)
% 3.42/0.94 % (4118999)Instruction limit reached!
% 3.42/0.94 % (4118999)------------------------------
% 3.42/0.94 % (4118999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.94 % (4118999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.94 % (4118999)CaDiCaL version: 2.1.3
% 3.42/0.94 % (4118999)Termination reason: Instruction limit
% 3.42/0.94 % (4118999)Termination phase: Function definition elimination
% 3.42/0.94 % (4118999)Time elapsed: 0.026 s
% 3.42/0.94 % (4118999)Peak memory usage: 10 MB
% 3.42/0.94 % (4118999)Instructions burned: 31 (million)
% 3.42/0.94 % (4119005)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2569883846:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.42/0.94 % (4118990)Instruction limit reached!
% 3.42/0.94 % (4118990)------------------------------
% 3.42/0.94 % (4118990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.94 % (4118990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.94 % (4118990)CaDiCaL version: 2.1.3
% 3.42/0.94 % (4118990)Termination reason: Instruction limit
% 3.42/0.94 % (4118990)Termination phase: Saturation
% 3.42/0.94 % (4118990)Time elapsed: 0.114 s
% 3.42/0.94 % (4118990)Peak memory usage: 13 MB
% 3.42/0.94 % (4118990)Instructions burned: 201 (million)
% 3.42/0.94 % (4119006)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.42/0.94 % (4119008)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2214756844:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 3.42/0.94 % (4119006)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1027761201:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.42/0.94 % (4119005)Instruction limit reached!
% 3.42/0.94 % (4119005)------------------------------
% 3.42/0.94 % (4119005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.94 % (4119005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.94 % (4119005)CaDiCaL version: 2.1.3
% 3.42/0.94 % (4119005)Termination reason: Instruction limit
% 3.42/0.94 % (4119005)Termination phase: Property scanning
% 3.42/0.94 % (4119005)Time elapsed: 0.026 s
% 3.42/0.94 % (4119005)Peak memory usage: 11 MB
% 3.42/0.94 % (4119005)Instructions burned: 69 (million)
% 3.42/0.94 % (4118959)Instruction limit reached!
% 3.42/0.94 % (4118959)------------------------------
% 3.42/0.94 % (4118959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.94 % (4118959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.94 % (4118959)CaDiCaL version: 2.1.3
% 3.42/0.94 % (4118959)Termination reason: Instruction limit
% 3.42/0.94 % (4118959)Termination phase: Saturation
% 3.42/0.94 % (4118959)Time elapsed: 0.325 s
% 3.42/0.94 % (4118959)Peak memory usage: 18 MB
% 3.42/0.94 % (4118959)Instructions burned: 1241 (million)
% 3.42/0.94 % (4119008)Refutation not found, incomplete strategy
% 3.42/0.94 % (4119008)------------------------------
% 3.42/0.94 % (4119008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.94 % (4119008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.94 % (4119008)CaDiCaL version: 2.1.3
% 3.42/0.94 % (4119008)Termination reason: Refutation not found, incomplete strategy
% 3.42/0.94 % (4119008)Time elapsed: 0.016 s
% 3.42/0.94 % (4119008)Peak memory usage: 12 MB
% 3.42/0.94 % (4119008)Instructions burned: 38 (million)
% 3.42/0.94 % (4119008)------------------------------
% 3.42/0.94 % (4119008)------------------------------
% 3.42/0.94 % (4119011)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2879840683:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 3.42/0.94 % (4119012)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3133667761:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 3.42/0.99 % (4119012)Refutation not found, incomplete strategy
% 3.42/0.99 % (4119012)------------------------------
% 3.42/0.99 % (4119012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.99 % (4119012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.99 % (4119012)CaDiCaL version: 2.1.3
% 3.42/0.99 % (4119012)Termination reason: Refutation not found, incomplete strategy
% 3.42/0.99 % (4119012)Time elapsed: 0.007 s
% 3.42/0.99 % (4119012)Peak memory usage: 12 MB
% 3.42/0.99 % (4119012)Instructions burned: 32 (million)
% 3.42/0.99 % (4119012)------------------------------
% 3.42/0.99 % (4119012)------------------------------
% 3.42/0.99 % (4119013)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1227489698:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 3.42/0.99 % (4119000)Instruction limit reached!
% 3.42/0.99 % (4119000)------------------------------
% 3.42/0.99 % (4119000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.99 % (4119000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.99 % (4119000)CaDiCaL version: 2.1.3
% 3.42/0.99 % (4119000)Termination reason: Instruction limit
% 3.42/0.99 % (4119000)Termination phase: Saturation
% 3.42/0.99 % (4119000)Time elapsed: 0.119 s
% 3.42/0.99 % (4119000)Peak memory usage: 13 MB
% 3.42/0.99 % (4119000)Instructions burned: 138 (million)
% 3.42/0.99 % (4119016)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1277571501:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 3.42/0.99 % (4119013)Refutation not found, incomplete strategy
% 3.42/0.99 % (4119013)------------------------------
% 3.42/0.99 % (4119013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.99 % (4119013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.99 % (4119013)CaDiCaL version: 2.1.3
% 3.42/0.99 % (4119013)Termination reason: Refutation not found, incomplete strategy
% 3.42/0.99 % (4119013)Time elapsed: 0.018 s
% 3.42/0.99 % (4119013)Peak memory usage: 12 MB
% 3.42/0.99 % (4119013)Instructions burned: 43 (million)
% 3.42/0.99 % (4119013)------------------------------
% 3.42/0.99 % (4119013)------------------------------
% 3.42/0.99 % (4119011)Instruction limit reached!
% 3.42/0.99 % (4119011)------------------------------
% 3.42/0.99 % (4119011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.99 % (4119011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.99 % (4119011)CaDiCaL version: 2.1.3
% 3.42/0.99 % (4119011)Termination reason: Instruction limit
% 3.42/0.99 % (4119011)Termination phase: Saturation
% 3.42/0.99 % (4119011)Time elapsed: 0.038 s
% 3.42/0.99 % (4119011)Peak memory usage: 12 MB
% 3.42/0.99 % (4119011)Instructions burned: 97 (million)
% 3.42/0.99 % (4119016)Refutation not found, incomplete strategy
% 3.42/0.99 % (4119016)------------------------------
% 3.42/0.99 % (4119016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.99 % (4119016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.99 % (4119016)CaDiCaL version: 2.1.3
% 3.42/0.99 % (4119016)Termination reason: Refutation not found, incomplete strategy
% 3.42/0.99 % (4119016)Time elapsed: 0.015 s
% 3.42/0.99 % (4119016)Peak memory usage: 13 MB
% 3.42/0.99 % (4119016)Instructions burned: 67 (million)
% 3.42/0.99 % (4119016)------------------------------
% 3.42/0.99 % (4119016)------------------------------
% 3.42/0.99 % (4119019)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3016639906:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 3.42/0.99 % (4119022)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=4294462459:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 3.42/0.99 % (4119020)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3892188891:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 3.42/0.99 % (4118980)Instruction limit reached!
% 3.42/0.99 % (4118980)------------------------------
% 3.42/0.99 % (4118980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.99 % (4118980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.99 % (4118980)CaDiCaL version: 2.1.3
% 3.42/0.99 % (4118980)Termination reason: Instruction limit
% 3.42/0.99 % (4118980)Termination phase: Saturation
% 4.41/1.06 % (4118980)Time elapsed: 0.283 s
% 4.41/1.06 % (4118980)Peak memory usage: 15 MB
% 4.41/1.06 % (4118980)Instructions burned: 316 (million)
% 4.41/1.06 % (4119021)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2448707332:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 4.41/1.06 % (4119019)Refutation not found, incomplete strategy
% 4.41/1.06 % (4119019)------------------------------
% 4.41/1.06 % (4119019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.41/1.06 % (4119019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.06 % (4119019)CaDiCaL version: 2.1.3
% 4.41/1.06 % (4119019)Termination reason: Refutation not found, incomplete strategy
% 4.41/1.06 % (4119019)Time elapsed: 0.013 s
% 4.41/1.06 % (4119019)Peak memory usage: 12 MB
% 4.41/1.06 % (4119019)Instructions burned: 29 (million)
% 4.41/1.06 % (4119019)------------------------------
% 4.41/1.06 % (4119019)------------------------------
% 4.41/1.06 % (4119020)Instruction limit reached!
% 4.41/1.06 % (4119020)------------------------------
% 4.41/1.06 % (4119020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.41/1.06 % (4119020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.06 % (4119020)CaDiCaL version: 2.1.3
% 4.41/1.06 % (4119020)Termination reason: Instruction limit
% 4.41/1.06 % (4119020)Termination phase: Property scanning
% 4.41/1.06 % (4119020)Time elapsed: 0.018 s
% 4.41/1.06 % (4119020)Peak memory usage: 10 MB
% 4.41/1.06 % (4119020)Instructions burned: 46 (million)
% 4.41/1.06 % (4119021)Refutation not found, incomplete strategy
% 4.41/1.06 % (4119021)------------------------------
% 4.41/1.06 % (4119021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.41/1.06 % (4119021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.06 % (4119021)CaDiCaL version: 2.1.3
% 4.41/1.06 % (4119021)Termination reason: Refutation not found, incomplete strategy
% 4.41/1.06 % (4119021)Time elapsed: 0.027 s
% 4.41/1.06 % (4119021)Peak memory usage: 13 MB
% 4.41/1.06 % (4119021)Instructions burned: 64 (million)
% 4.41/1.06 % (4119021)------------------------------
% 4.41/1.06 % (4119021)------------------------------
% 4.41/1.06 % (4119029)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=1031304348: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_2993 on theBenchmark for (2993ds/105Mi)
% 4.41/1.06 % (4119026)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3629006261:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 4.41/1.06 % (4119028)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=3137651022:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 4.41/1.06 % (4119006)Instruction limit reached!
% 4.41/1.06 % (4119006)------------------------------
% 4.41/1.06 % (4119006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.41/1.06 % (4119006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.06 % (4119006)CaDiCaL version: 2.1.3
% 4.41/1.06 % (4119006)Termination reason: Instruction limit
% 4.41/1.06 % (4119006)Termination phase: Saturation
% 4.41/1.06 % (4119006)Time elapsed: 0.124 s
% 4.41/1.06 % (4119006)Peak memory usage: 12 MB
% 4.41/1.06 % (4119006)Instructions burned: 182 (million)
% 4.41/1.06 % (4119030)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=4170167510:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 4.41/1.06 % (4119030)Refutation not found, incomplete strategy
% 4.41/1.06 % (4119030)------------------------------
% 4.41/1.06 % (4119030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.41/1.06 % (4119030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.06 % (4119030)CaDiCaL version: 2.1.3
% 4.41/1.06 % (4119030)Termination reason: Refutation not found, incomplete strategy
% 4.41/1.06 % (4119030)Time elapsed: 0.017 s
% 4.41/1.06 % (4119030)Peak memory usage: 13 MB
% 4.41/1.06 % (4119030)Instructions burned: 40 (million)
% 4.41/1.06 % (4119034)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=704405699:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/375Mi)
% 4.83/1.19 % (4119030)------------------------------
% 4.83/1.19 % (4119030)------------------------------
% 4.83/1.19 % (4119029)Instruction limit reached!
% 4.83/1.19 % (4119029)------------------------------
% 4.83/1.19 % (4119029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.83/1.19 % (4119029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.19 % (4119029)CaDiCaL version: 2.1.3
% 4.83/1.19 % (4119029)Termination reason: Instruction limit
% 4.83/1.19 % (4119029)Termination phase: Saturation
% 4.83/1.19 % (4119029)Time elapsed: 0.042 s
% 4.83/1.19 % (4119029)Peak memory usage: 12 MB
% 4.83/1.19 % (4119029)Instructions burned: 105 (million)
% 4.83/1.19 % (4119034)Refutation not found, incomplete strategy
% 4.83/1.19 % (4119034)------------------------------
% 4.83/1.19 % (4119034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.83/1.19 % (4119034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.19 % (4119034)CaDiCaL version: 2.1.3
% 4.83/1.19 % (4119034)Termination reason: Refutation not found, incomplete strategy
% 4.83/1.19 % (4119034)Time elapsed: 0.017 s
% 4.83/1.19 % (4119034)Peak memory usage: 12 MB
% 4.83/1.19 % (4119034)Instructions burned: 40 (million)
% 4.83/1.19 % (4119034)------------------------------
% 4.83/1.19 % (4119034)------------------------------
% 4.83/1.19 % (4119037)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1304034885:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/495Mi)
% 4.83/1.19 % (4119038)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=849441285:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 4.83/1.19 % (4119022)Instruction limit reached!
% 4.83/1.19 % (4119022)------------------------------
% 4.83/1.19 % (4119022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.83/1.19 % (4119022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.19 % (4119022)CaDiCaL version: 2.1.3
% 4.83/1.19 % (4119022)Termination reason: Instruction limit
% 4.83/1.19 % (4119022)Termination phase: Saturation
% 4.83/1.19 % (4119022)Time elapsed: 0.102 s
% 4.83/1.19 % (4119022)Peak memory usage: 15 MB
% 4.83/1.19 % (4119022)Instructions burned: 453 (million)
% 4.83/1.19 % (4119028)Instruction limit reached!
% 4.83/1.19 % (4119028)------------------------------
% 4.83/1.19 % (4119028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.83/1.19 % (4119028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.19 % (4119028)CaDiCaL version: 2.1.3
% 4.83/1.19 % (4119028)Termination reason: Instruction limit
% 4.83/1.19 % (4119028)Termination phase: Property scanning
% 4.83/1.19 % (4119028)Time elapsed: 0.051 s
% 4.83/1.19 % (4119028)Peak memory usage: 11 MB
% 4.83/1.19 % (4119028)Instructions burned: 65 (million)
% 4.83/1.19 % (4119039)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3617407581:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/91Mi)
% 4.83/1.19 % (4119042)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=266450903:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2993 on theBenchmark for (2993ds/66Mi)
% 4.83/1.19 % (4119038)Instruction limit reached!
% 4.83/1.19 % (4119038)------------------------------
% 4.83/1.19 % (4119038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.83/1.19 % (4119038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.19 % (4119038)CaDiCaL version: 2.1.3
% 4.83/1.19 % (4119038)Termination reason: Instruction limit
% 4.83/1.19 % (4119038)Termination phase: shuffling
% 4.83/1.19 % (4119038)Time elapsed: 0.014 s
% 4.83/1.19 % (4119038)Peak memory usage: 10 MB
% 4.83/1.19 % (4119038)Instructions burned: 37 (million)
% 4.83/1.19 % (4119026)Instruction limit reached!
% 4.83/1.19 % (4119026)------------------------------
% 4.83/1.19 % (4119026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.83/1.19 % (4119026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.19 % (4119026)CaDiCaL version: 2.1.3
% 4.83/1.19 % (4119026)Termination reason: Instruction limit
% 4.83/1.19 % (4119026)Termination phase: Saturation
% 5.08/1.26 % (4119026)Time elapsed: 0.073 s
% 5.08/1.26 % (4119026)Peak memory usage: 12 MB
% 5.08/1.26 % (4119026)Instructions burned: 96 (million)
% 5.08/1.26 % (4119042)Refutation not found, incomplete strategy
% 5.08/1.26 % (4119042)------------------------------
% 5.08/1.26 % (4119042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.08/1.26 % (4119042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.26 % (4119042)CaDiCaL version: 2.1.3
% 5.08/1.26 % (4119042)Termination reason: Refutation not found, incomplete strategy
% 5.08/1.26 % (4119042)Time elapsed: 0.008 s
% 5.08/1.26 % (4119042)Peak memory usage: 12 MB
% 5.08/1.26 % (4119042)Instructions burned: 37 (million)
% 5.08/1.26 % (4119042)------------------------------
% 5.08/1.26 % (4119042)------------------------------
% 5.08/1.26 % (4119043)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3776605053:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2993 on theBenchmark for (2993ds/22Mi)
% 5.08/1.26 % (4119046)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=819997098:i=338:bd=all:ins=4:rtra=on_2992 on theBenchmark for (2992ds/338Mi)
% 5.08/1.26 % (4119048)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 5.08/1.26 % (4119043)Instruction limit reached!
% 5.08/1.26 % (4119043)------------------------------
% 5.08/1.26 % (4119043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.08/1.26 % (4119043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.26 % (4119043)CaDiCaL version: 2.1.3
% 5.08/1.26 % (4119043)Termination reason: Instruction limit
% 5.08/1.26 % (4119043)Termination phase: Property scanning
% 5.08/1.26 % (4119043)Time elapsed: 0.009 s
% 5.08/1.26 % (4119043)Peak memory usage: 10 MB
% 5.08/1.26 % (4119043)Instructions burned: 25 (million)
% 5.08/1.26 % (4119048)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3030905399:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2992 on theBenchmark for (2992ds/137Mi)
% 5.08/1.26 % (4119047)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3323138922:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/28Mi)
% 5.08/1.26 % (4119047)Instruction limit reached!
% 5.08/1.26 % (4119047)------------------------------
% 5.08/1.26 % (4119047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.08/1.26 % (4119047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.26 % (4119047)CaDiCaL version: 2.1.3
% 5.08/1.26 % (4119047)Termination reason: Instruction limit
% 5.08/1.26 % (4119047)Termination phase: Saturation
% 5.08/1.26 % (4119047)Time elapsed: 0.007 s
% 5.08/1.26 % (4119047)Peak memory usage: 11 MB
% 5.08/1.26 % (4119047)Instructions burned: 31 (million)
% 5.08/1.26 % (4119039)Instruction limit reached!
% 5.08/1.26 % (4119039)------------------------------
% 5.08/1.26 % (4119039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.08/1.26 % (4119039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.26 % (4119039)CaDiCaL version: 2.1.3
% 5.08/1.26 % (4119039)Termination reason: Instruction limit
% 5.08/1.26 % (4119039)Termination phase: Saturation
% 5.08/1.26 % (4119039)Time elapsed: 0.056 s
% 5.08/1.26 % (4119039)Peak memory usage: 12 MB
% 5.08/1.26 % (4119039)Instructions burned: 92 (million)
% 5.08/1.26 % (4119051)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=1580556526:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2992 on theBenchmark for (2992ds/340Mi)
% 5.08/1.26 % (4119055)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 5.08/1.26 % (4119055)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1290289783:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/373Mi)
% 5.08/1.26 % (4119048)Instruction limit reached!
% 5.08/1.26 % (4119048)------------------------------
% 5.08/1.26 % (4119048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.08/1.26 % (4119048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.26 % (4119048)CaDiCaL version: 2.1.3
% 5.43/1.33 % (4119048)Termination reason: Instruction limit
% 5.43/1.33 % (4119048)Termination phase: Saturation
% 5.43/1.33 % (4119048)Time elapsed: 0.047 s
% 5.43/1.33 % (4119048)Peak memory usage: 12 MB
% 5.43/1.33 % (4119048)Instructions burned: 139 (million)
% 5.43/1.33 % (4119054)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3743434511:i=227:sd=1:bd=all:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/227Mi)
% 5.43/1.33 % (4119054)Refutation not found, incomplete strategy
% 5.43/1.33 % (4119054)------------------------------
% 5.43/1.33 % (4119054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.33 % (4119054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.33 % (4119054)CaDiCaL version: 2.1.3
% 5.43/1.33 % (4119054)Termination reason: Refutation not found, incomplete strategy
% 5.43/1.33 % (4119054)Time elapsed: 0.013 s
% 5.43/1.33 % (4119054)Peak memory usage: 12 MB
% 5.43/1.33 % (4119054)Instructions burned: 32 (million)
% 5.43/1.33 % (4119054)------------------------------
% 5.43/1.33 % (4119054)------------------------------
% 5.43/1.33 % (4119058)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=4240330336:i=116:ep=RSTC:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/116Mi)
% 5.43/1.33 % (4119060)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=4271289546:i=575:rtra=on_2991 on theBenchmark for (2991ds/575Mi)
% 5.43/1.33 % (4119058)Instruction limit reached!
% 5.43/1.33 % (4119058)------------------------------
% 5.43/1.33 % (4119058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.33 % (4119058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.33 % (4119058)CaDiCaL version: 2.1.3
% 5.43/1.33 % (4119058)Termination reason: Instruction limit
% 5.43/1.33 % (4119058)Termination phase: Saturation
% 5.43/1.33 % (4119058)Time elapsed: 0.050 s
% 5.43/1.33 % (4119058)Peak memory usage: 12 MB
% 5.43/1.33 % (4119058)Instructions burned: 119 (million)
% 5.43/1.33 % (4119063)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=437603678:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2991 on theBenchmark for (2991ds/270Mi)
% 5.43/1.33 % (4119046)Instruction limit reached!
% 5.43/1.33 % (4119046)------------------------------
% 5.43/1.33 % (4119046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.33 % (4119046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.33 % (4119046)CaDiCaL version: 2.1.3
% 5.43/1.33 % (4119046)Termination reason: Instruction limit
% 5.43/1.33 % (4119046)Termination phase: Saturation
% 5.43/1.33 % (4119046)Time elapsed: 0.160 s
% 5.43/1.33 % (4119046)Peak memory usage: 16 MB
% 5.43/1.33 % (4119046)Instructions burned: 339 (million)
% 5.43/1.33 % (4119060)Refutation not found, incomplete strategy
% 5.43/1.33 % (4119060)------------------------------
% 5.43/1.33 % (4119060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.33 % (4119060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.33 % (4119060)CaDiCaL version: 2.1.3
% 5.43/1.33 % (4119060)Termination reason: Refutation not found, incomplete strategy
% 5.43/1.33 % (4119060)Time elapsed: 0.076 s
% 5.43/1.33 % (4119060)Peak memory usage: 14 MB
% 5.43/1.33 % (4119060)Instructions burned: 186 (million)
% 5.43/1.33 % (4119060)------------------------------
% 5.43/1.33 % (4119060)------------------------------
% 5.43/1.33 % (4119037)Instruction limit reached!
% 5.43/1.33 % (4119037)------------------------------
% 5.43/1.33 % (4119037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.33 % (4119037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.33 % (4119037)CaDiCaL version: 2.1.3
% 5.43/1.33 % (4119037)Termination reason: Instruction limit
% 5.43/1.33 % (4119037)Termination phase: Saturation
% 5.43/1.33 % (4119037)Time elapsed: 0.220 s
% 5.43/1.33 % (4119037)Peak memory usage: 16 MB
% 5.43/1.33 % (4119037)Instructions burned: 495 (million)
% 5.43/1.33 % (4119065)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=3849525602: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_2991 on theBenchmark for (2991ds/9840Mi)
% 5.43/1.33 % (4119066)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1046462957:i=421:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/421Mi)
% 5.98/1.45 % (4119067)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
% 5.98/1.45 % (4119067)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=1670925910:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/270Mi)
% 5.98/1.45 % (4119066)Refutation not found, incomplete strategy
% 5.98/1.45 % (4119066)------------------------------
% 5.98/1.45 % (4119066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.45 % (4119066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.45 % (4119066)CaDiCaL version: 2.1.3
% 5.98/1.45 % (4119066)Termination reason: Refutation not found, incomplete strategy
% 5.98/1.45 % (4119066)Time elapsed: 0.029 s
% 5.98/1.45 % (4119066)Peak memory usage: 12 MB
% 5.98/1.45 % (4119066)Instructions burned: 34 (million)
% 5.98/1.45 % (4119066)------------------------------
% 5.98/1.45 % (4119066)------------------------------
% 5.98/1.45 % (4118981)Instruction limit reached!
% 5.98/1.45 % (4118981)------------------------------
% 5.98/1.45 % (4118981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.45 % (4118981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.45 % (4118981)CaDiCaL version: 2.1.3
% 5.98/1.45 % (4118981)Termination reason: Instruction limit
% 5.98/1.45 % (4118981)Termination phase: Saturation
% 5.98/1.45 % (4118981)Time elapsed: 0.629 s
% 5.98/1.45 % (4118981)Peak memory usage: 18 MB
% 5.98/1.45 % (4118981)Instructions burned: 855 (million)
% 5.98/1.45 % (4119063)Instruction limit reached!
% 5.98/1.45 % (4119063)------------------------------
% 5.98/1.45 % (4119063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.45 % (4119063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.45 % (4119063)CaDiCaL version: 2.1.3
% 5.98/1.45 % (4119063)Termination reason: Instruction limit
% 5.98/1.45 % (4119063)Termination phase: Saturation
% 5.98/1.45 % (4119063)Time elapsed: 0.085 s
% 5.98/1.45 % (4119063)Peak memory usage: 13 MB
% 5.98/1.45 % (4119063)Instructions burned: 271 (million)
% 5.98/1.45 % (4119055)Instruction limit reached!
% 5.98/1.45 % (4119055)------------------------------
% 5.98/1.45 % (4119055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.45 % (4119055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.45 % (4119055)CaDiCaL version: 2.1.3
% 5.98/1.45 % (4119055)Termination reason: Instruction limit
% 5.98/1.45 % (4119055)Termination phase: Saturation
% 5.98/1.45 % (4119055)Time elapsed: 0.184 s
% 5.98/1.45 % (4119055)Peak memory usage: 13 MB
% 5.98/1.45 % (4119055)Instructions burned: 373 (million)
% 5.98/1.45 % (4119072)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 5.98/1.45 % (4119072)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
% 5.98/1.45 % (4119073)dis+10_2_sil=128000:si=on:random_seed=1735710495:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2990 on theBenchmark for (2990ds/339Mi)
% 5.98/1.45 % (4119072)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=515549407:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2990 on theBenchmark for (2990ds/1440Mi)
% 5.98/1.45 % (4119071)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3185686135:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/31Mi)
% 5.98/1.45 % (4119073)Refutation not found, incomplete strategy
% 5.98/1.45 % (4119073)------------------------------
% 5.98/1.45 % (4119073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/1.45 % (4119073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.45 % (4119073)CaDiCaL version: 2.1.3
% 5.98/1.45 % (4119073)Termination reason: Refutation not found, incomplete strategy
% 5.98/1.45 % (4119073)Time elapsed: 0.015 s
% 5.98/1.45 % (4119073)Peak memory usage: 12 MB
% 6.22/1.58 % (4119073)Instructions burned: 66 (million)
% 6.22/1.58 % (4119074)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2466213723:i=111:add=on:fgj=on:rtra=on:fdi=1024_2990 on theBenchmark for (2990ds/111Mi)
% 6.22/1.58 % (4119073)------------------------------
% 6.22/1.58 % (4119073)------------------------------
% 6.22/1.58 % (4119079)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=1242929961:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/122Mi)
% 6.22/1.58 % (4119079)Refutation not found, incomplete strategy
% 6.22/1.58 % (4119079)------------------------------
% 6.22/1.58 % (4119079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.22/1.58 % (4119079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.58 % (4119079)CaDiCaL version: 2.1.3
% 6.22/1.58 % (4119079)Termination reason: Refutation not found, incomplete strategy
% 6.22/1.58 % (4119079)Time elapsed: 0.008 s
% 6.22/1.58 % (4119079)Peak memory usage: 12 MB
% 6.22/1.58 % (4119079)Instructions burned: 36 (million)
% 6.22/1.58 % (4119079)------------------------------
% 6.22/1.58 % (4119079)------------------------------
% 6.22/1.58 % (4119071)Instruction limit reached!
% 6.22/1.58 % (4119071)------------------------------
% 6.22/1.58 % (4119071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.22/1.58 % (4119071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.58 % (4119071)CaDiCaL version: 2.1.3
% 6.22/1.58 % (4119071)Termination reason: Instruction limit
% 6.22/1.58 % (4119071)Termination phase: Function definition elimination
% 6.22/1.58 % (4119071)Time elapsed: 0.028 s
% 6.22/1.58 % (4119071)Peak memory usage: 10 MB
% 6.22/1.58 % (4119071)Instructions burned: 32 (million)
% 6.22/1.58 % (4119081)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=3886323747:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/136Mi)
% 6.22/1.58 % (4119074)Instruction limit reached!
% 6.22/1.58 % (4119074)------------------------------
% 6.22/1.58 % (4119074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.22/1.58 % (4119074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.58 % (4119074)CaDiCaL version: 2.1.3
% 6.22/1.58 % (4119074)Termination reason: Instruction limit
% 6.22/1.58 % (4119074)Termination phase: Saturation
% 6.22/1.58 % (4119074)Time elapsed: 0.044 s
% 6.22/1.58 % (4119074)Peak memory usage: 12 MB
% 6.22/1.58 % (4119074)Instructions burned: 112 (million)
% 6.22/1.58 % (4119082)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1978805155:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2989 on theBenchmark for (2989ds/232Mi)
% 6.22/1.58 % (4119051)Instruction limit reached!
% 6.22/1.58 % (4119051)------------------------------
% 6.22/1.58 % (4119051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.22/1.58 % (4119051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.58 % (4119051)CaDiCaL version: 2.1.3
% 6.22/1.58 % (4119051)Termination reason: Instruction limit
% 6.22/1.58 % (4119051)Termination phase: Saturation
% 6.22/1.58 % (4119051)Time elapsed: 0.274 s
% 6.22/1.58 % (4119051)Peak memory usage: 15 MB
% 6.22/1.58 % (4119051)Instructions burned: 340 (million)
% 6.22/1.58 % (4119067)Refutation not found, incomplete strategy
% 6.22/1.58 % (4119067)------------------------------
% 6.22/1.58 % (4119067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.22/1.58 % (4119067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.58 % (4119067)CaDiCaL version: 2.1.3
% 6.22/1.58 % (4119067)Termination reason: Refutation not found, incomplete strategy
% 6.22/1.58 % (4119067)Time elapsed: 0.119 s
% 6.22/1.58 % (4119067)Peak memory usage: 14 MB
% 6.22/1.58 % (4119067)Instructions burned: 203 (million)
% 6.22/1.58 % (4119067)------------------------------
% 6.22/1.58 % (4119067)------------------------------
% 6.22/1.58 % (4119082)Refutation not found, incomplete strategy
% 6.22/1.58 % (4119082)------------------------------
% 6.22/1.58 % (4119082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.22/1.58 % (4119082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/1.58 % (4119082)CaDiCaL version: 2.1.3
% 6.52/1.70 % (4119082)Termination reason: Refutation not found, incomplete strategy
% 6.52/1.70 % (4119082)Time elapsed: 0.019 s
% 6.52/1.70 % (4119082)Peak memory usage: 12 MB
% 6.52/1.70 % (4119082)Instructions burned: 38 (million)
% 6.52/1.70 % (4119082)------------------------------
% 6.52/1.70 % (4119082)------------------------------
% 6.52/1.70 % (4119086)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 6.52/1.70 % (4119085)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=488302999:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/1254Mi)
% 6.52/1.70 % (4119081)Instruction limit reached!
% 6.52/1.70 % (4119081)------------------------------
% 6.52/1.70 % (4119081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.70 % (4119081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.70 % (4119081)CaDiCaL version: 2.1.3
% 6.52/1.70 % (4119081)Termination reason: Instruction limit
% 6.52/1.70 % (4119081)Termination phase: Saturation
% 6.52/1.70 % (4119081)Time elapsed: 0.045 s
% 6.52/1.70 % (4119081)Peak memory usage: 12 MB
% 6.52/1.70 % (4119081)Instructions burned: 140 (million)
% 6.52/1.70 % (4119086)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=3082914723:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2989 on theBenchmark for (2989ds/281Mi)
% 6.52/1.70 % (4119087)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1764027363:i=619:add=on:rtra=on_2989 on theBenchmark for (2989ds/619Mi)
% 6.52/1.70 % (4119090)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2009721965:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/212Mi)
% 6.52/1.70 % (4119090)Refutation not found, incomplete strategy
% 6.52/1.70 % (4119090)------------------------------
% 6.52/1.70 % (4119090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.70 % (4119090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.70 % (4119090)CaDiCaL version: 2.1.3
% 6.52/1.70 % (4119090)Termination reason: Refutation not found, incomplete strategy
% 6.52/1.70 % (4119090)Time elapsed: 0.007 s
% 6.52/1.70 % (4119090)Peak memory usage: 12 MB
% 6.52/1.70 % (4119090)Instructions burned: 32 (million)
% 6.52/1.70 % (4119090)------------------------------
% 6.52/1.70 % (4119090)------------------------------
% 6.52/1.70 % (4119088)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=1611301623:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/865Mi)
% 6.52/1.70 % (4119094)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=1246784267:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/130Mi)
% 6.52/1.70 % (4119094)Refutation not found, incomplete strategy
% 6.52/1.70 % (4119094)------------------------------
% 6.52/1.70 % (4119094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.70 % (4119094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.70 % (4119094)CaDiCaL version: 2.1.3
% 6.52/1.70 % (4119094)Termination reason: Refutation not found, incomplete strategy
% 6.52/1.70 % (4119094)Time elapsed: 0.014 s
% 6.52/1.70 % (4119094)Peak memory usage: 12 MB
% 6.52/1.70 % (4119094)Instructions burned: 34 (million)
% 6.52/1.70 % (4119094)------------------------------
% 6.52/1.70 % (4119094)------------------------------
% 6.52/1.70 % (4119097)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2713202087:st=1.5:i=346:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/346Mi)
% 6.52/1.70 % (4119097)Refutation not found, incomplete strategy
% 6.52/1.70 % (4119097)------------------------------
% 6.52/1.70 % (4119097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.70 % (4119097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.70 % (4119097)CaDiCaL version: 2.1.3
% 6.52/1.70 % (4119097)Termination reason: Refutation not found, incomplete strategy
% 6.52/1.70 % (4119097)Time elapsed: 0.011 s
% 6.52/1.70 % (4119097)Peak memory usage: 12 MB
% 6.52/1.70 % (4119097)Instructions burned: 28 (million)
% 6.52/1.70 % (4119097)------------------------------
% 6.52/1.70 % (4119097)------------------------------
% 6.52/1.70 % (4119087)Refutation not found, incomplete strategy
% 7.31/1.83 % (4119087)------------------------------
% 7.31/1.83 % (4119087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.31/1.83 % (4119087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/1.83 % (4119087)CaDiCaL version: 2.1.3
% 7.31/1.83 % (4119087)Termination reason: Refutation not found, incomplete strategy
% 7.31/1.83 % (4119087)Time elapsed: 0.092 s
% 7.31/1.83 % (4119087)Peak memory usage: 14 MB
% 7.31/1.83 % (4119087)Instructions burned: 176 (million)
% 7.31/1.83 % (4119087)------------------------------
% 7.31/1.83 % (4119087)------------------------------
% 7.31/1.83 % (4119099)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=1299814108:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/152Mi)
% 7.31/1.83 % (4119100)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=195818700:i=75:ep=R:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/75Mi)
% 7.31/1.83 % (4119085)Refutation not found, incomplete strategy
% 7.31/1.83 % (4119085)------------------------------
% 7.31/1.83 % (4119085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.31/1.83 % (4119085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/1.83 % (4119085)CaDiCaL version: 2.1.3
% 7.31/1.83 % (4119085)Termination reason: Refutation not found, incomplete strategy
% 7.31/1.83 % (4119085)Time elapsed: 0.151 s
% 7.31/1.83 % (4119085)Peak memory usage: 14 MB
% 7.31/1.83 % (4119085)Instructions burned: 181 (million)
% 7.31/1.83 % (4119085)------------------------------
% 7.31/1.83 % (4119085)------------------------------
% 7.31/1.83 % (4119100)Instruction limit reached!
% 7.31/1.83 % (4119100)------------------------------
% 7.31/1.83 % (4119100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.31/1.83 % (4119100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/1.83 % (4119100)CaDiCaL version: 2.1.3
% 7.31/1.83 % (4119100)Termination reason: Instruction limit
% 7.31/1.83 % (4119100)Termination phase: Saturation
% 7.31/1.83 % (4119100)Time elapsed: 0.029 s
% 7.31/1.83 % (4119100)Peak memory usage: 11 MB
% 7.31/1.83 % (4119100)Instructions burned: 79 (million)
% 7.31/1.83 % (4119099)Instruction limit reached!
% 7.31/1.83 % (4119099)------------------------------
% 7.31/1.83 % (4119099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.31/1.83 % (4119099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/1.83 % (4119099)CaDiCaL version: 2.1.3
% 7.31/1.83 % (4119099)Termination reason: Instruction limit
% 7.31/1.83 % (4119099)Termination phase: Saturation
% 7.31/1.83 % (4119099)Time elapsed: 0.062 s
% 7.31/1.83 % (4119099)Peak memory usage: 13 MB
% 7.31/1.83 % (4119099)Instructions burned: 152 (million)
% 7.31/1.83 % (4119103)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=694393578:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/387Mi)
% 7.31/1.83 % (4119104)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=1723879051:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2987 on theBenchmark for (2987ds/148Mi)
% 7.31/1.83 % (4119105)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=17234576:i=161:piset=and:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/161Mi)
% 7.31/1.83 % (4119103)Refutation not found, incomplete strategy
% 7.31/1.83 % (4119103)------------------------------
% 7.31/1.83 % (4119103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.31/1.83 % (4119103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/1.83 % (4119103)CaDiCaL version: 2.1.3
% 7.31/1.83 % (4119103)Termination reason: Refutation not found, incomplete strategy
% 7.31/1.83 % (4119103)Time elapsed: 0.027 s
% 7.31/1.83 % (4119103)Peak memory usage: 12 MB
% 7.31/1.83 % (4119103)Instructions burned: 30 (million)
% 7.31/1.83 % (4119103)------------------------------
% 7.31/1.83 % (4119103)------------------------------
% 7.31/1.83 % (4119086)Instruction limit reached!
% 7.31/1.83 % (4119086)------------------------------
% 7.31/1.83 % (4119086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.31/1.83 % (4119086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/1.83 % (4119086)CaDiCaL version: 2.1.3
% 7.31/1.83 % (4119086)Termination reason: Instruction limit
% 11.63/2.21 % (4119086)Termination phase: Saturation
% 11.63/2.21 % (4119086)Time elapsed: 0.229 s
% 11.63/2.21 % (4119086)Peak memory usage: 13 MB
% 11.63/2.21 % (4119086)Instructions burned: 282 (million)
% 11.63/2.21 % (4119105)Instruction limit reached!
% 11.63/2.21 % (4119105)------------------------------
% 11.63/2.21 % (4119105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.21 % (4119105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.21 % (4119105)CaDiCaL version: 2.1.3
% 11.63/2.21 % (4119105)Termination reason: Instruction limit
% 11.63/2.21 % (4119105)Termination phase: Saturation
% 11.63/2.21 % (4119105)Time elapsed: 0.065 s
% 11.63/2.21 % (4119105)Peak memory usage: 13 MB
% 11.63/2.21 % (4119105)Instructions burned: 161 (million)
% 11.63/2.21 % (4119109)lrs+10_1_sil=128000:si=on:random_seed=3828888169:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/888Mi)
% 11.63/2.21 % (4119110)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=4081234500:i=136:add=on:ins=4:rtra=on:sup=off_2986 on theBenchmark for (2986ds/136Mi)
% 11.63/2.21 % (4119111)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=3020984709:i=88:s2at=3:nm=2:rtra=on:rawr=on_2986 on theBenchmark for (2986ds/88Mi)
% 11.63/2.21 % (4119104)Instruction limit reached!
% 11.63/2.21 % (4119104)------------------------------
% 11.63/2.21 % (4119104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.21 % (4119104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.21 % (4119104)CaDiCaL version: 2.1.3
% 11.63/2.21 % (4119104)Termination reason: Instruction limit
% 11.63/2.21 % (4119104)Termination phase: Saturation
% 11.63/2.21 % (4119104)Time elapsed: 0.095 s
% 11.63/2.21 % (4119104)Peak memory usage: 13 MB
% 11.63/2.21 % (4119104)Instructions burned: 148 (million)
% 11.63/2.21 % (4119115)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=560162909:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2986 on theBenchmark for (2986ds/93Mi)
% 11.63/2.21 % (4119088)Instruction limit reached!
% 11.63/2.21 % (4119088)------------------------------
% 11.63/2.21 % (4119088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.21 % (4119088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.21 % (4119088)CaDiCaL version: 2.1.3
% 11.63/2.21 % (4119088)Termination reason: Instruction limit
% 11.63/2.21 % (4119088)Termination phase: Saturation
% 11.63/2.21 % (4119088)Time elapsed: 0.295 s
% 11.63/2.21 % (4119088)Peak memory usage: 20 MB
% 11.63/2.21 % (4119088)Instructions burned: 866 (million)
% 11.63/2.21 % (4119111)Instruction limit reached!
% 11.63/2.21 % (4119111)------------------------------
% 11.63/2.21 % (4119111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.21 % (4119111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.21 % (4119111)CaDiCaL version: 2.1.3
% 11.63/2.21 % (4119111)Termination reason: Instruction limit
% 11.63/2.21 % (4119111)Termination phase: Saturation
% 11.63/2.21 % (4119111)Time elapsed: 0.036 s
% 11.63/2.21 % (4119111)Peak memory usage: 12 MB
% 11.63/2.21 % (4119111)Instructions burned: 90 (million)
% 11.63/2.21 % (4119109)Refutation not found, incomplete strategy
% 11.63/2.21 % (4119109)------------------------------
% 11.63/2.21 % (4119109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.21 % (4119109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.21 % (4119109)CaDiCaL version: 2.1.3
% 11.63/2.21 % (4119109)Termination reason: Refutation not found, incomplete strategy
% 11.63/2.21 % (4119109)Time elapsed: 0.062 s
% 11.63/2.21 % (4119109)Peak memory usage: 13 MB
% 11.63/2.21 % (4119109)Instructions burned: 72 (million)
% 11.63/2.21 % (4119117)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1768074226:i=2186:rtra=on:ixr=off_2986 on theBenchmark for (2986ds/2186Mi)
% 11.63/2.21 % (4119109)------------------------------
% 11.63/2.21 % (4119109)------------------------------
% 11.63/2.21 % (4119120)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2347804116:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2985 on theBenchmark for (2985ds/805Mi)
% 11.63/2.21 % (4119118)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3558484132:s2a=on:i=240:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/240Mi)
% 11.63/2.26 % (4119110)Instruction limit reached!
% 11.63/2.26 % (4119110)------------------------------
% 11.63/2.26 % (4119110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.26 % (4119110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.26 % (4119110)CaDiCaL version: 2.1.3
% 11.63/2.26 % (4119110)Termination reason: Instruction limit
% 11.63/2.26 % (4119110)Termination phase: Saturation
% 11.63/2.26 % (4119110)Time elapsed: 0.083 s
% 11.63/2.26 % (4119110)Peak memory usage: 13 MB
% 11.63/2.26 % (4119110)Instructions burned: 137 (million)
% 11.63/2.26 % (4119123)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 11.63/2.26 % (4119123)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=3126259812:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2985 on theBenchmark for (2985ds/391Mi)
% 11.63/2.26 % (4119115)Instruction limit reached!
% 11.63/2.26 % (4119115)------------------------------
% 11.63/2.26 % (4119115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.26 % (4119115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.26 % (4119115)CaDiCaL version: 2.1.3
% 11.63/2.26 % (4119115)Termination reason: Instruction limit
% 11.63/2.26 % (4119115)Termination phase: Saturation
% 11.63/2.26 % (4119115)Time elapsed: 0.069 s
% 11.63/2.26 % (4119115)Peak memory usage: 12 MB
% 11.63/2.26 % (4119115)Instructions burned: 94 (million)
% 11.63/2.26 % (4119123)Refutation not found, incomplete strategy
% 11.63/2.26 % (4119123)------------------------------
% 11.63/2.26 % (4119123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.26 % (4119123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.26 % (4119123)CaDiCaL version: 2.1.3
% 11.63/2.26 % (4119123)Termination reason: Refutation not found, incomplete strategy
% 11.63/2.26 % (4119123)Time elapsed: 0.015 s
% 11.63/2.26 % (4119123)Peak memory usage: 12 MB
% 11.63/2.26 % (4119123)Instructions burned: 34 (million)
% 11.63/2.26 % (4119123)------------------------------
% 11.63/2.26 % (4119123)------------------------------
% 11.63/2.26 % (4119126)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=3278806317:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/314Mi)
% 11.63/2.26 % (4119125)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=4142469666:i=355:av=off:fsr=off:rtra=on:ixr=off_2985 on theBenchmark for (2985ds/355Mi)
% 11.63/2.26 % (4119126)Refutation not found, incomplete strategy
% 11.63/2.26 % (4119126)------------------------------
% 11.63/2.26 % (4119126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.26 % (4119126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.26 % (4119126)CaDiCaL version: 2.1.3
% 11.63/2.26 % (4119126)Termination reason: Refutation not found, incomplete strategy
% 11.63/2.26 % (4119126)Time elapsed: 0.015 s
% 11.63/2.26 % (4119126)Peak memory usage: 12 MB
% 11.63/2.26 % (4119126)Instructions burned: 35 (million)
% 11.63/2.26 % (4119126)------------------------------
% 11.63/2.26 % (4119126)------------------------------
% 11.63/2.26 % (4119129)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=449325806:s2a=on:i=251:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/251Mi)
% 11.63/2.26 % (4119118)Instruction limit reached!
% 11.63/2.26 % (4119118)------------------------------
% 11.63/2.26 % (4119118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.63/2.26 % (4119118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.63/2.26 % (4119118)CaDiCaL version: 2.1.3
% 11.63/2.26 % (4119118)Termination reason: Instruction limit
% 11.63/2.26 % (4119118)Termination phase: Saturation
% 11.63/2.26 % (4119118)Time elapsed: 0.116 s
% 11.63/2.26 % (4119118)Peak memory usage: 14 MB
% 11.63/2.26 % (4119118)Instructions burned: 240 (million)
% 11.63/2.26 % (4119131)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=3971450750: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_2984 on theBenchmark for (2984ds/2470Mi)
% 12.18/2.37 % (4119129)Instruction limit reached!
% 12.18/2.37 % (4119129)------------------------------
% 12.18/2.37 % (4119129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.18/2.37 % (4119129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.37 % (4119129)CaDiCaL version: 2.1.3
% 12.18/2.37 % (4119129)Termination reason: Instruction limit
% 12.18/2.37 % (4119129)Termination phase: Saturation
% 12.18/2.37 % (4119129)Time elapsed: 0.100 s
% 12.18/2.37 % (4119129)Peak memory usage: 12 MB
% 12.18/2.37 % (4119129)Instructions burned: 252 (million)
% 12.18/2.37 % (4119133)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=1133493572:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2983 on theBenchmark for (2983ds/673Mi)
% 12.18/2.37 % (4119125)Instruction limit reached!
% 12.18/2.37 % (4119125)------------------------------
% 12.18/2.37 % (4119125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.18/2.37 % (4119125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.37 % (4119125)CaDiCaL version: 2.1.3
% 12.18/2.37 % (4119125)Termination reason: Instruction limit
% 12.18/2.37 % (4119125)Termination phase: Saturation
% 12.18/2.37 % (4119125)Time elapsed: 0.193 s
% 12.18/2.37 % (4119125)Peak memory usage: 14 MB
% 12.18/2.37 % (4119125)Instructions burned: 365 (million)
% 12.18/2.37 % (4119135)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2772766049:i=116:ep=RSTC:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/116Mi)
% 12.18/2.37 % (4119135)Instruction limit reached!
% 12.18/2.37 % (4119135)------------------------------
% 12.18/2.37 % (4119135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.18/2.37 % (4119135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.37 % (4119135)CaDiCaL version: 2.1.3
% 12.18/2.37 % (4119135)Termination reason: Instruction limit
% 12.18/2.37 % (4119135)Termination phase: Saturation
% 12.18/2.37 % (4119135)Time elapsed: 0.047 s
% 12.18/2.37 % (4119135)Peak memory usage: 12 MB
% 12.18/2.37 % (4119135)Instructions burned: 118 (million)
% 12.18/2.37 % (4119137)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2737309318:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2982 on theBenchmark for (2982ds/270Mi)
% 12.18/2.37 % (4119137)Instruction limit reached!
% 12.18/2.37 % (4119137)------------------------------
% 12.18/2.37 % (4119137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.18/2.37 % (4119137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.37 % (4119137)CaDiCaL version: 2.1.3
% 12.18/2.37 % (4119137)Termination reason: Instruction limit
% 12.18/2.37 % (4119137)Termination phase: Saturation
% 12.18/2.37 % (4119137)Time elapsed: 0.136 s
% 12.18/2.37 % (4119137)Peak memory usage: 13 MB
% 12.18/2.37 % (4119137)Instructions burned: 272 (million)
% 12.18/2.37 % (4119117)Instruction limit reached!
% 12.18/2.37 % (4119117)------------------------------
% 12.18/2.37 % (4119117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.18/2.37 % (4119117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.37 % (4119117)CaDiCaL version: 2.1.3
% 12.18/2.37 % (4119117)Termination reason: Instruction limit
% 12.18/2.37 % (4119117)Termination phase: Saturation
% 12.18/2.37 % (4119117)Time elapsed: 0.526 s
% 12.18/2.37 % (4119117)Peak memory usage: 19 MB
% 12.18/2.37 % (4119117)Instructions burned: 2192 (million)
% 12.18/2.37 % (4119072)Instruction limit reached!
% 12.18/2.37 % (4119072)------------------------------
% 12.18/2.37 % (4119072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.18/2.37 % (4119072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.37 % (4119072)CaDiCaL version: 2.1.3
% 12.18/2.37 % (4119072)Termination reason: Instruction limit
% 12.18/2.37 % (4119072)Termination phase: Saturation
% 12.18/2.37 % (4119072)Time elapsed: 0.948 s
% 12.18/2.37 % (4119072)Peak memory usage: 19 MB
% 12.18/2.37 % (4119072)Instructions burned: 1440 (million)
% 12.18/2.37 % (4119139)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=2408723295: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_2980 on theBenchmark for (2980ds/30Mi)
% 12.18/2.37 % (4119133)Instruction limit reached!
% 13.40/2.53 % (4119133)------------------------------
% 13.40/2.53 % (4119133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.40/2.53 % (4119133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/2.53 % (4119133)CaDiCaL version: 2.1.3
% 13.40/2.53 % (4119133)Termination reason: Instruction limit
% 13.40/2.53 % (4119133)Termination phase: Saturation
% 13.40/2.53 % (4119133)Time elapsed: 0.289 s
% 13.40/2.53 % (4119133)Peak memory usage: 15 MB
% 13.40/2.53 % (4119133)Instructions burned: 674 (million)
% 13.40/2.53 % (4119140)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 13.40/2.53 % (4119140)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=1779603564:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2980 on theBenchmark for (2980ds/39Mi)
% 13.40/2.53 % (4119139)Instruction limit reached!
% 13.40/2.53 % (4119139)------------------------------
% 13.40/2.53 % (4119139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.40/2.53 % (4119139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/2.53 % (4119139)CaDiCaL version: 2.1.3
% 13.40/2.53 % (4119139)Termination reason: Instruction limit
% 13.40/2.53 % (4119139)Termination phase: Property scanning
% 13.40/2.53 % (4119139)Time elapsed: 0.012 s
% 13.40/2.53 % (4119139)Peak memory usage: 10 MB
% 13.40/2.53 % (4119139)Instructions burned: 30 (million)
% 13.40/2.53 % (4119140)Instruction limit reached!
% 13.40/2.53 % (4119140)------------------------------
% 13.40/2.53 % (4119140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.40/2.53 % (4119140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/2.53 % (4119140)CaDiCaL version: 2.1.3
% 13.40/2.53 % (4119140)Termination reason: Instruction limit
% 13.40/2.53 % (4119140)Termination phase: Property scanning
% 13.40/2.53 % (4119140)Time elapsed: 0.009 s
% 13.40/2.53 % (4119140)Peak memory usage: 10 MB
% 13.40/2.53 % (4119140)Instructions burned: 43 (million)
% 13.40/2.53 % (4119142)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1468594137:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2980 on theBenchmark for (2980ds/365Mi)
% 13.40/2.53 % (4119143)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=824425047:i=158:av=off:rtra=on_2980 on theBenchmark for (2980ds/158Mi)
% 13.40/2.53 % (4119145)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
% 13.40/2.53 % (4119146)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=37621270:i=213:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/213Mi)
% 13.40/2.53 % (4119145)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=1401796502:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/252Mi)
% 13.40/2.53 % (4119146)Refutation not found, incomplete strategy
% 13.40/2.53 % (4119146)------------------------------
% 13.40/2.53 % (4119146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.40/2.53 % (4119146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/2.53 % (4119146)CaDiCaL version: 2.1.3
% 13.40/2.53 % (4119146)Termination reason: Refutation not found, incomplete strategy
% 13.40/2.53 % (4119146)Time elapsed: 0.007 s
% 13.40/2.53 % (4119146)Peak memory usage: 12 MB
% 13.40/2.53 % (4119146)Instructions burned: 34 (million)
% 13.40/2.53 % (4119146)------------------------------
% 13.40/2.53 % (4119146)------------------------------
% 13.40/2.53 % (4119151)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=4144291421:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2980 on theBenchmark for (2980ds/160Mi)
% 13.40/2.53 % (4119151)Refutation not found, incomplete strategy
% 13.40/2.53 % (4119151)------------------------------
% 13.40/2.53 % (4119151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.40/2.53 % (4119151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/2.53 % (4119151)CaDiCaL version: 2.1.3
% 13.40/2.53 % (4119151)Termination reason: Refutation not found, incomplete strategy
% 13.40/2.53 % (4119151)Time elapsed: 0.011 s
% 13.40/2.53 % (4119151)Peak memory usage: 12 MB
% 13.40/2.53 % (4119151)Instructions burned: 51 (million)
% 13.87/2.62 % (4119151)------------------------------
% 13.87/2.62 % (4119151)------------------------------
% 13.87/2.62 % (4119153)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=4222751641:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/763Mi)
% 13.87/2.62 % (4119143)Instruction limit reached!
% 13.87/2.62 % (4119143)------------------------------
% 13.87/2.62 % (4119143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.62 % (4119143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.62 % (4119143)CaDiCaL version: 2.1.3
% 13.87/2.62 % (4119143)Termination reason: Instruction limit
% 13.87/2.62 % (4119143)Termination phase: Saturation
% 13.87/2.62 % (4119143)Time elapsed: 0.074 s
% 13.87/2.62 % (4119143)Peak memory usage: 13 MB
% 13.87/2.62 % (4119143)Instructions burned: 158 (million)
% 13.87/2.62 % (4119155)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 13.87/2.62 % (4119145)Refutation not found, incomplete strategy
% 13.87/2.62 % (4119145)------------------------------
% 13.87/2.62 % (4119145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.62 % (4119145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.62 % (4119145)CaDiCaL version: 2.1.3
% 13.87/2.62 % (4119145)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.62 % (4119145)Time elapsed: 0.084 s
% 13.87/2.62 % (4119145)Peak memory usage: 14 MB
% 13.87/2.62 % (4119145)Instructions burned: 202 (million)
% 13.87/2.62 % (4119145)------------------------------
% 13.87/2.62 % (4119145)------------------------------
% 13.87/2.62 % (4119155)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=3863462032:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2979 on theBenchmark for (2979ds/237Mi)
% 13.87/2.62 % (4119153)Refutation not found, incomplete strategy
% 13.87/2.62 % (4119153)------------------------------
% 13.87/2.62 % (4119153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.62 % (4119153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.62 % (4119153)CaDiCaL version: 2.1.3
% 13.87/2.62 % (4119153)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.62 % (4119153)Time elapsed: 0.046 s
% 13.87/2.62 % (4119153)Peak memory usage: 14 MB
% 13.87/2.62 % (4119153)Instructions burned: 208 (million)
% 13.87/2.62 % (4119153)------------------------------
% 13.87/2.62 % (4119153)------------------------------
% 13.87/2.62 % (4119158)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=1165509032:i=300:piset=and:nm=32:rtra=on_2979 on theBenchmark for (2979ds/300Mi)
% 13.87/2.62 % (4119155)Refutation not found, incomplete strategy
% 13.87/2.62 % (4119155)------------------------------
% 13.87/2.62 % (4119155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.62 % (4119155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.62 % (4119155)CaDiCaL version: 2.1.3
% 13.87/2.62 % (4119155)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.62 % (4119155)Time elapsed: 0.016 s
% 13.87/2.62 % (4119155)Peak memory usage: 12 MB
% 13.87/2.62 % (4119155)Instructions burned: 37 (million)
% 13.87/2.62 % (4119155)------------------------------
% 13.87/2.62 % (4119155)------------------------------
% 13.87/2.62 % (4119157)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=78425184:s2a=on:i=386:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/386Mi)
% 13.87/2.62 % (4119120)Instruction limit reached!
% 13.87/2.62 % (4119120)------------------------------
% 13.87/2.62 % (4119120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.62 % (4119120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.62 % (4119120)CaDiCaL version: 2.1.3
% 13.87/2.62 % (4119120)Termination reason: Instruction limit
% 13.87/2.62 % (4119120)Termination phase: Saturation
% 13.87/2.62 % (4119120)Time elapsed: 0.640 s
% 13.87/2.62 % (4119120)Peak memory usage: 16 MB
% 13.87/2.62 % (4119120)Instructions burned: 805 (million)
% 13.87/2.62 % (4119160)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=921806288:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/567Mi)
% 13.87/2.62 % (4119162)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=3377791681:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2979 on theBenchmark for (2979ds/379Mi)
% 14.64/2.73 % (4119142)Instruction limit reached!
% 14.64/2.73 % (4119142)------------------------------
% 14.64/2.73 % (4119142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.64/2.73 % (4119142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/2.73 % (4119142)CaDiCaL version: 2.1.3
% 14.64/2.73 % (4119142)Termination reason: Instruction limit
% 14.64/2.73 % (4119142)Termination phase: Saturation
% 14.64/2.73 % (4119142)Time elapsed: 0.159 s
% 14.64/2.73 % (4119142)Peak memory usage: 15 MB
% 14.64/2.73 % (4119142)Instructions burned: 365 (million)
% 14.64/2.73 % (4119165)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=3416294951:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2978 on theBenchmark for (2978ds/429Mi)
% 14.64/2.73 % (4119158)Instruction limit reached!
% 14.64/2.73 % (4119158)------------------------------
% 14.64/2.73 % (4119158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.64/2.73 % (4119158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/2.73 % (4119158)CaDiCaL version: 2.1.3
% 14.64/2.73 % (4119158)Termination reason: Instruction limit
% 14.64/2.73 % (4119158)Termination phase: Saturation
% 14.64/2.73 % (4119158)Time elapsed: 0.067 s
% 14.64/2.73 % (4119158)Peak memory usage: 14 MB
% 14.64/2.73 % (4119158)Instructions burned: 301 (million)
% 14.64/2.73 % (4119167)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=871775560:i=478:bd=all:rtra=on_2978 on theBenchmark for (2978ds/478Mi)
% 14.64/2.73 % (4119160)Refutation not found, incomplete strategy
% 14.64/2.73 % (4119160)------------------------------
% 14.64/2.73 % (4119160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.64/2.73 % (4119160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/2.73 % (4119160)CaDiCaL version: 2.1.3
% 14.64/2.73 % (4119160)Termination reason: Refutation not found, incomplete strategy
% 14.64/2.73 % (4119160)Time elapsed: 0.050 s
% 14.64/2.73 % (4119160)Peak memory usage: 12 MB
% 14.64/2.73 % (4119160)Instructions burned: 52 (million)
% 14.64/2.73 % (4119160)------------------------------
% 14.64/2.73 % (4119160)------------------------------
% 14.64/2.73 % (4119169)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2621064327:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2978 on theBenchmark for (2978ds/445Mi)
% 14.64/2.73 % (4119167)Refutation not found, incomplete strategy
% 14.64/2.73 % (4119167)------------------------------
% 14.64/2.73 % (4119167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.64/2.73 % (4119167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/2.73 % (4119167)CaDiCaL version: 2.1.3
% 14.64/2.73 % (4119167)Termination reason: Refutation not found, incomplete strategy
% 14.64/2.73 % (4119167)Time elapsed: 0.072 s
% 14.64/2.73 % (4119167)Peak memory usage: 14 MB
% 14.64/2.73 % (4119167)Instructions burned: 189 (million)
% 14.64/2.73 % (4119167)------------------------------
% 14.64/2.73 % (4119167)------------------------------
% 14.64/2.73 % (4119157)Instruction limit reached!
% 14.64/2.73 % (4119157)------------------------------
% 14.64/2.73 % (4119157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.64/2.73 % (4119157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/2.73 % (4119157)CaDiCaL version: 2.1.3
% 14.64/2.73 % (4119157)Termination reason: Instruction limit
% 14.64/2.73 % (4119157)Termination phase: Saturation
% 14.64/2.73 % (4119157)Time elapsed: 0.156 s
% 14.64/2.73 % (4119157)Peak memory usage: 13 MB
% 14.64/2.73 % (4119157)Instructions burned: 388 (million)
% 14.64/2.73 % (4119173)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3449457044:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/302Mi)
% 14.64/2.73 % (4119172)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=3295807110:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2977 on theBenchmark for (2977ds/71Mi)
% 14.64/2.73 % (4119173)Refutation not found, incomplete strategy
% 14.64/2.73 % (4119173)------------------------------
% 14.64/2.73 % (4119173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.64/2.73 % (4119173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/2.85 % (4119173)CaDiCaL version: 2.1.3
% 15.11/2.85 % (4119173)Termination reason: Refutation not found, incomplete strategy
% 15.11/2.85 % (4119173)Time elapsed: 0.015 s
% 15.11/2.85 % (4119173)Peak memory usage: 12 MB
% 15.11/2.85 % (4119173)Instructions burned: 34 (million)
% 15.11/2.85 % (4119173)------------------------------
% 15.11/2.85 % (4119173)------------------------------
% 15.11/2.85 % (4119176)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=2746785219:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2977 on theBenchmark for (2977ds/4980Mi)
% 15.11/2.85 % (4119176)Refutation not found, incomplete strategy
% 15.11/2.85 % (4119176)------------------------------
% 15.11/2.85 % (4119176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.11/2.85 % (4119176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/2.85 % (4119176)CaDiCaL version: 2.1.3
% 15.11/2.85 % (4119176)Termination reason: Refutation not found, incomplete strategy
% 15.11/2.85 % (4119176)Time elapsed: 0.015 s
% 15.11/2.85 % (4119176)Peak memory usage: 12 MB
% 15.11/2.85 % (4119176)Instructions burned: 36 (million)
% 15.11/2.85 % (4119176)------------------------------
% 15.11/2.85 % (4119176)------------------------------
% 15.11/2.85 % (4119169)Instruction limit reached!
% 15.11/2.85 % (4119169)------------------------------
% 15.11/2.85 % (4119169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.11/2.85 % (4119169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/2.85 % (4119169)CaDiCaL version: 2.1.3
% 15.11/2.85 % (4119169)Termination reason: Instruction limit
% 15.11/2.85 % (4119169)Termination phase: Saturation
% 15.11/2.85 % (4119169)Time elapsed: 0.124 s
% 15.11/2.85 % (4119169)Peak memory usage: 15 MB
% 15.11/2.85 % (4119169)Instructions burned: 446 (million)
% 15.11/2.85 % (4119179)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=599746335:i=76:piset=equals:rtra=on:ntd=on_2977 on theBenchmark for (2977ds/76Mi)
% 15.11/2.85 % (4119172)Instruction limit reached!
% 15.11/2.85 % (4119172)------------------------------
% 15.11/2.85 % (4119172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.11/2.85 % (4119172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/2.85 % (4119172)CaDiCaL version: 2.1.3
% 15.11/2.85 % (4119172)Termination reason: Instruction limit
% 15.11/2.85 % (4119172)Termination phase: Property scanning
% 15.11/2.85 % (4119172)Time elapsed: 0.053 s
% 15.11/2.85 % (4119172)Peak memory usage: 10 MB
% 15.11/2.85 % (4119172)Instructions burned: 71 (million)
% 15.11/2.85 % (4119178)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
% 15.11/2.85 % (4119178)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 15.11/2.85 % (4119178)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=730625995:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2977 on theBenchmark for (2977ds/100Mi)
% 15.11/2.85 % (4119179)Instruction limit reached!
% 15.11/2.85 % (4119179)------------------------------
% 15.11/2.85 % (4119179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.11/2.85 % (4119179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/2.85 % (4119179)CaDiCaL version: 2.1.3
% 15.11/2.85 % (4119179)Termination reason: Instruction limit
% 15.11/2.85 % (4119179)Termination phase: Saturation
% 15.11/2.85 % (4119179)Time elapsed: 0.016 s
% 15.11/2.85 % (4119179)Peak memory usage: 11 MB
% 15.11/2.85 % (4119179)Instructions burned: 77 (million)
% 15.11/2.85 % (4119183)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=2143520462:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2976 on theBenchmark for (2976ds/493Mi)
% 15.11/2.85 % (4119181)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=1410535043:i=289:rtra=on_2976 on theBenchmark for (2976ds/289Mi)
% 15.11/2.85 % (4119165)Instruction limit reached!
% 15.11/2.85 % (4119165)------------------------------
% 15.11/2.85 % (4119165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.11/2.85 % (4119165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.06 % (4119165)CaDiCaL version: 2.1.3
% 16.89/3.06 % (4119165)Termination reason: Instruction limit
% 16.89/3.06 % (4119165)Termination phase: Saturation
% 16.89/3.06 % (4119165)Time elapsed: 0.220 s
% 16.89/3.06 % (4119165)Peak memory usage: 15 MB
% 16.89/3.06 % (4119165)Instructions burned: 429 (million)
% 16.89/3.06 % (4119186)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=2520851515:cond=on:i=34:hud=10:nm=10:rtra=on_2976 on theBenchmark for (2976ds/34Mi)
% 16.89/3.06 % (4119162)Instruction limit reached!
% 16.89/3.06 % (4119162)------------------------------
% 16.89/3.06 % (4119162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.89/3.06 % (4119162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.06 % (4119162)CaDiCaL version: 2.1.3
% 16.89/3.06 % (4119162)Termination reason: Instruction limit
% 16.89/3.06 % (4119162)Termination phase: Saturation
% 16.89/3.06 % (4119162)Time elapsed: 0.276 s
% 16.89/3.06 % (4119162)Peak memory usage: 15 MB
% 16.89/3.06 % (4119162)Instructions burned: 380 (million)
% 16.89/3.06 % (4119186)Instruction limit reached!
% 16.89/3.06 % (4119186)------------------------------
% 16.89/3.06 % (4119186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.89/3.06 % (4119186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.06 % (4119186)CaDiCaL version: 2.1.3
% 16.89/3.06 % (4119186)Termination reason: Instruction limit
% 16.89/3.06 % (4119186)Termination phase: Function definition elimination
% 16.89/3.06 % (4119186)Time elapsed: 0.015 s
% 16.89/3.06 % (4119186)Peak memory usage: 10 MB
% 16.89/3.06 % (4119186)Instructions burned: 34 (million)
% 16.89/3.06 % (4119178)Instruction limit reached!
% 16.89/3.06 % (4119178)------------------------------
% 16.89/3.06 % (4119178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.89/3.06 % (4119178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.06 % (4119178)CaDiCaL version: 2.1.3
% 16.89/3.06 % (4119178)Termination reason: Instruction limit
% 16.89/3.06 % (4119178)Termination phase: Saturation
% 16.89/3.06 % (4119178)Time elapsed: 0.078 s
% 16.89/3.06 % (4119178)Peak memory usage: 12 MB
% 16.89/3.06 % (4119178)Instructions burned: 102 (million)
% 16.89/3.06 % (4119188)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 16.89/3.06 % (4119188)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=328517206:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2976 on theBenchmark for (2976ds/372Mi)
% 16.89/3.06 % (4119189)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=2950717645:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2976 on theBenchmark for (2976ds/670Mi)
% 16.89/3.06 % (4119190)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2645811960:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2975 on theBenchmark for (2975ds/647Mi)
% 16.89/3.06 % (4119183)Instruction limit reached!
% 16.89/3.06 % (4119183)------------------------------
% 16.89/3.06 % (4119183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.89/3.06 % (4119183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.06 % (4119183)CaDiCaL version: 2.1.3
% 16.89/3.06 % (4119183)Termination reason: Instruction limit
% 16.89/3.06 % (4119183)Termination phase: Saturation
% 16.89/3.06 % (4119183)Time elapsed: 0.117 s
% 16.89/3.06 % (4119183)Peak memory usage: 14 MB
% 16.89/3.06 % (4119183)Instructions burned: 496 (million)
% 16.89/3.06 % (4119190)Refutation not found, incomplete strategy
% 16.89/3.06 % (4119190)------------------------------
% 16.89/3.06 % (4119190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.89/3.06 % (4119190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.06 % (4119190)CaDiCaL version: 2.1.3
% 16.89/3.06 % (4119190)Termination reason: Refutation not found, incomplete strategy
% 16.89/3.06 % (4119190)Time elapsed: 0.025 s
% 16.89/3.06 % (4119190)Peak memory usage: 12 MB
% 16.89/3.06 % (4119190)Instructions burned: 38 (million)
% 16.89/3.06 % (4119190)------------------------------
% 16.89/3.06 % (4119190)------------------------------
% 16.89/3.06 % (4119194)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=1979275995:i=857:add=off:kws=frequency:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/857Mi)
% 17.40/3.17 % (4119181)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119181)------------------------------
% 17.40/3.17 % (4119181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119181)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119181)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119181)Time elapsed: 0.132 s
% 17.40/3.17 % (4119181)Peak memory usage: 13 MB
% 17.40/3.17 % (4119181)Instructions burned: 184 (million)
% 17.40/3.17 % (4119195)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=3789937657:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2975 on theBenchmark for (2975ds/693Mi)
% 17.40/3.17 % (4119181)------------------------------
% 17.40/3.17 % (4119181)------------------------------
% 17.40/3.17 % (4119198)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=3637931498:i=285:hud=10:bd=all:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/285Mi)
% 17.40/3.17 % (4119198)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119198)------------------------------
% 17.40/3.17 % (4119198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119198)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119198)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119198)Time elapsed: 0.012 s
% 17.40/3.17 % (4119198)Peak memory usage: 12 MB
% 17.40/3.17 % (4119198)Instructions burned: 27 (million)
% 17.40/3.17 % (4119198)------------------------------
% 17.40/3.17 % (4119198)------------------------------
% 17.40/3.17 % (4119200)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 17.40/3.17 % (4119200)dis+1002_50_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=1:si=on:sp=occurrence:plsqr=64,1:nwc=3:flr=on:chr=on:random_seed=3749578403:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2974 on theBenchmark for (2974ds/52Mi)
% 17.40/3.17 % (4119194)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119194)------------------------------
% 17.40/3.17 % (4119194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119194)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119194)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119194)Time elapsed: 0.091 s
% 17.40/3.17 % (4119194)Peak memory usage: 14 MB
% 17.40/3.17 % (4119194)Instructions burned: 199 (million)
% 17.40/3.17 % (4119194)------------------------------
% 17.40/3.17 % (4119194)------------------------------
% 17.40/3.17 % (4119200)Instruction limit reached!
% 17.40/3.17 % (4119200)------------------------------
% 17.40/3.17 % (4119200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119200)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119200)Termination reason: Instruction limit
% 17.40/3.17 % (4119200)Termination phase: Property scanning
% 17.40/3.17 % (4119200)Time elapsed: 0.021 s
% 17.40/3.17 % (4119200)Peak memory usage: 11 MB
% 17.40/3.17 % (4119200)Instructions burned: 53 (million)
% 17.40/3.17 % (4119188)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119188)------------------------------
% 17.40/3.17 % (4119188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119188)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119188)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119188)Time elapsed: 0.141 s
% 17.40/3.17 % (4119188)Peak memory usage: 13 MB
% 17.40/3.17 % (4119188)Instructions burned: 176 (million)
% 17.40/3.17 % (4119188)------------------------------
% 17.40/3.17 % (4119188)------------------------------
% 17.40/3.17 % (4119203)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=3221329989:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2974 on theBenchmark for (2974ds/2240Mi)
% 17.40/3.17 % (4119202)dis+10_1_si=on:random_seed=646962080:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2974 on theBenchmark for (2974ds/407Mi)
% 17.40/3.17 % (4119204)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=3861102679:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2974 on theBenchmark for (2974ds/336Mi)
% 17.40/3.17 % (4119204)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119204)------------------------------
% 17.40/3.17 % (4119204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119204)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119204)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119204)Time elapsed: 0.028 s
% 17.40/3.17 % (4119204)Peak memory usage: 12 MB
% 17.40/3.17 % (4119204)Instructions burned: 33 (million)
% 17.40/3.17 % (4119204)------------------------------
% 17.40/3.17 % (4119204)------------------------------
% 17.40/3.17 % (4119202)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119202)------------------------------
% 17.40/3.17 % (4119202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119202)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119202)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119202)Time elapsed: 0.070 s
% 17.40/3.17 % (4119202)Peak memory usage: 13 MB
% 17.40/3.17 % (4119202)Instructions burned: 102 (million)
% 17.40/3.17 % (4119202)------------------------------
% 17.40/3.17 % (4119202)------------------------------
% 17.40/3.17 % (4119208)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=92001168:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2973 on theBenchmark for (2973ds/1142Mi)
% 17.40/3.17 % (4119210)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=408306647:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2973 on theBenchmark for (2973ds/376Mi)
% 17.40/3.17 % (4119210)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119210)------------------------------
% 17.40/3.17 % (4119210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119210)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119210)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119210)Time elapsed: 0.017 s
% 17.40/3.17 % (4119210)Peak memory usage: 12 MB
% 17.40/3.17 % (4119210)Instructions burned: 40 (million)
% 17.40/3.17 % (4119210)------------------------------
% 17.40/3.17 % (4119210)------------------------------
% 17.40/3.17 % (4119212)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=3121070897:i=766:bd=all:rtra=on_2973 on theBenchmark for (2973ds/766Mi)
% 17.40/3.17 % (4119195)Instruction limit reached!
% 17.40/3.17 % (4119195)------------------------------
% 17.40/3.17 % (4119195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119195)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119195)Termination reason: Instruction limit
% 17.40/3.17 % (4119195)Termination phase: Saturation
% 17.40/3.17 % (4119195)Time elapsed: 0.276 s
% 17.40/3.17 % (4119195)Peak memory usage: 15 MB
% 17.40/3.17 % (4119195)Instructions burned: 694 (million)
% 17.40/3.17 % (4119208)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119208)------------------------------
% 17.40/3.17 % (4119208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119208)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119208)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119208)Time elapsed: 0.125 s
% 17.40/3.17 % (4119208)Peak memory usage: 14 MB
% 17.40/3.17 % (4119208)Instructions burned: 277 (million)
% 17.40/3.17 % (4119208)------------------------------
% 17.40/3.17 % (4119208)------------------------------
% 17.40/3.17 % (4119214)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 17.40/3.17 % (4119215)dis+1010_1024_sil=128000:plsq=on:plsqc=1:e2e=on:si=on:lma=off:plsqr=64,1:uwa=interpreted_only:fd=off:random_seed=250022486:i=6359:add=on:kws=inv_frequency:aac=none:rtra=on:c=on:er=filter:ntd=on_2972 on theBenchmark for (2972ds/6359Mi)
% 17.40/3.17 % (4119214)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=4015264148:st=3:uwa_fpi=on:i=959:fgj=on:piset=pi_sigma:hud=5:nm=16:rtra=on:fe=abstraction:ss=axioms:ixr=off:ntd=on_2972 on theBenchmark for (2972ds/959Mi)
% 17.40/3.17 % (4119212)Refutation not found, incomplete strategy
% 17.40/3.17 % (4119212)------------------------------
% 17.40/3.17 % (4119212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.17 % (4119212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.17 % (4119212)CaDiCaL version: 2.1.3
% 17.40/3.17 % (4119212)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.17 % (4119212)Time elapsed: 0.109 s
% 17.40/3.17 % (4119212)Peak memory usage: 14 MB
% 17.40/3.17 % (4119212)Instructions burned: 189 (million)
% 17.40/3.17 % (4119212)------------------------------
% 17.40/3.17 % (4119212)------------------------------
% 17.40/3.17 % (4119218)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3385644958:st=4:i=35:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2971 on theBenchmark for (2971ds/35Mi)
% 17.40/3.18 % (4119218)Instruction limit reached!
% 17.40/3.18 % (4119218)------------------------------
% 17.40/3.18 % (4119218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.18 % (4119218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.18 % (4119218)CaDiCaL version: 2.1.3
% 17.40/3.18 % (4119218)Termination reason: Instruction limit
% 17.40/3.18 % (4119218)Termination phase: Twee Goal Transformation
% 17.40/3.18 % (4119218)Time elapsed: 0.014 s
% 17.40/3.18 % (4119218)Peak memory usage: 11 MB
% 17.40/3.18 % (4119218)Instructions burned: 36 (million)
% 17.40/3.18 % (4119220)dis+10_1_sfv=off:sil=128000:cnfonf=lazy_gen:si=on:uwa=off:nwc=1:chr=on:random_seed=330441305:hsq=on:hsqr=1,8:i=53:hsql=off:bd=all:rtra=on:ixr=off_2971 on theBenchmark for (2971ds/53Mi)
% 17.40/3.18 % (4119214)Refutation not found, incomplete strategy
% 17.40/3.18 % (4119214)------------------------------
% 17.40/3.18 % (4119214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.18 % (4119214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.18 % (4119214)CaDiCaL version: 2.1.3
% 17.40/3.18 % (4119214)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.18 % (4119214)Time elapsed: 0.092 s
% 17.40/3.18 % (4119214)Peak memory usage: 13 MB
% 17.40/3.18 % (4119214)Instructions burned: 170 (million)
% 17.40/3.18 % (4119203) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4118893-4119203"...
% 17.40/3.18 % (4119214)------------------------------
% 17.40/3.18 % (4119214)------------------------------
% 17.40/3.18 % (4119203)...printing done.
% 17.40/3.18 % (4119203)Refutation found. Thanks to Tanya!
% 17.40/3.18 % SZS status Theorem for theBenchmark
% 17.40/3.18 % SZS output start Proof for theBenchmark
% See solution above
% 17.40/3.18 % (4119203)------------------------------
% 17.40/3.18 % (4119203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.40/3.18 % (4119203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.18 % (4119203)CaDiCaL version: 2.1.3
% 17.40/3.18 % (4119203)Termination reason: Refutation
% 17.40/3.18 % (4119203)Time elapsed: 0.320 s
% 17.40/3.18 % (4119203)Peak memory usage: 16 MB
% 17.40/3.18 % (4119203)Instructions burned: 446 (million)
% 17.40/3.18 % (4118893)Success in time 2.9 s
% 17.40/3.18 % Vampire exiting
%------------------------------------------------------------------------------