%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ144^1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:20:58 AM UTC 2026
% Result : Theorem 19.64s 3.10s
% Output : Refutation 19.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 49
% Syntax : Number of formulae : 294 ( 257 unt; 0 typ; 0 def)
% Number of atoms : 580 ( 394 equ; 0 cnn)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 1171 ( 61 ~; 57 |; 0 &;1000 @)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 94 ( 89 usr; 79 con; 0-4 aty)
% ( 28 !!; 3 ??; 0 @@+; 0 @@-)
% Number of variables : 169 ( 40 ^; 127 !; 2 ?; 169 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
position: $tType ).
thf(type_def_6,type,
direction: $tType ).
thf(type_def_7,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(type_def_8,type,
movelist: $tType ).
thf(func_def_0,type,
left: direction ).
thf(func_def_1,type,
right: direction ).
thf(func_def_2,type,
top: direction ).
thf(func_def_3,type,
bottom: direction ).
thf(func_def_4,type,
next: position > direction > position ).
thf(func_def_6,type,
wall: position > $o ).
thf(func_def_7,type,
nomove: movelist ).
thf(func_def_8,type,
movedir: movelist > direction > movelist ).
thf(func_def_9,type,
playerpos: movelist > position ).
thf(func_def_10,type,
c00: position ).
thf(func_def_11,type,
c10: position ).
thf(func_def_12,type,
c20: position ).
thf(func_def_13,type,
c30: position ).
thf(func_def_14,type,
c40: position ).
thf(func_def_15,type,
c50: position ).
thf(func_def_16,type,
c60: position ).
thf(func_def_17,type,
c70: position ).
thf(func_def_18,type,
c80: position ).
thf(func_def_19,type,
c90: position ).
thf(func_def_20,type,
c01: position ).
thf(func_def_21,type,
c11: position ).
thf(func_def_22,type,
c21: position ).
thf(func_def_23,type,
c31: position ).
thf(func_def_24,type,
c41: position ).
thf(func_def_25,type,
c51: position ).
thf(func_def_26,type,
c61: position ).
thf(func_def_27,type,
c71: position ).
thf(func_def_28,type,
c81: position ).
thf(func_def_29,type,
c91: position ).
thf(func_def_30,type,
c02: position ).
thf(func_def_31,type,
c12: position ).
thf(func_def_32,type,
c22: position ).
thf(func_def_33,type,
c32: position ).
thf(func_def_34,type,
c42: position ).
thf(func_def_35,type,
c52: position ).
thf(func_def_36,type,
c62: position ).
thf(func_def_37,type,
c72: position ).
thf(func_def_38,type,
c82: position ).
thf(func_def_39,type,
c92: position ).
thf(func_def_40,type,
c03: position ).
thf(func_def_41,type,
c13: position ).
thf(func_def_42,type,
c23: position ).
thf(func_def_43,type,
c33: position ).
thf(func_def_44,type,
c43: position ).
thf(func_def_45,type,
c53: position ).
thf(func_def_46,type,
c63: position ).
thf(func_def_47,type,
c73: position ).
thf(func_def_48,type,
c83: position ).
thf(func_def_49,type,
c93: position ).
thf(func_def_50,type,
c04: position ).
thf(func_def_51,type,
c14: position ).
thf(func_def_52,type,
c24: position ).
thf(func_def_53,type,
c34: position ).
thf(func_def_54,type,
c44: position ).
thf(func_def_55,type,
c54: position ).
thf(func_def_56,type,
c64: position ).
thf(func_def_57,type,
c74: position ).
thf(func_def_58,type,
c84: position ).
thf(func_def_59,type,
c94: position ).
thf(func_def_60,type,
c05: position ).
thf(func_def_61,type,
c15: position ).
thf(func_def_62,type,
c25: position ).
thf(func_def_63,type,
c35: position ).
thf(func_def_64,type,
c45: position ).
thf(func_def_65,type,
c55: position ).
thf(func_def_66,type,
c65: position ).
thf(func_def_67,type,
c75: position ).
thf(func_def_68,type,
c85: position ).
thf(func_def_69,type,
c95: position ).
thf(func_def_70,type,
c06: position ).
thf(func_def_71,type,
c16: position ).
thf(func_def_72,type,
c26: position ).
thf(func_def_73,type,
c36: position ).
thf(func_def_74,type,
c46: position ).
thf(func_def_75,type,
c56: position ).
thf(func_def_76,type,
c66: position ).
thf(func_def_77,type,
c76: position ).
thf(func_def_78,type,
c86: position ).
thf(func_def_79,type,
c96: position ).
thf(func_def_82,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_83,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_84,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_85,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_86,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_87,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_88,type,
vNOT: $o > $o ).
thf(func_def_89,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_90,type,
vIMP: $o > $o > $o ).
thf(f1,axiom,
! [X0: direction,X2: position,X1: direction] :
( ( next @ ( next @ X2 @ X0 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',next_comm) ).
thf(f2,axiom,
! [X0: position] :
( ( next @ ( next @ X0 @ left ) @ right )
= X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_right) ).
thf(f3,axiom,
! [X0: position] :
( ( next @ ( next @ X0 @ top ) @ bottom )
= X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',top_bottom) ).
thf(f4,axiom,
! [X2: direction,X1: movelist,X0: position] :
( ( ( playerpos @ X1 )
= X0 )
=> ( ~ ( wall @ ( next @ X0 @ X2 ) )
=> ( ( playerpos @ ( movedir @ X1 @ X2 ) )
= ( next @ X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',player_move_legal) ).
thf(f9,axiom,
( c40
= ( next @ c30 @ right ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c40_defin) ).
thf(f10,axiom,
( c50
= ( next @ c40 @ right ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c50_defin) ).
thf(f11,axiom,
( c60
= ( next @ c50 @ right ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c60_defin) ).
thf(f12,axiom,
( c70
= ( next @ c60 @ right ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c70_defin) ).
thf(f13,axiom,
( c80
= ( next @ c70 @ right ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c80_defin) ).
thf(f33,axiom,
( c31
= ( next @ c30 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c31_defin) ).
thf(f34,axiom,
( c32
= ( next @ c31 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c32_defin) ).
thf(f35,axiom,
( c33
= ( next @ c32 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c33_defin) ).
thf(f39,axiom,
( c41
= ( next @ c40 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c41_defin) ).
thf(f40,axiom,
( c42
= ( next @ c41 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c42_defin) ).
thf(f41,axiom,
( c43
= ( next @ c42 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c43_defin) ).
thf(f42,axiom,
( c44
= ( next @ c43 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c44_defin) ).
thf(f43,axiom,
( c45
= ( next @ c44 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c45_defin) ).
thf(f45,axiom,
( c51
= ( next @ c50 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c51_defin) ).
thf(f46,axiom,
( c52
= ( next @ c51 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c52_defin) ).
thf(f47,axiom,
( c53
= ( next @ c52 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c53_defin) ).
thf(f48,axiom,
( c54
= ( next @ c53 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c54_defin) ).
thf(f49,axiom,
( c55
= ( next @ c54 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c55_defin) ).
thf(f51,axiom,
( c61
= ( next @ c60 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c61_defin) ).
thf(f52,axiom,
( c62
= ( next @ c61 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c62_defin) ).
thf(f53,axiom,
( c63
= ( next @ c62 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c63_defin) ).
thf(f54,axiom,
( c64
= ( next @ c63 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c64_defin) ).
thf(f55,axiom,
( c65
= ( next @ c64 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c65_defin) ).
thf(f57,axiom,
( c71
= ( next @ c70 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c71_defin) ).
thf(f58,axiom,
( c72
= ( next @ c71 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c72_defin) ).
thf(f59,axiom,
( c73
= ( next @ c72 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c73_defin) ).
thf(f60,axiom,
( c74
= ( next @ c73 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c74_defin) ).
thf(f61,axiom,
( c75
= ( next @ c74 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c75_defin) ).
thf(f63,axiom,
( c81
= ( next @ c80 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c81_defin) ).
thf(f64,axiom,
( c82
= ( next @ c81 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c82_defin) ).
thf(f65,axiom,
( c83
= ( next @ c82 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c83_defin) ).
thf(f66,axiom,
( c84
= ( next @ c83 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c84_defin) ).
thf(f67,axiom,
( c85
= ( next @ c84 @ top ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c85_defin) ).
thf(f98,axiom,
( $false
= ( wall @ c32 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c32_axiom) ).
thf(f108,axiom,
( $false
= ( wall @ c33 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c33_axiom) ).
thf(f109,axiom,
( $false
= ( wall @ c43 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c43_axiom) ).
thf(f119,axiom,
( $false
= ( wall @ c44 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c44_axiom) ).
thf(f123,axiom,
( $false
= ( wall @ c84 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c84_axiom) ).
thf(f129,axiom,
( ( wall @ c45 )
= $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c45_axiom) ).
thf(f130,axiom,
( ( wall @ c55 )
= $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c55_axiom) ).
thf(f131,axiom,
( $false
= ( wall @ c65 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c65_axiom) ).
thf(f132,axiom,
( $false
= ( wall @ c75 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c75_axiom) ).
thf(f133,axiom,
( ( wall @ c85 )
= $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c85_axiom) ).
thf(f145,axiom,
( ( playerpos @ nomove )
= c31 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',start_axiom) ).
thf(f146,conjecture,
? [X0: movelist] :
( ( playerpos @ X0 )
= c84 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exercise) ).
thf(f147,negated_conjecture,
~ ? [X0: movelist] :
( ( playerpos @ X0 )
= c84 ),
inference(negated_conjecture,[status(cth)],[f146]) ).
thf(f148,plain,
( c43
= ( next @ c42 @ top ) ),
inference(fool_elimination,[],[f41]) ).
thf(f154,plain,
! [X0: direction,X1: position,X2: direction] :
( ( next @ ( next @ X1 @ X0 ) @ X2 )
= ( next @ ( next @ X1 @ X2 ) @ X0 ) ),
inference(rectify,[],[f1]) ).
thf(f155,plain,
( ( !! @ direction
@ ^ [Y0: direction] :
( !! @ position
@ ^ [Y1: position] :
( !! @ direction
@ ^ [Y2: direction] :
( ( next @ ( next @ Y1 @ Y2 ) @ Y0 )
= ( next @ ( next @ Y1 @ Y0 ) @ Y2 ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f154]) ).
thf(f157,plain,
( c65
= ( next @ c64 @ top ) ),
inference(fool_elimination,[],[f55]) ).
thf(f158,plain,
( c74
= ( next @ c73 @ top ) ),
inference(fool_elimination,[],[f60]) ).
thf(f161,plain,
( c75
= ( next @ c74 @ top ) ),
inference(fool_elimination,[],[f61]) ).
thf(f163,plain,
( c51
= ( next @ c50 @ top ) ),
inference(fool_elimination,[],[f45]) ).
thf(f166,plain,
( ( !! @ position
@ ^ [Y0: position] :
( ( next @ ( next @ Y0 @ left ) @ right )
= Y0 ) )
= $true ),
inference(fool_elimination,[],[f2]) ).
thf(f168,plain,
( c54
= ( next @ c53 @ top ) ),
inference(fool_elimination,[],[f48]) ).
thf(f169,plain,
( c83
= ( next @ c82 @ top ) ),
inference(fool_elimination,[],[f65]) ).
thf(f170,plain,
( $true
= ( !! @ position
@ ^ [Y0: position] :
( ( next @ ( next @ Y0 @ top ) @ bottom )
= Y0 ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f173,plain,
( c64
= ( next @ c63 @ top ) ),
inference(fool_elimination,[],[f54]) ).
thf(f174,plain,
( c63
= ( next @ c62 @ top ) ),
inference(fool_elimination,[],[f53]) ).
thf(f176,plain,
( c53
= ( next @ c52 @ top ) ),
inference(fool_elimination,[],[f47]) ).
thf(f185,plain,
( ( wall @ c44 )
= $false ),
inference(fool_elimination,[],[f119]) ).
thf(f186,plain,
( c80
= ( next @ c70 @ right ) ),
inference(fool_elimination,[],[f13]) ).
thf(f187,plain,
( c42
= ( next @ c41 @ top ) ),
inference(fool_elimination,[],[f40]) ).
thf(f191,plain,
( ( wall @ c84 )
= $false ),
inference(fool_elimination,[],[f123]) ).
thf(f194,plain,
( ( ~ ( ?? @ movelist
@ ^ [Y0: movelist] :
( c84
= ( playerpos @ Y0 ) ) ) )
= $true ),
inference(fool_elimination,[],[f147]) ).
thf(f197,plain,
( c31
= ( next @ c30 @ top ) ),
inference(fool_elimination,[],[f33]) ).
thf(f201,plain,
( c62
= ( next @ c61 @ top ) ),
inference(fool_elimination,[],[f52]) ).
thf(f202,plain,
( ( wall @ c32 )
= $false ),
inference(fool_elimination,[],[f98]) ).
thf(f203,plain,
( c52
= ( next @ c51 @ top ) ),
inference(fool_elimination,[],[f46]) ).
thf(f206,plain,
( c61
= ( next @ c60 @ top ) ),
inference(fool_elimination,[],[f51]) ).
thf(f210,plain,
( c41
= ( next @ c40 @ top ) ),
inference(fool_elimination,[],[f39]) ).
thf(f216,plain,
( c32
= ( next @ c31 @ top ) ),
inference(fool_elimination,[],[f34]) ).
thf(f219,plain,
( c44
= ( next @ c43 @ top ) ),
inference(fool_elimination,[],[f42]) ).
thf(f221,plain,
( c40
= ( next @ c30 @ right ) ),
inference(fool_elimination,[],[f9]) ).
thf(f229,plain,
( c81
= ( next @ c80 @ top ) ),
inference(fool_elimination,[],[f63]) ).
thf(f231,plain,
( ( wall @ c55 )
= $false ),
inference(fool_elimination,[],[f130]) ).
thf(f235,plain,
( ( wall @ c75 )
= $false ),
inference(fool_elimination,[],[f132]) ).
thf(f236,plain,
( c72
= ( next @ c71 @ top ) ),
inference(fool_elimination,[],[f58]) ).
thf(f237,plain,
( c45
= ( next @ c44 @ top ) ),
inference(fool_elimination,[],[f43]) ).
thf(f242,plain,
! [X0: direction,X1: movelist,X2: position] :
( ( ( playerpos @ X1 )
= X2 )
=> ( ~ ( wall @ ( next @ X2 @ X0 ) )
=> ( ( next @ X2 @ X0 )
= ( playerpos @ ( movedir @ X1 @ X0 ) ) ) ) ),
inference(rectify,[],[f4]) ).
thf(f243,plain,
( ( !! @ position
@ ^ [Y0: position] :
( !! @ movelist
@ ^ [Y1: movelist] :
( !! @ direction
@ ^ [Y2: direction] :
( ( ( playerpos @ Y1 )
= Y0 )
=> ( ~ ( wall @ ( next @ Y0 @ Y2 ) )
=> ( ( next @ Y0 @ Y2 )
= ( playerpos @ ( movedir @ Y1 @ Y2 ) ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f242]) ).
thf(f246,plain,
( c55
= ( next @ c54 @ top ) ),
inference(fool_elimination,[],[f49]) ).
thf(f247,plain,
( ( wall @ c43 )
= $false ),
inference(fool_elimination,[],[f109]) ).
thf(f249,plain,
( c73
= ( next @ c72 @ top ) ),
inference(fool_elimination,[],[f59]) ).
thf(f251,plain,
( ( wall @ c33 )
= $false ),
inference(fool_elimination,[],[f108]) ).
thf(f252,plain,
( c31
= ( playerpos @ nomove ) ),
inference(fool_elimination,[],[f145]) ).
thf(f259,plain,
( ( wall @ c85 )
= $false ),
inference(fool_elimination,[],[f133]) ).
thf(f261,plain,
( c84
= ( next @ c83 @ top ) ),
inference(fool_elimination,[],[f66]) ).
thf(f267,plain,
( ( wall @ c45 )
= $false ),
inference(fool_elimination,[],[f129]) ).
thf(f268,plain,
( c33
= ( next @ c32 @ top ) ),
inference(fool_elimination,[],[f35]) ).
thf(f271,plain,
( c82
= ( next @ c81 @ top ) ),
inference(fool_elimination,[],[f64]) ).
thf(f275,plain,
( c70
= ( next @ c60 @ right ) ),
inference(fool_elimination,[],[f12]) ).
thf(f279,plain,
( c50
= ( next @ c40 @ right ) ),
inference(fool_elimination,[],[f10]) ).
thf(f280,plain,
( c60
= ( next @ c50 @ right ) ),
inference(fool_elimination,[],[f11]) ).
thf(f281,plain,
( c71
= ( next @ c70 @ top ) ),
inference(fool_elimination,[],[f57]) ).
thf(f287,plain,
( c85
= ( next @ c84 @ top ) ),
inference(fool_elimination,[],[f67]) ).
thf(f295,plain,
( ( wall @ c65 )
= $false ),
inference(fool_elimination,[],[f131]) ).
thf(f300,plain,
( ( ~ ( ?? @ movelist
@ ^ [Y0: movelist] :
( c84
= ( playerpos @ Y0 ) ) ) )
= $true ),
inference(cnf_transformation,[],[f194]) ).
thf(f301,plain,
( c73
= ( next @ c72 @ top ) ),
inference(cnf_transformation,[],[f249]) ).
thf(f305,plain,
( ( wall @ c85 )
= $false ),
inference(cnf_transformation,[],[f259]) ).
thf(f306,plain,
( c60
= ( next @ c50 @ right ) ),
inference(cnf_transformation,[],[f280]) ).
thf(f310,plain,
( c50
= ( next @ c40 @ right ) ),
inference(cnf_transformation,[],[f279]) ).
thf(f311,plain,
( c83
= ( next @ c82 @ top ) ),
inference(cnf_transformation,[],[f169]) ).
thf(f312,plain,
( c31
= ( playerpos @ nomove ) ),
inference(cnf_transformation,[],[f252]) ).
thf(f315,plain,
( ( wall @ c33 )
= $false ),
inference(cnf_transformation,[],[f251]) ).
thf(f319,plain,
( c45
= ( next @ c44 @ top ) ),
inference(cnf_transformation,[],[f237]) ).
thf(f320,plain,
( ( wall @ c65 )
= $false ),
inference(cnf_transformation,[],[f295]) ).
thf(f324,plain,
( c82
= ( next @ c81 @ top ) ),
inference(cnf_transformation,[],[f271]) ).
thf(f326,plain,
( c62
= ( next @ c61 @ top ) ),
inference(cnf_transformation,[],[f201]) ).
thf(f330,plain,
( c52
= ( next @ c51 @ top ) ),
inference(cnf_transformation,[],[f203]) ).
thf(f332,plain,
( c54
= ( next @ c53 @ top ) ),
inference(cnf_transformation,[],[f168]) ).
thf(f333,plain,
( $true
= ( !! @ position
@ ^ [Y0: position] :
( ( next @ ( next @ Y0 @ top ) @ bottom )
= Y0 ) ) ),
inference(cnf_transformation,[],[f170]) ).
thf(f334,plain,
( c42
= ( next @ c41 @ top ) ),
inference(cnf_transformation,[],[f187]) ).
thf(f340,plain,
( ( wall @ c55 )
= $false ),
inference(cnf_transformation,[],[f231]) ).
thf(f344,plain,
( c41
= ( next @ c40 @ top ) ),
inference(cnf_transformation,[],[f210]) ).
thf(f349,plain,
( c70
= ( next @ c60 @ right ) ),
inference(cnf_transformation,[],[f275]) ).
thf(f354,plain,
( c43
= ( next @ c42 @ top ) ),
inference(cnf_transformation,[],[f148]) ).
thf(f359,plain,
( c31
= ( next @ c30 @ top ) ),
inference(cnf_transformation,[],[f197]) ).
thf(f361,plain,
( c61
= ( next @ c60 @ top ) ),
inference(cnf_transformation,[],[f206]) ).
thf(f362,plain,
( c51
= ( next @ c50 @ top ) ),
inference(cnf_transformation,[],[f163]) ).
thf(f363,plain,
( ( !! @ direction
@ ^ [Y0: direction] :
( !! @ position
@ ^ [Y1: position] :
( !! @ direction
@ ^ [Y2: direction] :
( ( next @ ( next @ Y1 @ Y2 ) @ Y0 )
= ( next @ ( next @ Y1 @ Y0 ) @ Y2 ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f155]) ).
thf(f365,plain,
( ( wall @ c45 )
= $false ),
inference(cnf_transformation,[],[f267]) ).
thf(f369,plain,
( c71
= ( next @ c70 @ top ) ),
inference(cnf_transformation,[],[f281]) ).
thf(f371,plain,
( c80
= ( next @ c70 @ right ) ),
inference(cnf_transformation,[],[f186]) ).
thf(f372,plain,
( c33
= ( next @ c32 @ top ) ),
inference(cnf_transformation,[],[f268]) ).
thf(f378,plain,
( c84
= ( next @ c83 @ top ) ),
inference(cnf_transformation,[],[f261]) ).
thf(f380,plain,
( ( wall @ c32 )
= $false ),
inference(cnf_transformation,[],[f202]) ).
thf(f381,plain,
( c74
= ( next @ c73 @ top ) ),
inference(cnf_transformation,[],[f158]) ).
thf(f382,plain,
( c64
= ( next @ c63 @ top ) ),
inference(cnf_transformation,[],[f173]) ).
thf(f388,plain,
( c72
= ( next @ c71 @ top ) ),
inference(cnf_transformation,[],[f236]) ).
thf(f389,plain,
( ( wall @ c84 )
= $false ),
inference(cnf_transformation,[],[f191]) ).
thf(f393,plain,
( ( wall @ c44 )
= $false ),
inference(cnf_transformation,[],[f185]) ).
thf(f406,plain,
( c63
= ( next @ c62 @ top ) ),
inference(cnf_transformation,[],[f174]) ).
thf(f408,plain,
( ( !! @ position
@ ^ [Y0: position] :
( !! @ movelist
@ ^ [Y1: movelist] :
( !! @ direction
@ ^ [Y2: direction] :
( ( ( playerpos @ Y1 )
= Y0 )
=> ( ~ ( wall @ ( next @ Y0 @ Y2 ) )
=> ( ( next @ Y0 @ Y2 )
= ( playerpos @ ( movedir @ Y1 @ Y2 ) ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f243]) ).
thf(f409,plain,
( c85
= ( next @ c84 @ top ) ),
inference(cnf_transformation,[],[f287]) ).
thf(f414,plain,
( c55
= ( next @ c54 @ top ) ),
inference(cnf_transformation,[],[f246]) ).
thf(f416,plain,
( ( !! @ position
@ ^ [Y0: position] :
( ( next @ ( next @ Y0 @ left ) @ right )
= Y0 ) )
= $true ),
inference(cnf_transformation,[],[f166]) ).
thf(f417,plain,
( c65
= ( next @ c64 @ top ) ),
inference(cnf_transformation,[],[f157]) ).
thf(f420,plain,
( ( wall @ c75 )
= $false ),
inference(cnf_transformation,[],[f235]) ).
thf(f421,plain,
( c81
= ( next @ c80 @ top ) ),
inference(cnf_transformation,[],[f229]) ).
thf(f431,plain,
( c53
= ( next @ c52 @ top ) ),
inference(cnf_transformation,[],[f176]) ).
thf(f432,plain,
( c40
= ( next @ c30 @ right ) ),
inference(cnf_transformation,[],[f221]) ).
thf(f436,plain,
( c44
= ( next @ c43 @ top ) ),
inference(cnf_transformation,[],[f219]) ).
thf(f439,plain,
( c75
= ( next @ c74 @ top ) ),
inference(cnf_transformation,[],[f161]) ).
thf(f440,plain,
( ( wall @ c43 )
= $false ),
inference(cnf_transformation,[],[f247]) ).
thf(f441,plain,
( c32
= ( next @ c31 @ top ) ),
inference(cnf_transformation,[],[f216]) ).
thf(f445,plain,
( ( ?? @ movelist
@ ^ [Y0: movelist] :
( c84
= ( playerpos @ Y0 ) ) )
= $false ),
inference(not_proxy_clausification,[],[f300]) ).
thf(f509,plain,
! [X1: position] :
( $true
= ( ^ [Y0: position] :
( ( next @ ( next @ Y0 @ top ) @ bottom )
= Y0 )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f333]) ).
thf(f510,plain,
! [X1: position] :
( $true
= ( ( next @ ( next @ X1 @ top ) @ bottom )
= X1 ) ),
inference(beta-eta_normalization,[],[f509]) ).
thf(f511,plain,
! [X1: position] :
( ( next @ ( next @ X1 @ top ) @ bottom )
= X1 ),
inference(equality_proxy_clausification,[],[f510]) ).
thf(f551,plain,
( c84
= ( next @ c85 @ bottom ) ),
inference(constrained_superposition,[],[f511,f409]) ).
thf(f560,plain,
! [X1: position] :
( $true
= ( ^ [Y0: position] :
( ( next @ ( next @ Y0 @ left ) @ right )
= Y0 )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f416]) ).
thf(f561,plain,
! [X1: position] :
( ( ( next @ ( next @ X1 @ left ) @ right )
= X1 )
= $true ),
inference(beta-eta_normalization,[],[f560]) ).
thf(f562,plain,
! [X1: position] :
( ( next @ ( next @ X1 @ left ) @ right )
= X1 ),
inference(equality_proxy_clausification,[],[f561]) ).
thf(f575,plain,
! [X1: movelist] :
( ( ^ [Y0: movelist] :
( c84
= ( playerpos @ Y0 ) )
@ X1 )
= $false ),
inference(pi_proxy_clausification,[],[f445]) ).
thf(f578,plain,
! [X1: movelist] :
( ( c84
= ( playerpos @ X1 ) )
= $false ),
inference(beta-eta_normalization,[],[f575]) ).
thf(f579,plain,
! [X1: movelist] :
( ( playerpos @ X1 )
!= c84 ),
inference(equality_proxy_clausification,[],[f578]) ).
thf(f581,plain,
! [X1: direction] :
( $true
= ( ^ [Y0: direction] :
( !! @ position
@ ^ [Y1: position] :
( !! @ direction
@ ^ [Y2: direction] :
( ( next @ ( next @ Y1 @ Y2 ) @ Y0 )
= ( next @ ( next @ Y1 @ Y0 ) @ Y2 ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f363]) ).
thf(f582,plain,
! [X1: direction] :
( $true
= ( !! @ position
@ ^ [Y0: position] :
( !! @ direction
@ ^ [Y1: direction] :
( ( next @ ( next @ Y0 @ Y1 ) @ X1 )
= ( next @ ( next @ Y0 @ X1 ) @ Y1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f581]) ).
thf(f583,plain,
! [X2: position,X1: direction] :
( $true
= ( ^ [Y0: position] :
( !! @ direction
@ ^ [Y1: direction] :
( ( next @ ( next @ Y0 @ Y1 ) @ X1 )
= ( next @ ( next @ Y0 @ X1 ) @ Y1 ) ) )
@ X2 ) ),
inference(pi_proxy_clausification,[],[f582]) ).
thf(f584,plain,
! [X2: position,X1: direction] :
( ( !! @ direction
@ ^ [Y0: direction] :
( ( next @ ( next @ X2 @ Y0 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ Y0 ) ) )
= $true ),
inference(beta-eta_normalization,[],[f583]) ).
thf(f585,plain,
! [X2: position,X3: direction,X1: direction] :
( $true
= ( ^ [Y0: direction] :
( ( next @ ( next @ X2 @ Y0 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ Y0 ) )
@ X3 ) ),
inference(pi_proxy_clausification,[],[f584]) ).
thf(f586,plain,
! [X2: position,X3: direction,X1: direction] :
( $true
= ( ( next @ ( next @ X2 @ X3 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ X3 ) ) ),
inference(beta-eta_normalization,[],[f585]) ).
thf(f587,plain,
! [X2: position,X3: direction,X1: direction] :
( ( next @ ( next @ X2 @ X3 ) @ X1 )
= ( next @ ( next @ X2 @ X1 ) @ X3 ) ),
inference(equality_proxy_clausification,[],[f586]) ).
thf(f595,plain,
! [X0: direction] :
( ( next @ c50 @ X0 )
= ( next @ ( next @ c40 @ X0 ) @ right ) ),
inference(constrained_superposition,[],[f587,f310]) ).
thf(f597,plain,
! [X0: direction] :
( ( next @ ( next @ c60 @ X0 ) @ right )
= ( next @ c70 @ X0 ) ),
inference(constrained_superposition,[],[f587,f349]) ).
thf(f603,plain,
! [X0: direction] :
( ( next @ ( next @ c30 @ X0 ) @ top )
= ( next @ c31 @ X0 ) ),
inference(constrained_superposition,[],[f587,f359]) ).
thf(f613,plain,
! [X0: direction] :
( ( next @ c32 @ X0 )
= ( next @ ( next @ c31 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f441]) ).
thf(f617,plain,
! [X0: direction] :
( ( next @ ( next @ c71 @ X0 ) @ top )
= ( next @ c72 @ X0 ) ),
inference(constrained_superposition,[],[f587,f388]) ).
thf(f623,plain,
! [X0: direction] :
( ( next @ c33 @ X0 )
= ( next @ ( next @ c32 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f372]) ).
thf(f625,plain,
! [X0: direction] :
( ( next @ ( next @ c52 @ X0 ) @ top )
= ( next @ c53 @ X0 ) ),
inference(constrained_superposition,[],[f587,f431]) ).
thf(f634,plain,
! [X0: direction] :
( ( next @ ( next @ c43 @ X0 ) @ top )
= ( next @ c44 @ X0 ) ),
inference(constrained_superposition,[],[f587,f436]) ).
thf(f637,plain,
! [X0: direction] :
( ( next @ c74 @ X0 )
= ( next @ ( next @ c73 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f381]) ).
thf(f646,plain,
! [X0: direction] :
( ( next @ ( next @ c64 @ X0 ) @ top )
= ( next @ c65 @ X0 ) ),
inference(constrained_superposition,[],[f587,f417]) ).
thf(f730,plain,
! [X0: direction] :
( ( next @ ( next @ c50 @ X0 ) @ right )
= ( next @ c60 @ X0 ) ),
inference(constrained_superposition,[],[f587,f306]) ).
thf(f732,plain,
! [X0: direction] :
( ( next @ ( next @ c70 @ X0 ) @ right )
= ( next @ c80 @ X0 ) ),
inference(constrained_superposition,[],[f587,f371]) ).
thf(f739,plain,
! [X0: direction] :
( ( next @ ( next @ c50 @ X0 ) @ top )
= ( next @ c51 @ X0 ) ),
inference(constrained_superposition,[],[f587,f362]) ).
thf(f740,plain,
! [X0: direction] :
( ( next @ ( next @ c60 @ X0 ) @ top )
= ( next @ c61 @ X0 ) ),
inference(constrained_superposition,[],[f587,f361]) ).
thf(f741,plain,
! [X0: direction] :
( ( next @ c71 @ X0 )
= ( next @ ( next @ c70 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f369]) ).
thf(f749,plain,
! [X0: direction] :
( ( next @ c52 @ X0 )
= ( next @ ( next @ c51 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f330]) ).
thf(f750,plain,
! [X0: direction] :
( ( next @ ( next @ c61 @ X0 ) @ top )
= ( next @ c62 @ X0 ) ),
inference(constrained_superposition,[],[f587,f326]) ).
thf(f760,plain,
! [X0: direction] :
( ( next @ ( next @ c62 @ X0 ) @ top )
= ( next @ c63 @ X0 ) ),
inference(constrained_superposition,[],[f587,f406]) ).
thf(f761,plain,
! [X0: direction] :
( ( next @ c73 @ X0 )
= ( next @ ( next @ c72 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f301]) ).
thf(f770,plain,
! [X0: direction] :
( ( next @ ( next @ c63 @ X0 ) @ top )
= ( next @ c64 @ X0 ) ),
inference(constrained_superposition,[],[f587,f382]) ).
thf(f778,plain,
! [X0: direction] :
( ( next @ c45 @ X0 )
= ( next @ ( next @ c44 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f319]) ).
thf(f781,plain,
! [X0: direction] :
( ( next @ c75 @ X0 )
= ( next @ ( next @ c74 @ X0 ) @ top ) ),
inference(constrained_superposition,[],[f587,f439]) ).
thf(f983,plain,
( c40
= ( next @ c50 @ left ) ),
inference(constrained_superposition,[],[f562,f595]) ).
thf(f998,plain,
( c60
= ( next @ c70 @ left ) ),
inference(constrained_superposition,[],[f562,f597]) ).
thf(f1052,plain,
( ( next @ c40 @ top )
= ( next @ c31 @ right ) ),
inference(constrained_superposition,[],[f603,f432]) ).
thf(f1062,plain,
( c41
= ( next @ c31 @ right ) ),
inference(forward_demodulation,[],[f1052,f344]) ).
thf(f1156,plain,
( ( next @ c41 @ top )
= ( next @ c32 @ right ) ),
inference(constrained_superposition,[],[f613,f1062]) ).
thf(f1167,plain,
( c42
= ( next @ c32 @ right ) ),
inference(forward_demodulation,[],[f1156,f334]) ).
thf(f1274,plain,
( ( next @ c42 @ top )
= ( next @ c33 @ right ) ),
inference(constrained_superposition,[],[f623,f1167]) ).
thf(f1287,plain,
( c43
= ( next @ c33 @ right ) ),
inference(forward_demodulation,[],[f1274,f354]) ).
thf(f1564,plain,
( c50
= ( next @ c60 @ left ) ),
inference(constrained_superposition,[],[f562,f730]) ).
thf(f1579,plain,
( ( next @ c80 @ top )
= ( next @ c71 @ right ) ),
inference(constrained_superposition,[],[f732,f369]) ).
thf(f1588,plain,
( c81
= ( next @ c71 @ right ) ),
inference(forward_demodulation,[],[f1579,f421]) ).
thf(f1597,plain,
( ( next @ c81 @ top )
= ( next @ c72 @ right ) ),
inference(constrained_superposition,[],[f617,f1588]) ).
thf(f1600,plain,
( c82
= ( next @ c72 @ right ) ),
inference(forward_demodulation,[],[f1597,f324]) ).
thf(f1648,plain,
( ( next @ c40 @ top )
= ( next @ c51 @ left ) ),
inference(constrained_superposition,[],[f739,f983]) ).
thf(f1660,plain,
( c41
= ( next @ c51 @ left ) ),
inference(forward_demodulation,[],[f1648,f344]) ).
thf(f1664,plain,
( ( next @ c50 @ top )
= ( next @ c61 @ left ) ),
inference(constrained_superposition,[],[f740,f1564]) ).
thf(f1676,plain,
( c51
= ( next @ c61 @ left ) ),
inference(forward_demodulation,[],[f1664,f362]) ).
thf(f1680,plain,
( ( next @ c60 @ top )
= ( next @ c71 @ left ) ),
inference(constrained_superposition,[],[f741,f998]) ).
thf(f1691,plain,
( c61
= ( next @ c71 @ left ) ),
inference(forward_demodulation,[],[f1680,f361]) ).
thf(f1694,plain,
( ( next @ c61 @ top )
= ( next @ c72 @ left ) ),
inference(constrained_superposition,[],[f617,f1691]) ).
thf(f1697,plain,
( c62
= ( next @ c72 @ left ) ),
inference(forward_demodulation,[],[f1694,f326]) ).
thf(f1703,plain,
( ( next @ c41 @ top )
= ( next @ c52 @ left ) ),
inference(constrained_superposition,[],[f749,f1660]) ).
thf(f1717,plain,
( c42
= ( next @ c52 @ left ) ),
inference(forward_demodulation,[],[f1703,f334]) ).
thf(f1723,plain,
( ( next @ c42 @ top )
= ( next @ c53 @ left ) ),
inference(constrained_superposition,[],[f625,f1717]) ).
thf(f1726,plain,
( c43
= ( next @ c53 @ left ) ),
inference(forward_demodulation,[],[f1723,f354]) ).
thf(f1731,plain,
( c53
= ( next @ c43 @ right ) ),
inference(constrained_superposition,[],[f562,f1726]) ).
thf(f1738,plain,
( ( next @ c53 @ top )
= ( next @ c44 @ right ) ),
inference(constrained_superposition,[],[f634,f1731]) ).
thf(f1741,plain,
( c54
= ( next @ c44 @ right ) ),
inference(forward_demodulation,[],[f1738,f332]) ).
thf(f1747,plain,
( ( next @ c51 @ top )
= ( next @ c62 @ left ) ),
inference(constrained_superposition,[],[f750,f1676]) ).
thf(f1761,plain,
( c52
= ( next @ c62 @ left ) ),
inference(forward_demodulation,[],[f1747,f330]) ).
thf(f1808,plain,
( ( next @ c52 @ top )
= ( next @ c63 @ left ) ),
inference(constrained_superposition,[],[f760,f1761]) ).
thf(f1820,plain,
( c53
= ( next @ c63 @ left ) ),
inference(forward_demodulation,[],[f1808,f431]) ).
thf(f1828,plain,
( ( next @ c62 @ top )
= ( next @ c73 @ left ) ),
inference(constrained_superposition,[],[f761,f1697]) ).
thf(f1829,plain,
( ( next @ c82 @ top )
= ( next @ c73 @ right ) ),
inference(constrained_superposition,[],[f761,f1600]) ).
thf(f1841,plain,
( c83
= ( next @ c73 @ right ) ),
inference(forward_demodulation,[],[f1829,f311]) ).
thf(f1842,plain,
( c63
= ( next @ c73 @ left ) ),
inference(forward_demodulation,[],[f1828,f406]) ).
thf(f1843,plain,
( ( next @ c83 @ top )
= ( next @ c74 @ right ) ),
inference(constrained_superposition,[],[f637,f1841]) ).
thf(f1846,plain,
( c84
= ( next @ c74 @ right ) ),
inference(forward_demodulation,[],[f1843,f378]) ).
thf(f1848,plain,
( ( next @ c63 @ top )
= ( next @ c74 @ left ) ),
inference(constrained_superposition,[],[f637,f1842]) ).
thf(f1851,plain,
( c64
= ( next @ c74 @ left ) ),
inference(forward_demodulation,[],[f1848,f382]) ).
thf(f1854,plain,
( c74
= ( next @ c64 @ right ) ),
inference(constrained_superposition,[],[f562,f1851]) ).
thf(f1857,plain,
( ( next @ c74 @ top )
= ( next @ c65 @ right ) ),
inference(constrained_superposition,[],[f646,f1854]) ).
thf(f1860,plain,
( c75
= ( next @ c65 @ right ) ),
inference(forward_demodulation,[],[f1857,f439]) ).
thf(f1930,plain,
( ( next @ c53 @ top )
= ( next @ c64 @ left ) ),
inference(constrained_superposition,[],[f770,f1820]) ).
thf(f1943,plain,
( c54
= ( next @ c64 @ left ) ),
inference(forward_demodulation,[],[f1930,f332]) ).
thf(f1946,plain,
( ( next @ c54 @ top )
= ( next @ c65 @ left ) ),
inference(constrained_superposition,[],[f646,f1943]) ).
thf(f1949,plain,
( c55
= ( next @ c65 @ left ) ),
inference(forward_demodulation,[],[f1946,f414]) ).
thf(f1950,plain,
( c65
= ( next @ c55 @ right ) ),
inference(constrained_superposition,[],[f562,f1949]) ).
thf(f2025,plain,
( ( next @ c54 @ top )
= ( next @ c45 @ right ) ),
inference(constrained_superposition,[],[f778,f1741]) ).
thf(f2037,plain,
( c55
= ( next @ c45 @ right ) ),
inference(forward_demodulation,[],[f2025,f414]) ).
thf(f2070,plain,
( ( next @ c84 @ top )
= ( next @ c75 @ right ) ),
inference(constrained_superposition,[],[f781,f1846]) ).
thf(f2083,plain,
( c85
= ( next @ c75 @ right ) ),
inference(forward_demodulation,[],[f2070,f409]) ).
thf(f3364,plain,
! [X1: position] :
( ( ^ [Y0: position] :
( !! @ movelist
@ ^ [Y1: movelist] :
( !! @ direction
@ ^ [Y2: direction] :
( ( ( playerpos @ Y1 )
= Y0 )
=> ( ~ ( wall @ ( next @ Y0 @ Y2 ) )
=> ( ( next @ Y0 @ Y2 )
= ( playerpos @ ( movedir @ Y1 @ Y2 ) ) ) ) ) ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f408]) ).
thf(f3365,plain,
! [X1: position] :
( $true
= ( !! @ movelist
@ ^ [Y0: movelist] :
( !! @ direction
@ ^ [Y1: direction] :
( ( ( playerpos @ Y0 )
= X1 )
=> ( ~ ( wall @ ( next @ X1 @ Y1 ) )
=> ( ( next @ X1 @ Y1 )
= ( playerpos @ ( movedir @ Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f3364]) ).
thf(f3366,plain,
! [X2: movelist,X1: position] :
( $true
= ( ^ [Y0: movelist] :
( !! @ direction
@ ^ [Y1: direction] :
( ( ( playerpos @ Y0 )
= X1 )
=> ( ~ ( wall @ ( next @ X1 @ Y1 ) )
=> ( ( next @ X1 @ Y1 )
= ( playerpos @ ( movedir @ Y0 @ Y1 ) ) ) ) ) )
@ X2 ) ),
inference(pi_proxy_clausification,[],[f3365]) ).
thf(f3367,plain,
! [X2: movelist,X1: position] :
( ( !! @ direction
@ ^ [Y0: direction] :
( ( ( playerpos @ X2 )
= X1 )
=> ( ~ ( wall @ ( next @ X1 @ Y0 ) )
=> ( ( next @ X1 @ Y0 )
= ( playerpos @ ( movedir @ X2 @ Y0 ) ) ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f3366]) ).
thf(f3956,plain,
! [X2: movelist,X3: direction,X1: position] :
( $true
= ( ^ [Y0: direction] :
( ( ( playerpos @ X2 )
= X1 )
=> ( ~ ( wall @ ( next @ X1 @ Y0 ) )
=> ( ( next @ X1 @ Y0 )
= ( playerpos @ ( movedir @ X2 @ Y0 ) ) ) ) )
@ X3 ) ),
inference(pi_proxy_clausification,[],[f3367]) ).
thf(f3957,plain,
! [X2: movelist,X3: direction,X1: position] :
( $true
= ( ( ( playerpos @ X2 )
= X1 )
=> ( ~ ( wall @ ( next @ X1 @ X3 ) )
=> ( ( next @ X1 @ X3 )
= ( playerpos @ ( movedir @ X2 @ X3 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f3956]) ).
thf(f3958,plain,
! [X2: movelist,X3: direction,X1: position] :
( ( ( ( playerpos @ X2 )
= X1 )
= $false )
| ( ( ~ ( wall @ ( next @ X1 @ X3 ) )
=> ( ( next @ X1 @ X3 )
= ( playerpos @ ( movedir @ X2 @ X3 ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f3957]) ).
thf(f3959,plain,
! [X2: movelist,X3: direction,X1: position] :
( ( ( playerpos @ X2 )
!= X1 )
| ( ( ~ ( wall @ ( next @ X1 @ X3 ) )
=> ( ( next @ X1 @ X3 )
= ( playerpos @ ( movedir @ X2 @ X3 ) ) ) )
= $true ) ),
inference(equality_proxy_clausification,[],[f3958]) ).
thf(f3960,plain,
! [X2: movelist,X3: direction,X1: position] :
( ( ( ~ ( wall @ ( next @ X1 @ X3 ) ) )
= $false )
| ( $true
= ( ( next @ X1 @ X3 )
= ( playerpos @ ( movedir @ X2 @ X3 ) ) ) )
| ( ( playerpos @ X2 )
!= X1 ) ),
inference(imp_proxy_clausification,[],[f3959]) ).
thf(f3961,plain,
! [X2: movelist,X3: direction,X1: position] :
( ( ( playerpos @ X2 )
!= X1 )
| ( $true
= ( ( next @ X1 @ X3 )
= ( playerpos @ ( movedir @ X2 @ X3 ) ) ) )
| ( $true
= ( wall @ ( next @ X1 @ X3 ) ) ) ),
inference(not_proxy_clausification,[],[f3960]) ).
thf(f3962,plain,
! [X2: movelist,X3: direction,X1: position] :
( ( ( playerpos @ ( movedir @ X2 @ X3 ) )
= ( next @ X1 @ X3 ) )
| ( $true
= ( wall @ ( next @ X1 @ X3 ) ) )
| ( ( playerpos @ X2 )
!= X1 ) ),
inference(equality_proxy_clausification,[],[f3961]) ).
thf(f4148,plain,
! [X0: movelist] :
( ( c33
!= ( playerpos @ X0 ) )
| ( c43
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( ( wall @ c43 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f1287]) ).
thf(f4167,plain,
! [X0: movelist] :
( ( c45
!= ( playerpos @ X0 ) )
| ( c55
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( ( wall @ c55 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f2037]) ).
thf(f4168,plain,
! [X0: movelist] :
( ( c55
!= ( playerpos @ X0 ) )
| ( c65
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( ( wall @ c65 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f1950]) ).
thf(f4169,plain,
! [X0: movelist] :
( ( c65
!= ( playerpos @ X0 ) )
| ( c75
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( ( wall @ c75 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f1860]) ).
thf(f4170,plain,
! [X0: movelist] :
( ( c75
!= ( playerpos @ X0 ) )
| ( c85
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( ( wall @ c85 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f2083]) ).
thf(f4250,plain,
! [X0: movelist] :
( ( ( wall @ c32 )
= $true )
| ( c31
!= ( playerpos @ X0 ) )
| ( c32
= ( playerpos @ ( movedir @ X0 @ top ) ) ) ),
inference(constrained_superposition,[],[f3962,f441]) ).
thf(f4260,plain,
! [X0: movelist] :
( ( ( wall @ c33 )
= $true )
| ( c33
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c32
!= ( playerpos @ X0 ) ) ),
inference(constrained_superposition,[],[f3962,f372]) ).
thf(f4271,plain,
! [X0: movelist] :
( ( c43
!= ( playerpos @ X0 ) )
| ( c44
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( ( wall @ c44 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f436]) ).
thf(f4281,plain,
! [X0: movelist] :
( ( ( wall @ c45 )
= $true )
| ( c45
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c44
!= ( playerpos @ X0 ) ) ),
inference(constrained_superposition,[],[f3962,f319]) ).
thf(f4346,plain,
! [X0: movelist] :
( ( c85
!= ( playerpos @ X0 ) )
| ( c84
= ( playerpos @ ( movedir @ X0 @ bottom ) ) )
| ( ( wall @ c84 )
= $true ) ),
inference(constrained_superposition,[],[f3962,f551]) ).
thf(f4545,plain,
! [X0: movelist] :
( ( c45
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c44
!= ( playerpos @ X0 ) )
| ( $true = $false ) ),
inference(forward_demodulation,[],[f4281,f365]) ).
thf(f4546,plain,
! [X0: movelist] :
( ( c45
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c44
!= ( playerpos @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f4545]) ).
thf(f4549,plain,
! [X0: movelist] :
( ( $true = $false )
| ( c44
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c43
!= ( playerpos @ X0 ) ) ),
inference(forward_demodulation,[],[f4271,f393]) ).
thf(f4550,plain,
! [X0: movelist] :
( ( c44
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c43
!= ( playerpos @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f4549]) ).
thf(f4560,plain,
! [X0: movelist] :
( ( c43
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( $true = $false )
| ( c33
!= ( playerpos @ X0 ) ) ),
inference(forward_demodulation,[],[f4148,f440]) ).
thf(f4561,plain,
! [X0: movelist] :
( ( c43
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( c33
!= ( playerpos @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f4560]) ).
thf(f4586,plain,
! [X0: movelist] :
( ( $true = $false )
| ( c55
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( c45
!= ( playerpos @ X0 ) ) ),
inference(forward_demodulation,[],[f4167,f340]) ).
thf(f4587,plain,
! [X0: movelist] :
( ( c55
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( c45
!= ( playerpos @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f4586]) ).
thf(f4588,plain,
! [X0: movelist] :
( ( $true = $false )
| ( c32
!= ( playerpos @ X0 ) )
| ( c33
= ( playerpos @ ( movedir @ X0 @ top ) ) ) ),
inference(forward_demodulation,[],[f4260,f315]) ).
thf(f4589,plain,
! [X0: movelist] :
( ( c33
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( c32
!= ( playerpos @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f4588]) ).
thf(f4599,plain,
! [X0: movelist] :
( ( c85
!= ( playerpos @ X0 ) )
| ( ( wall @ c84 )
= $true ) ),
inference(forward_subsumption_resolution,[],[f4346,f579]) ).
thf(f4624,plain,
! [X0: movelist] :
( ( $true = $false )
| ( c65
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( c55
!= ( playerpos @ X0 ) ) ),
inference(forward_demodulation,[],[f4168,f320]) ).
thf(f4625,plain,
! [X0: movelist] :
( ( c55
!= ( playerpos @ X0 ) )
| ( c65
= ( playerpos @ ( movedir @ X0 @ right ) ) ) ),
inference(trivial_inequality_removal,[],[f4624]) ).
thf(f4648,plain,
! [X0: movelist] :
( ( $true = $false )
| ( c65
!= ( playerpos @ X0 ) )
| ( c75
= ( playerpos @ ( movedir @ X0 @ right ) ) ) ),
inference(forward_demodulation,[],[f4169,f420]) ).
thf(f4649,plain,
! [X0: movelist] :
( ( c65
!= ( playerpos @ X0 ) )
| ( c75
= ( playerpos @ ( movedir @ X0 @ right ) ) ) ),
inference(trivial_inequality_removal,[],[f4648]) ).
thf(f4688,plain,
! [X0: movelist] :
( ( c32
= ( playerpos @ ( movedir @ X0 @ top ) ) )
| ( $true = $false )
| ( c31
!= ( playerpos @ X0 ) ) ),
inference(forward_demodulation,[],[f4250,f380]) ).
thf(f4689,plain,
! [X0: movelist] :
( ( c31
!= ( playerpos @ X0 ) )
| ( c32
= ( playerpos @ ( movedir @ X0 @ top ) ) ) ),
inference(trivial_inequality_removal,[],[f4688]) ).
thf(f4745,plain,
! [X0: movelist] :
( ( c75
!= ( playerpos @ X0 ) )
| ( $true = $false )
| ( c85
= ( playerpos @ ( movedir @ X0 @ right ) ) ) ),
inference(forward_demodulation,[],[f4170,f305]) ).
thf(f4746,plain,
! [X0: movelist] :
( ( c85
= ( playerpos @ ( movedir @ X0 @ right ) ) )
| ( c75
!= ( playerpos @ X0 ) ) ),
inference(trivial_inequality_removal,[],[f4745]) ).
thf(f4769,plain,
! [X0: movelist] :
( ( $true = $false )
| ( c85
!= ( playerpos @ X0 ) ) ),
inference(forward_demodulation,[],[f4599,f389]) ).
thf(f4770,plain,
! [X0: movelist] :
( c85
!= ( playerpos @ X0 ) ),
inference(trivial_inequality_removal,[],[f4769]) ).
thf(f4778,plain,
! [X0: movelist] :
( c75
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4746,f4770]) ).
thf(f4785,plain,
! [X0: movelist] :
( c65
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4649,f4778]) ).
thf(f4793,plain,
! [X0: movelist] :
( c55
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4625,f4785]) ).
thf(f4805,plain,
! [X0: movelist] :
( c45
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4587,f4793]) ).
thf(f4813,plain,
! [X0: movelist] :
( c44
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4546,f4805]) ).
thf(f4827,plain,
! [X0: movelist] :
( c43
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4550,f4813]) ).
thf(f4830,plain,
! [X0: movelist] :
( c33
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4561,f4827]) ).
thf(f4842,plain,
! [X0: movelist] :
( c32
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4589,f4830]) ).
thf(f4855,plain,
! [X0: movelist] :
( c31
!= ( playerpos @ X0 ) ),
inference(backward_subsumption_resolution,[],[f4689,f4842]) ).
thf(f4866,plain,
$false,
inference(backward_subsumption_resolution,[],[f312,f4855]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ144^1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 13:28:59 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.77/0.37 % (2494119)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.77/0.37 % (2494124)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1043186802:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.77/0.37 % (2494130)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.77/0.37 % (2494130)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.77/0.37 % (2494126)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1786900716:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.77/0.37 % (2494125)lrs+10_16_si=on:nwc=1.5:random_seed=3934343682:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.77/0.37 % (2494128)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1729619797:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.77/0.37 % (2494127)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=693869261:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.77/0.37 % (2494129)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3409475967:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.77/0.37 % (2494130)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2045391711:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.77/0.37 % (2494126)Instruction limit reached!
% 0.77/0.37 % (2494126)------------------------------
% 0.77/0.37 % (2494126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (2494126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (2494126)CaDiCaL version: 2.1.3
% 0.77/0.37 % (2494126)Termination reason: Instruction limit
% 0.77/0.37 % (2494126)Termination phase: Property scanning
% 0.77/0.37 % (2494126)Time elapsed: 0.002 s
% 0.77/0.37 % (2494126)Peak memory usage: 10 MB
% 0.77/0.37 % (2494126)Instructions burned: 4 (million)
% 0.77/0.37 % (2494125)Instruction limit reached!
% 0.77/0.37 % (2494125)------------------------------
% 0.77/0.37 % (2494125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (2494125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (2494125)CaDiCaL version: 2.1.3
% 0.77/0.37 % (2494125)Termination reason: Instruction limit
% 0.77/0.37 % (2494125)Termination phase: Saturation
% 0.77/0.37 % (2494125)Time elapsed: 0.009 s
% 0.77/0.37 % (2494125)Peak memory usage: 12 MB
% 0.77/0.37 % (2494125)Instructions burned: 20 (million)
% 0.77/0.37 % (2494128)Instruction limit reached!
% 0.77/0.37 % (2494128)------------------------------
% 0.77/0.37 % (2494128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (2494128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (2494128)CaDiCaL version: 2.1.3
% 0.77/0.37 % (2494128)Termination reason: Instruction limit
% 0.77/0.37 % (2494128)Termination phase: Saturation
% 0.77/0.37 % (2494128)Time elapsed: 0.013 s
% 0.77/0.37 % (2494128)Peak memory usage: 12 MB
% 0.77/0.37 % (2494128)Instructions burned: 26 (million)
% 0.77/0.37 % (2494124)Instruction limit reached!
% 0.77/0.37 % (2494124)------------------------------
% 0.77/0.37 % (2494124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (2494124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (2494124)CaDiCaL version: 2.1.3
% 0.77/0.37 % (2494124)Termination reason: Instruction limit
% 0.77/0.37 % (2494124)Termination phase: Saturation
% 0.77/0.37 % (2494124)Time elapsed: 0.022 s
% 0.77/0.37 % (2494124)Peak memory usage: 12 MB
% 0.77/0.37 % (2494124)Instructions burned: 88 (million)
% 0.77/0.37 % (2494138)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=194962275:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.37 % (2494138)Instruction limit reached!
% 0.77/0.37 % (2494138)------------------------------
% 0.77/0.37 % (2494138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (2494138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (2494138)CaDiCaL version: 2.1.3
% 0.77/0.40 % (2494138)Termination reason: Instruction limit
% 0.77/0.40 % (2494138)Termination phase: Property scanning
% 0.77/0.40 % (2494138)Time elapsed: 0.002 s
% 0.77/0.40 % (2494138)Peak memory usage: 10 MB
% 0.77/0.40 % (2494138)Instructions burned: 4 (million)
% 0.77/0.40 % (2494141)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1220344848:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.77/0.40 % (2494140)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.40 % (2494139)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2577189900:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.77/0.40 % (2494141)Instruction limit reached!
% 0.77/0.40 % (2494141)------------------------------
% 0.77/0.40 % (2494141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (2494141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (2494141)CaDiCaL version: 2.1.3
% 0.77/0.40 % (2494141)Termination reason: Instruction limit
% 0.77/0.40 % (2494141)Termination phase: Saturation
% 0.77/0.40 % (2494141)Time elapsed: 0.004 s
% 0.77/0.40 % (2494141)Peak memory usage: 12 MB
% 0.77/0.40 % (2494141)Instructions burned: 16 (million)
% 0.77/0.40 % (2494140)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2279352710:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.77/0.40 % (2494139)Instruction limit reached!
% 0.77/0.40 % (2494139)------------------------------
% 0.77/0.40 % (2494139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (2494139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (2494139)CaDiCaL version: 2.1.3
% 0.77/0.40 % (2494139)Termination reason: Instruction limit
% 0.77/0.40 % (2494139)Termination phase: Property scanning
% 0.77/0.40 % (2494139)Time elapsed: 0.003 s
% 0.77/0.40 % (2494139)Peak memory usage: 10 MB
% 0.77/0.40 % (2494139)Instructions burned: 6 (million)
% 0.77/0.40 % (2494129)Instruction limit reached!
% 0.77/0.40 % (2494129)------------------------------
% 0.77/0.40 % (2494129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (2494129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (2494129)CaDiCaL version: 2.1.3
% 0.77/0.40 % (2494129)Termination reason: Instruction limit
% 0.77/0.40 % (2494129)Termination phase: Saturation
% 0.77/0.40 % (2494129)Time elapsed: 0.037 s
% 0.77/0.40 % (2494129)Peak memory usage: 13 MB
% 0.77/0.40 % (2494129)Instructions burned: 79 (million)
% 0.77/0.40 % (2494140)Instruction limit reached!
% 0.77/0.40 % (2494140)------------------------------
% 0.77/0.40 % (2494140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (2494140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (2494140)CaDiCaL version: 2.1.3
% 0.77/0.40 % (2494140)Termination reason: Instruction limit
% 0.77/0.40 % (2494140)Termination phase: Saturation
% 0.77/0.40 % (2494140)Time elapsed: 0.006 s
% 0.77/0.40 % (2494140)Peak memory usage: 12 MB
% 0.77/0.40 % (2494140)Instructions burned: 11 (million)
% 0.77/0.40 % (2494143)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.77/0.40 % (2494143)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.40 % (2494146)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3002340576:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.77/0.40 % (2494143)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2007003096:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.77/0.40 % (2494148)lrs+10_1_si=on:cs=on:random_seed=2667227523:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.77/0.40 % (2494149)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.77/0.43 % (2494148)Instruction limit reached!
% 0.77/0.43 % (2494148)------------------------------
% 0.77/0.43 % (2494148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (2494148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (2494148)CaDiCaL version: 2.1.3
% 0.77/0.43 % (2494148)Termination reason: Instruction limit
% 0.77/0.43 % (2494148)Termination phase: Saturation
% 0.77/0.43 % (2494148)Time elapsed: 0.004 s
% 0.77/0.43 % (2494148)Peak memory usage: 12 MB
% 0.77/0.43 % (2494148)Instructions burned: 9 (million)
% 0.77/0.43 % (2494149)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1650353381:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.43 % (2494150)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3663192071:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.77/0.43 % (2494143)Instruction limit reached!
% 0.77/0.43 % (2494143)------------------------------
% 0.77/0.43 % (2494143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (2494143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (2494143)CaDiCaL version: 2.1.3
% 0.77/0.43 % (2494143)Termination reason: Instruction limit
% 0.77/0.43 % (2494143)Termination phase: Saturation
% 0.77/0.43 % (2494143)Time elapsed: 0.014 s
% 0.77/0.43 % (2494143)Peak memory usage: 12 MB
% 0.77/0.43 % (2494143)Instructions burned: 29 (million)
% 0.77/0.43 % (2494149)Instruction limit reached!
% 0.77/0.43 % (2494149)------------------------------
% 0.77/0.43 % (2494149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (2494149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (2494149)CaDiCaL version: 2.1.3
% 0.77/0.43 % (2494149)Termination reason: Instruction limit
% 0.77/0.43 % (2494149)Termination phase: Property scanning
% 0.77/0.43 % (2494149)Time elapsed: 0.001 s
% 0.77/0.43 % (2494149)Peak memory usage: 10 MB
% 0.77/0.43 % (2494149)Instructions burned: 2 (million)
% 0.77/0.43 % (2494150)Refutation not found, incomplete strategy
% 0.77/0.43 % (2494150)------------------------------
% 0.77/0.43 % (2494150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (2494150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (2494150)CaDiCaL version: 2.1.3
% 0.77/0.43 % (2494150)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.43 % (2494150)Time elapsed: 0.002 s
% 0.77/0.43 % (2494150)Peak memory usage: 12 MB
% 0.77/0.43 % (2494150)Instructions burned: 4 (million)
% 0.77/0.43 % (2494150)------------------------------
% 0.77/0.43 % (2494150)------------------------------
% 0.77/0.43 % (2494146)Instruction limit reached!
% 0.77/0.43 % (2494146)------------------------------
% 0.77/0.43 % (2494146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (2494146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (2494146)CaDiCaL version: 2.1.3
% 0.77/0.43 % (2494146)Termination reason: Instruction limit
% 0.77/0.43 % (2494146)Termination phase: Saturation
% 0.77/0.43 % (2494146)Time elapsed: 0.022 s
% 0.77/0.43 % (2494146)Peak memory usage: 13 MB
% 0.77/0.43 % (2494146)Instructions burned: 89 (million)
% 0.77/0.43 % (2494154)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=666337905:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.77/0.43 % (2494157)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2843982709:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.77/0.43 % (2494130)Instruction limit reached!
% 0.77/0.43 % (2494130)------------------------------
% 0.77/0.43 % (2494130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.43 % (2494130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.43 % (2494130)CaDiCaL version: 2.1.3
% 0.77/0.43 % (2494130)Termination reason: Instruction limit
% 0.77/0.43 % (2494130)Termination phase: Saturation
% 0.77/0.43 % (2494130)Time elapsed: 0.077 s
% 0.77/0.43 % (2494130)Peak memory usage: 13 MB
% 0.77/0.43 % (2494130)Instructions burned: 157 (million)
% 1.40/0.48 % (2494154)Refutation not found, incomplete strategy
% 1.40/0.48 % (2494154)------------------------------
% 1.40/0.48 % (2494154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.48 % (2494158)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2010051847:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 1.40/0.48 % (2494154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.48 % (2494154)CaDiCaL version: 2.1.3
% 1.40/0.48 % (2494154)Termination reason: Refutation not found, incomplete strategy
% 1.40/0.48 % (2494154)Time elapsed: 0.003 s
% 1.40/0.48 % (2494154)Peak memory usage: 12 MB
% 1.40/0.48 % (2494154)Instructions burned: 5 (million)
% 1.40/0.48 % (2494154)------------------------------
% 1.40/0.48 % (2494154)------------------------------
% 1.40/0.48 % (2494159)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=872588539:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 1.40/0.48 % (2494160)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=341563288:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.40/0.48 % (2494158)Instruction limit reached!
% 1.40/0.48 % (2494158)------------------------------
% 1.40/0.48 % (2494158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.48 % (2494158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.48 % (2494158)CaDiCaL version: 2.1.3
% 1.40/0.48 % (2494158)Termination reason: Instruction limit
% 1.40/0.48 % (2494158)Termination phase: Saturation
% 1.40/0.48 % (2494158)Time elapsed: 0.007 s
% 1.40/0.48 % (2494158)Peak memory usage: 12 MB
% 1.40/0.48 % (2494158)Instructions burned: 14 (million)
% 1.40/0.48 % (2494157)Instruction limit reached!
% 1.40/0.48 % (2494157)------------------------------
% 1.40/0.48 % (2494157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.48 % (2494157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.48 % (2494157)CaDiCaL version: 2.1.3
% 1.40/0.48 % (2494157)Termination reason: Instruction limit
% 1.40/0.48 % (2494157)Termination phase: Saturation
% 1.40/0.48 % (2494157)Time elapsed: 0.013 s
% 1.40/0.48 % (2494157)Peak memory usage: 12 MB
% 1.40/0.48 % (2494157)Instructions burned: 25 (million)
% 1.40/0.48 % (2494160)Instruction limit reached!
% 1.40/0.48 % (2494160)------------------------------
% 1.40/0.48 % (2494160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.48 % (2494160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.48 % (2494160)CaDiCaL version: 2.1.3
% 1.40/0.48 % (2494160)Termination reason: Instruction limit
% 1.40/0.48 % (2494160)Termination phase: Saturation
% 1.40/0.48 % (2494160)Time elapsed: 0.007 s
% 1.40/0.48 % (2494160)Peak memory usage: 12 MB
% 1.40/0.48 % (2494160)Instructions burned: 15 (million)
% 1.40/0.48 % (2494163)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1193738574:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.40/0.48 % (2494165)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1864452387:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.40/0.48 % (2494163)Instruction limit reached!
% 1.40/0.48 % (2494163)------------------------------
% 1.40/0.48 % (2494163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.48 % (2494163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.48 % (2494163)CaDiCaL version: 2.1.3
% 1.40/0.48 % (2494163)Termination reason: Instruction limit
% 1.40/0.48 % (2494163)Termination phase: Preprocessing 1
% 1.40/0.48 % (2494163)Time elapsed: 0.002 s
% 1.40/0.48 % (2494163)Peak memory usage: 10 MB
% 1.40/0.48 % (2494163)Instructions burned: 4 (million)
% 1.40/0.48 % (2494168)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=848581284:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.40/0.48 % (2494170)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.40/0.48 % (2494170)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.40/0.51 % (2494169)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2170925190:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.40/0.51 % (2494170)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3457393554:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.40/0.51 % (2494165)Instruction limit reached!
% 1.40/0.51 % (2494165)------------------------------
% 1.40/0.51 % (2494165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.51 % (2494165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.51 % (2494165)CaDiCaL version: 2.1.3
% 1.40/0.51 % (2494165)Termination reason: Instruction limit
% 1.40/0.51 % (2494165)Termination phase: Saturation
% 1.40/0.51 % (2494165)Time elapsed: 0.012 s
% 1.40/0.51 % (2494165)Peak memory usage: 12 MB
% 1.40/0.51 % (2494165)Instructions burned: 26 (million)
% 1.40/0.51 % (2494173)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.40/0.51 % (2494168)Instruction limit reached!
% 1.40/0.51 % (2494168)------------------------------
% 1.40/0.51 % (2494168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.51 % (2494168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.51 % (2494168)CaDiCaL version: 2.1.3
% 1.40/0.51 % (2494168)Termination reason: Instruction limit
% 1.40/0.51 % (2494168)Termination phase: Saturation
% 1.40/0.51 % (2494168)Time elapsed: 0.010 s
% 1.40/0.51 % (2494168)Peak memory usage: 12 MB
% 1.40/0.51 % (2494168)Instructions burned: 24 (million)
% 1.40/0.51 % (2494170)Instruction limit reached!
% 1.40/0.51 % (2494170)------------------------------
% 1.40/0.51 % (2494170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.51 % (2494170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.51 % (2494170)CaDiCaL version: 2.1.3
% 1.40/0.51 % (2494170)Termination reason: Instruction limit
% 1.40/0.51 % (2494170)Termination phase: Saturation
% 1.40/0.51 % (2494170)Time elapsed: 0.007 s
% 1.40/0.51 % (2494170)Peak memory usage: 12 MB
% 1.40/0.51 % (2494170)Instructions burned: 15 (million)
% 1.40/0.51 % (2494173)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=4288150987:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.40/0.51 % (2494173)Instruction limit reached!
% 1.40/0.51 % (2494173)------------------------------
% 1.40/0.51 % (2494173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.51 % (2494173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.51 % (2494173)CaDiCaL version: 2.1.3
% 1.40/0.51 % (2494173)Termination reason: Instruction limit
% 1.40/0.51 % (2494173)Termination phase: Saturation
% 1.40/0.51 % (2494173)Time elapsed: 0.004 s
% 1.40/0.51 % (2494173)Peak memory usage: 11 MB
% 1.40/0.51 % (2494173)Instructions burned: 9 (million)
% 1.40/0.51 % (2494177)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=3466507836:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.40/0.51 % (2494178)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3501015952:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.40/0.51 % (2494179)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=59680486:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.40/0.51 % (2494178)Instruction limit reached!
% 1.40/0.51 % (2494178)------------------------------
% 1.40/0.51 % (2494178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.40/0.51 % (2494178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.40/0.51 % (2494178)CaDiCaL version: 2.1.3
% 1.40/0.51 % (2494178)Termination reason: Instruction limit
% 1.40/0.51 % (2494178)Termination phase: Saturation
% 1.40/0.51 % (2494178)Time elapsed: 0.005 s
% 1.40/0.51 % (2494178)Peak memory usage: 12 MB
% 1.40/0.51 % (2494178)Instructions burned: 10 (million)
% 1.40/0.51 % (2494169)Instruction limit reached!
% 1.40/0.51 % (2494169)------------------------------
% 1.40/0.51 % (2494169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.12/0.57 % (2494169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.12/0.57 % (2494169)CaDiCaL version: 2.1.3
% 2.12/0.57 % (2494169)Termination reason: Instruction limit
% 2.12/0.57 % (2494169)Termination phase: Saturation
% 2.12/0.57 % (2494169)Time elapsed: 0.030 s
% 2.12/0.57 % (2494169)Peak memory usage: 12 MB
% 2.12/0.57 % (2494169)Instructions burned: 66 (million)
% 2.12/0.57 % (2494181)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=851686013:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.12/0.57 % (2494179)Instruction limit reached!
% 2.12/0.57 % (2494179)------------------------------
% 2.12/0.57 % (2494179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.12/0.57 % (2494179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.12/0.57 % (2494179)CaDiCaL version: 2.1.3
% 2.12/0.57 % (2494179)Termination reason: Instruction limit
% 2.12/0.57 % (2494179)Termination phase: Saturation
% 2.12/0.57 % (2494179)Time elapsed: 0.007 s
% 2.12/0.57 % (2494179)Peak memory usage: 12 MB
% 2.12/0.57 % (2494177)Instruction limit reached!
% 2.12/0.57 % (2494177)------------------------------
% 2.12/0.57 % (2494177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.12/0.57 % (2494177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.12/0.57 % (2494177)CaDiCaL version: 2.1.3
% 2.12/0.57 % (2494177)Termination reason: Instruction limit
% 2.12/0.57 % (2494177)Termination phase: Saturation
% 2.12/0.57 % (2494177)Time elapsed: 0.014 s
% 2.12/0.57 % (2494177)Peak memory usage: 12 MB
% 2.12/0.57 % (2494177)Instructions burned: 31 (million)
% 2.12/0.57 % (2494179)Instructions burned: 28 (million)
% 2.12/0.57 % (2494181)Instruction limit reached!
% 2.12/0.57 % (2494181)------------------------------
% 2.12/0.57 % (2494181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.12/0.57 % (2494181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.12/0.57 % (2494181)CaDiCaL version: 2.1.3
% 2.12/0.57 % (2494181)Termination reason: Instruction limit
% 2.12/0.57 % (2494181)Termination phase: Saturation
% 2.12/0.57 % (2494181)Time elapsed: 0.010 s
% 2.12/0.57 % (2494181)Peak memory usage: 12 MB
% 2.12/0.57 % (2494181)Instructions burned: 20 (million)
% 2.12/0.57 % (2494188)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2573231107:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.12/0.57 % (2494185)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2278669263:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.12/0.57 % (2494186)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3930369581:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.12/0.57 % (2494189)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2111355898:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.12/0.57 % (2494190)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.12/0.57 % (2494190)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3866768882:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 2.12/0.57 % (2494190)Instruction limit reached!
% 2.12/0.57 % (2494190)------------------------------
% 2.12/0.57 % (2494190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.12/0.57 % (2494190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.12/0.57 % (2494190)CaDiCaL version: 2.1.3
% 2.12/0.57 % (2494190)Termination reason: Instruction limit
% 2.12/0.57 % (2494190)Termination phase: Saturation
% 2.12/0.57 % (2494190)Time elapsed: 0.004 s
% 2.12/0.57 % (2494190)Peak memory usage: 11 MB
% 2.12/0.57 % (2494190)Instructions burned: 9 (million)
% 2.12/0.57 % (2494189)Instruction limit reached!
% 2.12/0.57 % (2494189)------------------------------
% 2.12/0.57 % (2494189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.12/0.57 % (2494189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.12/0.57 % (2494189)CaDiCaL version: 2.1.3
% 2.12/0.57 % (2494189)Termination reason: Instruction limit
% 2.12/0.57 % (2494189)Termination phase: Saturation
% 2.12/0.57 % (2494189)Time elapsed: 0.018 s
% 2.51/0.65 % (2494189)Peak memory usage: 12 MB
% 2.51/0.65 % (2494189)Instructions burned: 42 (million)
% 2.51/0.65 % (2494196)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=164259119:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.51/0.65 % (2494196)Refutation not found, incomplete strategy
% 2.51/0.65 % (2494196)------------------------------
% 2.51/0.65 % (2494196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (2494196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (2494196)CaDiCaL version: 2.1.3
% 2.51/0.65 % (2494196)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.65 % (2494196)Time elapsed: 0.003 s
% 2.51/0.65 % (2494196)Peak memory usage: 12 MB
% 2.51/0.65 % (2494196)Instructions burned: 4 (million)
% 2.51/0.65 % (2494196)------------------------------
% 2.51/0.65 % (2494196)------------------------------
% 2.51/0.65 % (2494188)Instruction limit reached!
% 2.51/0.65 % (2494188)------------------------------
% 2.51/0.65 % (2494188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (2494188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (2494188)CaDiCaL version: 2.1.3
% 2.51/0.65 % (2494188)Termination reason: Instruction limit
% 2.51/0.65 % (2494188)Termination phase: Saturation
% 2.51/0.65 % (2494188)Time elapsed: 0.045 s
% 2.51/0.65 % (2494188)Peak memory usage: 13 MB
% 2.51/0.65 % (2494188)Instructions burned: 196 (million)
% 2.51/0.65 % (2494197)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=2554750514:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.51/0.65 % (2494197)Refutation not found, incomplete strategy
% 2.51/0.65 % (2494197)------------------------------
% 2.51/0.65 % (2494197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (2494197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (2494197)CaDiCaL version: 2.1.3
% 2.51/0.65 % (2494197)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.65 % (2494197)Time elapsed: 0.003 s
% 2.51/0.65 % (2494197)Peak memory usage: 12 MB
% 2.51/0.65 % (2494197)Instructions burned: 6 (million)
% 2.51/0.65 % (2494197)------------------------------
% 2.51/0.65 % (2494197)------------------------------
% 2.51/0.65 % (2494201)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3964124350:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.51/0.65 % (2494199)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.51/0.65 % (2494201)Instruction limit reached!
% 2.51/0.65 % (2494201)------------------------------
% 2.51/0.65 % (2494201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (2494201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (2494201)CaDiCaL version: 2.1.3
% 2.51/0.65 % (2494201)Termination reason: Instruction limit
% 2.51/0.65 % (2494201)Termination phase: Saturation
% 2.51/0.65 % (2494201)Time elapsed: 0.006 s
% 2.51/0.65 % (2494201)Peak memory usage: 12 MB
% 2.51/0.65 % (2494201)Instructions burned: 27 (million)
% 2.51/0.65 % (2494186)Instruction limit reached!
% 2.51/0.65 % (2494186)------------------------------
% 2.51/0.65 % (2494186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (2494199)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=133631442:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.51/0.65 % (2494186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.65 % (2494186)CaDiCaL version: 2.1.3
% 2.51/0.65 % (2494186)Termination reason: Instruction limit
% 2.51/0.65 % (2494186)Termination phase: Saturation
% 2.51/0.65 % (2494186)Time elapsed: 0.059 s
% 2.51/0.65 % (2494186)Peak memory usage: 13 MB
% 2.51/0.65 % (2494186)Instructions burned: 143 (million)
% 2.51/0.65 % (2494159)Instruction limit reached!
% 2.51/0.65 % (2494159)------------------------------
% 2.51/0.65 % (2494159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.65 % (2494159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.73 % (2494159)CaDiCaL version: 2.1.3
% 3.04/0.73 % (2494159)Termination reason: Instruction limit
% 3.04/0.73 % (2494159)Termination phase: Saturation
% 3.04/0.73 % (2494159)Time elapsed: 0.138 s
% 3.04/0.73 % (2494159)Peak memory usage: 13 MB
% 3.04/0.73 % (2494159)Instructions burned: 327 (million)
% 3.04/0.73 % (2494199)Instruction limit reached!
% 3.04/0.73 % (2494199)------------------------------
% 3.04/0.73 % (2494199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.73 % (2494199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.73 % (2494199)CaDiCaL version: 2.1.3
% 3.04/0.73 % (2494199)Termination reason: Instruction limit
% 3.04/0.73 % (2494199)Termination phase: Preprocessing 2
% 3.04/0.73 % (2494199)Time elapsed: 0.003 s
% 3.04/0.73 % (2494199)Peak memory usage: 10 MB
% 3.04/0.73 % (2494199)Instructions burned: 6 (million)
% 3.04/0.73 % (2494202)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3364440372:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 3.04/0.73 % (2494204)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=483649636:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.04/0.73 % (2494202)Refutation not found, incomplete strategy
% 3.04/0.73 % (2494202)------------------------------
% 3.04/0.73 % (2494202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.73 % (2494202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.73 % (2494202)CaDiCaL version: 2.1.3
% 3.04/0.73 % (2494202)Termination reason: Refutation not found, incomplete strategy
% 3.04/0.73 % (2494202)Time elapsed: 0.006 s
% 3.04/0.73 % (2494202)Peak memory usage: 12 MB
% 3.04/0.73 % (2494202)Instructions burned: 12 (million)
% 3.04/0.73 % (2494202)------------------------------
% 3.04/0.73 % (2494202)------------------------------
% 3.04/0.73 % (2494206)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=4042031891:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 3.04/0.73 % (2494207)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=2379621445:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 3.04/0.73 % (2494208)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2651765966:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 3.04/0.73 % (2494211)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=147981971:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 3.04/0.73 % (2494211)Instruction limit reached!
% 3.04/0.73 % (2494211)------------------------------
% 3.04/0.73 % (2494211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.73 % (2494211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.73 % (2494211)CaDiCaL version: 2.1.3
% 3.04/0.73 % (2494211)Termination reason: Instruction limit
% 3.04/0.73 % (2494211)Termination phase: Saturation
% 3.04/0.73 % (2494211)Time elapsed: 0.011 s
% 3.04/0.73 % (2494211)Peak memory usage: 12 MB
% 3.04/0.73 % (2494211)Instructions burned: 21 (million)
% 3.04/0.73 % (2494207)Instruction limit reached!
% 3.04/0.73 % (2494207)------------------------------
% 3.04/0.73 % (2494207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.73 % (2494207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.73 % (2494207)CaDiCaL version: 2.1.3
% 3.04/0.73 % (2494207)Termination reason: Instruction limit
% 3.04/0.73 % (2494207)Termination phase: Saturation
% 3.04/0.73 % (2494207)Time elapsed: 0.027 s
% 3.04/0.73 % (2494207)Peak memory usage: 13 MB
% 3.04/0.73 % (2494207)Instructions burned: 46 (million)
% 3.04/0.73 % (2494216)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.04/0.73 % (2494216)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1123061308:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 3.63/0.84 % (2494217)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2417569459:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.63/0.84 % (2494127)Instruction limit reached!
% 3.63/0.84 % (2494127)------------------------------
% 3.63/0.84 % (2494127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.84 % (2494127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.84 % (2494127)CaDiCaL version: 2.1.3
% 3.63/0.84 % (2494127)Termination reason: Instruction limit
% 3.63/0.84 % (2494127)Termination phase: Saturation
% 3.63/0.84 % (2494127)Time elapsed: 0.284 s
% 3.63/0.84 % (2494127)Peak memory usage: 15 MB
% 3.63/0.84 % (2494127)Instructions burned: 636 (million)
% 3.63/0.84 % (2494217)Instruction limit reached!
% 3.63/0.84 % (2494217)------------------------------
% 3.63/0.84 % (2494217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.84 % (2494217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.84 % (2494217)CaDiCaL version: 2.1.3
% 3.63/0.84 % (2494217)Termination reason: Instruction limit
% 3.63/0.84 % (2494217)Termination phase: Saturation
% 3.63/0.84 % (2494217)Time elapsed: 0.006 s
% 3.63/0.84 % (2494217)Peak memory usage: 12 MB
% 3.63/0.84 % (2494217)Instructions burned: 13 (million)
% 3.63/0.84 % (2494220)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=3121331423:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.63/0.84 % (2494221)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3535705504:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.63/0.84 % (2494204)Instruction limit reached!
% 3.63/0.84 % (2494204)------------------------------
% 3.63/0.84 % (2494204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.84 % (2494204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.84 % (2494204)CaDiCaL version: 2.1.3
% 3.63/0.84 % (2494204)Termination reason: Instruction limit
% 3.63/0.84 % (2494204)Termination phase: Saturation
% 3.63/0.84 % (2494204)Time elapsed: 0.084 s
% 3.63/0.84 % (2494204)Peak memory usage: 15 MB
% 3.63/0.84 % (2494204)Instructions burned: 319 (million)
% 3.63/0.84 % (2494224)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2885243984:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.63/0.84 % (2494224)Instruction limit reached!
% 3.63/0.84 % (2494224)------------------------------
% 3.63/0.84 % (2494224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.84 % (2494224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.84 % (2494224)CaDiCaL version: 2.1.3
% 3.63/0.84 % (2494224)Termination reason: Instruction limit
% 3.63/0.84 % (2494224)Termination phase: Saturation
% 3.63/0.84 % (2494224)Time elapsed: 0.008 s
% 3.63/0.84 % (2494224)Peak memory usage: 12 MB
% 3.63/0.84 % (2494224)Instructions burned: 32 (million)
% 3.63/0.84 % (2494221)Instruction limit reached!
% 3.63/0.84 % (2494221)------------------------------
% 3.63/0.84 % (2494221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.84 % (2494221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.84 % (2494221)CaDiCaL version: 2.1.3
% 3.63/0.84 % (2494221)Termination reason: Instruction limit
% 3.63/0.84 % (2494221)Termination phase: Saturation
% 3.63/0.84 % (2494221)Time elapsed: 0.026 s
% 3.63/0.84 % (2494221)Peak memory usage: 12 MB
% 3.63/0.84 % (2494221)Instructions burned: 53 (million)
% 3.63/0.84 % (2494220)Instruction limit reached!
% 3.63/0.84 % (2494220)------------------------------
% 3.63/0.84 % (2494220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.84 % (2494220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.84 % (2494220)CaDiCaL version: 2.1.3
% 3.63/0.84 % (2494220)Termination reason: Instruction limit
% 3.63/0.84 % (2494220)Termination phase: Saturation
% 3.63/0.84 % (2494220)Time elapsed: 0.033 s
% 3.63/0.84 % (2494220)Peak memory usage: 13 MB
% 3.63/0.84 % (2494220)Instructions burned: 68 (million)
% 3.63/0.84 % (2494226)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1835398948:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 3.63/0.84 % (2494227)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=347589711:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 4.33/0.96 % (2494228)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4120786620:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 4.33/0.96 % (2494228)Refutation not found, incomplete strategy
% 4.33/0.96 % (2494228)------------------------------
% 4.33/0.96 % (2494228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.96 % (2494228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.96 % (2494228)CaDiCaL version: 2.1.3
% 4.33/0.96 % (2494228)Termination reason: Refutation not found, incomplete strategy
% 4.33/0.96 % (2494228)Time elapsed: 0.007 s
% 4.33/0.96 % (2494228)Peak memory usage: 12 MB
% 4.33/0.96 % (2494228)Instructions burned: 13 (million)
% 4.33/0.96 % (2494216)Instruction limit reached!
% 4.33/0.96 % (2494216)------------------------------
% 4.33/0.96 % (2494216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.96 % (2494216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.96 % (2494216)CaDiCaL version: 2.1.3
% 4.33/0.96 % (2494216)Termination reason: Instruction limit
% 4.33/0.96 % (2494216)Termination phase: Saturation
% 4.33/0.96 % (2494216)Time elapsed: 0.083 s
% 4.33/0.96 % (2494216)Peak memory usage: 12 MB
% 4.33/0.96 % (2494216)Instructions burned: 200 (million)
% 4.33/0.96 % (2494228)------------------------------
% 4.33/0.96 % (2494228)------------------------------
% 4.33/0.96 % (2494227)Instruction limit reached!
% 4.33/0.96 % (2494227)------------------------------
% 4.33/0.96 % (2494227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.96 % (2494227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.96 % (2494227)CaDiCaL version: 2.1.3
% 4.33/0.96 % (2494227)Termination reason: Instruction limit
% 4.33/0.96 % (2494227)Termination phase: Saturation
% 4.33/0.96 % (2494227)Time elapsed: 0.016 s
% 4.33/0.96 % (2494227)Peak memory usage: 12 MB
% 4.33/0.96 % (2494227)Instructions burned: 35 (million)
% 4.33/0.96 % (2494232)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 4.33/0.96 % (2494226)Instruction limit reached!
% 4.33/0.96 % (2494226)------------------------------
% 4.33/0.96 % (2494226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.96 % (2494226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.96 % (2494226)CaDiCaL version: 2.1.3
% 4.33/0.96 % (2494226)Termination reason: Instruction limit
% 4.33/0.96 % (2494226)Termination phase: Saturation
% 4.33/0.96 % (2494226)Time elapsed: 0.037 s
% 4.33/0.96 % (2494226)Peak memory usage: 13 MB
% 4.33/0.96 % (2494226)Instructions burned: 138 (million)
% 4.33/0.96 % (2494232)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=620346011:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 4.33/0.96 % (2494233)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1324572141:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 4.33/0.96 % (2494234)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1752128749:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 4.33/0.96 % (2494235)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1858534319:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 4.33/0.96 % (2494235)Refutation not found, incomplete strategy
% 4.33/0.96 % (2494235)------------------------------
% 4.33/0.96 % (2494235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/0.96 % (2494235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/0.96 % (2494235)CaDiCaL version: 2.1.3
% 4.33/0.96 % (2494235)Termination reason: Refutation not found, incomplete strategy
% 4.33/0.96 % (2494235)Time elapsed: 0.001 s
% 4.33/0.96 % (2494235)Peak memory usage: 12 MB
% 4.33/0.96 % (2494235)Instructions burned: 4 (million)
% 4.33/0.96 % (2494235)------------------------------
% 4.33/0.96 % (2494235)------------------------------
% 4.33/0.96 % (2494240)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1744589619:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 4.33/0.96 % (2494234)Instruction limit reached!
% 4.33/0.96 % (2494234)------------------------------
% 5.51/1.04 % (2494234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.04 % (2494234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.04 % (2494234)CaDiCaL version: 2.1.3
% 5.51/1.04 % (2494234)Termination reason: Instruction limit
% 5.51/1.04 % (2494234)Termination phase: Saturation
% 5.51/1.04 % (2494234)Time elapsed: 0.049 s
% 5.51/1.04 % (2494234)Peak memory usage: 13 MB
% 5.51/1.04 % (2494234)Instructions burned: 97 (million)
% 5.51/1.04 % (2494242)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3978094563:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 5.51/1.04 % (2494232)Instruction limit reached!
% 5.51/1.04 % (2494232)------------------------------
% 5.51/1.04 % (2494232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.04 % (2494232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.04 % (2494232)CaDiCaL version: 2.1.3
% 5.51/1.04 % (2494232)Termination reason: Instruction limit
% 5.51/1.04 % (2494232)Termination phase: Saturation
% 5.51/1.04 % (2494232)Time elapsed: 0.080 s
% 5.51/1.04 % (2494232)Peak memory usage: 12 MB
% 5.51/1.04 % (2494232)Instructions burned: 180 (million)
% 5.51/1.04 % (2494208)Instruction limit reached!
% 5.51/1.04 % (2494208)------------------------------
% 5.51/1.04 % (2494208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.04 % (2494208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.04 % (2494208)CaDiCaL version: 2.1.3
% 5.51/1.04 % (2494208)Termination reason: Instruction limit
% 5.51/1.04 % (2494208)Termination phase: Saturation
% 5.51/1.04 % (2494208)Time elapsed: 0.223 s
% 5.51/1.04 % (2494208)Peak memory usage: 13 MB
% 5.51/1.04 % (2494208)Instructions burned: 481 (million)
% 5.51/1.04 % (2494244)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2939528721:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.51/1.04 % (2494245)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=260775729:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.51/1.04 % (2494233)Instruction limit reached!
% 5.51/1.04 % (2494233)------------------------------
% 5.51/1.04 % (2494233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.04 % (2494233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.04 % (2494233)CaDiCaL version: 2.1.3
% 5.51/1.04 % (2494233)Termination reason: Instruction limit
% 5.51/1.04 % (2494233)Termination phase: Saturation
% 5.51/1.04 % (2494233)Time elapsed: 0.111 s
% 5.51/1.04 % (2494233)Peak memory usage: 13 MB
% 5.51/1.04 % (2494233)Instructions burned: 248 (million)
% 5.51/1.04 % (2494245)Instruction limit reached!
% 5.51/1.04 % (2494245)------------------------------
% 5.51/1.04 % (2494245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.04 % (2494245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.04 % (2494245)CaDiCaL version: 2.1.3
% 5.51/1.04 % (2494245)Termination reason: Instruction limit
% 5.51/1.04 % (2494245)Termination phase: Saturation
% 5.51/1.04 % (2494245)Time elapsed: 0.022 s
% 5.51/1.04 % (2494245)Peak memory usage: 12 MB
% 5.51/1.04 % (2494245)Instructions burned: 45 (million)
% 5.51/1.04 % (2494248)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1709033011:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.51/1.04 % (2494248)Refutation not found, incomplete strategy
% 5.51/1.04 % (2494248)------------------------------
% 5.51/1.04 % (2494248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.04 % (2494248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.04 % (2494248)CaDiCaL version: 2.1.3
% 5.51/1.04 % (2494248)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.04 % (2494248)Time elapsed: 0.007 s
% 5.51/1.04 % (2494248)Peak memory usage: 12 MB
% 5.51/1.04 % (2494248)Instructions burned: 13 (million)
% 5.51/1.04 % (2494248)------------------------------
% 5.51/1.04 % (2494248)------------------------------
% 5.51/1.04 % (2494249)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1014891331:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 5.51/1.04 % (2494251)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3807239763:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/95Mi)
% 5.88/1.13 % (2494244)Instruction limit reached!
% 5.88/1.13 % (2494244)------------------------------
% 5.88/1.13 % (2494244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.13 % (2494244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.13 % (2494244)CaDiCaL version: 2.1.3
% 5.88/1.13 % (2494244)Termination reason: Instruction limit
% 5.88/1.13 % (2494244)Termination phase: Saturation
% 5.88/1.13 % (2494244)Time elapsed: 0.065 s
% 5.88/1.13 % (2494244)Peak memory usage: 13 MB
% 5.88/1.13 % (2494244)Instructions burned: 130 (million)
% 5.88/1.13 % (2494254)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=3531748787:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2994 on theBenchmark for (2994ds/65Mi)
% 5.88/1.13 % (2494251)Instruction limit reached!
% 5.88/1.13 % (2494251)------------------------------
% 5.88/1.13 % (2494251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.13 % (2494251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.13 % (2494251)CaDiCaL version: 2.1.3
% 5.88/1.13 % (2494251)Termination reason: Instruction limit
% 5.88/1.13 % (2494251)Termination phase: Saturation
% 5.88/1.13 % (2494251)Time elapsed: 0.046 s
% 5.88/1.13 % (2494251)Peak memory usage: 13 MB
% 5.88/1.13 % (2494251)Instructions burned: 97 (million)
% 5.88/1.13 % (2494240)Instruction limit reached!
% 5.88/1.13 % (2494240)------------------------------
% 5.88/1.13 % (2494240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.13 % (2494240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.13 % (2494240)CaDiCaL version: 2.1.3
% 5.88/1.13 % (2494240)Termination reason: Instruction limit
% 5.88/1.13 % (2494240)Termination phase: Saturation
% 5.88/1.13 % (2494240)Time elapsed: 0.192 s
% 5.88/1.13 % (2494240)Peak memory usage: 13 MB
% 5.88/1.13 % (2494240)Instructions burned: 878 (million)
% 5.88/1.13 % (2494254)Instruction limit reached!
% 5.88/1.13 % (2494254)------------------------------
% 5.88/1.13 % (2494254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.13 % (2494254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.13 % (2494254)CaDiCaL version: 2.1.3
% 5.88/1.13 % (2494254)Termination reason: Instruction limit
% 5.88/1.13 % (2494254)Termination phase: Saturation
% 5.88/1.13 % (2494254)Time elapsed: 0.032 s
% 5.88/1.13 % (2494254)Peak memory usage: 13 MB
% 5.88/1.13 % (2494254)Instructions burned: 67 (million)
% 5.88/1.13 % (2494257)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=191832798:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 5.88/1.13 % (2494256)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=3392724352:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2993 on theBenchmark for (2993ds/105Mi)
% 5.88/1.13 % (2494258)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2297981241:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/375Mi)
% 5.88/1.13 % (2494206)Instruction limit reached!
% 5.88/1.13 % (2494206)------------------------------
% 5.88/1.13 % (2494206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.13 % (2494206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.13 % (2494206)CaDiCaL version: 2.1.3
% 5.88/1.13 % (2494206)Termination reason: Instruction limit
% 5.88/1.13 % (2494206)Termination phase: Saturation
% 5.88/1.13 % (2494206)Time elapsed: 0.384 s
% 5.88/1.13 % (2494206)Peak memory usage: 16 MB
% 5.88/1.13 % (2494206)Instructions burned: 855 (million)
% 5.88/1.13 % (2494262)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4091495447:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/495Mi)
% 5.88/1.13 % (2494256)Instruction limit reached!
% 5.88/1.13 % (2494256)------------------------------
% 5.88/1.13 % (2494256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.88/1.13 % (2494256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494256)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494256)Termination reason: Instruction limit
% 6.21/1.21 % (2494256)Termination phase: Saturation
% 6.21/1.21 % (2494256)Time elapsed: 0.054 s
% 6.21/1.21 % (2494256)Peak memory usage: 13 MB
% 6.21/1.21 % (2494256)Instructions burned: 105 (million)
% 6.21/1.21 % (2494264)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=3213804084:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 6.21/1.21 % (2494242)Instruction limit reached!
% 6.21/1.21 % (2494242)------------------------------
% 6.21/1.21 % (2494242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.21 % (2494242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494242)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494242)Termination reason: Instruction limit
% 6.21/1.21 % (2494242)Termination phase: Saturation
% 6.21/1.21 % (2494242)Time elapsed: 0.225 s
% 6.21/1.21 % (2494242)Peak memory usage: 14 MB
% 6.21/1.21 % (2494242)Instructions burned: 517 (million)
% 6.21/1.21 % (2494264)Instruction limit reached!
% 6.21/1.21 % (2494264)------------------------------
% 6.21/1.21 % (2494264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.21 % (2494264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494264)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494264)Termination reason: Instruction limit
% 6.21/1.21 % (2494264)Termination phase: Saturation
% 6.21/1.21 % (2494264)Time elapsed: 0.016 s
% 6.21/1.21 % (2494264)Peak memory usage: 12 MB
% 6.21/1.21 % (2494264)Instructions burned: 36 (million)
% 6.21/1.21 % (2494266)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3599410699:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.21/1.21 % (2494267)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3511516364:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 6.21/1.21 % (2494267)Refutation not found, incomplete strategy
% 6.21/1.21 % (2494267)------------------------------
% 6.21/1.21 % (2494267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.21 % (2494267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494267)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494267)Termination reason: Refutation not found, incomplete strategy
% 6.21/1.21 % (2494267)Time elapsed: 0.002 s
% 6.21/1.21 % (2494267)Peak memory usage: 12 MB
% 6.21/1.21 % (2494267)Instructions burned: 4 (million)
% 6.21/1.21 % (2494267)------------------------------
% 6.21/1.21 % (2494267)------------------------------
% 6.21/1.21 % (2494249)Instruction limit reached!
% 6.21/1.21 % (2494249)------------------------------
% 6.21/1.21 % (2494249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.21 % (2494249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494249)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494249)Termination reason: Instruction limit
% 6.21/1.21 % (2494249)Termination phase: Saturation
% 6.21/1.21 % (2494249)Time elapsed: 0.206 s
% 6.21/1.21 % (2494249)Peak memory usage: 14 MB
% 6.21/1.21 % (2494249)Instructions burned: 451 (million)
% 6.21/1.21 % (2494185)Instruction limit reached!
% 6.21/1.21 % (2494185)------------------------------
% 6.21/1.21 % (2494185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.21 % (2494185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494185)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494185)Termination reason: Instruction limit
% 6.21/1.21 % (2494185)Termination phase: Saturation
% 6.21/1.21 % (2494185)Time elapsed: 0.574 s
% 6.21/1.21 % (2494185)Peak memory usage: 17 MB
% 6.21/1.21 % (2494185)Instructions burned: 1240 (million)
% 6.21/1.21 % (2494270)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1686392617:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2992 on theBenchmark for (2992ds/22Mi)
% 6.21/1.21 % (2494266)Instruction limit reached!
% 6.21/1.21 % (2494266)------------------------------
% 6.21/1.21 % (2494266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.21 % (2494266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.21 % (2494266)CaDiCaL version: 2.1.3
% 6.21/1.21 % (2494266)Termination reason: Instruction limit
% 6.21/1.29 % (2494266)Termination phase: Saturation
% 6.21/1.29 % (2494266)Time elapsed: 0.042 s
% 6.21/1.29 % (2494266)Peak memory usage: 12 MB
% 6.21/1.29 % (2494266)Instructions burned: 92 (million)
% 6.21/1.29 % (2494271)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=1569631275:i=338:bd=all:ins=4:rtra=on_2992 on theBenchmark for (2992ds/338Mi)
% 6.21/1.29 % (2494272)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3205040472:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/28Mi)
% 6.21/1.29 % (2494270)Instruction limit reached!
% 6.21/1.29 % (2494270)------------------------------
% 6.21/1.29 % (2494270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.29 % (2494270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.29 % (2494270)CaDiCaL version: 2.1.3
% 6.21/1.29 % (2494270)Termination reason: Instruction limit
% 6.21/1.29 % (2494270)Termination phase: Saturation
% 6.21/1.29 % (2494270)Time elapsed: 0.012 s
% 6.21/1.29 % (2494270)Peak memory usage: 12 MB
% 6.21/1.29 % (2494270)Instructions burned: 24 (million)
% 6.21/1.29 % (2494274)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.21/1.29 % (2494274)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4237725431:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2992 on theBenchmark for (2992ds/137Mi)
% 6.21/1.29 % (2494272)Instruction limit reached!
% 6.21/1.29 % (2494272)------------------------------
% 6.21/1.29 % (2494272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.29 % (2494272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.29 % (2494272)CaDiCaL version: 2.1.3
% 6.21/1.29 % (2494272)Termination reason: Instruction limit
% 6.21/1.29 % (2494272)Termination phase: Saturation
% 6.21/1.29 % (2494272)Time elapsed: 0.015 s
% 6.21/1.29 % (2494272)Peak memory usage: 12 MB
% 6.21/1.29 % (2494272)Instructions burned: 29 (million)
% 6.21/1.29 % (2494277)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=369436736:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2992 on theBenchmark for (2992ds/340Mi)
% 6.21/1.29 % (2494279)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1646879780:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 6.21/1.29 % (2494279)Refutation not found, incomplete strategy
% 6.21/1.29 % (2494279)------------------------------
% 6.21/1.29 % (2494279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.29 % (2494279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.29 % (2494279)CaDiCaL version: 2.1.3
% 6.21/1.29 % (2494279)Termination reason: Refutation not found, incomplete strategy
% 6.21/1.29 % (2494279)Time elapsed: 0.002 s
% 6.21/1.29 % (2494279)Peak memory usage: 12 MB
% 6.21/1.29 % (2494279)Instructions burned: 4 (million)
% 6.21/1.29 % (2494279)------------------------------
% 6.21/1.29 % (2494279)------------------------------
% 6.21/1.29 % (2494258)Instruction limit reached!
% 6.21/1.29 % (2494258)------------------------------
% 6.21/1.29 % (2494258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.21/1.29 % (2494258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.21/1.29 % (2494258)CaDiCaL version: 2.1.3
% 6.21/1.29 % (2494258)Termination reason: Instruction limit
% 6.21/1.29 % (2494258)Termination phase: Saturation
% 6.21/1.29 % (2494258)Time elapsed: 0.178 s
% 6.21/1.29 % (2494258)Peak memory usage: 14 MB
% 6.21/1.29 % (2494258)Instructions burned: 377 (million)
% 6.21/1.29 % (2494282)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 6.21/1.29 % (2494282)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2297546701:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/373Mi)
% 6.21/1.29 % (2494283)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3081590498:i=116:ep=RSTC:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/116Mi)
% 6.21/1.29 % (2494274)Instruction limit reached!
% 6.21/1.29 % (2494274)------------------------------
% 6.21/1.29 % (2494274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.37 % (2494274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.37 % (2494274)CaDiCaL version: 2.1.3
% 7.07/1.37 % (2494274)Termination reason: Instruction limit
% 7.07/1.37 % (2494274)Termination phase: Saturation
% 7.07/1.37 % (2494274)Time elapsed: 0.070 s
% 7.07/1.37 % (2494274)Peak memory usage: 13 MB
% 7.07/1.37 % (2494274)Instructions burned: 137 (million)
% 7.07/1.37 % (2494286)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=4275989576:i=575:rtra=on_2991 on theBenchmark for (2991ds/575Mi)
% 7.07/1.37 % (2494262)Instruction limit reached!
% 7.07/1.37 % (2494262)------------------------------
% 7.07/1.37 % (2494262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.37 % (2494262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.37 % (2494262)CaDiCaL version: 2.1.3
% 7.07/1.37 % (2494262)Termination reason: Instruction limit
% 7.07/1.37 % (2494262)Termination phase: Saturation
% 7.07/1.37 % (2494262)Time elapsed: 0.218 s
% 7.07/1.37 % (2494262)Peak memory usage: 14 MB
% 7.07/1.37 % (2494262)Instructions burned: 497 (million)
% 7.07/1.37 % (2494286)Refutation not found, incomplete strategy
% 7.07/1.37 % (2494286)------------------------------
% 7.07/1.37 % (2494286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.37 % (2494286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.37 % (2494286)CaDiCaL version: 2.1.3
% 7.07/1.37 % (2494286)Termination reason: Refutation not found, incomplete strategy
% 7.07/1.37 % (2494286)Time elapsed: 0.006 s
% 7.07/1.37 % (2494286)Peak memory usage: 12 MB
% 7.07/1.37 % (2494286)Instructions burned: 11 (million)
% 7.07/1.37 % (2494286)------------------------------
% 7.07/1.37 % (2494286)------------------------------
% 7.07/1.37 % (2494283)Instruction limit reached!
% 7.07/1.37 % (2494283)------------------------------
% 7.07/1.37 % (2494283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.37 % (2494283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.37 % (2494283)CaDiCaL version: 2.1.3
% 7.07/1.37 % (2494283)Termination reason: Instruction limit
% 7.07/1.37 % (2494283)Termination phase: Saturation
% 7.07/1.37 % (2494283)Time elapsed: 0.057 s
% 7.07/1.37 % (2494283)Peak memory usage: 13 MB
% 7.07/1.37 % (2494283)Instructions burned: 116 (million)
% 7.07/1.37 % (2494288)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4240795572:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2991 on theBenchmark for (2991ds/270Mi)
% 7.07/1.37 % (2494289)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=4018552772:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/9840Mi)
% 7.07/1.37 % (2494290)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1950947516:i=421:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/421Mi)
% 7.07/1.37 % (2494290)Refutation not found, incomplete strategy
% 7.07/1.37 % (2494290)------------------------------
% 7.07/1.37 % (2494290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.07/1.37 % (2494290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.07/1.37 % (2494290)CaDiCaL version: 2.1.3
% 7.07/1.37 % (2494290)Termination reason: Refutation not found, incomplete strategy
% 7.07/1.37 % (2494290)Time elapsed: 0.002 s
% 7.07/1.37 % (2494290)Peak memory usage: 12 MB
% 7.07/1.37 % (2494290)Instructions burned: 4 (million)
% 7.07/1.37 % (2494290)------------------------------
% 7.07/1.37 % (2494290)------------------------------
% 7.07/1.37 % (2494294)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 7.07/1.37 % (2494294)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=3687273789:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/270Mi)
% 7.07/1.37 % (2494271)Instruction limit reached!
% 7.07/1.37 % (2494271)------------------------------
% 7.07/1.37 % (2494271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.56 % (2494271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.56 % (2494271)CaDiCaL version: 2.1.3
% 7.94/1.56 % (2494271)Termination reason: Instruction limit
% 7.94/1.56 % (2494271)Termination phase: Saturation
% 7.94/1.56 % (2494271)Time elapsed: 0.165 s
% 7.94/1.56 % (2494271)Peak memory usage: 15 MB
% 7.94/1.56 % (2494271)Instructions burned: 340 (million)
% 7.94/1.56 % (2494277)Instruction limit reached!
% 7.94/1.56 % (2494277)------------------------------
% 7.94/1.56 % (2494277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.56 % (2494277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.56 % (2494277)CaDiCaL version: 2.1.3
% 7.94/1.56 % (2494277)Termination reason: Instruction limit
% 7.94/1.56 % (2494277)Termination phase: Saturation
% 7.94/1.56 % (2494277)Time elapsed: 0.148 s
% 7.94/1.56 % (2494277)Peak memory usage: 13 MB
% 7.94/1.56 % (2494277)Instructions burned: 342 (million)
% 7.94/1.56 % (2494296)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=530319257:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/31Mi)
% 7.94/1.57 % (2494297)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 7.94/1.57 % (2494297)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 7.94/1.57 % (2494297)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=80674784:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2990 on theBenchmark for (2990ds/1440Mi)
% 7.94/1.57 % (2494296)Instruction limit reached!
% 7.94/1.57 % (2494296)------------------------------
% 7.94/1.57 % (2494296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (2494296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (2494296)CaDiCaL version: 2.1.3
% 7.94/1.57 % (2494296)Termination reason: Instruction limit
% 7.94/1.57 % (2494296)Termination phase: Saturation
% 7.94/1.57 % (2494296)Time elapsed: 0.015 s
% 7.94/1.57 % (2494296)Peak memory usage: 12 MB
% 7.94/1.57 % (2494296)Instructions burned: 31 (million)
% 7.94/1.57 % (2494282)Instruction limit reached!
% 7.94/1.57 % (2494282)------------------------------
% 7.94/1.57 % (2494282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (2494282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (2494282)CaDiCaL version: 2.1.3
% 7.94/1.57 % (2494282)Termination reason: Instruction limit
% 7.94/1.57 % (2494282)Termination phase: Saturation
% 7.94/1.57 % (2494282)Time elapsed: 0.158 s
% 7.94/1.57 % (2494282)Peak memory usage: 13 MB
% 7.94/1.57 % (2494282)Instructions burned: 373 (million)
% 7.94/1.57 % (2494300)dis+10_2_sil=128000:si=on:random_seed=3549551027:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2990 on theBenchmark for (2990ds/339Mi)
% 7.94/1.57 % (2494300)Refutation not found, incomplete strategy
% 7.94/1.57 % (2494300)------------------------------
% 7.94/1.57 % (2494300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.57 % (2494300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.57 % (2494300)CaDiCaL version: 2.1.3
% 7.94/1.57 % (2494300)Termination reason: Refutation not found, incomplete strategy
% 7.94/1.57 % (2494300)Time elapsed: 0.002 s
% 7.94/1.57 % (2494300)Peak memory usage: 12 MB
% 7.94/1.57 % (2494300)Instructions burned: 4 (million)
% 7.94/1.57 % (2494300)------------------------------
% 7.94/1.57 % (2494300)------------------------------
% 7.94/1.57 % (2494301)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=3535307519:i=111:add=on:fgj=on:rtra=on:fdi=1024_2989 on theBenchmark for (2989ds/111Mi)
% 7.94/1.57 % (2494303)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1272990375:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2989 on theBenchmark for (2989ds/122Mi)
% 7.94/1.57 % (2494303)Refutation not found, incomplete strategy
% 7.94/1.57 % (2494303)------------------------------
% 7.94/1.57 % (2494303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.75/1.78 % (2494303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.75/1.78 % (2494303)CaDiCaL version: 2.1.3
% 8.75/1.78 % (2494303)Termination reason: Refutation not found, incomplete strategy
% 8.75/1.78 % (2494303)Time elapsed: 0.003 s
% 8.75/1.78 % (2494303)Peak memory usage: 12 MB
% 8.75/1.78 % (2494303)Instructions burned: 5 (million)
% 8.75/1.78 % (2494303)------------------------------
% 8.75/1.78 % (2494303)------------------------------
% 8.75/1.78 % (2494288)Instruction limit reached!
% 8.75/1.78 % (2494288)------------------------------
% 8.75/1.78 % (2494288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.75/1.78 % (2494288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.75/1.78 % (2494288)CaDiCaL version: 2.1.3
% 8.75/1.78 % (2494288)Termination reason: Instruction limit
% 8.75/1.78 % (2494288)Termination phase: Saturation
% 8.75/1.78 % (2494288)Time elapsed: 0.122 s
% 8.75/1.78 % (2494288)Peak memory usage: 13 MB
% 8.75/1.78 % (2494288)Instructions burned: 272 (million)
% 8.75/1.78 % (2494306)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=1349667509:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/136Mi)
% 8.75/1.78 % (2494307)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2666284311:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2989 on theBenchmark for (2989ds/232Mi)
% 8.75/1.78 % (2494301)Instruction limit reached!
% 8.75/1.78 % (2494301)------------------------------
% 8.75/1.78 % (2494301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.75/1.78 % (2494301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.75/1.78 % (2494301)CaDiCaL version: 2.1.3
% 8.75/1.78 % (2494301)Termination reason: Instruction limit
% 8.75/1.78 % (2494301)Termination phase: Saturation
% 8.75/1.78 % (2494301)Time elapsed: 0.055 s
% 8.75/1.78 % (2494301)Peak memory usage: 13 MB
% 8.75/1.78 % (2494301)Instructions burned: 113 (million)
% 8.75/1.78 % (2494294)Instruction limit reached!
% 8.75/1.78 % (2494294)------------------------------
% 8.75/1.78 % (2494294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.75/1.78 % (2494294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.75/1.78 % (2494294)CaDiCaL version: 2.1.3
% 8.75/1.78 % (2494294)Termination reason: Instruction limit
% 8.75/1.78 % (2494294)Termination phase: Saturation
% 8.75/1.78 % (2494294)Time elapsed: 0.133 s
% 8.75/1.78 % (2494294)Peak memory usage: 14 MB
% 8.75/1.78 % (2494294)Instructions burned: 271 (million)
% 8.75/1.78 % (2494310)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=2946170714:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/1254Mi)
% 8.75/1.78 % (2494311)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 8.75/1.78 % (2494311)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=1365417024:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2989 on theBenchmark for (2989ds/281Mi)
% 8.75/1.78 % (2494310)Refutation not found, incomplete strategy
% 8.75/1.78 % (2494310)------------------------------
% 8.75/1.78 % (2494310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.75/1.78 % (2494310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.75/1.78 % (2494310)CaDiCaL version: 2.1.3
% 8.75/1.78 % (2494310)Termination reason: Refutation not found, incomplete strategy
% 8.75/1.78 % (2494310)Time elapsed: 0.010 s
% 8.75/1.78 % (2494310)Peak memory usage: 12 MB
% 8.75/1.78 % (2494310)Instructions burned: 19 (million)
% 8.75/1.78 % (2494310)------------------------------
% 8.75/1.78 % (2494310)------------------------------
% 8.75/1.78 % (2494306)Instruction limit reached!
% 8.75/1.78 % (2494306)------------------------------
% 8.75/1.78 % (2494306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.75/1.78 % (2494306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.75/1.78 % (2494306)CaDiCaL version: 2.1.3
% 8.75/1.78 % (2494306)Termination reason: Instruction limit
% 8.75/1.78 % (2494306)Termination phase: Saturation
% 8.75/1.78 % (2494306)Time elapsed: 0.061 s
% 8.75/1.78 % (2494306)Peak memory usage: 12 MB
% 8.75/1.78 % (2494306)Instructions burned: 138 (million)
% 9.85/1.92 % (2494314)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1851272884:i=619:add=on:rtra=on_2988 on theBenchmark for (2988ds/619Mi)
% 9.85/1.92 % (2494314)Refutation not found, incomplete strategy
% 9.85/1.92 % (2494314)------------------------------
% 9.85/1.92 % (2494314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.85/1.92 % (2494314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/1.92 % (2494314)CaDiCaL version: 2.1.3
% 9.85/1.92 % (2494314)Termination reason: Refutation not found, incomplete strategy
% 9.85/1.92 % (2494314)Time elapsed: 0.006 s
% 9.85/1.92 % (2494314)Peak memory usage: 12 MB
% 9.85/1.92 % (2494314)Instructions burned: 12 (million)
% 9.85/1.92 % (2494314)------------------------------
% 9.85/1.92 % (2494314)------------------------------
% 9.85/1.92 % (2494315)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=2990083613:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/865Mi)
% 9.85/1.92 % (2494318)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2162890564:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/212Mi)
% 9.85/1.92 % (2494307)Instruction limit reached!
% 9.85/1.92 % (2494307)------------------------------
% 9.85/1.92 % (2494307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.85/1.92 % (2494307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/1.92 % (2494307)CaDiCaL version: 2.1.3
% 9.85/1.92 % (2494307)Termination reason: Instruction limit
% 9.85/1.92 % (2494307)Termination phase: Saturation
% 9.85/1.92 % (2494307)Time elapsed: 0.111 s
% 9.85/1.92 % (2494307)Peak memory usage: 13 MB
% 9.85/1.92 % (2494307)Instructions burned: 232 (million)
% 9.85/1.92 % (2494320)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3492844509:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/130Mi)
% 9.85/1.92 % (2494311)Instruction limit reached!
% 9.85/1.92 % (2494311)------------------------------
% 9.85/1.92 % (2494311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.85/1.92 % (2494311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/1.92 % (2494311)CaDiCaL version: 2.1.3
% 9.85/1.92 % (2494311)Termination reason: Instruction limit
% 9.85/1.92 % (2494311)Termination phase: Saturation
% 9.85/1.92 % (2494311)Time elapsed: 0.132 s
% 9.85/1.92 % (2494311)Peak memory usage: 13 MB
% 9.85/1.92 % (2494311)Instructions burned: 282 (million)
% 9.85/1.92 % (2494320)Instruction limit reached!
% 9.85/1.92 % (2494320)------------------------------
% 9.85/1.92 % (2494320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.85/1.92 % (2494320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/1.92 % (2494320)CaDiCaL version: 2.1.3
% 9.85/1.92 % (2494320)Termination reason: Instruction limit
% 9.85/1.92 % (2494320)Termination phase: Saturation
% 9.85/1.92 % (2494320)Time elapsed: 0.061 s
% 9.85/1.92 % (2494320)Peak memory usage: 12 MB
% 9.85/1.92 % (2494320)Instructions burned: 131 (million)
% 9.85/1.92 % (2494318)Instruction limit reached!
% 9.85/1.92 % (2494318)------------------------------
% 9.85/1.92 % (2494318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.85/1.92 % (2494318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/1.92 % (2494318)CaDiCaL version: 2.1.3
% 9.85/1.92 % (2494318)Termination reason: Instruction limit
% 9.85/1.92 % (2494318)Termination phase: Saturation
% 9.85/1.92 % (2494318)Time elapsed: 0.097 s
% 9.85/1.92 % (2494318)Peak memory usage: 13 MB
% 9.85/1.92 % (2494318)Instructions burned: 214 (million)
% 9.85/1.92 % (2494322)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3234773979:st=1.5:i=346:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/346Mi)
% 9.85/1.92 % (2494323)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3945840260:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/152Mi)
% 9.85/1.92 % (2494324)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1650300341:i=75:ep=R:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/75Mi)
% 9.85/1.92 % (2494324)Instruction limit reached!
% 9.85/1.92 % (2494324)------------------------------
% 9.85/1.92 % (2494324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.13 % (2494324)CaDiCaL version: 2.1.3
% 12.57/2.13 % (2494324)Termination reason: Instruction limit
% 12.57/2.13 % (2494324)Termination phase: Saturation
% 12.57/2.13 % (2494324)Time elapsed: 0.037 s
% 12.57/2.13 % (2494324)Peak memory usage: 13 MB
% 12.57/2.13 % (2494324)Instructions burned: 75 (million)
% 12.57/2.13 % (2494328)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=3523547770:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/387Mi)
% 12.57/2.13 % (2494323)Instruction limit reached!
% 12.57/2.13 % (2494323)------------------------------
% 12.57/2.13 % (2494323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.13 % (2494323)CaDiCaL version: 2.1.3
% 12.57/2.13 % (2494323)Termination reason: Instruction limit
% 12.57/2.13 % (2494323)Termination phase: Saturation
% 12.57/2.13 % (2494323)Time elapsed: 0.063 s
% 12.57/2.13 % (2494323)Peak memory usage: 12 MB
% 12.57/2.13 % (2494323)Instructions burned: 153 (million)
% 12.57/2.13 % (2494330)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=3503327250:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2986 on theBenchmark for (2986ds/148Mi)
% 12.57/2.13 % (2494330)Instruction limit reached!
% 12.57/2.13 % (2494330)------------------------------
% 12.57/2.13 % (2494330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.13 % (2494330)CaDiCaL version: 2.1.3
% 12.57/2.13 % (2494330)Termination reason: Instruction limit
% 12.57/2.13 % (2494330)Termination phase: Saturation
% 12.57/2.13 % (2494330)Time elapsed: 0.061 s
% 12.57/2.13 % (2494330)Peak memory usage: 12 MB
% 12.57/2.13 % (2494330)Instructions burned: 149 (million)
% 12.57/2.13 % (2494322)Instruction limit reached!
% 12.57/2.13 % (2494322)------------------------------
% 12.57/2.13 % (2494322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.13 % (2494322)CaDiCaL version: 2.1.3
% 12.57/2.13 % (2494322)Termination reason: Instruction limit
% 12.57/2.13 % (2494322)Termination phase: Saturation
% 12.57/2.13 % (2494322)Time elapsed: 0.165 s
% 12.57/2.13 % (2494322)Peak memory usage: 15 MB
% 12.57/2.13 % (2494322)Instructions burned: 348 (million)
% 12.57/2.13 % (2494332)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=272885436:i=161:piset=and:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/161Mi)
% 12.57/2.13 % (2494333)lrs+10_1_sil=128000:si=on:random_seed=3974127445:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/888Mi)
% 12.57/2.13 % (2494328)Instruction limit reached!
% 12.57/2.13 % (2494328)------------------------------
% 12.57/2.13 % (2494328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.13 % (2494328)CaDiCaL version: 2.1.3
% 12.57/2.13 % (2494328)Termination reason: Instruction limit
% 12.57/2.13 % (2494328)Termination phase: Saturation
% 12.57/2.13 % (2494328)Time elapsed: 0.164 s
% 12.57/2.13 % (2494328)Peak memory usage: 13 MB
% 12.57/2.13 % (2494328)Instructions burned: 387 (million)
% 12.57/2.13 % (2494332)Instruction limit reached!
% 12.57/2.13 % (2494332)------------------------------
% 12.57/2.13 % (2494332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.13 % (2494332)CaDiCaL version: 2.1.3
% 12.57/2.13 % (2494332)Termination reason: Instruction limit
% 12.57/2.13 % (2494332)Termination phase: Saturation
% 12.57/2.13 % (2494332)Time elapsed: 0.077 s
% 12.57/2.13 % (2494332)Peak memory usage: 13 MB
% 12.57/2.13 % (2494332)Instructions burned: 161 (million)
% 12.57/2.13 % (2494336)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=950896818:i=136:add=on:ins=4:rtra=on:sup=off_2985 on theBenchmark for (2985ds/136Mi)
% 12.57/2.13 % (2494336)Refutation not found, incomplete strategy
% 12.57/2.13 % (2494336)------------------------------
% 12.57/2.13 % (2494336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.57/2.13 % (2494336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.28 % (2494336)CaDiCaL version: 2.1.3
% 13.55/2.28 % (2494336)Termination reason: Refutation not found, incomplete strategy
% 13.55/2.28 % (2494336)Time elapsed: 0.008 s
% 13.55/2.28 % (2494336)Peak memory usage: 12 MB
% 13.55/2.28 % (2494336)Instructions burned: 15 (million)
% 13.55/2.28 % (2494336)------------------------------
% 13.55/2.28 % (2494336)------------------------------
% 13.55/2.28 % (2494337)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=1145339717:i=88:s2at=3:nm=2:rtra=on:rawr=on_2984 on theBenchmark for (2984ds/88Mi)
% 13.55/2.28 % (2494339)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3076605933:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2984 on theBenchmark for (2984ds/93Mi)
% 13.55/2.28 % (2494337)Instruction limit reached!
% 13.55/2.28 % (2494337)------------------------------
% 13.55/2.28 % (2494337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.55/2.28 % (2494337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.28 % (2494337)CaDiCaL version: 2.1.3
% 13.55/2.28 % (2494337)Termination reason: Instruction limit
% 13.55/2.28 % (2494337)Termination phase: Saturation
% 13.55/2.28 % (2494337)Time elapsed: 0.043 s
% 13.55/2.28 % (2494337)Peak memory usage: 13 MB
% 13.55/2.28 % (2494337)Instructions burned: 90 (million)
% 13.55/2.28 % (2494315)Instruction limit reached!
% 13.55/2.28 % (2494315)------------------------------
% 13.55/2.28 % (2494315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.55/2.28 % (2494315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.28 % (2494315)CaDiCaL version: 2.1.3
% 13.55/2.28 % (2494315)Termination reason: Instruction limit
% 13.55/2.28 % (2494315)Termination phase: Saturation
% 13.55/2.28 % (2494315)Time elapsed: 0.444 s
% 13.55/2.28 % (2494315)Peak memory usage: 19 MB
% 13.55/2.28 % (2494315)Instructions burned: 867 (million)
% 13.55/2.28 % (2494339)Instruction limit reached!
% 13.55/2.28 % (2494339)------------------------------
% 13.55/2.28 % (2494339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.55/2.28 % (2494339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.28 % (2494339)CaDiCaL version: 2.1.3
% 13.55/2.28 % (2494339)Termination reason: Instruction limit
% 13.55/2.28 % (2494339)Termination phase: Saturation
% 13.55/2.28 % (2494339)Time elapsed: 0.040 s
% 13.55/2.28 % (2494339)Peak memory usage: 12 MB
% 13.55/2.28 % (2494339)Instructions burned: 95 (million)
% 13.55/2.28 % (2494342)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3933083958:i=2186:rtra=on:ixr=off_2984 on theBenchmark for (2984ds/2186Mi)
% 13.55/2.28 % (2494343)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3217783866:s2a=on:i=240:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/240Mi)
% 13.55/2.28 % (2494344)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=3743702685:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2984 on theBenchmark for (2984ds/805Mi)
% 13.55/2.28 % (2494297)Instruction limit reached!
% 13.55/2.28 % (2494297)------------------------------
% 13.55/2.28 % (2494297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.55/2.28 % (2494297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.28 % (2494297)CaDiCaL version: 2.1.3
% 13.55/2.28 % (2494297)Termination reason: Instruction limit
% 13.55/2.28 % (2494297)Termination phase: Saturation
% 13.55/2.28 % (2494297)Time elapsed: 0.662 s
% 13.55/2.28 % (2494297)Peak memory usage: 16 MB
% 13.55/2.28 % (2494297)Instructions burned: 1442 (million)
% 13.55/2.28 % (2494348)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 13.55/2.28 % (2494348)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=2937046713:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2983 on theBenchmark for (2983ds/391Mi)
% 13.55/2.28 % (2494344)Refutation not found, incomplete strategy
% 13.55/2.28 % (2494344)------------------------------
% 13.55/2.28 % (2494344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.55/2.28 % (2494344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.42 % (2494344)CaDiCaL version: 2.1.3
% 14.29/2.42 % (2494344)Termination reason: Refutation not found, incomplete strategy
% 14.29/2.42 % (2494344)Time elapsed: 0.064 s
% 14.29/2.42 % (2494344)Peak memory usage: 13 MB
% 14.29/2.42 % (2494344)Instructions burned: 128 (million)
% 14.29/2.42 % (2494344)------------------------------
% 14.29/2.42 % (2494344)------------------------------
% 14.29/2.42 % (2494350)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=462205855:i=355:av=off:fsr=off:rtra=on:ixr=off_2983 on theBenchmark for (2983ds/355Mi)
% 14.29/2.42 % (2494343)Instruction limit reached!
% 14.29/2.42 % (2494343)------------------------------
% 14.29/2.42 % (2494343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.42 % (2494343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.42 % (2494343)CaDiCaL version: 2.1.3
% 14.29/2.42 % (2494343)Termination reason: Instruction limit
% 14.29/2.42 % (2494343)Termination phase: Saturation
% 14.29/2.42 % (2494343)Time elapsed: 0.114 s
% 14.29/2.42 % (2494343)Peak memory usage: 13 MB
% 14.29/2.42 % (2494343)Instructions burned: 241 (million)
% 14.29/2.42 % (2494352)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=2017368734:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/314Mi)
% 14.29/2.42 % (2494352)Refutation not found, incomplete strategy
% 14.29/2.42 % (2494352)------------------------------
% 14.29/2.42 % (2494352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.42 % (2494352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.42 % (2494352)CaDiCaL version: 2.1.3
% 14.29/2.42 % (2494352)Termination reason: Refutation not found, incomplete strategy
% 14.29/2.42 % (2494352)Time elapsed: 0.003 s
% 14.29/2.42 % (2494352)Peak memory usage: 12 MB
% 14.29/2.42 % (2494352)Instructions burned: 5 (million)
% 14.29/2.42 % (2494352)------------------------------
% 14.29/2.42 % (2494352)------------------------------
% 14.29/2.42 % (2494354)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=550058768:s2a=on:i=251:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/251Mi)
% 14.29/2.42 % (2494333)Instruction limit reached!
% 14.29/2.42 % (2494333)------------------------------
% 14.29/2.42 % (2494333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.42 % (2494333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.42 % (2494333)CaDiCaL version: 2.1.3
% 14.29/2.42 % (2494333)Termination reason: Instruction limit
% 14.29/2.42 % (2494333)Termination phase: Saturation
% 14.29/2.42 % (2494333)Time elapsed: 0.385 s
% 14.29/2.42 % (2494333)Peak memory usage: 14 MB
% 14.29/2.42 % (2494333)Instructions burned: 889 (million)
% 14.29/2.42 % (2494356)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=1110514163:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2981 on theBenchmark for (2981ds/2470Mi)
% 14.29/2.42 % (2494348)Instruction limit reached!
% 14.29/2.42 % (2494348)------------------------------
% 14.29/2.42 % (2494348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.42 % (2494348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.42 % (2494348)CaDiCaL version: 2.1.3
% 14.29/2.42 % (2494348)Termination reason: Instruction limit
% 14.29/2.42 % (2494348)Termination phase: Saturation
% 14.29/2.42 % (2494348)Time elapsed: 0.188 s
% 14.29/2.42 % (2494348)Peak memory usage: 13 MB
% 14.29/2.42 % (2494348)Instructions burned: 392 (million)
% 14.29/2.42 % (2494350)Instruction limit reached!
% 14.29/2.42 % (2494350)------------------------------
% 14.29/2.42 % (2494350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.42 % (2494350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.42 % (2494350)CaDiCaL version: 2.1.3
% 14.29/2.42 % (2494350)Termination reason: Instruction limit
% 14.29/2.42 % (2494350)Termination phase: Saturation
% 14.29/2.42 % (2494350)Time elapsed: 0.171 s
% 14.29/2.42 % (2494350)Peak memory usage: 14 MB
% 14.29/2.42 % (2494350)Instructions burned: 356 (million)
% 14.29/2.42 % (2494358)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=1135240917:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2981 on theBenchmark for (2981ds/673Mi)
% 15.88/2.67 % (2494359)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2260578713:i=116:ep=RSTC:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/116Mi)
% 15.88/2.67 % (2494354)Instruction limit reached!
% 15.88/2.67 % (2494354)------------------------------
% 15.88/2.67 % (2494354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.67 % (2494354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.67 % (2494354)CaDiCaL version: 2.1.3
% 15.88/2.67 % (2494354)Termination reason: Instruction limit
% 15.88/2.67 % (2494354)Termination phase: Saturation
% 15.88/2.67 % (2494354)Time elapsed: 0.119 s
% 15.88/2.67 % (2494354)Peak memory usage: 14 MB
% 15.88/2.67 % (2494354)Instructions burned: 252 (million)
% 15.88/2.67 % (2494362)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1288656241:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2981 on theBenchmark for (2981ds/270Mi)
% 15.88/2.67 % (2494359)Instruction limit reached!
% 15.88/2.67 % (2494359)------------------------------
% 15.88/2.67 % (2494359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.67 % (2494359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.67 % (2494359)CaDiCaL version: 2.1.3
% 15.88/2.67 % (2494359)Termination reason: Instruction limit
% 15.88/2.67 % (2494359)Termination phase: Saturation
% 15.88/2.67 % (2494359)Time elapsed: 0.057 s
% 15.88/2.67 % (2494359)Peak memory usage: 13 MB
% 15.88/2.67 % (2494359)Instructions burned: 118 (million)
% 15.88/2.67 % (2494364)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=2897481490:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2980 on theBenchmark for (2980ds/30Mi)
% 15.88/2.67 % (2494257)Instruction limit reached!
% 15.88/2.67 % (2494257)------------------------------
% 15.88/2.67 % (2494257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.67 % (2494257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.67 % (2494257)CaDiCaL version: 2.1.3
% 15.88/2.67 % (2494257)Termination reason: Instruction limit
% 15.88/2.67 % (2494257)Termination phase: Saturation
% 15.88/2.67 % (2494257)Time elapsed: 1.322 s
% 15.88/2.67 % (2494257)Peak memory usage: 35 MB
% 15.88/2.67 % (2494257)Instructions burned: 5755 (million)
% 15.88/2.67 % (2494364)Instruction limit reached!
% 15.88/2.67 % (2494364)------------------------------
% 15.88/2.67 % (2494364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.67 % (2494364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.67 % (2494364)CaDiCaL version: 2.1.3
% 15.88/2.67 % (2494364)Termination reason: Instruction limit
% 15.88/2.67 % (2494364)Termination phase: Saturation
% 15.88/2.67 % (2494364)Time elapsed: 0.017 s
% 15.88/2.67 % (2494364)Peak memory usage: 13 MB
% 15.88/2.67 % (2494364)Instructions burned: 31 (million)
% 15.88/2.67 % (2494366)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 15.88/2.67 % (2494366)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=1946082737:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2980 on theBenchmark for (2980ds/39Mi)
% 15.88/2.67 % (2494366)Instruction limit reached!
% 15.88/2.67 % (2494366)------------------------------
% 15.88/2.67 % (2494366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.88/2.67 % (2494366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.88/2.67 % (2494366)CaDiCaL version: 2.1.3
% 15.88/2.67 % (2494366)Termination reason: Instruction limit
% 15.88/2.67 % (2494366)Termination phase: Saturation
% 15.88/2.67 % (2494366)Time elapsed: 0.010 s
% 15.88/2.67 % (2494366)Peak memory usage: 12 MB
% 15.88/2.67 % (2494366)Instructions burned: 42 (million)
% 15.88/2.67 % (2494367)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2794073525:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2980 on theBenchmark for (2980ds/365Mi)
% 15.88/2.67 % (2494369)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4007614120:i=158:av=off:rtra=on_2980 on theBenchmark for (2980ds/158Mi)
% 15.88/2.67 % (2494362)Instruction limit reached!
% 15.88/2.67 % (2494362)------------------------------
% 15.88/2.67 % (2494362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.82 % (2494362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.82 % (2494362)CaDiCaL version: 2.1.3
% 16.97/2.82 % (2494362)Termination reason: Instruction limit
% 16.97/2.82 % (2494362)Termination phase: Saturation
% 16.97/2.82 % (2494362)Time elapsed: 0.127 s
% 16.97/2.82 % (2494362)Peak memory usage: 13 MB
% 16.97/2.82 % (2494362)Instructions burned: 270 (million)
% 16.97/2.82 % (2494372)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 16.97/2.82 % (2494369)Instruction limit reached!
% 16.97/2.82 % (2494369)------------------------------
% 16.97/2.82 % (2494369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.82 % (2494369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.82 % (2494369)CaDiCaL version: 2.1.3
% 16.97/2.82 % (2494369)Termination reason: Instruction limit
% 16.97/2.82 % (2494369)Termination phase: Saturation
% 16.97/2.82 % (2494369)Time elapsed: 0.041 s
% 16.97/2.82 % (2494369)Peak memory usage: 12 MB
% 16.97/2.82 % (2494369)Instructions burned: 160 (million)
% 16.97/2.82 % (2494372)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=538699895:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/252Mi)
% 16.97/2.82 % (2494373)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2918150077:i=213:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/213Mi)
% 16.97/2.82 % (2494373)Refutation not found, incomplete strategy
% 16.97/2.82 % (2494373)------------------------------
% 16.97/2.82 % (2494373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.82 % (2494373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.82 % (2494373)CaDiCaL version: 2.1.3
% 16.97/2.82 % (2494373)Termination reason: Refutation not found, incomplete strategy
% 16.97/2.82 % (2494373)Time elapsed: 0.001 s
% 16.97/2.82 % (2494373)Peak memory usage: 12 MB
% 16.97/2.82 % (2494373)Instructions burned: 5 (million)
% 16.97/2.82 % (2494373)------------------------------
% 16.97/2.82 % (2494373)------------------------------
% 16.97/2.82 % (2494376)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=3048804236:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2979 on theBenchmark for (2979ds/160Mi)
% 16.97/2.82 % (2494376)Instruction limit reached!
% 16.97/2.82 % (2494376)------------------------------
% 16.97/2.82 % (2494376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.82 % (2494376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.82 % (2494376)CaDiCaL version: 2.1.3
% 16.97/2.82 % (2494376)Termination reason: Instruction limit
% 16.97/2.82 % (2494376)Termination phase: Saturation
% 16.97/2.82 % (2494376)Time elapsed: 0.038 s
% 16.97/2.82 % (2494376)Peak memory usage: 13 MB
% 16.97/2.82 % (2494376)Instructions burned: 162 (million)
% 16.97/2.82 % (2494378)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=3531086594:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/763Mi)
% 16.97/2.82 % (2494367)Instruction limit reached!
% 16.97/2.82 % (2494367)------------------------------
% 16.97/2.82 % (2494367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.82 % (2494367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.82 % (2494367)CaDiCaL version: 2.1.3
% 16.97/2.82 % (2494367)Termination reason: Instruction limit
% 16.97/2.82 % (2494367)Termination phase: Saturation
% 16.97/2.82 % (2494367)Time elapsed: 0.151 s
% 16.97/2.82 % (2494367)Peak memory usage: 13 MB
% 16.97/2.82 % (2494367)Instructions burned: 366 (million)
% 16.97/2.82 % (2494380)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 16.97/2.82 % (2494380)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=1974277339:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2978 on theBenchmark for (2978ds/237Mi)
% 16.97/2.82 % (2494372)Instruction limit reached!
% 16.97/2.82 % (2494372)------------------------------
% 16.97/2.88 % (2494372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.88 % (2494372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.88 % (2494372)CaDiCaL version: 2.1.3
% 16.97/2.88 % (2494372)Termination reason: Instruction limit
% 16.97/2.88 % (2494372)Termination phase: Saturation
% 16.97/2.88 % (2494372)Time elapsed: 0.123 s
% 16.97/2.88 % (2494372)Peak memory usage: 14 MB
% 16.97/2.88 % (2494372)Instructions burned: 252 (million)
% 16.97/2.88 % (2494358)Instruction limit reached!
% 16.97/2.88 % (2494358)------------------------------
% 16.97/2.88 % (2494358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.88 % (2494358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.88 % (2494358)CaDiCaL version: 2.1.3
% 16.97/2.88 % (2494358)Termination reason: Instruction limit
% 16.97/2.88 % (2494358)Termination phase: Saturation
% 16.97/2.88 % (2494358)Time elapsed: 0.302 s
% 16.97/2.88 % (2494358)Peak memory usage: 15 MB
% 16.97/2.88 % (2494358)Instructions burned: 674 (million)
% 16.97/2.88 % (2494382)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=466376001:s2a=on:i=386:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/386Mi)
% 16.97/2.88 % (2494383)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=279499197:i=300:piset=and:nm=32:rtra=on_2978 on theBenchmark for (2978ds/300Mi)
% 16.97/2.88 % (2494380)Instruction limit reached!
% 16.97/2.88 % (2494380)------------------------------
% 16.97/2.88 % (2494380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.88 % (2494380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.88 % (2494380)CaDiCaL version: 2.1.3
% 16.97/2.88 % (2494380)Termination reason: Instruction limit
% 16.97/2.88 % (2494380)Termination phase: Saturation
% 16.97/2.88 % (2494380)Time elapsed: 0.111 s
% 16.97/2.88 % (2494380)Peak memory usage: 13 MB
% 16.97/2.88 % (2494380)Instructions burned: 238 (million)
% 16.97/2.88 % (2494386)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=1067857719:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/567Mi)
% 16.97/2.88 % (2494378)Instruction limit reached!
% 16.97/2.88 % (2494378)------------------------------
% 16.97/2.88 % (2494378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.88 % (2494378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.88 % (2494378)CaDiCaL version: 2.1.3
% 16.97/2.88 % (2494378)Termination reason: Instruction limit
% 16.97/2.88 % (2494378)Termination phase: Saturation
% 16.97/2.88 % (2494378)Time elapsed: 0.207 s
% 16.97/2.88 % (2494378)Peak memory usage: 16 MB
% 16.97/2.88 % (2494378)Instructions burned: 767 (million)
% 16.97/2.88 % (2494388)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=1347095347:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2976 on theBenchmark for (2976ds/379Mi)
% 16.97/2.88 % (2494383)Instruction limit reached!
% 16.97/2.88 % (2494383)------------------------------
% 16.97/2.88 % (2494383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.88 % (2494383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.88 % (2494383)CaDiCaL version: 2.1.3
% 16.97/2.88 % (2494383)Termination reason: Instruction limit
% 16.97/2.88 % (2494383)Termination phase: Saturation
% 16.97/2.88 % (2494383)Time elapsed: 0.142 s
% 16.97/2.88 % (2494383)Peak memory usage: 13 MB
% 16.97/2.88 % (2494383)Instructions burned: 300 (million)
% 16.97/2.88 % (2494390)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=1423670377:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2976 on theBenchmark for (2976ds/429Mi)
% 16.97/2.88 % (2494382)Instruction limit reached!
% 16.97/2.88 % (2494382)------------------------------
% 16.97/2.88 % (2494382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.88 % (2494382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.88 % (2494382)CaDiCaL version: 2.1.3
% 16.97/2.88 % (2494382)Termination reason: Instruction limit
% 16.97/2.88 % (2494382)Termination phase: Saturation
% 16.97/2.88 % (2494382)Time elapsed: 0.173 s
% 16.97/2.88 % (2494382)Peak memory usage: 12 MB
% 16.97/2.88 % (2494382)Instructions burned: 387 (million)
% 16.97/2.88 % (2494392)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=1192002335:i=478:bd=all:rtra=on_2976 on theBenchmark for (2976ds/478Mi)
% 16.97/2.88 % (2494388)Instruction limit reached!
% 19.64/3.10 % (2494388)------------------------------
% 19.64/3.10 % (2494388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494388)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494388)Termination reason: Instruction limit
% 19.64/3.10 % (2494388)Termination phase: Saturation
% 19.64/3.10 % (2494388)Time elapsed: 0.086 s
% 19.64/3.10 % (2494388)Peak memory usage: 14 MB
% 19.64/3.10 % (2494388)Instructions burned: 380 (million)
% 19.64/3.10 % (2494394)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=461089728:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2975 on theBenchmark for (2975ds/445Mi)
% 19.64/3.10 % (2494386)Instruction limit reached!
% 19.64/3.10 % (2494386)------------------------------
% 19.64/3.10 % (2494386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494386)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494386)Termination reason: Instruction limit
% 19.64/3.10 % (2494386)Termination phase: Saturation
% 19.64/3.10 % (2494386)Time elapsed: 0.240 s
% 19.64/3.10 % (2494386)Peak memory usage: 14 MB
% 19.64/3.10 % (2494386)Instructions burned: 568 (million)
% 19.64/3.10 % (2494394)Instruction limit reached!
% 19.64/3.10 % (2494394)------------------------------
% 19.64/3.10 % (2494394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494394)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494394)Termination reason: Instruction limit
% 19.64/3.10 % (2494394)Termination phase: Saturation
% 19.64/3.10 % (2494394)Time elapsed: 0.111 s
% 19.64/3.10 % (2494394)Peak memory usage: 15 MB
% 19.64/3.10 % (2494394)Instructions burned: 447 (million)
% 19.64/3.10 % (2494390)Instruction limit reached!
% 19.64/3.10 % (2494390)------------------------------
% 19.64/3.10 % (2494390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494390)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494390)Termination reason: Instruction limit
% 19.64/3.10 % (2494390)Termination phase: Saturation
% 19.64/3.10 % (2494390)Time elapsed: 0.190 s
% 19.64/3.10 % (2494390)Peak memory usage: 14 MB
% 19.64/3.10 % (2494390)Instructions burned: 431 (million)
% 19.64/3.10 % (2494397)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3226369970:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/302Mi)
% 19.64/3.10 % (2494397)Refutation not found, incomplete strategy
% 19.64/3.10 % (2494397)------------------------------
% 19.64/3.10 % (2494397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494397)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494397)Termination reason: Refutation not found, incomplete strategy
% 19.64/3.10 % (2494397)Time elapsed: 0.001 s
% 19.64/3.10 % (2494397)Peak memory usage: 12 MB
% 19.64/3.10 % (2494397)Instructions burned: 4 (million)
% 19.64/3.10 % (2494397)------------------------------
% 19.64/3.10 % (2494397)------------------------------
% 19.64/3.10 % (2494396)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=1698989227:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2974 on theBenchmark for (2974ds/71Mi)
% 19.64/3.10 % (2494400)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 19.64/3.10 % (2494400)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 19.64/3.10 % (2494398)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=3677406633:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2974 on theBenchmark for (2974ds/4980Mi)
% 19.64/3.10 % (2494400)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1305491593:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2974 on theBenchmark for (2974ds/100Mi)
% 19.64/3.10 % (2494398)Refutation not found, incomplete strategy
% 19.64/3.10 % (2494398)------------------------------
% 19.64/3.10 % (2494398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494398)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494398)Termination reason: Refutation not found, incomplete strategy
% 19.64/3.10 % (2494398)Time elapsed: 0.003 s
% 19.64/3.10 % (2494398)Peak memory usage: 12 MB
% 19.64/3.10 % (2494398)Instructions burned: 6 (million)
% 19.64/3.10 % (2494398)------------------------------
% 19.64/3.10 % (2494398)------------------------------
% 19.64/3.10 % (2494404)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3786157444:i=76:piset=equals:rtra=on:ntd=on_2974 on theBenchmark for (2974ds/76Mi)
% 19.64/3.10 % (2494400)Instruction limit reached!
% 19.64/3.10 % (2494400)------------------------------
% 19.64/3.10 % (2494400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494400)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494400)Termination reason: Instruction limit
% 19.64/3.10 % (2494400)Termination phase: Saturation
% 19.64/3.10 % (2494400)Time elapsed: 0.023 s
% 19.64/3.10 % (2494400)Peak memory usage: 12 MB
% 19.64/3.10 % (2494400)Instructions burned: 105 (million)
% 19.64/3.10 % (2494396)Instruction limit reached!
% 19.64/3.10 % (2494396)------------------------------
% 19.64/3.10 % (2494396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494396)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494396)Termination reason: Instruction limit
% 19.64/3.10 % (2494396)Termination phase: Saturation
% 19.64/3.10 % (2494396)Time elapsed: 0.030 s
% 19.64/3.10 % (2494396)Peak memory usage: 12 MB
% 19.64/3.10 % (2494396)Instructions burned: 74 (million)
% 19.64/3.10 % (2494406)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=4175772198:i=289:rtra=on_2974 on theBenchmark for (2974ds/289Mi)
% 19.64/3.10 % (2494342)Instruction limit reached!
% 19.64/3.10 % (2494342)------------------------------
% 19.64/3.10 % (2494342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494342)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494342)Termination reason: Instruction limit
% 19.64/3.10 % (2494342)Termination phase: Saturation
% 19.64/3.10 % (2494342)Time elapsed: 1.012 s
% 19.64/3.10 % (2494342)Peak memory usage: 18 MB
% 19.64/3.10 % (2494342)Instructions burned: 2187 (million)
% 19.64/3.10 % (2494407)lrs+2_64_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_first:bsr=unit_only:cbe=off:uwa=interpreted_only:nwc=0.5:slsqc=5:sac=on:slsq=on:random_seed=1623360743:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2974 on theBenchmark for (2974ds/493Mi)
% 19.64/3.10 % (2494392)Instruction limit reached!
% 19.64/3.10 % (2494392)------------------------------
% 19.64/3.10 % (2494392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494392)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494392)Termination reason: Instruction limit
% 19.64/3.10 % (2494392)Termination phase: Saturation
% 19.64/3.10 % (2494392)Time elapsed: 0.227 s
% 19.64/3.10 % (2494392)Peak memory usage: 14 MB
% 19.64/3.10 % (2494392)Instructions burned: 479 (million)
% 19.64/3.10 % (2494404)Instruction limit reached!
% 19.64/3.10 % (2494404)------------------------------
% 19.64/3.10 % (2494404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494404)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494404)Termination reason: Instruction limit
% 19.64/3.10 % (2494404)Termination phase: Saturation
% 19.64/3.10 % (2494404)Time elapsed: 0.036 s
% 19.64/3.10 % (2494404)Peak memory usage: 13 MB
% 19.64/3.10 % (2494404)Instructions burned: 78 (million)
% 19.64/3.10 % (2494409)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=2948763397:cond=on:i=34:hud=10:nm=10:rtra=on_2973 on theBenchmark for (2973ds/34Mi)
% 19.64/3.10 % (2494411)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 19.64/3.10 % (2494411)dis+1010_1_to=lpo:irw=on:plsq=on:drc=ordering:plsqc=4:cnfonf=lazy_simp:si=on:sp=reverse_frequency:sos=on:plsqr=32,1:cbe=off:uwa=off:rp=on:lwlo=on:random_seed=826017158:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2973 on theBenchmark for (2973ds/372Mi)
% 19.64/3.10 % (2494411)Refutation not found, incomplete strategy
% 19.64/3.10 % (2494411)------------------------------
% 19.64/3.10 % (2494411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494411)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494411)Termination reason: Refutation not found, incomplete strategy
% 19.64/3.10 % (2494411)Time elapsed: 0.006 s
% 19.64/3.10 % (2494411)Peak memory usage: 12 MB
% 19.64/3.10 % (2494411)Instructions burned: 12 (million)
% 19.64/3.10 % (2494411)------------------------------
% 19.64/3.10 % (2494411)------------------------------
% 19.64/3.10 % (2494412)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=1790779146:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2973 on theBenchmark for (2973ds/670Mi)
% 19.64/3.10 % (2494409)Instruction limit reached!
% 19.64/3.10 % (2494409)------------------------------
% 19.64/3.10 % (2494409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494409)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494409)Termination reason: Instruction limit
% 19.64/3.10 % (2494409)Termination phase: Saturation
% 19.64/3.10 % (2494409)Time elapsed: 0.016 s
% 19.64/3.10 % (2494409)Peak memory usage: 12 MB
% 19.64/3.10 % (2494409)Instructions burned: 36 (million)
% 19.64/3.10 % (2494415)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2027958523:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2973 on theBenchmark for (2973ds/647Mi)
% 19.64/3.10 % (2494417)dis+10_128_sil=128000:tgt=full:plsq=on:plsqc=3:cnfonf=off:si=on:sp=arity:spb=goal_then_units:uwa=one_side_interpreted:nwc=1.5:random_seed=3709870438:i=857:add=off:kws=frequency:rtra=on:ntd=on_2973 on theBenchmark for (2973ds/857Mi)
% 19.64/3.10 % (2494406)Instruction limit reached!
% 19.64/3.10 % (2494406)------------------------------
% 19.64/3.10 % (2494406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.10 % (2494406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.10 % (2494406)CaDiCaL version: 2.1.3
% 19.64/3.10 % (2494406)Termination reason: Instruction limit
% 19.64/3.10 % (2494406)Termination phase: Saturation
% 19.64/3.10 % (2494406)Time elapsed: 0.071 s
% 19.64/3.10 % (2494406)Peak memory usage: 13 MB
% 19.64/3.10 % (2494406)Instructions burned: 291 (million)
% 19.64/3.10 % (2494420)dis+1010_4_anc=all_dependent:to=lpo:sil=128000:fde=unused:cnfonf=conj_eager:si=on:sp=reverse_frequency:lma=off:spb=intro:cbe=off:uwa=off:random_seed=406629532:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2973 on theBenchmark for (2973ds/693Mi)
% 19.64/3.10 % (2494407) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2494119-2494407"...
% 19.64/3.10 % (2494407)...printing done.
% 19.64/3.10 % (2494407)Refutation found. Thanks to Tanya!
% 19.64/3.10 % SZS status Theorem for theBenchmark
% 19.64/3.10 % SZS output start Proof for theBenchmark
% See solution above
% 19.64/3.11 % (2494407)------------------------------
% 19.64/3.11 % (2494407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.64/3.11 % (2494407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.64/3.11 % (2494407)CaDiCaL version: 2.1.3
% 19.64/3.11 % (2494407)Termination reason: Refutation
% 19.64/3.11 % (2494407)Time elapsed: 0.232 s
% 19.64/3.11 % (2494407)Peak memory usage: 16 MB
% 19.64/3.11 % (2494407)Instructions burned: 445 (million)
% 19.64/3.11 % (2494119)Success in time 2.842 s
% 19.64/3.11 % Vampire exiting
%------------------------------------------------------------------------------