%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP021^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:54:19 AM UTC 2026
% Result : Theorem 1.87s 1.55s
% Output : Refutation 1.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 15
% Syntax : Number of formulae : 149 ( 62 unt; 0 typ; 8 def)
% Number of atoms : 767 ( 198 equ; 0 cnn)
% Maximal formula atoms : 6 ( 5 avg)
% Number of connectives : 1104 ( 128 ~; 144 |; 57 &; 690 @)
% ( 17 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 28 ( 24 usr; 16 con; 0-4 aty)
% ( 58 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 179 ( 70 ^; 109 !; 0 ?; 179 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_6,type,
tyop_2Eextreal_2Eextreal: $tType ).
thf(func_def_0,type,
tyop_2Eextreal_2Eextreal: $tType ).
thf(func_def_1,type,
tyop_2Emin_2Ebool: $tType ).
thf(func_def_2,type,
tyop_2Emin_2Efun: ( $tType * $tType ) > $tType ).
thf(func_def_3,type,
c_2Ebool_2E_21:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_4,type,
c_2Ebool_2E_2F_5C: $o > $o > $o ).
thf(func_def_5,type,
c_2Emin_2E_3D:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_6,type,
c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
thf(func_def_7,type,
c_2Ebool_2E_3F:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_8,type,
c_2Ebool_2ECOND:
!>[X0: $tType] : ( $o > X0 > X0 > X0 ) ).
thf(func_def_11,type,
c_2Ebool_2E_5C_2F: $o > $o > $o ).
thf(func_def_12,type,
c_2Eextreal_2Eextreal__le: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > $o ).
thf(func_def_13,type,
c_2Eextreal_2Eextreal__max: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal ).
thf(func_def_14,type,
c_2Ebool_2E_7E: $o > $o ).
thf(func_def_31,type,
sK1: tyop_2Eextreal_2Eextreal ).
thf(func_def_32,type,
sK2: tyop_2Eextreal_2Eextreal ).
thf(func_def_33,type,
sK3: tyop_2Eextreal_2Eextreal ).
thf(f2038,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f1288,f1299,f1304,f1363,f1432,f1434,f1436,f1474,f1784,f1875,f1940,f2037]) ).
thf(f2037,plain,
( spl0_4
| ~ spl0_5
| spl0_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f2036]) ).
thf(f2036,plain,
( $false
| spl0_4
| ~ spl0_5
| spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f2035]) ).
thf(f2035,plain,
( ( $false = $true )
| spl0_4
| ~ spl0_5
| spl0_6 ),
inference(forward_demodulation,[status(thm)],[f2024,f1958]) ).
thf(f1958,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false )
| spl0_4
| ~ spl0_5 ),
inference(subsumption_resolution,[status(thm)],[f1952,f1283]) ).
thf(f1283,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $false )
| ~ spl0_5 ),
inference(avatar_component_clause,[status(thm)],[f1281]) ).
thf(f1281,definition,
( spl0_5
<=> ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition]) ).
thf(f1952,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
!= $false )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false )
| spl0_4 ),
inference(superposition,[status(thm)],[f1278,f1407]) ).
thf(f1407,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__max @ X2 @ X1 )
= X1 )
| ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
= $false ) ),
inference(forward_demodulation,[status(thm)],[f1398,f183]) ).
thf(f183,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1 )
= X2 ),
inference(equality_proxy_clausification,[status(thm)],[f181]) ).
thf(f181,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1 )
= X2 )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f179]) ).
thf(f179,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( ( ( c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1 )
= X2 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1 )
= X1 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f178]) ).
thf(f178,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( ^ [Y0: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ $true @ Y0 @ X1 )
= Y0 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y0 @ X1 )
= X1 ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f177]) ).
thf(f177,plain,
! [X0: $tType,X1: X0] :
( ( !! @ X0
@ ^ [Y0: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ $true @ Y0 @ X1 )
= Y0 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y0 @ X1 )
= X1 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f176]) ).
thf(f176,plain,
! [X0: $tType,X1: X0] :
( ( ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ $true @ Y1 @ Y0 )
= Y1 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0 )
= Y0 ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f138]) ).
thf(f138,plain,
! [X0: $tType] :
( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ $true @ Y1 @ Y0 )
= Y1 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0 )
= Y0 ) ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f117,f134]) ).
thf(f134,plain,
c_2Ebool_2ET = $true,
inference(cnf_transformation,[status(thm)],[f63]) ).
thf(f63,plain,
c_2Ebool_2ET = $true,
inference(fool_elimination,[status(thm)],[f62]) ).
thf(f62,plain,
c_2Ebool_2ET,
inference(rectify,[status(thm)],[f8]) ).
thf(f8,axiom,
c_2Ebool_2ET,
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Ebool_2ETRUTH) ).
thf(f117,plain,
! [X0: $tType] :
( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0 )
= Y1 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0 )
= Y0 ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f108]) ).
thf(f108,plain,
! [X0: $tType] :
( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0 )
= Y1 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0 )
= Y0 ) ) ) )
= $true ),
inference(closure,[status(thm)],[f91]) ).
thf(f91,plain,
! [X0: $tType] :
( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0 )
= Y1 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0 )
= Y0 ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f90]) ).
thf(f90,plain,
! [X0: $tType,X1: X0,X2: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2 )
= X2 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2 )
= X1 ) ),
inference(rectify,[status(thm)],[f18]) ).
thf(f18,axiom,
! [X0: $tType,X5: X0,X6: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X5 @ X6 )
= X6 )
& ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X5 @ X6 )
= X5 ) ),
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Ebool_2ECOND__CLAUSES) ).
thf(f1398,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
= $false )
| ( ( c_2Eextreal_2Eextreal__max @ X2 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $true @ X1 @ X2 ) ) ),
inference(fool_paramodulation,[status(thm)],[f733]) ).
thf(f733,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ X2 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ X2 @ X1 ) @ X1 @ X2 ) ),
inference(equality_proxy_clausification,[status(thm)],[f732]) ).
thf(f732,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__max @ X2 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ X2 @ X1 ) @ X1 @ X2 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f731]) ).
thf(f731,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ Y0 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 ) @ X1 @ Y0 ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f730]) ).
thf(f730,plain,
! [X1: tyop_2Eextreal_2Eextreal] :
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ Y0 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 ) @ X1 @ Y0 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f729]) ).
thf(f729,plain,
! [X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 ) @ Y0 @ Y1 ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f110]) ).
thf(f110,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 ) @ Y0 @ Y1 ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f87]) ).
thf(f87,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 ) @ Y0 @ Y1 ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f86]) ).
thf(f86,plain,
! [X0: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ X0 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ X0 @ X1 ) @ X1 @ X0 ) ),
inference(rectify,[status(thm)],[f24]) ).
thf(f24,axiom,
! [X8: tyop_2Eextreal_2Eextreal,X9: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ X8 @ X9 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ X8 @ X9 ) @ X9 @ X8 ) ),
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Eextreal__max__def) ).
thf(f1278,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
!= $false )
| spl0_4 ),
inference(avatar_component_clause,[status(thm)],[f1277]) ).
thf(f1277,definition,
( spl0_4
<=> ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition]) ).
thf(f2024,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $true )
| ~ spl0_5
| spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f2019]) ).
thf(f2019,plain,
( ( $false = $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $true )
| ~ spl0_5
| spl0_6 ),
inference(superposition,[status(thm)],[f1881,f1946]) ).
thf(f1946,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK3 @ sK1 )
= $true )
| ~ spl0_5 ),
inference(trivial_inequality_removal,[status(thm)],[f1944]) ).
thf(f1944,plain,
( ( $false = $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK3 @ sK1 )
= $true )
| ~ spl0_5 ),
inference(superposition,[status(thm)],[f914,f1283]) ).
thf(f914,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ X1 @ X2 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f913]) ).
thf(f913,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
| ( c_2Eextreal_2Eextreal__le @ X1 @ X2 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f912]) ).
thf(f912,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 )
| ( c_2Eextreal_2Eextreal__le @ X1 @ Y0 ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f911]) ).
thf(f911,plain,
! [X1: tyop_2Eextreal_2Eextreal] :
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 )
| ( c_2Eextreal_2Eextreal__le @ X1 @ Y0 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f910]) ).
thf(f910,plain,
! [X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 )
| ( c_2Eextreal_2Eextreal__le @ Y0 @ Y1 ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f125]) ).
thf(f125,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 )
| ( c_2Eextreal_2Eextreal__le @ Y0 @ Y1 ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f99]) ).
thf(f99,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 )
| ( c_2Eextreal_2Eextreal__le @ Y0 @ Y1 ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f98]) ).
thf(f98,plain,
! [X0: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ X1 @ X0 )
| ( c_2Eextreal_2Eextreal__le @ X0 @ X1 ) ),
inference(rectify,[status(thm)],[f23]) ).
thf(f23,axiom,
! [X8: tyop_2Eextreal_2Eextreal,X9: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ X9 @ X8 )
| ( c_2Eextreal_2Eextreal__le @ X8 @ X9 ) ),
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Ele__total) ).
thf(f1881,plain,
( ! [X0: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ sK3 @ X0 )
= $false )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ X0 )
= $true ) )
| spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f1878]) ).
thf(f1878,plain,
( ! [X0: tyop_2Eextreal_2Eextreal] :
( ( $false != $false )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ X0 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK3 @ X0 )
= $false ) )
| spl0_6 ),
inference(superposition,[status(thm)],[f1286,f888]) ).
thf(f888,plain,
! [X2: tyop_2Eextreal_2Eextreal,X3: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X3 @ X2 )
= $false )
| ( ( c_2Eextreal_2Eextreal__le @ X3 @ X1 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f887]) ).
thf(f887,plain,
! [X2: tyop_2Eextreal_2Eextreal,X3: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X3 @ X1 )
= $true )
| ( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ X3 @ X2 ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f886]) ).
thf(f886,plain,
! [X2: tyop_2Eextreal_2Eextreal,X3: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ X3 @ X2 ) )
=> ( c_2Eextreal_2Eextreal__le @ X3 @ X1 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f885]) ).
thf(f885,plain,
! [X2: tyop_2Eextreal_2Eextreal,X3: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ Y0 @ X2 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f884]) ).
thf(f884,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X2 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ Y0 @ X2 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f883]) ).
thf(f883,plain,
! [X2: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y1 @ X1 ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f882]) ).
thf(f882,plain,
! [X1: tyop_2Eextreal_2Eextreal] :
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ Y0 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y1 @ X1 ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f881]) ).
thf(f881,plain,
! [X1: tyop_2Eextreal_2Eextreal] :
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 )
& ( c_2Eextreal_2Eextreal__le @ Y2 @ Y1 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y2 @ Y0 ) ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f129]) ).
thf(f129,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 )
& ( c_2Eextreal_2Eextreal__le @ Y2 @ Y1 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y2 @ Y0 ) ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f89]) ).
thf(f89,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ Y1 @ Y0 )
& ( c_2Eextreal_2Eextreal__le @ Y2 @ Y1 ) )
=> ( c_2Eextreal_2Eextreal__le @ Y2 @ Y0 ) ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f88]) ).
thf(f88,plain,
! [X0: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal,X2: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X0 @ X1 )
& ( c_2Eextreal_2Eextreal__le @ X1 @ X2 ) )
=> ( c_2Eextreal_2Eextreal__le @ X0 @ X2 ) ),
inference(rectify,[status(thm)],[f22]) ).
thf(f22,axiom,
! [X8: tyop_2Eextreal_2Eextreal,X9: tyop_2Eextreal_2Eextreal,X13: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X8 @ X9 )
& ( c_2Eextreal_2Eextreal__le @ X9 @ X13 ) )
=> ( c_2Eextreal_2Eextreal__le @ X8 @ X13 ) ),
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Ele__trans) ).
thf(f1286,plain,
( ( $false
!= ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
| spl0_6 ),
inference(avatar_component_clause,[status(thm)],[f1285]) ).
thf(f1285,definition,
( spl0_6
<=> ( $false
= ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) ) ),
introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition]) ).
thf(f1940,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_5
| spl0_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f1939]) ).
thf(f1939,plain,
( $false
| ~ spl0_2
| ~ spl0_4
| spl0_5
| spl0_6 ),
inference(subsumption_resolution,[status(thm)],[f1934,f1286]) ).
thf(f1934,plain,
( ( $false
= ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
| ~ spl0_2
| ~ spl0_4
| spl0_5 ),
inference(backward_demodulation,[status(thm)],[f1279,f1928]) ).
thf(f1928,plain,
( ( ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 )
= sK2 )
| ~ spl0_2
| ~ spl0_4
| spl0_5 ),
inference(forward_demodulation,[status(thm)],[f1923,f1493]) ).
thf(f1493,plain,
( ! [X0: $tType,X2: X0,X1: X0] :
( ( c_2Ebool_2ECOND @ X0 @ $false @ X2 @ X1 )
= X1 )
| ~ spl0_2 ),
inference(forward_demodulation,[status(thm)],[f182,f908]) ).
thf(f908,plain,
( ( c_2Ebool_2EF = $false )
| ~ spl0_2 ),
inference(avatar_component_clause,[status(thm)],[f906]) ).
thf(f906,definition,
( spl0_2
<=> ( c_2Ebool_2EF = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition]) ).
thf(f182,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1 )
= X1 ),
inference(equality_proxy_clausification,[status(thm)],[f180]) ).
thf(f180,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( ( c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1 )
= X1 )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f179]) ).
thf(f1923,plain,
( ( ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ sK1 @ sK2 ) )
| ~ spl0_4
| spl0_5 ),
inference(superposition,[status(thm)],[f733,f1895]) ).
thf(f1895,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false )
| ~ spl0_4
| spl0_5 ),
inference(subsumption_resolution,[status(thm)],[f1885,f1282]) ).
thf(f1282,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
!= $false )
| spl0_5 ),
inference(avatar_component_clause,[status(thm)],[f1281]) ).
thf(f1885,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $false )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false )
| ~ spl0_4 ),
inference(superposition,[status(thm)],[f1279,f1407]) ).
thf(f1279,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $false )
| ~ spl0_4 ),
inference(avatar_component_clause,[status(thm)],[f1277]) ).
thf(f1875,plain,
( ~ spl0_2
| spl0_5
| ~ spl0_6
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[status(thm)],[f1874]) ).
thf(f1874,plain,
( $false
| ~ spl0_2
| spl0_5
| ~ spl0_6
| ~ spl0_8 ),
inference(subsumption_resolution,[status(thm)],[f1865,f1282]) ).
thf(f1865,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $false )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_8 ),
inference(trivial_inequality_removal,[status(thm)],[f1857]) ).
thf(f1857,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $false )
| ( $false = $true )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_8 ),
inference(superposition,[status(thm)],[f1287,f1751]) ).
thf(f1751,plain,
( ! [X0: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ X0 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK1 @ X0 )
= $false ) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_8 ),
inference(trivial_inequality_removal,[status(thm)],[f1750]) ).
thf(f1750,plain,
( ! [X0: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ X0 )
= $false )
| ( $false = $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ X0 )
= $true ) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[status(thm)],[f1745,f1287]) ).
thf(f1745,plain,
( ! [X0: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ X0 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ sK1 @ X0 )
= $false ) )
| ~ spl0_2
| ~ spl0_8 ),
inference(superposition,[status(thm)],[f1298,f1562]) ).
thf(f1562,plain,
( ! [X2: tyop_2Eextreal_2Eextreal,X0: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__max @ X0 @ X1 )
= X0 )
| ( ( c_2Eextreal_2Eextreal__le @ X1 @ X2 )
= $false )
| ( ( c_2Eextreal_2Eextreal__le @ X0 @ X2 )
= $true ) )
| ~ spl0_2 ),
inference(forward_demodulation,[status(thm)],[f1549,f1493]) ).
thf(f1549,plain,
! [X2: tyop_2Eextreal_2Eextreal,X0: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ X0 @ X2 )
= $true )
| ( ( c_2Eextreal_2Eextreal__max @ X0 @ X1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ X1 @ X0 ) )
| ( ( c_2Eextreal_2Eextreal__le @ X1 @ X2 )
= $false ) ),
inference(superposition,[status(thm)],[f733,f888]) ).
thf(f1298,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $true )
| ~ spl0_8 ),
inference(avatar_component_clause,[status(thm)],[f1296]) ).
thf(f1296,definition,
( spl0_8
<=> ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_8])],[avatar_definition]) ).
thf(f1287,plain,
( ( $false
= ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
| ~ spl0_6 ),
inference(avatar_component_clause,[status(thm)],[f1285]) ).
thf(f1784,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_6
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f1783]) ).
thf(f1783,plain,
( $false
| ~ spl0_2
| spl0_4
| ~ spl0_6
| ~ spl0_10 ),
inference(subsumption_resolution,[status(thm)],[f1774,f1287]) ).
thf(f1774,plain,
( ( $false
!= ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
| ~ spl0_2
| spl0_4
| ~ spl0_10 ),
inference(backward_demodulation,[status(thm)],[f1278,f1722]) ).
thf(f1722,plain,
( ( ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 )
= sK2 )
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_demodulation,[status(thm)],[f1717,f1493]) ).
thf(f1717,plain,
( ( ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ sK1 @ sK2 ) )
| ~ spl0_10 ),
inference(superposition,[status(thm)],[f733,f1424]) ).
thf(f1424,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false )
| ~ spl0_10 ),
inference(avatar_component_clause,[status(thm)],[f1422]) ).
thf(f1422,definition,
( spl0_10
<=> ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition]) ).
thf(f1474,plain,
( ~ spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[status(thm)],[f1473]) ).
thf(f1473,plain,
( $false
| ~ spl0_6
| ~ spl0_7 ),
inference(trivial_inequality_removal,[status(thm)],[f1472]) ).
thf(f1472,plain,
( ( $false = $true )
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_demodulation,[status(thm)],[f1294,f1287]) ).
thf(f1294,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 )
= $true )
| ~ spl0_7 ),
inference(avatar_component_clause,[status(thm)],[f1292]) ).
thf(f1292,definition,
( spl0_7
<=> ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_7])],[avatar_definition]) ).
thf(f1436,plain,
( spl0_10
| ~ spl0_5
| spl0_4 ),
inference(avatar_split_clause,[status(thm)],[f1416,f1277,f1281,f1422]) ).
thf(f1416,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
!= $false )
| ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK1 )
= $false )
| spl0_4 ),
inference(superposition,[status(thm)],[f1278,f1407]) ).
thf(f1434,plain,
spl0_2,
inference(avatar_split_clause,[status(thm)],[f169,f906]) ).
thf(f169,plain,
c_2Ebool_2EF = $false,
inference(not_proxy_clausification,[status(thm)],[f167]) ).
thf(f167,plain,
( ( ~ c_2Ebool_2EF ) = $true ),
inference(binary_proxy_clausification,[status(thm)],[f165]) ).
thf(f165,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] : $true )
& ~ c_2Ebool_2EF )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f163]) ).
thf(f163,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] : $true )
& ~ c_2Ebool_2EF
& ~ c_2Ebool_2EF )
= $true ),
inference(boolean_simplification,[status(thm)],[f162]) ).
thf(f162,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] : ( Y0 = Y0 ) )
& ~ c_2Ebool_2EF
& ~ c_2Ebool_2EF )
= $true ),
inference(boolean_simplification,[status(thm)],[f161]) ).
thf(f161,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] :
( ( ~ ~ Y0 )
= Y0 ) )
& ~ c_2Ebool_2EF
& ~ c_2Ebool_2EF )
= $true ),
inference(boolean_simplification,[status(thm)],[f160]) ).
thf(f160,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] :
( ( ~ ~ Y0 )
= Y0 ) )
& ( c_2Ebool_2EF = $false )
& ~ c_2Ebool_2EF )
= $true ),
inference(boolean_simplification,[status(thm)],[f159]) ).
thf(f159,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] :
( ( ~ ~ Y0 )
= Y0 ) )
& ( c_2Ebool_2EF = ( ~ $true ) )
& ~ c_2Ebool_2EF )
= $true ),
inference(boolean_simplification,[status(thm)],[f139]) ).
thf(f139,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] :
( ( ~ ~ Y0 )
= Y0 ) )
& ( c_2Ebool_2EF = ( ~ $true ) )
& ( $true = ( ~ c_2Ebool_2EF ) ) )
= $true ),
inference(definition_unfolding,[status(thm)],[f128,f134,f134]) ).
thf(f128,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] :
( ( ~ ~ Y0 )
= Y0 ) )
& ( c_2Ebool_2EF = ( ~ c_2Ebool_2ET ) )
& ( c_2Ebool_2ET = ( ~ c_2Ebool_2EF ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f45]) ).
thf(f45,plain,
( ( ( !! @ $o
@ ^ [Y0: $o] :
( ( ~ ~ Y0 )
= Y0 ) )
& ( c_2Ebool_2EF = ( ~ c_2Ebool_2ET ) )
& ( c_2Ebool_2ET = ( ~ c_2Ebool_2EF ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f44]) ).
thf(f44,plain,
( ( c_2Ebool_2ET
<=> ~ c_2Ebool_2EF )
& ( c_2Ebool_2EF
<=> ~ c_2Ebool_2ET )
& ! [X0: $o] :
( ~ ~ X0
<=> X0 ) ),
inference(rectify,[status(thm)],[f15]) ).
thf(f15,axiom,
( ( c_2Ebool_2ET
<=> ~ c_2Ebool_2EF )
& ( c_2Ebool_2EF
<=> ~ c_2Ebool_2ET )
& ! [X7: $o] :
( ~ ~ X7
<=> X7 ) ),
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Ebool_2ENOT__CLAUSES) ).
thf(f1432,plain,
( ~ spl0_5
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[status(thm)],[f1431]) ).
thf(f1431,plain,
( $false
| ~ spl0_5
| ~ spl0_9 ),
inference(trivial_inequality_removal,[status(thm)],[f1430]) ).
thf(f1430,plain,
( ( $false = $true )
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[status(thm)],[f1303,f1283]) ).
thf(f1303,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $true )
| ~ spl0_9 ),
inference(avatar_component_clause,[status(thm)],[f1301]) ).
thf(f1301,definition,
( spl0_9
<=> ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition]) ).
thf(f1363,plain,
( ~ spl0_4
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[status(thm)],[f1362]) ).
thf(f1362,plain,
( $false
| ~ spl0_4
| ~ spl0_8 ),
inference(trivial_inequality_removal,[status(thm)],[f1361]) ).
thf(f1361,plain,
( ( $false = $true )
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[status(thm)],[f1298,f1279]) ).
thf(f1304,plain,
( spl0_8
| spl0_9 ),
inference(avatar_split_clause,[status(thm)],[f1290,f1301,f1296]) ).
thf(f1290,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f1273]) ).
thf(f1273,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $true )
| ( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
& ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f1272]) ).
thf(f1272,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
& ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
!= ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 ) ),
inference(binary_proxy_clausification,[status(thm)],[f1271]) ).
thf(f1271,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
& ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) ) )
= $false ),
inference(beta_eta_normalization,[status(thm)],[f1270]) ).
thf(f1270,plain,
( $false
= ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ Y0 )
= ( ( c_2Eextreal_2Eextreal__le @ sK1 @ Y0 )
& ( c_2Eextreal_2Eextreal__le @ sK2 @ Y0 ) ) )
@ sK3 ) ),
inference(sigma_clausification,[status(thm)],[f1269]) ).
thf(f1269,plain,
( $false
= ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ Y0 )
= ( ( c_2Eextreal_2Eextreal__le @ sK1 @ Y0 )
& ( c_2Eextreal_2Eextreal__le @ sK2 @ Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f1268]) ).
thf(f1268,plain,
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ Y0 @ sK1 ) @ Y1 )
= ( ( c_2Eextreal_2Eextreal__le @ sK1 @ Y1 )
& ( c_2Eextreal_2Eextreal__le @ Y0 @ Y1 ) ) ) )
@ sK2 )
= $false ),
inference(sigma_clausification,[status(thm)],[f1267]) ).
thf(f1267,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ Y0 @ sK1 ) @ Y1 )
= ( ( c_2Eextreal_2Eextreal__le @ sK1 @ Y1 )
& ( c_2Eextreal_2Eextreal__le @ Y0 @ Y1 ) ) ) ) )
= $false ),
inference(beta_eta_normalization,[status(thm)],[f1266]) ).
thf(f1266,plain,
( ( ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 ) @ Y2 )
= ( ( c_2Eextreal_2Eextreal__le @ Y0 @ Y2 )
& ( c_2Eextreal_2Eextreal__le @ Y1 @ Y2 ) ) ) ) )
@ sK1 )
= $false ),
inference(sigma_clausification,[status(thm)],[f1265]) ).
thf(f1265,plain,
( ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 ) @ Y2 )
= ( ( c_2Eextreal_2Eextreal__le @ Y0 @ Y2 )
& ( c_2Eextreal_2Eextreal__le @ Y1 @ Y2 ) ) ) ) ) )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f118]) ).
thf(f118,plain,
( ( ~ ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 ) @ Y2 )
= ( ( c_2Eextreal_2Eextreal__le @ Y0 @ Y2 )
& ( c_2Eextreal_2Eextreal__le @ Y1 @ Y2 ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f75]) ).
thf(f75,plain,
( ( ~ ( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y0: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y1: tyop_2Eextreal_2Eextreal] :
( !! @ tyop_2Eextreal_2Eextreal
@ ^ [Y2: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ Y1 @ Y0 ) @ Y2 )
= ( ( c_2Eextreal_2Eextreal__le @ Y0 @ Y2 )
& ( c_2Eextreal_2Eextreal__le @ Y1 @ Y2 ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f74]) ).
thf(f74,plain,
~ ! [X0: tyop_2Eextreal_2Eextreal,X1: tyop_2Eextreal_2Eextreal,X2: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ X1 @ X2 ) @ X0 )
<=> ( ( c_2Eextreal_2Eextreal__le @ X1 @ X0 )
& ( c_2Eextreal_2Eextreal__le @ X2 @ X0 ) ) ),
inference(rectify,[status(thm)],[f36]) ).
thf(f36,negated_conjecture,
~ ! [X21: tyop_2Eextreal_2Eextreal,X4: tyop_2Eextreal_2Eextreal,X22: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ X4 @ X22 ) @ X21 )
<=> ( ( c_2Eextreal_2Eextreal__le @ X4 @ X21 )
& ( c_2Eextreal_2Eextreal__le @ X22 @ X21 ) ) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
thf(f35,conjecture,
! [X21: tyop_2Eextreal_2Eextreal,X4: tyop_2Eextreal_2Eextreal,X22: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ X4 @ X22 ) @ X21 )
<=> ( ( c_2Eextreal_2Eextreal__le @ X4 @ X21 )
& ( c_2Eextreal_2Eextreal__le @ X22 @ X21 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Emax__le) ).
thf(f1299,plain,
( spl0_7
| spl0_8 ),
inference(avatar_split_clause,[status(thm)],[f1289,f1296,f1292]) ).
thf(f1289,plain,
( ( ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 )
= $true )
| ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f1273]) ).
thf(f1288,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(avatar_split_clause,[status(thm)],[f1275,f1285,f1281,f1277]) ).
thf(f1275,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $false )
| ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
= $false )
| ( $false
= ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f1274]) ).
thf(f1274,plain,
( ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ sK2 @ sK1 ) @ sK3 )
= $false )
| ( ( ( c_2Eextreal_2Eextreal__le @ sK1 @ sK3 )
& ( c_2Eextreal_2Eextreal__le @ sK2 @ sK3 ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f1272]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP021^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.35 % Computer : n010.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Tue Feb 24 08:22:18 EST 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.26/0.47 ---- Original DTF file ---
% 0.26/0.47 thf(spec,logic,$$dhol).
% 0.26/0.47 %------------------------------------------------------------------------------
% 0.26/0.47 % File : ITP021^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.26/0.47 % Domain : Interactive Theorem Proving
% 0.26/0.47 % Problem : HOL4 syntactic export of thm_2Eextreal_2Emax__le.p, bushy mode
% 0.26/0.47 % Version : [BG+19] axioms.
% 0.26/0.47 % English :
% 0.26/0.47
% 0.26/0.47 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.26/0.47 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.26/0.47 % Source : [BG+19]
% 0.26/0.47 % Names : thm_2Eextreal_2Emax__le.p [Gau19]
% 0.26/0.47 % : HL410001^3.p [TPAP]
% 0.26/0.47
% 0.26/0.47 % Status : Theorem
% 0.26/0.47 % Rating : 0.33 v8.1.0, 0.25 v7.5.0
% 0.26/0.47 % Syntax : Number of formulae : 50 ( 10 unt; 15 typ; 0 def)
% 0.26/0.47 % Number of atoms : 103 ( 12 equ; 45 cnn)
% 0.26/0.47 % Maximal formula atoms : 8 ( 2 avg)
% 0.26/0.47 % Number of connectives : 271 ( 45 ~; 36 |; 27 &; 95 @)
% 0.26/0.47 % ( 38 <=>; 30 =>; 0 <=; 0 <~>)
% 0.26/0.47 % Maximal formula depth : 11 ( 6 avg)
% 0.26/0.47 % Number of types : 3 ( 2 usr)
% 0.26/0.47 % Number of type conns : 24 ( 24 >; 0 *; 0 +; 0 <<)
% 0.26/0.47 % Number of symbols : 15 ( 13 usr; 3 con; 0-4 aty)
% 0.26/0.47 % Number of variables : 73 ( 0 ^; 68 !; 1 ?; 73 :)
% 0.26/0.47 % ( 4 !>; 0 ?*; 0 @-; 0 @+)
% 0.26/0.47 % SPC : TH1_THM_EQU_NAR
% 0.26/0.47
% 0.26/0.47 % Comments :
% 0.26/0.47 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.26/0.47 %------------------------------------------------------------------------------
% 0.26/0.47 thf(tyop_2Eextreal_2Eextreal,type,
% 0.26/0.47 tyop_2Eextreal_2Eextreal: $tType ).
% 0.26/0.47
% 0.26/0.47 thf(tyop_2Emin_2Ebool,type,
% 0.26/0.47 tyop_2Emin_2Ebool: $tType ).
% 0.26/0.47
% 0.26/0.47 thf(tyop_2Emin_2Efun,type,
% 0.26/0.47 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2E_21,type,
% 0.26/0.47 c_2Ebool_2E_21:
% 0.26/0.47 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2E_2F_5C,type,
% 0.26/0.47 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Emin_2E_3D,type,
% 0.26/0.47 c_2Emin_2E_3D:
% 0.26/0.47 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Emin_2E_3D_3D_3E,type,
% 0.26/0.47 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2E_3F,type,
% 0.26/0.47 c_2Ebool_2E_3F:
% 0.26/0.47 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2ECOND,type,
% 0.26/0.47 c_2Ebool_2ECOND:
% 0.26/0.47 !>[A_27a: $tType] : ( $o > A_27a > A_27a > A_27a ) ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2EF,type,
% 0.26/0.47 c_2Ebool_2EF: $o ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2ET,type,
% 0.26/0.47 c_2Ebool_2ET: $o ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2E_5C_2F,type,
% 0.26/0.47 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Eextreal_2Eextreal__le,type,
% 0.26/0.47 c_2Eextreal_2Eextreal__le: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > $o ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Eextreal_2Eextreal__max,type,
% 0.26/0.47 c_2Eextreal_2Eextreal__max: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal ).
% 0.26/0.47
% 0.26/0.47 thf(c_2Ebool_2E_7E,type,
% 0.26/0.47 c_2Ebool_2E_7E: $o > $o ).
% 0.26/0.47
% 0.26/0.47 thf(logicdef_2E_2F_5C,axiom,
% 0.26/0.47 ! [V0: $o,V1: $o] :
% 0.26/0.47 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.26/0.47 <=> ( V0
% 0.26/0.47 & V1 ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(logicdef_2E_5C_2F,axiom,
% 0.26/0.47 ! [V0: $o,V1: $o] :
% 0.26/0.47 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.26/0.47 <=> ( V0
% 0.26/0.47 | V1 ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(logicdef_2E_7E,axiom,
% 0.26/0.47 ! [V0: $o] :
% 0.26/0.47 ( ( c_2Ebool_2E_7E @ V0 )
% 0.26/0.47 <=> ( (~) @ V0 ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(logicdef_2E_3D_3D_3E,axiom,
% 0.26/0.47 ! [V0: $o,V1: $o] :
% 0.26/0.47 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.26/0.47 <=> ( V0
% 0.26/0.47 => V1 ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(logicdef_2E_3D,axiom,
% 0.26/0.47 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 0.26/0.47 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 0.26/0.47 <=> ( V0 = V1 ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(quantdef_2E_21,axiom,
% 0.26/0.47 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.26/0.47 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 0.26/0.47 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(quantdef_2E_3F,axiom,
% 0.26/0.47 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.26/0.47 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 0.26/0.47 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2ETRUTH,axiom,
% 0.26/0.47 c_2Ebool_2ET ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 0.26/0.47 ! [V0t1: $o,V1t2: $o] :
% 0.26/0.47 ( ( V0t1
% 0.26/0.47 => V1t2 )
% 0.26/0.47 => ( ( V1t2
% 0.26/0.47 => V0t1 )
% 0.26/0.47 => ( V0t1 = V1t2 ) ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EFALSITY,axiom,
% 0.26/0.47 ! [V0t: $o] :
% 0.26/0.47 ( c_2Ebool_2EF
% 0.26/0.47 => V0t ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EEXCLUDED__MIDDLE,axiom,
% 0.26/0.47 ! [V0t: $o] :
% 0.26/0.47 ( V0t
% 0.26/0.47 | ( (~) @ V0t ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EIMP__F,axiom,
% 0.26/0.47 ! [V0t: $o] :
% 0.26/0.47 ( ( V0t
% 0.26/0.47 => c_2Ebool_2EF )
% 0.26/0.47 => ( (~) @ V0t ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EF__IMP,axiom,
% 0.26/0.47 ! [V0t: $o] :
% 0.26/0.47 ( ( (~) @ V0t )
% 0.26/0.47 => ( V0t
% 0.26/0.47 => c_2Ebool_2EF ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 0.26/0.47 ! [V0t: $o] :
% 0.26/0.47 ( ( ( c_2Ebool_2ET
% 0.26/0.47 => V0t )
% 0.26/0.47 <=> V0t )
% 0.26/0.47 & ( ( V0t
% 0.26/0.47 => c_2Ebool_2ET )
% 0.26/0.47 <=> c_2Ebool_2ET )
% 0.26/0.47 & ( ( c_2Ebool_2EF
% 0.26/0.47 => V0t )
% 0.26/0.47 <=> c_2Ebool_2ET )
% 0.26/0.47 & ( ( V0t
% 0.26/0.47 => V0t )
% 0.26/0.47 <=> c_2Ebool_2ET )
% 0.26/0.47 & ( ( V0t
% 0.26/0.47 => c_2Ebool_2EF )
% 0.26/0.47 <=> ( (~) @ V0t ) ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 0.26/0.47 ( ! [V0t: $o] :
% 0.26/0.47 ( ( (~) @ ( (~) @ V0t ) )
% 0.26/0.47 <=> V0t )
% 0.26/0.47 & ( ( (~) @ c_2Ebool_2ET )
% 0.26/0.47 <=> c_2Ebool_2EF )
% 0.26/0.47 & ( ( (~) @ c_2Ebool_2EF )
% 0.26/0.47 <=> c_2Ebool_2ET ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 0.26/0.47 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 0.26/0.47 ( ( V0x = V1y )
% 0.26/0.47 <=> ( V1y = V0x ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 0.26/0.47 ! [V0t: $o] :
% 0.26/0.47 ( ( ( c_2Ebool_2ET = V0t )
% 0.26/0.47 <=> V0t )
% 0.26/0.47 & ( ( V0t = c_2Ebool_2ET )
% 0.26/0.47 <=> V0t )
% 0.26/0.47 & ( ( c_2Ebool_2EF = V0t )
% 0.26/0.47 <=> ( (~) @ V0t ) )
% 0.26/0.47 & ( ( V0t = c_2Ebool_2EF )
% 0.26/0.47 <=> ( (~) @ V0t ) ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2ECOND__CLAUSES,axiom,
% 0.26/0.47 ! [A_27a: $tType,V0t1: A_27a,V1t2: A_27a] :
% 0.26/0.47 ( ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2ET @ V0t1 @ V1t2 )
% 0.26/0.47 = V0t1 )
% 0.26/0.47 & ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2EF @ V0t1 @ V1t2 )
% 0.26/0.47 = V1t2 ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EDISJ__ASSOC,axiom,
% 0.26/0.47 ! [V0A: $o,V1B: $o,V2C: $o] :
% 0.26/0.47 ( ( V0A
% 0.26/0.47 | V1B
% 0.26/0.47 | V2C )
% 0.26/0.47 <=> ( V0A
% 0.26/0.47 | V1B
% 0.26/0.47 | V2C ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EDISJ__SYM,axiom,
% 0.26/0.47 ! [V0A: $o,V1B: $o] :
% 0.26/0.47 ( ( V0A
% 0.26/0.47 | V1B )
% 0.26/0.47 <=> ( V1B
% 0.26/0.47 | V0A ) ) ).
% 0.26/0.47
% 0.26/0.47 thf(thm_2Ebool_2EDE__MORGAN__THM,axiom,
% 0.26/0.47 ! [V0A: $o,V1B: $o] :
% 0.26/0.47 ( ( ( (~)
% 0.26/0.47 @ ( V0A
% 0.26/0.47 & V1B ) )
% 0.26/0.47 <=> ( ( (~) @ V0A )
% 0.26/0.47 | ( (~) @ V1B ) ) )
% 0.26/0.47 & ( ( (~)
% 0.26/0.48 @ ( V0A
% 0.26/0.48 | V1B ) )
% 0.26/0.48 <=> ( ( (~) @ V0A )
% 0.26/0.48 & ( (~) @ V1B ) ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Eextreal_2Ele__trans,axiom,
% 0.26/0.48 ! [V0x: tyop_2Eextreal_2Eextreal,V1y: tyop_2Eextreal_2Eextreal,V2z: tyop_2Eextreal_2Eextreal] :
% 0.26/0.48 ( ( ( c_2Eextreal_2Eextreal__le @ V0x @ V1y )
% 0.26/0.48 & ( c_2Eextreal_2Eextreal__le @ V1y @ V2z ) )
% 0.26/0.48 => ( c_2Eextreal_2Eextreal__le @ V0x @ V2z ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Eextreal_2Ele__total,axiom,
% 0.26/0.48 ! [V0x: tyop_2Eextreal_2Eextreal,V1y: tyop_2Eextreal_2Eextreal] :
% 0.26/0.48 ( ( c_2Eextreal_2Eextreal__le @ V0x @ V1y )
% 0.26/0.48 | ( c_2Eextreal_2Eextreal__le @ V1y @ V0x ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Eextreal_2Eextreal__max__def,axiom,
% 0.26/0.48 ! [V0x: tyop_2Eextreal_2Eextreal,V1y: tyop_2Eextreal_2Eextreal] :
% 0.26/0.48 ( ( c_2Eextreal_2Eextreal__max @ V0x @ V1y )
% 0.26/0.48 = ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ V0x @ V1y ) @ V1y @ V0x ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2ENOT__NOT,axiom,
% 0.26/0.48 ! [V0t: $o] :
% 0.26/0.48 ( ( (~) @ ( (~) @ V0t ) )
% 0.26/0.48 <=> V0t ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 0.26/0.48 ! [V0A: $o] :
% 0.26/0.48 ( V0A
% 0.26/0.48 => ( ( (~) @ V0A )
% 0.26/0.48 => c_2Ebool_2EF ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 0.26/0.48 ! [V0B: $o,V1A: $o] :
% 0.26/0.48 ( ( ( (~)
% 0.26/0.48 @ ( V1A
% 0.26/0.48 | V0B ) )
% 0.26/0.48 => c_2Ebool_2EF )
% 0.26/0.48 <=> ( ( V1A
% 0.26/0.48 => c_2Ebool_2EF )
% 0.26/0.48 => ( ( (~) @ V0B )
% 0.26/0.48 => c_2Ebool_2EF ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 0.26/0.48 ! [V0B: $o,V1A: $o] :
% 0.26/0.48 ( ( ( (~)
% 0.26/0.48 @ ( ( (~) @ V1A )
% 0.26/0.48 | V0B ) )
% 0.26/0.48 => c_2Ebool_2EF )
% 0.26/0.48 <=> ( V1A
% 0.26/0.48 => ( ( (~) @ V0B )
% 0.26/0.48 => c_2Ebool_2EF ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2EAND__INV2,axiom,
% 0.26/0.48 ! [V0A: $o] :
% 0.26/0.48 ( ( ( (~) @ V0A )
% 0.26/0.48 => c_2Ebool_2EF )
% 0.26/0.48 => ( ( V0A
% 0.26/0.48 => c_2Ebool_2EF )
% 0.26/0.48 => c_2Ebool_2EF ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2Edc__eq,axiom,
% 0.26/0.48 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.26/0.48 ( ( V2p
% 0.26/0.48 <=> ( V1q = V0r ) )
% 0.26/0.48 <=> ( ( V2p
% 0.26/0.48 | V1q
% 0.26/0.48 | V0r )
% 0.26/0.48 & ( V2p
% 0.26/0.48 | ( (~) @ V0r )
% 0.26/0.48 | ( (~) @ V1q ) )
% 0.26/0.48 & ( V1q
% 0.26/0.48 | ( (~) @ V0r )
% 0.26/0.48 | ( (~) @ V2p ) )
% 0.26/0.48 & ( V0r
% 0.26/0.48 | ( (~) @ V1q )
% 0.26/0.48 | ( (~) @ V2p ) ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2Edc__conj,axiom,
% 0.26/0.48 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.26/0.48 ( ( V2p
% 0.26/0.48 <=> ( V1q
% 0.26/0.48 & V0r ) )
% 0.26/0.48 <=> ( ( V2p
% 0.26/0.48 | ( (~) @ V1q )
% 0.26/0.48 | ( (~) @ V0r ) )
% 0.26/0.48 & ( V1q
% 0.26/0.48 | ( (~) @ V2p ) )
% 0.26/0.48 & ( V0r
% 0.26/0.48 | ( (~) @ V2p ) ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2Edc__disj,axiom,
% 0.26/0.48 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.26/0.48 ( ( V2p
% 0.26/0.48 <=> ( V1q
% 0.26/0.48 | V0r ) )
% 0.26/0.48 <=> ( ( V2p
% 0.26/0.48 | ( (~) @ V1q ) )
% 0.26/0.48 & ( V2p
% 0.26/0.48 | ( (~) @ V0r ) )
% 0.26/0.48 & ( V1q
% 0.26/0.48 | V0r
% 0.26/0.48 | ( (~) @ V2p ) ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2Edc__imp,axiom,
% 0.26/0.48 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.26/0.48 ( ( V2p
% 0.26/0.48 <=> ( V1q
% 0.26/0.48 => V0r ) )
% 0.26/0.48 <=> ( ( V2p
% 0.26/0.48 | V1q )
% 0.26/0.48 & ( V2p
% 0.26/0.48 | ( (~) @ V0r ) )
% 0.26/0.48 & ( ( (~) @ V1q )
% 0.26/0.48 | V0r
% 0.26/0.48 | ( (~) @ V2p ) ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Esat_2Edc__neg,axiom,
% 0.26/0.48 ! [V0q: $o,V1p: $o] :
% 0.26/0.48 ( ( V1p
% 0.26/0.48 <=> ( (~) @ V0q ) )
% 0.26/0.48 <=> ( ( V1p
% 0.26/0.48 | V0q )
% 0.26/0.48 & ( ( (~) @ V0q )
% 0.26/0.48 | ( (~) @ V1p ) ) ) ) ).
% 0.26/0.48
% 0.26/0.48 thf(thm_2Eextreal_2Emax__le,conjecture,
% 0.26/0.48 ! [V0z: tyop_2Eextreal_2Eextreal,V1x: tyop_2Eextreal_2Eextreal,V2y: tyop_2Eextreal_2Eextreal] :
% 0.26/0.48 ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ V1x @ V2y ) @ V0z )
% 0.26/0.48 <=> ( ( c_2Eextreal_2Eextreal__le @ V1x @ V0z )
% 0.26/0.48 & ( c_2Eextreal_2Eextreal__le @ V2y @ V0z ) ) ) ).
% 0.26/0.48
% 0.26/0.48 %------------------------------------------------------------------------------
% 0.26/0.48 ------------------------
% 1.72/1.35 ---- Embedded in THF ---
% 1.72/1.35 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.72/1.35 %%% Generated on Tue Feb 24 08:22:19 EST 2026
% 1.72/1.35 %%% using '$$dhol' embedding, version 1.3.0.
% 1.72/1.35 %%% Logic specification used:
% 1.72/1.35 %%% thf(spec, logic, $$dhol).
% 1.72/1.35
% 1.72/1.35 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2DTF2251.p
% See solution above
% 1.72/1.35 ------------------------
% 1.72/1.37 ---- Cleaned THF ---
% 1.72/1.37 thf(tyop_2Eextreal_2Eextreal,type,
% 1.72/1.37 tyop_2Eextreal_2Eextreal: $tType ).
% 1.72/1.37
% 1.72/1.37 thf(tyop_2Emin_2Ebool,type,
% 1.72/1.37 tyop_2Emin_2Ebool: $tType ).
% 1.72/1.37
% 1.72/1.37 thf(tyop_2Emin_2Efun,type,
% 1.72/1.37 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2E_21,type,
% 1.72/1.37 c_2Ebool_2E_21:
% 1.72/1.37 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2E_2F_5C,type,
% 1.72/1.37 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Emin_2E_3D,type,
% 1.72/1.37 c_2Emin_2E_3D:
% 1.72/1.37 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Emin_2E_3D_3D_3E,type,
% 1.72/1.37 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2E_3F,type,
% 1.72/1.37 c_2Ebool_2E_3F:
% 1.72/1.37 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2ECOND,type,
% 1.72/1.37 c_2Ebool_2ECOND:
% 1.72/1.37 !>[A_27a: $tType] : ( $o > A_27a > A_27a > A_27a ) ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2EF,type,
% 1.72/1.37 c_2Ebool_2EF: $o ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2ET,type,
% 1.72/1.37 c_2Ebool_2ET: $o ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2E_5C_2F,type,
% 1.72/1.37 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Eextreal_2Eextreal__le,type,
% 1.72/1.37 c_2Eextreal_2Eextreal__le: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > $o ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Eextreal_2Eextreal__max,type,
% 1.72/1.37 c_2Eextreal_2Eextreal__max: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal ).
% 1.72/1.37
% 1.72/1.37 thf(c_2Ebool_2E_7E,type,
% 1.72/1.37 c_2Ebool_2E_7E: $o > $o ).
% 1.72/1.37
% 1.72/1.37 thf(logicdef_2E_2F_5C,axiom,
% 1.72/1.37 ! [V0: $o,V1: $o] :
% 1.72/1.37 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 1.72/1.37 <=> ( V0
% 1.72/1.37 & V1 ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(logicdef_2E_5C_2F,axiom,
% 1.72/1.37 ! [V0: $o,V1: $o] :
% 1.72/1.37 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 1.72/1.37 <=> ( V0
% 1.72/1.37 | V1 ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(logicdef_2E_7E,axiom,
% 1.72/1.37 ! [V0: $o] :
% 1.72/1.37 ( ( c_2Ebool_2E_7E @ V0 )
% 1.72/1.37 <=> ( (~) @ V0 ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(logicdef_2E_3D_3D_3E,axiom,
% 1.72/1.37 ! [V0: $o,V1: $o] :
% 1.72/1.37 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 1.72/1.37 <=> ( V0
% 1.72/1.37 => V1 ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(logicdef_2E_3D,axiom,
% 1.72/1.37 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 1.72/1.37 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 1.72/1.37 <=> ( V0 = V1 ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(quantdef_2E_21,axiom,
% 1.72/1.37 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.72/1.37 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 1.72/1.37 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(quantdef_2E_3F,axiom,
% 1.72/1.37 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.72/1.37 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 1.72/1.37 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2ETRUTH,axiom,
% 1.72/1.37 c_2Ebool_2ET ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 1.72/1.37 ! [V0t1: $o,V1t2: $o] :
% 1.72/1.37 ( ( V0t1
% 1.72/1.37 => V1t2 )
% 1.72/1.37 => ( ( V1t2
% 1.72/1.37 => V0t1 )
% 1.72/1.37 => ( V0t1 = V1t2 ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EFALSITY,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( c_2Ebool_2EF
% 1.72/1.37 => V0t ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EEXCLUDED__MIDDLE,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( V0t
% 1.72/1.37 | ( (~) @ V0t ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EIMP__F,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( ( V0t
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 => ( (~) @ V0t ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EF__IMP,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( ( (~) @ V0t )
% 1.72/1.37 => ( V0t
% 1.72/1.37 => c_2Ebool_2EF ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( ( ( c_2Ebool_2ET
% 1.72/1.37 => V0t )
% 1.72/1.37 <=> V0t )
% 1.72/1.37 & ( ( V0t
% 1.72/1.37 => c_2Ebool_2ET )
% 1.72/1.37 <=> c_2Ebool_2ET )
% 1.72/1.37 & ( ( c_2Ebool_2EF
% 1.72/1.37 => V0t )
% 1.72/1.37 <=> c_2Ebool_2ET )
% 1.72/1.37 & ( ( V0t
% 1.72/1.37 => V0t )
% 1.72/1.37 <=> c_2Ebool_2ET )
% 1.72/1.37 & ( ( V0t
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 <=> ( (~) @ V0t ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 1.72/1.37 ( ! [V0t: $o] :
% 1.72/1.37 ( ( (~) @ ( (~) @ V0t ) )
% 1.72/1.37 <=> V0t )
% 1.72/1.37 & ( ( (~) @ c_2Ebool_2ET )
% 1.72/1.37 <=> c_2Ebool_2EF )
% 1.72/1.37 & ( ( (~) @ c_2Ebool_2EF )
% 1.72/1.37 <=> c_2Ebool_2ET ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 1.72/1.37 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 1.72/1.37 ( ( V0x = V1y )
% 1.72/1.37 <=> ( V1y = V0x ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( ( ( c_2Ebool_2ET = V0t )
% 1.72/1.37 <=> V0t )
% 1.72/1.37 & ( ( V0t = c_2Ebool_2ET )
% 1.72/1.37 <=> V0t )
% 1.72/1.37 & ( ( c_2Ebool_2EF = V0t )
% 1.72/1.37 <=> ( (~) @ V0t ) )
% 1.72/1.37 & ( ( V0t = c_2Ebool_2EF )
% 1.72/1.37 <=> ( (~) @ V0t ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2ECOND__CLAUSES,axiom,
% 1.72/1.37 ! [A_27a: $tType,V0t1: A_27a,V1t2: A_27a] :
% 1.72/1.37 ( ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2ET @ V0t1 @ V1t2 )
% 1.72/1.37 = V0t1 )
% 1.72/1.37 & ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2EF @ V0t1 @ V1t2 )
% 1.72/1.37 = V1t2 ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EDISJ__ASSOC,axiom,
% 1.72/1.37 ! [V0A: $o,V1B: $o,V2C: $o] :
% 1.72/1.37 ( ( V0A
% 1.72/1.37 | V1B
% 1.72/1.37 | V2C )
% 1.72/1.37 <=> ( V0A
% 1.72/1.37 | V1B
% 1.72/1.37 | V2C ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EDISJ__SYM,axiom,
% 1.72/1.37 ! [V0A: $o,V1B: $o] :
% 1.72/1.37 ( ( V0A
% 1.72/1.37 | V1B )
% 1.72/1.37 <=> ( V1B
% 1.72/1.37 | V0A ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Ebool_2EDE__MORGAN__THM,axiom,
% 1.72/1.37 ! [V0A: $o,V1B: $o] :
% 1.72/1.37 ( ( ( (~)
% 1.72/1.37 @ ( V0A
% 1.72/1.37 & V1B ) )
% 1.72/1.37 <=> ( ( (~) @ V0A )
% 1.72/1.37 | ( (~) @ V1B ) ) )
% 1.72/1.37 & ( ( (~)
% 1.72/1.37 @ ( V0A
% 1.72/1.37 | V1B ) )
% 1.72/1.37 <=> ( ( (~) @ V0A )
% 1.72/1.37 & ( (~) @ V1B ) ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Eextreal_2Ele__trans,axiom,
% 1.72/1.37 ! [V0x: tyop_2Eextreal_2Eextreal,V1y: tyop_2Eextreal_2Eextreal,V2z: tyop_2Eextreal_2Eextreal] :
% 1.72/1.37 ( ( ( c_2Eextreal_2Eextreal__le @ V0x @ V1y )
% 1.72/1.37 & ( c_2Eextreal_2Eextreal__le @ V1y @ V2z ) )
% 1.72/1.37 => ( c_2Eextreal_2Eextreal__le @ V0x @ V2z ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Eextreal_2Ele__total,axiom,
% 1.72/1.37 ! [V0x: tyop_2Eextreal_2Eextreal,V1y: tyop_2Eextreal_2Eextreal] :
% 1.72/1.37 ( ( c_2Eextreal_2Eextreal__le @ V0x @ V1y )
% 1.72/1.37 | ( c_2Eextreal_2Eextreal__le @ V1y @ V0x ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Eextreal_2Eextreal__max__def,axiom,
% 1.72/1.37 ! [V0x: tyop_2Eextreal_2Eextreal,V1y: tyop_2Eextreal_2Eextreal] :
% 1.72/1.37 ( ( c_2Eextreal_2Eextreal__max @ V0x @ V1y )
% 1.72/1.37 = ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ V0x @ V1y ) @ V1y @ V0x ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2ENOT__NOT,axiom,
% 1.72/1.37 ! [V0t: $o] :
% 1.72/1.37 ( ( (~) @ ( (~) @ V0t ) )
% 1.72/1.37 <=> V0t ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 1.72/1.37 ! [V0A: $o] :
% 1.72/1.37 ( V0A
% 1.72/1.37 => ( ( (~) @ V0A )
% 1.72/1.37 => c_2Ebool_2EF ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 1.72/1.37 ! [V0B: $o,V1A: $o] :
% 1.72/1.37 ( ( ( (~)
% 1.72/1.37 @ ( V1A
% 1.72/1.37 | V0B ) )
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 <=> ( ( V1A
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 => ( ( (~) @ V0B )
% 1.72/1.37 => c_2Ebool_2EF ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 1.72/1.37 ! [V0B: $o,V1A: $o] :
% 1.72/1.37 ( ( ( (~)
% 1.72/1.37 @ ( ( (~) @ V1A )
% 1.72/1.37 | V0B ) )
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 <=> ( V1A
% 1.72/1.37 => ( ( (~) @ V0B )
% 1.72/1.37 => c_2Ebool_2EF ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2EAND__INV2,axiom,
% 1.72/1.37 ! [V0A: $o] :
% 1.72/1.37 ( ( ( (~) @ V0A )
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 => ( ( V0A
% 1.72/1.37 => c_2Ebool_2EF )
% 1.72/1.37 => c_2Ebool_2EF ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2Edc__eq,axiom,
% 1.72/1.37 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.72/1.37 ( ( V2p
% 1.72/1.37 <=> ( V1q = V0r ) )
% 1.72/1.37 <=> ( ( V2p
% 1.72/1.37 | V1q
% 1.72/1.37 | V0r )
% 1.72/1.37 & ( V2p
% 1.72/1.37 | ( (~) @ V0r )
% 1.72/1.37 | ( (~) @ V1q ) )
% 1.72/1.37 & ( V1q
% 1.72/1.37 | ( (~) @ V0r )
% 1.72/1.37 | ( (~) @ V2p ) )
% 1.72/1.37 & ( V0r
% 1.72/1.37 | ( (~) @ V1q )
% 1.72/1.37 | ( (~) @ V2p ) ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2Edc__conj,axiom,
% 1.72/1.37 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.72/1.37 ( ( V2p
% 1.72/1.37 <=> ( V1q
% 1.72/1.37 & V0r ) )
% 1.72/1.37 <=> ( ( V2p
% 1.72/1.37 | ( (~) @ V1q )
% 1.72/1.37 | ( (~) @ V0r ) )
% 1.72/1.37 & ( V1q
% 1.72/1.37 | ( (~) @ V2p ) )
% 1.72/1.37 & ( V0r
% 1.72/1.37 | ( (~) @ V2p ) ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2Edc__disj,axiom,
% 1.72/1.37 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.72/1.37 ( ( V2p
% 1.72/1.37 <=> ( V1q
% 1.72/1.37 | V0r ) )
% 1.72/1.37 <=> ( ( V2p
% 1.72/1.37 | ( (~) @ V1q ) )
% 1.72/1.37 & ( V2p
% 1.72/1.37 | ( (~) @ V0r ) )
% 1.72/1.37 & ( V1q
% 1.72/1.37 | V0r
% 1.72/1.37 | ( (~) @ V2p ) ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2Edc__imp,axiom,
% 1.72/1.37 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.72/1.37 ( ( V2p
% 1.72/1.37 <=> ( V1q
% 1.72/1.37 => V0r ) )
% 1.72/1.37 <=> ( ( V2p
% 1.72/1.37 | V1q )
% 1.72/1.37 & ( V2p
% 1.72/1.37 | ( (~) @ V0r ) )
% 1.72/1.37 & ( ( (~) @ V1q )
% 1.72/1.37 | V0r
% 1.72/1.37 | ( (~) @ V2p ) ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Esat_2Edc__neg,axiom,
% 1.72/1.37 ! [V0q: $o,V1p: $o] :
% 1.72/1.37 ( ( V1p
% 1.72/1.37 <=> ( (~) @ V0q ) )
% 1.72/1.37 <=> ( ( V1p
% 1.72/1.37 | V0q )
% 1.72/1.37 & ( ( (~) @ V0q )
% 1.72/1.37 | ( (~) @ V1p ) ) ) ) ).
% 1.72/1.37
% 1.72/1.37 thf(thm_2Eextreal_2Emax__le,conjecture,
% 1.72/1.37 ! [V0z: tyop_2Eextreal_2Eextreal,V1x: tyop_2Eextreal_2Eextreal,V2y: tyop_2Eextreal_2Eextreal] :
% 1.72/1.37 ( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ V1x @ V2y ) @ V0z )
% 1.72/1.37 <=> ( ( c_2Eextreal_2Eextreal__le @ V1x @ V0z )
% 1.72/1.37 & ( c_2Eextreal_2Eextreal__le @ V2y @ V0z ) ) ) ).
% 1.72/1.37 ------------------------
% 1.72/1.38 % (2369)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/27Mi)
% 1.72/1.38 % (2370)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/2Mi)
% 1.72/1.38 % (2373)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/18Mi)
% 1.72/1.38 % (2370)Instruction limit reached!
% 1.72/1.38 % (2370)------------------------------
% 1.72/1.38 % (2370)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.72/1.38 % (2370)Termination reason: Unknown
% 1.72/1.38 % (2370)Termination phase: Preprocessing 1
% 1.72/1.38
% 1.72/1.38 % (2370)Memory used [KB]: 1023
% 1.72/1.38 % (2370)Time elapsed: 0.002 s
% 1.72/1.38 % (2370)Instructions burned: 3 (million)
% 1.72/1.38 % (2370)------------------------------
% 1.72/1.38 % (2370)------------------------------
% 1.72/1.39 % (2373)Instruction limit reached!
% 1.72/1.39 % (2373)------------------------------
% 1.72/1.39 % (2373)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.72/1.39 % (2373)Termination reason: Unknown
% 1.72/1.39 % (2373)Termination phase: Saturation
% 1.72/1.39
% 1.72/1.39 % (2373)Memory used [KB]: 5756
% 1.72/1.39 % (2373)Time elapsed: 0.007 s
% 1.72/1.39 % (2373)Instructions burned: 19 (million)
% 1.72/1.39 % (2373)------------------------------
% 1.72/1.39 % (2373)------------------------------
% 1.72/1.39 % (2367)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/183Mi)
% 1.72/1.39 % (2368)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/4Mi)
% 1.72/1.39 % (2372)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/275Mi)
% 1.72/1.39 % (2371)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/2Mi)
% 1.72/1.39 % (2369)Instruction limit reached!
% 1.72/1.39 % (2369)------------------------------
% 1.72/1.39 % (2369)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.72/1.39 % (2369)Termination reason: Unknown
% 1.72/1.39 % (2369)Termination phase: Saturation
% 1.72/1.39
% 1.72/1.39 % (2369)Memory used [KB]: 5884
% 1.72/1.39 % (2369)Time elapsed: 0.010 s
% 1.72/1.39 % (2369)Instructions burned: 28 (million)
% 1.72/1.39 % (2369)------------------------------
% 1.72/1.39 % (2369)------------------------------
% 1.72/1.39 % (2368)Instruction limit reached!
% 1.72/1.39 % (2368)------------------------------
% 1.72/1.39 % (2368)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.72/1.39 % (2368)Termination reason: Unknown
% 1.72/1.39 % (2368)Termination phase: shuffling
% 1.72/1.39
% 1.72/1.39 % (2368)Memory used [KB]: 1023
% 1.72/1.39 % (2368)Time elapsed: 0.004 s
% 1.72/1.39 % (2368)Instructions burned: 4 (million)
% 1.72/1.39 % (2368)------------------------------
% 1.72/1.39 % (2368)------------------------------
% 1.72/1.39 % (2371)Instruction limit reached!
% 1.72/1.39 % (2371)------------------------------
% 1.72/1.39 % (2371)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.72/1.39 % (2371)Termination reason: Unknown
% 1.72/1.39 % (2371)Termination phase: shuffling
% 1.72/1.39
% 1.72/1.39 % (2371)Memory used [KB]: 1023
% 1.72/1.39 % (2371)Time elapsed: 0.003 s
% 1.72/1.39 % (2371)Instructions burned: 3 (million)
% 1.72/1.39 % (2371)------------------------------
% 1.72/1.39 % (2371)------------------------------
% 1.72/1.39 % (2374)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/3Mi)
% 1.72/1.39 % (2374)Instruction limit reached!
% 1.72/1.39 % (2374)------------------------------
% 1.72/1.39 % (2374)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.72/1.39 % (2374)Termination reason: Unknown
% 1.72/1.39 % (2374)Termination phase: Unused predicate definition removal
% 1.72/1.39
% 1.72/1.39 % (2374)Memory used [KB]: 1023
% 1.72/1.39 % (2374)Time elapsed: 0.003 s
% 1.72/1.39 % (2374)Instructions burned: 3 (million)
% 1.72/1.39 % (2374)------------------------------
% 1.72/1.39 % (2374)------------------------------
% 1.87/1.40 % (2375)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/37Mi)
% 1.87/1.40 % (2376)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/15Mi)
% 1.87/1.40 % (2376)Instruction limit reached!
% 1.87/1.40 % (2376)------------------------------
% 1.87/1.40 % (2376)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.40 % (2376)Termination reason: Unknown
% 1.87/1.40 % (2376)Termination phase: Saturation
% 1.87/1.40
% 1.87/1.40 % (2376)Memory used [KB]: 1279
% 1.87/1.40 % (2376)Time elapsed: 0.006 s
% 1.87/1.40 % (2376)Instructions burned: 18 (million)
% 1.87/1.40 % (2376)------------------------------
% 1.87/1.40 % (2376)------------------------------
% 1.87/1.40 % (2379)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/7Mi)
% 1.87/1.41 % (2379)Instruction limit reached!
% 1.87/1.41 % (2379)------------------------------
% 1.87/1.41 % (2379)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.41 % (2379)Termination reason: Unknown
% 1.87/1.41 % (2379)Termination phase: Function definition elimination
% 1.87/1.41
% 1.87/1.41 % (2379)Memory used [KB]: 1151
% 1.87/1.41 % (2379)Time elapsed: 0.005 s
% 1.87/1.41 % (2379)Instructions burned: 10 (million)
% 1.87/1.41 % (2379)------------------------------
% 1.87/1.41 % (2379)------------------------------
% 1.87/1.41 % (2377)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/3Mi)
% 1.87/1.41 % (2378)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/1041Mi)
% 1.87/1.41 % (2377)Instruction limit reached!
% 1.87/1.41 % (2377)------------------------------
% 1.87/1.41 % (2377)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.41 % (2377)Termination reason: Unknown
% 1.87/1.41 % (2377)Termination phase: Preprocessing 2
% 1.87/1.41
% 1.87/1.41 % (2377)Memory used [KB]: 1023
% 1.87/1.41 % (2377)Time elapsed: 0.004 s
% 1.87/1.41 % (2377)Instructions burned: 3 (million)
% 1.87/1.41 % (2377)------------------------------
% 1.87/1.41 % (2377)------------------------------
% 1.87/1.41 % (2375)Instruction limit reached!
% 1.87/1.41 % (2375)------------------------------
% 1.87/1.41 % (2375)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.41 % (2375)Termination reason: Unknown
% 1.87/1.41 % (2375)Termination phase: Saturation
% 1.87/1.41
% 1.87/1.41 % (2375)Memory used [KB]: 5884
% 1.87/1.41 % (2375)Time elapsed: 0.014 s
% 1.87/1.41 % (2375)Instructions burned: 38 (million)
% 1.87/1.41 % (2375)------------------------------
% 1.87/1.41 % (2375)------------------------------
% 1.87/1.41 % (2380)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/16Mi)
% 1.87/1.42 % (2381)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/3Mi)
% 1.87/1.42 % (2380)Instruction limit reached!
% 1.87/1.42 % (2380)------------------------------
% 1.87/1.42 % (2380)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.42 % (2380)Termination reason: Unknown
% 1.87/1.42 % (2380)Termination phase: Saturation
% 1.87/1.42
% 1.87/1.42 % (2380)Memory used [KB]: 5756
% 1.87/1.42 % (2380)Time elapsed: 0.006 s
% 1.87/1.42 % (2380)Instructions burned: 17 (million)
% 1.87/1.42 % (2380)------------------------------
% 1.87/1.42 % (2380)------------------------------
% 1.87/1.42 % (2381)Instruction limit reached!
% 1.87/1.42 % (2381)------------------------------
% 1.87/1.42 % (2381)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.42 % (2381)Termination reason: Unknown
% 1.87/1.42 % (2381)Termination phase: Preprocessing 1
% 1.87/1.42
% 1.87/1.42 % (2381)Memory used [KB]: 1023
% 1.87/1.42 % (2381)Time elapsed: 0.003 s
% 1.87/1.42 % (2381)Instructions burned: 4 (million)
% 1.87/1.42 % (2381)------------------------------
% 1.87/1.42 % (2381)------------------------------
% 1.87/1.42 % (2382)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/3Mi)
% 1.87/1.42 % (2382)Instruction limit reached!
% 1.87/1.42 % (2382)------------------------------
% 1.87/1.42 % (2382)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.42 % (2382)Termination reason: Unknown
% 1.87/1.42 % (2382)Termination phase: Unused predicate definition removal
% 1.87/1.42
% 1.87/1.42 % (2382)Memory used [KB]: 1023
% 1.87/1.42 % (2382)Time elapsed: 0.003 s
% 1.87/1.42 % (2382)Instructions burned: 4 (million)
% 1.87/1.42 % (2382)------------------------------
% 1.87/1.42 % (2382)------------------------------
% 1.87/1.43 % (2384)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/3Mi)
% 1.87/1.43 % (2383)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/7Mi)
% 1.87/1.43 % (2384)Instruction limit reached!
% 1.87/1.43 % (2384)------------------------------
% 1.87/1.43 % (2384)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.43 % (2384)Termination reason: Unknown
% 1.87/1.43 % (2384)Termination phase: shuffling
% 1.87/1.43
% 1.87/1.43 % (2384)Memory used [KB]: 1023
% 1.87/1.43 % (2384)Time elapsed: 0.002 s
% 1.87/1.43 % (2384)Instructions burned: 4 (million)
% 1.87/1.43 % (2384)------------------------------
% 1.87/1.43 % (2384)------------------------------
% 1.87/1.43 % (2385)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/4Mi)
% 1.87/1.43 % (2385)Instruction limit reached!
% 1.87/1.43 % (2385)------------------------------
% 1.87/1.43 % (2385)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.43 % (2385)Termination reason: Unknown
% 1.87/1.43 % (2385)Termination phase: Naming
% 1.87/1.43
% 1.87/1.43 % (2385)Memory used [KB]: 1023
% 1.87/1.43 % (2385)Time elapsed: 0.003 s
% 1.87/1.43 % (2385)Instructions burned: 4 (million)
% 1.87/1.43 % (2385)------------------------------
% 1.87/1.43 % (2385)------------------------------
% 1.87/1.43 % (2383)Instruction limit reached!
% 1.87/1.43 % (2383)------------------------------
% 1.87/1.43 % (2383)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.43 % (2383)Termination reason: Unknown
% 1.87/1.43 % (2383)Termination phase: Property scanning
% 1.87/1.43
% 1.87/1.43 % (2383)Memory used [KB]: 1151
% 1.87/1.43 % (2383)Time elapsed: 0.006 s
% 1.87/1.43 % (2383)Instructions burned: 7 (million)
% 1.87/1.43 % (2383)------------------------------
% 1.87/1.43 % (2383)------------------------------
% 1.87/1.43 % (2386)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/18Mi)
% 1.87/1.44 % (2386)Instruction limit reached!
% 1.87/1.44 % (2386)------------------------------
% 1.87/1.44 % (2386)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.44 % (2386)Termination reason: Unknown
% 1.87/1.44 % (2386)Termination phase: Saturation
% 1.87/1.44
% 1.87/1.44 % (2386)Memory used [KB]: 5756
% 1.87/1.44 % (2386)Time elapsed: 0.008 s
% 1.87/1.44 % (2386)Instructions burned: 19 (million)
% 1.87/1.44 % (2386)------------------------------
% 1.87/1.44 % (2386)------------------------------
% 1.87/1.44 % (2387)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/710Mi)
% 1.87/1.44 % (2388)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/6Mi)
% 1.87/1.44 % (2388)Instruction limit reached!
% 1.87/1.44 % (2388)------------------------------
% 1.87/1.44 % (2388)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.44 % (2388)Termination reason: Unknown
% 1.87/1.44 % (2388)Termination phase: Property scanning
% 1.87/1.44
% 1.87/1.44 % (2388)Memory used [KB]: 1151
% 1.87/1.44 % (2388)Time elapsed: 0.004 s
% 1.87/1.44 % (2388)Instructions burned: 7 (million)
% 1.87/1.44 % (2388)------------------------------
% 1.87/1.44 % (2388)------------------------------
% 1.87/1.45 % (2390)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/21Mi)
% 1.87/1.45 % (2389)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/902Mi)
% 1.87/1.45 % (2391)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/5Mi)
% 1.87/1.45 % (2390)Instruction limit reached!
% 1.87/1.45 % (2390)------------------------------
% 1.87/1.45 % (2390)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.45 % (2390)Termination reason: Unknown
% 1.87/1.45 % (2390)Termination phase: Property scanning
% 1.87/1.45
% 1.87/1.45 % (2390)Memory used [KB]: 1535
% 1.87/1.45 % (2390)Time elapsed: 0.008 s
% 1.87/1.45 % (2390)Instructions burned: 21 (million)
% 1.87/1.45 % (2390)------------------------------
% 1.87/1.45 % (2390)------------------------------
% 1.87/1.46 % (2391)Instruction limit reached!
% 1.87/1.46 % (2391)------------------------------
% 1.87/1.46 % (2391)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.46 % (2391)Termination reason: Unknown
% 1.87/1.46 % (2391)Termination phase: Property scanning
% 1.87/1.46
% 1.87/1.46 % (2391)Memory used [KB]: 1023
% 1.87/1.46 % (2391)Time elapsed: 0.003 s
% 1.87/1.46 % (2391)Instructions burned: 6 (million)
% 1.87/1.46 % (2391)------------------------------
% 1.87/1.46 % (2391)------------------------------
% 1.87/1.47 % (2392)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/6Mi)
% 1.87/1.47 % (2393)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_2251 for (2999ds/377Mi)
% 1.87/1.47 % (2392)Instruction limit reached!
% 1.87/1.47 % (2392)------------------------------
% 1.87/1.47 % (2392)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.47 % (2392)Termination reason: Unknown
% 1.87/1.47 % (2392)Termination phase: Property scanning
% 1.87/1.47
% 1.87/1.47 % (2392)Memory used [KB]: 1023
% 1.87/1.47 % (2392)Time elapsed: 0.004 s
% 1.87/1.47 % (2392)Instructions burned: 7 (million)
% 1.87/1.47 % (2392)------------------------------
% 1.87/1.47 % (2392)------------------------------
% 1.87/1.48 % (2394)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_2251 for (2998ds/779Mi)
% 1.87/1.48 % (2367)Instruction limit reached!
% 1.87/1.48 % (2367)------------------------------
% 1.87/1.48 % (2367)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.48 % (2367)Termination reason: Unknown
% 1.87/1.48 % (2367)Termination phase: Saturation
% 1.87/1.48
% 1.87/1.48 % (2367)Memory used [KB]: 6908
% 1.87/1.48 % (2367)Time elapsed: 0.095 s
% 1.87/1.48 % (2367)Instructions burned: 183 (million)
% 1.87/1.48 % (2367)------------------------------
% 1.87/1.48 % (2367)------------------------------
% 1.87/1.49 % (2395)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_2251 for (2998ds/19Mi)
% 1.87/1.50 % (2395)Instruction limit reached!
% 1.87/1.50 % (2395)------------------------------
% 1.87/1.50 % (2395)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.50 % (2395)Termination reason: Unknown
% 1.87/1.50 % (2395)Termination phase: Saturation
% 1.87/1.50
% 1.87/1.50 % (2395)Memory used [KB]: 5628
% 1.87/1.50 % (2395)Time elapsed: 0.008 s
% 1.87/1.50 % (2395)Instructions burned: 21 (million)
% 1.87/1.50 % (2395)------------------------------
% 1.87/1.50 % (2395)------------------------------
% 1.87/1.51 % (2396)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_2251 for (2998ds/879Mi)
% 1.87/1.54 % (2372)Instruction limit reached!
% 1.87/1.54 % (2372)------------------------------
% 1.87/1.54 % (2372)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.54 % (2372)Termination reason: Unknown
% 1.87/1.54 % (2372)Termination phase: Saturation
% 1.87/1.54
% 1.87/1.54 % (2372)Memory used [KB]: 6268
% 1.87/1.54 % (2372)Time elapsed: 0.150 s
% 1.87/1.54 % (2372)Instructions burned: 277 (million)
% 1.87/1.54 % (2372)------------------------------
% 1.87/1.54 % (2372)------------------------------
% 1.87/1.54 % (2394)First to succeed.
% 1.87/1.55 % (2394)Refutation found. Thanks to Tanya!
% 1.87/1.55 % SZS status Theorem for DTF2THF_2251
% 1.87/1.55 % SZS output start Proof for DTF2THF_2251
% 1.87/1.55 thf(type_def_6, type, tyop_2Eextreal_2Eextreal: $tType).
% 1.87/1.55 thf(func_def_0, type, tyop_2Eextreal_2Eextreal: $tType).
% 1.87/1.55 thf(func_def_1, type, tyop_2Emin_2Ebool: $tType).
% 1.87/1.55 thf(func_def_2, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 1.87/1.55 thf(func_def_3, type, c_2Ebool_2E_21: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.87/1.55 thf(func_def_4, type, c_2Ebool_2E_2F_5C: $o > $o > $o).
% 1.87/1.55 thf(func_def_5, type, c_2Emin_2E_3D: !>[X0: $tType]:(X0 > X0 > $o)).
% 1.87/1.55 thf(func_def_6, type, c_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 1.87/1.55 thf(func_def_7, type, c_2Ebool_2E_3F: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.87/1.55 thf(func_def_8, type, c_2Ebool_2ECOND: !>[X0: $tType]:($o > X0 > X0 > X0)).
% 1.87/1.55 thf(func_def_11, type, c_2Ebool_2E_5C_2F: $o > $o > $o).
% 1.87/1.55 thf(func_def_12, type, c_2Eextreal_2Eextreal__le: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > $o).
% 1.87/1.55 thf(func_def_13, type, c_2Eextreal_2Eextreal__max: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal).
% 1.87/1.55 thf(func_def_14, type, c_2Ebool_2E_7E: $o > $o).
% 1.87/1.55 thf(func_def_31, type, sK1: tyop_2Eextreal_2Eextreal).
% 1.87/1.55 thf(func_def_32, type, sK2: tyop_2Eextreal_2Eextreal).
% 1.87/1.55 thf(func_def_33, type, sK3: tyop_2Eextreal_2Eextreal).
% 1.87/1.55 thf(f2038,plain,(
% 1.87/1.55 $false),
% 1.87/1.55 inference(avatar_sat_refutation,[status(thm)],[f1288,f1299,f1304,f1363,f1432,f1434,f1436,f1474,f1784,f1875,f1940,f2037])).
% 1.87/1.55 thf(f2037,plain,(
% 1.87/1.55 spl0_4 | ~spl0_5 | spl0_6),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f2036])).
% 1.87/1.55 thf(f2036,plain,(
% 1.87/1.55 $false | (spl0_4 | ~spl0_5 | spl0_6)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f2035])).
% 1.87/1.55 thf(f2035,plain,(
% 1.87/1.55 ($false = $true) | (spl0_4 | ~spl0_5 | spl0_6)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f2024,f1958])).
% 1.87/1.55 thf(f1958,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false) | (spl0_4 | ~spl0_5)),
% 1.87/1.55 inference(subsumption_resolution,[status(thm)],[f1952,f1283])).
% 1.87/1.55 thf(f1283,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $false) | ~spl0_5),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1281])).
% 1.87/1.55 thf(f1281,definition,(
% 1.87/1.55 spl0_5 <=> ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $false)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition])).
% 1.87/1.55 thf(f1952,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) != $false) | ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false) | spl0_4),
% 1.87/1.55 inference(superposition,[status(thm)],[f1278,f1407])).
% 1.87/1.55 thf(f1407,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__max @ X2 @ X1) = X1) | ((c_2Eextreal_2Eextreal__le @ X2 @ X1) = $false)) )),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1398,f183])).
% 1.87/1.55 thf(f183,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1) = X2)) )),
% 1.87/1.55 inference(equality_proxy_clausification,[status(thm)],[f181])).
% 1.87/1.55 thf(f181,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1) = X2) = $true)) )),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f179])).
% 1.87/1.55 thf(f179,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1) = X2) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1) = X1)) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f178])).
% 1.87/1.55 thf(f178,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((^[Y0 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y0 @ X1) = Y0) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y0 @ X1) = X1))) @ X2) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f177])).
% 1.87/1.55 thf(f177,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X1 : X0] : (((!! @ X0 @ (^[Y0 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y0 @ X1) = Y0) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y0 @ X1) = X1)))) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f176])).
% 1.87/1.55 thf(f176,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X1 : X0] : ((((^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0))))) @ X1) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f138])).
% 1.87/1.55 thf(f138,plain,(
% 1.87/1.55 ( ! [X0 : $tType] : (((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0)))))) = $true)) )),
% 1.87/1.55 inference(definition_unfolding,[status(thm)],[f117,f134])).
% 1.87/1.55 thf(f134,plain,(
% 1.87/1.55 (c_2Ebool_2ET = $true)),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f63])).
% 1.87/1.55 thf(f63,plain,(
% 1.87/1.55 (c_2Ebool_2ET = $true)),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f62])).
% 1.87/1.55 thf(f62,plain,(
% 1.87/1.55 c_2Ebool_2ET),
% 1.87/1.55 inference(rectify,[status(thm)],[f8])).
% 1.87/1.55 thf(f8,axiom,(
% 1.87/1.55 c_2Ebool_2ET),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Ebool_2ETRUTH)).
% 1.87/1.55 thf(f117,plain,(
% 1.87/1.55 ( ! [X0 : $tType] : (((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0)))))) = $true)) )),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f108])).
% 1.87/1.55 thf(f108,plain,(
% 1.87/1.55 ! [X0 : $tType] : ((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0)))))) = $true)),
% 1.87/1.55 inference(closure,[status(thm)],[f91])).
% 1.87/1.55 thf(f91,plain,(
% 1.87/1.55 ( ! [X0 : $tType] : (((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0)))))) = $true)) )),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f90])).
% 1.87/1.55 thf(f90,plain,(
% 1.87/1.55 ! [X0 : $tType,X1 : X0,X2 : X0] : (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2) = X2) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2) = X1))),
% 1.87/1.55 inference(rectify,[status(thm)],[f18])).
% 1.87/1.55 thf(f18,axiom,(
% 1.87/1.55 ! [X0 : $tType,X5 : X0,X6 : X0] : (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X5 @ X6) = X6) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X5 @ X6) = X5))),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Ebool_2ECOND__CLAUSES)).
% 1.87/1.55 thf(f1398,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X2 @ X1) = $false) | ((c_2Eextreal_2Eextreal__max @ X2 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $true @ X1 @ X2))) )),
% 1.87/1.55 inference(fool_paramodulation,[status(thm)],[f733])).
% 1.87/1.55 thf(f733,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__max @ X2 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X2 @ X1) @ X1 @ X2))) )),
% 1.87/1.55 inference(equality_proxy_clausification,[status(thm)],[f732])).
% 1.87/1.55 thf(f732,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__max @ X2 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X2 @ X1) @ X1 @ X2)) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f731])).
% 1.87/1.55 thf(f731,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y0 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y0 @ X1) @ X1 @ Y0))) @ X2) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f730])).
% 1.87/1.55 thf(f730,plain,(
% 1.87/1.55 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y0 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y0 @ X1) @ X1 @ Y0)))) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f729])).
% 1.87/1.55 thf(f729,plain,(
% 1.87/1.55 ( ! [X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y1 @ Y0) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y1 @ Y0) @ Y0 @ Y1))))) @ X1) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f110])).
% 1.87/1.55 thf(f110,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y1 @ Y0) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y1 @ Y0) @ Y0 @ Y1)))))) = $true)),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f87])).
% 1.87/1.55 thf(f87,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y1 @ Y0) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y1 @ Y0) @ Y0 @ Y1)))))) = $true)),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f86])).
% 1.87/1.55 thf(f86,plain,(
% 1.87/1.55 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__max @ X0 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X0 @ X1) @ X1 @ X0))),
% 1.87/1.55 inference(rectify,[status(thm)],[f24])).
% 1.87/1.55 thf(f24,axiom,(
% 1.87/1.55 ! [X8 : tyop_2Eextreal_2Eextreal,X9 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__max @ X8 @ X9) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X8 @ X9) @ X9 @ X8))),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Eextreal__max__def)).
% 1.87/1.55 thf(f1278,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) != $false) | spl0_4),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1277])).
% 1.87/1.55 thf(f1277,definition,(
% 1.87/1.55 spl0_4 <=> ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $false)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition])).
% 1.87/1.55 thf(f2024,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $true) | (~spl0_5 | spl0_6)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f2019])).
% 1.87/1.55 thf(f2019,plain,(
% 1.87/1.55 ($false = $true) | ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $true) | (~spl0_5 | spl0_6)),
% 1.87/1.55 inference(superposition,[status(thm)],[f1881,f1946])).
% 1.87/1.55 thf(f1946,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK3 @ sK1) = $true) | ~spl0_5),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1944])).
% 1.87/1.55 thf(f1944,plain,(
% 1.87/1.55 ($false = $true) | ((c_2Eextreal_2Eextreal__le @ sK3 @ sK1) = $true) | ~spl0_5),
% 1.87/1.55 inference(superposition,[status(thm)],[f914,f1283])).
% 1.87/1.55 thf(f914,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X2 @ X1) = $true) | ((c_2Eextreal_2Eextreal__le @ X1 @ X2) = $true)) )),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f913])).
% 1.87/1.55 thf(f913,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ X2 @ X1) | (c_2Eextreal_2Eextreal__le @ X1 @ X2)) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f912])).
% 1.87/1.55 thf(f912,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y0 @ X1) | (c_2Eextreal_2Eextreal__le @ X1 @ Y0))) @ X2) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f911])).
% 1.87/1.55 thf(f911,plain,(
% 1.87/1.55 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y0 @ X1) | (c_2Eextreal_2Eextreal__le @ X1 @ Y0)))) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f910])).
% 1.87/1.55 thf(f910,plain,(
% 1.87/1.55 ( ! [X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) | (c_2Eextreal_2Eextreal__le @ Y0 @ Y1))))) @ X1) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f125])).
% 1.87/1.55 thf(f125,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) | (c_2Eextreal_2Eextreal__le @ Y0 @ Y1)))))) = $true)),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f99])).
% 1.87/1.55 thf(f99,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) | (c_2Eextreal_2Eextreal__le @ Y0 @ Y1)))))) = $true)),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f98])).
% 1.87/1.55 thf(f98,plain,(
% 1.87/1.55 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ X1 @ X0) | (c_2Eextreal_2Eextreal__le @ X0 @ X1))),
% 1.87/1.55 inference(rectify,[status(thm)],[f23])).
% 1.87/1.55 thf(f23,axiom,(
% 1.87/1.55 ! [X8 : tyop_2Eextreal_2Eextreal,X9 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ X9 @ X8) | (c_2Eextreal_2Eextreal__le @ X8 @ X9))),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Ele__total)).
% 1.87/1.55 thf(f1881,plain,(
% 1.87/1.55 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ sK3 @ X0) = $false) | ((c_2Eextreal_2Eextreal__le @ sK2 @ X0) = $true)) ) | spl0_6),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1878])).
% 1.87/1.55 thf(f1878,plain,(
% 1.87/1.55 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (($false != $false) | ((c_2Eextreal_2Eextreal__le @ sK2 @ X0) = $true) | ((c_2Eextreal_2Eextreal__le @ sK3 @ X0) = $false)) ) | spl0_6),
% 1.87/1.55 inference(superposition,[status(thm)],[f1286,f888])).
% 1.87/1.55 thf(f888,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X3 @ X2) = $false) | ((c_2Eextreal_2Eextreal__le @ X3 @ X1) = $true) | ((c_2Eextreal_2Eextreal__le @ X2 @ X1) = $false)) )),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f887])).
% 1.87/1.55 thf(f887,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X3 @ X1) = $true) | (((c_2Eextreal_2Eextreal__le @ X2 @ X1) & (c_2Eextreal_2Eextreal__le @ X3 @ X2)) = $false)) )),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f886])).
% 1.87/1.55 thf(f886,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((((c_2Eextreal_2Eextreal__le @ X2 @ X1) & (c_2Eextreal_2Eextreal__le @ X3 @ X2)) => (c_2Eextreal_2Eextreal__le @ X3 @ X1)) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f885])).
% 1.87/1.55 thf(f885,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ X2 @ X1) & (c_2Eextreal_2Eextreal__le @ Y0 @ X2)) => (c_2Eextreal_2Eextreal__le @ Y0 @ X1))) @ X3) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f884])).
% 1.87/1.55 thf(f884,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ X2 @ X1) & (c_2Eextreal_2Eextreal__le @ Y0 @ X2)) => (c_2Eextreal_2Eextreal__le @ Y0 @ X1)))) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f883])).
% 1.87/1.55 thf(f883,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ X1) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y0)) => (c_2Eextreal_2Eextreal__le @ Y1 @ X1))))) @ X2) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f882])).
% 1.87/1.55 thf(f882,plain,(
% 1.87/1.55 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ X1) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y0)) => (c_2Eextreal_2Eextreal__le @ Y1 @ X1)))))) = $true)) )),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f881])).
% 1.87/1.55 thf(f881,plain,(
% 1.87/1.55 ( ! [X1 : tyop_2Eextreal_2Eextreal] : ((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) & (c_2Eextreal_2Eextreal__le @ Y2 @ Y1)) => (c_2Eextreal_2Eextreal__le @ Y2 @ Y0))))))) @ X1) = $true)) )),
% 1.87/1.55 inference(pi_clausification,[status(thm)],[f129])).
% 1.87/1.55 thf(f129,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) & (c_2Eextreal_2Eextreal__le @ Y2 @ Y1)) => (c_2Eextreal_2Eextreal__le @ Y2 @ Y0)))))))) = $true)),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f89])).
% 1.87/1.55 thf(f89,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) & (c_2Eextreal_2Eextreal__le @ Y2 @ Y1)) => (c_2Eextreal_2Eextreal__le @ Y2 @ Y0)))))))) = $true)),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f88])).
% 1.87/1.55 thf(f88,plain,(
% 1.87/1.55 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X0 @ X1) & (c_2Eextreal_2Eextreal__le @ X1 @ X2)) => (c_2Eextreal_2Eextreal__le @ X0 @ X2))),
% 1.87/1.55 inference(rectify,[status(thm)],[f22])).
% 1.87/1.55 thf(f22,axiom,(
% 1.87/1.55 ! [X8 : tyop_2Eextreal_2Eextreal,X9 : tyop_2Eextreal_2Eextreal,X13 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X8 @ X9) & (c_2Eextreal_2Eextreal__le @ X9 @ X13)) => (c_2Eextreal_2Eextreal__le @ X8 @ X13))),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Ele__trans)).
% 1.87/1.55 thf(f1286,plain,(
% 1.87/1.55 ($false != (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) | spl0_6),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1285])).
% 1.87/1.55 thf(f1285,definition,(
% 1.87/1.55 spl0_6 <=> ($false = (c_2Eextreal_2Eextreal__le @ sK2 @ sK3))),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition])).
% 1.87/1.55 thf(f1940,plain,(
% 1.87/1.55 ~spl0_2 | ~spl0_4 | spl0_5 | spl0_6),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f1939])).
% 1.87/1.55 thf(f1939,plain,(
% 1.87/1.55 $false | (~spl0_2 | ~spl0_4 | spl0_5 | spl0_6)),
% 1.87/1.55 inference(subsumption_resolution,[status(thm)],[f1934,f1286])).
% 1.87/1.55 thf(f1934,plain,(
% 1.87/1.55 ($false = (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) | (~spl0_2 | ~spl0_4 | spl0_5)),
% 1.87/1.55 inference(backward_demodulation,[status(thm)],[f1279,f1928])).
% 1.87/1.55 thf(f1928,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__max @ sK2 @ sK1) = sK2) | (~spl0_2 | ~spl0_4 | spl0_5)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1923,f1493])).
% 1.87/1.55 thf(f1493,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ $false @ X2 @ X1) = X1)) ) | ~spl0_2),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f182,f908])).
% 1.87/1.55 thf(f908,plain,(
% 1.87/1.55 (c_2Ebool_2EF = $false) | ~spl0_2),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f906])).
% 1.87/1.55 thf(f906,definition,(
% 1.87/1.55 spl0_2 <=> (c_2Ebool_2EF = $false)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition])).
% 1.87/1.55 thf(f182,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1) = X1)) )),
% 1.87/1.55 inference(equality_proxy_clausification,[status(thm)],[f180])).
% 1.87/1.55 thf(f180,plain,(
% 1.87/1.55 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1) = X1) = $true)) )),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f179])).
% 1.87/1.55 thf(f1923,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__max @ sK2 @ sK1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ sK1 @ sK2)) | (~spl0_4 | spl0_5)),
% 1.87/1.55 inference(superposition,[status(thm)],[f733,f1895])).
% 1.87/1.55 thf(f1895,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false) | (~spl0_4 | spl0_5)),
% 1.87/1.55 inference(subsumption_resolution,[status(thm)],[f1885,f1282])).
% 1.87/1.55 thf(f1282,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) != $false) | spl0_5),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1281])).
% 1.87/1.55 thf(f1885,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $false) | ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false) | ~spl0_4),
% 1.87/1.55 inference(superposition,[status(thm)],[f1279,f1407])).
% 1.87/1.55 thf(f1279,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $false) | ~spl0_4),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1277])).
% 1.87/1.55 thf(f1875,plain,(
% 1.87/1.55 ~spl0_2 | spl0_5 | ~spl0_6 | ~spl0_8),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f1874])).
% 1.87/1.55 thf(f1874,plain,(
% 1.87/1.55 $false | (~spl0_2 | spl0_5 | ~spl0_6 | ~spl0_8)),
% 1.87/1.55 inference(subsumption_resolution,[status(thm)],[f1865,f1282])).
% 1.87/1.55 thf(f1865,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $false) | (~spl0_2 | ~spl0_6 | ~spl0_8)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1857])).
% 1.87/1.55 thf(f1857,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $false) | ($false = $true) | (~spl0_2 | ~spl0_6 | ~spl0_8)),
% 1.87/1.55 inference(superposition,[status(thm)],[f1287,f1751])).
% 1.87/1.55 thf(f1751,plain,(
% 1.87/1.55 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ sK2 @ X0) = $true) | ((c_2Eextreal_2Eextreal__le @ sK1 @ X0) = $false)) ) | (~spl0_2 | ~spl0_6 | ~spl0_8)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1750])).
% 1.87/1.55 thf(f1750,plain,(
% 1.87/1.55 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ sK1 @ X0) = $false) | ($false = $true) | ((c_2Eextreal_2Eextreal__le @ sK2 @ X0) = $true)) ) | (~spl0_2 | ~spl0_6 | ~spl0_8)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1745,f1287])).
% 1.87/1.55 thf(f1745,plain,(
% 1.87/1.55 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ sK2 @ sK3) = $true) | ((c_2Eextreal_2Eextreal__le @ sK2 @ X0) = $true) | ((c_2Eextreal_2Eextreal__le @ sK1 @ X0) = $false)) ) | (~spl0_2 | ~spl0_8)),
% 1.87/1.55 inference(superposition,[status(thm)],[f1298,f1562])).
% 1.87/1.55 thf(f1562,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__max @ X0 @ X1) = X0) | ((c_2Eextreal_2Eextreal__le @ X1 @ X2) = $false) | ((c_2Eextreal_2Eextreal__le @ X0 @ X2) = $true)) ) | ~spl0_2),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1549,f1493])).
% 1.87/1.55 thf(f1549,plain,(
% 1.87/1.55 ( ! [X2 : tyop_2Eextreal_2Eextreal,X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X0 @ X2) = $true) | ((c_2Eextreal_2Eextreal__max @ X0 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ X1 @ X0)) | ((c_2Eextreal_2Eextreal__le @ X1 @ X2) = $false)) )),
% 1.87/1.55 inference(superposition,[status(thm)],[f733,f888])).
% 1.87/1.55 thf(f1298,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $true) | ~spl0_8),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1296])).
% 1.87/1.55 thf(f1296,definition,(
% 1.87/1.55 spl0_8 <=> ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $true)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_8])],[avatar_definition])).
% 1.87/1.55 thf(f1287,plain,(
% 1.87/1.55 ($false = (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) | ~spl0_6),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1285])).
% 1.87/1.55 thf(f1784,plain,(
% 1.87/1.55 ~spl0_2 | spl0_4 | ~spl0_6 | ~spl0_10),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f1783])).
% 1.87/1.55 thf(f1783,plain,(
% 1.87/1.55 $false | (~spl0_2 | spl0_4 | ~spl0_6 | ~spl0_10)),
% 1.87/1.55 inference(subsumption_resolution,[status(thm)],[f1774,f1287])).
% 1.87/1.55 thf(f1774,plain,(
% 1.87/1.55 ($false != (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) | (~spl0_2 | spl0_4 | ~spl0_10)),
% 1.87/1.55 inference(backward_demodulation,[status(thm)],[f1278,f1722])).
% 1.87/1.55 thf(f1722,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__max @ sK2 @ sK1) = sK2) | (~spl0_2 | ~spl0_10)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1717,f1493])).
% 1.87/1.55 thf(f1717,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__max @ sK2 @ sK1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ sK1 @ sK2)) | ~spl0_10),
% 1.87/1.55 inference(superposition,[status(thm)],[f733,f1424])).
% 1.87/1.55 thf(f1424,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false) | ~spl0_10),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1422])).
% 1.87/1.55 thf(f1422,definition,(
% 1.87/1.55 spl0_10 <=> ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition])).
% 1.87/1.55 thf(f1474,plain,(
% 1.87/1.55 ~spl0_6 | ~spl0_7),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f1473])).
% 1.87/1.55 thf(f1473,plain,(
% 1.87/1.55 $false | (~spl0_6 | ~spl0_7)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1472])).
% 1.87/1.55 thf(f1472,plain,(
% 1.87/1.55 ($false = $true) | (~spl0_6 | ~spl0_7)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1294,f1287])).
% 1.87/1.55 thf(f1294,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK2 @ sK3) = $true) | ~spl0_7),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1292])).
% 1.87/1.55 thf(f1292,definition,(
% 1.87/1.55 spl0_7 <=> ((c_2Eextreal_2Eextreal__le @ sK2 @ sK3) = $true)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_7])],[avatar_definition])).
% 1.87/1.55 thf(f1436,plain,(
% 1.87/1.55 spl0_10 | ~spl0_5 | spl0_4),
% 1.87/1.55 inference(avatar_split_clause,[status(thm)],[f1416,f1277,f1281,f1422])).
% 1.87/1.55 thf(f1416,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) != $false) | ((c_2Eextreal_2Eextreal__le @ sK2 @ sK1) = $false) | spl0_4),
% 1.87/1.55 inference(superposition,[status(thm)],[f1278,f1407])).
% 1.87/1.55 thf(f1434,plain,(
% 1.87/1.55 spl0_2),
% 1.87/1.55 inference(avatar_split_clause,[status(thm)],[f169,f906])).
% 1.87/1.55 thf(f169,plain,(
% 1.87/1.55 (c_2Ebool_2EF = $false)),
% 1.87/1.55 inference(not_proxy_clausification,[status(thm)],[f167])).
% 1.87/1.55 thf(f167,plain,(
% 1.87/1.55 ((~ c_2Ebool_2EF) = $true)),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f165])).
% 1.87/1.55 thf(f165,plain,(
% 1.87/1.55 (((!! @ $o @ (^[Y0 : $o]: ($true))) & (~ c_2Ebool_2EF)) = $true)),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f163])).
% 1.87/1.55 thf(f163,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ($true))) & (~ c_2Ebool_2EF)) & (~ c_2Ebool_2EF)) = $true)),
% 1.87/1.55 inference(boolean_simplification,[status(thm)],[f162])).
% 1.87/1.55 thf(f162,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: (Y0 = Y0))) & (~ c_2Ebool_2EF)) & (~ c_2Ebool_2EF)) = $true)),
% 1.87/1.55 inference(boolean_simplification,[status(thm)],[f161])).
% 1.87/1.55 thf(f161,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ((~ (~ Y0)) = Y0))) & (~ c_2Ebool_2EF)) & (~ c_2Ebool_2EF)) = $true)),
% 1.87/1.55 inference(boolean_simplification,[status(thm)],[f160])).
% 1.87/1.55 thf(f160,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ((~ (~ Y0)) = Y0))) & (c_2Ebool_2EF = $false)) & (~ c_2Ebool_2EF)) = $true)),
% 1.87/1.55 inference(boolean_simplification,[status(thm)],[f159])).
% 1.87/1.55 thf(f159,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ((~ (~ Y0)) = Y0))) & (c_2Ebool_2EF = (~ $true))) & (~ c_2Ebool_2EF)) = $true)),
% 1.87/1.55 inference(boolean_simplification,[status(thm)],[f139])).
% 1.87/1.55 thf(f139,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ((~ (~ Y0)) = Y0))) & (c_2Ebool_2EF = (~ $true))) & ($true = (~ c_2Ebool_2EF))) = $true)),
% 1.87/1.55 inference(definition_unfolding,[status(thm)],[f128,f134,f134])).
% 1.87/1.55 thf(f128,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ((~ (~ Y0)) = Y0))) & (c_2Ebool_2EF = (~ c_2Ebool_2ET))) & (c_2Ebool_2ET = (~ c_2Ebool_2EF))) = $true)),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f45])).
% 1.87/1.55 thf(f45,plain,(
% 1.87/1.55 ((((!! @ $o @ (^[Y0 : $o]: ((~ (~ Y0)) = Y0))) & (c_2Ebool_2EF = (~ c_2Ebool_2ET))) & (c_2Ebool_2ET = (~ c_2Ebool_2EF))) = $true)),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f44])).
% 1.87/1.55 thf(f44,plain,(
% 1.87/1.55 (c_2Ebool_2ET <=> (~ c_2Ebool_2EF)) & (c_2Ebool_2EF <=> (~ c_2Ebool_2ET)) & ! [X0 : $o] : ((~ (~ X0)) <=> X0)),
% 1.87/1.55 inference(rectify,[status(thm)],[f15])).
% 1.87/1.55 thf(f15,axiom,(
% 1.87/1.55 (c_2Ebool_2ET <=> (~ c_2Ebool_2EF)) & (c_2Ebool_2EF <=> (~ c_2Ebool_2ET)) & ! [X7 : $o] : ((~ (~ X7)) <=> X7)),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Ebool_2ENOT__CLAUSES)).
% 1.87/1.55 thf(f1432,plain,(
% 1.87/1.55 ~spl0_5 | ~spl0_9),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f1431])).
% 1.87/1.55 thf(f1431,plain,(
% 1.87/1.55 $false | (~spl0_5 | ~spl0_9)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1430])).
% 1.87/1.55 thf(f1430,plain,(
% 1.87/1.55 ($false = $true) | (~spl0_5 | ~spl0_9)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1303,f1283])).
% 1.87/1.55 thf(f1303,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $true) | ~spl0_9),
% 1.87/1.55 inference(avatar_component_clause,[status(thm)],[f1301])).
% 1.87/1.55 thf(f1301,definition,(
% 1.87/1.55 spl0_9 <=> ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $true)),
% 1.87/1.55 introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition])).
% 1.87/1.55 thf(f1363,plain,(
% 1.87/1.55 ~spl0_4 | ~spl0_8),
% 1.87/1.55 inference(avatar_contradiction_clause,[status(thm)],[f1362])).
% 1.87/1.55 thf(f1362,plain,(
% 1.87/1.55 $false | (~spl0_4 | ~spl0_8)),
% 1.87/1.55 inference(trivial_inequality_removal,[status(thm)],[f1361])).
% 1.87/1.55 thf(f1361,plain,(
% 1.87/1.55 ($false = $true) | (~spl0_4 | ~spl0_8)),
% 1.87/1.55 inference(forward_demodulation,[status(thm)],[f1298,f1279])).
% 1.87/1.55 thf(f1304,plain,(
% 1.87/1.55 spl0_8 | spl0_9),
% 1.87/1.55 inference(avatar_split_clause,[status(thm)],[f1290,f1301,f1296])).
% 1.87/1.55 thf(f1290,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $true) | ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $true)),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f1273])).
% 1.87/1.55 thf(f1273,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $true) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) & (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) = $true)),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f1272])).
% 1.87/1.55 thf(f1272,plain,(
% 1.87/1.55 (((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) & (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) != (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3))),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f1271])).
% 1.87/1.55 thf(f1271,plain,(
% 1.87/1.55 (((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) & (c_2Eextreal_2Eextreal__le @ sK2 @ sK3))) = $false)),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f1270])).
% 1.87/1.55 thf(f1270,plain,(
% 1.87/1.55 ($false = ((^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ Y0) = ((c_2Eextreal_2Eextreal__le @ sK1 @ Y0) & (c_2Eextreal_2Eextreal__le @ sK2 @ Y0)))) @ sK3))),
% 1.87/1.55 inference(sigma_clausification,[status(thm)],[f1269])).
% 1.87/1.55 thf(f1269,plain,(
% 1.87/1.55 ($false = (!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ Y0) = ((c_2Eextreal_2Eextreal__le @ sK1 @ Y0) & (c_2Eextreal_2Eextreal__le @ sK2 @ Y0))))))),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f1268])).
% 1.87/1.55 thf(f1268,plain,(
% 1.87/1.55 (((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y0 @ sK1) @ Y1) = ((c_2Eextreal_2Eextreal__le @ sK1 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y0 @ Y1)))))) @ sK2) = $false)),
% 1.87/1.55 inference(sigma_clausification,[status(thm)],[f1267])).
% 1.87/1.55 thf(f1267,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y0 @ sK1) @ Y1) = ((c_2Eextreal_2Eextreal__le @ sK1 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y0 @ Y1))))))) = $false)),
% 1.87/1.55 inference(beta_eta_normalization,[status(thm)],[f1266])).
% 1.87/1.55 thf(f1266,plain,(
% 1.87/1.55 (((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y1 @ Y0) @ Y2) = ((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)))))))) @ sK1) = $false)),
% 1.87/1.55 inference(sigma_clausification,[status(thm)],[f1265])).
% 1.87/1.55 thf(f1265,plain,(
% 1.87/1.55 ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y1 @ Y0) @ Y2) = ((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2))))))))) = $false)),
% 1.87/1.55 inference(not_proxy_clausification,[status(thm)],[f118])).
% 1.87/1.55 thf(f118,plain,(
% 1.87/1.55 ((~ (!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y1 @ Y0) @ Y2) = ((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)))))))))) = $true)),
% 1.87/1.55 inference(cnf_transformation,[status(thm)],[f75])).
% 1.87/1.55 thf(f75,plain,(
% 1.87/1.55 ((~ (!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y1 @ Y0) @ Y2) = ((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)))))))))) = $true)),
% 1.87/1.55 inference(fool_elimination,[status(thm)],[f74])).
% 1.87/1.55 thf(f74,plain,(
% 1.87/1.55 ~! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ X1 @ X2) @ X0) <=> ((c_2Eextreal_2Eextreal__le @ X1 @ X0) & (c_2Eextreal_2Eextreal__le @ X2 @ X0)))),
% 1.87/1.55 inference(rectify,[status(thm)],[f36])).
% 1.87/1.55 thf(f36,negated_conjecture,(
% 1.87/1.55 ~! [X21 : tyop_2Eextreal_2Eextreal,X4 : tyop_2Eextreal_2Eextreal,X22 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ X4 @ X22) @ X21) <=> ((c_2Eextreal_2Eextreal__le @ X4 @ X21) & (c_2Eextreal_2Eextreal__le @ X22 @ X21)))),
% 1.87/1.55 inference(negated_conjecture,[status(cth)],[f35])).
% 1.87/1.55 thf(f35,conjecture,(
% 1.87/1.55 ! [X21 : tyop_2Eextreal_2Eextreal,X4 : tyop_2Eextreal_2Eextreal,X22 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ X4 @ X22) @ X21) <=> ((c_2Eextreal_2Eextreal__le @ X4 @ X21) & (c_2Eextreal_2Eextreal__le @ X22 @ X21)))),
% 1.87/1.55 file('/export/starexec/sandbox2/tmp/tmp.PiIfeZGtBI/DTF2THF_2251.p',thm_2Eextreal_2Emax__le)).
% 1.87/1.55 thf(f1299,plain,(
% 1.87/1.55 spl0_7 | spl0_8),
% 1.87/1.55 inference(avatar_split_clause,[status(thm)],[f1289,f1296,f1292])).
% 1.87/1.55 thf(f1289,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ sK2 @ sK3) = $true) | ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $true)),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f1273])).
% 1.87/1.55 thf(f1288,plain,(
% 1.87/1.55 spl0_4 | spl0_5 | spl0_6),
% 1.87/1.55 inference(avatar_split_clause,[status(thm)],[f1275,f1285,f1281,f1277])).
% 1.87/1.55 thf(f1275,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $false) | ((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) = $false) | ($false = (c_2Eextreal_2Eextreal__le @ sK2 @ sK3))),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f1274])).
% 1.87/1.55 thf(f1274,plain,(
% 1.87/1.55 ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK2 @ sK1) @ sK3) = $false) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK3) & (c_2Eextreal_2Eextreal__le @ sK2 @ sK3)) = $false)),
% 1.87/1.55 inference(binary_proxy_clausification,[status(thm)],[f1272])).
% 1.87/1.55 % SZS output end Proof for DTF2THF_2251
% 1.87/1.55 % (2394)------------------------------
% 1.87/1.55 % (2394)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.87/1.55 % (2394)Termination reason: Refutation
% 1.87/1.55
% 1.87/1.55 % (2394)Memory used [KB]: 6012
% 1.87/1.55 % (2394)Time elapsed: 0.068 s
% 1.87/1.55 % (2394)Instructions burned: 190 (million)
% 1.87/1.55 % (2394)------------------------------
% 1.87/1.55 % (2394)------------------------------
% 1.87/1.55 % (2366)Success in time 0.178 s
%------------------------------------------------------------------------------