%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP021^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:06 AM UTC 2026
% Result : Theorem 38.92s 30.93s
% Output : CNFRefutation 38.92s
% 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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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/sandbox/tmp/tmp.ElVHMWwPY3/E---3.1_254946.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__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_25,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_26,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_21,c_0_24]) ).
thf(c_0_27,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_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_25,c_0_26]) ).
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_27,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_25,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_24]) ).
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 @ 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_39,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_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.03 % Problem : ITP021^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n009.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 19:34:32 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
% 11.36/11.46 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.ElVHMWwPY3/E---3.1_254946.p
% 38.92/30.93 % Version: 3.5.1-ho
% 38.92/30.93 % partial match(3): HMLMSLSLSSSCHFA
% 38.92/30.93 % Preprocessing class: HMLLMLLLSSSCHFA.
% 38.92/30.93 % Scheduled 4 strats onto 8 cores with 284 seconds (2272 total)
% 38.92/30.93 % Starting new_ho_2 with 1136s (4) cores
% 38.92/30.93 % Starting sh3l with 568s (2) cores
% 38.92/30.93 % Starting lpo5_rw_fix with 284s (1) cores
% 38.92/30.93 % Starting full_lambda_7 with 284s (1) cores
% 38.92/30.93 % sh3l with pid 255199 completed with status 0
% 38.92/30.93 % Result found by sh3l
% 38.92/30.93 % partial match(3): HMLMSLSLSSSCHFA
% 38.92/30.93 % Preprocessing class: HMLLMLLLSSSCHFA.
% 38.92/30.93 % Scheduled 4 strats onto 8 cores with 284 seconds (2272 total)
% 38.92/30.93 % Starting new_ho_2 with 1136s (4) cores
% 38.92/30.93 % Starting sh3l with 568s (2) cores
% 38.92/30.93 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 38.92/30.93 % SinE strategy is gf120_gu_RUU_F100_L01000
% 38.92/30.93 % Search class: HGHSM-SMLM32-DHFFFSBN
% 38.92/30.93 % Scheduled 7 strats onto 2 cores with 567 seconds (567 total)
% 38.92/30.93 % Starting SubtermCWHack with 52s (1) cores
% 38.92/30.93 % Starting sh3l with 57s (1) cores
% 38.92/30.93 % SubtermCWHack with pid 255205 completed with status 0
% 38.92/30.93 % Result found by SubtermCWHack
% 38.92/30.93 % partial match(3): HMLMSLSLSSSCHFA
% 38.92/30.93 % Preprocessing class: HMLLMLLLSSSCHFA.
% 38.92/30.93 % Scheduled 4 strats onto 8 cores with 284 seconds (2272 total)
% 38.92/30.93 % Starting new_ho_2 with 1136s (4) cores
% 38.92/30.93 % Starting sh3l with 568s (2) cores
% 38.92/30.93 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 38.92/30.93 % SinE strategy is gf120_gu_RUU_F100_L01000
% 38.92/30.93 % Search class: HGHSM-SMLM32-DHFFFSBN
% 38.92/30.93 % Scheduled 7 strats onto 2 cores with 567 seconds (567 total)
% 38.92/30.93 % Starting SubtermCWHack with 52s (1) cores
% 38.92/30.93 % Preprocessing time : 0.108 s
% 38.92/30.93
% 38.92/30.93 % Proof found!
% 38.92/30.93 % SZS status Theorem
% 38.92/30.93 % SZS output start CNFRefutation
% See solution above
% 38.92/30.93 % Parsed axioms : 73510
% 38.92/30.93 % Removed by relevancy pruning/SinE : 72509
% 38.92/30.93 % Initial clauses : 1876
% 38.92/30.93 % Removed in clause preprocessing : 93
% 38.92/30.93 % Initial clauses in saturation : 1783
% 38.92/30.93 % Processed clauses : 3866
% 38.92/30.93 % ...of these trivial : 351
% 38.92/30.93 % ...subsumed : 2534
% 38.92/30.93 % ...remaining for further processing : 981
% 38.92/30.93 % Other redundant clauses eliminated : 38
% 38.92/30.93 % Clauses deleted for lack of memory : 0
% 38.92/30.93 % Backward-subsumed : 63
% 38.92/30.93 % Backward-rewritten : 87
% 38.92/30.93 % Generated clauses : 15429
% 38.92/30.93 % ...of the previous two non-redundant : 10740
% 38.92/30.93 % ...aggressively subsumed : 0
% 38.92/30.93 % Contextual simplify-reflections : 3
% 38.92/30.93 % Paramodulations : 15349
% 38.92/30.93 % Factorizations : 36
% 38.92/30.93 % NegExts : 0
% 38.92/30.93 % Equation resolutions : 44
% 38.92/30.93 % Disequality decompositions : 0
% 38.92/30.93 % Total rewrite steps : 8506
% 38.92/30.93 % ...of those cached : 7462
% 38.92/30.93 % Propositional unsat checks : 0
% 38.92/30.93 % Propositional check models : 0
% 38.92/30.93 % Propositional check unsatisfiable : 0
% 38.92/30.93 % Propositional clauses : 0
% 38.92/30.93 % Propositional clauses after purity: 0
% 38.92/30.93 % Propositional unsat core size : 0
% 38.92/30.93 % Propositional preprocessing time : 0.000
% 38.92/30.93 % Propositional encoding time : 0.000
% 38.92/30.93 % Propositional solver time : 0.000
% 38.92/30.93 % Success case prop preproc time : 0.000
% 38.92/30.93 % Success case prop encoding time : 0.000
% 38.92/30.93 % Success case prop solver time : 0.000
% 38.92/30.93 % Current number of processed clauses : 805
% 38.92/30.93 % Positive orientable unit clauses : 221
% 38.92/30.93 % Positive unorientable unit clauses: 9
% 38.92/30.93 % Negative unit clauses : 125
% 38.92/30.93 % Non-unit-clauses : 450
% 38.92/30.93 % Current number of unprocessed clauses: 8395
% 38.92/30.93 % ...number of literals in the above : 20569
% 38.92/30.93 % Current number of archived formulas : 0
% 38.92/30.93 % Current number of archived clauses : 150
% 38.92/30.93 % Clause-clause subsumption calls (NU) : 72357
% 38.92/30.93 % Rec. Clause-clause subsumption calls : 61102
% 38.92/30.93 % Non-unit clause-clause subsumptions : 1323
% 38.92/30.93 % Unit Clause-clause subsumption calls : 9291
% 38.92/30.93 % Rewrite failures with RHS unbound : 46
% 38.92/30.93 % BW rewrite match attempts : 411
% 38.92/30.93 % BW rewrite match successes : 81
% 38.92/30.93 % Condensation attempts : 0
% 38.92/30.93 % Condensation successes : 0
% 38.92/30.93 % Termbank termtop insertions : 2747125
% 38.92/30.93 % Search garbage collected termcells : 521995
% 38.92/30.93
% 38.92/30.93 % -------------------------------------------------
% 38.92/30.93 % User time : 2.924 s
% 38.92/30.93 % System time : 0.320 s
% 38.92/30.93 % Total time : 3.244 s
% 38.92/30.93 % Maximum resident set size: 145600 pages
% 38.92/30.93
% 38.92/30.93 % -------------------------------------------------
% 38.92/30.93 % User time : 20.124 s
% 38.92/30.93 % System time : 0.757 s
% 38.92/30.93 % Total time : 20.881 s
% 38.92/30.93 % Maximum resident set size: 126340 pages
% 38.92/30.93 % E exiting
%------------------------------------------------------------------------------