%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV001^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:37:26 AM UTC 2026
% Result : Theorem 14.06s 2.38s
% Output : Refutation 14.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 5
% Syntax : Number of formulae : 70 ( 19 unt; 0 typ; 4 def)
% Number of atoms : 211 ( 141 equ; 0 cnn)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1150 ( 57 ~; 56 |; 73 &; 952 @)
% ( 7 <=>; 3 =>; 0 <=; 2 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 1 usr)
% Number of type conns : 32 ( 32 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 304 ( 0 sgn 276 !; 28 ?; 304 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_1,type,
sK0: a > a > a ).
thf(func_def_2,type,
sK1: a > a > a ).
thf(func_def_3,type,
sK2: a ).
thf(func_def_4,type,
sK3: a ).
thf(func_def_5,type,
sK4: a ).
thf(func_def_6,type,
sK5: a ).
thf(func_def_7,type,
sK6: a ).
thf(func_def_8,type,
sK7: a ).
thf(f1,conjecture,
! [X1: a > a > a,X0: a > a > a] :
( ( ! [X3: a,X4: a,X2: a] :
( ( X0 @ ( X0 @ X2 @ X3 ) @ X4 )
= ( X0 @ X2 @ ( X0 @ X3 @ X4 ) ) )
& ! [X2: a] :
( ( X1 @ X2 @ X2 )
= X2 )
& ! [X2: a,X3: a] :
( ( X0 @ ( X1 @ X2 @ X3 ) @ X3 )
= X3 )
& ! [X3: a,X2: a] :
( ( X1 @ X2 @ X3 )
= ( X1 @ X3 @ X2 ) )
& ! [X2: a] :
( ( X0 @ X2 @ X2 )
= X2 )
& ! [X3: a,X2: a] :
( ( X1 @ ( X0 @ X2 @ X3 ) @ X3 )
= X3 )
& ! [X3: a,X2: a] :
( ( X0 @ X2 @ X3 )
= ( X0 @ X3 @ X2 ) )
& ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ X2 @ ( X1 @ X3 @ X4 ) ) ) )
=> ( ! [X2: a,X3: a,X4: a] :
( ( X0 @ X2 @ ( X1 @ X3 @ X4 ) )
= ( X1 @ ( X0 @ X2 @ X3 ) @ ( X0 @ X2 @ X4 ) ) )
<=> ! [X2: a,X4: a,X3: a] :
( ( X1 @ X2 @ ( X0 @ X3 @ X4 ) )
= ( X0 @ ( X1 @ X2 @ X3 ) @ ( X1 @ X2 @ X4 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cDISTRIB_THM_pme) ).
thf(f2,negated_conjecture,
~ ! [X1: a > a > a,X0: a > a > a] :
( ( ! [X3: a,X4: a,X2: a] :
( ( X0 @ ( X0 @ X2 @ X3 ) @ X4 )
= ( X0 @ X2 @ ( X0 @ X3 @ X4 ) ) )
& ! [X2: a] :
( ( X1 @ X2 @ X2 )
= X2 )
& ! [X2: a,X3: a] :
( ( X0 @ ( X1 @ X2 @ X3 ) @ X3 )
= X3 )
& ! [X3: a,X2: a] :
( ( X1 @ X2 @ X3 )
= ( X1 @ X3 @ X2 ) )
& ! [X2: a] :
( ( X0 @ X2 @ X2 )
= X2 )
& ! [X3: a,X2: a] :
( ( X1 @ ( X0 @ X2 @ X3 ) @ X3 )
= X3 )
& ! [X3: a,X2: a] :
( ( X0 @ X2 @ X3 )
= ( X0 @ X3 @ X2 ) )
& ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ X2 @ ( X1 @ X3 @ X4 ) ) ) )
=> ( ! [X2: a,X3: a,X4: a] :
( ( X0 @ X2 @ ( X1 @ X3 @ X4 ) )
= ( X1 @ ( X0 @ X2 @ X3 ) @ ( X0 @ X2 @ X4 ) ) )
<=> ! [X2: a,X4: a,X3: a] :
( ( X1 @ X2 @ ( X0 @ X3 @ X4 ) )
= ( X0 @ ( X1 @ X2 @ X3 ) @ ( X1 @ X2 @ X4 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f3,plain,
~ ! [X0: a > a > a,X1: a > a > a] :
( ( ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X4 @ X2 ) @ X3 )
= ( X1 @ X4 @ ( X1 @ X2 @ X3 ) ) )
& ! [X16: a,X17: a,X15: a] :
( ( X0 @ ( X0 @ X16 @ X15 ) @ X17 )
= ( X0 @ X16 @ ( X0 @ X15 @ X17 ) ) )
& ! [X13: a,X14: a] :
( ( X1 @ X13 @ X14 )
= ( X1 @ X14 @ X13 ) )
& ! [X5: a] :
( ( X0 @ X5 @ X5 )
= X5 )
& ! [X6: a,X7: a] :
( ( X1 @ ( X0 @ X6 @ X7 ) @ X7 )
= X7 )
& ! [X12: a,X11: a] :
( ( X0 @ ( X1 @ X12 @ X11 ) @ X11 )
= X11 )
& ! [X8: a,X9: a] :
( ( X0 @ X8 @ X9 )
= ( X0 @ X9 @ X8 ) )
& ! [X10: a] :
( ( X1 @ X10 @ X10 )
= X10 ) )
=> ( ! [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) )
<=> ! [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f4,plain,
? [X0: a > a > a,X1: a > a > a] :
( ( ! [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) )
<~> ! [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) ) )
& ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X4 @ X2 ) @ X3 )
= ( X1 @ X4 @ ( X1 @ X2 @ X3 ) ) )
& ! [X16: a,X17: a,X15: a] :
( ( X0 @ ( X0 @ X16 @ X15 ) @ X17 )
= ( X0 @ X16 @ ( X0 @ X15 @ X17 ) ) )
& ! [X13: a,X14: a] :
( ( X1 @ X13 @ X14 )
= ( X1 @ X14 @ X13 ) )
& ! [X5: a] :
( ( X0 @ X5 @ X5 )
= X5 )
& ! [X6: a,X7: a] :
( ( X1 @ ( X0 @ X6 @ X7 ) @ X7 )
= X7 )
& ! [X12: a,X11: a] :
( ( X0 @ ( X1 @ X12 @ X11 ) @ X11 )
= X11 )
& ! [X8: a,X9: a] :
( ( X0 @ X8 @ X9 )
= ( X0 @ X9 @ X8 ) )
& ! [X10: a] :
( ( X1 @ X10 @ X10 )
= X10 ) ),
inference(ennf_transformation,[],[f3]) ).
thf(f5,plain,
? [X1: a > a > a,X0: a > a > a] :
( ! [X10: a] :
( ( X1 @ X10 @ X10 )
= X10 )
& ! [X13: a,X14: a] :
( ( X1 @ X13 @ X14 )
= ( X1 @ X14 @ X13 ) )
& ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X4 @ X2 ) @ X3 )
= ( X1 @ X4 @ ( X1 @ X2 @ X3 ) ) )
& ! [X12: a,X11: a] :
( ( X0 @ ( X1 @ X12 @ X11 ) @ X11 )
= X11 )
& ! [X16: a,X17: a,X15: a] :
( ( X0 @ ( X0 @ X16 @ X15 ) @ X17 )
= ( X0 @ X16 @ ( X0 @ X15 @ X17 ) ) )
& ! [X6: a,X7: a] :
( ( X1 @ ( X0 @ X6 @ X7 ) @ X7 )
= X7 )
& ! [X5: a] :
( ( X0 @ X5 @ X5 )
= X5 )
& ! [X8: a,X9: a] :
( ( X0 @ X8 @ X9 )
= ( X0 @ X9 @ X8 ) )
& ( ! [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) )
<~> ! [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) ) ) ),
inference(flattening,[],[f4]) ).
thf(f6,plain,
? [X1: a > a > a,X0: a > a > a] :
( ! [X10: a] :
( ( X1 @ X10 @ X10 )
= X10 )
& ! [X13: a,X14: a] :
( ( X1 @ X13 @ X14 )
= ( X1 @ X14 @ X13 ) )
& ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X4 @ X2 ) @ X3 )
= ( X1 @ X4 @ ( X1 @ X2 @ X3 ) ) )
& ! [X12: a,X11: a] :
( ( X0 @ ( X1 @ X12 @ X11 ) @ X11 )
= X11 )
& ! [X16: a,X17: a,X15: a] :
( ( X0 @ ( X0 @ X16 @ X15 ) @ X17 )
= ( X0 @ X16 @ ( X0 @ X15 @ X17 ) ) )
& ! [X6: a,X7: a] :
( ( X1 @ ( X0 @ X6 @ X7 ) @ X7 )
= X7 )
& ! [X5: a] :
( ( X0 @ X5 @ X5 )
= X5 )
& ! [X8: a,X9: a] :
( ( X0 @ X8 @ X9 )
= ( X0 @ X9 @ X8 ) )
& ( ? [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
!= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) )
| ? [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
!= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) ) )
& ( ! [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) )
| ! [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) ) ) ),
inference(nnf_transformation,[],[f5]) ).
thf(f7,plain,
? [X1: a > a > a,X0: a > a > a] :
( ! [X10: a] :
( ( X1 @ X10 @ X10 )
= X10 )
& ! [X13: a,X14: a] :
( ( X1 @ X13 @ X14 )
= ( X1 @ X14 @ X13 ) )
& ! [X3: a,X2: a,X4: a] :
( ( X1 @ ( X1 @ X4 @ X2 ) @ X3 )
= ( X1 @ X4 @ ( X1 @ X2 @ X3 ) ) )
& ! [X12: a,X11: a] :
( ( X0 @ ( X1 @ X12 @ X11 ) @ X11 )
= X11 )
& ! [X16: a,X17: a,X15: a] :
( ( X0 @ ( X0 @ X16 @ X15 ) @ X17 )
= ( X0 @ X16 @ ( X0 @ X15 @ X17 ) ) )
& ! [X6: a,X7: a] :
( ( X1 @ ( X0 @ X6 @ X7 ) @ X7 )
= X7 )
& ! [X5: a] :
( ( X0 @ X5 @ X5 )
= X5 )
& ! [X8: a,X9: a] :
( ( X0 @ X8 @ X9 )
= ( X0 @ X9 @ X8 ) )
& ( ? [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
!= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) )
| ? [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
!= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) ) )
& ( ! [X19: a,X20: a,X18: a] :
( ( X0 @ ( X1 @ X18 @ X19 ) @ ( X1 @ X18 @ X20 ) )
= ( X1 @ X18 @ ( X0 @ X19 @ X20 ) ) )
| ! [X23: a,X22: a,X21: a] :
( ( X0 @ X21 @ ( X1 @ X23 @ X22 ) )
= ( X1 @ ( X0 @ X21 @ X23 ) @ ( X0 @ X21 @ X22 ) ) ) ) ),
inference(flattening,[],[f6]) ).
thf(f8,plain,
? [X0: a > a > a,X1: a > a > a] :
( ! [X2: a] :
( ( X0 @ X2 @ X2 )
= X2 )
& ! [X3: a,X4: a] :
( ( X0 @ X3 @ X4 )
= ( X0 @ X4 @ X3 ) )
& ! [X5: a,X6: a,X7: a] :
( ( X0 @ X7 @ ( X0 @ X6 @ X5 ) )
= ( X0 @ ( X0 @ X7 @ X6 ) @ X5 ) )
& ! [X8: a,X9: a] :
( ( X1 @ ( X0 @ X8 @ X9 ) @ X9 )
= X9 )
& ! [X10: a,X11: a,X12: a] :
( ( X1 @ X10 @ ( X1 @ X12 @ X11 ) )
= ( X1 @ ( X1 @ X10 @ X12 ) @ X11 ) )
& ! [X13: a,X14: a] :
( ( X0 @ ( X1 @ X13 @ X14 ) @ X14 )
= X14 )
& ! [X15: a] :
( ( X1 @ X15 @ X15 )
= X15 )
& ! [X16: a,X17: a] :
( ( X1 @ X17 @ X16 )
= ( X1 @ X16 @ X17 ) )
& ( ? [X18: a,X19: a,X20: a] :
( ( X1 @ ( X0 @ X20 @ X18 ) @ ( X0 @ X20 @ X19 ) )
!= ( X0 @ X20 @ ( X1 @ X18 @ X19 ) ) )
| ? [X21: a,X22: a,X23: a] :
( ( X0 @ ( X1 @ X23 @ X21 ) @ ( X1 @ X23 @ X22 ) )
!= ( X1 @ X23 @ ( X0 @ X21 @ X22 ) ) ) )
& ( ! [X24: a,X25: a,X26: a] :
( ( X1 @ ( X0 @ X26 @ X24 ) @ ( X0 @ X26 @ X25 ) )
= ( X0 @ X26 @ ( X1 @ X24 @ X25 ) ) )
| ! [X27: a,X28: a,X29: a] :
( ( X0 @ ( X1 @ X29 @ X27 ) @ ( X1 @ X29 @ X28 ) )
= ( X1 @ X29 @ ( X0 @ X27 @ X28 ) ) ) ) ),
inference(rectify,[],[f7]) ).
thf(f9,plain,
( ! [X2: a] :
( ( sK0 @ X2 @ X2 )
= X2 )
& ! [X3: a,X4: a] :
( ( sK0 @ X3 @ X4 )
= ( sK0 @ X4 @ X3 ) )
& ! [X5: a,X6: a,X7: a] :
( ( sK0 @ ( sK0 @ X7 @ X6 ) @ X5 )
= ( sK0 @ X7 @ ( sK0 @ X6 @ X5 ) ) )
& ! [X8: a,X9: a] :
( ( sK1 @ ( sK0 @ X8 @ X9 ) @ X9 )
= X9 )
& ! [X10: a,X11: a,X12: a] :
( ( sK1 @ X10 @ ( sK1 @ X12 @ X11 ) )
= ( sK1 @ ( sK1 @ X10 @ X12 ) @ X11 ) )
& ! [X13: a,X14: a] :
( ( sK0 @ ( sK1 @ X13 @ X14 ) @ X14 )
= X14 )
& ! [X15: a] :
( ( sK1 @ X15 @ X15 )
= X15 )
& ! [X16: a,X17: a] :
( ( sK1 @ X17 @ X16 )
= ( sK1 @ X16 @ X17 ) )
& ( ( ( sK1 @ ( sK0 @ sK4 @ sK2 ) @ ( sK0 @ sK4 @ sK3 ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK2 @ sK3 ) ) )
| ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ ( sK1 @ sK7 @ sK6 ) ) ) )
& ( ! [X24: a,X25: a,X26: a] :
( ( sK0 @ X26 @ ( sK1 @ X24 @ X25 ) )
= ( sK1 @ ( sK0 @ X26 @ X24 ) @ ( sK0 @ X26 @ X25 ) ) )
| ! [X27: a,X28: a,X29: a] :
( ( sK1 @ X29 @ ( sK0 @ X27 @ X28 ) )
= ( sK0 @ ( sK1 @ X29 @ X27 ) @ ( sK1 @ X29 @ X28 ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X18,sK2),skolemize(X19,sK3),skolemize(X20,sK4),skolemize(X21,sK5),skolemize(X22,sK6),skolemize(X23,sK7)],[f8]) ).
thf(f10,plain,
! [X28: a,X29: a,X26: a,X27: a,X24: a,X25: a] :
( ( ( sK0 @ X26 @ ( sK1 @ X24 @ X25 ) )
= ( sK1 @ ( sK0 @ X26 @ X24 ) @ ( sK0 @ X26 @ X25 ) ) )
| ( ( sK1 @ X29 @ ( sK0 @ X27 @ X28 ) )
= ( sK0 @ ( sK1 @ X29 @ X27 ) @ ( sK1 @ X29 @ X28 ) ) ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f11,plain,
( ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ ( sK1 @ sK7 @ sK6 ) ) )
| ( ( sK1 @ ( sK0 @ sK4 @ sK2 ) @ ( sK0 @ sK4 @ sK3 ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK2 @ sK3 ) ) ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f12,plain,
! [X16: a,X17: a] :
( ( sK1 @ X17 @ X16 )
= ( sK1 @ X16 @ X17 ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f14,plain,
! [X14: a,X13: a] :
( ( sK0 @ ( sK1 @ X13 @ X14 ) @ X14 )
= X14 ),
inference(cnf_transformation,[],[f9]) ).
thf(f15,plain,
! [X10: a,X11: a,X12: a] :
( ( sK1 @ X10 @ ( sK1 @ X12 @ X11 ) )
= ( sK1 @ ( sK1 @ X10 @ X12 ) @ X11 ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f16,plain,
! [X8: a,X9: a] :
( ( sK1 @ ( sK0 @ X8 @ X9 ) @ X9 )
= X9 ),
inference(cnf_transformation,[],[f9]) ).
thf(f17,plain,
! [X6: a,X7: a,X5: a] :
( ( sK0 @ ( sK0 @ X7 @ X6 ) @ X5 )
= ( sK0 @ X7 @ ( sK0 @ X6 @ X5 ) ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f18,plain,
! [X3: a,X4: a] :
( ( sK0 @ X3 @ X4 )
= ( sK0 @ X4 @ X3 ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f20,plain,
( ( ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) )
!= ( sK1 @ ( sK0 @ sK4 @ sK2 ) @ ( sK0 @ sK4 @ sK3 ) ) )
| ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ ( sK1 @ sK7 @ sK6 ) ) ) ),
inference(forward_demodulation,[],[f11,f12]) ).
thf(f22,definition,
( spl8_1
<=> ! [X29: a,X27: a,X28: a] :
( ( sK1 @ X29 @ ( sK0 @ X27 @ X28 ) )
= ( sK0 @ ( sK1 @ X29 @ X27 ) @ ( sK1 @ X29 @ X28 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
thf(f23,plain,
( ! [X28: a,X29: a,X27: a] :
( ( sK1 @ X29 @ ( sK0 @ X27 @ X28 ) )
= ( sK0 @ ( sK1 @ X29 @ X27 ) @ ( sK1 @ X29 @ X28 ) ) )
| ~ spl8_1 ),
inference(avatar_component_clause,[],[f22]) ).
thf(f25,definition,
( spl8_2
<=> ! [X25: a,X24: a,X26: a] :
( ( sK0 @ X26 @ ( sK1 @ X24 @ X25 ) )
= ( sK1 @ ( sK0 @ X26 @ X24 ) @ ( sK0 @ X26 @ X25 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
thf(f26,plain,
( ! [X26: a,X24: a,X25: a] :
( ( sK0 @ X26 @ ( sK1 @ X24 @ X25 ) )
= ( sK1 @ ( sK0 @ X26 @ X24 ) @ ( sK0 @ X26 @ X25 ) ) )
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f25]) ).
thf(f27,plain,
( spl8_1
| spl8_2 ),
inference(avatar_split_clause,[],[f10,f25,f22]) ).
thf(f28,plain,
! [X8: a,X9: a] :
( ( sK1 @ X9 @ ( sK0 @ X8 @ X9 ) )
= X9 ),
inference(forward_demodulation,[],[f16,f12]) ).
thf(f29,plain,
( ( ( sK1 @ ( sK0 @ sK4 @ sK3 ) @ ( sK0 @ sK4 @ sK2 ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) ) )
| ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ ( sK1 @ sK7 @ sK6 ) ) ) ),
inference(forward_demodulation,[],[f20,f12]) ).
thf(f31,definition,
( spl8_3
<=> ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
= ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ ( sK1 @ sK7 @ sK6 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
thf(f33,plain,
( ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ ( sK1 @ sK7 @ sK6 ) ) )
| spl8_3 ),
inference(avatar_component_clause,[],[f31]) ).
thf(f35,definition,
( spl8_4
<=> ( ( sK1 @ ( sK0 @ sK4 @ sK3 ) @ ( sK0 @ sK4 @ sK2 ) )
= ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition]) ).
thf(f37,plain,
( ( ( sK1 @ ( sK0 @ sK4 @ sK3 ) @ ( sK0 @ sK4 @ sK2 ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) ) )
| spl8_4 ),
inference(avatar_component_clause,[],[f35]) ).
thf(f38,plain,
( ~ spl8_3
| ~ spl8_4 ),
inference(avatar_split_clause,[],[f29,f35,f31]) ).
thf(f39,plain,
( ( ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) ) )
| ~ spl8_2
| spl8_4 ),
inference(backward_demodulation,[],[f37,f26]) ).
thf(f40,plain,
( $false
| ~ spl8_2
| spl8_4 ),
inference(trivial_inequality_removal,[],[f39]) ).
thf(f41,plain,
( ~ spl8_2
| spl8_4 ),
inference(avatar_contradiction_clause,[],[f40]) ).
thf(f44,plain,
! [X0: a,X1: a] :
( ( sK0 @ ( sK1 @ X0 @ X1 ) @ X0 )
= X0 ),
inference(constrained_superposition,[],[f14,f12]) ).
thf(f45,plain,
! [X0: a,X1: a] :
( ( sK0 @ X0 @ ( sK1 @ X0 @ X1 ) )
= X0 ),
inference(forward_demodulation,[],[f44,f18]) ).
thf(f48,plain,
! [X0: a,X1: a] :
( ( sK0 @ X0 @ ( sK1 @ X1 @ X0 ) )
= X0 ),
inference(constrained_superposition,[],[f18,f14]) ).
thf(f52,plain,
! [X0: a,X1: a] :
( ( sK1 @ X0 @ ( sK0 @ X0 @ X1 ) )
= X0 ),
inference(constrained_superposition,[],[f28,f18]) ).
thf(f65,plain,
! [X2: a,X0: a,X1: a] :
( ( sK1 @ X0 @ X2 )
= ( sK1 @ X0 @ ( sK1 @ ( sK0 @ X1 @ X0 ) @ X2 ) ) ),
inference(constrained_superposition,[],[f15,f28]) ).
thf(f94,plain,
! [X2: a,X0: a,X1: a] :
( ( sK0 @ X0 @ ( sK0 @ ( sK1 @ X1 @ X0 ) @ X2 ) )
= ( sK0 @ X0 @ X2 ) ),
inference(constrained_superposition,[],[f17,f48]) ).
thf(f130,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK0 @ X1 @ ( sK1 @ X2 @ X0 ) )
= ( sK1 @ ( sK0 @ X1 @ X2 ) @ ( sK0 @ X0 @ X1 ) ) )
| ~ spl8_2 ),
inference(constrained_superposition,[],[f26,f18]) ).
thf(f138,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK0 @ X1 @ ( sK1 @ X0 @ X2 ) )
= ( sK1 @ ( sK0 @ X0 @ X1 ) @ ( sK0 @ X1 @ X2 ) ) )
| ~ spl8_2 ),
inference(constrained_superposition,[],[f26,f18]) ).
thf(f1465,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK1 @ X1 @ ( sK0 @ X2 @ X0 ) )
= ( sK1 @ X1 @ ( sK0 @ X0 @ ( sK1 @ X1 @ X2 ) ) ) )
| ~ spl8_2 ),
inference(constrained_superposition,[],[f65,f130]) ).
thf(f1705,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK1 @ X0 @ ( sK0 @ ( sK1 @ X0 @ X1 ) @ X2 ) )
= ( sK0 @ ( sK1 @ X0 @ X1 ) @ ( sK1 @ X0 @ X2 ) ) )
| ~ spl8_2 ),
inference(constrained_superposition,[],[f138,f45]) ).
thf(f1772,plain,
( ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK1 @ sK7 @ ( sK0 @ ( sK1 @ sK7 @ sK5 ) @ sK6 ) ) )
| ~ spl8_2
| spl8_3 ),
inference(backward_demodulation,[],[f33,f1705]) ).
thf(f1821,plain,
( ( ( sK1 @ sK7 @ ( sK0 @ sK6 @ ( sK1 @ sK7 @ sK5 ) ) )
!= ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) ) )
| ~ spl8_2
| spl8_3 ),
inference(forward_demodulation,[],[f1772,f18]) ).
thf(f1848,plain,
( $false
| ~ spl8_2
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f1821,f1465]) ).
thf(f1849,plain,
( ~ spl8_2
| spl8_3 ),
inference(avatar_contradiction_clause,[],[f1848]) ).
thf(f1878,plain,
( ( ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) )
!= ( sK1 @ sK7 @ ( sK0 @ sK5 @ sK6 ) ) )
| ~ spl8_1
| spl8_3 ),
inference(backward_demodulation,[],[f33,f23]) ).
thf(f1879,plain,
( $false
| ~ spl8_1
| spl8_3 ),
inference(trivial_inequality_removal,[],[f1878]) ).
thf(f1880,plain,
( ~ spl8_1
| spl8_3 ),
inference(avatar_contradiction_clause,[],[f1879]) ).
thf(f1954,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK1 @ X1 @ ( sK0 @ X2 @ X0 ) )
= ( sK0 @ ( sK1 @ X1 @ X2 ) @ ( sK1 @ X0 @ X1 ) ) )
| ~ spl8_1 ),
inference(constrained_superposition,[],[f23,f12]) ).
thf(f1970,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK1 @ X1 @ ( sK0 @ X0 @ X2 ) )
= ( sK0 @ ( sK1 @ X0 @ X1 ) @ ( sK1 @ X1 @ X2 ) ) )
| ~ spl8_1 ),
inference(constrained_superposition,[],[f23,f12]) ).
thf(f2404,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK0 @ X1 @ ( sK1 @ X2 @ X0 ) )
= ( sK0 @ X1 @ ( sK1 @ X0 @ ( sK0 @ X1 @ X2 ) ) ) )
| ~ spl8_1 ),
inference(constrained_superposition,[],[f94,f1954]) ).
thf(f2646,plain,
( ! [X2: a,X0: a,X1: a] :
( ( sK1 @ ( sK0 @ X0 @ X1 ) @ ( sK0 @ X0 @ X2 ) )
= ( sK0 @ X0 @ ( sK1 @ ( sK0 @ X0 @ X1 ) @ X2 ) ) )
| ~ spl8_1 ),
inference(constrained_superposition,[],[f1970,f52]) ).
thf(f2725,plain,
( ( ( sK0 @ sK4 @ ( sK1 @ ( sK0 @ sK4 @ sK3 ) @ sK2 ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) ) )
| ~ spl8_1
| spl8_4 ),
inference(backward_demodulation,[],[f37,f2646]) ).
thf(f2762,plain,
( ( ( sK0 @ sK4 @ ( sK1 @ sK2 @ ( sK0 @ sK4 @ sK3 ) ) )
!= ( sK0 @ sK4 @ ( sK1 @ sK3 @ sK2 ) ) )
| ~ spl8_1
| spl8_4 ),
inference(forward_demodulation,[],[f2725,f12]) ).
thf(f2791,plain,
( $false
| ~ spl8_1
| spl8_4 ),
inference(forward_subsumption_resolution,[],[f2762,f2404]) ).
thf(f2792,plain,
( ~ spl8_1
| spl8_4 ),
inference(avatar_contradiction_clause,[],[f2791]) ).
cnf(s1,plain,
( spl8_1
| spl8_2 ),
inference(sat_conversion,[],[f27]) ).
cnf(s2,plain,
( ~ spl8_3
| ~ spl8_4 ),
inference(sat_conversion,[],[f38]) ).
cnf(s3,plain,
( ~ spl8_2
| spl8_4 ),
inference(sat_conversion,[],[f41]) ).
cnf(s4,plain,
( ~ spl8_2
| spl8_3 ),
inference(sat_conversion,[],[f1849]) ).
cnf(s5,plain,
( ~ spl8_1
| spl8_3 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s6,plain,
( ~ spl8_1
| spl8_4 ),
inference(sat_conversion,[],[f2792]) ).
cnf(s7,plain,
~ spl8_2,
inference(rat,[],[s2,s3,s4]) ).
cnf(s8,plain,
spl8_1,
inference(rat,[],[s1,s7]) ).
cnf(s9,plain,
spl8_4,
inference(rat,[],[s6,s8]) ).
cnf(s10,plain,
spl8_3,
inference(rat,[],[s5,s8]) ).
cnf(s11,plain,
$false,
inference(rat,[],[s2,s9,s10]) ).
thf(f2813,plain,
$false,
inference(avatar_sat_refutation,[],[s11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV001^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n014.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 14:57:30 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.40 % (2773356)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.82/0.40 % (2773361)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3342476002:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.82/0.40 % (2773362)lrs+10_16_si=on:nwc=1.5:random_seed=1296499043:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.82/0.40 % (2773364)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=2568651334: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.82/0.40 % (2773366)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=739216142:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.82/0.40 % (2773363)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1850086031:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.82/0.40 % (2773361)Instruction limit reached!
% 0.82/0.40 % (2773361)------------------------------
% 0.82/0.40 % (2773361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2773361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2773361)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2773361)Termination reason: Instruction limit
% 0.82/0.40 % (2773361)Termination phase: Saturation
% 0.82/0.40 % (2773361)Time elapsed: 0.023 s
% 0.82/0.40 % (2773361)Peak memory usage: 12 MB
% 0.82/0.40 % (2773361)Instructions burned: 90 (million)
% 0.82/0.40 % (2773363)Instruction limit reached!
% 0.82/0.40 % (2773363)------------------------------
% 0.82/0.40 % (2773363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2773363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2773363)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2773363)Termination reason: Instruction limit
% 0.82/0.40 % (2773363)Termination phase: Saturation
% 0.82/0.40 % (2773363)Time elapsed: 0.004 s
% 0.82/0.40 % (2773363)Peak memory usage: 12 MB
% 0.82/0.40 % (2773363)Instructions burned: 3 (million)
% 0.82/0.40 % (2773367)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.82/0.40 % (2773367)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.82/0.40 % (2773365)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2817183869:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.82/0.40 % (2773362)Instruction limit reached!
% 0.82/0.40 % (2773362)------------------------------
% 0.82/0.40 % (2773362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2773362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2773362)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2773362)Termination reason: Instruction limit
% 0.82/0.40 % (2773362)Termination phase: Saturation
% 0.82/0.40 % (2773362)Time elapsed: 0.021 s
% 0.82/0.40 % (2773362)Peak memory usage: 12 MB
% 0.82/0.40 % (2773362)Instructions burned: 18 (million)
% 0.82/0.40 % (2773367)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=4140394754:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.82/0.40 % (2773373)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3915002185:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.82/0.40 % (2773373)Instruction limit reached!
% 0.82/0.40 % (2773373)------------------------------
% 0.82/0.40 % (2773373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.40 % (2773373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.40 % (2773373)CaDiCaL version: 2.1.3
% 0.82/0.40 % (2773373)Termination reason: Instruction limit
% 0.82/0.40 % (2773373)Termination phase: Saturation
% 0.82/0.40 % (2773373)Time elapsed: 0.002 s
% 0.82/0.40 % (2773373)Peak memory usage: 11 MB
% 0.82/0.40 % (2773373)Instructions burned: 2 (million)
% 0.82/0.40 % (2773376)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.82/0.43 % (2773376)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3623574921:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.82/0.43 % (2773376)Instruction limit reached!
% 0.82/0.43 % (2773376)------------------------------
% 0.82/0.43 % (2773376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.43 % (2773376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.43 % (2773376)CaDiCaL version: 2.1.3
% 0.82/0.43 % (2773376)Termination reason: Instruction limit
% 0.82/0.43 % (2773376)Termination phase: Saturation
% 0.82/0.43 % (2773376)Time elapsed: 0.002 s
% 0.82/0.43 % (2773376)Peak memory usage: 12 MB
% 0.82/0.43 % (2773376)Instructions burned: 8 (million)
% 0.82/0.43 % (2773365)Instruction limit reached!
% 0.82/0.43 % (2773365)------------------------------
% 0.82/0.43 % (2773365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.43 % (2773365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.43 % (2773365)CaDiCaL version: 2.1.3
% 0.82/0.43 % (2773365)Termination reason: Instruction limit
% 0.82/0.43 % (2773365)Termination phase: Saturation
% 0.82/0.43 % (2773365)Time elapsed: 0.021 s
% 0.82/0.43 % (2773365)Peak memory usage: 12 MB
% 0.82/0.43 % (2773365)Instructions burned: 24 (million)
% 0.82/0.43 % (2773374)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=699541835:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.82/0.43 % (2773382)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=3445997138:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.82/0.43 % (2773374)Instruction limit reached!
% 0.82/0.43 % (2773374)------------------------------
% 0.82/0.43 % (2773374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.43 % (2773374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.43 % (2773374)CaDiCaL version: 2.1.3
% 0.82/0.43 % (2773374)Termination reason: Instruction limit
% 0.82/0.43 % (2773374)Termination phase: Saturation
% 0.82/0.43 % (2773374)Time elapsed: 0.006 s
% 0.82/0.43 % (2773374)Peak memory usage: 11 MB
% 0.82/0.43 % (2773374)Instructions burned: 5 (million)
% 0.82/0.43 % (2773379)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=4150006903:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.82/0.43 % (2773366)Instruction limit reached!
% 0.82/0.43 % (2773366)------------------------------
% 0.82/0.43 % (2773366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.43 % (2773366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.43 % (2773366)CaDiCaL version: 2.1.3
% 0.82/0.43 % (2773366)Termination reason: Instruction limit
% 0.82/0.43 % (2773366)Termination phase: Saturation
% 0.82/0.43 % (2773366)Time elapsed: 0.048 s
% 0.82/0.43 % (2773366)Peak memory usage: 13 MB
% 0.82/0.43 % (2773366)Instructions burned: 76 (million)
% 0.82/0.43 % (2773381)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.82/0.43 % (2773381)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.82/0.43 % (2773381)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1534240445:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.82/0.43 % (2773379)Instruction limit reached!
% 0.82/0.43 % (2773379)------------------------------
% 0.82/0.43 % (2773379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.43 % (2773379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.43 % (2773379)CaDiCaL version: 2.1.3
% 0.82/0.43 % (2773379)Termination reason: Instruction limit
% 0.82/0.43 % (2773379)Termination phase: Saturation
% 0.82/0.43 % (2773379)Time elapsed: 0.013 s
% 0.82/0.43 % (2773379)Peak memory usage: 12 MB
% 0.82/0.43 % (2773379)Instructions burned: 12 (million)
% 0.82/0.43 % (2773382)Instruction limit reached!
% 0.82/0.43 % (2773382)------------------------------
% 0.82/0.43 % (2773382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.46 % (2773382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.46 % (2773382)CaDiCaL version: 2.1.3
% 0.82/0.46 % (2773382)Termination reason: Instruction limit
% 0.82/0.46 % (2773382)Termination phase: Saturation
% 0.82/0.46 % (2773382)Time elapsed: 0.023 s
% 0.82/0.46 % (2773382)Peak memory usage: 13 MB
% 0.82/0.46 % (2773382)Instructions burned: 89 (million)
% 0.82/0.46 % (2773390)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1042630183:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.82/0.46 % (2773386)lrs+10_1_si=on:cs=on:random_seed=1663851486:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.82/0.46 % (2773387)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.82/0.46 % (2773381)Instruction limit reached!
% 0.82/0.46 % (2773381)------------------------------
% 0.82/0.46 % (2773381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.46 % (2773381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.46 % (2773381)CaDiCaL version: 2.1.3
% 0.82/0.46 % (2773381)Termination reason: Instruction limit
% 0.82/0.46 % (2773381)Termination phase: Saturation
% 0.82/0.46 % (2773381)Time elapsed: 0.024 s
% 0.82/0.46 % (2773381)Peak memory usage: 12 MB
% 0.82/0.46 % (2773381)Instructions burned: 28 (million)
% 0.82/0.46 % (2773386)Instruction limit reached!
% 0.82/0.46 % (2773386)------------------------------
% 0.82/0.46 % (2773386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.46 % (2773386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.46 % (2773386)CaDiCaL version: 2.1.3
% 0.82/0.46 % (2773386)Termination reason: Instruction limit
% 0.82/0.46 % (2773386)Termination phase: Saturation
% 0.82/0.46 % (2773386)Time elapsed: 0.005 s
% 0.82/0.46 % (2773386)Peak memory usage: 12 MB
% 0.82/0.46 % (2773386)Instructions burned: 8 (million)
% 0.82/0.46 % (2773387)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=1878775338:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.82/0.46 % (2773387)Instruction limit reached!
% 0.82/0.46 % (2773387)------------------------------
% 0.82/0.46 % (2773387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.46 % (2773387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.46 % (2773387)CaDiCaL version: 2.1.3
% 0.82/0.46 % (2773387)Termination reason: Instruction limit
% 0.82/0.46 % (2773387)Termination phase: Saturation
% 0.82/0.46 % (2773387)Time elapsed: 0.002 s
% 0.82/0.46 % (2773387)Peak memory usage: 11 MB
% 0.82/0.46 % (2773387)Instructions burned: 4 (million)
% 0.82/0.46 % (2773389)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=673274023:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 0.82/0.46 % (2773393)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=6517778:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.82/0.46 % (2773394)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=55130785:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.82/0.46 % (2773389)Refutation not found, incomplete strategy
% 0.82/0.46 % (2773389)------------------------------
% 0.82/0.46 % (2773389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.46 % (2773389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.46 % (2773389)CaDiCaL version: 2.1.3
% 0.82/0.46 % (2773389)Termination reason: Refutation not found, incomplete strategy
% 0.82/0.46 % (2773389)Time elapsed: 0.005 s
% 0.82/0.46 % (2773389)Peak memory usage: 12 MB
% 0.82/0.46 % (2773389)Instructions burned: 4 (million)
% 0.82/0.46 % (2773389)------------------------------
% 0.82/0.46 % (2773389)------------------------------
% 0.82/0.46 % (2773394)Instruction limit reached!
% 0.82/0.46 % (2773394)------------------------------
% 0.82/0.46 % (2773394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.82/0.46 % (2773394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.82/0.46 % (2773394)CaDiCaL version: 2.1.3
% 0.82/0.46 % (2773394)Termination reason: Instruction limit
% 1.57/0.52 % (2773394)Termination phase: Saturation
% 1.57/0.52 % (2773394)Time elapsed: 0.009 s
% 1.57/0.52 % (2773394)Peak memory usage: 12 MB
% 1.57/0.52 % (2773394)Instructions burned: 16 (million)
% 1.57/0.52 % (2773396)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3421839539:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.57/0.52 % (2773393)Instruction limit reached!
% 1.57/0.52 % (2773393)------------------------------
% 1.57/0.52 % (2773393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.52 % (2773393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.52 % (2773393)CaDiCaL version: 2.1.3
% 1.57/0.52 % (2773393)Termination reason: Instruction limit
% 1.57/0.52 % (2773393)Termination phase: Saturation
% 1.57/0.52 % (2773393)Time elapsed: 0.014 s
% 1.57/0.52 % (2773393)Peak memory usage: 12 MB
% 1.57/0.52 % (2773393)Instructions burned: 25 (million)
% 1.57/0.52 % (2773367)Instruction limit reached!
% 1.57/0.52 % (2773367)------------------------------
% 1.57/0.52 % (2773367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.52 % (2773400)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=119372401:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.57/0.52 % (2773367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.52 % (2773367)CaDiCaL version: 2.1.3
% 1.57/0.52 % (2773367)Termination reason: Instruction limit
% 1.57/0.52 % (2773367)Termination phase: Saturation
% 1.57/0.52 % (2773367)Time elapsed: 0.107 s
% 1.57/0.52 % (2773367)Peak memory usage: 13 MB
% 1.57/0.52 % (2773367)Instructions burned: 159 (million)
% 1.57/0.52 % (2773400)Instruction limit reached!
% 1.57/0.52 % (2773400)------------------------------
% 1.57/0.52 % (2773400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.52 % (2773400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.52 % (2773400)CaDiCaL version: 2.1.3
% 1.57/0.52 % (2773400)Termination reason: Instruction limit
% 1.57/0.52 % (2773400)Termination phase: Saturation
% 1.57/0.52 % (2773400)Time elapsed: 0.008 s
% 1.57/0.52 % (2773400)Peak memory usage: 12 MB
% 1.57/0.52 % (2773400)Instructions burned: 14 (million)
% 1.57/0.52 % (2773403)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2463054238:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.57/0.52 % (2773402)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1883268294:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.57/0.52 % (2773402)Instruction limit reached!
% 1.57/0.52 % (2773402)------------------------------
% 1.57/0.52 % (2773402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.52 % (2773402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.52 % (2773402)CaDiCaL version: 2.1.3
% 1.57/0.52 % (2773402)Termination reason: Instruction limit
% 1.57/0.52 % (2773402)Termination phase: Saturation
% 1.57/0.52 % (2773402)Time elapsed: 0.002 s
% 1.57/0.52 % (2773402)Peak memory usage: 11 MB
% 1.57/0.52 % (2773402)Instructions burned: 3 (million)
% 1.57/0.52 % (2773405)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2368990557:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.57/0.52 % (2773390)Instruction limit reached!
% 1.57/0.52 % (2773390)------------------------------
% 1.57/0.52 % (2773390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.52 % (2773390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.52 % (2773390)CaDiCaL version: 2.1.3
% 1.57/0.52 % (2773390)Termination reason: Instruction limit
% 1.57/0.52 % (2773390)Termination phase: Saturation
% 1.57/0.52 % (2773390)Time elapsed: 0.066 s
% 1.57/0.52 % (2773390)Peak memory usage: 13 MB
% 1.57/0.52 % (2773390)Instructions burned: 251 (million)
% 1.57/0.52 % (2773403)Instruction limit reached!
% 1.57/0.52 % (2773403)------------------------------
% 1.57/0.52 % (2773403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.52 % (2773403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.52 % (2773403)CaDiCaL version: 2.1.3
% 1.57/0.52 % (2773403)Termination reason: Instruction limit
% 1.57/0.52 % (2773403)Termination phase: Saturation
% 1.57/0.52 % (2773403)Time elapsed: 0.015 s
% 2.18/0.61 % (2773403)Peak memory usage: 12 MB
% 2.18/0.61 % (2773403)Instructions burned: 26 (million)
% 2.18/0.61 % (2773406)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1504468357:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.18/0.61 % (2773409)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.18/0.61 % (2773409)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.18/0.61 % (2773411)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.18/0.61 % (2773409)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=3548230819:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.18/0.61 % (2773405)Instruction limit reached!
% 2.18/0.61 % (2773405)------------------------------
% 2.18/0.61 % (2773405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.18/0.61 % (2773405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.18/0.61 % (2773405)CaDiCaL version: 2.1.3
% 2.18/0.61 % (2773405)Termination reason: Instruction limit
% 2.18/0.61 % (2773405)Termination phase: Saturation
% 2.18/0.61 % (2773405)Time elapsed: 0.013 s
% 2.18/0.61 % (2773405)Peak memory usage: 11 MB
% 2.18/0.61 % (2773405)Instructions burned: 25 (million)
% 2.18/0.61 % (2773411)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=190337639:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.18/0.61 % (2773412)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=3542041409:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.18/0.61 % (2773409)Instruction limit reached!
% 2.18/0.61 % (2773409)------------------------------
% 2.18/0.61 % (2773409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.18/0.61 % (2773409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.18/0.61 % (2773409)CaDiCaL version: 2.1.3
% 2.18/0.61 % (2773409)Termination reason: Instruction limit
% 2.18/0.61 % (2773409)Termination phase: Saturation
% 2.18/0.61 % (2773409)Time elapsed: 0.008 s
% 2.18/0.61 % (2773409)Peak memory usage: 12 MB
% 2.18/0.61 % (2773409)Instructions burned: 14 (million)
% 2.18/0.61 % (2773411)Instruction limit reached!
% 2.18/0.61 % (2773411)------------------------------
% 2.18/0.61 % (2773411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.18/0.61 % (2773411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.18/0.61 % (2773411)CaDiCaL version: 2.1.3
% 2.18/0.61 % (2773411)Termination reason: Instruction limit
% 2.18/0.61 % (2773411)Termination phase: Saturation
% 2.18/0.61 % (2773411)Time elapsed: 0.008 s
% 2.18/0.61 % (2773411)Peak memory usage: 12 MB
% 2.18/0.61 % (2773411)Instructions burned: 8 (million)
% 2.18/0.61 % (2773412)Instruction limit reached!
% 2.18/0.61 % (2773412)------------------------------
% 2.18/0.61 % (2773412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.18/0.61 % (2773412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.18/0.61 % (2773412)CaDiCaL version: 2.1.3
% 2.18/0.61 % (2773412)Termination reason: Instruction limit
% 2.18/0.61 % (2773412)Termination phase: Saturation
% 2.18/0.61 % (2773412)Time elapsed: 0.008 s
% 2.18/0.61 % (2773412)Peak memory usage: 12 MB
% 2.18/0.61 % (2773412)Instructions burned: 31 (million)
% 2.18/0.61 % (2773415)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=976474346:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.18/0.61 % (2773415)Instruction limit reached!
% 2.18/0.61 % (2773415)------------------------------
% 2.18/0.61 % (2773415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.18/0.61 % (2773415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.18/0.61 % (2773415)CaDiCaL version: 2.1.3
% 2.18/0.61 % (2773415)Termination reason: Instruction limit
% 2.18/0.61 % (2773415)Termination phase: Saturation
% 2.18/0.61 % (2773415)Time elapsed: 0.004 s
% 2.46/0.69 % (2773415)Peak memory usage: 12 MB
% 2.46/0.69 % (2773415)Instructions burned: 7 (million)
% 2.46/0.69 % (2773419)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=247717570:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.46/0.69 % (2773418)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4045615865:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.46/0.69 % (2773419)Instruction limit reached!
% 2.46/0.69 % (2773419)------------------------------
% 2.46/0.69 % (2773419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (2773419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (2773419)CaDiCaL version: 2.1.3
% 2.46/0.69 % (2773419)Termination reason: Instruction limit
% 2.46/0.69 % (2773419)Termination phase: Saturation
% 2.46/0.69 % (2773419)Time elapsed: 0.006 s
% 2.46/0.69 % (2773419)Peak memory usage: 12 MB
% 2.46/0.69 % (2773419)Instructions burned: 22 (million)
% 2.46/0.69 % (2773418)Instruction limit reached!
% 2.46/0.69 % (2773418)------------------------------
% 2.46/0.69 % (2773418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (2773418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (2773418)CaDiCaL version: 2.1.3
% 2.46/0.69 % (2773418)Termination reason: Instruction limit
% 2.46/0.69 % (2773418)Termination phase: Saturation
% 2.46/0.69 % (2773418)Time elapsed: 0.009 s
% 2.46/0.69 % (2773418)Peak memory usage: 11 MB
% 2.46/0.69 % (2773418)Instructions burned: 23 (million)
% 2.46/0.69 % (2773420)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3429249914:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.46/0.69 % (2773406)Instruction limit reached!
% 2.46/0.69 % (2773406)------------------------------
% 2.46/0.69 % (2773406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (2773406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (2773406)CaDiCaL version: 2.1.3
% 2.46/0.69 % (2773406)Termination reason: Instruction limit
% 2.46/0.69 % (2773406)Termination phase: Saturation
% 2.46/0.69 % (2773406)Time elapsed: 0.046 s
% 2.46/0.69 % (2773406)Peak memory usage: 12 MB
% 2.46/0.69 % (2773406)Instructions burned: 60 (million)
% 2.46/0.69 % (2773425)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3379312178:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.46/0.69 % (2773426)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1845166979:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.46/0.69 % (2773428)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.46/0.69 % (2773428)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1267254426:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.46/0.69 % (2773424)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2243072285:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.46/0.69 % (2773428)Instruction limit reached!
% 2.46/0.69 % (2773428)------------------------------
% 2.46/0.69 % (2773428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (2773428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (2773428)CaDiCaL version: 2.1.3
% 2.46/0.69 % (2773428)Termination reason: Instruction limit
% 2.46/0.69 % (2773428)Termination phase: Saturation
% 2.46/0.69 % (2773428)Time elapsed: 0.004 s
% 2.46/0.69 % (2773428)Peak memory usage: 12 MB
% 2.46/0.69 % (2773428)Instructions burned: 8 (million)
% 2.46/0.69 % (2773426)Instruction limit reached!
% 2.46/0.69 % (2773426)------------------------------
% 2.46/0.69 % (2773426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (2773426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (2773426)CaDiCaL version: 2.1.3
% 2.46/0.69 % (2773426)Termination reason: Instruction limit
% 2.46/0.69 % (2773426)Termination phase: Saturation
% 2.46/0.69 % (2773426)Time elapsed: 0.022 s
% 2.46/0.69 % (2773426)Peak memory usage: 12 MB
% 2.46/0.69 % (2773426)Instructions burned: 43 (million)
% 2.46/0.69 % (2773433)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=762515044:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.69/0.77 % (2773434)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=1333852869:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.69/0.77 % (2773396)Instruction limit reached!
% 2.69/0.77 % (2773396)------------------------------
% 2.69/0.77 % (2773396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2773396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2773396)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2773396)Termination reason: Instruction limit
% 2.69/0.77 % (2773396)Termination phase: Saturation
% 2.69/0.77 % (2773396)Time elapsed: 0.152 s
% 2.69/0.77 % (2773396)Peak memory usage: 14 MB
% 2.69/0.77 % (2773396)Instructions burned: 333 (million)
% 2.69/0.77 % (2773437)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.69/0.77 % (2773437)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2046921261:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 2.69/0.77 % (2773437)Instruction limit reached!
% 2.69/0.77 % (2773437)------------------------------
% 2.69/0.77 % (2773437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2773437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2773437)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2773437)Termination reason: Instruction limit
% 2.69/0.77 % (2773437)Termination phase: Saturation
% 2.69/0.77 % (2773437)Time elapsed: 0.003 s
% 2.69/0.77 % (2773437)Peak memory usage: 12 MB
% 2.69/0.77 % (2773437)Instructions burned: 6 (million)
% 2.69/0.77 % (2773425)Instruction limit reached!
% 2.69/0.77 % (2773425)------------------------------
% 2.69/0.77 % (2773425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2773425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2773425)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2773425)Termination reason: Instruction limit
% 2.69/0.77 % (2773425)Termination phase: Saturation
% 2.69/0.77 % (2773425)Time elapsed: 0.092 s
% 2.69/0.77 % (2773425)Peak memory usage: 13 MB
% 2.69/0.77 % (2773425)Instructions burned: 194 (million)
% 2.69/0.77 % (2773424)Instruction limit reached!
% 2.69/0.77 % (2773424)------------------------------
% 2.69/0.77 % (2773424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2773424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2773424)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2773424)Termination reason: Instruction limit
% 2.69/0.77 % (2773424)Termination phase: Saturation
% 2.69/0.77 % (2773424)Time elapsed: 0.084 s
% 2.69/0.77 % (2773424)Peak memory usage: 13 MB
% 2.69/0.77 % (2773424)Instructions burned: 143 (million)
% 2.69/0.77 % (2773439)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1234183013:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.69/0.77 % (2773440)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1457538175:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.69/0.77 % (2773439)Instruction limit reached!
% 2.69/0.77 % (2773439)------------------------------
% 2.69/0.77 % (2773439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2773439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2773439)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2773439)Termination reason: Instruction limit
% 2.69/0.77 % (2773439)Termination phase: Saturation
% 2.69/0.77 % (2773439)Time elapsed: 0.012 s
% 2.69/0.77 % (2773439)Peak memory usage: 12 MB
% 2.69/0.77 % (2773439)Instructions burned: 24 (million)
% 2.69/0.77 % (2773441)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=3018547982:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.69/0.77 % (2773440)Instruction limit reached!
% 2.69/0.77 % (2773440)------------------------------
% 2.69/0.77 % (2773440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.89 % (2773440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.89 % (2773440)CaDiCaL version: 2.1.3
% 3.24/0.89 % (2773440)Termination reason: Instruction limit
% 3.24/0.89 % (2773440)Termination phase: Saturation
% 3.24/0.89 % (2773440)Time elapsed: 0.011 s
% 3.24/0.89 % (2773440)Peak memory usage: 13 MB
% 3.24/0.89 % (2773440)Instructions burned: 20 (million)
% 3.24/0.89 % (2773434)Instruction limit reached!
% 3.24/0.89 % (2773434)------------------------------
% 3.24/0.89 % (2773434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.89 % (2773434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.89 % (2773434)CaDiCaL version: 2.1.3
% 3.24/0.89 % (2773434)Termination reason: Instruction limit
% 3.24/0.89 % (2773434)Termination phase: Saturation
% 3.24/0.89 % (2773434)Time elapsed: 0.081 s
% 3.24/0.89 % (2773434)Peak memory usage: 13 MB
% 3.24/0.89 % (2773434)Instructions burned: 175 (million)
% 3.24/0.89 % (2773433)Instruction limit reached!
% 3.24/0.89 % (2773433)------------------------------
% 3.24/0.89 % (2773433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.89 % (2773433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.89 % (2773433)CaDiCaL version: 2.1.3
% 3.24/0.89 % (2773433)Termination reason: Instruction limit
% 3.24/0.89 % (2773433)Termination phase: Saturation
% 3.24/0.89 % (2773433)Time elapsed: 0.094 s
% 3.24/0.89 % (2773433)Peak memory usage: 13 MB
% 3.24/0.89 % (2773433)Instructions burned: 186 (million)
% 3.24/0.89 % (2773444)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=1984524386:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.24/0.89 % (2773446)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=2891349158:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.24/0.89 % (2773447)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=611013091:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.24/0.89 % (2773448)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3993153279:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.24/0.89 % (2773448)Instruction limit reached!
% 3.24/0.89 % (2773448)------------------------------
% 3.24/0.89 % (2773448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.89 % (2773448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.89 % (2773448)CaDiCaL version: 2.1.3
% 3.24/0.89 % (2773448)Termination reason: Instruction limit
% 3.24/0.89 % (2773448)Termination phase: Saturation
% 3.24/0.89 % (2773448)Time elapsed: 0.012 s
% 3.24/0.89 % (2773448)Peak memory usage: 12 MB
% 3.24/0.89 % (2773448)Instructions burned: 22 (million)
% 3.24/0.89 % (2773446)Instruction limit reached!
% 3.24/0.89 % (2773446)------------------------------
% 3.24/0.89 % (2773446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.89 % (2773446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.89 % (2773446)CaDiCaL version: 2.1.3
% 3.24/0.89 % (2773446)Termination reason: Instruction limit
% 3.24/0.89 % (2773446)Termination phase: Saturation
% 3.24/0.89 % (2773446)Time elapsed: 0.026 s
% 3.24/0.89 % (2773446)Peak memory usage: 12 MB
% 3.24/0.89 % (2773446)Instructions burned: 47 (million)
% 3.24/0.89 % (2773453)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.24/0.89 % (2773453)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1624167538:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.24/0.89 % (2773454)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2500661929:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.24/0.89 % (2773364)Instruction limit reached!
% 3.24/0.89 % (2773364)------------------------------
% 3.24/0.89 % (2773364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.89 % (2773364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773364)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773364)Termination reason: Instruction limit
% 5.30/1.04 % (2773364)Termination phase: Saturation
% 5.30/1.04 % (2773364)Time elapsed: 0.400 s
% 5.30/1.04 % (2773364)Peak memory usage: 15 MB
% 5.30/1.04 % (2773364)Instructions burned: 634 (million)
% 5.30/1.04 % (2773454)Instruction limit reached!
% 5.30/1.04 % (2773454)------------------------------
% 5.30/1.04 % (2773454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.04 % (2773454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773454)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773454)Termination reason: Instruction limit
% 5.30/1.04 % (2773454)Termination phase: Saturation
% 5.30/1.04 % (2773454)Time elapsed: 0.008 s
% 5.30/1.04 % (2773454)Peak memory usage: 12 MB
% 5.30/1.04 % (2773454)Instructions burned: 13 (million)
% 5.30/1.04 % (2773457)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=1359693279:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 5.30/1.04 % (2773458)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2440349282:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 5.30/1.04 % (2773458)Instruction limit reached!
% 5.30/1.04 % (2773458)------------------------------
% 5.30/1.04 % (2773458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.04 % (2773458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773458)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773458)Termination reason: Instruction limit
% 5.30/1.04 % (2773458)Termination phase: Saturation
% 5.30/1.04 % (2773458)Time elapsed: 0.026 s
% 5.30/1.04 % (2773458)Peak memory usage: 12 MB
% 5.30/1.04 % (2773458)Instructions burned: 52 (million)
% 5.30/1.04 % (2773457)Instruction limit reached!
% 5.30/1.04 % (2773457)------------------------------
% 5.30/1.04 % (2773457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.04 % (2773457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773457)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773457)Termination reason: Instruction limit
% 5.30/1.04 % (2773457)Termination phase: Saturation
% 5.30/1.04 % (2773457)Time elapsed: 0.034 s
% 5.30/1.04 % (2773457)Peak memory usage: 13 MB
% 5.30/1.04 % (2773457)Instructions burned: 67 (million)
% 5.30/1.04 % (2773461)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3422559330:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 5.30/1.04 % (2773462)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3601894639:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 5.30/1.04 % (2773453)Instruction limit reached!
% 5.30/1.04 % (2773453)------------------------------
% 5.30/1.04 % (2773453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.04 % (2773453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773453)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773453)Termination reason: Instruction limit
% 5.30/1.04 % (2773453)Termination phase: Saturation
% 5.30/1.04 % (2773453)Time elapsed: 0.091 s
% 5.30/1.04 % (2773453)Peak memory usage: 12 MB
% 5.30/1.04 % (2773453)Instructions burned: 200 (million)
% 5.30/1.04 % (2773441)Instruction limit reached!
% 5.30/1.04 % (2773441)------------------------------
% 5.30/1.04 % (2773441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.04 % (2773441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773441)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773441)Termination reason: Instruction limit
% 5.30/1.04 % (2773441)Termination phase: Saturation
% 5.30/1.04 % (2773441)Time elapsed: 0.159 s
% 5.30/1.04 % (2773441)Peak memory usage: 14 MB
% 5.30/1.04 % (2773441)Instructions burned: 316 (million)
% 5.30/1.04 % (2773461)Instruction limit reached!
% 5.30/1.04 % (2773461)------------------------------
% 5.30/1.04 % (2773461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.04 % (2773461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.04 % (2773461)CaDiCaL version: 2.1.3
% 5.30/1.04 % (2773461)Termination reason: Instruction limit
% 5.30/1.04 % (2773461)Termination phase: Saturation
% 5.30/1.12 % (2773461)Time elapsed: 0.016 s
% 5.30/1.12 % (2773461)Peak memory usage: 12 MB
% 5.30/1.12 % (2773461)Instructions burned: 31 (million)
% 5.30/1.12 % (2773465)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=3531958286:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 5.30/1.12 % (2773466)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3396644044:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2994 on theBenchmark for (2994ds/67Mi)
% 5.30/1.12 % (2773467)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.30/1.12 % (2773467)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2056077522:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.30/1.12 % (2773465)Instruction limit reached!
% 5.30/1.12 % (2773465)------------------------------
% 5.30/1.12 % (2773465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.12 % (2773465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.12 % (2773465)CaDiCaL version: 2.1.3
% 5.30/1.12 % (2773465)Termination reason: Instruction limit
% 5.30/1.12 % (2773465)Termination phase: Saturation
% 5.30/1.12 % (2773465)Time elapsed: 0.019 s
% 5.30/1.12 % (2773465)Peak memory usage: 12 MB
% 5.30/1.12 % (2773465)Instructions burned: 34 (million)
% 5.30/1.12 % (2773466)Instruction limit reached!
% 5.30/1.12 % (2773466)------------------------------
% 5.30/1.12 % (2773466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.12 % (2773466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.12 % (2773466)CaDiCaL version: 2.1.3
% 5.30/1.12 % (2773466)Termination reason: Instruction limit
% 5.30/1.12 % (2773466)Termination phase: Saturation
% 5.30/1.12 % (2773466)Time elapsed: 0.034 s
% 5.30/1.12 % (2773466)Peak memory usage: 12 MB
% 5.30/1.12 % (2773466)Instructions burned: 67 (million)
% 5.30/1.12 % (2773462)Instruction limit reached!
% 5.30/1.12 % (2773462)------------------------------
% 5.30/1.12 % (2773462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.12 % (2773462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.12 % (2773462)CaDiCaL version: 2.1.3
% 5.30/1.12 % (2773462)Termination reason: Instruction limit
% 5.30/1.12 % (2773462)Termination phase: Saturation
% 5.30/1.12 % (2773462)Time elapsed: 0.069 s
% 5.30/1.12 % (2773462)Peak memory usage: 12 MB
% 5.30/1.12 % (2773462)Instructions burned: 138 (million)
% 5.30/1.12 % (2773471)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3385948556:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.30/1.12 % (2773472)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1252570435:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.30/1.12 % (2773473)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1316130003:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.30/1.12 % (2773447)Instruction limit reached!
% 5.30/1.12 % (2773447)------------------------------
% 5.30/1.12 % (2773447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.12 % (2773447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.12 % (2773447)CaDiCaL version: 2.1.3
% 5.30/1.12 % (2773447)Termination reason: Instruction limit
% 5.30/1.12 % (2773447)Termination phase: Saturation
% 5.30/1.12 % (2773447)Time elapsed: 0.222 s
% 5.30/1.12 % (2773447)Peak memory usage: 14 MB
% 5.30/1.12 % (2773447)Instructions burned: 480 (million)
% 5.30/1.12 % (2773467)Instruction limit reached!
% 5.30/1.12 % (2773467)------------------------------
% 5.30/1.12 % (2773467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.30/1.12 % (2773467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.30/1.12 % (2773467)CaDiCaL version: 2.1.3
% 5.30/1.12 % (2773467)Termination reason: Instruction limit
% 5.30/1.12 % (2773467)Termination phase: Saturation
% 5.30/1.12 % (2773467)Time elapsed: 0.083 s
% 5.30/1.12 % (2773467)Peak memory usage: 13 MB
% 5.30/1.12 % (2773467)Instructions burned: 181 (million)
% 5.30/1.12 % (2773477)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3678962635:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/874Mi)
% 5.30/1.12 % (2773472)Instruction limit reached!
% 5.30/1.12 % (2773472)------------------------------
% 5.80/1.20 % (2773472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.80/1.20 % (2773472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.20 % (2773472)CaDiCaL version: 2.1.3
% 5.80/1.20 % (2773472)Termination reason: Instruction limit
% 5.80/1.20 % (2773472)Termination phase: Saturation
% 5.80/1.20 % (2773472)Time elapsed: 0.053 s
% 5.80/1.20 % (2773472)Peak memory usage: 13 MB
% 5.80/1.20 % (2773472)Instructions burned: 97 (million)
% 5.80/1.20 % (2773478)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2238194937:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/515Mi)
% 5.80/1.20 % (2773480)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=4097565575:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 5.80/1.20 % (2773471)Instruction limit reached!
% 5.80/1.20 % (2773471)------------------------------
% 5.80/1.20 % (2773471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.80/1.20 % (2773471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.20 % (2773471)CaDiCaL version: 2.1.3
% 5.80/1.20 % (2773471)Termination reason: Instruction limit
% 5.80/1.20 % (2773471)Termination phase: Saturation
% 5.80/1.20 % (2773471)Time elapsed: 0.127 s
% 5.80/1.20 % (2773471)Peak memory usage: 13 MB
% 5.80/1.20 % (2773471)Instructions burned: 246 (million)
% 5.80/1.20 % (2773480)Instruction limit reached!
% 5.80/1.20 % (2773480)------------------------------
% 5.80/1.20 % (2773480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.80/1.20 % (2773480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.20 % (2773480)CaDiCaL version: 2.1.3
% 5.80/1.20 % (2773480)Termination reason: Instruction limit
% 5.80/1.20 % (2773480)Termination phase: Saturation
% 5.80/1.20 % (2773480)Time elapsed: 0.064 s
% 5.80/1.20 % (2773480)Peak memory usage: 13 MB
% 5.80/1.20 % (2773480)Instructions burned: 131 (million)
% 5.80/1.20 % (2773483)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4283707941:i=44:ep=R:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/44Mi)
% 5.80/1.20 % (2773484)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2413461935:s2a=on:i=571:nm=16:rtra=on_2992 on theBenchmark for (2992ds/571Mi)
% 6.05/1.20 % (2773484)Refutation not found, incomplete strategy
% 6.05/1.20 % (2773484)------------------------------
% 6.05/1.20 % (2773484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.20 % (2773484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.20 % (2773484)CaDiCaL version: 2.1.3
% 6.05/1.20 % (2773484)Termination reason: Refutation not found, incomplete strategy
% 6.05/1.20 % (2773484)Time elapsed: 0.002 s
% 6.05/1.20 % (2773484)Peak memory usage: 12 MB
% 6.05/1.20 % (2773484)Instructions burned: 3 (million)
% 6.05/1.20 % (2773484)------------------------------
% 6.05/1.20 % (2773484)------------------------------
% 6.05/1.20 % (2773483)Instruction limit reached!
% 6.05/1.20 % (2773483)------------------------------
% 6.05/1.20 % (2773483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.20 % (2773483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.20 % (2773483)CaDiCaL version: 2.1.3
% 6.05/1.20 % (2773483)Termination reason: Instruction limit
% 6.05/1.20 % (2773483)Termination phase: Saturation
% 6.05/1.20 % (2773483)Time elapsed: 0.027 s
% 6.05/1.20 % (2773483)Peak memory usage: 12 MB
% 6.05/1.20 % (2773483)Instructions burned: 44 (million)
% 6.05/1.20 % (2773487)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=951440264:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 6.05/1.20 % (2773420)Instruction limit reached!
% 6.05/1.20 % (2773420)------------------------------
% 6.05/1.20 % (2773420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.20 % (2773420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.20 % (2773420)CaDiCaL version: 2.1.3
% 6.05/1.20 % (2773420)Termination reason: Instruction limit
% 6.05/1.20 % (2773420)Termination phase: Saturation
% 6.05/1.20 % (2773420)Time elapsed: 0.543 s
% 6.05/1.20 % (2773420)Peak memory usage: 15 MB
% 6.05/1.20 % (2773420)Instructions burned: 1240 (million)
% 6.05/1.20 % (2773488)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3072760163:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.51/1.35 % (2773490)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=4204639526:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 6.51/1.35 % (2773473)Instruction limit reached!
% 6.51/1.35 % (2773473)------------------------------
% 6.51/1.35 % (2773473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.51/1.35 % (2773473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.51/1.35 % (2773473)CaDiCaL version: 2.1.3
% 6.51/1.35 % (2773473)Termination reason: Instruction limit
% 6.51/1.35 % (2773473)Termination phase: Saturation
% 6.51/1.35 % (2773473)Time elapsed: 0.199 s
% 6.51/1.35 % (2773473)Peak memory usage: 14 MB
% 6.51/1.35 % (2773473)Instructions burned: 429 (million)
% 6.51/1.35 % (2773444)Instruction limit reached!
% 6.51/1.35 % (2773444)------------------------------
% 6.51/1.35 % (2773444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.51/1.35 % (2773444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.51/1.35 % (2773444)CaDiCaL version: 2.1.3
% 6.51/1.35 % (2773444)Termination reason: Instruction limit
% 6.51/1.35 % (2773444)Termination phase: Saturation
% 6.51/1.35 % (2773444)Time elapsed: 0.434 s
% 6.51/1.35 % (2773444)Peak memory usage: 16 MB
% 6.51/1.35 % (2773444)Instructions burned: 853 (million)
% 6.51/1.35 % (2773493)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=461683966: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_2991 on theBenchmark for (2991ds/105Mi)
% 6.51/1.35 % (2773490)Instruction limit reached!
% 6.51/1.35 % (2773490)------------------------------
% 6.51/1.35 % (2773490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.51/1.35 % (2773490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.51/1.35 % (2773490)CaDiCaL version: 2.1.3
% 6.51/1.35 % (2773490)Termination reason: Instruction limit
% 6.51/1.35 % (2773490)Termination phase: Saturation
% 6.51/1.35 % (2773490)Time elapsed: 0.035 s
% 6.51/1.35 % (2773490)Peak memory usage: 12 MB
% 6.51/1.35 % (2773490)Instructions burned: 66 (million)
% 6.51/1.35 % (2773494)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=3527904725:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2991 on theBenchmark for (2991ds/5755Mi)
% 6.51/1.35 % (2773488)Instruction limit reached!
% 6.51/1.35 % (2773488)------------------------------
% 6.51/1.35 % (2773488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.51/1.35 % (2773488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.51/1.35 % (2773488)CaDiCaL version: 2.1.3
% 6.51/1.35 % (2773488)Termination reason: Instruction limit
% 6.51/1.35 % (2773488)Termination phase: Saturation
% 6.51/1.35 % (2773488)Time elapsed: 0.048 s
% 6.51/1.35 % (2773488)Peak memory usage: 12 MB
% 6.51/1.35 % (2773488)Instructions burned: 95 (million)
% 6.51/1.35 % (2773497)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3582215602:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/375Mi)
% 6.51/1.35 % (2773497)Refutation not found, incomplete strategy
% 6.51/1.35 % (2773497)------------------------------
% 6.51/1.35 % (2773497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.51/1.35 % (2773497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.51/1.35 % (2773497)CaDiCaL version: 2.1.3
% 6.51/1.35 % (2773497)Termination reason: Refutation not found, incomplete strategy
% 6.51/1.35 % (2773497)Time elapsed: 0.003 s
% 6.51/1.35 % (2773497)Peak memory usage: 12 MB
% 6.51/1.35 % (2773497)Instructions burned: 4 (million)
% 6.51/1.35 % (2773497)------------------------------
% 6.51/1.35 % (2773497)------------------------------
% 6.51/1.35 % (2773498)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=963620468:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 6.51/1.35 % (2773493)Instruction limit reached!
% 6.51/1.35 % (2773493)------------------------------
% 6.51/1.35 % (2773493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.34/1.49 % (2773493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.49 % (2773493)CaDiCaL version: 2.1.3
% 7.34/1.49 % (2773493)Termination reason: Instruction limit
% 7.34/1.49 % (2773493)Termination phase: Saturation
% 7.34/1.49 % (2773493)Time elapsed: 0.052 s
% 7.34/1.49 % (2773493)Peak memory usage: 13 MB
% 7.34/1.49 % (2773493)Instructions burned: 107 (million)
% 7.34/1.49 % (2773500)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=3614685789:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 7.34/1.49 % (2773478)Instruction limit reached!
% 7.34/1.49 % (2773478)------------------------------
% 7.34/1.49 % (2773478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.34/1.49 % (2773478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.49 % (2773478)CaDiCaL version: 2.1.3
% 7.34/1.49 % (2773478)Termination reason: Instruction limit
% 7.34/1.49 % (2773478)Termination phase: Saturation
% 7.34/1.49 % (2773478)Time elapsed: 0.231 s
% 7.34/1.49 % (2773478)Peak memory usage: 14 MB
% 7.34/1.49 % (2773478)Instructions burned: 516 (million)
% 7.34/1.49 % (2773502)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3526213294:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 7.34/1.49 % (2773500)Instruction limit reached!
% 7.34/1.49 % (2773500)------------------------------
% 7.34/1.49 % (2773500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.34/1.49 % (2773500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.49 % (2773500)CaDiCaL version: 2.1.3
% 7.34/1.49 % (2773500)Termination reason: Instruction limit
% 7.34/1.49 % (2773500)Termination phase: Saturation
% 7.34/1.49 % (2773500)Time elapsed: 0.019 s
% 7.34/1.49 % (2773500)Peak memory usage: 12 MB
% 7.34/1.49 % (2773500)Instructions burned: 34 (million)
% 7.34/1.49 % (2773504)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3046882314:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 7.34/1.49 % (2773506)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=148975610:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 7.34/1.49 % (2773506)Instruction limit reached!
% 7.34/1.49 % (2773506)------------------------------
% 7.34/1.49 % (2773506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.34/1.49 % (2773506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.49 % (2773506)CaDiCaL version: 2.1.3
% 7.34/1.49 % (2773506)Termination reason: Instruction limit
% 7.34/1.49 % (2773506)Termination phase: Saturation
% 7.34/1.49 % (2773506)Time elapsed: 0.011 s
% 7.34/1.49 % (2773506)Peak memory usage: 12 MB
% 7.34/1.49 % (2773506)Instructions burned: 22 (million)
% 7.34/1.49 % (2773504)Instruction limit reached!
% 7.34/1.49 % (2773504)------------------------------
% 7.34/1.49 % (2773504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.34/1.49 % (2773504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.49 % (2773504)CaDiCaL version: 2.1.3
% 7.34/1.49 % (2773504)Termination reason: Instruction limit
% 7.34/1.49 % (2773504)Termination phase: Saturation
% 7.34/1.49 % (2773504)Time elapsed: 0.034 s
% 7.34/1.49 % (2773504)Peak memory usage: 12 MB
% 7.34/1.49 % (2773504)Instructions burned: 66 (million)
% 7.34/1.49 % (2773502)Instruction limit reached!
% 7.34/1.49 % (2773502)------------------------------
% 7.34/1.49 % (2773502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.34/1.49 % (2773502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.34/1.49 % (2773502)CaDiCaL version: 2.1.3
% 7.34/1.49 % (2773502)Termination reason: Instruction limit
% 7.34/1.49 % (2773502)Termination phase: Saturation
% 7.34/1.49 % (2773502)Time elapsed: 0.045 s
% 7.34/1.49 % (2773502)Peak memory usage: 12 MB
% 7.34/1.49 % (2773502)Instructions burned: 91 (million)
% 7.34/1.49 % (2773509)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=3517929971:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 7.34/1.49 % (2773511)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 8.09/1.63 % (2773510)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2966756491:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/28Mi)
% 8.09/1.63 % (2773511)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=478766292:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2990 on theBenchmark for (2990ds/137Mi)
% 8.09/1.63 % (2773510)Instruction limit reached!
% 8.09/1.63 % (2773510)------------------------------
% 8.09/1.63 % (2773510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.09/1.63 % (2773510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.63 % (2773510)CaDiCaL version: 2.1.3
% 8.09/1.63 % (2773510)Termination reason: Instruction limit
% 8.09/1.63 % (2773510)Termination phase: Saturation
% 8.09/1.63 % (2773510)Time elapsed: 0.015 s
% 8.09/1.63 % (2773510)Peak memory usage: 12 MB
% 8.09/1.63 % (2773510)Instructions burned: 29 (million)
% 8.09/1.63 % (2773515)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=378807462:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 8.09/1.63 % (2773487)Instruction limit reached!
% 8.09/1.63 % (2773487)------------------------------
% 8.09/1.63 % (2773487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.09/1.63 % (2773487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.63 % (2773487)CaDiCaL version: 2.1.3
% 8.09/1.63 % (2773487)Termination reason: Instruction limit
% 8.09/1.63 % (2773487)Termination phase: Saturation
% 8.09/1.63 % (2773487)Time elapsed: 0.223 s
% 8.09/1.63 % (2773487)Peak memory usage: 14 MB
% 8.09/1.63 % (2773487)Instructions burned: 450 (million)
% 8.09/1.63 % (2773517)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3826385231:i=227:sd=1:bd=all:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/227Mi)
% 8.09/1.63 % (2773511)Instruction limit reached!
% 8.09/1.63 % (2773511)------------------------------
% 8.09/1.63 % (2773511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.09/1.63 % (2773511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.63 % (2773511)CaDiCaL version: 2.1.3
% 8.09/1.63 % (2773511)Termination reason: Instruction limit
% 8.09/1.63 % (2773511)Termination phase: Saturation
% 8.09/1.63 % (2773511)Time elapsed: 0.066 s
% 8.09/1.63 % (2773511)Peak memory usage: 13 MB
% 8.09/1.63 % (2773511)Instructions burned: 137 (million)
% 8.09/1.63 % (2773477)Instruction limit reached!
% 8.09/1.63 % (2773477)------------------------------
% 8.09/1.63 % (2773477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.09/1.63 % (2773477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.63 % (2773477)CaDiCaL version: 2.1.3
% 8.09/1.63 % (2773477)Termination reason: Instruction limit
% 8.09/1.63 % (2773477)Termination phase: Saturation
% 8.09/1.63 % (2773477)Time elapsed: 0.391 s
% 8.09/1.63 % (2773477)Peak memory usage: 15 MB
% 8.09/1.63 % (2773477)Instructions burned: 876 (million)
% 8.09/1.63 % (2773519)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 8.09/1.63 % (2773519)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2662876338:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/373Mi)
% 8.09/1.63 % (2773520)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=47335274:i=116:ep=RSTC:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/116Mi)
% 8.09/1.63 % (2773520)Instruction limit reached!
% 8.09/1.63 % (2773520)------------------------------
% 8.09/1.63 % (2773520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.09/1.63 % (2773520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.63 % (2773520)CaDiCaL version: 2.1.3
% 8.09/1.63 % (2773520)Termination reason: Instruction limit
% 8.09/1.63 % (2773520)Termination phase: Saturation
% 8.09/1.63 % (2773520)Time elapsed: 0.055 s
% 8.09/1.63 % (2773520)Peak memory usage: 12 MB
% 8.09/1.63 % (2773520)Instructions burned: 116 (million)
% 8.09/1.63 % (2773498)Instruction limit reached!
% 8.09/1.63 % (2773498)------------------------------
% 8.09/1.63 % (2773498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/1.88 % (2773498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/1.88 % (2773498)CaDiCaL version: 2.1.3
% 8.92/1.88 % (2773498)Termination reason: Instruction limit
% 8.92/1.88 % (2773498)Termination phase: Saturation
% 8.92/1.88 % (2773498)Time elapsed: 0.248 s
% 8.92/1.88 % (2773498)Peak memory usage: 14 MB
% 8.92/1.88 % (2773498)Instructions burned: 497 (million)
% 8.92/1.88 % (2773509)Instruction limit reached!
% 8.92/1.88 % (2773509)------------------------------
% 8.92/1.88 % (2773509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/1.88 % (2773509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/1.88 % (2773509)CaDiCaL version: 2.1.3
% 8.92/1.88 % (2773509)Termination reason: Instruction limit
% 8.92/1.88 % (2773509)Termination phase: Saturation
% 8.92/1.88 % (2773509)Time elapsed: 0.167 s
% 8.92/1.88 % (2773509)Peak memory usage: 15 MB
% 8.92/1.88 % (2773509)Instructions burned: 340 (million)
% 8.92/1.88 % (2773523)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2437968601:i=575:rtra=on_2988 on theBenchmark for (2988ds/575Mi)
% 8.92/1.88 % (2773524)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=643400993:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2988 on theBenchmark for (2988ds/270Mi)
% 8.92/1.88 % (2773517)Instruction limit reached!
% 8.92/1.88 % (2773517)------------------------------
% 8.92/1.88 % (2773517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/1.88 % (2773517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/1.88 % (2773517)CaDiCaL version: 2.1.3
% 8.92/1.88 % (2773517)Termination reason: Instruction limit
% 8.92/1.88 % (2773517)Termination phase: Saturation
% 8.92/1.88 % (2773517)Time elapsed: 0.106 s
% 8.92/1.88 % (2773517)Peak memory usage: 13 MB
% 8.92/1.88 % (2773517)Instructions burned: 229 (million)
% 8.92/1.88 % (2773525)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=1327980611: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_2988 on theBenchmark for (2988ds/9840Mi)
% 8.92/1.88 % (2773515)Instruction limit reached!
% 8.92/1.88 % (2773515)------------------------------
% 8.92/1.88 % (2773515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/1.88 % (2773515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/1.88 % (2773515)CaDiCaL version: 2.1.3
% 8.92/1.88 % (2773515)Termination reason: Instruction limit
% 8.92/1.88 % (2773515)Termination phase: Saturation
% 8.92/1.88 % (2773515)Time elapsed: 0.152 s
% 8.92/1.88 % (2773515)Peak memory usage: 13 MB
% 8.92/1.88 % (2773515)Instructions burned: 341 (million)
% 8.92/1.88 % (2773528)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2063442022:i=421:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/421Mi)
% 8.92/1.88 % (2773530)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 8.92/1.88 % (2773530)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=3828888282:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/270Mi)
% 8.92/1.88 % (2773519)Instruction limit reached!
% 8.92/1.88 % (2773519)------------------------------
% 8.92/1.88 % (2773519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.92/1.88 % (2773519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/1.88 % (2773519)CaDiCaL version: 2.1.3
% 8.92/1.88 % (2773519)Termination reason: Instruction limit
% 8.92/1.88 % (2773519)Termination phase: Saturation
% 8.92/1.88 % (2773519)Time elapsed: 0.171 s
% 8.92/1.88 % (2773519)Peak memory usage: 13 MB
% 8.92/1.88 % (2773519)Instructions burned: 374 (million)
% 8.92/1.88 % (2773533)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2640569373:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/31Mi)
% 8.92/1.88 % (2773533)Instruction limit reached!
% 8.92/1.88 % (2773533)------------------------------
% 8.92/1.88 % (2773533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.12/2.19 % (2773533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.12/2.19 % (2773533)CaDiCaL version: 2.1.3
% 13.12/2.19 % (2773533)Termination reason: Instruction limit
% 13.12/2.19 % (2773533)Termination phase: Saturation
% 13.12/2.19 % (2773533)Time elapsed: 0.016 s
% 13.12/2.19 % (2773533)Peak memory usage: 12 MB
% 13.12/2.19 % (2773533)Instructions burned: 31 (million)
% 13.12/2.19 % (2773524)Instruction limit reached!
% 13.12/2.19 % (2773524)------------------------------
% 13.12/2.19 % (2773524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.12/2.19 % (2773524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.12/2.19 % (2773524)CaDiCaL version: 2.1.3
% 13.12/2.19 % (2773524)Termination reason: Instruction limit
% 13.12/2.19 % (2773524)Termination phase: Saturation
% 13.12/2.19 % (2773524)Time elapsed: 0.128 s
% 13.12/2.19 % (2773524)Peak memory usage: 13 MB
% 13.12/2.19 % (2773524)Instructions burned: 272 (million)
% 13.12/2.19 % (2773535)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 13.12/2.19 % (2773535)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
% 13.12/2.19 % (2773535)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=32278101:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2987 on theBenchmark for (2987ds/1440Mi)
% 13.12/2.19 % (2773536)dis+10_2_sil=128000:si=on:random_seed=64685302:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2987 on theBenchmark for (2987ds/339Mi)
% 13.12/2.19 % (2773530)Instruction limit reached!
% 13.12/2.19 % (2773530)------------------------------
% 13.12/2.19 % (2773530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.12/2.19 % (2773530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.12/2.19 % (2773530)CaDiCaL version: 2.1.3
% 13.12/2.19 % (2773530)Termination reason: Instruction limit
% 13.12/2.19 % (2773530)Termination phase: Saturation
% 13.12/2.19 % (2773530)Time elapsed: 0.131 s
% 13.12/2.19 % (2773530)Peak memory usage: 14 MB
% 13.12/2.19 % (2773530)Instructions burned: 271 (million)
% 13.12/2.19 % (2773539)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1107995208:i=111:add=on:fgj=on:rtra=on:fdi=1024_2987 on theBenchmark for (2987ds/111Mi)
% 13.12/2.19 % (2773528)Instruction limit reached!
% 13.12/2.19 % (2773528)------------------------------
% 13.12/2.19 % (2773528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.12/2.19 % (2773528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.12/2.19 % (2773528)CaDiCaL version: 2.1.3
% 13.12/2.19 % (2773528)Termination reason: Instruction limit
% 13.12/2.19 % (2773528)Termination phase: Saturation
% 13.12/2.19 % (2773528)Time elapsed: 0.196 s
% 13.12/2.19 % (2773528)Peak memory usage: 14 MB
% 13.12/2.19 % (2773528)Instructions burned: 421 (million)
% 13.12/2.19 % (2773541)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=2143626025:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/122Mi)
% 13.12/2.19 % (2773539)Instruction limit reached!
% 13.12/2.19 % (2773539)------------------------------
% 13.12/2.19 % (2773539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.12/2.19 % (2773539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.12/2.19 % (2773539)CaDiCaL version: 2.1.3
% 13.12/2.19 % (2773539)Termination reason: Instruction limit
% 13.12/2.19 % (2773539)Termination phase: Saturation
% 13.12/2.19 % (2773539)Time elapsed: 0.054 s
% 13.12/2.19 % (2773539)Peak memory usage: 12 MB
% 13.12/2.19 % (2773539)Instructions burned: 112 (million)
% 13.12/2.19 % (2773523)Instruction limit reached!
% 13.12/2.19 % (2773523)------------------------------
% 13.12/2.19 % (2773523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.12/2.19 % (2773523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.12/2.19 % (2773523)CaDiCaL version: 2.1.3
% 13.12/2.19 % (2773523)Termination reason: Instruction limit
% 13.12/2.19 % (2773523)Termination phase: Saturation
% 13.12/2.19 % (2773523)Time elapsed: 0.265 s
% 13.12/2.19 % (2773523)Peak memory usage: 15 MB
% 13.12/2.19 % (2773523)Instructions burned: 577 (million)
% 13.54/2.29 % (2773543)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=684361379:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/136Mi)
% 13.54/2.29 % (2773545)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=189997461:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/232Mi)
% 13.54/2.29 % (2773541)Instruction limit reached!
% 13.54/2.29 % (2773541)------------------------------
% 13.54/2.29 % (2773541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.54/2.29 % (2773541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.54/2.29 % (2773541)CaDiCaL version: 2.1.3
% 13.54/2.29 % (2773541)Termination reason: Instruction limit
% 13.54/2.29 % (2773541)Termination phase: Saturation
% 13.54/2.29 % (2773541)Time elapsed: 0.059 s
% 13.54/2.29 % (2773541)Peak memory usage: 12 MB
% 13.54/2.29 % (2773541)Instructions burned: 123 (million)
% 13.54/2.29 % (2773536)Instruction limit reached!
% 13.54/2.29 % (2773536)------------------------------
% 13.54/2.29 % (2773536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.54/2.29 % (2773536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.54/2.29 % (2773536)CaDiCaL version: 2.1.3
% 13.54/2.29 % (2773536)Termination reason: Instruction limit
% 13.54/2.29 % (2773536)Termination phase: Saturation
% 13.54/2.29 % (2773536)Time elapsed: 0.154 s
% 13.54/2.29 % (2773536)Peak memory usage: 13 MB
% 13.54/2.29 % (2773536)Instructions burned: 341 (million)
% 13.54/2.29 % (2773547)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=2991652036:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/1254Mi)
% 13.54/2.29 % (2773548)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 13.54/2.29 % (2773548)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=314561698:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2985 on theBenchmark for (2985ds/281Mi)
% 13.54/2.29 % (2773543)Instruction limit reached!
% 13.54/2.29 % (2773543)------------------------------
% 13.54/2.29 % (2773543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.54/2.29 % (2773543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.54/2.29 % (2773543)CaDiCaL version: 2.1.3
% 13.54/2.29 % (2773543)Termination reason: Instruction limit
% 13.54/2.29 % (2773543)Termination phase: Saturation
% 13.54/2.29 % (2773543)Time elapsed: 0.066 s
% 13.54/2.29 % (2773543)Peak memory usage: 13 MB
% 13.54/2.29 % (2773543)Instructions burned: 136 (million)
% 13.54/2.29 % (2773551)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1336049117:i=619:add=on:rtra=on_2985 on theBenchmark for (2985ds/619Mi)
% 13.54/2.29 % (2773545)Instruction limit reached!
% 13.54/2.29 % (2773545)------------------------------
% 13.54/2.29 % (2773545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.54/2.29 % (2773545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.54/2.29 % (2773545)CaDiCaL version: 2.1.3
% 13.54/2.29 % (2773545)Termination reason: Instruction limit
% 13.54/2.29 % (2773545)Termination phase: Saturation
% 13.54/2.29 % (2773545)Time elapsed: 0.116 s
% 13.54/2.29 % (2773545)Peak memory usage: 13 MB
% 13.54/2.29 % (2773545)Instructions burned: 234 (million)
% 13.54/2.29 % (2773553)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=4214280808:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/865Mi)
% 13.54/2.29 % (2773548)Instruction limit reached!
% 13.54/2.29 % (2773548)------------------------------
% 13.54/2.29 % (2773548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.54/2.29 % (2773548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.54/2.29 % (2773548)CaDiCaL version: 2.1.3
% 13.54/2.29 % (2773548)Termination reason: Instruction limit
% 13.54/2.29 % (2773548)Termination phase: Saturation
% 13.54/2.29 % (2773548)Time elapsed: 0.164 s
% 13.54/2.29 % (2773548)Peak memory usage: 13 MB
% 13.54/2.29 % (2773548)Instructions burned: 281 (million)
% 13.54/2.29 % (2773555)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3426124195:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/212Mi)
% 14.06/2.38 % (2773555)Instruction limit reached!
% 14.06/2.38 % (2773555)------------------------------
% 14.06/2.38 % (2773555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773555)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773555)Termination reason: Instruction limit
% 14.06/2.38 % (2773555)Termination phase: Saturation
% 14.06/2.38 % (2773555)Time elapsed: 0.102 s
% 14.06/2.38 % (2773555)Peak memory usage: 13 MB
% 14.06/2.38 % (2773555)Instructions burned: 213 (million)
% 14.06/2.38 % (2773551)Instruction limit reached!
% 14.06/2.38 % (2773551)------------------------------
% 14.06/2.38 % (2773551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773551)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773551)Termination reason: Instruction limit
% 14.06/2.38 % (2773551)Termination phase: Saturation
% 14.06/2.38 % (2773551)Time elapsed: 0.270 s
% 14.06/2.38 % (2773551)Peak memory usage: 16 MB
% 14.06/2.38 % (2773551)Instructions burned: 619 (million)
% 14.06/2.38 % (2773557)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2318166971:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/130Mi)
% 14.06/2.38 % (2773558)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2495649481:st=1.5:i=346:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/346Mi)
% 14.06/2.38 % (2773557)Instruction limit reached!
% 14.06/2.38 % (2773557)------------------------------
% 14.06/2.38 % (2773557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773557)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773557)Termination reason: Instruction limit
% 14.06/2.38 % (2773557)Termination phase: Saturation
% 14.06/2.38 % (2773557)Time elapsed: 0.037 s
% 14.06/2.38 % (2773557)Peak memory usage: 12 MB
% 14.06/2.38 % (2773557)Instructions burned: 131 (million)
% 14.06/2.38 % (2773561)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=571457992:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/152Mi)
% 14.06/2.38 % (2773561)Instruction limit reached!
% 14.06/2.38 % (2773561)------------------------------
% 14.06/2.38 % (2773561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773561)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773561)Termination reason: Instruction limit
% 14.06/2.38 % (2773561)Termination phase: Saturation
% 14.06/2.38 % (2773561)Time elapsed: 0.073 s
% 14.06/2.38 % (2773561)Peak memory usage: 13 MB
% 14.06/2.38 % (2773561)Instructions burned: 153 (million)
% 14.06/2.38 % (2773564)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1212968646:i=75:ep=R:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/75Mi)
% 14.06/2.38 % (2773558)Instruction limit reached!
% 14.06/2.38 % (2773558)------------------------------
% 14.06/2.38 % (2773558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773558)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773558)Termination reason: Instruction limit
% 14.06/2.38 % (2773558)Termination phase: Saturation
% 14.06/2.38 % (2773558)Time elapsed: 0.154 s
% 14.06/2.38 % (2773558)Peak memory usage: 14 MB
% 14.06/2.38 % (2773558)Instructions burned: 346 (million)
% 14.06/2.38 % (2773553)Instruction limit reached!
% 14.06/2.38 % (2773553)------------------------------
% 14.06/2.38 % (2773553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773553)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773553)Termination reason: Instruction limit
% 14.06/2.38 % (2773553)Termination phase: Saturation
% 14.06/2.38 % (2773553)Time elapsed: 0.388 s
% 14.06/2.38 % (2773553)Peak memory usage: 16 MB
% 14.06/2.38 % (2773553)Instructions burned: 866 (million)
% 14.06/2.38 % (2773567)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=1664440443:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/387Mi)
% 14.06/2.38 % (2773564)Instruction limit reached!
% 14.06/2.38 % (2773564)------------------------------
% 14.06/2.38 % (2773564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773564)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773564)Termination reason: Instruction limit
% 14.06/2.38 % (2773564)Termination phase: Saturation
% 14.06/2.38 % (2773564)Time elapsed: 0.039 s
% 14.06/2.38 % (2773564)Peak memory usage: 12 MB
% 14.06/2.38 % (2773564)Instructions burned: 76 (million)
% 14.06/2.38 % (2773568)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=4289295555:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2980 on theBenchmark for (2980ds/148Mi)
% 14.06/2.38 % (2773570)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1438726553:i=161:piset=and:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/161Mi)
% 14.06/2.38 % (2773535)Instruction limit reached!
% 14.06/2.38 % (2773535)------------------------------
% 14.06/2.38 % (2773535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773535)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773535)Termination reason: Instruction limit
% 14.06/2.38 % (2773535)Termination phase: Saturation
% 14.06/2.38 % (2773535)Time elapsed: 0.702 s
% 14.06/2.38 % (2773535)Peak memory usage: 21 MB
% 14.06/2.38 % (2773535)Instructions burned: 1442 (million)
% 14.06/2.38 % (2773573)lrs+10_1_sil=128000:si=on:random_seed=2776712253:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/888Mi)
% 14.06/2.38 % (2773568)Instruction limit reached!
% 14.06/2.38 % (2773568)------------------------------
% 14.06/2.38 % (2773568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773568)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773568)Termination reason: Instruction limit
% 14.06/2.38 % (2773568)Termination phase: Saturation
% 14.06/2.38 % (2773568)Time elapsed: 0.070 s
% 14.06/2.38 % (2773568)Peak memory usage: 12 MB
% 14.06/2.38 % (2773568)Instructions burned: 150 (million)
% 14.06/2.38 % (2773570)Instruction limit reached!
% 14.06/2.38 % (2773570)------------------------------
% 14.06/2.38 % (2773570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773570)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773570)Termination reason: Instruction limit
% 14.06/2.38 % (2773570)Termination phase: Saturation
% 14.06/2.38 % (2773570)Time elapsed: 0.059 s
% 14.06/2.38 % (2773570)Peak memory usage: 13 MB
% 14.06/2.38 % (2773570)Instructions burned: 165 (million)
% 14.06/2.38 % (2773547)Instruction limit reached!
% 14.06/2.38 % (2773547)------------------------------
% 14.06/2.38 % (2773547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773547)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773547)Termination reason: Instruction limit
% 14.06/2.38 % (2773547)Termination phase: Saturation
% 14.06/2.38 % (2773547)Time elapsed: 0.594 s
% 14.06/2.38 % (2773547)Peak memory usage: 17 MB
% 14.06/2.38 % (2773547)Instructions burned: 1255 (million)
% 14.06/2.38 % (2773577)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=2975342754:i=88:s2at=3:nm=2:rtra=on:rawr=on_2979 on theBenchmark for (2979ds/88Mi)
% 14.06/2.38 % (2773576)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=3294361658:i=136:add=on:ins=4:rtra=on:sup=off_2979 on theBenchmark for (2979ds/136Mi)
% 14.06/2.38 % (2773576)Refutation not found, incomplete strategy
% 14.06/2.38 % (2773576)------------------------------
% 14.06/2.38 % (2773576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773576)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773576)Termination reason: Refutation not found, incomplete strategy
% 14.06/2.38 % (2773576)Time elapsed: 0.002 s
% 14.06/2.38 % (2773576)Peak memory usage: 12 MB
% 14.06/2.38 % (2773576)Instructions burned: 4 (million)
% 14.06/2.38 % (2773576)------------------------------
% 14.06/2.38 % (2773576)------------------------------
% 14.06/2.38 % (2773578)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=1720642172:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2979 on theBenchmark for (2979ds/93Mi)
% 14.06/2.38 % (2773581)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=110669436:i=2186:rtra=on:ixr=off_2979 on theBenchmark for (2979ds/2186Mi)
% 14.06/2.38 % (2773577)Instruction limit reached!
% 14.06/2.38 % (2773577)------------------------------
% 14.06/2.38 % (2773577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773577)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773577)Termination reason: Instruction limit
% 14.06/2.38 % (2773577)Termination phase: Saturation
% 14.06/2.38 % (2773577)Time elapsed: 0.034 s
% 14.06/2.38 % (2773577)Peak memory usage: 13 MB
% 14.06/2.38 % (2773577)Instructions burned: 88 (million)
% 14.06/2.38 % (2773584)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4194517970:s2a=on:i=240:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/240Mi)
% 14.06/2.38 % (2773578)Instruction limit reached!
% 14.06/2.38 % (2773578)------------------------------
% 14.06/2.38 % (2773578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773578)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773578)Termination reason: Instruction limit
% 14.06/2.38 % (2773578)Termination phase: Saturation
% 14.06/2.38 % (2773578)Time elapsed: 0.054 s
% 14.06/2.38 % (2773578)Peak memory usage: 12 MB
% 14.06/2.38 % (2773578)Instructions burned: 93 (million)
% 14.06/2.38 % (2773567)Instruction limit reached!
% 14.06/2.38 % (2773567)------------------------------
% 14.06/2.38 % (2773567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773567)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773567)Termination reason: Instruction limit
% 14.06/2.38 % (2773567)Termination phase: Saturation
% 14.06/2.38 % (2773567)Time elapsed: 0.172 s
% 14.06/2.38 % (2773567)Peak memory usage: 14 MB
% 14.06/2.38 % (2773567)Instructions burned: 389 (million)
% 14.06/2.38 % (2773573) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2773356-2773573"...
% 14.06/2.38 % (2773573)...printing done.
% 14.06/2.38 % (2773573)Refutation found. Thanks to Tanya!
% 14.06/2.38 % SZS status Theorem for theBenchmark
% 14.06/2.38 % SZS output start Proof for theBenchmark
% See solution above
% 14.06/2.38 % (2773573)------------------------------
% 14.06/2.38 % (2773573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.38 % (2773573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.38 % (2773573)CaDiCaL version: 2.1.3
% 14.06/2.38 % (2773573)Termination reason: Refutation
% 14.06/2.38 % (2773573)Time elapsed: 0.135 s
% 14.06/2.38 % (2773573)Peak memory usage: 14 MB
% 14.06/2.38 % (2773573)Instructions burned: 271 (million)
% 14.06/2.38 % (2773356)Success in time 2.133 s
% 14.06/2.38 % Vampire exiting
%------------------------------------------------------------------------------