%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU960^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 : n002.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:02 AM UTC 2026
% Result : Theorem 22.16s 3.79s
% Output : Refutation 22.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 3
% Syntax : Number of formulae : 67 ( 32 unt; 0 typ; 2 def)
% Number of atoms : 330 ( 72 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 1060 ( 24 ~; 36 |; 63 &; 718 @)
% ( 2 <=>; 121 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 358 ( 358 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 25 usr; 6 con; 0-4 aty)
% ( 96 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 304 ( 10 sgn 38 !; 0 ?; 304 :)
% 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,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_3,type,
vIMP: $o > $o > $o ).
thf(func_def_4,type,
vAND: $o > $o > $o ).
thf(func_def_5,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_6,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_7,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_8,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_9,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_10,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_13,type,
sK0: a > a ).
thf(func_def_14,type,
sK1: a > a ).
thf(func_def_15,type,
sK2: a > a ).
thf(func_def_16,type,
sK3: ( a > a ) > $o ).
thf(func_def_17,type,
sK4: ( ( a > a ) > $o ) > a > a ).
thf(func_def_18,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
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,
! [X2: a > a,X1: a > a,X0: a > a] :
( ( ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X1 ) )
& ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X2 ) ) )
=> ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3
@ ^ [X5: a] : ( X1 @ ( X2 @ X5 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM135D_pme) ).
thf(f2,negated_conjecture,
~ ! [X2: a > a,X1: a > a,X0: a > a] :
( ( ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X1 ) )
& ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X2 ) ) )
=> ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X0 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X0 @ ( X4 @ X5 ) ) ) ) )
=> ( X3
@ ^ [X5: a] : ( X1 @ ( X2 @ X5 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ! [X0: a > a,X1: a > a,X2: a > a] :
( ( ! [X3: ( a > a ) > $o] :
( ( ( X3 @ X2 )
& ! [X4: a > a] :
( ( X3 @ X4 )
=> ( X3
@ ^ [X5: a] : ( X2 @ ( X4 @ X5 ) ) ) ) )
=> ( X3 @ X1 ) )
& ! [X6: ( a > a ) > $o] :
( ( ( X6 @ X2 )
& ! [X7: a > a] :
( ( X6 @ X7 )
=> ( X6
@ ^ [X8: a] : ( X2 @ ( X7 @ X8 ) ) ) ) )
=> ( X6 @ X0 ) ) )
=> ! [X9: ( a > a ) > $o] :
( ( ( X9 @ X2 )
& ! [X10: a > a] :
( ( X9 @ X10 )
=> ( X9
@ ^ [X11: a] : ( X2 @ ( X10 @ X11 ) ) ) ) )
=> ( X9
@ ^ [X12: a] : ( X1 @ ( X0 @ X12 ) ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
( $true
= ( ~ ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y1 @ ( Y2 @ Y4 ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( $true
= ( ~ ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y1 @ ( Y2 @ Y4 ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f4]) ).
thf(f8,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y1 @ ( Y2 @ Y4 ) ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f5]) ).
thf(f16,plain,
( $false
= ( ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3 @ Y1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y3: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y4: a > a] :
( ( Y3 @ Y4 )
=> ( Y3
@ ^ [Y5: a] : ( Y0 @ ( Y4 @ Y5 ) ) ) ) )
& ( Y3 @ Y0 ) )
=> ( Y3
@ ^ [Y4: a] : ( Y1 @ ( Y2 @ Y4 ) ) ) ) ) ) ) )
@ sK0 ) ),
inference(sigma_proxy_clausification,[],[f8]) ).
thf(f19,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK0 ) )
=> ( Y2 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK0 ) )
=> ( Y2 @ Y0 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK0 ) )
=> ( Y2
@ ^ [Y3: a] : ( Y0 @ ( Y1 @ Y3 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f16]) ).
thf(f20,plain,
( $false
= ( ^ [Y0: a > a] :
( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK0 ) )
=> ( Y2 @ Y1 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK0 ) )
=> ( Y2 @ Y0 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y2: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y3: a > a] :
( ( Y2 @ Y3 )
=> ( Y2
@ ^ [Y4: a] : ( sK0 @ ( Y3 @ Y4 ) ) ) ) )
& ( Y2 @ sK0 ) )
=> ( Y2
@ ^ [Y3: a] : ( Y0 @ ( Y1 @ Y3 ) ) ) ) ) ) )
@ sK1 ) ),
inference(sigma_proxy_clausification,[],[f19]) ).
thf(f23,plain,
( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK0 ) )
=> ( Y1 @ Y0 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK0 ) )
=> ( Y1 @ sK1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK0 ) )
=> ( Y1
@ ^ [Y2: a] : ( sK1 @ ( Y0 @ Y2 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f20]) ).
thf(f24,plain,
( $false
= ( ^ [Y0: a > a] :
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK0 ) )
=> ( Y1 @ Y0 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK0 ) )
=> ( Y1 @ sK1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y1: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y2: a > a] :
( ( Y1 @ Y2 )
=> ( Y1
@ ^ [Y3: a] : ( sK0 @ ( Y2 @ Y3 ) ) ) ) )
& ( Y1 @ sK0 ) )
=> ( Y1
@ ^ [Y2: a] : ( sK1 @ ( Y0 @ Y2 ) ) ) ) ) )
@ sK2 ) ),
inference(sigma_proxy_clausification,[],[f23]) ).
thf(f27,plain,
( $false
= ( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK1 ) ) ) )
=> ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0
@ ^ [Y1: a] : ( sK1 @ ( sK2 @ Y1 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f24]) ).
thf(f28,plain,
( $false
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0
@ ^ [Y1: a] : ( sK1 @ ( sK2 @ Y1 ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f27]) ).
thf(f29,plain,
( ( ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK2 ) ) )
& ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK1 ) ) ) )
= $true ),
inference(imp_proxy_clausification,[],[f27]) ).
thf(f30,plain,
( $true
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK1 ) ) ) ),
inference(and_proxy_clausification,[],[f29]) ).
thf(f31,plain,
( $true
= ( !! @ ( ( a > a ) > $o )
@ ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK2 ) ) ) ),
inference(and_proxy_clausification,[],[f29]) ).
thf(f32,plain,
( $false
= ( ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0
@ ^ [Y1: a] : ( sK1 @ ( sK2 @ Y1 ) ) ) )
@ sK3 ) ),
inference(sigma_proxy_clausification,[],[f28]) ).
thf(f34,plain,
( $false
= ( ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( sK3 @ sK0 ) )
=> ( sK3
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f32]) ).
thf(f36,plain,
( $false
= ( sK3
@ ^ [Y0: a] : ( sK1 @ ( sK2 @ Y0 ) ) ) ),
inference(imp_proxy_clausification,[],[f34]) ).
thf(f37,plain,
( $true
= ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( sK3 @ sK0 ) ) ),
inference(imp_proxy_clausification,[],[f34]) ).
thf(f38,plain,
( $true
= ( sK3 @ sK0 ) ),
inference(and_proxy_clausification,[],[f37]) ).
thf(f39,plain,
( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
= $true ),
inference(and_proxy_clausification,[],[f37]) ).
thf(f42,plain,
! [X1: a > a] :
( $true
= ( ^ [Y0: a > a] :
( ( sK3 @ Y0 )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f39]) ).
thf(f43,plain,
! [X1: a > a] :
( $true
= ( ( sK3 @ X1 )
=> ( sK3
@ ^ [Y0: a] : ( sK0 @ ( X1 @ Y0 ) ) ) ) ),
inference(beta-eta_normalization,[],[f42]) ).
thf(f44,plain,
! [X1: a > a] :
( ( $true
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( X1 @ Y0 ) ) ) )
| ( $false
= ( sK3 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f43]) ).
thf(f45,plain,
! [X1: ( a > a ) > $o] :
( ( ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK1 ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f30]) ).
thf(f46,plain,
! [X1: ( a > a ) > $o] :
( $true
= ( ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( X1 @ sK0 ) )
=> ( X1 @ sK1 ) ) ),
inference(beta-eta_normalization,[],[f45]) ).
thf(f47,plain,
! [X1: ( a > a ) > $o] :
( ( $true
= ( X1 @ sK1 ) )
| ( $false
= ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( X1 @ sK0 ) ) ) ),
inference(imp_proxy_clausification,[],[f46]) ).
thf(f48,plain,
! [X1: ( a > a ) > $o] :
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $true
= ( X1 @ sK1 ) )
| ( ( X1 @ sK0 )
= $false ) ),
inference(and_proxy_clausification,[],[f47]) ).
thf(f73,plain,
( ( $false
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] :
( sK2
@ ( ^ [Y5: a > a,Y6: a] : Y6
@ Y3
@ Y4 ) )
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK0 ) )
| ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ^ [Y1: a > a] :
( sK3
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK2
@ ( ^ [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] :
( sK2
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $false = $true ) ),
inference(constrained_superposition,[],[f36,f48]) ).
thf(f116,plain,
( ( $false
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] :
( sK2
@ ( ^ [Y5: a > a,Y6: a] : Y6
@ Y3
@ Y4 ) )
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK0 ) )
| ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( ^ [Y1: a > a] :
( sK3
@ ( ^ [Y2: a > a,Y3: a] :
( Y2
@ ( ^ [Y4: a > a,Y5: a] :
( sK2
@ ( ^ [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] :
( sK2
@ ( ^ [Y6: a > a,Y7: a] : Y7
@ Y4
@ Y5 ) )
@ Y2
@ Y3 ) )
@ Y1 ) )
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) ) ),
inference(trivial_inequality_removal,[],[f73]) ).
thf(f117,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK2 @ Y0 ) ) ) )
| ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f116]) ).
thf(f131,definition,
( spl5_1
<=> ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
thf(f133,plain,
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) ) ) )
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f131]) ).
thf(f135,definition,
( spl5_2
<=> ( $false
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK2 @ Y0 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
thf(f137,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK2 @ Y0 ) ) ) )
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f135]) ).
thf(f162,plain,
( spl5_2
| spl5_1 ),
inference(avatar_split_clause,[],[f117,f131,f135]) ).
thf(f168,plain,
! [X1: ( a > a ) > $o] :
( $true
= ( ^ [Y0: ( a > a ) > $o] :
( ( ( !! @ ( a > a )
@ ^ [Y1: a > a] :
( ( Y0 @ Y1 )
=> ( Y0
@ ^ [Y2: a] : ( sK0 @ ( Y1 @ Y2 ) ) ) ) )
& ( Y0 @ sK0 ) )
=> ( Y0 @ sK2 ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f31]) ).
thf(f169,plain,
! [X1: ( a > a ) > $o] :
( ( ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( X1 @ sK0 ) )
=> ( X1 @ sK2 ) )
= $true ),
inference(beta-eta_normalization,[],[f168]) ).
thf(f170,plain,
! [X1: ( a > a ) > $o] :
( ( $true
= ( X1 @ sK2 ) )
| ( $false
= ( ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) )
& ( X1 @ sK0 ) ) ) ),
inference(imp_proxy_clausification,[],[f169]) ).
thf(f171,plain,
! [X1: ( a > a ) > $o] :
( ( $false
= ( !! @ ( a > a )
@ ^ [Y0: a > a] :
( ( X1 @ Y0 )
=> ( X1
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ Y1 ) ) ) ) ) )
| ( $true
= ( X1 @ sK2 ) )
| ( ( X1 @ sK0 )
= $false ) ),
inference(and_proxy_clausification,[],[f170]) ).
thf(f180,plain,
( ( ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK0 )
= $false )
| ( $false = $true )
| ( $true
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK2 ) ) ),
inference(constrained_superposition,[],[f171,f39]) ).
thf(f204,plain,
( ( ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK0 )
= $false )
| ( $true
= ( ^ [Y0: a > a] :
( sK3
@ ( ^ [Y1: a > a,Y2: a] :
( Y1
@ ( ^ [Y3: a > a,Y4: a] : Y4
@ Y1
@ Y2 ) )
@ Y0 ) )
@ sK2 ) ) ),
inference(trivial_inequality_removal,[],[f180]) ).
thf(f205,plain,
( ( $false
= ( sK3 @ sK0 ) )
| ( ( sK3 @ sK2 )
= $true ) ),
inference(beta-eta_normalization,[],[f204]) ).
thf(f250,plain,
( ( $false = $true )
| ( ( sK3 @ sK2 )
= $true ) ),
inference(forward_demodulation,[],[f205,f38]) ).
thf(f251,plain,
( ( sK3 @ sK2 )
= $true ),
inference(trivial_inequality_removal,[],[f250]) ).
thf(f283,plain,
( ( $false = $true )
| ( $false
= ( sK3
@ ^ [Y0: a] :
( sK2
@ ( ^ [Y1: a] : Y1
@ Y0 ) ) ) )
| ~ spl5_2 ),
inference(constrained_superposition,[],[f137,f44]) ).
thf(f286,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] :
( sK2
@ ( ^ [Y1: a] : Y1
@ Y0 ) ) ) )
| ~ spl5_2 ),
inference(trivial_inequality_removal,[],[f283]) ).
thf(f287,plain,
( ( $false
= ( sK3 @ sK2 ) )
| ~ spl5_2 ),
inference(beta-eta_normalization,[],[f286]) ).
thf(f311,plain,
( ( $false
= ( ^ [Y0: a > a] :
( ( sK3
@ ^ [Y1: a] : ( Y0 @ ( sK2 @ Y1 ) ) )
=> ( sK3
@ ^ [Y1: a] : ( sK0 @ ( Y0 @ ( sK2 @ Y1 ) ) ) ) )
@ sK6 ) )
| ~ spl5_1 ),
inference(sigma_proxy_clausification,[],[f133]) ).
thf(f313,plain,
( ( $false
= ( ( sK3
@ ^ [Y0: a] : ( sK6 @ ( sK2 @ Y0 ) ) )
=> ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK6 @ ( sK2 @ Y0 ) ) ) ) ) )
| ~ spl5_1 ),
inference(beta-eta_normalization,[],[f311]) ).
thf(f315,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] : ( sK0 @ ( sK6 @ ( sK2 @ Y0 ) ) ) ) )
| ~ spl5_1 ),
inference(imp_proxy_clausification,[],[f313]) ).
thf(f316,plain,
( ( ( sK3
@ ^ [Y0: a] : ( sK6 @ ( sK2 @ Y0 ) ) )
= $true )
| ~ spl5_1 ),
inference(imp_proxy_clausification,[],[f313]) ).
thf(f326,plain,
( ( $false = $true )
| ( $false
= ( sK3
@ ^ [Y0: a] :
( sK6
@ ( ^ [Y1: a] :
( sK2
@ ( ^ [Y2: a] : Y2
@ Y1 ) )
@ Y0 ) ) ) )
| ~ spl5_1 ),
inference(constrained_superposition,[],[f315,f44]) ).
thf(f328,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] :
( sK6
@ ( ^ [Y1: a] :
( sK2
@ ( ^ [Y2: a] : Y2
@ Y1 ) )
@ Y0 ) ) ) )
| ~ spl5_1 ),
inference(trivial_inequality_removal,[],[f326]) ).
thf(f329,plain,
( ( $false
= ( sK3
@ ^ [Y0: a] : ( sK6 @ ( sK2 @ Y0 ) ) ) )
| ~ spl5_1 ),
inference(beta-eta_normalization,[],[f328]) ).
thf(f334,plain,
( ( $false = $true )
| ~ spl5_1 ),
inference(backward_demodulation,[],[f316,f329]) ).
thf(f337,plain,
( $false
| ~ spl5_1 ),
inference(trivial_inequality_removal,[],[f334]) ).
thf(f338,plain,
~ spl5_1,
inference(avatar_contradiction_clause,[],[f337]) ).
thf(f540,plain,
( ( $false = $true )
| ~ spl5_2 ),
inference(backward_demodulation,[],[f251,f287]) ).
thf(f563,plain,
( $false
| ~ spl5_2 ),
inference(trivial_inequality_removal,[],[f540]) ).
thf(f564,plain,
~ spl5_2,
inference(avatar_contradiction_clause,[],[f563]) ).
cnf(s4,plain,
( spl5_1
| spl5_2 ),
inference(sat_conversion,[],[f162]) ).
cnf(s10,plain,
~ spl5_1,
inference(sat_conversion,[],[f338]) ).
cnf(s15,plain,
~ spl5_2,
inference(sat_conversion,[],[f564]) ).
cnf(s16,plain,
$false,
inference(rat,[],[s4,s15,s10]) ).
thf(f569,plain,
$false,
inference(avatar_sat_refutation,[],[s16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU960^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 14:53:37 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.09/0.24 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.22/0.36 % (1396708)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.36 % (1396725)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=300756932:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.36 % (1396731)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.36 % (1396731)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.22/0.36 % (1396726)lrs+10_16_si=on:nwc=1.5:random_seed=704868164:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.36 % (1396727)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=438864173:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.36 % (1396730)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2690225733:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.36 % (1396731)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=1142099863:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.36 % (1396729)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2889253353:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.36 % (1396728)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=4227284705: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.22/0.36 % (1396727)Instruction limit reached!
% 0.22/0.36 % (1396727)------------------------------
% 0.22/0.36 % (1396727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (1396727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (1396727)CaDiCaL version: 2.1.3
% 0.22/0.36 % (1396727)Termination reason: Instruction limit
% 0.22/0.36 % (1396727)Termination phase: Saturation
% 0.22/0.36 % (1396727)Time elapsed: 0.003 s
% 0.22/0.36 % (1396727)Peak memory usage: 12 MB
% 0.22/0.36 % (1396727)Instructions burned: 4 (million)
% 0.22/0.36 % (1396729)Refutation not found, incomplete strategy
% 0.22/0.36 % (1396729)------------------------------
% 0.22/0.36 % (1396729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (1396729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (1396729)CaDiCaL version: 2.1.3
% 0.22/0.36 % (1396729)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.36 % (1396729)Time elapsed: 0.008 s
% 0.22/0.36 % (1396729)Peak memory usage: 12 MB
% 0.22/0.36 % (1396729)Instructions burned: 13 (million)
% 0.22/0.36 % (1396728)Refutation not found, incomplete strategy
% 0.22/0.36 % (1396728)------------------------------
% 0.22/0.36 % (1396728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (1396728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (1396728)CaDiCaL version: 2.1.3
% 0.22/0.36 % (1396728)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.36 % (1396728)Time elapsed: 0.008 s
% 0.22/0.36 % (1396728)Peak memory usage: 12 MB
% 0.22/0.36 % (1396728)Instructions burned: 11 (million)
% 0.22/0.36 % (1396729)------------------------------
% 0.22/0.36 % (1396729)------------------------------
% 0.22/0.36 % (1396728)------------------------------
% 0.22/0.36 % (1396728)------------------------------
% 0.22/0.36 % (1396726)Instruction limit reached!
% 0.22/0.36 % (1396726)------------------------------
% 0.22/0.36 % (1396726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (1396726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (1396726)CaDiCaL version: 2.1.3
% 0.22/0.36 % (1396726)Termination reason: Instruction limit
% 0.22/0.36 % (1396726)Termination phase: Saturation
% 0.22/0.36 % (1396726)Time elapsed: 0.011 s
% 0.22/0.36 % (1396726)Peak memory usage: 12 MB
% 0.22/0.36 % (1396726)Instructions burned: 20 (million)
% 0.22/0.36 % (1396731)Refutation not found, incomplete strategy
% 0.22/0.36 % (1396731)------------------------------
% 0.22/0.36 % (1396731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.38 % (1396731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.38 % (1396731)CaDiCaL version: 2.1.3
% 0.71/0.38 % (1396731)Termination reason: Refutation not found, incomplete strategy
% 0.71/0.38 % (1396731)Time elapsed: 0.014 s
% 0.71/0.38 % (1396731)Peak memory usage: 12 MB
% 0.71/0.38 % (1396731)Instructions burned: 24 (million)
% 0.71/0.38 % (1396731)------------------------------
% 0.71/0.38 % (1396731)------------------------------
% 0.71/0.38 % (1396725)Instruction limit reached!
% 0.71/0.38 % (1396725)------------------------------
% 0.71/0.38 % (1396725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.38 % (1396725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.38 % (1396725)CaDiCaL version: 2.1.3
% 0.71/0.38 % (1396725)Termination reason: Instruction limit
% 0.71/0.38 % (1396725)Termination phase: Saturation
% 0.71/0.38 % (1396725)Time elapsed: 0.025 s
% 0.71/0.38 % (1396725)Peak memory usage: 12 MB
% 0.71/0.38 % (1396725)Instructions burned: 90 (million)
% 0.71/0.38 % (1396750)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=606133208:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.71/0.38 % (1396755)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.71/0.38 % (1396750)Instruction limit reached!
% 0.71/0.38 % (1396750)------------------------------
% 0.71/0.38 % (1396750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.38 % (1396750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.38 % (1396750)CaDiCaL version: 2.1.3
% 0.71/0.38 % (1396750)Termination reason: Instruction limit
% 0.71/0.38 % (1396750)Termination phase: Saturation
% 0.71/0.38 % (1396750)Time elapsed: 0.002 s
% 0.71/0.38 % (1396750)Peak memory usage: 12 MB
% 0.71/0.38 % (1396750)Instructions burned: 2 (million)
% 0.71/0.38 % (1396764)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=4056926974:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.71/0.38 % (1396755)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=517845609:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.71/0.38 % (1396754)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=561450100:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.71/0.38 % (1396756)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3597980656:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.71/0.38 % (1396761)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.71/0.38 % (1396761)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.71/0.38 % (1396755)Instruction limit reached!
% 0.71/0.38 % (1396755)------------------------------
% 0.71/0.38 % (1396755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.38 % (1396755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.38 % (1396755)CaDiCaL version: 2.1.3
% 0.71/0.38 % (1396755)Termination reason: Instruction limit
% 0.71/0.38 % (1396755)Termination phase: Saturation
% 0.71/0.38 % (1396755)Time elapsed: 0.004 s
% 0.71/0.38 % (1396755)Peak memory usage: 12 MB
% 0.71/0.38 % (1396755)Instructions burned: 7 (million)
% 0.71/0.38 % (1396754)Instruction limit reached!
% 0.71/0.38 % (1396754)------------------------------
% 0.71/0.38 % (1396754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.38 % (1396754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.38 % (1396754)CaDiCaL version: 2.1.3
% 0.71/0.38 % (1396754)Termination reason: Instruction limit
% 0.71/0.38 % (1396754)Termination phase: Saturation
% 0.71/0.38 % (1396754)Time elapsed: 0.004 s
% 0.71/0.38 % (1396754)Peak memory usage: 12 MB
% 0.71/0.38 % (1396754)Instructions burned: 6 (million)
% 0.71/0.38 % (1396761)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3083568903: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.71/0.40 % (1396730)Instruction limit reached!
% 0.71/0.40 % (1396730)------------------------------
% 0.71/0.40 % (1396730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.40 % (1396730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.40 % (1396730)CaDiCaL version: 2.1.3
% 0.71/0.40 % (1396730)Termination reason: Instruction limit
% 0.71/0.40 % (1396730)Termination phase: Saturation
% 0.71/0.40 % (1396730)Time elapsed: 0.042 s
% 0.71/0.40 % (1396730)Peak memory usage: 12 MB
% 0.71/0.40 % (1396730)Instructions burned: 78 (million)
% 0.71/0.40 % (1396756)Instruction limit reached!
% 0.71/0.40 % (1396756)------------------------------
% 0.71/0.40 % (1396756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.40 % (1396756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.40 % (1396756)CaDiCaL version: 2.1.3
% 0.71/0.40 % (1396756)Termination reason: Instruction limit
% 0.71/0.40 % (1396756)Termination phase: Saturation
% 0.71/0.40 % (1396756)Time elapsed: 0.011 s
% 0.71/0.40 % (1396756)Peak memory usage: 12 MB
% 0.71/0.40 % (1396756)Instructions burned: 19 (million)
% 0.71/0.40 % (1396771)lrs+10_1_si=on:cs=on:random_seed=1341979751:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.71/0.40 % (1396776)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.71/0.40 % (1396771)Instruction limit reached!
% 0.71/0.40 % (1396771)------------------------------
% 0.71/0.40 % (1396771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.40 % (1396764)Instruction limit reached!
% 0.71/0.40 % (1396764)------------------------------
% 0.71/0.40 % (1396764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.40 % (1396771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.40 % (1396771)CaDiCaL version: 2.1.3
% 0.71/0.40 % (1396771)Termination reason: Instruction limit
% 0.71/0.40 % (1396771)Termination phase: Saturation
% 0.71/0.40 % (1396764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.40 % (1396771)Time elapsed: 0.005 s
% 0.71/0.40 % (1396771)Peak memory usage: 12 MB
% 0.71/0.40 % (1396771)Instructions burned: 8 (million)
% 0.71/0.40 % (1396764)CaDiCaL version: 2.1.3
% 0.71/0.40 % (1396764)Termination reason: Instruction limit
% 0.71/0.40 % (1396764)Termination phase: Saturation
% 0.71/0.40 % (1396764)Time elapsed: 0.023 s
% 0.71/0.40 % (1396764)Peak memory usage: 12 MB
% 0.71/0.40 % (1396764)Instructions burned: 89 (million)
% 0.71/0.40 % (1396776)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=3209528534:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.71/0.40 % (1396777)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=906373457:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.71/0.40 % (1396761)Instruction limit reached!
% 0.71/0.40 % (1396761)------------------------------
% 0.71/0.40 % (1396761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.40 % (1396761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.40 % (1396761)CaDiCaL version: 2.1.3
% 0.71/0.40 % (1396761)Termination reason: Instruction limit
% 0.71/0.40 % (1396761)Termination phase: Saturation
% 0.71/0.40 % (1396761)Time elapsed: 0.019 s
% 0.71/0.40 % (1396761)Peak memory usage: 12 MB
% 0.71/0.40 % (1396761)Instructions burned: 28 (million)
% 0.71/0.40 % (1396776)Instruction limit reached!
% 0.71/0.40 % (1396776)------------------------------
% 0.71/0.40 % (1396776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.40 % (1396776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.40 % (1396776)CaDiCaL version: 2.1.3
% 0.71/0.40 % (1396776)Termination reason: Instruction limit
% 0.71/0.40 % (1396776)Termination phase: Saturation
% 0.71/0.40 % (1396776)Time elapsed: 0.002 s
% 0.71/0.40 % (1396776)Peak memory usage: 11 MB
% 0.71/0.40 % (1396776)Instructions burned: 3 (million)
% 0.71/0.40 % (1396788)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3496816543:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.71/0.40 % (1396784)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=382544466:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.71/0.43 % (1396788)Instruction limit reached!
% 0.71/0.43 % (1396788)------------------------------
% 0.71/0.43 % (1396788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.43 % (1396788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.43 % (1396788)CaDiCaL version: 2.1.3
% 0.71/0.43 % (1396788)Termination reason: Instruction limit
% 0.71/0.43 % (1396788)Termination phase: Saturation
% 0.71/0.43 % (1396788)Time elapsed: 0.006 s
% 0.71/0.43 % (1396788)Peak memory usage: 12 MB
% 0.71/0.43 % (1396788)Instructions burned: 17 (million)
% 0.71/0.43 % (1396789)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1648194433:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.71/0.43 % (1396785)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2543766443:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.71/0.43 % (1396785)Refutation not found, incomplete strategy
% 0.71/0.43 % (1396785)------------------------------
% 0.71/0.43 % (1396785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.43 % (1396785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.43 % (1396785)CaDiCaL version: 2.1.3
% 0.71/0.43 % (1396785)Termination reason: Refutation not found, incomplete strategy
% 0.71/0.43 % (1396785)Time elapsed: 0.002 s
% 0.71/0.43 % (1396785)Peak memory usage: 12 MB
% 0.71/0.43 % (1396785)Instructions burned: 2 (million)
% 0.71/0.43 % (1396792)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=369285061:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.71/0.43 % (1396784)Refutation not found, incomplete strategy
% 0.71/0.43 % (1396784)------------------------------
% 0.71/0.43 % (1396784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.43 % (1396784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.43 % (1396784)CaDiCaL version: 2.1.3
% 0.71/0.43 % (1396784)Termination reason: Refutation not found, incomplete strategy
% 0.71/0.43 % (1396784)Time elapsed: 0.007 s
% 0.71/0.43 % (1396784)Peak memory usage: 12 MB
% 0.71/0.43 % (1396784)Instructions burned: 11 (million)
% 0.71/0.43 % (1396785)------------------------------
% 0.71/0.43 % (1396785)------------------------------
% 0.71/0.43 % (1396777)Instruction limit reached!
% 0.71/0.43 % (1396777)------------------------------
% 0.71/0.43 % (1396777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.43 % (1396793)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2446907294: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.71/0.43 % (1396777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.43 % (1396777)CaDiCaL version: 2.1.3
% 0.71/0.43 % (1396777)Termination reason: Instruction limit
% 0.71/0.43 % (1396777)Termination phase: Saturation
% 0.71/0.43 % (1396777)Time elapsed: 0.021 s
% 0.71/0.43 % (1396777)Peak memory usage: 12 MB
% 0.71/0.43 % (1396777)Instructions burned: 39 (million)
% 0.71/0.43 % (1396784)------------------------------
% 0.71/0.43 % (1396784)------------------------------
% 0.71/0.43 % (1396793)Instruction limit reached!
% 0.71/0.43 % (1396793)------------------------------
% 0.71/0.43 % (1396793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.43 % (1396793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.43 % (1396793)CaDiCaL version: 2.1.3
% 0.71/0.43 % (1396793)Termination reason: Instruction limit
% 0.71/0.43 % (1396793)Termination phase: Saturation
% 0.71/0.43 % (1396793)Time elapsed: 0.002 s
% 0.71/0.43 % (1396793)Peak memory usage: 12 MB
% 0.71/0.43 % (1396793)Instructions burned: 2 (million)
% 0.71/0.43 % (1396796)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=783021679:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.71/0.43 % (1396796)Refutation not found, incomplete strategy
% 0.71/0.43 % (1396796)------------------------------
% 0.71/0.43 % (1396796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.43 % (1396796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.47 % (1396796)CaDiCaL version: 2.1.3
% 0.71/0.47 % (1396796)Termination reason: Refutation not found, incomplete strategy
% 0.71/0.47 % (1396796)Time elapsed: 0.002 s
% 0.71/0.47 % (1396796)Peak memory usage: 12 MB
% 0.71/0.47 % (1396796)Instructions burned: 7 (million)
% 0.71/0.47 % (1396796)------------------------------
% 0.71/0.47 % (1396796)------------------------------
% 0.71/0.47 % (1396792)Instruction limit reached!
% 0.71/0.47 % (1396792)------------------------------
% 0.71/0.47 % (1396792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.47 % (1396792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.47 % (1396792)CaDiCaL version: 2.1.3
% 0.71/0.47 % (1396792)Termination reason: Instruction limit
% 0.71/0.47 % (1396792)Termination phase: Saturation
% 0.71/0.47 % (1396792)Time elapsed: 0.009 s
% 0.71/0.47 % (1396792)Peak memory usage: 12 MB
% 0.71/0.47 % (1396792)Instructions burned: 15 (million)
% 0.71/0.47 % (1396805)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.71/0.47 % (1396805)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.71/0.47 % (1396806)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.71/0.47 % (1396810)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=3601550442:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.71/0.47 % (1396804)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=495286660:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.71/0.47 % (1396805)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=109839776:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.71/0.47 % (1396806)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=620278221:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.71/0.47 % (1396803)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=862454423:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.71/0.47 % (1396804)Refutation not found, incomplete strategy
% 0.71/0.47 % (1396804)------------------------------
% 0.71/0.47 % (1396804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.47 % (1396804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.47 % (1396804)CaDiCaL version: 2.1.3
% 0.71/0.47 % (1396804)Termination reason: Refutation not found, incomplete strategy
% 0.71/0.47 % (1396804)Time elapsed: 0.004 s
% 0.71/0.47 % (1396804)Peak memory usage: 12 MB
% 0.71/0.47 % (1396804)Instructions burned: 6 (million)
% 0.71/0.47 % (1396804)------------------------------
% 0.71/0.47 % (1396804)------------------------------
% 0.71/0.47 % (1396811)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1619539045:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.71/0.47 % (1396810)Instruction limit reached!
% 0.71/0.47 % (1396810)------------------------------
% 0.71/0.47 % (1396810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.47 % (1396810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.47 % (1396810)CaDiCaL version: 2.1.3
% 0.71/0.47 % (1396810)Termination reason: Instruction limit
% 0.71/0.47 % (1396810)Termination phase: Saturation
% 0.71/0.47 % (1396810)Time elapsed: 0.009 s
% 0.71/0.47 % (1396810)Peak memory usage: 12 MB
% 0.71/0.47 % (1396810)Instructions burned: 34 (million)
% 0.71/0.47 % (1396806)Instruction limit reached!
% 0.71/0.47 % (1396806)------------------------------
% 0.71/0.47 % (1396806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.71/0.47 % (1396806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.71/0.47 % (1396806)CaDiCaL version: 2.1.3
% 0.71/0.47 % (1396806)Termination reason: Instruction limit
% 0.71/0.47 % (1396806)Termination phase: Saturation
% 0.71/0.47 % (1396806)Time elapsed: 0.006 s
% 0.71/0.47 % (1396806)Peak memory usage: 12 MB
% 1.54/0.53 % (1396806)Instructions burned: 9 (million)
% 1.54/0.53 % (1396805)Instruction limit reached!
% 1.54/0.53 % (1396805)------------------------------
% 1.54/0.53 % (1396805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (1396805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (1396805)CaDiCaL version: 2.1.3
% 1.54/0.53 % (1396805)Termination reason: Instruction limit
% 1.54/0.53 % (1396805)Termination phase: Saturation
% 1.54/0.53 % (1396805)Time elapsed: 0.009 s
% 1.54/0.53 % (1396805)Peak memory usage: 12 MB
% 1.54/0.53 % (1396805)Instructions burned: 15 (million)
% 1.54/0.53 % (1396811)Instruction limit reached!
% 1.54/0.53 % (1396811)------------------------------
% 1.54/0.53 % (1396811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (1396811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (1396811)CaDiCaL version: 2.1.3
% 1.54/0.53 % (1396811)Termination reason: Instruction limit
% 1.54/0.53 % (1396811)Termination phase: Saturation
% 1.54/0.53 % (1396811)Time elapsed: 0.004 s
% 1.54/0.53 % (1396811)Peak memory usage: 12 MB
% 1.54/0.53 % (1396811)Instructions burned: 8 (million)
% 1.54/0.53 % (1396803)Instruction limit reached!
% 1.54/0.53 % (1396803)------------------------------
% 1.54/0.53 % (1396803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (1396803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (1396803)CaDiCaL version: 2.1.3
% 1.54/0.53 % (1396803)Termination reason: Instruction limit
% 1.54/0.53 % (1396803)Termination phase: Saturation
% 1.54/0.53 % (1396803)Time elapsed: 0.015 s
% 1.54/0.53 % (1396803)Peak memory usage: 11 MB
% 1.54/0.53 % (1396803)Instructions burned: 24 (million)
% 1.54/0.53 % (1396825)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4085666309:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.54/0.53 % (1396826)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2297231583:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.54/0.53 % (1396822)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=408783676:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.54/0.53 % (1396825)Instruction limit reached!
% 1.54/0.53 % (1396825)------------------------------
% 1.54/0.53 % (1396825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (1396825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (1396825)CaDiCaL version: 2.1.3
% 1.54/0.53 % (1396825)Termination reason: Instruction limit
% 1.54/0.53 % (1396825)Termination phase: Saturation
% 1.54/0.53 % (1396825)Time elapsed: 0.009 s
% 1.54/0.53 % (1396825)Peak memory usage: 12 MB
% 1.54/0.53 % (1396825)Instructions burned: 29 (million)
% 1.54/0.53 % (1396827)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=45810751:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.54/0.53 % (1396829)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2516230254:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.54/0.53 % (1396839)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.54/0.53 % (1396839)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3417076098:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.54/0.53 % (1396822)Instruction limit reached!
% 1.54/0.53 % (1396822)------------------------------
% 1.54/0.53 % (1396822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (1396822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (1396822)CaDiCaL version: 2.1.3
% 1.54/0.53 % (1396822)Termination reason: Instruction limit
% 1.54/0.53 % (1396822)Termination phase: Saturation
% 1.54/0.53 % (1396822)Time elapsed: 0.010 s
% 1.54/0.53 % (1396822)Peak memory usage: 11 MB
% 1.54/0.53 % (1396822)Instructions burned: 25 (million)
% 1.54/0.53 % (1396829)Refutation not found, incomplete strategy
% 1.54/0.53 % (1396829)------------------------------
% 1.54/0.53 % (1396829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (1396829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.59 % (1396829)CaDiCaL version: 2.1.3
% 1.54/0.59 % (1396829)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.59 % (1396829)Time elapsed: 0.007 s
% 1.54/0.59 % (1396829)Peak memory usage: 12 MB
% 1.54/0.59 % (1396829)Instructions burned: 10 (million)
% 1.54/0.59 % (1396831)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=261595262:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.54/0.59 % (1396826)Refutation not found, incomplete strategy
% 1.54/0.59 % (1396826)------------------------------
% 1.54/0.59 % (1396826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.59 % (1396826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.59 % (1396826)CaDiCaL version: 2.1.3
% 1.54/0.59 % (1396826)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.59 % (1396826)Time elapsed: 0.011 s
% 1.54/0.59 % (1396826)Peak memory usage: 12 MB
% 1.54/0.59 % (1396826)Instructions burned: 11 (million)
% 1.54/0.59 % (1396829)------------------------------
% 1.54/0.59 % (1396829)------------------------------
% 1.54/0.59 % (1396826)------------------------------
% 1.54/0.59 % (1396826)------------------------------
% 1.54/0.59 % (1396839)Instruction limit reached!
% 1.54/0.59 % (1396839)------------------------------
% 1.54/0.59 % (1396839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.59 % (1396839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.59 % (1396839)CaDiCaL version: 2.1.3
% 1.54/0.59 % (1396839)Termination reason: Instruction limit
% 1.54/0.59 % (1396839)Termination phase: Saturation
% 1.54/0.59 % (1396839)Time elapsed: 0.002 s
% 1.54/0.59 % (1396839)Peak memory usage: 12 MB
% 1.54/0.59 % (1396839)Instructions burned: 8 (million)
% 1.54/0.59 % (1396847)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.54/0.59 % (1396845)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1577312930:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.54/0.59 % (1396846)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=2914399789: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.54/0.59 % (1396831)Instruction limit reached!
% 1.54/0.59 % (1396831)------------------------------
% 1.54/0.59 % (1396831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.59 % (1396831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.59 % (1396831)CaDiCaL version: 2.1.3
% 1.54/0.59 % (1396831)Termination reason: Instruction limit
% 1.54/0.59 % (1396831)Termination phase: Saturation
% 1.54/0.59 % (1396831)Time elapsed: 0.020 s
% 1.54/0.59 % (1396831)Peak memory usage: 12 MB
% 1.54/0.59 % (1396831)Instructions burned: 43 (million)
% 1.54/0.59 % (1396847)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2719108484: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.54/0.59 % (1396847)Instruction limit reached!
% 1.54/0.59 % (1396847)------------------------------
% 1.54/0.59 % (1396847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.59 % (1396847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.59 % (1396847)CaDiCaL version: 2.1.3
% 1.54/0.59 % (1396847)Termination reason: Instruction limit
% 1.54/0.59 % (1396847)Termination phase: Saturation
% 1.54/0.59 % (1396847)Time elapsed: 0.004 s
% 1.54/0.59 % (1396847)Peak memory usage: 12 MB
% 1.54/0.59 % (1396847)Instructions burned: 6 (million)
% 1.54/0.59 % (1396848)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1539104442:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 1.54/0.59 % (1396827)Instruction limit reached!
% 1.54/0.59 % (1396827)------------------------------
% 1.54/0.59 % (1396827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.59 % (1396827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.59 % (1396827)CaDiCaL version: 2.1.3
% 1.54/0.59 % (1396827)Termination reason: Instruction limit
% 1.54/0.59 % (1396827)Termination phase: Saturation
% 1.54/0.59 % (1396827)Time elapsed: 0.047 s
% 2.35/0.62 % (1396827)Peak memory usage: 13 MB
% 2.35/0.62 % (1396827)Instructions burned: 144 (million)
% 2.35/0.62 % (1396852)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2495317143:i=19:add=on:rtra=on_2998 on theBenchmark for (2998ds/19Mi)
% 2.35/0.62 % (1396853)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=3842752044:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.35/0.62 % (1396848)Instruction limit reached!
% 2.35/0.62 % (1396848)------------------------------
% 2.35/0.62 % (1396848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.62 % (1396848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.62 % (1396848)CaDiCaL version: 2.1.3
% 2.35/0.62 % (1396848)Termination reason: Instruction limit
% 2.35/0.62 % (1396848)Termination phase: Saturation
% 2.35/0.62 % (1396848)Time elapsed: 0.013 s
% 2.35/0.62 % (1396848)Peak memory usage: 12 MB
% 2.35/0.62 % (1396848)Instructions burned: 22 (million)
% 2.35/0.62 % (1396857)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=3622646717:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.35/0.62 % (1396852)Refutation not found, incomplete strategy
% 2.35/0.62 % (1396852)------------------------------
% 2.35/0.62 % (1396852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.62 % (1396852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.62 % (1396852)CaDiCaL version: 2.1.3
% 2.35/0.62 % (1396852)Termination reason: Refutation not found, incomplete strategy
% 2.35/0.62 % (1396852)Time elapsed: 0.009 s
% 2.35/0.62 % (1396852)Peak memory usage: 12 MB
% 2.35/0.62 % (1396852)Instructions burned: 14 (million)
% 2.35/0.62 % (1396852)------------------------------
% 2.35/0.62 % (1396852)------------------------------
% 2.35/0.62 % (1396864)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=1337368087:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.35/0.62 % (1396869)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=466338599:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.35/0.62 % (1396869)Refutation not found, incomplete strategy
% 2.35/0.62 % (1396869)------------------------------
% 2.35/0.62 % (1396869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.62 % (1396869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.62 % (1396869)CaDiCaL version: 2.1.3
% 2.35/0.62 % (1396869)Termination reason: Refutation not found, incomplete strategy
% 2.35/0.62 % (1396869)Time elapsed: 0.007 s
% 2.35/0.62 % (1396869)Peak memory usage: 12 MB
% 2.35/0.62 % (1396869)Instructions burned: 11 (million)
% 2.35/0.62 % (1396869)------------------------------
% 2.35/0.62 % (1396869)------------------------------
% 2.35/0.62 % (1396846)Instruction limit reached!
% 2.35/0.62 % (1396846)------------------------------
% 2.35/0.62 % (1396846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.62 % (1396846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.62 % (1396846)CaDiCaL version: 2.1.3
% 2.35/0.62 % (1396846)Termination reason: Instruction limit
% 2.35/0.62 % (1396846)Termination phase: Saturation
% 2.35/0.62 % (1396846)Time elapsed: 0.075 s
% 2.35/0.62 % (1396846)Peak memory usage: 13 MB
% 2.35/0.62 % (1396846)Instructions burned: 171 (million)
% 2.35/0.62 % (1396789)Instruction limit reached!
% 2.35/0.62 % (1396789)------------------------------
% 2.35/0.62 % (1396789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.62 % (1396789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.62 % (1396789)CaDiCaL version: 2.1.3
% 2.35/0.62 % (1396789)Termination reason: Instruction limit
% 2.35/0.62 % (1396789)Termination phase: Saturation
% 2.35/0.62 % (1396789)Time elapsed: 0.162 s
% 2.35/0.62 % (1396789)Peak memory usage: 13 MB
% 2.35/0.62 % (1396789)Instructions burned: 329 (million)
% 2.35/0.62 % (1396879)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2356603486:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 2.82/0.72 % (1396864)Instruction limit reached!
% 2.82/0.72 % (1396864)------------------------------
% 2.82/0.72 % (1396864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.82/0.72 % (1396864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/0.72 % (1396864)CaDiCaL version: 2.1.3
% 2.82/0.72 % (1396864)Termination reason: Instruction limit
% 2.82/0.72 % (1396864)Termination phase: Saturation
% 2.82/0.72 % (1396864)Time elapsed: 0.032 s
% 2.82/0.72 % (1396864)Peak memory usage: 12 MB
% 2.82/0.72 % (1396864)Instructions burned: 46 (million)
% 2.82/0.72 % (1396884)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.82/0.72 % (1396845)Instruction limit reached!
% 2.82/0.72 % (1396845)------------------------------
% 2.82/0.72 % (1396845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.82/0.72 % (1396845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/0.72 % (1396845)CaDiCaL version: 2.1.3
% 2.82/0.72 % (1396845)Termination reason: Instruction limit
% 2.82/0.72 % (1396845)Termination phase: Saturation
% 2.82/0.72 % (1396845)Time elapsed: 0.093 s
% 2.82/0.72 % (1396845)Peak memory usage: 13 MB
% 2.82/0.72 % (1396845)Instructions burned: 181 (million)
% 2.82/0.72 % (1396884)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3699474258:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.82/0.72 % (1396879)Instruction limit reached!
% 2.82/0.72 % (1396879)------------------------------
% 2.82/0.72 % (1396879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.82/0.72 % (1396879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/0.72 % (1396879)CaDiCaL version: 2.1.3
% 2.82/0.72 % (1396879)Termination reason: Instruction limit
% 2.82/0.72 % (1396879)Termination phase: Saturation
% 2.82/0.72 % (1396879)Time elapsed: 0.016 s
% 2.82/0.72 % (1396879)Peak memory usage: 12 MB
% 2.82/0.72 % (1396879)Instructions burned: 21 (million)
% 2.82/0.72 % (1396885)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3999985450:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.82/0.72 % (1396887)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=2031970167:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.82/0.72 % (1396885)Instruction limit reached!
% 2.82/0.72 % (1396885)------------------------------
% 2.82/0.72 % (1396885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.82/0.72 % (1396885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/0.72 % (1396885)CaDiCaL version: 2.1.3
% 2.82/0.72 % (1396885)Termination reason: Instruction limit
% 2.82/0.72 % (1396885)Termination phase: Saturation
% 2.82/0.72 % (1396885)Time elapsed: 0.008 s
% 2.82/0.72 % (1396885)Peak memory usage: 12 MB
% 2.82/0.72 % (1396885)Instructions burned: 14 (million)
% 2.82/0.72 % (1396890)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=965483288:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 2.82/0.72 % (1396893)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1185240206:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.82/0.72 % (1396893)Refutation not found, incomplete strategy
% 2.82/0.72 % (1396893)------------------------------
% 2.82/0.72 % (1396893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.82/0.72 % (1396893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/0.72 % (1396893)CaDiCaL version: 2.1.3
% 2.82/0.72 % (1396893)Termination reason: Refutation not found, incomplete strategy
% 2.82/0.72 % (1396893)Time elapsed: 0.004 s
% 2.82/0.72 % (1396893)Peak memory usage: 12 MB
% 2.82/0.72 % (1396893)Instructions burned: 7 (million)
% 2.82/0.72 % (1396893)------------------------------
% 2.82/0.72 % (1396893)------------------------------
% 2.82/0.72 % (1396899)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1456118258:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 2.82/0.72 % (1396887)Instruction limit reached!
% 2.82/0.72 % (1396887)------------------------------
% 3.15/0.86 % (1396887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.15/0.86 % (1396887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/0.86 % (1396887)CaDiCaL version: 2.1.3
% 3.15/0.86 % (1396887)Termination reason: Instruction limit
% 3.15/0.86 % (1396887)Termination phase: Saturation
% 3.15/0.86 % (1396887)Time elapsed: 0.036 s
% 3.15/0.86 % (1396887)Peak memory usage: 12 MB
% 3.15/0.86 % (1396887)Instructions burned: 66 (million)
% 3.15/0.86 % (1396890)Instruction limit reached!
% 3.15/0.86 % (1396890)------------------------------
% 3.15/0.86 % (1396890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.15/0.86 % (1396890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/0.86 % (1396890)CaDiCaL version: 2.1.3
% 3.15/0.86 % (1396890)Termination reason: Instruction limit
% 3.15/0.86 % (1396890)Termination phase: Saturation
% 3.15/0.86 % (1396890)Time elapsed: 0.032 s
% 3.15/0.86 % (1396890)Peak memory usage: 12 MB
% 3.15/0.86 % (1396890)Instructions burned: 53 (million)
% 3.15/0.86 % (1396904)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=3441458026:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 3.15/0.86 % (1396899)Refutation not found, incomplete strategy
% 3.15/0.86 % (1396899)------------------------------
% 3.15/0.86 % (1396899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.15/0.86 % (1396899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/0.86 % (1396899)CaDiCaL version: 2.1.3
% 3.15/0.86 % (1396899)Termination reason: Refutation not found, incomplete strategy
% 3.15/0.86 % (1396899)Time elapsed: 0.013 s
% 3.15/0.86 % (1396899)Peak memory usage: 12 MB
% 3.15/0.86 % (1396899)Instructions burned: 18 (million)
% 3.15/0.86 % (1396899)------------------------------
% 3.15/0.86 % (1396899)------------------------------
% 3.15/0.86 % (1396909)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2525953252:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 3.15/0.86 % (1396904)Refutation not found, incomplete strategy
% 3.15/0.86 % (1396904)------------------------------
% 3.15/0.86 % (1396904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.15/0.86 % (1396904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/0.86 % (1396904)CaDiCaL version: 2.1.3
% 3.15/0.86 % (1396904)Termination reason: Refutation not found, incomplete strategy
% 3.15/0.86 % (1396904)Time elapsed: 0.018 s
% 3.15/0.86 % (1396904)Peak memory usage: 12 MB
% 3.15/0.86 % (1396904)Instructions burned: 20 (million)
% 3.15/0.86 % (1396904)------------------------------
% 3.15/0.86 % (1396904)------------------------------
% 3.15/0.86 % (1396911)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.15/0.86 % (1396915)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1089428165:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 3.15/0.86 % (1396911)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3855841356:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 3.15/0.86 % (1396915)Refutation not found, incomplete strategy
% 3.15/0.86 % (1396915)------------------------------
% 3.15/0.86 % (1396915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.15/0.86 % (1396915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/0.86 % (1396915)CaDiCaL version: 2.1.3
% 3.15/0.86 % (1396915)Termination reason: Refutation not found, incomplete strategy
% 3.15/0.86 % (1396915)Time elapsed: 0.005 s
% 3.15/0.86 % (1396915)Peak memory usage: 12 MB
% 3.15/0.86 % (1396915)Instructions burned: 7 (million)
% 3.15/0.86 % (1396915)------------------------------
% 3.15/0.86 % (1396915)------------------------------
% 3.15/0.86 % (1396853)Instruction limit reached!
% 3.15/0.86 % (1396853)------------------------------
% 3.15/0.86 % (1396853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.15/0.86 % (1396853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.15/0.86 % (1396853)CaDiCaL version: 2.1.3
% 3.15/0.86 % (1396853)Termination reason: Instruction limit
% 3.15/0.86 % (1396853)Termination phase: Saturation
% 3.15/0.86 % (1396853)Time elapsed: 0.150 s
% 3.15/0.86 % (1396853)Peak memory usage: 13 MB
% 3.40/1.00 % (1396853)Instructions burned: 318 (million)
% 3.40/1.00 % (1396884)Instruction limit reached!
% 3.40/1.00 % (1396884)------------------------------
% 3.40/1.00 % (1396884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/1.00 % (1396884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/1.00 % (1396884)CaDiCaL version: 2.1.3
% 3.40/1.00 % (1396884)Termination reason: Instruction limit
% 3.40/1.00 % (1396884)Termination phase: Saturation
% 3.40/1.00 % (1396884)Time elapsed: 0.094 s
% 3.40/1.00 % (1396884)Peak memory usage: 12 MB
% 3.40/1.00 % (1396884)Instructions burned: 200 (million)
% 3.40/1.00 % (1396921)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=581563406:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 3.40/1.00 % (1396909)Instruction limit reached!
% 3.40/1.00 % (1396909)------------------------------
% 3.40/1.00 % (1396909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/1.00 % (1396909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/1.00 % (1396909)CaDiCaL version: 2.1.3
% 3.40/1.00 % (1396909)Termination reason: Instruction limit
% 3.40/1.00 % (1396909)Termination phase: Saturation
% 3.40/1.00 % (1396909)Time elapsed: 0.036 s
% 3.40/1.00 % (1396909)Peak memory usage: 12 MB
% 3.40/1.00 % (1396909)Instructions burned: 69 (million)
% 3.40/1.00 % (1396925)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=37150203:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/874Mi)
% 3.40/1.00 % (1396924)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2494967998:i=427:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/427Mi)
% 3.40/1.00 % (1396928)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1186625347:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/515Mi)
% 3.40/1.00 % (1396931)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1867759642:st=1.5:i=130:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/130Mi)
% 3.40/1.00 % (1396921)Refutation not found, incomplete strategy
% 3.40/1.00 % (1396921)------------------------------
% 3.40/1.00 % (1396921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/1.00 % (1396921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/1.00 % (1396921)CaDiCaL version: 2.1.3
% 3.40/1.00 % (1396921)Termination reason: Refutation not found, incomplete strategy
% 3.40/1.00 % (1396921)Time elapsed: 0.037 s
% 3.40/1.00 % (1396921)Peak memory usage: 12 MB
% 3.40/1.00 % (1396921)Instructions burned: 56 (million)
% 3.40/1.00 % (1396921)------------------------------
% 3.40/1.00 % (1396921)------------------------------
% 3.40/1.00 % (1396931)Refutation not found, incomplete strategy
% 3.40/1.00 % (1396931)------------------------------
% 3.40/1.00 % (1396931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/1.00 % (1396931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/1.00 % (1396931)CaDiCaL version: 2.1.3
% 3.40/1.00 % (1396931)Termination reason: Refutation not found, incomplete strategy
% 3.40/1.00 % (1396931)Time elapsed: 0.019 s
% 3.40/1.00 % (1396931)Peak memory usage: 12 MB
% 3.40/1.00 % (1396931)Instructions burned: 25 (million)
% 3.40/1.00 % (1396931)------------------------------
% 3.40/1.00 % (1396931)------------------------------
% 3.40/1.00 % (1396951)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=563140031:i=44:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/44Mi)
% 3.40/1.00 % (1396952)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1065590057:s2a=on:i=571:nm=16:rtra=on_2995 on theBenchmark for (2995ds/571Mi)
% 3.40/1.00 % (1396951)Refutation not found, incomplete strategy
% 3.40/1.00 % (1396951)------------------------------
% 3.40/1.00 % (1396951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/1.00 % (1396951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/1.00 % (1396951)CaDiCaL version: 2.1.3
% 3.40/1.00 % (1396951)Termination reason: Refutation not found, incomplete strategy
% 3.40/1.00 % (1396951)Time elapsed: 0.005 s
% 3.40/1.00 % (1396951)Peak memory usage: 12 MB
% 3.40/1.00 % (1396951)Instructions burned: 8 (million)
% 3.40/1.00 % (1396951)------------------------------
% 3.40/1.00 % (1396951)------------------------------
% 3.40/1.00 % (1396911)Instruction limit reached!
% 5.42/1.07 % (1396911)------------------------------
% 5.42/1.07 % (1396911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (1396911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (1396911)CaDiCaL version: 2.1.3
% 5.42/1.07 % (1396911)Termination reason: Instruction limit
% 5.42/1.07 % (1396911)Termination phase: Saturation
% 5.42/1.07 % (1396911)Time elapsed: 0.104 s
% 5.42/1.07 % (1396911)Peak memory usage: 17 MB
% 5.42/1.07 % (1396911)Instructions burned: 182 (million)
% 5.42/1.07 % (1396857)Instruction limit reached!
% 5.42/1.07 % (1396857)------------------------------
% 5.42/1.07 % (1396857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (1396857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (1396857)CaDiCaL version: 2.1.3
% 5.42/1.07 % (1396857)Termination reason: Instruction limit
% 5.42/1.07 % (1396857)Termination phase: Saturation
% 5.42/1.07 % (1396857)Time elapsed: 0.251 s
% 5.42/1.07 % (1396857)Peak memory usage: 15 MB
% 5.42/1.07 % (1396857)Instructions burned: 854 (million)
% 5.42/1.07 % (1396957)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3454667425:i=450:rtra=on:ixr=off:ntd=on_2995 on theBenchmark for (2995ds/450Mi)
% 5.42/1.07 % (1396958)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=649378591:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/95Mi)
% 5.42/1.07 % (1396959)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=781844612:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 5.42/1.07 % (1396959)Refutation not found, incomplete strategy
% 5.42/1.07 % (1396959)------------------------------
% 5.42/1.07 % (1396959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (1396959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (1396959)CaDiCaL version: 2.1.3
% 5.42/1.07 % (1396959)Termination reason: Refutation not found, incomplete strategy
% 5.42/1.07 % (1396959)Time elapsed: 0.006 s
% 5.42/1.07 % (1396959)Peak memory usage: 12 MB
% 5.42/1.07 % (1396959)Instructions burned: 18 (million)
% 5.42/1.07 % (1396959)------------------------------
% 5.42/1.07 % (1396959)------------------------------
% 5.42/1.07 % (1396963)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=1941604844:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2995 on theBenchmark for (2995ds/105Mi)
% 5.42/1.07 % (1396963)Instruction limit reached!
% 5.42/1.07 % (1396963)------------------------------
% 5.42/1.07 % (1396963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (1396963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (1396963)CaDiCaL version: 2.1.3
% 5.42/1.07 % (1396963)Termination reason: Instruction limit
% 5.42/1.07 % (1396963)Termination phase: Saturation
% 5.42/1.07 % (1396963)Time elapsed: 0.029 s
% 5.42/1.07 % (1396963)Peak memory usage: 13 MB
% 5.42/1.07 % (1396963)Instructions burned: 109 (million)
% 5.42/1.07 % (1396958)Instruction limit reached!
% 5.42/1.07 % (1396958)------------------------------
% 5.42/1.07 % (1396958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (1396958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (1396958)CaDiCaL version: 2.1.3
% 5.42/1.07 % (1396958)Termination reason: Instruction limit
% 5.42/1.07 % (1396958)Termination phase: Saturation
% 5.42/1.07 % (1396958)Time elapsed: 0.050 s
% 5.42/1.07 % (1396958)Peak memory usage: 12 MB
% 5.42/1.07 % (1396958)Instructions burned: 96 (million)
% 5.42/1.07 % (1396965)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=2277024124: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)
% 5.42/1.07 % (1396966)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=49020614:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/375Mi)
% 5.42/1.07 % (1396924)Instruction limit reached!
% 5.42/1.07 % (1396924)------------------------------
% 5.82/1.18 % (1396924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.18 % (1396924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.18 % (1396924)CaDiCaL version: 2.1.3
% 5.82/1.18 % (1396924)Termination reason: Instruction limit
% 5.82/1.18 % (1396924)Termination phase: Saturation
% 5.82/1.18 % (1396924)Time elapsed: 0.215 s
% 5.82/1.18 % (1396924)Peak memory usage: 13 MB
% 5.82/1.18 % (1396924)Instructions burned: 429 (million)
% 5.82/1.18 % (1396972)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=776673305:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/495Mi)
% 5.82/1.18 % (1396928)Instruction limit reached!
% 5.82/1.18 % (1396928)------------------------------
% 5.82/1.18 % (1396928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.18 % (1396928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.18 % (1396928)CaDiCaL version: 2.1.3
% 5.82/1.18 % (1396928)Termination reason: Instruction limit
% 5.82/1.18 % (1396928)Termination phase: Saturation
% 5.82/1.18 % (1396928)Time elapsed: 0.245 s
% 5.82/1.18 % (1396928)Peak memory usage: 13 MB
% 5.82/1.18 % (1396928)Instructions burned: 517 (million)
% 5.82/1.18 % (1396991)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=3100836551:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 5.82/1.18 % (1396991)Instruction limit reached!
% 5.82/1.18 % (1396991)------------------------------
% 5.82/1.18 % (1396991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.18 % (1396991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.18 % (1396991)CaDiCaL version: 2.1.3
% 5.82/1.18 % (1396991)Termination reason: Instruction limit
% 5.82/1.18 % (1396991)Termination phase: Saturation
% 5.82/1.18 % (1396991)Time elapsed: 0.019 s
% 5.82/1.18 % (1396991)Peak memory usage: 12 MB
% 5.82/1.18 % (1396991)Instructions burned: 36 (million)
% 5.82/1.18 % (1396957)Instruction limit reached!
% 5.82/1.18 % (1396957)------------------------------
% 5.82/1.18 % (1396957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.18 % (1396957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.18 % (1396957)CaDiCaL version: 2.1.3
% 5.82/1.18 % (1396957)Termination reason: Instruction limit
% 5.82/1.18 % (1396957)Termination phase: Saturation
% 5.82/1.18 % (1396957)Time elapsed: 0.206 s
% 5.82/1.18 % (1396957)Peak memory usage: 13 MB
% 5.82/1.18 % (1396957)Instructions burned: 450 (million)
% 5.82/1.18 % (1397012)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=323728427:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/91Mi)
% 5.82/1.18 % (1397013)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2691570197: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.82/1.18 % (1396952)Instruction limit reached!
% 5.82/1.18 % (1396952)------------------------------
% 5.82/1.18 % (1396952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.18 % (1396952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.18 % (1396952)CaDiCaL version: 2.1.3
% 5.82/1.18 % (1396952)Termination reason: Instruction limit
% 5.82/1.18 % (1396952)Termination phase: Saturation
% 5.82/1.18 % (1396952)Time elapsed: 0.250 s
% 5.82/1.18 % (1396952)Peak memory usage: 13 MB
% 5.82/1.18 % (1396952)Instructions burned: 571 (million)
% 5.82/1.18 % (1397022)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=953421520:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2992 on theBenchmark for (2992ds/22Mi)
% 5.82/1.18 % (1397022)Instruction limit reached!
% 5.82/1.18 % (1397022)------------------------------
% 5.82/1.18 % (1397022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.82/1.18 % (1397022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.82/1.18 % (1397022)CaDiCaL version: 2.1.3
% 5.82/1.18 % (1397022)Termination reason: Instruction limit
% 5.82/1.18 % (1397022)Termination phase: Saturation
% 5.82/1.18 % (1397022)Time elapsed: 0.012 s
% 5.82/1.18 % (1397022)Peak memory usage: 12 MB
% 5.82/1.18 % (1397022)Instructions burned: 24 (million)
% 5.82/1.18 % (1397013)Instruction limit reached!
% 5.82/1.18 % (1397013)------------------------------
% 5.82/1.18 % (1397013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.26 % (1397013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.26 % (1397013)CaDiCaL version: 2.1.3
% 6.34/1.26 % (1397013)Termination reason: Instruction limit
% 6.34/1.26 % (1397013)Termination phase: Saturation
% 6.34/1.26 % (1397013)Time elapsed: 0.032 s
% 6.34/1.26 % (1397013)Peak memory usage: 12 MB
% 6.34/1.26 % (1397013)Instructions burned: 67 (million)
% 6.34/1.26 % (1397012)Instruction limit reached!
% 6.34/1.26 % (1397012)------------------------------
% 6.34/1.26 % (1397012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.26 % (1397012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.26 % (1397012)CaDiCaL version: 2.1.3
% 6.34/1.26 % (1397012)Termination reason: Instruction limit
% 6.34/1.26 % (1397012)Termination phase: Saturation
% 6.34/1.26 % (1397012)Time elapsed: 0.047 s
% 6.34/1.26 % (1397012)Peak memory usage: 12 MB
% 6.34/1.26 % (1397012)Instructions burned: 91 (million)
% 6.34/1.26 % (1396966)Instruction limit reached!
% 6.34/1.26 % (1396966)------------------------------
% 6.34/1.26 % (1396966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.26 % (1396966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.26 % (1396966)CaDiCaL version: 2.1.3
% 6.34/1.26 % (1396966)Termination reason: Instruction limit
% 6.34/1.26 % (1396966)Termination phase: Saturation
% 6.34/1.26 % (1396966)Time elapsed: 0.203 s
% 6.34/1.26 % (1396966)Peak memory usage: 15 MB
% 6.34/1.26 % (1396966)Instructions burned: 376 (million)
% 6.34/1.26 % (1397042)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1843176507:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/28Mi)
% 6.34/1.26 % (1397040)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=1528930475:i=338:bd=all:ins=4:rtra=on_2992 on theBenchmark for (2992ds/338Mi)
% 6.34/1.26 % (1397048)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.34/1.26 % (1397048)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2879204371:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2992 on theBenchmark for (2992ds/137Mi)
% 6.34/1.26 % (1397048)Refutation not found, incomplete strategy
% 6.34/1.26 % (1397048)------------------------------
% 6.34/1.26 % (1397048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.26 % (1397049)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=1479052044:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2992 on theBenchmark for (2992ds/340Mi)
% 6.34/1.26 % (1397048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.26 % (1397048)CaDiCaL version: 2.1.3
% 6.34/1.26 % (1397048)Termination reason: Refutation not found, incomplete strategy
% 6.34/1.26 % (1397048)Time elapsed: 0.006 s
% 6.34/1.26 % (1397048)Peak memory usage: 12 MB
% 6.34/1.26 % (1397048)Instructions burned: 10 (million)
% 6.34/1.26 % (1397042)Instruction limit reached!
% 6.34/1.26 % (1397042)------------------------------
% 6.34/1.26 % (1397042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.26 % (1397042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.26 % (1397042)CaDiCaL version: 2.1.3
% 6.34/1.26 % (1397042)Termination reason: Instruction limit
% 6.34/1.26 % (1397042)Termination phase: Saturation
% 6.34/1.26 % (1397042)Time elapsed: 0.017 s
% 6.34/1.26 % (1397042)Peak memory usage: 12 MB
% 6.34/1.26 % (1397042)Instructions burned: 30 (million)
% 6.34/1.26 % (1397048)------------------------------
% 6.34/1.26 % (1397048)------------------------------
% 6.34/1.26 % (1397061)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 6.34/1.26 % (1397060)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1415324346:i=227:sd=1:bd=all:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/227Mi)
% 6.34/1.26 % (1397061)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=166414493:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/373Mi)
% 6.34/1.26 % (1396925)Instruction limit reached!
% 6.87/1.38 % (1396925)------------------------------
% 6.87/1.38 % (1396925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.38 % (1396925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.38 % (1396925)CaDiCaL version: 2.1.3
% 6.87/1.38 % (1396925)Termination reason: Instruction limit
% 6.87/1.38 % (1396925)Termination phase: Saturation
% 6.87/1.38 % (1396925)Time elapsed: 0.422 s
% 6.87/1.38 % (1396925)Peak memory usage: 14 MB
% 6.87/1.38 % (1396925)Instructions burned: 876 (million)
% 6.87/1.38 % (1397078)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=125774550:i=116:ep=RSTC:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/116Mi)
% 6.87/1.38 % (1396972)Instruction limit reached!
% 6.87/1.38 % (1396972)------------------------------
% 6.87/1.38 % (1396972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.38 % (1396972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.38 % (1396972)CaDiCaL version: 2.1.3
% 6.87/1.38 % (1396972)Termination reason: Instruction limit
% 6.87/1.38 % (1396972)Termination phase: Saturation
% 6.87/1.38 % (1396972)Time elapsed: 0.242 s
% 6.87/1.38 % (1396972)Peak memory usage: 13 MB
% 6.87/1.38 % (1396972)Instructions burned: 496 (million)
% 6.87/1.38 % (1397097)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=839534972:i=575:rtra=on_2991 on theBenchmark for (2991ds/575Mi)
% 6.87/1.38 % (1397078)Instruction limit reached!
% 6.87/1.38 % (1397078)------------------------------
% 6.87/1.38 % (1397078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.38 % (1397078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.38 % (1397078)CaDiCaL version: 2.1.3
% 6.87/1.38 % (1397078)Termination reason: Instruction limit
% 6.87/1.38 % (1397078)Termination phase: Saturation
% 6.87/1.38 % (1397078)Time elapsed: 0.059 s
% 6.87/1.38 % (1397078)Peak memory usage: 12 MB
% 6.87/1.38 % (1397078)Instructions burned: 118 (million)
% 6.87/1.38 % (1397060)Instruction limit reached!
% 6.87/1.38 % (1397060)------------------------------
% 6.87/1.38 % (1397060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.38 % (1397060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.38 % (1397060)CaDiCaL version: 2.1.3
% 6.87/1.38 % (1397060)Termination reason: Instruction limit
% 6.87/1.38 % (1397060)Termination phase: Saturation
% 6.87/1.38 % (1397060)Time elapsed: 0.100 s
% 6.87/1.38 % (1397060)Peak memory usage: 13 MB
% 6.87/1.38 % (1397060)Instructions burned: 229 (million)
% 6.87/1.38 % (1397100)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2749750492:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2991 on theBenchmark for (2991ds/270Mi)
% 6.87/1.38 % (1397040)Instruction limit reached!
% 6.87/1.38 % (1397040)------------------------------
% 6.87/1.38 % (1397040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.38 % (1397040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.38 % (1397040)CaDiCaL version: 2.1.3
% 6.87/1.38 % (1397040)Termination reason: Instruction limit
% 6.87/1.38 % (1397040)Termination phase: Saturation
% 6.87/1.38 % (1397040)Time elapsed: 0.151 s
% 6.87/1.38 % (1397040)Peak memory usage: 14 MB
% 6.87/1.38 % (1397040)Instructions burned: 338 (million)
% 6.87/1.38 % (1397101)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=237910337: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_2990 on theBenchmark for (2990ds/9840Mi)
% 6.87/1.38 % (1397101)Refutation not found, incomplete strategy
% 6.87/1.38 % (1397101)------------------------------
% 6.87/1.38 % (1397101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.38 % (1397101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.38 % (1397101)CaDiCaL version: 2.1.3
% 6.87/1.38 % (1397101)Termination reason: Refutation not found, incomplete strategy
% 6.87/1.38 % (1397101)Time elapsed: 0.004 s
% 6.87/1.38 % (1397101)Peak memory usage: 12 MB
% 6.87/1.38 % (1397101)Instructions burned: 5 (million)
% 6.87/1.38 % (1397101)------------------------------
% 6.87/1.38 % (1397101)------------------------------
% 6.87/1.38 % (1397049)Instruction limit reached!
% 7.52/1.49 % (1397049)------------------------------
% 7.52/1.49 % (1397049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.49 % (1397049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.49 % (1397049)CaDiCaL version: 2.1.3
% 7.52/1.49 % (1397049)Termination reason: Instruction limit
% 7.52/1.49 % (1397049)Termination phase: Saturation
% 7.52/1.49 % (1397049)Time elapsed: 0.150 s
% 7.52/1.49 % (1397049)Peak memory usage: 13 MB
% 7.52/1.49 % (1397049)Instructions burned: 342 (million)
% 7.52/1.49 % (1397103)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3846684523:i=421:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/421Mi)
% 7.52/1.49 % (1397105)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.52/1.49 % (1397105)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=3456137979:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/270Mi)
% 7.52/1.49 % (1397106)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2948784446:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/31Mi)
% 7.52/1.49 % (1397106)Refutation not found, incomplete strategy
% 7.52/1.49 % (1397106)------------------------------
% 7.52/1.49 % (1397106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.49 % (1397106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.49 % (1397106)CaDiCaL version: 2.1.3
% 7.52/1.49 % (1397106)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.49 % (1397106)Time elapsed: 0.004 s
% 7.52/1.49 % (1397106)Peak memory usage: 12 MB
% 7.52/1.49 % (1397106)Instructions burned: 7 (million)
% 7.52/1.49 % (1397106)------------------------------
% 7.52/1.49 % (1397106)------------------------------
% 7.52/1.49 % (1397061)Instruction limit reached!
% 7.52/1.49 % (1397061)------------------------------
% 7.52/1.49 % (1397061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.49 % (1397061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.49 % (1397061)CaDiCaL version: 2.1.3
% 7.52/1.49 % (1397061)Termination reason: Instruction limit
% 7.52/1.49 % (1397061)Termination phase: Saturation
% 7.52/1.49 % (1397061)Time elapsed: 0.167 s
% 7.52/1.49 % (1397061)Peak memory usage: 14 MB
% 7.52/1.49 % (1397061)Instructions burned: 373 (million)
% 7.52/1.49 % (1397110)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 7.52/1.49 % (1397110)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.52/1.49 % (1397110)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=1966155790:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2990 on theBenchmark for (2990ds/1440Mi)
% 7.52/1.49 % (1397110)Refutation not found, incomplete strategy
% 7.52/1.49 % (1397110)------------------------------
% 7.52/1.49 % (1397110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.49 % (1397110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.49 % (1397110)CaDiCaL version: 2.1.3
% 7.52/1.49 % (1397110)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.49 % (1397110)Time elapsed: 0.013 s
% 7.52/1.49 % (1397110)Peak memory usage: 12 MB
% 7.52/1.49 % (1397110)Instructions burned: 21 (million)
% 7.52/1.49 % (1397110)------------------------------
% 7.52/1.49 % (1397110)------------------------------
% 7.52/1.49 % (1397111)dis+10_2_sil=128000:si=on:random_seed=20506274:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2990 on theBenchmark for (2990ds/339Mi)
% 7.52/1.49 % (1397114)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=310013345:i=111:add=on:fgj=on:rtra=on:fdi=1024_2990 on theBenchmark for (2990ds/111Mi)
% 7.52/1.49 % (1397114)Refutation not found, incomplete strategy
% 7.52/1.49 % (1397114)------------------------------
% 7.52/1.49 % (1397114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.52/1.49 % (1397114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.24/1.55 % (1397114)CaDiCaL version: 2.1.3
% 8.24/1.55 % (1397114)Termination reason: Refutation not found, incomplete strategy
% 8.24/1.55 % (1397114)Time elapsed: 0.003 s
% 8.24/1.55 % (1397114)Peak memory usage: 12 MB
% 8.24/1.55 % (1397114)Instructions burned: 4 (million)
% 8.24/1.55 % (1397114)------------------------------
% 8.24/1.55 % (1397114)------------------------------
% 8.24/1.55 % (1397121)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=3035960206:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2989 on theBenchmark for (2989ds/122Mi)
% 8.24/1.55 % (1397100)Instruction limit reached!
% 8.24/1.55 % (1397100)------------------------------
% 8.24/1.55 % (1397100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.24/1.55 % (1397100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.24/1.55 % (1397100)CaDiCaL version: 2.1.3
% 8.24/1.55 % (1397100)Termination reason: Instruction limit
% 8.24/1.55 % (1397100)Termination phase: Saturation
% 8.24/1.55 % (1397100)Time elapsed: 0.129 s
% 8.24/1.55 % (1397100)Peak memory usage: 13 MB
% 8.24/1.55 % (1397100)Instructions burned: 271 (million)
% 8.24/1.55 % (1397134)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=2198194766:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/136Mi)
% 8.24/1.55 % (1397105)Instruction limit reached!
% 8.24/1.55 % (1397105)------------------------------
% 8.24/1.55 % (1397105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.24/1.55 % (1397105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.24/1.55 % (1397105)CaDiCaL version: 2.1.3
% 8.24/1.55 % (1397105)Termination reason: Instruction limit
% 8.24/1.55 % (1397105)Termination phase: Saturation
% 8.24/1.55 % (1397105)Time elapsed: 0.126 s
% 8.24/1.55 % (1397105)Peak memory usage: 13 MB
% 8.24/1.55 % (1397105)Instructions burned: 271 (million)
% 8.24/1.55 % (1397121)Instruction limit reached!
% 8.24/1.55 % (1397121)------------------------------
% 8.24/1.55 % (1397121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.24/1.55 % (1397121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.24/1.55 % (1397121)CaDiCaL version: 2.1.3
% 8.24/1.55 % (1397121)Termination reason: Instruction limit
% 8.24/1.55 % (1397121)Termination phase: Saturation
% 8.24/1.55 % (1397121)Time elapsed: 0.053 s
% 8.24/1.55 % (1397121)Peak memory usage: 12 MB
% 8.24/1.55 % (1397121)Instructions burned: 122 (million)
% 8.24/1.55 % (1397154)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2764059167:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2989 on theBenchmark for (2989ds/232Mi)
% 8.24/1.55 % (1397154)Refutation not found, incomplete strategy
% 8.24/1.55 % (1397154)------------------------------
% 8.24/1.55 % (1397154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.24/1.55 % (1397154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.24/1.55 % (1397154)CaDiCaL version: 2.1.3
% 8.24/1.55 % (1397154)Termination reason: Refutation not found, incomplete strategy
% 8.24/1.55 % (1397154)Time elapsed: 0.002 s
% 8.24/1.55 % (1397154)Peak memory usage: 12 MB
% 8.24/1.55 % (1397154)Instructions burned: 2 (million)
% 8.24/1.55 % (1397154)------------------------------
% 8.24/1.55 % (1397154)------------------------------
% 8.24/1.55 % (1397161)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=1491961109:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/1254Mi)
% 8.24/1.55 % (1397166)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 8.24/1.55 % (1397166)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=2103495208:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2989 on theBenchmark for (2989ds/281Mi)
% 8.24/1.55 % (1397134)Instruction limit reached!
% 8.24/1.55 % (1397134)------------------------------
% 8.24/1.55 % (1397134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.24/1.55 % (1397134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.68 % (1397134)CaDiCaL version: 2.1.3
% 8.80/1.68 % (1397134)Termination reason: Instruction limit
% 8.80/1.68 % (1397134)Termination phase: Saturation
% 8.80/1.68 % (1397134)Time elapsed: 0.068 s
% 8.80/1.68 % (1397134)Peak memory usage: 13 MB
% 8.80/1.68 % (1397134)Instructions burned: 136 (million)
% 8.80/1.68 % (1397103)Instruction limit reached!
% 8.80/1.68 % (1397103)------------------------------
% 8.80/1.68 % (1397103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.68 % (1397103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.68 % (1397103)CaDiCaL version: 2.1.3
% 8.80/1.68 % (1397103)Termination reason: Instruction limit
% 8.80/1.68 % (1397103)Termination phase: Saturation
% 8.80/1.68 % (1397103)Time elapsed: 0.202 s
% 8.80/1.68 % (1397103)Peak memory usage: 13 MB
% 8.80/1.68 % (1397103)Instructions burned: 422 (million)
% 8.80/1.68 % (1397097)Instruction limit reached!
% 8.80/1.68 % (1397097)------------------------------
% 8.80/1.68 % (1397097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.68 % (1397097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.68 % (1397097)CaDiCaL version: 2.1.3
% 8.80/1.68 % (1397097)Termination reason: Instruction limit
% 8.80/1.68 % (1397097)Termination phase: Saturation
% 8.80/1.68 % (1397097)Time elapsed: 0.259 s
% 8.80/1.68 % (1397097)Peak memory usage: 14 MB
% 8.80/1.68 % (1397097)Instructions burned: 576 (million)
% 8.80/1.68 % (1397173)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3446750156:i=619:add=on:rtra=on_2988 on theBenchmark for (2988ds/619Mi)
% 8.80/1.68 % (1397111)Instruction limit reached!
% 8.80/1.68 % (1397111)------------------------------
% 8.80/1.68 % (1397111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.68 % (1397111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.68 % (1397111)CaDiCaL version: 2.1.3
% 8.80/1.68 % (1397111)Termination reason: Instruction limit
% 8.80/1.68 % (1397111)Termination phase: Saturation
% 8.80/1.68 % (1397111)Time elapsed: 0.167 s
% 8.80/1.68 % (1397111)Peak memory usage: 12 MB
% 8.80/1.68 % (1397111)Instructions burned: 341 (million)
% 8.80/1.68 % (1397174)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=3895018833:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/865Mi)
% 8.80/1.68 % (1397173)Refutation not found, incomplete strategy
% 8.80/1.68 % (1397173)------------------------------
% 8.80/1.68 % (1397173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.68 % (1397173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.68 % (1397173)CaDiCaL version: 2.1.3
% 8.80/1.68 % (1397173)Termination reason: Refutation not found, incomplete strategy
% 8.80/1.68 % (1397173)Time elapsed: 0.008 s
% 8.80/1.68 % (1397173)Peak memory usage: 12 MB
% 8.80/1.68 % (1397173)Instructions burned: 13 (million)
% 8.80/1.68 % (1397173)------------------------------
% 8.80/1.68 % (1397173)------------------------------
% 8.80/1.68 % (1397175)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1460114301:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/212Mi)
% 8.80/1.68 % (1397177)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3308231099:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/130Mi)
% 8.80/1.68 % (1397179)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2891050656:st=1.5:i=346:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/346Mi)
% 8.80/1.68 % (1397179)Refutation not found, incomplete strategy
% 8.80/1.68 % (1397179)------------------------------
% 8.80/1.68 % (1397179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.80/1.68 % (1397179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.80/1.68 % (1397179)CaDiCaL version: 2.1.3
% 8.80/1.68 % (1397179)Termination reason: Refutation not found, incomplete strategy
% 8.80/1.68 % (1397179)Time elapsed: 0.012 s
% 8.80/1.68 % (1397179)Peak memory usage: 12 MB
% 8.80/1.68 % (1397179)Instructions burned: 20 (million)
% 8.80/1.68 % (1397179)------------------------------
% 8.80/1.68 % (1397179)------------------------------
% 8.80/1.68 % (1397183)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3579951267:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/152Mi)
% 8.80/1.68 % (1397177)Instruction limit reached!
% 10.23/1.95 % (1397177)------------------------------
% 10.23/1.95 % (1397177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.23/1.95 % (1397177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/1.95 % (1397177)CaDiCaL version: 2.1.3
% 10.23/1.95 % (1397177)Termination reason: Instruction limit
% 10.23/1.95 % (1397177)Termination phase: Saturation
% 10.23/1.95 % (1397177)Time elapsed: 0.065 s
% 10.23/1.95 % (1397177)Peak memory usage: 12 MB
% 10.23/1.95 % (1397177)Instructions burned: 130 (million)
% 10.23/1.95 % (1397166)Instruction limit reached!
% 10.23/1.95 % (1397166)------------------------------
% 10.23/1.95 % (1397166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.23/1.95 % (1397166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/1.95 % (1397166)CaDiCaL version: 2.1.3
% 10.23/1.95 % (1397166)Termination reason: Instruction limit
% 10.23/1.95 % (1397166)Termination phase: Saturation
% 10.23/1.95 % (1397166)Time elapsed: 0.140 s
% 10.23/1.95 % (1397166)Peak memory usage: 13 MB
% 10.23/1.95 % (1397166)Instructions burned: 281 (million)
% 10.23/1.95 % (1397185)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=839858953:i=75:ep=R:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/75Mi)
% 10.23/1.95 % (1397185)Refutation not found, incomplete strategy
% 10.23/1.95 % (1397185)------------------------------
% 10.23/1.95 % (1397185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.23/1.95 % (1397185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/1.95 % (1397185)CaDiCaL version: 2.1.3
% 10.23/1.95 % (1397185)Termination reason: Refutation not found, incomplete strategy
% 10.23/1.95 % (1397185)Time elapsed: 0.004 s
% 10.23/1.95 % (1397185)Peak memory usage: 12 MB
% 10.23/1.95 % (1397185)Instructions burned: 7 (million)
% 10.23/1.95 % (1397185)------------------------------
% 10.23/1.95 % (1397185)------------------------------
% 10.23/1.95 % (1397186)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=4206320312:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/387Mi)
% 10.23/1.95 % (1397175)Instruction limit reached!
% 10.23/1.95 % (1397175)------------------------------
% 10.23/1.95 % (1397175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.23/1.95 % (1397175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/1.95 % (1397175)CaDiCaL version: 2.1.3
% 10.23/1.95 % (1397175)Termination reason: Instruction limit
% 10.23/1.95 % (1397175)Termination phase: Saturation
% 10.23/1.95 % (1397175)Time elapsed: 0.106 s
% 10.23/1.95 % (1397175)Peak memory usage: 13 MB
% 10.23/1.95 % (1397175)Instructions burned: 214 (million)
% 10.23/1.95 % (1397186)Refutation not found, incomplete strategy
% 10.23/1.95 % (1397186)------------------------------
% 10.23/1.95 % (1397186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.23/1.95 % (1397186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/1.95 % (1397186)CaDiCaL version: 2.1.3
% 10.23/1.95 % (1397186)Termination reason: Refutation not found, incomplete strategy
% 10.23/1.95 % (1397186)Time elapsed: 0.007 s
% 10.23/1.95 % (1397186)Peak memory usage: 12 MB
% 10.23/1.95 % (1397186)Instructions burned: 11 (million)
% 10.23/1.95 % (1397186)------------------------------
% 10.23/1.95 % (1397186)------------------------------
% 10.23/1.95 % (1397188)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=3765569906:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2987 on theBenchmark for (2987ds/148Mi)
% 10.23/1.95 % (1397183)Instruction limit reached!
% 10.23/1.95 % (1397183)------------------------------
% 10.23/1.95 % (1397183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.23/1.95 % (1397183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/1.95 % (1397183)CaDiCaL version: 2.1.3
% 10.23/1.95 % (1397183)Termination reason: Instruction limit
% 10.23/1.95 % (1397183)Termination phase: Saturation
% 10.23/1.95 % (1397183)Time elapsed: 0.074 s
% 10.23/1.95 % (1397183)Peak memory usage: 13 MB
% 10.23/1.95 % (1397183)Instructions burned: 153 (million)
% 10.23/1.95 % (1397190)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1446699302:i=161:piset=and:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/161Mi)
% 10.23/1.95 % (1397191)lrs+10_1_sil=128000:si=on:random_seed=3442744446:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/888Mi)
% 12.54/2.05 % (1397193)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=1374617041:i=136:add=on:ins=4:rtra=on:sup=off_2987 on theBenchmark for (2987ds/136Mi)
% 12.54/2.05 % (1397188)Instruction limit reached!
% 12.54/2.05 % (1397188)------------------------------
% 12.54/2.05 % (1397188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.54/2.05 % (1397188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.05 % (1397188)CaDiCaL version: 2.1.3
% 12.54/2.05 % (1397188)Termination reason: Instruction limit
% 12.54/2.05 % (1397188)Termination phase: Saturation
% 12.54/2.05 % (1397188)Time elapsed: 0.073 s
% 12.54/2.05 % (1397188)Peak memory usage: 13 MB
% 12.54/2.05 % (1397188)Instructions burned: 148 (million)
% 12.54/2.05 % (1397190)Instruction limit reached!
% 12.54/2.05 % (1397190)------------------------------
% 12.54/2.05 % (1397190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.54/2.05 % (1397190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.05 % (1397190)CaDiCaL version: 2.1.3
% 12.54/2.05 % (1397190)Termination reason: Instruction limit
% 12.54/2.05 % (1397190)Termination phase: Saturation
% 12.54/2.05 % (1397190)Time elapsed: 0.070 s
% 12.54/2.05 % (1397190)Peak memory usage: 12 MB
% 12.54/2.05 % (1397190)Instructions burned: 162 (million)
% 12.54/2.05 % (1397193)Instruction limit reached!
% 12.54/2.05 % (1397193)------------------------------
% 12.54/2.05 % (1397193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.54/2.05 % (1397193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.05 % (1397193)CaDiCaL version: 2.1.3
% 12.54/2.05 % (1397193)Termination reason: Instruction limit
% 12.54/2.05 % (1397193)Termination phase: Saturation
% 12.54/2.05 % (1397193)Time elapsed: 0.063 s
% 12.54/2.05 % (1397193)Peak memory usage: 12 MB
% 12.54/2.05 % (1397193)Instructions burned: 136 (million)
% 12.54/2.05 % (1397197)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=1174213176:i=88:s2at=3:nm=2:rtra=on:rawr=on_2986 on theBenchmark for (2986ds/88Mi)
% 12.54/2.05 % (1397198)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3750738312:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2986 on theBenchmark for (2986ds/93Mi)
% 12.54/2.05 % (1397199)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1205789424:i=2186:rtra=on:ixr=off_2986 on theBenchmark for (2986ds/2186Mi)
% 12.54/2.05 % (1397199)Refutation not found, incomplete strategy
% 12.54/2.05 % (1397199)------------------------------
% 12.54/2.05 % (1397199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.54/2.05 % (1397199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.05 % (1397199)CaDiCaL version: 2.1.3
% 12.54/2.05 % (1397199)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.05 % (1397199)Time elapsed: 0.006 s
% 12.54/2.05 % (1397199)Peak memory usage: 12 MB
% 12.54/2.05 % (1397199)Instructions burned: 11 (million)
% 12.54/2.05 % (1397199)------------------------------
% 12.54/2.05 % (1397199)------------------------------
% 12.54/2.05 % (1397203)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1438758417:s2a=on:i=240:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/240Mi)
% 12.54/2.05 % (1397197)Instruction limit reached!
% 12.54/2.05 % (1397197)------------------------------
% 12.54/2.05 % (1397197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.54/2.05 % (1397197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.05 % (1397197)CaDiCaL version: 2.1.3
% 12.54/2.05 % (1397197)Termination reason: Instruction limit
% 12.54/2.05 % (1397197)Termination phase: Saturation
% 12.54/2.05 % (1397197)Time elapsed: 0.041 s
% 12.54/2.05 % (1397197)Peak memory usage: 13 MB
% 12.54/2.05 % (1397197)Instructions burned: 88 (million)
% 12.54/2.05 % (1397198)Instruction limit reached!
% 12.54/2.05 % (1397198)------------------------------
% 12.54/2.05 % (1397198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.54/2.05 % (1397198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.05 % (1397198)CaDiCaL version: 2.1.3
% 12.54/2.05 % (1397198)Termination reason: Instruction limit
% 12.54/2.05 % (1397198)Termination phase: Saturation
% 13.38/2.21 % (1397198)Time elapsed: 0.048 s
% 13.38/2.21 % (1397198)Peak memory usage: 12 MB
% 13.38/2.21 % (1397198)Instructions burned: 94 (million)
% 13.38/2.21 % (1397205)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=2716829407:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2985 on theBenchmark for (2985ds/805Mi)
% 13.38/2.21 % (1397206)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 13.38/2.21 % (1397206)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=2270799284:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2985 on theBenchmark for (2985ds/391Mi)
% 13.38/2.21 % (1397203)Instruction limit reached!
% 13.38/2.21 % (1397203)------------------------------
% 13.38/2.21 % (1397203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.21 % (1397203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.21 % (1397203)CaDiCaL version: 2.1.3
% 13.38/2.21 % (1397203)Termination reason: Instruction limit
% 13.38/2.21 % (1397203)Termination phase: Saturation
% 13.38/2.21 % (1397203)Time elapsed: 0.093 s
% 13.38/2.21 % (1397203)Peak memory usage: 13 MB
% 13.38/2.21 % (1397203)Instructions burned: 242 (million)
% 13.38/2.21 % (1397209)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=2078106860:i=355:av=off:fsr=off:rtra=on:ixr=off_2984 on theBenchmark for (2984ds/355Mi)
% 13.38/2.21 % (1397174)Instruction limit reached!
% 13.38/2.21 % (1397174)------------------------------
% 13.38/2.21 % (1397174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.21 % (1397174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.21 % (1397174)CaDiCaL version: 2.1.3
% 13.38/2.21 % (1397174)Termination reason: Instruction limit
% 13.38/2.21 % (1397174)Termination phase: Saturation
% 13.38/2.21 % (1397174)Time elapsed: 0.389 s
% 13.38/2.21 % (1397174)Peak memory usage: 14 MB
% 13.38/2.21 % (1397174)Instructions burned: 867 (million)
% 13.38/2.21 % (1397211)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=2249504567:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/314Mi)
% 13.38/2.21 % (1397206)Instruction limit reached!
% 13.38/2.21 % (1397206)------------------------------
% 13.38/2.21 % (1397206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.21 % (1397206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.21 % (1397206)CaDiCaL version: 2.1.3
% 13.38/2.21 % (1397206)Termination reason: Instruction limit
% 13.38/2.21 % (1397206)Termination phase: Saturation
% 13.38/2.21 % (1397206)Time elapsed: 0.169 s
% 13.38/2.21 % (1397206)Peak memory usage: 13 MB
% 13.38/2.21 % (1397206)Instructions burned: 391 (million)
% 13.38/2.21 % (1397213)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=2148321476:s2a=on:i=251:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/251Mi)
% 13.38/2.21 % (1397161)Instruction limit reached!
% 13.38/2.21 % (1397161)------------------------------
% 13.38/2.21 % (1397161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.21 % (1397161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.21 % (1397161)CaDiCaL version: 2.1.3
% 13.38/2.21 % (1397161)Termination reason: Instruction limit
% 13.38/2.21 % (1397161)Termination phase: Saturation
% 13.38/2.21 % (1397161)Time elapsed: 0.556 s
% 13.38/2.21 % (1397161)Peak memory usage: 14 MB
% 13.38/2.21 % (1397161)Instructions burned: 1254 (million)
% 13.38/2.21 % (1397215)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=3607422842: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_2983 on theBenchmark for (2983ds/2470Mi)
% 13.38/2.21 % (1397209)Instruction limit reached!
% 13.38/2.21 % (1397209)------------------------------
% 13.38/2.21 % (1397209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.21 % (1397209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.21 % (1397209)CaDiCaL version: 2.1.3
% 13.38/2.21 % (1397209)Termination reason: Instruction limit
% 13.38/2.21 % (1397209)Termination phase: Saturation
% 13.38/2.21 % (1397209)Time elapsed: 0.170 s
% 14.16/2.35 % (1397209)Peak memory usage: 13 MB
% 14.16/2.35 % (1397209)Instructions burned: 356 (million)
% 14.16/2.35 % (1397211)Instruction limit reached!
% 14.16/2.35 % (1397211)------------------------------
% 14.16/2.35 % (1397211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.16/2.35 % (1397211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.35 % (1397211)CaDiCaL version: 2.1.3
% 14.16/2.35 % (1397211)Termination reason: Instruction limit
% 14.16/2.35 % (1397211)Termination phase: Saturation
% 14.16/2.35 % (1397211)Time elapsed: 0.139 s
% 14.16/2.35 % (1397211)Peak memory usage: 13 MB
% 14.16/2.35 % (1397211)Instructions burned: 314 (million)
% 14.16/2.35 % (1397191)Instruction limit reached!
% 14.16/2.35 % (1397191)------------------------------
% 14.16/2.35 % (1397191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.16/2.35 % (1397191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.35 % (1397191)CaDiCaL version: 2.1.3
% 14.16/2.35 % (1397191)Termination reason: Instruction limit
% 14.16/2.35 % (1397191)Termination phase: Saturation
% 14.16/2.35 % (1397191)Time elapsed: 0.414 s
% 14.16/2.35 % (1397191)Peak memory usage: 15 MB
% 14.16/2.35 % (1397191)Instructions burned: 889 (million)
% 14.16/2.35 % (1397217)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=174317336:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2983 on theBenchmark for (2983ds/673Mi)
% 14.16/2.35 % (1397218)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=383011588:i=116:ep=RSTC:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/116Mi)
% 14.16/2.35 % (1397219)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3687763943:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2982 on theBenchmark for (2982ds/270Mi)
% 14.16/2.35 % (1397213)Instruction limit reached!
% 14.16/2.35 % (1397213)------------------------------
% 14.16/2.35 % (1397213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.16/2.35 % (1397213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.35 % (1397213)CaDiCaL version: 2.1.3
% 14.16/2.35 % (1397213)Termination reason: Instruction limit
% 14.16/2.35 % (1397213)Termination phase: Saturation
% 14.16/2.35 % (1397213)Time elapsed: 0.117 s
% 14.16/2.35 % (1397213)Peak memory usage: 13 MB
% 14.16/2.35 % (1397213)Instructions burned: 253 (million)
% 14.16/2.35 % (1397223)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=1681964566: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_2982 on theBenchmark for (2982ds/30Mi)
% 14.16/2.35 % (1397223)Refutation not found, incomplete strategy
% 14.16/2.35 % (1397223)------------------------------
% 14.16/2.35 % (1397223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.16/2.35 % (1397223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.35 % (1397223)CaDiCaL version: 2.1.3
% 14.16/2.35 % (1397223)Termination reason: Refutation not found, incomplete strategy
% 14.16/2.35 % (1397223)Time elapsed: 0.004 s
% 14.16/2.35 % (1397223)Peak memory usage: 12 MB
% 14.16/2.35 % (1397223)Instructions burned: 5 (million)
% 14.16/2.35 % (1397223)------------------------------
% 14.16/2.35 % (1397223)------------------------------
% 14.16/2.35 % (1397218)Instruction limit reached!
% 14.16/2.35 % (1397218)------------------------------
% 14.16/2.35 % (1397218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.16/2.35 % (1397218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.35 % (1397218)CaDiCaL version: 2.1.3
% 14.16/2.35 % (1397218)Termination reason: Instruction limit
% 14.16/2.35 % (1397218)Termination phase: Saturation
% 14.16/2.35 % (1397218)Time elapsed: 0.059 s
% 14.16/2.35 % (1397218)Peak memory usage: 12 MB
% 14.16/2.35 % (1397218)Instructions burned: 118 (million)
% 14.16/2.35 % (1397205)Instruction limit reached!
% 14.16/2.35 % (1397205)------------------------------
% 14.16/2.35 % (1397205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.16/2.35 % (1397205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.35 % (1397205)CaDiCaL version: 2.1.3
% 14.16/2.35 % (1397205)Termination reason: Instruction limit
% 14.16/2.35 % (1397205)Termination phase: Saturation
% 14.93/2.54 % (1397205)Time elapsed: 0.356 s
% 14.93/2.54 % (1397205)Peak memory usage: 13 MB
% 14.93/2.54 % (1397205)Instructions burned: 806 (million)
% 14.93/2.54 % (1397225)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 14.93/2.54 % (1397225)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=4094213159:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2982 on theBenchmark for (2982ds/39Mi)
% 14.93/2.54 % (1397226)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=591995486:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2982 on theBenchmark for (2982ds/365Mi)
% 14.93/2.54 % (1397227)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3036694532:i=158:av=off:rtra=on_2982 on theBenchmark for (2982ds/158Mi)
% 14.93/2.54 % (1397227)Refutation not found, incomplete strategy
% 14.93/2.54 % (1397227)------------------------------
% 14.93/2.54 % (1397227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.93/2.54 % (1397227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/2.54 % (1397227)CaDiCaL version: 2.1.3
% 14.93/2.54 % (1397227)Termination reason: Refutation not found, incomplete strategy
% 14.93/2.54 % (1397227)Time elapsed: 0.008 s
% 14.93/2.54 % (1397227)Peak memory usage: 12 MB
% 14.93/2.54 % (1397227)Instructions burned: 13 (million)
% 14.93/2.54 % (1397225)Instruction limit reached!
% 14.93/2.54 % (1397225)------------------------------
% 14.93/2.54 % (1397225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.93/2.54 % (1397225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/2.54 % (1397225)CaDiCaL version: 2.1.3
% 14.93/2.54 % (1397225)Termination reason: Instruction limit
% 14.93/2.54 % (1397225)Termination phase: Saturation
% 14.93/2.54 % (1397225)Time elapsed: 0.021 s
% 14.93/2.54 % (1397225)Peak memory usage: 12 MB
% 14.93/2.54 % (1397225)Instructions burned: 41 (million)
% 14.93/2.54 % (1397227)------------------------------
% 14.93/2.54 % (1397227)------------------------------
% 14.93/2.54 % (1397231)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
% 14.93/2.54 % (1397232)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=3040845553:i=213:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/213Mi)
% 14.93/2.54 % (1397231)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=1843260033:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/252Mi)
% 14.93/2.54 % (1397219)Instruction limit reached!
% 14.93/2.54 % (1397219)------------------------------
% 14.93/2.54 % (1397219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.93/2.54 % (1397219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/2.54 % (1397219)CaDiCaL version: 2.1.3
% 14.93/2.54 % (1397219)Termination reason: Instruction limit
% 14.93/2.54 % (1397219)Termination phase: Saturation
% 14.93/2.54 % (1397219)Time elapsed: 0.126 s
% 14.93/2.54 % (1397219)Peak memory usage: 14 MB
% 14.93/2.54 % (1397219)Instructions burned: 271 (million)
% 14.93/2.54 % (1397235)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=1659902633:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2981 on theBenchmark for (2981ds/160Mi)
% 14.93/2.54 % (1397232)Instruction limit reached!
% 14.93/2.54 % (1397232)------------------------------
% 14.93/2.54 % (1397232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.93/2.54 % (1397232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/2.54 % (1397232)CaDiCaL version: 2.1.3
% 14.93/2.54 % (1397232)Termination reason: Instruction limit
% 14.93/2.54 % (1397232)Termination phase: Saturation
% 14.93/2.54 % (1397232)Time elapsed: 0.103 s
% 14.93/2.54 % (1397232)Peak memory usage: 13 MB
% 14.93/2.54 % (1397232)Instructions burned: 215 (million)
% 14.93/2.54 % (1397235)Instruction limit reached!
% 14.93/2.54 % (1397235)------------------------------
% 14.93/2.54 % (1397235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.93/2.54 % (1397235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/2.54 % (1397235)CaDiCaL version: 2.1.3
% 14.93/2.54 % (1397235)Termination reason: Instruction limit
% 16.12/2.63 % (1397235)Termination phase: Saturation
% 16.12/2.63 % (1397235)Time elapsed: 0.075 s
% 16.12/2.63 % (1397235)Peak memory usage: 13 MB
% 16.12/2.63 % (1397235)Instructions burned: 161 (million)
% 16.12/2.63 % (1397231)Instruction limit reached!
% 16.12/2.63 % (1397231)------------------------------
% 16.12/2.63 % (1397231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.63 % (1397231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.63 % (1397231)CaDiCaL version: 2.1.3
% 16.12/2.63 % (1397231)Termination reason: Instruction limit
% 16.12/2.63 % (1397231)Termination phase: Saturation
% 16.12/2.63 % (1397231)Time elapsed: 0.121 s
% 16.12/2.63 % (1397231)Peak memory usage: 13 MB
% 16.12/2.63 % (1397231)Instructions burned: 252 (million)
% 16.12/2.63 % (1397237)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=2095174626:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/763Mi)
% 16.12/2.63 % (1397238)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 16.12/2.63 % (1397238)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=965048350:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2980 on theBenchmark for (2980ds/237Mi)
% 16.12/2.63 % (1397239)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=2877745907:s2a=on:i=386:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/386Mi)
% 16.12/2.63 % (1397239)Refutation not found, incomplete strategy
% 16.12/2.63 % (1397239)------------------------------
% 16.12/2.63 % (1397239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.63 % (1397239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.63 % (1397239)CaDiCaL version: 2.1.3
% 16.12/2.63 % (1397239)Termination reason: Refutation not found, incomplete strategy
% 16.12/2.63 % (1397239)Time elapsed: 0.004 s
% 16.12/2.63 % (1397239)Peak memory usage: 12 MB
% 16.12/2.63 % (1397239)Instructions burned: 6 (million)
% 16.12/2.63 % (1397239)------------------------------
% 16.12/2.63 % (1397239)------------------------------
% 16.12/2.63 % (1397226)Instruction limit reached!
% 16.12/2.63 % (1397226)------------------------------
% 16.12/2.63 % (1397226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.63 % (1397226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.63 % (1397226)CaDiCaL version: 2.1.3
% 16.12/2.63 % (1397226)Termination reason: Instruction limit
% 16.12/2.63 % (1397226)Termination phase: Saturation
% 16.12/2.63 % (1397226)Time elapsed: 0.187 s
% 16.12/2.63 % (1397226)Peak memory usage: 14 MB
% 16.12/2.63 % (1397226)Instructions burned: 365 (million)
% 16.12/2.63 % (1397243)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=3944458906:i=300:piset=and:nm=32:rtra=on_2980 on theBenchmark for (2980ds/300Mi)
% 16.12/2.63 % (1397244)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=1764614185:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/567Mi)
% 16.12/2.63 % (1397217)Instruction limit reached!
% 16.12/2.63 % (1397217)------------------------------
% 16.12/2.63 % (1397217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.63 % (1397217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.63 % (1397217)CaDiCaL version: 2.1.3
% 16.12/2.63 % (1397217)Termination reason: Instruction limit
% 16.12/2.63 % (1397217)Termination phase: Saturation
% 16.12/2.63 % (1397217)Time elapsed: 0.295 s
% 16.12/2.63 % (1397217)Peak memory usage: 14 MB
% 16.12/2.63 % (1397217)Instructions burned: 674 (million)
% 16.12/2.63 % (1397247)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=1829595944:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2979 on theBenchmark for (2979ds/379Mi)
% 16.12/2.63 % (1397238)Instruction limit reached!
% 16.12/2.63 % (1397238)------------------------------
% 16.12/2.63 % (1397238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.63 % (1397238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.63 % (1397238)CaDiCaL version: 2.1.3
% 16.12/2.63 % (1397238)Termination reason: Instruction limit
% 16.12/2.63 % (1397238)Termination phase: Saturation
% 16.12/2.63 % (1397238)Time elapsed: 0.120 s
% 16.12/2.63 % (1397238)Peak memory usage: 13 MB
% 16.12/2.68 % (1397238)Instructions burned: 237 (million)
% 16.12/2.68 % (1397249)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=3281368165:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2979 on theBenchmark for (2979ds/429Mi)
% 16.12/2.68 % (1396965)Instruction limit reached!
% 16.12/2.68 % (1396965)------------------------------
% 16.12/2.68 % (1396965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.68 % (1396965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.68 % (1396965)CaDiCaL version: 2.1.3
% 16.12/2.68 % (1396965)Termination reason: Instruction limit
% 16.12/2.68 % (1396965)Termination phase: Saturation
% 16.12/2.68 % (1396965)Time elapsed: 1.574 s
% 16.12/2.68 % (1396965)Peak memory usage: 48 MB
% 16.12/2.68 % (1396965)Instructions burned: 5758 (million)
% 16.12/2.68 % (1397251)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=2201248487:i=478:bd=all:rtra=on_2978 on theBenchmark for (2978ds/478Mi)
% 16.12/2.68 % (1397243)Instruction limit reached!
% 16.12/2.68 % (1397243)------------------------------
% 16.12/2.68 % (1397243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.68 % (1397243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.68 % (1397243)CaDiCaL version: 2.1.3
% 16.12/2.68 % (1397243)Termination reason: Instruction limit
% 16.12/2.68 % (1397243)Termination phase: Saturation
% 16.12/2.68 % (1397243)Time elapsed: 0.143 s
% 16.12/2.68 % (1397243)Peak memory usage: 13 MB
% 16.12/2.68 % (1397243)Instructions burned: 301 (million)
% 16.12/2.68 % (1397253)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3231787727:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2978 on theBenchmark for (2978ds/445Mi)
% 16.12/2.68 % (1397247)Instruction limit reached!
% 16.12/2.68 % (1397247)------------------------------
% 16.12/2.68 % (1397247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.68 % (1397247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.68 % (1397247)CaDiCaL version: 2.1.3
% 16.12/2.68 % (1397247)Termination reason: Instruction limit
% 16.12/2.68 % (1397247)Termination phase: Saturation
% 16.12/2.68 % (1397247)Time elapsed: 0.159 s
% 16.12/2.68 % (1397247)Peak memory usage: 13 MB
% 16.12/2.68 % (1397247)Instructions burned: 379 (million)
% 16.12/2.68 % (1397255)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=1035447323:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2978 on theBenchmark for (2978ds/71Mi)
% 16.12/2.68 % (1397255)Instruction limit reached!
% 16.12/2.68 % (1397255)------------------------------
% 16.12/2.68 % (1397255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.68 % (1397255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.68 % (1397255)CaDiCaL version: 2.1.3
% 16.12/2.68 % (1397255)Termination reason: Instruction limit
% 16.12/2.68 % (1397255)Termination phase: Saturation
% 16.12/2.68 % (1397255)Time elapsed: 0.035 s
% 16.12/2.68 % (1397255)Peak memory usage: 12 MB
% 16.12/2.68 % (1397255)Instructions burned: 73 (million)
% 16.12/2.68 % (1397251)Instruction limit reached!
% 16.12/2.68 % (1397251)------------------------------
% 16.12/2.68 % (1397251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.68 % (1397251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.68 % (1397251)CaDiCaL version: 2.1.3
% 16.12/2.68 % (1397251)Termination reason: Instruction limit
% 16.12/2.68 % (1397251)Termination phase: Saturation
% 16.12/2.68 % (1397251)Time elapsed: 0.126 s
% 16.12/2.68 % (1397251)Peak memory usage: 14 MB
% 16.12/2.68 % (1397251)Instructions burned: 478 (million)
% 16.12/2.68 % (1397257)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3367249210:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/302Mi)
% 16.12/2.68 % (1397258)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=3566884648:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2977 on theBenchmark for (2977ds/4980Mi)
% 16.12/2.68 % (1397244)Instruction limit reached!
% 16.12/2.68 % (1397244)------------------------------
% 16.12/2.68 % (1397244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.12/2.68 % (1397244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/2.68 % (1397244)CaDiCaL version: 2.1.3
% 16.12/2.68 % (1397244)Termination reason: Instruction limit
% 17.47/2.95 % (1397244)Termination phase: Saturation
% 17.47/2.95 % (1397244)Time elapsed: 0.275 s
% 17.47/2.95 % (1397244)Peak memory usage: 15 MB
% 17.47/2.95 % (1397244)Instructions burned: 568 (million)
% 17.47/2.95 % (1397261)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
% 17.47/2.95 % (1397261)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 17.47/2.95 % (1397261)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1674728865:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2977 on theBenchmark for (2977ds/100Mi)
% 17.47/2.95 % (1397249)Instruction limit reached!
% 17.47/2.95 % (1397249)------------------------------
% 17.47/2.95 % (1397249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.95 % (1397249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.95 % (1397249)CaDiCaL version: 2.1.3
% 17.47/2.95 % (1397249)Termination reason: Instruction limit
% 17.47/2.95 % (1397249)Termination phase: Saturation
% 17.47/2.95 % (1397249)Time elapsed: 0.196 s
% 17.47/2.95 % (1397249)Peak memory usage: 14 MB
% 17.47/2.95 % (1397249)Instructions burned: 430 (million)
% 17.47/2.95 % (1397237)Instruction limit reached!
% 17.47/2.95 % (1397237)------------------------------
% 17.47/2.95 % (1397237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.95 % (1397237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.95 % (1397237)CaDiCaL version: 2.1.3
% 17.47/2.95 % (1397237)Termination reason: Instruction limit
% 17.47/2.95 % (1397237)Termination phase: Saturation
% 17.47/2.95 % (1397237)Time elapsed: 0.359 s
% 17.47/2.95 % (1397237)Peak memory usage: 21 MB
% 17.47/2.95 % (1397237)Instructions burned: 765 (million)
% 17.47/2.95 % (1397263)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=3554496497:i=76:piset=equals:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/76Mi)
% 17.47/2.95 % (1397264)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=2433435936:i=289:rtra=on_2976 on theBenchmark for (2976ds/289Mi)
% 17.47/2.95 % (1397261)Instruction limit reached!
% 17.47/2.95 % (1397261)------------------------------
% 17.47/2.95 % (1397261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.95 % (1397261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.95 % (1397261)CaDiCaL version: 2.1.3
% 17.47/2.95 % (1397261)Termination reason: Instruction limit
% 17.47/2.95 % (1397261)Termination phase: Saturation
% 17.47/2.95 % (1397261)Time elapsed: 0.049 s
% 17.47/2.95 % (1397261)Peak memory usage: 12 MB
% 17.47/2.95 % (1397261)Instructions burned: 100 (million)
% 17.47/2.95 % (1397263)Instruction limit reached!
% 17.47/2.95 % (1397263)------------------------------
% 17.47/2.95 % (1397263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.95 % (1397263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.95 % (1397263)CaDiCaL version: 2.1.3
% 17.47/2.95 % (1397263)Termination reason: Instruction limit
% 17.47/2.95 % (1397263)Termination phase: Saturation
% 17.47/2.95 % (1397263)Time elapsed: 0.035 s
% 17.47/2.95 % (1397263)Peak memory usage: 12 MB
% 17.47/2.95 % (1397263)Instructions burned: 77 (million)
% 17.47/2.95 % (1397267)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=2827438173:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2976 on theBenchmark for (2976ds/493Mi)
% 17.47/2.95 % (1397267)Refutation not found, incomplete strategy
% 17.47/2.95 % (1397267)------------------------------
% 17.47/2.95 % (1397267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.47/2.95 % (1397267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.47/2.95 % (1397267)CaDiCaL version: 2.1.3
% 17.47/2.95 % (1397267)Termination reason: Refutation not found, incomplete strategy
% 17.47/2.95 % (1397267)Time elapsed: 0.006 s
% 17.47/2.95 % (1397267)Peak memory usage: 12 MB
% 17.47/2.95 % (1397267)Instructions burned: 10 (million)
% 17.47/2.95 % (1397267)------------------------------
% 17.47/2.95 % (1397267)------------------------------
% 19.60/3.03 % (1397253)Instruction limit reached!
% 19.60/3.03 % (1397253)------------------------------
% 19.60/3.03 % (1397253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.60/3.03 % (1397253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.60/3.03 % (1397253)CaDiCaL version: 2.1.3
% 19.60/3.03 % (1397253)Termination reason: Instruction limit
% 19.60/3.03 % (1397253)Termination phase: Saturation
% 19.60/3.03 % (1397253)Time elapsed: 0.210 s
% 19.60/3.03 % (1397253)Peak memory usage: 14 MB
% 19.60/3.03 % (1397253)Instructions burned: 446 (million)
% 19.60/3.03 % (1397268)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=3456133624:cond=on:i=34:hud=10:nm=10:rtra=on_2976 on theBenchmark for (2976ds/34Mi)
% 19.60/3.03 % (1397270)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 19.60/3.03 % (1397270)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=2943351534:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2976 on theBenchmark for (2976ds/372Mi)
% 19.60/3.03 % (1397271)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=2371964550:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2976 on theBenchmark for (2976ds/670Mi)
% 19.60/3.03 % (1397270)Refutation not found, incomplete strategy
% 19.60/3.03 % (1397270)------------------------------
% 19.60/3.03 % (1397270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.60/3.03 % (1397270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.60/3.03 % (1397270)CaDiCaL version: 2.1.3
% 19.60/3.03 % (1397270)Termination reason: Refutation not found, incomplete strategy
% 19.60/3.03 % (1397270)Time elapsed: 0.003 s
% 19.60/3.03 % (1397270)Peak memory usage: 12 MB
% 19.60/3.03 % (1397270)Instructions burned: 6 (million)
% 19.60/3.03 % (1397270)------------------------------
% 19.60/3.03 % (1397270)------------------------------
% 19.60/3.03 % (1397268)Instruction limit reached!
% 19.60/3.03 % (1397268)------------------------------
% 19.60/3.03 % (1397268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.60/3.03 % (1397268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.60/3.03 % (1397268)CaDiCaL version: 2.1.3
% 19.60/3.03 % (1397268)Termination reason: Instruction limit
% 19.60/3.03 % (1397268)Termination phase: Saturation
% 19.60/3.03 % (1397268)Time elapsed: 0.019 s
% 19.60/3.03 % (1397268)Peak memory usage: 12 MB
% 19.60/3.03 % (1397268)Instructions burned: 35 (million)
% 19.60/3.03 % (1397271)Refutation not found, incomplete strategy
% 19.60/3.03 % (1397271)------------------------------
% 19.60/3.03 % (1397271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.60/3.03 % (1397271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.60/3.03 % (1397271)CaDiCaL version: 2.1.3
% 19.60/3.03 % (1397271)Termination reason: Refutation not found, incomplete strategy
% 19.60/3.03 % (1397271)Time elapsed: 0.007 s
% 19.60/3.03 % (1397271)Peak memory usage: 12 MB
% 19.60/3.03 % (1397271)Instructions burned: 11 (million)
% 19.60/3.03 % (1397271)------------------------------
% 19.60/3.03 % (1397271)------------------------------
% 19.60/3.03 % (1397257)Instruction limit reached!
% 19.60/3.03 % (1397257)------------------------------
% 19.60/3.03 % (1397257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.60/3.03 % (1397257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.60/3.03 % (1397257)CaDiCaL version: 2.1.3
% 19.60/3.03 % (1397257)Termination reason: Instruction limit
% 19.60/3.03 % (1397257)Termination phase: Saturation
% 19.60/3.03 % (1397257)Time elapsed: 0.149 s
% 19.60/3.03 % (1397257)Peak memory usage: 13 MB
% 19.60/3.03 % (1397257)Instructions burned: 302 (million)
% 19.60/3.03 % (1397276)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=1370140204:i=857:add=off:kws=frequency:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/857Mi)
% 19.60/3.03 % (1397275)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=625918885:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2975 on theBenchmark for (2975ds/647Mi)
% 19.60/3.03 % (1397275)Refutation not found, incomplete strategy
% 19.60/3.03 % (1397275)------------------------------
% 20.44/3.25 % (1397275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.25 % (1397275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.25 % (1397275)CaDiCaL version: 2.1.3
% 20.44/3.25 % (1397275)Termination reason: Refutation not found, incomplete strategy
% 20.44/3.25 % (1397275)Time elapsed: 0.002 s
% 20.44/3.25 % (1397275)Peak memory usage: 12 MB
% 20.44/3.25 % (1397275)Instructions burned: 2 (million)
% 20.44/3.25 % (1397277)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=247738793:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2975 on theBenchmark for (2975ds/693Mi)
% 20.44/3.25 % (1397275)------------------------------
% 20.44/3.25 % (1397275)------------------------------
% 20.44/3.25 % (1397278)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=1075805746:i=285:hud=10:bd=all:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/285Mi)
% 20.44/3.25 % (1397282)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 20.44/3.25 % (1397282)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=2587735596:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2975 on theBenchmark for (2975ds/52Mi)
% 20.44/3.25 % (1397282)Instruction limit reached!
% 20.44/3.25 % (1397282)------------------------------
% 20.44/3.25 % (1397282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.25 % (1397282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.25 % (1397282)CaDiCaL version: 2.1.3
% 20.44/3.25 % (1397282)Termination reason: Instruction limit
% 20.44/3.25 % (1397282)Termination phase: Saturation
% 20.44/3.25 % (1397282)Time elapsed: 0.027 s
% 20.44/3.25 % (1397282)Peak memory usage: 12 MB
% 20.44/3.25 % (1397282)Instructions burned: 54 (million)
% 20.44/3.25 % (1397264)Instruction limit reached!
% 20.44/3.25 % (1397264)------------------------------
% 20.44/3.25 % (1397264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.25 % (1397264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.25 % (1397264)CaDiCaL version: 2.1.3
% 20.44/3.25 % (1397264)Termination reason: Instruction limit
% 20.44/3.25 % (1397264)Termination phase: Saturation
% 20.44/3.25 % (1397264)Time elapsed: 0.145 s
% 20.44/3.25 % (1397264)Peak memory usage: 13 MB
% 20.44/3.25 % (1397264)Instructions burned: 291 (million)
% 20.44/3.25 % (1397285)dis+10_1_si=on:random_seed=2509818720:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2975 on theBenchmark for (2975ds/407Mi)
% 20.44/3.25 % (1397286)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=3445183894:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/2240Mi)
% 20.44/3.25 % (1397278)Instruction limit reached!
% 20.44/3.25 % (1397278)------------------------------
% 20.44/3.25 % (1397278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.25 % (1397278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.25 % (1397278)CaDiCaL version: 2.1.3
% 20.44/3.25 % (1397278)Termination reason: Instruction limit
% 20.44/3.25 % (1397278)Termination phase: Saturation
% 20.44/3.25 % (1397278)Time elapsed: 0.131 s
% 20.44/3.25 % (1397278)Peak memory usage: 14 MB
% 20.44/3.25 % (1397278)Instructions burned: 286 (million)
% 20.44/3.25 % (1397289)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=4191288611:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2974 on theBenchmark for (2974ds/336Mi)
% 20.44/3.25 % (1397285)Instruction limit reached!
% 20.44/3.25 % (1397285)------------------------------
% 20.44/3.25 % (1397285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.44/3.25 % (1397285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.25 % (1397285)CaDiCaL version: 2.1.3
% 20.44/3.25 % (1397285)Termination reason: Instruction limit
% 20.44/3.25 % (1397285)Termination phase: Saturation
% 20.44/3.25 % (1397285)Time elapsed: 0.191 s
% 20.44/3.25 % (1397285)Peak memory usage: 13 MB
% 20.44/3.25 % (1397285)Instructions burned: 407 (million)
% 20.44/3.25 % (1397277)Instruction limit reached!
% 20.44/3.25 % (1397277)------------------------------
% 20.44/3.25 % (1397277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.59/3.48 % (1397277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.48 % (1397277)CaDiCaL version: 2.1.3
% 21.59/3.48 % (1397277)Termination reason: Instruction limit
% 21.59/3.48 % (1397277)Termination phase: Saturation
% 21.59/3.48 % (1397277)Time elapsed: 0.273 s
% 21.59/3.48 % (1397277)Peak memory usage: 13 MB
% 21.59/3.48 % (1397277)Instructions burned: 694 (million)
% 21.59/3.48 % (1397291)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=777134327:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2973 on theBenchmark for (2973ds/1142Mi)
% 21.59/3.48 % (1397292)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=4051343215:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2972 on theBenchmark for (2972ds/376Mi)
% 21.59/3.48 % (1397292)Refutation not found, incomplete strategy
% 21.59/3.48 % (1397292)------------------------------
% 21.59/3.48 % (1397292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.59/3.48 % (1397292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.48 % (1397292)CaDiCaL version: 2.1.3
% 21.59/3.48 % (1397292)Termination reason: Refutation not found, incomplete strategy
% 21.59/3.48 % (1397292)Time elapsed: 0.004 s
% 21.59/3.48 % (1397292)Peak memory usage: 12 MB
% 21.59/3.48 % (1397292)Instructions burned: 6 (million)
% 21.59/3.48 % (1397289)Instruction limit reached!
% 21.59/3.48 % (1397289)------------------------------
% 21.59/3.48 % (1397289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.59/3.48 % (1397289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.48 % (1397289)CaDiCaL version: 2.1.3
% 21.59/3.48 % (1397289)Termination reason: Instruction limit
% 21.59/3.48 % (1397289)Termination phase: Saturation
% 21.59/3.48 % (1397289)Time elapsed: 0.139 s
% 21.59/3.48 % (1397289)Peak memory usage: 13 MB
% 21.59/3.48 % (1397289)Instructions burned: 338 (million)
% 21.59/3.48 % (1397292)------------------------------
% 21.59/3.48 % (1397292)------------------------------
% 21.59/3.48 % (1397296)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 21.59/3.48 % (1397295)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=3086651288:i=766:bd=all:rtra=on_2972 on theBenchmark for (2972ds/766Mi)
% 21.59/3.48 % (1397296)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=2297585536:st=3:uwa_fpi=on:i=959:fgj=on:piset=pi_sigma:hud=5:nm=16:rtra=on:fe=abstraction:ss=axioms:ixr=off:ntd=on_2972 on theBenchmark for (2972ds/959Mi)
% 21.59/3.48 % (1397295)Refutation not found, incomplete strategy
% 21.59/3.48 % (1397295)------------------------------
% 21.59/3.48 % (1397295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.59/3.48 % (1397295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.48 % (1397295)CaDiCaL version: 2.1.3
% 21.59/3.48 % (1397295)Termination reason: Refutation not found, incomplete strategy
% 21.59/3.48 % (1397295)Time elapsed: 0.005 s
% 21.59/3.48 % (1397295)Peak memory usage: 13 MB
% 21.59/3.48 % (1397295)Instructions burned: 6 (million)
% 21.59/3.48 % (1397295)------------------------------
% 21.59/3.48 % (1397295)------------------------------
% 21.59/3.48 % (1397215)Instruction limit reached!
% 21.59/3.48 % (1397215)------------------------------
% 21.59/3.48 % (1397215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.59/3.48 % (1397215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.48 % (1397215)CaDiCaL version: 2.1.3
% 21.59/3.48 % (1397215)Termination reason: Instruction limit
% 21.59/3.48 % (1397215)Termination phase: Saturation
% 21.59/3.48 % (1397215)Time elapsed: 1.084 s
% 21.59/3.48 % (1397215)Peak memory usage: 33 MB
% 21.59/3.48 % (1397215)Instructions burned: 2470 (million)
% 21.59/3.48 % (1397299)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=3120226906:i=6359:add=on:kws=inv_frequency:aac=none:rtra=on:c=on:er=filter:ntd=on_2972 on theBenchmark for (2972ds/6359Mi)
% 21.59/3.48 % (1397276)Instruction limit reached!
% 21.59/3.48 % (1397276)------------------------------
% 21.59/3.48 % (1397276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.59/3.48 % (1397276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.48 % (1397276)CaDiCaL version: 2.1.3
% 21.59/3.48 % (1397276)Termination reason: Instruction limit
% 22.78/3.65 % (1397276)Termination phase: Saturation
% 22.78/3.65 % (1397276)Time elapsed: 0.357 s
% 22.78/3.65 % (1397276)Peak memory usage: 14 MB
% 22.78/3.65 % (1397276)Instructions burned: 857 (million)
% 22.78/3.65 % (1397300)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=687696557:st=4:i=35:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2972 on theBenchmark for (2972ds/35Mi)
% 22.78/3.65 % (1397300)Refutation not found, incomplete strategy
% 22.78/3.65 % (1397300)------------------------------
% 22.78/3.65 % (1397300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.78/3.65 % (1397300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.78/3.65 % (1397300)CaDiCaL version: 2.1.3
% 22.78/3.65 % (1397300)Termination reason: Refutation not found, incomplete strategy
% 22.78/3.65 % (1397300)Time elapsed: 0.006 s
% 22.78/3.65 % (1397300)Peak memory usage: 12 MB
% 22.78/3.65 % (1397300)Instructions burned: 9 (million)
% 22.78/3.65 % (1397300)------------------------------
% 22.78/3.65 % (1397300)------------------------------
% 22.78/3.65 % (1397302)dis+10_1_sfv=off:sil=128000:cnfonf=lazy_gen:si=on:uwa=off:nwc=1:chr=on:random_seed=2350907264:hsq=on:hsqr=1,8:i=53:hsql=off:bd=all:rtra=on:ixr=off_2972 on theBenchmark for (2972ds/53Mi)
% 22.78/3.65 % (1397304)dis+21_1_sil=128000:tgt=full:fde=none:e2e=on:si=on:urr=on:uwa=interpreted_only:s2agt=32:sac=on:random_seed=3559637817:s2a=on:i=876:s2at=6:nm=2:rtra=on_2972 on theBenchmark for (2972ds/876Mi)
% 22.78/3.65 % (1397302)Instruction limit reached!
% 22.78/3.65 % (1397302)------------------------------
% 22.78/3.65 % (1397302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.78/3.65 % (1397302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.78/3.65 % (1397302)CaDiCaL version: 2.1.3
% 22.78/3.65 % (1397302)Termination reason: Instruction limit
% 22.78/3.65 % (1397302)Termination phase: Saturation
% 22.78/3.65 % (1397302)Time elapsed: 0.031 s
% 22.78/3.65 % (1397302)Peak memory usage: 12 MB
% 22.78/3.65 % (1397302)Instructions burned: 55 (million)
% 22.78/3.65 % (1397304)Refutation not found, incomplete strategy
% 22.78/3.65 % (1397304)------------------------------
% 22.78/3.65 % (1397304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.78/3.65 % (1397304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.78/3.65 % (1397304)CaDiCaL version: 2.1.3
% 22.78/3.65 % (1397304)Termination reason: Refutation not found, incomplete strategy
% 22.78/3.65 % (1397304)Time elapsed: 0.030 s
% 22.78/3.65 % (1397304)Peak memory usage: 12 MB
% 22.78/3.65 % (1397304)Instructions burned: 50 (million)
% 22.78/3.65 % (1397304)------------------------------
% 22.78/3.65 % (1397304)------------------------------
% 22.78/3.65 % (1397307)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=347487672:i=57:ep=R:rtra=on:ntd=on_2971 on theBenchmark for (2971ds/57Mi)
% 22.78/3.65 % (1397308)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 22.78/3.65 % (1397307)Refutation not found, incomplete strategy
% 22.78/3.65 % (1397307)------------------------------
% 22.78/3.65 % (1397307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.78/3.65 % (1397307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.78/3.65 % (1397307)CaDiCaL version: 2.1.3
% 22.78/3.65 % (1397307)Termination reason: Refutation not found, incomplete strategy
% 22.78/3.65 % (1397307)Time elapsed: 0.004 s
% 22.78/3.65 % (1397307)Peak memory usage: 12 MB
% 22.78/3.65 % (1397307)Instructions burned: 7 (million)
% 22.78/3.65 % (1397307)------------------------------
% 22.78/3.65 % (1397307)------------------------------
% 22.78/3.65 % (1397308)dis+1002_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_min:sos=on:fd=preordered:slsqc=2:chr=on:random_seed=2969425008:i=306:bd=all:rtra=on_2971 on theBenchmark for (2971ds/306Mi)
% 22.78/3.65 % (1397310)dis+10_8:1_sil=128000:si=on:uwa=off:random_seed=735328177:i=262:sd=2:bd=preordered:rtra=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/262Mi)
% 22.78/3.65 % (1397310)Instruction limit reached!
% 22.78/3.65 % (1397310)------------------------------
% 22.78/3.65 % (1397310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.78/3.65 % (1397310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.78/3.65 % (1397310)CaDiCaL version: 2.1.3
% 22.16/3.78 % (1397310)Termination reason: Instruction limit
% 22.16/3.78 % (1397310)Termination phase: Saturation
% 22.16/3.78 % (1397310)Time elapsed: 0.124 s
% 22.16/3.78 % (1397310)Peak memory usage: 13 MB
% 22.16/3.78 % (1397310)Instructions burned: 264 (million)
% 22.16/3.78 % (1397308)Instruction limit reached!
% 22.16/3.78 % (1397308)------------------------------
% 22.16/3.78 % (1397308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.78 % (1397308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.78 % (1397308)CaDiCaL version: 2.1.3
% 22.16/3.78 % (1397308)Termination reason: Instruction limit
% 22.16/3.78 % (1397308)Termination phase: Saturation
% 22.16/3.78 % (1397308)Time elapsed: 0.153 s
% 22.16/3.78 % (1397308)Peak memory usage: 13 MB
% 22.16/3.78 % (1397308)Instructions burned: 307 (million)
% 22.16/3.78 % (1397313)WARNING Broken Constraint: if ho_split_queue_ratios(1,3) has been set then ho_split_queue(off) is equal to on
% 22.16/3.78 % (1397313)ott+1002_16_sil=128000:si=on:random_seed=2598479660:hsqr=1,3:i=409:add=on:rtra=on:fe=abstraction_2970 on theBenchmark for (2970ds/409Mi)
% 22.16/3.78 % (1397314)dis+10_1_sil=128000:plsq=on:si=on:plsqr=32,1:uwa=off:random_seed=770416799:s2a=on:i=381:rtra=on_2969 on theBenchmark for (2969ds/381Mi)
% 22.16/3.79 % (1397296)Instruction limit reached!
% 22.16/3.79 % (1397296)------------------------------
% 22.16/3.79 % (1397296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397296)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397296)Termination reason: Instruction limit
% 22.16/3.79 % (1397296)Termination phase: Saturation
% 22.16/3.79 % (1397296)Time elapsed: 0.454 s
% 22.16/3.79 % (1397296)Peak memory usage: 15 MB
% 22.16/3.79 % (1397296)Instructions burned: 960 (million)
% 22.16/3.79 % (1397291)Instruction limit reached!
% 22.16/3.79 % (1397291)------------------------------
% 22.16/3.79 % (1397291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397291)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397291)Termination reason: Instruction limit
% 22.16/3.79 % (1397291)Termination phase: Saturation
% 22.16/3.79 % (1397291)Time elapsed: 0.496 s
% 22.16/3.79 % (1397291)Peak memory usage: 14 MB
% 22.16/3.79 % (1397291)Instructions burned: 1143 (million)
% 22.16/3.79 % (1397314)Instruction limit reached!
% 22.16/3.79 % (1397314)------------------------------
% 22.16/3.79 % (1397314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397314)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397314)Termination reason: Instruction limit
% 22.16/3.79 % (1397314)Termination phase: Saturation
% 22.16/3.79 % (1397314)Time elapsed: 0.181 s
% 22.16/3.79 % (1397314)Peak memory usage: 13 MB
% 22.16/3.79 % (1397314)Instructions burned: 382 (million)
% 22.16/3.79 % (1397313)Instruction limit reached!
% 22.16/3.79 % (1397313)------------------------------
% 22.16/3.79 % (1397313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397313)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397313)Termination reason: Instruction limit
% 22.16/3.79 % (1397313)Termination phase: Saturation
% 22.16/3.79 % (1397313)Time elapsed: 0.200 s
% 22.16/3.79 % (1397313)Peak memory usage: 13 MB
% 22.16/3.79 % (1397313)Instructions burned: 409 (million)
% 22.16/3.79 % (1397317)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3254320117:cond=on:i=324:rtra=on:ntd=on_2968 on theBenchmark for (2968ds/324Mi)
% 22.16/3.79 % (1397318)lrs+10_1_sil=128000:fde=none:si=on:sos=on:spb=goal_then_units:urr=on:random_seed=3092810981:i=240:kws=inv_precedence:rtra=on_2968 on theBenchmark for (2968ds/240Mi)
% 22.16/3.79 % (1397317)Refutation not found, incomplete strategy
% 22.16/3.79 % (1397317)------------------------------
% 22.16/3.79 % (1397317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397317)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397317)Termination reason: Refutation not found, incomplete strategy
% 22.16/3.79 % (1397317)Time elapsed: 0.005 s
% 22.16/3.79 % (1397317)Peak memory usage: 12 MB
% 22.16/3.79 % (1397317)Instructions burned: 7 (million)
% 22.16/3.79 % (1397317)------------------------------
% 22.16/3.79 % (1397317)------------------------------
% 22.16/3.79 % (1397319)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 22.16/3.79 % (1397319)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1767228884:cts=off:uwa_fpi=on:i=124:av=off:fsr=off:rtra=on:ntd=on_2967 on theBenchmark for (2967ds/124Mi)
% 22.16/3.79 % (1397322)lrs+1010_2_to=lpo:cnfonf=off:e2e=on:si=on:random_seed=2705229066:uwa_fpi=on:i=223:bd=all:rtra=on:fe=abstraction:ntd=on_2967 on theBenchmark for (2967ds/223Mi)
% 22.16/3.79 % (1397323)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=446604786:s2a=on:i=282:kws=inv_frequency:bd=all:rtra=on_2967 on theBenchmark for (2967ds/282Mi)
% 22.16/3.79 % (1397319)Instruction limit reached!
% 22.16/3.79 % (1397319)------------------------------
% 22.16/3.79 % (1397319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397319)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397319)Termination reason: Instruction limit
% 22.16/3.79 % (1397319)Termination phase: Saturation
% 22.16/3.79 % (1397319)Time elapsed: 0.059 s
% 22.16/3.79 % (1397319)Peak memory usage: 12 MB
% 22.16/3.79 % (1397319)Instructions burned: 126 (million)
% 22.16/3.79 % (1397327)lrs+10_1_sil=128000:tgt=ground:cnfonf=conj_eager:si=on:random_seed=2815284158:s2a=on:i=464:kws=frequency:bd=all:rtra=on:ss=axioms_2967 on theBenchmark for (2967ds/464Mi)
% 22.16/3.79 % (1397318)Instruction limit reached!
% 22.16/3.79 % (1397318)------------------------------
% 22.16/3.79 % (1397318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397318)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397318)Termination reason: Instruction limit
% 22.16/3.79 % (1397318)Termination phase: Saturation
% 22.16/3.79 % (1397318)Time elapsed: 0.116 s
% 22.16/3.79 % (1397318)Peak memory usage: 13 MB
% 22.16/3.79 % (1397318)Instructions burned: 241 (million)
% 22.16/3.79 % (1397322)Instruction limit reached!
% 22.16/3.79 % (1397322)------------------------------
% 22.16/3.79 % (1397322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397322)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397322)Termination reason: Instruction limit
% 22.16/3.79 % (1397322)Termination phase: Saturation
% 22.16/3.79 % (1397322)Time elapsed: 0.113 s
% 22.16/3.79 % (1397322)Peak memory usage: 14 MB
% 22.16/3.79 % (1397322)Instructions burned: 224 (million)
% 22.16/3.79 % (1397329)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=2759828322:i=88:s2at=3:nm=2:rtra=on:rawr=on_2966 on theBenchmark for (2966ds/88Mi)
% 22.16/3.79 % (1397330)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=2356682652:s2a=on:cond=on:i=280:add=on:bd=preordered:rtra=on:er=filter_2966 on theBenchmark for (2966ds/280Mi)
% 22.16/3.79 % (1397323)Instruction limit reached!
% 22.16/3.79 % (1397323)------------------------------
% 22.16/3.79 % (1397323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397323)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397323)Termination reason: Instruction limit
% 22.16/3.79 % (1397323)Termination phase: Saturation
% 22.16/3.79 % (1397323)Time elapsed: 0.136 s
% 22.16/3.79 % (1397323)Peak memory usage: 14 MB
% 22.16/3.79 % (1397323)Instructions burned: 282 (million)
% 22.16/3.79 % (1397333)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 22.16/3.79 % (1397329)Instruction limit reached!
% 22.16/3.79 % (1397329)------------------------------
% 22.16/3.79 % (1397329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397329)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397329)Termination reason: Instruction limit
% 22.16/3.79 % (1397329)Termination phase: Saturation
% 22.16/3.79 % (1397329)Time elapsed: 0.042 s
% 22.16/3.79 % (1397329)Peak memory usage: 13 MB
% 22.16/3.79 % (1397329)Instructions burned: 88 (million)
% 22.16/3.79 % (1397333)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1860003914:i=4386:hud=10:nm=16:av=off:rtra=on:ntd=on_2966 on theBenchmark for (2966ds/4386Mi)
% 22.16/3.79 % (1397334)WARNING Broken Constraint: if lookahaed_delay(10) has been set then selection(21) is not lookahead selection
% 22.16/3.79 % (1397334)WARNING Broken Constraint: if mono_ep(off) has been set then equality_proxy(off) is not equal to off
% 22.16/3.79 % (1397334)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=3364934767:hsq=on:st=2:i=483:sd=1:hsql=off:rtra=on:fe=abstraction:fdi=32:ss=axioms:sgt=20:ntd=on_2966 on theBenchmark for (2966ds/483Mi)
% 22.16/3.79 % (1397258)Instruction limit reached!
% 22.16/3.79 % (1397258)------------------------------
% 22.16/3.79 % (1397258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397258)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397258)Termination reason: Instruction limit
% 22.16/3.79 % (1397258)Termination phase: Saturation
% 22.16/3.79 % (1397258)Time elapsed: 1.173 s
% 22.16/3.79 % (1397258)Peak memory usage: 17 MB
% 22.16/3.79 % (1397258)Instructions burned: 4981 (million)
% 22.16/3.79 % (1397337)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=4246251921:i=73:rtra=on_2965 on theBenchmark for (2965ds/73Mi)
% 22.16/3.79 % (1397337)Instruction limit reached!
% 22.16/3.79 % (1397337)------------------------------
% 22.16/3.79 % (1397337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397337)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397337)Termination reason: Instruction limit
% 22.16/3.79 % (1397337)Termination phase: Saturation
% 22.16/3.79 % (1397337)Time elapsed: 0.022 s
% 22.16/3.79 % (1397337)Peak memory usage: 12 MB
% 22.16/3.79 % (1397337)Instructions burned: 75 (million)
% 22.16/3.79 % (1397339)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=733811301:cts=off:i=176:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2965 on theBenchmark for (2965ds/176Mi)
% 22.16/3.79 % (1397286)Instruction limit reached!
% 22.16/3.79 % (1397286)------------------------------
% 22.16/3.79 % (1397286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397286)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397286)Termination reason: Instruction limit
% 22.16/3.79 % (1397286)Termination phase: Saturation
% 22.16/3.79 % (1397286)Time elapsed: 0.981 s
% 22.16/3.79 % (1397286)Peak memory usage: 24 MB
% 22.16/3.79 % (1397286)Instructions burned: 2241 (million)
% 22.16/3.79 % (1397330)Instruction limit reached!
% 22.16/3.79 % (1397330)------------------------------
% 22.16/3.79 % (1397330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397330)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397330)Termination reason: Instruction limit
% 22.16/3.79 % (1397330)Termination phase: Saturation
% 22.16/3.79 % (1397330)Time elapsed: 0.137 s
% 22.16/3.79 % (1397330)Peak memory usage: 13 MB
% 22.16/3.79 % (1397330)Instructions burned: 280 (million)
% 22.16/3.79 % (1397341)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 22.16/3.79 % (1397341)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=3387737887:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2965 on theBenchmark for (2965ds/39Mi)
% 22.16/3.79 % (1397342)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=65176916:i=708:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2964 on theBenchmark for (2964ds/708Mi)
% 22.16/3.79 % (1397339) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1396708-1397339"...
% 22.16/3.79 % (1397341)Instruction limit reached!
% 22.16/3.79 % (1397341)------------------------------
% 22.16/3.79 % (1397341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397341)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397341)Termination reason: Instruction limit
% 22.16/3.79 % (1397341)Termination phase: Saturation
% 22.16/3.79 % (1397341)Time elapsed: 0.021 s
% 22.16/3.79 % (1397341)Peak memory usage: 12 MB
% 22.16/3.79 % (1397341)Instructions burned: 39 (million)
% 22.16/3.79 % (1397339)...printing done.
% 22.16/3.79 % (1397339)Refutation found. Thanks to Tanya!
% 22.16/3.79 % SZS status Theorem for theBenchmark
% 22.16/3.79 % SZS output start Proof for theBenchmark
% See solution above
% 22.16/3.79 % (1397339)------------------------------
% 22.16/3.79 % (1397339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.16/3.79 % (1397339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.16/3.79 % (1397339)CaDiCaL version: 2.1.3
% 22.16/3.79 % (1397339)Termination reason: Refutation
% 22.16/3.79 % (1397339)Time elapsed: 0.042 s
% 22.16/3.79 % (1397339)Peak memory usage: 14 MB
% 22.16/3.79 % (1397339)Instructions burned: 162 (million)
% 22.16/3.79 % (1396708)Success in time 3.537 s
% 22.16/3.79 % Vampire exiting
%------------------------------------------------------------------------------