%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU968^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:32:03 AM UTC 2026
% Result : Theorem 35.74s 5.48s
% Output : Refutation 35.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 3
% Syntax : Number of formulae : 67 ( 38 unt; 0 typ; 2 def)
% Number of atoms : 361 ( 77 equ; 0 cnn)
% Maximal formula atoms : 3 ( 5 avg)
% Number of connectives : 1244 ( 23 ~; 32 |; 75 &; 834 @)
% ( 2 <=>; 150 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 443 ( 443 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 25 usr; 6 con; 0-4 aty)
% ( 128 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 416 ( 12 sgn 41 !; 0 ?; 416 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_1,type,
vNOT: $o > $o ).
thf(func_def_2,type,
vIMP: $o > $o > $o ).
thf(func_def_3,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_4,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_5,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_6,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_7,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_8,type,
vAND: $o > $o > $o ).
thf(func_def_9,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_10,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_11,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_14,type,
sK0: a > a ).
thf(func_def_15,type,
sK1: a > a ).
thf(func_def_16,type,
sK2: a > a ).
thf(func_def_17,type,
sK3: ( a > a ) > $o ).
thf(func_def_18,type,
sK4: ( ( a > a ) > $o ) > a > a ).
thf(func_def_19,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_20,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_21,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_23,type,
sK6: a > a ).
thf(func_def_24,type,
sK7: a > a ).
thf(func_def_25,type,
sK8: a ).
thf(f1,conjecture,
( ! [X0: a > a] :
( X0
= ( ^ [X1: a] : ( X0 @ X1 ) ) )
=> ! [X3: a > a,X4: a > a,X2: a > a] :
( ( ! [X5: ( a > a ) > $o] :
( ( ! [X7: a > a] :
( ( X5 @ X7 )
=> ( X5
@ ^ [X1: a] : ( X2 @ ( X7 @ X1 ) ) ) )
& ( X5
@ ^ [X6: a] : X6 ) )
=> ( X5 @ X3 ) )
& ! [X5: ( a > a ) > $o] :
( ( ! [X7: a > a] :
( ( X5 @ X7 )
=> ( X5
@ ^ [X1: a] : ( X2 @ ( X7 @ X1 ) ) ) )
& ( X5
@ ^ [X6: a] : X6 ) )
=> ( X5 @ X4 ) ) )
=> ! [X5: ( a > a ) > $o] :
( ( ( X5
@ ^ [X6: a] : X6 )
& ! [X7: a > a] :
( ( X5 @ X7 )
=> ( X5
@ ^ [X1: a] : ( X2 @ ( X7 @ X1 ) ) ) ) )
=> ( X5
@ ^ [X1: a] : ( X3 @ ( X4 @ X1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM135C_pme) ).
thf(f2,negated_conjecture,
~ ( ! [X0: a > a] :
( X0
= ( ^ [X1: a] : ( X0 @ X1 ) ) )
=> ! [X3: a > a,X4: a > a,X2: a > a] :
( ( ! [X5: ( a > a ) > $o] :
( ( ! [X7: a > a] :
( ( X5 @ X7 )
=> ( X5
@ ^ [X1: a] : ( X2 @ ( X7 @ X1 ) ) ) )
& ( X5
@ ^ [X6: a] : X6 ) )
=> ( X5 @ X3 ) )
& ! [X5: ( a > a ) > $o] :
( ( ! [X7: a > a] :
( ( X5 @ X7 )
=> ( X5
@ ^ [X1: a] : ( X2 @ ( X7 @ X1 ) ) ) )
& ( X5
@ ^ [X6: a] : X6 ) )
=> ( X5 @ X4 ) ) )
=> ! [X5: ( a > a ) > $o] :
( ( ( X5
@ ^ [X6: a] : X6 )
& ! [X7: a > a] :
( ( X5 @ X7 )
=> ( X5
@ ^ [X1: a] : ( X2 @ ( X7 @ X1 ) ) ) ) )
=> ( X5
@ ^ [X1: a] : ( X3 @ ( X4 @ X1 ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ( ! [X0: a > a] :
( X0
= ( ^ [X1: a] : ( X0 @ X1 ) ) )
=> ! [X2: a > a,X3: a > a,X4: a > a] :
( ( ! [X5: ( a > a ) > $o] :
( ( ! [X6: a > a] :
( ( X5 @ X6 )
=> ( X5
@ ^ [X7: a] : ( X4 @ ( X6 @ X7 ) ) ) )
& ( X5
@ ^ [X8: a] : X8 ) )
=> ( X5 @ X2 ) )
& ! [X9: ( a > a ) > $o] :
( ( ! [X10: a > a] :
( ( X9 @ X10 )
=> ( X9
@ ^ [X11: a] : ( X4 @ ( X10 @ X11 ) ) ) )
& ( X9
@ ^ [X12: a] : X12 ) )
=> ( X9 @ X3 ) ) )
=> ! [X13: ( a > a ) > $o] :
( ( ( X13
@ ^ [X14: a] : X14 )
& ! [X15: a > a] :
( ( X13 @ X15 )
=> ( X13
@ ^ [X16: a] : ( X4 @ ( X15 @ X16 ) ) ) ) )
=> ( X13
@ ^ [X17: a] : ( X2 @ ( X3 @ X17 ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
( $true
= ( ~ ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( Y0
= ( ^ [Y1: a] : ( Y0 @ Y1 ) ) ) )
=> ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( $true
= ( ~ ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( Y0
= ( ^ [Y1: a] : ( Y0 @ Y1 ) ) ) )
=> ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f4]) ).
thf(f8,plain,
( ( ~ ( ( !! @ ( a > a )
@ ^ [Y0: a > a] : ( Y0 = Y0 ) )
=> ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f5]) ).
thf(f9,plain,
( $true
= ( ~ ( ( !! @ ( a > a )
@ ^ [Y0: a > a] : $true )
=> ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) ) ),
inference(boolean_simplification,[],[f8]) ).
thf(f10,plain,
( $false
= ( ( !! @ ( a > a )
@ ^ [Y0: a > a] : $true )
=> ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f9]) ).
thf(f11,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f10]) ).
thf(f22,plain,
( $false
= ( ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( Y3
@ ^ [Y4: a] : Y4 )
& ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) ) )
=> ( Y3 @ Y2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3
@ ^ [Y4: a] : Y4 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y2 @ ( Y1 @ Y4 ) ) ) ) ) ) ) )
@ sK0 ) ),
inference(sigma_proxy_clausification,[],[f11]) ).
thf(f24,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2
@ ^ [Y3: a] : Y3 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2 @ Y0 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2
@ ^ [Y3: a] : Y3 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : Y3 ) )
=> ( Y2
@ ^ [Y3: a] : ( Y1 @ ( Y0 @ Y3 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f22]) ).
thf(f26,plain,
( $false
= ( ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2
@ ^ [Y3: a] : Y3 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2 @ Y0 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( Y2
@ ^ [Y3: a] : Y3 )
& ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) ) )
=> ( Y2 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : Y3 ) )
=> ( Y2
@ ^ [Y3: a] : ( Y1 @ ( Y0 @ Y3 ) ) ) ) ) ) )
@ sK1 ) ),
inference(sigma_proxy_clausification,[],[f24]) ).
thf(f28,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1
@ ^ [Y2: a] : Y2 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1 @ sK1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1
@ ^ [Y2: a] : Y2 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1
@ ^ [Y2: a] : Y2 ) )
=> ( Y1
@ ^ [Y2: a] : ( Y0 @ ( sK1 @ Y2 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f26]) ).
thf(f30,plain,
( $false
= ( ^ [Y0: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1
@ ^ [Y2: a] : Y2 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1 @ sK1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( Y1
@ ^ [Y2: a] : Y2 )
& ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) ) )
=> ( Y1 @ Y0 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1
@ ^ [Y2: a] : Y2 ) )
=> ( Y1
@ ^ [Y2: a] : ( Y0 @ ( sK1 @ Y2 ) ) ) ) ) )
@ sK2 ) ),
inference(sigma_proxy_clausification,[],[f28]) ).
thf(f33,plain,
( $false
= ( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK2 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0
@ ^ [Y1: a] : Y1 ) )
=> ( Y0
@ ^ [Y1: a] : ( sK2 @ ( sK1 @ Y1 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f30]) ).
thf(f34,plain,
( $false
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0
@ ^ [Y1: a] : Y1 ) )
=> ( Y0
@ ^ [Y1: a] : ( sK2 @ ( sK1 @ Y1 ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f33]) ).
thf(f35,plain,
( $true
= ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK2 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f33]) ).
thf(f36,plain,
( $true
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK2 ) ) ) ),
inference(and_proxy_clausification,[],[f35]) ).
thf(f37,plain,
( $true
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK1 ) ) ) ),
inference(and_proxy_clausification,[],[f35]) ).
thf(f38,plain,
! [X1: ( a > a ) > $o] :
( $true
= ( ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK2 ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f36]) ).
thf(f39,plain,
! [X1: ( a > a ) > $o] :
( $true
= ( ( ( X1
@ ^ [Y0: a] : Y0 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
=> ( X1 @ sK2 ) ) ),
inference(beta-eta_normalization,[],[f38]) ).
thf(f40,plain,
! [X1: ( a > a ) > $o] :
( ( $true
= ( X1 @ sK2 ) )
| ( $false
= ( ( X1
@ ^ [Y0: a] : Y0 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f39]) ).
thf(f41,plain,
! [X1: ( a > a ) > $o] :
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $true
= ( X1 @ sK2 ) )
| ( $false
= ( X1
@ ^ [Y0: a] : Y0 ) ) ),
inference(and_proxy_clausification,[],[f40]) ).
thf(f42,plain,
( $false
= ( ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0
@ ^ [Y1: a] : Y1 ) )
=> ( Y0
@ ^ [Y1: a] : ( sK2 @ ( sK1 @ Y1 ) ) ) )
@ sK3 ) ),
inference(sigma_proxy_clausification,[],[f34]) ).
thf(f44,plain,
( $false
= ( ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( sK3
@ ^ [Y0: a] : Y0 ) )
=> ( sK3
@ ^ [Y0: a] : ( sK2 @ ( sK1 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f42]) ).
thf(f46,plain,
( $false
= ( sK3
@ ^ [Y0: a] : ( sK2 @ ( sK1 @ Y0 ) ) ) ),
inference(imp_proxy_clausification,[],[f44]) ).
thf(f47,plain,
( $true
= ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( sK3
@ ^ [Y0: a] : Y0 ) ) ),
inference(imp_proxy_clausification,[],[f44]) ).
thf(f48,plain,
( $true
= ( sK3
@ ^ [Y0: a] : Y0 ) ),
inference(and_proxy_clausification,[],[f47]) ).
thf(f49,plain,
( $true
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f47]) ).
thf(f52,plain,
! [X1: a > a] :
( $true
= ( ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f49]) ).
thf(f53,plain,
! [X1: a > a] :
( $true
= ( ( sK3 @ X1 )
=> ( sK3
@ ^ [Y0: a] : ( sK0 @ ( X1 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f52]) ).
thf(f54,plain,
! [X1: a > a] :
( ( $true
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( X1 @ Y0 ) ) ) )
| ( $false
= ( sK3 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f53]) ).
thf(f70,plain,
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ^ [Y1: a > a] :
( sK3
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK1
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ Y0 )
=> ( ^ [Y1: a > a] :
( sK3
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK1
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $false = $true )
| ( $false
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] :
( sK1
@ ( ^ [Y5: a > a,Y6: a] : Y6
@ Y3
@ Y4 ) )
@ Y1
@ Y2 ) )
@ Y0 ) )
@ ^ [Y0: a] : Y0 ) ) ),
inference(constrained_superposition,[],[f41,f46]) ).
thf(f133,plain,
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ^ [Y1: a > a] :
( sK3
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK1
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ Y0 )
=> ( ^ [Y1: a > a] :
( sK3
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK1
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $false
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] :
( sK1
@ ( ^ [Y5: a > a,Y6: a] : Y6
@ Y3
@ Y4 ) )
@ Y1
@ Y2 ) )
@ Y0 ) )
@ ^ [Y0: a] : Y0 ) ) ),
inference(trivial_inequality_removal,[],[f70]) ).
thf(f134,plain,
( ( $false
= ( sK3 @ sK1 ) )
| ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK1 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK1 @ Y1 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f133]) ).
thf(f153,definition,
( spl5_3
<=> ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK1 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK1 @ Y1 ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
thf(f155,plain,
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK1 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK1 @ Y1 ) ) ) ) ) ) )
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f153]) ).
thf(f157,definition,
( spl5_4
<=> ( $false
= ( sK3 @ sK1 ) ) ),
introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).
thf(f159,plain,
( ( $false
= ( sK3 @ sK1 ) )
| ~ spl5_4 ),
inference(avatar_component_clause,[],[f157]) ).
thf(f170,plain,
( spl5_3
| spl5_4 ),
inference(avatar_split_clause,[],[f134,f157,f153]) ).
thf(f175,plain,
! [X1: ( a > a ) > $o] :
( ( ^ [Y0: ( a > a ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : Y1 )
& ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) ) )
=> ( Y0 @ sK1 ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f37]) ).
thf(f176,plain,
! [X1: ( a > a ) > $o] :
( ( ( ( X1
@ ^ [Y0: a] : Y0 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
=> ( X1 @ sK1 ) )
= $true ),
inference(beta-eta_normalization,[],[f175]) ).
thf(f177,plain,
! [X1: ( a > a ) > $o] :
( ( $true
= ( X1 @ sK1 ) )
| ( $false
= ( ( X1
@ ^ [Y0: a] : Y0 )
& ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f176]) ).
thf(f178,plain,
! [X1: ( a > a ) > $o] :
( ( $true
= ( X1 @ sK1 ) )
| ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $false
= ( X1
@ ^ [Y0: a] : Y0 ) ) ),
inference(and_proxy_clausification,[],[f177]) ).
thf(f185,plain,
( ( $false
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ ^ [Y0: a] : Y0 ) )
| ( $false = $true )
| ( $true
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK1 ) ) ),
inference(constrained_superposition,[],[f178,f49]) ).
thf(f219,plain,
( ( $false
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ ^ [Y0: a] : Y0 ) )
| ( $true
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK1 ) ) ),
inference(trivial_inequality_removal,[],[f185]) ).
thf(f220,plain,
( ( ( sK3 @ sK1 )
= $true )
| ( $false
= ( sK3
@ ^ [Y0: a] : Y0 ) ) ),
inference(beta-eta_normalization,[],[f219]) ).
thf(f262,plain,
( ( ( sK3 @ sK1 )
= $true )
| ( $false = $true ) ),
inference(forward_demodulation,[],[f220,f48]) ).
thf(f263,plain,
( ( sK3 @ sK1 )
= $true ),
inference(trivial_inequality_removal,[],[f262]) ).
thf(f293,plain,
( ( $false
= ( ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK1 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK1 @ Y1 ) ) ) ) )
@ sK6 ) )
| ~ spl5_3 ),
inference(sigma_proxy_clausification,[],[f155]) ).
thf(f296,plain,
( ( $false
= ( ( sK3
@ ^ [Y0: a] : ( sK6 @ ( sK1 @ Y0 ) ) )
=> ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK6 @ ( sK1 @ Y0 ) ) ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f293]) ).
thf(f297,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK6 @ ( sK1 @ Y0 ) ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f296]) ).
thf(f298,plain,
( ( $true
= ( sK3
@ ^ [Y0: a] : ( sK6 @ ( sK1 @ Y0 ) ) ) )
| ~ spl5_3 ),
inference(imp_proxy_clausification,[],[f296]) ).
thf(f307,plain,
( ( $false = $true )
| ( $false
= ( sK3
@ ^ [Y0: a] :
( sK6
@ ( ^ [Y1: a] :
( sK1
@ ( ^ [Y2: a] : Y2
@ Y1 ) )
@ Y0 ) ) ) )
| ~ spl5_3 ),
inference(constrained_superposition,[],[f54,f297]) ).
thf(f308,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] :
( sK6
@ ( ^ [Y1: a] :
( sK1
@ ( ^ [Y2: a] : Y2
@ Y1 ) )
@ Y0 ) ) ) )
| ~ spl5_3 ),
inference(trivial_inequality_removal,[],[f307]) ).
thf(f309,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] : ( sK6 @ ( sK1 @ Y0 ) ) ) )
| ~ spl5_3 ),
inference(beta-eta_normalization,[],[f308]) ).
thf(f314,plain,
( ( $false = $true )
| ~ spl5_3 ),
inference(backward_demodulation,[],[f298,f309]) ).
thf(f317,plain,
( $false
| ~ spl5_3 ),
inference(trivial_inequality_removal,[],[f314]) ).
thf(f318,plain,
~ spl5_3,
inference(avatar_contradiction_clause,[],[f317]) ).
thf(f515,plain,
( ( $false = $true )
| ~ spl5_4 ),
inference(forward_demodulation,[],[f263,f159]) ).
thf(f516,plain,
( $false
| ~ spl5_4 ),
inference(trivial_inequality_removal,[],[f515]) ).
thf(f517,plain,
~ spl5_4,
inference(avatar_contradiction_clause,[],[f516]) ).
cnf(s4,plain,
( spl5_3
| spl5_4 ),
inference(sat_conversion,[],[f170]) ).
cnf(s7,plain,
~ spl5_3,
inference(sat_conversion,[],[f318]) ).
cnf(s11,plain,
~ spl5_4,
inference(sat_conversion,[],[f517]) ).
cnf(s12,plain,
$false,
inference(rat,[],[s4,s11,s7]) ).
thf(f518,plain,
$false,
inference(avatar_sat_refutation,[],[s12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU968^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.16 % Computer : n007.cluster.edu
% 0.07/0.16 % Model : x86_64 x86_64
% 0.07/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.16 % Memory : 8046.5625MB
% 0.07/0.16 % OS : Linux 6.8.0-71-generic
% 0.07/0.16 % CPULimit : 300
% 0.07/0.16 % WCLimit : 300
% 0.07/0.16 % DateTime : Tue Sep 29 14:52:39 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 Running higher-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.31 % (3462881)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.19/0.31 % (3462891)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=110889574:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.19/0.31 % (3462892)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.19/0.31 % (3462892)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.19/0.31 % (3462886)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3794604705:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.19/0.31 % (3462887)lrs+10_16_si=on:nwc=1.5:random_seed=3225585737:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.19/0.31 % (3462888)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2324095200:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.19/0.31 % (3462890)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2311641350:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.19/0.31 % (3462889)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=1578941083: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.19/0.31 % (3462892)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=811469695:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.19/0.31 % (3462888)Instruction limit reached!
% 0.19/0.31 % (3462888)------------------------------
% 0.19/0.31 % (3462888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (3462888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (3462888)CaDiCaL version: 2.1.3
% 0.19/0.31 % (3462888)Termination reason: Instruction limit
% 0.19/0.31 % (3462888)Termination phase: Saturation
% 0.19/0.31 % (3462888)Time elapsed: 0.003 s
% 0.19/0.31 % (3462888)Peak memory usage: 12 MB
% 0.19/0.31 % (3462888)Instructions burned: 4 (million)
% 0.19/0.31 % (3462889)Refutation not found, incomplete strategy
% 0.19/0.31 % (3462889)------------------------------
% 0.19/0.31 % (3462889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (3462889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (3462889)CaDiCaL version: 2.1.3
% 0.19/0.31 % (3462889)Termination reason: Refutation not found, incomplete strategy
% 0.19/0.31 % (3462889)Time elapsed: 0.007 s
% 0.19/0.31 % (3462889)Peak memory usage: 12 MB
% 0.19/0.31 % (3462889)Instructions burned: 9 (million)
% 0.19/0.31 % (3462890)Refutation not found, incomplete strategy
% 0.19/0.31 % (3462890)------------------------------
% 0.19/0.31 % (3462890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (3462890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (3462890)CaDiCaL version: 2.1.3
% 0.19/0.31 % (3462890)Termination reason: Refutation not found, incomplete strategy
% 0.19/0.31 % (3462890)Time elapsed: 0.008 s
% 0.19/0.31 % (3462890)Peak memory usage: 12 MB
% 0.19/0.31 % (3462890)Instructions burned: 13 (million)
% 0.19/0.31 % (3462889)------------------------------
% 0.19/0.31 % (3462889)------------------------------
% 0.19/0.31 % (3462890)------------------------------
% 0.19/0.31 % (3462890)------------------------------
% 0.19/0.31 % (3462887)Instruction limit reached!
% 0.19/0.31 % (3462887)------------------------------
% 0.19/0.31 % (3462887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (3462887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (3462887)CaDiCaL version: 2.1.3
% 0.19/0.31 % (3462887)Termination reason: Instruction limit
% 0.19/0.31 % (3462887)Termination phase: Saturation
% 0.19/0.31 % (3462887)Time elapsed: 0.010 s
% 0.19/0.31 % (3462887)Peak memory usage: 12 MB
% 0.19/0.31 % (3462887)Instructions burned: 19 (million)
% 0.19/0.31 % (3462892)Refutation not found, incomplete strategy
% 0.19/0.31 % (3462892)------------------------------
% 0.19/0.31 % (3462892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.34 % (3462892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.34 % (3462892)CaDiCaL version: 2.1.3
% 0.19/0.34 % (3462892)Termination reason: Refutation not found, incomplete strategy
% 0.19/0.34 % (3462892)Time elapsed: 0.013 s
% 0.19/0.34 % (3462892)Peak memory usage: 12 MB
% 0.19/0.34 % (3462892)Instructions burned: 23 (million)
% 0.19/0.34 % (3462891)Instruction limit reached!
% 0.19/0.34 % (3462891)------------------------------
% 0.19/0.34 % (3462891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.34 % (3462891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.34 % (3462891)CaDiCaL version: 2.1.3
% 0.19/0.34 % (3462891)Termination reason: Instruction limit
% 0.19/0.34 % (3462891)Termination phase: Saturation
% 0.19/0.34 % (3462891)Time elapsed: 0.023 s
% 0.19/0.34 % (3462891)Peak memory usage: 12 MB
% 0.19/0.34 % (3462892)------------------------------
% 0.19/0.34 % (3462892)------------------------------
% 0.19/0.34 % (3462891)Instructions burned: 79 (million)
% 0.19/0.34 % (3462900)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=328366709:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.19/0.34 % (3462904)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.19/0.34 % (3462904)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.19/0.34 % (3462902)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.19/0.34 % (3462900)Instruction limit reached!
% 0.19/0.34 % (3462900)------------------------------
% 0.19/0.34 % (3462900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.34 % (3462900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.34 % (3462900)CaDiCaL version: 2.1.3
% 0.19/0.34 % (3462900)Termination reason: Instruction limit
% 0.19/0.34 % (3462900)Termination phase: Saturation
% 0.19/0.34 % (3462900)Time elapsed: 0.002 s
% 0.19/0.34 % (3462900)Peak memory usage: 12 MB
% 0.19/0.34 % (3462900)Instructions burned: 2 (million)
% 0.19/0.34 % (3462904)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=49733225: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.19/0.34 % (3462901)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1091759733:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.19/0.34 % (3462902)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2718868007:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.19/0.34 % (3462903)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2281306065:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.19/0.34 % (3462901)Instruction limit reached!
% 0.19/0.34 % (3462901)------------------------------
% 0.19/0.34 % (3462901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.34 % (3462901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.34 % (3462901)CaDiCaL version: 2.1.3
% 0.19/0.34 % (3462901)Termination reason: Instruction limit
% 0.19/0.34 % (3462901)Termination phase: Saturation
% 0.19/0.34 % (3462901)Time elapsed: 0.004 s
% 0.19/0.34 % (3462901)Peak memory usage: 12 MB
% 0.19/0.34 % (3462901)Instructions burned: 6 (million)
% 0.19/0.34 % (3462902)Instruction limit reached!
% 0.19/0.34 % (3462902)------------------------------
% 0.19/0.34 % (3462902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.34 % (3462902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.34 % (3462902)CaDiCaL version: 2.1.3
% 0.19/0.34 % (3462902)Termination reason: Instruction limit
% 0.19/0.34 % (3462902)Termination phase: Saturation
% 0.19/0.34 % (3462902)Time elapsed: 0.004 s
% 0.19/0.34 % (3462902)Peak memory usage: 12 MB
% 0.19/0.34 % (3462902)Instructions burned: 7 (million)
% 0.19/0.34 % (3462905)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=2711251655:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.19/0.36 % (3462904)Instruction limit reached!
% 0.19/0.36 % (3462904)------------------------------
% 0.19/0.36 % (3462904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3462904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3462904)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3462904)Termination reason: Instruction limit
% 0.19/0.36 % (3462904)Termination phase: Saturation
% 0.19/0.36 % (3462904)Time elapsed: 0.008 s
% 0.19/0.36 % (3462904)Peak memory usage: 12 MB
% 0.19/0.36 % (3462904)Instructions burned: 31 (million)
% 0.19/0.36 % (3462903)Instruction limit reached!
% 0.19/0.36 % (3462903)------------------------------
% 0.19/0.36 % (3462903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3462903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3462903)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3462903)Termination reason: Instruction limit
% 0.19/0.36 % (3462903)Termination phase: Saturation
% 0.19/0.36 % (3462903)Time elapsed: 0.007 s
% 0.19/0.36 % (3462903)Peak memory usage: 12 MB
% 0.19/0.36 % (3462903)Instructions burned: 13 (million)
% 0.19/0.36 % (3462886)Instruction limit reached!
% 0.19/0.36 % (3462886)------------------------------
% 0.19/0.36 % (3462886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3462886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3462886)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3462886)Termination reason: Instruction limit
% 0.19/0.36 % (3462886)Termination phase: Saturation
% 0.19/0.36 % (3462886)Time elapsed: 0.044 s
% 0.19/0.36 % (3462886)Peak memory usage: 12 MB
% 0.19/0.36 % (3462886)Instructions burned: 89 (million)
% 0.19/0.36 % (3462907)lrs+10_1_si=on:cs=on:random_seed=224978331:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.19/0.36 % (3462915)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=141144407:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.19/0.36 % (3462912)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.19/0.36 % (3462907)Instruction limit reached!
% 0.19/0.36 % (3462907)------------------------------
% 0.19/0.36 % (3462907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3462907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3462907)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3462907)Termination reason: Instruction limit
% 0.19/0.36 % (3462907)Termination phase: Saturation
% 0.19/0.36 % (3462907)Time elapsed: 0.004 s
% 0.19/0.36 % (3462907)Peak memory usage: 12 MB
% 0.19/0.36 % (3462907)Instructions burned: 8 (million)
% 0.19/0.36 % (3462915)Refutation not found, incomplete strategy
% 0.19/0.36 % (3462915)------------------------------
% 0.19/0.36 % (3462915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3462915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3462915)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3462915)Termination reason: Refutation not found, incomplete strategy
% 0.19/0.36 % (3462915)Time elapsed: 0.003 s
% 0.19/0.36 % (3462915)Peak memory usage: 12 MB
% 0.19/0.36 % (3462915)Instructions burned: 9 (million)
% 0.19/0.36 % (3462915)------------------------------
% 0.19/0.36 % (3462915)------------------------------
% 0.19/0.36 % (3462912)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=4071990981:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.19/0.36 % (3462913)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1880360243:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.19/0.36 % (3462912)Instruction limit reached!
% 0.19/0.36 % (3462912)------------------------------
% 0.19/0.36 % (3462912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3462912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3462912)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3462912)Termination reason: Instruction limit
% 0.19/0.36 % (3462912)Termination phase: Saturation
% 0.19/0.36 % (3462912)Time elapsed: 0.002 s
% 0.19/0.36 % (3462912)Peak memory usage: 11 MB
% 0.19/0.36 % (3462912)Instructions burned: 3 (million)
% 0.94/0.38 % (3462916)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3762915251:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.94/0.38 % (3462916)Refutation not found, incomplete strategy
% 0.94/0.38 % (3462916)------------------------------
% 0.94/0.38 % (3462916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.38 % (3462916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.38 % (3462916)CaDiCaL version: 2.1.3
% 0.94/0.38 % (3462916)Termination reason: Refutation not found, incomplete strategy
% 0.94/0.38 % (3462916)Time elapsed: 0.002 s
% 0.94/0.38 % (3462916)Peak memory usage: 12 MB
% 0.94/0.38 % (3462916)Instructions burned: 2 (million)
% 0.94/0.38 % (3462921)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=712374002:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.94/0.38 % (3462916)------------------------------
% 0.94/0.38 % (3462916)------------------------------
% 0.94/0.38 % (3462918)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=4272774702:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.94/0.38 % (3462921)Instruction limit reached!
% 0.94/0.38 % (3462921)------------------------------
% 0.94/0.38 % (3462921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.38 % (3462921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.38 % (3462921)CaDiCaL version: 2.1.3
% 0.94/0.38 % (3462921)Termination reason: Instruction limit
% 0.94/0.38 % (3462921)Termination phase: Saturation
% 0.94/0.38 % (3462921)Time elapsed: 0.005 s
% 0.94/0.38 % (3462921)Peak memory usage: 12 MB
% 0.94/0.38 % (3462921)Instructions burned: 17 (million)
% 0.94/0.38 % (3462920)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=171632511:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.94/0.38 % (3462905)Instruction limit reached!
% 0.94/0.38 % (3462905)------------------------------
% 0.94/0.38 % (3462905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.38 % (3462905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.38 % (3462905)CaDiCaL version: 2.1.3
% 0.94/0.38 % (3462905)Termination reason: Instruction limit
% 0.94/0.38 % (3462905)Termination phase: Saturation
% 0.94/0.38 % (3462905)Time elapsed: 0.037 s
% 0.94/0.38 % (3462905)Peak memory usage: 12 MB
% 0.94/0.38 % (3462905)Instructions burned: 87 (million)
% 0.94/0.38 % (3462924)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2539330589: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.94/0.38 % (3462918)Instruction limit reached!
% 0.94/0.38 % (3462918)------------------------------
% 0.94/0.38 % (3462918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.38 % (3462918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.38 % (3462918)CaDiCaL version: 2.1.3
% 0.94/0.38 % (3462918)Termination reason: Instruction limit
% 0.94/0.38 % (3462918)Termination phase: Saturation
% 0.94/0.38 % (3462918)Time elapsed: 0.012 s
% 0.94/0.38 % (3462918)Peak memory usage: 12 MB
% 0.94/0.38 % (3462918)Instructions burned: 19 (million)
% 0.94/0.38 % (3462913)Instruction limit reached!
% 0.94/0.38 % (3462913)------------------------------
% 0.94/0.38 % (3462913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.38 % (3462913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.38 % (3462913)CaDiCaL version: 2.1.3
% 0.94/0.38 % (3462913)Termination reason: Instruction limit
% 0.94/0.38 % (3462913)Termination phase: Saturation
% 0.94/0.38 % (3462913)Time elapsed: 0.023 s
% 0.94/0.38 % (3462913)Peak memory usage: 12 MB
% 0.94/0.38 % (3462913)Instructions burned: 41 (million)
% 0.94/0.38 % (3462929)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1208957038:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.94/0.38 % (3462924)Instruction limit reached!
% 0.94/0.38 % (3462924)------------------------------
% 0.94/0.38 % (3462924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.38 % (3462924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.38 % (3462924)CaDiCaL version: 2.1.3
% 0.94/0.43 % (3462924)Termination reason: Instruction limit
% 0.94/0.43 % (3462924)Termination phase: Saturation
% 0.94/0.43 % (3462924)Time elapsed: 0.005 s
% 0.94/0.43 % (3462924)Peak memory usage: 12 MB
% 0.94/0.43 % (3462924)Instructions burned: 8 (million)
% 0.94/0.43 % (3462927)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1787584312:i=26:ep=R:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/26Mi)
% 0.94/0.43 % (3462929)Instruction limit reached!
% 0.94/0.43 % (3462929)------------------------------
% 0.94/0.43 % (3462929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.43 % (3462929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.43 % (3462929)CaDiCaL version: 2.1.3
% 0.94/0.43 % (3462929)Termination reason: Instruction limit
% 0.94/0.43 % (3462929)Termination phase: Saturation
% 0.94/0.43 % (3462929)Time elapsed: 0.007 s
% 0.94/0.43 % (3462929)Peak memory usage: 11 MB
% 0.94/0.43 % (3462929)Instructions burned: 24 (million)
% 0.94/0.43 % (3462927)Refutation not found, incomplete strategy
% 0.94/0.43 % (3462927)------------------------------
% 0.94/0.43 % (3462927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.43 % (3462927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.43 % (3462927)CaDiCaL version: 2.1.3
% 0.94/0.43 % (3462927)Termination reason: Refutation not found, incomplete strategy
% 0.94/0.43 % (3462927)Time elapsed: 0.005 s
% 0.94/0.43 % (3462927)Peak memory usage: 12 MB
% 0.94/0.43 % (3462927)Instructions burned: 8 (million)
% 0.94/0.43 % (3462927)------------------------------
% 0.94/0.43 % (3462927)------------------------------
% 0.94/0.43 % (3462933)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.94/0.43 % (3462933)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.94/0.43 % (3462935)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.94/0.43 % (3462932)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2923853525:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.94/0.43 % (3462938)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=297572012:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.94/0.43 % (3462933)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=114898165:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.94/0.43 % (3462935)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=1916646140:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.94/0.43 % (3462938)Instruction limit reached!
% 0.94/0.43 % (3462938)------------------------------
% 0.94/0.43 % (3462938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.43 % (3462938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.43 % (3462938)CaDiCaL version: 2.1.3
% 0.94/0.43 % (3462938)Termination reason: Instruction limit
% 0.94/0.43 % (3462938)Termination phase: Saturation
% 0.94/0.43 % (3462938)Time elapsed: 0.003 s
% 0.94/0.43 % (3462938)Peak memory usage: 12 MB
% 0.94/0.43 % (3462938)Instructions burned: 12 (million)
% 0.94/0.43 % (3462936)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=4214476331:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.94/0.43 % (3462935)Instruction limit reached!
% 0.94/0.43 % (3462935)------------------------------
% 0.94/0.43 % (3462935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.43 % (3462935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.43 % (3462935)CaDiCaL version: 2.1.3
% 0.94/0.43 % (3462935)Termination reason: Instruction limit
% 0.94/0.43 % (3462935)Termination phase: Saturation
% 0.94/0.43 % (3462935)Time elapsed: 0.006 s
% 0.94/0.43 % (3462935)Peak memory usage: 12 MB
% 0.94/0.43 % (3462935)Instructions burned: 9 (million)
% 0.94/0.43 % (3462932)Refutation not found, incomplete strategy
% 1.73/0.48 % (3462932)------------------------------
% 1.73/0.48 % (3462932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.48 % (3462932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.48 % (3462932)CaDiCaL version: 2.1.3
% 1.73/0.48 % (3462932)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.48 % (3462932)Time elapsed: 0.009 s
% 1.73/0.48 % (3462932)Peak memory usage: 12 MB
% 1.73/0.48 % (3462932)Instructions burned: 13 (million)
% 1.73/0.48 % (3462932)------------------------------
% 1.73/0.48 % (3462932)------------------------------
% 1.73/0.48 % (3462933)Instruction limit reached!
% 1.73/0.48 % (3462933)------------------------------
% 1.73/0.48 % (3462933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.48 % (3462933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.48 % (3462933)CaDiCaL version: 2.1.3
% 1.73/0.48 % (3462933)Termination reason: Instruction limit
% 1.73/0.48 % (3462933)Termination phase: Saturation
% 1.73/0.48 % (3462933)Time elapsed: 0.009 s
% 1.73/0.48 % (3462933)Peak memory usage: 12 MB
% 1.73/0.48 % (3462933)Instructions burned: 14 (million)
% 1.73/0.48 % (3462939)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1584210359:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.73/0.48 % (3462944)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2554168233:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.73/0.48 % (3462936)Instruction limit reached!
% 1.73/0.48 % (3462936)------------------------------
% 1.73/0.48 % (3462936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.48 % (3462936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.48 % (3462936)CaDiCaL version: 2.1.3
% 1.73/0.48 % (3462936)Termination reason: Instruction limit
% 1.73/0.48 % (3462936)Termination phase: Saturation
% 1.73/0.48 % (3462936)Time elapsed: 0.015 s
% 1.73/0.48 % (3462936)Peak memory usage: 12 MB
% 1.73/0.48 % (3462936)Instructions burned: 31 (million)
% 1.73/0.48 % (3462944)Instruction limit reached!
% 1.73/0.48 % (3462944)------------------------------
% 1.73/0.48 % (3462944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.48 % (3462944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.48 % (3462944)CaDiCaL version: 2.1.3
% 1.73/0.48 % (3462944)Termination reason: Instruction limit
% 1.73/0.48 % (3462944)Termination phase: Saturation
% 1.73/0.48 % (3462944)Time elapsed: 0.006 s
% 1.73/0.48 % (3462944)Peak memory usage: 12 MB
% 1.73/0.48 % (3462944)Instructions burned: 20 (million)
% 1.73/0.48 % (3462939)Instruction limit reached!
% 1.73/0.48 % (3462939)------------------------------
% 1.73/0.48 % (3462939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.48 % (3462939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.48 % (3462939)CaDiCaL version: 2.1.3
% 1.73/0.48 % (3462939)Termination reason: Instruction limit
% 1.73/0.48 % (3462939)Termination phase: Saturation
% 1.73/0.48 % (3462939)Time elapsed: 0.009 s
% 1.73/0.48 % (3462939)Peak memory usage: 11 MB
% 1.73/0.48 % (3462939)Instructions burned: 23 (million)
% 1.73/0.48 % (3462946)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=96915363:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.73/0.48 % (3462947)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2002413196:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.73/0.48 % (3462952)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.73/0.48 % (3462948)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2721220136:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.73/0.48 % (3462952)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3864018848:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.73/0.48 % (3462952)Instruction limit reached!
% 1.73/0.48 % (3462952)------------------------------
% 1.73/0.48 % (3462952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.48 % (3462952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.52 % (3462952)CaDiCaL version: 2.1.3
% 1.73/0.52 % (3462952)Termination reason: Instruction limit
% 1.73/0.52 % (3462952)Termination phase: Saturation
% 1.73/0.52 % (3462952)Time elapsed: 0.002 s
% 1.73/0.52 % (3462952)Peak memory usage: 12 MB
% 1.73/0.52 % (3462952)Instructions burned: 7 (million)
% 1.73/0.52 % (3462948)Refutation not found, incomplete strategy
% 1.73/0.52 % (3462948)------------------------------
% 1.73/0.52 % (3462948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.52 % (3462948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.52 % (3462948)CaDiCaL version: 2.1.3
% 1.73/0.52 % (3462948)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.52 % (3462948)Time elapsed: 0.005 s
% 1.73/0.52 % (3462948)Peak memory usage: 12 MB
% 1.73/0.52 % (3462948)Instructions burned: 8 (million)
% 1.73/0.52 % (3462948)------------------------------
% 1.73/0.52 % (3462948)------------------------------
% 1.73/0.52 % (3462951)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1566516115:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.73/0.52 % (3462953)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1218089780:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.73/0.52 % (3462946)Refutation not found, incomplete strategy
% 1.73/0.52 % (3462946)------------------------------
% 1.73/0.52 % (3462946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.52 % (3462946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.52 % (3462946)CaDiCaL version: 2.1.3
% 1.73/0.52 % (3462946)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.52 % (3462946)Time elapsed: 0.017 s
% 1.73/0.52 % (3462946)Peak memory usage: 12 MB
% 1.73/0.52 % (3462946)Instructions burned: 29 (million)
% 1.73/0.52 % (3462958)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=504823479: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.73/0.52 % (3462946)------------------------------
% 1.73/0.52 % (3462946)------------------------------
% 1.73/0.52 % (3462959)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.73/0.52 % (3462959)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2962265123: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.73/0.52 % (3462959)Instruction limit reached!
% 1.73/0.52 % (3462959)------------------------------
% 1.73/0.52 % (3462959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.52 % (3462959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.52 % (3462959)CaDiCaL version: 2.1.3
% 1.73/0.52 % (3462959)Termination reason: Instruction limit
% 1.73/0.52 % (3462959)Termination phase: Saturation
% 1.73/0.52 % (3462959)Time elapsed: 0.004 s
% 1.73/0.52 % (3462959)Peak memory usage: 12 MB
% 1.73/0.52 % (3462959)Instructions burned: 7 (million)
% 1.73/0.52 % (3462951)Instruction limit reached!
% 1.73/0.52 % (3462951)------------------------------
% 1.73/0.52 % (3462951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.52 % (3462951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.52 % (3462951)CaDiCaL version: 2.1.3
% 1.73/0.52 % (3462951)Termination reason: Instruction limit
% 1.73/0.52 % (3462951)Termination phase: Saturation
% 1.73/0.52 % (3462951)Time elapsed: 0.021 s
% 1.73/0.52 % (3462951)Peak memory usage: 12 MB
% 1.73/0.52 % (3462951)Instructions burned: 43 (million)
% 1.73/0.52 % (3462963)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4285506596:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 1.73/0.52 % (3462963)Instruction limit reached!
% 1.73/0.52 % (3462963)------------------------------
% 1.73/0.52 % (3462963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.52 % (3462963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.52 % (3462963)CaDiCaL version: 2.1.3
% 1.73/0.52 % (3462963)Termination reason: Instruction limit
% 1.73/0.52 % (3462963)Termination phase: Saturation
% 1.73/0.52 % (3462963)Time elapsed: 0.011 s
% 1.73/0.56 % (3462963)Peak memory usage: 12 MB
% 1.73/0.56 % (3462963)Instructions burned: 23 (million)
% 1.73/0.56 % (3462966)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=4197836568:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/316Mi)
% 1.73/0.56 % (3462965)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=429836471:i=19:add=on:rtra=on_2998 on theBenchmark for (2998ds/19Mi)
% 1.73/0.56 % (3462958)Instruction limit reached!
% 1.73/0.56 % (3462958)------------------------------
% 1.73/0.56 % (3462958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.56 % (3462958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.56 % (3462958)CaDiCaL version: 2.1.3
% 1.73/0.56 % (3462958)Termination reason: Instruction limit
% 1.73/0.56 % (3462958)Termination phase: Saturation
% 1.73/0.56 % (3462958)Time elapsed: 0.038 s
% 1.73/0.56 % (3462958)Peak memory usage: 13 MB
% 1.73/0.56 % (3462958)Instructions burned: 173 (million)
% 1.73/0.56 % (3462971)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=767760135: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)
% 1.73/0.56 % (3462968)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=4048785308: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)
% 1.73/0.56 % (3462965)Refutation not found, incomplete strategy
% 1.73/0.56 % (3462965)------------------------------
% 1.73/0.56 % (3462965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.56 % (3462965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.56 % (3462965)CaDiCaL version: 2.1.3
% 1.73/0.56 % (3462965)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.56 % (3462965)Time elapsed: 0.014 s
% 1.73/0.56 % (3462965)Peak memory usage: 13 MB
% 1.73/0.56 % (3462965)Instructions burned: 16 (million)
% 1.73/0.56 % (3462965)------------------------------
% 1.73/0.56 % (3462965)------------------------------
% 1.73/0.56 % (3462947)Instruction limit reached!
% 1.73/0.56 % (3462947)------------------------------
% 1.73/0.56 % (3462947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.56 % (3462947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.56 % (3462947)CaDiCaL version: 2.1.3
% 1.73/0.56 % (3462947)Termination reason: Instruction limit
% 1.73/0.56 % (3462947)Termination phase: Saturation
% 1.73/0.56 % (3462947)Time elapsed: 0.075 s
% 1.73/0.56 % (3462947)Peak memory usage: 13 MB
% 1.73/0.56 % (3462947)Instructions burned: 143 (million)
% 1.73/0.56 % (3462971)Instruction limit reached!
% 1.73/0.56 % (3462971)------------------------------
% 1.73/0.56 % (3462971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.56 % (3462971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.56 % (3462971)CaDiCaL version: 2.1.3
% 1.73/0.56 % (3462971)Termination reason: Instruction limit
% 1.73/0.56 % (3462971)Termination phase: Saturation
% 1.73/0.56 % (3462971)Time elapsed: 0.014 s
% 1.73/0.56 % (3462971)Peak memory usage: 12 MB
% 1.73/0.56 % (3462971)Instructions burned: 49 (million)
% 1.73/0.56 % (3462976)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 1.73/0.56 % (3462974)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1051100528:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 1.73/0.56 % (3462976)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3947376646:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 1.73/0.56 % (3462975)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2885812236: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)
% 1.73/0.56 % (3462920)Instruction limit reached!
% 1.73/0.56 % (3462920)------------------------------
% 1.73/0.56 % (3462920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.63 % (3462920)CaDiCaL version: 2.1.3
% 2.58/0.63 % (3462920)Termination reason: Instruction limit
% 2.58/0.63 % (3462920)Termination phase: Saturation
% 2.58/0.63 % (3462920)Time elapsed: 0.154 s
% 2.58/0.63 % (3462920)Peak memory usage: 13 MB
% 2.58/0.63 % (3462920)Instructions burned: 327 (million)
% 2.58/0.63 % (3462974)Refutation not found, incomplete strategy
% 2.58/0.63 % (3462974)------------------------------
% 2.58/0.63 % (3462974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.63 % (3462974)CaDiCaL version: 2.1.3
% 2.58/0.63 % (3462974)Termination reason: Refutation not found, incomplete strategy
% 2.58/0.63 % (3462974)Time elapsed: 0.015 s
% 2.58/0.63 % (3462974)Peak memory usage: 12 MB
% 2.58/0.63 % (3462974)Instructions burned: 21 (million)
% 2.58/0.63 % (3462974)------------------------------
% 2.58/0.63 % (3462974)------------------------------
% 2.58/0.63 % (3462953)Instruction limit reached!
% 2.58/0.63 % (3462953)------------------------------
% 2.58/0.63 % (3462953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.63 % (3462953)CaDiCaL version: 2.1.3
% 2.58/0.63 % (3462953)Termination reason: Instruction limit
% 2.58/0.63 % (3462953)Termination phase: Saturation
% 2.58/0.63 % (3462953)Time elapsed: 0.093 s
% 2.58/0.63 % (3462953)Peak memory usage: 13 MB
% 2.58/0.63 % (3462953)Instructions burned: 183 (million)
% 2.58/0.63 % (3462975)Instruction limit reached!
% 2.58/0.63 % (3462975)------------------------------
% 2.58/0.63 % (3462975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.63 % (3462975)CaDiCaL version: 2.1.3
% 2.58/0.63 % (3462975)Termination reason: Instruction limit
% 2.58/0.63 % (3462975)Termination phase: Saturation
% 2.58/0.63 % (3462975)Time elapsed: 0.014 s
% 2.58/0.63 % (3462975)Peak memory usage: 12 MB
% 2.58/0.63 % (3462975)Instructions burned: 23 (million)
% 2.58/0.63 % (3462980)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1427906272:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.58/0.63 % (3462982)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=437560300:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.58/0.63 % (3462983)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2149094943:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 2.58/0.63 % (3462984)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=679935780:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.58/0.63 % (3462980)Instruction limit reached!
% 2.58/0.63 % (3462980)------------------------------
% 2.58/0.63 % (3462980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.63 % (3462980)CaDiCaL version: 2.1.3
% 2.58/0.63 % (3462980)Termination reason: Instruction limit
% 2.58/0.63 % (3462980)Termination phase: Saturation
% 2.58/0.63 % (3462980)Time elapsed: 0.008 s
% 2.58/0.63 % (3462980)Peak memory usage: 12 MB
% 2.58/0.63 % (3462980)Instructions burned: 13 (million)
% 2.58/0.63 % (3462984)Refutation not found, incomplete strategy
% 2.58/0.63 % (3462984)------------------------------
% 2.58/0.63 % (3462984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.63 % (3462984)CaDiCaL version: 2.1.3
% 2.58/0.63 % (3462984)Termination reason: Refutation not found, incomplete strategy
% 2.58/0.63 % (3462984)Time elapsed: 0.004 s
% 2.58/0.63 % (3462984)Peak memory usage: 12 MB
% 2.58/0.63 % (3462984)Instructions burned: 8 (million)
% 2.58/0.63 % (3462984)------------------------------
% 2.58/0.63 % (3462984)------------------------------
% 2.58/0.63 % (3462976)Instruction limit reached!
% 2.58/0.63 % (3462976)------------------------------
% 2.58/0.63 % (3462976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.63 % (3462976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.74/0.79 % (3462976)CaDiCaL version: 2.1.3
% 2.74/0.79 % (3462976)Termination reason: Instruction limit
% 2.74/0.79 % (3462976)Termination phase: Saturation
% 2.74/0.79 % (3462976)Time elapsed: 0.050 s
% 2.74/0.79 % (3462976)Peak memory usage: 12 MB
% 2.74/0.79 % (3462976)Instructions burned: 204 (million)
% 2.74/0.79 % (3462989)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2300341000:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2997 on theBenchmark for (2997ds/137Mi)
% 2.74/0.79 % (3462990)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=66254403:cond=on:i=34:hud=10:nm=10:rtra=on_2997 on theBenchmark for (2997ds/34Mi)
% 2.74/0.79 % (3462991)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1234861609:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/67Mi)
% 2.74/0.79 % (3462983)Instruction limit reached!
% 2.74/0.79 % (3462983)------------------------------
% 2.74/0.79 % (3462983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.74/0.79 % (3462983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.74/0.79 % (3462983)CaDiCaL version: 2.1.3
% 2.74/0.79 % (3462983)Termination reason: Instruction limit
% 2.74/0.79 % (3462983)Termination phase: Saturation
% 2.74/0.79 % (3462983)Time elapsed: 0.028 s
% 2.74/0.79 % (3462983)Peak memory usage: 12 MB
% 2.74/0.79 % (3462983)Instructions burned: 52 (million)
% 2.74/0.79 % (3462982)Instruction limit reached!
% 2.74/0.79 % (3462982)------------------------------
% 2.74/0.79 % (3462982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.74/0.79 % (3462989)Refutation not found, incomplete strategy
% 2.74/0.79 % (3462989)------------------------------
% 2.74/0.79 % (3462989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.74/0.79 % (3462989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.74/0.79 % (3462982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.74/0.79 % (3462982)CaDiCaL version: 2.1.3
% 2.74/0.79 % (3462982)Termination reason: Instruction limit
% 2.74/0.79 % (3462982)Termination phase: Saturation
% 2.74/0.79 % (3462982)Time elapsed: 0.035 s
% 2.74/0.79 % (3462989)CaDiCaL version: 2.1.3
% 2.74/0.79 % (3462982)Peak memory usage: 13 MB
% 2.74/0.79 % (3462989)Termination reason: Refutation not found, incomplete strategy
% 2.74/0.79 % (3462989)Time elapsed: 0.014 s
% 2.74/0.79 % (3462982)Instructions burned: 66 (million)
% 2.74/0.79 % (3462989)Peak memory usage: 12 MB
% 2.74/0.79 % (3462989)Instructions burned: 23 (million)
% 2.74/0.79 % (3462989)------------------------------
% 2.74/0.79 % (3462989)------------------------------
% 2.74/0.79 % (3462990)Refutation not found, incomplete strategy
% 2.74/0.79 % (3462990)------------------------------
% 2.74/0.79 % (3462990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.74/0.79 % (3462990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.74/0.79 % (3462990)CaDiCaL version: 2.1.3
% 2.74/0.79 % (3462990)Termination reason: Refutation not found, incomplete strategy
% 2.74/0.79 % (3462990)Time elapsed: 0.013 s
% 2.74/0.79 % (3462990)Peak memory usage: 12 MB
% 2.74/0.79 % (3462990)Instructions burned: 24 (million)
% 2.74/0.79 % (3462990)------------------------------
% 2.74/0.79 % (3462990)------------------------------
% 2.74/0.79 % (3462996)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.74/0.79 % (3462991)Instruction limit reached!
% 2.74/0.79 % (3462991)------------------------------
% 2.74/0.79 % (3462991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.74/0.79 % (3462991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.74/0.79 % (3462991)CaDiCaL version: 2.1.3
% 2.74/0.79 % (3462991)Termination reason: Instruction limit
% 2.74/0.79 % (3462991)Termination phase: Saturation
% 2.74/0.79 % (3462991)Time elapsed: 0.020 s
% 2.74/0.79 % (3462991)Peak memory usage: 12 MB
% 2.74/0.79 % (3462991)Instructions burned: 71 (million)
% 2.74/0.79 % (3462996)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3186316315:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 2.74/0.79 % (3462997)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=874446354:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 2.74/0.79 % (3462998)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=4085349658:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 3.46/0.90 % (3463001)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3310591850:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/874Mi)
% 3.46/0.90 % (3462999)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1959434901:i=427:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/427Mi)
% 3.46/0.90 % (3462997)Refutation not found, incomplete strategy
% 3.46/0.90 % (3462997)------------------------------
% 3.46/0.90 % (3462997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.90 % (3462997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.90 % (3462997)CaDiCaL version: 2.1.3
% 3.46/0.90 % (3462997)Termination reason: Refutation not found, incomplete strategy
% 3.46/0.90 % (3462997)Time elapsed: 0.012 s
% 3.46/0.90 % (3462997)Peak memory usage: 12 MB
% 3.46/0.90 % (3462997)Instructions burned: 17 (million)
% 3.46/0.90 % (3462997)------------------------------
% 3.46/0.90 % (3462997)------------------------------
% 3.46/0.90 % (3462966)Instruction limit reached!
% 3.46/0.90 % (3462966)------------------------------
% 3.46/0.90 % (3462966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.90 % (3462966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.90 % (3462966)CaDiCaL version: 2.1.3
% 3.46/0.90 % (3462966)Termination reason: Instruction limit
% 3.46/0.90 % (3462966)Termination phase: Saturation
% 3.46/0.90 % (3462966)Time elapsed: 0.146 s
% 3.46/0.90 % (3462966)Peak memory usage: 13 MB
% 3.46/0.90 % (3462966)Instructions burned: 317 (million)
% 3.46/0.90 % (3463009)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2821705251:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/515Mi)
% 3.46/0.90 % (3462998)Refutation not found, incomplete strategy
% 3.46/0.90 % (3462998)------------------------------
% 3.46/0.90 % (3462998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.90 % (3462998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.90 % (3462998)CaDiCaL version: 2.1.3
% 3.46/0.90 % (3462998)Termination reason: Refutation not found, incomplete strategy
% 3.46/0.90 % (3462998)Time elapsed: 0.033 s
% 3.46/0.90 % (3462998)Peak memory usage: 12 MB
% 3.46/0.90 % (3462998)Instructions burned: 53 (million)
% 3.46/0.90 % (3463013)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3531387305:st=1.5:i=130:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/130Mi)
% 3.46/0.90 % (3462998)------------------------------
% 3.46/0.90 % (3462998)------------------------------
% 3.46/0.90 % (3463013)Refutation not found, incomplete strategy
% 3.46/0.90 % (3463013)------------------------------
% 3.46/0.90 % (3463013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.90 % (3463013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.90 % (3463013)CaDiCaL version: 2.1.3
% 3.46/0.90 % (3463013)Termination reason: Refutation not found, incomplete strategy
% 3.46/0.90 % (3463013)Time elapsed: 0.016 s
% 3.46/0.90 % (3463013)Peak memory usage: 12 MB
% 3.46/0.90 % (3463013)Instructions burned: 27 (million)
% 3.46/0.90 % (3463013)------------------------------
% 3.46/0.90 % (3463013)------------------------------
% 3.46/0.90 % (3463027)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3180100005:i=44:ep=R:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/44Mi)
% 3.46/0.90 % (3463027)Refutation not found, incomplete strategy
% 3.46/0.90 % (3463027)------------------------------
% 3.46/0.90 % (3463027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.90 % (3463027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/0.90 % (3463027)CaDiCaL version: 2.1.3
% 3.46/0.90 % (3463027)Termination reason: Refutation not found, incomplete strategy
% 3.46/0.90 % (3463027)Time elapsed: 0.004 s
% 3.46/0.90 % (3463027)Peak memory usage: 12 MB
% 3.46/0.90 % (3463027)Instructions burned: 8 (million)
% 3.46/0.90 % (3463027)------------------------------
% 3.46/0.90 % (3463027)------------------------------
% 3.46/0.90 % (3462996)Instruction limit reached!
% 3.46/0.90 % (3462996)------------------------------
% 3.46/0.90 % (3462996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.46/0.90 % (3462996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.93 % (3462996)CaDiCaL version: 2.1.3
% 4.33/0.93 % (3462996)Termination reason: Instruction limit
% 4.33/0.93 % (3462996)Termination phase: Saturation
% 4.33/0.93 % (3462996)Time elapsed: 0.079 s
% 4.33/0.93 % (3462996)Peak memory usage: 15 MB
% 4.33/0.93 % (3462996)Instructions burned: 180 (million)
% 4.33/0.93 % (3463035)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1446477703:s2a=on:i=571:nm=16:rtra=on_2996 on theBenchmark for (2996ds/571Mi)
% 4.33/0.93 % (3463037)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=513975542:i=450:rtra=on:ixr=off:ntd=on_2996 on theBenchmark for (2996ds/450Mi)
% 4.33/0.93 % (3463043)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1442411783:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/95Mi)
% 4.33/0.93 % (3463043)Instruction limit reached!
% 4.33/0.93 % (3463043)------------------------------
% 4.33/0.93 % (3463043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.93 % (3463043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.93 % (3463043)CaDiCaL version: 2.1.3
% 4.33/0.93 % (3463043)Termination reason: Instruction limit
% 4.33/0.93 % (3463043)Termination phase: Saturation
% 4.33/0.93 % (3463043)Time elapsed: 0.050 s
% 4.33/0.93 % (3463043)Peak memory usage: 12 MB
% 4.33/0.93 % (3463043)Instructions burned: 96 (million)
% 4.33/0.93 % (3463065)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=904005029:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 4.33/0.93 % (3463065)Refutation not found, incomplete strategy
% 4.33/0.93 % (3463065)------------------------------
% 4.33/0.93 % (3463065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.93 % (3463065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.93 % (3463065)CaDiCaL version: 2.1.3
% 4.33/0.93 % (3463065)Termination reason: Refutation not found, incomplete strategy
% 4.33/0.93 % (3463065)Time elapsed: 0.014 s
% 4.33/0.93 % (3463065)Peak memory usage: 12 MB
% 4.33/0.93 % (3463065)Instructions burned: 24 (million)
% 4.33/0.93 % (3463065)------------------------------
% 4.33/0.93 % (3463065)------------------------------
% 4.33/0.93 % (3463078)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=3235038746: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_2994 on theBenchmark for (2994ds/105Mi)
% 4.33/0.93 % (3462999)Instruction limit reached!
% 4.33/0.93 % (3462999)------------------------------
% 4.33/0.93 % (3462999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.93 % (3462999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.93 % (3462999)CaDiCaL version: 2.1.3
% 4.33/0.93 % (3462999)Termination reason: Instruction limit
% 4.33/0.93 % (3462999)Termination phase: Saturation
% 4.33/0.93 % (3462999)Time elapsed: 0.201 s
% 4.33/0.93 % (3462999)Peak memory usage: 14 MB
% 4.33/0.93 % (3462999)Instructions burned: 429 (million)
% 4.33/0.93 % (3463078)Refutation not found, incomplete strategy
% 4.33/0.93 % (3463078)------------------------------
% 4.33/0.93 % (3463078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.93 % (3463078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.93 % (3463078)CaDiCaL version: 2.1.3
% 4.33/0.93 % (3463078)Termination reason: Refutation not found, incomplete strategy
% 4.33/0.93 % (3463078)Time elapsed: 0.014 s
% 4.33/0.93 % (3463078)Peak memory usage: 12 MB
% 4.33/0.93 % (3463078)Instructions burned: 24 (million)
% 4.33/0.93 % (3463078)------------------------------
% 4.33/0.93 % (3463078)------------------------------
% 4.33/0.93 % (3463102)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=3713370111:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2994 on theBenchmark for (2994ds/5755Mi)
% 4.33/0.93 % (3463105)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2019092715:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/375Mi)
% 5.85/1.09 % (3463001)Instruction limit reached!
% 5.85/1.09 % (3463001)------------------------------
% 5.85/1.09 % (3463001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.09 % (3463001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.09 % (3463001)CaDiCaL version: 2.1.3
% 5.85/1.09 % (3463001)Termination reason: Instruction limit
% 5.85/1.09 % (3463001)Termination phase: Saturation
% 5.85/1.09 % (3463001)Time elapsed: 0.229 s
% 5.85/1.09 % (3463001)Peak memory usage: 14 MB
% 5.85/1.09 % (3463001)Instructions burned: 878 (million)
% 5.85/1.09 % (3463117)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1702020471:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/495Mi)
% 5.85/1.09 % (3463009)Instruction limit reached!
% 5.85/1.09 % (3463009)------------------------------
% 5.85/1.09 % (3463009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.09 % (3463009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.09 % (3463009)CaDiCaL version: 2.1.3
% 5.85/1.09 % (3463009)Termination reason: Instruction limit
% 5.85/1.09 % (3463009)Termination phase: Saturation
% 5.85/1.09 % (3463009)Time elapsed: 0.235 s
% 5.85/1.09 % (3463009)Peak memory usage: 13 MB
% 5.85/1.09 % (3463009)Instructions burned: 517 (million)
% 5.85/1.09 % (3462968)Instruction limit reached!
% 5.85/1.09 % (3462968)------------------------------
% 5.85/1.09 % (3462968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.09 % (3462968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.09 % (3462968)CaDiCaL version: 2.1.3
% 5.85/1.09 % (3462968)Termination reason: Instruction limit
% 5.85/1.09 % (3462968)Termination phase: Saturation
% 5.85/1.09 % (3462968)Time elapsed: 0.389 s
% 5.85/1.09 % (3462968)Peak memory usage: 14 MB
% 5.85/1.09 % (3462968)Instructions burned: 853 (million)
% 5.85/1.09 % (3463037)Instruction limit reached!
% 5.85/1.09 % (3463037)------------------------------
% 5.85/1.09 % (3463037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.09 % (3463037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.09 % (3463037)CaDiCaL version: 2.1.3
% 5.85/1.09 % (3463037)Termination reason: Instruction limit
% 5.85/1.09 % (3463037)Termination phase: Saturation
% 5.85/1.09 % (3463037)Time elapsed: 0.207 s
% 5.85/1.09 % (3463037)Peak memory usage: 13 MB
% 5.85/1.09 % (3463037)Instructions burned: 450 (million)
% 5.85/1.09 % (3463142)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=3912078648:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 5.85/1.09 % (3463143)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=791867242:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/91Mi)
% 5.85/1.09 % (3463145)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=40435482:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2993 on theBenchmark for (2993ds/66Mi)
% 5.85/1.09 % (3463142)Instruction limit reached!
% 5.85/1.09 % (3463142)------------------------------
% 5.85/1.09 % (3463142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.09 % (3463142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.09 % (3463142)CaDiCaL version: 2.1.3
% 5.85/1.09 % (3463142)Termination reason: Instruction limit
% 5.85/1.09 % (3463142)Termination phase: Saturation
% 5.85/1.09 % (3463142)Time elapsed: 0.018 s
% 5.85/1.09 % (3463142)Peak memory usage: 12 MB
% 5.85/1.09 % (3463142)Instructions burned: 34 (million)
% 5.85/1.09 % (3463035)Instruction limit reached!
% 5.85/1.09 % (3463035)------------------------------
% 5.85/1.09 % (3463035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.09 % (3463035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.09 % (3463035)CaDiCaL version: 2.1.3
% 5.85/1.09 % (3463035)Termination reason: Instruction limit
% 5.85/1.09 % (3463035)Termination phase: Saturation
% 5.85/1.09 % (3463035)Time elapsed: 0.252 s
% 5.85/1.09 % (3463035)Peak memory usage: 13 MB
% 5.85/1.09 % (3463035)Instructions burned: 572 (million)
% 5.85/1.09 % (3463157)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1747658141:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2993 on theBenchmark for (2993ds/22Mi)
% 5.85/1.09 % (3463157)Instruction limit reached!
% 5.85/1.13 % (3463157)------------------------------
% 5.85/1.13 % (3463157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.13 % (3463157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.13 % (3463157)CaDiCaL version: 2.1.3
% 5.85/1.13 % (3463157)Termination reason: Instruction limit
% 5.85/1.13 % (3463157)Termination phase: Saturation
% 5.85/1.13 % (3463157)Time elapsed: 0.011 s
% 5.85/1.13 % (3463157)Peak memory usage: 12 MB
% 5.85/1.13 % (3463157)Instructions burned: 23 (million)
% 5.85/1.13 % (3463143)Instruction limit reached!
% 5.85/1.13 % (3463143)------------------------------
% 5.85/1.13 % (3463143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.13 % (3463143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.13 % (3463143)CaDiCaL version: 2.1.3
% 5.85/1.13 % (3463143)Termination reason: Instruction limit
% 5.85/1.13 % (3463143)Termination phase: Saturation
% 5.85/1.13 % (3463143)Time elapsed: 0.047 s
% 5.85/1.13 % (3463143)Peak memory usage: 12 MB
% 5.85/1.13 % (3463143)Instructions burned: 91 (million)
% 5.85/1.13 % (3463145)Instruction limit reached!
% 5.85/1.13 % (3463145)------------------------------
% 5.85/1.13 % (3463145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.13 % (3463145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.13 % (3463145)CaDiCaL version: 2.1.3
% 5.85/1.13 % (3463145)Termination reason: Instruction limit
% 5.85/1.13 % (3463145)Termination phase: Saturation
% 5.85/1.13 % (3463145)Time elapsed: 0.037 s
% 5.85/1.13 % (3463145)Peak memory usage: 12 MB
% 5.85/1.13 % (3463145)Instructions burned: 66 (million)
% 5.85/1.13 % (3463165)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=2217605774:i=338:bd=all:ins=4:rtra=on_2993 on theBenchmark for (2993ds/338Mi)
% 5.85/1.13 % (3463169)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3750108394:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/28Mi)
% 5.85/1.13 % (3463173)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 5.85/1.13 % (3463173)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=441421218:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2993 on theBenchmark for (2993ds/137Mi)
% 5.85/1.13 % (3463174)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=3699750307:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2993 on theBenchmark for (2993ds/340Mi)
% 5.85/1.13 % (3463173)Refutation not found, incomplete strategy
% 5.85/1.13 % (3463173)------------------------------
% 5.85/1.13 % (3463173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.13 % (3463173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.13 % (3463173)CaDiCaL version: 2.1.3
% 5.85/1.13 % (3463173)Termination reason: Refutation not found, incomplete strategy
% 5.85/1.13 % (3463173)Time elapsed: 0.006 s
% 5.85/1.13 % (3463173)Peak memory usage: 12 MB
% 5.85/1.13 % (3463173)Instructions burned: 11 (million)
% 5.85/1.13 % (3463173)------------------------------
% 5.85/1.13 % (3463173)------------------------------
% 5.85/1.13 % (3463169)Instruction limit reached!
% 5.85/1.13 % (3463169)------------------------------
% 5.85/1.13 % (3463169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.13 % (3463169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.13 % (3463169)CaDiCaL version: 2.1.3
% 5.85/1.13 % (3463169)Termination reason: Instruction limit
% 5.85/1.13 % (3463169)Termination phase: Saturation
% 5.85/1.13 % (3463169)Time elapsed: 0.016 s
% 5.85/1.13 % (3463169)Peak memory usage: 12 MB
% 5.85/1.13 % (3463169)Instructions burned: 29 (million)
% 5.85/1.13 % (3463117)Instruction limit reached!
% 5.85/1.13 % (3463117)------------------------------
% 5.85/1.13 % (3463117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.13 % (3463117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.13 % (3463117)CaDiCaL version: 2.1.3
% 5.85/1.13 % (3463117)Termination reason: Instruction limit
% 5.85/1.13 % (3463117)Termination phase: Saturation
% 5.85/1.13 % (3463117)Time elapsed: 0.129 s
% 5.85/1.13 % (3463117)Peak memory usage: 14 MB
% 6.52/1.25 % (3463117)Instructions burned: 496 (million)
% 6.52/1.25 % (3463192)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 6.52/1.25 % (3463189)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2083034829:i=227:sd=1:bd=all:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/227Mi)
% 6.52/1.25 % (3463192)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1040734300:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/373Mi)
% 6.52/1.25 % (3463194)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3538723059:i=116:ep=RSTC:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/116Mi)
% 6.52/1.25 % (3463105)Instruction limit reached!
% 6.52/1.25 % (3463105)------------------------------
% 6.52/1.25 % (3463105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.25 % (3463105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.25 % (3463105)CaDiCaL version: 2.1.3
% 6.52/1.25 % (3463105)Termination reason: Instruction limit
% 6.52/1.25 % (3463105)Termination phase: Saturation
% 6.52/1.25 % (3463105)Time elapsed: 0.206 s
% 6.52/1.25 % (3463105)Peak memory usage: 15 MB
% 6.52/1.25 % (3463105)Instructions burned: 377 (million)
% 6.52/1.25 % (3463194)Instruction limit reached!
% 6.52/1.25 % (3463194)------------------------------
% 6.52/1.25 % (3463194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.25 % (3463194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.25 % (3463194)CaDiCaL version: 2.1.3
% 6.52/1.25 % (3463194)Termination reason: Instruction limit
% 6.52/1.25 % (3463194)Termination phase: Saturation
% 6.52/1.25 % (3463194)Time elapsed: 0.052 s
% 6.52/1.25 % (3463194)Peak memory usage: 12 MB
% 6.52/1.25 % (3463194)Instructions burned: 117 (million)
% 6.52/1.25 % (3463231)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=195143445:i=575:rtra=on_2992 on theBenchmark for (2992ds/575Mi)
% 6.52/1.25 % (3463232)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3757802431:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2992 on theBenchmark for (2992ds/270Mi)
% 6.52/1.25 % (3463189)Instruction limit reached!
% 6.52/1.25 % (3463189)------------------------------
% 6.52/1.25 % (3463189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.25 % (3463189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.25 % (3463189)CaDiCaL version: 2.1.3
% 6.52/1.25 % (3463189)Termination reason: Instruction limit
% 6.52/1.25 % (3463189)Termination phase: Saturation
% 6.52/1.25 % (3463189)Time elapsed: 0.123 s
% 6.52/1.25 % (3463189)Peak memory usage: 13 MB
% 6.52/1.25 % (3463189)Instructions burned: 228 (million)
% 6.52/1.25 % (3463174)Instruction limit reached!
% 6.52/1.25 % (3463174)------------------------------
% 6.52/1.25 % (3463174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.25 % (3463174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.25 % (3463174)CaDiCaL version: 2.1.3
% 6.52/1.25 % (3463174)Termination reason: Instruction limit
% 6.52/1.25 % (3463174)Termination phase: Saturation
% 6.52/1.25 % (3463174)Time elapsed: 0.154 s
% 6.52/1.25 % (3463174)Peak memory usage: 13 MB
% 6.52/1.25 % (3463174)Instructions burned: 341 (million)
% 6.52/1.25 % (3463165)Instruction limit reached!
% 6.52/1.25 % (3463165)------------------------------
% 6.52/1.25 % (3463165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.25 % (3463165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.25 % (3463165)CaDiCaL version: 2.1.3
% 6.52/1.25 % (3463165)Termination reason: Instruction limit
% 6.52/1.25 % (3463165)Termination phase: Saturation
% 6.52/1.25 % (3463165)Time elapsed: 0.173 s
% 6.52/1.25 % (3463165)Peak memory usage: 14 MB
% 6.52/1.25 % (3463165)Instructions burned: 339 (million)
% 6.52/1.25 % (3463249)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=2407826531:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/9840Mi)
% 6.52/1.25 % (3463249)Refutation not found, incomplete strategy
% 7.62/1.40 % (3463249)------------------------------
% 7.62/1.40 % (3463249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.62/1.40 % (3463249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.62/1.40 % (3463249)CaDiCaL version: 2.1.3
% 7.62/1.40 % (3463249)Termination reason: Refutation not found, incomplete strategy
% 7.62/1.40 % (3463249)Time elapsed: 0.005 s
% 7.62/1.40 % (3463249)Peak memory usage: 12 MB
% 7.62/1.40 % (3463249)Instructions burned: 13 (million)
% 7.62/1.40 % (3463249)------------------------------
% 7.62/1.40 % (3463249)------------------------------
% 7.62/1.40 % (3463250)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3327345180:i=421:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/421Mi)
% 7.62/1.40 % (3463251)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
% 7.62/1.40 % (3463257)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1852850646:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/31Mi)
% 7.62/1.40 % (3463257)Refutation not found, incomplete strategy
% 7.62/1.40 % (3463257)------------------------------
% 7.62/1.40 % (3463257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.62/1.40 % (3463257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.62/1.40 % (3463257)CaDiCaL version: 2.1.3
% 7.62/1.40 % (3463257)Termination reason: Refutation not found, incomplete strategy
% 7.62/1.40 % (3463257)Time elapsed: 0.003 s
% 7.62/1.40 % (3463257)Peak memory usage: 12 MB
% 7.62/1.40 % (3463257)Instructions burned: 8 (million)
% 7.62/1.40 % (3463257)------------------------------
% 7.62/1.40 % (3463257)------------------------------
% 7.62/1.40 % (3463251)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=3299788338:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/270Mi)
% 7.62/1.40 % (3463269)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 7.62/1.40 % (3463269)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
% 7.62/1.40 % (3463269)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=566504403:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2991 on theBenchmark for (2991ds/1440Mi)
% 7.62/1.40 % (3463192)Instruction limit reached!
% 7.62/1.40 % (3463192)------------------------------
% 7.62/1.40 % (3463192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.62/1.40 % (3463192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.62/1.40 % (3463192)CaDiCaL version: 2.1.3
% 7.62/1.40 % (3463192)Termination reason: Instruction limit
% 7.62/1.40 % (3463192)Termination phase: Saturation
% 7.62/1.40 % (3463192)Time elapsed: 0.163 s
% 7.62/1.40 % (3463192)Peak memory usage: 15 MB
% 7.62/1.40 % (3463192)Instructions burned: 374 (million)
% 7.62/1.40 % (3463269)Refutation not found, incomplete strategy
% 7.62/1.40 % (3463269)------------------------------
% 7.62/1.40 % (3463269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.62/1.40 % (3463269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.62/1.40 % (3463269)CaDiCaL version: 2.1.3
% 7.62/1.40 % (3463269)Termination reason: Refutation not found, incomplete strategy
% 7.62/1.40 % (3463269)Time elapsed: 0.007 s
% 7.62/1.40 % (3463269)Peak memory usage: 12 MB
% 7.62/1.40 % (3463269)Instructions burned: 25 (million)
% 7.62/1.40 % (3463269)------------------------------
% 7.62/1.40 % (3463269)------------------------------
% 7.62/1.40 % (3463276)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1367613181:i=111:add=on:fgj=on:rtra=on:fdi=1024_2991 on theBenchmark for (2991ds/111Mi)
% 7.62/1.40 % (3463275)dis+10_2_sil=128000:si=on:random_seed=3727258676:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2991 on theBenchmark for (2991ds/339Mi)
% 7.62/1.40 % (3463276)Refutation not found, incomplete strategy
% 7.62/1.40 % (3463276)------------------------------
% 7.62/1.40 % (3463276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.55 % (3463276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.55 % (3463276)CaDiCaL version: 2.1.3
% 8.17/1.55 % (3463276)Termination reason: Refutation not found, incomplete strategy
% 8.17/1.55 % (3463276)Time elapsed: 0.001 s
% 8.17/1.55 % (3463276)Peak memory usage: 12 MB
% 8.17/1.55 % (3463276)Instructions burned: 4 (million)
% 8.17/1.55 % (3463276)------------------------------
% 8.17/1.55 % (3463276)------------------------------
% 8.17/1.55 % (3463283)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=1168174833:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/122Mi)
% 8.17/1.55 % (3463232)Instruction limit reached!
% 8.17/1.55 % (3463232)------------------------------
% 8.17/1.55 % (3463232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.55 % (3463232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.55 % (3463232)CaDiCaL version: 2.1.3
% 8.17/1.55 % (3463232)Termination reason: Instruction limit
% 8.17/1.55 % (3463232)Termination phase: Saturation
% 8.17/1.55 % (3463232)Time elapsed: 0.130 s
% 8.17/1.55 % (3463232)Peak memory usage: 14 MB
% 8.17/1.55 % (3463232)Instructions burned: 272 (million)
% 8.17/1.55 % (3463283)Instruction limit reached!
% 8.17/1.55 % (3463283)------------------------------
% 8.17/1.55 % (3463283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.55 % (3463283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.55 % (3463283)CaDiCaL version: 2.1.3
% 8.17/1.55 % (3463283)Termination reason: Instruction limit
% 8.17/1.55 % (3463283)Termination phase: Saturation
% 8.17/1.55 % (3463283)Time elapsed: 0.029 s
% 8.17/1.55 % (3463283)Peak memory usage: 12 MB
% 8.17/1.55 % (3463283)Instructions burned: 123 (million)
% 8.17/1.55 % (3463287)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=1460787535:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/136Mi)
% 8.17/1.55 % (3463292)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1725945815:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/232Mi)
% 8.17/1.55 % (3463292)Refutation not found, incomplete strategy
% 8.17/1.55 % (3463292)------------------------------
% 8.17/1.55 % (3463292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.55 % (3463292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.55 % (3463292)CaDiCaL version: 2.1.3
% 8.17/1.55 % (3463292)Termination reason: Refutation not found, incomplete strategy
% 8.17/1.55 % (3463292)Time elapsed: 0.001 s
% 8.17/1.55 % (3463292)Peak memory usage: 12 MB
% 8.17/1.55 % (3463292)Instructions burned: 2 (million)
% 8.17/1.55 % (3463292)------------------------------
% 8.17/1.55 % (3463292)------------------------------
% 8.17/1.55 % (3463297)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=2124923488:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/1254Mi)
% 8.17/1.55 % (3463287)Instruction limit reached!
% 8.17/1.55 % (3463287)------------------------------
% 8.17/1.55 % (3463287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.55 % (3463287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.55 % (3463287)CaDiCaL version: 2.1.3
% 8.17/1.55 % (3463287)Termination reason: Instruction limit
% 8.17/1.55 % (3463287)Termination phase: Saturation
% 8.17/1.55 % (3463287)Time elapsed: 0.056 s
% 8.17/1.55 % (3463287)Peak memory usage: 12 MB
% 8.17/1.55 % (3463287)Instructions burned: 138 (million)
% 8.17/1.55 % (3463309)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 8.17/1.55 % (3463309)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=1685407007:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2989 on theBenchmark for (2989ds/281Mi)
% 8.17/1.55 % (3463251)Instruction limit reached!
% 8.17/1.55 % (3463251)------------------------------
% 8.17/1.55 % (3463251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.55 % (3463251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/1.72 % (3463251)CaDiCaL version: 2.1.3
% 9.76/1.72 % (3463251)Termination reason: Instruction limit
% 9.76/1.72 % (3463251)Termination phase: Saturation
% 9.76/1.72 % (3463251)Time elapsed: 0.148 s
% 9.76/1.72 % (3463251)Peak memory usage: 13 MB
% 9.76/1.72 % (3463251)Instructions burned: 270 (million)
% 9.76/1.72 % (3463315)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=268512384:i=619:add=on:rtra=on_2989 on theBenchmark for (2989ds/619Mi)
% 9.76/1.72 % (3463231)Instruction limit reached!
% 9.76/1.72 % (3463231)------------------------------
% 9.76/1.72 % (3463231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.76/1.72 % (3463231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/1.72 % (3463231)CaDiCaL version: 2.1.3
% 9.76/1.72 % (3463231)Termination reason: Instruction limit
% 9.76/1.72 % (3463231)Termination phase: Saturation
% 9.76/1.72 % (3463231)Time elapsed: 0.282 s
% 9.76/1.72 % (3463231)Peak memory usage: 14 MB
% 9.76/1.72 % (3463231)Instructions burned: 575 (million)
% 9.76/1.72 % (3463275)Instruction limit reached!
% 9.76/1.72 % (3463275)------------------------------
% 9.76/1.72 % (3463275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.76/1.72 % (3463275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/1.72 % (3463275)CaDiCaL version: 2.1.3
% 9.76/1.72 % (3463275)Termination reason: Instruction limit
% 9.76/1.72 % (3463275)Termination phase: Saturation
% 9.76/1.72 % (3463275)Time elapsed: 0.168 s
% 9.76/1.72 % (3463275)Peak memory usage: 13 MB
% 9.76/1.72 % (3463275)Instructions burned: 340 (million)
% 9.76/1.72 % (3463315)Refutation not found, incomplete strategy
% 9.76/1.72 % (3463315)------------------------------
% 9.76/1.72 % (3463315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.76/1.72 % (3463315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/1.72 % (3463315)CaDiCaL version: 2.1.3
% 9.76/1.72 % (3463315)Termination reason: Refutation not found, incomplete strategy
% 9.76/1.72 % (3463315)Time elapsed: 0.018 s
% 9.76/1.72 % (3463315)Peak memory usage: 12 MB
% 9.76/1.72 % (3463315)Instructions burned: 16 (million)
% 9.76/1.72 % (3463315)------------------------------
% 9.76/1.72 % (3463315)------------------------------
% 9.76/1.72 % (3463250)Instruction limit reached!
% 9.76/1.72 % (3463250)------------------------------
% 9.76/1.72 % (3463250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.76/1.72 % (3463250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/1.72 % (3463250)CaDiCaL version: 2.1.3
% 9.76/1.72 % (3463250)Termination reason: Instruction limit
% 9.76/1.72 % (3463250)Termination phase: Saturation
% 9.76/1.72 % (3463250)Time elapsed: 0.225 s
% 9.76/1.72 % (3463250)Peak memory usage: 13 MB
% 9.76/1.72 % (3463250)Instructions burned: 421 (million)
% 9.76/1.72 % (3463335)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=1525979778:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/865Mi)
% 9.76/1.72 % (3463336)lrs+10_1_sil=128000:si=on:urr=on:random_seed=48153425:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/212Mi)
% 9.76/1.72 % (3463337)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=200490979:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/130Mi)
% 9.76/1.72 % (3463338)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3513659189:st=1.5:i=346:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/346Mi)
% 9.76/1.72 % (3463338)Refutation not found, incomplete strategy
% 9.76/1.72 % (3463338)------------------------------
% 9.76/1.72 % (3463338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.76/1.72 % (3463338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/1.72 % (3463338)CaDiCaL version: 2.1.3
% 9.76/1.72 % (3463338)Termination reason: Refutation not found, incomplete strategy
% 9.76/1.72 % (3463338)Time elapsed: 0.014 s
% 9.76/1.72 % (3463338)Peak memory usage: 12 MB
% 9.76/1.72 % (3463338)Instructions burned: 14 (million)
% 9.76/1.72 % (3463338)------------------------------
% 9.76/1.72 % (3463338)------------------------------
% 9.76/1.72 % (3463343)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=2242140665:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/152Mi)
% 10.25/2.05 % (3463337)Instruction limit reached!
% 10.25/2.05 % (3463337)------------------------------
% 10.25/2.05 % (3463337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.25/2.05 % (3463337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.25/2.05 % (3463337)CaDiCaL version: 2.1.3
% 10.25/2.05 % (3463337)Termination reason: Instruction limit
% 10.25/2.05 % (3463337)Termination phase: Saturation
% 10.25/2.05 % (3463337)Time elapsed: 0.111 s
% 10.25/2.05 % (3463337)Peak memory usage: 12 MB
% 10.25/2.05 % (3463337)Instructions burned: 130 (million)
% 10.25/2.05 % (3463309)Instruction limit reached!
% 10.25/2.05 % (3463309)------------------------------
% 10.25/2.05 % (3463309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.25/2.05 % (3463309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.25/2.05 % (3463309)CaDiCaL version: 2.1.3
% 10.25/2.05 % (3463309)Termination reason: Instruction limit
% 10.25/2.05 % (3463309)Termination phase: Saturation
% 10.25/2.05 % (3463309)Time elapsed: 0.222 s
% 10.25/2.05 % (3463309)Peak memory usage: 13 MB
% 10.25/2.05 % (3463309)Instructions burned: 282 (million)
% 10.25/2.05 % (3463345)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4269230873:i=75:ep=R:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/75Mi)
% 10.25/2.05 % (3463345)Refutation not found, incomplete strategy
% 10.25/2.05 % (3463345)------------------------------
% 10.25/2.05 % (3463345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.25/2.05 % (3463345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.25/2.05 % (3463345)CaDiCaL version: 2.1.3
% 10.25/2.05 % (3463345)Termination reason: Refutation not found, incomplete strategy
% 10.25/2.05 % (3463345)Time elapsed: 0.008 s
% 10.25/2.05 % (3463345)Peak memory usage: 12 MB
% 10.25/2.05 % (3463345)Instructions burned: 8 (million)
% 10.25/2.05 % (3463345)------------------------------
% 10.25/2.05 % (3463345)------------------------------
% 10.25/2.05 % (3463346)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=941761689:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/387Mi)
% 10.25/2.05 % (3463336)Instruction limit reached!
% 10.25/2.05 % (3463336)------------------------------
% 10.25/2.05 % (3463336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.25/2.05 % (3463336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.25/2.05 % (3463336)CaDiCaL version: 2.1.3
% 10.25/2.05 % (3463336)Termination reason: Instruction limit
% 10.25/2.05 % (3463336)Termination phase: Saturation
% 10.25/2.05 % (3463336)Time elapsed: 0.182 s
% 10.25/2.05 % (3463336)Peak memory usage: 13 MB
% 10.25/2.05 % (3463336)Instructions burned: 212 (million)
% 10.25/2.05 % (3463346)Refutation not found, incomplete strategy
% 10.25/2.05 % (3463346)------------------------------
% 10.25/2.05 % (3463346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.25/2.05 % (3463346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.25/2.05 % (3463346)CaDiCaL version: 2.1.3
% 10.25/2.05 % (3463346)Termination reason: Refutation not found, incomplete strategy
% 10.25/2.05 % (3463346)Time elapsed: 0.012 s
% 10.25/2.05 % (3463346)Peak memory usage: 12 MB
% 10.25/2.05 % (3463346)Instructions burned: 12 (million)
% 10.25/2.05 % (3463346)------------------------------
% 10.25/2.05 % (3463346)------------------------------
% 10.25/2.05 % (3463348)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=1620175870:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2987 on theBenchmark for (2987ds/148Mi)
% 10.25/2.05 % (3463343)Instruction limit reached!
% 10.25/2.05 % (3463343)------------------------------
% 10.25/2.05 % (3463343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.25/2.05 % (3463343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.25/2.05 % (3463343)CaDiCaL version: 2.1.3
% 10.25/2.05 % (3463343)Termination reason: Instruction limit
% 10.25/2.05 % (3463343)Termination phase: Saturation
% 10.25/2.05 % (3463343)Time elapsed: 0.137 s
% 10.25/2.05 % (3463343)Peak memory usage: 13 MB
% 10.25/2.05 % (3463343)Instructions burned: 152 (million)
% 10.25/2.05 % (3463350)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=2534789651:i=161:piset=and:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/161Mi)
% 10.25/2.05 % (3463351)lrs+10_1_sil=128000:si=on:random_seed=3354230008:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/888Mi)
% 13.63/2.29 % (3463353)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=51520057:i=136:add=on:ins=4:rtra=on:sup=off_2986 on theBenchmark for (2986ds/136Mi)
% 13.63/2.29 % (3463297)Instruction limit reached!
% 13.63/2.29 % (3463297)------------------------------
% 13.63/2.29 % (3463297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.63/2.29 % (3463297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.29 % (3463297)CaDiCaL version: 2.1.3
% 13.63/2.29 % (3463297)Termination reason: Instruction limit
% 13.63/2.29 % (3463297)Termination phase: Saturation
% 13.63/2.29 % (3463297)Time elapsed: 0.418 s
% 13.63/2.29 % (3463297)Peak memory usage: 14 MB
% 13.63/2.29 % (3463297)Instructions burned: 1256 (million)
% 13.63/2.29 % (3463357)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=1770597581:i=88:s2at=3:nm=2:rtra=on:rawr=on_2986 on theBenchmark for (2986ds/88Mi)
% 13.63/2.29 % (3463348)Instruction limit reached!
% 13.63/2.29 % (3463348)------------------------------
% 13.63/2.29 % (3463348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.63/2.29 % (3463348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.29 % (3463348)CaDiCaL version: 2.1.3
% 13.63/2.29 % (3463348)Termination reason: Instruction limit
% 13.63/2.29 % (3463348)Termination phase: Saturation
% 13.63/2.29 % (3463348)Time elapsed: 0.127 s
% 13.63/2.29 % (3463348)Peak memory usage: 12 MB
% 13.63/2.29 % (3463348)Instructions burned: 148 (million)
% 13.63/2.29 % (3463353)Instruction limit reached!
% 13.63/2.29 % (3463353)------------------------------
% 13.63/2.29 % (3463353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.63/2.29 % (3463353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.29 % (3463353)CaDiCaL version: 2.1.3
% 13.63/2.29 % (3463353)Termination reason: Instruction limit
% 13.63/2.29 % (3463353)Termination phase: Saturation
% 13.63/2.29 % (3463353)Time elapsed: 0.100 s
% 13.63/2.29 % (3463353)Peak memory usage: 12 MB
% 13.63/2.29 % (3463353)Instructions burned: 137 (million)
% 13.63/2.29 % (3463357)Instruction limit reached!
% 13.63/2.29 % (3463357)------------------------------
% 13.63/2.29 % (3463357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.63/2.29 % (3463357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.29 % (3463357)CaDiCaL version: 2.1.3
% 13.63/2.29 % (3463357)Termination reason: Instruction limit
% 13.63/2.29 % (3463357)Termination phase: Saturation
% 13.63/2.29 % (3463357)Time elapsed: 0.042 s
% 13.63/2.29 % (3463357)Peak memory usage: 13 MB
% 13.63/2.29 % (3463357)Instructions burned: 89 (million)
% 13.63/2.29 % (3463350)Instruction limit reached!
% 13.63/2.29 % (3463350)------------------------------
% 13.63/2.29 % (3463350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.63/2.29 % (3463350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.29 % (3463350)CaDiCaL version: 2.1.3
% 13.63/2.29 % (3463350)Termination reason: Instruction limit
% 13.63/2.29 % (3463350)Termination phase: Saturation
% 13.63/2.29 % (3463350)Time elapsed: 0.127 s
% 13.63/2.29 % (3463350)Peak memory usage: 12 MB
% 13.63/2.29 % (3463350)Instructions burned: 162 (million)
% 13.63/2.29 % (3463359)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3280738631:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2985 on theBenchmark for (2985ds/93Mi)
% 13.63/2.29 % (3463361)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2343465158:s2a=on:i=240:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/240Mi)
% 13.63/2.29 % (3463360)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3432702039:i=2186:rtra=on:ixr=off_2985 on theBenchmark for (2985ds/2186Mi)
% 13.63/2.29 % (3463362)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=3948050171:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2985 on theBenchmark for (2985ds/805Mi)
% 13.63/2.29 % (3463360)Refutation not found, incomplete strategy
% 13.63/2.29 % (3463360)------------------------------
% 13.63/2.29 % (3463360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.02/2.53 % (3463360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/2.53 % (3463360)CaDiCaL version: 2.1.3
% 15.02/2.53 % (3463360)Termination reason: Refutation not found, incomplete strategy
% 15.02/2.53 % (3463360)Time elapsed: 0.012 s
% 15.02/2.53 % (3463360)Peak memory usage: 12 MB
% 15.02/2.53 % (3463360)Instructions burned: 12 (million)
% 15.02/2.53 % (3463360)------------------------------
% 15.02/2.53 % (3463360)------------------------------
% 15.02/2.53 % (3463367)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 15.02/2.53 % (3463367)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=3853511698:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2985 on theBenchmark for (2985ds/391Mi)
% 15.02/2.53 % (3463359)Instruction limit reached!
% 15.02/2.53 % (3463359)------------------------------
% 15.02/2.53 % (3463359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.02/2.53 % (3463359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/2.53 % (3463359)CaDiCaL version: 2.1.3
% 15.02/2.53 % (3463359)Termination reason: Instruction limit
% 15.02/2.53 % (3463359)Termination phase: Saturation
% 15.02/2.53 % (3463359)Time elapsed: 0.089 s
% 15.02/2.53 % (3463359)Peak memory usage: 12 MB
% 15.02/2.53 % (3463359)Instructions burned: 93 (million)
% 15.02/2.53 % (3463361)Instruction limit reached!
% 15.02/2.53 % (3463361)------------------------------
% 15.02/2.53 % (3463361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.02/2.53 % (3463361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/2.53 % (3463361)CaDiCaL version: 2.1.3
% 15.02/2.53 % (3463361)Termination reason: Instruction limit
% 15.02/2.53 % (3463361)Termination phase: Saturation
% 15.02/2.53 % (3463361)Time elapsed: 0.098 s
% 15.02/2.53 % (3463361)Peak memory usage: 13 MB
% 15.02/2.53 % (3463361)Instructions burned: 243 (million)
% 15.02/2.53 % (3463369)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=3980250543:i=355:av=off:fsr=off:rtra=on:ixr=off_2984 on theBenchmark for (2984ds/355Mi)
% 15.02/2.54 % (3463370)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=73541866:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/314Mi)
% 15.02/2.54 % (3463370)Instruction limit reached!
% 15.02/2.54 % (3463370)------------------------------
% 15.02/2.54 % (3463370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.02/2.54 % (3463370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/2.54 % (3463370)CaDiCaL version: 2.1.3
% 15.02/2.54 % (3463370)Termination reason: Instruction limit
% 15.02/2.54 % (3463370)Termination phase: Saturation
% 15.02/2.54 % (3463370)Time elapsed: 0.132 s
% 15.02/2.54 % (3463370)Peak memory usage: 13 MB
% 15.02/2.54 % (3463370)Instructions burned: 316 (million)
% 15.02/2.54 % (3463335)Instruction limit reached!
% 15.02/2.54 % (3463335)------------------------------
% 15.02/2.54 % (3463335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.02/2.54 % (3463335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/2.54 % (3463335)CaDiCaL version: 2.1.3
% 15.02/2.54 % (3463335)Termination reason: Instruction limit
% 15.02/2.54 % (3463335)Termination phase: Saturation
% 15.02/2.54 % (3463335)Time elapsed: 0.633 s
% 15.02/2.54 % (3463335)Peak memory usage: 14 MB
% 15.02/2.54 % (3463335)Instructions burned: 866 (million)
% 15.02/2.54 % (3463373)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=230008026:s2a=on:i=251:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/251Mi)
% 15.02/2.54 % (3463374)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=2235096406: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_2982 on theBenchmark for (2982ds/2470Mi)
% 15.02/2.54 % (3463367)Instruction limit reached!
% 15.02/2.54 % (3463367)------------------------------
% 15.02/2.54 % (3463367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.02/2.54 % (3463367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/2.54 % (3463367)CaDiCaL version: 2.1.3
% 15.02/2.54 % (3463367)Termination reason: Instruction limit
% 16.80/2.76 % (3463367)Termination phase: Saturation
% 16.80/2.76 % (3463367)Time elapsed: 0.294 s
% 16.80/2.76 % (3463367)Peak memory usage: 13 MB
% 16.80/2.76 % (3463367)Instructions burned: 392 (million)
% 16.80/2.76 % (3463377)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=1448925148:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2981 on theBenchmark for (2981ds/673Mi)
% 16.80/2.76 % (3463369)Instruction limit reached!
% 16.80/2.76 % (3463369)------------------------------
% 16.80/2.76 % (3463369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.80/2.76 % (3463369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/2.76 % (3463369)CaDiCaL version: 2.1.3
% 16.80/2.76 % (3463369)Termination reason: Instruction limit
% 16.80/2.76 % (3463369)Termination phase: Saturation
% 16.80/2.76 % (3463369)Time elapsed: 0.288 s
% 16.80/2.76 % (3463369)Peak memory usage: 13 MB
% 16.80/2.76 % (3463369)Instructions burned: 355 (million)
% 16.80/2.76 % (3463379)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1356419653:i=116:ep=RSTC:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/116Mi)
% 16.80/2.77 % (3463373)Instruction limit reached!
% 16.80/2.77 % (3463373)------------------------------
% 16.80/2.77 % (3463373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.80/2.77 % (3463373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/2.77 % (3463373)CaDiCaL version: 2.1.3
% 16.80/2.77 % (3463373)Termination reason: Instruction limit
% 16.80/2.77 % (3463373)Termination phase: Saturation
% 16.80/2.77 % (3463373)Time elapsed: 0.174 s
% 16.80/2.77 % (3463373)Peak memory usage: 13 MB
% 16.80/2.77 % (3463373)Instructions burned: 251 (million)
% 16.80/2.77 % (3463381)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3801702838:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2980 on theBenchmark for (2980ds/270Mi)
% 16.80/2.77 % (3463379)Instruction limit reached!
% 16.80/2.77 % (3463379)------------------------------
% 16.80/2.77 % (3463379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.80/2.77 % (3463379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/2.77 % (3463379)CaDiCaL version: 2.1.3
% 16.80/2.77 % (3463379)Termination reason: Instruction limit
% 16.80/2.77 % (3463379)Termination phase: Saturation
% 16.80/2.77 % (3463379)Time elapsed: 0.091 s
% 16.80/2.77 % (3463379)Peak memory usage: 12 MB
% 16.80/2.77 % (3463379)Instructions burned: 116 (million)
% 16.80/2.77 % (3463383)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=3405688838:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2980 on theBenchmark for (2980ds/30Mi)
% 16.80/2.77 % (3463383)Refutation not found, incomplete strategy
% 16.80/2.77 % (3463383)------------------------------
% 16.80/2.77 % (3463383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.80/2.77 % (3463383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/2.77 % (3463383)CaDiCaL version: 2.1.3
% 16.80/2.77 % (3463383)Termination reason: Refutation not found, incomplete strategy
% 16.80/2.77 % (3463383)Time elapsed: 0.027 s
% 16.80/2.77 % (3463383)Peak memory usage: 12 MB
% 16.80/2.77 % (3463383)Instructions burned: 21 (million)
% 16.80/2.77 % (3463383)------------------------------
% 16.80/2.77 % (3463383)------------------------------
% 16.80/2.77 % (3463351)Instruction limit reached!
% 16.80/2.77 % (3463351)------------------------------
% 16.80/2.77 % (3463351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.80/2.77 % (3463351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/2.77 % (3463351)CaDiCaL version: 2.1.3
% 16.80/2.77 % (3463351)Termination reason: Instruction limit
% 16.80/2.77 % (3463351)Termination phase: Saturation
% 16.80/2.77 % (3463351)Time elapsed: 0.734 s
% 16.80/2.77 % (3463351)Peak memory usage: 14 MB
% 16.80/2.77 % (3463351)Instructions burned: 889 (million)
% 16.80/2.77 % (3463381)Instruction limit reached!
% 16.80/2.77 % (3463381)------------------------------
% 16.80/2.77 % (3463381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.80/2.77 % (3463381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.08 % (3463381)CaDiCaL version: 2.1.3
% 20.00/3.08 % (3463381)Termination reason: Instruction limit
% 20.00/3.08 % (3463381)Termination phase: Saturation
% 20.00/3.08 % (3463381)Time elapsed: 0.119 s
% 20.00/3.08 % (3463381)Peak memory usage: 14 MB
% 20.00/3.08 % (3463381)Instructions burned: 273 (million)
% 20.00/3.08 % (3463362)Instruction limit reached!
% 20.00/3.08 % (3463362)------------------------------
% 20.00/3.08 % (3463362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.00/3.08 % (3463362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.08 % (3463362)CaDiCaL version: 2.1.3
% 20.00/3.08 % (3463362)Termination reason: Instruction limit
% 20.00/3.08 % (3463362)Termination phase: Saturation
% 20.00/3.08 % (3463362)Time elapsed: 0.590 s
% 20.00/3.08 % (3463362)Peak memory usage: 13 MB
% 20.00/3.08 % (3463362)Instructions burned: 805 (million)
% 20.00/3.08 % (3463387)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=612749002:i=158:av=off:rtra=on_2979 on theBenchmark for (2979ds/158Mi)
% 20.00/3.08 % (3463385)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 20.00/3.08 % (3463387)Refutation not found, incomplete strategy
% 20.00/3.08 % (3463387)------------------------------
% 20.00/3.08 % (3463387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.00/3.08 % (3463387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.08 % (3463387)CaDiCaL version: 2.1.3
% 20.00/3.08 % (3463387)Termination reason: Refutation not found, incomplete strategy
% 20.00/3.08 % (3463387)Time elapsed: 0.007 s
% 20.00/3.08 % (3463387)Peak memory usage: 12 MB
% 20.00/3.08 % (3463387)Instructions burned: 13 (million)
% 20.00/3.08 % (3463387)------------------------------
% 20.00/3.08 % (3463387)------------------------------
% 20.00/3.08 % (3463386)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2319440510:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2979 on theBenchmark for (2979ds/365Mi)
% 20.00/3.08 % (3463385)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=1913973415:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2979 on theBenchmark for (2979ds/39Mi)
% 20.00/3.08 % (3463388)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
% 20.00/3.08 % (3463390)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2004740533:i=213:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/213Mi)
% 20.00/3.08 % (3463388)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=358253174:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/252Mi)
% 20.00/3.08 % (3463385)Instruction limit reached!
% 20.00/3.08 % (3463385)------------------------------
% 20.00/3.08 % (3463385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.00/3.08 % (3463385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.08 % (3463385)CaDiCaL version: 2.1.3
% 20.00/3.08 % (3463385)Termination reason: Instruction limit
% 20.00/3.08 % (3463385)Termination phase: Saturation
% 20.00/3.08 % (3463385)Time elapsed: 0.037 s
% 20.00/3.08 % (3463385)Peak memory usage: 12 MB
% 20.00/3.08 % (3463385)Instructions burned: 39 (million)
% 20.00/3.08 % (3463395)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=4194941863:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/160Mi)
% 20.00/3.08 % (3463390)Instruction limit reached!
% 20.00/3.08 % (3463390)------------------------------
% 20.00/3.08 % (3463390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.00/3.08 % (3463390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/3.08 % (3463390)CaDiCaL version: 2.1.3
% 20.00/3.08 % (3463390)Termination reason: Instruction limit
% 20.00/3.08 % (3463390)Termination phase: Saturation
% 20.00/3.08 % (3463390)Time elapsed: 0.098 s
% 20.00/3.08 % (3463390)Peak memory usage: 13 MB
% 20.00/3.08 % (3463390)Instructions burned: 215 (million)
% 20.00/3.08 % (3463397)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=3215365622:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2977 on theBenchmark for (2977ds/763Mi)
% 20.00/3.08 % (3463395)Instruction limit reached!
% 20.77/3.23 % (3463395)------------------------------
% 20.77/3.23 % (3463395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.77/3.23 % (3463395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.23 % (3463395)CaDiCaL version: 2.1.3
% 20.77/3.23 % (3463395)Termination reason: Instruction limit
% 20.77/3.23 % (3463395)Termination phase: Saturation
% 20.77/3.23 % (3463395)Time elapsed: 0.142 s
% 20.77/3.23 % (3463395)Peak memory usage: 13 MB
% 20.77/3.23 % (3463395)Instructions burned: 160 (million)
% 20.77/3.23 % (3463388)Instruction limit reached!
% 20.77/3.23 % (3463388)------------------------------
% 20.77/3.23 % (3463388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.77/3.23 % (3463388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.23 % (3463388)CaDiCaL version: 2.1.3
% 20.77/3.23 % (3463388)Termination reason: Instruction limit
% 20.77/3.23 % (3463388)Termination phase: Saturation
% 20.77/3.23 % (3463388)Time elapsed: 0.200 s
% 20.77/3.23 % (3463388)Peak memory usage: 13 MB
% 20.77/3.23 % (3463388)Instructions burned: 253 (million)
% 20.77/3.23 % (3463399)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 20.77/3.23 % (3463400)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=1564500880:s2a=on:i=386:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/386Mi)
% 20.77/3.23 % (3463399)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=1192667835:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2976 on theBenchmark for (2976ds/237Mi)
% 20.77/3.23 % (3463400)Refutation not found, incomplete strategy
% 20.77/3.23 % (3463400)------------------------------
% 20.77/3.23 % (3463400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.77/3.23 % (3463400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.23 % (3463400)CaDiCaL version: 2.1.3
% 20.77/3.23 % (3463400)Termination reason: Refutation not found, incomplete strategy
% 20.77/3.23 % (3463400)Time elapsed: 0.008 s
% 20.77/3.23 % (3463400)Peak memory usage: 12 MB
% 20.77/3.23 % (3463400)Instructions burned: 8 (million)
% 20.77/3.23 % (3463400)------------------------------
% 20.77/3.23 % (3463400)------------------------------
% 20.77/3.23 % (3463403)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=2375240184:i=300:piset=and:nm=32:rtra=on_2976 on theBenchmark for (2976ds/300Mi)
% 20.77/3.23 % (3463377)Instruction limit reached!
% 20.77/3.23 % (3463377)------------------------------
% 20.77/3.23 % (3463377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.77/3.23 % (3463377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.23 % (3463377)CaDiCaL version: 2.1.3
% 20.77/3.23 % (3463377)Termination reason: Instruction limit
% 20.77/3.23 % (3463377)Termination phase: Saturation
% 20.77/3.23 % (3463377)Time elapsed: 0.551 s
% 20.77/3.23 % (3463377)Peak memory usage: 15 MB
% 20.77/3.23 % (3463377)Instructions burned: 674 (million)
% 20.77/3.23 % (3463386)Instruction limit reached!
% 20.77/3.23 % (3463386)------------------------------
% 20.77/3.23 % (3463386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.77/3.23 % (3463386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.23 % (3463386)CaDiCaL version: 2.1.3
% 20.77/3.23 % (3463386)Termination reason: Instruction limit
% 20.77/3.23 % (3463386)Termination phase: Saturation
% 20.77/3.23 % (3463386)Time elapsed: 0.320 s
% 20.77/3.23 % (3463386)Peak memory usage: 14 MB
% 20.77/3.23 % (3463386)Instructions burned: 366 (million)
% 20.77/3.23 % (3463405)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=1826998360:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/567Mi)
% 20.77/3.23 % (3463406)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=1890157381:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2975 on theBenchmark for (2975ds/379Mi)
% 20.77/3.23 % (3463397)Instruction limit reached!
% 20.77/3.23 % (3463397)------------------------------
% 20.77/3.23 % (3463397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.77/3.23 % (3463397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.23 % (3463397)CaDiCaL version: 2.1.3
% 20.77/3.23 % (3463397)Termination reason: Instruction limit
% 21.27/3.30 % (3463397)Termination phase: Saturation
% 21.27/3.30 % (3463397)Time elapsed: 0.316 s
% 21.27/3.30 % (3463397)Peak memory usage: 13 MB
% 21.27/3.30 % (3463397)Instructions burned: 767 (million)
% 21.27/3.30 % (3463409)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=2017779098:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2974 on theBenchmark for (2974ds/429Mi)
% 21.27/3.30 % (3463399)Instruction limit reached!
% 21.27/3.30 % (3463399)------------------------------
% 21.27/3.30 % (3463399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.27/3.30 % (3463399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.30 % (3463399)CaDiCaL version: 2.1.3
% 21.27/3.30 % (3463399)Termination reason: Instruction limit
% 21.27/3.30 % (3463399)Termination phase: Saturation
% 21.27/3.30 % (3463399)Time elapsed: 0.216 s
% 21.27/3.30 % (3463399)Peak memory usage: 13 MB
% 21.27/3.30 % (3463399)Instructions burned: 238 (million)
% 21.27/3.30 % (3463411)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=1646967205:i=478:bd=all:rtra=on_2974 on theBenchmark for (2974ds/478Mi)
% 21.27/3.30 % (3463403)Instruction limit reached!
% 21.27/3.30 % (3463403)------------------------------
% 21.27/3.30 % (3463403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.27/3.30 % (3463403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.30 % (3463403)CaDiCaL version: 2.1.3
% 21.27/3.30 % (3463403)Termination reason: Instruction limit
% 21.27/3.30 % (3463403)Termination phase: Saturation
% 21.27/3.30 % (3463403)Time elapsed: 0.233 s
% 21.27/3.30 % (3463403)Peak memory usage: 12 MB
% 21.27/3.30 % (3463403)Instructions burned: 300 (million)
% 21.27/3.30 % (3463413)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=725345279:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2973 on theBenchmark for (2973ds/445Mi)
% 21.27/3.30 % (3463409)Instruction limit reached!
% 21.27/3.30 % (3463409)------------------------------
% 21.27/3.30 % (3463409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.27/3.30 % (3463409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.30 % (3463409)CaDiCaL version: 2.1.3
% 21.27/3.30 % (3463409)Termination reason: Instruction limit
% 21.27/3.30 % (3463409)Termination phase: Saturation
% 21.27/3.30 % (3463409)Time elapsed: 0.181 s
% 21.27/3.30 % (3463409)Peak memory usage: 13 MB
% 21.27/3.30 % (3463409)Instructions burned: 431 (million)
% 21.27/3.30 % (3463406)Instruction limit reached!
% 21.27/3.30 % (3463406)------------------------------
% 21.27/3.30 % (3463406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.27/3.30 % (3463406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.30 % (3463406)CaDiCaL version: 2.1.3
% 21.27/3.30 % (3463406)Termination reason: Instruction limit
% 21.27/3.30 % (3463406)Termination phase: Saturation
% 21.27/3.30 % (3463406)Time elapsed: 0.294 s
% 21.27/3.30 % (3463406)Peak memory usage: 13 MB
% 21.27/3.30 % (3463406)Instructions burned: 380 (million)
% 21.27/3.30 % (3463415)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=1656085308:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2972 on theBenchmark for (2972ds/71Mi)
% 21.27/3.30 % (3463416)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2808666538:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/302Mi)
% 21.27/3.30 % (3463415)Instruction limit reached!
% 21.27/3.30 % (3463415)------------------------------
% 21.27/3.30 % (3463415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.27/3.30 % (3463415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.30 % (3463415)CaDiCaL version: 2.1.3
% 21.27/3.30 % (3463415)Termination reason: Instruction limit
% 21.27/3.30 % (3463415)Termination phase: Saturation
% 21.27/3.30 % (3463415)Time elapsed: 0.031 s
% 21.27/3.30 % (3463415)Peak memory usage: 13 MB
% 21.27/3.30 % (3463415)Instructions burned: 72 (million)
% 21.27/3.30 % (3463419)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=3644924333:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2972 on theBenchmark for (2972ds/4980Mi)
% 21.27/3.30 % (3463405)Instruction limit reached!
% 21.27/3.30 % (3463405)------------------------------
% 21.27/3.30 % (3463405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.27/3.30 % (3463405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.88 % (3463405)CaDiCaL version: 2.1.3
% 23.23/3.88 % (3463405)Termination reason: Instruction limit
% 23.23/3.88 % (3463405)Termination phase: Saturation
% 23.23/3.88 % (3463405)Time elapsed: 0.420 s
% 23.23/3.88 % (3463405)Peak memory usage: 14 MB
% 23.23/3.88 % (3463405)Instructions burned: 571 (million)
% 23.23/3.88 % (3463421)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
% 23.23/3.88 % (3463421)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 23.23/3.88 % (3463421)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1078624302:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2971 on theBenchmark for (2971ds/100Mi)
% 23.23/3.88 % (3463421)Instruction limit reached!
% 23.23/3.88 % (3463421)------------------------------
% 23.23/3.88 % (3463421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.88 % (3463421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.88 % (3463421)CaDiCaL version: 2.1.3
% 23.23/3.88 % (3463421)Termination reason: Instruction limit
% 23.23/3.88 % (3463421)Termination phase: Saturation
% 23.23/3.88 % (3463421)Time elapsed: 0.047 s
% 23.23/3.88 % (3463421)Peak memory usage: 12 MB
% 23.23/3.88 % (3463421)Instructions burned: 101 (million)
% 23.23/3.88 % (3463423)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=3812836146:i=76:piset=equals:rtra=on:ntd=on_2970 on theBenchmark for (2970ds/76Mi)
% 23.23/3.88 % (3463411)Instruction limit reached!
% 23.23/3.88 % (3463411)------------------------------
% 23.23/3.88 % (3463411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.88 % (3463411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.88 % (3463411)CaDiCaL version: 2.1.3
% 23.23/3.88 % (3463411)Termination reason: Instruction limit
% 23.23/3.88 % (3463411)Termination phase: Saturation
% 23.23/3.88 % (3463411)Time elapsed: 0.372 s
% 23.23/3.88 % (3463411)Peak memory usage: 13 MB
% 23.23/3.88 % (3463411)Instructions burned: 479 (million)
% 23.23/3.88 % (3463423)Instruction limit reached!
% 23.23/3.88 % (3463423)------------------------------
% 23.23/3.88 % (3463423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.88 % (3463423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.88 % (3463423)CaDiCaL version: 2.1.3
% 23.23/3.88 % (3463423)Termination reason: Instruction limit
% 23.23/3.88 % (3463423)Termination phase: Saturation
% 23.23/3.88 % (3463423)Time elapsed: 0.032 s
% 23.23/3.88 % (3463423)Peak memory usage: 12 MB
% 23.23/3.88 % (3463423)Instructions burned: 76 (million)
% 23.23/3.88 % (3463426)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=1662307993:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2970 on theBenchmark for (2970ds/493Mi)
% 23.23/3.88 % (3463425)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=425940422:i=289:rtra=on_2970 on theBenchmark for (2970ds/289Mi)
% 23.23/3.88 % (3463426)Refutation not found, incomplete strategy
% 23.23/3.88 % (3463426)------------------------------
% 23.23/3.88 % (3463426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.88 % (3463426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.88 % (3463426)CaDiCaL version: 2.1.3
% 23.23/3.88 % (3463426)Termination reason: Refutation not found, incomplete strategy
% 23.23/3.88 % (3463426)Time elapsed: 0.006 s
% 23.23/3.88 % (3463426)Peak memory usage: 12 MB
% 23.23/3.88 % (3463426)Instructions burned: 11 (million)
% 23.23/3.88 % (3463426)------------------------------
% 23.23/3.88 % (3463426)------------------------------
% 23.23/3.88 % (3463413)Instruction limit reached!
% 23.23/3.88 % (3463413)------------------------------
% 23.23/3.88 % (3463413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.88 % (3463413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.88 % (3463413)CaDiCaL version: 2.1.3
% 23.23/3.88 % (3463413)Termination reason: Instruction limit
% 23.23/3.88 % (3463413)Termination phase: Saturation
% 23.23/3.88 % (3463413)Time elapsed: 0.358 s
% 23.71/4.04 % (3463413)Peak memory usage: 14 MB
% 23.71/4.04 % (3463413)Instructions burned: 446 (million)
% 23.71/4.04 % (3463429)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=3485777364:cond=on:i=34:hud=10:nm=10:rtra=on_2969 on theBenchmark for (2969ds/34Mi)
% 23.71/4.04 % (3463430)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 23.71/4.04 % (3463429)Instruction limit reached!
% 23.71/4.04 % (3463429)------------------------------
% 23.71/4.04 % (3463429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.71/4.04 % (3463429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.71/4.04 % (3463429)CaDiCaL version: 2.1.3
% 23.71/4.04 % (3463429)Termination reason: Instruction limit
% 23.71/4.04 % (3463429)Termination phase: Saturation
% 23.71/4.04 % (3463429)Time elapsed: 0.017 s
% 23.71/4.04 % (3463429)Peak memory usage: 12 MB
% 23.71/4.04 % (3463429)Instructions burned: 34 (million)
% 23.71/4.04 % (3463416)Instruction limit reached!
% 23.71/4.04 % (3463416)------------------------------
% 23.71/4.04 % (3463416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.71/4.04 % (3463416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.71/4.04 % (3463416)CaDiCaL version: 2.1.3
% 23.71/4.04 % (3463416)Termination reason: Instruction limit
% 23.71/4.04 % (3463416)Termination phase: Saturation
% 23.71/4.04 % (3463416)Time elapsed: 0.266 s
% 23.71/4.04 % (3463416)Peak memory usage: 13 MB
% 23.71/4.04 % (3463416)Instructions burned: 302 (million)
% 23.71/4.04 % (3463430)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=4085103007:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2969 on theBenchmark for (2969ds/372Mi)
% 23.71/4.04 % (3463430)Refutation not found, incomplete strategy
% 23.71/4.04 % (3463430)------------------------------
% 23.71/4.04 % (3463430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.71/4.04 % (3463430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.71/4.04 % (3463430)CaDiCaL version: 2.1.3
% 23.71/4.04 % (3463430)Termination reason: Refutation not found, incomplete strategy
% 23.71/4.04 % (3463430)Time elapsed: 0.007 s
% 23.71/4.04 % (3463430)Peak memory usage: 12 MB
% 23.71/4.04 % (3463430)Instructions burned: 7 (million)
% 23.71/4.04 % (3463430)------------------------------
% 23.71/4.04 % (3463430)------------------------------
% 23.71/4.04 % (3463432)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=3647652223:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2969 on theBenchmark for (2969ds/670Mi)
% 23.71/4.04 % (3463432)Refutation not found, incomplete strategy
% 23.71/4.04 % (3463432)------------------------------
% 23.71/4.04 % (3463432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.71/4.04 % (3463432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.71/4.04 % (3463432)CaDiCaL version: 2.1.3
% 23.71/4.04 % (3463432)Termination reason: Refutation not found, incomplete strategy
% 23.71/4.04 % (3463432)Time elapsed: 0.007 s
% 23.71/4.04 % (3463432)Peak memory usage: 12 MB
% 23.71/4.04 % (3463432)Instructions burned: 12 (million)
% 23.71/4.04 % (3463432)------------------------------
% 23.71/4.04 % (3463432)------------------------------
% 23.71/4.04 % (3463434)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=190158375:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2969 on theBenchmark for (2969ds/647Mi)
% 23.71/4.04 % (3463434)Refutation not found, incomplete strategy
% 23.71/4.04 % (3463434)------------------------------
% 23.71/4.04 % (3463434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.71/4.04 % (3463434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.71/4.04 % (3463434)CaDiCaL version: 2.1.3
% 23.71/4.04 % (3463434)Termination reason: Refutation not found, incomplete strategy
% 23.71/4.04 % (3463434)Time elapsed: 0.003 s
% 23.71/4.04 % (3463434)Peak memory usage: 12 MB
% 23.71/4.04 % (3463434)Instructions burned: 2 (million)
% 23.71/4.04 % (3463434)------------------------------
% 23.71/4.04 % (3463434)------------------------------
% 23.71/4.04 % (3463437)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=1451967833:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2969 on theBenchmark for (2969ds/693Mi)
% 29.91/4.56 % (3463435)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=1374151945:i=857:add=off:kws=frequency:rtra=on:ntd=on_2969 on theBenchmark for (2969ds/857Mi)
% 29.91/4.56 % (3463440)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=1441595911:i=285:hud=10:bd=all:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/285Mi)
% 29.91/4.56 % (3463425)Instruction limit reached!
% 29.91/4.56 % (3463425)------------------------------
% 29.91/4.56 % (3463425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.91/4.56 % (3463425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/4.56 % (3463425)CaDiCaL version: 2.1.3
% 29.91/4.56 % (3463425)Termination reason: Instruction limit
% 29.91/4.56 % (3463425)Termination phase: Saturation
% 29.91/4.56 % (3463425)Time elapsed: 0.232 s
% 29.91/4.56 % (3463425)Peak memory usage: 13 MB
% 29.91/4.56 % (3463425)Instructions burned: 290 (million)
% 29.91/4.56 % (3463443)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 29.91/4.56 % (3463443)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=2905618304:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2967 on theBenchmark for (2967ds/52Mi)
% 29.91/4.56 % (3463443)Instruction limit reached!
% 29.91/4.56 % (3463443)------------------------------
% 29.91/4.56 % (3463443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.91/4.56 % (3463443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/4.56 % (3463443)CaDiCaL version: 2.1.3
% 29.91/4.56 % (3463443)Termination reason: Instruction limit
% 29.91/4.56 % (3463443)Termination phase: Saturation
% 29.91/4.56 % (3463443)Time elapsed: 0.045 s
% 29.91/4.56 % (3463443)Peak memory usage: 12 MB
% 29.91/4.56 % (3463443)Instructions burned: 53 (million)
% 29.91/4.56 % (3463437)Instruction limit reached!
% 29.91/4.56 % (3463437)------------------------------
% 29.91/4.56 % (3463437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.91/4.56 % (3463437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/4.56 % (3463437)CaDiCaL version: 2.1.3
% 29.91/4.56 % (3463437)Termination reason: Instruction limit
% 29.91/4.56 % (3463437)Termination phase: Saturation
% 29.91/4.56 % (3463437)Time elapsed: 0.257 s
% 29.91/4.56 % (3463437)Peak memory usage: 13 MB
% 29.91/4.56 % (3463437)Instructions burned: 695 (million)
% 29.91/4.56 % (3463445)dis+10_1_si=on:random_seed=3426415880:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2966 on theBenchmark for (2966ds/407Mi)
% 29.91/4.56 % (3463440)Instruction limit reached!
% 29.91/4.56 % (3463440)------------------------------
% 29.91/4.56 % (3463440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.91/4.56 % (3463440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/4.56 % (3463440)CaDiCaL version: 2.1.3
% 29.91/4.56 % (3463440)Termination reason: Instruction limit
% 29.91/4.56 % (3463440)Termination phase: Saturation
% 29.91/4.56 % (3463440)Time elapsed: 0.231 s
% 29.91/4.56 % (3463440)Peak memory usage: 14 MB
% 29.91/4.56 % (3463440)Instructions burned: 285 (million)
% 29.91/4.56 % (3463446)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=69656508:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2966 on theBenchmark for (2966ds/2240Mi)
% 29.91/4.56 % (3463448)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=3970046054:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2966 on theBenchmark for (2966ds/336Mi)
% 29.91/4.56 % (3463448)Instruction limit reached!
% 29.91/4.56 % (3463448)------------------------------
% 29.91/4.56 % (3463448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.91/4.56 % (3463448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/4.56 % (3463448)CaDiCaL version: 2.1.3
% 29.91/4.56 % (3463448)Termination reason: Instruction limit
% 29.91/4.56 % (3463448)Termination phase: Saturation
% 29.91/4.56 % (3463448)Time elapsed: 0.251 s
% 29.91/4.56 % (3463448)Peak memory usage: 13 MB
% 29.91/4.56 % (3463448)Instructions burned: 336 (million)
% 29.91/4.56 % (3463451)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=2438775714:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2963 on theBenchmark for (2963ds/1142Mi)
% 32.11/4.83 % (3463445)Instruction limit reached!
% 32.11/4.83 % (3463445)------------------------------
% 32.11/4.83 % (3463445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.11/4.83 % (3463445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.11/4.83 % (3463445)CaDiCaL version: 2.1.3
% 32.11/4.83 % (3463445)Termination reason: Instruction limit
% 32.11/4.83 % (3463445)Termination phase: Saturation
% 32.11/4.83 % (3463445)Time elapsed: 0.332 s
% 32.11/4.83 % (3463445)Peak memory usage: 13 MB
% 32.11/4.83 % (3463445)Instructions burned: 408 (million)
% 32.11/4.83 % (3463453)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=3966686341:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2963 on theBenchmark for (2963ds/376Mi)
% 32.11/4.83 % (3463453)Refutation not found, incomplete strategy
% 32.11/4.83 % (3463453)------------------------------
% 32.11/4.83 % (3463453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.11/4.83 % (3463453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.11/4.83 % (3463453)CaDiCaL version: 2.1.3
% 32.11/4.83 % (3463453)Termination reason: Refutation not found, incomplete strategy
% 32.11/4.83 % (3463453)Time elapsed: 0.016 s
% 32.11/4.83 % (3463453)Peak memory usage: 12 MB
% 32.11/4.83 % (3463453)Instructions burned: 16 (million)
% 32.11/4.83 % (3463435)Instruction limit reached!
% 32.11/4.83 % (3463435)------------------------------
% 32.11/4.83 % (3463435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.11/4.83 % (3463435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.11/4.83 % (3463435)CaDiCaL version: 2.1.3
% 32.11/4.83 % (3463435)Termination reason: Instruction limit
% 32.11/4.83 % (3463435)Termination phase: Saturation
% 32.11/4.83 % (3463435)Time elapsed: 0.641 s
% 32.11/4.83 % (3463435)Peak memory usage: 14 MB
% 32.11/4.83 % (3463435)Instructions burned: 857 (million)
% 32.11/4.83 % (3463453)------------------------------
% 32.11/4.83 % (3463453)------------------------------
% 32.11/4.83 % (3463456)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 32.11/4.83 % (3463455)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=1574208852:i=766:bd=all:rtra=on_2962 on theBenchmark for (2962ds/766Mi)
% 32.11/4.83 % (3463374)Instruction limit reached!
% 32.11/4.83 % (3463374)------------------------------
% 32.11/4.83 % (3463374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.11/4.83 % (3463374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.11/4.83 % (3463374)CaDiCaL version: 2.1.3
% 32.11/4.83 % (3463374)Termination reason: Instruction limit
% 32.11/4.83 % (3463374)Termination phase: Saturation
% 32.11/4.83 % (3463374)Time elapsed: 1.985 s
% 32.11/4.83 % (3463374)Peak memory usage: 21 MB
% 32.11/4.83 % (3463456)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=2376757919: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_2962 on theBenchmark for (2962ds/959Mi)
% 32.11/4.83 % (3463374)Instructions burned: 2471 (million)
% 32.11/4.83 % (3463455)Refutation not found, incomplete strategy
% 32.11/4.83 % (3463455)------------------------------
% 32.11/4.83 % (3463455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.11/4.83 % (3463455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.11/4.83 % (3463455)CaDiCaL version: 2.1.3
% 32.11/4.83 % (3463455)Termination reason: Refutation not found, incomplete strategy
% 32.11/4.83 % (3463455)Time elapsed: 0.010 s
% 32.11/4.83 % (3463455)Peak memory usage: 13 MB
% 32.11/4.83 % (3463455)Instructions burned: 8 (million)
% 32.11/4.83 % (3463455)------------------------------
% 32.11/4.83 % (3463455)------------------------------
% 32.11/4.83 % (3463459)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=2996743834:i=6359:add=on:kws=inv_frequency:aac=none:rtra=on:c=on:er=filter:ntd=on_2962 on theBenchmark for (2962ds/6359Mi)
% 32.11/4.83 % (3463460)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1749340201:st=4:i=35:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2962 on theBenchmark for (2962ds/35Mi)
% 32.11/4.83 % (3463460)Refutation not found, incomplete strategy
% 32.53/5.05 % (3463460)------------------------------
% 32.53/5.05 % (3463460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/5.05 % (3463460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.05 % (3463460)CaDiCaL version: 2.1.3
% 32.53/5.05 % (3463460)Termination reason: Refutation not found, incomplete strategy
% 32.53/5.05 % (3463460)Time elapsed: 0.012 s
% 32.53/5.05 % (3463460)Peak memory usage: 12 MB
% 32.53/5.05 % (3463460)Instructions burned: 10 (million)
% 32.53/5.05 % (3463460)------------------------------
% 32.53/5.05 % (3463460)------------------------------
% 32.53/5.05 % (3463463)dis+10_1_sfv=off:sil=128000:cnfonf=lazy_gen:si=on:uwa=off:nwc=1:chr=on:random_seed=1984687290:hsq=on:hsqr=1,8:i=53:hsql=off:bd=all:rtra=on:ixr=off_2961 on theBenchmark for (2961ds/53Mi)
% 32.53/5.05 % (3463463)Instruction limit reached!
% 32.53/5.05 % (3463463)------------------------------
% 32.53/5.05 % (3463463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/5.05 % (3463463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.05 % (3463463)CaDiCaL version: 2.1.3
% 32.53/5.05 % (3463463)Termination reason: Instruction limit
% 32.53/5.05 % (3463463)Termination phase: Saturation
% 32.53/5.05 % (3463463)Time elapsed: 0.051 s
% 32.53/5.05 % (3463463)Peak memory usage: 12 MB
% 32.53/5.05 % (3463463)Instructions burned: 54 (million)
% 32.53/5.05 % (3463465)dis+21_1_sil=128000:tgt=full:fde=none:e2e=on:si=on:urr=on:uwa=interpreted_only:s2agt=32:sac=on:random_seed=1302321276:s2a=on:i=876:s2at=6:nm=2:rtra=on_2960 on theBenchmark for (2960ds/876Mi)
% 32.53/5.05 % (3463465)Refutation not found, incomplete strategy
% 32.53/5.05 % (3463465)------------------------------
% 32.53/5.05 % (3463465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/5.05 % (3463465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.05 % (3463465)CaDiCaL version: 2.1.3
% 32.53/5.05 % (3463465)Termination reason: Refutation not found, incomplete strategy
% 32.53/5.05 % (3463465)Time elapsed: 0.051 s
% 32.53/5.05 % (3463465)Peak memory usage: 12 MB
% 32.53/5.05 % (3463465)Instructions burned: 47 (million)
% 32.53/5.05 % (3463465)------------------------------
% 32.53/5.05 % (3463465)------------------------------
% 32.53/5.05 % (3463467)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=321367116:i=57:ep=R:rtra=on:ntd=on_2960 on theBenchmark for (2960ds/57Mi)
% 32.53/5.05 % (3463467)Refutation not found, incomplete strategy
% 32.53/5.05 % (3463467)------------------------------
% 32.53/5.05 % (3463467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/5.05 % (3463467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.05 % (3463467)CaDiCaL version: 2.1.3
% 32.53/5.05 % (3463467)Termination reason: Refutation not found, incomplete strategy
% 32.53/5.05 % (3463467)Time elapsed: 0.009 s
% 32.53/5.05 % (3463467)Peak memory usage: 12 MB
% 32.53/5.05 % (3463467)Instructions burned: 8 (million)
% 32.53/5.05 % (3463467)------------------------------
% 32.53/5.05 % (3463467)------------------------------
% 32.53/5.05 % (3463469)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 32.53/5.05 % (3463469)dis+1002_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_min:sos=on:fd=preordered:slsqc=2:chr=on:random_seed=1510643133:i=306:bd=all:rtra=on_2959 on theBenchmark for (2959ds/306Mi)
% 32.53/5.05 % (3463446)Instruction limit reached!
% 32.53/5.05 % (3463446)------------------------------
% 32.53/5.05 % (3463446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/5.05 % (3463446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.05 % (3463446)CaDiCaL version: 2.1.3
% 32.53/5.05 % (3463446)Termination reason: Instruction limit
% 32.53/5.05 % (3463446)Termination phase: Saturation
% 32.53/5.05 % (3463446)Time elapsed: 0.845 s
% 32.53/5.05 % (3463446)Peak memory usage: 15 MB
% 32.53/5.05 % (3463446)Instructions burned: 2240 (million)
% 32.53/5.05 % (3463471)dis+10_8:1_sil=128000:si=on:uwa=off:random_seed=3455171647:i=262:sd=2:bd=preordered:rtra=on:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/262Mi)
% 32.53/5.05 % (3463471)Instruction limit reached!
% 32.53/5.05 % (3463471)------------------------------
% 32.53/5.05 % (3463471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/5.05 % (3463471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.04/5.38 % (3463471)CaDiCaL version: 2.1.3
% 35.04/5.38 % (3463471)Termination reason: Instruction limit
% 35.04/5.38 % (3463471)Termination phase: Saturation
% 35.04/5.38 % (3463471)Time elapsed: 0.114 s
% 35.04/5.38 % (3463471)Peak memory usage: 13 MB
% 35.04/5.38 % (3463471)Instructions burned: 267 (million)
% 35.04/5.38 % (3463473)WARNING Broken Constraint: if ho_split_queue_ratios(1,3) has been set then ho_split_queue(off) is equal to on
% 35.04/5.38 % (3463473)ott+1002_16_sil=128000:si=on:random_seed=352286292:hsqr=1,3:i=409:add=on:rtra=on:fe=abstraction_2956 on theBenchmark for (2956ds/409Mi)
% 35.04/5.38 % (3463469)Instruction limit reached!
% 35.04/5.38 % (3463469)------------------------------
% 35.04/5.38 % (3463469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.04/5.38 % (3463469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.04/5.38 % (3463469)CaDiCaL version: 2.1.3
% 35.04/5.38 % (3463469)Termination reason: Instruction limit
% 35.04/5.38 % (3463469)Termination phase: Saturation
% 35.04/5.38 % (3463469)Time elapsed: 0.290 s
% 35.04/5.38 % (3463469)Peak memory usage: 13 MB
% 35.04/5.38 % (3463469)Instructions burned: 306 (million)
% 35.04/5.38 % (3463475)dis+10_1_sil=128000:plsq=on:si=on:plsqr=32,1:uwa=off:random_seed=111175914:s2a=on:i=381:rtra=on_2956 on theBenchmark for (2956ds/381Mi)
% 35.04/5.38 % (3463456)Instruction limit reached!
% 35.04/5.38 % (3463456)------------------------------
% 35.04/5.38 % (3463456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.04/5.38 % (3463456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.04/5.38 % (3463456)CaDiCaL version: 2.1.3
% 35.04/5.38 % (3463456)Termination reason: Instruction limit
% 35.04/5.38 % (3463456)Termination phase: Saturation
% 35.04/5.38 % (3463456)Time elapsed: 0.759 s
% 35.04/5.38 % (3463456)Peak memory usage: 15 MB
% 35.04/5.38 % (3463456)Instructions burned: 959 (million)
% 35.04/5.38 % (3463473)Instruction limit reached!
% 35.04/5.38 % (3463473)------------------------------
% 35.04/5.38 % (3463473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.04/5.38 % (3463473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.04/5.38 % (3463473)CaDiCaL version: 2.1.3
% 35.04/5.38 % (3463473)Termination reason: Instruction limit
% 35.04/5.38 % (3463473)Termination phase: Saturation
% 35.04/5.38 % (3463473)Time elapsed: 0.182 s
% 35.04/5.38 % (3463473)Peak memory usage: 14 MB
% 35.04/5.38 % (3463473)Instructions burned: 410 (million)
% 35.04/5.38 % (3463477)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4246877502:cond=on:i=324:rtra=on:ntd=on_2954 on theBenchmark for (2954ds/324Mi)
% 35.04/5.38 % (3463478)lrs+10_1_sil=128000:fde=none:si=on:sos=on:spb=goal_then_units:urr=on:random_seed=3098038524:i=240:kws=inv_precedence:rtra=on_2954 on theBenchmark for (2954ds/240Mi)
% 35.04/5.38 % (3463451)Instruction limit reached!
% 35.04/5.38 % (3463451)------------------------------
% 35.04/5.38 % (3463451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.04/5.38 % (3463451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.04/5.38 % (3463451)CaDiCaL version: 2.1.3
% 35.04/5.38 % (3463451)Termination reason: Instruction limit
% 35.04/5.38 % (3463451)Termination phase: Saturation
% 35.04/5.38 % (3463451)Time elapsed: 0.897 s
% 35.04/5.38 % (3463451)Peak memory usage: 14 MB
% 35.04/5.38 % (3463451)Instructions burned: 1143 (million)
% 35.04/5.38 % (3463477)Refutation not found, incomplete strategy
% 35.04/5.38 % (3463477)------------------------------
% 35.04/5.38 % (3463477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.04/5.38 % (3463477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.04/5.38 % (3463477)CaDiCaL version: 2.1.3
% 35.04/5.38 % (3463477)Termination reason: Refutation not found, incomplete strategy
% 35.04/5.38 % (3463477)Time elapsed: 0.020 s
% 35.04/5.38 % (3463477)Peak memory usage: 12 MB
% 35.04/5.38 % (3463477)Instructions burned: 19 (million)
% 35.04/5.38 % (3463477)------------------------------
% 35.04/5.38 % (3463477)------------------------------
% 35.04/5.38 % (3463481)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 35.04/5.38 % (3463481)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1949208560:cts=off:uwa_fpi=on:i=124:av=off:fsr=off:rtra=on:ntd=on_2954 on theBenchmark for (2954ds/124Mi)
% 35.04/5.38 % (3463482)lrs+1010_2_to=lpo:cnfonf=off:e2e=on:si=on:random_seed=2981079140:uwa_fpi=on:i=223:bd=all:rtra=on:fe=abstraction:ntd=on_2954 on theBenchmark for (2954ds/223Mi)
% 35.74/5.48 % (3463478)Instruction limit reached!
% 35.74/5.48 % (3463478)------------------------------
% 35.74/5.48 % (3463478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463478)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463478)Termination reason: Instruction limit
% 35.74/5.48 % (3463478)Termination phase: Saturation
% 35.74/5.48 % (3463478)Time elapsed: 0.105 s
% 35.74/5.48 % (3463478)Peak memory usage: 13 MB
% 35.74/5.48 % (3463478)Instructions burned: 242 (million)
% 35.74/5.48 % (3463485)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=422449194:s2a=on:i=282:kws=inv_frequency:bd=all:rtra=on_2953 on theBenchmark for (2953ds/282Mi)
% 35.74/5.48 % (3463481)Instruction limit reached!
% 35.74/5.48 % (3463481)------------------------------
% 35.74/5.48 % (3463481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463481)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463481)Termination reason: Instruction limit
% 35.74/5.48 % (3463481)Termination phase: Saturation
% 35.74/5.48 % (3463481)Time elapsed: 0.103 s
% 35.74/5.48 % (3463481)Peak memory usage: 12 MB
% 35.74/5.48 % (3463481)Instructions burned: 124 (million)
% 35.74/5.48 % (3463475)Instruction limit reached!
% 35.74/5.48 % (3463475)------------------------------
% 35.74/5.48 % (3463475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463475)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463475)Termination reason: Instruction limit
% 35.74/5.48 % (3463475)Termination phase: Saturation
% 35.74/5.48 % (3463475)Time elapsed: 0.320 s
% 35.74/5.48 % (3463475)Peak memory usage: 13 MB
% 35.74/5.48 % (3463475)Instructions burned: 381 (million)
% 35.74/5.48 % (3463487)lrs+10_1_sil=128000:tgt=ground:cnfonf=conj_eager:si=on:random_seed=295984290:s2a=on:i=464:kws=frequency:bd=all:rtra=on:ss=axioms_2953 on theBenchmark for (2953ds/464Mi)
% 35.74/5.48 % (3463488)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=3056831962:i=88:s2at=3:nm=2:rtra=on:rawr=on_2952 on theBenchmark for (2952ds/88Mi)
% 35.74/5.48 % (3463482)Instruction limit reached!
% 35.74/5.48 % (3463482)------------------------------
% 35.74/5.48 % (3463482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463482)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463482)Termination reason: Instruction limit
% 35.74/5.48 % (3463482)Termination phase: Saturation
% 35.74/5.48 % (3463482)Time elapsed: 0.188 s
% 35.74/5.48 % (3463482)Peak memory usage: 13 MB
% 35.74/5.48 % (3463482)Instructions burned: 223 (million)
% 35.74/5.48 % (3463485)Instruction limit reached!
% 35.74/5.48 % (3463485)------------------------------
% 35.74/5.48 % (3463485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463485)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463485)Termination reason: Instruction limit
% 35.74/5.48 % (3463485)Termination phase: Saturation
% 35.74/5.48 % (3463485)Time elapsed: 0.126 s
% 35.74/5.48 % (3463485)Peak memory usage: 13 MB
% 35.74/5.48 % (3463485)Instructions burned: 282 (million)
% 35.74/5.48 % (3463492)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 35.74/5.48 % (3463492)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1226770311:i=4386:hud=10:nm=16:av=off:rtra=on:ntd=on_2951 on theBenchmark for (2951ds/4386Mi)
% 35.74/5.48 % (3463488)Instruction limit reached!
% 35.74/5.48 % (3463488)------------------------------
% 35.74/5.48 % (3463488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463488)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463488)Termination reason: Instruction limit
% 35.74/5.48 % (3463488)Termination phase: Saturation
% 35.74/5.48 % (3463488)Time elapsed: 0.075 s
% 35.74/5.48 % (3463488)Peak memory usage: 13 MB
% 35.74/5.48 % (3463488)Instructions burned: 93 (million)
% 35.74/5.48 % (3463491)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=1896496726:s2a=on:cond=on:i=280:add=on:bd=preordered:rtra=on:er=filter_2952 on theBenchmark for (2952ds/280Mi)
% 35.74/5.48 % (3463495)WARNING Broken Constraint: if lookahaed_delay(10) has been set then selection(21) is not lookahead selection
% 35.74/5.48 % (3463495)WARNING Broken Constraint: if mono_ep(off) has been set then equality_proxy(off) is not equal to off
% 35.74/5.48 % (3463495)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=4232769430:hsq=on:st=2:i=483:sd=1:hsql=off:rtra=on:fe=abstraction:fdi=32:ss=axioms:sgt=20:ntd=on_2951 on theBenchmark for (2951ds/483Mi)
% 35.74/5.48 % (3463102)Instruction limit reached!
% 35.74/5.48 % (3463102)------------------------------
% 35.74/5.48 % (3463102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463102)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463102)Termination reason: Instruction limit
% 35.74/5.48 % (3463102)Termination phase: Saturation
% 35.74/5.48 % (3463102)Time elapsed: 4.412 s
% 35.74/5.48 % (3463102)Peak memory usage: 44 MB
% 35.74/5.48 % (3463102)Instructions burned: 5756 (million)
% 35.74/5.48 % (3463497)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3235096010:i=73:rtra=on_2950 on theBenchmark for (2950ds/73Mi)
% 35.74/5.48 % (3463491)Instruction limit reached!
% 35.74/5.48 % (3463491)------------------------------
% 35.74/5.48 % (3463491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463491)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463491)Termination reason: Instruction limit
% 35.74/5.48 % (3463491)Termination phase: Saturation
% 35.74/5.48 % (3463491)Time elapsed: 0.251 s
% 35.74/5.48 % (3463491)Peak memory usage: 13 MB
% 35.74/5.48 % (3463491)Instructions burned: 281 (million)
% 35.74/5.48 % (3463497)Instruction limit reached!
% 35.74/5.48 % (3463497)------------------------------
% 35.74/5.48 % (3463497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463497)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463497)Termination reason: Instruction limit
% 35.74/5.48 % (3463497)Termination phase: Saturation
% 35.74/5.48 % (3463497)Time elapsed: 0.070 s
% 35.74/5.48 % (3463497)Peak memory usage: 12 MB
% 35.74/5.48 % (3463497)Instructions burned: 73 (million)
% 35.74/5.48 % (3463499)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=418669746:cts=off:i=176:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2949 on theBenchmark for (2949ds/176Mi)
% 35.74/5.48 % (3463487)Instruction limit reached!
% 35.74/5.48 % (3463487)------------------------------
% 35.74/5.48 % (3463487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463487)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463487)Termination reason: Instruction limit
% 35.74/5.48 % (3463487)Termination phase: Saturation
% 35.74/5.48 % (3463487)Time elapsed: 0.385 s
% 35.74/5.48 % (3463487)Peak memory usage: 13 MB
% 35.74/5.48 % (3463487)Instructions burned: 464 (million)
% 35.74/5.48 % (3463500)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 35.74/5.48 % (3463500)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=1921195207:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2949 on theBenchmark for (2949ds/39Mi)
% 35.74/5.48 % (3463502)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3321903420:i=708:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2948 on theBenchmark for (2948ds/708Mi)
% 35.74/5.48 % (3463500)Instruction limit reached!
% 35.74/5.48 % (3463500)------------------------------
% 35.74/5.48 % (3463500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463500)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463500)Termination reason: Instruction limit
% 35.74/5.48 % (3463500)Termination phase: Saturation
% 35.74/5.48 % (3463500)Time elapsed: 0.035 s
% 35.74/5.48 % (3463500)Peak memory usage: 12 MB
% 35.74/5.48 % (3463500)Instructions burned: 39 (million)
% 35.74/5.48 % (3463505)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 35.74/5.48 % (3463505)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=529554051:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2948 on theBenchmark for (2948ds/252Mi)
% 35.74/5.48 % (3463499) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3462881-3463499"...
% 35.74/5.48 % (3463499)...printing done.
% 35.74/5.48 % (3463499)Refutation found. Thanks to Tanya!
% 35.74/5.48 % SZS status Theorem for theBenchmark
% 35.74/5.48 % SZS output start Proof for theBenchmark
% See solution above
% 35.74/5.48 % (3463499)------------------------------
% 35.74/5.48 % (3463499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.74/5.48 % (3463499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.48 % (3463499)CaDiCaL version: 2.1.3
% 35.74/5.48 % (3463499)Termination reason: Refutation
% 35.74/5.48 % (3463499)Time elapsed: 0.138 s
% 35.74/5.48 % (3463499)Peak memory usage: 14 MB
% 35.74/5.48 % (3463499)Instructions burned: 163 (million)
% 35.74/5.48 % (3462881)Success in time 5.259 s
% 35.74/5.48 % Vampire exiting
%------------------------------------------------------------------------------