%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO532^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:48:21 AM UTC 2026
% Result : Theorem 19.40s 3.05s
% Output : Refutation 19.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 3
% Syntax : Number of formulae : 33 ( 28 unt; 0 typ; 0 def)
% Number of atoms : 136 ( 27 equ; 0 cnn)
% Maximal formula atoms : 1 ( 4 avg)
% Number of connectives : 389 ( 6 ~; 0 |; 0 &; 303 @)
% ( 0 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 156 ( 156 >; 0 *; 0 +; 0 <<)
% Number of symbols : 39 ( 34 usr; 4 con; 0-6 aty)
% ( 10 !!; 46 ??; 0 @@+; 0 @@-)
% Number of variables : 100 ( 72 ^; 17 !; 11 ?; 100 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
eps: ( $i > $o ) > $i ).
thf(func_def_2,type,
epsb: ( ( $i > $i > $o ) > $i ) > ( $i > $i > $o ) > $i ).
thf(func_def_3,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_4,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_5,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_6,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_7,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_8,type,
vIMP: $o > $o > $o ).
thf(func_def_9,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_12,type,
vNOT: $o > $o ).
thf(func_def_13,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_14,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_15,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_16,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_17,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_18,type,
db8:
!>[X0: $tType] : X0 ).
thf(func_def_19,type,
sK0: ( ( $i > $i > $o ) > $i ) > $i > $i > $o ).
thf(func_def_20,type,
sK1: ( ( $i > $i > $o ) > $i ) > $i ).
thf(func_def_21,type,
sK2: ( ( $i > $i > $o ) > $i ) > $i ).
thf(func_def_22,type,
sK3: ( ( $i > $i > $o ) > $i ) > $i ).
thf(func_def_23,type,
sK4: ( $i > ( $i > $i > $o ) > $i ) > ( $i > ( $i > $i > $o ) > $i > $i > $i ) > ( $i > ( $i > $i > $o ) > $i > $i ) > $i > $i > $o ).
thf(func_def_24,type,
db9:
!>[X0: $tType] : X0 ).
thf(func_def_25,type,
db10:
!>[X0: $tType] : X0 ).
thf(func_def_26,type,
db11:
!>[X0: $tType] : X0 ).
thf(func_def_27,type,
db12:
!>[X0: $tType] : X0 ).
thf(func_def_28,type,
db13:
!>[X0: $tType] : X0 ).
thf(func_def_29,type,
db14:
!>[X0: $tType] : X0 ).
thf(func_def_30,type,
db15:
!>[X0: $tType] : X0 ).
thf(func_def_31,type,
db16:
!>[X0: $tType] : X0 ).
thf(func_def_32,type,
db17:
!>[X0: $tType] : X0 ).
thf(func_def_33,type,
sK5: ( $i > ( $i > $i > $o ) > $i ) > ( $i > ( $i > $i > $o ) > $i > $i > $i ) > ( $i > ( $i > $i > $o ) > $i > $i ) > $i > $i > $o ).
thf(func_def_34,type,
sK6: ( $i > ( $i > $i > $o ) > $i ) > ( $i > ( $i > $i > $o ) > $i > $i > $i ) > $i > ( $i > ( $i > $i > $o ) > $i > $i ) > $i > $i > $o ).
thf(func_def_35,type,
sK7: ( $i > ( $i > $i > $o ) > $i ) > ( $i > ( $i > $i > $o ) > $i > $i > $i ) > ( $i > ( $i > $i > $o ) > $i > $i ) > $i > $i > $o ).
thf(f1,axiom,
! [X0: $i > $o] :
( ? [X1: $i] : ( X0 @ X1 )
=> ( X0 @ ( eps @ X0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',choiceax) ).
thf(f2,axiom,
( epsb
= ( ^ [X0: ( $i > $i > $o ) > $i,X1: $i > $i > $o] :
( eps
@ ^ [X2: $i] : ( X1 @ ( X0 @ X1 ) @ X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',epsbd) ).
thf(f3,conjecture,
? [X0: ( $i > $i > $o ) > $i] :
! [X1: $i > $i > $o] :
( ? [X3: $i,X2: $i] : ( X1 @ X2 @ X3 )
=> ( X1 @ ( X0 @ X1 ) @ ( epsb @ X0 @ X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
thf(f4,negated_conjecture,
~ ? [X0: ( $i > $i > $o ) > $i] :
! [X1: $i > $i > $o] :
( ? [X3: $i,X2: $i] : ( X1 @ X2 @ X3 )
=> ( X1 @ ( X0 @ X1 ) @ ( epsb @ X0 @ X1 ) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
thf(f5,plain,
( epsb
= ( ^ [X0: ( $i > $i > $o ) > $i,X1: $i > $i > $o] :
( eps
@ ^ [X2: $i] : ( X1 @ ( X0 @ X1 ) @ X2 ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f6,plain,
( epsb
= ( ^ [Y0: ( $i > $i > $o ) > $i,Y1: $i > $i > $o] :
( eps
@ ^ [Y2: $i] : ( Y1 @ ( Y0 @ Y1 ) @ Y2 ) ) ) ),
inference(fool_elimination,[],[f5]) ).
thf(f7,plain,
! [X0: $i > $o] :
( ? [X1: $i] : ( X0 @ X1 )
=> ( X0 @ ( eps @ X0 ) ) ),
inference(rectify,[],[f1]) ).
thf(f8,plain,
( $true
= ( !! @ ( $i > $o )
@ ^ [Y0: $i > $o] :
( ( ?? @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
=> ( Y0 @ ( eps @ Y0 ) ) ) ) ),
inference(fool_elimination,[],[f7]) ).
thf(f9,plain,
~ ? [X0: ( $i > $i > $o ) > $i] :
! [X1: $i > $i > $o] :
( ? [X2: $i,X3: $i] : ( X1 @ X3 @ X2 )
=> ( X1 @ ( X0 @ X1 ) @ ( epsb @ X0 @ X1 ) ) ),
inference(rectify,[],[f4]) ).
thf(f10,plain,
( $true
= ( ~ ( ?? @ ( ( $i > $i > $o ) > $i )
@ ^ [Y0: ( $i > $i > $o ) > $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y2: $i] :
( ?? @ $i
@ ^ [Y3: $i] : ( Y1 @ Y2 @ Y3 ) ) )
=> ( Y1 @ ( Y0 @ Y1 ) @ ( epsb @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f9]) ).
thf(f11,plain,
( $true
= ( !! @ ( $i > $o )
@ ^ [Y0: $i > $o] :
( ( ?? @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
=> ( Y0 @ ( eps @ Y0 ) ) ) ) ),
inference(cnf_transformation,[],[f8]) ).
thf(f12,plain,
( $true
= ( ~ ( ?? @ ( ( $i > $i > $o ) > $i )
@ ^ [Y0: ( $i > $i > $o ) > $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y2: $i] :
( ?? @ $i
@ ^ [Y3: $i] : ( Y1 @ Y2 @ Y3 ) ) )
=> ( Y1 @ ( Y0 @ Y1 ) @ ( epsb @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f10]) ).
thf(f13,plain,
( epsb
= ( ^ [Y0: ( $i > $i > $o ) > $i,Y1: $i > $i > $o] :
( eps
@ ^ [Y2: $i] : ( Y1 @ ( Y0 @ Y1 ) @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f6]) ).
thf(f16,plain,
( ( ~ ( ?? @ ( ( $i > $i > $o ) > $i )
@ ^ [Y0: ( $i > $i > $o ) > $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y2: $i] :
( ?? @ $i
@ ^ [Y3: $i] : ( Y1 @ Y2 @ Y3 ) ) )
=> ( Y1 @ ( Y0 @ Y1 )
@ ( ^ [Y2: ( $i > $i > $o ) > $i,Y3: $i > $i > $o] :
( eps
@ ^ [Y4: $i] : ( Y3 @ ( Y2 @ Y3 ) @ Y4 ) )
@ Y0
@ Y1 ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f12,f13]) ).
thf(f17,plain,
( $true
= ( !! @ ( $i > $o )
@ ^ [Y0: $i > $o] :
( ( ?? @ $i @ Y0 )
=> ( Y0 @ ( eps @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f11]) ).
thf(f18,plain,
( $true
= ( ~ ( ?? @ ( ( $i > $i > $o ) > $i )
@ ^ [Y0: ( $i > $i > $o ) > $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y2: $i] : ( ?? @ $i @ ( Y1 @ Y2 ) ) )
=> ( Y1 @ ( Y0 @ Y1 ) @ ( eps @ ( Y1 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f16]) ).
thf(f19,plain,
! [X1: $i > $o] :
( $true
= ( ^ [Y0: $i > $o] :
( ( ?? @ $i @ Y0 )
=> ( Y0 @ ( eps @ Y0 ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f17]) ).
thf(f20,plain,
! [X1: $i > $o] :
( $true
= ( ( ?? @ $i @ X1 )
=> ( X1 @ ( eps @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f19]) ).
thf(f28,plain,
( ( ?? @ ( ( $i > $i > $o ) > $i )
@ ^ [Y0: ( $i > $i > $o ) > $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y2: $i] : ( ?? @ $i @ ( Y1 @ Y2 ) ) )
=> ( Y1 @ ( Y0 @ Y1 ) @ ( eps @ ( Y1 @ ( Y0 @ Y1 ) ) ) ) ) ) )
= $false ),
inference(not_proxy_clausification,[],[f18]) ).
thf(f32,plain,
! [X1: ( $i > $i > $o ) > $i] :
( ( ^ [Y0: ( $i > $i > $o ) > $i] :
( !! @ ( $i > $i > $o )
@ ^ [Y1: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y2: $i] : ( ?? @ $i @ ( Y1 @ Y2 ) ) )
=> ( Y1 @ ( Y0 @ Y1 ) @ ( eps @ ( Y1 @ ( Y0 @ Y1 ) ) ) ) ) )
@ X1 )
= $false ),
inference(pi_proxy_clausification,[],[f28]) ).
thf(f37,plain,
! [X1: ( $i > $i > $o ) > $i] :
( ( !! @ ( $i > $i > $o )
@ ^ [Y0: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y1: $i] : ( ?? @ $i @ ( Y0 @ Y1 ) ) )
=> ( Y0 @ ( X1 @ Y0 ) @ ( eps @ ( Y0 @ ( X1 @ Y0 ) ) ) ) ) )
= $false ),
inference(beta-eta_normalization,[],[f32]) ).
thf(f39,plain,
! [X1: ( $i > $i > $o ) > $i] :
( ( ^ [Y0: $i > $i > $o] :
( ( ?? @ $i
@ ^ [Y1: $i] : ( ?? @ $i @ ( Y0 @ Y1 ) ) )
=> ( Y0 @ ( X1 @ Y0 ) @ ( eps @ ( Y0 @ ( X1 @ Y0 ) ) ) ) )
@ ( sK0 @ X1 ) )
= $false ),
inference(sigma_proxy_clausification,[],[f37]) ).
thf(f41,plain,
! [X1: ( $i > $i > $o ) > $i] :
( ( ( ?? @ $i
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X1 @ Y0 ) ) )
=> ( sK0 @ X1 @ ( X1 @ ( sK0 @ X1 ) ) @ ( eps @ ( sK0 @ X1 @ ( X1 @ ( sK0 @ X1 ) ) ) ) ) )
= $false ),
inference(beta-eta_normalization,[],[f39]) ).
thf(f45,plain,
! [X1: ( $i > $i > $o ) > $i] :
( $true
= ( ?? @ $i
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X1 @ Y0 ) ) ) ),
inference(imp_proxy_clausification,[],[f41]) ).
thf(f50,plain,
! [X0: ( $i > $i > $o ) > $i] :
( $true
= ( $true
=> ( ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) )
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) ) ) ) ),
inference(constrained_superposition,[],[f20,f45]) ).
thf(f57,plain,
! [X0: ( $i > $i > $o ) > $i] :
( ( $true
=> ( ?? @ $i
@ ( sK0 @ X0
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f50]) ).
thf(f58,plain,
! [X0: ( $i > $i > $o ) > $i] :
( ( ?? @ $i
@ ( sK0 @ X0
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) ) ) )
= $true ),
inference(boolean_simplification,[],[f57]) ).
thf(f79,plain,
! [X0: ( $i > $i > $o ) > $i] :
( $true
= ( $true
=> ( sK0 @ X0
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) )
@ ( eps
@ ( sK0 @ X0
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) ) ) ) ) ) ),
inference(constrained_superposition,[],[f20,f58]) ).
thf(f82,plain,
! [X0: ( $i > $i > $o ) > $i] :
( ( sK0 @ X0
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) )
@ ( eps
@ ( sK0 @ X0
@ ( eps
@ ^ [Y0: $i] : ( ?? @ $i @ ( sK0 @ X0 @ Y0 ) ) ) ) ) )
= $true ),
inference(boolean_simplification,[],[f79]) ).
thf(f136,plain,
( ( ( ?? @ $i
@ ^ [Y0: $i] :
( ?? @ $i
@ ( sK0
@ ^ [Y1: $i > $i > $o] :
( eps
@ ( ^ [Y2: $i > $i > $o,Y3: $i] :
( ?? @ $i
@ ( ^ [Y4: $i > $i > $o,Y5: $i,Y6: $i] :
( Y4
@ ( ^ [Y7: $i > $i > $o,Y8: $i,Y9: $i] : Y8
@ Y4
@ Y5
@ Y6 )
@ ( ^ [Y7: $i > $i > $o,Y8: $i,Y9: $i] : Y9
@ Y4
@ Y5
@ Y6 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ Y0 ) ) )
=> $true )
= $false ),
inference(constrained_superposition,[],[f41,f82]) ).
thf(f146,plain,
( ( ( ?? @ $i
@ ^ [Y0: $i] :
( ?? @ $i
@ ( sK0
@ ^ [Y1: $i > $i > $o] :
( eps
@ ^ [Y2: $i] : ( ?? @ $i @ ( Y1 @ Y2 ) ) )
@ Y0 ) ) )
=> $true )
= $false ),
inference(beta-eta_normalization,[],[f136]) ).
thf(f147,plain,
$true = $false,
inference(boolean_simplification,[],[f146]) ).
thf(f148,plain,
$false,
inference(trivial_inequality_removal,[],[f147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO532^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n007.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 17:11:11 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/0.22 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.21/0.33 % (3665673)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.33 % (3665679)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1835042356:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.33 % (3665679)Refutation not found, incomplete strategy
% 0.21/0.33 % (3665679)------------------------------
% 0.21/0.33 % (3665679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3665679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3665679)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3665679)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.33 % (3665679)Time elapsed: 0.002 s
% 0.21/0.33 % (3665679)Peak memory usage: 12 MB
% 0.21/0.33 % (3665679)Instructions burned: 6 (million)
% 0.21/0.33 % (3665679)------------------------------
% 0.21/0.33 % (3665679)------------------------------
% 0.21/0.33 % (3665682)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=3741885994: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.21/0.33 % (3665681)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3514067:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.33 % (3665680)lrs+10_16_si=on:nwc=1.5:random_seed=3426610557:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.33 % (3665681)Refutation not found, incomplete strategy
% 0.21/0.33 % (3665681)------------------------------
% 0.21/0.33 % (3665681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3665681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3665681)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3665681)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.33 % (3665681)Time elapsed: 0.002 s
% 0.21/0.33 % (3665681)Peak memory usage: 12 MB
% 0.21/0.33 % (3665681)Instructions burned: 2 (million)
% 0.21/0.33 % (3665681)------------------------------
% 0.21/0.33 % (3665681)------------------------------
% 0.21/0.33 % (3665687)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2636655803:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.33 % (3665687)Instruction limit reached!
% 0.21/0.33 % (3665687)------------------------------
% 0.21/0.33 % (3665687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3665687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3665687)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3665687)Termination reason: Instruction limit
% 0.21/0.33 % (3665687)Termination phase: Saturation
% 0.21/0.33 % (3665687)Time elapsed: 0.001 s
% 0.21/0.33 % (3665687)Peak memory usage: 12 MB
% 0.21/0.33 % (3665687)Instructions burned: 2 (million)
% 0.21/0.33 % (3665683)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=654263401:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.33 % (3665685)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.33 % (3665685)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.21/0.33 % (3665693)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.33 % (3665680)Instruction limit reached!
% 0.21/0.33 % (3665680)------------------------------
% 0.21/0.33 % (3665680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (3665680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (3665680)CaDiCaL version: 2.1.3
% 0.21/0.33 % (3665680)Termination reason: Instruction limit
% 0.21/0.33 % (3665680)Termination phase: Saturation
% 0.21/0.33 % (3665680)Time elapsed: 0.013 s
% 0.21/0.33 % (3665680)Peak memory usage: 12 MB
% 0.21/0.33 % (3665680)Instructions burned: 19 (million)
% 0.21/0.33 % (3665693)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2755429445:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.33 % (3665684)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=275142602:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.36 % (3665693)Instruction limit reached!
% 0.21/0.36 % (3665693)------------------------------
% 0.21/0.36 % (3665693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (3665693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (3665693)CaDiCaL version: 2.1.3
% 0.21/0.36 % (3665693)Termination reason: Instruction limit
% 0.21/0.36 % (3665693)Termination phase: Saturation
% 0.21/0.36 % (3665693)Time elapsed: 0.003 s
% 0.21/0.36 % (3665693)Peak memory usage: 12 MB
% 0.21/0.36 % (3665693)Instructions burned: 7 (million)
% 0.21/0.36 % (3665685)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=2358065384:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.36 % (3665691)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=706146630:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.36 % (3665685)Refutation not found, incomplete strategy
% 0.21/0.36 % (3665685)------------------------------
% 0.21/0.36 % (3665685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (3665685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (3665685)CaDiCaL version: 2.1.3
% 0.21/0.36 % (3665685)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.36 % (3665685)Time elapsed: 0.003 s
% 0.21/0.36 % (3665685)Peak memory usage: 12 MB
% 0.21/0.36 % (3665685)Instructions burned: 4 (million)
% 0.21/0.36 % (3665685)------------------------------
% 0.21/0.36 % (3665685)------------------------------
% 0.21/0.36 % (3665691)Instruction limit reached!
% 0.21/0.36 % (3665691)------------------------------
% 0.21/0.36 % (3665691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (3665691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (3665691)CaDiCaL version: 2.1.3
% 0.21/0.36 % (3665691)Termination reason: Instruction limit
% 0.21/0.36 % (3665691)Termination phase: Saturation
% 0.21/0.36 % (3665691)Time elapsed: 0.004 s
% 0.21/0.36 % (3665691)Peak memory usage: 12 MB
% 0.21/0.36 % (3665691)Instructions burned: 6 (million)
% 0.21/0.36 % (3665698)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.21/0.36 % (3665698)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.36 % (3665698)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2789234180: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.21/0.36 % (3665695)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2104750905:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.21/0.36 % (3665683)Instruction limit reached!
% 0.21/0.36 % (3665683)------------------------------
% 0.21/0.36 % (3665683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (3665683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (3665683)CaDiCaL version: 2.1.3
% 0.21/0.36 % (3665683)Termination reason: Instruction limit
% 0.21/0.36 % (3665683)Termination phase: Saturation
% 0.21/0.36 % (3665683)Time elapsed: 0.024 s
% 0.21/0.36 % (3665683)Peak memory usage: 12 MB
% 0.21/0.36 % (3665683)Instructions burned: 25 (million)
% 0.21/0.36 % (3665698)Instruction limit reached!
% 0.21/0.36 % (3665698)------------------------------
% 0.21/0.36 % (3665698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.36 % (3665698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.36 % (3665698)CaDiCaL version: 2.1.3
% 0.21/0.36 % (3665698)Termination reason: Instruction limit
% 0.21/0.36 % (3665698)Termination phase: Saturation
% 0.21/0.36 % (3665698)Time elapsed: 0.008 s
% 0.21/0.36 % (3665698)Peak memory usage: 12 MB
% 0.21/0.36 % (3665698)Instructions burned: 28 (million)
% 0.21/0.36 % (3665695)Instruction limit reached!
% 0.21/0.36 % (3665695)------------------------------
% 0.21/0.36 % (3665695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.39 % (3665695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.39 % (3665695)CaDiCaL version: 2.1.3
% 0.93/0.39 % (3665695)Termination reason: Instruction limit
% 0.93/0.39 % (3665695)Termination phase: Saturation
% 0.93/0.39 % (3665695)Time elapsed: 0.008 s
% 0.93/0.39 % (3665695)Peak memory usage: 12 MB
% 0.93/0.39 % (3665695)Instructions burned: 12 (million)
% 0.93/0.39 % (3665702)lrs+10_1_si=on:cs=on:random_seed=1886654039:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.93/0.39 % (3665701)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=3442986308:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.93/0.39 % (3665706)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=192072325:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.93/0.39 % (3665706)Refutation not found, incomplete strategy
% 0.93/0.39 % (3665706)------------------------------
% 0.93/0.39 % (3665706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.39 % (3665706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.39 % (3665706)CaDiCaL version: 2.1.3
% 0.93/0.39 % (3665706)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.39 % (3665706)Time elapsed: 0.001 s
% 0.93/0.39 % (3665706)Peak memory usage: 12 MB
% 0.93/0.39 % (3665706)Instructions burned: 3 (million)
% 0.93/0.39 % (3665706)------------------------------
% 0.93/0.39 % (3665706)------------------------------
% 0.93/0.39 % (3665702)Instruction limit reached!
% 0.93/0.39 % (3665702)------------------------------
% 0.93/0.39 % (3665702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.39 % (3665702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.39 % (3665702)CaDiCaL version: 2.1.3
% 0.93/0.39 % (3665702)Termination reason: Instruction limit
% 0.93/0.39 % (3665702)Termination phase: Saturation
% 0.93/0.39 % (3665702)Time elapsed: 0.006 s
% 0.93/0.39 % (3665702)Peak memory usage: 12 MB
% 0.93/0.39 % (3665702)Instructions burned: 10 (million)
% 0.93/0.39 % (3665705)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.93/0.39 % (3665705)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=334803628:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.93/0.39 % (3665705)Instruction limit reached!
% 0.93/0.39 % (3665705)------------------------------
% 0.93/0.39 % (3665705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.39 % (3665705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.39 % (3665705)CaDiCaL version: 2.1.3
% 0.93/0.39 % (3665705)Termination reason: Instruction limit
% 0.93/0.39 % (3665705)Termination phase: Saturation
% 0.93/0.39 % (3665705)Time elapsed: 0.002 s
% 0.93/0.39 % (3665705)Peak memory usage: 12 MB
% 0.93/0.39 % (3665705)Instructions burned: 3 (million)
% 0.93/0.39 % (3665707)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=721295911:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.93/0.39 % (3665711)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1043405931:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.93/0.39 % (3665707)Refutation not found, incomplete strategy
% 0.93/0.39 % (3665707)------------------------------
% 0.93/0.39 % (3665707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.39 % (3665707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.39 % (3665707)CaDiCaL version: 2.1.3
% 0.93/0.39 % (3665707)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.39 % (3665707)Time elapsed: 0.002 s
% 0.93/0.39 % (3665707)Peak memory usage: 12 MB
% 0.93/0.39 % (3665707)Instructions burned: 2 (million)
% 0.93/0.39 % (3665684)Instruction limit reached!
% 0.93/0.39 % (3665684)------------------------------
% 0.93/0.39 % (3665684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.39 % (3665684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.39 % (3665684)CaDiCaL version: 2.1.3
% 0.93/0.42 % (3665684)Termination reason: Instruction limit
% 0.93/0.42 % (3665684)Termination phase: Saturation
% 0.93/0.42 % (3665684)Time elapsed: 0.046 s
% 0.93/0.42 % (3665684)Peak memory usage: 13 MB
% 0.93/0.42 % (3665684)Instructions burned: 75 (million)
% 0.93/0.42 % (3665707)------------------------------
% 0.93/0.42 % (3665707)------------------------------
% 0.93/0.42 % (3665711)Instruction limit reached!
% 0.93/0.42 % (3665711)------------------------------
% 0.93/0.42 % (3665711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.42 % (3665711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.42 % (3665711)CaDiCaL version: 2.1.3
% 0.93/0.42 % (3665711)Termination reason: Instruction limit
% 0.93/0.42 % (3665711)Termination phase: Saturation
% 0.93/0.42 % (3665711)Time elapsed: 0.007 s
% 0.93/0.42 % (3665711)Peak memory usage: 12 MB
% 0.93/0.42 % (3665711)Instructions burned: 26 (million)
% 0.93/0.42 % (3665712)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1043092571:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.93/0.42 % (3665712)Refutation not found, incomplete strategy
% 0.93/0.42 % (3665712)------------------------------
% 0.93/0.42 % (3665712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.42 % (3665712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.42 % (3665712)CaDiCaL version: 2.1.3
% 0.93/0.42 % (3665712)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.42 % (3665712)Time elapsed: 0.006 s
% 0.93/0.42 % (3665712)Peak memory usage: 12 MB
% 0.93/0.42 % (3665712)Instructions burned: 8 (million)
% 0.93/0.42 % (3665712)------------------------------
% 0.93/0.42 % (3665712)------------------------------
% 0.93/0.42 % (3665719)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1593976942:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.93/0.42 % (3665717)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2352971100:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.93/0.42 % (3665719)Refutation not found, incomplete strategy
% 0.93/0.42 % (3665719)------------------------------
% 0.93/0.42 % (3665719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.42 % (3665719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.42 % (3665719)CaDiCaL version: 2.1.3
% 0.93/0.42 % (3665719)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.42 % (3665719)Time elapsed: 0.002 s
% 0.93/0.42 % (3665719)Peak memory usage: 12 MB
% 0.93/0.42 % (3665719)Instructions burned: 6 (million)
% 0.93/0.42 % (3665719)------------------------------
% 0.93/0.42 % (3665719)------------------------------
% 0.93/0.42 % (3665718)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2397092193:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.93/0.42 % (3665718)Instruction limit reached!
% 0.93/0.42 % (3665718)------------------------------
% 0.93/0.42 % (3665718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.42 % (3665718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.42 % (3665718)CaDiCaL version: 2.1.3
% 0.93/0.42 % (3665718)Termination reason: Instruction limit
% 0.93/0.42 % (3665718)Termination phase: Saturation
% 0.93/0.42 % (3665718)Time elapsed: 0.003 s
% 0.93/0.42 % (3665718)Peak memory usage: 12 MB
% 0.93/0.42 % (3665718)Instructions burned: 4 (million)
% 0.93/0.42 % (3665714)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2164550887:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.93/0.42 % (3665717)Instruction limit reached!
% 0.93/0.42 % (3665717)------------------------------
% 0.93/0.42 % (3665717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.42 % (3665717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.42 % (3665717)CaDiCaL version: 2.1.3
% 0.93/0.42 % (3665717)Termination reason: Instruction limit
% 0.93/0.42 % (3665717)Termination phase: Saturation
% 0.93/0.42 % (3665717)Time elapsed: 0.009 s
% 0.93/0.42 % (3665717)Peak memory usage: 12 MB
% 0.93/0.42 % (3665717)Instructions burned: 15 (million)
% 0.93/0.42 % (3665725)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3384553452:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.93/0.46 % (3665721)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1903935670:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.93/0.46 % (3665714)Refutation not found, incomplete strategy
% 0.93/0.46 % (3665714)------------------------------
% 0.93/0.46 % (3665714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.46 % (3665714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.46 % (3665714)CaDiCaL version: 2.1.3
% 0.93/0.46 % (3665714)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.46 % (3665714)Time elapsed: 0.008 s
% 0.93/0.46 % (3665714)Peak memory usage: 12 MB
% 0.93/0.46 % (3665714)Instructions burned: 6 (million)
% 0.93/0.46 % (3665714)------------------------------
% 0.93/0.46 % (3665714)------------------------------
% 0.93/0.46 % (3665701)Instruction limit reached!
% 0.93/0.46 % (3665701)------------------------------
% 0.93/0.46 % (3665701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.46 % (3665701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.46 % (3665701)CaDiCaL version: 2.1.3
% 0.93/0.46 % (3665701)Termination reason: Instruction limit
% 0.93/0.46 % (3665701)Termination phase: Saturation
% 0.93/0.46 % (3665701)Time elapsed: 0.058 s
% 0.93/0.46 % (3665701)Peak memory usage: 13 MB
% 0.93/0.46 % (3665701)Instructions burned: 86 (million)
% 0.93/0.46 % (3665726)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
% 0.93/0.46 % (3665726)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.93/0.46 % (3665728)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.93/0.46 % (3665721)Instruction limit reached!
% 0.93/0.46 % (3665721)------------------------------
% 0.93/0.46 % (3665721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.46 % (3665721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.46 % (3665721)CaDiCaL version: 2.1.3
% 0.93/0.46 % (3665721)Termination reason: Instruction limit
% 0.93/0.46 % (3665721)Termination phase: Saturation
% 0.93/0.46 % (3665721)Time elapsed: 0.013 s
% 0.93/0.46 % (3665721)Peak memory usage: 11 MB
% 0.93/0.46 % (3665721)Instructions burned: 24 (million)
% 0.93/0.46 % (3665728)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=2113387267:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.93/0.46 % (3665725)Instruction limit reached!
% 0.93/0.46 % (3665725)------------------------------
% 0.93/0.46 % (3665725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.46 % (3665725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.46 % (3665725)CaDiCaL version: 2.1.3
% 0.93/0.46 % (3665725)Termination reason: Instruction limit
% 0.93/0.46 % (3665725)Termination phase: Saturation
% 0.93/0.46 % (3665725)Time elapsed: 0.017 s
% 0.93/0.46 % (3665725)Peak memory usage: 12 MB
% 0.93/0.46 % (3665725)Instructions burned: 61 (million)
% 0.93/0.46 % (3665728)Refutation not found, incomplete strategy
% 0.93/0.46 % (3665728)------------------------------
% 0.93/0.46 % (3665728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.46 % (3665728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.46 % (3665728)CaDiCaL version: 2.1.3
% 0.93/0.46 % (3665728)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.46 % (3665728)Time elapsed: 0.002 s
% 0.93/0.46 % (3665728)Peak memory usage: 12 MB
% 0.93/0.46 % (3665728)Instructions burned: 2 (million)
% 0.93/0.46 % (3665728)------------------------------
% 0.93/0.46 % (3665728)------------------------------
% 0.93/0.46 % (3665726)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=935099696:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.93/0.46 % (3665735)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2350770705:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 0.93/0.46 % (3665733)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1031529253:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.64/0.49 % (3665735)Instruction limit reached!
% 1.64/0.49 % (3665735)------------------------------
% 1.64/0.49 % (3665735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.49 % (3665732)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=182643824:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.64/0.49 % (3665735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.49 % (3665735)CaDiCaL version: 2.1.3
% 1.64/0.49 % (3665735)Termination reason: Instruction limit
% 1.64/0.49 % (3665735)Termination phase: Saturation
% 1.64/0.49 % (3665735)Time elapsed: 0.006 s
% 1.64/0.49 % (3665735)Peak memory usage: 12 MB
% 1.64/0.49 % (3665735)Instructions burned: 21 (million)
% 1.64/0.49 % (3665726)Instruction limit reached!
% 1.64/0.49 % (3665726)------------------------------
% 1.64/0.49 % (3665726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.49 % (3665726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.49 % (3665726)CaDiCaL version: 2.1.3
% 1.64/0.49 % (3665726)Termination reason: Instruction limit
% 1.64/0.49 % (3665726)Termination phase: Saturation
% 1.64/0.49 % (3665726)Time elapsed: 0.017 s
% 1.64/0.49 % (3665726)Peak memory usage: 12 MB
% 1.64/0.49 % (3665726)Instructions burned: 14 (million)
% 1.64/0.49 % (3665737)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2192614037:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.64/0.49 % (3665732)Instruction limit reached!
% 1.64/0.49 % (3665732)------------------------------
% 1.64/0.49 % (3665732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.49 % (3665732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.49 % (3665732)CaDiCaL version: 2.1.3
% 1.64/0.49 % (3665732)Termination reason: Instruction limit
% 1.64/0.49 % (3665732)Termination phase: Saturation
% 1.64/0.49 % (3665732)Time elapsed: 0.005 s
% 1.64/0.49 % (3665732)Peak memory usage: 12 MB
% 1.64/0.49 % (3665732)Instructions burned: 7 (million)
% 1.64/0.49 % (3665737)Refutation not found, incomplete strategy
% 1.64/0.49 % (3665737)------------------------------
% 1.64/0.49 % (3665737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.49 % (3665737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.49 % (3665737)CaDiCaL version: 2.1.3
% 1.64/0.49 % (3665737)Termination reason: Refutation not found, incomplete strategy
% 1.64/0.49 % (3665737)Time elapsed: 0.006 s
% 1.64/0.49 % (3665737)Peak memory usage: 12 MB
% 1.64/0.49 % (3665737)Instructions burned: 9 (million)
% 1.64/0.49 % (3665731)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=2235579957:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.64/0.49 % (3665737)------------------------------
% 1.64/0.49 % (3665737)------------------------------
% 1.64/0.49 % (3665733)Instruction limit reached!
% 1.64/0.49 % (3665733)------------------------------
% 1.64/0.49 % (3665733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.49 % (3665733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.49 % (3665733)CaDiCaL version: 2.1.3
% 1.64/0.49 % (3665733)Termination reason: Instruction limit
% 1.64/0.49 % (3665733)Termination phase: Saturation
% 1.64/0.49 % (3665733)Time elapsed: 0.012 s
% 1.64/0.49 % (3665733)Peak memory usage: 12 MB
% 1.64/0.49 % (3665733)Instructions burned: 23 (million)
% 1.64/0.49 % (3665743)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3027514259:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.64/0.49 % (3665743)Refutation not found, incomplete strategy
% 1.64/0.49 % (3665743)------------------------------
% 1.64/0.49 % (3665743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.49 % (3665743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.49 % (3665743)CaDiCaL version: 2.1.3
% 1.64/0.49 % (3665743)Termination reason: Refutation not found, incomplete strategy
% 1.64/0.49 % (3665743)Time elapsed: 0.002 s
% 1.64/0.49 % (3665743)Peak memory usage: 12 MB
% 1.64/0.49 % (3665743)Instructions burned: 5 (million)
% 1.64/0.49 % (3665743)------------------------------
% 1.64/0.54 % (3665743)------------------------------
% 1.64/0.54 % (3665741)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1843256436:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.64/0.54 % (3665746)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.64/0.54 % (3665746)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=86458971:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.64/0.54 % (3665747)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=510512276:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.64/0.54 % (3665731)Instruction limit reached!
% 1.64/0.54 % (3665731)------------------------------
% 1.64/0.54 % (3665731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.54 % (3665731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.54 % (3665731)CaDiCaL version: 2.1.3
% 1.64/0.54 % (3665731)Termination reason: Instruction limit
% 1.64/0.54 % (3665731)Termination phase: Saturation
% 1.64/0.54 % (3665731)Time elapsed: 0.024 s
% 1.64/0.54 % (3665731)Peak memory usage: 12 MB
% 1.64/0.54 % (3665731)Instructions burned: 32 (million)
% 1.64/0.54 % (3665746)Instruction limit reached!
% 1.64/0.54 % (3665746)------------------------------
% 1.64/0.54 % (3665746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.54 % (3665746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.54 % (3665746)CaDiCaL version: 2.1.3
% 1.64/0.54 % (3665746)Termination reason: Instruction limit
% 1.64/0.54 % (3665746)Termination phase: Saturation
% 1.64/0.54 % (3665746)Time elapsed: 0.005 s
% 1.64/0.54 % (3665746)Peak memory usage: 12 MB
% 1.64/0.54 % (3665746)Instructions burned: 9 (million)
% 1.64/0.54 % (3665744)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2700941579:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.64/0.54 % (3665753)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.64/0.54 % (3665753)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3512448424:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2998 on theBenchmark for (2998ds/6Mi)
% 1.64/0.54 % (3665750)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=2308988897:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/169Mi)
% 1.64/0.54 % (3665753)Instruction limit reached!
% 1.64/0.54 % (3665753)------------------------------
% 1.64/0.54 % (3665753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.54 % (3665753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.54 % (3665753)CaDiCaL version: 2.1.3
% 1.64/0.54 % (3665753)Termination reason: Instruction limit
% 1.64/0.54 % (3665753)Termination phase: Saturation
% 1.64/0.54 % (3665753)Time elapsed: 0.002 s
% 1.64/0.54 % (3665753)Peak memory usage: 12 MB
% 1.64/0.54 % (3665753)Instructions burned: 8 (million)
% 1.64/0.54 % (3665750)Refutation not found, incomplete strategy
% 1.64/0.54 % (3665750)------------------------------
% 1.64/0.54 % (3665750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.64/0.54 % (3665750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.64/0.54 % (3665750)CaDiCaL version: 2.1.3
% 1.64/0.54 % (3665750)Termination reason: Refutation not found, incomplete strategy
% 1.64/0.54 % (3665750)Time elapsed: 0.002 s
% 1.64/0.54 % (3665750)Peak memory usage: 12 MB
% 1.64/0.54 % (3665750)Instructions burned: 2 (million)
% 1.64/0.54 % (3665750)------------------------------
% 1.64/0.54 % (3665750)------------------------------
% 1.64/0.54 % (3665754)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3949408385:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 1.64/0.54 % (3665758)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3912367974:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 1.64/0.54 % (3665758)Refutation not found, incomplete strategy
% 2.27/0.58 % (3665758)------------------------------
% 2.27/0.58 % (3665758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.58 % (3665758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.58 % (3665758)CaDiCaL version: 2.1.3
% 2.27/0.58 % (3665758)Termination reason: Refutation not found, incomplete strategy
% 2.27/0.58 % (3665758)Time elapsed: 0.001 s
% 2.27/0.58 % (3665758)Peak memory usage: 12 MB
% 2.27/0.58 % (3665758)Instructions burned: 3 (million)
% 2.27/0.58 % (3665758)------------------------------
% 2.27/0.58 % (3665758)------------------------------
% 2.27/0.58 % (3665754)Instruction limit reached!
% 2.27/0.58 % (3665754)------------------------------
% 2.27/0.58 % (3665754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.58 % (3665754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.58 % (3665754)CaDiCaL version: 2.1.3
% 2.27/0.58 % (3665754)Termination reason: Instruction limit
% 2.27/0.58 % (3665754)Termination phase: Saturation
% 2.27/0.58 % (3665754)Time elapsed: 0.012 s
% 2.27/0.58 % (3665754)Peak memory usage: 12 MB
% 2.27/0.58 % (3665754)Instructions burned: 22 (million)
% 2.27/0.58 % (3665759)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=733503078:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.27/0.58 % (3665762)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=2431086076: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.27/0.58 % (3665744)Instruction limit reached!
% 2.27/0.58 % (3665744)------------------------------
% 2.27/0.58 % (3665744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.58 % (3665744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.58 % (3665744)CaDiCaL version: 2.1.3
% 2.27/0.58 % (3665744)Termination reason: Instruction limit
% 2.27/0.58 % (3665744)Termination phase: Saturation
% 2.27/0.58 % (3665744)Time elapsed: 0.036 s
% 2.27/0.58 % (3665744)Peak memory usage: 12 MB
% 2.27/0.58 % (3665744)Instructions burned: 42 (million)
% 2.27/0.58 % (3665763)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=3734585896:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.27/0.58 % (3665763)Refutation not found, incomplete strategy
% 2.27/0.58 % (3665763)------------------------------
% 2.27/0.58 % (3665763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.58 % (3665763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.58 % (3665763)CaDiCaL version: 2.1.3
% 2.27/0.58 % (3665763)Termination reason: Refutation not found, incomplete strategy
% 2.27/0.58 % (3665763)Time elapsed: 0.005 s
% 2.27/0.58 % (3665763)Peak memory usage: 12 MB
% 2.27/0.58 % (3665763)Instructions burned: 7 (million)
% 2.27/0.58 % (3665763)------------------------------
% 2.27/0.58 % (3665763)------------------------------
% 2.27/0.58 % (3665766)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2277431983:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.27/0.58 % (3665759)Refutation not found, incomplete strategy
% 2.27/0.58 % (3665759)------------------------------
% 2.27/0.58 % (3665759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.58 % (3665759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.58 % (3665759)CaDiCaL version: 2.1.3
% 2.27/0.58 % (3665759)Termination reason: Refutation not found, incomplete strategy
% 2.27/0.58 % (3665759)Time elapsed: 0.026 s
% 2.27/0.58 % (3665759)Peak memory usage: 12 MB
% 2.27/0.58 % (3665759)Instructions burned: 46 (million)
% 2.27/0.58 % (3665766)Refutation not found, incomplete strategy
% 2.27/0.58 % (3665766)------------------------------
% 2.27/0.58 % (3665766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.58 % (3665766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.58 % (3665766)CaDiCaL version: 2.1.3
% 2.27/0.58 % (3665766)Termination reason: Refutation not found, incomplete strategy
% 2.27/0.63 % (3665766)Time elapsed: 0.002 s
% 2.27/0.63 % (3665766)Peak memory usage: 12 MB
% 2.27/0.63 % (3665766)Instructions burned: 1 (million)
% 2.27/0.63 % (3665759)------------------------------
% 2.27/0.63 % (3665759)------------------------------
% 2.27/0.63 % (3665766)------------------------------
% 2.27/0.63 % (3665766)------------------------------
% 2.27/0.63 % (3665770)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.27/0.63 % (3665769)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=4196883801:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 2.27/0.63 % (3665770)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3774601330:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.27/0.63 % (3665771)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3463817807:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.27/0.63 % (3665747)Instruction limit reached!
% 2.27/0.63 % (3665747)------------------------------
% 2.27/0.63 % (3665747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.63 % (3665747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.63 % (3665747)CaDiCaL version: 2.1.3
% 2.27/0.63 % (3665747)Termination reason: Instruction limit
% 2.27/0.63 % (3665747)Termination phase: Saturation
% 2.27/0.63 % (3665747)Time elapsed: 0.092 s
% 2.27/0.63 % (3665747)Peak memory usage: 13 MB
% 2.27/0.63 % (3665747)Instructions burned: 181 (million)
% 2.27/0.63 % (3665769)Instruction limit reached!
% 2.27/0.63 % (3665769)------------------------------
% 2.27/0.63 % (3665769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.63 % (3665769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.63 % (3665769)CaDiCaL version: 2.1.3
% 2.27/0.63 % (3665769)Termination reason: Instruction limit
% 2.27/0.63 % (3665769)Termination phase: Saturation
% 2.27/0.63 % (3665769)Time elapsed: 0.013 s
% 2.27/0.63 % (3665769)Peak memory usage: 12 MB
% 2.27/0.63 % (3665769)Instructions burned: 23 (million)
% 2.27/0.63 % (3665771)Instruction limit reached!
% 2.27/0.63 % (3665771)------------------------------
% 2.27/0.63 % (3665771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.63 % (3665771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.63 % (3665771)CaDiCaL version: 2.1.3
% 2.27/0.63 % (3665771)Termination reason: Instruction limit
% 2.27/0.63 % (3665771)Termination phase: Saturation
% 2.27/0.63 % (3665771)Time elapsed: 0.012 s
% 2.27/0.63 % (3665771)Peak memory usage: 12 MB
% 2.27/0.63 % (3665771)Instructions burned: 18 (million)
% 2.27/0.63 % (3665741)Instruction limit reached!
% 2.27/0.63 % (3665741)------------------------------
% 2.27/0.63 % (3665741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.63 % (3665741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.63 % (3665741)CaDiCaL version: 2.1.3
% 2.27/0.63 % (3665741)Termination reason: Instruction limit
% 2.27/0.63 % (3665741)Termination phase: Saturation
% 2.27/0.63 % (3665741)Time elapsed: 0.111 s
% 2.27/0.63 % (3665741)Peak memory usage: 12 MB
% 2.27/0.63 % (3665741)Instructions burned: 143 (million)
% 2.27/0.63 % (3665775)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=414207663:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.27/0.63 % (3665776)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2438813955:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 2.27/0.63 % (3665776)Refutation not found, incomplete strategy
% 2.27/0.63 % (3665776)------------------------------
% 2.27/0.63 % (3665776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.63 % (3665776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.63 % (3665776)CaDiCaL version: 2.1.3
% 2.27/0.63 % (3665776)Termination reason: Refutation not found, incomplete strategy
% 2.27/0.63 % (3665776)Time elapsed: 0.003 s
% 2.27/0.63 % (3665776)Peak memory usage: 12 MB
% 2.27/0.63 % (3665776)Instructions burned: 3 (million)
% 2.27/0.63 % (3665775)Refutation not found, incomplete strategy
% 2.27/0.63 % (3665775)------------------------------
% 2.27/0.63 % (3665775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (3665775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (3665775)CaDiCaL version: 2.1.3
% 2.60/0.67 % (3665775)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.67 % (3665775)Time elapsed: 0.004 s
% 2.60/0.67 % (3665775)Peak memory usage: 13 MB
% 2.60/0.67 % (3665775)Instructions burned: 5 (million)
% 2.60/0.67 % (3665776)------------------------------
% 2.60/0.67 % (3665776)------------------------------
% 2.60/0.67 % (3665775)------------------------------
% 2.60/0.67 % (3665775)------------------------------
% 2.60/0.67 % (3665778)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3549427552:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2997 on theBenchmark for (2997ds/137Mi)
% 2.60/0.67 % (3665777)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2377111893:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.60/0.67 % (3665777)Refutation not found, incomplete strategy
% 2.60/0.67 % (3665777)------------------------------
% 2.60/0.67 % (3665777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (3665777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (3665777)CaDiCaL version: 2.1.3
% 2.60/0.67 % (3665777)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.67 % (3665777)Time elapsed: 0.005 s
% 2.60/0.67 % (3665777)Peak memory usage: 12 MB
% 2.60/0.67 % (3665777)Instructions burned: 4 (million)
% 2.60/0.67 % (3665682)Instruction limit reached!
% 2.60/0.67 % (3665682)------------------------------
% 2.60/0.67 % (3665682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (3665682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (3665682)CaDiCaL version: 2.1.3
% 2.60/0.67 % (3665682)Termination reason: Instruction limit
% 2.60/0.67 % (3665682)Termination phase: Saturation
% 2.60/0.67 % (3665682)Time elapsed: 0.290 s
% 2.60/0.67 % (3665682)Peak memory usage: 18 MB
% 2.60/0.67 % (3665682)Instructions burned: 637 (million)
% 2.60/0.67 % (3665777)------------------------------
% 2.60/0.67 % (3665777)------------------------------
% 2.60/0.67 % (3665778)Refutation not found, incomplete strategy
% 2.60/0.67 % (3665778)------------------------------
% 2.60/0.67 % (3665778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (3665778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (3665778)CaDiCaL version: 2.1.3
% 2.60/0.67 % (3665778)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.67 % (3665778)Time elapsed: 0.009 s
% 2.60/0.67 % (3665778)Peak memory usage: 12 MB
% 2.60/0.67 % (3665778)Instructions burned: 6 (million)
% 2.60/0.67 % (3665778)------------------------------
% 2.60/0.67 % (3665778)------------------------------
% 2.60/0.67 % (3665781)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=901518115:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 2.60/0.67 % (3665782)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2300770860:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 2.60/0.67 % (3665785)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.60/0.67 % (3665786)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3989733967:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 2.60/0.67 % (3665785)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2402127437:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 2.60/0.67 % (3665786)Refutation not found, incomplete strategy
% 2.60/0.67 % (3665786)------------------------------
% 2.60/0.67 % (3665786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.67 % (3665786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.67 % (3665786)CaDiCaL version: 2.1.3
% 2.60/0.67 % (3665786)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.67 % (3665786)Time elapsed: 0.004 s
% 2.60/0.67 % (3665786)Peak memory usage: 12 MB
% 2.60/0.67 % (3665786)Instructions burned: 5 (million)
% 2.60/0.67 % (3665781)Instruction limit reached!
% 2.60/0.67 % (3665781)------------------------------
% 2.85/0.76 % (3665781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.76 % (3665781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.76 % (3665781)CaDiCaL version: 2.1.3
% 2.85/0.76 % (3665781)Termination reason: Instruction limit
% 2.85/0.76 % (3665781)Termination phase: Saturation
% 2.85/0.76 % (3665781)Time elapsed: 0.017 s
% 2.85/0.76 % (3665781)Peak memory usage: 12 MB
% 2.85/0.76 % (3665781)Instructions burned: 34 (million)
% 2.85/0.76 % (3665786)------------------------------
% 2.85/0.76 % (3665786)------------------------------
% 2.85/0.76 % (3665787)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3532658001:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 2.85/0.76 % (3665792)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1853061343:i=427:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/427Mi)
% 2.85/0.76 % (3665793)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3606482491:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/874Mi)
% 2.85/0.76 % (3665782)Instruction limit reached!
% 2.85/0.76 % (3665782)------------------------------
% 2.85/0.76 % (3665782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.76 % (3665782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.76 % (3665782)CaDiCaL version: 2.1.3
% 2.85/0.76 % (3665782)Termination reason: Instruction limit
% 2.85/0.76 % (3665782)Termination phase: Saturation
% 2.85/0.76 % (3665782)Time elapsed: 0.035 s
% 2.85/0.76 % (3665782)Peak memory usage: 12 MB
% 2.85/0.76 % (3665782)Instructions burned: 69 (million)
% 2.85/0.76 % (3665770)Instruction limit reached!
% 2.85/0.76 % (3665770)------------------------------
% 2.85/0.76 % (3665770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.76 % (3665770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.76 % (3665770)CaDiCaL version: 2.1.3
% 2.85/0.76 % (3665770)Termination reason: Instruction limit
% 2.85/0.76 % (3665770)Termination phase: Saturation
% 2.85/0.76 % (3665770)Time elapsed: 0.094 s
% 2.85/0.76 % (3665770)Peak memory usage: 13 MB
% 2.85/0.76 % (3665770)Instructions burned: 201 (million)
% 2.85/0.76 % (3665793)Refutation not found, incomplete strategy
% 2.85/0.76 % (3665793)------------------------------
% 2.85/0.76 % (3665793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.76 % (3665793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.76 % (3665793)CaDiCaL version: 2.1.3
% 2.85/0.76 % (3665793)Termination reason: Refutation not found, incomplete strategy
% 2.85/0.76 % (3665793)Time elapsed: 0.004 s
% 2.85/0.76 % (3665793)Peak memory usage: 12 MB
% 2.85/0.76 % (3665793)Instructions burned: 5 (million)
% 2.85/0.76 % (3665793)------------------------------
% 2.85/0.76 % (3665793)------------------------------
% 2.85/0.76 % (3665787)Refutation not found, incomplete strategy
% 2.85/0.76 % (3665787)------------------------------
% 2.85/0.76 % (3665787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.85/0.76 % (3665787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.85/0.76 % (3665787)CaDiCaL version: 2.1.3
% 2.85/0.76 % (3665787)Termination reason: Refutation not found, incomplete strategy
% 2.85/0.76 % (3665787)Time elapsed: 0.011 s
% 2.85/0.76 % (3665787)Peak memory usage: 12 MB
% 2.85/0.76 % (3665787)Instructions burned: 9 (million)
% 2.85/0.76 % (3665787)------------------------------
% 2.85/0.76 % (3665787)------------------------------
% 2.85/0.76 % (3665797)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2945381012:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/515Mi)
% 2.85/0.76 % (3665798)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2328636800:st=1.5:i=130:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/130Mi)
% 2.85/0.76 % (3665799)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3066741783:i=44:ep=R:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/44Mi)
% 2.85/0.76 % (3665800)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2884164441:s2a=on:i=571:nm=16:rtra=on_2996 on theBenchmark for (2996ds/571Mi)
% 2.85/0.76 % (3665799)Refutation not found, incomplete strategy
% 2.85/0.76 % (3665799)------------------------------
% 2.85/0.76 % (3665799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.84 % (3665799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.84 % (3665799)CaDiCaL version: 2.1.3
% 3.16/0.84 % (3665799)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.84 % (3665799)Time elapsed: 0.004 s
% 3.16/0.84 % (3665799)Peak memory usage: 12 MB
% 3.16/0.84 % (3665799)Instructions burned: 6 (million)
% 3.16/0.84 % (3665798)Refutation not found, incomplete strategy
% 3.16/0.84 % (3665798)------------------------------
% 3.16/0.84 % (3665798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.84 % (3665798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.84 % (3665798)CaDiCaL version: 2.1.3
% 3.16/0.84 % (3665798)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.84 % (3665798)Time elapsed: 0.006 s
% 3.16/0.84 % (3665798)Peak memory usage: 12 MB
% 3.16/0.84 % (3665798)Instructions burned: 8 (million)
% 3.16/0.84 % (3665799)------------------------------
% 3.16/0.84 % (3665799)------------------------------
% 3.16/0.84 % (3665798)------------------------------
% 3.16/0.84 % (3665798)------------------------------
% 3.16/0.84 % (3665800)Refutation not found, incomplete strategy
% 3.16/0.84 % (3665800)------------------------------
% 3.16/0.84 % (3665800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.84 % (3665800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.84 % (3665800)CaDiCaL version: 2.1.3
% 3.16/0.84 % (3665800)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.84 % (3665800)Time elapsed: 0.002 s
% 3.16/0.84 % (3665800)Peak memory usage: 12 MB
% 3.16/0.84 % (3665800)Instructions burned: 1 (million)
% 3.16/0.84 % (3665800)------------------------------
% 3.16/0.84 % (3665800)------------------------------
% 3.16/0.84 % (3665805)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=145382267:i=450:rtra=on:ixr=off:ntd=on_2996 on theBenchmark for (2996ds/450Mi)
% 3.16/0.84 % (3665806)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=4125842982:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/95Mi)
% 3.16/0.84 % (3665805)Refutation not found, incomplete strategy
% 3.16/0.84 % (3665805)------------------------------
% 3.16/0.84 % (3665805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.84 % (3665805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.84 % (3665805)CaDiCaL version: 2.1.3
% 3.16/0.84 % (3665805)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.84 % (3665805)Time elapsed: 0.002 s
% 3.16/0.84 % (3665805)Peak memory usage: 12 MB
% 3.16/0.84 % (3665805)Instructions burned: 1 (million)
% 3.16/0.84 % (3665807)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=3357368624:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 3.16/0.84 % (3665805)------------------------------
% 3.16/0.84 % (3665805)------------------------------
% 3.16/0.84 % (3665807)Refutation not found, incomplete strategy
% 3.16/0.84 % (3665807)------------------------------
% 3.16/0.84 % (3665807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.84 % (3665807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.84 % (3665807)CaDiCaL version: 2.1.3
% 3.16/0.84 % (3665807)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.84 % (3665807)Time elapsed: 0.005 s
% 3.16/0.84 % (3665807)Peak memory usage: 12 MB
% 3.16/0.84 % (3665807)Instructions burned: 8 (million)
% 3.16/0.84 % (3665807)------------------------------
% 3.16/0.84 % (3665807)------------------------------
% 3.16/0.84 % (3665785)Instruction limit reached!
% 3.16/0.84 % (3665785)------------------------------
% 3.16/0.84 % (3665785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.84 % (3665785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.84 % (3665785)CaDiCaL version: 2.1.3
% 3.16/0.84 % (3665785)Termination reason: Instruction limit
% 3.16/0.84 % (3665785)Termination phase: Saturation
% 3.16/0.84 % (3665785)Time elapsed: 0.090 s
% 3.16/0.84 % (3665785)Peak memory usage: 14 MB
% 3.16/0.84 % (3665785)Instructions burned: 181 (million)
% 3.16/0.84 % (3665811)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=3355932815: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_2995 on theBenchmark for (2995ds/105Mi)
% 3.16/0.90 % (3665812)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=1946280695:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2995 on theBenchmark for (2995ds/5755Mi)
% 3.16/0.90 % (3665762)Instruction limit reached!
% 3.16/0.90 % (3665762)------------------------------
% 3.16/0.90 % (3665762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (3665762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (3665762)CaDiCaL version: 2.1.3
% 3.16/0.90 % (3665762)Termination reason: Instruction limit
% 3.16/0.90 % (3665762)Termination phase: Saturation
% 3.16/0.90 % (3665762)Time elapsed: 0.214 s
% 3.16/0.90 % (3665762)Peak memory usage: 22 MB
% 3.16/0.90 % (3665762)Instructions burned: 855 (million)
% 3.16/0.90 % (3665813)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2990437067:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/375Mi)
% 3.16/0.90 % (3665816)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=345950064:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/495Mi)
% 3.16/0.90 % (3665806)Instruction limit reached!
% 3.16/0.90 % (3665806)------------------------------
% 3.16/0.90 % (3665806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (3665806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (3665806)CaDiCaL version: 2.1.3
% 3.16/0.90 % (3665806)Termination reason: Instruction limit
% 3.16/0.90 % (3665806)Termination phase: Saturation
% 3.16/0.90 % (3665806)Time elapsed: 0.054 s
% 3.16/0.90 % (3665806)Peak memory usage: 12 MB
% 3.16/0.90 % (3665806)Instructions burned: 95 (million)
% 3.16/0.90 % (3665819)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=873877226:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.16/0.90 % (3665811)Instruction limit reached!
% 3.16/0.90 % (3665811)------------------------------
% 3.16/0.90 % (3665811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (3665811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (3665811)CaDiCaL version: 2.1.3
% 3.16/0.90 % (3665811)Termination reason: Instruction limit
% 3.16/0.90 % (3665811)Termination phase: Saturation
% 3.16/0.90 % (3665811)Time elapsed: 0.054 s
% 3.16/0.90 % (3665811)Peak memory usage: 13 MB
% 3.16/0.90 % (3665811)Instructions burned: 107 (million)
% 3.16/0.90 % (3665819)Instruction limit reached!
% 3.16/0.90 % (3665819)------------------------------
% 3.16/0.90 % (3665819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (3665819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (3665819)CaDiCaL version: 2.1.3
% 3.16/0.90 % (3665819)Termination reason: Instruction limit
% 3.16/0.90 % (3665819)Termination phase: Saturation
% 3.16/0.90 % (3665819)Time elapsed: 0.017 s
% 3.16/0.90 % (3665819)Peak memory usage: 12 MB
% 3.16/0.90 % (3665819)Instructions burned: 34 (million)
% 3.16/0.90 % (3665821)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3606877983:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/91Mi)
% 3.16/0.90 % (3665822)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2975197062:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2994 on theBenchmark for (2994ds/66Mi)
% 3.16/0.90 % (3665822)Refutation not found, incomplete strategy
% 3.16/0.90 % (3665822)------------------------------
% 3.16/0.90 % (3665822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.90 % (3665822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.90 % (3665822)CaDiCaL version: 2.1.3
% 3.16/0.90 % (3665822)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.90 % (3665822)Time elapsed: 0.002 s
% 3.16/0.90 % (3665822)Peak memory usage: 12 MB
% 3.16/0.90 % (3665822)Instructions burned: 1 (million)
% 3.16/0.90 % (3665822)------------------------------
% 3.16/0.90 % (3665822)------------------------------
% 3.98/0.95 % (3665825)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=366075795:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2994 on theBenchmark for (2994ds/22Mi)
% 3.98/0.95 % (3665821)Instruction limit reached!
% 3.98/0.95 % (3665821)------------------------------
% 3.98/0.95 % (3665821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.95 % (3665821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.95 % (3665821)CaDiCaL version: 2.1.3
% 3.98/0.95 % (3665821)Termination reason: Instruction limit
% 3.98/0.95 % (3665821)Termination phase: Saturation
% 3.98/0.95 % (3665821)Time elapsed: 0.046 s
% 3.98/0.95 % (3665821)Peak memory usage: 13 MB
% 3.98/0.95 % (3665821)Instructions burned: 93 (million)
% 3.98/0.95 % (3665825)Instruction limit reached!
% 3.98/0.95 % (3665825)------------------------------
% 3.98/0.95 % (3665825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.95 % (3665825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.95 % (3665825)CaDiCaL version: 2.1.3
% 3.98/0.95 % (3665825)Termination reason: Instruction limit
% 3.98/0.95 % (3665825)Termination phase: Saturation
% 3.98/0.95 % (3665825)Time elapsed: 0.012 s
% 3.98/0.95 % (3665825)Peak memory usage: 12 MB
% 3.98/0.95 % (3665825)Instructions burned: 22 (million)
% 3.98/0.95 % (3665827)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=1642915955:i=338:bd=all:ins=4:rtra=on_2994 on theBenchmark for (2994ds/338Mi)
% 3.98/0.95 % (3665828)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1327050267:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/28Mi)
% 3.98/0.95 % (3665792)Instruction limit reached!
% 3.98/0.95 % (3665792)------------------------------
% 3.98/0.95 % (3665792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.95 % (3665792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.95 % (3665792)CaDiCaL version: 2.1.3
% 3.98/0.95 % (3665792)Termination reason: Instruction limit
% 3.98/0.95 % (3665792)Termination phase: Saturation
% 3.98/0.95 % (3665792)Time elapsed: 0.214 s
% 3.98/0.95 % (3665792)Peak memory usage: 15 MB
% 3.98/0.95 % (3665792)Instructions burned: 428 (million)
% 3.98/0.95 % (3665816)Instruction limit reached!
% 3.98/0.95 % (3665816)------------------------------
% 3.98/0.95 % (3665816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.95 % (3665816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.95 % (3665816)CaDiCaL version: 2.1.3
% 3.98/0.95 % (3665816)Termination reason: Instruction limit
% 3.98/0.95 % (3665816)Termination phase: Saturation
% 3.98/0.95 % (3665816)Time elapsed: 0.127 s
% 3.98/0.95 % (3665816)Peak memory usage: 16 MB
% 3.98/0.95 % (3665816)Instructions burned: 498 (million)
% 3.98/0.95 % (3665828)Instruction limit reached!
% 3.98/0.95 % (3665828)------------------------------
% 3.98/0.95 % (3665828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.95 % (3665828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.95 % (3665828)CaDiCaL version: 2.1.3
% 3.98/0.95 % (3665828)Termination reason: Instruction limit
% 3.98/0.95 % (3665828)Termination phase: Saturation
% 3.98/0.95 % (3665828)Time elapsed: 0.015 s
% 3.98/0.95 % (3665828)Peak memory usage: 12 MB
% 3.98/0.95 % (3665828)Instructions burned: 28 (million)
% 3.98/0.95 % (3665832)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=1549786571:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2994 on theBenchmark for (2994ds/340Mi)
% 3.98/0.95 % (3665827)Refutation not found, incomplete strategy
% 3.98/0.95 % (3665827)------------------------------
% 3.98/0.95 % (3665827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.95 % (3665827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.95 % (3665827)CaDiCaL version: 2.1.3
% 3.98/0.95 % (3665827)Termination reason: Refutation not found, incomplete strategy
% 3.98/0.95 % (3665827)Time elapsed: 0.019 s
% 3.98/0.95 % (3665827)Peak memory usage: 13 MB
% 3.98/0.95 % (3665827)Instructions burned: 32 (million)
% 3.98/0.95 % (3665827)------------------------------
% 3.98/0.95 % (3665827)------------------------------
% 3.98/0.95 % (3665831)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 3.98/1.04 % (3665831)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2437678060:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2994 on theBenchmark for (2994ds/137Mi)
% 3.98/1.04 % (3665831)Refutation not found, incomplete strategy
% 3.98/1.04 % (3665831)------------------------------
% 3.98/1.04 % (3665831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/1.04 % (3665831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/1.04 % (3665831)CaDiCaL version: 2.1.3
% 3.98/1.04 % (3665831)Termination reason: Refutation not found, incomplete strategy
% 3.98/1.04 % (3665831)Time elapsed: 0.005 s
% 3.98/1.04 % (3665831)Peak memory usage: 12 MB
% 3.98/1.04 % (3665831)Instructions burned: 5 (million)
% 3.98/1.04 % (3665831)------------------------------
% 3.98/1.04 % (3665831)------------------------------
% 3.98/1.04 % (3665797)Instruction limit reached!
% 3.98/1.04 % (3665797)------------------------------
% 3.98/1.04 % (3665797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/1.04 % (3665797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/1.04 % (3665797)CaDiCaL version: 2.1.3
% 3.98/1.04 % (3665797)Termination reason: Instruction limit
% 3.98/1.04 % (3665797)Termination phase: Saturation
% 3.98/1.04 % (3665797)Time elapsed: 0.237 s
% 3.98/1.04 % (3665797)Peak memory usage: 15 MB
% 3.98/1.04 % (3665797)Instructions burned: 515 (million)
% 3.98/1.04 % (3665833)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=580490992:i=227:sd=1:bd=all:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/227Mi)
% 3.98/1.04 % (3665835)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 3.98/1.04 % (3665833)Refutation not found, incomplete strategy
% 3.98/1.04 % (3665833)------------------------------
% 3.98/1.04 % (3665833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/1.04 % (3665833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/1.04 % (3665833)CaDiCaL version: 2.1.3
% 3.98/1.04 % (3665833)Termination reason: Refutation not found, incomplete strategy
% 3.98/1.04 % (3665833)Time elapsed: 0.006 s
% 3.98/1.04 % (3665833)Peak memory usage: 12 MB
% 3.98/1.04 % (3665833)Instructions burned: 2 (million)
% 3.98/1.04 % (3665833)------------------------------
% 3.98/1.04 % (3665833)------------------------------
% 3.98/1.04 % (3665835)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1068586520:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/373Mi)
% 3.98/1.04 % (3665837)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2331033384:i=116:ep=RSTC:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/116Mi)
% 3.98/1.04 % (3665837)Refutation not found, incomplete strategy
% 3.98/1.04 % (3665837)------------------------------
% 3.98/1.04 % (3665837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/1.04 % (3665837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/1.04 % (3665837)CaDiCaL version: 2.1.3
% 3.98/1.04 % (3665837)Termination reason: Refutation not found, incomplete strategy
% 3.98/1.04 % (3665837)Time elapsed: 0.001 s
% 3.98/1.04 % (3665837)Peak memory usage: 12 MB
% 3.98/1.04 % (3665837)Instructions burned: 1 (million)
% 3.98/1.04 % (3665837)------------------------------
% 3.98/1.04 % (3665837)------------------------------
% 3.98/1.04 % (3665838)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1365701554:i=575:rtra=on_2993 on theBenchmark for (2993ds/575Mi)
% 3.98/1.04 % (3665838)Refutation not found, incomplete strategy
% 3.98/1.04 % (3665838)------------------------------
% 3.98/1.04 % (3665838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/1.04 % (3665838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/1.04 % (3665838)CaDiCaL version: 2.1.3
% 3.98/1.04 % (3665838)Termination reason: Refutation not found, incomplete strategy
% 3.98/1.04 % (3665838)Time elapsed: 0.003 s
% 3.98/1.04 % (3665838)Peak memory usage: 12 MB
% 3.98/1.04 % (3665838)Instructions burned: 3 (million)
% 3.98/1.04 % (3665838)------------------------------
% 3.98/1.04 % (3665838)------------------------------
% 3.98/1.04 % (3665845)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1920201189:i=421:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/421Mi)
% 5.62/1.12 % (3665845)Refutation not found, incomplete strategy
% 5.62/1.12 % (3665845)------------------------------
% 5.62/1.12 % (3665845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.12 % (3665845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.12 % (3665845)CaDiCaL version: 2.1.3
% 5.62/1.12 % (3665845)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.12 % (3665845)Time elapsed: 0.002 s
% 5.62/1.12 % (3665845)Peak memory usage: 12 MB
% 5.62/1.12 % (3665845)Instructions burned: 2 (million)
% 5.62/1.12 % (3665840)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1833243755:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2993 on theBenchmark for (2993ds/270Mi)
% 5.62/1.12 % (3665845)------------------------------
% 5.62/1.12 % (3665845)------------------------------
% 5.62/1.12 % (3665844)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=4283710996: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_2993 on theBenchmark for (2993ds/9840Mi)
% 5.62/1.12 % (3665832)Instruction limit reached!
% 5.62/1.12 % (3665832)------------------------------
% 5.62/1.12 % (3665832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.12 % (3665848)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.62/1.12 % (3665832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.12 % (3665832)CaDiCaL version: 2.1.3
% 5.62/1.12 % (3665832)Termination reason: Instruction limit
% 5.62/1.12 % (3665832)Termination phase: Saturation
% 5.62/1.12 % (3665832)Time elapsed: 0.087 s
% 5.62/1.12 % (3665832)Peak memory usage: 12 MB
% 5.62/1.12 % (3665832)Instructions burned: 344 (million)
% 5.62/1.12 % (3665848)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=750931678:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/270Mi)
% 5.62/1.12 % (3665848)Refutation not found, incomplete strategy
% 5.62/1.12 % (3665848)------------------------------
% 5.62/1.12 % (3665848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.12 % (3665848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.12 % (3665848)CaDiCaL version: 2.1.3
% 5.62/1.12 % (3665848)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.12 % (3665848)Time elapsed: 0.003 s
% 5.62/1.12 % (3665848)Peak memory usage: 12 MB
% 5.62/1.12 % (3665848)Instructions burned: 4 (million)
% 5.62/1.12 % (3665848)------------------------------
% 5.62/1.12 % (3665848)------------------------------
% 5.62/1.12 % (3665850)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2693222911:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 5.62/1.12 % (3665850)Refutation not found, incomplete strategy
% 5.62/1.12 % (3665850)------------------------------
% 5.62/1.12 % (3665850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.12 % (3665850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.12 % (3665850)CaDiCaL version: 2.1.3
% 5.62/1.12 % (3665850)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.12 % (3665850)Time elapsed: 0.001 s
% 5.62/1.12 % (3665850)Peak memory usage: 12 MB
% 5.62/1.12 % (3665850)Instructions burned: 4 (million)
% 5.62/1.12 % (3665850)------------------------------
% 5.62/1.12 % (3665850)------------------------------
% 5.62/1.12 % (3665854)dis+10_2_sil=128000:si=on:random_seed=90287464:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2993 on theBenchmark for (2993ds/339Mi)
% 5.62/1.12 % (3665852)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 5.62/1.12 % (3665852)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.62/1.12 % (3665813)Instruction limit reached!
% 5.62/1.16 % (3665813)------------------------------
% 5.62/1.16 % (3665813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.16 % (3665813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.16 % (3665813)CaDiCaL version: 2.1.3
% 5.62/1.16 % (3665813)Termination reason: Instruction limit
% 5.62/1.16 % (3665813)Termination phase: Saturation
% 5.62/1.16 % (3665813)Time elapsed: 0.254 s
% 5.62/1.16 % (3665813)Peak memory usage: 14 MB
% 5.62/1.16 % (3665813)Instructions burned: 377 (million)
% 5.62/1.16 % (3665852)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=4093040329:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2993 on theBenchmark for (2993ds/1440Mi)
% 5.62/1.16 % (3665852)Refutation not found, incomplete strategy
% 5.62/1.16 % (3665852)------------------------------
% 5.62/1.16 % (3665852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.16 % (3665852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.16 % (3665852)CaDiCaL version: 2.1.3
% 5.62/1.16 % (3665852)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.16 % (3665852)Time elapsed: 0.003 s
% 5.62/1.16 % (3665852)Peak memory usage: 12 MB
% 5.62/1.16 % (3665852)Instructions burned: 4 (million)
% 5.62/1.16 % (3665852)------------------------------
% 5.62/1.16 % (3665852)------------------------------
% 5.62/1.16 % (3665856)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1302149362:i=111:add=on:fgj=on:rtra=on:fdi=1024_2992 on theBenchmark for (2992ds/111Mi)
% 5.62/1.16 % (3665858)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=2119509715:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2992 on theBenchmark for (2992ds/122Mi)
% 5.62/1.16 % (3665858)Refutation not found, incomplete strategy
% 5.62/1.16 % (3665858)------------------------------
% 5.62/1.16 % (3665858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.16 % (3665858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.16 % (3665858)CaDiCaL version: 2.1.3
% 5.62/1.16 % (3665858)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.16 % (3665858)Time elapsed: 0.002 s
% 5.62/1.16 % (3665858)Peak memory usage: 12 MB
% 5.62/1.16 % (3665858)Instructions burned: 2 (million)
% 5.62/1.16 % (3665856)Refutation not found, incomplete strategy
% 5.62/1.16 % (3665856)------------------------------
% 5.62/1.16 % (3665856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.16 % (3665856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.16 % (3665856)CaDiCaL version: 2.1.3
% 5.62/1.16 % (3665856)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.16 % (3665856)Time elapsed: 0.006 s
% 5.62/1.16 % (3665856)Peak memory usage: 12 MB
% 5.62/1.16 % (3665856)Instructions burned: 4 (million)
% 5.62/1.16 % (3665858)------------------------------
% 5.62/1.16 % (3665858)------------------------------
% 5.62/1.16 % (3665856)------------------------------
% 5.62/1.16 % (3665856)------------------------------
% 5.62/1.16 % (3665862)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3450033269:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2992 on theBenchmark for (2992ds/232Mi)
% 5.62/1.16 % (3665861)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=1119319349:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/136Mi)
% 5.62/1.16 % (3665854)Instruction limit reached!
% 5.62/1.16 % (3665854)------------------------------
% 5.62/1.16 % (3665854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.16 % (3665854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.16 % (3665854)CaDiCaL version: 2.1.3
% 5.62/1.16 % (3665854)Termination reason: Instruction limit
% 5.62/1.16 % (3665854)Termination phase: Saturation
% 5.62/1.16 % (3665854)Time elapsed: 0.087 s
% 5.62/1.16 % (3665854)Peak memory usage: 13 MB
% 5.62/1.16 % (3665854)Instructions burned: 342 (million)
% 5.62/1.16 % (3665865)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=762109116:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2992 on theBenchmark for (2992ds/1254Mi)
% 6.41/1.22 % (3665865)Refutation not found, incomplete strategy
% 6.41/1.22 % (3665865)------------------------------
% 6.41/1.22 % (3665865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.22 % (3665865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.22 % (3665865)CaDiCaL version: 2.1.3
% 6.41/1.22 % (3665865)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.22 % (3665865)Time elapsed: 0.002 s
% 6.41/1.22 % (3665865)Peak memory usage: 12 MB
% 6.41/1.22 % (3665865)Instructions burned: 5 (million)
% 6.41/1.22 % (3665865)------------------------------
% 6.41/1.22 % (3665865)------------------------------
% 6.41/1.22 % (3665835)Instruction limit reached!
% 6.41/1.22 % (3665835)------------------------------
% 6.41/1.22 % (3665835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.22 % (3665835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.22 % (3665835)CaDiCaL version: 2.1.3
% 6.41/1.22 % (3665835)Termination reason: Instruction limit
% 6.41/1.22 % (3665835)Termination phase: Saturation
% 6.41/1.22 % (3665835)Time elapsed: 0.173 s
% 6.41/1.22 % (3665835)Peak memory usage: 15 MB
% 6.41/1.22 % (3665835)Instructions burned: 374 (million)
% 6.41/1.22 % (3665867)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 6.41/1.22 % (3665867)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=2898454086:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2991 on theBenchmark for (2991ds/281Mi)
% 6.41/1.22 % (3665868)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3866098555:i=619:add=on:rtra=on_2991 on theBenchmark for (2991ds/619Mi)
% 6.41/1.22 % (3665868)Refutation not found, incomplete strategy
% 6.41/1.22 % (3665868)------------------------------
% 6.41/1.22 % (3665868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.22 % (3665868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.22 % (3665868)CaDiCaL version: 2.1.3
% 6.41/1.22 % (3665868)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.22 % (3665868)Time elapsed: 0.003 s
% 6.41/1.22 % (3665868)Peak memory usage: 12 MB
% 6.41/1.22 % (3665868)Instructions burned: 3 (million)
% 6.41/1.22 % (3665868)------------------------------
% 6.41/1.22 % (3665868)------------------------------
% 6.41/1.22 % (3665840)Instruction limit reached!
% 6.41/1.22 % (3665840)------------------------------
% 6.41/1.22 % (3665840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.22 % (3665840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.22 % (3665840)CaDiCaL version: 2.1.3
% 6.41/1.22 % (3665840)Termination reason: Instruction limit
% 6.41/1.22 % (3665840)Termination phase: Saturation
% 6.41/1.22 % (3665840)Time elapsed: 0.190 s
% 6.41/1.22 % (3665840)Peak memory usage: 13 MB
% 6.41/1.22 % (3665840)Instructions burned: 270 (million)
% 6.41/1.22 % (3665871)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=2899520290:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/865Mi)
% 6.41/1.22 % (3665872)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2710982033:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/212Mi)
% 6.41/1.22 % (3665862)Instruction limit reached!
% 6.41/1.22 % (3665862)------------------------------
% 6.41/1.22 % (3665862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.22 % (3665862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.22 % (3665862)CaDiCaL version: 2.1.3
% 6.41/1.22 % (3665862)Termination reason: Instruction limit
% 6.41/1.22 % (3665862)Termination phase: Saturation
% 6.41/1.22 % (3665862)Time elapsed: 0.108 s
% 6.41/1.22 % (3665862)Peak memory usage: 12 MB
% 6.41/1.22 % (3665862)Instructions burned: 232 (million)
% 6.41/1.22 % (3665871)Refutation not found, incomplete strategy
% 6.41/1.22 % (3665871)------------------------------
% 6.41/1.22 % (3665871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.22 % (3665871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.22 % (3665871)CaDiCaL version: 2.1.3
% 6.41/1.22 % (3665871)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.26 % (3665871)Time elapsed: 0.022 s
% 6.41/1.26 % (3665871)Peak memory usage: 12 MB
% 6.41/1.26 % (3665871)Instructions burned: 37 (million)
% 6.41/1.26 % (3665871)------------------------------
% 6.41/1.26 % (3665871)------------------------------
% 6.41/1.26 % (3665861)Instruction limit reached!
% 6.41/1.26 % (3665861)------------------------------
% 6.41/1.26 % (3665861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.26 % (3665861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.26 % (3665861)CaDiCaL version: 2.1.3
% 6.41/1.26 % (3665861)Termination reason: Instruction limit
% 6.41/1.26 % (3665861)Termination phase: Saturation
% 6.41/1.26 % (3665861)Time elapsed: 0.111 s
% 6.41/1.26 % (3665861)Peak memory usage: 13 MB
% 6.41/1.26 % (3665861)Instructions burned: 136 (million)
% 6.41/1.26 % (3665867)Instruction limit reached!
% 6.41/1.26 % (3665867)------------------------------
% 6.41/1.26 % (3665867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.26 % (3665867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.26 % (3665867)CaDiCaL version: 2.1.3
% 6.41/1.26 % (3665867)Termination reason: Instruction limit
% 6.41/1.26 % (3665867)Termination phase: Saturation
% 6.41/1.26 % (3665867)Time elapsed: 0.076 s
% 6.41/1.26 % (3665867)Peak memory usage: 13 MB
% 6.41/1.26 % (3665867)Instructions burned: 283 (million)
% 6.41/1.26 % (3665875)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=4080964488:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 6.41/1.26 % (3665875)Refutation not found, incomplete strategy
% 6.41/1.26 % (3665875)------------------------------
% 6.41/1.26 % (3665875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.26 % (3665875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.26 % (3665875)CaDiCaL version: 2.1.3
% 6.41/1.26 % (3665875)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.26 % (3665875)Time elapsed: 0.004 s
% 6.41/1.26 % (3665875)Peak memory usage: 12 MB
% 6.41/1.26 % (3665875)Instructions burned: 5 (million)
% 6.41/1.26 % (3665876)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2063022467:st=1.5:i=346:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/346Mi)
% 6.41/1.26 % (3665875)------------------------------
% 6.41/1.26 % (3665875)------------------------------
% 6.41/1.26 % (3665877)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=176003223:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/152Mi)
% 6.41/1.26 % (3665879)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3506874138:i=75:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/75Mi)
% 6.41/1.26 % (3665876)Refutation not found, incomplete strategy
% 6.41/1.26 % (3665876)------------------------------
% 6.41/1.26 % (3665876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.26 % (3665876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.26 % (3665876)CaDiCaL version: 2.1.3
% 6.41/1.26 % (3665876)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.26 % (3665876)Time elapsed: 0.005 s
% 6.41/1.26 % (3665876)Peak memory usage: 12 MB
% 6.41/1.26 % (3665876)Instructions burned: 8 (million)
% 6.41/1.26 % (3665879)Refutation not found, incomplete strategy
% 6.41/1.26 % (3665879)------------------------------
% 6.41/1.26 % (3665879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.26 % (3665879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.26 % (3665879)CaDiCaL version: 2.1.3
% 6.41/1.26 % (3665879)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.26 % (3665879)Time elapsed: 0.002 s
% 6.41/1.26 % (3665879)Peak memory usage: 12 MB
% 6.41/1.26 % (3665879)Instructions burned: 6 (million)
% 6.41/1.26 % (3665876)------------------------------
% 6.41/1.26 % (3665876)------------------------------
% 6.41/1.26 % (3665879)------------------------------
% 6.41/1.26 % (3665879)------------------------------
% 6.41/1.26 % (3665884)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=160752423:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2990 on theBenchmark for (2990ds/148Mi)
% 6.41/1.26 % (3665881)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=998981323:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/387Mi)
% 6.41/1.29 % (3665881)Refutation not found, incomplete strategy
% 6.41/1.29 % (3665881)------------------------------
% 6.41/1.29 % (3665881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.29 % (3665881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.29 % (3665881)CaDiCaL version: 2.1.3
% 6.41/1.29 % (3665881)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.29 % (3665881)Time elapsed: 0.007 s
% 6.41/1.29 % (3665881)Peak memory usage: 12 MB
% 6.41/1.29 % (3665881)Instructions burned: 10 (million)
% 6.41/1.29 % (3665885)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1928276992:i=161:piset=and:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/161Mi)
% 6.41/1.29 % (3665881)------------------------------
% 6.41/1.29 % (3665881)------------------------------
% 6.41/1.29 % (3665889)lrs+10_1_sil=128000:si=on:random_seed=2864184223:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/888Mi)
% 6.41/1.29 % (3665884)Instruction limit reached!
% 6.41/1.29 % (3665884)------------------------------
% 6.41/1.29 % (3665884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.29 % (3665884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.29 % (3665884)CaDiCaL version: 2.1.3
% 6.41/1.29 % (3665884)Termination reason: Instruction limit
% 6.41/1.29 % (3665884)Termination phase: Saturation
% 6.41/1.29 % (3665884)Time elapsed: 0.038 s
% 6.41/1.29 % (3665884)Peak memory usage: 14 MB
% 6.41/1.29 % (3665884)Instructions burned: 151 (million)
% 6.41/1.29 % (3665891)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=3701650900:i=136:add=on:ins=4:rtra=on:sup=off_2990 on theBenchmark for (2990ds/136Mi)
% 6.41/1.29 % (3665891)Refutation not found, incomplete strategy
% 6.41/1.29 % (3665891)------------------------------
% 6.41/1.29 % (3665891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.29 % (3665891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.29 % (3665891)CaDiCaL version: 2.1.3
% 6.41/1.29 % (3665891)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.29 % (3665891)Time elapsed: 0.001 s
% 6.41/1.29 % (3665891)Peak memory usage: 12 MB
% 6.41/1.29 % (3665891)Instructions burned: 2 (million)
% 6.41/1.29 % (3665891)------------------------------
% 6.41/1.29 % (3665891)------------------------------
% 6.41/1.29 % (3665877)Instruction limit reached!
% 6.41/1.29 % (3665877)------------------------------
% 6.41/1.29 % (3665877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.29 % (3665877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.29 % (3665877)CaDiCaL version: 2.1.3
% 6.41/1.29 % (3665877)Termination reason: Instruction limit
% 6.41/1.29 % (3665877)Termination phase: Saturation
% 6.41/1.29 % (3665877)Time elapsed: 0.074 s
% 6.41/1.29 % (3665877)Peak memory usage: 13 MB
% 6.41/1.29 % (3665877)Instructions burned: 153 (million)
% 6.41/1.29 % (3665893)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=4239498850:i=88:s2at=3:nm=2:rtra=on:rawr=on_2990 on theBenchmark for (2990ds/88Mi)
% 6.41/1.29 % (3665893)Refutation not found, incomplete strategy
% 6.41/1.29 % (3665893)------------------------------
% 6.41/1.29 % (3665893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.29 % (3665893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.29 % (3665893)CaDiCaL version: 2.1.3
% 6.41/1.29 % (3665893)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.29 % (3665893)Time elapsed: 0.002 s
% 6.41/1.29 % (3665893)Peak memory usage: 12 MB
% 6.41/1.29 % (3665893)Instructions burned: 5 (million)
% 6.41/1.29 % (3665893)------------------------------
% 6.41/1.29 % (3665893)------------------------------
% 6.41/1.29 % (3665872)Instruction limit reached!
% 6.41/1.29 % (3665872)------------------------------
% 6.41/1.29 % (3665872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.29 % (3665872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.29 % (3665872)CaDiCaL version: 2.1.3
% 6.41/1.29 % (3665872)Termination reason: Instruction limit
% 6.41/1.29 % (3665872)Termination phase: Saturation
% 6.41/1.29 % (3665872)Time elapsed: 0.106 s
% 6.41/1.29 % (3665872)Peak memory usage: 14 MB
% 7.12/1.38 % (3665872)Instructions burned: 212 (million)
% 7.12/1.38 % (3665896)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=730424996:i=2186:rtra=on:ixr=off_2990 on theBenchmark for (2990ds/2186Mi)
% 7.12/1.38 % (3665896)Refutation not found, incomplete strategy
% 7.12/1.38 % (3665896)------------------------------
% 7.12/1.38 % (3665896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.12/1.38 % (3665896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/1.38 % (3665896)CaDiCaL version: 2.1.3
% 7.12/1.38 % (3665896)Termination reason: Refutation not found, incomplete strategy
% 7.12/1.38 % (3665896)Time elapsed: 0.003 s
% 7.12/1.38 % (3665896)Peak memory usage: 12 MB
% 7.12/1.38 % (3665896)Instructions burned: 9 (million)
% 7.12/1.38 % (3665896)------------------------------
% 7.12/1.38 % (3665896)------------------------------
% 7.12/1.38 % (3665894)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=1836529624:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2990 on theBenchmark for (2990ds/93Mi)
% 7.12/1.38 % (3665897)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3696867388:s2a=on:i=240:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/240Mi)
% 7.12/1.38 % (3665897)Refutation not found, incomplete strategy
% 7.12/1.38 % (3665897)------------------------------
% 7.12/1.38 % (3665897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.12/1.38 % (3665897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/1.38 % (3665897)CaDiCaL version: 2.1.3
% 7.12/1.38 % (3665897)Termination reason: Refutation not found, incomplete strategy
% 7.12/1.38 % (3665897)Time elapsed: 0.004 s
% 7.12/1.38 % (3665897)Peak memory usage: 12 MB
% 7.12/1.38 % (3665897)Instructions burned: 6 (million)
% 7.12/1.38 % (3665897)------------------------------
% 7.12/1.38 % (3665897)------------------------------
% 7.12/1.38 % (3665899)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2157071086:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/805Mi)
% 7.12/1.38 % (3665885)Instruction limit reached!
% 7.12/1.38 % (3665885)------------------------------
% 7.12/1.38 % (3665885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.12/1.38 % (3665885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/1.38 % (3665885)CaDiCaL version: 2.1.3
% 7.12/1.38 % (3665885)Termination reason: Instruction limit
% 7.12/1.38 % (3665885)Termination phase: Saturation
% 7.12/1.38 % (3665885)Time elapsed: 0.082 s
% 7.12/1.38 % (3665885)Peak memory usage: 13 MB
% 7.12/1.38 % (3665885)Instructions burned: 162 (million)
% 7.12/1.38 % (3665899)Refutation not found, incomplete strategy
% 7.12/1.38 % (3665899)------------------------------
% 7.12/1.38 % (3665899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.12/1.38 % (3665899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/1.38 % (3665899)CaDiCaL version: 2.1.3
% 7.12/1.38 % (3665899)Termination reason: Refutation not found, incomplete strategy
% 7.12/1.38 % (3665899)Time elapsed: 0.001 s
% 7.12/1.38 % (3665899)Peak memory usage: 12 MB
% 7.12/1.38 % (3665899)Instructions burned: 3 (million)
% 7.12/1.38 % (3665899)------------------------------
% 7.12/1.38 % (3665899)------------------------------
% 7.12/1.38 % (3665905)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=2175886602:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/314Mi)
% 7.12/1.38 % (3665903)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 7.12/1.38 % (3665905)Refutation not found, incomplete strategy
% 7.12/1.38 % (3665905)------------------------------
% 7.12/1.38 % (3665905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.12/1.38 % (3665905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/1.38 % (3665905)CaDiCaL version: 2.1.3
% 7.12/1.38 % (3665905)Termination reason: Refutation not found, incomplete strategy
% 7.12/1.38 % (3665905)Time elapsed: 0.002 s
% 7.12/1.38 % (3665905)Peak memory usage: 12 MB
% 7.12/1.38 % (3665905)Instructions burned: 4 (million)
% 7.12/1.38 % (3665905)------------------------------
% 7.12/1.38 % (3665905)------------------------------
% 7.12/1.38 % (3665903)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=760984920:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2989 on theBenchmark for (2989ds/391Mi)
% 7.96/1.51 % (3665904)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=253921864:i=355:av=off:fsr=off:rtra=on:ixr=off_2989 on theBenchmark for (2989ds/355Mi)
% 7.96/1.51 % (3665903)Refutation not found, incomplete strategy
% 7.96/1.51 % (3665903)------------------------------
% 7.96/1.51 % (3665903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.51 % (3665903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.51 % (3665903)CaDiCaL version: 2.1.3
% 7.96/1.51 % (3665903)Termination reason: Refutation not found, incomplete strategy
% 7.96/1.51 % (3665903)Time elapsed: 0.003 s
% 7.96/1.51 % (3665903)Peak memory usage: 12 MB
% 7.96/1.51 % (3665903)Instructions burned: 3 (million)
% 7.96/1.51 % (3665903)------------------------------
% 7.96/1.51 % (3665903)------------------------------
% 7.96/1.51 % (3665907)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=2974469873:s2a=on:i=251:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/251Mi)
% 7.96/1.51 % (3665904)Refutation not found, incomplete strategy
% 7.96/1.51 % (3665904)------------------------------
% 7.96/1.51 % (3665904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.51 % (3665904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.51 % (3665904)CaDiCaL version: 2.1.3
% 7.96/1.51 % (3665904)Termination reason: Refutation not found, incomplete strategy
% 7.96/1.51 % (3665904)Time elapsed: 0.006 s
% 7.96/1.51 % (3665904)Peak memory usage: 12 MB
% 7.96/1.51 % (3665904)Instructions burned: 8 (million)
% 7.96/1.51 % (3665904)------------------------------
% 7.96/1.51 % (3665904)------------------------------
% 7.96/1.51 % (3665907)Refutation not found, incomplete strategy
% 7.96/1.51 % (3665907)------------------------------
% 7.96/1.51 % (3665907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.51 % (3665907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.51 % (3665907)CaDiCaL version: 2.1.3
% 7.96/1.51 % (3665907)Termination reason: Refutation not found, incomplete strategy
% 7.96/1.51 % (3665907)Time elapsed: 0.001 s
% 7.96/1.51 % (3665907)Peak memory usage: 12 MB
% 7.96/1.51 % (3665907)Instructions burned: 4 (million)
% 7.96/1.51 % (3665907)------------------------------
% 7.96/1.51 % (3665907)------------------------------
% 7.96/1.51 % (3665913)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3033597483:i=116:ep=RSTC:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/116Mi)
% 7.96/1.51 % (3665913)Refutation not found, incomplete strategy
% 7.96/1.51 % (3665913)------------------------------
% 7.96/1.51 % (3665913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.51 % (3665913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.51 % (3665913)CaDiCaL version: 2.1.3
% 7.96/1.51 % (3665913)Termination reason: Refutation not found, incomplete strategy
% 7.96/1.51 % (3665913)Time elapsed: 0.001 s
% 7.96/1.51 % (3665913)Peak memory usage: 12 MB
% 7.96/1.51 % (3665913)Instructions burned: 1 (million)
% 7.96/1.51 % (3665913)------------------------------
% 7.96/1.51 % (3665913)------------------------------
% 7.96/1.51 % (3665910)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=48046410: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_2989 on theBenchmark for (2989ds/2470Mi)
% 7.96/1.51 % (3665912)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=978116714:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2989 on theBenchmark for (2989ds/673Mi)
% 7.96/1.51 % (3665912)Refutation not found, incomplete strategy
% 7.96/1.51 % (3665912)------------------------------
% 7.96/1.51 % (3665912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.51 % (3665912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.51 % (3665912)CaDiCaL version: 2.1.3
% 7.96/1.51 % (3665912)Termination reason: Refutation not found, incomplete strategy
% 7.96/1.51 % (3665912)Time elapsed: 0.002 s
% 8.58/1.63 % (3665912)Peak memory usage: 12 MB
% 8.58/1.63 % (3665912)Instructions burned: 2 (million)
% 8.58/1.63 % (3665912)------------------------------
% 8.58/1.63 % (3665912)------------------------------
% 8.58/1.63 % (3665915)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4170140743:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.58/1.63 % (3665894)Instruction limit reached!
% 8.58/1.63 % (3665894)------------------------------
% 8.58/1.63 % (3665894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.58/1.63 % (3665894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.58/1.63 % (3665894)CaDiCaL version: 2.1.3
% 8.58/1.63 % (3665894)Termination reason: Instruction limit
% 8.58/1.63 % (3665894)Termination phase: Saturation
% 8.58/1.63 % (3665894)Time elapsed: 0.062 s
% 8.58/1.63 % (3665894)Peak memory usage: 12 MB
% 8.58/1.63 % (3665894)Instructions burned: 93 (million)
% 8.58/1.63 % (3665918)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=2400187638: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_2989 on theBenchmark for (2989ds/30Mi)
% 8.58/1.63 % (3665920)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 8.58/1.63 % (3665920)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=128699598:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2989 on theBenchmark for (2989ds/39Mi)
% 8.58/1.63 % (3665918)Instruction limit reached!
% 8.58/1.63 % (3665918)------------------------------
% 8.58/1.63 % (3665918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.58/1.63 % (3665918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.58/1.63 % (3665918)CaDiCaL version: 2.1.3
% 8.58/1.63 % (3665918)Termination reason: Instruction limit
% 8.58/1.63 % (3665918)Termination phase: Saturation
% 8.58/1.63 % (3665918)Time elapsed: 0.018 s
% 8.58/1.63 % (3665918)Peak memory usage: 12 MB
% 8.58/1.63 % (3665918)Instructions burned: 30 (million)
% 8.58/1.63 % (3665920)Instruction limit reached!
% 8.58/1.63 % (3665920)------------------------------
% 8.58/1.63 % (3665920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.58/1.63 % (3665920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.58/1.63 % (3665920)CaDiCaL version: 2.1.3
% 8.58/1.63 % (3665920)Termination reason: Instruction limit
% 8.58/1.63 % (3665920)Termination phase: Saturation
% 8.58/1.63 % (3665920)Time elapsed: 0.021 s
% 8.58/1.63 % (3665920)Peak memory usage: 12 MB
% 8.58/1.63 % (3665920)Instructions burned: 39 (million)
% 8.58/1.63 % (3665923)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1529348115:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/365Mi)
% 8.58/1.63 % (3665924)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=324170888:i=158:av=off:rtra=on_2988 on theBenchmark for (2988ds/158Mi)
% 8.58/1.63 % (3665915)Instruction limit reached!
% 8.58/1.63 % (3665915)------------------------------
% 8.58/1.63 % (3665915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.58/1.63 % (3665915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.58/1.63 % (3665915)CaDiCaL version: 2.1.3
% 8.58/1.63 % (3665915)Termination reason: Instruction limit
% 8.58/1.63 % (3665915)Termination phase: Saturation
% 8.58/1.63 % (3665915)Time elapsed: 0.068 s
% 8.58/1.63 % (3665915)Peak memory usage: 13 MB
% 8.58/1.63 % (3665915)Instructions burned: 274 (million)
% 8.58/1.63 % (3665927)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
% 8.58/1.63 % (3665927)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=1033055125:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/252Mi)
% 8.58/1.63 % (3665927)Refutation not found, incomplete strategy
% 8.58/1.63 % (3665927)------------------------------
% 8.58/1.63 % (3665927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.58/1.63 % (3665927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/1.80 % (3665927)CaDiCaL version: 2.1.3
% 9.37/1.80 % (3665927)Termination reason: Refutation not found, incomplete strategy
% 9.37/1.80 % (3665927)Time elapsed: 0.002 s
% 9.37/1.80 % (3665927)Peak memory usage: 12 MB
% 9.37/1.80 % (3665927)Instructions burned: 4 (million)
% 9.37/1.80 % (3665927)------------------------------
% 9.37/1.80 % (3665927)------------------------------
% 9.37/1.80 % (3665929)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=1377779553:i=213:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/213Mi)
% 9.37/1.80 % (3665929)Refutation not found, incomplete strategy
% 9.37/1.80 % (3665929)------------------------------
% 9.37/1.80 % (3665929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.37/1.80 % (3665929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/1.80 % (3665929)CaDiCaL version: 2.1.3
% 9.37/1.80 % (3665929)Termination reason: Refutation not found, incomplete strategy
% 9.37/1.80 % (3665929)Time elapsed: 0.001 s
% 9.37/1.80 % (3665929)Peak memory usage: 12 MB
% 9.37/1.80 % (3665929)Instructions burned: 2 (million)
% 10.04/1.80 % (3665929)------------------------------
% 10.04/1.80 % (3665929)------------------------------
% 10.04/1.80 % (3665931)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=4140167044:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2988 on theBenchmark for (2988ds/160Mi)
% 10.04/1.80 % (3665931)Refutation not found, incomplete strategy
% 10.04/1.80 % (3665931)------------------------------
% 10.04/1.80 % (3665931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.80 % (3665931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.80 % (3665931)CaDiCaL version: 2.1.3
% 10.04/1.80 % (3665931)Termination reason: Refutation not found, incomplete strategy
% 10.04/1.80 % (3665931)Time elapsed: 0.002 s
% 10.04/1.80 % (3665931)Peak memory usage: 12 MB
% 10.04/1.80 % (3665931)Instructions burned: 5 (million)
% 10.04/1.80 % (3665931)------------------------------
% 10.04/1.80 % (3665931)------------------------------
% 10.04/1.80 % (3665933)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=3949622815:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/763Mi)
% 10.04/1.80 % (3665924)Instruction limit reached!
% 10.04/1.80 % (3665924)------------------------------
% 10.04/1.80 % (3665924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.80 % (3665924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.80 % (3665924)CaDiCaL version: 2.1.3
% 10.04/1.80 % (3665924)Termination reason: Instruction limit
% 10.04/1.80 % (3665924)Termination phase: Saturation
% 10.04/1.80 % (3665924)Time elapsed: 0.092 s
% 10.04/1.80 % (3665924)Peak memory usage: 12 MB
% 10.04/1.80 % (3665924)Instructions burned: 160 (million)
% 10.04/1.80 % (3665935)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 10.04/1.80 % (3665935)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=3953650425:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2987 on theBenchmark for (2987ds/237Mi)
% 10.04/1.80 % (3665935)Refutation not found, incomplete strategy
% 10.04/1.80 % (3665935)------------------------------
% 10.04/1.80 % (3665935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.80 % (3665935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.80 % (3665935)CaDiCaL version: 2.1.3
% 10.04/1.80 % (3665935)Termination reason: Refutation not found, incomplete strategy
% 10.04/1.80 % (3665935)Time elapsed: 0.005 s
% 10.04/1.80 % (3665935)Peak memory usage: 12 MB
% 10.04/1.80 % (3665935)Instructions burned: 3 (million)
% 10.04/1.80 % (3665935)------------------------------
% 10.04/1.80 % (3665935)------------------------------
% 10.04/1.80 % (3665937)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=228273391:s2a=on:i=386:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/386Mi)
% 10.04/1.80 % (3665937)Refutation not found, incomplete strategy
% 10.04/1.80 % (3665937)------------------------------
% 10.04/1.80 % (3665937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.80 % (3665937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.85 % (3665937)CaDiCaL version: 2.1.3
% 10.04/1.85 % (3665937)Termination reason: Refutation not found, incomplete strategy
% 10.04/1.85 % (3665937)Time elapsed: 0.004 s
% 10.04/1.85 % (3665937)Peak memory usage: 12 MB
% 10.04/1.85 % (3665937)Instructions burned: 3 (million)
% 10.04/1.85 % (3665937)------------------------------
% 10.04/1.85 % (3665937)------------------------------
% 10.04/1.85 % (3665923)Instruction limit reached!
% 10.04/1.85 % (3665923)------------------------------
% 10.04/1.85 % (3665923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.85 % (3665923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.85 % (3665923)CaDiCaL version: 2.1.3
% 10.04/1.85 % (3665923)Termination reason: Instruction limit
% 10.04/1.85 % (3665923)Termination phase: Saturation
% 10.04/1.85 % (3665923)Time elapsed: 0.188 s
% 10.04/1.85 % (3665923)Peak memory usage: 14 MB
% 10.04/1.85 % (3665923)Instructions burned: 366 (million)
% 10.04/1.85 % (3665939)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=195382780:i=300:piset=and:nm=32:rtra=on_2987 on theBenchmark for (2987ds/300Mi)
% 10.04/1.85 % (3665941)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=2013256372:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/567Mi)
% 10.04/1.85 % (3665933)Instruction limit reached!
% 10.04/1.85 % (3665933)------------------------------
% 10.04/1.85 % (3665933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.85 % (3665933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.85 % (3665933)CaDiCaL version: 2.1.3
% 10.04/1.85 % (3665933)Termination reason: Instruction limit
% 10.04/1.85 % (3665933)Termination phase: Saturation
% 10.04/1.85 % (3665933)Time elapsed: 0.174 s
% 10.04/1.85 % (3665933)Peak memory usage: 18 MB
% 10.04/1.85 % (3665933)Instructions burned: 764 (million)
% 10.04/1.85 % (3665943)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=1311198562:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2986 on theBenchmark for (2986ds/379Mi)
% 10.04/1.85 % (3665943)Refutation not found, incomplete strategy
% 10.04/1.85 % (3665943)------------------------------
% 10.04/1.85 % (3665943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.85 % (3665943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.85 % (3665943)CaDiCaL version: 2.1.3
% 10.04/1.85 % (3665943)Termination reason: Refutation not found, incomplete strategy
% 10.04/1.85 % (3665943)Time elapsed: 0.002 s
% 10.04/1.85 % (3665943)Peak memory usage: 12 MB
% 10.04/1.85 % (3665943)Instructions burned: 5 (million)
% 10.04/1.85 % (3665943)------------------------------
% 10.04/1.85 % (3665943)------------------------------
% 10.04/1.85 % (3665945)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=2048195073:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2986 on theBenchmark for (2986ds/429Mi)
% 10.04/1.85 % (3665945)Refutation not found, incomplete strategy
% 10.04/1.85 % (3665945)------------------------------
% 10.04/1.85 % (3665945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.85 % (3665945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.85 % (3665945)CaDiCaL version: 2.1.3
% 10.04/1.85 % (3665945)Termination reason: Refutation not found, incomplete strategy
% 10.04/1.85 % (3665945)Time elapsed: 0.002 s
% 10.04/1.85 % (3665945)Peak memory usage: 12 MB
% 10.04/1.85 % (3665945)Instructions burned: 7 (million)
% 10.04/1.85 % (3665945)------------------------------
% 10.04/1.85 % (3665945)------------------------------
% 10.04/1.85 % (3665947)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=2413948078:i=478:bd=all:rtra=on_2986 on theBenchmark for (2986ds/478Mi)
% 10.04/1.85 % (3665947)Refutation not found, incomplete strategy
% 10.04/1.85 % (3665947)------------------------------
% 10.04/1.85 % (3665947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.04/1.85 % (3665947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/1.85 % (3665947)CaDiCaL version: 2.1.3
% 10.04/1.85 % (3665947)Termination reason: Refutation not found, incomplete strategy
% 10.04/1.85 % (3665947)Time elapsed: 0.001 s
% 10.04/1.85 % (3665947)Peak memory usage: 12 MB
% 10.04/1.85 % (3665947)Instructions burned: 2 (million)
% 10.04/1.85 % (3665947)------------------------------
% 10.04/1.85 % (3665947)------------------------------
% 10.77/1.93 % (3665949)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4123641762:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2986 on theBenchmark for (2986ds/445Mi)
% 10.77/1.93 % (3665889)Instruction limit reached!
% 10.77/1.93 % (3665889)------------------------------
% 10.77/1.93 % (3665889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.77/1.93 % (3665889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.77/1.93 % (3665889)CaDiCaL version: 2.1.3
% 10.77/1.93 % (3665889)Termination reason: Instruction limit
% 10.77/1.93 % (3665889)Termination phase: Saturation
% 10.77/1.93 % (3665889)Time elapsed: 0.500 s
% 10.77/1.93 % (3665889)Peak memory usage: 19 MB
% 10.77/1.93 % (3665889)Instructions burned: 888 (million)
% 10.77/1.93 % (3665951)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=3792650434:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2985 on theBenchmark for (2985ds/71Mi)
% 10.77/1.93 % (3665939)Instruction limit reached!
% 10.77/1.93 % (3665939)------------------------------
% 10.77/1.93 % (3665939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.77/1.93 % (3665939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.77/1.93 % (3665939)CaDiCaL version: 2.1.3
% 10.77/1.93 % (3665939)Termination reason: Instruction limit
% 10.77/1.93 % (3665939)Termination phase: Saturation
% 10.77/1.93 % (3665939)Time elapsed: 0.191 s
% 10.77/1.93 % (3665939)Peak memory usage: 12 MB
% 10.77/1.93 % (3665939)Instructions burned: 302 (million)
% 10.77/1.93 % (3665953)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2669638645:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/302Mi)
% 10.77/1.93 % (3665949)Instruction limit reached!
% 10.77/1.93 % (3665949)------------------------------
% 10.77/1.93 % (3665949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.77/1.93 % (3665949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.77/1.93 % (3665949)CaDiCaL version: 2.1.3
% 10.77/1.93 % (3665949)Termination reason: Instruction limit
% 10.77/1.93 % (3665949)Termination phase: Saturation
% 10.77/1.93 % (3665949)Time elapsed: 0.117 s
% 10.77/1.93 % (3665949)Peak memory usage: 15 MB
% 10.77/1.93 % (3665949)Instructions burned: 447 (million)
% 10.77/1.93 % (3665955)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=1756535343:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2984 on theBenchmark for (2984ds/4980Mi)
% 10.77/1.93 % (3665955)Refutation not found, incomplete strategy
% 10.77/1.93 % (3665955)------------------------------
% 10.77/1.93 % (3665955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.77/1.93 % (3665955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.77/1.93 % (3665955)CaDiCaL version: 2.1.3
% 10.77/1.93 % (3665955)Termination reason: Refutation not found, incomplete strategy
% 10.77/1.93 % (3665955)Time elapsed: 0.001 s
% 10.77/1.93 % (3665955)Peak memory usage: 12 MB
% 10.77/1.93 % (3665955)Instructions burned: 2 (million)
% 10.77/1.93 % (3665955)------------------------------
% 10.77/1.93 % (3665955)------------------------------
% 10.77/1.93 % (3665951)Instruction limit reached!
% 10.77/1.93 % (3665951)------------------------------
% 10.77/1.93 % (3665951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.77/1.93 % (3665951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.77/1.93 % (3665951)CaDiCaL version: 2.1.3
% 10.77/1.93 % (3665951)Termination reason: Instruction limit
% 10.77/1.93 % (3665951)Termination phase: Saturation
% 10.77/1.93 % (3665951)Time elapsed: 0.058 s
% 10.77/1.93 % (3665951)Peak memory usage: 13 MB
% 10.77/1.93 % (3665951)Instructions burned: 73 (million)
% 10.77/1.93 % (3665957)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
% 10.77/1.93 % (3665957)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 10.77/1.93 % (3665957)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1626977221:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2984 on theBenchmark for (2984ds/100Mi)
% 10.77/1.93 % (3665958)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=3391404621:i=76:piset=equals:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/76Mi)
% 12.55/2.05 % (3665957)Instruction limit reached!
% 12.55/2.05 % (3665957)------------------------------
% 12.55/2.05 % (3665957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.05 % (3665957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.05 % (3665957)CaDiCaL version: 2.1.3
% 12.55/2.05 % (3665957)Termination reason: Instruction limit
% 12.55/2.05 % (3665957)Termination phase: Saturation
% 12.55/2.05 % (3665957)Time elapsed: 0.026 s
% 12.55/2.05 % (3665957)Peak memory usage: 12 MB
% 12.55/2.05 % (3665957)Instructions burned: 101 (million)
% 12.55/2.05 % (3665961)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=2145211264:i=289:rtra=on_2984 on theBenchmark for (2984ds/289Mi)
% 12.55/2.05 % (3665961)Refutation not found, incomplete strategy
% 12.55/2.05 % (3665961)------------------------------
% 12.55/2.05 % (3665961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.05 % (3665961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.05 % (3665961)CaDiCaL version: 2.1.3
% 12.55/2.05 % (3665961)Termination reason: Refutation not found, incomplete strategy
% 12.55/2.05 % (3665961)Time elapsed: 0.001 s
% 12.55/2.05 % (3665961)Peak memory usage: 12 MB
% 12.55/2.05 % (3665961)Instructions burned: 2 (million)
% 12.55/2.05 % (3665961)------------------------------
% 12.55/2.05 % (3665961)------------------------------
% 12.55/2.05 % (3665963)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=2691867362:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2984 on theBenchmark for (2984ds/493Mi)
% 12.55/2.05 % (3665941)Instruction limit reached!
% 12.55/2.05 % (3665941)------------------------------
% 12.55/2.05 % (3665941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.05 % (3665941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.05 % (3665941)CaDiCaL version: 2.1.3
% 12.55/2.05 % (3665941)Termination reason: Instruction limit
% 12.55/2.05 % (3665941)Termination phase: Saturation
% 12.55/2.05 % (3665941)Time elapsed: 0.273 s
% 12.55/2.05 % (3665941)Peak memory usage: 15 MB
% 12.55/2.05 % (3665941)Instructions burned: 567 (million)
% 12.55/2.05 % (3665963)Refutation not found, incomplete strategy
% 12.55/2.05 % (3665963)------------------------------
% 12.55/2.05 % (3665963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.05 % (3665963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.05 % (3665963)CaDiCaL version: 2.1.3
% 12.55/2.05 % (3665963)Termination reason: Refutation not found, incomplete strategy
% 12.55/2.05 % (3665963)Time elapsed: 0.002 s
% 12.55/2.05 % (3665963)Peak memory usage: 12 MB
% 12.55/2.05 % (3665963)Instructions burned: 6 (million)
% 12.55/2.05 % (3665963)------------------------------
% 12.55/2.05 % (3665963)------------------------------
% 12.55/2.05 % (3665958)Instruction limit reached!
% 12.55/2.05 % (3665958)------------------------------
% 12.55/2.05 % (3665958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.05 % (3665958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.05 % (3665958)CaDiCaL version: 2.1.3
% 12.55/2.05 % (3665958)Termination reason: Instruction limit
% 12.55/2.05 % (3665958)Termination phase: Saturation
% 12.55/2.05 % (3665958)Time elapsed: 0.039 s
% 12.55/2.05 % (3665958)Peak memory usage: 12 MB
% 12.55/2.05 % (3665958)Instructions burned: 76 (million)
% 12.55/2.05 % (3665966)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 12.55/2.05 % (3665966)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=1054177998:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2983 on theBenchmark for (2983ds/372Mi)
% 12.55/2.05 % (3665966)Refutation not found, incomplete strategy
% 12.55/2.05 % (3665966)------------------------------
% 12.55/2.05 % (3665966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.05 % (3665966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.05 % (3665966)CaDiCaL version: 2.1.3
% 12.55/2.05 % (3665966)Termination reason: Refutation not found, incomplete strategy
% 12.55/2.05 % (3665966)Time elapsed: 0.001 s
% 12.55/2.12 % (3665966)Peak memory usage: 12 MB
% 12.55/2.12 % (3665966)Instructions burned: 2 (million)
% 12.55/2.12 % (3665966)------------------------------
% 12.55/2.12 % (3665966)------------------------------
% 12.55/2.12 % (3665965)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=4038996464:cond=on:i=34:hud=10:nm=10:rtra=on_2984 on theBenchmark for (2984ds/34Mi)
% 12.55/2.12 % (3665969)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2257945577:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2983 on theBenchmark for (2983ds/647Mi)
% 12.55/2.12 % (3665967)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=2278569208:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2983 on theBenchmark for (2983ds/670Mi)
% 12.55/2.12 % (3665967)Refutation not found, incomplete strategy
% 12.55/2.12 % (3665967)------------------------------
% 12.55/2.12 % (3665967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.12 % (3665967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.12 % (3665967)CaDiCaL version: 2.1.3
% 12.55/2.12 % (3665967)Termination reason: Refutation not found, incomplete strategy
% 12.55/2.12 % (3665967)Time elapsed: 0.004 s
% 12.55/2.12 % (3665967)Peak memory usage: 12 MB
% 12.55/2.12 % (3665967)Instructions burned: 5 (million)
% 12.55/2.12 % (3665967)------------------------------
% 12.55/2.12 % (3665967)------------------------------
% 12.55/2.12 % (3665965)Instruction limit reached!
% 12.55/2.12 % (3665965)------------------------------
% 12.55/2.12 % (3665965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.12 % (3665965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.12 % (3665965)CaDiCaL version: 2.1.3
% 12.55/2.12 % (3665965)Termination reason: Instruction limit
% 12.55/2.12 % (3665965)Termination phase: Saturation
% 12.55/2.12 % (3665965)Time elapsed: 0.017 s
% 12.55/2.12 % (3665965)Peak memory usage: 12 MB
% 12.55/2.12 % (3665965)Instructions burned: 35 (million)
% 12.55/2.12 % (3665973)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=535052207:i=857:add=off:kws=frequency:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/857Mi)
% 12.55/2.12 % (3665973)Refutation not found, incomplete strategy
% 12.55/2.12 % (3665973)------------------------------
% 12.55/2.12 % (3665973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.12 % (3665973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.12 % (3665973)CaDiCaL version: 2.1.3
% 12.55/2.12 % (3665973)Termination reason: Refutation not found, incomplete strategy
% 12.55/2.12 % (3665973)Time elapsed: 0.003 s
% 12.55/2.12 % (3665973)Peak memory usage: 12 MB
% 12.55/2.12 % (3665973)Instructions burned: 4 (million)
% 12.55/2.12 % (3665973)------------------------------
% 12.55/2.12 % (3665973)------------------------------
% 12.55/2.12 % (3665974)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=4103267101:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2983 on theBenchmark for (2983ds/693Mi)
% 12.55/2.12 % (3665976)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=755759126:i=285:hud=10:bd=all:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/285Mi)
% 12.55/2.12 % (3665976)Refutation not found, incomplete strategy
% 12.55/2.12 % (3665976)------------------------------
% 12.55/2.12 % (3665976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.55/2.12 % (3665976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.12 % (3665976)CaDiCaL version: 2.1.3
% 12.55/2.12 % (3665976)Termination reason: Refutation not found, incomplete strategy
% 12.55/2.12 % (3665976)Time elapsed: 0.005 s
% 12.55/2.12 % (3665976)Peak memory usage: 12 MB
% 12.55/2.12 % (3665976)Instructions burned: 7 (million)
% 12.55/2.12 % (3665976)------------------------------
% 12.55/2.12 % (3665976)------------------------------
% 12.55/2.12 % (3665979)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 12.55/2.12 % (3665979)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=3712747638:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2983 on theBenchmark for (2983ds/52Mi)
% 13.97/2.39 % (3665979)Instruction limit reached!
% 13.97/2.39 % (3665979)------------------------------
% 13.97/2.39 % (3665979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.39 % (3665979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.39 % (3665979)CaDiCaL version: 2.1.3
% 13.97/2.39 % (3665979)Termination reason: Instruction limit
% 13.97/2.39 % (3665979)Termination phase: Saturation
% 13.97/2.39 % (3665979)Time elapsed: 0.023 s
% 13.97/2.39 % (3665979)Peak memory usage: 12 MB
% 13.97/2.39 % (3665979)Instructions burned: 54 (million)
% 13.97/2.39 % (3665953)Instruction limit reached!
% 13.97/2.39 % (3665953)------------------------------
% 13.97/2.39 % (3665953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.39 % (3665953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.39 % (3665953)CaDiCaL version: 2.1.3
% 13.97/2.39 % (3665953)Termination reason: Instruction limit
% 13.97/2.39 % (3665953)Termination phase: Saturation
% 13.97/2.39 % (3665953)Time elapsed: 0.215 s
% 13.97/2.39 % (3665953)Peak memory usage: 14 MB
% 13.97/2.39 % (3665953)Instructions burned: 302 (million)
% 13.97/2.39 % (3665981)dis+10_1_si=on:random_seed=4202552648:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2982 on theBenchmark for (2982ds/407Mi)
% 13.97/2.39 % (3665982)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=3082494687:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/2240Mi)
% 13.97/2.39 % (3665969)Instruction limit reached!
% 13.97/2.39 % (3665969)------------------------------
% 13.97/2.39 % (3665969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.39 % (3665969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.39 % (3665969)CaDiCaL version: 2.1.3
% 13.97/2.39 % (3665969)Termination reason: Instruction limit
% 13.97/2.39 % (3665969)Termination phase: Saturation
% 13.97/2.39 % (3665969)Time elapsed: 0.147 s
% 13.97/2.39 % (3665969)Peak memory usage: 13 MB
% 13.97/2.39 % (3665969)Instructions burned: 653 (million)
% 13.97/2.39 % (3665986)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=3156739117:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2982 on theBenchmark for (2982ds/336Mi)
% 13.97/2.39 % (3665986)Refutation not found, incomplete strategy
% 13.97/2.39 % (3665986)------------------------------
% 13.97/2.39 % (3665986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.39 % (3665986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.39 % (3665986)CaDiCaL version: 2.1.3
% 13.97/2.39 % (3665986)Termination reason: Refutation not found, incomplete strategy
% 13.97/2.39 % (3665986)Time elapsed: 0.002 s
% 13.97/2.39 % (3665986)Peak memory usage: 12 MB
% 13.97/2.39 % (3665986)Instructions burned: 6 (million)
% 13.97/2.39 % (3665986)------------------------------
% 13.97/2.39 % (3665986)------------------------------
% 13.97/2.39 % (3665988)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=1213077910:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2982 on theBenchmark for (2982ds/1142Mi)
% 13.97/2.39 % (3665988)Refutation not found, incomplete strategy
% 13.97/2.39 % (3665988)------------------------------
% 13.97/2.39 % (3665988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.39 % (3665988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.39 % (3665988)CaDiCaL version: 2.1.3
% 13.97/2.39 % (3665988)Termination reason: Refutation not found, incomplete strategy
% 13.97/2.39 % (3665988)Time elapsed: 0.003 s
% 13.97/2.39 % (3665988)Peak memory usage: 13 MB
% 13.97/2.39 % (3665988)Instructions burned: 6 (million)
% 13.97/2.39 % (3665988)------------------------------
% 13.97/2.39 % (3665988)------------------------------
% 13.97/2.39 % (3665982)Refutation not found, incomplete strategy
% 13.97/2.39 % (3665982)------------------------------
% 13.97/2.39 % (3665982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.39 % (3665982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.39 % (3665982)CaDiCaL version: 2.1.3
% 13.97/2.39 % (3665982)Termination reason: Refutation not found, incomplete strategy
% 13.97/2.39 % (3665982)Time elapsed: 0.042 s
% 13.97/2.39 % (3665982)Peak memory usage: 12 MB
% 13.97/2.39 % (3665982)Instructions burned: 46 (million)
% 13.97/2.39 % (3665982)------------------------------
% 15.70/2.63 % (3665982)------------------------------
% 15.70/2.63 % (3665990)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=3229592979:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2981 on theBenchmark for (2981ds/376Mi)
% 15.70/2.63 % (3665990)Refutation not found, incomplete strategy
% 15.70/2.63 % (3665990)------------------------------
% 15.70/2.63 % (3665990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.70/2.63 % (3665990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/2.63 % (3665990)CaDiCaL version: 2.1.3
% 15.70/2.63 % (3665990)Termination reason: Refutation not found, incomplete strategy
% 15.70/2.63 % (3665990)Time elapsed: 0.003 s
% 15.70/2.63 % (3665990)Peak memory usage: 12 MB
% 15.70/2.63 % (3665990)Instructions burned: 4 (million)
% 15.70/2.63 % (3665990)------------------------------
% 15.70/2.63 % (3665990)------------------------------
% 15.70/2.63 % (3665991)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=1774135363:i=766:bd=all:rtra=on_2981 on theBenchmark for (2981ds/766Mi)
% 15.70/2.63 % (3665991)Refutation not found, incomplete strategy
% 15.70/2.63 % (3665991)------------------------------
% 15.70/2.63 % (3665991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.70/2.63 % (3665991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/2.63 % (3665991)CaDiCaL version: 2.1.3
% 15.70/2.63 % (3665991)Termination reason: Refutation not found, incomplete strategy
% 15.70/2.63 % (3665991)Time elapsed: 0.001 s
% 15.70/2.63 % (3665991)Peak memory usage: 13 MB
% 15.70/2.63 % (3665991)Instructions burned: 3 (million)
% 15.70/2.63 % (3665991)------------------------------
% 15.70/2.63 % (3665991)------------------------------
% 15.70/2.63 % (3665995)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=3745423489:i=6359:add=on:kws=inv_frequency:aac=none:rtra=on:c=on:er=filter:ntd=on_2981 on theBenchmark for (2981ds/6359Mi)
% 15.70/2.63 % (3665994)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 15.70/2.63 % (3665995)Refutation not found, incomplete strategy
% 15.70/2.63 % (3665995)------------------------------
% 15.70/2.63 % (3665995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.70/2.63 % (3665995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/2.63 % (3665995)CaDiCaL version: 2.1.3
% 15.70/2.63 % (3665995)Termination reason: Refutation not found, incomplete strategy
% 15.70/2.63 % (3665995)Time elapsed: 0.002 s
% 15.70/2.63 % (3665995)Peak memory usage: 12 MB
% 15.70/2.63 % (3665995)Instructions burned: 4 (million)
% 15.70/2.63 % (3665995)------------------------------
% 15.70/2.63 % (3665995)------------------------------
% 15.70/2.63 % (3665994)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=318333256: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_2981 on theBenchmark for (2981ds/959Mi)
% 15.70/2.63 % (3665997)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1131364581:st=4:i=35:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2981 on theBenchmark for (2981ds/35Mi)
% 15.70/2.63 % (3665997)Refutation not found, incomplete strategy
% 15.70/2.63 % (3665997)------------------------------
% 15.70/2.63 % (3665997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.70/2.63 % (3665997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/2.63 % (3665997)CaDiCaL version: 2.1.3
% 15.70/2.63 % (3665997)Termination reason: Refutation not found, incomplete strategy
% 15.70/2.63 % (3665997)Time elapsed: 0.002 s
% 15.70/2.63 % (3665997)Peak memory usage: 12 MB
% 15.70/2.63 % (3665997)Instructions burned: 6 (million)
% 15.70/2.63 % (3665997)------------------------------
% 15.70/2.63 % (3665997)------------------------------
% 15.70/2.63 % (3666000)dis+10_1_sfv=off:sil=128000:cnfonf=lazy_gen:si=on:uwa=off:nwc=1:chr=on:random_seed=3293188647:hsq=on:hsqr=1,8:i=53:hsql=off:bd=all:rtra=on:ixr=off_2981 on theBenchmark for (2981ds/53Mi)
% 15.70/2.63 % (3666000)Instruction limit reached!
% 15.70/2.63 % (3666000)------------------------------
% 15.70/2.63 % (3666000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.70/2.63 % (3666000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/2.76 % (3666000)CaDiCaL version: 2.1.3
% 16.38/2.76 % (3666000)Termination reason: Instruction limit
% 16.38/2.76 % (3666000)Termination phase: Saturation
% 16.38/2.76 % (3666000)Time elapsed: 0.018 s
% 16.38/2.76 % (3666000)Peak memory usage: 12 MB
% 16.38/2.76 % (3666000)Instructions burned: 55 (million)
% 16.38/2.76 % (3666002)dis+21_1_sil=128000:tgt=full:fde=none:e2e=on:si=on:urr=on:uwa=interpreted_only:s2agt=32:sac=on:random_seed=3694821459:s2a=on:i=876:s2at=6:nm=2:rtra=on_2981 on theBenchmark for (2981ds/876Mi)
% 16.38/2.76 % (3665974)Instruction limit reached!
% 16.38/2.76 % (3665974)------------------------------
% 16.38/2.76 % (3665974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.38/2.76 % (3665974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/2.76 % (3665974)CaDiCaL version: 2.1.3
% 16.38/2.76 % (3665974)Termination reason: Instruction limit
% 16.38/2.76 % (3665974)Termination phase: Saturation
% 16.38/2.76 % (3665974)Time elapsed: 0.302 s
% 16.38/2.76 % (3665974)Peak memory usage: 19 MB
% 16.38/2.76 % (3665974)Instructions burned: 694 (million)
% 16.38/2.76 % (3666005)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3460508877:i=57:ep=R:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/57Mi)
% 16.38/2.76 % (3666005)Refutation not found, incomplete strategy
% 16.38/2.76 % (3666005)------------------------------
% 16.38/2.76 % (3666005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.38/2.76 % (3666005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/2.76 % (3666005)CaDiCaL version: 2.1.3
% 16.38/2.76 % (3666005)Termination reason: Refutation not found, incomplete strategy
% 16.38/2.76 % (3666005)Time elapsed: 0.004 s
% 16.38/2.76 % (3666005)Peak memory usage: 12 MB
% 16.38/2.76 % (3666005)Instructions burned: 6 (million)
% 16.38/2.76 % (3666005)------------------------------
% 16.38/2.76 % (3666005)------------------------------
% 16.38/2.76 % (3665981)Instruction limit reached!
% 16.38/2.76 % (3665981)------------------------------
% 16.38/2.76 % (3665981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.38/2.76 % (3665981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/2.76 % (3665981)CaDiCaL version: 2.1.3
% 16.38/2.76 % (3665981)Termination reason: Instruction limit
% 16.38/2.76 % (3665981)Termination phase: Saturation
% 16.38/2.76 % (3665981)Time elapsed: 0.249 s
% 16.38/2.76 % (3665981)Peak memory usage: 14 MB
% 16.38/2.76 % (3665981)Instructions burned: 408 (million)
% 16.38/2.76 % (3666010)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 16.38/2.76 % (3666010)dis+1002_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_min:sos=on:fd=preordered:slsqc=2:chr=on:random_seed=2766161114:i=306:bd=all:rtra=on_2980 on theBenchmark for (2980ds/306Mi)
% 16.38/2.76 % (3666012)dis+10_8:1_sil=128000:si=on:uwa=off:random_seed=1168306145:i=262:sd=2:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/262Mi)
% 16.38/2.76 % (3666012)Refutation not found, incomplete strategy
% 16.38/2.76 % (3666012)------------------------------
% 16.38/2.76 % (3666012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.38/2.76 % (3666012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/2.76 % (3666012)CaDiCaL version: 2.1.3
% 16.38/2.76 % (3666012)Termination reason: Refutation not found, incomplete strategy
% 16.38/2.76 % (3666012)Time elapsed: 0.006 s
% 16.38/2.76 % (3666012)Peak memory usage: 12 MB
% 16.38/2.76 % (3666012)Instructions burned: 8 (million)
% 16.38/2.76 % (3666012)------------------------------
% 16.38/2.76 % (3666012)------------------------------
% 16.38/2.76 % (3666015)WARNING Broken Constraint: if ho_split_queue_ratios(1,3) has been set then ho_split_queue(off) is equal to on
% 16.38/2.76 % (3666015)ott+1002_16_sil=128000:si=on:random_seed=4044157952:hsqr=1,3:i=409:add=on:rtra=on:fe=abstraction_2979 on theBenchmark for (2979ds/409Mi)
% 16.38/2.76 % (3666010)Instruction limit reached!
% 16.38/2.76 % (3666010)------------------------------
% 16.38/2.76 % (3666010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.38/2.76 % (3666010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/2.76 % (3666010)CaDiCaL version: 2.1.3
% 16.38/2.76 % (3666010)Termination reason: Instruction limit
% 16.38/2.76 % (3666010)Termination phase: Saturation
% 16.38/2.76 % (3666010)Time elapsed: 0.150 s
% 16.38/2.76 % (3666010)Peak memory usage: 14 MB
% 17.94/2.95 % (3666010)Instructions burned: 308 (million)
% 17.94/2.95 % (3666017)dis+10_1_sil=128000:plsq=on:si=on:plsqr=32,1:uwa=off:random_seed=4168451063:s2a=on:i=381:rtra=on_2978 on theBenchmark for (2978ds/381Mi)
% 17.94/2.95 % (3666017)Refutation not found, incomplete strategy
% 17.94/2.95 % (3666017)------------------------------
% 17.94/2.95 % (3666017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.94/2.95 % (3666017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/2.95 % (3666017)CaDiCaL version: 2.1.3
% 17.94/2.95 % (3666017)Termination reason: Refutation not found, incomplete strategy
% 17.94/2.95 % (3666017)Time elapsed: 0.005 s
% 17.94/2.95 % (3666017)Peak memory usage: 12 MB
% 17.94/2.95 % (3666017)Instructions burned: 8 (million)
% 17.94/2.95 % (3666017)------------------------------
% 17.94/2.95 % (3666017)------------------------------
% 17.94/2.95 % (3666019)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1074024634:cond=on:i=324:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/324Mi)
% 17.94/2.95 % (3666002)Instruction limit reached!
% 17.94/2.95 % (3666002)------------------------------
% 17.94/2.95 % (3666002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.94/2.95 % (3666002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/2.95 % (3666002)CaDiCaL version: 2.1.3
% 17.94/2.95 % (3666002)Termination reason: Instruction limit
% 17.94/2.95 % (3666002)Termination phase: Saturation
% 17.94/2.95 % (3666002)Time elapsed: 0.360 s
% 17.94/2.95 % (3666002)Peak memory usage: 13 MB
% 17.94/2.95 % (3666002)Instructions burned: 879 (million)
% 17.94/2.95 % (3665910)Instruction limit reached!
% 17.94/2.95 % (3665910)------------------------------
% 17.94/2.95 % (3665910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.94/2.95 % (3665910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/2.95 % (3665910)CaDiCaL version: 2.1.3
% 17.94/2.95 % (3665910)Termination reason: Instruction limit
% 17.94/2.95 % (3665910)Termination phase: Saturation
% 17.94/2.95 % (3665910)Time elapsed: 1.226 s
% 17.94/2.95 % (3665910)Peak memory usage: 20 MB
% 17.94/2.95 % (3665910)Instructions burned: 2471 (million)
% 17.94/2.95 % (3666025)lrs+10_1_sil=128000:fde=none:si=on:sos=on:spb=goal_then_units:urr=on:random_seed=2183075425:i=240:kws=inv_precedence:rtra=on_2977 on theBenchmark for (2977ds/240Mi)
% 17.94/2.95 % (3666027)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 17.94/2.95 % (3666027)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3007661767:cts=off:uwa_fpi=on:i=124:av=off:fsr=off:rtra=on:ntd=on_2977 on theBenchmark for (2977ds/124Mi)
% 17.94/2.95 % (3666015)Instruction limit reached!
% 17.94/2.95 % (3666015)------------------------------
% 17.94/2.95 % (3666015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.94/2.95 % (3666015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/2.95 % (3666015)CaDiCaL version: 2.1.3
% 17.94/2.95 % (3666015)Termination reason: Instruction limit
% 17.94/2.95 % (3666015)Termination phase: Saturation
% 17.94/2.95 % (3666015)Time elapsed: 0.305 s
% 17.94/2.95 % (3666015)Peak memory usage: 14 MB
% 17.94/2.95 % (3666015)Instructions burned: 409 (million)
% 17.94/2.95 % (3666037)lrs+1010_2_to=lpo:cnfonf=off:e2e=on:si=on:random_seed=2613082466:uwa_fpi=on:i=223:bd=all:rtra=on:fe=abstraction:ntd=on_2976 on theBenchmark for (2976ds/223Mi)
% 17.94/2.95 % (3666025)Instruction limit reached!
% 17.94/2.95 % (3666025)------------------------------
% 17.94/2.95 % (3666025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.94/2.95 % (3666025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/2.95 % (3666025)CaDiCaL version: 2.1.3
% 17.94/2.95 % (3666025)Termination reason: Instruction limit
% 17.94/2.95 % (3666025)Termination phase: Saturation
% 17.94/2.95 % (3666025)Time elapsed: 0.094 s
% 17.94/2.95 % (3666025)Peak memory usage: 14 MB
% 17.94/2.95 % (3666025)Instructions burned: 240 (million)
% 17.94/2.95 % (3666019)Instruction limit reached!
% 17.94/2.95 % (3666019)------------------------------
% 17.94/2.95 % (3666019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.94/2.95 % (3666019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/2.95 % (3666019)CaDiCaL version: 2.1.3
% 17.94/2.95 % (3666019)Termination reason: Instruction limit
% 17.94/2.95 % (3666019)Termination phase: Saturation
% 19.40/3.05 % (3666019)Time elapsed: 0.195 s
% 19.40/3.05 % (3666019)Peak memory usage: 13 MB
% 19.40/3.05 % (3666019)Instructions burned: 324 (million)
% 19.40/3.05 % (3666039)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=403350444:s2a=on:i=282:kws=inv_frequency:bd=all:rtra=on_2976 on theBenchmark for (2976ds/282Mi)
% 19.40/3.05 % (3666040)lrs+10_1_sil=128000:tgt=ground:cnfonf=conj_eager:si=on:random_seed=4124124269:s2a=on:i=464:kws=frequency:bd=all:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/464Mi)
% 19.40/3.05 % (3666040)Refutation not found, incomplete strategy
% 19.40/3.05 % (3666040)------------------------------
% 19.40/3.05 % (3666040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666040)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666040)Termination reason: Refutation not found, incomplete strategy
% 19.40/3.05 % (3666040)Time elapsed: 0.002 s
% 19.40/3.05 % (3666040)Peak memory usage: 12 MB
% 19.40/3.05 % (3666040)Instructions burned: 2 (million)
% 19.40/3.05 % (3666040)------------------------------
% 19.40/3.05 % (3666040)------------------------------
% 19.40/3.05 % (3666027)Instruction limit reached!
% 19.40/3.05 % (3666027)------------------------------
% 19.40/3.05 % (3666027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666027)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666027)Termination reason: Instruction limit
% 19.40/3.05 % (3666027)Termination phase: Saturation
% 19.40/3.05 % (3666027)Time elapsed: 0.092 s
% 19.40/3.05 % (3666027)Peak memory usage: 12 MB
% 19.40/3.05 % (3666027)Instructions burned: 125 (million)
% 19.40/3.05 % (3666044)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3149807923:s2a=on:cond=on:i=280:add=on:bd=preordered:rtra=on:er=filter_2975 on theBenchmark for (2975ds/280Mi)
% 19.40/3.05 % (3666043)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=3376654340:i=88:s2at=3:nm=2:rtra=on:rawr=on_2975 on theBenchmark for (2975ds/88Mi)
% 19.40/3.05 % (3666043)Refutation not found, incomplete strategy
% 19.40/3.05 % (3666043)------------------------------
% 19.40/3.05 % (3666043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666043)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666043)Termination reason: Refutation not found, incomplete strategy
% 19.40/3.05 % (3666043)Time elapsed: 0.008 s
% 19.40/3.05 % (3666043)Peak memory usage: 13 MB
% 19.40/3.05 % (3666043)Instructions burned: 5 (million)
% 19.40/3.05 % (3666043)------------------------------
% 19.40/3.05 % (3666043)------------------------------
% 19.40/3.05 % (3665994)Instruction limit reached!
% 19.40/3.05 % (3665994)------------------------------
% 19.40/3.05 % (3665994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3665994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3665994)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3665994)Termination reason: Instruction limit
% 19.40/3.05 % (3665994)Termination phase: Saturation
% 19.40/3.05 % (3665994)Time elapsed: 0.636 s
% 19.40/3.05 % (3665994)Peak memory usage: 20 MB
% 19.40/3.05 % (3665994)Instructions burned: 959 (million)
% 19.40/3.05 % (3666048)WARNING Broken Constraint: if lookahaed_delay(10) has been set then selection(21) is not lookahead selection
% 19.40/3.05 % (3666048)WARNING Broken Constraint: if mono_ep(off) has been set then equality_proxy(off) is not equal to off
% 19.40/3.05 % (3666048)ott+21_3:13_sil=128000:cnfonf=off:sas=cadical:si=on:sp=arity:lma=off:lsd=10:uwa=one_side_interpreted:mep=off:chr=on:random_seed=1772861621:hsq=on:st=2:i=483:sd=1:hsql=off:rtra=on:fe=abstraction:fdi=32:ss=axioms:sgt=20:ntd=on_2975 on theBenchmark for (2975ds/483Mi)
% 19.40/3.05 % (3666047)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 19.40/3.05 % (3666047)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3594322209:i=4386:hud=10:nm=16:av=off:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/4386Mi)
% 19.40/3.05 % (3666039)Instruction limit reached!
% 19.40/3.05 % (3666039)------------------------------
% 19.40/3.05 % (3666039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666039)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666039)Termination reason: Instruction limit
% 19.40/3.05 % (3666039)Termination phase: Saturation
% 19.40/3.05 % (3666039)Time elapsed: 0.124 s
% 19.40/3.05 % (3666039)Peak memory usage: 14 MB
% 19.40/3.05 % (3666039)Instructions burned: 282 (million)
% 19.40/3.05 % (3666037)Instruction limit reached!
% 19.40/3.05 % (3666037)------------------------------
% 19.40/3.05 % (3666037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666037)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666037)Termination reason: Instruction limit
% 19.40/3.05 % (3666037)Termination phase: Saturation
% 19.40/3.05 % (3666037)Time elapsed: 0.192 s
% 19.40/3.05 % (3666037)Peak memory usage: 14 MB
% 19.40/3.05 % (3666037)Instructions burned: 224 (million)
% 19.40/3.05 % (3666051)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1782068522:i=73:rtra=on_2974 on theBenchmark for (2974ds/73Mi)
% 19.40/3.05 % (3666051)Refutation not found, incomplete strategy
% 19.40/3.05 % (3666051)------------------------------
% 19.40/3.05 % (3666051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666051)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666051)Termination reason: Refutation not found, incomplete strategy
% 19.40/3.05 % (3666051)Time elapsed: 0.002 s
% 19.40/3.05 % (3666051)Peak memory usage: 12 MB
% 19.40/3.05 % (3666051)Instructions burned: 3 (million)
% 19.40/3.05 % (3666051)------------------------------
% 19.40/3.05 % (3666051)------------------------------
% 19.40/3.05 % (3666052)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=481035516:cts=off:i=176:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2974 on theBenchmark for (2974ds/176Mi)
% 19.40/3.05 % (3666055)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 19.40/3.05 % (3666055)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=4202437695:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2973 on theBenchmark for (2973ds/39Mi)
% 19.40/3.05 % (3666055)Instruction limit reached!
% 19.40/3.05 % (3666055)------------------------------
% 19.40/3.05 % (3666055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666055)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666055)Termination reason: Instruction limit
% 19.40/3.05 % (3666055)Termination phase: Saturation
% 19.40/3.05 % (3666055)Time elapsed: 0.020 s
% 19.40/3.05 % (3666055)Peak memory usage: 12 MB
% 19.40/3.05 % (3666055)Instructions burned: 41 (million)
% 19.40/3.05 % (3666057)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1333917301:i=708:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2973 on theBenchmark for (2973ds/708Mi)
% 19.40/3.05 % (3666044)Instruction limit reached!
% 19.40/3.05 % (3666044)------------------------------
% 19.40/3.05 % (3666044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666044)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666044)Termination reason: Instruction limit
% 19.40/3.05 % (3666044)Termination phase: Saturation
% 19.40/3.05 % (3666044)Time elapsed: 0.232 s
% 19.40/3.05 % (3666044)Peak memory usage: 13 MB
% 19.40/3.05 % (3666044)Instructions burned: 281 (million)
% 19.40/3.05 % (3666059)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
% 19.40/3.05 % (3666059)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=1021571959:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2973 on theBenchmark for (2973ds/252Mi)
% 19.40/3.05 % (3666059)Refutation not found, incomplete strategy
% 19.40/3.05 % (3666059)------------------------------
% 19.40/3.05 % (3666059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666059)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666059)Termination reason: Refutation not found, incomplete strategy
% 19.40/3.05 % (3666059)Time elapsed: 0.003 s
% 19.40/3.05 % (3666059)Peak memory usage: 12 MB
% 19.40/3.05 % (3666059)Instructions burned: 4 (million)
% 19.40/3.05 % (3666059)------------------------------
% 19.40/3.05 % (3666059)------------------------------
% 19.40/3.05 % (3666061)dis+10_4_sil=128000:tgt=full:fde=unused:cnfonf=lazy_not_gen:sas=cadical:si=on:uwa=off:sac=on:random_seed=912272129:i=823:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/823Mi)
% 19.40/3.05 % (3666052)Instruction limit reached!
% 19.40/3.05 % (3666052)------------------------------
% 19.40/3.05 % (3666052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666052)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666052)Termination reason: Instruction limit
% 19.40/3.05 % (3666052)Termination phase: Saturation
% 19.40/3.05 % (3666052)Time elapsed: 0.151 s
% 19.40/3.05 % (3666052)Peak memory usage: 13 MB
% 19.40/3.05 % (3666052)Instructions burned: 177 (million)
% 19.40/3.05 % (3666063)WARNING Broken Constraint: lrs_first_time_check(100) is less than 100
% 19.40/3.05 % (3666047) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3665673-3666047"...
% 19.40/3.05 % (3666047)...printing done.
% 19.40/3.05 % (3666063)lrs+1010_7_anc=all_dependent:sil=128000:cnfonf=lazy_not_gen:si=on:urr=on:rp=on:sac=on:lftc=100:random_seed=853476658:lrd=on:st=3:i=16202:add=on:sd=3:kws=frequency:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/16202Mi)
% 19.40/3.05 % (3666047)Refutation found. Thanks to Tanya!
% 19.40/3.05 % SZS status Theorem for theBenchmark
% 19.40/3.05 % SZS output start Proof for theBenchmark
% See solution above
% 19.40/3.05 % (3666047)------------------------------
% 19.40/3.05 % (3666047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.40/3.05 % (3666047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.05 % (3666047)CaDiCaL version: 2.1.3
% 19.40/3.05 % (3666047)Termination reason: Refutation
% 19.40/3.05 % (3666047)Time elapsed: 0.293 s
% 19.40/3.05 % (3666047)Peak memory usage: 14 MB
% 19.40/3.05 % (3666047)Instructions burned: 335 (million)
% 19.40/3.05 % (3665673)Success in time 2.813 s
% 19.40/3.05 % Vampire exiting
%------------------------------------------------------------------------------