%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP111^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:23 AM UTC 2026
% Result : Theorem 6.31s 1.22s
% Output : Refutation 6.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 14
% Syntax : Number of formulae : 237 ( 34 unt; 0 typ; 8 def)
% Number of atoms : 1978 ( 297 equ; 0 cnn)
% Maximal formula atoms : 5 ( 8 avg)
% Number of connectives : 3793 ( 370 ~; 398 |; 276 &;2168 @)
% ( 8 <=>; 285 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 66 ( 61 usr; 37 con; 0-4 aty)
% ( 195 !!; 93 ??; 0 @@+; 0 @@-)
% Number of variables : 354 ( 0 sgn 37 !; 9 ?; 354 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
extended_ereal: $tType ).
thf(type_def_6,type,
set_a: $tType ).
thf(type_def_7,type,
a: $tType ).
thf(type_def_8,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
extend1289208545_ereal: extended_ereal ).
thf(func_def_1,type,
extended_MInfty: extended_ereal ).
thf(func_def_2,type,
extended_PInfty: extended_ereal ).
thf(func_def_3,type,
times_1966848393_ereal: extended_ereal > extended_ereal > extended_ereal ).
thf(func_def_4,type,
uminus1208298309_ereal: extended_ereal > extended_ereal ).
thf(func_def_5,type,
zero_z163181189_ereal: extended_ereal ).
thf(func_def_6,type,
lower_191460856_ereal: a > ( a > extended_ereal ) > $o ).
thf(func_def_7,type,
ord_le2001149050_ereal: extended_ereal > extended_ereal > $o ).
thf(func_def_8,type,
divide595620860_ereal: extended_ereal > extended_ereal > extended_ereal ).
thf(func_def_9,type,
collect_a: ( a > $o ) > set_a ).
thf(func_def_10,type,
topolo1276428101open_a: set_a > $o ).
thf(func_def_11,type,
member_a: a > set_a > $o ).
thf(func_def_12,type,
f: a > extended_ereal ).
thf(func_def_13,type,
x0: a ).
thf(func_def_15,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_16,type,
vIMP: $o > $o > $o ).
thf(func_def_17,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_18,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_19,type,
vNOT: $o > $o ).
thf(func_def_20,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_21,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_22,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_25,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_26,type,
vAND: $o > $o > $o ).
thf(func_def_27,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_28,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_29,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_30,type,
vOR: $o > $o > $o ).
thf(func_def_31,type,
sP0: extended_ereal > $o ).
thf(func_def_32,type,
sP1: extended_ereal > $o ).
thf(func_def_34,type,
sK3: extended_ereal ).
thf(func_def_35,type,
sK4: set_a ).
thf(func_def_36,type,
sK5: extended_ereal ).
thf(func_def_37,type,
sK6: extended_ereal > set_a ).
thf(func_def_38,type,
sK7: set_a ).
thf(func_def_39,type,
sK8: set_a ).
thf(func_def_40,type,
sK9: set_a ).
thf(func_def_41,type,
sK10: extended_ereal ).
thf(func_def_42,type,
sK11: a ).
thf(func_def_43,type,
sK12: a ).
thf(func_def_44,type,
sK13: a ).
thf(func_def_45,type,
sK14: a ).
thf(func_def_46,type,
sK15: extended_ereal > extended_ereal ).
thf(func_def_47,type,
sK16: set_a ).
thf(func_def_48,type,
sK17: extended_ereal ).
thf(func_def_49,type,
sK18: a ).
thf(func_def_50,type,
sK19: a ).
thf(func_def_51,type,
sK20: a ).
thf(func_def_52,type,
sK21: set_a ).
thf(func_def_53,type,
sK22: set_a ).
thf(func_def_54,type,
sK23: set_a ).
thf(func_def_55,type,
sK24: a ).
thf(f1,axiom,
( ( ( f @ x0 )
= extend1289208545_ereal )
=> ! [X0: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ( member_a @ x0 @ X1 )
& ( topolo1276428101open_a @ X1 )
& ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__092_060open_062f_Ax0_A_061_A_092_060infinity_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062) ).
thf(f2,axiom,
( ( ( f @ x0 )
= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ! [X0: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ( topolo1276428101open_a @ X1 )
& ( member_a @ x0 @ X1 )
& ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_062f_Ax0_A_061_A_N_A_092_060infinity_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062) ).
thf(f3,axiom,
( ( ( f @ x0 )
!= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ( ( ( f @ x0 )
!= extend1289208545_ereal )
=> ! [X0: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ( member_a @ x0 @ X1 )
& ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) )
& ( topolo1276428101open_a @ X1 ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__092_060open_062_092_060lbrakk_062f_Ax0_A_092_060noteq_062_A_N_A_092_060infinity_062_059_Af_Ax0_A_092_060noteq_062_A_092_060infinity_062_092_060rbrakk_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062) ).
thf(f40,axiom,
( ( uminus1208298309_ereal @ extended_PInfty )
= extended_MInfty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_uminus__ereal_Osimps_I2_J) ).
thf(f50,axiom,
extend1289208545_ereal = extended_PInfty,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_infinity__ereal__def) ).
thf(f121,conjecture,
( ( lower_191460856_ereal @ x0 @ f )
!= ( ~ ! [X0: extended_ereal] :
( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) )
& ( member_a @ x0 @ X1 )
& ( topolo1276428101open_a @ X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(f122,negated_conjecture,
~ ( ( ( lower_191460856_ereal @ x0 @ f )
!= ( ~ ! [X0: extended_ereal] :
( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) )
& ( member_a @ x0 @ X1 )
& ( topolo1276428101open_a @ X1 ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f121]) ).
thf(f149,plain,
( extended_MInfty
= ( uminus1208298309_ereal @ extended_PInfty ) ),
inference(fool_elimination,[],[f40]) ).
thf(f160,plain,
( ( ( f @ x0 )
= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ! [X0: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ( topolo1276428101open_a @ X1 )
& ( member_a @ x0 @ X1 )
& ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ),
inference(rectify,[],[f2]) ).
thf(f161,plain,
( ( ( ( f @ x0 )
= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(fool_elimination,[],[f160]) ).
thf(f163,plain,
( ( ( f @ x0 )
= extend1289208545_ereal )
=> ! [X0: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ( member_a @ x0 @ X1 )
& ( topolo1276428101open_a @ X1 )
& ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ),
inference(rectify,[],[f1]) ).
thf(f164,plain,
( ( ( ( f @ x0 )
= extend1289208545_ereal )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(fool_elimination,[],[f163]) ).
thf(f280,plain,
~ ( ( ( lower_191460856_ereal @ x0 @ f )
!= ( ~ ! [X0: extended_ereal] :
( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) )
& ( member_a @ x0 @ X1 )
& ( topolo1276428101open_a @ X1 ) ) ) ) ) ),
inference(rectify,[],[f122]) ).
thf(f281,plain,
( ( ~ ( ( ( lower_191460856_ereal @ x0 @ f )
!= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f280]) ).
thf(f297,plain,
( ( ( f @ x0 )
!= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ( ( ( f @ x0 )
!= extend1289208545_ereal )
=> ! [X0: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X0 @ ( f @ x0 ) )
=> ? [X1: set_a] :
( ( member_a @ x0 @ X1 )
& ! [X2: a] :
( ( member_a @ X2 @ X1 )
=> ( ord_le2001149050_ereal @ X0 @ ( f @ X2 ) ) )
& ( topolo1276428101open_a @ X1 ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ) ),
inference(rectify,[],[f3]) ).
thf(f298,plain,
( $true
= ( ( ( f @ x0 )
!= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ( ( ( f @ x0 )
!= extend1289208545_ereal )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ) ) ),
inference(fool_elimination,[],[f297]) ).
thf(f303,plain,
extend1289208545_ereal = extended_PInfty,
inference(fool_elimination,[],[f50]) ).
thf(f344,plain,
( ( ( ( f @ x0 )
= extend1289208545_ereal )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(cnf_transformation,[],[f164]) ).
thf(f349,plain,
( $true
= ( ( ( f @ x0 )
!= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ( ( ( f @ x0 )
!= extend1289208545_ereal )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ) ) ),
inference(cnf_transformation,[],[f298]) ).
thf(f353,plain,
( extended_MInfty
= ( uminus1208298309_ereal @ extended_PInfty ) ),
inference(cnf_transformation,[],[f149]) ).
thf(f360,plain,
extend1289208545_ereal = extended_PInfty,
inference(cnf_transformation,[],[f303]) ).
thf(f368,plain,
( ( ( ( f @ x0 )
= ( uminus1208298309_ereal @ extend1289208545_ereal ) )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(cnf_transformation,[],[f161]) ).
thf(f393,plain,
( ( ~ ( ( ( lower_191460856_ereal @ x0 @ f )
!= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f281]) ).
thf(f460,plain,
( ( ( ( f @ x0 )
= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(definition_unfolding,[],[f344,f360]) ).
thf(f463,plain,
( ( ( ( f @ x0 )
!= ( uminus1208298309_ereal @ extended_PInfty ) )
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ) )
= $true ),
inference(definition_unfolding,[],[f349,f360,f360]) ).
thf(f466,plain,
( ( ( ( f @ x0 )
= ( uminus1208298309_ereal @ extended_PInfty ) )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(definition_unfolding,[],[f368,f360]) ).
thf(f496,plain,
( ( ( lower_191460856_ereal @ x0 @ f )
= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) )
= $true ),
inference(boolean_simplification,[],[f393]) ).
thf(f500,plain,
( ( ( ( f @ x0 )
= extended_MInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) )
= $true ),
inference(backward_demodulation,[],[f466,f353]) ).
thf(f501,plain,
( ( ( ( f @ x0 )
!= extended_MInfty )
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= ( lower_191460856_ereal @ x0 @ f ) ) ) )
= $true ),
inference(backward_demodulation,[],[f463,f353]) ).
thf(f748,plain,
( ( lower_191460856_ereal @ x0 @ f )
= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) ),
inference(equality_proxy_clausification,[],[f496]) ).
thf(f752,plain,
( ( $true
= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) )
| ( ( lower_191460856_ereal @ x0 @ f )
= $false ) ),
inference(iff_proxy_clausification,[],[f748]) ).
thf(f754,plain,
( ( ( lower_191460856_ereal @ x0 @ f )
= $false )
| ( ( lower_191460856_ereal @ x0 @ f )
= $true ) ),
inference(forward_demodulation,[],[f752,f748]) ).
thf(f756,definition,
( spl2_3
<=> ( ( lower_191460856_ereal @ x0 @ f )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
thf(f758,plain,
( ( ( lower_191460856_ereal @ x0 @ f )
= $false )
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f756]) ).
thf(f760,definition,
( spl2_4
<=> ( ( lower_191460856_ereal @ x0 @ f )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
thf(f762,plain,
( ( ( lower_191460856_ereal @ x0 @ f )
= $true )
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f760]) ).
thf(f764,plain,
( spl2_3
| spl2_4 ),
inference(avatar_split_clause,[],[f754,f760,f756]) ).
thf(f765,plain,
( ( $false
= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) )
| ~ spl2_3 ),
inference(backward_demodulation,[],[f748,f758]) ).
thf(f766,plain,
( ( $true
= ( ( ( f @ x0 )
= extended_MInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= $false ) ) )
| ~ spl2_3 ),
inference(backward_demodulation,[],[f500,f758]) ).
thf(f767,plain,
( ( ( ( ( f @ x0 )
!= extended_MInfty )
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) ) )
= $true )
| ~ spl2_3 ),
inference(backward_demodulation,[],[f501,f758]) ).
thf(f768,plain,
( ( ( ( ( f @ x0 )
= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) )
= $true )
| ~ spl2_3 ),
inference(backward_demodulation,[],[f460,f758]) ).
thf(f769,plain,
( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) )
= $true )
| ~ spl2_3 ),
inference(not_proxy_clausification,[],[f765]) ).
thf(f772,plain,
( ! [X1: extended_ereal] :
( ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) )
@ X1 )
= $true )
| ~ spl2_3 ),
inference(pi_proxy_clausification,[],[f769]) ).
thf(f773,plain,
( ! [X1: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X1 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ X1 @ ( f @ Y1 ) ) ) ) ) ) )
= $true )
| ~ spl2_3 ),
inference(beta-eta_normalization,[],[f772]) ).
thf(f779,plain,
( ( $true
= ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= $false ) )
| ( $false
= ( ( f @ x0 )
= extended_MInfty ) )
| ~ spl2_3 ),
inference(imp_proxy_clausification,[],[f766]) ).
thf(f781,definition,
( spl2_5
<=> ( $true
= ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
thf(f782,plain,
( ( $true
!= ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= $false ) )
| spl2_5 ),
inference(avatar_component_clause,[],[f781]) ).
thf(f783,plain,
( ( $true
= ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= $false ) )
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f781]) ).
thf(f785,definition,
( spl2_6
<=> ( $false
= ( ( f @ x0 )
= extended_MInfty ) ) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
thf(f787,plain,
( ( $false
= ( ( f @ x0 )
= extended_MInfty ) )
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f785]) ).
thf(f788,plain,
( spl2_5
| spl2_6
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f779,f756,f785,f781]) ).
thf(f791,plain,
( ( $false
= ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) ) )
| ~ spl2_5 ),
inference(equality_proxy_clausification,[],[f783]) ).
thf(f794,plain,
( ( ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) )
@ sK3 )
= $false )
| ~ spl2_5 ),
inference(sigma_proxy_clausification,[],[f791]) ).
thf(f795,plain,
( ( $false
= ( ( ord_le2001149050_ereal @ sK3 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) ) )
| ~ spl2_5 ),
inference(beta-eta_normalization,[],[f794]) ).
thf(f796,plain,
( ( $false
= ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) )
| ~ spl2_5 ),
inference(imp_proxy_clausification,[],[f795]) ).
thf(f797,plain,
( ( $true
= ( ord_le2001149050_ereal @ sK3 @ ( f @ x0 ) ) )
| ~ spl2_5 ),
inference(imp_proxy_clausification,[],[f795]) ).
thf(f800,plain,
( ( ( $true
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) ) ) ) )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(constrained_superposition,[],[f773,f797]) ).
thf(f801,plain,
( ( ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) ) ) )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(boolean_simplification,[],[f800]) ).
thf(f802,plain,
( ! [X1: set_a] :
( $false
= ( ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) )
@ X1 ) )
| ~ spl2_5 ),
inference(pi_proxy_clausification,[],[f796]) ).
thf(f803,plain,
( ! [X1: set_a] :
( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ X1 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ X1 )
& ( topolo1276428101open_a @ X1 ) ) )
| ~ spl2_5 ),
inference(beta-eta_normalization,[],[f802]) ).
thf(f805,plain,
( ( ( ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) ) )
@ sK4 )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(sigma_proxy_clausification,[],[f801]) ).
thf(f806,plain,
( ( ( ( topolo1276428101open_a @ sK4 )
& ( member_a @ x0 @ sK4 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK4 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) ) )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(beta-eta_normalization,[],[f805]) ).
thf(f807,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK4 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(and_proxy_clausification,[],[f806]) ).
thf(f808,plain,
( ( ( ( topolo1276428101open_a @ sK4 )
& ( member_a @ x0 @ sK4 ) )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(and_proxy_clausification,[],[f806]) ).
thf(f811,plain,
( ( $true
= ( member_a @ x0 @ sK4 ) )
| ~ spl2_3
| ~ spl2_5 ),
inference(and_proxy_clausification,[],[f808]) ).
thf(f812,plain,
( ( ( topolo1276428101open_a @ sK4 )
= $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(and_proxy_clausification,[],[f808]) ).
thf(f815,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK4 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK4 )
& $true ) )
| ~ spl2_3
| ~ spl2_5 ),
inference(constrained_superposition,[],[f803,f812]) ).
thf(f816,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK4 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK4 ) )
= $false )
| ~ spl2_3
| ~ spl2_5 ),
inference(boolean_simplification,[],[f815]) ).
thf(f817,plain,
( ( $false
= ( $true
& ( member_a @ x0 @ sK4 ) ) )
| ~ spl2_3
| ~ spl2_5 ),
inference(forward_demodulation,[],[f816,f807]) ).
thf(f818,plain,
( ( $false
= ( member_a @ x0 @ sK4 ) )
| ~ spl2_3
| ~ spl2_5 ),
inference(boolean_simplification,[],[f817]) ).
thf(f819,plain,
( ( $false = $true )
| ~ spl2_3
| ~ spl2_5 ),
inference(backward_demodulation,[],[f811,f818]) ).
thf(f820,plain,
( $false
| ~ spl2_3
| ~ spl2_5 ),
inference(trivial_inequality_removal,[],[f819]) ).
thf(f821,plain,
( ~ spl2_3
| ~ spl2_5 ),
inference(avatar_contradiction_clause,[],[f820]) ).
thf(f823,plain,
( ( ( ~ $false
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) ) )
= $true )
| ~ spl2_3
| ~ spl2_6 ),
inference(backward_demodulation,[],[f767,f787]) ).
thf(f824,plain,
( ( ( $true
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) ) )
= $true )
| ~ spl2_3
| ~ spl2_6 ),
inference(boolean_simplification,[],[f823]) ).
thf(f825,plain,
( ( ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) )
= $true )
| ~ spl2_3
| ~ spl2_6 ),
inference(boolean_simplification,[],[f824]) ).
thf(f828,plain,
( ( $false
!= ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) ) )
| spl2_5 ),
inference(equality_proxy_clausification,[],[f782]) ).
thf(f829,plain,
( ! [X1: extended_ereal] :
( ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) )
@ X1 )
= $true )
| spl2_5 ),
inference(pi_proxy_clausification,[],[f828]) ).
thf(f830,plain,
( ! [X1: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X1 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ X1 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) )
= $true )
| spl2_5 ),
inference(beta-eta_normalization,[],[f829]) ).
thf(f836,plain,
( ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false )
= $true )
| ( $false
= ( ( f @ x0 )
= extended_PInfty ) )
| ~ spl2_3 ),
inference(imp_proxy_clausification,[],[f768]) ).
thf(f838,definition,
( spl2_7
<=> ( $false
= ( ( f @ x0 )
= extended_PInfty ) ) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
thf(f839,plain,
( ( $false
!= ( ( f @ x0 )
= extended_PInfty ) )
| spl2_7 ),
inference(avatar_component_clause,[],[f838]) ).
thf(f840,plain,
( ( $false
= ( ( f @ x0 )
= extended_PInfty ) )
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f838]) ).
thf(f842,definition,
( spl2_8
<=> ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
thf(f844,plain,
( ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false )
= $true )
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f842]) ).
thf(f845,plain,
( spl2_7
| spl2_8
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f836,f756,f842,f838]) ).
thf(f846,plain,
( ( ( ~ $false
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) )
= $true )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(backward_demodulation,[],[f825,f840]) ).
thf(f849,plain,
( ( $true
= ( $true
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(boolean_simplification,[],[f846]) ).
thf(f850,plain,
( ( $true
= ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $false ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(boolean_simplification,[],[f849]) ).
thf(f852,plain,
( ( $false
= ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(equality_proxy_clausification,[],[f850]) ).
thf(f855,plain,
( ( $false
= ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) )
@ sK5 ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(sigma_proxy_clausification,[],[f852]) ).
thf(f856,plain,
( ( ( ( ord_le2001149050_ereal @ sK5 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) ) ) )
= $false )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(beta-eta_normalization,[],[f855]) ).
thf(f857,plain,
( ( $false
= ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) ) ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(imp_proxy_clausification,[],[f856]) ).
thf(f858,plain,
( ( ( ord_le2001149050_ereal @ sK5 @ ( f @ x0 ) )
= $true )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(imp_proxy_clausification,[],[f856]) ).
thf(f863,plain,
( ( ( $true
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) )
= $true )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(constrained_superposition,[],[f830,f858]) ).
thf(f865,plain,
( ( $true
= ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(boolean_simplification,[],[f863]) ).
thf(f867,plain,
( ! [X1: set_a] :
( $false
= ( ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) )
@ X1 ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(pi_proxy_clausification,[],[f857]) ).
thf(f868,plain,
( ! [X1: set_a] :
( $false
= ( ( topolo1276428101open_a @ X1 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ X1 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ X1 ) ) )
| ~ spl2_3
| ~ spl2_6
| ~ spl2_7 ),
inference(beta-eta_normalization,[],[f867]) ).
thf(f872,plain,
( ( ( ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) )
@ sK7 )
= $true )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(sigma_proxy_clausification,[],[f865]) ).
thf(f873,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK7 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK7 )
& ( topolo1276428101open_a @ sK7 ) )
= $true )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(beta-eta_normalization,[],[f872]) ).
thf(f874,plain,
( ( $true
= ( topolo1276428101open_a @ sK7 ) )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(and_proxy_clausification,[],[f873]) ).
thf(f875,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK7 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK7 ) )
= $true )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(and_proxy_clausification,[],[f873]) ).
thf(f878,plain,
( ( ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK7 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK7 ) )
= $false )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(constrained_superposition,[],[f868,f874]) ).
thf(f879,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK7 )
=> ( ord_le2001149050_ereal @ sK5 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK7 ) ) )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(boolean_simplification,[],[f878]) ).
thf(f880,plain,
( ( $false = $true )
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(backward_demodulation,[],[f875,f879]) ).
thf(f881,plain,
( $false
| ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(trivial_inequality_removal,[],[f880]) ).
thf(f882,plain,
( ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(avatar_contradiction_clause,[],[f881]) ).
thf(f885,plain,
( ( ( f @ x0 )
= extended_PInfty )
| spl2_7 ),
inference(equality_proxy_clausification,[],[f839]) ).
thf(f886,plain,
( ! [X1: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X1 @ extended_PInfty )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ X1 @ ( f @ Y1 ) ) ) ) ) ) )
= $true )
| ~ spl2_3
| spl2_7 ),
inference(backward_demodulation,[],[f773,f885]) ).
thf(f1005,plain,
( ( $false
= ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) ) )
| ~ spl2_8 ),
inference(equality_proxy_clausification,[],[f844]) ).
thf(f1008,plain,
( ( $false
= ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) )
@ sK10 ) )
| ~ spl2_8 ),
inference(sigma_proxy_clausification,[],[f1005]) ).
thf(f1009,plain,
( ( ( ( ord_le2001149050_ereal @ sK10 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) ) )
= $false )
| ~ spl2_8 ),
inference(beta-eta_normalization,[],[f1008]) ).
thf(f1010,plain,
( ( ( ( ord_le2001149050_ereal @ sK10 @ extended_PInfty )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) ) )
= $false )
| spl2_7
| ~ spl2_8 ),
inference(forward_demodulation,[],[f1009,f885]) ).
thf(f1011,plain,
( ( ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) )
= $false )
| spl2_7
| ~ spl2_8 ),
inference(imp_proxy_clausification,[],[f1010]) ).
thf(f1012,plain,
( ( ( ord_le2001149050_ereal @ sK10 @ extended_PInfty )
= $true )
| spl2_7
| ~ spl2_8 ),
inference(imp_proxy_clausification,[],[f1010]) ).
thf(f1020,plain,
( ( ( $true
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) ) ) ) )
= $true )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(constrained_superposition,[],[f886,f1012]) ).
thf(f1021,plain,
( ( $true
= ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) ) ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(boolean_simplification,[],[f1020]) ).
thf(f1023,plain,
( ! [X1: set_a] :
( ( ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) )
@ X1 )
= $false )
| spl2_7
| ~ spl2_8 ),
inference(pi_proxy_clausification,[],[f1011]) ).
thf(f1024,plain,
( ! [X1: set_a] :
( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ X1 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ X1 )
& ( member_a @ x0 @ X1 ) )
= $false )
| spl2_7
| ~ spl2_8 ),
inference(beta-eta_normalization,[],[f1023]) ).
thf(f1110,plain,
( ( ( ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) ) )
@ ( sK6 @ sK10 ) )
= $true )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(sigma_proxy_clausification,[],[f1021]) ).
thf(f1111,plain,
( ( $true
= ( ( topolo1276428101open_a @ ( sK6 @ sK10 ) )
& ( member_a @ x0 @ ( sK6 @ sK10 ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ ( sK6 @ sK10 ) )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(beta-eta_normalization,[],[f1110]) ).
thf(f1117,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ ( sK6 @ sK10 ) )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(and_proxy_clausification,[],[f1111]) ).
thf(f1118,plain,
( ( ( ( topolo1276428101open_a @ ( sK6 @ sK10 ) )
& ( member_a @ x0 @ ( sK6 @ sK10 ) ) )
= $true )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(and_proxy_clausification,[],[f1111]) ).
thf(f1121,plain,
( ( ( member_a @ x0 @ ( sK6 @ sK10 ) )
= $true )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(and_proxy_clausification,[],[f1118]) ).
thf(f1122,plain,
( ( $true
= ( topolo1276428101open_a @ ( sK6 @ sK10 ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(and_proxy_clausification,[],[f1118]) ).
thf(f1125,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ ( sK6 @ sK10 ) )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& $true
& ( member_a @ x0 @ ( sK6 @ sK10 ) ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(constrained_superposition,[],[f1024,f1122]) ).
thf(f1126,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ ( sK6 @ sK10 ) )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ ( sK6 @ sK10 ) ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(boolean_simplification,[],[f1125]) ).
thf(f1127,plain,
( ( ( $true
& ( member_a @ x0 @ ( sK6 @ sK10 ) ) )
= $false )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(forward_demodulation,[],[f1126,f1117]) ).
thf(f1128,plain,
( ( $false
= ( member_a @ x0 @ ( sK6 @ sK10 ) ) )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(boolean_simplification,[],[f1127]) ).
thf(f1129,plain,
( ( $false = $true )
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(backward_demodulation,[],[f1121,f1128]) ).
thf(f1130,plain,
( $false
| ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(trivial_inequality_removal,[],[f1129]) ).
thf(f1131,plain,
( ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(avatar_contradiction_clause,[],[f1130]) ).
thf(f1132,plain,
( ( $true
= ( ~ ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) ) )
| ~ spl2_4 ),
inference(forward_demodulation,[],[f748,f762]) ).
thf(f1196,plain,
( ( $false
= ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) ) ) )
| ~ spl2_4 ),
inference(not_proxy_clausification,[],[f1132]) ).
thf(f1199,plain,
( ( $false
= ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) ) ) ) )
@ sK17 ) )
| ~ spl2_4 ),
inference(sigma_proxy_clausification,[],[f1196]) ).
thf(f1200,plain,
( ( $false
= ( ( ord_le2001149050_ereal @ sK17 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y1 ) ) ) ) ) ) ) )
| ~ spl2_4 ),
inference(beta-eta_normalization,[],[f1199]) ).
thf(f1296,plain,
( ( ( ( ( f @ x0 )
= extended_MInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 )
& ( topolo1276428101open_a @ Y1 ) ) ) ) )
= $true ) )
= $true )
| ~ spl2_4 ),
inference(forward_demodulation,[],[f500,f762]) ).
thf(f1309,plain,
( ( $false
= ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y1 ) ) ) ) ) ) )
| ~ spl2_4 ),
inference(imp_proxy_clausification,[],[f1200]) ).
thf(f1310,plain,
( ( ( ord_le2001149050_ereal @ sK17 @ ( f @ x0 ) )
= $true )
| ~ spl2_4 ),
inference(imp_proxy_clausification,[],[f1200]) ).
thf(f1313,plain,
( ( ( $true
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) )
= $true )
| ~ spl2_4
| spl2_5 ),
inference(constrained_superposition,[],[f830,f1310]) ).
thf(f1314,plain,
( ( $true
= ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) ) ) )
| ~ spl2_4
| spl2_5 ),
inference(boolean_simplification,[],[f1313]) ).
thf(f1315,plain,
( ! [X1: set_a] :
( $false
= ( ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y1 ) ) ) ) )
@ X1 ) )
| ~ spl2_4 ),
inference(pi_proxy_clausification,[],[f1309]) ).
thf(f1316,plain,
( ! [X1: set_a] :
( $false
= ( ( topolo1276428101open_a @ X1 )
& ( member_a @ x0 @ X1 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ X1 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) ) ) )
| ~ spl2_4 ),
inference(beta-eta_normalization,[],[f1315]) ).
thf(f1318,plain,
( ( ( ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 )
& ( topolo1276428101open_a @ Y0 ) )
@ sK21 )
= $true )
| ~ spl2_4
| spl2_5 ),
inference(sigma_proxy_clausification,[],[f1314]) ).
thf(f1319,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK21 )
& ( topolo1276428101open_a @ sK21 ) )
= $true )
| ~ spl2_4
| spl2_5 ),
inference(beta-eta_normalization,[],[f1318]) ).
thf(f1320,plain,
( ( ( topolo1276428101open_a @ sK21 )
= $true )
| ~ spl2_4
| spl2_5 ),
inference(and_proxy_clausification,[],[f1319]) ).
thf(f1321,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK21 ) )
= $true )
| ~ spl2_4
| spl2_5 ),
inference(and_proxy_clausification,[],[f1319]) ).
thf(f1324,plain,
( ( ( $true
& ( member_a @ x0 @ sK21 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) ) )
= $false )
| ~ spl2_4
| spl2_5 ),
inference(constrained_superposition,[],[f1316,f1320]) ).
thf(f1325,plain,
( ( ( ( member_a @ x0 @ sK21 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) ) )
= $false )
| ~ spl2_4
| spl2_5 ),
inference(boolean_simplification,[],[f1324]) ).
thf(f1326,plain,
( ( $true
= ( member_a @ x0 @ sK21 ) )
| ~ spl2_4
| spl2_5 ),
inference(and_proxy_clausification,[],[f1321]) ).
thf(f1327,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) ) )
| ~ spl2_4
| spl2_5 ),
inference(and_proxy_clausification,[],[f1321]) ).
thf(f1328,plain,
( ( $false
= ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) ) ) )
| ~ spl2_4
| spl2_5 ),
inference(backward_demodulation,[],[f1325,f1326]) ).
thf(f1331,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK21 )
=> ( ord_le2001149050_ereal @ sK17 @ ( f @ Y0 ) ) ) ) )
| ~ spl2_4
| spl2_5 ),
inference(boolean_simplification,[],[f1328]) ).
thf(f1332,plain,
( ( $false = $true )
| ~ spl2_4
| spl2_5 ),
inference(backward_demodulation,[],[f1327,f1331]) ).
thf(f1333,plain,
( $false
| ~ spl2_4
| spl2_5 ),
inference(trivial_inequality_removal,[],[f1332]) ).
thf(f1334,plain,
( ~ spl2_4
| spl2_5 ),
inference(avatar_contradiction_clause,[],[f1333]) ).
thf(f1339,plain,
( ( ( ( ( f @ x0 )
= extended_MInfty )
=> ( $false = $true ) )
= $true )
| ~ spl2_4
| ~ spl2_5 ),
inference(backward_demodulation,[],[f1296,f791]) ).
thf(f1340,plain,
( ( ( ( ( f @ x0 )
= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) )
= $true )
| ~ spl2_4 ),
inference(forward_demodulation,[],[f460,f762]) ).
thf(f1343,plain,
( ( ( ( ( f @ x0 )
!= extended_MInfty )
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) ) )
= $true )
| ~ spl2_4 ),
inference(forward_demodulation,[],[f501,f762]) ).
thf(f1348,plain,
( ( ( $false = $true )
= $true )
| ( $false
= ( ( f @ x0 )
= extended_MInfty ) )
| ~ spl2_4
| ~ spl2_5 ),
inference(imp_proxy_clausification,[],[f1339]) ).
thf(f1350,definition,
( spl2_9
<=> ( ( $false = $true )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
thf(f1352,plain,
( ( ( $false = $true )
= $true )
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f1350]) ).
thf(f1353,plain,
( spl2_9
| spl2_6
| ~ spl2_4
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1348,f781,f760,f785,f1350]) ).
thf(f1356,plain,
( ( $false = $true )
| ~ spl2_9 ),
inference(equality_proxy_clausification,[],[f1352]) ).
thf(f1357,plain,
( $false
| ~ spl2_9 ),
inference(trivial_inequality_removal,[],[f1356]) ).
thf(f1358,plain,
~ spl2_9,
inference(avatar_contradiction_clause,[],[f1357]) ).
thf(f1359,plain,
( ( $true
= ( ~ $false
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) ) ) )
| ~ spl2_4
| ~ spl2_6 ),
inference(backward_demodulation,[],[f1343,f787]) ).
thf(f1360,plain,
( ( ( $true
=> ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6 ),
inference(boolean_simplification,[],[f1359]) ).
thf(f1361,plain,
( ( ( ( ( f @ x0 )
!= extended_PInfty )
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) )
= $true )
| ~ spl2_4
| ~ spl2_6 ),
inference(boolean_simplification,[],[f1360]) ).
thf(f1374,plain,
( ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true )
= $true )
| ( $false
= ( ( f @ x0 )
= extended_PInfty ) )
| ~ spl2_4 ),
inference(imp_proxy_clausification,[],[f1340]) ).
thf(f1376,definition,
( spl2_10
<=> ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
thf(f1377,plain,
( ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true )
!= $true )
| spl2_10 ),
inference(avatar_component_clause,[],[f1376]) ).
thf(f1378,plain,
( ( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true )
= $true )
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f1376]) ).
thf(f1379,plain,
( spl2_7
| spl2_10
| ~ spl2_4 ),
inference(avatar_split_clause,[],[f1374,f760,f1376,f838]) ).
thf(f1382,plain,
( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true )
| ~ spl2_10 ),
inference(equality_proxy_clausification,[],[f1378]) ).
thf(f1385,plain,
( ! [X1: extended_ereal] :
( ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) )
@ X1 )
= $true )
| ~ spl2_10 ),
inference(pi_proxy_clausification,[],[f1382]) ).
thf(f1386,plain,
( ! [X1: extended_ereal] :
( $true
= ( ( ord_le2001149050_ereal @ X1 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ X1 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) ) ) )
| ~ spl2_10 ),
inference(beta-eta_normalization,[],[f1385]) ).
thf(f1389,plain,
( ( ( $true
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) ) )
= $true )
| ~ spl2_5
| ~ spl2_10 ),
inference(constrained_superposition,[],[f1386,f797]) ).
thf(f1394,plain,
( ( ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) )
= $true )
| ~ spl2_5
| ~ spl2_10 ),
inference(boolean_simplification,[],[f1389]) ).
thf(f1396,plain,
( ( ( ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) )
@ sK22 )
= $true )
| ~ spl2_5
| ~ spl2_10 ),
inference(sigma_proxy_clausification,[],[f1394]) ).
thf(f1397,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK22 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ sK22 )
& ( member_a @ x0 @ sK22 ) )
= $true )
| ~ spl2_5
| ~ spl2_10 ),
inference(beta-eta_normalization,[],[f1396]) ).
thf(f1398,plain,
( ( ( member_a @ x0 @ sK22 )
= $true )
| ~ spl2_5
| ~ spl2_10 ),
inference(and_proxy_clausification,[],[f1397]) ).
thf(f1399,plain,
( ( $true
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK22 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ sK22 ) ) )
| ~ spl2_5
| ~ spl2_10 ),
inference(and_proxy_clausification,[],[f1397]) ).
thf(f1402,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK22 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& $true
& ( topolo1276428101open_a @ sK22 ) )
= $false )
| ~ spl2_5
| ~ spl2_10 ),
inference(constrained_superposition,[],[f803,f1398]) ).
thf(f1406,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK22 )
=> ( ord_le2001149050_ereal @ sK3 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ sK22 ) ) )
| ~ spl2_5
| ~ spl2_10 ),
inference(boolean_simplification,[],[f1402]) ).
thf(f1408,plain,
( ( $false = $true )
| ~ spl2_5
| ~ spl2_10 ),
inference(backward_demodulation,[],[f1399,f1406]) ).
thf(f1409,plain,
( $false
| ~ spl2_5
| ~ spl2_10 ),
inference(trivial_inequality_removal,[],[f1408]) ).
thf(f1410,plain,
( ~ spl2_5
| ~ spl2_10 ),
inference(avatar_contradiction_clause,[],[f1409]) ).
thf(f1420,plain,
( ( ( ~ $false
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7 ),
inference(backward_demodulation,[],[f1361,f840]) ).
thf(f1421,plain,
( ( $true
= ( $true
=> ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7 ),
inference(boolean_simplification,[],[f1420]) ).
thf(f1422,plain,
( ( $true
= ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7 ),
inference(boolean_simplification,[],[f1421]) ).
thf(f1426,plain,
( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) ) )
!= $true )
| spl2_10 ),
inference(equality_proxy_clausification,[],[f1377]) ).
thf(f1427,plain,
( ( $false
= ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( topolo1276428101open_a @ Y1 )
& ( member_a @ x0 @ Y1 ) ) ) )
@ sK10 ) )
| spl2_10 ),
inference(sigma_proxy_clausification,[],[f1426]) ).
thf(f1428,plain,
( ( ( ( ord_le2001149050_ereal @ sK10 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) ) )
= $false )
| spl2_10 ),
inference(beta-eta_normalization,[],[f1427]) ).
thf(f1429,plain,
( ( ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) ) )
= $false )
| spl2_10 ),
inference(imp_proxy_clausification,[],[f1428]) ).
thf(f1430,plain,
( ( ( ord_le2001149050_ereal @ sK10 @ ( f @ x0 ) )
= $true )
| spl2_10 ),
inference(imp_proxy_clausification,[],[f1428]) ).
thf(f1435,plain,
( ! [X1: set_a] :
( ( ^ [Y0: set_a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( topolo1276428101open_a @ Y0 )
& ( member_a @ x0 @ Y0 ) )
@ X1 )
= $false )
| spl2_10 ),
inference(pi_proxy_clausification,[],[f1429]) ).
thf(f1436,plain,
( ! [X1: set_a] :
( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ X1 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ X1 )
& ( member_a @ x0 @ X1 ) )
= $false )
| spl2_10 ),
inference(beta-eta_normalization,[],[f1435]) ).
thf(f1438,plain,
( ( ( !! @ extended_ereal
@ ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7 ),
inference(equality_proxy_clausification,[],[f1422]) ).
thf(f1441,plain,
( ! [X1: extended_ereal] :
( ( ^ [Y0: extended_ereal] :
( ( ord_le2001149050_ereal @ Y0 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y1: set_a] :
( ( topolo1276428101open_a @ Y1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y1 )
=> ( ord_le2001149050_ereal @ Y0 @ ( f @ Y2 ) ) ) )
& ( member_a @ x0 @ Y1 ) ) ) )
@ X1 )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7 ),
inference(pi_proxy_clausification,[],[f1438]) ).
thf(f1442,plain,
( ! [X1: extended_ereal] :
( ( ( ord_le2001149050_ereal @ X1 @ ( f @ x0 ) )
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ X1 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7 ),
inference(beta-eta_normalization,[],[f1441]) ).
thf(f1446,plain,
( ( ( $true
=> ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(constrained_superposition,[],[f1442,f1430]) ).
thf(f1450,plain,
( ( ( ?? @ set_a
@ ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(boolean_simplification,[],[f1446]) ).
thf(f1454,plain,
( ( $true
= ( ^ [Y0: set_a] :
( ( topolo1276428101open_a @ Y0 )
& ( !! @ a
@ ^ [Y1: a] :
( ( member_a @ Y1 @ Y0 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y1 ) ) ) )
& ( member_a @ x0 @ Y0 ) )
@ sK23 ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(sigma_proxy_clausification,[],[f1450]) ).
thf(f1455,plain,
( ( ( ( topolo1276428101open_a @ sK23 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& ( member_a @ x0 @ sK23 ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(beta-eta_normalization,[],[f1454]) ).
thf(f1456,plain,
( ( $true
= ( member_a @ x0 @ sK23 ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(and_proxy_clausification,[],[f1455]) ).
thf(f1457,plain,
( ( ( ( topolo1276428101open_a @ sK23 )
& ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(and_proxy_clausification,[],[f1455]) ).
thf(f1460,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ sK23 )
& $true ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(constrained_superposition,[],[f1436,f1456]) ).
thf(f1464,plain,
( ( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& ( topolo1276428101open_a @ sK23 ) ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(boolean_simplification,[],[f1460]) ).
thf(f1487,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(and_proxy_clausification,[],[f1457]) ).
thf(f1488,plain,
( ( ( topolo1276428101open_a @ sK23 )
= $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(and_proxy_clausification,[],[f1457]) ).
thf(f1490,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) )
& $true )
= $false )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(backward_demodulation,[],[f1464,f1488]) ).
thf(f1493,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ sK23 )
=> ( ord_le2001149050_ereal @ sK10 @ ( f @ Y0 ) ) ) ) )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(boolean_simplification,[],[f1490]) ).
thf(f1495,plain,
( ( $false = $true )
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(backward_demodulation,[],[f1487,f1493]) ).
thf(f1496,plain,
( $false
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(trivial_inequality_removal,[],[f1495]) ).
thf(f1497,plain,
( ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(avatar_contradiction_clause,[],[f1496]) ).
cnf(s4,plain,
( spl2_3
| spl2_4 ),
inference(sat_conversion,[],[f764]) ).
cnf(s5,plain,
( ~ spl2_3
| spl2_5
| spl2_6 ),
inference(sat_conversion,[],[f788]) ).
cnf(s6,plain,
( ~ spl2_3
| ~ spl2_5 ),
inference(sat_conversion,[],[f821]) ).
cnf(s7,plain,
( ~ spl2_3
| spl2_7
| spl2_8 ),
inference(sat_conversion,[],[f845]) ).
cnf(s8,plain,
( ~ spl2_3
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(sat_conversion,[],[f882]) ).
cnf(s9,plain,
( ~ spl2_3
| spl2_7
| ~ spl2_8 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s13,plain,
( ~ spl2_4
| spl2_5 ),
inference(sat_conversion,[],[f1334]) ).
cnf(s14,plain,
( ~ spl2_4
| ~ spl2_5
| spl2_6
| spl2_9 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s15,plain,
~ spl2_9,
inference(sat_conversion,[],[f1358]) ).
cnf(s16,plain,
( ~ spl2_4
| spl2_7
| spl2_10 ),
inference(sat_conversion,[],[f1379]) ).
cnf(s17,plain,
( ~ spl2_5
| ~ spl2_10 ),
inference(sat_conversion,[],[f1410]) ).
cnf(s20,plain,
( ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| spl2_10 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s21,plain,
( ~ spl2_4
| ~ spl2_5
| spl2_6 ),
inference(rat,[],[s14,s15]) ).
cnf(s23,plain,
~ spl2_4,
inference(rat,[],[s20,s16,s21,s17,s13]) ).
cnf(s24,plain,
spl2_3,
inference(rat,[],[s4,s23]) ).
cnf(s25,plain,
~ spl2_5,
inference(rat,[],[s6,s24]) ).
cnf(s26,plain,
spl2_6,
inference(rat,[],[s5,s24,s25]) ).
cnf(s27,plain,
~ spl2_7,
inference(rat,[],[s8,s25,s24,s26]) ).
cnf(s28,plain,
~ spl2_8,
inference(rat,[],[s9,s24,s27]) ).
cnf(s29,plain,
$false,
inference(rat,[],[s7,s24,s28,s27]) ).
thf(f1498,plain,
$false,
inference(avatar_sat_refutation,[],[s29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP111^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n014.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % 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 19:55:00 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.87/0.37 % (3129940)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.87/0.37 % (3129949)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4025369788:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.87/0.37 % (3129951)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.87/0.37 % (3129951)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.87/0.37 % (3129949)Instruction limit reached!
% 0.87/0.37 % (3129949)------------------------------
% 0.87/0.37 % (3129949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.37 % (3129949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.37 % (3129949)CaDiCaL version: 2.1.3
% 0.87/0.37 % (3129949)Termination reason: Instruction limit
% 0.87/0.37 % (3129949)Termination phase: Property scanning
% 0.87/0.37 % (3129949)Time elapsed: 0.006 s
% 0.87/0.37 % (3129949)Peak memory usage: 11 MB
% 0.87/0.37 % (3129949)Instructions burned: 26 (million)
% 0.87/0.37 % (3129945)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3183887261:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.87/0.37 % (3129946)lrs+10_16_si=on:nwc=1.5:random_seed=4220248368:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.87/0.37 % (3129947)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=409282191:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.87/0.37 % (3129948)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=1758667548: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.87/0.37 % (3129951)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=4004780922:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.87/0.37 % (3129947)Instruction limit reached!
% 0.87/0.37 % (3129947)------------------------------
% 0.87/0.37 % (3129947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.37 % (3129947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.37 % (3129947)CaDiCaL version: 2.1.3
% 0.87/0.37 % (3129947)Termination reason: Instruction limit
% 0.87/0.37 % (3129947)Termination phase: shuffling
% 0.87/0.37 % (3129947)Time elapsed: 0.002 s
% 0.87/0.37 % (3129947)Peak memory usage: 10 MB
% 0.87/0.37 % (3129947)Instructions burned: 3 (million)
% 0.87/0.37 % (3129946)Instruction limit reached!
% 0.87/0.37 % (3129946)------------------------------
% 0.87/0.37 % (3129946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.37 % (3129946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.37 % (3129946)CaDiCaL version: 2.1.3
% 0.87/0.37 % (3129946)Termination reason: Instruction limit
% 0.87/0.37 % (3129946)Termination phase: Property scanning
% 0.87/0.37 % (3129946)Time elapsed: 0.009 s
% 0.87/0.37 % (3129946)Peak memory usage: 10 MB
% 0.87/0.37 % (3129946)Instructions burned: 20 (million)
% 0.87/0.37 % (3129955)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1196298155:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.87/0.37 % (3129955)Instruction limit reached!
% 0.87/0.37 % (3129955)------------------------------
% 0.87/0.37 % (3129955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.37 % (3129955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.37 % (3129955)CaDiCaL version: 2.1.3
% 0.87/0.37 % (3129955)Termination reason: Instruction limit
% 0.87/0.37 % (3129955)Termination phase: shuffling
% 0.87/0.37 % (3129955)Time elapsed: 0.001 s
% 0.87/0.37 % (3129955)Peak memory usage: 10 MB
% 0.87/0.37 % (3129955)Instructions burned: 4 (million)
% 0.87/0.37 % (3129950)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2555396141:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.87/0.37 % (3129959)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4162263237:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.87/0.40 % (3129959)Instruction limit reached!
% 0.87/0.40 % (3129959)------------------------------
% 0.87/0.40 % (3129959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (3129960)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.87/0.40 % (3129959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (3129959)CaDiCaL version: 2.1.3
% 0.87/0.40 % (3129959)Termination reason: Instruction limit
% 0.87/0.40 % (3129959)Termination phase: Property scanning
% 0.87/0.40 % (3129959)Time elapsed: 0.003 s
% 0.87/0.40 % (3129959)Peak memory usage: 10 MB
% 0.87/0.40 % (3129959)Instructions burned: 6 (million)
% 0.87/0.40 % (3129960)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2533647235:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.87/0.40 % (3129962)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3933287814:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.87/0.40 % (3129960)Instruction limit reached!
% 0.87/0.40 % (3129960)------------------------------
% 0.87/0.40 % (3129960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (3129960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (3129960)CaDiCaL version: 2.1.3
% 0.87/0.40 % (3129960)Termination reason: Instruction limit
% 0.87/0.40 % (3129960)Termination phase: shuffling
% 0.87/0.40 % (3129960)Time elapsed: 0.004 s
% 0.87/0.40 % (3129960)Peak memory usage: 10 MB
% 0.87/0.40 % (3129960)Instructions burned: 9 (million)
% 0.87/0.40 % (3129962)Instruction limit reached!
% 0.87/0.40 % (3129962)------------------------------
% 0.87/0.40 % (3129962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (3129962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (3129962)CaDiCaL version: 2.1.3
% 0.87/0.40 % (3129962)Termination reason: Instruction limit
% 0.87/0.40 % (3129962)Termination phase: Preprocessing 1
% 0.87/0.40 % (3129962)Time elapsed: 0.006 s
% 0.87/0.40 % (3129962)Peak memory usage: 10 MB
% 0.87/0.40 % (3129962)Instructions burned: 13 (million)
% 0.87/0.40 % (3129965)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.87/0.40 % (3129965)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.87/0.40 % (3129945)Instruction limit reached!
% 0.87/0.40 % (3129945)------------------------------
% 0.87/0.40 % (3129945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (3129945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (3129945)CaDiCaL version: 2.1.3
% 0.87/0.40 % (3129945)Termination reason: Instruction limit
% 0.87/0.40 % (3129945)Termination phase: Saturation
% 0.87/0.40 % (3129945)Time elapsed: 0.042 s
% 0.87/0.40 % (3129945)Peak memory usage: 13 MB
% 0.87/0.40 % (3129945)Instructions burned: 87 (million)
% 0.87/0.40 % (3129965)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1193637222: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.87/0.40 % (3129968)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=4116683657:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.87/0.40 % (3129969)lrs+10_1_si=on:cs=on:random_seed=1992538938:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.87/0.40 % (3129965)Instruction limit reached!
% 0.87/0.40 % (3129965)------------------------------
% 0.87/0.40 % (3129965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (3129965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (3129965)CaDiCaL version: 2.1.3
% 0.87/0.40 % (3129965)Termination reason: Instruction limit
% 0.87/0.40 % (3129965)Termination phase: Property scanning
% 0.87/0.40 % (3129965)Time elapsed: 0.012 s
% 0.87/0.40 % (3129965)Peak memory usage: 10 MB
% 0.87/0.40 % (3129965)Instructions burned: 29 (million)
% 0.87/0.44 % (3129969)Instruction limit reached!
% 0.87/0.44 % (3129969)------------------------------
% 0.87/0.44 % (3129969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (3129969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (3129969)CaDiCaL version: 2.1.3
% 0.87/0.44 % (3129969)Termination reason: Instruction limit
% 0.87/0.44 % (3129969)Termination phase: Property scanning
% 0.87/0.44 % (3129969)Time elapsed: 0.002 s
% 0.87/0.44 % (3129969)Peak memory usage: 10 MB
% 0.87/0.44 % (3129969)Instructions burned: 8 (million)
% 0.87/0.44 % (3129970)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.87/0.44 % (3129970)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=1139630067:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.87/0.44 % (3129970)Instruction limit reached!
% 0.87/0.44 % (3129970)------------------------------
% 0.87/0.44 % (3129970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (3129970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (3129970)CaDiCaL version: 2.1.3
% 0.87/0.44 % (3129970)Termination reason: Instruction limit
% 0.87/0.44 % (3129970)Termination phase: shuffling
% 0.87/0.44 % (3129970)Time elapsed: 0.002 s
% 0.87/0.44 % (3129970)Peak memory usage: 10 MB
% 0.87/0.44 % (3129970)Instructions burned: 3 (million)
% 0.87/0.44 % (3129974)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=959280038:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.87/0.44 % (3129975)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1952328863:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.87/0.44 % (3129951)Instruction limit reached!
% 0.87/0.44 % (3129951)------------------------------
% 0.87/0.44 % (3129951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (3129951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (3129951)CaDiCaL version: 2.1.3
% 0.87/0.44 % (3129951)Termination reason: Instruction limit
% 0.87/0.44 % (3129951)Termination phase: Saturation
% 0.87/0.44 % (3129951)Time elapsed: 0.076 s
% 0.87/0.44 % (3129951)Peak memory usage: 13 MB
% 0.87/0.44 % (3129951)Instructions burned: 157 (million)
% 0.87/0.44 % (3129950)Instruction limit reached!
% 0.87/0.44 % (3129950)------------------------------
% 0.87/0.44 % (3129950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (3129950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (3129950)CaDiCaL version: 2.1.3
% 0.87/0.44 % (3129950)Termination reason: Instruction limit
% 0.87/0.44 % (3129950)Termination phase: Saturation
% 0.87/0.44 % (3129950)Time elapsed: 0.065 s
% 0.87/0.44 % (3129950)Peak memory usage: 13 MB
% 0.87/0.44 % (3129950)Instructions burned: 75 (million)
% 0.87/0.44 % (3129974)Instruction limit reached!
% 0.87/0.44 % (3129974)------------------------------
% 0.87/0.44 % (3129974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (3129974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (3129974)CaDiCaL version: 2.1.3
% 0.87/0.44 % (3129974)Termination reason: Instruction limit
% 0.87/0.44 % (3129974)Termination phase: Saturation
% 0.87/0.44 % (3129974)Time elapsed: 0.010 s
% 0.87/0.44 % (3129974)Peak memory usage: 12 MB
% 0.87/0.44 % (3129974)Instructions burned: 38 (million)
% 0.87/0.44 % (3129977)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1784231207:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.87/0.44 % (3129982)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=205905509:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.87/0.44 % (3129968)Instruction limit reached!
% 0.87/0.44 % (3129968)------------------------------
% 0.87/0.44 % (3129968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (3129968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (3129968)CaDiCaL version: 2.1.3
% 0.87/0.44 % (3129968)Termination reason: Instruction limit
% 0.87/0.44 % (3129968)Termination phase: Saturation
% 1.59/0.51 % (3129968)Time elapsed: 0.042 s
% 1.59/0.51 % (3129968)Peak memory usage: 13 MB
% 1.59/0.51 % (3129968)Instructions burned: 87 (million)
% 1.59/0.51 % (3129977)Instruction limit reached!
% 1.59/0.51 % (3129977)------------------------------
% 1.59/0.51 % (3129977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.51 % (3129977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.51 % (3129977)CaDiCaL version: 2.1.3
% 1.59/0.51 % (3129980)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3792510226:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.59/0.51 % (3129977)Termination reason: Instruction limit
% 1.59/0.51 % (3129977)Termination phase: Property scanning
% 1.59/0.51 % (3129977)Time elapsed: 0.012 s
% 1.59/0.51 % (3129977)Peak memory usage: 11 MB
% 1.59/0.51 % (3129977)Instructions burned: 27 (million)
% 1.59/0.51 % (3129981)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=880643715:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.59/0.51 % (3129982)Instruction limit reached!
% 1.59/0.51 % (3129982)------------------------------
% 1.59/0.51 % (3129982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.51 % (3129982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.51 % (3129982)CaDiCaL version: 2.1.3
% 1.59/0.51 % (3129982)Termination reason: Instruction limit
% 1.59/0.51 % (3129982)Termination phase: Property scanning
% 1.59/0.51 % (3129982)Time elapsed: 0.004 s
% 1.59/0.51 % (3129982)Peak memory usage: 10 MB
% 1.59/0.51 % (3129982)Instructions burned: 16 (million)
% 1.59/0.51 % (3129980)Instruction limit reached!
% 1.59/0.51 % (3129980)------------------------------
% 1.59/0.51 % (3129980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.51 % (3129980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.51 % (3129980)CaDiCaL version: 2.1.3
% 1.59/0.51 % (3129980)Termination reason: Instruction limit
% 1.59/0.51 % (3129980)Termination phase: Preprocessing 3
% 1.59/0.51 % (3129980)Time elapsed: 0.007 s
% 1.59/0.51 % (3129980)Peak memory usage: 10 MB
% 1.59/0.51 % (3129980)Instructions burned: 15 (million)
% 1.59/0.51 % (3129989)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3344097044:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.59/0.51 % (3129985)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2278480907: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.59/0.51 % (3129989)Instruction limit reached!
% 1.59/0.51 % (3129989)------------------------------
% 1.59/0.51 % (3129989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.51 % (3129989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.51 % (3129989)CaDiCaL version: 2.1.3
% 1.59/0.51 % (3129989)Termination reason: Instruction limit
% 1.59/0.51 % (3129989)Termination phase: Property scanning
% 1.59/0.51 % (3129989)Time elapsed: 0.006 s
% 1.59/0.51 % (3129989)Peak memory usage: 11 MB
% 1.59/0.51 % (3129989)Instructions burned: 27 (million)
% 1.59/0.51 % (3129987)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2990464750:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.59/0.51 % (3129985)Instruction limit reached!
% 1.59/0.51 % (3129985)------------------------------
% 1.59/0.51 % (3129985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.51 % (3129985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.51 % (3129985)CaDiCaL version: 2.1.3
% 1.59/0.51 % (3129985)Termination reason: Instruction limit
% 1.59/0.51 % (3129985)Termination phase: Property scanning
% 1.59/0.51 % (3129985)Time elapsed: 0.003 s
% 1.59/0.51 % (3129985)Peak memory usage: 10 MB
% 1.59/0.51 % (3129985)Instructions burned: 6 (million)
% 1.59/0.51 % (3129990)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=416519776:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.59/0.51 % (3129993)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.59/0.51 % (3129993)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.59/0.57 % (3129993)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=686654141:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.59/0.57 % (3129987)Instruction limit reached!
% 1.59/0.57 % (3129987)------------------------------
% 1.59/0.57 % (3129987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.57 % (3129987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.57 % (3129987)CaDiCaL version: 2.1.3
% 1.59/0.57 % (3129987)Termination reason: Instruction limit
% 1.59/0.57 % (3129987)Termination phase: Property scanning
% 1.59/0.57 % (3129987)Time elapsed: 0.011 s
% 1.59/0.57 % (3129987)Peak memory usage: 10 MB
% 1.59/0.57 % (3129987)Instructions burned: 27 (million)
% 1.59/0.57 % (3129993)Instruction limit reached!
% 1.59/0.57 % (3129993)------------------------------
% 1.59/0.57 % (3129993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.57 % (3129993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.57 % (3129993)CaDiCaL version: 2.1.3
% 1.59/0.57 % (3129993)Termination reason: Instruction limit
% 1.59/0.57 % (3129993)Termination phase: Property scanning
% 1.59/0.57 % (3129993)Time elapsed: 0.004 s
% 1.59/0.57 % (3129993)Peak memory usage: 10 MB
% 1.59/0.57 % (3129993)Instructions burned: 17 (million)
% 1.59/0.57 % (3129995)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.59/0.57 % (3129995)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=83639958:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.59/0.57 % (3129999)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3092081609:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.59/0.57 % (3129995)Instruction limit reached!
% 1.59/0.57 % (3129995)------------------------------
% 1.59/0.57 % (3129995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.57 % (3129995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.57 % (3129995)CaDiCaL version: 2.1.3
% 1.59/0.57 % (3129995)Termination reason: Instruction limit
% 1.59/0.57 % (3129995)Termination phase: Property scanning
% 1.59/0.57 % (3129995)Time elapsed: 0.004 s
% 1.59/0.57 % (3129995)Peak memory usage: 10 MB
% 1.59/0.57 % (3129995)Instructions burned: 9 (million)
% 1.59/0.57 % (3129999)Instruction limit reached!
% 1.59/0.57 % (3129999)------------------------------
% 1.59/0.57 % (3129999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.57 % (3129999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.57 % (3129999)CaDiCaL version: 2.1.3
% 1.59/0.57 % (3129999)Termination reason: Instruction limit
% 1.59/0.57 % (3129999)Termination phase: Property scanning
% 1.59/0.57 % (3129999)Time elapsed: 0.002 s
% 1.59/0.57 % (3129999)Peak memory usage: 10 MB
% 1.59/0.57 % (3129999)Instructions burned: 9 (million)
% 1.59/0.57 % (3129998)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=3462627399:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.59/0.57 % (3129990)Instruction limit reached!
% 1.59/0.57 % (3129990)------------------------------
% 1.59/0.57 % (3129990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.57 % (3129990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.57 % (3129990)CaDiCaL version: 2.1.3
% 1.59/0.57 % (3129990)Termination reason: Instruction limit
% 1.59/0.57 % (3129990)Termination phase: Saturation
% 1.59/0.57 % (3129990)Time elapsed: 0.028 s
% 1.59/0.57 % (3129990)Peak memory usage: 12 MB
% 1.59/0.57 % (3129990)Instructions burned: 60 (million)
% 1.59/0.57 % (3129998)Instruction limit reached!
% 1.59/0.57 % (3129998)------------------------------
% 1.59/0.57 % (3129998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.57 % (3129998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.57 % (3129998)CaDiCaL version: 2.1.3
% 1.59/0.57 % (3129998)Termination reason: Instruction limit
% 1.59/0.57 % (3129998)Termination phase: Property scanning
% 2.60/0.64 % (3129998)Time elapsed: 0.013 s
% 2.60/0.64 % (3129998)Peak memory usage: 10 MB
% 2.60/0.64 % (3129998)Instructions burned: 31 (million)
% 2.60/0.64 % (3130002)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3522611792:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.60/0.64 % (3130003)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=629859945:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.60/0.64 % (3130005)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3350420601:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.60/0.64 % (3130002)Instruction limit reached!
% 2.60/0.64 % (3130002)------------------------------
% 2.60/0.64 % (3130002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.64 % (3130002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.64 % (3130002)CaDiCaL version: 2.1.3
% 2.60/0.64 % (3130002)Termination reason: Instruction limit
% 2.60/0.64 % (3130002)Termination phase: Property scanning
% 2.60/0.64 % (3130002)Time elapsed: 0.011 s
% 2.60/0.64 % (3130002)Peak memory usage: 10 MB
% 2.60/0.64 % (3130002)Instructions burned: 26 (million)
% 2.60/0.64 % (3130003)Instruction limit reached!
% 2.60/0.64 % (3130003)------------------------------
% 2.60/0.64 % (3130003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.64 % (3130003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.64 % (3130003)CaDiCaL version: 2.1.3
% 2.60/0.64 % (3130003)Termination reason: Instruction limit
% 2.60/0.64 % (3130003)Termination phase: Property scanning
% 2.60/0.64 % (3130003)Time elapsed: 0.011 s
% 2.60/0.64 % (3130003)Peak memory usage: 11 MB
% 2.60/0.64 % (3130003)Instructions burned: 24 (million)
% 2.60/0.64 % (3130008)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2415874186:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.60/0.64 % (3130010)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=4208160219:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.60/0.64 % (3130011)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3541055144:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.60/0.64 % (3130011)Instruction limit reached!
% 2.60/0.64 % (3130011)------------------------------
% 2.60/0.64 % (3130011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.64 % (3130011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.64 % (3130011)CaDiCaL version: 2.1.3
% 2.60/0.64 % (3130011)Termination reason: Instruction limit
% 2.60/0.64 % (3130011)Termination phase: Saturation
% 2.60/0.64 % (3130011)Time elapsed: 0.019 s
% 2.60/0.64 % (3130011)Peak memory usage: 12 MB
% 2.60/0.64 % (3130011)Instructions burned: 42 (million)
% 2.60/0.64 % (3129981)Instruction limit reached!
% 2.60/0.64 % (3129981)------------------------------
% 2.60/0.64 % (3129981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.64 % (3129981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.64 % (3129981)CaDiCaL version: 2.1.3
% 2.60/0.64 % (3129981)Termination reason: Instruction limit
% 2.60/0.64 % (3129981)Termination phase: Saturation
% 2.60/0.64 % (3129981)Time elapsed: 0.120 s
% 2.60/0.64 % (3129981)Peak memory usage: 14 MB
% 2.60/0.64 % (3129981)Instructions burned: 331 (million)
% 2.60/0.64 % (3130015)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.60/0.64 % (3130016)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1265043296:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.60/0.64 % (3130015)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1481071378:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.60/0.64 % (3130015)Instruction limit reached!
% 2.60/0.64 % (3130015)------------------------------
% 2.60/0.64 % (3130015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.64 % (3130015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.64 % (3130015)CaDiCaL version: 2.1.3
% 2.60/0.64 % (3130015)Termination reason: Instruction limit
% 2.93/0.71 % (3130015)Termination phase: shuffling
% 2.93/0.71 % (3130015)Time elapsed: 0.003 s
% 2.93/0.71 % (3130015)Peak memory usage: 10 MB
% 2.93/0.71 % (3130015)Instructions burned: 7 (million)
% 2.93/0.71 % (3129975)Instruction limit reached!
% 2.93/0.71 % (3129975)------------------------------
% 2.93/0.71 % (3129975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.93/0.71 % (3129975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/0.71 % (3129975)CaDiCaL version: 2.1.3
% 2.93/0.71 % (3129975)Termination reason: Instruction limit
% 2.93/0.71 % (3129975)Termination phase: Saturation
% 2.93/0.71 % (3129975)Time elapsed: 0.165 s
% 2.93/0.71 % (3129975)Peak memory usage: 14 MB
% 2.93/0.71 % (3129975)Instructions burned: 249 (million)
% 2.93/0.71 % (3130019)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=2765281613: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.93/0.71 % (3130008)Instruction limit reached!
% 2.93/0.71 % (3130008)------------------------------
% 2.93/0.71 % (3130008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.93/0.71 % (3130008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/0.71 % (3130008)CaDiCaL version: 2.1.3
% 2.93/0.71 % (3130008)Termination reason: Instruction limit
% 2.93/0.71 % (3130008)Termination phase: Saturation
% 2.93/0.71 % (3130008)Time elapsed: 0.070 s
% 2.93/0.71 % (3130008)Peak memory usage: 13 MB
% 2.93/0.71 % (3130008)Instructions burned: 145 (million)
% 2.93/0.71 % (3130020)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.93/0.71 % (3130020)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3736115665: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.93/0.71 % (3130022)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3100560321:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.93/0.71 % (3130020)Instruction limit reached!
% 2.93/0.71 % (3130020)------------------------------
% 2.93/0.71 % (3130020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.93/0.71 % (3130020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/0.71 % (3130020)CaDiCaL version: 2.1.3
% 2.93/0.71 % (3130020)Termination reason: Instruction limit
% 2.93/0.71 % (3130020)Termination phase: shuffling
% 2.93/0.71 % (3130020)Time elapsed: 0.006 s
% 2.93/0.71 % (3130020)Peak memory usage: 9 MB
% 2.93/0.71 % (3130020)Instructions burned: 6 (million)
% 2.93/0.71 % (3130016)Instruction limit reached!
% 2.93/0.71 % (3130016)------------------------------
% 2.93/0.71 % (3130016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.93/0.71 % (3130016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/0.71 % (3130016)CaDiCaL version: 2.1.3
% 2.93/0.71 % (3130016)Termination reason: Instruction limit
% 2.93/0.71 % (3130016)Termination phase: Saturation
% 2.93/0.71 % (3130016)Time elapsed: 0.049 s
% 2.93/0.71 % (3130016)Peak memory usage: 14 MB
% 2.93/0.71 % (3130016)Instructions burned: 182 (million)
% 2.93/0.71 % (3130022)Instruction limit reached!
% 2.93/0.72 % (3130022)------------------------------
% 2.93/0.72 % (3130022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.93/0.72 % (3130022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/0.72 % (3130022)CaDiCaL version: 2.1.3
% 2.93/0.72 % (3130022)Termination reason: Instruction limit
% 2.93/0.72 % (3130022)Termination phase: Property scanning
% 2.93/0.72 % (3130022)Time elapsed: 0.010 s
% 2.93/0.72 % (3130022)Peak memory usage: 10 MB
% 2.93/0.72 % (3130022)Instructions burned: 23 (million)
% 2.93/0.72 % (3130026)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=2412061911:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.93/0.72 % (3130010)Instruction limit reached!
% 2.93/0.72 % (3130010)------------------------------
% 2.93/0.72 % (3130010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.93/0.72 % (3130010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.81 % (3130010)CaDiCaL version: 2.1.3
% 3.35/0.81 % (3130010)Termination reason: Instruction limit
% 3.35/0.81 % (3130010)Termination phase: Saturation
% 3.35/0.81 % (3130010)Time elapsed: 0.099 s
% 3.35/0.81 % (3130010)Peak memory usage: 13 MB
% 3.35/0.81 % (3130010)Instructions burned: 193 (million)
% 3.35/0.81 % (3130027)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=3441498671:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.35/0.81 % (3130025)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2003604987:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 3.35/0.81 % (3130029)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=3207843107:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.35/0.81 % (3130025)Instruction limit reached!
% 3.35/0.81 % (3130025)------------------------------
% 3.35/0.81 % (3130025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.81 % (3130025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.81 % (3130025)CaDiCaL version: 2.1.3
% 3.35/0.81 % (3130025)Termination reason: Instruction limit
% 3.35/0.81 % (3130025)Termination phase: Property scanning
% 3.35/0.81 % (3130025)Time elapsed: 0.016 s
% 3.35/0.81 % (3130025)Peak memory usage: 10 MB
% 3.35/0.81 % (3130025)Instructions burned: 19 (million)
% 3.35/0.81 % (3130029)Instruction limit reached!
% 3.35/0.81 % (3130029)------------------------------
% 3.35/0.81 % (3130029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.81 % (3130029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.81 % (3130029)CaDiCaL version: 2.1.3
% 3.35/0.81 % (3130029)Termination reason: Instruction limit
% 3.35/0.81 % (3130029)Termination phase: Saturation
% 3.35/0.81 % (3130029)Time elapsed: 0.020 s
% 3.35/0.81 % (3130029)Peak memory usage: 12 MB
% 3.35/0.81 % (3130029)Instructions burned: 46 (million)
% 3.35/0.81 % (3130019)Instruction limit reached!
% 3.35/0.81 % (3130019)------------------------------
% 3.35/0.81 % (3130019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.81 % (3130019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.81 % (3130019)CaDiCaL version: 2.1.3
% 3.35/0.81 % (3130019)Termination reason: Instruction limit
% 3.35/0.81 % (3130019)Termination phase: Saturation
% 3.35/0.81 % (3130019)Time elapsed: 0.083 s
% 3.35/0.81 % (3130019)Peak memory usage: 13 MB
% 3.35/0.81 % (3130019)Instructions burned: 170 (million)
% 3.35/0.81 % (3130033)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=4273724503:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.35/0.81 % (3129948)Instruction limit reached!
% 3.35/0.81 % (3129948)------------------------------
% 3.35/0.81 % (3129948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.81 % (3129948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.81 % (3129948)CaDiCaL version: 2.1.3
% 3.35/0.81 % (3129948)Termination reason: Instruction limit
% 3.35/0.81 % (3129948)Termination phase: Saturation
% 3.35/0.81 % (3129948)Time elapsed: 0.348 s
% 3.35/0.81 % (3129948)Peak memory usage: 17 MB
% 3.35/0.81 % (3129948)Instructions burned: 634 (million)
% 3.35/0.81 % (3130035)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.35/0.81 % (3130034)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1313190005:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.35/0.81 % (3130035)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2874131398:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.35/0.81 % (3130034)Instruction limit reached!
% 3.35/0.81 % (3130034)------------------------------
% 3.35/0.81 % (3130034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.81 % (3130034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.81 % (3130034)CaDiCaL version: 2.1.3
% 3.64/0.97 % (3130034)Termination reason: Instruction limit
% 3.64/0.97 % (3130034)Termination phase: Property scanning
% 3.64/0.97 % (3130034)Time elapsed: 0.009 s
% 3.64/0.97 % (3130034)Peak memory usage: 10 MB
% 3.64/0.97 % (3130034)Instructions burned: 21 (million)
% 3.64/0.97 % (3130037)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1857230681:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.64/0.97 % (3130037)Instruction limit reached!
% 3.64/0.97 % (3130037)------------------------------
% 3.64/0.97 % (3130037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.97 % (3130037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.97 % (3130037)CaDiCaL version: 2.1.3
% 3.64/0.97 % (3130037)Termination reason: Instruction limit
% 3.64/0.97 % (3130037)Termination phase: Preprocessing 3
% 3.64/0.97 % (3130037)Time elapsed: 0.007 s
% 3.64/0.97 % (3130037)Peak memory usage: 10 MB
% 3.64/0.97 % (3130037)Instructions burned: 15 (million)
% 3.64/0.97 % (3130026)Instruction limit reached!
% 3.64/0.97 % (3130026)------------------------------
% 3.64/0.97 % (3130026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.97 % (3130026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.97 % (3130026)CaDiCaL version: 2.1.3
% 3.64/0.97 % (3130026)Termination reason: Instruction limit
% 3.64/0.97 % (3130026)Termination phase: Saturation
% 3.64/0.97 % (3130026)Time elapsed: 0.090 s
% 3.64/0.97 % (3130026)Peak memory usage: 15 MB
% 3.64/0.97 % (3130026)Instructions burned: 326 (million)
% 3.64/0.97 % (3130040)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=3709731382:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.64/0.97 % (3130043)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2596574783:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.64/0.97 % (3130042)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=200577197:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.64/0.97 % (3130043)Instruction limit reached!
% 3.64/0.97 % (3130043)------------------------------
% 3.64/0.97 % (3130043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.97 % (3130043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.97 % (3130043)CaDiCaL version: 2.1.3
% 3.64/0.97 % (3130043)Termination reason: Instruction limit
% 3.64/0.97 % (3130043)Termination phase: Property scanning
% 3.64/0.97 % (3130043)Time elapsed: 0.007 s
% 3.64/0.97 % (3130043)Peak memory usage: 10 MB
% 3.64/0.97 % (3130043)Instructions burned: 31 (million)
% 3.64/0.97 % (3130047)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=334515875:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.64/0.97 % (3130040)Instruction limit reached!
% 3.64/0.97 % (3130040)------------------------------
% 3.64/0.97 % (3130040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.97 % (3130040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.97 % (3130040)CaDiCaL version: 2.1.3
% 3.64/0.97 % (3130040)Termination reason: Instruction limit
% 3.64/0.97 % (3130040)Termination phase: Saturation
% 3.64/0.97 % (3130040)Time elapsed: 0.028 s
% 3.64/0.97 % (3130040)Peak memory usage: 12 MB
% 3.64/0.97 % (3130040)Instructions burned: 67 (million)
% 3.64/0.97 % (3130042)Instruction limit reached!
% 3.64/0.97 % (3130042)------------------------------
% 3.64/0.97 % (3130042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.64/0.97 % (3130042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.64/0.97 % (3130042)CaDiCaL version: 2.1.3
% 3.64/0.97 % (3130042)Termination reason: Instruction limit
% 3.64/0.97 % (3130042)Termination phase: Saturation
% 3.64/0.97 % (3130042)Time elapsed: 0.024 s
% 3.64/0.97 % (3130042)Peak memory usage: 12 MB
% 3.64/0.97 % (3130042)Instructions burned: 51 (million)
% 3.64/0.97 % (3130049)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=175794938:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.64/0.97 % (3130050)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3117396201:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.56/1.10 % (3130049)Instruction limit reached!
% 5.56/1.10 % (3130049)------------------------------
% 5.56/1.10 % (3130049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.10 % (3130049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.10 % (3130049)CaDiCaL version: 2.1.3
% 5.56/1.10 % (3130049)Termination reason: Instruction limit
% 5.56/1.10 % (3130049)Termination phase: Function definition elimination
% 5.56/1.10 % (3130049)Time elapsed: 0.014 s
% 5.56/1.10 % (3130049)Peak memory usage: 10 MB
% 5.56/1.10 % (3130049)Instructions burned: 34 (million)
% 5.56/1.10 % (3130047)Instruction limit reached!
% 5.56/1.10 % (3130047)------------------------------
% 5.56/1.10 % (3130047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.10 % (3130047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.10 % (3130047)CaDiCaL version: 2.1.3
% 5.56/1.10 % (3130047)Termination reason: Instruction limit
% 5.56/1.10 % (3130047)Termination phase: Saturation
% 5.56/1.10 % (3130047)Time elapsed: 0.036 s
% 5.56/1.10 % (3130047)Peak memory usage: 13 MB
% 5.56/1.10 % (3130047)Instructions burned: 140 (million)
% 5.56/1.10 % (3130035)Instruction limit reached!
% 5.56/1.10 % (3130035)------------------------------
% 5.56/1.10 % (3130035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.10 % (3130035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.10 % (3130035)CaDiCaL version: 2.1.3
% 5.56/1.10 % (3130035)Termination reason: Instruction limit
% 5.56/1.10 % (3130035)Termination phase: Saturation
% 5.56/1.10 % (3130035)Time elapsed: 0.094 s
% 5.56/1.10 % (3130035)Peak memory usage: 12 MB
% 5.56/1.10 % (3130035)Instructions burned: 202 (million)
% 5.56/1.10 % (3130054)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2304290790:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.56/1.10 % (3130053)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.56/1.10 % (3130053)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3251056377:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.56/1.10 % (3130055)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=744027537:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.56/1.10 % (3130050)Instruction limit reached!
% 5.56/1.10 % (3130050)------------------------------
% 5.56/1.10 % (3130050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.10 % (3130050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.10 % (3130050)CaDiCaL version: 2.1.3
% 5.56/1.10 % (3130050)Termination reason: Instruction limit
% 5.56/1.10 % (3130050)Termination phase: Saturation
% 5.56/1.10 % (3130050)Time elapsed: 0.033 s
% 5.56/1.10 % (3130050)Peak memory usage: 13 MB
% 5.56/1.10 % (3130050)Instructions burned: 69 (million)
% 5.56/1.10 % (3130059)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=158050389:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.56/1.10 % (3130055)Instruction limit reached!
% 5.56/1.10 % (3130055)------------------------------
% 5.56/1.10 % (3130055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.10 % (3130055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.10 % (3130055)CaDiCaL version: 2.1.3
% 5.56/1.10 % (3130055)Termination reason: Instruction limit
% 5.56/1.10 % (3130055)Termination phase: Saturation
% 5.56/1.10 % (3130055)Time elapsed: 0.042 s
% 5.56/1.10 % (3130055)Peak memory usage: 12 MB
% 5.56/1.10 % (3130055)Instructions burned: 97 (million)
% 5.56/1.10 % (3130054)Instruction limit reached!
% 5.56/1.10 % (3130054)------------------------------
% 5.56/1.10 % (3130054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.56/1.10 % (3130054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.10 % (3130054)CaDiCaL version: 2.1.3
% 5.56/1.10 % (3130054)Termination reason: Instruction limit
% 5.56/1.10 % (3130054)Termination phase: Saturation
% 5.56/1.10 % (3130054)Time elapsed: 0.065 s
% 5.56/1.10 % (3130054)Peak memory usage: 14 MB
% 5.56/1.10 % (3130054)Instructions burned: 246 (million)
% 5.56/1.10 % (3130062)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1273019575:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 6.31/1.20 % (3130061)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1309418630:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 6.31/1.20 % (3130053)Instruction limit reached!
% 6.31/1.20 % (3130053)------------------------------
% 6.31/1.20 % (3130053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (3130053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (3130053)CaDiCaL version: 2.1.3
% 6.31/1.20 % (3130053)Termination reason: Instruction limit
% 6.31/1.20 % (3130053)Termination phase: Saturation
% 6.31/1.20 % (3130053)Time elapsed: 0.087 s
% 6.31/1.20 % (3130053)Peak memory usage: 13 MB
% 6.31/1.20 % (3130053)Instructions burned: 181 (million)
% 6.31/1.20 % (3130065)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2117437012:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 6.31/1.20 % (3130065)Instruction limit reached!
% 6.31/1.20 % (3130065)------------------------------
% 6.31/1.20 % (3130065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (3130065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (3130065)CaDiCaL version: 2.1.3
% 6.31/1.20 % (3130065)Termination reason: Instruction limit
% 6.31/1.20 % (3130065)Termination phase: Saturation
% 6.31/1.20 % (3130065)Time elapsed: 0.068 s
% 6.31/1.20 % (3130065)Peak memory usage: 13 MB
% 6.31/1.20 % (3130065)Instructions burned: 132 (million)
% 6.31/1.20 % (3130067)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1564977144:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 6.31/1.20 % (3130062)Instruction limit reached!
% 6.31/1.20 % (3130062)------------------------------
% 6.31/1.20 % (3130062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (3130062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (3130062)CaDiCaL version: 2.1.3
% 6.31/1.20 % (3130062)Termination reason: Instruction limit
% 6.31/1.20 % (3130062)Termination phase: Saturation
% 6.31/1.20 % (3130062)Time elapsed: 0.135 s
% 6.31/1.20 % (3130062)Peak memory usage: 16 MB
% 6.31/1.20 % (3130062)Instructions burned: 519 (million)
% 6.31/1.20 % (3130059)Instruction limit reached!
% 6.31/1.20 % (3130059)------------------------------
% 6.31/1.20 % (3130059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (3130059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (3130059)CaDiCaL version: 2.1.3
% 6.31/1.20 % (3130059)Termination reason: Instruction limit
% 6.31/1.20 % (3130059)Termination phase: Saturation
% 6.31/1.20 % (3130059)Time elapsed: 0.183 s
% 6.31/1.20 % (3130059)Peak memory usage: 14 MB
% 6.31/1.20 % (3130059)Instructions burned: 427 (million)
% 6.31/1.20 % (3130033)Instruction limit reached!
% 6.31/1.20 % (3130033)------------------------------
% 6.31/1.20 % (3130033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (3130033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (3130033)CaDiCaL version: 2.1.3
% 6.31/1.20 % (3130033)Termination reason: Instruction limit
% 6.31/1.20 % (3130033)Termination phase: Saturation
% 6.31/1.20 % (3130033)Time elapsed: 0.329 s
% 6.31/1.20 % (3130033)Peak memory usage: 14 MB
% 6.31/1.20 % (3130033)Instructions burned: 480 (million)
% 6.31/1.20 % (3130067)Instruction limit reached!
% 6.31/1.20 % (3130067)------------------------------
% 6.31/1.20 % (3130067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (3130067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (3130067)CaDiCaL version: 2.1.3
% 6.31/1.20 % (3130067)Termination reason: Instruction limit
% 6.31/1.20 % (3130067)Termination phase: Property scanning
% 6.31/1.20 % (3130067)Time elapsed: 0.019 s
% 6.31/1.20 % (3130067)Peak memory usage: 11 MB
% 6.31/1.20 % (3130067)Instructions burned: 47 (million)
% 6.31/1.20 % (3130069)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1550708450:s2a=on:i=571:nm=16:rtra=on_2992 on theBenchmark for (2992ds/571Mi)
% 6.31/1.20 % (3130070)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2508513935:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 6.31/1.20 % (3130071)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=63421699:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.31/1.22 % (3130072)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=1293342717:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 6.31/1.22 % (3130072)Instruction limit reached!
% 6.31/1.22 % (3130072)------------------------------
% 6.31/1.22 % (3130072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130072)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130072)Termination reason: Instruction limit
% 6.31/1.22 % (3130072)Termination phase: Saturation
% 6.31/1.22 % (3130072)Time elapsed: 0.028 s
% 6.31/1.22 % (3130072)Peak memory usage: 12 MB
% 6.31/1.22 % (3130072)Instructions burned: 65 (million)
% 6.31/1.22 % (3130071)Instruction limit reached!
% 6.31/1.22 % (3130071)------------------------------
% 6.31/1.22 % (3130071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130071)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130071)Termination reason: Instruction limit
% 6.31/1.22 % (3130071)Termination phase: Saturation
% 6.31/1.22 % (3130071)Time elapsed: 0.043 s
% 6.31/1.22 % (3130071)Peak memory usage: 12 MB
% 6.31/1.22 % (3130071)Instructions burned: 95 (million)
% 6.31/1.22 % (3130077)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=836607102: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_2992 on theBenchmark for (2992ds/105Mi)
% 6.31/1.22 % (3130078)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=390299957:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.31/1.22 % (3130027)Instruction limit reached!
% 6.31/1.22 % (3130027)------------------------------
% 6.31/1.22 % (3130027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130027)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130027)Termination reason: Instruction limit
% 6.31/1.22 % (3130027)Termination phase: Saturation
% 6.31/1.22 % (3130027)Time elapsed: 0.487 s
% 6.31/1.22 % (3130027)Peak memory usage: 18 MB
% 6.31/1.22 % (3130027)Instructions burned: 854 (million)
% 6.31/1.22 % (3130077)Instruction limit reached!
% 6.31/1.22 % (3130077)------------------------------
% 6.31/1.22 % (3130077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130077)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130077)Termination reason: Instruction limit
% 6.31/1.22 % (3130077)Termination phase: Saturation
% 6.31/1.22 % (3130077)Time elapsed: 0.051 s
% 6.31/1.22 % (3130077)Peak memory usage: 14 MB
% 6.31/1.22 % (3130077)Instructions burned: 106 (million)
% 6.31/1.22 % (3130005)Instruction limit reached!
% 6.31/1.22 % (3130005)------------------------------
% 6.31/1.22 % (3130005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130005)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130005)Termination reason: Instruction limit
% 6.31/1.22 % (3130005)Termination phase: Saturation
% 6.31/1.22 % (3130005)Time elapsed: 0.635 s
% 6.31/1.22 % (3130005)Peak memory usage: 17 MB
% 6.31/1.22 % (3130005)Instructions burned: 1241 (million)
% 6.31/1.22 % (3130081)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2886887786:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/375Mi)
% 6.31/1.22 % (3130082)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=956852420:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 6.31/1.22 % (3130069)Instruction limit reached!
% 6.31/1.22 % (3130069)------------------------------
% 6.31/1.22 % (3130069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130069)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130069)Termination reason: Instruction limit
% 6.31/1.22 % (3130069)Termination phase: Saturation
% 6.31/1.22 % (3130069)Time elapsed: 0.141 s
% 6.31/1.22 % (3130069)Peak memory usage: 15 MB
% 6.31/1.22 % (3130069)Instructions burned: 573 (million)
% 6.31/1.22 % (3130083)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=93653945:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 6.31/1.22 % (3130086)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1170634289:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 6.31/1.22 % (3130083)Instruction limit reached!
% 6.31/1.22 % (3130083)------------------------------
% 6.31/1.22 % (3130083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130083)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130083)Termination reason: Instruction limit
% 6.31/1.22 % (3130083)Termination phase: Property scanning
% 6.31/1.22 % (3130083)Time elapsed: 0.014 s
% 6.31/1.22 % (3130083)Peak memory usage: 10 MB
% 6.31/1.22 % (3130083)Instructions burned: 34 (million)
% 6.31/1.22 % (3130086)Instruction limit reached!
% 6.31/1.22 % (3130086)------------------------------
% 6.31/1.22 % (3130086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130086)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130086)Termination reason: Instruction limit
% 6.31/1.22 % (3130086)Termination phase: Saturation
% 6.31/1.22 % (3130086)Time elapsed: 0.022 s
% 6.31/1.22 % (3130086)Peak memory usage: 13 MB
% 6.31/1.22 % (3130086)Instructions burned: 94 (million)
% 6.31/1.22 % (3130089)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2914575209:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 6.31/1.22 % (3130090)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2335610793:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.31/1.22 % (3130090)Instruction limit reached!
% 6.31/1.22 % (3130090)------------------------------
% 6.31/1.22 % (3130090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130090)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130090)Termination reason: Instruction limit
% 6.31/1.22 % (3130090)Termination phase: Inequality splitting
% 6.31/1.22 % (3130090)Time elapsed: 0.006 s
% 6.31/1.22 % (3130090)Peak memory usage: 11 MB
% 6.31/1.22 % (3130090)Instructions burned: 26 (million)
% 6.31/1.22 % (3130093)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=268124768:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 6.31/1.22 % (3130089)Instruction limit reached!
% 6.31/1.22 % (3130089)------------------------------
% 6.31/1.22 % (3130089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130089)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130089)Termination reason: Instruction limit
% 6.31/1.22 % (3130089)Termination phase: Saturation
% 6.31/1.22 % (3130089)Time elapsed: 0.031 s
% 6.31/1.22 % (3130089)Peak memory usage: 12 MB
% 6.31/1.22 % (3130089)Instructions burned: 68 (million)
% 6.31/1.22 % (3130070)Instruction limit reached!
% 6.31/1.22 % (3130070)------------------------------
% 6.31/1.22 % (3130070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130070)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130070)Termination reason: Instruction limit
% 6.31/1.22 % (3130070)Termination phase: Saturation
% 6.31/1.22 % (3130070)Time elapsed: 0.217 s
% 6.31/1.22 % (3130070)Peak memory usage: 13 MB
% 6.31/1.22 % (3130070)Instructions burned: 451 (million)
% 6.31/1.22 % (3130095)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1212851133:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/28Mi)
% 6.31/1.22 % (3130095)Instruction limit reached!
% 6.31/1.22 % (3130095)------------------------------
% 6.31/1.22 % (3130095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.22 % (3130095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.22 % (3130095)CaDiCaL version: 2.1.3
% 6.31/1.22 % (3130095)Termination reason: Instruction limit
% 6.31/1.22 % (3130095)Termination phase: Saturation
% 6.31/1.22 % (3130095)Time elapsed: 0.013 s
% 6.31/1.22 % (3130095)Peak memory usage: 12 MB
% 6.31/1.22 % (3130095)Instructions burned: 28 (million)
% 6.31/1.22 % (3130096)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.31/1.22 % (3130096)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3069116263:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2990 on theBenchmark for (2990ds/137Mi)
% 6.31/1.22 % (3130093) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3129940-3130093"...
% 6.31/1.22 % (3130093)...printing done.
% 6.31/1.22 % (3130098)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=1357452278:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 6.31/1.22 % (3130093)Refutation found. Thanks to Tanya!
% 6.31/1.22 % SZS status Theorem for theBenchmark
% 6.31/1.22 % SZS output start Proof for theBenchmark
% See solution above
% 6.31/1.23 % (3130093)------------------------------
% 6.31/1.23 % (3130093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.23 % (3130093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.23 % (3130093)CaDiCaL version: 2.1.3
% 6.31/1.23 % (3130093)Termination reason: Refutation
% 6.31/1.23 % (3130093)Time elapsed: 0.060 s
% 6.31/1.23 % (3130093)Peak memory usage: 14 MB
% 6.31/1.23 % (3130093)Instructions burned: 214 (million)
% 6.31/1.23 % (3129940)Success in time 0.982 s
% 6.31/1.23 % Vampire exiting
%------------------------------------------------------------------------------