%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP021^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:05:16 AM UTC 2026
% Result : Theorem 68.79s 53.07s
% Output : CNFRefutation 68.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 44 ( 18 unt; 0 typ; 0 def)
% Number of atoms : 96 ( 13 equ; 0 cnn)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 302 ( 24 ~; 37 |; 10 &; 226 @)
% ( 4 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 7 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 59 ( 0 ^; 59 !; 0 ?; 59 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
mono_2Etyop_2Eextreal_2Eextreal: $tType ).
thf(decl_12822,type,
mono_2Ec_2Eextreal_2Eextreal__le: mono_2Etyop_2Eextreal_2Eextreal > mono_2Etyop_2Eextreal_2Eextreal > $o ).
thf(decl_12826,type,
mono_2Ec_2Eextreal_2Eextreal__max: mono_2Etyop_2Eextreal_2Eextreal > mono_2Etyop_2Eextreal_2Eextreal > mono_2Etyop_2Eextreal_2Eextreal ).
thf(decl_12939,type,
esk1_0: mono_2Etyop_2Eextreal_2Eextreal ).
thf(decl_12940,type,
esk2_0: mono_2Etyop_2Eextreal_2Eextreal ).
thf(decl_12941,type,
esk3_0: mono_2Etyop_2Eextreal_2Eextreal ).
thf(thm_2Eextreal_2Ele__max,axiom,
! [X49825: mono_2Etyop_2Eextreal_2Eextreal,X49826: mono_2Etyop_2Eextreal_2Eextreal,X49827: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ X49825 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X49826 @ X49827 ) )
<=> ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X49825 @ X49826 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X49825 @ X49827 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Ele__max) ).
thf(thm_2Eextreal_2Ele__refl,axiom,
! [X49271: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X49271 @ X49271 ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Ele__refl) ).
thf(thm_2Eextreal_2Ele__antisym,axiom,
! [X49291: mono_2Etyop_2Eextreal_2Eextreal,X49292: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X49291 @ X49292 )
& ( mono_2Ec_2Eextreal_2Eextreal__le @ X49292 @ X49291 ) )
<=> ( X49291 = X49292 ) ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Ele__antisym) ).
thf(thm_2Eextreal_2Ele__max1,axiom,
! [X49828: mono_2Etyop_2Eextreal_2Eextreal,X49829: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X49828 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X49828 @ X49829 ) ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Ele__max1) ).
thf(thm_2Eextreal_2Emax__le,conjecture,
! [X49832: mono_2Etyop_2Eextreal_2Eextreal,X49833: mono_2Etyop_2Eextreal_2Eextreal,X49834: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X49833 @ X49834 ) @ X49832 )
<=> ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X49833 @ X49832 )
& ( mono_2Ec_2Eextreal_2Eextreal__le @ X49834 @ X49832 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Emax__le) ).
thf(thm_2Eextreal_2Ele__max2,axiom,
! [X49830: mono_2Etyop_2Eextreal_2Eextreal,X49831: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X49831 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X49830 @ X49831 ) ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Ele__max2) ).
thf(thm_2Eextreal_2Ele__trans,axiom,
! [X49282: mono_2Etyop_2Eextreal_2Eextreal,X49283: mono_2Etyop_2Eextreal_2Eextreal,X49284: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X49282 @ X49283 )
& ( mono_2Ec_2Eextreal_2Eextreal__le @ X49283 @ X49284 ) )
=> ( mono_2Ec_2Eextreal_2Eextreal__le @ X49282 @ X49284 ) ),
file('/export/starexec/sandbox2/tmp/tmp.kDkZCkUJWN/E---3.1_3628051.p',thm_2Eextreal_2Ele__trans) ).
thf(c_0_7,plain,
! [X52486: mono_2Etyop_2Eextreal_2Eextreal,X52487: mono_2Etyop_2Eextreal_2Eextreal,X52488: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X52487 @ X52488 ) )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ X52487 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ X52488 ) )
& ( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ X52487 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X52487 @ X52488 ) ) )
& ( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ X52488 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X52486 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X52487 @ X52488 ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Eextreal_2Ele__max])])])]) ).
thf(c_0_8,plain,
! [X52475: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X52475 @ X52475 ),
inference(variable_rename,[status(thm)],[thm_2Eextreal_2Ele__refl]) ).
thf(c_0_9,plain,
! [X52479: mono_2Etyop_2Eextreal_2Eextreal,X52480: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52479 @ X52480 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52480 @ X52479 )
| ( X52479 = X52480 ) )
& ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X52479 @ X52480 )
| ( X52479 != X52480 ) )
& ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X52480 @ X52479 )
| ( X52479 != X52480 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Eextreal_2Ele__antisym])])])]) ).
thf(c_0_10,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal,X48760: mono_2Etyop_2Eextreal_2Eextreal,X48761: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48760 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48761 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48760 @ X48761 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
thf(c_0_11,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48682 ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
thf(c_0_12,plain,
! [X52489: mono_2Etyop_2Eextreal_2Eextreal,X52490: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X52489 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X52489 @ X52490 ) ),
inference(variable_rename,[status(thm)],[thm_2Eextreal_2Ele__max1]) ).
thf(c_0_13,negated_conjecture,
~ ! [X49832: mono_2Etyop_2Eextreal_2Eextreal,X49833: mono_2Etyop_2Eextreal_2Eextreal,X49834: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X49833 @ X49834 ) @ X49832 )
<=> ( ( mono_2Ec_2Eextreal_2Eextreal__le @ X49833 @ X49832 )
& ( mono_2Ec_2Eextreal_2Eextreal__le @ X49834 @ X49832 ) ) ),
inference(assume_negation,[status(cth)],[thm_2Eextreal_2Emax__le]) ).
thf(c_0_14,plain,
! [X48760: mono_2Etyop_2Eextreal_2Eextreal,X48682: mono_2Etyop_2Eextreal_2Eextreal] :
( ( X48682 = X48760 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48760 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48760 @ X48682 ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
thf(c_0_15,plain,
! [X48760: mono_2Etyop_2Eextreal_2Eextreal,X48682: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 ) @ X48760 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 ) @ X48682 ) ),
inference(spm,[status(thm)],[c_0_10,c_0_11]) ).
thf(c_0_16,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal,X48760: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 ) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_17,plain,
! [X52491: mono_2Etyop_2Eextreal_2Eextreal,X52492: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X52492 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X52491 @ X52492 ) ),
inference(variable_rename,[status(thm)],[thm_2Eextreal_2Ele__max2]) ).
thf(c_0_18,negated_conjecture,
( ( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 ) )
& ( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 ) )
& ( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])])]) ).
thf(c_0_19,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal,X48760: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 )
= X48682 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 ) @ X48760 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_15]),c_0_16])]) ).
thf(c_0_20,plain,
! [X48760: mono_2Etyop_2Eextreal_2Eextreal,X48682: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48760 @ X48682 ) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_21,negated_conjecture,
( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 ) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_22,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal,X48760: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 )
= X48682 )
| ( ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 )
= X48760 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_19]),c_0_20])]) ).
thf(c_0_23,plain,
! [X52476: mono_2Etyop_2Eextreal_2Eextreal,X52477: mono_2Etyop_2Eextreal_2Eextreal,X52478: mono_2Etyop_2Eextreal_2Eextreal] :
( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52476 @ X52477 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X52477 @ X52478 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X52476 @ X52478 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Eextreal_2Ele__trans])])]) ).
thf(c_0_24,negated_conjecture,
( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 ) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_25,negated_conjecture,
( ( ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 )
= esk2_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
thf(c_0_26,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal,X48760: mono_2Etyop_2Eextreal_2Eextreal,X48761: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48761 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48760 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48760 @ X48761 ) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
thf(c_0_27,negated_conjecture,
( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
thf(c_0_28,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal,X48760: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 )
= X48682 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ X48760 ) ),
inference(spm,[status(thm)],[c_0_16,c_0_22]) ).
thf(c_0_29,negated_conjecture,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ esk1_0 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ esk3_0 ) ),
inference(spm,[status(thm)],[c_0_26,c_0_27]) ).
thf(c_0_30,negated_conjecture,
( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk3_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_24,c_0_28]) ).
thf(c_0_31,negated_conjecture,
mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0,
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
thf(c_0_32,negated_conjecture,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ esk1_0 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ X48682 @ esk2_0 ) ),
inference(spm,[status(thm)],[c_0_26,c_0_31]) ).
thf(c_0_33,negated_conjecture,
( ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk2_0 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_25]) ).
thf(c_0_34,negated_conjecture,
( ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk1_0 )
| ~ ( mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0 ) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_35,negated_conjecture,
mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk1_0,
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
thf(c_0_36,negated_conjecture,
~ ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ esk2_0 @ esk3_0 ) @ esk1_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_31])]),c_0_35])]) ).
thf(c_0_37,plain,
! [X48760: mono_2Etyop_2Eextreal_2Eextreal,X48682: mono_2Etyop_2Eextreal_2Eextreal] :
( ( ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48760 )
= X48760 )
| ( mono_2Ec_2Eextreal_2Eextreal__le @ X48760 @ X48682 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_22]) ).
thf(c_0_38,negated_conjecture,
mono_2Ec_2Eextreal_2Eextreal__le @ esk2_0 @ esk3_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_28]),c_0_31])]) ).
thf(c_0_39,negated_conjecture,
mono_2Ec_2Eextreal_2Eextreal__le @ esk3_0 @ esk2_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_35])]) ).
thf(c_0_40,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal] : ( mono_2Ec_2Eextreal_2Eextreal__le @ ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48682 ) @ X48682 ),
inference(ef,[status(thm)],[c_0_15]) ).
thf(c_0_41,negated_conjecture,
esk3_0 = esk2_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_38]),c_0_39])]) ).
thf(c_0_42,plain,
! [X48682: mono_2Etyop_2Eextreal_2Eextreal] :
( ( mono_2Ec_2Eextreal_2Eextreal__max @ X48682 @ X48682 )
= X48682 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_40]),c_0_16])]) ).
thf(c_0_43,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_41]),c_0_42]),c_0_31])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP021^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.17 % Computer : n008.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Tue Sep 29 19:35:11 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running higher-order theorem proving
% 26.65/26.73 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.kDkZCkUJWN/E---3.1_3628051.p
% 68.79/53.07 % Version: 3.5.1-ho
% 68.79/53.07 % partial match(3): HMLMSLSLSSSCHFA
% 68.79/53.07 % Preprocessing class: HMLLMLLLSSSCHFA.
% 68.79/53.07 % Scheduled 4 strats onto 8 cores with 279 seconds (2232 total)
% 68.79/53.07 % Starting new_ho_2 with 1116s (4) cores
% 68.79/53.07 % Starting sh3l with 558s (2) cores
% 68.79/53.07 % Starting lpo5_rw_fix with 279s (1) cores
% 68.79/53.07 % Starting full_lambda_7 with 279s (1) cores
% 68.79/53.07 % sh3l with pid 3628321 completed with status 0
% 68.79/53.07 % Result found by sh3l
% 68.79/53.07 % partial match(3): HMLMSLSLSSSCHFA
% 68.79/53.07 % Preprocessing class: HMLLMLLLSSSCHFA.
% 68.79/53.07 % Scheduled 4 strats onto 8 cores with 279 seconds (2232 total)
% 68.79/53.07 % Starting new_ho_2 with 1116s (4) cores
% 68.79/53.07 % Starting sh3l with 558s (2) cores
% 68.79/53.07 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 68.79/53.07 % SinE strategy is gf120_gu_RUU_F100_L01000
% 68.79/53.07 % Search class: HGHSM-SMLM32-DHFFFSBN
% 68.79/53.07 % Scheduled 7 strats onto 2 cores with 556 seconds (556 total)
% 68.79/53.07 % Starting SubtermCWHack with 51s (1) cores
% 68.79/53.07 % Starting sh3l with 56s (1) cores
% 68.79/53.07 % SubtermCWHack with pid 3628325 completed with status 0
% 68.79/53.07 % Result found by SubtermCWHack
% 68.79/53.07 % partial match(3): HMLMSLSLSSSCHFA
% 68.79/53.07 % Preprocessing class: HMLLMLLLSSSCHFA.
% 68.79/53.07 % Scheduled 4 strats onto 8 cores with 279 seconds (2232 total)
% 68.79/53.07 % Starting new_ho_2 with 1116s (4) cores
% 68.79/53.07 % Starting sh3l with 558s (2) cores
% 68.79/53.07 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 68.79/53.07 % SinE strategy is gf120_gu_RUU_F100_L01000
% 68.79/53.07 % Search class: HGHSM-SMLM32-DHFFFSBN
% 68.79/53.07 % Scheduled 7 strats onto 2 cores with 556 seconds (556 total)
% 68.79/53.07 % Starting SubtermCWHack with 51s (1) cores
% 68.79/53.07 % Preprocessing time : 0.144 s
% 68.79/53.07
% 68.79/53.07 % Proof found!
% 68.79/53.07 % SZS status Theorem
% 68.79/53.07 % SZS output start CNFRefutation
% See solution above
% 68.79/53.07 % Parsed axioms : 73510
% 68.79/53.07 % Removed by relevancy pruning/SinE : 72509
% 68.79/53.07 % Initial clauses : 1876
% 68.79/53.07 % Removed in clause preprocessing : 93
% 68.79/53.07 % Initial clauses in saturation : 1783
% 68.79/53.07 % Processed clauses : 3858
% 68.79/53.07 % ...of these trivial : 354
% 68.79/53.07 % ...subsumed : 2524
% 68.79/53.07 % ...remaining for further processing : 980
% 68.79/53.07 % Other redundant clauses eliminated : 38
% 68.79/53.07 % Clauses deleted for lack of memory : 0
% 68.79/53.07 % Backward-subsumed : 62
% 68.79/53.07 % Backward-rewritten : 86
% 68.79/53.07 % Generated clauses : 15352
% 68.79/53.07 % ...of the previous two non-redundant : 10701
% 68.79/53.07 % ...aggressively subsumed : 0
% 68.79/53.07 % Contextual simplify-reflections : 3
% 68.79/53.07 % Paramodulations : 15272
% 68.79/53.07 % Factorizations : 36
% 68.79/53.07 % NegExts : 0
% 68.79/53.07 % Equation resolutions : 44
% 68.79/53.07 % Disequality decompositions : 0
% 68.79/53.07 % Total rewrite steps : 8453
% 68.79/53.07 % ...of those cached : 7411
% 68.79/53.07 % Propositional unsat checks : 0
% 68.79/53.07 % Propositional check models : 0
% 68.79/53.07 % Propositional check unsatisfiable : 0
% 68.79/53.07 % Propositional clauses : 0
% 68.79/53.07 % Propositional clauses after purity: 0
% 68.79/53.07 % Propositional unsat core size : 0
% 68.79/53.07 % Propositional preprocessing time : 0.000
% 68.79/53.07 % Propositional encoding time : 0.000
% 68.79/53.07 % Propositional solver time : 0.000
% 68.79/53.07 % Success case prop preproc time : 0.000
% 68.79/53.07 % Success case prop encoding time : 0.000
% 68.79/53.07 % Success case prop solver time : 0.000
% 68.79/53.07 % Current number of processed clauses : 806
% 68.79/53.07 % Positive orientable unit clauses : 223
% 68.79/53.07 % Positive unorientable unit clauses: 9
% 68.79/53.07 % Negative unit clauses : 125
% 68.79/53.07 % Non-unit-clauses : 449
% 68.79/53.07 % Current number of unprocessed clauses: 8373
% 68.79/53.07 % ...number of literals in the above : 20446
% 68.79/53.07 % Current number of archived formulas : 0
% 68.79/53.07 % Current number of archived clauses : 148
% 68.79/53.07 % Clause-clause subsumption calls (NU) : 71715
% 68.79/53.07 % Rec. Clause-clause subsumption calls : 60570
% 68.79/53.07 % Non-unit clause-clause subsumptions : 1303
% 68.79/53.07 % Unit Clause-clause subsumption calls : 9281
% 68.79/53.07 % Rewrite failures with RHS unbound : 46
% 68.79/53.07 % BW rewrite match attempts : 429
% 68.79/53.07 % BW rewrite match successes : 80
% 68.79/53.07 % Condensation attempts : 0
% 68.79/53.07 % Condensation successes : 0
% 68.79/53.07 % Termbank termtop insertions : 2746403
% 68.79/53.07 % Search garbage collected termcells : 521995
% 68.79/53.07
% 68.79/53.07 % -------------------------------------------------
% 68.79/53.07 % User time : 4.279 s
% 68.79/53.07 % System time : 0.462 s
% 68.79/53.07 % Total time : 4.742 s
% 68.79/53.07 % Maximum resident set size: 145856 pages
% 68.79/53.07
% 68.79/53.07 % -------------------------------------------------
% 68.79/53.07 % User time : 27.540 s
% 68.79/53.07 % System time : 0.962 s
% 68.79/53.07 % Total time : 28.501 s
% 68.79/53.07 % Maximum resident set size: 126348 pages
% 68.79/53.07 % E exiting
%------------------------------------------------------------------------------