%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP146^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 2.35s 0.67s
% Output : CNFRefutation 2.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 19
% Syntax : Number of formulae : 82 ( 63 unt; 0 typ; 0 def)
% Number of atoms : 104 ( 68 equ; 0 cnn)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 789 ( 21 ~; 15 |; 0 &; 746 @)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 17 ( 15 usr; 8 con; 0-4 aty)
% Number of variables : 121 ( 2 ^; 119 !; 0 ?; 121 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
set_real: $tType ).
thf(decl_sort2,type,
a: $tType ).
thf(decl_sort3,type,
set_a: $tType ).
thf(decl_sort4,type,
real: $tType ).
thf(decl_23,type,
auto_l612940ivl0_a: ( a > a ) > set_a > a > set_real ).
thf(decl_24,type,
auto_ll_on_flow0_a: ( a > a ) > set_a > a > real > a ).
thf(decl_25,type,
minus_minus_real: real > real > real ).
thf(decl_27,type,
plus_plus_real: real > real > real ).
thf(decl_29,type,
uminus_uminus_a_a: ( a > a ) > a > a ).
thf(decl_30,type,
uminus_uminus_real: real > real ).
thf(decl_32,type,
zero_zero_real: real ).
thf(decl_33,type,
zero_zero_a: a ).
thf(decl_44,type,
member_real: real > set_real > $o ).
thf(decl_46,type,
x: set_a ).
thf(decl_48,type,
f: a > a ).
thf(decl_51,type,
ss: real ).
thf(decl_53,type,
tt: real ).
thf(decl_54,type,
x2: a ).
thf(decl_55,type,
xx: a ).
thf(fact_57_rev__eq__flow,axiom,
! [X7: a,X2: real] :
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ X7 @ X2 )
= ( auto_ll_on_flow0_a @ f @ x @ X7 @ ( uminus_uminus_real @ X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_57_rev__eq__flow) ).
thf(fact_29_diff__0,axiom,
! [X10: real] :
( ( minus_minus_real @ zero_zero_real @ X10 )
= ( uminus_uminus_real @ X10 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_29_diff__0) ).
thf(fact_335_add__diff__eq,axiom,
! [X270: real,X271: real,X272: real] :
( ( plus_plus_real @ X270 @ ( minus_minus_real @ X271 @ X272 ) )
= ( minus_minus_real @ ( plus_plus_real @ X270 @ X271 ) @ X272 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_335_add__diff__eq) ).
thf(fact_333_diff__diff__eq2,axiom,
! [X267: real,X268: real,X269: real] :
( ( minus_minus_real @ X267 @ ( minus_minus_real @ X268 @ X269 ) )
= ( minus_minus_real @ ( plus_plus_real @ X267 @ X269 ) @ X268 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_333_diff__diff__eq2) ).
thf(fact_33_local_Oflows__reverse,axiom,
! [X2: real,X4: a] :
( ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X4 ) )
=> ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X4 @ X2 ) @ ( minus_minus_real @ zero_zero_real @ X2 ) )
= X4 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_33_local_Oflows__reverse) ).
thf(fact_34_local_Oexistence__ivl__reverse,axiom,
! [X2: real,X4: a] :
( ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X4 ) )
=> ( member_real @ ( minus_minus_real @ zero_zero_real @ X2 ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X4 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_34_local_Oexistence__ivl__reverse) ).
thf(fact_202_add__diff__cancel__right,axiom,
! [X108: real,X109: real,X110: real] :
( ( minus_minus_real @ ( plus_plus_real @ X108 @ X109 ) @ ( plus_plus_real @ X110 @ X109 ) )
= ( minus_minus_real @ X108 @ X110 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_202_add__diff__cancel__right) ).
thf(fact_329_diff__add__eq__diff__diff__swap,axiom,
! [X261: real,X262: real,X263: real] :
( ( minus_minus_real @ X261 @ ( plus_plus_real @ X262 @ X263 ) )
= ( minus_minus_real @ ( minus_minus_real @ X261 @ X263 ) @ X262 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_329_diff__add__eq__diff__diff__swap) ).
thf(fact_105_diff__self,axiom,
! [X40: real] :
( ( minus_minus_real @ X40 @ X40 )
= zero_zero_real ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_105_diff__self) ).
thf(fact_159_local_Oflow__trans,axiom,
! [X29: real,X4: a,X2: real] :
( ( member_real @ X29 @ ( auto_l612940ivl0_a @ f @ x @ X4 ) )
=> ( ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X4 @ X29 ) ) )
=> ( ( auto_ll_on_flow0_a @ f @ x @ X4 @ ( plus_plus_real @ X29 @ X2 ) )
= ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X4 @ X29 ) @ X2 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_159_local_Oflow__trans) ).
thf(fact_2_eq,axiom,
( ( auto_ll_on_flow0_a @ f @ x @ xx @ tt )
= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ss ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_2_eq) ).
thf(fact_5_ss__ex,axiom,
member_real @ ss @ ( auto_l612940ivl0_a @ f @ x @ x2 ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_5_ss__ex) ).
thf(conj_0,conjecture,
( xx
= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ( minus_minus_real @ ss @ tt ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',conj_0) ).
thf(fact_275_add_Ocommute,axiom,
( plus_plus_real
= ( ^ [X180: real,X181: real] : ( plus_plus_real @ X181 @ X180 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_275_add_Ocommute) ).
thf(fact_4_tt__ex,axiom,
member_real @ tt @ ( auto_l612940ivl0_a @ f @ x @ xx ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_4_tt__ex) ).
thf(fact_208_diff__add__cancel,axiom,
! [X116: real,X117: real] :
( ( plus_plus_real @ ( minus_minus_real @ X116 @ X117 ) @ X117 )
= X116 ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_208_diff__add__cancel) ).
thf(fact_11_general_Oflows__reverse,axiom,
! [X2: real,X3: real,X4: a] :
( ( member_real @ ( minus_minus_real @ X2 @ X3 ) @ ( auto_l612940ivl0_a @ f @ x @ X4 ) )
=> ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X4 @ ( minus_minus_real @ X2 @ X3 ) ) @ ( minus_minus_real @ X3 @ X2 ) )
= X4 ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_11_general_Oflows__reverse) ).
thf(fact_18_local_Oflow__undefined0,axiom,
! [X2: real,X1: a] :
( ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) )
=> ( ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 )
= zero_zero_a ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_18_local_Oflow__undefined0) ).
thf(fact_7_neg__tt__ex,axiom,
member_real @ ( uminus_uminus_real @ tt ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) ),
file('/export/starexec/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p',fact_7_neg__tt__ex) ).
thf(c_0_19,plain,
! [X1102: a,X1103: real] :
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ X1102 @ X1103 )
= ( auto_ll_on_flow0_a @ f @ x @ X1102 @ ( uminus_uminus_real @ X1103 ) ) ),
inference(variable_rename,[status(thm)],[fact_57_rev__eq__flow]) ).
thf(c_0_20,plain,
! [X1056: real] :
( ( minus_minus_real @ zero_zero_real @ X1056 )
= ( uminus_uminus_real @ X1056 ) ),
inference(variable_rename,[status(thm)],[fact_29_diff__0]) ).
thf(c_0_21,plain,
! [X1707: real,X1708: real,X1709: real] :
( ( plus_plus_real @ X1707 @ ( minus_minus_real @ X1708 @ X1709 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1707 @ X1708 ) @ X1709 ) ),
inference(variable_rename,[status(thm)],[fact_335_add__diff__eq]) ).
thf(c_0_22,plain,
! [X1701: real,X1702: real,X1703: real] :
( ( minus_minus_real @ X1701 @ ( minus_minus_real @ X1702 @ X1703 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1701 @ X1703 ) @ X1702 ) ),
inference(variable_rename,[status(thm)],[fact_333_diff__diff__eq2]) ).
thf(c_0_23,plain,
! [X1063: real,X1064: a] :
( ~ ( member_real @ X1063 @ ( auto_l612940ivl0_a @ f @ x @ X1064 ) )
| ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1064 @ X1063 ) @ ( minus_minus_real @ zero_zero_real @ X1063 ) )
= X1064 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_33_local_Oflows__reverse])])]) ).
thf(c_0_24,plain,
! [X1: a,X2: real] :
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ X1 @ X2 )
= ( auto_ll_on_flow0_a @ f @ x @ X1 @ ( uminus_uminus_real @ X2 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
thf(c_0_25,plain,
! [X2: real] :
( ( minus_minus_real @ zero_zero_real @ X2 )
= ( uminus_uminus_real @ X2 ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_26,plain,
! [X2: real,X3: real,X5: real] :
( ( plus_plus_real @ X2 @ ( minus_minus_real @ X3 @ X5 ) )
= ( minus_minus_real @ ( plus_plus_real @ X2 @ X3 ) @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
thf(c_0_27,plain,
! [X2: real,X5: real,X3: real] :
( ( minus_minus_real @ X2 @ ( minus_minus_real @ X3 @ X5 ) )
= ( minus_minus_real @ ( plus_plus_real @ X2 @ X5 ) @ X3 ) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
thf(c_0_28,plain,
! [X1065: real,X1066: a] :
( ~ ( member_real @ X1065 @ ( auto_l612940ivl0_a @ f @ x @ X1066 ) )
| ( member_real @ ( minus_minus_real @ zero_zero_real @ X1065 ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1066 @ X1065 ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_34_local_Oexistence__ivl__reverse])])]) ).
thf(c_0_29,plain,
! [X2: real,X1: a] :
( ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 ) @ ( minus_minus_real @ zero_zero_real @ X2 ) )
= X1 )
| ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
thf(c_0_30,plain,
! [X1: a,X2: real] :
( ( auto_ll_on_flow0_a @ f @ x @ X1 @ ( minus_minus_real @ zero_zero_real @ X2 ) )
= ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ X1 @ X2 ) ),
inference(rw,[status(thm)],[c_0_24,c_0_25]) ).
thf(c_0_31,plain,
! [X1389: real,X1390: real,X1391: real] :
( ( minus_minus_real @ ( plus_plus_real @ X1389 @ X1390 ) @ ( plus_plus_real @ X1391 @ X1390 ) )
= ( minus_minus_real @ X1389 @ X1391 ) ),
inference(variable_rename,[status(thm)],[fact_202_add__diff__cancel__right]) ).
thf(c_0_32,plain,
! [X2: real,X5: real,X3: real] :
( ( minus_minus_real @ X2 @ ( minus_minus_real @ X3 @ X5 ) )
= ( plus_plus_real @ X2 @ ( minus_minus_real @ X5 @ X3 ) ) ),
inference(rw,[status(thm)],[c_0_26,c_0_27]) ).
thf(c_0_33,plain,
! [X1689: real,X1690: real,X1691: real] :
( ( minus_minus_real @ X1689 @ ( plus_plus_real @ X1690 @ X1691 ) )
= ( minus_minus_real @ ( minus_minus_real @ X1689 @ X1691 ) @ X1690 ) ),
inference(variable_rename,[status(thm)],[fact_329_diff__add__eq__diff__diff__swap]) ).
thf(c_0_34,plain,
! [X1197: real] :
( ( minus_minus_real @ X1197 @ X1197 )
= zero_zero_real ),
inference(variable_rename,[status(thm)],[fact_105_diff__self]) ).
thf(c_0_35,plain,
! [X1290: real,X1291: a,X1292: real] :
( ~ ( member_real @ X1290 @ ( auto_l612940ivl0_a @ f @ x @ X1291 ) )
| ~ ( member_real @ X1292 @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1291 @ X1290 ) ) )
| ( ( auto_ll_on_flow0_a @ f @ x @ X1291 @ ( plus_plus_real @ X1290 @ X1292 ) )
= ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1291 @ X1290 ) @ X1292 ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_159_local_Oflow__trans])])]) ).
thf(c_0_36,plain,
! [X2: real,X1: a] :
( ( member_real @ ( minus_minus_real @ zero_zero_real @ X2 ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 ) ) )
| ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
thf(c_0_37,plain,
( ( auto_ll_on_flow0_a @ f @ x @ xx @ tt )
= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ss ) ),
inference(split_conjunct,[status(thm)],[fact_2_eq]) ).
thf(c_0_38,plain,
member_real @ ss @ ( auto_l612940ivl0_a @ f @ x @ x2 ),
inference(split_conjunct,[status(thm)],[fact_5_ss__ex]) ).
thf(c_0_39,plain,
! [X2: real,X1: a] :
( ( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 ) @ X2 )
= X1 )
| ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) ) ),
inference(rw,[status(thm)],[c_0_29,c_0_30]) ).
thf(c_0_40,plain,
! [X2: real,X3: real,X5: real] :
( ( minus_minus_real @ ( plus_plus_real @ X2 @ X3 ) @ ( plus_plus_real @ X5 @ X3 ) )
= ( minus_minus_real @ X2 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_41,plain,
! [X2: real,X3: real,X5: real] :
( ( minus_minus_real @ ( plus_plus_real @ X2 @ X3 ) @ X5 )
= ( plus_plus_real @ X2 @ ( minus_minus_real @ X3 @ X5 ) ) ),
inference(rw,[status(thm)],[c_0_27,c_0_32]) ).
thf(c_0_42,plain,
! [X2: real,X5: real,X3: real] :
( ( minus_minus_real @ X2 @ ( plus_plus_real @ X3 @ X5 ) )
= ( minus_minus_real @ ( minus_minus_real @ X2 @ X5 ) @ X3 ) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_43,plain,
! [X2: real] :
( ( minus_minus_real @ X2 @ X2 )
= zero_zero_real ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
thf(c_0_44,negated_conjecture,
( xx
!= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ( minus_minus_real @ ss @ tt ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(c_0_45,plain,
! [X1007: real,X1008: real] :
( ( plus_plus_real @ X1007 @ X1008 )
= ( plus_plus_real @ X1008 @ X1007 ) ),
inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_275_add_Ocommute])]) ).
thf(c_0_46,plain,
! [X3: real,X1: a,X2: real] :
( ( ( auto_ll_on_flow0_a @ f @ x @ X1 @ ( plus_plus_real @ X2 @ X3 ) )
= ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 ) @ X3 ) )
| ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) )
| ~ ( member_real @ X3 @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
thf(c_0_47,plain,
member_real @ ( minus_minus_real @ zero_zero_real @ ss ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_38])]) ).
thf(c_0_48,plain,
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) @ ss )
= x2 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_37]),c_0_38])]) ).
thf(c_0_49,plain,
member_real @ tt @ ( auto_l612940ivl0_a @ f @ x @ xx ),
inference(split_conjunct,[status(thm)],[fact_4_tt__ex]) ).
thf(c_0_50,plain,
! [X2: real,X3: real,X5: real] :
( ( plus_plus_real @ X2 @ ( minus_minus_real @ X3 @ ( plus_plus_real @ X5 @ X3 ) ) )
= ( minus_minus_real @ X2 @ X5 ) ),
inference(rw,[status(thm)],[c_0_40,c_0_41]) ).
thf(c_0_51,plain,
! [X2: real,X3: real] :
( ( minus_minus_real @ X2 @ ( plus_plus_real @ X3 @ X2 ) )
= ( minus_minus_real @ zero_zero_real @ X3 ) ),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
thf(c_0_52,negated_conjecture,
( xx
!= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ( minus_minus_real @ ss @ tt ) ) ),
inference(fof_simplification,[status(thm)],[c_0_44]) ).
thf(c_0_53,plain,
! [X1404: real,X1405: real] :
( ( plus_plus_real @ ( minus_minus_real @ X1404 @ X1405 ) @ X1405 )
= X1404 ),
inference(variable_rename,[status(thm)],[fact_208_diff__add__cancel]) ).
thf(c_0_54,plain,
! [X1540: real,X1541: real] :
( ( plus_plus_real @ X1540 @ X1541 )
= ( plus_plus_real @ X1541 @ X1540 ) ),
inference(variable_rename,[status(thm)],[c_0_45]) ).
thf(c_0_55,plain,
! [X1020: real,X1021: real,X1022: a] :
( ~ ( member_real @ ( minus_minus_real @ X1020 @ X1021 ) @ ( auto_l612940ivl0_a @ f @ x @ X1022 ) )
| ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1022 @ ( minus_minus_real @ X1020 @ X1021 ) ) @ ( minus_minus_real @ X1021 @ X1020 ) )
= X1022 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_11_general_Oflows__reverse])])]) ).
thf(c_0_56,plain,
( ( auto_ll_on_flow0_a @ f @ x @ xx @ ( plus_plus_real @ tt @ ( minus_minus_real @ zero_zero_real @ ss ) ) )
= x2 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_47]),c_0_30]),c_0_48]),c_0_49])]) ).
thf(c_0_57,plain,
! [X2: real,X3: real] :
( ( plus_plus_real @ X2 @ ( minus_minus_real @ zero_zero_real @ X3 ) )
= ( minus_minus_real @ X2 @ X3 ) ),
inference(rw,[status(thm)],[c_0_50,c_0_51]) ).
thf(c_0_58,negated_conjecture,
( xx
!= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ( minus_minus_real @ ss @ tt ) ) ),
inference(fof_nnf,[status(thm)],[c_0_52]) ).
thf(c_0_59,plain,
! [X2: real,X1: a] :
( ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) )
=> ( ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 )
= zero_zero_a ) ),
inference(fof_simplification,[status(thm)],[fact_18_local_Oflow__undefined0]) ).
thf(c_0_60,plain,
member_real @ ( uminus_uminus_real @ tt ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) ),
inference(split_conjunct,[status(thm)],[fact_7_neg__tt__ex]) ).
thf(c_0_61,plain,
! [X3: real,X2: real] :
( ( plus_plus_real @ ( minus_minus_real @ X2 @ X3 ) @ X3 )
= X2 ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
thf(c_0_62,plain,
! [X3: real,X2: real] :
( ( plus_plus_real @ X2 @ X3 )
= ( plus_plus_real @ X3 @ X2 ) ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
thf(c_0_63,plain,
! [X2: real,X3: real,X1: a] :
( ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ X1 @ ( minus_minus_real @ X2 @ X3 ) ) @ ( minus_minus_real @ X3 @ X2 ) )
= X1 )
| ~ ( member_real @ ( minus_minus_real @ X2 @ X3 ) @ ( auto_l612940ivl0_a @ f @ x @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
thf(c_0_64,plain,
( ( auto_ll_on_flow0_a @ f @ x @ xx @ ( minus_minus_real @ tt @ ss ) )
= x2 ),
inference(rw,[status(thm)],[c_0_56,c_0_57]) ).
thf(c_0_65,negated_conjecture,
( xx
!= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ( minus_minus_real @ ss @ tt ) ) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
thf(c_0_66,plain,
! [X1034: real,X1035: a] :
( ( member_real @ X1034 @ ( auto_l612940ivl0_a @ f @ x @ X1035 ) )
| ( ( auto_ll_on_flow0_a @ f @ x @ X1035 @ X1034 )
= zero_zero_a ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_59])]) ).
thf(c_0_67,plain,
member_real @ ( minus_minus_real @ zero_zero_real @ tt ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) ),
inference(rw,[status(thm)],[c_0_60,c_0_25]) ).
thf(c_0_68,plain,
! [X2: real,X3: real] :
( ( plus_plus_real @ X2 @ ( minus_minus_real @ X3 @ X2 ) )
= X3 ),
inference(rw,[status(thm)],[c_0_61,c_0_62]) ).
thf(c_0_69,plain,
~ ( member_real @ ( minus_minus_real @ tt @ ss ) @ ( auto_l612940ivl0_a @ f @ x @ xx ) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_65]) ).
thf(c_0_70,plain,
! [X1: a,X2: real] :
( ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ X1 ) )
| ( ( auto_ll_on_flow0_a @ f @ x @ X1 @ X2 )
= zero_zero_a ) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
thf(c_0_71,plain,
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) @ tt )
= ( auto_ll_on_flow0_a @ f @ x @ xx @ zero_zero_real ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_67]),c_0_30]),c_0_68]),c_0_49])]) ).
thf(c_0_72,plain,
x2 = zero_zero_a,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_64]) ).
thf(c_0_73,plain,
( ( auto_ll_on_flow0_a @ f @ x @ xx @ zero_zero_real )
= xx ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_71]),c_0_49])]) ).
thf(c_0_74,plain,
! [X2: real] :
( ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) @ X2 )
= ( auto_ll_on_flow0_a @ f @ x @ x2 @ ( plus_plus_real @ ss @ X2 ) ) )
| ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_37]),c_0_38])]) ).
thf(c_0_75,plain,
( ( auto_ll_on_flow0_a @ f @ x @ xx @ tt )
= ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ss ) ),
inference(rw,[status(thm)],[c_0_37,c_0_72]) ).
thf(c_0_76,plain,
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ ( auto_ll_on_flow0_a @ f @ x @ xx @ tt ) @ tt )
= xx ),
inference(rw,[status(thm)],[c_0_71,c_0_73]) ).
thf(c_0_77,plain,
! [X2: real] :
( ( ( auto_ll_on_flow0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ss ) @ X2 )
= ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ( plus_plus_real @ ss @ X2 ) ) )
| ~ ( member_real @ X2 @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ss ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_74,c_0_72]),c_0_75]),c_0_75]) ).
thf(c_0_78,plain,
member_real @ ( minus_minus_real @ zero_zero_real @ tt ) @ ( auto_l612940ivl0_a @ f @ x @ ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ss ) ),
inference(spm,[status(thm)],[c_0_67,c_0_75]) ).
thf(c_0_79,plain,
( ( auto_ll_on_flow0_a @ ( uminus_uminus_a_a @ f ) @ x @ ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ss ) @ tt )
= xx ),
inference(rw,[status(thm)],[c_0_76,c_0_75]) ).
thf(c_0_80,negated_conjecture,
( ( auto_ll_on_flow0_a @ f @ x @ zero_zero_a @ ( minus_minus_real @ ss @ tt ) )
!= xx ),
inference(rw,[status(thm)],[c_0_65,c_0_72]) ).
thf(c_0_81,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78]),c_0_30]),c_0_79]),c_0_57]),c_0_80]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP146^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n017.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 19:56:07 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.27 Running higher-order theorem proving
% 0.27/0.32 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.Hu9uRHsDUq/E---3.1_821947.p
% 2.35/0.67 % Version: 3.5.1-ho
% 2.35/0.67 % Preprocessing class: HSLSSMSMSSMNSSA.
% 2.35/0.67 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.35/0.67 % Starting new_ho_10 with 900s (3) cores
% 2.35/0.67 % Starting sh1 with 900s (3) cores
% 2.35/0.67 % Starting sh8 with 300s (1) cores
% 2.35/0.67 % Starting new_bool_1 with 300s (1) cores
% 2.35/0.67 % new_ho_10 with pid 821963 completed with status 0
% 2.35/0.67 % Result found by new_ho_10
% 2.35/0.67 % Preprocessing class: HSLSSMSMSSMNSSA.
% 2.35/0.67 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.35/0.67 % Starting new_ho_10 with 900s (3) cores
% 2.35/0.67 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 2.35/0.67 % No SInE strategy applied
% 2.35/0.67 % Search class: HGHSM-FSLM31-MSSFFFBN
% 2.35/0.67 % Scheduled 6 strats onto 3 cores with 900 seconds (900 total)
% 2.35/0.67 % Starting SubtermCWHack with 91s (1) cores
% 2.35/0.67 % Starting new_ho_10 with 386s (1) cores
% 2.35/0.67 % Starting sh5l with 129s (1) cores
% 2.35/0.67 % new_ho_10 with pid 821970 completed with status 0
% 2.35/0.67 % Result found by new_ho_10
% 2.35/0.67 % Preprocessing class: HSLSSMSMSSMNSSA.
% 2.35/0.67 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.35/0.67 % Starting new_ho_10 with 900s (3) cores
% 2.35/0.67 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 2.35/0.67 % No SInE strategy applied
% 2.35/0.67 % Search class: HGHSM-FSLM31-MSSFFFBN
% 2.35/0.67 % Scheduled 6 strats onto 3 cores with 900 seconds (900 total)
% 2.35/0.67 % Starting SubtermCWHack with 91s (1) cores
% 2.35/0.67 % Starting new_ho_10 with 386s (1) cores
% 2.35/0.67 % Preprocessing time : 0.007 s
% 2.35/0.67 % Presaturation interreduction done
% 2.35/0.67
% 2.35/0.67 % Proof found!
% 2.35/0.67 % SZS status Theorem
% 2.35/0.67 % SZS output start CNFRefutation
% See solution above
% 2.35/0.67 % Parsed axioms : 380
% 2.35/0.67 % Removed by relevancy pruning/SinE : 0
% 2.35/0.67 % Initial clauses : 499
% 2.35/0.67 % Removed in clause preprocessing : 63
% 2.35/0.67 % Initial clauses in saturation : 436
% 2.35/0.67 % Processed clauses : 1936
% 2.35/0.67 % ...of these trivial : 96
% 2.35/0.67 % ...subsumed : 791
% 2.35/0.67 % ...remaining for further processing : 1049
% 2.35/0.67 % Other redundant clauses eliminated : 239
% 2.35/0.67 % Clauses deleted for lack of memory : 0
% 2.35/0.67 % Backward-subsumed : 72
% 2.35/0.67 % Backward-rewritten : 111
% 2.35/0.67 % Generated clauses : 10381
% 2.35/0.67 % ...of the previous two non-redundant : 8702
% 2.35/0.67 % ...aggressively subsumed : 0
% 2.35/0.67 % Contextual simplify-reflections : 9
% 2.35/0.67 % Paramodulations : 10116
% 2.35/0.67 % Factorizations : 5
% 2.35/0.67 % NegExts : 0
% 2.35/0.67 % Equation resolutions : 256
% 2.35/0.67 % Disequality decompositions : 0
% 2.35/0.67 % Total rewrite steps : 8188
% 2.35/0.67 % ...of those cached : 6691
% 2.35/0.67 % Propositional unsat checks : 0
% 2.35/0.67 % Propositional check models : 0
% 2.35/0.67 % Propositional check unsatisfiable : 0
% 2.35/0.67 % Propositional clauses : 0
% 2.35/0.67 % Propositional clauses after purity: 0
% 2.35/0.67 % Propositional unsat core size : 0
% 2.35/0.67 % Propositional preprocessing time : 0.000
% 2.35/0.67 % Propositional encoding time : 0.000
% 2.35/0.67 % Propositional solver time : 0.000
% 2.35/0.67 % Success case prop preproc time : 0.000
% 2.35/0.67 % Success case prop encoding time : 0.000
% 2.35/0.67 % Success case prop solver time : 0.000
% 2.35/0.67 % Current number of processed clauses : 556
% 2.35/0.67 % Positive orientable unit clauses : 88
% 2.35/0.67 % Positive unorientable unit clauses: 6
% 2.35/0.67 % Negative unit clauses : 56
% 2.35/0.67 % Non-unit-clauses : 406
% 2.35/0.67 % Current number of unprocessed clauses: 7271
% 2.35/0.67 % ...number of literals in the above : 17102
% 2.35/0.67 % Current number of archived formulas : 0
% 2.35/0.67 % Current number of archived clauses : 442
% 2.35/0.67 % Clause-clause subsumption calls (NU) : 65828
% 2.35/0.67 % Rec. Clause-clause subsumption calls : 54522
% 2.35/0.67 % Non-unit clause-clause subsumptions : 603
% 2.35/0.67 % Unit Clause-clause subsumption calls : 15375
% 2.35/0.67 % Rewrite failures with RHS unbound : 0
% 2.35/0.67 % BW rewrite match attempts : 494
% 2.35/0.67 % BW rewrite match successes : 185
% 2.35/0.67 % Condensation attempts : 1936
% 2.35/0.67 % Condensation successes : 10
% 2.35/0.67 % Termbank termtop insertions : 155082
% 2.35/0.67 % Search garbage collected termcells : 7482
% 2.35/0.67
% 2.35/0.67 % -------------------------------------------------
% 2.35/0.67 % User time : 0.306 s
% 2.35/0.67 % System time : 0.010 s
% 2.35/0.67 % Total time : 0.317 s
% 2.35/0.67 % Maximum resident set size: 5704 pages
% 2.35/0.67
% 2.35/0.67 % -------------------------------------------------
% 2.35/0.67 % User time : 0.872 s
% 2.35/0.67 % System time : 0.040 s
% 2.35/0.67 % Total time : 0.913 s
% 2.35/0.67 % Maximum resident set size: 5120 pages
% 2.35/0.67 % E exiting
%------------------------------------------------------------------------------