%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ142^1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:20:58 AM UTC 2026
% Result : Theorem 12.56s 2.26s
% Output : Refutation 12.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 18
% Syntax : Number of formulae : 86 ( 59 unt; 0 typ; 1 def)
% Number of atoms : 271 ( 142 equ; 0 cnn)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 571 ( 27 ~; 51 |; 0 &; 485 @)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 39 ( 36 usr; 32 con; 0-2 aty)
% Number of variables : 90 ( 0 ^; 88 !; 2 ?; 90 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
position: $tType ).
thf(type_def_6,type,
direction: $tType ).
thf(type_def_7,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(type_def_8,type,
movelist: $tType ).
thf(func_def_0,type,
left: direction ).
thf(func_def_1,type,
right: direction ).
thf(func_def_2,type,
top: direction ).
thf(func_def_3,type,
bottom: direction ).
thf(func_def_4,type,
next: position > direction > position ).
thf(func_def_6,type,
wall: position > $o ).
thf(func_def_7,type,
nomove: movelist ).
thf(func_def_8,type,
movedir: movelist > direction > movelist ).
thf(func_def_9,type,
playerpos: movelist > position ).
thf(func_def_10,type,
c00: position ).
thf(func_def_11,type,
c10: position ).
thf(func_def_12,type,
c20: position ).
thf(func_def_13,type,
c30: position ).
thf(func_def_14,type,
c40: position ).
thf(func_def_15,type,
c01: position ).
thf(func_def_16,type,
c11: position ).
thf(func_def_17,type,
c21: position ).
thf(func_def_18,type,
c31: position ).
thf(func_def_19,type,
c41: position ).
thf(func_def_20,type,
c02: position ).
thf(func_def_21,type,
c12: position ).
thf(func_def_22,type,
c22: position ).
thf(func_def_23,type,
c32: position ).
thf(func_def_24,type,
c42: position ).
thf(func_def_25,type,
c03: position ).
thf(func_def_26,type,
c13: position ).
thf(func_def_27,type,
c23: position ).
thf(func_def_28,type,
c33: position ).
thf(func_def_29,type,
c43: position ).
thf(func_def_30,type,
c04: position ).
thf(func_def_31,type,
c14: position ).
thf(func_def_32,type,
c24: position ).
thf(func_def_33,type,
c34: position ).
thf(func_def_34,type,
c44: position ).
thf(func_def_37,type,
sF0: movelist > position ).
thf(f1,axiom,
! [X1: direction,X0: direction,X2: position] :
( ( next @ ( next @ X2 @ X0 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',next_comm) ).
thf(f3,axiom,
! [X0: position] :
( ( next @ ( next @ X0 @ top ) @ bottom )
= X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',top_bottom) ).
thf(f4,axiom,
! [X0: position,X2: direction,X1: movelist] :
( ( ( playerpos @ X1 )
= X0 )
=> ( ~ ( wall @ ( next @ X0 @ X2 ) )
=> ( ( playerpos @ ( movedir @ X1 @ X2 ) )
= ( next @ X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',player_move_legal) ).
thf(f7,axiom,
( c20
= ( next @ c10 @ right ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c20_defin) ).
thf(f8,axiom,
( c30
= ( next @ c20 @ right ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c30_defin) ).
thf(f14,axiom,
( c11
= ( next @ c10 @ top ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11_defin) ).
thf(f15,axiom,
( c12
= ( next @ c11 @ top ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c12_defin) ).
thf(f18,axiom,
( c21
= ( next @ c20 @ top ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c21_defin) ).
thf(f19,axiom,
( c22
= ( next @ c21 @ top ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c22_defin) ).
thf(f22,axiom,
( c31
= ( next @ c30 @ top ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c31_defin) ).
thf(f23,axiom,
( c32
= ( next @ c31 @ top ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c32_defin) ).
thf(f34,axiom,
( ( wall @ c31 )
= $false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c31_axiom) ).
thf(f37,axiom,
( $false
= ( wall @ c12 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c12_axiom) ).
thf(f38,axiom,
( ( wall @ c22 )
= $false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c22_axiom) ).
thf(f39,axiom,
( ( wall @ c32 )
= $false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c32_axiom) ).
thf(f46,axiom,
( ( playerpos @ nomove )
= c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',start_axiom) ).
thf(f47,conjecture,
? [X0: movelist] :
( ( playerpos @ X0 )
= c31 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exercise) ).
thf(f48,negated_conjecture,
~ ? [X0: movelist] :
( ( playerpos @ X0 )
= c31 ),
inference(negated_conjecture,[status(cth)],[f47]) ).
thf(f52,plain,
( ( wall @ c32 )
= $false ),
inference(fool_elimination,[],[f39]) ).
thf(f60,plain,
( ( wall @ c22 )
= $false ),
inference(fool_elimination,[],[f38]) ).
thf(f67,plain,
( ( wall @ c12 )
= $false ),
inference(fool_elimination,[],[f37]) ).
thf(f68,plain,
! [X0: position,X1: direction,X2: movelist] :
( ( ( playerpos @ X2 )
= X0 )
=> ( ~ ( wall @ ( next @ X0 @ X1 ) )
=> ( ( next @ X0 @ X1 )
= ( playerpos @ ( movedir @ X2 @ X1 ) ) ) ) ),
inference(rectify,[],[f4]) ).
thf(f69,plain,
! [X0: position,X1: direction,X2: movelist] :
( ( ( playerpos @ X2 )
= X0 )
=> ( ( ( wall @ ( next @ X0 @ X1 ) )
!= $true )
=> ( ( next @ X0 @ X1 )
= ( playerpos @ ( movedir @ X2 @ X1 ) ) ) ) ),
inference(fool_elimination,[],[f68]) ).
thf(f72,plain,
( ( wall @ c31 )
= $false ),
inference(fool_elimination,[],[f34]) ).
thf(f73,plain,
! [X0: direction,X1: direction,X2: position] :
( ( next @ ( next @ X2 @ X0 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ X0 ) ),
inference(rectify,[],[f1]) ).
thf(f74,plain,
! [X2: movelist,X1: direction,X0: position] :
( ( ( playerpos @ X2 )
= X0 )
=> ( ( ( wall @ ( next @ X0 @ X1 ) )
!= $true )
=> ( ( next @ X0 @ X1 )
= ( playerpos @ ( movedir @ X2 @ X1 ) ) ) ) ),
inference(flattening,[],[f69]) ).
thf(f75,plain,
! [X0: movelist] :
( c31
!= ( playerpos @ X0 ) ),
inference(ennf_transformation,[],[f48]) ).
thf(f78,plain,
! [X2: movelist,X1: direction,X0: position] :
( ( ( next @ X0 @ X1 )
= ( playerpos @ ( movedir @ X2 @ X1 ) ) )
| ( ( wall @ ( next @ X0 @ X1 ) )
= $true )
| ( ( playerpos @ X2 )
!= X0 ) ),
inference(ennf_transformation,[],[f74]) ).
thf(f79,plain,
! [X1: direction,X2: movelist,X0: position] :
( ( ( playerpos @ X2 )
!= X0 )
| ( ( next @ X0 @ X1 )
= ( playerpos @ ( movedir @ X2 @ X1 ) ) )
| ( ( wall @ ( next @ X0 @ X1 ) )
= $true ) ),
inference(flattening,[],[f78]) ).
thf(f81,plain,
! [X0: direction,X1: movelist,X2: position] :
( ( ( playerpos @ X1 )
!= X2 )
| ( ( next @ X2 @ X0 )
= ( playerpos @ ( movedir @ X1 @ X0 ) ) )
| ( ( wall @ ( next @ X2 @ X0 ) )
= $true ) ),
inference(rectify,[],[f79]) ).
thf(f85,plain,
( c30
= ( next @ c20 @ right ) ),
inference(cnf_transformation,[],[f8]) ).
thf(f93,plain,
( ( wall @ c31 )
= $false ),
inference(cnf_transformation,[],[f72]) ).
thf(f95,plain,
( c32
= ( next @ c31 @ top ) ),
inference(cnf_transformation,[],[f23]) ).
thf(f99,plain,
! [X2: position,X0: direction,X1: movelist] :
( ( ( playerpos @ X1 )
!= X2 )
| ( ( next @ X2 @ X0 )
= ( playerpos @ ( movedir @ X1 @ X0 ) ) )
| ( ( wall @ ( next @ X2 @ X0 ) )
= $true ) ),
inference(cnf_transformation,[],[f81]) ).
thf(f100,plain,
( c20
= ( next @ c10 @ right ) ),
inference(cnf_transformation,[],[f7]) ).
thf(f101,plain,
! [X0: movelist] :
( c31
!= ( playerpos @ X0 ) ),
inference(cnf_transformation,[],[f75]) ).
thf(f103,plain,
( c12
= ( next @ c11 @ top ) ),
inference(cnf_transformation,[],[f15]) ).
thf(f107,plain,
( c21
= ( next @ c20 @ top ) ),
inference(cnf_transformation,[],[f18]) ).
thf(f109,plain,
( ( wall @ c12 )
= $false ),
inference(cnf_transformation,[],[f67]) ).
thf(f112,plain,
( c11
= ( playerpos @ nomove ) ),
inference(cnf_transformation,[],[f46]) ).
thf(f114,plain,
( c11
= ( next @ c10 @ top ) ),
inference(cnf_transformation,[],[f14]) ).
thf(f115,plain,
! [X2: position,X0: direction,X1: direction] :
( ( next @ ( next @ X2 @ X0 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ X0 ) ),
inference(cnf_transformation,[],[f73]) ).
thf(f118,plain,
( c31
= ( next @ c30 @ top ) ),
inference(cnf_transformation,[],[f22]) ).
thf(f119,plain,
( ( wall @ c32 )
= $false ),
inference(cnf_transformation,[],[f52]) ).
thf(f122,plain,
( c22
= ( next @ c21 @ top ) ),
inference(cnf_transformation,[],[f19]) ).
thf(f125,plain,
! [X0: position] :
( ( next @ ( next @ X0 @ top ) @ bottom )
= X0 ),
inference(cnf_transformation,[],[f3]) ).
thf(f126,plain,
( ( wall @ c22 )
= $false ),
inference(cnf_transformation,[],[f60]) ).
thf(f132,plain,
! [X0: direction,X1: movelist] :
( ( ( wall @ ( next @ ( playerpos @ X1 ) @ X0 ) )
= $true )
| ( ( next @ ( playerpos @ X1 ) @ X0 )
= ( playerpos @ ( movedir @ X1 @ X0 ) ) ) ),
inference(equality_resolution,[],[f99]) ).
thf(f133,definition,
! [X0: movelist] :
( ( sF0 @ X0 )
= ( playerpos @ X0 ) ),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
thf(f134,plain,
! [X0: movelist] :
( ( playerpos @ X0 )
= ( sF0 @ X0 ) ),
inference(reorient_equations,[],[f133]) ).
thf(f135,plain,
! [X0: movelist] :
( c31
!= ( sF0 @ X0 ) ),
inference(definition_folding,[],[f101,f134]) ).
thf(f153,plain,
( c11
= ( sF0 @ nomove ) ),
inference(constrained_superposition,[],[f134,f112]) ).
thf(f163,plain,
( c31
= ( next @ c32 @ bottom ) ),
inference(constrained_superposition,[],[f125,f95]) ).
thf(f180,plain,
! [X0: direction] :
( ( next @ c20 @ X0 )
= ( next @ ( next @ c10 @ X0 ) @ right ) ),
inference(constrained_superposition,[],[f115,f100]) ).
thf(f181,plain,
! [X0: direction] :
( ( next @ c30 @ X0 )
= ( next @ ( next @ c20 @ X0 ) @ right ) ),
inference(constrained_superposition,[],[f115,f85]) ).
thf(f188,plain,
! [X0: direction] :
( ( next @ ( next @ c11 @ X0 ) @ top )
= ( next @ c12 @ X0 ) ),
inference(constrained_superposition,[],[f115,f103]) ).
thf(f189,plain,
! [X0: direction] :
( ( next @ ( next @ c21 @ X0 ) @ top )
= ( next @ c22 @ X0 ) ),
inference(constrained_superposition,[],[f115,f122]) ).
thf(f275,plain,
! [X0: direction,X1: movelist] :
( ( ( wall @ ( next @ ( sF0 @ X1 ) @ X0 ) )
= $true )
| ( ( next @ ( playerpos @ X1 ) @ X0 )
= ( playerpos @ ( movedir @ X1 @ X0 ) ) ) ),
inference(forward_demodulation,[],[f132,f134]) ).
thf(f276,plain,
! [X0: direction,X1: movelist] :
( ( ( wall @ ( next @ ( sF0 @ X1 ) @ X0 ) )
= $true )
| ( ( sF0 @ ( movedir @ X1 @ X0 ) )
= ( next @ ( playerpos @ X1 ) @ X0 ) ) ),
inference(forward_demodulation,[],[f275,f134]) ).
thf(f277,plain,
! [X0: direction,X1: movelist] :
( ( ( next @ ( sF0 @ X1 ) @ X0 )
= ( sF0 @ ( movedir @ X1 @ X0 ) ) )
| ( ( wall @ ( next @ ( sF0 @ X1 ) @ X0 ) )
= $true ) ),
inference(forward_demodulation,[],[f276,f134]) ).
thf(f279,plain,
( ( next @ c20 @ top )
= ( next @ c11 @ right ) ),
inference(constrained_superposition,[],[f180,f114]) ).
thf(f288,plain,
( c21
= ( next @ c11 @ right ) ),
inference(forward_demodulation,[],[f279,f107]) ).
thf(f296,plain,
( ( next @ c30 @ top )
= ( next @ c21 @ right ) ),
inference(constrained_superposition,[],[f181,f107]) ).
thf(f306,plain,
( c31
= ( next @ c21 @ right ) ),
inference(forward_demodulation,[],[f296,f118]) ).
thf(f312,plain,
! [X0: movelist,X1: direction] :
( ( ( wall @ ( next @ ( sF0 @ X0 ) @ X1 ) )
= $true )
| ( c31
!= ( next @ ( sF0 @ X0 ) @ X1 ) ) ),
inference(constrained_superposition,[],[f135,f277]) ).
thf(f314,plain,
! [X2: direction,X0: movelist,X1: direction] :
( ( ( wall @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( ( wall @ ( next @ ( sF0 @ X0 ) @ X1 ) )
= $true )
| ( c31
!= ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) ) ),
inference(constrained_superposition,[],[f312,f277]) ).
thf(f322,plain,
! [X2: direction,X3: direction,X0: movelist,X1: direction] :
( ( ( wall @ ( next @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) @ X3 ) )
= $true )
| ( ( wall @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( c31
!= ( next @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) @ X3 ) )
| ( ( wall @ ( next @ ( sF0 @ X0 ) @ X1 ) )
= $true ) ),
inference(constrained_superposition,[],[f314,f277]) ).
thf(f394,plain,
! [X2: direction,X3: direction,X0: movelist,X1: direction,X4: direction] :
( ( ( wall @ ( next @ ( next @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) @ X3 ) @ X4 ) )
= $true )
| ( ( wall @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( ( wall @ ( next @ ( sF0 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ ( next @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) @ X3 ) )
= $true )
| ( c31
!= ( next @ ( next @ ( next @ ( next @ ( sF0 @ X0 ) @ X1 ) @ X2 ) @ X3 ) @ X4 ) ) ),
inference(constrained_superposition,[],[f322,f277]) ).
thf(f727,plain,
( ( next @ c21 @ top )
= ( next @ c12 @ right ) ),
inference(constrained_superposition,[],[f188,f288]) ).
thf(f750,plain,
( c22
= ( next @ c12 @ right ) ),
inference(forward_demodulation,[],[f727,f122]) ).
thf(f831,plain,
( ( next @ c31 @ top )
= ( next @ c22 @ right ) ),
inference(constrained_superposition,[],[f189,f306]) ).
thf(f846,plain,
( c32
= ( next @ c22 @ right ) ),
inference(forward_demodulation,[],[f831,f95]) ).
thf(f1717,plain,
! [X2: direction,X3: direction,X0: direction,X1: direction] :
( ( ( wall @ ( next @ ( next @ ( next @ ( next @ c11 @ X0 ) @ X1 ) @ X2 ) @ X3 ) )
= $true )
| ( c31
!= ( next @ ( next @ ( next @ ( next @ c11 @ X0 ) @ X1 ) @ X2 ) @ X3 ) )
| ( ( wall @ ( next @ c11 @ X0 ) )
= $true )
| ( ( wall @ ( next @ ( next @ ( next @ c11 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( ( wall @ ( next @ ( next @ c11 @ X0 ) @ X1 ) )
= $true ) ),
inference(constrained_superposition,[],[f394,f153]) ).
thf(f1738,plain,
! [X2: direction,X0: direction,X1: direction] :
( ( ( wall @ c12 )
= $true )
| ( c31
!= ( next @ ( next @ ( next @ c12 @ X0 ) @ X1 ) @ X2 ) )
| ( ( wall @ ( next @ ( next @ c12 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ ( next @ ( next @ ( next @ c12 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( ( wall @ ( next @ c12 @ X0 ) )
= $true ) ),
inference(constrained_superposition,[],[f1717,f103]) ).
thf(f1757,plain,
! [X2: direction,X0: direction,X1: direction] :
( ( c31
!= ( next @ ( next @ ( next @ c12 @ X0 ) @ X1 ) @ X2 ) )
| ( ( wall @ ( next @ c12 @ X0 ) )
= $true )
| ( ( wall @ ( next @ ( next @ c12 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ ( next @ ( next @ ( next @ c12 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( $false = $true ) ),
inference(forward_demodulation,[],[f1738,f109]) ).
thf(f1758,plain,
! [X2: direction,X0: direction,X1: direction] :
( ( ( wall @ ( next @ ( next @ ( next @ c12 @ X0 ) @ X1 ) @ X2 ) )
= $true )
| ( c31
!= ( next @ ( next @ ( next @ c12 @ X0 ) @ X1 ) @ X2 ) )
| ( ( wall @ ( next @ ( next @ c12 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ ( next @ c12 @ X0 ) )
= $true ) ),
inference(trivial_inequality_removal,[],[f1757]) ).
thf(f1760,plain,
! [X0: direction,X1: direction] :
( ( c31
!= ( next @ ( next @ c22 @ X0 ) @ X1 ) )
| ( ( wall @ ( next @ c22 @ X0 ) )
= $true )
| ( ( wall @ ( next @ ( next @ c22 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ c22 )
= $true ) ),
inference(constrained_superposition,[],[f1758,f750]) ).
thf(f1774,plain,
! [X0: direction,X1: direction] :
( ( c31
!= ( next @ ( next @ c22 @ X0 ) @ X1 ) )
| ( ( wall @ ( next @ ( next @ c22 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ ( next @ c22 @ X0 ) )
= $true )
| ( $false = $true ) ),
inference(forward_demodulation,[],[f1760,f126]) ).
thf(f1775,plain,
! [X0: direction,X1: direction] :
( ( ( wall @ ( next @ ( next @ c22 @ X0 ) @ X1 ) )
= $true )
| ( ( wall @ ( next @ c22 @ X0 ) )
= $true )
| ( c31
!= ( next @ ( next @ c22 @ X0 ) @ X1 ) ) ),
inference(trivial_inequality_removal,[],[f1774]) ).
thf(f1777,plain,
! [X0: direction] :
( ( $true
= ( wall @ ( next @ c32 @ X0 ) ) )
| ( c31
!= ( next @ c32 @ X0 ) )
| ( ( wall @ c32 )
= $true ) ),
inference(constrained_superposition,[],[f1775,f846]) ).
thf(f1785,plain,
! [X0: direction] :
( ( c31
!= ( next @ c32 @ X0 ) )
| ( $true
= ( wall @ ( next @ c32 @ X0 ) ) )
| ( $false = $true ) ),
inference(forward_demodulation,[],[f1777,f119]) ).
thf(f1786,plain,
! [X0: direction] :
( ( $true
= ( wall @ ( next @ c32 @ X0 ) ) )
| ( c31
!= ( next @ c32 @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f1785]) ).
thf(f1789,plain,
( ( c31 != c31 )
| ( ( wall @ c31 )
= $true ) ),
inference(constrained_superposition,[],[f1786,f163]) ).
thf(f1790,plain,
( ( wall @ c31 )
= $true ),
inference(trivial_inequality_removal,[],[f1789]) ).
thf(f1791,plain,
$false = $true,
inference(forward_demodulation,[],[f1790,f93]) ).
thf(f1792,plain,
$false,
inference(trivial_inequality_removal,[],[f1791]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PUZ142^1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.29 % Computer : n010.cluster.edu
% 0.11/0.29 % Model : x86_64 x86_64
% 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.29 % Memory : 8046.5625MB
% 0.11/0.29 % OS : Linux 6.8.0-71-generic
% 0.11/0.29 % CPULimit : 300
% 0.11/0.29 % WCLimit : 300
% 0.11/0.29 % DateTime : Tue Sep 29 13:27:18 UTC 2026
% 0.11/0.29 % CPUTime :
% 0.11/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.29/0.33 Running higher-order theorem proving
% 0.29/0.36 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
% 1.17/0.57 % (2844136)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.17/0.57 % (2844142)lrs+10_16_si=on:nwc=1.5:random_seed=3164654775:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.17/0.57 % (2844147)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.17/0.57 % (2844147)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.17/0.57 % (2844142)Instruction limit reached!
% 1.17/0.57 % (2844142)------------------------------
% 1.17/0.57 % (2844142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.57 % (2844142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.57 % (2844142)CaDiCaL version: 2.1.3
% 1.17/0.57 % (2844142)Termination reason: Instruction limit
% 1.17/0.57 % (2844142)Termination phase: Saturation
% 1.17/0.57 % (2844142)Time elapsed: 0.009 s
% 1.17/0.57 % (2844142)Peak memory usage: 12 MB
% 1.17/0.57 % (2844142)Instructions burned: 18 (million)
% 1.17/0.57 % (2844141)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3686115034:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.17/0.57 % (2844145)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=252781288:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.17/0.57 % (2844143)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2024784064:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.17/0.57 % (2844144)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=485003214: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)
% 1.17/0.57 % (2844146)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1992470024:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.17/0.57 % (2844147)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=979768472:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.17/0.57 % (2844143)Instruction limit reached!
% 1.17/0.57 % (2844143)------------------------------
% 1.17/0.57 % (2844143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.57 % (2844143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.57 % (2844143)CaDiCaL version: 2.1.3
% 1.17/0.57 % (2844143)Termination reason: Instruction limit
% 1.17/0.57 % (2844143)Termination phase: Property scanning
% 1.17/0.57 % (2844143)Time elapsed: 0.003 s
% 1.17/0.57 % (2844143)Peak memory usage: 10 MB
% 1.17/0.57 % (2844143)Instructions burned: 3 (million)
% 1.17/0.57 % (2844145)Instruction limit reached!
% 1.17/0.57 % (2844145)------------------------------
% 1.17/0.57 % (2844145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.57 % (2844145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.57 % (2844145)CaDiCaL version: 2.1.3
% 1.17/0.57 % (2844145)Termination reason: Instruction limit
% 1.17/0.57 % (2844145)Termination phase: Saturation
% 1.17/0.57 % (2844145)Time elapsed: 0.021 s
% 1.17/0.57 % (2844145)Peak memory usage: 11 MB
% 1.17/0.57 % (2844145)Instructions burned: 24 (million)
% 1.17/0.57 % (2844149)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3835787897:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.17/0.57 % (2844149)Instruction limit reached!
% 1.17/0.57 % (2844149)------------------------------
% 1.17/0.57 % (2844149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.57 % (2844149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.57 % (2844149)CaDiCaL version: 2.1.3
% 1.17/0.57 % (2844149)Termination reason: Instruction limit
% 1.17/0.57 % (2844149)Termination phase: Saturation
% 1.17/0.57 % (2844149)Time elapsed: 0.003 s
% 1.17/0.57 % (2844149)Peak memory usage: 11 MB
% 1.17/0.57 % (2844149)Instructions burned: 3 (million)
% 1.17/0.57 % (2844156)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1982687688:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.17/0.63 % (2844157)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.17/0.63 % (2844157)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=351242159:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.17/0.63 % (2844156)Instruction limit reached!
% 1.17/0.63 % (2844156)------------------------------
% 1.17/0.63 % (2844156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.63 % (2844156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.63 % (2844156)CaDiCaL version: 2.1.3
% 1.17/0.63 % (2844156)Termination reason: Instruction limit
% 1.17/0.63 % (2844156)Termination phase: Saturation
% 1.17/0.63 % (2844156)Time elapsed: 0.005 s
% 1.17/0.63 % (2844156)Peak memory usage: 11 MB
% 1.17/0.63 % (2844156)Instructions burned: 5 (million)
% 1.17/0.63 % (2844157)Instruction limit reached!
% 1.17/0.63 % (2844157)------------------------------
% 1.17/0.63 % (2844157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.63 % (2844157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.63 % (2844157)CaDiCaL version: 2.1.3
% 1.17/0.63 % (2844157)Termination reason: Instruction limit
% 1.17/0.63 % (2844157)Termination phase: Saturation
% 1.17/0.63 % (2844157)Time elapsed: 0.004 s
% 1.17/0.63 % (2844157)Peak memory usage: 12 MB
% 1.17/0.63 % (2844157)Instructions burned: 8 (million)
% 1.17/0.63 % (2844163)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=1650964109:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.17/0.63 % (2844146)Instruction limit reached!
% 1.17/0.63 % (2844146)------------------------------
% 1.17/0.63 % (2844146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.63 % (2844146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.63 % (2844146)CaDiCaL version: 2.1.3
% 1.17/0.63 % (2844146)Termination reason: Instruction limit
% 1.17/0.63 % (2844146)Termination phase: Saturation
% 1.17/0.63 % (2844146)Time elapsed: 0.066 s
% 1.17/0.63 % (2844146)Peak memory usage: 12 MB
% 1.17/0.63 % (2844146)Instructions burned: 75 (million)
% 1.17/0.63 % (2844162)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.17/0.63 % (2844162)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.17/0.63 % (2844162)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3680054168:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.17/0.63 % (2844141)Instruction limit reached!
% 1.17/0.63 % (2844141)------------------------------
% 1.17/0.63 % (2844141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.63 % (2844141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.63 % (2844141)CaDiCaL version: 2.1.3
% 1.17/0.63 % (2844141)Termination reason: Instruction limit
% 1.17/0.63 % (2844141)Termination phase: Saturation
% 1.17/0.63 % (2844141)Time elapsed: 0.074 s
% 1.17/0.63 % (2844141)Peak memory usage: 12 MB
% 1.17/0.63 % (2844141)Instructions burned: 87 (million)
% 1.17/0.63 % (2844162)Instruction limit reached!
% 1.17/0.63 % (2844162)------------------------------
% 1.17/0.63 % (2844162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.63 % (2844162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.63 % (2844162)CaDiCaL version: 2.1.3
% 1.17/0.63 % (2844162)Termination reason: Instruction limit
% 1.17/0.63 % (2844162)Termination phase: Saturation
% 1.17/0.63 % (2844162)Time elapsed: 0.024 s
% 1.17/0.63 % (2844162)Peak memory usage: 12 MB
% 1.17/0.63 % (2844162)Instructions burned: 28 (million)
% 1.17/0.63 % (2844163)Instruction limit reached!
% 1.17/0.63 % (2844163)------------------------------
% 1.17/0.63 % (2844163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.63 % (2844163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.63 % (2844163)CaDiCaL version: 2.1.3
% 2.04/0.69 % (2844163)Termination reason: Instruction limit
% 2.04/0.69 % (2844163)Termination phase: Saturation
% 2.04/0.69 % (2844163)Time elapsed: 0.039 s
% 2.04/0.69 % (2844163)Peak memory usage: 12 MB
% 2.04/0.69 % (2844163)Instructions burned: 86 (million)
% 2.04/0.69 % (2844159)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3982111671:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 2.04/0.69 % (2844167)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.04/0.69 % (2844165)lrs+10_1_si=on:cs=on:random_seed=1934825065:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.04/0.69 % (2844167)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=2521965275:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.04/0.69 % (2844167)Instruction limit reached!
% 2.04/0.69 % (2844167)------------------------------
% 2.04/0.69 % (2844167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.04/0.69 % (2844167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.04/0.69 % (2844167)CaDiCaL version: 2.1.3
% 2.04/0.69 % (2844167)Termination reason: Instruction limit
% 2.04/0.69 % (2844167)Termination phase: Property scanning
% 2.04/0.69 % (2844167)Time elapsed: 0.002 s
% 2.04/0.69 % (2844167)Peak memory usage: 9 MB
% 2.04/0.69 % (2844167)Instructions burned: 2 (million)
% 2.04/0.69 % (2844165)Instruction limit reached!
% 2.04/0.69 % (2844165)------------------------------
% 2.04/0.69 % (2844165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.04/0.69 % (2844165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.04/0.69 % (2844165)CaDiCaL version: 2.1.3
% 2.04/0.69 % (2844165)Termination reason: Instruction limit
% 2.04/0.69 % (2844165)Termination phase: Saturation
% 2.04/0.69 % (2844165)Time elapsed: 0.008 s
% 2.04/0.69 % (2844165)Peak memory usage: 12 MB
% 2.04/0.69 % (2844165)Instructions burned: 8 (million)
% 2.04/0.69 % (2844159)Instruction limit reached!
% 2.04/0.69 % (2844159)------------------------------
% 2.04/0.69 % (2844159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.04/0.69 % (2844159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.04/0.69 % (2844159)CaDiCaL version: 2.1.3
% 2.04/0.69 % (2844159)Termination reason: Instruction limit
% 2.04/0.69 % (2844159)Termination phase: Saturation
% 2.04/0.69 % (2844159)Time elapsed: 0.013 s
% 2.04/0.69 % (2844159)Peak memory usage: 12 MB
% 2.04/0.69 % (2844159)Instructions burned: 13 (million)
% 2.04/0.69 % (2844147)Instruction limit reached!
% 2.04/0.69 % (2844147)------------------------------
% 2.04/0.69 % (2844147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.04/0.69 % (2844147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.04/0.69 % (2844147)CaDiCaL version: 2.1.3
% 2.04/0.69 % (2844147)Termination reason: Instruction limit
% 2.04/0.69 % (2844147)Termination phase: Saturation
% 2.04/0.69 % (2844147)Time elapsed: 0.129 s
% 2.04/0.69 % (2844147)Peak memory usage: 13 MB
% 2.04/0.69 % (2844147)Instructions burned: 158 (million)
% 2.04/0.69 % (2844168)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3590055474:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.04/0.69 % (2844168)Refutation not found, incomplete strategy
% 2.04/0.69 % (2844168)------------------------------
% 2.04/0.69 % (2844168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.04/0.69 % (2844168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.04/0.69 % (2844168)CaDiCaL version: 2.1.3
% 2.04/0.69 % (2844168)Termination reason: Refutation not found, incomplete strategy
% 2.04/0.69 % (2844168)Time elapsed: 0.002 s
% 2.04/0.69 % (2844168)Peak memory usage: 12 MB
% 2.04/0.69 % (2844168)Instructions burned: 3 (million)
% 2.04/0.69 % (2844168)------------------------------
% 2.04/0.69 % (2844168)------------------------------
% 2.04/0.69 % (2844174)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=207777389:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.04/0.69 % (2844169)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=822740032:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.04/0.69 % (2844173)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=638182542:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.31/0.80 % (2844175)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=364232630:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.31/0.80 % (2844178)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4071817922:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.31/0.80 % (2844178)Instruction limit reached!
% 2.31/0.80 % (2844178)------------------------------
% 2.31/0.80 % (2844178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.80 % (2844178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.80 % (2844178)CaDiCaL version: 2.1.3
% 2.31/0.80 % (2844178)Termination reason: Instruction limit
% 2.31/0.80 % (2844178)Termination phase: Saturation
% 2.31/0.80 % (2844178)Time elapsed: 0.002 s
% 2.31/0.80 % (2844178)Peak memory usage: 11 MB
% 2.31/0.80 % (2844178)Instructions burned: 4 (million)
% 2.31/0.80 % (2844176)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=286862255:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.31/0.80 % (2844174)Instruction limit reached!
% 2.31/0.80 % (2844174)------------------------------
% 2.31/0.80 % (2844174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.80 % (2844174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.80 % (2844174)CaDiCaL version: 2.1.3
% 2.31/0.80 % (2844174)Termination reason: Instruction limit
% 2.31/0.80 % (2844174)Termination phase: Saturation
% 2.31/0.80 % (2844174)Time elapsed: 0.014 s
% 2.31/0.80 % (2844174)Peak memory usage: 12 MB
% 2.31/0.80 % (2844174)Instructions burned: 15 (million)
% 2.31/0.80 % (2844173)Instruction limit reached!
% 2.31/0.80 % (2844173)------------------------------
% 2.31/0.80 % (2844173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.80 % (2844173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.80 % (2844173)CaDiCaL version: 2.1.3
% 2.31/0.80 % (2844173)Termination reason: Instruction limit
% 2.31/0.80 % (2844173)Termination phase: Saturation
% 2.31/0.80 % (2844173)Time elapsed: 0.024 s
% 2.31/0.80 % (2844173)Peak memory usage: 12 MB
% 2.31/0.80 % (2844173)Instructions burned: 25 (million)
% 2.31/0.80 % (2844185)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=916591338:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 2.31/0.80 % (2844176)Instruction limit reached!
% 2.31/0.80 % (2844176)------------------------------
% 2.31/0.80 % (2844176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.80 % (2844176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.80 % (2844176)CaDiCaL version: 2.1.3
% 2.31/0.80 % (2844176)Termination reason: Instruction limit
% 2.31/0.80 % (2844176)Termination phase: Saturation
% 2.31/0.80 % (2844176)Time elapsed: 0.025 s
% 2.31/0.80 % (2844176)Peak memory usage: 12 MB
% 2.31/0.80 % (2844176)Instructions burned: 15 (million)
% 2.31/0.80 % (2844185)Instruction limit reached!
% 2.31/0.80 % (2844185)------------------------------
% 2.31/0.80 % (2844185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.31/0.80 % (2844186)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3595306339:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.31/0.80 % (2844185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.31/0.80 % (2844185)CaDiCaL version: 2.1.3
% 2.31/0.80 % (2844185)Termination reason: Instruction limit
% 2.31/0.80 % (2844185)Termination phase: Saturation
% 2.31/0.80 % (2844185)Time elapsed: 0.016 s
% 2.31/0.80 % (2844185)Peak memory usage: 12 MB
% 2.31/0.80 % (2844185)Instructions burned: 33 (million)
% 2.31/0.80 % (2844187)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3667144234:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.31/0.80 % (2844191)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.31/0.80 % (2844191)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=2530179533:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.84/0.87 % (2844186)Instruction limit reached!
% 2.84/0.87 % (2844186)------------------------------
% 2.84/0.87 % (2844186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.87 % (2844186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.87 % (2844186)CaDiCaL version: 2.1.3
% 2.84/0.87 % (2844186)Termination reason: Instruction limit
% 2.84/0.87 % (2844186)Termination phase: Saturation
% 2.84/0.87 % (2844186)Time elapsed: 0.019 s
% 2.84/0.87 % (2844186)Peak memory usage: 11 MB
% 2.84/0.87 % (2844186)Instructions burned: 24 (million)
% 2.84/0.87 % (2844189)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.84/0.87 % (2844189)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.84/0.87 % (2844191)Instruction limit reached!
% 2.84/0.87 % (2844191)------------------------------
% 2.84/0.87 % (2844191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.87 % (2844191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.87 % (2844191)CaDiCaL version: 2.1.3
% 2.84/0.87 % (2844191)Termination reason: Instruction limit
% 2.84/0.87 % (2844191)Termination phase: Saturation
% 2.84/0.87 % (2844191)Time elapsed: 0.007 s
% 2.84/0.87 % (2844191)Peak memory usage: 12 MB
% 2.84/0.87 % (2844191)Instructions burned: 13 (million)
% 2.84/0.87 % (2844189)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=1462176649:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.84/0.87 % (2844195)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2469264670:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.84/0.87 % (2844189)Instruction limit reached!
% 2.84/0.87 % (2844189)------------------------------
% 2.84/0.87 % (2844189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.87 % (2844189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.87 % (2844189)CaDiCaL version: 2.1.3
% 2.84/0.87 % (2844189)Termination reason: Instruction limit
% 2.84/0.87 % (2844189)Termination phase: Saturation
% 2.84/0.87 % (2844189)Time elapsed: 0.015 s
% 2.84/0.87 % (2844189)Peak memory usage: 12 MB
% 2.84/0.87 % (2844189)Instructions burned: 14 (million)
% 2.84/0.87 % (2844195)Instruction limit reached!
% 2.84/0.87 % (2844195)------------------------------
% 2.84/0.87 % (2844195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.87 % (2844195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.87 % (2844195)CaDiCaL version: 2.1.3
% 2.84/0.87 % (2844195)Termination reason: Instruction limit
% 2.84/0.87 % (2844195)Termination phase: Saturation
% 2.84/0.87 % (2844195)Time elapsed: 0.004 s
% 2.84/0.87 % (2844195)Peak memory usage: 12 MB
% 2.84/0.87 % (2844195)Instructions burned: 8 (million)
% 2.84/0.87 % (2844194)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=3302384267:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.84/0.87 % (2844198)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2495814140:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.84/0.87 % (2844187)Instruction limit reached!
% 2.84/0.87 % (2844187)------------------------------
% 2.84/0.87 % (2844187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.87 % (2844187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.87 % (2844187)CaDiCaL version: 2.1.3
% 2.84/0.87 % (2844187)Termination reason: Instruction limit
% 2.84/0.87 % (2844187)Termination phase: Saturation
% 2.84/0.87 % (2844187)Time elapsed: 0.056 s
% 2.84/0.87 % (2844187)Peak memory usage: 12 MB
% 2.84/0.87 % (2844187)Instructions burned: 61 (million)
% 2.84/0.87 % (2844198)Instruction limit reached!
% 2.84/0.87 % (2844198)------------------------------
% 2.84/0.87 % (2844198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.87 % (2844198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/0.92 % (2844198)CaDiCaL version: 2.1.3
% 3.43/0.92 % (2844198)Termination reason: Instruction limit
% 3.43/0.92 % (2844198)Termination phase: Saturation
% 3.43/0.92 % (2844198)Time elapsed: 0.012 s
% 3.43/0.92 % (2844198)Peak memory usage: 11 MB
% 3.43/0.92 % (2844198)Instructions burned: 27 (million)
% 3.43/0.92 % (2844194)Instruction limit reached!
% 3.43/0.92 % (2844194)------------------------------
% 3.43/0.92 % (2844194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/0.92 % (2844194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/0.92 % (2844194)CaDiCaL version: 2.1.3
% 3.43/0.92 % (2844194)Termination reason: Instruction limit
% 3.43/0.92 % (2844194)Termination phase: Saturation
% 3.43/0.92 % (2844194)Time elapsed: 0.027 s
% 3.43/0.92 % (2844194)Peak memory usage: 12 MB
% 3.43/0.92 % (2844194)Instructions burned: 31 (million)
% 3.43/0.92 % (2844199)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2981611482:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.43/0.92 % (2844203)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2452672267:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.43/0.92 % (2844202)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=123101680:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.43/0.92 % (2844199)Instruction limit reached!
% 3.43/0.92 % (2844199)------------------------------
% 3.43/0.92 % (2844199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/0.92 % (2844199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/0.92 % (2844199)CaDiCaL version: 2.1.3
% 3.43/0.92 % (2844199)Termination reason: Instruction limit
% 3.43/0.92 % (2844199)Termination phase: Saturation
% 3.43/0.92 % (2844199)Time elapsed: 0.020 s
% 3.43/0.92 % (2844199)Peak memory usage: 12 MB
% 3.43/0.92 % (2844199)Instructions burned: 20 (million)
% 3.43/0.92 % (2844204)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2512206280:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.43/0.92 % (2844209)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2910514681:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.43/0.92 % (2844169)Instruction limit reached!
% 3.43/0.92 % (2844169)------------------------------
% 3.43/0.92 % (2844169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/0.92 % (2844169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/0.92 % (2844169)CaDiCaL version: 2.1.3
% 3.43/0.92 % (2844169)Termination reason: Instruction limit
% 3.43/0.92 % (2844169)Termination phase: Saturation
% 3.43/0.92 % (2844169)Time elapsed: 0.188 s
% 3.43/0.92 % (2844169)Peak memory usage: 12 MB
% 3.43/0.92 % (2844169)Instructions burned: 249 (million)
% 3.43/0.92 % (2844203)Instruction limit reached!
% 3.43/0.92 % (2844203)------------------------------
% 3.43/0.92 % (2844203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/0.92 % (2844203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/0.92 % (2844203)CaDiCaL version: 2.1.3
% 3.43/0.92 % (2844203)Termination reason: Instruction limit
% 3.43/0.92 % (2844203)Termination phase: Saturation
% 3.43/0.92 % (2844203)Time elapsed: 0.066 s
% 3.43/0.92 % (2844203)Peak memory usage: 12 MB
% 3.43/0.92 % (2844203)Instructions burned: 145 (million)
% 3.43/0.92 % (2844212)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.43/0.92 % (2844209)Instruction limit reached!
% 3.43/0.92 % (2844209)------------------------------
% 3.43/0.92 % (2844209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/0.92 % (2844209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/0.92 % (2844209)CaDiCaL version: 2.1.3
% 3.43/0.92 % (2844209)Termination reason: Instruction limit
% 3.43/0.92 % (2844209)Termination phase: Saturation
% 3.43/0.92 % (2844209)Time elapsed: 0.034 s
% 3.43/0.92 % (2844209)Peak memory usage: 12 MB
% 3.43/0.92 % (2844209)Instructions burned: 42 (million)
% 3.43/0.92 % (2844212)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=474176509:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.43/0.92 % (2844212)Instruction limit reached!
% 3.43/1.02 % (2844212)------------------------------
% 3.43/1.02 % (2844212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/1.02 % (2844212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.02 % (2844212)CaDiCaL version: 2.1.3
% 3.43/1.02 % (2844212)Termination reason: Instruction limit
% 3.43/1.02 % (2844212)Termination phase: Saturation
% 3.43/1.02 % (2844212)Time elapsed: 0.007 s
% 3.43/1.02 % (2844212)Peak memory usage: 12 MB
% 3.43/1.02 % (2844212)Instructions burned: 8 (million)
% 3.43/1.02 % (2844213)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=166388755:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/181Mi)
% 3.43/1.02 % (2844214)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=80614804:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/169Mi)
% 3.43/1.02 % (2844175)Instruction limit reached!
% 3.43/1.02 % (2844175)------------------------------
% 3.43/1.02 % (2844175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/1.02 % (2844175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.02 % (2844175)CaDiCaL version: 2.1.3
% 3.43/1.02 % (2844175)Termination reason: Instruction limit
% 3.43/1.02 % (2844175)Termination phase: Saturation
% 3.43/1.02 % (2844175)Time elapsed: 0.245 s
% 3.43/1.02 % (2844175)Peak memory usage: 13 MB
% 3.43/1.02 % (2844175)Instructions burned: 327 (million)
% 3.43/1.02 % (2844217)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.43/1.02 % (2844214)Refutation not found, incomplete strategy
% 3.43/1.02 % (2844214)------------------------------
% 3.43/1.02 % (2844214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/1.02 % (2844214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.02 % (2844214)CaDiCaL version: 2.1.3
% 3.43/1.02 % (2844214)Termination reason: Refutation not found, incomplete strategy
% 3.43/1.02 % (2844214)Time elapsed: 0.004 s
% 3.43/1.02 % (2844214)Peak memory usage: 12 MB
% 3.43/1.02 % (2844214)Instructions burned: 3 (million)
% 3.43/1.02 % (2844214)------------------------------
% 3.43/1.02 % (2844214)------------------------------
% 3.43/1.02 % (2844217)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1494154405:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 3.43/1.02 % (2844217)Instruction limit reached!
% 3.43/1.02 % (2844217)------------------------------
% 3.43/1.02 % (2844217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/1.02 % (2844217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.02 % (2844217)CaDiCaL version: 2.1.3
% 3.43/1.02 % (2844217)Termination reason: Instruction limit
% 3.43/1.02 % (2844217)Termination phase: Saturation
% 3.43/1.02 % (2844217)Time elapsed: 0.006 s
% 3.43/1.02 % (2844217)Peak memory usage: 12 MB
% 3.43/1.02 % (2844217)Instructions burned: 6 (million)
% 3.43/1.02 % (2844219)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1079809768:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 3.43/1.02 % (2844220)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3720239003:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.43/1.02 % (2844220)Refutation not found, incomplete strategy
% 3.43/1.02 % (2844220)------------------------------
% 3.43/1.02 % (2844220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.43/1.02 % (2844220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.02 % (2844220)CaDiCaL version: 2.1.3
% 3.43/1.02 % (2844220)Termination reason: Refutation not found, incomplete strategy
% 3.43/1.02 % (2844220)Time elapsed: 0.006 s
% 3.43/1.02 % (2844220)Peak memory usage: 12 MB
% 3.43/1.02 % (2844220)Instructions burned: 6 (million)
% 3.43/1.02 % (2844220)------------------------------
% 3.43/1.02 % (2844220)------------------------------
% 3.43/1.02 % (2844222)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=442320077:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 5.36/1.18 % (2844219)Instruction limit reached!
% 5.36/1.18 % (2844219)------------------------------
% 5.36/1.18 % (2844219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/1.18 % (2844219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.18 % (2844219)CaDiCaL version: 2.1.3
% 5.36/1.18 % (2844219)Termination reason: Instruction limit
% 5.36/1.18 % (2844219)Termination phase: Saturation
% 5.36/1.18 % (2844219)Time elapsed: 0.021 s
% 5.36/1.18 % (2844219)Peak memory usage: 12 MB
% 5.36/1.18 % (2844219)Instructions burned: 23 (million)
% 5.36/1.18 % (2844204)Instruction limit reached!
% 5.36/1.18 % (2844204)------------------------------
% 5.36/1.18 % (2844204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/1.18 % (2844204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.18 % (2844204)CaDiCaL version: 2.1.3
% 5.36/1.18 % (2844204)Termination reason: Instruction limit
% 5.36/1.18 % (2844204)Termination phase: Saturation
% 5.36/1.18 % (2844204)Time elapsed: 0.147 s
% 5.36/1.18 % (2844204)Peak memory usage: 13 MB
% 5.36/1.18 % (2844204)Instructions burned: 194 (million)
% 5.36/1.18 % (2844213)Instruction limit reached!
% 5.36/1.18 % (2844213)------------------------------
% 5.36/1.18 % (2844213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/1.18 % (2844213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.18 % (2844213)CaDiCaL version: 2.1.3
% 5.36/1.18 % (2844213)Termination reason: Instruction limit
% 5.36/1.18 % (2844213)Termination phase: Saturation
% 5.36/1.18 % (2844213)Time elapsed: 0.079 s
% 5.36/1.18 % (2844213)Peak memory usage: 13 MB
% 5.36/1.18 % (2844213)Instructions burned: 181 (million)
% 5.36/1.18 % (2844229)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3335965901:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.36/1.18 % (2844225)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=207684975:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.36/1.18 % (2844229)Instruction limit reached!
% 5.36/1.18 % (2844229)------------------------------
% 5.36/1.18 % (2844229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/1.18 % (2844229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.18 % (2844229)CaDiCaL version: 2.1.3
% 5.36/1.18 % (2844229)Termination reason: Instruction limit
% 5.36/1.18 % (2844229)Termination phase: Saturation
% 5.36/1.18 % (2844229)Time elapsed: 0.011 s
% 5.36/1.18 % (2844229)Peak memory usage: 12 MB
% 5.36/1.18 % (2844229)Instructions burned: 21 (million)
% 5.36/1.18 % (2844228)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2157613670:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 5.36/1.18 % (2844227)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=770349382:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 5.36/1.18 % (2844228)Refutation not found, incomplete strategy
% 5.36/1.18 % (2844228)------------------------------
% 5.36/1.18 % (2844228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/1.18 % (2844228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.18 % (2844228)CaDiCaL version: 2.1.3
% 5.36/1.18 % (2844228)Termination reason: Refutation not found, incomplete strategy
% 5.36/1.18 % (2844228)Time elapsed: 0.005 s
% 5.36/1.18 % (2844228)Peak memory usage: 12 MB
% 5.36/1.18 % (2844228)Instructions burned: 4 (million)
% 5.36/1.18 % (2844228)------------------------------
% 5.36/1.18 % (2844228)------------------------------
% 5.36/1.18 % (2844144)Instruction limit reached!
% 5.36/1.18 % (2844144)------------------------------
% 5.36/1.18 % (2844144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.36/1.18 % (2844144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.18 % (2844144)CaDiCaL version: 2.1.3
% 5.36/1.18 % (2844144)Termination reason: Instruction limit
% 5.36/1.18 % (2844144)Termination phase: Saturation
% 5.36/1.18 % (2844144)Time elapsed: 0.503 s
% 6.05/1.33 % (2844144)Peak memory usage: 14 MB
% 6.05/1.33 % (2844144)Instructions burned: 634 (million)
% 6.05/1.33 % (2844232)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.05/1.33 % (2844232)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=889372782:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 6.05/1.33 % (2844235)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1576913945:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 6.05/1.33 % (2844227)Instruction limit reached!
% 6.05/1.33 % (2844227)------------------------------
% 6.05/1.33 % (2844227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.33 % (2844227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.33 % (2844227)CaDiCaL version: 2.1.3
% 6.05/1.33 % (2844227)Termination reason: Instruction limit
% 6.05/1.33 % (2844227)Termination phase: Saturation
% 6.05/1.33 % (2844227)Time elapsed: 0.046 s
% 6.05/1.33 % (2844227)Peak memory usage: 12 MB
% 6.05/1.33 % (2844227)Instructions burned: 46 (million)
% 6.05/1.33 % (2844236)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=3148745395:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 6.05/1.33 % (2844235)Instruction limit reached!
% 6.05/1.33 % (2844235)------------------------------
% 6.05/1.33 % (2844235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.33 % (2844235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.33 % (2844235)CaDiCaL version: 2.1.3
% 6.05/1.33 % (2844235)Termination reason: Instruction limit
% 6.05/1.33 % (2844235)Termination phase: Saturation
% 6.05/1.33 % (2844235)Time elapsed: 0.013 s
% 6.05/1.33 % (2844235)Peak memory usage: 12 MB
% 6.05/1.33 % (2844235)Instructions burned: 13 (million)
% 6.05/1.33 % (2844240)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2847111195:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 6.05/1.33 % (2844241)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1356816671:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/31Mi)
% 6.05/1.33 % (2844240)Refutation not found, incomplete strategy
% 6.05/1.33 % (2844240)------------------------------
% 6.05/1.33 % (2844240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.33 % (2844240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.33 % (2844240)CaDiCaL version: 2.1.3
% 6.05/1.33 % (2844240)Termination reason: Refutation not found, incomplete strategy
% 6.05/1.33 % (2844240)Time elapsed: 0.006 s
% 6.05/1.33 % (2844240)Peak memory usage: 12 MB
% 6.05/1.33 % (2844240)Instructions burned: 5 (million)
% 6.05/1.33 % (2844240)------------------------------
% 6.05/1.33 % (2844240)------------------------------
% 6.05/1.33 % (2844232)Instruction limit reached!
% 6.05/1.33 % (2844232)------------------------------
% 6.05/1.33 % (2844232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.33 % (2844232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.33 % (2844232)CaDiCaL version: 2.1.3
% 6.05/1.33 % (2844232)Termination reason: Instruction limit
% 6.05/1.33 % (2844232)Termination phase: Saturation
% 6.05/1.33 % (2844232)Time elapsed: 0.086 s
% 6.05/1.33 % (2844232)Peak memory usage: 12 MB
% 6.05/1.33 % (2844232)Instructions burned: 200 (million)
% 6.05/1.33 % (2844236)Instruction limit reached!
% 6.05/1.33 % (2844236)------------------------------
% 6.05/1.33 % (2844236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.33 % (2844236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.33 % (2844236)CaDiCaL version: 2.1.3
% 6.05/1.33 % (2844236)Termination reason: Instruction limit
% 6.05/1.33 % (2844236)Termination phase: Saturation
% 6.05/1.33 % (2844236)Time elapsed: 0.060 s
% 6.05/1.33 % (2844236)Peak memory usage: 12 MB
% 6.05/1.33 % (2844236)Instructions burned: 66 (million)
% 6.05/1.33 % (2844241)Instruction limit reached!
% 6.05/1.33 % (2844241)------------------------------
% 6.05/1.33 % (2844241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.33 % (2844241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.33 % (2844241)CaDiCaL version: 2.1.3
% 6.99/1.59 % (2844241)Termination reason: Instruction limit
% 6.99/1.59 % (2844241)Termination phase: Saturation
% 6.99/1.59 % (2844241)Time elapsed: 0.027 s
% 6.99/1.59 % (2844241)Peak memory usage: 12 MB
% 6.99/1.59 % (2844241)Instructions burned: 31 (million)
% 6.99/1.59 % (2844244)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3536788654:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.99/1.59 % (2844247)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.99/1.59 % (2844246)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3879060882:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 6.99/1.59 % (2844247)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1580317171:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2993 on theBenchmark for (2993ds/180Mi)
% 6.99/1.59 % (2844245)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=27261251:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 6.99/1.59 % (2844245)Instruction limit reached!
% 6.99/1.59 % (2844245)------------------------------
% 6.99/1.59 % (2844245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.59 % (2844245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.59 % (2844245)CaDiCaL version: 2.1.3
% 6.99/1.59 % (2844245)Termination reason: Instruction limit
% 6.99/1.59 % (2844245)Termination phase: Saturation
% 6.99/1.59 % (2844245)Time elapsed: 0.018 s
% 6.99/1.59 % (2844245)Peak memory usage: 12 MB
% 6.99/1.59 % (2844245)Instructions burned: 35 (million)
% 6.99/1.59 % (2844246)Instruction limit reached!
% 6.99/1.59 % (2844246)------------------------------
% 6.99/1.59 % (2844246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.59 % (2844246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.59 % (2844246)CaDiCaL version: 2.1.3
% 6.99/1.59 % (2844246)Termination reason: Instruction limit
% 6.99/1.59 % (2844246)Termination phase: Saturation
% 6.99/1.59 % (2844246)Time elapsed: 0.058 s
% 6.99/1.59 % (2844246)Peak memory usage: 12 MB
% 6.99/1.59 % (2844246)Instructions burned: 68 (million)
% 6.99/1.59 % (2844252)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=687611546:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 6.99/1.59 % (2844253)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1114345938:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 6.99/1.59 % (2844222)Instruction limit reached!
% 6.99/1.59 % (2844222)------------------------------
% 6.99/1.59 % (2844222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.59 % (2844222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.59 % (2844222)CaDiCaL version: 2.1.3
% 6.99/1.59 % (2844222)Termination reason: Instruction limit
% 6.99/1.59 % (2844222)Termination phase: Saturation
% 6.99/1.59 % (2844222)Time elapsed: 0.277 s
% 6.99/1.59 % (2844222)Peak memory usage: 14 MB
% 6.99/1.59 % (2844222)Instructions burned: 316 (million)
% 6.99/1.59 % (2844244)Instruction limit reached!
% 6.99/1.59 % (2844244)------------------------------
% 6.99/1.59 % (2844244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.59 % (2844244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.59 % (2844244)CaDiCaL version: 2.1.3
% 6.99/1.59 % (2844244)Termination reason: Instruction limit
% 6.99/1.59 % (2844244)Termination phase: Saturation
% 6.99/1.59 % (2844244)Time elapsed: 0.123 s
% 6.99/1.59 % (2844244)Peak memory usage: 12 MB
% 6.99/1.59 % (2844244)Instructions burned: 137 (million)
% 6.99/1.59 % (2844256)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3553353878:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 6.99/1.59 % (2844256)Refutation not found, incomplete strategy
% 6.99/1.59 % (2844256)------------------------------
% 6.99/1.59 % (2844256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.59 % (2844256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.59 % (2844256)CaDiCaL version: 2.1.3
% 6.99/1.59 % (2844256)Termination reason: Refutation not found, incomplete strategy
% 6.99/1.59 % (2844256)Time elapsed: 0.003 s
% 8.17/1.74 % (2844256)Peak memory usage: 12 MB
% 8.17/1.74 % (2844256)Instructions burned: 1 (million)
% 8.17/1.74 % (2844256)------------------------------
% 8.17/1.74 % (2844256)------------------------------
% 8.17/1.74 % (2844257)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2224682674:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/874Mi)
% 8.17/1.74 % (2844247)Instruction limit reached!
% 8.17/1.74 % (2844247)------------------------------
% 8.17/1.74 % (2844247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.74 % (2844247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.74 % (2844247)CaDiCaL version: 2.1.3
% 8.17/1.74 % (2844247)Termination reason: Instruction limit
% 8.17/1.74 % (2844247)Termination phase: Saturation
% 8.17/1.74 % (2844247)Time elapsed: 0.135 s
% 8.17/1.74 % (2844247)Peak memory usage: 12 MB
% 8.17/1.74 % (2844247)Instructions burned: 182 (million)
% 8.17/1.74 % (2844261)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3442803581:st=1.5:i=130:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 8.17/1.74 % (2844260)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3087674225:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/515Mi)
% 8.17/1.74 % (2844253)Instruction limit reached!
% 8.17/1.74 % (2844253)------------------------------
% 8.17/1.74 % (2844253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.74 % (2844253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.74 % (2844253)CaDiCaL version: 2.1.3
% 8.17/1.74 % (2844253)Termination reason: Instruction limit
% 8.17/1.74 % (2844253)Termination phase: Saturation
% 8.17/1.74 % (2844253)Time elapsed: 0.087 s
% 8.17/1.74 % (2844253)Peak memory usage: 12 MB
% 8.17/1.74 % (2844253)Instructions burned: 96 (million)
% 8.17/1.74 % (2844264)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2819652671:i=44:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/44Mi)
% 8.17/1.74 % (2844261)Instruction limit reached!
% 8.17/1.74 % (2844261)------------------------------
% 8.17/1.74 % (2844261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.74 % (2844261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.74 % (2844261)CaDiCaL version: 2.1.3
% 8.17/1.74 % (2844261)Termination reason: Instruction limit
% 8.17/1.74 % (2844261)Termination phase: Saturation
% 8.17/1.74 % (2844261)Time elapsed: 0.063 s
% 8.17/1.74 % (2844261)Peak memory usage: 13 MB
% 8.17/1.74 % (2844261)Instructions burned: 132 (million)
% 8.17/1.74 % (2844266)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2283126295:s2a=on:i=571:nm=16:rtra=on_2990 on theBenchmark for (2990ds/571Mi)
% 8.17/1.74 % (2844266)Refutation not found, incomplete strategy
% 8.17/1.74 % (2844266)------------------------------
% 8.17/1.74 % (2844266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.74 % (2844266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.74 % (2844266)CaDiCaL version: 2.1.3
% 8.17/1.74 % (2844266)Termination reason: Refutation not found, incomplete strategy
% 8.17/1.74 % (2844266)Time elapsed: 0.003 s
% 8.17/1.74 % (2844266)Peak memory usage: 12 MB
% 8.17/1.74 % (2844266)Instructions burned: 5 (million)
% 8.17/1.74 % (2844266)------------------------------
% 8.17/1.74 % (2844266)------------------------------
% 8.17/1.74 % (2844264)Instruction limit reached!
% 8.17/1.74 % (2844264)------------------------------
% 8.17/1.74 % (2844264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.74 % (2844264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.17/1.74 % (2844264)CaDiCaL version: 2.1.3
% 8.17/1.74 % (2844264)Termination reason: Instruction limit
% 8.17/1.74 % (2844264)Termination phase: Saturation
% 8.17/1.74 % (2844264)Time elapsed: 0.042 s
% 8.17/1.74 % (2844264)Peak memory usage: 12 MB
% 8.17/1.74 % (2844264)Instructions burned: 44 (million)
% 8.17/1.74 % (2844268)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=440223259:i=450:rtra=on:ixr=off:ntd=on_2990 on theBenchmark for (2990ds/450Mi)
% 8.17/1.74 % (2844252)Instruction limit reached!
% 8.17/1.74 % (2844252)------------------------------
% 8.17/1.74 % (2844252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.17/1.74 % (2844252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.88 % (2844252)CaDiCaL version: 2.1.3
% 8.62/1.88 % (2844252)Termination reason: Instruction limit
% 8.62/1.88 % (2844252)Termination phase: Saturation
% 8.62/1.88 % (2844252)Time elapsed: 0.208 s
% 8.62/1.88 % (2844252)Peak memory usage: 13 MB
% 8.62/1.88 % (2844252)Instructions burned: 247 (million)
% 8.62/1.88 % (2844269)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=4115467311:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/95Mi)
% 8.62/1.88 % (2844271)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=3211875668:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 8.62/1.88 % (2844271)Instruction limit reached!
% 8.62/1.88 % (2844271)------------------------------
% 8.62/1.88 % (2844271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.88 % (2844271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.88 % (2844271)CaDiCaL version: 2.1.3
% 8.62/1.88 % (2844271)Termination reason: Instruction limit
% 8.62/1.88 % (2844271)Termination phase: Saturation
% 8.62/1.88 % (2844271)Time elapsed: 0.060 s
% 8.62/1.88 % (2844271)Peak memory usage: 12 MB
% 8.62/1.88 % (2844271)Instructions burned: 65 (million)
% 8.62/1.88 % (2844269)Instruction limit reached!
% 8.62/1.88 % (2844269)------------------------------
% 8.62/1.88 % (2844269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.88 % (2844269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.88 % (2844269)CaDiCaL version: 2.1.3
% 8.62/1.88 % (2844269)Termination reason: Instruction limit
% 8.62/1.88 % (2844269)Termination phase: Saturation
% 8.62/1.88 % (2844269)Time elapsed: 0.093 s
% 8.62/1.88 % (2844269)Peak memory usage: 12 MB
% 8.62/1.88 % (2844269)Instructions burned: 96 (million)
% 8.62/1.88 % (2844274)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=4001780908:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2989 on theBenchmark for (2989ds/105Mi)
% 8.62/1.88 % (2844275)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=289827190:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2989 on theBenchmark for (2989ds/5755Mi)
% 8.62/1.88 % (2844268)Instruction limit reached!
% 8.62/1.88 % (2844268)------------------------------
% 8.62/1.88 % (2844268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.88 % (2844268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.88 % (2844268)CaDiCaL version: 2.1.3
% 8.62/1.88 % (2844268)Termination reason: Instruction limit
% 8.62/1.88 % (2844268)Termination phase: Saturation
% 8.62/1.88 % (2844268)Time elapsed: 0.194 s
% 8.62/1.88 % (2844268)Peak memory usage: 13 MB
% 8.62/1.88 % (2844268)Instructions burned: 451 (million)
% 8.62/1.88 % (2844278)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=498585795:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/375Mi)
% 8.62/1.88 % (2844274)Instruction limit reached!
% 8.62/1.88 % (2844274)------------------------------
% 8.62/1.88 % (2844274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.88 % (2844274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.88 % (2844274)CaDiCaL version: 2.1.3
% 8.62/1.88 % (2844274)Termination reason: Instruction limit
% 8.62/1.88 % (2844274)Termination phase: Saturation
% 8.62/1.88 % (2844274)Time elapsed: 0.091 s
% 8.62/1.88 % (2844274)Peak memory usage: 12 MB
% 8.62/1.88 % (2844274)Instructions burned: 105 (million)
% 8.62/1.88 % (2844280)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1667225908:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2988 on theBenchmark for (2988ds/495Mi)
% 8.62/1.88 % (2844225)Instruction limit reached!
% 8.62/1.88 % (2844225)------------------------------
% 8.62/1.88 % (2844225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.88 % (2844225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.88 % (2844225)CaDiCaL version: 2.1.3
% 8.62/1.88 % (2844225)Termination reason: Instruction limit
% 9.87/1.97 % (2844225)Termination phase: Saturation
% 9.87/1.97 % (2844225)Time elapsed: 0.692 s
% 9.87/1.97 % (2844225)Peak memory usage: 15 MB
% 9.87/1.97 % (2844225)Instructions burned: 854 (million)
% 9.87/1.97 % (2844260)Instruction limit reached!
% 9.87/1.97 % (2844260)------------------------------
% 9.87/1.97 % (2844260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.87/1.97 % (2844260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/1.97 % (2844260)CaDiCaL version: 2.1.3
% 9.87/1.97 % (2844260)Termination reason: Instruction limit
% 9.87/1.97 % (2844260)Termination phase: Saturation
% 9.87/1.97 % (2844260)Time elapsed: 0.390 s
% 9.87/1.97 % (2844260)Peak memory usage: 13 MB
% 9.87/1.97 % (2844260)Instructions burned: 515 (million)
% 9.87/1.97 % (2844282)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=1643394026:cond=on:i=34:hud=10:nm=10:rtra=on_2987 on theBenchmark for (2987ds/34Mi)
% 9.87/1.97 % (2844283)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1849475653:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/91Mi)
% 9.87/1.97 % (2844282)Instruction limit reached!
% 9.87/1.97 % (2844282)------------------------------
% 9.87/1.97 % (2844282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.87/1.97 % (2844282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/1.97 % (2844282)CaDiCaL version: 2.1.3
% 9.87/1.97 % (2844282)Termination reason: Instruction limit
% 9.87/1.97 % (2844282)Termination phase: Saturation
% 9.87/1.97 % (2844282)Time elapsed: 0.030 s
% 9.87/1.97 % (2844282)Peak memory usage: 12 MB
% 9.87/1.97 % (2844282)Instructions burned: 34 (million)
% 9.87/1.97 % (2844202)Instruction limit reached!
% 9.87/1.97 % (2844202)------------------------------
% 9.87/1.97 % (2844202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.87/1.97 % (2844202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/1.97 % (2844202)CaDiCaL version: 2.1.3
% 9.87/1.97 % (2844202)Termination reason: Instruction limit
% 9.87/1.97 % (2844202)Termination phase: Saturation
% 9.87/1.97 % (2844202)Time elapsed: 0.967 s
% 9.87/1.97 % (2844202)Peak memory usage: 15 MB
% 9.87/1.97 % (2844202)Instructions burned: 1240 (million)
% 9.87/1.97 % (2844286)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=43732903:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2987 on theBenchmark for (2987ds/66Mi)
% 9.87/1.97 % (2844286)Refutation not found, incomplete strategy
% 9.87/1.97 % (2844286)------------------------------
% 9.87/1.97 % (2844286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.87/1.97 % (2844286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/1.97 % (2844286)CaDiCaL version: 2.1.3
% 9.87/1.97 % (2844286)Termination reason: Refutation not found, incomplete strategy
% 9.87/1.97 % (2844286)Time elapsed: 0.003 s
% 9.87/1.97 % (2844286)Peak memory usage: 12 MB
% 9.87/1.97 % (2844286)Instructions burned: 2 (million)
% 9.87/1.97 % (2844286)------------------------------
% 9.87/1.97 % (2844286)------------------------------
% 9.87/1.97 % (2844283)Instruction limit reached!
% 9.87/1.97 % (2844283)------------------------------
% 9.87/1.97 % (2844283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.87/1.97 % (2844283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/1.97 % (2844283)CaDiCaL version: 2.1.3
% 9.87/1.97 % (2844283)Termination reason: Instruction limit
% 9.87/1.97 % (2844283)Termination phase: Saturation
% 9.87/1.97 % (2844283)Time elapsed: 0.076 s
% 9.87/1.97 % (2844283)Peak memory usage: 12 MB
% 9.87/1.97 % (2844283)Instructions burned: 91 (million)
% 9.87/1.97 % (2844287)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1276740107:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2986 on theBenchmark for (2986ds/22Mi)
% 9.87/1.97 % (2844289)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=3646825344:i=338:bd=all:ins=4:rtra=on_2986 on theBenchmark for (2986ds/338Mi)
% 9.87/1.97 % (2844287)Instruction limit reached!
% 9.87/1.97 % (2844287)------------------------------
% 9.87/1.97 % (2844287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.87/1.97 % (2844287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.42/2.17 % (2844287)CaDiCaL version: 2.1.3
% 12.42/2.17 % (2844287)Termination reason: Instruction limit
% 12.42/2.17 % (2844287)Termination phase: Saturation
% 12.42/2.17 % (2844287)Time elapsed: 0.019 s
% 12.42/2.17 % (2844287)Peak memory usage: 12 MB
% 12.42/2.17 % (2844287)Instructions burned: 22 (million)
% 12.42/2.17 % (2844290)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2197928455:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/28Mi)
% 12.42/2.17 % (2844293)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 12.42/2.17 % (2844293)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=527083151:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2986 on theBenchmark for (2986ds/137Mi)
% 12.42/2.17 % (2844280)Instruction limit reached!
% 12.42/2.17 % (2844280)------------------------------
% 12.42/2.17 % (2844280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.42/2.17 % (2844280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.42/2.17 % (2844280)CaDiCaL version: 2.1.3
% 12.42/2.17 % (2844280)Termination reason: Instruction limit
% 12.42/2.17 % (2844280)Termination phase: Saturation
% 12.42/2.17 % (2844280)Time elapsed: 0.203 s
% 12.42/2.17 % (2844280)Peak memory usage: 14 MB
% 12.42/2.17 % (2844280)Instructions burned: 496 (million)
% 12.42/2.17 % (2844290)Instruction limit reached!
% 12.42/2.17 % (2844290)------------------------------
% 12.42/2.17 % (2844290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.42/2.17 % (2844290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.42/2.17 % (2844290)CaDiCaL version: 2.1.3
% 12.42/2.17 % (2844290)Termination reason: Instruction limit
% 12.42/2.17 % (2844290)Termination phase: Saturation
% 12.42/2.17 % (2844290)Time elapsed: 0.025 s
% 12.42/2.17 % (2844290)Peak memory usage: 12 MB
% 12.42/2.17 % (2844290)Instructions burned: 28 (million)
% 12.42/2.17 % (2844296)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=190410128:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/340Mi)
% 12.42/2.17 % (2844297)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2255809127:i=227:sd=1:bd=all:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/227Mi)
% 12.42/2.17 % (2844297)Refutation not found, incomplete strategy
% 12.42/2.17 % (2844297)------------------------------
% 12.42/2.17 % (2844297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.42/2.17 % (2844297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.42/2.17 % (2844297)CaDiCaL version: 2.1.3
% 12.42/2.17 % (2844297)Termination reason: Refutation not found, incomplete strategy
% 12.42/2.17 % (2844297)Time elapsed: 0.003 s
% 12.42/2.17 % (2844297)Peak memory usage: 12 MB
% 12.42/2.17 % (2844297)Instructions burned: 1 (million)
% 12.42/2.17 % (2844297)------------------------------
% 12.42/2.17 % (2844297)------------------------------
% 12.42/2.17 % (2844257)Instruction limit reached!
% 12.42/2.17 % (2844257)------------------------------
% 12.42/2.17 % (2844257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.42/2.17 % (2844257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.42/2.17 % (2844257)CaDiCaL version: 2.1.3
% 12.42/2.17 % (2844257)Termination reason: Instruction limit
% 12.42/2.17 % (2844257)Termination phase: Saturation
% 12.42/2.17 % (2844257)Time elapsed: 0.651 s
% 12.42/2.17 % (2844257)Peak memory usage: 14 MB
% 12.42/2.17 % (2844257)Instructions burned: 874 (million)
% 12.42/2.17 % (2844300)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 12.42/2.17 % (2844300)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2219217593:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/373Mi)
% 12.42/2.17 % (2844301)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3030937310:i=116:ep=RSTC:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/116Mi)
% 12.42/2.17 % (2844278)Instruction limit reached!
% 12.42/2.17 % (2844278)------------------------------
% 12.42/2.17 % (2844278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.42/2.17 % (2844278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844278)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844278)Termination reason: Instruction limit
% 12.56/2.26 % (2844278)Termination phase: Saturation
% 12.56/2.26 % (2844278)Time elapsed: 0.330 s
% 12.56/2.26 % (2844278)Peak memory usage: 13 MB
% 12.56/2.26 % (2844278)Instructions burned: 376 (million)
% 12.56/2.26 % (2844293)Instruction limit reached!
% 12.56/2.26 % (2844293)------------------------------
% 12.56/2.26 % (2844293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844293)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844293)Termination reason: Instruction limit
% 12.56/2.26 % (2844293)Termination phase: Saturation
% 12.56/2.26 % (2844293)Time elapsed: 0.123 s
% 12.56/2.26 % (2844293)Peak memory usage: 13 MB
% 12.56/2.26 % (2844293)Instructions burned: 137 (million)
% 12.56/2.26 % (2844304)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1635142611:i=575:rtra=on_2984 on theBenchmark for (2984ds/575Mi)
% 12.56/2.26 % (2844304)Refutation not found, incomplete strategy
% 12.56/2.26 % (2844304)------------------------------
% 12.56/2.26 % (2844304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844304)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844304)Termination reason: Refutation not found, incomplete strategy
% 12.56/2.26 % (2844304)Time elapsed: 0.005 s
% 12.56/2.26 % (2844304)Peak memory usage: 12 MB
% 12.56/2.26 % (2844304)Instructions burned: 4 (million)
% 12.56/2.26 % (2844304)------------------------------
% 12.56/2.26 % (2844304)------------------------------
% 12.56/2.26 % (2844305)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3140550657:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2984 on theBenchmark for (2984ds/270Mi)
% 12.56/2.26 % (2844296)Instruction limit reached!
% 12.56/2.26 % (2844296)------------------------------
% 12.56/2.26 % (2844296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844296)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844296)Termination reason: Instruction limit
% 12.56/2.26 % (2844296)Termination phase: Saturation
% 12.56/2.26 % (2844296)Time elapsed: 0.146 s
% 12.56/2.26 % (2844296)Peak memory usage: 13 MB
% 12.56/2.26 % (2844296)Instructions burned: 341 (million)
% 12.56/2.26 % (2844307)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=2777637472: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_2984 on theBenchmark for (2984ds/9840Mi)
% 12.56/2.26 % (2844309)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3352534931:i=421:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/421Mi)
% 12.56/2.26 % (2844309)Refutation not found, incomplete strategy
% 12.56/2.26 % (2844309)------------------------------
% 12.56/2.26 % (2844309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844309)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844309)Termination reason: Refutation not found, incomplete strategy
% 12.56/2.26 % (2844309)Time elapsed: 0.002 s
% 12.56/2.26 % (2844309)Peak memory usage: 12 MB
% 12.56/2.26 % (2844309)Instructions burned: 2 (million)
% 12.56/2.26 % (2844309)------------------------------
% 12.56/2.26 % (2844309)------------------------------
% 12.56/2.26 % (2844312)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
% 12.56/2.26 % (2844301)Instruction limit reached!
% 12.56/2.26 % (2844301)------------------------------
% 12.56/2.26 % (2844301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844301)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844301)Termination reason: Instruction limit
% 12.56/2.26 % (2844301)Termination phase: Saturation
% 12.56/2.26 % (2844301)Time elapsed: 0.103 s
% 12.56/2.26 % (2844301)Peak memory usage: 12 MB
% 12.56/2.26 % (2844301)Instructions burned: 117 (million)
% 12.56/2.26 % (2844312)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=2715894961:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/270Mi)
% 12.56/2.26 % (2844314)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3291881346:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/31Mi)
% 12.56/2.26 % (2844289)Instruction limit reached!
% 12.56/2.26 % (2844289)------------------------------
% 12.56/2.26 % (2844289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844289)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844289)Termination reason: Instruction limit
% 12.56/2.26 % (2844289)Termination phase: Saturation
% 12.56/2.26 % (2844289)Time elapsed: 0.296 s
% 12.56/2.26 % (2844289)Peak memory usage: 15 MB
% 12.56/2.26 % (2844289)Instructions burned: 338 (million)
% 12.56/2.26 % (2844314)Instruction limit reached!
% 12.56/2.26 % (2844314)------------------------------
% 12.56/2.26 % (2844314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844314)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844314)Termination reason: Instruction limit
% 12.56/2.26 % (2844314)Termination phase: Saturation
% 12.56/2.26 % (2844314)Time elapsed: 0.030 s
% 12.56/2.26 % (2844314)Peak memory usage: 12 MB
% 12.56/2.26 % (2844314)Instructions burned: 31 (million)
% 12.56/2.26 % (2844316)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 12.56/2.26 % (2844316)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
% 12.56/2.26 % (2844316)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=3834851337:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2983 on theBenchmark for (2983ds/1440Mi)
% 12.56/2.26 % (2844317)dis+10_2_sil=128000:si=on:random_seed=1995607562:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2983 on theBenchmark for (2983ds/339Mi)
% 12.56/2.26 % (2844312)Instruction limit reached!
% 12.56/2.26 % (2844312)------------------------------
% 12.56/2.26 % (2844312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844312)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844312)Termination reason: Instruction limit
% 12.56/2.26 % (2844312)Termination phase: Saturation
% 12.56/2.26 % (2844312)Time elapsed: 0.118 s
% 12.56/2.26 % (2844312)Peak memory usage: 13 MB
% 12.56/2.26 % (2844312)Instructions burned: 271 (million)
% 12.56/2.26 % (2844320)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=99670660:i=111:add=on:fgj=on:rtra=on:fdi=1024_2982 on theBenchmark for (2982ds/111Mi)
% 12.56/2.26 % (2844300)Instruction limit reached!
% 12.56/2.26 % (2844300)------------------------------
% 12.56/2.26 % (2844300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844300)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844300)Termination reason: Instruction limit
% 12.56/2.26 % (2844300)Termination phase: Saturation
% 12.56/2.26 % (2844300)Time elapsed: 0.304 s
% 12.56/2.26 % (2844300)Peak memory usage: 13 MB
% 12.56/2.26 % (2844300)Instructions burned: 374 (million)
% 12.56/2.26 % (2844320)Instruction limit reached!
% 12.56/2.26 % (2844320)------------------------------
% 12.56/2.26 % (2844320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844320)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844320)Termination reason: Instruction limit
% 12.56/2.26 % (2844320)Termination phase: Saturation
% 12.56/2.26 % (2844320)Time elapsed: 0.050 s
% 12.56/2.26 % (2844320)Peak memory usage: 12 MB
% 12.56/2.26 % (2844320)Instructions burned: 111 (million)
% 12.56/2.26 % (2844305)Instruction limit reached!
% 12.56/2.26 % (2844305)------------------------------
% 12.56/2.26 % (2844305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844305)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844305)Termination reason: Instruction limit
% 12.56/2.26 % (2844305)Termination phase: Saturation
% 12.56/2.26 % (2844305)Time elapsed: 0.245 s
% 12.56/2.26 % (2844305)Peak memory usage: 13 MB
% 12.56/2.26 % (2844305)Instructions burned: 270 (million)
% 12.56/2.26 % (2844322)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=4153236032:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2982 on theBenchmark for (2982ds/122Mi)
% 12.56/2.26 % (2844323)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=1524389618:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/136Mi)
% 12.56/2.26 % (2844322)Refutation not found, incomplete strategy
% 12.56/2.26 % (2844322)------------------------------
% 12.56/2.26 % (2844322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844322)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844322)Termination reason: Refutation not found, incomplete strategy
% 12.56/2.26 % (2844322)Time elapsed: 0.004 s
% 12.56/2.26 % (2844322)Peak memory usage: 12 MB
% 12.56/2.26 % (2844322)Instructions burned: 3 (million)
% 12.56/2.26 % (2844322)------------------------------
% 12.56/2.26 % (2844322)------------------------------
% 12.56/2.26 % (2844324)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3053070538:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2981 on theBenchmark for (2981ds/232Mi)
% 12.56/2.26 % (2844327)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=2376473037:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2981 on theBenchmark for (2981ds/1254Mi)
% 12.56/2.26 % (2844327)Refutation not found, incomplete strategy
% 12.56/2.26 % (2844327)------------------------------
% 12.56/2.26 % (2844327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844327)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844327)Termination reason: Refutation not found, incomplete strategy
% 12.56/2.26 % (2844327)Time elapsed: 0.009 s
% 12.56/2.26 % (2844327)Peak memory usage: 12 MB
% 12.56/2.26 % (2844327)Instructions burned: 9 (million)
% 12.56/2.26 % (2844327)------------------------------
% 12.56/2.26 % (2844327)------------------------------
% 12.56/2.26 % (2844323)Instruction limit reached!
% 12.56/2.26 % (2844323)------------------------------
% 12.56/2.26 % (2844323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.26 % (2844323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.26 % (2844323)CaDiCaL version: 2.1.3
% 12.56/2.26 % (2844323)Termination reason: Instruction limit
% 12.56/2.26 % (2844323)Termination phase: Saturation
% 12.56/2.26 % (2844323)Time elapsed: 0.059 s
% 12.56/2.26 % (2844323)Peak memory usage: 12 MB
% 12.56/2.26 % (2844323)Instructions burned: 137 (million)
% 12.56/2.26 % (2844316) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2844136-2844316"...
% 12.56/2.26 % (2844330)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 12.56/2.26 % (2844316)...printing done.
% 12.56/2.26 % (2844331)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=875036468:i=619:add=on:rtra=on_2981 on theBenchmark for (2981ds/619Mi)
% 12.56/2.26 % (2844316)Refutation found. Thanks to Tanya!
% 12.56/2.26 % SZS status Theorem for theBenchmark
% 12.56/2.26 % SZS output start Proof for theBenchmark
% See solution above
% 12.56/2.27 % (2844316)------------------------------
% 12.56/2.27 % (2844316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.56/2.27 % (2844316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.27 % (2844316)CaDiCaL version: 2.1.3
% 12.56/2.27 % (2844316)Termination reason: Refutation
% 12.56/2.27 % (2844316)Time elapsed: 0.200 s
% 12.56/2.27 % (2844316)Peak memory usage: 13 MB
% 12.56/2.27 % (2844316)Instructions burned: 233 (million)
% 12.56/2.27 % (2844136)Success in time 1.895 s
% 12.56/2.27 % Vampire exiting
%------------------------------------------------------------------------------