%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO011^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:48:43 AM UTC 2026
% Result : Theorem 113.02s 24.05s
% Output : Refutation 113.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 10
% Syntax : Number of formulae : 72 ( 31 unt; 0 typ; 8 def)
% Number of atoms : 306 ( 106 equ; 0 cnn)
% Maximal formula atoms : 5 ( 4 avg)
% Number of connectives : 297 ( 33 ~; 52 |; 8 &; 182 @)
% ( 2 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 48 ( 48 >; 0 *; 0 +; 0 <<)
% Number of symbols : 76 ( 72 usr; 7 con; 0-6 aty)
% ( 6 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 105 ( 2 sgn 58 !; 0 ?; 105 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
leibeq: $i > $i > $o ).
thf(func_def_2,type,
p: ( $i > $i ) > $o ).
thf(func_def_3,type,
f: $i > $i ).
thf(func_def_4,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_5,type,
vIMP: $o > $o > $o ).
thf(func_def_6,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_7,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_8,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_9,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_12,type,
sF0: $o ).
thf(func_def_13,type,
sF1: $o ).
thf(func_def_14,type,
sF2: $i > $i ).
thf(func_def_15,type,
sF3: $i > $o ).
thf(func_def_16,type,
vNOT: $o > $o ).
thf(func_def_17,type,
sK4: $i > $i > $o ).
thf(func_def_19,type,
sF6: ( $i > $o ) > $i > $o ).
thf(func_def_20,type,
sF7:
!>[X0: $tType] : ( $i > ( $i > X0 ) > X0 ) ).
thf(func_def_21,type,
sF8: ( $i > $i ) > $o ).
thf(func_def_22,type,
sF9: ( ( $i > $i ) > $o ) > ( $i > $i ) > $o ).
thf(func_def_23,type,
sF10: ( $i > $i ) > $o ).
thf(func_def_24,type,
sF11: $i > $i ).
thf(func_def_25,type,
sF12: ( ( $i > $i ) > $o ) > $o ).
thf(func_def_26,type,
sF13:
!>[X0: $tType,X1: $tType] : ( ( ( X0 > X1 ) > $o ) > ( X0 > X1 ) > $o ) ).
thf(func_def_27,type,
sF14:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X1 > X2 ) > X0 > X1 > X2 ) ).
thf(func_def_28,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_29,type,
sF15: ( $i > $i ) > $i > $i ).
thf(func_def_30,type,
sF16: ( $i > $i > $i ) > $i > $i > $i ).
thf(func_def_31,type,
sF17: $i > ( ( $i > $i ) > $o ) > ( $i > $i > $i ) > $o ).
thf(func_def_32,type,
sF18: ( $i > $i > $i ) > $i > $i > $i ).
thf(func_def_33,type,
sF19:
!>[X0: $tType] : ( ( $i > X0 ) > ( ( $i > X0 ) > $o ) > $o ) ).
thf(func_def_34,type,
sF20:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( X0 > X2 ) > X1 > X2 ) > ( X0 > X2 ) > X1 > X2 ) ).
thf(func_def_35,type,
sF21:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( ( $i > X0 ) > X1 > X2 ) > ( $i > X0 ) > X1 > X2 ) ).
thf(func_def_36,type,
sF22: $i > ( ( $i > $i ) > $o ) > ( $i > $i > $i ) > $o ).
thf(func_def_37,type,
sF23: $i > $i > $i ).
thf(func_def_38,type,
sF24:
!>[X0: $tType,X1: $tType] : ( ( $i > X0 > X1 ) > $i > X0 > X1 ) ).
thf(func_def_39,type,
sF25:
!>[X0: $tType] : ( X0 > ( X0 > $o ) > $o ) ).
thf(func_def_40,type,
sF26: $i > ( ( $i > $i ) > $o ) > ( $i > $i > $i ) > $o ).
thf(func_def_41,type,
sF27: $i > ( $i > $i > $i ) > $i > $i ).
thf(func_def_42,type,
sF28: $i > ( $i > $i > $i ) > $i > $i ).
thf(func_def_43,type,
sK29: $i > $i ).
thf(func_def_44,type,
sF30: $i > ( $i > $i > $i ) > $i > $i ).
thf(func_def_45,type,
sF31:
!>[X0: $tType,X1: $tType,X2: $tType] : ( X0 > ( X0 > X2 > X1 ) > X2 > X1 ) ).
thf(func_def_46,type,
sF32:
!>[X0: $tType,X1: $tType] : ( ( ( $i > X0 ) > X1 ) > ( $i > X0 ) > X1 ) ).
thf(func_def_47,type,
sK33: $i > $i ).
thf(func_def_48,type,
sF34: $i > ( ( $i > $i ) > $o ) > ( $i > $i > $i ) > $o ).
thf(func_def_49,type,
sK35: ( $i > $i ) > $i ).
thf(func_def_50,type,
sF36: $i > ( $i > $i > $i ) > $i > $i ).
thf(func_def_51,type,
sF37:
!>[X0: $tType] : ( X0 > ( X0 > $i ) > $i ) ).
thf(func_def_52,type,
sF38:
!>[X0: $tType] : ( ( $i > $i ) > ( ( $i > $i ) > X0 ) > X0 ) ).
thf(func_def_53,type,
sF39:
!>[X0: $tType] : ( ( $i > $i ) > ( ( $i > $i ) > X0 ) > X0 ) ).
thf(func_def_54,type,
sF40: ( $i > $i ) > $i > $i ).
thf(func_def_55,type,
sF41:
!>[X0: $tType] : ( X0 > $i > X0 ) ).
thf(func_def_56,type,
sF42:
!>[X0: $tType] : ( ( $i > $i > $i > $i ) > ( ( $i > $i ) > X0 ) > X0 ) ).
thf(func_def_57,type,
sF43:
!>[X0: $tType,X1: $tType] : ( X1 > ( X1 > $i ) > ( $i > X0 ) > X0 ) ).
thf(func_def_58,type,
sF44:
!>[X0: $tType] : ( X0 > ( X0 > $i ) > $i > $i ) ).
thf(func_def_59,type,
sF45:
!>[X0: $tType] : ( ( $i > $i ) > ( ( $i > $i ) > X0 ) > X0 ) ).
thf(func_def_60,type,
sF46: ( $i > $i ) > $i > $i ).
thf(func_def_61,type,
sF47:
!>[X0: $tType,X1: $tType] : ( ( $i > X1 ) > ( X1 > $i ) > ( ( $i > $i ) > X0 ) > X0 ) ).
thf(func_def_62,type,
sF48: ( $i > $i ) > ( $i > $i > $i ) > $i > $i ).
thf(func_def_63,type,
sF49:
!>[X0: $tType] : ( ( X0 > $i ) > ( $i > X0 ) > X0 ) ).
thf(func_def_64,type,
sF50:
!>[X0: $tType] : ( ( $i > X0 ) > ( X0 > $i ) > $i ) ).
thf(func_def_65,type,
sF51: ( $i > $i ) > $i > $i ).
thf(func_def_66,type,
sF52:
!>[X0: $tType] : ( ( $i > $i ) > ( ( $i > $i ) > X0 ) > X0 ) ).
thf(func_def_67,type,
sF53:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( X0 > X2 ) > ( ( X0 > X2 ) > X1 ) > X1 ) ).
thf(func_def_68,type,
sF54: ( $i > $i ) > $i > $i ).
thf(func_def_69,type,
sF55:
!>[X0: $tType] : ( ( X0 > $i ) > ( ( X0 > $i ) > $i > $i ) > $i > $i ) ).
thf(func_def_70,type,
sF56:
!>[X0: $tType] : ( ( $i > X0 ) > ( ( $i > X0 ) > $i > $i ) > $i > $i ) ).
thf(func_def_71,type,
sF57:
!>[X0: $tType] : ( ( $i > X0 ) > ( X0 > $i ) > $i > $i ) ).
thf(func_def_72,type,
sF58:
!>[X0: $tType] : ( ( $i > X0 ) > ( ( $i > X0 ) > X0 ) > X0 ) ).
thf(f1,axiom,
( leibeq
= ( ^ [X0: $i,X1: $i] :
! [X2: $i > $o] :
( ( X2 @ X0 )
=> ( X2 @ X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leibeq) ).
thf(f2,conjecture,
( ( ! [X0: $i] : ( leibeq @ ( f @ X0 ) @ X0 )
& ( p
@ ^ [X0: $i] : X0 ) )
=> ( p @ f ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj) ).
thf(f3,negated_conjecture,
~ ( ( ! [X0: $i] : ( leibeq @ ( f @ X0 ) @ X0 )
& ( p
@ ^ [X0: $i] : X0 ) )
=> ( p @ f ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
thf(f4,plain,
( leibeq
= ( ^ [X0: $i,X1: $i] :
! [X2: $i > $o] :
( ( X2 @ X0 )
=> ( X2 @ X1 ) ) ) ),
inference(rectify,[],[f1]) ).
thf(f5,plain,
( leibeq
= ( ^ [Y0: $i,Y1: $i] :
( !! @ ( $i > $o )
@ ^ [Y2: $i > $o] :
( ( Y2 @ Y0 )
=> ( Y2 @ Y1 ) ) ) ) ),
inference(fool_elimination,[],[f4]) ).
thf(f6,plain,
~ ( ( ! [X0: $i] : ( leibeq @ ( f @ X0 ) @ X0 )
& ( p
@ ^ [X1: $i] : X1 ) )
=> ( p @ f ) ),
inference(rectify,[],[f3]) ).
thf(f7,plain,
~ ( ( ( $true
= ( p
@ ^ [Y0: $i] : Y0 ) )
& ! [X0: $i] :
( ( leibeq @ ( f @ X0 ) @ X0 )
= $true ) )
=> ( ( p @ f )
= $true ) ),
inference(fool_elimination,[],[f6]) ).
thf(f8,plain,
( ( ( p @ f )
!= $true )
& ( $true
= ( p
@ ^ [Y0: $i] : Y0 ) )
& ! [X0: $i] :
( ( leibeq @ ( f @ X0 ) @ X0 )
= $true ) ),
inference(ennf_transformation,[],[f7]) ).
thf(f9,plain,
( ( ( p @ f )
!= $true )
& ( $true
= ( p
@ ^ [Y0: $i] : Y0 ) )
& ! [X0: $i] :
( ( leibeq @ ( f @ X0 ) @ X0 )
= $true ) ),
inference(flattening,[],[f8]) ).
thf(f10,plain,
( leibeq
= ( ^ [Y0: $i,Y1: $i] :
( !! @ ( $i > $o )
@ ^ [Y2: $i > $o] :
( ( Y2 @ Y0 )
=> ( Y2 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[],[f5]) ).
thf(f11,plain,
! [X0: $i] :
( ( leibeq @ ( f @ X0 ) @ X0 )
= $true ),
inference(cnf_transformation,[],[f9]) ).
thf(f12,plain,
( $true
= ( p
@ ^ [Y0: $i] : Y0 ) ),
inference(cnf_transformation,[],[f9]) ).
thf(f13,plain,
( ( p @ f )
!= $true ),
inference(cnf_transformation,[],[f9]) ).
thf(f16,plain,
! [X0: $i] :
( $true
= ( ^ [Y0: $i,Y1: $i] :
( !! @ ( $i > $o )
@ ^ [Y2: $i > $o] :
( ( Y2 @ Y0 )
=> ( Y2 @ Y1 ) ) )
@ ( f @ X0 )
@ X0 ) ),
inference(definition_unfolding,[],[f11,f10]) ).
thf(f17,definition,
( sF0
= ( p @ f ) ),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
thf(f18,plain,
( ( p @ f )
= sF0 ),
inference(reorient_equations,[],[f17]) ).
thf(f19,plain,
$true != sF0,
inference(definition_folding,[],[f13,f18]) ).
thf(f20,definition,
( sF1
= ( p
@ ^ [Y0: $i] : Y0 ) ),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
thf(f21,plain,
( ( p
@ ^ [Y0: $i] : Y0 )
= sF1 ),
inference(reorient_equations,[],[f20]) ).
thf(f22,plain,
$true = sF1,
inference(definition_folding,[],[f12,f21]) ).
thf(f23,definition,
! [X0: $i] :
( ( sF2 @ X0 )
= ( f @ X0 ) ),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
thf(f24,plain,
! [X0: $i] :
( ( f @ X0 )
= ( sF2 @ X0 ) ),
inference(reorient_equations,[],[f23]) ).
thf(f25,definition,
! [X0: $i] :
( ( sF3 @ X0 )
= ( ^ [Y0: $i,Y1: $i] :
( !! @ ( $i > $o )
@ ^ [Y2: $i > $o] :
( ( Y2 @ Y0 )
=> ( Y2 @ Y1 ) ) )
@ ( sF2 @ X0 )
@ X0 ) ),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
thf(f26,plain,
! [X0: $i] :
( $true
= ( sF3 @ X0 ) ),
inference(definition_folding,[],[f16,f25,f24]) ).
thf(f28,plain,
( ( $true = sF0 )
| ( ( p @ f )
= $false ) ),
inference(iff_proxy_clausification,[],[f18]) ).
thf(f30,plain,
! [X0: $i] :
( ( $true
= ( ^ [Y0: $i,Y1: $i] :
( !! @ ( $i > $o )
@ ^ [Y2: $i > $o] :
( ( Y2 @ Y0 )
=> ( Y2 @ Y1 ) ) )
@ ( sF2 @ X0 )
@ X0 ) )
| ( ( sF3 @ X0 )
= $false ) ),
inference(iff_proxy_clausification,[],[f25]) ).
thf(f31,plain,
! [X0: $i] :
( ( $true
= ( !! @ ( $i > $o )
@ ^ [Y0: $i > $o] :
( ( Y0 @ ( sF2 @ X0 ) )
=> ( Y0 @ X0 ) ) ) )
| ( ( sF3 @ X0 )
= $false ) ),
inference(beta-eta_normalization,[],[f30]) ).
thf(f32,plain,
! [X0: $i,X1: $i > $o] :
( ( $true
= ( ^ [Y0: $i > $o] :
( ( Y0 @ ( sF2 @ X0 ) )
=> ( Y0 @ X0 ) )
@ X1 ) )
| ( ( sF3 @ X0 )
= $false ) ),
inference(pi_proxy_clausification,[],[f31]) ).
thf(f33,plain,
! [X0: $i,X1: $i > $o] :
( ( ( sF3 @ X0 )
= $false )
| ( $true
= ( ( X1 @ ( sF2 @ X0 ) )
=> ( X1 @ X0 ) ) ) ),
inference(beta-eta_normalization,[],[f32]) ).
thf(f34,plain,
! [X0: $i,X1: $i > $o] :
( ( $false
= ( X1 @ ( sF2 @ X0 ) ) )
| ( $true
= ( X1 @ X0 ) )
| ( ( sF3 @ X0 )
= $false ) ),
inference(imp_proxy_clausification,[],[f33]) ).
thf(f40,plain,
( ( $false = sF1 )
| ( $true
= ( p
@ ^ [Y0: $i] : Y0 ) ) ),
inference(iff_proxy_clausification,[],[f21]) ).
thf(f43,definition,
( spl5_1
<=> ( ( p @ f )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
thf(f45,plain,
( ( ( p @ f )
= $false )
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f43]) ).
thf(f47,definition,
( spl5_2
<=> ( $true = sF0 ) ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
thf(f50,plain,
( spl5_1
| spl5_2 ),
inference(avatar_split_clause,[],[f28,f47,f43]) ).
thf(f62,plain,
~ spl5_2,
inference(avatar_split_clause,[],[f19,f47]) ).
thf(f63,plain,
( ( $true
= ( p
@ ^ [Y0: $i] : Y0 ) )
| ( $true = $false ) ),
inference(forward_demodulation,[],[f40,f22]) ).
thf(f64,plain,
( $true
= ( p
@ ^ [Y0: $i] : Y0 ) ),
inference(trivial_inequality_removal,[],[f63]) ).
thf(f65,definition,
! [X0: $i > $i] :
( ( sF8 @ X0 )
= ( p @ X0 ) ),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
thf(f66,plain,
! [X0: $i > $i] :
( ( p @ X0 )
= ( sF8 @ X0 ) ),
inference(reorient_equations,[],[f65]) ).
thf(f73,plain,
! [X0: $i > $i] :
( ( ( p @ X0 )
= $true )
| ( ( sF8 @ X0 )
= $false ) ),
inference(iff_proxy_clausification,[],[f66]) ).
thf(f74,plain,
! [X0: $i > $i] :
( ( ( p @ X0 )
= $false )
| ( $true
= ( sF8 @ X0 ) ) ),
inference(iff_proxy_clausification,[],[f66]) ).
thf(f102,plain,
( ( $true
= ( sF8
@ ^ [Y0: $i] : Y0 ) )
| ( $true = $false ) ),
inference(constrained_superposition,[],[f64,f74]) ).
thf(f106,plain,
( $true
= ( sF8
@ ^ [Y0: $i] : Y0 ) ),
inference(trivial_inequality_removal,[],[f102]) ).
thf(f111,definition,
( sF11
= ( ^ [Y0: $i] : Y0 ) ),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
thf(f115,plain,
( $true
= ( sF8 @ sF11 ) ),
inference(constrained_superposition,[],[f106,f111]) ).
thf(f172,plain,
! [X0: $i] :
( ( ( sF2 @ X0 )
= X0 )
| ( ( sF3 @ X0 )
= $false ) ),
inference(leibniz_equality_elimination,[],[f34]) ).
thf(f179,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( $false
= ( sF8 @ X2 ) )
| ( ( sF3 @ X1 )
= $false )
| ( $true
= ( ^ [Y0: $i] : ( p @ ( X0 @ Y0 ) )
@ X1 ) )
| ( ( X0 @ ( sF2 @ X1 ) )
!= X2 )
| ( $true = $false ) ),
inference(constrained_superposition,[],[f34,f73]) ).
thf(f264,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( ( sF3 @ X1 )
= $false )
| ( $true
= ( ^ [Y0: $i] : ( p @ ( X0 @ Y0 ) )
@ X1 ) )
| ( ( X0 @ ( sF2 @ X1 ) )
!= X2 )
| ( $false
= ( sF8 @ X2 ) ) ),
inference(trivial_inequality_removal,[],[f179]) ).
thf(f265,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( ( sF3 @ X1 )
= $false )
| ( ( X0 @ ( sF2 @ X1 ) )
!= X2 )
| ( $false
= ( sF8 @ X2 ) )
| ( ( p @ ( X0 @ X1 ) )
= $true ) ),
inference(beta-eta_normalization,[],[f264]) ).
thf(f306,plain,
! [X0: $i] :
( ( ( sF3 @ X0 )
= $false )
| ( ( f @ X0 )
= X0 ) ),
inference(forward_demodulation,[],[f172,f24]) ).
thf(f308,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( $true = $false )
| ( $false
= ( sF8 @ X2 ) )
| ( ( X0 @ ( sF2 @ X1 ) )
!= X2 )
| ( ( p @ ( X0 @ X1 ) )
= $true ) ),
inference(forward_demodulation,[],[f265,f26]) ).
thf(f309,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( $false
= ( sF8 @ X2 ) )
| ( ( p @ ( X0 @ X1 ) )
= $true )
| ( ( X0 @ ( sF2 @ X1 ) )
!= X2 ) ),
inference(trivial_inequality_removal,[],[f308]) ).
thf(f330,plain,
! [X0: $i] :
( ( ( f @ X0 )
= X0 )
| ( $true = $false ) ),
inference(forward_demodulation,[],[f306,f26]) ).
thf(f331,plain,
! [X0: $i] :
( ( f @ X0 )
= X0 ),
inference(trivial_inequality_removal,[],[f330]) ).
thf(f334,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( $false
= ( sF8 @ X2 ) )
| ( ( X0 @ ( f @ X1 ) )
!= X2 )
| ( ( p @ ( X0 @ X1 ) )
= $true ) ),
inference(forward_demodulation,[],[f309,f24]) ).
thf(f349,plain,
! [X2: $i > $i,X0: $i > $i > $i,X1: $i] :
( ( $false
= ( sF8 @ X2 ) )
| ( ( p @ ( X0 @ X1 ) )
= $true )
| ( ( X0 @ X1 )
!= X2 ) ),
inference(forward_demodulation,[],[f334,f331]) ).
thf(f690,plain,
( ! [X2: $i,X1: $i > $i] :
( ( $false
= ( sF8 @ X1 ) )
| ( ( ^ [Y0: $i,Y1: $i] :
( f
@ ( ^ [Y2: $i,Y3: $i] : Y3
@ Y0
@ Y1 ) )
@ X2 )
!= X1 )
| ( $true = $false ) )
| ~ spl5_1 ),
inference(constrained_superposition,[],[f45,f349]) ).
thf(f693,plain,
( ! [X2: $i,X1: $i > $i] :
( ( ( ^ [Y0: $i,Y1: $i] :
( f
@ ( ^ [Y2: $i,Y3: $i] : Y3
@ Y0
@ Y1 ) )
@ X2 )
!= X1 )
| ( $false
= ( sF8 @ X1 ) ) )
| ~ spl5_1 ),
inference(trivial_inequality_removal,[],[f690]) ).
thf(f694,plain,
( ! [X1: $i > $i] :
( ( f != X1 )
| ( $false
= ( sF8 @ X1 ) ) )
| ~ spl5_1 ),
inference(beta-eta_normalization,[],[f693]) ).
thf(f738,plain,
( ! [X1: $i > $i] :
( ( $false
= ( sF8 @ X1 ) )
| ( ( f @ ( sK35 @ X1 ) )
!= ( X1 @ ( sK35 @ X1 ) ) ) )
| ~ spl5_1 ),
inference(negative_extensionality,[],[f694]) ).
thf(f743,plain,
( ! [X1: $i > $i] :
( ( ( X1 @ ( sK35 @ X1 ) )
!= ( sK35 @ X1 ) )
| ( $false
= ( sF8 @ X1 ) ) )
| ~ spl5_1 ),
inference(forward_demodulation,[],[f738,f331]) ).
thf(f752,plain,
( ( ( sF8
@ ^ [Y0: $i] : Y0 )
= $false )
| ~ spl5_1 ),
inference(equality_resolution,[],[f743]) ).
thf(f779,plain,
( ( ( sF8 @ sF11 )
= $false )
| ~ spl5_1 ),
inference(forward_demodulation,[],[f752,f111]) ).
thf(f791,plain,
( ( $true = $false )
| ~ spl5_1 ),
inference(constrained_superposition,[],[f779,f115]) ).
thf(f798,plain,
( $false
| ~ spl5_1 ),
inference(trivial_inequality_removal,[],[f791]) ).
thf(f799,plain,
~ spl5_1,
inference(avatar_contradiction_clause,[],[f798]) ).
cnf(s1,plain,
( spl5_1
| spl5_2 ),
inference(sat_conversion,[],[f50]) ).
cnf(s3,plain,
~ spl5_2,
inference(sat_conversion,[],[f62]) ).
cnf(s7,plain,
~ spl5_1,
inference(sat_conversion,[],[f799]) ).
cnf(s8,plain,
$false,
inference(rat,[],[s1,s3,s7]) ).
thf(f819,plain,
$false,
inference(avatar_sat_refutation,[],[s8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYO011^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Tue Sep 29 16:20:48 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.12 Running first-order model finding
% 0.08/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.49/0.42 % (312116)Will run a generic schedule for satisfiability detection.
% 1.49/0.42 % (312122)% WARNING: option uhcvi not known.
% 1.49/0.42 % (312126)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1795100496:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.49/0.42 % (312127)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=32231989:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.49/0.42 % (312124)dis+10_1_sil=32000:sp=arity:random_seed=3969843922:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.49/0.42 % (312121)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1374378745_2999 on theBenchmark for (2999ds/0Mi)
% 1.49/0.42 % (312125)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=748272945:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.49/0.42 % (312122)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=887029757:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.49/0.42 % (312123)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3299006212:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.49/0.42 % (312125)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.49/0.42 % (312122)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.49/0.42 % (312122)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.49/0.42 % Exception at run slice level
% 1.49/0.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.49/0.42 % (312124)Refutation not found, incomplete strategy
% 1.49/0.42 % (312124)------------------------------
% 1.49/0.42 % (312124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.42 % (312124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.42 % (312124)CaDiCaL version: 2.1.3
% 1.49/0.42 % (312124)Termination reason: Refutation not found, incomplete strategy
% 1.49/0.42 % (312124)Time elapsed: 0.002 s
% 1.49/0.42 % (312124)Peak memory usage: 11 MB
% 1.49/0.42 % (312124)Instructions burned: 3 (million)
% 1.49/0.42 % (312122)Refutation not found, incomplete strategy
% 1.49/0.42 % (312122)------------------------------
% 1.49/0.42 % (312122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.42 % (312122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.42 % (312122)CaDiCaL version: 2.1.3
% 1.49/0.42 % (312122)Termination reason: Refutation not found, incomplete strategy
% 1.49/0.42 % (312122)Time elapsed: 0.002 s
% 1.49/0.42 % (312122)Peak memory usage: 12 MB
% 1.49/0.42 % (312122)Instructions burned: 4 (million)
% 1.49/0.42 % (312124)------------------------------
% 1.49/0.42 % (312124)------------------------------
% 1.49/0.42 % (312122)------------------------------
% 1.49/0.42 % (312122)------------------------------
% 1.49/0.42 % (312135)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=588513387:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.49/0.42 % Exception at run slice level
% 1.49/0.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.49/0.42 % (312136)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=550719519:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.49/0.42 % (312137)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3865460794:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.49/0.42 % (312137)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.49/0.42 % (312137)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.49/0.42 % (312136)Refutation not found, incomplete strategy
% 1.49/0.42 % (312136)------------------------------
% 1.49/0.42 % (312136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.42 % (312136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.42 % (312136)CaDiCaL version: 2.1.3
% 1.49/0.42 % (312136)Termination reason: Refutation not found, incomplete strategy
% 1.49/0.42 % (312136)Time elapsed: 0.001 s
% 1.49/0.42 % (312136)Peak memory usage: 12 MB
% 1.49/0.42 % (312136)Instructions burned: 3 (million)
% 1.49/0.42 % (312137)Refutation not found, incomplete strategy
% 1.94/0.47 % (312137)------------------------------
% 1.94/0.47 % (312137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.47 % (312137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.47 % (312137)CaDiCaL version: 2.1.3
% 1.94/0.47 % (312137)Termination reason: Refutation not found, incomplete strategy
% 1.94/0.47 % (312137)Time elapsed: 0.001 s
% 1.94/0.47 % (312137)Peak memory usage: 12 MB
% 1.94/0.47 % (312137)Instructions burned: 3 (million)
% 1.94/0.47 % (312136)------------------------------
% 1.94/0.47 % (312136)------------------------------
% 1.94/0.47 % (312137)------------------------------
% 1.94/0.47 % (312137)------------------------------
% 1.94/0.47 % (312139)ott-21_1_sil=16000:fs=off:random_seed=2842569958:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.94/0.47 % (312142)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=272576451:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.94/0.47 % (312143)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1380956416:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 1.94/0.48 % Exception at run slice level
% 1.94/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.94/0.48 % (312125)Instruction limit reached!
% 1.94/0.48 % (312125)------------------------------
% 1.94/0.48 % (312125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.48 % (312125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.48 % (312125)CaDiCaL version: 2.1.3
% 1.94/0.48 % (312125)Termination reason: Instruction limit
% 1.94/0.48 % (312125)Termination phase: Saturation
% 1.94/0.48 % (312125)Time elapsed: 0.031 s
% 1.94/0.48 % (312125)Peak memory usage: 12 MB
% 1.94/0.48 % (312125)Instructions burned: 118 (million)
% 1.94/0.48 % (312142)Refutation not found, incomplete strategy
% 1.94/0.48 % (312142)------------------------------
% 1.94/0.48 % (312142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.48 % (312142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.48 % (312142)CaDiCaL version: 2.1.3
% 1.94/0.48 % (312142)Termination reason: Refutation not found, incomplete strategy
% 1.94/0.48 % (312142)Time elapsed: 0.006 s
% 1.94/0.48 % (312142)Peak memory usage: 12 MB
% 1.94/0.48 % (312142)Instructions burned: 17 (million)
% 1.94/0.48 % (312142)------------------------------
% 1.94/0.48 % (312142)------------------------------
% 1.94/0.48 % (312147)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3992635981:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 1.94/0.48 % (312148)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1240274700:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi)
% 1.94/0.48 % Exception at run slice level
% 1.94/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.94/0.48 % (312149)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4231162374:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2999 on theBenchmark for (2999ds/692Mi)
% 1.94/0.48 % (312149)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.94/0.48 % (312127)Instruction limit reached!
% 1.94/0.48 % (312127)------------------------------
% 1.94/0.48 % (312127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.48 % (312127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.48 % (312127)CaDiCaL version: 2.1.3
% 1.94/0.48 % (312127)Termination reason: Instruction limit
% 1.94/0.48 % (312127)Termination phase: Saturation
% 1.94/0.48 % (312127)Time elapsed: 0.046 s
% 1.94/0.48 % (312127)Peak memory usage: 13 MB
% 1.94/0.48 % (312127)Instructions burned: 161 (million)
% 1.94/0.48 % (312152)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2417145699:i=879:kws=inv_precedence:fsr=off_2999 on theBenchmark for (2999ds/879Mi)
% 1.94/0.48 % (312152)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.94/0.48 % (312154)fmb+10_1_sil=64000:random_seed=3225768361:i=22061:nm=2:gsp=on_2999 on theBenchmark for (2999ds/22061Mi)
% 1.94/0.48 % (312154)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 1.94/0.48 % Exception at run slice level
% 1.94/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.59/1.69 % (312126)Instruction limit reached!
% 9.59/1.69 % (312126)------------------------------
% 9.59/1.69 % (312126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.59/1.69 % (312126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.69 % (312126)CaDiCaL version: 2.1.3
% 9.59/1.69 % (312126)Termination reason: Instruction limit
% 9.59/1.69 % (312126)Termination phase: Saturation
% 9.59/1.69 % (312126)Time elapsed: 0.058 s
% 9.59/1.69 % (312126)Peak memory usage: 13 MB
% 9.59/1.69 % (312126)Instructions burned: 133 (million)
% 9.59/1.69 % (312139)Instruction limit reached!
% 9.59/1.69 % (312139)------------------------------
% 9.59/1.69 % (312139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.59/1.69 % (312139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.69 % (312139)CaDiCaL version: 2.1.3
% 9.59/1.69 % (312139)Termination reason: Instruction limit
% 9.59/1.69 % (312139)Termination phase: Saturation
% 9.59/1.69 % (312139)Time elapsed: 0.045 s
% 9.59/1.69 % (312139)Peak memory usage: 12 MB
% 9.59/1.69 % (312139)Instructions burned: 182 (million)
% 9.59/1.69 % (312157)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4098441358:i=9515:nm=5_2999 on theBenchmark for (2999ds/9515Mi)
% 9.59/1.69 % Exception at run slice level
% 9.59/1.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.59/1.69 % (312158)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2473863312:fmbsr=1.7:i=920_2999 on theBenchmark for (2999ds/920Mi)
% 9.59/1.69 % Exception at run slice level
% 9.59/1.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.59/1.69 % (312161)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3762857129:i=1472:ins=7:fdi=8:gsp=on_2999 on theBenchmark for (2999ds/1472Mi)
% 9.59/1.69 % (312160)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=83970152:i=5131_2999 on theBenchmark for (2999ds/5131Mi)
% 9.59/1.69 % (312160)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.59/1.69 % (312161)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 9.59/1.69 % (312161)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 9.59/1.69 % (312163)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=934993402:i=6324_2999 on theBenchmark for (2999ds/6324Mi)
% 9.59/1.69 % (312160)Refutation not found, incomplete strategy
% 9.59/1.69 % (312160)------------------------------
% 9.59/1.69 % (312160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.59/1.69 % (312160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.69 % (312160)CaDiCaL version: 2.1.3
% 9.59/1.69 % (312160)Termination reason: Refutation not found, incomplete strategy
% 9.59/1.69 % (312160)Time elapsed: 0.001 s
% 9.59/1.69 % (312160)Peak memory usage: 12 MB
% 9.59/1.69 % (312160)Instructions burned: 3 (million)
% 9.59/1.69 % Exception at run slice level
% 9.59/1.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.59/1.69 % (312160)------------------------------
% 9.59/1.69 % (312160)------------------------------
% 9.59/1.69 % (312167)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2459453574:fmbsr=2.30978:i=2174_2998 on theBenchmark for (2998ds/2174Mi)
% 9.59/1.69 % (312168)ott-2_1_sil=16000:newcnf=on:random_seed=2642442839:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2998 on theBenchmark for (2998ds/869Mi)
% 9.59/1.69 % Exception at run slice level
% 9.59/1.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.59/1.69 % (312168)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.59/1.69 % (312171)ott+10_1_sil=32000:tgt=ground:random_seed=3179401955:i=5114:av=off_2998 on theBenchmark for (2998ds/5114Mi)
% 9.59/1.69 % (312152)Instruction limit reached!
% 9.59/1.69 % (312152)------------------------------
% 9.59/1.69 % (312152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.59/1.69 % (312152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.69 % (312152)CaDiCaL version: 2.1.3
% 9.59/1.69 % (312152)Termination reason: Instruction limit
% 35.51/5.27 % (312152)Termination phase: Saturation
% 35.51/5.27 % (312152)Time elapsed: 0.214 s
% 35.51/5.27 % (312152)Peak memory usage: 20 MB
% 35.51/5.27 % (312152)Instructions burned: 879 (million)
% 35.51/5.27 % (312149)Instruction limit reached!
% 35.51/5.27 % (312149)------------------------------
% 35.51/5.27 % (312149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.51/5.27 % (312149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.51/5.27 % (312149)CaDiCaL version: 2.1.3
% 35.51/5.27 % (312149)Termination reason: Instruction limit
% 35.51/5.27 % (312149)Termination phase: Saturation
% 35.51/5.27 % (312149)Time elapsed: 0.229 s
% 35.51/5.27 % (312149)Peak memory usage: 21 MB
% 35.51/5.27 % (312149)Instructions burned: 693 (million)
% 35.51/5.27 % (312173)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=279685087:i=54282_2997 on theBenchmark for (2997ds/54282Mi)
% 35.51/5.27 % Exception at run slice level
% 35.51/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.51/5.27 % (312174)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1315476951:i=3512:aac=none_2996 on theBenchmark for (2996ds/3512Mi)
% 35.51/5.27 % (312174)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.51/5.27 % (312176)dis+21_1_sil=32000:sas=cadical:random_seed=717021477:i=3773:amm=off_2996 on theBenchmark for (2996ds/3773Mi)
% 35.51/5.27 % (312174)Refutation not found, incomplete strategy
% 35.51/5.27 % (312174)------------------------------
% 35.51/5.27 % (312174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.51/5.27 % (312174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.51/5.27 % (312174)CaDiCaL version: 2.1.3
% 35.51/5.27 % (312174)Termination reason: Refutation not found, incomplete strategy
% 35.51/5.27 % (312174)Time elapsed: 0.002 s
% 35.51/5.27 % (312174)Peak memory usage: 12 MB
% 35.51/5.27 % (312174)Instructions burned: 3 (million)
% 35.51/5.27 % (312176)Refutation not found, incomplete strategy
% 35.51/5.27 % (312176)------------------------------
% 35.51/5.27 % (312176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.51/5.27 % (312176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.51/5.27 % (312176)CaDiCaL version: 2.1.3
% 35.51/5.27 % (312176)Termination reason: Refutation not found, incomplete strategy
% 35.51/5.27 % (312176)Time elapsed: 0.001 s
% 35.51/5.27 % (312176)Peak memory usage: 12 MB
% 35.51/5.27 % (312176)Instructions burned: 4 (million)
% 35.51/5.27 % (312176)------------------------------
% 35.51/5.27 % (312176)------------------------------
% 35.51/5.27 % (312174)------------------------------
% 35.51/5.27 % (312174)------------------------------
% 35.51/5.27 % (312168)Instruction limit reached!
% 35.51/5.27 % (312168)------------------------------
% 35.51/5.27 % (312168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.51/5.27 % (312168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.51/5.27 % (312168)CaDiCaL version: 2.1.3
% 35.51/5.27 % (312168)Termination reason: Instruction limit
% 35.51/5.27 % (312168)Termination phase: Saturation
% 35.51/5.27 % (312168)Time elapsed: 0.210 s
% 35.51/5.27 % (312168)Peak memory usage: 23 MB
% 35.51/5.27 % (312168)Instructions burned: 873 (million)
% 35.51/5.27 % (312180)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1530491604:fmbsr=1.6:i=67534_2996 on theBenchmark for (2996ds/67534Mi)
% 35.51/5.27 % (312179)ott+11_1_sil=16000:gs=on:random_seed=1068896836:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2996 on theBenchmark for (2996ds/2251Mi)
% 35.51/5.27 % (312179)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.51/5.27 % Exception at run slice level
% 35.51/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.51/5.27 % (312181)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1381974438:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2996 on theBenchmark for (2996ds/4591Mi)
% 35.51/5.27 % (312147)Instruction limit reached!
% 35.51/5.27 % (312147)------------------------------
% 35.51/5.27 % (312147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.51/5.27 % (312147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.51/5.27 % (312147)CaDiCaL version: 2.1.3
% 35.51/5.27 % (312147)Termination reason: Instruction limit
% 48.40/7.09 % (312147)Termination phase: Saturation
% 48.40/7.09 % (312147)Time elapsed: 0.283 s
% 48.40/7.09 % (312147)Peak memory usage: 30 MB
% 48.40/7.09 % (312147)Instructions burned: 1179 (million)
% 48.40/7.09 % (312184)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2585495089:i=29340_2996 on theBenchmark for (2996ds/29340Mi)
% 48.40/7.09 % (312187)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1883745691:i=5211_2996 on theBenchmark for (2996ds/5211Mi)
% 48.40/7.09 % (312161)Instruction limit reached!
% 48.40/7.09 % (312161)------------------------------
% 48.40/7.09 % (312161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.40/7.09 % (312161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.40/7.09 % (312161)CaDiCaL version: 2.1.3
% 48.40/7.09 % (312161)Termination reason: Instruction limit
% 48.40/7.09 % (312161)Termination phase: Saturation
% 48.40/7.09 % (312161)Time elapsed: 0.367 s
% 48.40/7.09 % (312161)Peak memory usage: 16 MB
% 48.40/7.09 % (312161)Instructions burned: 1473 (million)
% 48.40/7.09 % (312189)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3253813923:i=5497:nm=2_2995 on theBenchmark for (2995ds/5497Mi)
% 48.40/7.09 % Exception at run slice level
% 48.40/7.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 48.40/7.09 % (312191)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1936896786:fmbsr=2:i=46332_2995 on theBenchmark for (2995ds/46332Mi)
% 48.40/7.09 % Exception at run slice level
% 48.40/7.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 48.40/7.09 % (312193)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1553546156:i=14071_2995 on theBenchmark for (2995ds/14071Mi)
% 48.40/7.09 % Exception at run slice level
% 48.40/7.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 48.40/7.09 % (312195)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2017980817:i=22565:add=on:rawr=on_2994 on theBenchmark for (2994ds/22565Mi)
% 48.40/7.09 % (312179)Instruction limit reached!
% 48.40/7.09 % (312179)------------------------------
% 48.40/7.09 % (312179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.40/7.09 % (312179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.40/7.09 % (312179)CaDiCaL version: 2.1.3
% 48.40/7.09 % (312179)Termination reason: Instruction limit
% 48.40/7.09 % (312179)Termination phase: Saturation
% 48.40/7.09 % (312179)Time elapsed: 0.534 s
% 48.40/7.09 % (312179)Peak memory usage: 43 MB
% 48.40/7.09 % (312179)Instructions burned: 2261 (million)
% 48.40/7.09 % (312197)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2026345343:i=8173:av=off_2991 on theBenchmark for (2991ds/8173Mi)
% 48.40/7.09 % (312171)Instruction limit reached!
% 48.40/7.09 % (312171)------------------------------
% 48.40/7.09 % (312171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.40/7.09 % (312171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.40/7.09 % (312171)CaDiCaL version: 2.1.3
% 48.40/7.09 % (312171)Termination reason: Instruction limit
% 48.40/7.09 % (312171)Termination phase: Saturation
% 48.40/7.09 % (312171)Time elapsed: 1.367 s
% 48.40/7.09 % (312171)Peak memory usage: 87 MB
% 48.40/7.09 % (312171)Instructions burned: 5117 (million)
% 48.40/7.09 % (312199)dis+10_16:1_sil=16000:random_seed=1293840252:i=9155:fsr=off_2984 on theBenchmark for (2984ds/9155Mi)
% 48.40/7.09 % (312199)Refutation not found, incomplete strategy
% 48.40/7.09 % (312199)------------------------------
% 48.40/7.09 % (312199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.40/7.09 % (312199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.40/7.09 % (312199)CaDiCaL version: 2.1.3
% 48.40/7.09 % (312199)Termination reason: Refutation not found, incomplete strategy
% 48.40/7.09 % (312199)Time elapsed: 0.002 s
% 48.40/7.09 % (312199)Peak memory usage: 12 MB
% 48.40/7.09 % (312199)Instructions burned: 3 (million)
% 48.40/7.09 % (312199)------------------------------
% 48.40/7.09 % (312199)------------------------------
% 48.40/7.09 % (312201)ott-3_8_sil=64000:random_seed=3526956323:i=20139:bs=on_2984 on theBenchmark for (2984ds/20139Mi)
% 48.40/7.09 % (312181)Instruction limit reached!
% 48.40/7.09 % (312181)------------------------------
% 48.40/7.09 % (312181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.40/7.09 % (312181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/7.27 % (312181)CaDiCaL version: 2.1.3
% 49.58/7.27 % (312181)Termination reason: Instruction limit
% 49.58/7.27 % (312181)Termination phase: Saturation
% 49.58/7.27 % (312181)Time elapsed: 1.223 s
% 49.58/7.27 % (312181)Peak memory usage: 30 MB
% 49.58/7.27 % (312181)Instructions burned: 4592 (million)
% 49.58/7.27 % (312203)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3582519551:fmbsr=2:i=32576_2984 on theBenchmark for (2984ds/32576Mi)
% 49.58/7.27 % Exception at run slice level
% 49.58/7.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 49.58/7.27 % (312205)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3254018014:i=11404_2984 on theBenchmark for (2984ds/11404Mi)
% 49.58/7.27 % (312187)Instruction limit reached!
% 49.58/7.27 % (312187)------------------------------
% 49.58/7.27 % (312187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.58/7.27 % (312187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/7.27 % (312187)CaDiCaL version: 2.1.3
% 49.58/7.27 % (312187)Termination reason: Instruction limit
% 49.58/7.27 % (312187)Termination phase: Saturation
% 49.58/7.27 % (312187)Time elapsed: 1.267 s
% 49.58/7.27 % (312187)Peak memory usage: 55 MB
% 49.58/7.27 % (312187)Instructions burned: 5215 (million)
% 49.58/7.27 % (312207)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=253964813:i=14134_2983 on theBenchmark for (2983ds/14134Mi)
% 49.58/7.27 % (312207)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 49.58/7.27 % (312197)Instruction limit reached!
% 49.58/7.27 % (312197)------------------------------
% 49.58/7.27 % (312197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.58/7.27 % (312197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/7.27 % (312197)CaDiCaL version: 2.1.3
% 49.58/7.27 % (312197)Termination reason: Instruction limit
% 49.58/7.27 % (312197)Termination phase: Saturation
% 49.58/7.27 % (312197)Time elapsed: 2.166 s
% 49.58/7.27 % (312197)Peak memory usage: 115 MB
% 49.58/7.27 % (312197)Instructions burned: 8175 (million)
% 49.58/7.27 % (312209)dis+33_16_sil=32000:sac=on:random_seed=393816229:i=15851:nm=0_2969 on theBenchmark for (2969ds/15851Mi)
% 49.58/7.27 % (312195)Instruction limit reached!
% 49.58/7.27 % (312195)------------------------------
% 49.58/7.27 % (312195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.58/7.27 % (312195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/7.27 % (312195)CaDiCaL version: 2.1.3
% 49.58/7.27 % (312195)Termination reason: Instruction limit
% 49.58/7.27 % (312195)Termination phase: Saturation
% 49.58/7.27 % (312195)Time elapsed: 4.022 s
% 49.58/7.27 % (312195)Peak memory usage: 25 MB
% 49.58/7.27 % (312195)Instructions burned: 22566 (million)
% 49.58/7.27 % (312211)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2513759348:avsq=on:i=17627:add=on:amm=off_2954 on theBenchmark for (2954ds/17627Mi)
% 49.58/7.27 % (312207)Instruction limit reached!
% 49.58/7.27 % (312207)------------------------------
% 49.58/7.27 % (312207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.58/7.27 % (312207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/7.27 % (312207)CaDiCaL version: 2.1.3
% 49.58/7.27 % (312207)Termination reason: Instruction limit
% 49.58/7.27 % (312207)Termination phase: Saturation
% 49.58/7.27 % (312207)Time elapsed: 3.458 s
% 49.58/7.27 % (312207)Peak memory usage: 213 MB
% 49.58/7.27 % (312207)Instructions burned: 14137 (million)
% 49.58/7.27 % (312213)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3809321908:s2a=on:i=53295_2948 on theBenchmark for (2948ds/53295Mi)
% 49.58/7.27 % (312213)Refutation not found, incomplete strategy
% 49.58/7.27 % (312213)------------------------------
% 49.58/7.27 % (312213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.58/7.27 % (312213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/7.27 % (312213)CaDiCaL version: 2.1.3
% 49.58/7.27 % (312213)Termination reason: Refutation not found, incomplete strategy
% 49.58/7.27 % (312213)Time elapsed: 0.003 s
% 49.58/7.27 % (312213)Peak memory usage: 12 MB
% 49.58/7.27 % (312213)Instructions burned: 5 (million)
% 49.58/7.27 % (312213)------------------------------
% 49.58/7.27 % (312213)------------------------------
% 49.58/7.27 % (312215)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1874633896:i=26857:ins=20_2948 on theBenchmark for (2948ds/26857Mi)
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312217)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2291535464:i=28120:bs=on:fsr=off_2948 on theBenchmark for (2948ds/28120Mi)
% 51.02/7.45 % (312205)Instruction limit reached!
% 51.02/7.45 % (312205)------------------------------
% 51.02/7.45 % (312205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.02/7.45 % (312205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.02/7.45 % (312205)CaDiCaL version: 2.1.3
% 51.02/7.45 % (312205)Termination reason: Instruction limit
% 51.02/7.45 % (312205)Termination phase: Saturation
% 51.02/7.45 % (312205)Time elapsed: 3.802 s
% 51.02/7.45 % (312205)Peak memory usage: 165 MB
% 51.02/7.45 % (312205)Instructions burned: 11405 (million)
% 51.02/7.45 % (312219)fmb+10_1_sil=256000:fmbss=7:random_seed=3266881791:fmbsr=1.6:i=182295_2945 on theBenchmark for (2945ds/182295Mi)
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312221)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3526087243:i=44625:gsp=on_2945 on theBenchmark for (2945ds/44625Mi)
% 51.02/7.45 % (312221)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 51.02/7.45 % (312221)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312223)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3261748261:i=160505_2945 on theBenchmark for (2945ds/160505Mi)
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312225)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2687433155:fmbsr=1.3:i=225729_2945 on theBenchmark for (2945ds/225729Mi)
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312227)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2678311114:fmbsr=2:i=185024:ins=7_2945 on theBenchmark for (2945ds/185024Mi)
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312229)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1153918824:rtra=on_2945 on theBenchmark for (2945ds/0Mi)
% 51.02/7.45 % Exception at run slice level
% 51.02/7.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.02/7.45 % (312231)% WARNING: option uhcvi not known.
% 51.02/7.45 % (312231)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3921593673:i=271062:add=off:rtra=on:rawr=on_2945 on theBenchmark for (2945ds/271062Mi)
% 51.02/7.45 % (312231)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 51.02/7.45 % (312231)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 51.02/7.45 % (312231)Refutation not found, incomplete strategy
% 51.02/7.45 % (312231)------------------------------
% 51.02/7.45 % (312231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.02/7.45 % (312231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.02/7.45 % (312231)CaDiCaL version: 2.1.3
% 51.02/7.45 % (312231)Termination reason: Refutation not found, incomplete strategy
% 51.02/7.45 % (312231)Time elapsed: 0.002 s
% 51.02/7.45 % (312231)Peak memory usage: 12 MB
% 51.02/7.45 % (312231)Instructions burned: 4 (million)
% 51.02/7.45 % (312231)------------------------------
% 51.02/7.45 % (312231)------------------------------
% 51.02/7.45 % (312233)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=482212682:i=176048:add=on:rtra=on:rawr=on_2944 on theBenchmark for (2944ds/176048Mi)
% 51.02/7.45 % (312201)Instruction limit reached!
% 51.02/7.45 % (312201)------------------------------
% 51.02/7.45 % (312201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.02/7.45 % (312201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.52/8.61 % (312201)CaDiCaL version: 2.1.3
% 59.52/8.61 % (312201)Termination reason: Instruction limit
% 59.52/8.61 % (312201)Termination phase: Saturation
% 59.52/8.61 % (312201)Time elapsed: 5.436 s
% 59.52/8.61 % (312201)Peak memory usage: 236 MB
% 59.52/8.61 % (312201)Instructions burned: 20141 (million)
% 59.52/8.61 % (312235)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2309850165:i=206:fgj=on:rtra=on_2930 on theBenchmark for (2930ds/206Mi)
% 59.52/8.61 % (312235)Refutation not found, incomplete strategy
% 59.52/8.61 % (312235)------------------------------
% 59.52/8.61 % (312235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.52/8.61 % (312235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.52/8.61 % (312235)CaDiCaL version: 2.1.3
% 59.52/8.61 % (312235)Termination reason: Refutation not found, incomplete strategy
% 59.52/8.61 % (312235)Time elapsed: 0.002 s
% 59.52/8.61 % (312235)Peak memory usage: 12 MB
% 59.52/8.61 % (312235)Instructions burned: 4 (million)
% 59.52/8.61 % (312235)------------------------------
% 59.52/8.61 % (312235)------------------------------
% 59.52/8.61 % (312237)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3963755658:i=232:rtra=on_2930 on theBenchmark for (2930ds/232Mi)
% 59.52/8.61 % (312237)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 59.52/8.61 % (312237)Refutation not found, incomplete strategy
% 59.52/8.61 % (312237)------------------------------
% 59.52/8.61 % (312237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.52/8.61 % (312237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.52/8.61 % (312237)CaDiCaL version: 2.1.3
% 59.52/8.61 % (312237)Termination reason: Refutation not found, incomplete strategy
% 59.52/8.61 % (312237)Time elapsed: 0.001 s
% 59.52/8.61 % (312237)Peak memory usage: 12 MB
% 59.52/8.61 % (312237)Instructions burned: 3 (million)
% 59.52/8.61 % (312237)------------------------------
% 59.52/8.61 % (312237)------------------------------
% 59.52/8.61 % (312239)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1840536981:i=262:rtra=on_2929 on theBenchmark for (2929ds/262Mi)
% 59.52/8.61 % (312239)Refutation not found, incomplete strategy
% 59.52/8.61 % (312239)------------------------------
% 59.52/8.61 % (312239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.52/8.61 % (312239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.52/8.61 % (312239)CaDiCaL version: 2.1.3
% 59.52/8.61 % (312239)Termination reason: Refutation not found, incomplete strategy
% 59.52/8.61 % (312239)Time elapsed: 0.001 s
% 59.52/8.61 % (312239)Peak memory usage: 12 MB
% 59.52/8.61 % (312239)Instructions burned: 3 (million)
% 59.52/8.61 % (312239)------------------------------
% 59.52/8.61 % (312239)------------------------------
% 59.52/8.61 % (312241)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3889876439:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2929 on theBenchmark for (2929ds/318Mi)
% 59.52/8.61 % (312241)Instruction limit reached!
% 59.52/8.61 % (312241)------------------------------
% 59.52/8.61 % (312241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.52/8.61 % (312241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.52/8.61 % (312241)CaDiCaL version: 2.1.3
% 59.52/8.61 % (312241)Termination reason: Instruction limit
% 59.52/8.61 % (312241)Termination phase: Saturation
% 59.52/8.61 % (312241)Time elapsed: 0.085 s
% 59.52/8.61 % (312241)Peak memory usage: 16 MB
% 59.52/8.61 % (312241)Instructions burned: 319 (million)
% 59.52/8.61 % (312243)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3863269487:i=1428:nm=2:rtra=on_2928 on theBenchmark for (2928ds/1428Mi)
% 59.52/8.61 % Exception at run slice level
% 59.52/8.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 59.52/8.61 % (312245)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=374564113:i=262:bd=preordered:rtra=on:fsd=on_2928 on theBenchmark for (2928ds/262Mi)
% 59.52/8.61 % (312245)Refutation not found, incomplete strategy
% 59.52/8.61 % (312245)------------------------------
% 59.52/8.61 % (312245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.52/8.61 % (312245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.52/8.61 % (312245)CaDiCaL version: 2.1.3
% 59.52/8.61 % (312245)Termination reason: Refutation not found, incomplete strategy
% 60.21/8.70 % (312245)Time elapsed: 0.002 s
% 60.21/8.70 % (312245)Peak memory usage: 12 MB
% 60.21/8.70 % (312245)Instructions burned: 3 (million)
% 60.21/8.70 % (312245)------------------------------
% 60.21/8.70 % (312245)------------------------------
% 60.21/8.70 % (312247)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1460169782:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2928 on theBenchmark for (2928ds/1368Mi)
% 60.21/8.70 % (312247)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 60.21/8.70 % (312247)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 60.21/8.70 % (312247)Refutation not found, incomplete strategy
% 60.21/8.70 % (312247)------------------------------
% 60.21/8.70 % (312247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.21/8.70 % (312247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.21/8.70 % (312247)CaDiCaL version: 2.1.3
% 60.21/8.70 % (312247)Termination reason: Refutation not found, incomplete strategy
% 60.21/8.70 % (312247)Time elapsed: 0.002 s
% 60.21/8.70 % (312247)Peak memory usage: 12 MB
% 60.21/8.70 % (312247)Instructions burned: 3 (million)
% 60.21/8.70 % (312247)------------------------------
% 60.21/8.70 % (312247)------------------------------
% 60.21/8.70 % (312249)ott-21_1_sil=16000:si=on:fs=off:random_seed=2830553007:i=360:av=off:fsr=off:rtra=on_2928 on theBenchmark for (2928ds/360Mi)
% 60.21/8.70 % (312249)Instruction limit reached!
% 60.21/8.70 % (312249)------------------------------
% 60.21/8.70 % (312249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.21/8.70 % (312249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.21/8.70 % (312249)CaDiCaL version: 2.1.3
% 60.21/8.70 % (312249)Termination reason: Instruction limit
% 60.21/8.70 % (312249)Termination phase: Saturation
% 60.21/8.70 % (312249)Time elapsed: 0.085 s
% 60.21/8.70 % (312249)Peak memory usage: 13 MB
% 60.21/8.70 % (312249)Instructions burned: 362 (million)
% 60.21/8.70 % (312251)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3879446177:i=954:bd=all:rtra=on_2927 on theBenchmark for (2927ds/954Mi)
% 60.21/8.70 % (312251)Refutation not found, incomplete strategy
% 60.21/8.70 % (312251)------------------------------
% 60.21/8.70 % (312251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.21/8.70 % (312251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.21/8.70 % (312251)CaDiCaL version: 2.1.3
% 60.21/8.70 % (312251)Termination reason: Refutation not found, incomplete strategy
% 60.21/8.70 % (312251)Time elapsed: 0.006 s
% 60.21/8.70 % (312251)Peak memory usage: 12 MB
% 60.21/8.70 % (312251)Instructions burned: 18 (million)
% 60.21/8.70 % (312251)------------------------------
% 60.21/8.70 % (312251)------------------------------
% 60.21/8.70 % (312253)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1750638360:fmbsr=1.3:i=1730:ins=25:rtra=on_2927 on theBenchmark for (2927ds/1730Mi)
% 60.21/8.70 % Exception at run slice level
% 60.21/8.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 60.21/8.70 % (312255)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2429914033:i=2358:rtra=on_2927 on theBenchmark for (2927ds/2358Mi)
% 60.21/8.70 % (312255)Refutation not found, incomplete strategy
% 60.21/8.70 % (312255)------------------------------
% 60.21/8.70 % (312255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.21/8.70 % (312255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.21/8.70 % (312255)CaDiCaL version: 2.1.3
% 60.21/8.70 % (312255)Termination reason: Refutation not found, incomplete strategy
% 60.21/8.70 % (312255)Time elapsed: 0.003 s
% 60.21/8.70 % (312255)Peak memory usage: 12 MB
% 60.21/8.70 % (312255)Instructions burned: 10 (million)
% 60.21/8.70 % (312255)------------------------------
% 60.21/8.70 % (312255)------------------------------
% 60.21/8.70 % (312257)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=769955120:i=1778:ins=1:rtra=on_2926 on theBenchmark for (2926ds/1778Mi)
% 60.21/8.70 % Exception at run slice level
% 60.21/8.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 60.21/8.70 % (312259)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2141359485:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2926 on theBenchmark for (2926ds/1384Mi)
% 68.68/9.91 % (312259)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 68.68/9.91 % (312259)Refutation not found, incomplete strategy
% 68.68/9.91 % (312259)------------------------------
% 68.68/9.91 % (312259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.68/9.91 % (312259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.68/9.91 % (312259)CaDiCaL version: 2.1.3
% 68.68/9.91 % (312259)Termination reason: Refutation not found, incomplete strategy
% 68.68/9.91 % (312259)Time elapsed: 0.002 s
% 68.68/9.91 % (312259)Peak memory usage: 12 MB
% 68.68/9.91 % (312259)Instructions burned: 3 (million)
% 68.68/9.91 % (312259)------------------------------
% 68.68/9.91 % (312259)------------------------------
% 68.68/9.91 % (312261)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=462532687:i=1758:kws=inv_precedence:fsr=off:rtra=on_2926 on theBenchmark for (2926ds/1758Mi)
% 68.68/9.91 % (312261)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 68.68/9.91 % (312261)Instruction limit reached!
% 68.68/9.91 % (312261)------------------------------
% 68.68/9.91 % (312261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.68/9.91 % (312261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.68/9.91 % (312261)CaDiCaL version: 2.1.3
% 68.68/9.91 % (312261)Termination reason: Instruction limit
% 68.68/9.91 % (312261)Termination phase: Saturation
% 68.68/9.91 % (312261)Time elapsed: 0.472 s
% 68.68/9.91 % (312261)Peak memory usage: 30 MB
% 68.68/9.91 % (312261)Instructions burned: 1762 (million)
% 68.68/9.91 % (312263)fmb+10_1_sil=64000:si=on:random_seed=2254932300:i=44122:nm=2:rtra=on:gsp=on_2921 on theBenchmark for (2921ds/44122Mi)
% 68.68/9.91 % (312263)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 68.68/9.91 % Exception at run slice level
% 68.68/9.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.68/9.91 % (312265)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1857527821:i=19030:nm=5:rtra=on_2921 on theBenchmark for (2921ds/19030Mi)
% 68.68/9.91 % Exception at run slice level
% 68.68/9.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.68/9.91 % (312267)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4132127743:fmbsr=1.7:i=1840:rtra=on_2921 on theBenchmark for (2921ds/1840Mi)
% 68.68/9.91 % Exception at run slice level
% 68.68/9.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 68.68/9.91 % (312269)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4078924555:i=10262:rtra=on_2921 on theBenchmark for (2921ds/10262Mi)
% 68.68/9.91 % (312269)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 68.68/9.91 % (312269)Refutation not found, incomplete strategy
% 68.68/9.91 % (312269)------------------------------
% 68.68/9.91 % (312269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.68/9.91 % (312269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.68/9.91 % (312269)CaDiCaL version: 2.1.3
% 68.68/9.91 % (312269)Termination reason: Refutation not found, incomplete strategy
% 68.68/9.91 % (312269)Time elapsed: 0.002 s
% 68.68/9.91 % (312269)Peak memory usage: 12 MB
% 68.68/9.91 % (312269)Instructions burned: 3 (million)
% 68.68/9.91 % (312269)------------------------------
% 68.68/9.91 % (312269)------------------------------
% 68.68/9.91 % (312271)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1195755924:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2921 on theBenchmark for (2921ds/2944Mi)
% 68.68/9.91 % (312271)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 68.68/9.91 % (312271)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 68.68/9.91 % (312209)Instruction limit reached!
% 68.68/9.91 % (312209)------------------------------
% 68.68/9.91 % (312209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.68/9.91 % (312209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.68/9.91 % (312209)CaDiCaL version: 2.1.3
% 68.68/9.91 % (312209)Termination reason: Instruction limit
% 79.53/11.54 % (312209)Termination phase: Saturation
% 79.53/11.54 % (312209)Time elapsed: 5.387 s
% 79.53/11.54 % (312209)Peak memory usage: 132 MB
% 79.53/11.54 % (312209)Instructions burned: 15854 (million)
% 79.53/11.54 % (312273)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1953948094:i=12648:rtra=on_2915 on theBenchmark for (2915ds/12648Mi)
% 79.53/11.54 % Exception at run slice level
% 79.53/11.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 79.53/11.54 % (312275)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2822979796:fmbsr=2.30978:i=4348:rtra=on_2914 on theBenchmark for (2914ds/4348Mi)
% 79.53/11.54 % Exception at run slice level
% 79.53/11.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 79.53/11.54 % (312277)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1351859217:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2914 on theBenchmark for (2914ds/1738Mi)
% 79.53/11.54 % (312277)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 79.53/11.54 % (312277)Refutation not found, incomplete strategy
% 79.53/11.54 % (312277)------------------------------
% 79.53/11.54 % (312277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.53/11.54 % (312277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.53/11.54 % (312277)CaDiCaL version: 2.1.3
% 79.53/11.54 % (312277)Termination reason: Refutation not found, incomplete strategy
% 79.53/11.54 % (312277)Time elapsed: 0.001 s
% 79.53/11.54 % (312277)Peak memory usage: 12 MB
% 79.53/11.54 % (312277)Instructions burned: 3 (million)
% 79.53/11.54 % (312277)------------------------------
% 79.53/11.54 % (312277)------------------------------
% 79.53/11.54 % (312279)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4158587038:i=10228:av=off:rtra=on_2914 on theBenchmark for (2914ds/10228Mi)
% 79.53/11.54 % (312279)Refutation not found, incomplete strategy
% 79.53/11.54 % (312279)------------------------------
% 79.53/11.54 % (312279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.53/11.54 % (312279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.53/11.54 % (312279)CaDiCaL version: 2.1.3
% 79.53/11.54 % (312279)Termination reason: Refutation not found, incomplete strategy
% 79.53/11.54 % (312279)Time elapsed: 0.002 s
% 79.53/11.54 % (312279)Peak memory usage: 12 MB
% 79.53/11.54 % (312279)Instructions burned: 4 (million)
% 79.53/11.54 % (312279)------------------------------
% 79.53/11.54 % (312279)------------------------------
% 79.53/11.54 % (312281)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2231458637:i=108564:rtra=on_2914 on theBenchmark for (2914ds/108564Mi)
% 79.53/11.54 % Exception at run slice level
% 79.53/11.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 79.53/11.54 % (312283)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3043034361:i=7024:aac=none:rtra=on_2914 on theBenchmark for (2914ds/7024Mi)
% 79.53/11.54 % (312283)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 79.53/11.54 % (312283)Refutation not found, incomplete strategy
% 79.53/11.54 % (312283)------------------------------
% 79.53/11.54 % (312283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.53/11.54 % (312283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.53/11.54 % (312283)CaDiCaL version: 2.1.3
% 79.53/11.54 % (312283)Termination reason: Refutation not found, incomplete strategy
% 79.53/11.54 % (312283)Time elapsed: 0.002 s
% 79.53/11.54 % (312283)Peak memory usage: 12 MB
% 79.53/11.54 % (312283)Instructions burned: 4 (million)
% 79.53/11.54 % (312283)------------------------------
% 79.53/11.54 % (312283)------------------------------
% 79.53/11.54 % (312285)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3930872648:i=7546:rtra=on:amm=off_2914 on theBenchmark for (2914ds/7546Mi)
% 79.53/11.54 % (312285)Refutation not found, incomplete strategy
% 79.53/11.54 % (312285)------------------------------
% 79.53/11.54 % (312285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.53/11.54 % (312285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.53/11.54 % (312285)CaDiCaL version: 2.1.3
% 79.53/11.54 % (312285)Termination reason: Refutation not found, incomplete strategy
% 79.53/11.54 % (312285)Time elapsed: 0.002 s
% 79.53/11.54 % (312285)Peak memory usage: 12 MB
% 79.53/11.54 % (312285)Instructions burned: 4 (million)
% 128.36/18.44 % (312285)------------------------------
% 128.36/18.44 % (312285)------------------------------
% 128.36/18.44 % (312287)ott+11_1_sil=16000:si=on:gs=on:random_seed=938718958:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2914 on theBenchmark for (2914ds/4502Mi)
% 128.36/18.44 % (312287)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 128.36/18.44 % (312287)Refutation not found, incomplete strategy
% 128.36/18.44 % (312287)------------------------------
% 128.36/18.44 % (312287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.36/18.44 % (312287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.36/18.44 % (312287)CaDiCaL version: 2.1.3
% 128.36/18.44 % (312287)Termination reason: Refutation not found, incomplete strategy
% 128.36/18.44 % (312287)Time elapsed: 0.001 s
% 128.36/18.44 % (312287)Peak memory usage: 12 MB
% 128.36/18.44 % (312287)Instructions burned: 3 (million)
% 128.36/18.44 % (312287)------------------------------
% 128.36/18.44 % (312287)------------------------------
% 128.36/18.44 % (312289)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=354281100:fmbsr=1.6:i=135068:rtra=on_2914 on theBenchmark for (2914ds/135068Mi)
% 128.36/18.44 % Exception at run slice level
% 128.36/18.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.36/18.44 % (312291)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3857256244:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2913 on theBenchmark for (2913ds/9182Mi)
% 128.36/18.44 % (312271)Instruction limit reached!
% 128.36/18.44 % (312271)------------------------------
% 128.36/18.44 % (312271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.36/18.44 % (312271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.36/18.44 % (312271)CaDiCaL version: 2.1.3
% 128.36/18.44 % (312271)Termination reason: Instruction limit
% 128.36/18.44 % (312271)Termination phase: Saturation
% 128.36/18.44 % (312271)Time elapsed: 0.779 s
% 128.36/18.44 % (312271)Peak memory usage: 17 MB
% 128.36/18.44 % (312271)Instructions burned: 2945 (million)
% 128.36/18.44 % (312293)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=2991388939:i=58680:rtra=on_2913 on theBenchmark for (2913ds/58680Mi)
% 128.36/18.44 % (312184)Instruction limit reached!
% 128.36/18.44 % (312184)------------------------------
% 128.36/18.44 % (312184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.36/18.44 % (312184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.36/18.44 % (312184)CaDiCaL version: 2.1.3
% 128.36/18.44 % (312184)Termination reason: Instruction limit
% 128.36/18.44 % (312184)Termination phase: Saturation
% 128.36/18.44 % (312184)Time elapsed: 8.451 s
% 128.36/18.44 % (312184)Peak memory usage: 228 MB
% 128.36/18.44 % (312184)Instructions burned: 29341 (million)
% 128.36/18.44 % (312295)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=162960288:i=10422:rtra=on_2911 on theBenchmark for (2911ds/10422Mi)
% 128.36/18.44 % (312211)Instruction limit reached!
% 128.36/18.44 % (312211)------------------------------
% 128.36/18.44 % (312211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.36/18.44 % (312211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.36/18.44 % (312211)CaDiCaL version: 2.1.3
% 128.36/18.44 % (312211)Termination reason: Instruction limit
% 128.36/18.44 % (312211)Termination phase: Saturation
% 128.36/18.44 % (312211)Time elapsed: 5.183 s
% 128.36/18.44 % (312211)Peak memory usage: 153 MB
% 128.36/18.44 % (312211)Instructions burned: 17628 (million)
% 128.36/18.44 % (312297)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=573641458:i=10994:nm=2:rtra=on_2902 on theBenchmark for (2902ds/10994Mi)
% 128.36/18.44 % Exception at run slice level
% 128.36/18.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.36/18.44 % (312299)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=2491584319:fmbsr=2:i=92664:rtra=on_2902 on theBenchmark for (2902ds/92664Mi)
% 128.36/18.44 % Exception at run slice level
% 128.36/18.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.36/18.44 % (312301)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=3815478142:i=28142:rtra=on_2902 on theBenchmark for (2902ds/28142Mi)
% 128.36/18.44 % Exception at run slice level
% 128.36/18.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 136.50/19.52 % (312303)dis+10_161_sil=128000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=662130722:i=45130:add=on:rtra=on:rawr=on_2902 on theBenchmark for (2902ds/45130Mi)
% 136.50/19.52 % (312291)Instruction limit reached!
% 136.50/19.52 % (312291)------------------------------
% 136.50/19.52 % (312291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.50/19.52 % (312291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.50/19.52 % (312291)CaDiCaL version: 2.1.3
% 136.50/19.52 % (312291)Termination reason: Instruction limit
% 136.50/19.52 % (312291)Termination phase: Saturation
% 136.50/19.52 % (312291)Time elapsed: 2.242 s
% 136.50/19.52 % (312291)Peak memory usage: 29 MB
% 136.50/19.52 % (312291)Instructions burned: 9183 (million)
% 136.50/19.52 % (312305)ott+4_1_sil=16000:si=on:sp=arity:gs=on:random_seed=3593498814:i=16346:av=off:rtra=on_2891 on theBenchmark for (2891ds/16346Mi)
% 136.50/19.52 % (312305)Refutation not found, incomplete strategy
% 136.50/19.52 % (312305)------------------------------
% 136.50/19.52 % (312305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.50/19.52 % (312305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.50/19.52 % (312305)CaDiCaL version: 2.1.3
% 136.50/19.52 % (312305)Termination reason: Refutation not found, incomplete strategy
% 136.50/19.52 % (312305)Time elapsed: 0.001 s
% 136.50/19.52 % (312305)Peak memory usage: 11 MB
% 136.50/19.52 % (312305)Instructions burned: 3 (million)
% 136.50/19.52 % (312305)------------------------------
% 136.50/19.52 % (312305)------------------------------
% 136.50/19.52 % (312307)dis+10_16:1_sil=16000:si=on:random_seed=270547548:i=18310:fsr=off:rtra=on_2891 on theBenchmark for (2891ds/18310Mi)
% 136.50/19.52 % (312307)Refutation not found, incomplete strategy
% 136.50/19.52 % (312307)------------------------------
% 136.50/19.52 % (312307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.50/19.52 % (312307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.50/19.52 % (312307)CaDiCaL version: 2.1.3
% 136.50/19.52 % (312307)Termination reason: Refutation not found, incomplete strategy
% 136.50/19.52 % (312307)Time elapsed: 0.002 s
% 136.50/19.52 % (312307)Peak memory usage: 12 MB
% 136.50/19.52 % (312307)Instructions burned: 3 (million)
% 136.50/19.52 % (312307)------------------------------
% 136.50/19.52 % (312307)------------------------------
% 136.50/19.52 % (312309)ott-3_8_sil=64000:si=on:random_seed=392478125:i=40278:bs=on:rtra=on_2891 on theBenchmark for (2891ds/40278Mi)
% 136.50/19.52 % (312309)Refutation not found, incomplete strategy
% 136.50/19.52 % (312309)------------------------------
% 136.50/19.52 % (312309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.50/19.52 % (312309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.50/19.52 % (312309)CaDiCaL version: 2.1.3
% 136.50/19.52 % (312309)Termination reason: Refutation not found, incomplete strategy
% 136.50/19.52 % (312309)Time elapsed: 0.002 s
% 136.50/19.52 % (312309)Peak memory usage: 12 MB
% 136.50/19.52 % (312309)Instructions burned: 3 (million)
% 136.50/19.52 % (312309)------------------------------
% 136.50/19.52 % (312309)------------------------------
% 136.50/19.52 % (312311)fmb+10_1_sil=64000:tgt=ground:sas=cadical:si=on:bce=on:fmbss=9:random_seed=2191071639:fmbsr=2:i=65152:rtra=on_2890 on theBenchmark for (2890ds/65152Mi)
% 136.50/19.52 % Exception at run slice level
% 136.50/19.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 136.50/19.52 % (312313)ott+10_8:1_sil=16000:si=on:sp=arity:gs=on:random_seed=2028627129:i=22808:rtra=on_2890 on theBenchmark for (2890ds/22808Mi)
% 136.50/19.52 % (312295)Instruction limit reached!
% 136.50/19.52 % (312295)------------------------------
% 136.50/19.52 % (312295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.50/19.52 % (312295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.50/19.52 % (312295)CaDiCaL version: 2.1.3
% 136.50/19.52 % (312295)Termination reason: Instruction limit
% 136.50/19.52 % (312295)Termination phase: Saturation
% 136.50/19.52 % (312295)Time elapsed: 2.562 s
% 136.50/19.52 % (312295)Peak memory usage: 92 MB
% 136.50/19.52 % (312295)Instructions burned: 10424 (million)
% 136.50/19.52 % (312315)ott-11_1_sil=16000:si=on:alpa=false:sac=on:random_seed=1914769393:i=28268:rtra=on_2886 on theBenchmark for (2886ds/28268Mi)
% 136.50/19.52 % (312315)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 140.25/20.06 % (312315)Refutation not found, incomplete strategy
% 140.25/20.06 % (312315)------------------------------
% 140.25/20.06 % (312315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.25/20.06 % (312315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.25/20.06 % (312315)CaDiCaL version: 2.1.3
% 140.25/20.06 % (312315)Termination reason: Refutation not found, incomplete strategy
% 140.25/20.06 % (312315)Time elapsed: 0.001 s
% 140.25/20.06 % (312315)Peak memory usage: 12 MB
% 140.25/20.06 % (312315)Instructions burned: 3 (million)
% 140.25/20.06 % (312315)------------------------------
% 140.25/20.06 % (312315)------------------------------
% 140.25/20.06 % (312317)dis+33_16_sil=32000:si=on:sac=on:random_seed=247451147:i=31702:nm=0:rtra=on_2885 on theBenchmark for (2885ds/31702Mi)
% 140.25/20.06 % (312217)Instruction limit reached!
% 140.25/20.06 % (312217)------------------------------
% 140.25/20.06 % (312217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.25/20.06 % (312217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.25/20.06 % (312217)CaDiCaL version: 2.1.3
% 140.25/20.06 % (312217)Termination reason: Instruction limit
% 140.25/20.06 % (312217)Termination phase: Saturation
% 140.25/20.06 % (312217)Time elapsed: 6.587 s
% 140.25/20.06 % (312217)Peak memory usage: 366 MB
% 140.25/20.06 % (312217)Instructions burned: 28121 (million)
% 140.25/20.06 % (312319)dis+4_1024_sil=32000:si=on:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3958334134:avsq=on:i=35254:add=on:rtra=on:amm=off_2882 on theBenchmark for (2882ds/35254Mi)
% 140.25/20.06 % (312123)Instruction limit reached!
% 140.25/20.06 % (312123)------------------------------
% 140.25/20.06 % (312123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.25/20.06 % (312123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.25/20.06 % (312123)CaDiCaL version: 2.1.3
% 140.25/20.06 % (312123)Termination reason: Instruction limit
% 140.25/20.06 % (312123)Termination phase: Saturation
% 140.25/20.06 % (312123)Time elapsed: 15.076 s
% 140.25/20.06 % (312123)Peak memory usage: 30 MB
% 140.25/20.06 % (312123)Instructions burned: 88030 (million)
% 140.25/20.06 % (312321)ott+10_64_anc=all:sil=128000:sas=cadical:si=on:bsr=unit_only:nwc=1:cn=on:random_seed=3335083934:s2a=on:i=106590:rtra=on_2848 on theBenchmark for (2848ds/106590Mi)
% 140.25/20.06 % (312313)Instruction limit reached!
% 140.25/20.06 % (312313)------------------------------
% 140.25/20.06 % (312313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.25/20.06 % (312313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.25/20.06 % (312313)CaDiCaL version: 2.1.3
% 140.25/20.06 % (312313)Termination reason: Instruction limit
% 140.25/20.06 % (312313)Termination phase: Saturation
% 140.25/20.06 % (312313)Time elapsed: 6.923 s
% 140.25/20.06 % (312313)Peak memory usage: 331 MB
% 140.25/20.06 % (312313)Instructions burned: 22812 (million)
% 140.25/20.06 % (312323)fmb+10_1_sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1271836182:i=53714:ins=20:rtra=on_2821 on theBenchmark for (2821ds/53714Mi)
% 140.25/20.06 % Exception at run slice level
% 140.25/20.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.25/20.06 % (312325)ott+10_1_sil=64000:plsq=on:plsqc=4:si=on:bsr=unit_only:gs=on:random_seed=971706874:i=56240:bs=on:fsr=off:rtra=on_2821 on theBenchmark for (2821ds/56240Mi)
% 140.25/20.06 % (312303)Instruction limit reached!
% 140.25/20.06 % (312303)------------------------------
% 140.25/20.06 % (312303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.25/20.06 % (312303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.25/20.06 % (312303)CaDiCaL version: 2.1.3
% 140.25/20.06 % (312303)Termination reason: Instruction limit
% 140.25/20.06 % (312303)Termination phase: Saturation
% 140.25/20.06 % (312303)Time elapsed: 8.488 s
% 140.25/20.06 % (312303)Peak memory usage: 27 MB
% 140.25/20.06 % (312303)Instructions burned: 45133 (million)
% 140.25/20.06 % (312327)fmb+10_1_sil=256000:si=on:fmbss=7:random_seed=4235863521:fmbsr=1.6:i=364590:rtra=on_2817 on theBenchmark for (2817ds/364590Mi)
% 140.25/20.06 % Exception at run slice level
% 140.25/20.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 140.25/20.06 % (312329)fmb+10_1_sil=128000:si=on:fmbss=21:newcnf=on:random_seed=1479615220:i=89250:rtra=on:gsp=on_2817 on theBenchmark for (2817ds/89250Mi)
% 140.25/20.06 % (312329)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 157.00/22.40 % (312329)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 157.00/22.40 % Exception at run slice level
% 157.00/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 157.00/22.40 % (312331)fmb+10_1_sil=256000:sas=cadical:si=on:fmbss=15:random_seed=2012443549:i=321010:rtra=on_2816 on theBenchmark for (2816ds/321010Mi)
% 157.00/22.40 % Exception at run slice level
% 157.00/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 157.00/22.40 % (312333)fmb+10_1_sil=256000:tgt=full:si=on:fmbss=10:random_seed=267529043:fmbsr=1.3:i=451458:rtra=on_2816 on theBenchmark for (2816ds/451458Mi)
% 157.00/22.40 % Exception at run slice level
% 157.00/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 157.00/22.40 % (312335)fmb+10_1_sil=256000:tgt=full:sas=cadical:si=on:fmbss=10:random_seed=947899270:fmbsr=2:i=370048:ins=7:rtra=on_2816 on theBenchmark for (2816ds/370048Mi)
% 157.00/22.40 % Exception at run slice level
% 157.00/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 157.00/22.40 % (312337)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2156455137:rtra=on_2816 on theBenchmark for (2816ds/0Mi)
% 157.00/22.40 % Exception at run slice level
% 157.00/22.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 157.00/22.40 % (312339)% WARNING: option uhcvi not known.
% 157.00/22.40 % (312339)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3334147774:i=542124:add=off:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/542124Mi)
% 157.00/22.40 % (312339)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 157.00/22.40 % (312339)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 157.00/22.40 % (312339)Refutation not found, incomplete strategy
% 157.00/22.40 % (312339)------------------------------
% 157.00/22.40 % (312339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 157.00/22.40 % (312339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.00/22.40 % (312339)CaDiCaL version: 2.1.3
% 157.00/22.40 % (312339)Termination reason: Refutation not found, incomplete strategy
% 157.00/22.40 % (312339)Time elapsed: 0.002 s
% 157.00/22.40 % (312339)Peak memory usage: 12 MB
% 157.00/22.40 % (312339)Instructions burned: 4 (million)
% 157.00/22.40 % (312339)------------------------------
% 157.00/22.40 % (312339)------------------------------
% 157.00/22.40 % (312341)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1568409204:i=352096:add=on:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/352096Mi)
% 157.00/22.40 % (312317)Instruction limit reached!
% 157.00/22.40 % (312317)------------------------------
% 157.00/22.40 % (312317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 157.00/22.40 % (312317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.00/22.40 % (312317)CaDiCaL version: 2.1.3
% 157.00/22.40 % (312317)Termination reason: Instruction limit
% 157.00/22.40 % (312317)Termination phase: Saturation
% 157.00/22.40 % (312317)Time elapsed: 7.925 s
% 157.00/22.40 % (312317)Peak memory usage: 236 MB
% 157.00/22.40 % (312317)Instructions burned: 31705 (million)
% 157.00/22.40 % (312343)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3193519939:i=412:fgj=on:rtra=on_2806 on theBenchmark for (2806ds/412Mi)
% 157.00/22.40 % (312343)Refutation not found, incomplete strategy
% 157.00/22.40 % (312343)------------------------------
% 157.00/22.40 % (312343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 157.00/22.40 % (312343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.00/22.40 % (312343)CaDiCaL version: 2.1.3
% 157.00/22.40 % (312343)Termination reason: Refutation not found, incomplete strategy
% 157.00/22.40 % (312343)Time elapsed: 0.002 s
% 157.00/22.40 % (312343)Peak memory usage: 12 MB
% 157.00/22.40 % (312343)Instructions burned: 4 (million)
% 157.00/22.40 % (312343)------------------------------
% 157.00/22.40 % (312343)------------------------------
% 157.00/22.40 % (312345)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3948949817:i=464:rtra=on_2806 on theBenchmark for (2806ds/464Mi)
% 157.00/22.40 % (312345)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 157.00/22.40 % (312345)Refutation not found, incomplete strategy
% 160.12/22.90 % (312345)------------------------------
% 160.12/22.90 % (312345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.12/22.90 % (312345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.12/22.90 % (312345)CaDiCaL version: 2.1.3
% 160.12/22.90 % (312345)Termination reason: Refutation not found, incomplete strategy
% 160.12/22.90 % (312345)Time elapsed: 0.001 s
% 160.12/22.90 % (312345)Peak memory usage: 12 MB
% 160.12/22.90 % (312345)Instructions burned: 3 (million)
% 160.12/22.90 % (312345)------------------------------
% 160.12/22.90 % (312345)------------------------------
% 160.12/22.90 % (312347)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=709367042:i=524:rtra=on_2806 on theBenchmark for (2806ds/524Mi)
% 160.12/22.90 % (312347)Instruction limit reached!
% 160.12/22.90 % (312347)------------------------------
% 160.12/22.90 % (312347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.12/22.90 % (312347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.12/22.90 % (312347)CaDiCaL version: 2.1.3
% 160.12/22.90 % (312347)Termination reason: Instruction limit
% 160.12/22.90 % (312347)Termination phase: Saturation
% 160.12/22.90 % (312347)Time elapsed: 0.124 s
% 160.12/22.90 % (312347)Peak memory usage: 19 MB
% 160.12/22.90 % (312347)Instructions burned: 524 (million)
% 160.12/22.90 % (312349)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=961629191:i=636:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2804 on theBenchmark for (2804ds/636Mi)
% 160.12/22.90 % (312349)Instruction limit reached!
% 160.12/22.90 % (312349)------------------------------
% 160.12/22.90 % (312349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.12/22.90 % (312349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.12/22.90 % (312349)CaDiCaL version: 2.1.3
% 160.12/22.90 % (312349)Termination reason: Instruction limit
% 160.12/22.90 % (312349)Termination phase: Saturation
% 160.12/22.90 % (312349)Time elapsed: 0.172 s
% 160.12/22.90 % (312349)Peak memory usage: 19 MB
% 160.12/22.90 % (312349)Instructions burned: 637 (million)
% 160.12/22.90 % (312351)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3779389900:i=2856:nm=2:rtra=on_2802 on theBenchmark for (2802ds/2856Mi)
% 160.12/22.90 % Exception at run slice level
% 160.12/22.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 160.12/22.90 % (312353)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=737747091:i=524:bd=preordered:rtra=on:fsd=on_2802 on theBenchmark for (2802ds/524Mi)
% 160.12/22.90 % (312353)Refutation not found, incomplete strategy
% 160.12/22.90 % (312353)------------------------------
% 160.12/22.90 % (312353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.12/22.90 % (312353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.12/22.90 % (312353)CaDiCaL version: 2.1.3
% 160.12/22.90 % (312353)Termination reason: Refutation not found, incomplete strategy
% 160.12/22.90 % (312353)Time elapsed: 0.002 s
% 160.12/22.90 % (312353)Peak memory usage: 12 MB
% 160.12/22.90 % (312353)Instructions burned: 3 (million)
% 160.12/22.90 % (312353)------------------------------
% 160.12/22.90 % (312353)------------------------------
% 160.12/22.90 % (312355)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3926939211:i=2736:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/2736Mi)
% 160.12/22.90 % (312355)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 160.12/22.90 % (312355)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 160.12/22.90 % (312355)Refutation not found, incomplete strategy
% 160.12/22.90 % (312355)------------------------------
% 160.12/22.90 % (312355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.12/22.90 % (312355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.12/22.90 % (312355)CaDiCaL version: 2.1.3
% 160.12/22.90 % (312355)Termination reason: Refutation not found, incomplete strategy
% 160.12/22.90 % (312355)Time elapsed: 0.002 s
% 160.12/22.90 % (312355)Peak memory usage: 13 MB
% 160.12/22.90 % (312355)Instructions burned: 3 (million)
% 160.12/22.90 % (312355)------------------------------
% 160.12/22.90 % (312355)------------------------------
% 160.12/22.90 % (312357)ott-21_1_sil=16000:si=on:fs=off:random_seed=2881766177:i=720:av=off:fsr=off:rtra=on_2802 on theBenchmark for (2802ds/720Mi)
% 160.12/22.90 % (312357)Instruction limit reached!
% 167.60/24.02 % (312357)------------------------------
% 167.60/24.02 % (312357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 167.60/24.02 % (312357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.60/24.02 % (312357)CaDiCaL version: 2.1.3
% 167.60/24.02 % (312357)Termination reason: Instruction limit
% 167.60/24.02 % (312357)Termination phase: Saturation
% 167.60/24.02 % (312357)Time elapsed: 0.164 s
% 167.60/24.02 % (312357)Peak memory usage: 16 MB
% 167.60/24.02 % (312357)Instructions burned: 721 (million)
% 167.60/24.02 % (312359)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2743548332:i=1908:bd=all:rtra=on_2800 on theBenchmark for (2800ds/1908Mi)
% 167.60/24.02 % (312359)Refutation not found, incomplete strategy
% 167.60/24.02 % (312359)------------------------------
% 167.60/24.02 % (312359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 167.60/24.02 % (312359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.60/24.02 % (312359)CaDiCaL version: 2.1.3
% 167.60/24.02 % (312359)Termination reason: Refutation not found, incomplete strategy
% 167.60/24.02 % (312359)Time elapsed: 0.006 s
% 167.60/24.02 % (312359)Peak memory usage: 12 MB
% 167.60/24.02 % (312359)Instructions burned: 18 (million)
% 167.60/24.02 % (312359)------------------------------
% 167.60/24.02 % (312359)------------------------------
% 167.60/24.02 % (312361)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1966114492:fmbsr=1.3:i=3460:ins=25:rtra=on_2800 on theBenchmark for (2800ds/3460Mi)
% 167.60/24.02 % Exception at run slice level
% 167.60/24.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 167.60/24.02 % (312363)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2788838799:i=4716:rtra=on_2800 on theBenchmark for (2800ds/4716Mi)
% 167.60/24.02 % (312363)Instruction limit reached!
% 167.60/24.02 % (312363)------------------------------
% 167.60/24.02 % (312363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 167.60/24.02 % (312363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.60/24.02 % (312363)CaDiCaL version: 2.1.3
% 167.60/24.02 % (312363)Termination reason: Instruction limit
% 167.60/24.02 % (312363)Termination phase: Saturation
% 167.60/24.02 % (312363)Time elapsed: 1.125 s
% 167.60/24.02 % (312363)Peak memory usage: 80 MB
% 167.60/24.02 % (312363)Instructions burned: 4717 (million)
% 167.60/24.02 % (312365)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4289918219:i=3556:ins=1:rtra=on_2788 on theBenchmark for (2788ds/3556Mi)
% 167.60/24.02 % Exception at run slice level
% 167.60/24.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 167.60/24.02 % (312367)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=473927446:avsq=on:s2a=on:i=2768:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/2768Mi)
% 167.60/24.02 % (312367)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 167.60/24.02 % (312367)Instruction limit reached!
% 167.60/24.02 % (312367)------------------------------
% 167.60/24.02 % (312367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 167.60/24.02 % (312367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.60/24.02 % (312367)CaDiCaL version: 2.1.3
% 167.60/24.02 % (312367)Termination reason: Instruction limit
% 167.60/24.02 % (312367)Termination phase: Saturation
% 167.60/24.02 % (312367)Time elapsed: 0.734 s
% 167.60/24.02 % (312367)Peak memory usage: 49 MB
% 167.60/24.02 % (312367)Instructions burned: 2772 (million)
% 167.60/24.02 % (312369)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3470603022:i=3516:kws=inv_precedence:fsr=off:rtra=on_2781 on theBenchmark for (2781ds/3516Mi)
% 167.60/24.02 % (312369)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 167.60/24.02 % (312319)Instruction limit reached!
% 167.60/24.02 % (312319)------------------------------
% 167.60/24.02 % (312319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 167.60/24.02 % (312319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.60/24.02 % (312319)CaDiCaL version: 2.1.3
% 167.60/24.02 % (312319)Termination reason: Instruction limit
% 167.60/24.02 % (312319)Termination phase: Saturation
% 167.60/24.02 % (312319)Time elapsed: 10.493 s
% 167.60/24.02 % (312319)Peak memory usage: 276 MB
% 113.02/24.05 % (312319)Instructions burned: 35255 (million)
% 113.02/24.05 % (312371)fmb+10_1_sil=64000:si=on:random_seed=3452072844:i=88244:nm=2:rtra=on:gsp=on_2777 on theBenchmark for (2777ds/88244Mi)
% 113.02/24.05 % (312371)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312373)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3765323229:i=38060:nm=5:rtra=on_2776 on theBenchmark for (2776ds/38060Mi)
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312375)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=361566240:fmbsr=1.7:i=3680:rtra=on_2776 on theBenchmark for (2776ds/3680Mi)
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312377)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1203283996:i=20524:rtra=on_2776 on theBenchmark for (2776ds/20524Mi)
% 113.02/24.05 % (312377)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 113.02/24.05 % (312377)Refutation not found, incomplete strategy
% 113.02/24.05 % (312377)------------------------------
% 113.02/24.05 % (312377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312377)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312377)Termination reason: Refutation not found, incomplete strategy
% 113.02/24.05 % (312377)Time elapsed: 0.002 s
% 113.02/24.05 % (312377)Peak memory usage: 12 MB
% 113.02/24.05 % (312377)Instructions burned: 3 (million)
% 113.02/24.05 % (312377)------------------------------
% 113.02/24.05 % (312377)------------------------------
% 113.02/24.05 % (312379)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3347707142:i=5888:ins=7:rtra=on:fdi=8:gsp=on_2776 on theBenchmark for (2776ds/5888Mi)
% 113.02/24.05 % (312379)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 113.02/24.05 % (312379)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 113.02/24.05 % (312369)Instruction limit reached!
% 113.02/24.05 % (312369)------------------------------
% 113.02/24.05 % (312369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312369)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312369)Termination reason: Instruction limit
% 113.02/24.05 % (312369)Termination phase: Saturation
% 113.02/24.05 % (312369)Time elapsed: 0.856 s
% 113.02/24.05 % (312369)Peak memory usage: 38 MB
% 113.02/24.05 % (312369)Instructions burned: 3516 (million)
% 113.02/24.05 % (312381)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=494890750:i=25296:rtra=on_2772 on theBenchmark for (2772ds/25296Mi)
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312383)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1267307018:fmbsr=2.30978:i=8696:rtra=on_2772 on theBenchmark for (2772ds/8696Mi)
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312385)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3454200703:avsq=on:i=3476:avsqr=1,16:kws=inv_arity_squared:rtra=on_2772 on theBenchmark for (2772ds/3476Mi)
% 113.02/24.05 % (312385)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 113.02/24.05 % (312385)Refutation not found, incomplete strategy
% 113.02/24.05 % (312385)------------------------------
% 113.02/24.05 % (312385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312385)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312385)Termination reason: Refutation not found, incomplete strategy
% 113.02/24.05 % (312385)Time elapsed: 0.003 s
% 113.02/24.05 % (312385)Peak memory usage: 12 MB
% 113.02/24.05 % (312385)Instructions burned: 3 (million)
% 113.02/24.05 % (312385)------------------------------
% 113.02/24.05 % (312385)------------------------------
% 113.02/24.05 % (312387)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3497652985:i=20456:av=off:rtra=on_2772 on theBenchmark for (2772ds/20456Mi)
% 113.02/24.05 % (312379)Instruction limit reached!
% 113.02/24.05 % (312379)------------------------------
% 113.02/24.05 % (312379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312379)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312379)Termination reason: Instruction limit
% 113.02/24.05 % (312379)Termination phase: Saturation
% 113.02/24.05 % (312379)Time elapsed: 1.434 s
% 113.02/24.05 % (312379)Peak memory usage: 18 MB
% 113.02/24.05 % (312379)Instructions burned: 5889 (million)
% 113.02/24.05 % (312389)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=539668122:i=217128:rtra=on_2762 on theBenchmark for (2762ds/217128Mi)
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312391)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3364816804:i=14048:aac=none:rtra=on_2761 on theBenchmark for (2761ds/14048Mi)
% 113.02/24.05 % (312391)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 113.02/24.05 % (312391)Refutation not found, incomplete strategy
% 113.02/24.05 % (312391)------------------------------
% 113.02/24.05 % (312391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312391)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312391)Termination reason: Refutation not found, incomplete strategy
% 113.02/24.05 % (312391)Time elapsed: 0.002 s
% 113.02/24.05 % (312391)Peak memory usage: 12 MB
% 113.02/24.05 % (312391)Instructions burned: 4 (million)
% 113.02/24.05 % (312391)------------------------------
% 113.02/24.05 % (312391)------------------------------
% 113.02/24.05 % (312393)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1199040558:i=15092:rtra=on:amm=off_2761 on theBenchmark for (2761ds/15092Mi)
% 113.02/24.05 % (312393)Refutation not found, incomplete strategy
% 113.02/24.05 % (312393)------------------------------
% 113.02/24.05 % (312393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312393)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312393)Termination reason: Refutation not found, incomplete strategy
% 113.02/24.05 % (312393)Time elapsed: 0.002 s
% 113.02/24.05 % (312393)Peak memory usage: 13 MB
% 113.02/24.05 % (312393)Instructions burned: 4 (million)
% 113.02/24.05 % (312393)------------------------------
% 113.02/24.05 % (312393)------------------------------
% 113.02/24.05 % (312395)ott+11_1_sil=16000:si=on:gs=on:random_seed=4160032930:s2a=on:i=9004:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2761 on theBenchmark for (2761ds/9004Mi)
% 113.02/24.05 % (312395)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 113.02/24.05 % (312395)Refutation not found, incomplete strategy
% 113.02/24.05 % (312395)------------------------------
% 113.02/24.05 % (312395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312395)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312395)Termination reason: Refutation not found, incomplete strategy
% 113.02/24.05 % (312395)Time elapsed: 0.002 s
% 113.02/24.05 % (312395)Peak memory usage: 12 MB
% 113.02/24.05 % (312395)Instructions burned: 3 (million)
% 113.02/24.05 % (312395)------------------------------
% 113.02/24.05 % (312395)------------------------------
% 113.02/24.05 % (312397)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3198213152:fmbsr=1.6:i=270136:rtra=on_2761 on theBenchmark for (2761ds/270136Mi)
% 113.02/24.05 % Exception at run slice level
% 113.02/24.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 113.02/24.05 % (312399)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3415439008:avsq=on:i=18364:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2761 on theBenchmark for (2761ds/18364Mi)
% 113.02/24.05 % (312399) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-312116-312399"...
% 113.02/24.05 % (312399)...printing done.
% 113.02/24.05 % (312399)Refutation found. Thanks to Tanya!
% 113.02/24.05 % SZS status Theorem for theBenchmark
% 113.02/24.05 % SZS output start Proof for theBenchmark
% See solution above
% 113.02/24.05 % (312399)------------------------------
% 113.02/24.05 % (312399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.02/24.05 % (312399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.02/24.05 % (312399)CaDiCaL version: 2.1.3
% 113.02/24.05 % (312399)Termination reason: Refutation
% 113.02/24.05 % (312399)Time elapsed: 0.018 s
% 113.02/24.05 % (312399)Peak memory usage: 13 MB
% 113.02/24.05 % (312399)Instructions burned: 59 (million)
% 113.02/24.05 % (312116)Success in time 23.924 s
% 113.02/24.05 % Vampire exiting
%------------------------------------------------------------------------------