%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP147^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:04:30 AM UTC 2026
% Result : Theorem 214.42s 31.58s
% Output : CNFRefutation 214.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 30 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 129 ( 18 equ; 0 cnn)
% Maximal formula atoms : 24 ( 4 avg)
% Number of connectives : 668 ( 70 ~; 70 |; 8 &; 499 @)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 9 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 13 ( 13 >; 0 *; 0 +; 0 <<)
% Number of symbols : 21 ( 19 usr; 9 con; 0-4 aty)
% Number of variables : 37 ( 0 ^; 37 !; 0 ?; 37 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
real: $tType ).
thf(decl_sort2,type,
set_a: $tType ).
thf(decl_sort3,type,
a: $tType ).
thf(decl_24,type,
elemen154694473ball_a: a > real > set_a ).
thf(decl_26,type,
auto_ll_on_flow0_a: ( a > a ) > set_a > a > real > a ).
thf(decl_27,type,
abs_abs_real: real > real ).
thf(decl_29,type,
one_one_real: real ).
thf(decl_35,type,
zero_zero_real: real ).
thf(decl_41,type,
line_open_segment_a: a > a > set_a ).
thf(decl_44,type,
ord_less_real: real > real > $o ).
thf(decl_55,type,
topolo1710226732a_real: set_a > ( a > real ) > $o ).
thf(decl_57,type,
member_a: a > set_a > $o ).
thf(decl_58,type,
x: set_a ).
thf(decl_59,type,
a2: a ).
thf(decl_60,type,
b: a ).
thf(decl_61,type,
f: a > a ).
thf(decl_62,type,
p: a ).
thf(decl_63,type,
thesisa: $o ).
thf(decl_65,type,
esk1_2: real > ( a > real ) > a ).
thf(decl_66,type,
esk2_2: real > ( a > real ) > a ).
thf(decl_73,type,
esk9_0: real ).
thf(decl_74,type,
esk10_0: a > real ).
thf(conj_1,conjecture,
thesisa,
file('/export/starexec/sandbox/tmp/tmp.LWZYIfH9g9/E---3.1_3333213.p',conj_1) ).
thf(conj_0,hypothesis,
! [X304: real,X305: a > real] :
( ( ord_less_real @ zero_zero_real @ X304 )
=> ( ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X304 ) @ X305 )
=> ( ( ( X305 @ p )
= zero_zero_real )
=> ( ! [X10: a] :
( ( member_a @ X10 @ ( elemen154694473ball_a @ p @ X304 ) )
=> ( ord_less_real @ ( abs_abs_real @ ( X305 @ X10 ) ) @ one_one_real ) )
=> ( ! [X10: a] :
( ( member_a @ X10 @ ( elemen154694473ball_a @ p @ X304 ) )
=> ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ X10 @ ( X305 @ X10 ) ) @ ( line_open_segment_a @ a2 @ b ) ) )
=> thesisa ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LWZYIfH9g9/E---3.1_3333213.p',conj_0) ).
thf(fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062d_At_O_A_092_060lbrakk_0620_A_060_Ad_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_Aflow0_Ay_A_It_Ay_J_A_092_060in_062_A_123a_060_N_N_060b_125_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_A_092_060bar_062t_Ay_092_060bar_062_A_060_A1_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_At_Ap_A_061_A0_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X5: real] :
( ( ord_less_real @ zero_zero_real @ X5 )
=> ! [X6: a > real] :
( ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
=> ( ! [X7: a] :
( ( member_a @ X7 @ ( elemen154694473ball_a @ p @ X5 ) )
=> ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ X7 @ ( X6 @ X7 ) ) @ ( line_open_segment_a @ a2 @ b ) ) )
=> ( ! [X7: a] :
( ( member_a @ X7 @ ( elemen154694473ball_a @ p @ X5 ) )
=> ( ord_less_real @ ( abs_abs_real @ ( X6 @ X7 ) ) @ one_one_real ) )
=> ( ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
=> ( ( X6 @ p )
!= zero_zero_real ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LWZYIfH9g9/E---3.1_3333213.p',fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062d_At_O_A_092_060lbrakk_0620_A_060_Ad_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_Aflow0_Ay_A_It_Ay_J_A_092_060in_062_A_123a_060_N_N_060b_125_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_A_092_060bar_062t_Ay_092_060bar_062_A_060_A1_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_At_Ap_A_061_A0_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062) ).
thf(c_0_3,negated_conjecture,
~ thesisa,
inference(assume_negation,[status(cth)],[conj_1]) ).
thf(c_0_4,negated_conjecture,
~ thesisa,
inference(fof_simplification,[status(thm)],[c_0_3]) ).
thf(c_0_5,hypothesis,
! [X464: real,X465: a > real] :
( ( ( member_a @ ( esk2_2 @ X464 @ X465 ) @ ( elemen154694473ball_a @ p @ X464 ) )
| thesisa
| ( member_a @ ( esk1_2 @ X464 @ X465 ) @ ( elemen154694473ball_a @ p @ X464 ) )
| ( ( X465 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X464 ) @ X465 )
| ~ ( ord_less_real @ zero_zero_real @ X464 ) )
& ( ~ ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ ( esk2_2 @ X464 @ X465 ) @ ( X465 @ ( esk2_2 @ X464 @ X465 ) ) ) @ ( line_open_segment_a @ a2 @ b ) )
| thesisa
| ( member_a @ ( esk1_2 @ X464 @ X465 ) @ ( elemen154694473ball_a @ p @ X464 ) )
| ( ( X465 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X464 ) @ X465 )
| ~ ( ord_less_real @ zero_zero_real @ X464 ) )
& ( ( member_a @ ( esk2_2 @ X464 @ X465 ) @ ( elemen154694473ball_a @ p @ X464 ) )
| thesisa
| ~ ( ord_less_real @ ( abs_abs_real @ ( X465 @ ( esk1_2 @ X464 @ X465 ) ) ) @ one_one_real )
| ( ( X465 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X464 ) @ X465 )
| ~ ( ord_less_real @ zero_zero_real @ X464 ) )
& ( ~ ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ ( esk2_2 @ X464 @ X465 ) @ ( X465 @ ( esk2_2 @ X464 @ X465 ) ) ) @ ( line_open_segment_a @ a2 @ b ) )
| thesisa
| ~ ( ord_less_real @ ( abs_abs_real @ ( X465 @ ( esk1_2 @ X464 @ X465 ) ) ) @ one_one_real )
| ( ( X465 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X464 ) @ X465 )
| ~ ( ord_less_real @ zero_zero_real @ X464 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_0])])])])])])]) ).
thf(c_0_6,negated_conjecture,
~ thesisa,
inference(fof_nnf,[status(thm)],[c_0_4]) ).
thf(c_0_7,plain,
~ ! [X5: real] :
( ( ord_less_real @ zero_zero_real @ X5 )
=> ! [X6: a > real] :
( ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
=> ( ! [X7: a] :
( ( member_a @ X7 @ ( elemen154694473ball_a @ p @ X5 ) )
=> ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ X7 @ ( X6 @ X7 ) ) @ ( line_open_segment_a @ a2 @ b ) ) )
=> ( ! [X7: a] :
( ( member_a @ X7 @ ( elemen154694473ball_a @ p @ X5 ) )
=> ( ord_less_real @ ( abs_abs_real @ ( X6 @ X7 ) ) @ one_one_real ) )
=> ( ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
=> ( ( X6 @ p )
!= zero_zero_real ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062d_At_O_A_092_060lbrakk_0620_A_060_Ad_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_Aflow0_Ay_A_It_Ay_J_A_092_060in_062_A_123a_060_N_N_060b_125_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_A_092_060bar_062t_Ay_092_060bar_062_A_060_A1_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_At_Ap_A_061_A0_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062]) ).
thf(c_0_8,hypothesis,
! [X6: a > real,X5: real] :
( thesisa
| ( member_a @ ( esk1_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ~ ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ ( esk2_2 @ X5 @ X6 ) @ ( X6 @ ( esk2_2 @ X5 @ X6 ) ) ) @ ( line_open_segment_a @ a2 @ b ) )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
thf(c_0_9,negated_conjecture,
~ thesisa,
inference(split_conjunct,[status(thm)],[c_0_6]) ).
thf(c_0_10,plain,
! [X612: a,X613: a] :
( ( ord_less_real @ zero_zero_real @ esk9_0 )
& ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ esk9_0 ) @ esk10_0 )
& ( ~ ( member_a @ X612 @ ( elemen154694473ball_a @ p @ esk9_0 ) )
| ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ X612 @ ( esk10_0 @ X612 ) ) @ ( line_open_segment_a @ a2 @ b ) ) )
& ( ~ ( member_a @ X613 @ ( elemen154694473ball_a @ p @ esk9_0 ) )
| ( ord_less_real @ ( abs_abs_real @ ( esk10_0 @ X613 ) ) @ one_one_real ) )
& ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ esk9_0 ) @ esk10_0 )
& ( ( esk10_0 @ p )
= zero_zero_real ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])]) ).
thf(c_0_11,hypothesis,
! [X6: a > real,X5: real] :
( ( member_a @ ( esk1_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ ( esk2_2 @ X5 @ X6 ) @ ( X6 @ ( esk2_2 @ X5 @ X6 ) ) ) @ ( line_open_segment_a @ a2 @ b ) )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(sr,[status(thm)],[c_0_8,c_0_9]) ).
thf(c_0_12,plain,
! [X1: a] :
( ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ ( esk10_0 @ X1 ) ) @ ( line_open_segment_a @ a2 @ b ) )
| ~ ( member_a @ X1 @ ( elemen154694473ball_a @ p @ esk9_0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_13,plain,
( ( esk10_0 @ p )
= zero_zero_real ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_14,hypothesis,
! [X6: a > real,X5: real] :
( ( member_a @ ( esk2_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| thesisa
| ( member_a @ ( esk1_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
thf(c_0_15,plain,
! [X1: a] :
( ( ord_less_real @ ( abs_abs_real @ ( esk10_0 @ X1 ) ) @ one_one_real )
| ~ ( member_a @ X1 @ ( elemen154694473ball_a @ p @ esk9_0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_16,hypothesis,
! [X5: real] :
( ( member_a @ ( esk1_2 @ X5 @ esk10_0 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ~ ( member_a @ ( esk2_2 @ X5 @ esk10_0 ) @ ( elemen154694473ball_a @ p @ esk9_0 ) )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ esk10_0 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_11,c_0_12]),c_0_13])]) ).
thf(c_0_17,plain,
topolo1710226732a_real @ ( elemen154694473ball_a @ p @ esk9_0 ) @ esk10_0,
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_18,plain,
ord_less_real @ zero_zero_real @ esk9_0,
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_19,hypothesis,
! [X6: a > real,X5: real] :
( ( member_a @ ( esk2_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ( member_a @ ( esk1_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(sr,[status(thm)],[c_0_14,c_0_9]) ).
thf(c_0_20,hypothesis,
! [X6: a > real,X5: real] :
( thesisa
| ~ ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ ( esk2_2 @ X5 @ X6 ) @ ( X6 @ ( esk2_2 @ X5 @ X6 ) ) ) @ ( line_open_segment_a @ a2 @ b ) )
| ~ ( ord_less_real @ ( abs_abs_real @ ( X6 @ ( esk1_2 @ X5 @ X6 ) ) ) @ one_one_real )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
thf(c_0_21,hypothesis,
! [X6: a > real,X5: real] :
( ( member_a @ ( esk2_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| thesisa
| ~ ( ord_less_real @ ( abs_abs_real @ ( X6 @ ( esk1_2 @ X5 @ X6 ) ) ) @ one_one_real )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
thf(c_0_22,hypothesis,
( ( ord_less_real @ ( abs_abs_real @ ( esk10_0 @ ( esk1_2 @ esk9_0 @ esk10_0 ) ) ) @ one_one_real )
| ~ ( member_a @ ( esk2_2 @ esk9_0 @ esk10_0 ) @ ( elemen154694473ball_a @ p @ esk9_0 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_16]),c_0_17]),c_0_18])]) ).
thf(c_0_23,hypothesis,
! [X6: a > real] :
( ( member_a @ ( esk2_2 @ esk9_0 @ X6 ) @ ( elemen154694473ball_a @ p @ esk9_0 ) )
| ( ord_less_real @ ( abs_abs_real @ ( esk10_0 @ ( esk1_2 @ esk9_0 @ X6 ) ) ) @ one_one_real )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ esk9_0 ) @ X6 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_19]),c_0_18])]) ).
thf(c_0_24,hypothesis,
! [X6: a > real,X5: real] :
( ( ( X6 @ p )
!= zero_zero_real )
| ~ ( member_a @ ( auto_ll_on_flow0_a @ f @ x @ ( esk2_2 @ X5 @ X6 ) @ ( X6 @ ( esk2_2 @ X5 @ X6 ) ) ) @ ( line_open_segment_a @ a2 @ b ) )
| ~ ( ord_less_real @ ( abs_abs_real @ ( X6 @ ( esk1_2 @ X5 @ X6 ) ) ) @ one_one_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(sr,[status(thm)],[c_0_20,c_0_9]) ).
thf(c_0_25,hypothesis,
! [X6: a > real,X5: real] :
( ( member_a @ ( esk2_2 @ X5 @ X6 ) @ ( elemen154694473ball_a @ p @ X5 ) )
| ( ( X6 @ p )
!= zero_zero_real )
| ~ ( ord_less_real @ ( abs_abs_real @ ( X6 @ ( esk1_2 @ X5 @ X6 ) ) ) @ one_one_real )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ X6 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(sr,[status(thm)],[c_0_21,c_0_9]) ).
thf(c_0_26,hypothesis,
ord_less_real @ ( abs_abs_real @ ( esk10_0 @ ( esk1_2 @ esk9_0 @ esk10_0 ) ) ) @ one_one_real,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_23]),c_0_13]),c_0_17])]) ).
thf(c_0_27,hypothesis,
! [X5: real] :
( ~ ( ord_less_real @ ( abs_abs_real @ ( esk10_0 @ ( esk1_2 @ X5 @ esk10_0 ) ) ) @ one_one_real )
| ~ ( member_a @ ( esk2_2 @ X5 @ esk10_0 ) @ ( elemen154694473ball_a @ p @ esk9_0 ) )
| ~ ( topolo1710226732a_real @ ( elemen154694473ball_a @ p @ X5 ) @ esk10_0 )
| ~ ( ord_less_real @ zero_zero_real @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24,c_0_12]),c_0_13])]) ).
thf(c_0_28,hypothesis,
member_a @ ( esk2_2 @ esk9_0 @ esk10_0 ) @ ( elemen154694473ball_a @ p @ esk9_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_13]),c_0_17]),c_0_18])]) ).
thf(c_0_29,hypothesis,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28]),c_0_26]),c_0_17]),c_0_18])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP147^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n010.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.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 20:01:23 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.20/0.28 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.LWZYIfH9g9/E---3.1_3333213.p
% 214.42/31.58 % Version: 3.5.1-ho
% 214.42/31.58 % Preprocessing class: HSLSSMSMSSMNHSA.
% 214.42/31.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 214.42/31.58 % Starting ehoh_best2 with 1500s (5) cores
% 214.42/31.58 % Starting additional_ho_6 with 300s (1) cores
% 214.42/31.58 % Starting new_bool_5 with 300s (1) cores
% 214.42/31.58 % Starting new_bool_1 with 300s (1) cores
% 214.42/31.58 % new_bool_5 with pid 3333228 completed with status 0
% 214.42/31.58 % Result found by new_bool_5
% 214.42/31.58 % Preprocessing class: HSLSSMSMSSMNHSA.
% 214.42/31.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 214.42/31.58 % Starting ehoh_best2 with 1500s (5) cores
% 214.42/31.58 % Starting additional_ho_6 with 300s (1) cores
% 214.42/31.58 % Starting new_bool_5 with 300s (1) cores
% 214.42/31.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1.0,,1,20000,1.0))
% 214.42/31.58 % SinE strategy is GSinE(CountFormulas,hypos,1.0,,1,20000,1.0)
% 214.42/31.58 % Search class: HGHSM-FFLM32-MHSFFFNN
% 214.42/31.58 % partial match(2): HGHSM-FSLM32-MHSFFFBN
% 214.42/31.58 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 214.42/31.58 % Starting SubtermCWHack with 28s (1) cores
% 214.42/31.58 % SubtermCWHack with pid 3333230 completed with status 8
% 214.42/31.58 % Starting new_bool_5 with 31s (1) cores
% 214.42/31.58 % new_bool_5 with pid 3333255 completed with status 0
% 214.42/31.58 % Result found by new_bool_5
% 214.42/31.58 % Preprocessing class: HSLSSMSMSSMNHSA.
% 214.42/31.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 214.42/31.58 % Starting ehoh_best2 with 1500s (5) cores
% 214.42/31.58 % Starting additional_ho_6 with 300s (1) cores
% 214.42/31.58 % Starting new_bool_5 with 300s (1) cores
% 214.42/31.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1.0,,1,20000,1.0))
% 214.42/31.58 % SinE strategy is GSinE(CountFormulas,hypos,1.0,,1,20000,1.0)
% 214.42/31.58 % Search class: HGHSM-FFLM32-MHSFFFNN
% 214.42/31.58 % partial match(2): HGHSM-FSLM32-MHSFFFBN
% 214.42/31.58 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 214.42/31.58 % Starting SubtermCWHack with 28s (1) cores
% 214.42/31.58 % SubtermCWHack with pid 3333230 completed with status 8
% 214.42/31.58 % Starting new_bool_5 with 31s (1) cores
% 214.42/31.58 % Preprocessing time : 0.004 s
% 214.42/31.58 % Presaturation interreduction done
% 214.42/31.58
% 214.42/31.58 % Proof found!
% 214.42/31.58 % SZS status Theorem
% 214.42/31.58 % SZS output start CNFRefutation
% See solution above
% 214.42/31.58 % Parsed axioms : 395
% 214.42/31.58 % Removed by relevancy pruning/SinE : 307
% 214.42/31.58 % Initial clauses : 127
% 214.42/31.58 % Removed in clause preprocessing : 5
% 214.42/31.58 % Initial clauses in saturation : 122
% 214.42/31.58 % Processed clauses : 3578
% 214.42/31.58 % ...of these trivial : 281
% 214.42/31.58 % ...subsumed : 1755
% 214.42/31.58 % ...remaining for further processing : 1542
% 214.42/31.58 % Other redundant clauses eliminated : 629
% 214.42/31.58 % Clauses deleted for lack of memory : 0
% 214.42/31.58 % Backward-subsumed : 32
% 214.42/31.58 % Backward-rewritten : 75
% 214.42/31.58 % Generated clauses : 100353
% 214.42/31.58 % ...of the previous two non-redundant : 86452
% 214.42/31.58 % ...aggressively subsumed : 0
% 214.42/31.58 % Contextual simplify-reflections : 46
% 214.42/31.58 % Paramodulations : 99238
% 214.42/31.58 % Factorizations : 20
% 214.42/31.58 % NegExts : 150
% 214.42/31.58 % Equation resolutions : 641
% 214.42/31.58 % Disequality decompositions : 0
% 214.42/31.58 % Total rewrite steps : 28049
% 214.42/31.58 % ...of those cached : 27296
% 214.42/31.58 % Propositional unsat checks : 0
% 214.42/31.58 % Propositional check models : 0
% 214.42/31.58 % Propositional check unsatisfiable : 0
% 214.42/31.58 % Propositional clauses : 0
% 214.42/31.58 % Propositional clauses after purity: 0
% 214.42/31.58 % Propositional unsat core size : 0
% 214.42/31.58 % Propositional preprocessing time : 0.000
% 214.42/31.58 % Propositional encoding time : 0.000
% 214.42/31.58 % Propositional solver time : 0.000
% 214.42/31.58 % Success case prop preproc time : 0.000
% 214.42/31.58 % Success case prop encoding time : 0.000
% 214.42/31.58 % Success case prop solver time : 0.000
% 214.42/31.58 % Current number of processed clauses : 1326
% 214.42/31.58 % Positive orientable unit clauses : 200
% 214.42/31.58 % Positive unorientable unit clauses: 0
% 214.42/31.58 % Negative unit clauses : 104
% 214.42/31.58 % Non-unit-clauses : 1022
% 214.42/31.58 % Current number of unprocessed clauses: 82486
% 214.42/31.58 % ...number of literals in the above : 248215
% 214.42/31.58 % Current number of archived formulas : 0
% 214.42/31.58 % Current number of archived clauses : 210
% 214.42/31.58 % Clause-clause subsumption calls (NU) : 213476
% 214.42/31.58 % Rec. Clause-clause subsumption calls : 91086
% 214.42/31.58 % Non-unit clause-clause subsumptions : 773
% 214.42/31.58 % Unit Clause-clause subsumption calls : 19202
% 214.42/31.58 % Rewrite failures with RHS unbound : 0
% 214.42/31.58 % BW rewrite match attempts : 565
% 214.42/31.58 % BW rewrite match successes : 21
% 214.42/31.58 % Condensation attempts : 3578
% 214.42/31.58 % Condensation successes : 2
% 214.42/31.58 % Termbank termtop insertions : 1793461
% 214.42/31.58 % Search garbage collected termcells : 4127
% 214.42/31.58
% 214.42/31.58 % -------------------------------------------------
% 214.42/31.58 % User time : 29.370 s
% 214.42/31.58 % System time : 1.021 s
% 214.42/31.58 % Total time : 30.390 s
% 214.42/31.58 % Maximum resident set size: 4472 pages
% 214.42/31.58
% 214.42/31.58 % -------------------------------------------------
% 214.42/31.58 % User time : 29.382 s
% 214.42/31.58 % System time : 1.029 s
% 214.42/31.58 % Total time : 30.410 s
% 214.42/31.58 % Maximum resident set size: 5376 pages
% 214.42/31.58 % E exiting
%------------------------------------------------------------------------------