%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP023^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:34 AM UTC 2026
% Result : Theorem 1.81s 1.41s
% Output : Refutation 1.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : ITP023^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.12/0.12 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue Feb 24 08:23:11 EST 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.19/0.45 ---- Original DTF file ---
% 0.19/0.45 thf(spec,logic,$$dhol).
% 0.19/0.45 %------------------------------------------------------------------------------
% 0.19/0.45 % File : ITP023^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.19/0.45 % Domain : Interactive Theorem Proving
% 0.19/0.45 % Problem : HOL4 syntactic export of thm_2Ereal__topology_2EBOUNDED__BALL.p, bushy mode
% 0.19/0.45 % Version : [BG+19] axioms.
% 0.19/0.45 % English :
% 0.19/0.45
% 0.19/0.45 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.19/0.45 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.19/0.45 % Source : [BG+19]
% 0.19/0.45 % Names : thm_2Ereal__topology_2EBOUNDED__BALL.p [Gau19]
% 0.19/0.45 % : HL411001^3.p [TPAP]
% 0.19/0.45
% 0.19/0.45 % Status : Theorem
% 0.19/0.45 % Rating : 0.33 v8.1.0, 0.25 v7.5.0
% 0.19/0.45 % Syntax : Number of formulae : 51 ( 7 unt; 18 typ; 0 def)
% 0.19/0.45 % Number of atoms : 99 ( 9 equ; 46 cnn)
% 0.19/0.45 % Maximal formula atoms : 8 ( 3 avg)
% 0.19/0.45 % Number of connectives : 272 ( 46 ~; 34 |; 25 &; 100 @)
% 0.19/0.45 % ( 38 <=>; 29 =>; 0 <=; 0 <~>)
% 0.19/0.45 % Maximal formula depth : 11 ( 7 avg)
% 0.19/0.45 % Number of types : 3 ( 2 usr)
% 0.19/0.45 % Number of type conns : 34 ( 34 >; 0 *; 0 +; 0 <<)
% 0.19/0.45 % Number of symbols : 18 ( 16 usr; 3 con; 0-4 aty)
% 0.19/0.45 % Number of variables : 72 ( 0 ^; 64 !; 2 ?; 72 :)
% 0.19/0.45 % ( 6 !>; 0 ?*; 0 @-; 0 @+)
% 0.19/0.45 % SPC : TH1_THM_EQU_NAR
% 0.19/0.45
% 0.19/0.45 % Comments :
% 0.19/0.45 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.19/0.45 %------------------------------------------------------------------------------
% 0.19/0.45 thf(tyop_2Emin_2Ebool,type,
% 0.19/0.45 tyop_2Emin_2Ebool: $tType ).
% 0.19/0.45
% 0.19/0.45 thf(tyop_2Emin_2Efun,type,
% 0.19/0.45 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 0.19/0.45
% 0.19/0.45 thf(tyop_2Epair_2Eprod,type,
% 0.19/0.45 tyop_2Epair_2Eprod: $tType > $tType > $tType ).
% 0.19/0.45
% 0.19/0.45 thf(tyop_2Erealax_2Ereal,type,
% 0.19/0.45 tyop_2Erealax_2Ereal: $tType ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2E_21,type,
% 0.19/0.45 c_2Ebool_2E_21:
% 0.19/0.45 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Epair_2E_2C,type,
% 0.19/0.45 c_2Epair_2E_2C:
% 0.19/0.45 !>[A_27a: $tType,A_27b: $tType] : ( A_27a > A_27b > ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2E_2F_5C,type,
% 0.19/0.45 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Emin_2E_3D,type,
% 0.19/0.45 c_2Emin_2E_3D:
% 0.19/0.45 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Emin_2E_3D_3D_3E,type,
% 0.19/0.45 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2E_3F,type,
% 0.19/0.45 c_2Ebool_2E_3F:
% 0.19/0.45 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2EF,type,
% 0.19/0.45 c_2Ebool_2EF: $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Epred__set_2ESUBSET,type,
% 0.19/0.45 c_2Epred__set_2ESUBSET:
% 0.19/0.45 !>[A_27a: $tType] : ( ( A_27a > $o ) > ( A_27a > $o ) > $o ) ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2ET,type,
% 0.19/0.45 c_2Ebool_2ET: $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2E_5C_2F,type,
% 0.19/0.45 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ereal__topology_2Eball,type,
% 0.19/0.45 c_2Ereal__topology_2Eball: ( tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal ) > tyop_2Erealax_2Ereal > $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ereal__topology_2Ebounded__def,type,
% 0.19/0.45 c_2Ereal__topology_2Ebounded__def: ( tyop_2Erealax_2Ereal > $o ) > $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ereal__topology_2Ecball,type,
% 0.19/0.45 c_2Ereal__topology_2Ecball: ( tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal ) > tyop_2Erealax_2Ereal > $o ).
% 0.19/0.45
% 0.19/0.45 thf(c_2Ebool_2E_7E,type,
% 0.19/0.45 c_2Ebool_2E_7E: $o > $o ).
% 0.19/0.45
% 0.19/0.45 thf(logicdef_2E_2F_5C,axiom,
% 0.19/0.45 ! [V0: $o,V1: $o] :
% 0.19/0.45 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.19/0.45 <=> ( V0
% 0.19/0.45 & V1 ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(logicdef_2E_5C_2F,axiom,
% 0.19/0.45 ! [V0: $o,V1: $o] :
% 0.19/0.45 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.19/0.45 <=> ( V0
% 0.19/0.45 | V1 ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(logicdef_2E_7E,axiom,
% 0.19/0.45 ! [V0: $o] :
% 0.19/0.45 ( ( c_2Ebool_2E_7E @ V0 )
% 0.19/0.45 <=> ( (~) @ V0 ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(logicdef_2E_3D_3D_3E,axiom,
% 0.19/0.45 ! [V0: $o,V1: $o] :
% 0.19/0.45 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.19/0.45 <=> ( V0
% 0.19/0.45 => V1 ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(logicdef_2E_3D,axiom,
% 0.19/0.45 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 0.19/0.45 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 0.19/0.45 <=> ( V0 = V1 ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(quantdef_2E_21,axiom,
% 0.19/0.45 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.19/0.45 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 0.19/0.45 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(quantdef_2E_3F,axiom,
% 0.19/0.45 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.19/0.45 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 0.19/0.45 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2ETRUTH,axiom,
% 0.19/0.45 c_2Ebool_2ET ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 0.19/0.45 ! [V0t1: $o,V1t2: $o] :
% 0.19/0.45 ( ( V0t1
% 0.19/0.45 => V1t2 )
% 0.19/0.45 => ( ( V1t2
% 0.19/0.45 => V0t1 )
% 0.19/0.45 => ( V0t1 = V1t2 ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EIMP__F,axiom,
% 0.19/0.45 ! [V0t: $o] :
% 0.19/0.45 ( ( V0t
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 => ( (~) @ V0t ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EF__IMP,axiom,
% 0.19/0.45 ! [V0t: $o] :
% 0.19/0.45 ( ( (~) @ V0t )
% 0.19/0.45 => ( V0t
% 0.19/0.45 => c_2Ebool_2EF ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 0.19/0.45 ! [V0t: $o] :
% 0.19/0.45 ( ( ( c_2Ebool_2ET
% 0.19/0.45 => V0t )
% 0.19/0.45 <=> V0t )
% 0.19/0.45 & ( ( V0t
% 0.19/0.45 => c_2Ebool_2ET )
% 0.19/0.45 <=> c_2Ebool_2ET )
% 0.19/0.45 & ( ( c_2Ebool_2EF
% 0.19/0.45 => V0t )
% 0.19/0.45 <=> c_2Ebool_2ET )
% 0.19/0.45 & ( ( V0t
% 0.19/0.45 => V0t )
% 0.19/0.45 <=> c_2Ebool_2ET )
% 0.19/0.45 & ( ( V0t
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 <=> ( (~) @ V0t ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 0.19/0.45 ( ! [V0t: $o] :
% 0.19/0.45 ( ( (~) @ ( (~) @ V0t ) )
% 0.19/0.45 <=> V0t )
% 0.19/0.45 & ( ( (~) @ c_2Ebool_2ET )
% 0.19/0.45 <=> c_2Ebool_2EF )
% 0.19/0.45 & ( ( (~) @ c_2Ebool_2EF )
% 0.19/0.45 <=> c_2Ebool_2ET ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 0.19/0.45 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 0.19/0.45 ( ( V0x = V1y )
% 0.19/0.45 <=> ( V1y = V0x ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 0.19/0.45 ! [V0t: $o] :
% 0.19/0.45 ( ( ( c_2Ebool_2ET = V0t )
% 0.19/0.45 <=> V0t )
% 0.19/0.45 & ( ( V0t = c_2Ebool_2ET )
% 0.19/0.45 <=> V0t )
% 0.19/0.45 & ( ( c_2Ebool_2EF = V0t )
% 0.19/0.45 <=> ( (~) @ V0t ) )
% 0.19/0.45 & ( ( V0t = c_2Ebool_2EF )
% 0.19/0.45 <=> ( (~) @ V0t ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2ENOT__FORALL__THM,axiom,
% 0.19/0.45 ! [A_27a: $tType,V0P: A_27a > $o] :
% 0.19/0.45 ( ( (~)
% 0.19/0.45 @ ! [V1x: A_27a] : ( V0P @ V1x ) )
% 0.19/0.45 <=> ? [V2x: A_27a] : ( (~) @ ( V0P @ V2x ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EDISJ__ASSOC,axiom,
% 0.19/0.45 ! [V0A: $o,V1B: $o,V2C: $o] :
% 0.19/0.45 ( ( V0A
% 0.19/0.45 | V1B
% 0.19/0.45 | V2C )
% 0.19/0.45 <=> ( V0A
% 0.19/0.45 | V1B
% 0.19/0.45 | V2C ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EDISJ__SYM,axiom,
% 0.19/0.45 ! [V0A: $o,V1B: $o] :
% 0.19/0.45 ( ( V0A
% 0.19/0.45 | V1B )
% 0.19/0.45 <=> ( V1B
% 0.19/0.45 | V0A ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ebool_2EDE__MORGAN__THM,axiom,
% 0.19/0.45 ! [V0A: $o,V1B: $o] :
% 0.19/0.45 ( ( ( (~)
% 0.19/0.45 @ ( V0A
% 0.19/0.45 & V1B ) )
% 0.19/0.45 <=> ( ( (~) @ V0A )
% 0.19/0.45 | ( (~) @ V1B ) ) )
% 0.19/0.45 & ( ( (~)
% 0.19/0.45 @ ( V0A
% 0.19/0.45 | V1B ) )
% 0.19/0.45 <=> ( ( (~) @ V0A )
% 0.19/0.45 & ( (~) @ V1B ) ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ereal__topology_2EBALL__SUBSET__CBALL,axiom,
% 0.19/0.45 ! [V0x: tyop_2Erealax_2Ereal,V1e: tyop_2Erealax_2Ereal] : ( c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ ( c_2Ereal__topology_2Eball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) @ ( c_2Ereal__topology_2Ecball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ereal__topology_2EBOUNDED__SUBSET,axiom,
% 0.19/0.45 ! [V0s: tyop_2Erealax_2Ereal > $o,V1t: tyop_2Erealax_2Ereal > $o] :
% 0.19/0.45 ( ( ( c_2Ereal__topology_2Ebounded__def @ V1t )
% 0.19/0.45 & ( c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ V0s @ V1t ) )
% 0.19/0.45 => ( c_2Ereal__topology_2Ebounded__def @ V0s ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ereal__topology_2EBOUNDED__CBALL,axiom,
% 0.19/0.45 ! [V0x: tyop_2Erealax_2Ereal,V1e: tyop_2Erealax_2Ereal] : ( c_2Ereal__topology_2Ebounded__def @ ( c_2Ereal__topology_2Ecball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2ENOT__NOT,axiom,
% 0.19/0.45 ! [V0t: $o] :
% 0.19/0.45 ( ( (~) @ ( (~) @ V0t ) )
% 0.19/0.45 <=> V0t ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 0.19/0.45 ! [V0A: $o] :
% 0.19/0.45 ( V0A
% 0.19/0.45 => ( ( (~) @ V0A )
% 0.19/0.45 => c_2Ebool_2EF ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 0.19/0.45 ! [V0B: $o,V1A: $o] :
% 0.19/0.45 ( ( ( (~)
% 0.19/0.45 @ ( V1A
% 0.19/0.45 | V0B ) )
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 <=> ( ( V1A
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 => ( ( (~) @ V0B )
% 0.19/0.45 => c_2Ebool_2EF ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 0.19/0.45 ! [V0B: $o,V1A: $o] :
% 0.19/0.45 ( ( ( (~)
% 0.19/0.45 @ ( ( (~) @ V1A )
% 0.19/0.45 | V0B ) )
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 <=> ( V1A
% 0.19/0.45 => ( ( (~) @ V0B )
% 0.19/0.45 => c_2Ebool_2EF ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2EAND__INV2,axiom,
% 0.19/0.45 ! [V0A: $o] :
% 0.19/0.45 ( ( ( (~) @ V0A )
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 => ( ( V0A
% 0.19/0.45 => c_2Ebool_2EF )
% 0.19/0.45 => c_2Ebool_2EF ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2Edc__eq,axiom,
% 0.19/0.45 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.19/0.45 ( ( V2p
% 0.19/0.45 <=> ( V1q = V0r ) )
% 0.19/0.45 <=> ( ( V2p
% 0.19/0.45 | V1q
% 0.19/0.45 | V0r )
% 0.19/0.45 & ( V2p
% 0.19/0.45 | ( (~) @ V0r )
% 0.19/0.45 | ( (~) @ V1q ) )
% 0.19/0.45 & ( V1q
% 0.19/0.45 | ( (~) @ V0r )
% 0.19/0.45 | ( (~) @ V2p ) )
% 0.19/0.45 & ( V0r
% 0.19/0.45 | ( (~) @ V1q )
% 0.19/0.45 | ( (~) @ V2p ) ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2Edc__conj,axiom,
% 0.19/0.45 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.19/0.45 ( ( V2p
% 0.19/0.45 <=> ( V1q
% 0.19/0.45 & V0r ) )
% 0.19/0.45 <=> ( ( V2p
% 0.19/0.45 | ( (~) @ V1q )
% 0.19/0.45 | ( (~) @ V0r ) )
% 0.19/0.45 & ( V1q
% 0.19/0.45 | ( (~) @ V2p ) )
% 0.19/0.45 & ( V0r
% 0.19/0.45 | ( (~) @ V2p ) ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2Edc__disj,axiom,
% 0.19/0.45 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.19/0.45 ( ( V2p
% 0.19/0.45 <=> ( V1q
% 0.19/0.45 | V0r ) )
% 0.19/0.45 <=> ( ( V2p
% 0.19/0.45 | ( (~) @ V1q ) )
% 0.19/0.45 & ( V2p
% 0.19/0.45 | ( (~) @ V0r ) )
% 0.19/0.45 & ( V1q
% 0.19/0.45 | V0r
% 0.19/0.45 | ( (~) @ V2p ) ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2Edc__imp,axiom,
% 0.19/0.45 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.19/0.45 ( ( V2p
% 0.19/0.45 <=> ( V1q
% 0.19/0.45 => V0r ) )
% 0.19/0.45 <=> ( ( V2p
% 0.19/0.45 | V1q )
% 0.19/0.45 & ( V2p
% 0.19/0.45 | ( (~) @ V0r ) )
% 0.19/0.45 & ( ( (~) @ V1q )
% 0.19/0.45 | V0r
% 0.19/0.45 | ( (~) @ V2p ) ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Esat_2Edc__neg,axiom,
% 0.19/0.45 ! [V0q: $o,V1p: $o] :
% 0.19/0.45 ( ( V1p
% 0.19/0.45 <=> ( (~) @ V0q ) )
% 0.19/0.45 <=> ( ( V1p
% 0.19/0.45 | V0q )
% 0.19/0.45 & ( ( (~) @ V0q )
% 0.19/0.45 | ( (~) @ V1p ) ) ) ) ).
% 0.19/0.45
% 0.19/0.45 thf(thm_2Ereal__topology_2EBOUNDED__BALL,conjecture,
% 0.19/0.45 ! [V0x: tyop_2Erealax_2Ereal,V1e: tyop_2Erealax_2Ereal] : ( c_2Ereal__topology_2Ebounded__def @ ( c_2Ereal__topology_2Eball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) ) ).
% 0.19/0.45
% 0.19/0.45 %------------------------------------------------------------------------------
% 0.19/0.45 ------------------------
% 1.66/1.37 ---- Embedded in THF ---
% 1.66/1.37 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.66/1.37 %%% Generated on Tue Feb 24 08:23:12 EST 2026
% 1.66/1.37 %%% using '$$dhol' embedding, version 1.3.0.
% 1.66/1.37 %%% Logic specification used:
% 1.66/1.37 %%% thf(spec, logic, $$dhol).
% 1.66/1.37
% 1.66/1.37 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2DTF20855.p
% 1.66/1.37 thf(tyop_2Emin_2Ebool, type, tyop_2Emin_2Ebool: $tType).
% 1.66/1.37 thf(tyop_2Emin_2Efun, type, tyop_2Emin_2Efun: ($tType > ($tType > $tType))).
% 1.66/1.37 thf(tyop_2Epair_2Eprod, type, tyop_2Epair_2Eprod: ($tType > ($tType > $tType))).
% 1.66/1.37 thf(tyop_2Erealax_2Ereal, type, tyop_2Erealax_2Ereal: $tType).
% 1.66/1.37 thf(c_2Ebool_2E_21, type, c_2Ebool_2E_21: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.66/1.37 thf(c_2Epair_2E_2C, type, c_2Epair_2E_2C: (!> [A_27a:$tType,A_27b:$tType]: ((A_27a > (A_27b > ((tyop_2Epair_2Eprod @ A_27a) @ A_27b)))))).
% 1.66/1.37 thf(c_2Ebool_2E_2F_5C, type, c_2Ebool_2E_2F_5C: ($o > ($o > $o))).
% 1.66/1.37 thf(c_2Emin_2E_3D, type, c_2Emin_2E_3D: (!> [A_27a:$tType]: ((A_27a > (A_27a > $o))))).
% 1.66/1.37 thf(c_2Emin_2E_3D_3D_3E, type, c_2Emin_2E_3D_3D_3E: ($o > ($o > $o))).
% 1.66/1.37 thf(c_2Ebool_2E_3F, type, c_2Ebool_2E_3F: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.66/1.37 thf(c_2Ebool_2EF, type, c_2Ebool_2EF: $o).
% 1.66/1.37 thf(c_2Epred__set_2ESUBSET, type, c_2Epred__set_2ESUBSET: (!> [A_27a:$tType]: (((A_27a > $o) > ((A_27a > $o) > $o))))).
% 1.66/1.37 thf(c_2Ebool_2ET, type, c_2Ebool_2ET: $o).
% 1.66/1.37 thf(c_2Ebool_2E_5C_2F, type, c_2Ebool_2E_5C_2F: ($o > ($o > $o))).
% 1.66/1.37 thf(c_2Ereal__topology_2Eball, type, c_2Ereal__topology_2Eball: (((tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal) @ tyop_2Erealax_2Ereal) > (tyop_2Erealax_2Ereal > $o))).
% 1.66/1.37 thf(c_2Ereal__topology_2Ebounded__def, type, c_2Ereal__topology_2Ebounded__def: ((tyop_2Erealax_2Ereal > $o) > $o)).
% 1.66/1.37 thf(c_2Ereal__topology_2Ecball, type, c_2Ereal__topology_2Ecball: (((tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal) @ tyop_2Erealax_2Ereal) > (tyop_2Erealax_2Ereal > $o))).
% 1.66/1.37 thf(c_2Ebool_2E_7E, type, c_2Ebool_2E_7E: ($o > $o)).
% 1.66/1.37 thf(logicdef_2E_2F_5C, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_2F_5C @ V0) @ V1) <=> (V0 & V1))))).
% 1.66/1.37 thf(logicdef_2E_5C_2F, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_5C_2F @ V0) @ V1) <=> (V0 | V1))))).
% 1.66/1.37 thf(logicdef_2E_7E, axiom, (! [V0:$o]: (((c_2Ebool_2E_7E @ V0) <=> ((~) @ V0))))).
% 1.66/1.37 thf(logicdef_2E_3D_3D_3E, axiom, (! [V0:$o,V1:$o]: ((((c_2Emin_2E_3D_3D_3E @ V0) @ V1) <=> (V0 => V1))))).
% 1.66/1.37 thf(logicdef_2E_3D, axiom, (! [A_27a:$tType,V0:A_27a,V1:A_27a]: (((((c_2Emin_2E_3D @ A_27a) @ V0) @ V1) <=> (V0 = V1))))).
% 1.66/1.37 thf(quantdef_2E_21, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_21 @ A_27a) @ V0f) <=> (! [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.66/1.37 thf(quantdef_2E_3F, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_3F @ A_27a) @ V0f) <=> (? [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.66/1.37 thf(thm_2Ebool_2ETRUTH, axiom, c_2Ebool_2ET).
% 1.66/1.37 thf(thm_2Ebool_2EIMP__ANTISYM__AX, axiom, (! [V0t1:$o,V1t2:$o]: (((V0t1 => V1t2) => ((V1t2 => V0t1) => (V0t1 = V1t2)))))).
% 1.66/1.37 thf(thm_2Ebool_2EIMP__F, axiom, (! [V0t:$o]: (((V0t => c_2Ebool_2EF) => ((~) @ V0t))))).
% 1.66/1.37 thf(thm_2Ebool_2EF__IMP, axiom, (! [V0t:$o]: ((((~) @ V0t) => (V0t => c_2Ebool_2EF))))).
% 1.66/1.37 thf(thm_2Ebool_2EIMP__CLAUSES, axiom, (! [V0t:$o]: ((((c_2Ebool_2ET => V0t) <=> V0t) & (((V0t => c_2Ebool_2ET) <=> c_2Ebool_2ET) & (((c_2Ebool_2EF => V0t) <=> c_2Ebool_2ET) & (((V0t => V0t) <=> c_2Ebool_2ET) & ((V0t => c_2Ebool_2EF) <=> ((~) @ V0t))))))))).
% 1.66/1.37 thf(thm_2Ebool_2ENOT__CLAUSES, axiom, ((! [V0t:$o]: ((((~) @ ((~) @ V0t)) <=> V0t))) & ((((~) @ c_2Ebool_2ET) <=> c_2Ebool_2EF) & (((~) @ c_2Ebool_2EF) <=> c_2Ebool_2ET)))).
% 1.66/1.37 thf(thm_2Ebool_2EEQ__SYM__EQ, axiom, (! [A_27a:$tType,V0x:A_27a,V1y:A_27a]: (((V0x = V1y) <=> (V1y = V0x))))).
% 1.66/1.37 thf(thm_2Ebool_2EEQ__CLAUSES, axiom, (! [V0t:$o]: ((((c_2Ebool_2ET = V0t) <=> V0t) & (((V0t = c_2Ebool_2ET) <=> V0t) & (((c_2Ebool_2EF = V0t) <=> ((~) @ V0t)) & ((V0t = c_2Ebool_2EF) <=> ((~) @ V0t)))))))).
% 1.66/1.37 thf(thm_2Ebool_2ENOT__FORALL__THM, axiom, (! [A_27a:$tType,V0P:(A_27a > $o)]: ((((~) @ (! [V1x:A_27a]: ((V0P @ V1x)))) <=> (? [V2x:A_27a]: (((~) @ (V0P @ V2x)))))))).
% 1.66/1.37 thf(thm_2Ebool_2EDISJ__ASSOC, axiom, (! [V0A:$o,V1B:$o,V2C:$o]: (((V0A | (V1B | V2C)) <=> (V0A | (V1B | V2C)))))).
% 1.66/1.37 thf(thm_2Ebool_2EDISJ__SYM, axiom, (! [V0A:$o,V1B:$o]: (((V0A | V1B) <=> (V1B | V0A))))).
% 1.66/1.37 thf(thm_2Ebool_2EDE__MORGAN__THM, axiom, (! [V0A:$o,V1B:$o]: (((((~) @ (V0A & V1B)) <=> (((~) @ V0A) | ((~) @ V1B))) & (((~) @ (V0A | V1B)) <=> (((~) @ V0A) & ((~) @ V1B))))))).
% 1.66/1.37 thf(thm_2Ereal__topology_2EBALL__SUBSET__CBALL, axiom, (! [V0x:tyop_2Erealax_2Ereal,V1e:tyop_2Erealax_2Ereal]: ((((c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal) @ (c_2Ereal__topology_2Eball @ ((((c_2Epair_2E_2C @ tyop_2Erealax_2Ereal) @ tyop_2Erealax_2Ereal) @ V0x) @ V1e))) @ (c_2Ereal__topology_2Ecball @ ((((c_2Epair_2E_2C @ tyop_2Erealax_2Ereal) @ tyop_2Erealax_2Ereal) @ V0x) @ V1e)))))).
% 1.66/1.37 thf(thm_2Ereal__topology_2EBOUNDED__SUBSET, axiom, (! [V0s:(tyop_2Erealax_2Ereal > $o),V1t:(tyop_2Erealax_2Ereal > $o)]: ((((c_2Ereal__topology_2Ebounded__def @ V1t) & (((c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal) @ V0s) @ V1t)) => (c_2Ereal__topology_2Ebounded__def @ V0s))))).
% 1.66/1.37 thf(thm_2Ereal__topology_2EBOUNDED__CBALL, axiom, (! [V0x:tyop_2Erealax_2Ereal,V1e:tyop_2Erealax_2Ereal]: ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ ((((c_2Epair_2E_2C @ tyop_2Erealax_2Ereal) @ tyop_2Erealax_2Ereal) @ V0x) @ V1e)))))).
% 1.66/1.37 thf(thm_2Esat_2ENOT__NOT, axiom, (! [V0t:$o]: ((((~) @ ((~) @ V0t)) <=> V0t)))).
% 1.66/1.37 thf(thm_2Esat_2EAND__INV__IMP, axiom, (! [V0A:$o]: ((V0A => (((~) @ V0A) => c_2Ebool_2EF))))).
% 1.66/1.37 thf(thm_2Esat_2EOR__DUAL2, axiom, (! [V0B:$o,V1A:$o]: (((((~) @ (V1A | V0B)) => c_2Ebool_2EF) <=> ((V1A => c_2Ebool_2EF) => (((~) @ V0B) => c_2Ebool_2EF)))))).
% 1.66/1.37 thf(thm_2Esat_2EOR__DUAL3, axiom, (! [V0B:$o,V1A:$o]: (((((~) @ (((~) @ V1A) | V0B)) => c_2Ebool_2EF) <=> (V1A => (((~) @ V0B) => c_2Ebool_2EF)))))).
% 1.66/1.37 thf(thm_2Esat_2EAND__INV2, axiom, (! [V0A:$o]: (((((~) @ V0A) => c_2Ebool_2EF) => ((V0A => c_2Ebool_2EF) => c_2Ebool_2EF))))).
% 1.66/1.37 thf(thm_2Esat_2Edc__eq, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q = V0r)) <=> ((V2p | (V1q | V0r)) & ((V2p | (((~) @ V0r) | ((~) @ V1q))) & ((V1q | (((~) @ V0r) | ((~) @ V2p))) & (V0r | (((~) @ V1q) | ((~) @ V2p)))))))))).
% 1.66/1.37 thf(thm_2Esat_2Edc__conj, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q & V0r)) <=> ((V2p | (((~) @ V1q) | ((~) @ V0r))) & ((V1q | ((~) @ V2p)) & (V0r | ((~) @ V2p)))))))).
% 1.66/1.37 thf(thm_2Esat_2Edc__disj, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q | V0r)) <=> ((V2p | ((~) @ V1q)) & ((V2p | ((~) @ V0r)) & (V1q | (V0r | ((~) @ V2p))))))))).
% 1.66/1.37 thf(thm_2Esat_2Edc__imp, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q => V0r)) <=> ((V2p | V1q) & ((V2p | ((~) @ V0r)) & (((~) @ V1q) | (V0r | ((~) @ V2p))))))))).
% 1.66/1.37 thf(thm_2Esat_2Edc__neg, axiom, (! [V0q:$o,V1p:$o]: (((V1p <=> ((~) @ V0q)) <=> ((V1p | V0q) & (((~) @ V0q) | ((~) @ V1p))))))).
% 1.66/1.37 thf(thm_2Ereal__topology_2EBOUNDED__BALL, conjecture, (! [V0x:tyop_2Erealax_2Ereal,V1e:tyop_2Erealax_2Ereal]: ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ ((((c_2Epair_2E_2C @ tyop_2Erealax_2Ereal) @ tyop_2Erealax_2Ereal) @ V0x) @ V1e)))))).
% 1.66/1.37 % SZS output end ListOfTHF for /export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2DTF20855.p
% 1.66/1.37 ------------------------
% 1.66/1.38 ---- Cleaned THF ---
% 1.66/1.38 thf(tyop_2Emin_2Ebool,type,
% 1.66/1.38 tyop_2Emin_2Ebool: $tType ).
% 1.66/1.38
% 1.66/1.38 thf(tyop_2Emin_2Efun,type,
% 1.66/1.38 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 1.66/1.38
% 1.66/1.38 thf(tyop_2Epair_2Eprod,type,
% 1.66/1.38 tyop_2Epair_2Eprod: $tType > $tType > $tType ).
% 1.66/1.38
% 1.66/1.38 thf(tyop_2Erealax_2Ereal,type,
% 1.66/1.38 tyop_2Erealax_2Ereal: $tType ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2E_21,type,
% 1.66/1.38 c_2Ebool_2E_21:
% 1.66/1.38 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Epair_2E_2C,type,
% 1.66/1.38 c_2Epair_2E_2C:
% 1.66/1.38 !>[A_27a: $tType,A_27b: $tType] : ( A_27a > A_27b > ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2E_2F_5C,type,
% 1.66/1.38 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Emin_2E_3D,type,
% 1.66/1.38 c_2Emin_2E_3D:
% 1.66/1.38 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Emin_2E_3D_3D_3E,type,
% 1.66/1.38 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2E_3F,type,
% 1.66/1.38 c_2Ebool_2E_3F:
% 1.66/1.38 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2EF,type,
% 1.66/1.38 c_2Ebool_2EF: $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Epred__set_2ESUBSET,type,
% 1.66/1.38 c_2Epred__set_2ESUBSET:
% 1.66/1.38 !>[A_27a: $tType] : ( ( A_27a > $o ) > ( A_27a > $o ) > $o ) ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2ET,type,
% 1.66/1.38 c_2Ebool_2ET: $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2E_5C_2F,type,
% 1.66/1.38 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ereal__topology_2Eball,type,
% 1.66/1.38 c_2Ereal__topology_2Eball: ( tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal ) > tyop_2Erealax_2Ereal > $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ereal__topology_2Ebounded__def,type,
% 1.66/1.38 c_2Ereal__topology_2Ebounded__def: ( tyop_2Erealax_2Ereal > $o ) > $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ereal__topology_2Ecball,type,
% 1.66/1.38 c_2Ereal__topology_2Ecball: ( tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal ) > tyop_2Erealax_2Ereal > $o ).
% 1.66/1.38
% 1.66/1.38 thf(c_2Ebool_2E_7E,type,
% 1.66/1.38 c_2Ebool_2E_7E: $o > $o ).
% 1.66/1.38
% 1.66/1.38 thf(logicdef_2E_2F_5C,axiom,
% 1.66/1.38 ! [V0: $o,V1: $o] :
% 1.66/1.38 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 1.66/1.38 <=> ( V0
% 1.66/1.38 & V1 ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(logicdef_2E_5C_2F,axiom,
% 1.66/1.38 ! [V0: $o,V1: $o] :
% 1.66/1.38 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 1.66/1.38 <=> ( V0
% 1.66/1.38 | V1 ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(logicdef_2E_7E,axiom,
% 1.66/1.38 ! [V0: $o] :
% 1.66/1.38 ( ( c_2Ebool_2E_7E @ V0 )
% 1.66/1.38 <=> ( (~) @ V0 ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(logicdef_2E_3D_3D_3E,axiom,
% 1.66/1.38 ! [V0: $o,V1: $o] :
% 1.66/1.38 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 1.66/1.38 <=> ( V0
% 1.66/1.38 => V1 ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(logicdef_2E_3D,axiom,
% 1.66/1.38 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 1.66/1.38 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 1.66/1.38 <=> ( V0 = V1 ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(quantdef_2E_21,axiom,
% 1.66/1.38 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.66/1.38 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 1.66/1.38 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(quantdef_2E_3F,axiom,
% 1.66/1.38 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.66/1.38 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 1.66/1.38 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2ETRUTH,axiom,
% 1.66/1.38 c_2Ebool_2ET ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 1.66/1.38 ! [V0t1: $o,V1t2: $o] :
% 1.66/1.38 ( ( V0t1
% 1.66/1.38 => V1t2 )
% 1.66/1.38 => ( ( V1t2
% 1.66/1.38 => V0t1 )
% 1.66/1.38 => ( V0t1 = V1t2 ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EIMP__F,axiom,
% 1.66/1.38 ! [V0t: $o] :
% 1.66/1.38 ( ( V0t
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 => ( (~) @ V0t ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EF__IMP,axiom,
% 1.66/1.38 ! [V0t: $o] :
% 1.66/1.38 ( ( (~) @ V0t )
% 1.66/1.38 => ( V0t
% 1.66/1.38 => c_2Ebool_2EF ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 1.66/1.38 ! [V0t: $o] :
% 1.66/1.38 ( ( ( c_2Ebool_2ET
% 1.66/1.38 => V0t )
% 1.66/1.38 <=> V0t )
% 1.66/1.38 & ( ( V0t
% 1.66/1.38 => c_2Ebool_2ET )
% 1.66/1.38 <=> c_2Ebool_2ET )
% 1.66/1.38 & ( ( c_2Ebool_2EF
% 1.66/1.38 => V0t )
% 1.66/1.38 <=> c_2Ebool_2ET )
% 1.66/1.38 & ( ( V0t
% 1.66/1.38 => V0t )
% 1.66/1.38 <=> c_2Ebool_2ET )
% 1.66/1.38 & ( ( V0t
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 <=> ( (~) @ V0t ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 1.66/1.38 ( ! [V0t: $o] :
% 1.66/1.38 ( ( (~) @ ( (~) @ V0t ) )
% 1.66/1.38 <=> V0t )
% 1.66/1.38 & ( ( (~) @ c_2Ebool_2ET )
% 1.66/1.38 <=> c_2Ebool_2EF )
% 1.66/1.38 & ( ( (~) @ c_2Ebool_2EF )
% 1.66/1.38 <=> c_2Ebool_2ET ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 1.66/1.38 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 1.66/1.38 ( ( V0x = V1y )
% 1.66/1.38 <=> ( V1y = V0x ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 1.66/1.38 ! [V0t: $o] :
% 1.66/1.38 ( ( ( c_2Ebool_2ET = V0t )
% 1.66/1.38 <=> V0t )
% 1.66/1.38 & ( ( V0t = c_2Ebool_2ET )
% 1.66/1.38 <=> V0t )
% 1.66/1.38 & ( ( c_2Ebool_2EF = V0t )
% 1.66/1.38 <=> ( (~) @ V0t ) )
% 1.66/1.38 & ( ( V0t = c_2Ebool_2EF )
% 1.66/1.38 <=> ( (~) @ V0t ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2ENOT__FORALL__THM,axiom,
% 1.66/1.38 ! [A_27a: $tType,V0P: A_27a > $o] :
% 1.66/1.38 ( ( (~)
% 1.66/1.38 @ ! [V1x: A_27a] : ( V0P @ V1x ) )
% 1.66/1.38 <=> ? [V2x: A_27a] : ( (~) @ ( V0P @ V2x ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EDISJ__ASSOC,axiom,
% 1.66/1.38 ! [V0A: $o,V1B: $o,V2C: $o] :
% 1.66/1.38 ( ( V0A
% 1.66/1.38 | V1B
% 1.66/1.38 | V2C )
% 1.66/1.38 <=> ( V0A
% 1.66/1.38 | V1B
% 1.66/1.38 | V2C ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EDISJ__SYM,axiom,
% 1.66/1.38 ! [V0A: $o,V1B: $o] :
% 1.66/1.38 ( ( V0A
% 1.66/1.38 | V1B )
% 1.66/1.38 <=> ( V1B
% 1.66/1.38 | V0A ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ebool_2EDE__MORGAN__THM,axiom,
% 1.66/1.38 ! [V0A: $o,V1B: $o] :
% 1.66/1.38 ( ( ( (~)
% 1.66/1.38 @ ( V0A
% 1.66/1.38 & V1B ) )
% 1.66/1.38 <=> ( ( (~) @ V0A )
% 1.66/1.38 | ( (~) @ V1B ) ) )
% 1.66/1.38 & ( ( (~)
% 1.66/1.38 @ ( V0A
% 1.66/1.38 | V1B ) )
% 1.66/1.38 <=> ( ( (~) @ V0A )
% 1.66/1.38 & ( (~) @ V1B ) ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ereal__topology_2EBALL__SUBSET__CBALL,axiom,
% 1.66/1.38 ! [V0x: tyop_2Erealax_2Ereal,V1e: tyop_2Erealax_2Ereal] : ( c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ ( c_2Ereal__topology_2Eball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) @ ( c_2Ereal__topology_2Ecball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ereal__topology_2EBOUNDED__SUBSET,axiom,
% 1.66/1.38 ! [V0s: tyop_2Erealax_2Ereal > $o,V1t: tyop_2Erealax_2Ereal > $o] :
% 1.66/1.38 ( ( ( c_2Ereal__topology_2Ebounded__def @ V1t )
% 1.66/1.38 & ( c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ V0s @ V1t ) )
% 1.66/1.38 => ( c_2Ereal__topology_2Ebounded__def @ V0s ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ereal__topology_2EBOUNDED__CBALL,axiom,
% 1.66/1.38 ! [V0x: tyop_2Erealax_2Ereal,V1e: tyop_2Erealax_2Ereal] : ( c_2Ereal__topology_2Ebounded__def @ ( c_2Ereal__topology_2Ecball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2ENOT__NOT,axiom,
% 1.66/1.38 ! [V0t: $o] :
% 1.66/1.38 ( ( (~) @ ( (~) @ V0t ) )
% 1.66/1.38 <=> V0t ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 1.66/1.38 ! [V0A: $o] :
% 1.66/1.38 ( V0A
% 1.66/1.38 => ( ( (~) @ V0A )
% 1.66/1.38 => c_2Ebool_2EF ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 1.66/1.38 ! [V0B: $o,V1A: $o] :
% 1.66/1.38 ( ( ( (~)
% 1.66/1.38 @ ( V1A
% 1.66/1.38 | V0B ) )
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 <=> ( ( V1A
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 => ( ( (~) @ V0B )
% 1.66/1.38 => c_2Ebool_2EF ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 1.66/1.38 ! [V0B: $o,V1A: $o] :
% 1.66/1.38 ( ( ( (~)
% 1.66/1.38 @ ( ( (~) @ V1A )
% 1.66/1.38 | V0B ) )
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 <=> ( V1A
% 1.66/1.38 => ( ( (~) @ V0B )
% 1.66/1.38 => c_2Ebool_2EF ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2EAND__INV2,axiom,
% 1.66/1.38 ! [V0A: $o] :
% 1.66/1.38 ( ( ( (~) @ V0A )
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 => ( ( V0A
% 1.66/1.38 => c_2Ebool_2EF )
% 1.66/1.38 => c_2Ebool_2EF ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2Edc__eq,axiom,
% 1.66/1.38 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.66/1.38 ( ( V2p
% 1.66/1.38 <=> ( V1q = V0r ) )
% 1.66/1.38 <=> ( ( V2p
% 1.66/1.38 | V1q
% 1.66/1.38 | V0r )
% 1.66/1.38 & ( V2p
% 1.66/1.38 | ( (~) @ V0r )
% 1.66/1.38 | ( (~) @ V1q ) )
% 1.66/1.38 & ( V1q
% 1.66/1.38 | ( (~) @ V0r )
% 1.66/1.38 | ( (~) @ V2p ) )
% 1.66/1.38 & ( V0r
% 1.66/1.38 | ( (~) @ V1q )
% 1.66/1.38 | ( (~) @ V2p ) ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2Edc__conj,axiom,
% 1.66/1.38 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.66/1.38 ( ( V2p
% 1.66/1.38 <=> ( V1q
% 1.66/1.38 & V0r ) )
% 1.66/1.38 <=> ( ( V2p
% 1.66/1.38 | ( (~) @ V1q )
% 1.66/1.38 | ( (~) @ V0r ) )
% 1.66/1.38 & ( V1q
% 1.66/1.38 | ( (~) @ V2p ) )
% 1.66/1.38 & ( V0r
% 1.66/1.38 | ( (~) @ V2p ) ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2Edc__disj,axiom,
% 1.66/1.38 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.66/1.38 ( ( V2p
% 1.66/1.38 <=> ( V1q
% 1.66/1.38 | V0r ) )
% 1.66/1.38 <=> ( ( V2p
% 1.66/1.38 | ( (~) @ V1q ) )
% 1.66/1.38 & ( V2p
% 1.66/1.38 | ( (~) @ V0r ) )
% 1.66/1.38 & ( V1q
% 1.66/1.38 | V0r
% 1.66/1.38 | ( (~) @ V2p ) ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2Edc__imp,axiom,
% 1.66/1.38 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.66/1.38 ( ( V2p
% 1.66/1.38 <=> ( V1q
% 1.66/1.38 => V0r ) )
% 1.66/1.38 <=> ( ( V2p
% 1.66/1.38 | V1q )
% 1.66/1.38 & ( V2p
% 1.66/1.38 | ( (~) @ V0r ) )
% 1.66/1.38 & ( ( (~) @ V1q )
% 1.66/1.38 | V0r
% 1.66/1.38 | ( (~) @ V2p ) ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Esat_2Edc__neg,axiom,
% 1.66/1.38 ! [V0q: $o,V1p: $o] :
% 1.66/1.38 ( ( V1p
% 1.66/1.38 <=> ( (~) @ V0q ) )
% 1.66/1.38 <=> ( ( V1p
% 1.66/1.38 | V0q )
% 1.66/1.38 & ( ( (~) @ V0q )
% 1.66/1.38 | ( (~) @ V1p ) ) ) ) ).
% 1.66/1.38
% 1.66/1.38 thf(thm_2Ereal__topology_2EBOUNDED__BALL,conjecture,
% 1.66/1.38 ! [V0x: tyop_2Erealax_2Ereal,V1e: tyop_2Erealax_2Ereal] : ( c_2Ereal__topology_2Ebounded__def @ ( c_2Ereal__topology_2Eball @ ( c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ V0x @ V1e ) ) ) ).
% 1.66/1.38 ------------------------
% 1.66/1.40 % (20970)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_20855 for (2999ds/4Mi)
% 1.66/1.40 % (20972)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_20855 for (2999ds/2Mi)
% 1.81/1.40 % (20972)Instruction limit reached!
% 1.81/1.40 % (20972)------------------------------
% 1.81/1.40 % (20972)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.81/1.40 % (20972)Termination reason: Unknown
% 1.81/1.40 % (20972)Termination phase: Preprocessing 1
% 1.81/1.40
% 1.81/1.40 % (20972)Memory used [KB]: 1023
% 1.81/1.40 % (20972)Time elapsed: 0.002 s
% 1.81/1.40 % (20972)Instructions burned: 3 (million)
% 1.81/1.40 % (20972)------------------------------
% 1.81/1.40 % (20972)------------------------------
% 1.81/1.40 % (20969)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_20855 for (2999ds/183Mi)
% 1.81/1.40 % (20970)Instruction limit reached!
% 1.81/1.40 % (20970)------------------------------
% 1.81/1.40 % (20970)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.81/1.40 % (20970)Termination reason: Unknown
% 1.81/1.40 % (20970)Termination phase: Property scanning
% 1.81/1.40
% 1.81/1.40 % (20970)Memory used [KB]: 1023
% 1.81/1.40 % (20970)Time elapsed: 0.003 s
% 1.81/1.40 % (20970)Instructions burned: 7 (million)
% 1.81/1.40 % (20970)------------------------------
% 1.81/1.40 % (20970)------------------------------
% 1.81/1.40 % (20971)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_20855 for (2999ds/27Mi)
% 1.81/1.40 % (20973)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_20855 for (2999ds/2Mi)
% 1.81/1.40 % (20974)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_20855 for (2999ds/275Mi)
% 1.81/1.40 % (20975)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_20855 for (2999ds/18Mi)
% 1.81/1.40 % (20973)Instruction limit reached!
% 1.81/1.40 % (20973)------------------------------
% 1.81/1.40 % (20973)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.81/1.40 % (20973)Termination reason: Unknown
% 1.81/1.40 % (20973)Termination phase: shuffling
% 1.81/1.40
% 1.81/1.40 % (20973)Memory used [KB]: 1023
% 1.81/1.40 % (20973)Time elapsed: 0.003 s
% 1.81/1.40 % (20973)Instructions burned: 2 (million)
% 1.81/1.40 % (20973)------------------------------
% 1.81/1.40 % (20973)------------------------------
% 1.81/1.41 % (20976)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_20855 for (2999ds/3Mi)
% 1.81/1.41 % (20977)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_20855 for (2999ds/37Mi)
% 1.81/1.41 % (20976)Instruction limit reached!
% 1.81/1.41 % (20976)------------------------------
% 1.81/1.41 % (20976)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.81/1.41 % (20976)Termination reason: Unknown
% 1.81/1.41 % (20976)Termination phase: Naming
% 1.81/1.41
% 1.81/1.41 % (20976)Memory used [KB]: 1023
% 1.81/1.41 % (20976)Time elapsed: 0.002 s
% 1.81/1.41 % (20976)Instructions burned: 4 (million)
% 1.81/1.41 % (20976)------------------------------
% 1.81/1.41 % (20976)------------------------------
% 1.81/1.41 % (20974)First to succeed.
% 1.81/1.41 % (20974)Refutation found. Thanks to Tanya!
% 1.81/1.41 % SZS status Theorem for DTF2THF_20855
% 1.81/1.41 % SZS output start Proof for DTF2THF_20855
% 1.81/1.41 thf(type_def_6, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 1.81/1.41 thf(type_def_7, type, tyop_2Erealax_2Ereal: $tType).
% 1.81/1.41 thf(func_def_0, type, tyop_2Emin_2Ebool: $tType).
% 1.81/1.41 thf(func_def_1, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 1.81/1.41 thf(func_def_2, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 1.81/1.41 thf(func_def_3, type, tyop_2Erealax_2Ereal: $tType).
% 1.81/1.41 thf(func_def_4, type, c_2Ebool_2E_21: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.81/1.41 thf(func_def_5, type, c_2Epair_2E_2C: !>[X0: $tType, X1: $tType]:(X0 > X1 > tyop_2Epair_2Eprod @ X0 @ X1)).
% 1.81/1.41 thf(func_def_6, type, c_2Ebool_2E_2F_5C: $o > $o > $o).
% 1.81/1.41 thf(func_def_7, type, c_2Emin_2E_3D: !>[X0: $tType]:(X0 > X0 > $o)).
% 1.81/1.41 thf(func_def_8, type, c_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 1.81/1.41 thf(func_def_9, type, c_2Ebool_2E_3F: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.81/1.41 thf(func_def_11, type, c_2Epred__set_2ESUBSET: !>[X0: $tType]:((X0 > $o) > (X0 > $o) > $o)).
% 1.81/1.41 thf(func_def_13, type, c_2Ebool_2E_5C_2F: $o > $o > $o).
% 1.81/1.41 thf(func_def_14, type, c_2Ereal__topology_2Eball: tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal > $o).
% 1.81/1.41 thf(func_def_15, type, c_2Ereal__topology_2Ebounded__def: (tyop_2Erealax_2Ereal > $o) > $o).
% 1.81/1.41 thf(func_def_16, type, c_2Ereal__topology_2Ecball: tyop_2Epair_2Eprod @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal > $o).
% 1.81/1.41 thf(func_def_17, type, c_2Ebool_2E_7E: $o > $o).
% 1.81/1.41 thf(func_def_27, type, sK0: tyop_2Erealax_2Ereal).
% 1.81/1.41 thf(func_def_28, type, sK1: tyop_2Erealax_2Ereal).
% 1.81/1.41 thf(func_def_30, type, ph3: !>[X0: $tType]:(X0)).
% 1.81/1.41 thf(f251,plain,(
% 1.81/1.41 $false),
% 1.81/1.41 inference(trivial_inequality_removal,[status(thm)],[f246])).
% 1.81/1.41 thf(f246,plain,(
% 1.81/1.41 ($true != $true)),
% 1.81/1.41 inference(superposition,[status(thm)],[f131,f243])).
% 1.81/1.41 thf(f243,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (($true = (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))))) )),
% 1.81/1.41 inference(subsumption_resolution,[status(thm)],[f242,f132])).
% 1.81/1.41 thf(f132,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))) = $true)) )),
% 1.81/1.41 inference(cnf_transformation,[status(thm)],[f73])).
% 1.81/1.41 thf(f73,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))) = $true)),
% 1.81/1.41 inference(fool_elimination,[status(thm)],[f72])).
% 1.81/1.41 thf(f72,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)))),
% 1.81/1.41 inference(rectify,[status(thm)],[f22])).
% 1.81/1.41 thf(f22,axiom,(
% 1.81/1.41 ! [X9 : tyop_2Erealax_2Ereal,X16 : tyop_2Erealax_2Ereal] : (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X9 @ X16)))),
% 1.81/1.41 file('/export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2THF_20855.p',thm_2Ereal__topology_2EBOUNDED__CBALL)).
% 1.81/1.41 thf(f242,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (($true = (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)))) | ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))) != $true)) )),
% 1.81/1.41 inference(trivial_inequality_removal,[status(thm)],[f234])).
% 1.81/1.41 thf(f234,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (($true = (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)))) | ($false = $true) | ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))) != $true)) )),
% 1.81/1.41 inference(superposition,[status(thm)],[f119,f193])).
% 1.81/1.41 thf(f193,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : (($false = (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1)) | ($true != (c_2Ereal__topology_2Ebounded__def @ X1)) | ($true = (c_2Ereal__topology_2Ebounded__def @ X0))) )),
% 1.81/1.41 inference(trivial_inequality_removal,[status(thm)],[f166])).
% 1.81/1.41 thf(f166,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : (($false = (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1)) | ($true != $true) | ($true != (c_2Ereal__topology_2Ebounded__def @ X1)) | ($true = (c_2Ereal__topology_2Ebounded__def @ X0))) )),
% 1.81/1.41 inference(superposition,[status(thm)],[f120,f154])).
% 1.81/1.41 thf(f154,plain,(
% 1.81/1.41 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.81/1.41 inference(subsumption_resolution,[status(thm)],[f151,f131])).
% 1.81/1.41 thf(f151,plain,(
% 1.81/1.41 ( ! [X0 : $o] : (($false = X0) | ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ sK0 @ sK1))) = $true) | ($true = X0)) )),
% 1.81/1.41 inference(binary_proxy_clausification,[status(thm)],[f150])).
% 1.81/1.41 thf(f150,plain,(
% 1.81/1.41 ( ! [X0 : $o] : (($true = X0) | ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ sK0 @ sK1))) = X0)) )),
% 1.81/1.41 inference(trivial_inequality_removal,[status(thm)],[f149])).
% 1.81/1.41 thf(f149,plain,(
% 1.81/1.41 ( ! [X0 : $o] : (($true = X0) | ($true != $true) | ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ sK0 @ sK1))) = X0)) )),
% 1.81/1.41 inference(superposition,[status(thm)],[f131,f128])).
% 1.81/1.41 thf(f128,plain,(
% 1.81/1.41 ( ! [X0 : $o,X1 : $o] : (($true = X1) | (X0 = X1) | ($true = X0)) )),
% 1.81/1.41 inference(cnf_transformation,[status(thm)],[f102])).
% 1.81/1.41 thf(f102,plain,(
% 1.81/1.41 ! [X0 : $o,X1 : $o] : ((X0 = X1) | (($true != X1) & ($true = X0)) | (($true = X1) & ($true != X0)))),
% 1.81/1.41 inference(flattening,[status(thm)],[f101])).
% 1.81/1.41 thf(f101,plain,(
% 1.81/1.41 ! [X0 : $o,X1 : $o] : (((X0 = X1) | (($true = X1) & ($true != X0))) | (($true != X1) & ($true = X0)))),
% 1.81/1.41 inference(ennf_transformation,[status(thm)],[f45])).
% 1.81/1.41 thf(f45,plain,(
% 1.81/1.41 ! [X0 : $o,X1 : $o] : ((($true = X0) => ($true = X1)) => ((($true = X1) => ($true = X0)) => (X0 = X1)))),
% 1.81/1.41 inference(fool_elimination,[status(thm)],[f44])).
% 1.81/1.41 thf(f44,plain,(
% 1.81/1.41 ! [X0 : $o,X1 : $o] : ((X0 => X1) => ((X1 => X0) => (X0 = X1)))),
% 1.81/1.41 inference(rectify,[status(thm)],[f9])).
% 1.81/1.41 thf(f9,axiom,(
% 1.81/1.41 ! [X6 : $o,X7 : $o] : ((X6 => X7) => ((X7 => X6) => (X6 = X7)))),
% 1.81/1.41 file('/export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2THF_20855.p',thm_2Ebool_2EIMP__ANTISYM__AX)).
% 1.81/1.41 thf(f120,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : (($true != (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1)) | ($true != (c_2Ereal__topology_2Ebounded__def @ X1)) | ($true = (c_2Ereal__topology_2Ebounded__def @ X0))) )),
% 1.81/1.41 inference(cnf_transformation,[status(thm)],[f104])).
% 1.81/1.41 thf(f104,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : (($true != (c_2Ereal__topology_2Ebounded__def @ X1)) | ($true != (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1)) | ($true = (c_2Ereal__topology_2Ebounded__def @ X0)))),
% 1.81/1.41 inference(flattening,[status(thm)],[f103])).
% 1.81/1.41 thf(f103,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : (($true = (c_2Ereal__topology_2Ebounded__def @ X0)) | (($true != (c_2Ereal__topology_2Ebounded__def @ X1)) | ($true != (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1))))),
% 1.81/1.41 inference(ennf_transformation,[status(thm)],[f69])).
% 1.81/1.41 thf(f69,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : ((($true = (c_2Ereal__topology_2Ebounded__def @ X1)) & ($true = (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1))) => ($true = (c_2Ereal__topology_2Ebounded__def @ X0)))),
% 1.81/1.41 inference(fool_elimination,[status(thm)],[f68])).
% 1.81/1.41 thf(f68,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal > $o,X1 : tyop_2Erealax_2Ereal > $o] : (((c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X0 @ X1) & (c_2Ereal__topology_2Ebounded__def @ X1)) => (c_2Ereal__topology_2Ebounded__def @ X0))),
% 1.81/1.41 inference(rectify,[status(thm)],[f21])).
% 1.81/1.41 thf(f21,axiom,(
% 1.81/1.41 ! [X17 : tyop_2Erealax_2Ereal > $o,X18 : tyop_2Erealax_2Ereal > $o] : (((c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ X17 @ X18) & (c_2Ereal__topology_2Ebounded__def @ X18)) => (c_2Ereal__topology_2Ebounded__def @ X17))),
% 1.81/1.41 file('/export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2THF_20855.p',thm_2Ereal__topology_2EBOUNDED__SUBSET)).
% 1.81/1.41 thf(f119,plain,(
% 1.81/1.41 ( ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (((c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)) @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))) = $true)) )),
% 1.81/1.41 inference(cnf_transformation,[status(thm)],[f85])).
% 1.81/1.41 thf(f85,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : ((c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)) @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))) = $true)),
% 1.81/1.41 inference(fool_elimination,[status(thm)],[f84])).
% 1.81/1.41 thf(f84,plain,(
% 1.81/1.41 ! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)) @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)))),
% 1.81/1.41 inference(rectify,[status(thm)],[f20])).
% 1.81/1.41 thf(f20,axiom,(
% 1.81/1.41 ! [X9 : tyop_2Erealax_2Ereal,X16 : tyop_2Erealax_2Ereal] : (c_2Epred__set_2ESUBSET @ tyop_2Erealax_2Ereal @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X9 @ X16)) @ (c_2Ereal__topology_2Ecball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X9 @ X16)))),
% 1.81/1.41 file('/export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2THF_20855.p',thm_2Ereal__topology_2EBALL__SUBSET__CBALL)).
% 1.81/1.41 thf(f131,plain,(
% 1.81/1.41 ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ sK0 @ sK1))) != $true)),
% 1.81/1.41 inference(cnf_transformation,[status(thm)],[f112])).
% 1.81/1.41 thf(f112,plain,(
% 1.81/1.41 ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ sK0 @ sK1))) != $true)),
% 1.81/1.41 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f105,f111])).
% 1.81/1.41 thf(f111,plain,(
% 1.81/1.41 ? [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : ($true != (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)))) => ((c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ sK0 @ sK1))) != $true)),
% 1.81/1.41 introduced(definition,[],[choice_axiom])).
% 1.81/1.41 thf(f105,plain,(
% 1.81/1.41 ? [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : ($true != (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))))),
% 1.81/1.41 inference(ennf_transformation,[status(thm)],[f95])).
% 1.81/1.41 thf(f95,plain,(
% 1.81/1.41 ~! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : ($true = (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1))))),
% 1.81/1.41 inference(fool_elimination,[status(thm)],[f94])).
% 1.81/1.41 thf(f94,plain,(
% 1.81/1.41 ~! [X0 : tyop_2Erealax_2Ereal,X1 : tyop_2Erealax_2Ereal] : (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X0 @ X1)))),
% 1.81/1.41 inference(rectify,[status(thm)],[f34])).
% 1.81/1.41 thf(f34,negated_conjecture,(
% 1.81/1.41 ~! [X9 : tyop_2Erealax_2Ereal,X16 : tyop_2Erealax_2Ereal] : (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X9 @ X16)))),
% 1.81/1.41 inference(negated_conjecture,[status(cth)],[f33])).
% 1.81/1.41 thf(f33,conjecture,(
% 1.81/1.41 ! [X9 : tyop_2Erealax_2Ereal,X16 : tyop_2Erealax_2Ereal] : (c_2Ereal__topology_2Ebounded__def @ (c_2Ereal__topology_2Eball @ (c_2Epair_2E_2C @ tyop_2Erealax_2Ereal @ tyop_2Erealax_2Ereal @ X9 @ X16)))),
% 1.81/1.41 file('/export/starexec/sandbox/tmp/tmp.4jWNxQv2E3/DTF2THF_20855.p',thm_2Ereal__topology_2EBOUNDED__BALL)).
% 1.81/1.41 % SZS output end Proof for DTF2THF_20855
% 1.81/1.41 % (20974)------------------------------
% 1.81/1.41 % (20974)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.81/1.41 % (20974)Termination reason: Refutation
% 1.81/1.41
% 1.81/1.41 % (20974)Memory used [KB]: 5628
% 1.81/1.41 % (20974)Time elapsed: 0.010 s
% 1.81/1.41 % (20974)Instructions burned: 10 (million)
% 1.81/1.41 % (20974)------------------------------
% 1.81/1.41 % (20974)------------------------------
% 1.81/1.41 % (20968)Success in time 0.019 s
%------------------------------------------------------------------------------