%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU876^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:31:51 AM UTC 2026
% Result : Theorem 41.57s 6.29s
% Output : Refutation 41.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 8
% Syntax : Number of formulae : 110 ( 17 unt; 0 typ; 7 def)
% Number of atoms : 1217 ( 170 equ; 0 cnn)
% Maximal formula atoms : 14 ( 11 avg)
% Number of connectives : 2309 ( 145 ~; 231 |; 170 &;1208 @)
% ( 7 <=>; 295 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 316 ( 316 >; 0 *; 0 +; 0 <<)
% Number of symbols : 56 ( 51 usr; 29 con; 0-4 aty)
% ( 243 !!; 10 ??; 0 @@+; 0 @@-)
% Number of variables : 412 ( 60 sgn 59 !; 3 ?; 412 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
cE: a > $o ).
thf(func_def_1,type,
cA: ( a > $o ) > $o ).
thf(func_def_3,type,
vNOT: $o > $o ).
thf(func_def_4,type,
vIMP: $o > $o > $o ).
thf(func_def_5,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_6,type,
vAND: $o > $o > $o ).
thf(func_def_7,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_10,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_11,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_12,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_13,type,
vOR: $o > $o > $o ).
thf(func_def_14,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_15,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_16,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_18,type,
sK1: a > $o ).
thf(func_def_19,type,
sK2: a > $o ).
thf(func_def_20,type,
sK3: ( ( a > $o ) > $o ) > a > $o ).
thf(func_def_21,type,
sK4: ( a > $o ) > ( a > $o ) > $o ).
thf(func_def_22,type,
sK5: ( a > $o ) > a > $o ).
thf(func_def_23,type,
sK6: a > $o ).
thf(func_def_24,type,
sK7: a ).
thf(func_def_25,type,
sK8: a > $o ).
thf(func_def_26,type,
sK9: a ).
thf(func_def_27,type,
sK10: a ).
thf(func_def_28,type,
sK11: a ).
thf(func_def_29,type,
sK12: a ).
thf(func_def_30,type,
sK13: a ).
thf(func_def_31,type,
sK14: a ).
thf(func_def_32,type,
sK15: a ).
thf(func_def_33,type,
sK16: a ).
thf(func_def_34,type,
sK17: a ).
thf(func_def_35,type,
sK18: a ).
thf(func_def_36,type,
sK19: ( ( a > $o ) > $o ) > a ).
thf(func_def_37,type,
sK20: a ).
thf(func_def_38,type,
sK21: a ).
thf(func_def_39,type,
sK22: a ).
thf(func_def_40,type,
sK23: a ).
thf(func_def_41,type,
sK24: a ).
thf(func_def_42,type,
sK25: a > $o ).
thf(func_def_43,type,
sK26: a ).
thf(func_def_44,type,
sK27: a ).
thf(func_def_45,type,
sK28: ( a > $o ) > a ).
thf(func_def_46,type,
sK29: ( a > $o ) > a ).
thf(f1,conjecture,
( ! [X0: ( a > $o ) > $o] :
( ( ! [X2: a > $o] :
( ( X0 @ X2 )
=> ! [X3: a] :
( ( cE @ X3 )
=> ( X0
@ ^ [X4: a] :
( ( X3 = X4 )
| ( X2 @ X4 ) ) ) ) )
& ( X0
@ ^ [X1: a] : $false ) )
=> ( X0 @ cE ) )
=> ( ! [X2: a > $o] :
( ( ! [X5: a] :
( ( cE @ X5 )
=> ( X2 @ X5 ) )
& ( cA @ X2 ) )
=> ? [X6: a > $o] :
( ! [X0: ( a > $o ) > $o] :
( ( ( X0
@ ^ [X1: a] : $false )
& ! [X5: a > $o] :
( ( X0 @ X5 )
=> ! [X3: a] :
( ( X6 @ X3 )
=> ( X0
@ ^ [X4: a] :
( ( X3 = X4 )
| ( X5 @ X4 ) ) ) ) ) )
=> ( X0 @ X6 ) )
& ! [X5: a] :
( ( X6 @ X5 )
=> ( X2 @ X5 ) )
& ! [X1: a > $o] :
( ( ( cA @ X1 )
& ! [X5: a] :
( ( X6 @ X5 )
=> ( X1 @ X5 ) ) )
=> ( ( cA @ X1 )
& ! [X5: a] :
( ( cE @ X5 )
=> ( X1 @ X5 ) ) ) ) ) )
& ! [X2: a > $o] :
( ( ( cA @ X2 )
& ! [X5: a] :
( ( cE @ X5 )
=> ( X2 @ X5 ) ) )
=> ( cA @ X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cDOMLEMMA4_pme) ).
thf(f2,negated_conjecture,
~ ( ! [X0: ( a > $o ) > $o] :
( ( ! [X2: a > $o] :
( ( X0 @ X2 )
=> ! [X3: a] :
( ( cE @ X3 )
=> ( X0
@ ^ [X4: a] :
( ( X3 = X4 )
| ( X2 @ X4 ) ) ) ) )
& ( X0
@ ^ [X1: a] : $false ) )
=> ( X0 @ cE ) )
=> ( ! [X2: a > $o] :
( ( ! [X5: a] :
( ( cE @ X5 )
=> ( X2 @ X5 ) )
& ( cA @ X2 ) )
=> ? [X6: a > $o] :
( ! [X0: ( a > $o ) > $o] :
( ( ( X0
@ ^ [X1: a] : $false )
& ! [X5: a > $o] :
( ( X0 @ X5 )
=> ! [X3: a] :
( ( X6 @ X3 )
=> ( X0
@ ^ [X4: a] :
( ( X3 = X4 )
| ( X5 @ X4 ) ) ) ) ) )
=> ( X0 @ X6 ) )
& ! [X5: a] :
( ( X6 @ X5 )
=> ( X2 @ X5 ) )
& ! [X1: a > $o] :
( ( ( cA @ X1 )
& ! [X5: a] :
( ( X6 @ X5 )
=> ( X1 @ X5 ) ) )
=> ( ( cA @ X1 )
& ! [X5: a] :
( ( cE @ X5 )
=> ( X1 @ X5 ) ) ) ) ) )
& ! [X2: a > $o] :
( ( ( cA @ X2 )
& ! [X5: a] :
( ( cE @ X5 )
=> ( X2 @ X5 ) ) )
=> ( cA @ X2 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ( ! [X0: ( a > $o ) > $o] :
( ( ! [X1: a > $o] :
( ( X0 @ X1 )
=> ! [X2: a] :
( ( cE @ X2 )
=> ( X0
@ ^ [X3: a] :
( ( X2 = X3 )
| ( X1 @ X3 ) ) ) ) )
& ( X0
@ ^ [X4: a] : $false ) )
=> ( X0 @ cE ) )
=> ( ! [X5: a > $o] :
( ( ! [X6: a] :
( ( cE @ X6 )
=> ( X5 @ X6 ) )
& ( cA @ X5 ) )
=> ? [X7: a > $o] :
( ! [X8: ( a > $o ) > $o] :
( ( ( X8
@ ^ [X9: a] : $false )
& ! [X10: a > $o] :
( ( X8 @ X10 )
=> ! [X11: a] :
( ( X7 @ X11 )
=> ( X8
@ ^ [X12: a] :
( ( X11 = X12 )
| ( X10 @ X12 ) ) ) ) ) )
=> ( X8 @ X7 ) )
& ! [X13: a] :
( ( X7 @ X13 )
=> ( X5 @ X13 ) )
& ! [X14: a > $o] :
( ( ( cA @ X14 )
& ! [X15: a] :
( ( X7 @ X15 )
=> ( X14 @ X15 ) ) )
=> ( ( cA @ X14 )
& ! [X16: a] :
( ( cE @ X16 )
=> ( X14 @ X16 ) ) ) ) ) )
& ! [X17: a > $o] :
( ( ( cA @ X17 )
& ! [X18: a] :
( ( cE @ X18 )
=> ( X17 @ X18 ) ) )
=> ( cA @ X17 ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
( ( ~ ( ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
=> ( Y0 @ cE ) ) )
=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f3]) ).
thf(f5,plain,
( ( ~ ( ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
=> ( Y0 @ cE ) ) )
=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f4]) ).
thf(f8,plain,
( $false
= ( ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
=> ( Y0 @ cE ) ) )
=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f5]) ).
thf(f9,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f8]) ).
thf(f10,plain,
( ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
=> ( Y0 @ cE ) ) )
= $true ),
inference(imp_proxy_clausification,[],[f8]) ).
thf(f11,plain,
! [X1: ( a > $o ) > $o] :
( ( ^ [Y0: ( a > $o ) > $o] :
( ( ( Y0
@ ^ [Y1: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
=> ( Y0 @ cE ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f10]) ).
thf(f12,plain,
! [X1: ( a > $o ) > $o] :
( ( ( ( X1
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( X1 @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( X1
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) )
=> ( X1 @ cE ) )
= $true ),
inference(beta-eta_normalization,[],[f11]) ).
thf(f14,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
= $false )
| ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) )
= $false ) ),
inference(and_proxy_clausification,[],[f9]) ).
thf(f16,definition,
( spl0_1
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
thf(f18,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) ) )
= $false )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f16]) ).
thf(f20,definition,
( spl0_2
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
thf(f22,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) ) )
= $false )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f20]) ).
thf(f23,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f14,f20,f16]) ).
thf(f24,plain,
( ( ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( cA @ Y0 ) )
@ sK1 )
= $false )
| ~ spl0_2 ),
inference(sigma_proxy_clausification,[],[f22]) ).
thf(f25,plain,
( ( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK1 @ Y0 ) ) )
& ( cA @ sK1 ) )
=> ( cA @ sK1 ) )
= $false )
| ~ spl0_2 ),
inference(beta-eta_normalization,[],[f24]) ).
thf(f26,plain,
( ( ( cA @ sK1 )
= $false )
| ~ spl0_2 ),
inference(imp_proxy_clausification,[],[f25]) ).
thf(f27,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK1 @ Y0 ) ) )
& ( cA @ sK1 ) )
= $true )
| ~ spl0_2 ),
inference(imp_proxy_clausification,[],[f25]) ).
thf(f28,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK1 @ Y0 ) ) )
& $false )
= $true )
| ~ spl0_2 ),
inference(forward_demodulation,[],[f27,f26]) ).
thf(f29,plain,
( ( $false = $true )
| ~ spl0_2 ),
inference(boolean_simplification,[],[f28]) ).
thf(f30,plain,
( $false
| ~ spl0_2 ),
inference(trivial_inequality_removal,[],[f29]) ).
thf(f31,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f30]) ).
thf(f35,plain,
( ( ( ^ [Y0: a > $o] :
( ( ( cA @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) )
=> ( ( !! @ a
@ ^ [Y3: a] :
( ( cE @ Y3 )
=> ( Y2 @ Y3 ) ) )
& ( cA @ Y2 ) ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y2: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y2 @ Y3 )
=> ( !! @ a
@ ^ [Y4: a] :
( ( Y1 @ Y4 )
=> ( Y2
@ ^ [Y5: a] :
( ( Y3 @ Y5 )
| ( Y4 = Y5 ) ) ) ) ) ) )
& ( Y2
@ ^ [Y3: a] : $false ) )
=> ( Y2 @ Y1 ) ) ) ) ) )
@ sK2 )
= $false )
| ~ spl0_1 ),
inference(sigma_proxy_clausification,[],[f18]) ).
thf(f36,plain,
( ( ( ( ( cA @ sK2 )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
=> ( ?? @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( cA @ Y1 ) )
=> ( ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( cA @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( sK2 @ Y1 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( !! @ a
@ ^ [Y3: a] :
( ( Y0 @ Y3 )
=> ( Y1
@ ^ [Y4: a] :
( ( Y2 @ Y4 )
| ( Y3 = Y4 ) ) ) ) ) ) )
& ( Y1
@ ^ [Y2: a] : $false ) )
=> ( Y1 @ Y0 ) ) ) ) ) )
= $false )
| ~ spl0_1 ),
inference(beta-eta_normalization,[],[f35]) ).
thf(f37,plain,
( ( ( ?? @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( cA @ Y1 ) )
=> ( ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( cA @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( sK2 @ Y1 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( !! @ a
@ ^ [Y3: a] :
( ( Y0 @ Y3 )
=> ( Y1
@ ^ [Y4: a] :
( ( Y2 @ Y4 )
| ( Y3 = Y4 ) ) ) ) ) ) )
& ( Y1
@ ^ [Y2: a] : $false ) )
=> ( Y1 @ Y0 ) ) ) ) )
= $false )
| ~ spl0_1 ),
inference(imp_proxy_clausification,[],[f36]) ).
thf(f38,plain,
( ( ( ( cA @ sK2 )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $true )
| ~ spl0_1 ),
inference(imp_proxy_clausification,[],[f36]) ).
thf(f39,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $true )
| ~ spl0_1 ),
inference(and_proxy_clausification,[],[f38]) ).
thf(f51,plain,
( ! [X1: a > $o] :
( ( ^ [Y0: a > $o] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( cA @ Y1 ) )
=> ( ( !! @ a
@ ^ [Y2: a] :
( ( cE @ Y2 )
=> ( Y1 @ Y2 ) ) )
& ( cA @ Y1 ) ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( sK2 @ Y1 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( !! @ a
@ ^ [Y3: a] :
( ( Y0 @ Y3 )
=> ( Y1
@ ^ [Y4: a] :
( ( Y2 @ Y4 )
| ( Y3 = Y4 ) ) ) ) ) ) )
& ( Y1
@ ^ [Y2: a] : $false ) )
=> ( Y1 @ Y0 ) ) ) )
@ X1 )
= $false )
| ~ spl0_1 ),
inference(pi_proxy_clausification,[],[f37]) ).
thf(f52,plain,
( ! [X1: a > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) )
& ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( X1 @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) )
& ( Y0
@ ^ [Y1: a] : $false ) )
=> ( Y0 @ X1 ) ) ) )
= $false )
| ~ spl0_1 ),
inference(beta-eta_normalization,[],[f51]) ).
thf(f53,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) )
@ X1 )
= $true )
| ~ spl0_1 ),
inference(pi_proxy_clausification,[],[f39]) ).
thf(f54,plain,
( ! [X1: a] :
( ( ( cE @ X1 )
=> ( sK2 @ X1 ) )
= $true )
| ~ spl0_1 ),
inference(beta-eta_normalization,[],[f53]) ).
thf(f55,plain,
( ! [X1: a > $o] :
( ( ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( X1 @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) )
& ( Y0
@ ^ [Y1: a] : $false ) )
=> ( Y0 @ X1 ) ) )
= $false )
| ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) ) ) ) )
| ~ spl0_1 ),
inference(and_proxy_clausification,[],[f52]) ).
thf(f91,plain,
( ! [X1: a > $o] :
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) ) ) )
| ( ( ^ [Y0: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( !! @ a
@ ^ [Y2: a] :
( ( X1 @ Y2 )
=> ( Y0
@ ^ [Y3: a] :
( ( Y1 @ Y3 )
| ( Y2 = Y3 ) ) ) ) ) ) )
& ( Y0
@ ^ [Y1: a] : $false ) )
=> ( Y0 @ X1 ) )
@ ( sK4 @ X1 ) )
= $false ) )
| ~ spl0_1 ),
inference(sigma_proxy_clausification,[],[f55]) ).
thf(f92,plain,
( ! [X1: a > $o] :
( ( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ X1 @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( sK4 @ X1
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ X1
@ ^ [Y0: a] : $false ) )
=> ( sK4 @ X1 @ X1 ) )
= $false )
| ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) ) ) ) )
| ~ spl0_1 ),
inference(beta-eta_normalization,[],[f91]) ).
thf(f133,definition,
( spl0_7
<=> ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
thf(f134,plain,
( ( $false
!= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) )
| spl0_7 ),
inference(avatar_component_clause,[],[f133]) ).
thf(f135,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f133]) ).
thf(f138,plain,
( ( ( ^ [Y0: a > $o] : $true
@ sK6 )
= $false )
| ~ spl0_7 ),
inference(sigma_proxy_clausification,[],[f135]) ).
thf(f139,plain,
( ( $false = $true )
| ~ spl0_7 ),
inference(beta-eta_normalization,[],[f138]) ).
thf(f140,plain,
( $false
| ~ spl0_7 ),
inference(trivial_inequality_removal,[],[f139]) ).
thf(f141,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f140]) ).
thf(f581,plain,
( ! [X1: a > $o] :
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) ) ) )
| ( ( sK4 @ X1 @ X1 )
= $false ) )
| ~ spl0_1 ),
inference(imp_proxy_clausification,[],[f92]) ).
thf(f821,plain,
( ! [X1: a > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
= $false )
| ( ( sK4 @ X1 @ X1 )
= $false )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false ) )
| ~ spl0_1 ),
inference(and_proxy_clausification,[],[f581]) ).
thf(f854,plain,
( ! [X1: a > $o] :
( ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( ( sK4 @ X1 @ X1 )
= $false )
| ( ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( X1 @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) )
@ ( sK5 @ X1 ) )
= $false ) )
| ~ spl0_1 ),
inference(sigma_proxy_clausification,[],[f821]) ).
thf(f856,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
= $false )
| ( ( ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) )
=> $false )
= $true )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ~ spl0_1 ),
inference(superposition,[],[f12,f821]) ).
thf(f877,plain,
( ! [X1: a > $o] :
( ( $false
= ( ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK5 @ X1 @ Y0 ) ) )
& ( cA @ ( sK5 @ X1 ) ) )
=> ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK5 @ X1 @ Y0 ) ) )
& ( cA @ ( sK5 @ X1 ) ) ) ) )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( ( sK4 @ X1 @ X1 )
= $false ) )
| ~ spl0_1 ),
inference(beta-eta_normalization,[],[f854]) ).
thf(f878,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) )
| ( ( ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) )
=> $false )
= $true )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ~ spl0_1 ),
inference(boolean_simplification,[],[f856]) ).
thf(f879,plain,
( ( $true
= ( ~ ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) ) ) )
| ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ~ spl0_1 ),
inference(boolean_simplification,[],[f878]) ).
thf(f893,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( $true
= ( ~ ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) ) ) )
| ~ spl0_1
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f879,f134]) ).
thf(f894,plain,
( ( $true
= ( ~ ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) ) ) )
| ( $false = $true )
| ~ spl0_1
| spl0_7 ),
inference(forward_demodulation,[],[f893,f39]) ).
thf(f895,plain,
( ( $true
= ( ~ ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) ) ) )
| ~ spl0_1
| spl0_7 ),
inference(trivial_inequality_removal,[],[f894]) ).
thf(f911,plain,
( ( ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) ) )
= $false )
| ~ spl0_1
| spl0_7 ),
inference(not_proxy_clausification,[],[f895]) ).
thf(f921,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
= $false )
| ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
= $false )
| ~ spl0_1
| spl0_7 ),
inference(and_proxy_clausification,[],[f911]) ).
thf(f923,definition,
( spl0_28
<=> ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
thf(f925,plain,
( ( ( sK4 @ cE
@ ^ [Y0: a] : $false )
= $false )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f923]) ).
thf(f927,definition,
( spl0_29
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
thf(f929,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
= $false )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f927]) ).
thf(f930,plain,
( spl0_28
| spl0_29
| ~ spl0_1
| spl0_7 ),
inference(avatar_split_clause,[],[f921,f133,f16,f927,f923]) ).
thf(f990,plain,
( ! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK5 @ X1 @ Y0 ) ) )
& ( cA @ ( sK5 @ X1 ) ) )
= $true )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( ( sK4 @ X1 @ X1 )
= $false ) )
| ~ spl0_1 ),
inference(imp_proxy_clausification,[],[f877]) ).
thf(f1041,plain,
( ! [X1: a > $o] :
( ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( ( sK4 @ X1 @ X1 )
= $false )
| ( ( cA @ ( sK5 @ X1 ) )
= $true ) )
| ~ spl0_1 ),
inference(and_proxy_clausification,[],[f990]) ).
thf(f1043,plain,
( ! [X1: a > $o] :
( ( ( sK4 @ X1 @ X1 )
= $false )
| ( ( ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( sK2 @ Y0 ) )
@ ( sK29 @ X1 ) )
= $false )
| ( ( cA @ ( sK5 @ X1 ) )
= $true ) )
| ~ spl0_1 ),
inference(sigma_proxy_clausification,[],[f1041]) ).
thf(f1056,plain,
( ! [X1: a > $o] :
( ( ( ( X1 @ ( sK29 @ X1 ) )
=> ( sK2 @ ( sK29 @ X1 ) ) )
= $false )
| ( ( sK4 @ X1 @ X1 )
= $false )
| ( ( cA @ ( sK5 @ X1 ) )
= $true ) )
| ~ spl0_1 ),
inference(beta-eta_normalization,[],[f1043]) ).
thf(f1086,plain,
( ( ( sK4 @ cE @ cE )
= $false )
| ( $false = $true )
| ( ( cA @ ( sK5 @ cE ) )
= $true )
| ~ spl0_1 ),
inference(superposition,[],[f1056,f54]) ).
thf(f1093,plain,
( ( ( sK4 @ cE @ cE )
= $false )
| ( ( cA @ ( sK5 @ cE ) )
= $true )
| ~ spl0_1 ),
inference(trivial_inequality_removal,[],[f1086]) ).
thf(f1099,definition,
( spl0_34
<=> ( ( cA @ ( sK5 @ cE ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
thf(f1101,plain,
( ( ( cA @ ( sK5 @ cE ) )
= $true )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f1099]) ).
thf(f1103,definition,
( spl0_35
<=> ( ( sK4 @ cE @ cE )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
thf(f1105,plain,
( ( ( sK4 @ cE @ cE )
= $false )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f1103]) ).
thf(f1107,plain,
( spl0_34
| spl0_35
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1093,f16,f1103,f1099]) ).
thf(f1124,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK5 @ cE @ Y0 ) ) )
& $true )
=> ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK5 @ cE @ Y0 ) ) )
& $true ) )
= $false )
| ( ( sK4 @ cE @ cE )
= $false )
| ~ spl0_1
| ~ spl0_34 ),
inference(superposition,[],[f877,f1101]) ).
thf(f1126,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ( ( sK4 @ cE @ cE )
= $false )
| ( $false = $true )
| ~ spl0_1
| ~ spl0_34 ),
inference(boolean_simplification,[],[f1124]) ).
thf(f1127,plain,
( ( ( sK4 @ cE @ cE )
= $false )
| ( ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) )
= $false )
| ~ spl0_1
| ~ spl0_34 ),
inference(trivial_inequality_removal,[],[f1126]) ).
thf(f1131,plain,
( ( ( sK4 @ cE @ cE )
= $false )
| ( $false = $true )
| ~ spl0_1
| ~ spl0_34 ),
inference(forward_demodulation,[],[f1127,f39]) ).
thf(f1132,plain,
( ( ( sK4 @ cE @ cE )
= $false )
| ~ spl0_1
| ~ spl0_34 ),
inference(trivial_inequality_removal,[],[f1131]) ).
thf(f1135,plain,
( spl0_35
| ~ spl0_1
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f1132,f1099,f16,f1103]) ).
thf(f1142,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) )
=> ( ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( Y0 @ Y1 ) ) )
& ( cA @ Y0 ) ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) )
=> $false )
= $false )
| ~ spl0_1
| ~ spl0_35 ),
inference(superposition,[],[f92,f1105]) ).
thf(f1144,plain,
( ( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) )
=> $false )
= $false )
| ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1142]) ).
thf(f1145,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) ) )
= $false )
| ~ spl0_1
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1144]) ).
thf(f1146,plain,
( ( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& $false ) )
= $false )
| ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_28
| ~ spl0_35 ),
inference(forward_demodulation,[],[f1145,f925]) ).
thf(f1147,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ( ( ~ $false ) = $false )
| ~ spl0_1
| ~ spl0_28
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1146]) ).
thf(f1148,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ( $false = $true )
| ~ spl0_1
| ~ spl0_28
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1147]) ).
thf(f1149,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( cE @ Y0 )
=> ( sK2 @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_28
| ~ spl0_35 ),
inference(trivial_inequality_removal,[],[f1148]) ).
thf(f1150,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& $true )
= $false )
| ~ spl0_1
| ~ spl0_28
| ~ spl0_35 ),
inference(forward_demodulation,[],[f1149,f39]) ).
thf(f1151,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) )
| ~ spl0_1
| ~ spl0_28
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1150]) ).
thf(f1152,plain,
( $false
| ~ spl0_1
| spl0_7
| ~ spl0_28
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1151,f134]) ).
thf(f1153,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_28
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1152]) ).
thf(f1154,plain,
( ( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) ) )
= $false )
| ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true )
& $true )
= $false )
| ~ spl0_1
| ~ spl0_35 ),
inference(forward_demodulation,[],[f1145,f39]) ).
thf(f1155,plain,
( ( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) ) )
= $false )
| ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] : $true ) )
| ~ spl0_1
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1154]) ).
thf(f1156,plain,
( ( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK4 @ cE @ Y0 )
=> ( !! @ a
@ ^ [Y1: a] :
( ( cE @ Y1 )
=> ( sK4 @ cE
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
| ( Y1 = Y2 ) ) ) ) ) ) )
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) ) )
= $false )
| ~ spl0_1
| spl0_7
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1155,f134]) ).
thf(f1157,plain,
( ( ( ~ ( $false
& ( sK4 @ cE
@ ^ [Y0: a] : $false ) ) )
= $false )
| ~ spl0_1
| spl0_7
| ~ spl0_29
| ~ spl0_35 ),
inference(forward_demodulation,[],[f1156,f929]) ).
thf(f1158,plain,
( ( ( ~ $false ) = $false )
| ~ spl0_1
| spl0_7
| ~ spl0_29
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1157]) ).
thf(f1159,plain,
( ( $false = $true )
| ~ spl0_1
| spl0_7
| ~ spl0_29
| ~ spl0_35 ),
inference(boolean_simplification,[],[f1158]) ).
thf(f1160,plain,
( $false
| ~ spl0_1
| spl0_7
| ~ spl0_29
| ~ spl0_35 ),
inference(trivial_inequality_removal,[],[f1159]) ).
thf(f1161,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_29
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1160]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f23]) ).
cnf(s2,plain,
~ spl0_2,
inference(sat_conversion,[],[f31]) ).
cnf(s7,plain,
~ spl0_7,
inference(sat_conversion,[],[f141]) ).
cnf(s25,plain,
( ~ spl0_1
| spl0_7
| spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f930]) ).
cnf(s29,plain,
( ~ spl0_1
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f1107]) ).
cnf(s32,plain,
( ~ spl0_1
| ~ spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f1135]) ).
cnf(s34,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_28
| ~ spl0_35 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s35,plain,
( ~ spl0_1
| spl0_7
| ~ spl0_29
| ~ spl0_35 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s39,plain,
spl0_1,
inference(rat,[],[s1,s2]) ).
cnf(s48,plain,
spl0_35,
inference(rat,[],[s29,s32,s39]) ).
cnf(s49,plain,
~ spl0_29,
inference(rat,[],[s35,s39,s7,s48]) ).
cnf(s50,plain,
~ spl0_28,
inference(rat,[],[s34,s39,s7,s48]) ).
cnf(s51,plain,
$false,
inference(rat,[],[s25,s39,s7,s49,s50]) ).
thf(f1162,plain,
$false,
inference(avatar_sat_refutation,[],[s51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU876^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 % Computer : n010.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 14:43:28 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.28 Running higher-order theorem proving
% 0.26/0.30 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/0.48 % (2951965)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.63/0.48 % (2951972)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4208086868:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.63/0.48 % (2951972)Instruction limit reached!
% 0.63/0.48 % (2951972)------------------------------
% 0.63/0.48 % (2951972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (2951972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (2951972)CaDiCaL version: 2.1.3
% 0.63/0.48 % (2951972)Termination reason: Instruction limit
% 0.63/0.48 % (2951972)Termination phase: Saturation
% 0.63/0.48 % (2951972)Time elapsed: 0.003 s
% 0.63/0.48 % (2951972)Peak memory usage: 12 MB
% 0.63/0.48 % (2951972)Instructions burned: 4 (million)
% 0.63/0.48 % (2951976)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.63/0.48 % (2951976)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.63/0.48 % (2951971)lrs+10_16_si=on:nwc=1.5:random_seed=470515835:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.63/0.48 % (2951970)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3185428626:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.63/0.48 % (2951974)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=816592944:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.63/0.48 % (2951973)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=1296729889: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.63/0.48 % (2951975)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4259732706:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.63/0.48 % (2951976)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=4257370124:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.63/0.48 % (2951978)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3141030430:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.63/0.48 % (2951978)Instruction limit reached!
% 0.63/0.48 % (2951978)------------------------------
% 0.63/0.48 % (2951978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (2951978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (2951978)CaDiCaL version: 2.1.3
% 0.63/0.48 % (2951978)Termination reason: Instruction limit
% 0.63/0.48 % (2951978)Termination phase: Saturation
% 0.63/0.48 % (2951978)Time elapsed: 0.001 s
% 0.63/0.48 % (2951978)Peak memory usage: 11 MB
% 0.63/0.48 % (2951978)Instructions burned: 2 (million)
% 0.63/0.48 % (2951971)Instruction limit reached!
% 0.63/0.48 % (2951971)------------------------------
% 0.63/0.48 % (2951971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (2951971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (2951971)CaDiCaL version: 2.1.3
% 0.63/0.48 % (2951971)Termination reason: Instruction limit
% 0.63/0.48 % (2951971)Termination phase: Saturation
% 0.63/0.48 % (2951971)Time elapsed: 0.019 s
% 0.63/0.48 % (2951971)Peak memory usage: 12 MB
% 0.63/0.48 % (2951971)Instructions burned: 18 (million)
% 0.63/0.48 % (2951974)Instruction limit reached!
% 0.63/0.48 % (2951974)------------------------------
% 0.63/0.48 % (2951974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (2951974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (2951974)CaDiCaL version: 2.1.3
% 0.63/0.48 % (2951974)Termination reason: Instruction limit
% 0.63/0.48 % (2951974)Termination phase: Saturation
% 0.63/0.48 % (2951974)Time elapsed: 0.023 s
% 0.63/0.48 % (2951974)Peak memory usage: 12 MB
% 0.63/0.48 % (2951974)Instructions burned: 24 (million)
% 0.63/0.48 % (2951986)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1679420064:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.36/0.52 % (2951986)Instruction limit reached!
% 1.36/0.52 % (2951986)------------------------------
% 1.36/0.52 % (2951986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.52 % (2951986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.52 % (2951986)CaDiCaL version: 2.1.3
% 1.36/0.52 % (2951986)Termination reason: Instruction limit
% 1.36/0.52 % (2951986)Termination phase: Saturation
% 1.36/0.52 % (2951986)Time elapsed: 0.004 s
% 1.36/0.52 % (2951986)Peak memory usage: 12 MB
% 1.36/0.52 % (2951986)Instructions burned: 6 (million)
% 1.36/0.52 % (2951987)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.36/0.52 % (2951990)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.36/0.52 % (2951990)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.36/0.52 % (2951990)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4086445231:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.36/0.52 % (2951987)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3014650740:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.36/0.52 % (2951988)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2639637346:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.36/0.52 % (2951987)Instruction limit reached!
% 1.36/0.52 % (2951987)------------------------------
% 1.36/0.52 % (2951987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.52 % (2951987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.52 % (2951987)CaDiCaL version: 2.1.3
% 1.36/0.52 % (2951987)Termination reason: Instruction limit
% 1.36/0.52 % (2951987)Termination phase: Saturation
% 1.36/0.52 % (2951987)Time elapsed: 0.007 s
% 1.36/0.52 % (2951987)Peak memory usage: 11 MB
% 1.36/0.52 % (2951987)Instructions burned: 8 (million)
% 1.36/0.52 % (2951990)Instruction limit reached!
% 1.36/0.52 % (2951990)------------------------------
% 1.36/0.52 % (2951990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.52 % (2951990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.52 % (2951990)CaDiCaL version: 2.1.3
% 1.36/0.52 % (2951990)Termination reason: Instruction limit
% 1.36/0.52 % (2951990)Termination phase: Saturation
% 1.36/0.52 % (2951990)Time elapsed: 0.014 s
% 1.36/0.52 % (2951990)Peak memory usage: 11 MB
% 1.36/0.52 % (2951990)Instructions burned: 31 (million)
% 1.36/0.52 % (2951975)Instruction limit reached!
% 1.36/0.52 % (2951975)------------------------------
% 1.36/0.52 % (2951975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.52 % (2951975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.52 % (2951975)CaDiCaL version: 2.1.3
% 1.36/0.52 % (2951975)Termination reason: Instruction limit
% 1.36/0.52 % (2951975)Termination phase: Saturation
% 1.36/0.52 % (2951975)Time elapsed: 0.069 s
% 1.36/0.52 % (2951975)Peak memory usage: 12 MB
% 1.36/0.52 % (2951975)Instructions burned: 76 (million)
% 1.36/0.52 % (2951988)Instruction limit reached!
% 1.36/0.52 % (2951988)------------------------------
% 1.36/0.52 % (2951988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.52 % (2951988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.52 % (2951988)CaDiCaL version: 2.1.3
% 1.36/0.52 % (2951988)Termination reason: Instruction limit
% 1.36/0.52 % (2951988)Termination phase: Saturation
% 1.36/0.52 % (2951988)Time elapsed: 0.014 s
% 1.36/0.52 % (2951988)Peak memory usage: 12 MB
% 1.36/0.52 % (2951988)Instructions burned: 12 (million)
% 1.36/0.52 % (2951994)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=2921305744:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.36/0.52 % (2951970)Instruction limit reached!
% 1.36/0.52 % (2951970)------------------------------
% 1.36/0.52 % (2951970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.57 % (2951970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.57 % (2951970)CaDiCaL version: 2.1.3
% 1.36/0.57 % (2951970)Termination reason: Instruction limit
% 1.36/0.57 % (2951970)Termination phase: Saturation
% 1.36/0.57 % (2951970)Time elapsed: 0.084 s
% 1.36/0.57 % (2951970)Peak memory usage: 13 MB
% 1.36/0.57 % (2951970)Instructions burned: 88 (million)
% 1.36/0.57 % (2951996)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.36/0.57 % (2951996)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=454899774:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.36/0.57 % (2951996)Instruction limit reached!
% 1.36/0.57 % (2951996)------------------------------
% 1.36/0.57 % (2951996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.57 % (2951996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.57 % (2951996)CaDiCaL version: 2.1.3
% 1.36/0.57 % (2951996)Termination reason: Instruction limit
% 1.36/0.57 % (2951996)Termination phase: Saturation
% 1.36/0.57 % (2951996)Time elapsed: 0.001 s
% 1.36/0.57 % (2951996)Peak memory usage: 11 MB
% 1.36/0.57 % (2951996)Instructions burned: 2 (million)
% 1.36/0.57 % (2951995)lrs+10_1_si=on:cs=on:random_seed=3898078144:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.36/0.57 % (2951997)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4169201966:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.36/0.57 % (2951995)Instruction limit reached!
% 1.36/0.57 % (2951995)------------------------------
% 1.36/0.57 % (2951995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.57 % (2951995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.57 % (2951995)CaDiCaL version: 2.1.3
% 1.36/0.57 % (2951995)Termination reason: Instruction limit
% 1.36/0.57 % (2951995)Termination phase: Saturation
% 1.36/0.57 % (2951995)Time elapsed: 0.009 s
% 1.36/0.57 % (2951995)Peak memory usage: 12 MB
% 1.36/0.57 % (2951995)Instructions burned: 8 (million)
% 1.36/0.57 % (2951997)Refutation not found, incomplete strategy
% 1.36/0.57 % (2951997)------------------------------
% 1.36/0.57 % (2951997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.57 % (2951997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.57 % (2951997)CaDiCaL version: 2.1.3
% 1.36/0.57 % (2951997)Termination reason: Refutation not found, incomplete strategy
% 1.36/0.57 % (2951997)Time elapsed: 0.010 s
% 1.36/0.57 % (2951997)Peak memory usage: 12 MB
% 1.36/0.57 % (2951997)Instructions burned: 8 (million)
% 1.36/0.57 % (2951997)------------------------------
% 1.36/0.57 % (2951997)------------------------------
% 1.36/0.57 % (2951999)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1469646722:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.36/0.57 % (2952001)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1843836000:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.36/0.57 % (2951999)Refutation not found, incomplete strategy
% 1.36/0.57 % (2951999)------------------------------
% 1.36/0.57 % (2951999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.57 % (2951999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.57 % (2951999)CaDiCaL version: 2.1.3
% 1.36/0.57 % (2951999)Termination reason: Refutation not found, incomplete strategy
% 1.36/0.57 % (2951999)Time elapsed: 0.007 s
% 1.36/0.57 % (2951999)Peak memory usage: 12 MB
% 1.36/0.57 % (2951999)Instructions burned: 6 (million)
% 1.36/0.57 % (2951999)------------------------------
% 1.36/0.57 % (2951999)------------------------------
% 1.36/0.57 % (2951994)Instruction limit reached!
% 1.36/0.57 % (2951994)------------------------------
% 1.36/0.57 % (2951994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.36/0.57 % (2951994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.36/0.57 % (2951994)CaDiCaL version: 2.1.3
% 1.36/0.57 % (2951994)Termination reason: Instruction limit
% 1.36/0.57 % (2951994)Termination phase: Saturation
% 1.36/0.57 % (2951994)Time elapsed: 0.049 s
% 1.36/0.57 % (2951994)Peak memory usage: 12 MB
% 2.31/0.64 % (2951994)Instructions burned: 87 (million)
% 2.31/0.64 % (2951976)Instruction limit reached!
% 2.31/0.64 % (2951976)------------------------------
% 2.31/0.64 % (2951976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (2951976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (2951976)CaDiCaL version: 2.1.3
% 2.31/0.64 % (2951976)Termination reason: Instruction limit
% 2.31/0.64 % (2951976)Termination phase: Saturation
% 2.31/0.64 % (2951976)Time elapsed: 0.133 s
% 2.31/0.64 % (2951976)Peak memory usage: 12 MB
% 2.31/0.64 % (2951976)Instructions burned: 158 (million)
% 2.31/0.64 % (2952004)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3698588872:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.31/0.64 % (2952001)Instruction limit reached!
% 2.31/0.64 % (2952001)------------------------------
% 2.31/0.64 % (2952001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (2952001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (2952001)CaDiCaL version: 2.1.3
% 2.31/0.64 % (2952001)Termination reason: Instruction limit
% 2.31/0.64 % (2952001)Termination phase: Saturation
% 2.31/0.64 % (2952001)Time elapsed: 0.023 s
% 2.31/0.64 % (2952001)Peak memory usage: 12 MB
% 2.31/0.64 % (2952001)Instructions burned: 25 (million)
% 2.31/0.64 % (2952009)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=209200016:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.31/0.64 % (2952006)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3217335502:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.31/0.64 % (2952009)Instruction limit reached!
% 2.31/0.64 % (2952009)------------------------------
% 2.31/0.64 % (2952009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (2952009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (2952009)CaDiCaL version: 2.1.3
% 2.31/0.64 % (2952009)Termination reason: Instruction limit
% 2.31/0.64 % (2952009)Termination phase: Property scanning
% 2.31/0.64 % (2952009)Time elapsed: 0.001 s
% 2.31/0.64 % (2952009)Peak memory usage: 10 MB
% 2.31/0.64 % (2952009)Instructions burned: 2 (million)
% 2.31/0.64 % (2952010)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=441946920:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.31/0.64 % (2952008)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2244266512:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.31/0.64 % (2952004)Instruction limit reached!
% 2.31/0.64 % (2952004)------------------------------
% 2.31/0.64 % (2952004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (2952004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (2952004)CaDiCaL version: 2.1.3
% 2.31/0.64 % (2952004)Termination reason: Instruction limit
% 2.31/0.64 % (2952004)Termination phase: Saturation
% 2.31/0.64 % (2952004)Time elapsed: 0.016 s
% 2.31/0.64 % (2952004)Peak memory usage: 12 MB
% 2.31/0.64 % (2952004)Instructions burned: 14 (million)
% 2.31/0.64 % (2952015)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3827606768:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.31/0.64 % (2952008)Instruction limit reached!
% 2.31/0.64 % (2952008)------------------------------
% 2.31/0.64 % (2952008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.64 % (2952008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.64 % (2952008)CaDiCaL version: 2.1.3
% 2.31/0.64 % (2952008)Termination reason: Instruction limit
% 2.31/0.64 % (2952008)Termination phase: Saturation
% 2.31/0.64 % (2952008)Time elapsed: 0.015 s
% 2.31/0.64 % (2952008)Peak memory usage: 12 MB
% 2.31/0.64 % (2952008)Instructions burned: 14 (million)
% 2.31/0.64 % (2952012)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1836910501:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.31/0.64 % (2952018)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.57/0.79 % (2952018)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.57/0.79 % (2952010)Instruction limit reached!
% 2.57/0.79 % (2952010)------------------------------
% 2.57/0.79 % (2952010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.79 % (2952010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.79 % (2952010)CaDiCaL version: 2.1.3
% 2.57/0.79 % (2952010)Termination reason: Instruction limit
% 2.57/0.79 % (2952010)Termination phase: Saturation
% 2.57/0.79 % (2952010)Time elapsed: 0.022 s
% 2.57/0.79 % (2952010)Peak memory usage: 12 MB
% 2.57/0.79 % (2952010)Instructions burned: 27 (million)
% 2.57/0.79 % (2952018)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=3183648241:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.57/0.79 % (2952018)Instruction limit reached!
% 2.57/0.79 % (2952018)------------------------------
% 2.57/0.79 % (2952018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.79 % (2952018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.79 % (2952018)CaDiCaL version: 2.1.3
% 2.57/0.79 % (2952018)Termination reason: Instruction limit
% 2.57/0.79 % (2952018)Termination phase: Saturation
% 2.57/0.79 % (2952018)Time elapsed: 0.010 s
% 2.57/0.79 % (2952018)Peak memory usage: 12 MB
% 2.57/0.79 % (2952018)Instructions burned: 14 (million)
% 2.57/0.79 % (2952015)Instruction limit reached!
% 2.57/0.79 % (2952015)------------------------------
% 2.57/0.79 % (2952015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.79 % (2952015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.79 % (2952015)CaDiCaL version: 2.1.3
% 2.57/0.79 % (2952015)Termination reason: Instruction limit
% 2.57/0.79 % (2952015)Termination phase: Saturation
% 2.57/0.79 % (2952015)Time elapsed: 0.029 s
% 2.57/0.79 % (2952015)Peak memory usage: 12 MB
% 2.57/0.79 % (2952015)Instructions burned: 60 (million)
% 2.57/0.79 % (2952012)Instruction limit reached!
% 2.57/0.79 % (2952012)------------------------------
% 2.57/0.79 % (2952012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.79 % (2952012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.79 % (2952012)CaDiCaL version: 2.1.3
% 2.57/0.79 % (2952012)Termination reason: Instruction limit
% 2.57/0.79 % (2952012)Termination phase: Saturation
% 2.57/0.79 % (2952012)Time elapsed: 0.022 s
% 2.57/0.79 % (2952012)Peak memory usage: 11 MB
% 2.57/0.79 % (2952012)Instructions burned: 23 (million)
% 2.57/0.79 % (2952021)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.57/0.79 % (2952021)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=2626873967:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.57/0.79 % (2952022)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=2915375614:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.57/0.79 % (2952025)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1973505290:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.57/0.79 % (2952024)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2900269025:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.57/0.79 % (2952021)Instruction limit reached!
% 2.57/0.79 % (2952021)------------------------------
% 2.57/0.79 % (2952021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.79 % (2952021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.79 % (2952021)CaDiCaL version: 2.1.3
% 2.57/0.79 % (2952021)Termination reason: Instruction limit
% 2.57/0.79 % (2952021)Termination phase: Saturation
% 2.57/0.79 % (2952021)Time elapsed: 0.009 s
% 2.57/0.79 % (2952021)Peak memory usage: 12 MB
% 2.57/0.79 % (2952021)Instructions burned: 8 (million)
% 2.57/0.79 % (2952025)Instruction limit reached!
% 2.57/0.79 % (2952025)------------------------------
% 2.57/0.79 % (2952025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.87 % (2952025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.87 % (2952025)CaDiCaL version: 2.1.3
% 3.04/0.87 % (2952025)Termination reason: Instruction limit
% 3.04/0.87 % (2952025)Termination phase: Saturation
% 3.04/0.87 % (2952025)Time elapsed: 0.012 s
% 3.04/0.87 % (2952025)Peak memory usage: 11 MB
% 3.04/0.87 % (2952025)Instructions burned: 30 (million)
% 3.04/0.87 % (2952024)Instruction limit reached!
% 3.04/0.87 % (2952024)------------------------------
% 3.04/0.87 % (2952024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.87 % (2952024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.87 % (2952024)CaDiCaL version: 2.1.3
% 3.04/0.87 % (2952024)Termination reason: Instruction limit
% 3.04/0.87 % (2952024)Termination phase: Saturation
% 3.04/0.87 % (2952024)Time elapsed: 0.008 s
% 3.04/0.87 % (2952024)Peak memory usage: 12 MB
% 3.04/0.87 % (2952024)Instructions burned: 8 (million)
% 3.04/0.87 % (2952026)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=446991705:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.04/0.87 % (2952022)Instruction limit reached!
% 3.04/0.87 % (2952022)------------------------------
% 3.04/0.87 % (2952022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.87 % (2952022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.87 % (2952022)CaDiCaL version: 2.1.3
% 3.04/0.87 % (2952022)Termination reason: Instruction limit
% 3.04/0.87 % (2952022)Termination phase: Saturation
% 3.04/0.87 % (2952022)Time elapsed: 0.028 s
% 3.04/0.87 % (2952022)Peak memory usage: 12 MB
% 3.04/0.87 % (2952022)Instructions burned: 31 (million)
% 3.04/0.87 % (2952032)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3390070114:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 3.04/0.87 % (2952031)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1096846433:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.04/0.87 % (2952026)Instruction limit reached!
% 3.04/0.87 % (2952026)------------------------------
% 3.04/0.87 % (2952026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.87 % (2952026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.87 % (2952026)CaDiCaL version: 2.1.3
% 3.04/0.87 % (2952026)Termination reason: Instruction limit
% 3.04/0.87 % (2952026)Termination phase: Saturation
% 3.04/0.87 % (2952026)Time elapsed: 0.021 s
% 3.04/0.87 % (2952026)Peak memory usage: 13 MB
% 3.04/0.87 % (2952026)Instructions burned: 20 (million)
% 3.04/0.87 % (2952035)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=580697467:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 3.04/0.87 % (2952033)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3761482874:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 3.04/0.87 % (2952038)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.04/0.87 % (2952035)Instruction limit reached!
% 3.04/0.87 % (2952035)------------------------------
% 3.04/0.87 % (2952035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.87 % (2952035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.87 % (2952035)CaDiCaL version: 2.1.3
% 3.04/0.87 % (2952035)Termination reason: Instruction limit
% 3.04/0.87 % (2952035)Termination phase: Saturation
% 3.04/0.87 % (2952035)Time elapsed: 0.027 s
% 3.04/0.87 % (2952035)Peak memory usage: 12 MB
% 3.04/0.87 % (2952035)Instructions burned: 43 (million)
% 3.04/0.87 % (2952038)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3425308706:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 3.04/0.87 % (2952038)Instruction limit reached!
% 3.04/0.87 % (2952038)------------------------------
% 3.04/0.87 % (2952038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.87 % (2952038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.87 % (2952038)CaDiCaL version: 2.1.3
% 3.04/0.87 % (2952038)Termination reason: Instruction limit
% 3.04/0.87 % (2952038)Termination phase: Saturation
% 3.04/0.87 % (2952038)Time elapsed: 0.007 s
% 3.04/0.87 % (2952038)Peak memory usage: 12 MB
% 3.64/0.99 % (2952038)Instructions burned: 7 (million)
% 3.64/0.99 % (2952032)Instruction limit reached!
% 3.64/0.99 % (2952032)------------------------------
% 3.64/0.99 % (2952032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.99 % (2952032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.99 % (2952032)CaDiCaL version: 2.1.3
% 3.64/0.99 % (2952032)Termination reason: Instruction limit
% 3.64/0.99 % (2952032)Termination phase: Saturation
% 3.64/0.99 % (2952032)Time elapsed: 0.069 s
% 3.64/0.99 % (2952032)Peak memory usage: 13 MB
% 3.64/0.99 % (2952032)Instructions burned: 144 (million)
% 3.64/0.99 % (2952043)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=2693380834:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.64/0.99 % (2952042)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3652015357:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.64/0.99 % (2952044)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.64/0.99 % (2952044)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3805477987:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.64/0.99 % (2952044)Instruction limit reached!
% 3.64/0.99 % (2952044)------------------------------
% 3.64/0.99 % (2952044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.99 % (2952044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.99 % (2952044)CaDiCaL version: 2.1.3
% 3.64/0.99 % (2952044)Termination reason: Instruction limit
% 3.64/0.99 % (2952044)Termination phase: Saturation
% 3.64/0.99 % (2952044)Time elapsed: 0.003 s
% 3.64/0.99 % (2952044)Peak memory usage: 12 MB
% 3.64/0.99 % (2952044)Instructions burned: 6 (million)
% 3.64/0.99 % (2952048)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1353558911:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.64/0.99 % (2952048)Instruction limit reached!
% 3.64/0.99 % (2952048)------------------------------
% 3.64/0.99 % (2952048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.99 % (2952048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.99 % (2952048)CaDiCaL version: 2.1.3
% 3.64/0.99 % (2952048)Termination reason: Instruction limit
% 3.64/0.99 % (2952048)Termination phase: Saturation
% 3.64/0.99 % (2952048)Time elapsed: 0.011 s
% 3.64/0.99 % (2952048)Peak memory usage: 12 MB
% 3.64/0.99 % (2952048)Instructions burned: 24 (million)
% 3.64/0.99 % (2952050)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3086092063:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.64/0.99 % (2952050)Instruction limit reached!
% 3.64/0.99 % (2952050)------------------------------
% 3.64/0.99 % (2952050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.99 % (2952050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.99 % (2952050)CaDiCaL version: 2.1.3
% 3.64/0.99 % (2952050)Termination reason: Instruction limit
% 3.64/0.99 % (2952050)Termination phase: Saturation
% 3.64/0.99 % (2952050)Time elapsed: 0.012 s
% 3.64/0.99 % (2952050)Peak memory usage: 13 MB
% 3.64/0.99 % (2952050)Instructions burned: 19 (million)
% 3.64/0.99 % (2952052)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=3066125838:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 3.64/0.99 % (2952033)Instruction limit reached!
% 3.64/0.99 % (2952033)------------------------------
% 3.64/0.99 % (2952033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.99 % (2952033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.99 % (2952033)CaDiCaL version: 2.1.3
% 3.64/0.99 % (2952033)Termination reason: Instruction limit
% 3.64/0.99 % (2952033)Termination phase: Saturation
% 3.64/0.99 % (2952033)Time elapsed: 0.165 s
% 3.64/0.99 % (2952033)Peak memory usage: 13 MB
% 3.64/0.99 % (2952033)Instructions burned: 193 (million)
% 3.64/0.99 % (2952006)Instruction limit reached!
% 3.64/0.99 % (2952006)------------------------------
% 5.63/1.17 % (2952006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.17 % (2952006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.17 % (2952006)CaDiCaL version: 2.1.3
% 5.63/1.17 % (2952006)Termination reason: Instruction limit
% 5.63/1.17 % (2952006)Termination phase: Saturation
% 5.63/1.17 % (2952006)Time elapsed: 0.293 s
% 5.63/1.17 % (2952006)Peak memory usage: 14 MB
% 5.63/1.17 % (2952006)Instructions burned: 327 (million)
% 5.63/1.17 % (2952054)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=746463575:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.63/1.17 % (2952043)Instruction limit reached!
% 5.63/1.17 % (2952043)------------------------------
% 5.63/1.17 % (2952043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.17 % (2952043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.17 % (2952043)CaDiCaL version: 2.1.3
% 5.63/1.17 % (2952043)Termination reason: Instruction limit
% 5.63/1.17 % (2952043)Termination phase: Saturation
% 5.63/1.17 % (2952043)Time elapsed: 0.147 s
% 5.63/1.17 % (2952043)Peak memory usage: 14 MB
% 5.63/1.17 % (2952043)Instructions burned: 169 (million)
% 5.63/1.17 % (2952055)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=969648129:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 5.63/1.17 % (2951973)Instruction limit reached!
% 5.63/1.17 % (2951973)------------------------------
% 5.63/1.17 % (2951973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.17 % (2951973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.17 % (2951973)CaDiCaL version: 2.1.3
% 5.63/1.17 % (2951973)Termination reason: Instruction limit
% 5.63/1.17 % (2951973)Termination phase: Saturation
% 5.63/1.17 % (2951973)Time elapsed: 0.483 s
% 5.63/1.17 % (2951973)Peak memory usage: 14 MB
% 5.63/1.17 % (2951973)Instructions burned: 634 (million)
% 5.63/1.17 % (2952057)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1793287647:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 5.63/1.17 % (2952042)Instruction limit reached!
% 5.63/1.17 % (2952042)------------------------------
% 5.63/1.17 % (2952042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.17 % (2952042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.17 % (2952042)CaDiCaL version: 2.1.3
% 5.63/1.17 % (2952042)Termination reason: Instruction limit
% 5.63/1.17 % (2952042)Termination phase: Saturation
% 5.63/1.17 % (2952042)Time elapsed: 0.164 s
% 5.63/1.17 % (2952042)Peak memory usage: 13 MB
% 5.63/1.17 % (2952042)Instructions burned: 181 (million)
% 5.63/1.17 % (2952057)Refutation not found, incomplete strategy
% 5.63/1.17 % (2952057)------------------------------
% 5.63/1.17 % (2952057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.17 % (2952057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.17 % (2952057)CaDiCaL version: 2.1.3
% 5.63/1.18 % (2952057)Termination reason: Refutation not found, incomplete strategy
% 5.63/1.18 % (2952057)Time elapsed: 0.005 s
% 5.63/1.18 % (2952057)Peak memory usage: 12 MB
% 5.63/1.18 % (2952057)Instructions burned: 6 (million)
% 5.63/1.18 % (2952057)------------------------------
% 5.63/1.18 % (2952057)------------------------------
% 5.63/1.18 % (2952062)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3564376537:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 5.63/1.18 % (2952059)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2341987954:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.63/1.18 % (2952061)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.63/1.18 % (2952061)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=853557377:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 5.63/1.18 % (2952055)Instruction limit reached!
% 6.56/1.31 % (2952055)------------------------------
% 6.56/1.31 % (2952055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.56/1.31 % (2952055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.56/1.31 % (2952055)CaDiCaL version: 2.1.3
% 6.56/1.31 % (2952055)Termination reason: Instruction limit
% 6.56/1.31 % (2952055)Termination phase: Saturation
% 6.56/1.31 % (2952055)Time elapsed: 0.047 s
% 6.56/1.31 % (2952055)Peak memory usage: 12 MB
% 6.56/1.31 % (2952055)Instructions burned: 45 (million)
% 6.56/1.31 % (2952062)Instruction limit reached!
% 6.56/1.31 % (2952062)------------------------------
% 6.56/1.31 % (2952062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.56/1.31 % (2952062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.56/1.31 % (2952062)CaDiCaL version: 2.1.3
% 6.56/1.31 % (2952062)Termination reason: Instruction limit
% 6.56/1.31 % (2952062)Termination phase: Saturation
% 6.56/1.31 % (2952062)Time elapsed: 0.010 s
% 6.56/1.31 % (2952062)Peak memory usage: 12 MB
% 6.56/1.31 % (2952062)Instructions burned: 14 (million)
% 6.56/1.31 % (2952059)Instruction limit reached!
% 6.56/1.31 % (2952059)------------------------------
% 6.56/1.31 % (2952059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.56/1.31 % (2952059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.56/1.31 % (2952059)CaDiCaL version: 2.1.3
% 6.56/1.31 % (2952059)Termination reason: Instruction limit
% 6.56/1.31 % (2952059)Termination phase: Saturation
% 6.56/1.31 % (2952059)Time elapsed: 0.023 s
% 6.56/1.31 % (2952059)Peak memory usage: 12 MB
% 6.56/1.31 % (2952059)Instructions burned: 22 (million)
% 6.56/1.31 % (2952066)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=103910378:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 6.56/1.31 % (2952067)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=729727744:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 6.56/1.31 % (2952068)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=246088751:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/31Mi)
% 6.56/1.31 % (2952068)Instruction limit reached!
% 6.56/1.31 % (2952068)------------------------------
% 6.56/1.31 % (2952068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.56/1.31 % (2952068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.56/1.31 % (2952068)CaDiCaL version: 2.1.3
% 6.56/1.31 % (2952068)Termination reason: Instruction limit
% 6.56/1.31 % (2952068)Termination phase: Saturation
% 6.56/1.31 % (2952068)Time elapsed: 0.027 s
% 6.56/1.31 % (2952068)Peak memory usage: 12 MB
% 6.56/1.31 % (2952068)Instructions burned: 31 (million)
% 6.56/1.31 % (2952067)Instruction limit reached!
% 6.56/1.31 % (2952067)------------------------------
% 6.56/1.31 % (2952067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.56/1.31 % (2952067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.56/1.31 % (2952067)CaDiCaL version: 2.1.3
% 6.56/1.31 % (2952067)Termination reason: Instruction limit
% 6.56/1.31 % (2952067)Termination phase: Saturation
% 6.56/1.31 % (2952067)Time elapsed: 0.049 s
% 6.56/1.31 % (2952067)Peak memory usage: 12 MB
% 6.56/1.31 % (2952067)Instructions burned: 51 (million)
% 6.56/1.31 % (2952066)Instruction limit reached!
% 6.56/1.31 % (2952066)------------------------------
% 6.56/1.31 % (2952066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.56/1.31 % (2952066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.56/1.31 % (2952066)CaDiCaL version: 2.1.3
% 6.56/1.31 % (2952066)Termination reason: Instruction limit
% 6.56/1.31 % (2952066)Termination phase: Saturation
% 6.56/1.31 % (2952066)Time elapsed: 0.066 s
% 6.56/1.31 % (2952066)Peak memory usage: 13 MB
% 6.56/1.31 % (2952066)Instructions burned: 69 (million)
% 6.56/1.31 % (2952072)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=746413939:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.56/1.31 % (2952073)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=1743585226:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 6.56/1.31 % (2952074)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=365518128:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 6.87/1.48 % (2952073)Instruction limit reached!
% 6.87/1.48 % (2952073)------------------------------
% 6.87/1.48 % (2952073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.48 % (2952073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.48 % (2952073)CaDiCaL version: 2.1.3
% 6.87/1.48 % (2952073)Termination reason: Instruction limit
% 6.87/1.48 % (2952073)Termination phase: Saturation
% 6.87/1.48 % (2952073)Time elapsed: 0.034 s
% 6.87/1.48 % (2952073)Peak memory usage: 12 MB
% 6.87/1.48 % (2952073)Instructions burned: 34 (million)
% 6.87/1.48 % (2952061)Instruction limit reached!
% 6.87/1.48 % (2952061)------------------------------
% 6.87/1.48 % (2952061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.48 % (2952061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.48 % (2952061)CaDiCaL version: 2.1.3
% 6.87/1.48 % (2952061)Termination reason: Instruction limit
% 6.87/1.48 % (2952061)Termination phase: Saturation
% 6.87/1.48 % (2952061)Time elapsed: 0.170 s
% 6.87/1.48 % (2952061)Peak memory usage: 13 MB
% 6.87/1.48 % (2952061)Instructions burned: 200 (million)
% 6.87/1.48 % (2952052)Instruction limit reached!
% 6.87/1.48 % (2952052)------------------------------
% 6.87/1.48 % (2952052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.48 % (2952052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.48 % (2952052)CaDiCaL version: 2.1.3
% 6.87/1.48 % (2952052)Termination reason: Instruction limit
% 6.87/1.48 % (2952052)Termination phase: Saturation
% 6.87/1.48 % (2952052)Time elapsed: 0.281 s
% 6.87/1.48 % (2952052)Peak memory usage: 14 MB
% 6.87/1.48 % (2952052)Instructions burned: 316 (million)
% 6.87/1.48 % (2952078)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.87/1.48 % (2952074)Instruction limit reached!
% 6.87/1.48 % (2952074)------------------------------
% 6.87/1.48 % (2952074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.48 % (2952074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.48 % (2952074)CaDiCaL version: 2.1.3
% 6.87/1.48 % (2952074)Termination reason: Instruction limit
% 6.87/1.48 % (2952074)Termination phase: Saturation
% 6.87/1.48 % (2952074)Time elapsed: 0.062 s
% 6.87/1.48 % (2952074)Peak memory usage: 12 MB
% 6.87/1.48 % (2952074)Instructions burned: 67 (million)
% 6.87/1.48 % (2952078)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2584832121:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 6.87/1.48 % (2952079)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=680131740:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 6.87/1.48 % (2952080)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3491194968:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 6.87/1.48 % (2952081)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3043364629:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 6.87/1.48 % (2952072)Instruction limit reached!
% 6.87/1.48 % (2952072)------------------------------
% 6.87/1.48 % (2952072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.48 % (2952072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.48 % (2952072)CaDiCaL version: 2.1.3
% 6.87/1.48 % (2952072)Termination reason: Instruction limit
% 6.87/1.48 % (2952072)Termination phase: Saturation
% 6.87/1.48 % (2952072)Time elapsed: 0.121 s
% 6.87/1.48 % (2952072)Peak memory usage: 13 MB
% 6.87/1.48 % (2952072)Instructions burned: 137 (million)
% 6.87/1.48 % (2952086)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3573211251:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/874Mi)
% 6.87/1.48 % (2952080)Instruction limit reached!
% 6.87/1.48 % (2952080)------------------------------
% 6.87/1.48 % (2952080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.87/1.48 % (2952080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.48 % (2952080)CaDiCaL version: 2.1.3
% 6.87/1.48 % (2952080)Termination reason: Instruction limit
% 6.87/1.48 % (2952080)Termination phase: Saturation
% 6.87/1.48 % (2952080)Time elapsed: 0.095 s
% 7.69/1.69 % (2952080)Peak memory usage: 13 MB
% 7.69/1.69 % (2952080)Instructions burned: 96 (million)
% 7.69/1.69 % (2952054)Instruction limit reached!
% 7.69/1.69 % (2952054)------------------------------
% 7.69/1.69 % (2952054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.69/1.69 % (2952054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/1.69 % (2952054)CaDiCaL version: 2.1.3
% 7.69/1.69 % (2952054)Termination reason: Instruction limit
% 7.69/1.69 % (2952054)Termination phase: Saturation
% 7.69/1.69 % (2952054)Time elapsed: 0.396 s
% 7.69/1.69 % (2952054)Peak memory usage: 16 MB
% 7.69/1.69 % (2952054)Instructions burned: 854 (million)
% 7.69/1.69 % (2952078)Instruction limit reached!
% 7.69/1.69 % (2952078)------------------------------
% 7.69/1.69 % (2952078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.69/1.69 % (2952078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/1.69 % (2952078)CaDiCaL version: 2.1.3
% 7.69/1.69 % (2952078)Termination reason: Instruction limit
% 7.69/1.69 % (2952078)Termination phase: Saturation
% 7.69/1.69 % (2952078)Time elapsed: 0.146 s
% 7.69/1.69 % (2952078)Peak memory usage: 14 MB
% 7.69/1.69 % (2952078)Instructions burned: 180 (million)
% 7.69/1.69 % (2952088)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=988422771:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/515Mi)
% 7.69/1.69 % (2952089)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2152018583:st=1.5:i=130:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 7.69/1.69 % (2952090)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1901154128:i=44:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/44Mi)
% 7.69/1.69 % (2952089)Instruction limit reached!
% 7.69/1.69 % (2952089)------------------------------
% 7.69/1.69 % (2952089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.69/1.69 % (2952089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/1.69 % (2952089)CaDiCaL version: 2.1.3
% 7.69/1.69 % (2952089)Termination reason: Instruction limit
% 7.69/1.69 % (2952089)Termination phase: Saturation
% 7.69/1.69 % (2952089)Time elapsed: 0.061 s
% 7.69/1.69 % (2952089)Peak memory usage: 12 MB
% 7.69/1.69 % (2952089)Instructions burned: 131 (million)
% 7.69/1.69 % (2952079)Instruction limit reached!
% 7.69/1.69 % (2952079)------------------------------
% 7.69/1.69 % (2952079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.69/1.69 % (2952079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/1.69 % (2952079)CaDiCaL version: 2.1.3
% 7.69/1.69 % (2952079)Termination reason: Instruction limit
% 7.69/1.69 % (2952079)Termination phase: Saturation
% 7.69/1.69 % (2952079)Time elapsed: 0.205 s
% 7.69/1.69 % (2952079)Peak memory usage: 13 MB
% 7.69/1.69 % (2952079)Instructions burned: 246 (million)
% 7.69/1.69 % (2952090)Instruction limit reached!
% 7.69/1.69 % (2952090)------------------------------
% 7.69/1.69 % (2952090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.69/1.69 % (2952090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/1.69 % (2952090)CaDiCaL version: 2.1.3
% 7.69/1.69 % (2952090)Termination reason: Instruction limit
% 7.69/1.69 % (2952090)Termination phase: Saturation
% 7.69/1.69 % (2952090)Time elapsed: 0.039 s
% 7.69/1.69 % (2952090)Peak memory usage: 12 MB
% 7.69/1.69 % (2952090)Instructions burned: 45 (million)
% 7.69/1.69 % (2952095)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=787040218:i=450:rtra=on:ixr=off:ntd=on_2990 on theBenchmark for (2990ds/450Mi)
% 7.69/1.69 % (2952096)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3159200736:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/95Mi)
% 7.69/1.69 % (2952094)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=572601041:s2a=on:i=571:nm=16:rtra=on_2990 on theBenchmark for (2990ds/571Mi)
% 7.69/1.69 % (2952095)Refutation not found, incomplete strategy
% 7.69/1.69 % (2952095)------------------------------
% 7.69/1.69 % (2952095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.69/1.69 % (2952095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/1.69 % (2952095)CaDiCaL version: 2.1.3
% 7.69/1.69 % (2952095)Termination reason: Refutation not found, incomplete strategy
% 9.68/1.95 % (2952095)Time elapsed: 0.010 s
% 9.68/1.95 % (2952095)Peak memory usage: 12 MB
% 9.68/1.95 % (2952095)Instructions burned: 17 (million)
% 9.68/1.95 % (2952095)------------------------------
% 9.68/1.95 % (2952095)------------------------------
% 9.68/1.95 % (2952094)Refutation not found, incomplete strategy
% 9.68/1.95 % (2952094)------------------------------
% 9.68/1.95 % (2952094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.68/1.95 % (2952094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/1.95 % (2952094)CaDiCaL version: 2.1.3
% 9.68/1.95 % (2952094)Termination reason: Refutation not found, incomplete strategy
% 9.68/1.95 % (2952094)Time elapsed: 0.012 s
% 9.68/1.95 % (2952094)Peak memory usage: 12 MB
% 9.68/1.95 % (2952094)Instructions burned: 10 (million)
% 9.68/1.95 % (2952094)------------------------------
% 9.68/1.95 % (2952094)------------------------------
% 9.68/1.95 % (2952100)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=693478932:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 9.68/1.95 % (2952101)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=958490768: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_2989 on theBenchmark for (2989ds/105Mi)
% 9.68/1.95 % (2952100)Instruction limit reached!
% 9.68/1.95 % (2952100)------------------------------
% 9.68/1.95 % (2952100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.68/1.95 % (2952100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/1.95 % (2952100)CaDiCaL version: 2.1.3
% 9.68/1.95 % (2952100)Termination reason: Instruction limit
% 9.68/1.95 % (2952100)Termination phase: Saturation
% 9.68/1.95 % (2952100)Time elapsed: 0.034 s
% 9.68/1.95 % (2952100)Peak memory usage: 12 MB
% 9.68/1.95 % (2952100)Instructions burned: 66 (million)
% 9.68/1.95 % (2952096)Instruction limit reached!
% 9.68/1.95 % (2952096)------------------------------
% 9.68/1.95 % (2952096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.68/1.95 % (2952096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/1.95 % (2952096)CaDiCaL version: 2.1.3
% 9.68/1.95 % (2952096)Termination reason: Instruction limit
% 9.68/1.95 % (2952096)Termination phase: Saturation
% 9.68/1.95 % (2952096)Time elapsed: 0.065 s
% 9.68/1.95 % (2952096)Peak memory usage: 13 MB
% 9.68/1.95 % (2952096)Instructions burned: 95 (million)
% 9.68/1.95 % (2952104)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=1210329744:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2989 on theBenchmark for (2989ds/5755Mi)
% 9.68/1.95 % (2952105)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1647313259:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/375Mi)
% 9.68/1.95 % (2952101)Instruction limit reached!
% 9.68/1.95 % (2952101)------------------------------
% 9.68/1.95 % (2952101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.68/1.95 % (2952101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/1.95 % (2952101)CaDiCaL version: 2.1.3
% 9.68/1.95 % (2952101)Termination reason: Instruction limit
% 9.68/1.95 % (2952101)Termination phase: Saturation
% 9.68/1.95 % (2952101)Time elapsed: 0.093 s
% 9.68/1.95 % (2952101)Peak memory usage: 13 MB
% 9.68/1.95 % (2952101)Instructions burned: 106 (million)
% 9.68/1.95 % (2952081)Instruction limit reached!
% 9.68/1.95 % (2952081)------------------------------
% 9.68/1.95 % (2952081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.68/1.95 % (2952081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/1.95 % (2952081)CaDiCaL version: 2.1.3
% 9.68/1.95 % (2952081)Termination reason: Instruction limit
% 9.68/1.95 % (2952081)Termination phase: Saturation
% 9.68/1.95 % (2952081)Time elapsed: 0.373 s
% 9.68/1.95 % (2952081)Peak memory usage: 14 MB
% 9.68/1.95 % (2952081)Instructions burned: 427 (million)
% 9.68/1.95 % (2952108)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=294266361:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2988 on theBenchmark for (2988ds/495Mi)
% 12.19/2.07 % (2952109)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=2448608378:cond=on:i=34:hud=10:nm=10:rtra=on_2988 on theBenchmark for (2988ds/34Mi)
% 12.19/2.07 % (2952109)Instruction limit reached!
% 12.19/2.07 % (2952109)------------------------------
% 12.19/2.07 % (2952109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.19/2.07 % (2952109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.19/2.07 % (2952109)CaDiCaL version: 2.1.3
% 12.19/2.07 % (2952109)Termination reason: Instruction limit
% 12.19/2.07 % (2952109)Termination phase: Saturation
% 12.19/2.07 % (2952109)Time elapsed: 0.039 s
% 12.19/2.07 % (2952109)Peak memory usage: 13 MB
% 12.19/2.07 % (2952109)Instructions burned: 35 (million)
% 12.19/2.07 % (2952112)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3659408007:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/91Mi)
% 12.19/2.07 % (2952031)Instruction limit reached!
% 12.19/2.07 % (2952031)------------------------------
% 12.19/2.07 % (2952031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.19/2.07 % (2952031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.19/2.07 % (2952031)CaDiCaL version: 2.1.3
% 12.19/2.07 % (2952031)Termination reason: Instruction limit
% 12.19/2.07 % (2952031)Termination phase: Saturation
% 12.19/2.07 % (2952031)Time elapsed: 0.990 s
% 12.19/2.07 % (2952031)Peak memory usage: 14 MB
% 12.19/2.07 % (2952031)Instructions burned: 1241 (million)
% 12.19/2.07 % (2952114)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=903033934:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2987 on theBenchmark for (2987ds/66Mi)
% 12.19/2.07 % (2952088)Instruction limit reached!
% 12.19/2.07 % (2952088)------------------------------
% 12.19/2.07 % (2952088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.19/2.07 % (2952088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.19/2.07 % (2952088)CaDiCaL version: 2.1.3
% 12.19/2.07 % (2952088)Termination reason: Instruction limit
% 12.19/2.07 % (2952088)Termination phase: Saturation
% 12.19/2.07 % (2952088)Time elapsed: 0.444 s
% 12.19/2.07 % (2952088)Peak memory usage: 15 MB
% 12.19/2.07 % (2952088)Instructions burned: 515 (million)
% 12.19/2.07 % (2952114)Instruction limit reached!
% 12.19/2.07 % (2952114)------------------------------
% 12.19/2.07 % (2952114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.19/2.07 % (2952114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.19/2.07 % (2952114)CaDiCaL version: 2.1.3
% 12.19/2.07 % (2952114)Termination reason: Instruction limit
% 12.19/2.07 % (2952114)Termination phase: Saturation
% 12.19/2.07 % (2952114)Time elapsed: 0.043 s
% 12.19/2.07 % (2952114)Peak memory usage: 12 MB
% 12.19/2.07 % (2952114)Instructions burned: 68 (million)
% 12.19/2.07 % (2952112)Instruction limit reached!
% 12.19/2.07 % (2952112)------------------------------
% 12.19/2.07 % (2952112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.19/2.07 % (2952112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.19/2.07 % (2952112)CaDiCaL version: 2.1.3
% 12.19/2.07 % (2952112)Termination reason: Instruction limit
% 12.19/2.07 % (2952112)Termination phase: Saturation
% 12.19/2.07 % (2952112)Time elapsed: 0.086 s
% 12.19/2.07 % (2952112)Peak memory usage: 12 MB
% 12.19/2.07 % (2952112)Instructions burned: 91 (million)
% 12.19/2.07 % (2952116)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=377750472:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2986 on theBenchmark for (2986ds/22Mi)
% 12.19/2.07 % (2952105)Instruction limit reached!
% 12.19/2.07 % (2952105)------------------------------
% 12.19/2.07 % (2952105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.19/2.07 % (2952105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.19/2.07 % (2952105)CaDiCaL version: 2.1.3
% 12.19/2.07 % (2952105)Termination reason: Instruction limit
% 12.19/2.07 % (2952105)Termination phase: Saturation
% 12.19/2.07 % (2952105)Time elapsed: 0.294 s
% 12.19/2.07 % (2952105)Peak memory usage: 15 MB
% 12.19/2.07 % (2952105)Instructions burned: 375 (million)
% 12.19/2.07 % (2952117)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=2085181956:i=338:bd=all:ins=4:rtra=on_2986 on theBenchmark for (2986ds/338Mi)
% 14.38/2.45 % (2952118)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1545274300:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/28Mi)
% 14.38/2.45 % (2952116)Instruction limit reached!
% 14.38/2.45 % (2952116)------------------------------
% 14.38/2.45 % (2952116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.38/2.45 % (2952116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/2.45 % (2952116)CaDiCaL version: 2.1.3
% 14.38/2.45 % (2952116)Termination reason: Instruction limit
% 14.38/2.45 % (2952116)Termination phase: Saturation
% 14.38/2.45 % (2952116)Time elapsed: 0.020 s
% 14.38/2.45 % (2952116)Peak memory usage: 12 MB
% 14.38/2.45 % (2952116)Instructions burned: 22 (million)
% 14.38/2.45 % (2952120)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 14.38/2.45 % (2952120)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=686821473:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2986 on theBenchmark for (2986ds/137Mi)
% 14.38/2.45 % (2952118)Instruction limit reached!
% 14.38/2.45 % (2952118)------------------------------
% 14.38/2.45 % (2952118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.38/2.45 % (2952118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/2.45 % (2952118)CaDiCaL version: 2.1.3
% 14.38/2.45 % (2952118)Termination reason: Instruction limit
% 14.38/2.45 % (2952118)Termination phase: Saturation
% 14.38/2.45 % (2952118)Time elapsed: 0.028 s
% 14.38/2.45 % (2952118)Peak memory usage: 13 MB
% 14.38/2.45 % (2952118)Instructions burned: 29 (million)
% 14.38/2.45 % (2952123)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=372129940:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2986 on theBenchmark for (2986ds/340Mi)
% 14.38/2.45 % (2952125)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2693381819:i=227:sd=1:bd=all:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/227Mi)
% 14.38/2.45 % (2952120)Instruction limit reached!
% 14.38/2.45 % (2952120)------------------------------
% 14.38/2.45 % (2952120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.38/2.45 % (2952120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/2.45 % (2952120)CaDiCaL version: 2.1.3
% 14.38/2.45 % (2952120)Termination reason: Instruction limit
% 14.38/2.45 % (2952120)Termination phase: Saturation
% 14.38/2.45 % (2952120)Time elapsed: 0.072 s
% 14.38/2.45 % (2952120)Peak memory usage: 12 MB
% 14.38/2.45 % (2952120)Instructions burned: 139 (million)
% 14.38/2.45 % (2952128)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 14.38/2.45 % (2952128)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3445723208:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/373Mi)
% 14.38/2.45 % (2952086)Instruction limit reached!
% 14.38/2.45 % (2952086)------------------------------
% 14.38/2.45 % (2952086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.38/2.45 % (2952086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/2.45 % (2952086)CaDiCaL version: 2.1.3
% 14.38/2.45 % (2952086)Termination reason: Instruction limit
% 14.38/2.45 % (2952086)Termination phase: Saturation
% 14.38/2.45 % (2952086)Time elapsed: 0.766 s
% 14.38/2.45 % (2952086)Peak memory usage: 16 MB
% 14.38/2.45 % (2952086)Instructions burned: 874 (million)
% 14.38/2.45 % (2952108)Instruction limit reached!
% 14.38/2.45 % (2952108)------------------------------
% 14.38/2.45 % (2952108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.38/2.45 % (2952108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.38/2.45 % (2952108)CaDiCaL version: 2.1.3
% 14.38/2.45 % (2952108)Termination reason: Instruction limit
% 14.38/2.45 % (2952108)Termination phase: Saturation
% 14.38/2.45 % (2952108)Time elapsed: 0.429 s
% 14.38/2.45 % (2952108)Peak memory usage: 15 MB
% 14.38/2.45 % (2952108)Instructions burned: 496 (million)
% 14.38/2.45 % (2952130)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=508008889:i=116:ep=RSTC:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/116Mi)
% 14.38/2.45 % (2952131)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3260952055:i=575:rtra=on_2983 on theBenchmark for (2983ds/575Mi)
% 16.19/2.83 % (2952125)Instruction limit reached!
% 16.19/2.83 % (2952125)------------------------------
% 16.19/2.83 % (2952125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.19/2.83 % (2952125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.19/2.83 % (2952125)CaDiCaL version: 2.1.3
% 16.19/2.83 % (2952125)Termination reason: Instruction limit
% 16.19/2.83 % (2952125)Termination phase: Saturation
% 16.19/2.83 % (2952125)Time elapsed: 0.207 s
% 16.19/2.83 % (2952125)Peak memory usage: 13 MB
% 16.19/2.83 % (2952125)Instructions burned: 228 (million)
% 16.19/2.83 % (2952128)Instruction limit reached!
% 16.19/2.83 % (2952128)------------------------------
% 16.19/2.83 % (2952128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.19/2.83 % (2952128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.19/2.83 % (2952128)CaDiCaL version: 2.1.3
% 16.19/2.83 % (2952128)Termination reason: Instruction limit
% 16.19/2.83 % (2952128)Termination phase: Saturation
% 16.19/2.83 % (2952128)Time elapsed: 0.184 s
% 16.19/2.83 % (2952128)Peak memory usage: 15 MB
% 16.19/2.83 % (2952128)Instructions burned: 373 (million)
% 16.19/2.83 % (2952117)Instruction limit reached!
% 16.19/2.83 % (2952117)------------------------------
% 16.19/2.83 % (2952117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.19/2.83 % (2952117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.19/2.83 % (2952117)CaDiCaL version: 2.1.3
% 16.19/2.83 % (2952117)Termination reason: Instruction limit
% 16.19/2.83 % (2952117)Termination phase: Saturation
% 16.19/2.83 % (2952117)Time elapsed: 0.309 s
% 16.19/2.83 % (2952117)Peak memory usage: 15 MB
% 16.19/2.83 % (2952117)Instructions burned: 338 (million)
% 16.19/2.83 % (2952134)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4260075041:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2983 on theBenchmark for (2983ds/270Mi)
% 16.19/2.83 % (2952135)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=1727526897:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2983 on theBenchmark for (2983ds/9840Mi)
% 16.19/2.83 % (2952123)Instruction limit reached!
% 16.19/2.83 % (2952123)------------------------------
% 16.19/2.83 % (2952123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.19/2.83 % (2952123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.19/2.83 % (2952123)CaDiCaL version: 2.1.3
% 16.19/2.83 % (2952123)Termination reason: Instruction limit
% 16.19/2.83 % (2952123)Termination phase: Saturation
% 16.19/2.83 % (2952123)Time elapsed: 0.291 s
% 16.19/2.83 % (2952123)Peak memory usage: 12 MB
% 16.19/2.83 % (2952123)Instructions burned: 340 (million)
% 16.19/2.83 % (2952136)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=4070237292:i=421:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/421Mi)
% 16.19/2.83 % (2952130)Instruction limit reached!
% 16.19/2.83 % (2952130)------------------------------
% 16.19/2.83 % (2952130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.19/2.83 % (2952130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.19/2.83 % (2952130)CaDiCaL version: 2.1.3
% 16.19/2.83 % (2952130)Termination reason: Instruction limit
% 16.19/2.83 % (2952130)Termination phase: Saturation
% 16.19/2.83 % (2952130)Time elapsed: 0.110 s
% 16.19/2.83 % (2952130)Peak memory usage: 13 MB
% 16.19/2.83 % (2952130)Instructions burned: 117 (million)
% 16.19/2.83 % (2952139)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
% 16.19/2.83 % (2952139)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=4231417715:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/270Mi)
% 16.19/2.83 % (2952141)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=806980069:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/31Mi)
% 20.90/3.30 % (2952141)Instruction limit reached!
% 20.90/3.30 % (2952141)------------------------------
% 20.90/3.30 % (2952141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.90/3.30 % (2952141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.30 % (2952141)CaDiCaL version: 2.1.3
% 20.90/3.30 % (2952141)Termination reason: Instruction limit
% 20.90/3.30 % (2952141)Termination phase: Saturation
% 20.90/3.30 % (2952141)Time elapsed: 0.027 s
% 20.90/3.30 % (2952141)Peak memory usage: 12 MB
% 20.90/3.30 % (2952141)Instructions burned: 32 (million)
% 20.90/3.30 % (2952144)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 20.90/3.30 % (2952144)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 20.90/3.30 % (2952144)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=3944367424:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2982 on theBenchmark for (2982ds/1440Mi)
% 20.90/3.30 % (2952134)Instruction limit reached!
% 20.90/3.30 % (2952134)------------------------------
% 20.90/3.30 % (2952134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.90/3.30 % (2952134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.30 % (2952134)CaDiCaL version: 2.1.3
% 20.90/3.30 % (2952134)Termination reason: Instruction limit
% 20.90/3.30 % (2952134)Termination phase: Saturation
% 20.90/3.30 % (2952134)Time elapsed: 0.226 s
% 20.90/3.30 % (2952134)Peak memory usage: 13 MB
% 20.90/3.30 % (2952134)Instructions burned: 270 (million)
% 20.90/3.30 % (2952146)dis+10_2_sil=128000:si=on:random_seed=189835354:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2980 on theBenchmark for (2980ds/339Mi)
% 20.90/3.30 % (2952139)Instruction limit reached!
% 20.90/3.30 % (2952139)------------------------------
% 20.90/3.30 % (2952139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.90/3.30 % (2952139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.30 % (2952139)CaDiCaL version: 2.1.3
% 20.90/3.30 % (2952139)Termination reason: Instruction limit
% 20.90/3.30 % (2952139)Termination phase: Saturation
% 20.90/3.30 % (2952139)Time elapsed: 0.253 s
% 20.90/3.30 % (2952139)Peak memory usage: 14 MB
% 20.90/3.30 % (2952139)Instructions burned: 271 (million)
% 20.90/3.30 % (2952148)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=220080533:i=111:add=on:fgj=on:rtra=on:fdi=1024_2979 on theBenchmark for (2979ds/111Mi)
% 20.90/3.30 % (2952136)Instruction limit reached!
% 20.90/3.30 % (2952136)------------------------------
% 20.90/3.30 % (2952136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.90/3.30 % (2952136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.30 % (2952136)CaDiCaL version: 2.1.3
% 20.90/3.30 % (2952136)Termination reason: Instruction limit
% 20.90/3.30 % (2952136)Termination phase: Saturation
% 20.90/3.30 % (2952136)Time elapsed: 0.373 s
% 20.90/3.30 % (2952136)Peak memory usage: 14 MB
% 20.90/3.30 % (2952136)Instructions burned: 421 (million)
% 20.90/3.30 % (2952148)Instruction limit reached!
% 20.90/3.30 % (2952148)------------------------------
% 20.90/3.30 % (2952148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.90/3.30 % (2952148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.30 % (2952148)CaDiCaL version: 2.1.3
% 20.90/3.30 % (2952148)Termination reason: Instruction limit
% 20.90/3.30 % (2952148)Termination phase: Saturation
% 20.90/3.30 % (2952148)Time elapsed: 0.083 s
% 20.90/3.30 % (2952148)Peak memory usage: 13 MB
% 20.90/3.30 % (2952148)Instructions burned: 111 (million)
% 20.90/3.30 % (2952152)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=519810385:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2979 on theBenchmark for (2979ds/122Mi)
% 20.90/3.30 % (2952131)Instruction limit reached!
% 20.90/3.30 % (2952131)------------------------------
% 20.90/3.30 % (2952131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.90/3.30 % (2952131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.30 % (2952131)CaDiCaL version: 2.1.3
% 20.90/3.30 % (2952131)Termination reason: Instruction limit
% 21.50/3.59 % (2952131)Termination phase: Saturation
% 21.50/3.59 % (2952131)Time elapsed: 0.507 s
% 21.50/3.59 % (2952131)Peak memory usage: 16 MB
% 21.50/3.59 % (2952131)Instructions burned: 575 (million)
% 21.50/3.59 % (2952153)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=2692682936:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/136Mi)
% 21.50/3.59 % (2952156)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=789944025:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/232Mi)
% 21.50/3.59 % (2952152)Instruction limit reached!
% 21.50/3.59 % (2952152)------------------------------
% 21.50/3.59 % (2952152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.50/3.59 % (2952152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/3.59 % (2952152)CaDiCaL version: 2.1.3
% 21.50/3.59 % (2952152)Termination reason: Instruction limit
% 21.50/3.59 % (2952152)Termination phase: Saturation
% 21.50/3.59 % (2952152)Time elapsed: 0.080 s
% 21.50/3.59 % (2952152)Peak memory usage: 13 MB
% 21.50/3.59 % (2952152)Instructions burned: 122 (million)
% 21.50/3.59 % (2952158)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=1806108650:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2977 on theBenchmark for (2977ds/1254Mi)
% 21.50/3.59 % (2952146)Instruction limit reached!
% 21.50/3.59 % (2952146)------------------------------
% 21.50/3.59 % (2952146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.50/3.59 % (2952146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/3.59 % (2952146)CaDiCaL version: 2.1.3
% 21.50/3.59 % (2952146)Termination reason: Instruction limit
% 21.50/3.59 % (2952146)Termination phase: Saturation
% 21.50/3.59 % (2952146)Time elapsed: 0.289 s
% 21.50/3.59 % (2952146)Peak memory usage: 13 MB
% 21.50/3.59 % (2952146)Instructions burned: 340 (million)
% 21.50/3.59 % (2952153)Instruction limit reached!
% 21.50/3.59 % (2952153)------------------------------
% 21.50/3.59 % (2952153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.50/3.59 % (2952153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/3.59 % (2952153)CaDiCaL version: 2.1.3
% 21.50/3.59 % (2952153)Termination reason: Instruction limit
% 21.50/3.59 % (2952153)Termination phase: Saturation
% 21.50/3.59 % (2952153)Time elapsed: 0.123 s
% 21.50/3.59 % (2952153)Peak memory usage: 13 MB
% 21.50/3.59 % (2952153)Instructions burned: 137 (million)
% 21.50/3.59 % (2952160)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 21.50/3.59 % (2952160)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=2752477197:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2977 on theBenchmark for (2977ds/281Mi)
% 21.50/3.59 % (2952161)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2992017863:i=619:add=on:rtra=on_2977 on theBenchmark for (2977ds/619Mi)
% 21.50/3.59 % (2952156)Instruction limit reached!
% 21.50/3.59 % (2952156)------------------------------
% 21.50/3.59 % (2952156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.50/3.59 % (2952156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/3.59 % (2952156)CaDiCaL version: 2.1.3
% 21.50/3.59 % (2952156)Termination reason: Instruction limit
% 21.50/3.59 % (2952156)Termination phase: Saturation
% 21.50/3.59 % (2952156)Time elapsed: 0.187 s
% 21.50/3.59 % (2952156)Peak memory usage: 13 MB
% 21.50/3.59 % (2952156)Instructions burned: 233 (million)
% 21.50/3.59 % (2952164)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=534079486:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/865Mi)
% 21.50/3.59 % (2952160)Instruction limit reached!
% 21.50/3.59 % (2952160)------------------------------
% 21.50/3.59 % (2952160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.50/3.59 % (2952160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/3.59 % (2952160)CaDiCaL version: 2.1.3
% 21.50/3.59 % (2952160)Termination reason: Instruction limit
% 21.50/3.59 % (2952160)Termination phase: Saturation
% 23.60/3.79 % (2952160)Time elapsed: 0.249 s
% 23.60/3.79 % (2952160)Peak memory usage: 14 MB
% 23.60/3.79 % (2952160)Instructions burned: 281 (million)
% 23.60/3.79 % (2952166)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2183372536:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/212Mi)
% 23.60/3.79 % (2952166)Instruction limit reached!
% 23.60/3.79 % (2952166)------------------------------
% 23.60/3.79 % (2952166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.60/3.79 % (2952166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.60/3.79 % (2952166)CaDiCaL version: 2.1.3
% 23.60/3.79 % (2952166)Termination reason: Instruction limit
% 23.60/3.79 % (2952166)Termination phase: Saturation
% 23.60/3.79 % (2952166)Time elapsed: 0.139 s
% 23.60/3.79 % (2952166)Peak memory usage: 13 MB
% 23.60/3.79 % (2952166)Instructions burned: 213 (million)
% 23.60/3.79 % (2952168)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=1238893939:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/130Mi)
% 23.60/3.79 % (2952161)Instruction limit reached!
% 23.60/3.79 % (2952161)------------------------------
% 23.60/3.79 % (2952161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.60/3.79 % (2952161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.60/3.79 % (2952161)CaDiCaL version: 2.1.3
% 23.60/3.79 % (2952161)Termination reason: Instruction limit
% 23.60/3.79 % (2952161)Termination phase: Saturation
% 23.60/3.79 % (2952161)Time elapsed: 0.492 s
% 23.60/3.79 % (2952161)Peak memory usage: 13 MB
% 23.60/3.79 % (2952161)Instructions burned: 619 (million)
% 23.60/3.79 % (2952144)Instruction limit reached!
% 23.60/3.79 % (2952144)------------------------------
% 23.60/3.79 % (2952144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.60/3.79 % (2952144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.60/3.79 % (2952144)CaDiCaL version: 2.1.3
% 23.60/3.79 % (2952144)Termination reason: Instruction limit
% 23.60/3.79 % (2952144)Termination phase: Saturation
% 23.60/3.79 % (2952144)Time elapsed: 1.002 s
% 23.60/3.79 % (2952144)Peak memory usage: 14 MB
% 23.60/3.79 % (2952144)Instructions burned: 1441 (million)
% 23.60/3.79 % (2952170)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3836443326:st=1.5:i=346:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/346Mi)
% 23.60/3.79 % (2952168)Instruction limit reached!
% 23.60/3.79 % (2952168)------------------------------
% 23.60/3.79 % (2952168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.60/3.79 % (2952168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.60/3.79 % (2952168)CaDiCaL version: 2.1.3
% 23.60/3.79 % (2952168)Termination reason: Instruction limit
% 23.60/3.79 % (2952168)Termination phase: Saturation
% 23.60/3.79 % (2952168)Time elapsed: 0.134 s
% 23.60/3.79 % (2952168)Peak memory usage: 13 MB
% 23.60/3.79 % (2952168)Instructions burned: 131 (million)
% 23.60/3.79 % (2952171)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3219614953:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2971 on theBenchmark for (2971ds/152Mi)
% 23.60/3.79 % (2952174)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2997435576:i=75:ep=R:rtra=on:ntd=on_2971 on theBenchmark for (2971ds/75Mi)
% 23.60/3.79 % (2952174)Instruction limit reached!
% 23.60/3.79 % (2952174)------------------------------
% 23.60/3.79 % (2952174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.60/3.79 % (2952174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.60/3.79 % (2952174)CaDiCaL version: 2.1.3
% 23.60/3.79 % (2952174)Termination reason: Instruction limit
% 23.60/3.79 % (2952174)Termination phase: Saturation
% 23.60/3.79 % (2952174)Time elapsed: 0.068 s
% 23.60/3.79 % (2952174)Peak memory usage: 12 MB
% 23.60/3.79 % (2952174)Instructions burned: 76 (million)
% 23.60/3.79 % (2952176)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=3476211129:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/387Mi)
% 23.60/3.79 % (2952171)Instruction limit reached!
% 23.60/3.79 % (2952171)------------------------------
% 23.60/3.79 % (2952171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.60/3.79 % (2952171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.60/3.79 % (2952171)CaDiCaL version: 2.1.3
% 23.60/3.79 % (2952171)Termination reason: Instruction limit
% 23.60/3.79 % (2952171)Termination phase: Saturation
% 27.05/4.16 % (2952171)Time elapsed: 0.133 s
% 27.05/4.16 % (2952171)Peak memory usage: 13 MB
% 27.05/4.16 % (2952171)Instructions burned: 152 (million)
% 27.05/4.16 % (2952178)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=1333218974:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2970 on theBenchmark for (2970ds/148Mi)
% 27.05/4.16 % (2952178)Instruction limit reached!
% 27.05/4.16 % (2952178)------------------------------
% 27.05/4.16 % (2952178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.16 % (2952178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.16 % (2952178)CaDiCaL version: 2.1.3
% 27.05/4.16 % (2952178)Termination reason: Instruction limit
% 27.05/4.16 % (2952178)Termination phase: Saturation
% 27.05/4.16 % (2952178)Time elapsed: 0.082 s
% 27.05/4.16 % (2952178)Peak memory usage: 12 MB
% 27.05/4.16 % (2952178)Instructions burned: 148 (million)
% 27.05/4.16 % (2952170)Instruction limit reached!
% 27.05/4.16 % (2952170)------------------------------
% 27.05/4.16 % (2952170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.16 % (2952170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.16 % (2952170)CaDiCaL version: 2.1.3
% 27.05/4.16 % (2952170)Termination reason: Instruction limit
% 27.05/4.16 % (2952170)Termination phase: Saturation
% 27.05/4.16 % (2952170)Time elapsed: 0.287 s
% 27.05/4.16 % (2952170)Peak memory usage: 13 MB
% 27.05/4.16 % (2952170)Instructions burned: 347 (million)
% 27.05/4.16 % (2952180)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=149649668:i=161:piset=and:rtra=on:ntd=on_2968 on theBenchmark for (2968ds/161Mi)
% 27.05/4.16 % (2952181)lrs+10_1_sil=128000:si=on:random_seed=3463056827:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/888Mi)
% 27.05/4.16 % (2952164)Instruction limit reached!
% 27.05/4.16 % (2952164)------------------------------
% 27.05/4.16 % (2952164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.16 % (2952164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.16 % (2952164)CaDiCaL version: 2.1.3
% 27.05/4.16 % (2952164)Termination reason: Instruction limit
% 27.05/4.16 % (2952164)Termination phase: Saturation
% 27.05/4.16 % (2952164)Time elapsed: 0.788 s
% 27.05/4.16 % (2952164)Peak memory usage: 21 MB
% 27.05/4.16 % (2952164)Instructions burned: 866 (million)
% 27.05/4.16 % (2952184)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=984951373:i=136:add=on:ins=4:rtra=on:sup=off_2968 on theBenchmark for (2968ds/136Mi)
% 27.05/4.16 % (2952184)Refutation not found, incomplete strategy
% 27.05/4.16 % (2952184)------------------------------
% 27.05/4.16 % (2952184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.16 % (2952184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.16 % (2952184)CaDiCaL version: 2.1.3
% 27.05/4.16 % (2952184)Termination reason: Refutation not found, incomplete strategy
% 27.05/4.16 % (2952184)Time elapsed: 0.005 s
% 27.05/4.16 % (2952184)Peak memory usage: 12 MB
% 27.05/4.16 % (2952184)Instructions burned: 7 (million)
% 27.05/4.16 % (2952184)------------------------------
% 27.05/4.16 % (2952184)------------------------------
% 27.05/4.16 % (2952180)Instruction limit reached!
% 27.05/4.16 % (2952180)------------------------------
% 27.05/4.16 % (2952180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.16 % (2952180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.16 % (2952180)CaDiCaL version: 2.1.3
% 27.05/4.16 % (2952180)Termination reason: Instruction limit
% 27.05/4.16 % (2952180)Termination phase: Saturation
% 27.05/4.16 % (2952180)Time elapsed: 0.117 s
% 27.05/4.16 % (2952180)Peak memory usage: 13 MB
% 27.05/4.16 % (2952180)Instructions burned: 161 (million)
% 27.05/4.16 % (2952186)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=4150095135:i=88:s2at=3:nm=2:rtra=on:rawr=on_2967 on theBenchmark for (2967ds/88Mi)
% 27.05/4.16 % (2952187)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=431158886:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2967 on theBenchmark for (2967ds/93Mi)
% 27.05/4.16 % (2952158)Instruction limit reached!
% 27.05/4.16 % (2952158)------------------------------
% 28.73/4.41 % (2952158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.73/4.41 % (2952158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.41 % (2952158)CaDiCaL version: 2.1.3
% 28.73/4.41 % (2952158)Termination reason: Instruction limit
% 28.73/4.41 % (2952158)Termination phase: Saturation
% 28.73/4.41 % (2952158)Time elapsed: 1.061 s
% 28.73/4.41 % (2952158)Peak memory usage: 15 MB
% 28.73/4.41 % (2952158)Instructions burned: 1254 (million)
% 28.73/4.41 % (2952176)Instruction limit reached!
% 28.73/4.41 % (2952176)------------------------------
% 28.73/4.41 % (2952176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.73/4.41 % (2952176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.41 % (2952176)CaDiCaL version: 2.1.3
% 28.73/4.41 % (2952176)Termination reason: Instruction limit
% 28.73/4.41 % (2952176)Termination phase: Saturation
% 28.73/4.41 % (2952176)Time elapsed: 0.317 s
% 28.73/4.41 % (2952176)Peak memory usage: 13 MB
% 28.73/4.41 % (2952176)Instructions burned: 388 (million)
% 28.73/4.41 % (2952186)Instruction limit reached!
% 28.73/4.41 % (2952186)------------------------------
% 28.73/4.41 % (2952186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.73/4.41 % (2952186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.41 % (2952186)CaDiCaL version: 2.1.3
% 28.73/4.41 % (2952186)Termination reason: Instruction limit
% 28.73/4.41 % (2952186)Termination phase: Saturation
% 28.73/4.41 % (2952186)Time elapsed: 0.063 s
% 28.73/4.41 % (2952186)Peak memory usage: 13 MB
% 28.73/4.41 % (2952186)Instructions burned: 89 (million)
% 28.73/4.41 % (2952190)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3250612858:i=2186:rtra=on:ixr=off_2967 on theBenchmark for (2967ds/2186Mi)
% 28.73/4.41 % (2952191)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3182002647:s2a=on:i=240:rtra=on:ntd=on_2967 on theBenchmark for (2967ds/240Mi)
% 28.73/4.41 % (2952192)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=3758629873:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2966 on theBenchmark for (2966ds/805Mi)
% 28.73/4.41 % (2952192)Refutation not found, incomplete strategy
% 28.73/4.41 % (2952192)------------------------------
% 28.73/4.41 % (2952192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.73/4.41 % (2952192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.41 % (2952192)CaDiCaL version: 2.1.3
% 28.73/4.41 % (2952192)Termination reason: Refutation not found, incomplete strategy
% 28.73/4.41 % (2952192)Time elapsed: 0.014 s
% 28.73/4.41 % (2952192)Peak memory usage: 12 MB
% 28.73/4.41 % (2952192)Instructions burned: 19 (million)
% 28.73/4.41 % (2952192)------------------------------
% 28.73/4.41 % (2952192)------------------------------
% 28.73/4.41 % (2952187)Instruction limit reached!
% 28.73/4.41 % (2952187)------------------------------
% 28.73/4.41 % (2952187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.73/4.41 % (2952187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.41 % (2952187)CaDiCaL version: 2.1.3
% 28.73/4.41 % (2952187)Termination reason: Instruction limit
% 28.73/4.41 % (2952187)Termination phase: Saturation
% 28.73/4.41 % (2952187)Time elapsed: 0.083 s
% 28.73/4.41 % (2952187)Peak memory usage: 12 MB
% 28.73/4.41 % (2952187)Instructions burned: 94 (million)
% 28.73/4.41 % (2952196)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 28.73/4.41 % (2952196)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=1562536830:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2966 on theBenchmark for (2966ds/391Mi)
% 28.73/4.41 % (2952197)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=3263505864:i=355:av=off:fsr=off:rtra=on:ixr=off_2966 on theBenchmark for (2966ds/355Mi)
% 28.73/4.41 % (2952104)Instruction limit reached!
% 28.73/4.41 % (2952104)------------------------------
% 28.73/4.41 % (2952104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.73/4.41 % (2952104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.73/4.41 % (2952104)CaDiCaL version: 2.1.3
% 28.73/4.41 % (2952104)Termination reason: Instruction limit
% 28.73/4.41 % (2952104)Termination phase: Saturation
% 30.86/4.78 % (2952104)Time elapsed: 2.407 s
% 30.86/4.78 % (2952104)Peak memory usage: 44 MB
% 30.86/4.78 % (2952104)Instructions burned: 5756 (million)
% 30.86/4.78 % (2952200)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=2434624559:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/314Mi)
% 30.86/4.78 % (2952191)Instruction limit reached!
% 30.86/4.78 % (2952191)------------------------------
% 30.86/4.78 % (2952191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.86/4.78 % (2952191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.86/4.78 % (2952191)CaDiCaL version: 2.1.3
% 30.86/4.78 % (2952191)Termination reason: Instruction limit
% 30.86/4.78 % (2952191)Termination phase: Saturation
% 30.86/4.78 % (2952191)Time elapsed: 0.213 s
% 30.86/4.78 % (2952191)Peak memory usage: 14 MB
% 30.86/4.78 % (2952191)Instructions burned: 240 (million)
% 30.86/4.78 % (2952202)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=2593703249:s2a=on:i=251:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/251Mi)
% 30.86/4.78 % (2952200)Instruction limit reached!
% 30.86/4.78 % (2952200)------------------------------
% 30.86/4.78 % (2952200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.86/4.78 % (2952200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.86/4.78 % (2952200)CaDiCaL version: 2.1.3
% 30.86/4.78 % (2952200)Termination reason: Instruction limit
% 30.86/4.78 % (2952200)Termination phase: Saturation
% 30.86/4.78 % (2952200)Time elapsed: 0.156 s
% 30.86/4.78 % (2952200)Peak memory usage: 13 MB
% 30.86/4.78 % (2952200)Instructions burned: 315 (million)
% 30.86/4.78 % (2952196)Instruction limit reached!
% 30.86/4.78 % (2952196)------------------------------
% 30.86/4.78 % (2952196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.86/4.78 % (2952196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.86/4.78 % (2952196)CaDiCaL version: 2.1.3
% 30.86/4.78 % (2952196)Termination reason: Instruction limit
% 30.86/4.78 % (2952196)Termination phase: Saturation
% 30.86/4.78 % (2952196)Time elapsed: 0.315 s
% 30.86/4.78 % (2952196)Peak memory usage: 14 MB
% 30.86/4.78 % (2952196)Instructions burned: 392 (million)
% 30.86/4.78 % (2952204)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=1814995863: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_2963 on theBenchmark for (2963ds/2470Mi)
% 30.86/4.78 % (2952197)Instruction limit reached!
% 30.86/4.78 % (2952197)------------------------------
% 30.86/4.78 % (2952197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.86/4.78 % (2952197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.86/4.78 % (2952197)CaDiCaL version: 2.1.3
% 30.86/4.78 % (2952197)Termination reason: Instruction limit
% 30.86/4.78 % (2952197)Termination phase: Saturation
% 30.86/4.78 % (2952197)Time elapsed: 0.315 s
% 30.86/4.78 % (2952197)Peak memory usage: 13 MB
% 30.86/4.78 % (2952197)Instructions burned: 355 (million)
% 30.86/4.78 % (2952205)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=864741522:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2963 on theBenchmark for (2963ds/673Mi)
% 30.86/4.78 % (2952207)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=866180730:i=116:ep=RSTC:rtra=on:ntd=on_2962 on theBenchmark for (2962ds/116Mi)
% 30.86/4.78 % (2952202)Instruction limit reached!
% 30.86/4.78 % (2952202)------------------------------
% 30.86/4.78 % (2952202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.86/4.78 % (2952202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.86/4.78 % (2952202)CaDiCaL version: 2.1.3
% 30.86/4.78 % (2952202)Termination reason: Instruction limit
% 30.86/4.78 % (2952202)Termination phase: Saturation
% 30.86/4.78 % (2952202)Time elapsed: 0.210 s
% 30.86/4.78 % (2952202)Peak memory usage: 13 MB
% 30.86/4.78 % (2952202)Instructions burned: 252 (million)
% 30.86/4.78 % (2952210)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=337800333:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2962 on theBenchmark for (2962ds/270Mi)
% 30.86/4.78 % (2952207)Instruction limit reached!
% 30.86/4.78 % (2952207)------------------------------
% 35.18/5.33 % (2952207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/5.33 % (2952207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/5.33 % (2952207)CaDiCaL version: 2.1.3
% 35.18/5.33 % (2952207)Termination reason: Instruction limit
% 35.18/5.33 % (2952207)Termination phase: Saturation
% 35.18/5.33 % (2952207)Time elapsed: 0.115 s
% 35.18/5.33 % (2952207)Peak memory usage: 13 MB
% 35.18/5.33 % (2952207)Instructions burned: 116 (million)
% 35.18/5.33 % (2952212)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=3322038837: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_2961 on theBenchmark for (2961ds/30Mi)
% 35.18/5.33 % (2952212)Instruction limit reached!
% 35.18/5.33 % (2952212)------------------------------
% 35.18/5.33 % (2952212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/5.33 % (2952212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/5.33 % (2952212)CaDiCaL version: 2.1.3
% 35.18/5.33 % (2952212)Termination reason: Instruction limit
% 35.18/5.33 % (2952212)Termination phase: Saturation
% 35.18/5.33 % (2952212)Time elapsed: 0.025 s
% 35.18/5.33 % (2952212)Peak memory usage: 12 MB
% 35.18/5.33 % (2952212)Instructions burned: 30 (million)
% 35.18/5.33 % (2952214)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 35.18/5.33 % (2952214)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=905055957:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2960 on theBenchmark for (2960ds/39Mi)
% 35.18/5.33 % (2952181)Instruction limit reached!
% 35.18/5.33 % (2952181)------------------------------
% 35.18/5.33 % (2952181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/5.33 % (2952181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/5.33 % (2952181)CaDiCaL version: 2.1.3
% 35.18/5.33 % (2952181)Termination reason: Instruction limit
% 35.18/5.33 % (2952181)Termination phase: Saturation
% 35.18/5.33 % (2952181)Time elapsed: 0.782 s
% 35.18/5.33 % (2952181)Peak memory usage: 17 MB
% 35.18/5.33 % (2952181)Instructions burned: 889 (million)
% 35.18/5.33 % (2952214)Instruction limit reached!
% 35.18/5.33 % (2952214)------------------------------
% 35.18/5.33 % (2952214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/5.33 % (2952214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/5.33 % (2952214)CaDiCaL version: 2.1.3
% 35.18/5.33 % (2952214)Termination reason: Instruction limit
% 35.18/5.33 % (2952214)Termination phase: Saturation
% 35.18/5.33 % (2952214)Time elapsed: 0.024 s
% 35.18/5.33 % (2952214)Peak memory usage: 12 MB
% 35.18/5.33 % (2952214)Instructions burned: 39 (million)
% 35.18/5.33 % (2952217)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3495944435:i=158:av=off:rtra=on_2960 on theBenchmark for (2960ds/158Mi)
% 35.18/5.33 % (2952216)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1951368916:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2960 on theBenchmark for (2960ds/365Mi)
% 35.18/5.33 % (2952210)Instruction limit reached!
% 35.18/5.33 % (2952210)------------------------------
% 35.18/5.33 % (2952210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/5.33 % (2952210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/5.33 % (2952210)CaDiCaL version: 2.1.3
% 35.18/5.33 % (2952210)Termination reason: Instruction limit
% 35.18/5.33 % (2952210)Termination phase: Saturation
% 35.18/5.33 % (2952210)Time elapsed: 0.229 s
% 35.18/5.33 % (2952210)Peak memory usage: 13 MB
% 35.18/5.33 % (2952210)Instructions burned: 270 (million)
% 35.18/5.33 % (2952220)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 35.18/5.33 % (2952220)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=1440338870:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2959 on theBenchmark for (2959ds/252Mi)
% 35.18/5.33 % (2952217)Instruction limit reached!
% 35.18/5.33 % (2952217)------------------------------
% 35.18/5.33 % (2952217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.82/5.46 % (2952217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.82/5.46 % (2952217)CaDiCaL version: 2.1.3
% 35.82/5.46 % (2952217)Termination reason: Instruction limit
% 35.82/5.46 % (2952217)Termination phase: Saturation
% 35.82/5.46 % (2952217)Time elapsed: 0.130 s
% 35.82/5.46 % (2952217)Peak memory usage: 12 MB
% 35.82/5.46 % (2952217)Instructions burned: 158 (million)
% 35.82/5.46 % (2952222)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2379493430:i=213:rtra=on:ss=axioms_2958 on theBenchmark for (2958ds/213Mi)
% 35.82/5.46 % (2952220)Instruction limit reached!
% 35.82/5.46 % (2952220)------------------------------
% 35.82/5.46 % (2952220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.82/5.46 % (2952220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.82/5.46 % (2952220)CaDiCaL version: 2.1.3
% 35.82/5.46 % (2952220)Termination reason: Instruction limit
% 35.82/5.46 % (2952220)Termination phase: Saturation
% 35.82/5.46 % (2952220)Time elapsed: 0.229 s
% 35.82/5.46 % (2952220)Peak memory usage: 13 MB
% 35.82/5.46 % (2952220)Instructions burned: 253 (million)
% 35.82/5.46 % (2952222)Instruction limit reached!
% 35.82/5.46 % (2952222)------------------------------
% 35.82/5.46 % (2952222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.82/5.46 % (2952222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.82/5.46 % (2952222)CaDiCaL version: 2.1.3
% 35.82/5.46 % (2952222)Termination reason: Instruction limit
% 35.82/5.46 % (2952222)Termination phase: Saturation
% 35.82/5.46 % (2952222)Time elapsed: 0.173 s
% 35.82/5.46 % (2952222)Peak memory usage: 13 MB
% 35.82/5.46 % (2952222)Instructions burned: 214 (million)
% 35.82/5.46 % (2952216)Instruction limit reached!
% 35.82/5.46 % (2952216)------------------------------
% 35.82/5.46 % (2952216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.82/5.46 % (2952216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.82/5.46 % (2952216)CaDiCaL version: 2.1.3
% 35.82/5.46 % (2952216)Termination reason: Instruction limit
% 35.82/5.46 % (2952216)Termination phase: Saturation
% 35.82/5.46 % (2952216)Time elapsed: 0.331 s
% 35.82/5.46 % (2952216)Peak memory usage: 15 MB
% 35.82/5.46 % (2952216)Instructions burned: 366 (million)
% 35.82/5.46 % (2952205)Instruction limit reached!
% 35.82/5.46 % (2952205)------------------------------
% 35.82/5.46 % (2952205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.82/5.46 % (2952205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.82/5.46 % (2952205)CaDiCaL version: 2.1.3
% 35.82/5.46 % (2952205)Termination reason: Instruction limit
% 35.82/5.46 % (2952205)Termination phase: Saturation
% 35.82/5.46 % (2952205)Time elapsed: 0.607 s
% 35.82/5.46 % (2952205)Peak memory usage: 14 MB
% 35.82/5.46 % (2952205)Instructions burned: 674 (million)
% 35.82/5.46 % (2952226)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 35.82/5.46 % (2952224)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=1725446362:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2957 on theBenchmark for (2957ds/160Mi)
% 35.82/5.46 % (2952226)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=3581048752:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2956 on theBenchmark for (2956ds/237Mi)
% 35.82/5.46 % (2952225)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=1148612255:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2956 on theBenchmark for (2956ds/763Mi)
% 35.82/5.46 % (2952227)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=1991679591:s2a=on:i=386:rtra=on:ntd=on_2956 on theBenchmark for (2956ds/386Mi)
% 35.82/5.46 % (2952226)Instruction limit reached!
% 35.82/5.46 % (2952226)------------------------------
% 35.82/5.46 % (2952226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.82/5.46 % (2952226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.82/5.46 % (2952226)CaDiCaL version: 2.1.3
% 35.82/5.46 % (2952226)Termination reason: Instruction limit
% 35.82/5.46 % (2952226)Termination phase: Saturation
% 35.82/5.46 % (2952226)Time elapsed: 0.143 s
% 35.82/5.46 % (2952226)Peak memory usage: 13 MB
% 36.45/5.69 % (2952226)Instructions burned: 237 (million)
% 36.45/5.69 % (2952224)Instruction limit reached!
% 36.45/5.69 % (2952224)------------------------------
% 36.45/5.69 % (2952224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.45/5.69 % (2952224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.45/5.69 % (2952224)CaDiCaL version: 2.1.3
% 36.45/5.69 % (2952224)Termination reason: Instruction limit
% 36.45/5.69 % (2952224)Termination phase: Saturation
% 36.45/5.69 % (2952224)Time elapsed: 0.147 s
% 36.45/5.69 % (2952224)Peak memory usage: 13 MB
% 36.45/5.69 % (2952224)Instructions burned: 160 (million)
% 36.45/5.69 % (2952232)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=3314182785:i=300:piset=and:nm=32:rtra=on_2955 on theBenchmark for (2955ds/300Mi)
% 36.45/5.69 % (2952233)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=636346980:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2955 on theBenchmark for (2955ds/567Mi)
% 36.45/5.69 % (2952227)Instruction limit reached!
% 36.45/5.69 % (2952227)------------------------------
% 36.45/5.69 % (2952227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.45/5.69 % (2952227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.45/5.69 % (2952227)CaDiCaL version: 2.1.3
% 36.45/5.69 % (2952227)Termination reason: Instruction limit
% 36.45/5.69 % (2952227)Termination phase: Saturation
% 36.45/5.69 % (2952227)Time elapsed: 0.305 s
% 36.45/5.69 % (2952227)Peak memory usage: 13 MB
% 36.45/5.69 % (2952227)Instructions burned: 387 (million)
% 36.45/5.69 % (2952232)Instruction limit reached!
% 36.45/5.69 % (2952232)------------------------------
% 36.45/5.69 % (2952232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.45/5.69 % (2952232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.45/5.69 % (2952232)CaDiCaL version: 2.1.3
% 36.45/5.69 % (2952232)Termination reason: Instruction limit
% 36.45/5.69 % (2952232)Termination phase: Saturation
% 36.45/5.69 % (2952232)Time elapsed: 0.180 s
% 36.45/5.69 % (2952232)Peak memory usage: 13 MB
% 36.45/5.69 % (2952232)Instructions burned: 300 (million)
% 36.45/5.69 % (2952238)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=2522360069:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2953 on theBenchmark for (2953ds/379Mi)
% 36.45/5.69 % (2952239)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=244678554:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2953 on theBenchmark for (2953ds/429Mi)
% 36.45/5.69 % (2952204)Instruction limit reached!
% 36.45/5.69 % (2952204)------------------------------
% 36.45/5.69 % (2952204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.45/5.69 % (2952204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.45/5.69 % (2952204)CaDiCaL version: 2.1.3
% 36.45/5.69 % (2952204)Termination reason: Instruction limit
% 36.45/5.69 % (2952204)Termination phase: Saturation
% 36.45/5.69 % (2952204)Time elapsed: 1.087 s
% 36.45/5.69 % (2952204)Peak memory usage: 22 MB
% 36.45/5.69 % (2952204)Instructions burned: 2472 (million)
% 36.45/5.69 % (2952242)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=3000684185:i=478:bd=all:rtra=on_2952 on theBenchmark for (2952ds/478Mi)
% 36.45/5.69 % (2952225)Instruction limit reached!
% 36.45/5.69 % (2952225)------------------------------
% 36.45/5.69 % (2952225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.45/5.69 % (2952225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.45/5.69 % (2952225)CaDiCaL version: 2.1.3
% 36.45/5.69 % (2952225)Termination reason: Instruction limit
% 36.45/5.69 % (2952225)Termination phase: Saturation
% 36.45/5.69 % (2952225)Time elapsed: 0.676 s
% 36.45/5.69 % (2952225)Peak memory usage: 18 MB
% 36.45/5.69 % (2952225)Instructions burned: 763 (million)
% 36.45/5.69 % (2952233)Instruction limit reached!
% 36.45/5.69 % (2952233)------------------------------
% 36.45/5.69 % (2952233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.45/5.69 % (2952233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.45/5.69 % (2952233)CaDiCaL version: 2.1.3
% 36.45/5.69 % (2952233)Termination reason: Instruction limit
% 36.45/5.69 % (2952233)Termination phase: Saturation
% 36.45/5.69 % (2952233)Time elapsed: 0.497 s
% 36.45/5.69 % (2952233)Peak memory usage: 14 MB
% 36.45/5.69 % (2952233)Instructions burned: 567 (million)
% 36.45/5.69 % (2952190)Instruction limit reached!
% 36.45/5.69 % (2952190)------------------------------
% 40.65/6.12 % (2952190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.65/6.12 % (2952190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.65/6.12 % (2952190)CaDiCaL version: 2.1.3
% 40.65/6.12 % (2952190)Termination reason: Instruction limit
% 40.65/6.12 % (2952190)Termination phase: Saturation
% 40.65/6.12 % (2952190)Time elapsed: 1.698 s
% 40.65/6.12 % (2952190)Peak memory usage: 15 MB
% 40.65/6.12 % (2952190)Instructions burned: 2187 (million)
% 40.65/6.12 % (2952242)Instruction limit reached!
% 40.65/6.12 % (2952242)------------------------------
% 40.65/6.12 % (2952242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.65/6.12 % (2952242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.65/6.12 % (2952242)CaDiCaL version: 2.1.3
% 40.65/6.12 % (2952242)Termination reason: Instruction limit
% 40.65/6.12 % (2952242)Termination phase: Saturation
% 40.65/6.12 % (2952242)Time elapsed: 0.228 s
% 40.65/6.12 % (2952242)Peak memory usage: 14 MB
% 40.65/6.12 % (2952242)Instructions burned: 482 (million)
% 40.65/6.12 % (2952244)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1724105006:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2949 on theBenchmark for (2949ds/445Mi)
% 40.65/6.12 % (2952247)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=2398565559:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2949 on theBenchmark for (2949ds/4980Mi)
% 40.65/6.12 % (2952238)Instruction limit reached!
% 40.65/6.12 % (2952238)------------------------------
% 40.65/6.12 % (2952238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.65/6.12 % (2952238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.65/6.12 % (2952238)CaDiCaL version: 2.1.3
% 40.65/6.12 % (2952238)Termination reason: Instruction limit
% 40.65/6.12 % (2952238)Termination phase: Saturation
% 40.65/6.12 % (2952238)Time elapsed: 0.347 s
% 40.65/6.12 % (2952238)Peak memory usage: 14 MB
% 40.65/6.12 % (2952238)Instructions burned: 379 (million)
% 40.65/6.12 % (2952245)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=3246768942:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2949 on theBenchmark for (2949ds/71Mi)
% 40.65/6.12 % (2952246)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1941157997:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2949 on theBenchmark for (2949ds/302Mi)
% 40.65/6.12 % (2952250)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
% 40.65/6.12 % (2952250)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 40.65/6.12 % (2952250)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2927067459:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2949 on theBenchmark for (2949ds/100Mi)
% 40.65/6.12 % (2952245)Instruction limit reached!
% 40.65/6.12 % (2952245)------------------------------
% 40.65/6.12 % (2952245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.65/6.12 % (2952245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.65/6.12 % (2952245)CaDiCaL version: 2.1.3
% 40.65/6.12 % (2952245)Termination reason: Instruction limit
% 40.65/6.12 % (2952245)Termination phase: Saturation
% 40.65/6.12 % (2952245)Time elapsed: 0.060 s
% 40.65/6.12 % (2952245)Peak memory usage: 12 MB
% 40.65/6.12 % (2952245)Instructions burned: 71 (million)
% 40.65/6.12 % (2952239)Instruction limit reached!
% 40.65/6.12 % (2952239)------------------------------
% 40.65/6.12 % (2952239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.65/6.12 % (2952239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.65/6.12 % (2952239)CaDiCaL version: 2.1.3
% 40.65/6.12 % (2952239)Termination reason: Instruction limit
% 40.65/6.12 % (2952239)Termination phase: Saturation
% 40.65/6.12 % (2952239)Time elapsed: 0.402 s
% 40.65/6.12 % (2952239)Peak memory usage: 14 MB
% 40.65/6.12 % (2952239)Instructions burned: 430 (million)
% 40.65/6.12 % (2952254)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=3602180132:i=76:piset=equals:rtra=on:ntd=on_2948 on theBenchmark for (2948ds/76Mi)
% 40.65/6.12 % (2952255)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=3981996488:i=289:rtra=on_2948 on theBenchmark for (2948ds/289Mi)
% 41.57/6.29 % (2952255)Refutation not found, incomplete strategy
% 41.57/6.29 % (2952255)------------------------------
% 41.57/6.29 % (2952255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952255)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952255)Termination reason: Refutation not found, incomplete strategy
% 41.57/6.29 % (2952255)Time elapsed: 0.010 s
% 41.57/6.29 % (2952255)Peak memory usage: 12 MB
% 41.57/6.29 % (2952255)Instructions burned: 9 (million)
% 41.57/6.29 % (2952255)------------------------------
% 41.57/6.29 % (2952255)------------------------------
% 41.57/6.29 % (2952250)Instruction limit reached!
% 41.57/6.29 % (2952250)------------------------------
% 41.57/6.29 % (2952250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952250)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952250)Termination reason: Instruction limit
% 41.57/6.29 % (2952250)Termination phase: Saturation
% 41.57/6.29 % (2952250)Time elapsed: 0.086 s
% 41.57/6.29 % (2952250)Peak memory usage: 12 MB
% 41.57/6.29 % (2952250)Instructions burned: 100 (million)
% 41.57/6.29 % (2952254)Instruction limit reached!
% 41.57/6.29 % (2952254)------------------------------
% 41.57/6.29 % (2952254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952254)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952254)Termination reason: Instruction limit
% 41.57/6.29 % (2952254)Termination phase: Saturation
% 41.57/6.29 % (2952254)Time elapsed: 0.047 s
% 41.57/6.29 % (2952254)Peak memory usage: 13 MB
% 41.57/6.29 % (2952254)Instructions burned: 77 (million)
% 41.57/6.29 % (2952260)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 41.57/6.29 % (2952258)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=1845349160:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2948 on theBenchmark for (2948ds/493Mi)
% 41.57/6.29 % (2952259)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=576591742:cond=on:i=34:hud=10:nm=10:rtra=on_2948 on theBenchmark for (2948ds/34Mi)
% 41.57/6.29 % (2952260)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=4283614960:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2948 on theBenchmark for (2948ds/372Mi)
% 41.57/6.29 % (2952259)Instruction limit reached!
% 41.57/6.29 % (2952259)------------------------------
% 41.57/6.29 % (2952259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952259)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952259)Termination reason: Instruction limit
% 41.57/6.29 % (2952259)Termination phase: Saturation
% 41.57/6.29 % (2952259)Time elapsed: 0.031 s
% 41.57/6.29 % (2952259)Peak memory usage: 12 MB
% 41.57/6.29 % (2952259)Instructions burned: 34 (million)
% 41.57/6.29 % (2952264)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=819627306:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2947 on theBenchmark for (2947ds/670Mi)
% 41.57/6.29 % (2952246)Instruction limit reached!
% 41.57/6.29 % (2952246)------------------------------
% 41.57/6.29 % (2952246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952246)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952246)Termination reason: Instruction limit
% 41.57/6.29 % (2952246)Termination phase: Saturation
% 41.57/6.29 % (2952246)Time elapsed: 0.268 s
% 41.57/6.29 % (2952246)Peak memory usage: 15 MB
% 41.57/6.29 % (2952246)Instructions burned: 303 (million)
% 41.57/6.29 % (2952266)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2470699508:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2946 on theBenchmark for (2946ds/647Mi)
% 41.57/6.29 % (2952244)Instruction limit reached!
% 41.57/6.29 % (2952244)------------------------------
% 41.57/6.29 % (2952244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952244)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952244)Termination reason: Instruction limit
% 41.57/6.29 % (2952244)Termination phase: Saturation
% 41.57/6.29 % (2952244)Time elapsed: 0.350 s
% 41.57/6.29 % (2952244)Peak memory usage: 14 MB
% 41.57/6.29 % (2952244)Instructions burned: 447 (million)
% 41.57/6.29 % (2952260)Instruction limit reached!
% 41.57/6.29 % (2952260)------------------------------
% 41.57/6.29 % (2952260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952260)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952260)Termination reason: Instruction limit
% 41.57/6.29 % (2952260)Termination phase: Saturation
% 41.57/6.29 % (2952260)Time elapsed: 0.202 s
% 41.57/6.29 % (2952260)Peak memory usage: 12 MB
% 41.57/6.29 % (2952260)Instructions burned: 373 (million)
% 41.57/6.29 % (2952268)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=1516550370:i=857:add=off:kws=frequency:rtra=on:ntd=on_2946 on theBenchmark for (2946ds/857Mi)
% 41.57/6.29 % (2952270)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=2125100004:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2945 on theBenchmark for (2945ds/693Mi)
% 41.57/6.29 % (2952258)Instruction limit reached!
% 41.57/6.29 % (2952258)------------------------------
% 41.57/6.29 % (2952258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952258)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952258)Termination reason: Instruction limit
% 41.57/6.29 % (2952258)Termination phase: Saturation
% 41.57/6.29 % (2952258)Time elapsed: 0.397 s
% 41.57/6.29 % (2952258)Peak memory usage: 13 MB
% 41.57/6.29 % (2952258)Instructions burned: 494 (million)
% 41.57/6.29 % (2952276)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=3439660556:i=285:hud=10:bd=all:rtra=on:ss=axioms_2944 on theBenchmark for (2944ds/285Mi)
% 41.57/6.29 % (2952264)Instruction limit reached!
% 41.57/6.29 % (2952264)------------------------------
% 41.57/6.29 % (2952264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952264)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952264)Termination reason: Instruction limit
% 41.57/6.29 % (2952264)Termination phase: Saturation
% 41.57/6.29 % (2952264)Time elapsed: 0.470 s
% 41.57/6.29 % (2952264)Peak memory usage: 13 MB
% 41.57/6.29 % (2952264)Instructions burned: 670 (million)
% 41.57/6.29 % (2952278)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 41.57/6.29 % (2952278)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=901246501:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2942 on theBenchmark for (2942ds/52Mi)
% 41.57/6.29 % (2952278)Instruction limit reached!
% 41.57/6.29 % (2952278)------------------------------
% 41.57/6.29 % (2952278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952278)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952278)Termination reason: Instruction limit
% 41.57/6.29 % (2952278)Termination phase: Saturation
% 41.57/6.29 % (2952266)Instruction limit reached!
% 41.57/6.29 % (2952266)------------------------------
% 41.57/6.29 % (2952266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952278)Time elapsed: 0.050 s
% 41.57/6.29 % (2952278)Peak memory usage: 12 MB
% 41.57/6.29 % (2952278)Instructions burned: 52 (million)
% 41.57/6.29 % (2952266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952266)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952266)Termination reason: Instruction limit
% 41.57/6.29 % (2952266)Termination phase: Saturation
% 41.57/6.29 % (2952266)Time elapsed: 0.464 s
% 41.57/6.29 % (2952266)Peak memory usage: 13 MB
% 41.57/6.29 % (2952266)Instructions burned: 647 (million)
% 41.57/6.29 % (2952276)Instruction limit reached!
% 41.57/6.29 % (2952276)------------------------------
% 41.57/6.29 % (2952276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952276)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952276)Termination reason: Instruction limit
% 41.57/6.29 % (2952276)Termination phase: Saturation
% 41.57/6.29 % (2952276)Time elapsed: 0.206 s
% 41.57/6.29 % (2952276)Peak memory usage: 13 MB
% 41.57/6.29 % (2952276)Instructions burned: 285 (million)
% 41.57/6.29 % (2952281)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=705674873:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2941 on theBenchmark for (2941ds/2240Mi)
% 41.57/6.29 % (2952280)dis+10_1_si=on:random_seed=84386890:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2941 on theBenchmark for (2941ds/407Mi)
% 41.57/6.29 % (2952282)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=4179258623:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2941 on theBenchmark for (2941ds/336Mi)
% 41.57/6.29 % (2952270)Instruction limit reached!
% 41.57/6.29 % (2952270)------------------------------
% 41.57/6.29 % (2952270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.29 % (2952270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.29 % (2952270)CaDiCaL version: 2.1.3
% 41.57/6.29 % (2952270)Termination reason: Instruction limit
% 41.57/6.29 % (2952270)Termination phase: Saturation
% 41.57/6.29 % (2952270)Time elapsed: 0.498 s
% 41.57/6.29 % (2952270)Peak memory usage: 16 MB
% 41.57/6.29 % (2952270)Instructions burned: 693 (million)
% 41.57/6.29 % (2952286)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=665333372:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2940 on theBenchmark for (2940ds/1142Mi)
% 41.57/6.29 % (2952281) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2951965-2952281"...
% 41.57/6.29 % (2952281)...printing done.
% 41.57/6.29 % (2952281)Refutation found. Thanks to Tanya!
% 41.57/6.29 % SZS status Theorem for theBenchmark
% 41.57/6.29 % SZS output start Proof for theBenchmark
% See solution above
% 41.57/6.30 % (2952281)------------------------------
% 41.57/6.30 % (2952281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.57/6.30 % (2952281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.57/6.30 % (2952281)CaDiCaL version: 2.1.3
% 41.57/6.30 % (2952281)Termination reason: Refutation
% 41.57/6.30 % (2952281)Time elapsed: 0.133 s
% 41.57/6.30 % (2952281)Peak memory usage: 14 MB
% 41.57/6.30 % (2952281)Instructions burned: 136 (million)
% 41.57/6.30 % (2951965)Success in time 5.985 s
% 41.57/6.30 % Vampire exiting
%------------------------------------------------------------------------------