%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP144^1 : TPTP v9.2.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n024.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:55:54 AM UTC 2026
% Result : Theorem 1.37s 1.02s
% Output : Refutation 1.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 6
% Syntax : Number of formulae : 32 ( 5 unt; 0 typ; 0 def)
% Number of atoms : 165 ( 62 equ; 0 cnn)
% Maximal formula atoms : 5 ( 5 avg)
% Number of connectives : 195 ( 36 ~; 23 |; 7 &; 118 @)
% ( 2 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 10 ( 10 >; 0 *; 0 +; 0 <<)
% Number of symbols : 38 ( 35 usr; 5 con; 0-3 aty)
% Number of variables : 51 ( 0 ^; 37 !; 14 ?; 51 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
b: $tType ).
thf(type_def_7,type,
set_b: $tType ).
thf(type_def_8,type,
set_set_b: $tType ).
thf(type_def_9,type,
a: $tType ).
thf(func_def_0,type,
set_set_b: $tType ).
thf(func_def_1,type,
set_b: $tType ).
thf(func_def_2,type,
b: $tType ).
thf(func_def_3,type,
a: $tType ).
thf(func_def_4,type,
bij_betw_b_b: ( b > b ) > set_b > set_b > $o ).
thf(func_def_5,type,
inj_on_b_set_b: ( b > set_b ) > set_b > $o ).
thf(func_def_6,type,
inj_on_b_b: ( b > b ) > set_b > $o ).
thf(func_def_7,type,
minus_minus_set_b: set_b > set_b > set_b ).
thf(func_def_8,type,
hilbert_Eps_b: ( b > $o ) > b ).
thf(func_def_9,type,
hilbert_inv_into_b_b: set_b > ( b > b ) > b > b ).
thf(func_def_10,type,
bot_bot_b_o: b > $o ).
thf(func_def_11,type,
bot_bot_set_b: set_b ).
thf(func_def_12,type,
top_top_b_o: b > $o ).
thf(func_def_13,type,
top_top_set_b: set_b ).
thf(func_def_14,type,
collect_b: ( b > $o ) > set_b ).
thf(func_def_15,type,
image_set_b_set_b: ( set_b > set_b ) > set_set_b > set_set_b ).
thf(func_def_16,type,
image_b_b: ( b > b ) > set_b > set_b ).
thf(func_def_17,type,
insert_b: b > set_b > set_b ).
thf(func_def_18,type,
is_empty_b: set_b > $o ).
thf(func_def_19,type,
is_singleton_b: set_b > $o ).
thf(func_def_20,type,
remove_b: b > set_b > set_b ).
thf(func_def_21,type,
the_elem_b: set_b > b ).
thf(func_def_22,type,
member_set_b: set_b > set_set_b > $o ).
thf(func_def_23,type,
member_b: b > set_b > $o ).
thf(func_def_24,type,
p: a > $o ).
thf(func_def_25,type,
q: a > b > $o ).
thf(func_def_39,type,
sK0: ( b > $o ) > b ).
thf(func_def_40,type,
sK1: ( b > $o ) > b ).
thf(func_def_41,type,
sK2: a > b ).
thf(func_def_42,type,
sK3: b > ( b > $o ) > b ).
thf(func_def_43,type,
sK4: b > ( b > $o ) > b ).
thf(func_def_44,type,
sK5: ( b > $o ) > ( b > $o ) > b ).
thf(func_def_45,type,
sK6: ( b > $o ) > b ).
thf(func_def_46,type,
sK7: ( b > $o ) > ( b > $o ) > b ).
thf(func_def_47,type,
sK8: ( b > $o ) > ( b > $o ) > b ).
thf(func_def_48,type,
sK9: ( b > $o ) > ( b > $o ) > b ).
thf(func_def_49,type,
sK10: a ).
thf(func_def_50,type,
sK11: ( b > $o ) > b ).
thf(func_def_52,type,
ph13:
!>[X0: $tType] : X0 ).
thf(f481,plain,
$false,
inference(subsumption_resolution,[status(thm)],[f459,f389]) ).
thf(f389,plain,
( $true
= ( p @ sK10 ) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
thf(f362,plain,
( ( ( q @ sK10 @ ( hilbert_Eps_b @ ( q @ sK10 ) ) )
!= $true )
& ( $true
= ( p @ sK10 ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK10])],[f322,f361]) ).
thf(f361,plain,
( ? [X0: a] :
( ( $true
!= ( q @ X0 @ ( hilbert_Eps_b @ ( q @ X0 ) ) ) )
& ( $true
= ( p @ X0 ) ) )
=> ( ( ( q @ sK10 @ ( hilbert_Eps_b @ ( q @ sK10 ) ) )
!= $true )
& ( $true
= ( p @ sK10 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f322,plain,
? [X0: a] :
( ( $true
!= ( q @ X0 @ ( hilbert_Eps_b @ ( q @ X0 ) ) ) )
& ( $true
= ( p @ X0 ) ) ),
inference(ennf_transformation,[status(thm)],[f308]) ).
thf(f308,plain,
~ ! [X0: a] :
( ( $true
= ( q @ X0 @ ( hilbert_Eps_b @ ( q @ X0 ) ) ) )
| ( $true
!= ( p @ X0 ) ) ),
inference(flattening,[status(thm)],[f168]) ).
thf(f168,plain,
~ ! [X0: a] :
( ( $true
= ( q @ X0 @ ( hilbert_Eps_b @ ( q @ X0 ) ) ) )
| ( $true
!= ( p @ X0 ) ) ),
inference(fool_elimination,[status(thm)],[f167]) ).
thf(f167,plain,
~ ! [X0: a] :
( ( q @ X0 @ ( hilbert_Eps_b @ ( q @ X0 ) ) )
| ~ ( p @ X0 ) ),
inference(rectify,[status(thm)],[f113]) ).
thf(f113,negated_conjecture,
~ ! [X2: a] :
( ( q @ X2 @ ( hilbert_Eps_b @ ( q @ X2 ) ) )
| ~ ( p @ X2 ) ),
inference(negated_conjecture,[status(cth)],[f112]) ).
thf(f112,conjecture,
! [X2: a] :
( ( q @ X2 @ ( hilbert_Eps_b @ ( q @ X2 ) ) )
| ~ ( p @ X2 ) ),
file('/export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2THF_5930.p',conj_1) ).
thf(f459,plain,
( $true
!= ( p @ sK10 ) ),
inference(trivial_inequality_removal,[status(thm)],[f438]) ).
thf(f438,plain,
( ( $true
!= ( p @ sK10 ) )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f433,f372]) ).
thf(f372,plain,
! [X0: a] :
( ( $true
= ( q @ X0 @ ( sK2 @ X0 ) ) )
| ( $true
!= ( p @ X0 ) ) ),
inference(cnf_transformation,[status(thm)],[f345]) ).
thf(f345,plain,
! [X0: a] :
( ( $true
= ( q @ X0 @ ( sK2 @ X0 ) ) )
| ( $true
!= ( p @ X0 ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK2])],[f330,f344]) ).
thf(f344,plain,
! [X0: a] :
( ? [X1: b] :
( $true
= ( q @ X0 @ X1 ) )
=> ( $true
= ( q @ X0 @ ( sK2 @ X0 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f330,plain,
! [X0: a] :
( ? [X1: b] :
( $true
= ( q @ X0 @ X1 ) )
| ( $true
!= ( p @ X0 ) ) ),
inference(ennf_transformation,[status(thm)],[f201]) ).
thf(f201,plain,
! [X0: a] :
( ( $true
= ( p @ X0 ) )
=> ? [X1: b] :
( $true
= ( q @ X0 @ X1 ) ) ),
inference(fool_elimination,[status(thm)],[f200]) ).
thf(f200,plain,
! [X0: a] :
( ( p @ X0 )
=> ? [X1: b] : ( q @ X0 @ X1 ) ),
inference(rectify,[status(thm)],[f111]) ).
thf(f111,axiom,
! [X15: a] :
( ( p @ X15 )
=> ? [X33: b] : ( q @ X15 @ X33 ) ),
file('/export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2THF_5930.p',conj_0) ).
thf(f433,plain,
! [X0: b] :
( $true
!= ( q @ sK10 @ X0 ) ),
inference(trivial_inequality_removal,[status(thm)],[f416]) ).
thf(f416,plain,
! [X0: b] :
( ( $true
!= ( q @ sK10 @ X0 ) )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f390,f398]) ).
thf(f398,plain,
! [X2: b,X0: b > $o] :
( ( ( X0 @ ( hilbert_Eps_b @ X0 ) )
= $true )
| ( ( X0 @ X2 )
!= $true ) ),
inference(equality_resolution,[status(thm)],[f371]) ).
thf(f371,plain,
! [X2: b,X0: b > $o,X1: b] :
( ( ( X0 @ X1 )
= $true )
| ( ( X0 @ X2 )
!= $true )
| ( ( hilbert_Eps_b @ X0 )
!= X1 ) ),
inference(cnf_transformation,[status(thm)],[f343]) ).
thf(f343,plain,
! [X0: b > $o,X1: b] :
( ( ( ( ( X0 @ X1 )
= $true )
| ! [X2: b] :
( ( X0 @ X2 )
!= $true ) )
& ( ( $true
= ( X0 @ ( sK1 @ X0 ) ) )
| ( ( X0 @ X1 )
!= $true ) ) )
| ( ( hilbert_Eps_b @ X0 )
!= X1 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK1])],[f341,f342]) ).
thf(f342,plain,
! [X0: b > $o] :
( ? [X3: b] :
( ( X0 @ X3 )
= $true )
=> ( $true
= ( X0 @ ( sK1 @ X0 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f341,plain,
! [X0: b > $o,X1: b] :
( ( ( ( ( X0 @ X1 )
= $true )
| ! [X2: b] :
( ( X0 @ X2 )
!= $true ) )
& ( ? [X3: b] :
( ( X0 @ X3 )
= $true )
| ( ( X0 @ X1 )
!= $true ) ) )
| ( ( hilbert_Eps_b @ X0 )
!= X1 ) ),
inference(rectify,[status(thm)],[f340]) ).
thf(f340,plain,
! [X0: b > $o,X1: b] :
( ( ( ( ( X0 @ X1 )
= $true )
| ! [X2: b] :
( ( X0 @ X2 )
!= $true ) )
& ( ? [X2: b] :
( ( X0 @ X2 )
= $true )
| ( ( X0 @ X1 )
!= $true ) ) )
| ( ( hilbert_Eps_b @ X0 )
!= X1 ) ),
inference(nnf_transformation,[status(thm)],[f313]) ).
thf(f313,plain,
! [X0: b > $o,X1: b] :
( ( ( ( X0 @ X1 )
= $true )
<=> ? [X2: b] :
( ( X0 @ X2 )
= $true ) )
| ( ( hilbert_Eps_b @ X0 )
!= X1 ) ),
inference(ennf_transformation,[status(thm)],[f192]) ).
thf(f192,plain,
! [X0: b > $o,X1: b] :
( ( ( hilbert_Eps_b @ X0 )
= X1 )
=> ( ( ( X0 @ X1 )
= $true )
<=> ? [X2: b] :
( ( X0 @ X2 )
= $true ) ) ),
inference(fool_elimination,[status(thm)],[f191]) ).
thf(f191,plain,
! [X0: b > $o,X1: b] :
( ( ( hilbert_Eps_b @ X0 )
= X1 )
=> ( ( X0 @ X1 )
= ( ? [X2: b] : ( X0 @ X2 ) ) ) ),
inference(rectify,[status(thm)],[f21]) ).
thf(f21,axiom,
! [X0: b > $o,X3: b] :
( ( ( hilbert_Eps_b @ X0 )
= X3 )
=> ( ( X0 @ X3 )
= ( ? [X8: b] : ( X0 @ X8 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2THF_5930.p',fact_20_verit__sko__ex__indirect) ).
thf(f390,plain,
( ( q @ sK10 @ ( hilbert_Eps_b @ ( q @ sK10 ) ) )
!= $true ),
inference(cnf_transformation,[status(thm)],[f362]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : ITP144^1 : TPTP v9.2.1. Released v7.5.0.
% 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.25 % Computer : n024.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Tue Feb 24 03:27:40 EST 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.32 ---- Original DTF file ---
% 0.07/0.32 thf(spec,logic,$$dhol).
% 0.07/0.32 %------------------------------------------------------------------------------
% 0.07/0.32 % File : ITP144^1 : TPTP v9.2.1. Released v7.5.0.
% 0.07/0.32 % Domain : Interactive Theorem Proving
% 0.07/0.32 % Problem : Sledgehammer PHoareTotal problem prob_493__3263728_1
% 0.07/0.32 % Version : Especial.
% 0.07/0.32 % English :
% 0.07/0.32
% 0.07/0.32 % Refs : [BH+15] Blanchette et al. (2015), Mining the Archive of Formal
% 0.07/0.32 % : [Des21] Desharnais (2021), Email to Geoff Sutcliffe
% 0.07/0.32 % Source : [Des21]
% 0.07/0.32 % Names : PHoareTotal/prob_493__3263728_1 [Des21]
% 0.07/0.32
% 0.07/0.32 % Status : Theorem
% 0.07/0.32 % Rating : 0.22 v9.1.0, 0.25 v9.0.0, 0.30 v8.2.0, 0.23 v8.1.0, 0.27 v7.5.0
% 0.07/0.32 % Syntax : Number of formulae : 138 ( 54 unt; 26 typ; 0 def)
% 0.07/0.32 % Number of atoms : 265 ( 153 equ; 0 cnn)
% 0.07/0.32 % Maximal formula atoms : 7 ( 2 avg)
% 0.07/0.32 % Number of connectives : 728 ( 51 ~; 4 |; 26 &; 546 @)
% 0.07/0.32 % ( 0 <=>; 101 =>; 0 <=; 0 <~>)
% 0.07/0.32 % Maximal formula depth : 15 ( 5 avg)
% 0.07/0.32 % Number of types : 5 ( 4 usr)
% 0.07/0.32 % Number of type conns : 91 ( 91 >; 0 *; 0 +; 0 <<)
% 0.07/0.32 % Number of symbols : 24 ( 22 usr; 3 con; 0-3 aty)
% 0.07/0.32 % Number of variables : 286 ( 41 ^; 230 !; 15 ?; 286 :)
% 0.07/0.32 % SPC : TH0_THM_EQU_NAR
% 0.07/0.32
% 0.07/0.32 % Comments : This file was generated by Sledgehammer 2021-02-23 15:33:49.690
% 0.07/0.32 %------------------------------------------------------------------------------
% 0.07/0.32 % Could-be-implicit typings (4)
% 0.07/0.32 thf(ty_n_t__Set__Oset_It__Set__Oset_Itf__b_J_J,type,
% 0.07/0.32 set_set_b: $tType ).
% 0.07/0.32
% 0.07/0.32 thf(ty_n_t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 set_b: $tType ).
% 0.07/0.32
% 0.07/0.32 thf(ty_n_tf__b,type,
% 0.07/0.32 b: $tType ).
% 0.07/0.32
% 0.07/0.32 thf(ty_n_tf__a,type,
% 0.07/0.32 a: $tType ).
% 0.07/0.32
% 0.07/0.32 % Explicit typings (22)
% 0.07/0.32 thf(sy_c_Fun_Obij__betw_001tf__b_001tf__b,type,
% 0.07/0.32 bij_betw_b_b: ( b > b ) > set_b > set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Fun_Oinj__on_001tf__b_001t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 inj_on_b_set_b: ( b > set_b ) > set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Fun_Oinj__on_001tf__b_001tf__b,type,
% 0.07/0.32 inj_on_b_b: ( b > b ) > set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Groups_Ominus__class_Ominus_001t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 minus_minus_set_b: set_b > set_b > set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Hilbert__Choice_OEps_001tf__b,type,
% 0.07/0.32 hilbert_Eps_b: ( b > $o ) > b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Hilbert__Choice_Oinv__into_001tf__b_001tf__b,type,
% 0.07/0.32 hilbert_inv_into_b_b: set_b > ( b > b ) > b > b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Orderings_Obot__class_Obot_001_062_Itf__b_M_Eo_J,type,
% 0.07/0.32 bot_bot_b_o: b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Orderings_Obot__class_Obot_001t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 bot_bot_set_b: set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Orderings_Otop__class_Otop_001_062_Itf__b_M_Eo_J,type,
% 0.07/0.32 top_top_b_o: b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Orderings_Otop__class_Otop_001t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 top_top_set_b: set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_OCollect_001tf__b,type,
% 0.07/0.32 collect_b: ( b > $o ) > set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Oimage_001t__Set__Oset_Itf__b_J_001t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 image_set_b_set_b: ( set_b > set_b ) > set_set_b > set_set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Oimage_001tf__b_001tf__b,type,
% 0.07/0.32 image_b_b: ( b > b ) > set_b > set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Oinsert_001tf__b,type,
% 0.07/0.32 insert_b: b > set_b > set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Ois__empty_001tf__b,type,
% 0.07/0.32 is_empty_b: set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Ois__singleton_001tf__b,type,
% 0.07/0.32 is_singleton_b: set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Oremove_001tf__b,type,
% 0.07/0.32 remove_b: b > set_b > set_b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_Set_Othe__elem_001tf__b,type,
% 0.07/0.32 the_elem_b: set_b > b ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_member_001t__Set__Oset_Itf__b_J,type,
% 0.07/0.32 member_set_b: set_b > set_set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_c_member_001tf__b,type,
% 0.07/0.32 member_b: b > set_b > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_v_P,type,
% 0.07/0.32 p: a > $o ).
% 0.07/0.32
% 0.07/0.32 thf(sy_v_Q,type,
% 0.07/0.32 q: a > b > $o ).
% 0.07/0.32
% 0.07/0.32 % Relevant facts (110)
% 0.07/0.32 thf(fact_0_some__equality,axiom,
% 0.07/0.32 ! [P: b > $o,A: b] :
% 0.07/0.32 ( ( P @ A )
% 0.07/0.32 => ( ! [X: b] :
% 0.07/0.32 ( ( P @ X )
% 0.07/0.32 => ( X = A ) )
% 0.07/0.32 => ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = A ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % some_equality
% 0.07/0.32 thf(fact_1_some__eq__trivial,axiom,
% 0.07/0.32 ! [X2: b] :
% 0.07/0.32 ( ( hilbert_Eps_b
% 0.07/0.32 @ ^ [Y: b] : ( Y = X2 ) )
% 0.07/0.32 = X2 ) ).
% 0.07/0.32
% 0.07/0.32 % some_eq_trivial
% 0.07/0.32 thf(fact_2_some__sym__eq__trivial,axiom,
% 0.07/0.32 ! [X2: b] :
% 0.07/0.32 ( ( hilbert_Eps_b
% 0.07/0.32 @ ( ^ [Y2: b,Z: b] : ( Y2 = Z )
% 0.07/0.32 @ X2 ) )
% 0.07/0.32 = X2 ) ).
% 0.07/0.32
% 0.07/0.32 % some_sym_eq_trivial
% 0.07/0.32 thf(fact_3_verit__sko__ex_H,axiom,
% 0.07/0.32 ! [P: b > $o,A2: $o] :
% 0.07/0.32 ( ( ( P @ ( hilbert_Eps_b @ P ) )
% 0.07/0.32 = A2 )
% 0.07/0.32 => ( ( ? [X3: b] : ( P @ X3 ) )
% 0.07/0.32 = A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_ex'
% 0.07/0.32 thf(fact_4_verit__sko__forall,axiom,
% 0.07/0.32 ( ( ^ [P2: b > $o] :
% 0.07/0.32 ! [X3: b] : ( P2 @ X3 ) )
% 0.07/0.32 = ( ^ [P3: b > $o] :
% 0.07/0.32 ( P3
% 0.07/0.32 @ ( hilbert_Eps_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ~ ( P3 @ X4 ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_forall
% 0.07/0.32 thf(fact_5_someI2,axiom,
% 0.07/0.32 ! [P: b > $o,A: b,Q: b > $o] :
% 0.07/0.32 ( ( P @ A )
% 0.07/0.32 => ( ! [X: b] :
% 0.07/0.32 ( ( P @ X )
% 0.07/0.32 => ( Q @ X ) )
% 0.07/0.32 => ( Q @ ( hilbert_Eps_b @ P ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % someI2
% 0.07/0.32 thf(fact_6_verit__sko__forall_H,axiom,
% 0.07/0.32 ! [P: b > $o,A2: $o] :
% 0.07/0.32 ( ( ( P
% 0.07/0.32 @ ( hilbert_Eps_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ~ ( P @ X4 ) ) )
% 0.07/0.32 = A2 )
% 0.07/0.32 => ( ( ! [X3: b] : ( P @ X3 ) )
% 0.07/0.32 = A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_forall'
% 0.07/0.32 thf(fact_7_verit__sko__forall_H_H,axiom,
% 0.07/0.32 ! [B: b,A2: b,P: b > $o] :
% 0.07/0.32 ( ( B = A2 )
% 0.07/0.32 => ( ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = A2 )
% 0.07/0.32 = ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_forall''
% 0.07/0.32 thf(fact_8_someI__ex,axiom,
% 0.07/0.32 ! [P: b > $o] :
% 0.07/0.32 ( ? [X_1: b] : ( P @ X_1 )
% 0.07/0.32 => ( P @ ( hilbert_Eps_b @ P ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % someI_ex
% 0.07/0.32 thf(fact_9_someI2__ex,axiom,
% 0.07/0.32 ! [P: b > $o,Q: b > $o] :
% 0.07/0.32 ( ? [X_1: b] : ( P @ X_1 )
% 0.07/0.32 => ( ! [X: b] :
% 0.07/0.32 ( ( P @ X )
% 0.07/0.32 => ( Q @ X ) )
% 0.07/0.32 => ( Q @ ( hilbert_Eps_b @ P ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % someI2_ex
% 0.07/0.32 thf(fact_10_someI2__bex,axiom,
% 0.07/0.32 ! [A2: set_b,P: b > $o,Q: b > $o] :
% 0.07/0.32 ( ? [X5: b] :
% 0.07/0.32 ( ( member_b @ X5 @ A2 )
% 0.07/0.32 & ( P @ X5 ) )
% 0.07/0.32 => ( ! [X: b] :
% 0.07/0.32 ( ( ( member_b @ X @ A2 )
% 0.07/0.32 & ( P @ X ) )
% 0.07/0.32 => ( Q @ X ) )
% 0.07/0.32 => ( Q
% 0.07/0.32 @ ( hilbert_Eps_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( member_b @ X4 @ A2 )
% 0.07/0.32 & ( P @ X4 ) ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % someI2_bex
% 0.07/0.32 thf(fact_11_some__eq__ex,axiom,
% 0.07/0.32 ! [P: b > $o] :
% 0.07/0.32 ( ( P @ ( hilbert_Eps_b @ P ) )
% 0.07/0.32 = ( ? [X3: b] : ( P @ X3 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % some_eq_ex
% 0.07/0.32 thf(fact_12_some__eq__imp,axiom,
% 0.07/0.32 ! [P: b > $o,A: b,B2: b] :
% 0.07/0.32 ( ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = A )
% 0.07/0.32 => ( ( P @ B2 )
% 0.07/0.32 => ( P @ A ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % some_eq_imp
% 0.07/0.32 thf(fact_13_tfl__some,axiom,
% 0.07/0.32 ! [P4: b > $o,X5: b] :
% 0.07/0.32 ( ( P4 @ X5 )
% 0.07/0.32 => ( P4 @ ( hilbert_Eps_b @ P4 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % tfl_some
% 0.07/0.32 thf(fact_14_Eps__cong,axiom,
% 0.07/0.32 ! [P: b > $o,Q: b > $o] :
% 0.07/0.32 ( ! [X: b] :
% 0.07/0.32 ( ( P @ X )
% 0.07/0.32 = ( Q @ X ) )
% 0.07/0.32 => ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = ( hilbert_Eps_b @ Q ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Eps_cong
% 0.07/0.32 thf(fact_15_someI,axiom,
% 0.07/0.32 ! [P: b > $o,X2: b] :
% 0.07/0.32 ( ( P @ X2 )
% 0.07/0.32 => ( P @ ( hilbert_Eps_b @ P ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % someI
% 0.07/0.32 thf(fact_16_verit__sko__forall__indirect2,axiom,
% 0.07/0.32 ! [X2: b,P: b > $o,P5: b > $o] :
% 0.07/0.32 ( ( X2
% 0.07/0.32 = ( hilbert_Eps_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ~ ( P @ X4 ) ) )
% 0.07/0.32 => ( ! [X: b] :
% 0.07/0.32 ( ( P @ X )
% 0.07/0.32 = ( P5 @ X ) )
% 0.07/0.32 => ( ( ! [X3: b] : ( P5 @ X3 ) )
% 0.07/0.32 = ( P @ X2 ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_forall_indirect2
% 0.07/0.32 thf(fact_17_verit__sko__forall__indirect,axiom,
% 0.07/0.32 ! [X2: b,P: b > $o] :
% 0.07/0.32 ( ( X2
% 0.07/0.32 = ( hilbert_Eps_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ~ ( P @ X4 ) ) )
% 0.07/0.32 => ( ( ! [X3: b] : ( P @ X3 ) )
% 0.07/0.32 = ( P @ X2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_forall_indirect
% 0.07/0.32 thf(fact_18_some1__equality,axiom,
% 0.07/0.32 ! [P: b > $o,A: b] :
% 0.07/0.32 ( ? [X5: b] :
% 0.07/0.32 ( ( P @ X5 )
% 0.07/0.32 & ! [Y3: b] :
% 0.07/0.32 ( ( P @ Y3 )
% 0.07/0.32 => ( Y3 = X5 ) ) )
% 0.07/0.32 => ( ( P @ A )
% 0.07/0.32 => ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = A ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % some1_equality
% 0.07/0.32 thf(fact_19_verit__sko__ex__indirect2,axiom,
% 0.07/0.32 ! [X2: b,P: b > $o,P5: b > $o] :
% 0.07/0.32 ( ( X2
% 0.07/0.32 = ( hilbert_Eps_b @ P ) )
% 0.07/0.32 => ( ! [X: b] :
% 0.07/0.32 ( ( P @ X )
% 0.07/0.32 = ( P5 @ X ) )
% 0.07/0.32 => ( ( ? [X3: b] : ( P5 @ X3 ) )
% 0.07/0.32 = ( P @ X2 ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_ex_indirect2
% 0.07/0.32 thf(fact_20_verit__sko__ex__indirect,axiom,
% 0.07/0.32 ! [X2: b,P: b > $o] :
% 0.07/0.32 ( ( X2
% 0.07/0.32 = ( hilbert_Eps_b @ P ) )
% 0.07/0.32 => ( ( ? [X3: b] : ( P @ X3 ) )
% 0.07/0.32 = ( P @ X2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % verit_sko_ex_indirect
% 0.07/0.32 thf(fact_21_Nitpick_OEps__psimp,axiom,
% 0.07/0.32 ! [P: b > $o,X2: b,Y4: b] :
% 0.07/0.32 ( ( P @ X2 )
% 0.07/0.32 => ( ~ ( P @ Y4 )
% 0.07/0.32 => ( ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = Y4 )
% 0.07/0.32 => ( ( hilbert_Eps_b @ P )
% 0.07/0.32 = X2 ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Nitpick.Eps_psimp
% 0.07/0.32 thf(fact_22_some__in__eq,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( member_b
% 0.07/0.32 @ ( hilbert_Eps_b
% 0.07/0.32 @ ^ [X4: b] : ( member_b @ X4 @ A2 ) )
% 0.07/0.32 @ A2 )
% 0.07/0.32 = ( A2 != bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % some_in_eq
% 0.07/0.32 thf(fact_23_exE__some,axiom,
% 0.07/0.32 ! [P: b > $o,C: b] :
% 0.07/0.32 ( ? [X_1: b] : ( P @ X_1 )
% 0.07/0.32 => ( ( C
% 0.07/0.32 = ( hilbert_Eps_b @ P ) )
% 0.07/0.32 => ( P @ C ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % exE_some
% 0.07/0.32 thf(fact_24_empty__Collect__eq,axiom,
% 0.07/0.32 ! [P: b > $o] :
% 0.07/0.32 ( ( bot_bot_set_b
% 0.07/0.32 = ( collect_b @ P ) )
% 0.07/0.32 = ( ! [X4: b] :
% 0.07/0.32 ~ ( P @ X4 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % empty_Collect_eq
% 0.07/0.32 thf(fact_25_Collect__empty__eq,axiom,
% 0.07/0.32 ! [P: b > $o] :
% 0.07/0.32 ( ( ( collect_b @ P )
% 0.07/0.32 = bot_bot_set_b )
% 0.07/0.32 = ( ! [X4: b] :
% 0.07/0.32 ~ ( P @ X4 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Collect_empty_eq
% 0.07/0.32 thf(fact_26_all__not__in__conv,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( ! [X4: b] :
% 0.07/0.32 ~ ( member_b @ X4 @ A2 ) )
% 0.07/0.32 = ( A2 = bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % all_not_in_conv
% 0.07/0.32 thf(fact_27_empty__iff,axiom,
% 0.07/0.32 ! [C: b] :
% 0.07/0.32 ~ ( member_b @ C @ bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % empty_iff
% 0.07/0.32 thf(fact_28_mem__Collect__eq,axiom,
% 0.07/0.32 ! [A: b,P: b > $o] :
% 0.07/0.32 ( ( member_b @ A @ ( collect_b @ P ) )
% 0.07/0.32 = ( P @ A ) ) ).
% 0.07/0.32
% 0.07/0.32 % mem_Collect_eq
% 0.07/0.32 thf(fact_29_Collect__mem__eq,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] : ( member_b @ X4 @ A2 ) )
% 0.07/0.32 = A2 ) ).
% 0.07/0.32
% 0.07/0.32 % Collect_mem_eq
% 0.07/0.32 thf(fact_30_bot__set__def,axiom,
% 0.07/0.32 ( bot_bot_set_b
% 0.07/0.32 = ( collect_b @ bot_bot_b_o ) ) ).
% 0.07/0.32
% 0.07/0.32 % bot_set_def
% 0.07/0.32 thf(fact_31_emptyE,axiom,
% 0.07/0.32 ! [A: b] :
% 0.07/0.32 ~ ( member_b @ A @ bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % emptyE
% 0.07/0.32 thf(fact_32_equals0D,axiom,
% 0.07/0.32 ! [A2: set_b,A: b] :
% 0.07/0.32 ( ( A2 = bot_bot_set_b )
% 0.07/0.32 => ~ ( member_b @ A @ A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % equals0D
% 0.07/0.32 thf(fact_33_equals0I,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ! [Y3: b] :
% 0.07/0.32 ~ ( member_b @ Y3 @ A2 )
% 0.07/0.32 => ( A2 = bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % equals0I
% 0.07/0.32 thf(fact_34_ex__in__conv,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( ? [X4: b] : ( member_b @ X4 @ A2 ) )
% 0.07/0.32 = ( A2 != bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % ex_in_conv
% 0.07/0.32 thf(fact_35_empty__def,axiom,
% 0.07/0.32 ( bot_bot_set_b
% 0.07/0.32 = ( collect_b
% 0.07/0.32 @ ^ [X4: b] : $false ) ) ).
% 0.07/0.32
% 0.07/0.32 % empty_def
% 0.07/0.32 thf(fact_36_Set_Ois__empty__def,axiom,
% 0.07/0.32 ( is_empty_b
% 0.07/0.32 = ( ^ [A3: set_b] : ( A3 = bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Set.is_empty_def
% 0.07/0.32 thf(fact_37_Collect__empty__eq__bot,axiom,
% 0.07/0.32 ! [P: b > $o] :
% 0.07/0.32 ( ( ( collect_b @ P )
% 0.07/0.32 = bot_bot_set_b )
% 0.07/0.32 = ( P = bot_bot_b_o ) ) ).
% 0.07/0.32
% 0.07/0.32 % Collect_empty_eq_bot
% 0.07/0.32 thf(fact_38_bot__empty__eq,axiom,
% 0.07/0.32 ( bot_bot_b_o
% 0.07/0.32 = ( ^ [X4: b] : ( member_b @ X4 @ bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % bot_empty_eq
% 0.07/0.32 thf(fact_39_is__singletonI_H,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( A2 != bot_bot_set_b )
% 0.07/0.32 => ( ! [X: b,Y3: b] :
% 0.07/0.32 ( ( member_b @ X @ A2 )
% 0.07/0.32 => ( ( member_b @ Y3 @ A2 )
% 0.07/0.32 => ( X = Y3 ) ) )
% 0.07/0.32 => ( is_singleton_b @ A2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % is_singletonI'
% 0.07/0.32 thf(fact_40_UNIV__I,axiom,
% 0.07/0.32 ! [X2: b] : ( member_b @ X2 @ top_top_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % UNIV_I
% 0.07/0.32 thf(fact_41_Collect__const,axiom,
% 0.07/0.32 ! [P: $o] :
% 0.07/0.32 ( ( P
% 0.07/0.32 => ( ( collect_b
% 0.07/0.32 @ ^ [S: b] : P )
% 0.07/0.32 = top_top_set_b ) )
% 0.07/0.32 & ( ~ P
% 0.07/0.32 => ( ( collect_b
% 0.07/0.32 @ ^ [S: b] : P )
% 0.07/0.32 = bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Collect_const
% 0.07/0.32 thf(fact_42_UNIV__eq__I,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ! [X: b] : ( member_b @ X @ A2 )
% 0.07/0.32 => ( top_top_set_b = A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % UNIV_eq_I
% 0.07/0.32 thf(fact_43_UNIV__witness,axiom,
% 0.07/0.32 ? [X: b] : ( member_b @ X @ top_top_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % UNIV_witness
% 0.07/0.32 thf(fact_44_empty__not__UNIV,axiom,
% 0.07/0.32 bot_bot_set_b != top_top_set_b ).
% 0.07/0.32
% 0.07/0.32 % empty_not_UNIV
% 0.07/0.32 thf(fact_45_iso__tuple__UNIV__I,axiom,
% 0.07/0.32 ! [X2: b] : ( member_b @ X2 @ top_top_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % iso_tuple_UNIV_I
% 0.07/0.32 thf(fact_46_is__singletonI,axiom,
% 0.07/0.32 ! [X2: b] : ( is_singleton_b @ ( insert_b @ X2 @ bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % is_singletonI
% 0.07/0.32 thf(fact_47_insert__iff,axiom,
% 0.07/0.32 ! [A: b,B2: b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ A @ ( insert_b @ B2 @ A2 ) )
% 0.07/0.32 = ( ( A = B2 )
% 0.07/0.32 | ( member_b @ A @ A2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_iff
% 0.07/0.32 thf(fact_48_insertCI,axiom,
% 0.07/0.32 ! [A: b,B: set_b,B2: b] :
% 0.07/0.32 ( ( ~ ( member_b @ A @ B )
% 0.07/0.32 => ( A = B2 ) )
% 0.07/0.32 => ( member_b @ A @ ( insert_b @ B2 @ B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insertCI
% 0.07/0.32 thf(fact_49_singletonI,axiom,
% 0.07/0.32 ! [A: b] : ( member_b @ A @ ( insert_b @ A @ bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % singletonI
% 0.07/0.32 thf(fact_50_singleton__conv,axiom,
% 0.07/0.32 ! [A: b] :
% 0.07/0.32 ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] : ( X4 = A ) )
% 0.07/0.32 = ( insert_b @ A @ bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % singleton_conv
% 0.07/0.32 thf(fact_51_singleton__conv2,axiom,
% 0.07/0.32 ! [A: b] :
% 0.07/0.32 ( ( collect_b
% 0.07/0.32 @ ( ^ [Y2: b,Z: b] : ( Y2 = Z )
% 0.07/0.32 @ A ) )
% 0.07/0.32 = ( insert_b @ A @ bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % singleton_conv2
% 0.07/0.32 thf(fact_52_mk__disjoint__insert,axiom,
% 0.07/0.32 ! [A: b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ A @ A2 )
% 0.07/0.32 => ? [B3: set_b] :
% 0.07/0.32 ( ( A2
% 0.07/0.32 = ( insert_b @ A @ B3 ) )
% 0.07/0.32 & ~ ( member_b @ A @ B3 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % mk_disjoint_insert
% 0.07/0.32 thf(fact_53_insert__eq__iff,axiom,
% 0.07/0.32 ! [A: b,A2: set_b,B2: b,B: set_b] :
% 0.07/0.32 ( ~ ( member_b @ A @ A2 )
% 0.07/0.32 => ( ~ ( member_b @ B2 @ B )
% 0.07/0.32 => ( ( ( insert_b @ A @ A2 )
% 0.07/0.32 = ( insert_b @ B2 @ B ) )
% 0.07/0.32 = ( ( ( A = B2 )
% 0.07/0.32 => ( A2 = B ) )
% 0.07/0.32 & ( ( A != B2 )
% 0.07/0.32 => ? [C2: set_b] :
% 0.07/0.32 ( ( A2
% 0.07/0.32 = ( insert_b @ B2 @ C2 ) )
% 0.07/0.32 & ~ ( member_b @ B2 @ C2 )
% 0.07/0.32 & ( B
% 0.07/0.32 = ( insert_b @ A @ C2 ) )
% 0.07/0.32 & ~ ( member_b @ A @ C2 ) ) ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_eq_iff
% 0.07/0.32 thf(fact_54_insert__absorb,axiom,
% 0.07/0.32 ! [A: b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ A @ A2 )
% 0.07/0.32 => ( ( insert_b @ A @ A2 )
% 0.07/0.32 = A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_absorb
% 0.07/0.32 thf(fact_55_insert__ident,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ~ ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( ~ ( member_b @ X2 @ B )
% 0.07/0.32 => ( ( ( insert_b @ X2 @ A2 )
% 0.07/0.32 = ( insert_b @ X2 @ B ) )
% 0.07/0.32 = ( A2 = B ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_ident
% 0.07/0.32 thf(fact_56_insert__compr,axiom,
% 0.07/0.32 ( insert_b
% 0.07/0.32 = ( ^ [A4: b,B4: set_b] :
% 0.07/0.32 ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( X4 = A4 )
% 0.07/0.32 | ( member_b @ X4 @ B4 ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_compr
% 0.07/0.32 thf(fact_57_Set_Oset__insert,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ X2 @ A2 )
% 0.07/0.32 => ~ ! [B3: set_b] :
% 0.07/0.32 ( ( A2
% 0.07/0.32 = ( insert_b @ X2 @ B3 ) )
% 0.07/0.32 => ( member_b @ X2 @ B3 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Set.set_insert
% 0.07/0.32 thf(fact_58_insertI2,axiom,
% 0.07/0.32 ! [A: b,B: set_b,B2: b] :
% 0.07/0.32 ( ( member_b @ A @ B )
% 0.07/0.32 => ( member_b @ A @ ( insert_b @ B2 @ B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insertI2
% 0.07/0.32 thf(fact_59_insertI1,axiom,
% 0.07/0.32 ! [A: b,B: set_b] : ( member_b @ A @ ( insert_b @ A @ B ) ) ).
% 0.07/0.32
% 0.07/0.32 % insertI1
% 0.07/0.32 thf(fact_60_insertE,axiom,
% 0.07/0.32 ! [A: b,B2: b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ A @ ( insert_b @ B2 @ A2 ) )
% 0.07/0.32 => ( ( A != B2 )
% 0.07/0.32 => ( member_b @ A @ A2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insertE
% 0.07/0.32 thf(fact_61_top__empty__eq,axiom,
% 0.07/0.32 ( top_top_b_o
% 0.07/0.32 = ( ^ [X4: b] : ( member_b @ X4 @ top_top_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % top_empty_eq
% 0.07/0.32 thf(fact_62_singleton__inject,axiom,
% 0.07/0.32 ! [A: b,B2: b] :
% 0.07/0.32 ( ( ( insert_b @ A @ bot_bot_set_b )
% 0.07/0.32 = ( insert_b @ B2 @ bot_bot_set_b ) )
% 0.07/0.32 => ( A = B2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % singleton_inject
% 0.07/0.32 thf(fact_63_insert__not__empty,axiom,
% 0.07/0.32 ! [A: b,A2: set_b] :
% 0.07/0.32 ( ( insert_b @ A @ A2 )
% 0.07/0.32 != bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % insert_not_empty
% 0.07/0.32 thf(fact_64_doubleton__eq__iff,axiom,
% 0.07/0.32 ! [A: b,B2: b,C: b,D: b] :
% 0.07/0.32 ( ( ( insert_b @ A @ ( insert_b @ B2 @ bot_bot_set_b ) )
% 0.07/0.32 = ( insert_b @ C @ ( insert_b @ D @ bot_bot_set_b ) ) )
% 0.07/0.32 = ( ( ( A = C )
% 0.07/0.32 & ( B2 = D ) )
% 0.07/0.32 | ( ( A = D )
% 0.07/0.32 & ( B2 = C ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % doubleton_eq_iff
% 0.07/0.32 thf(fact_65_singleton__iff,axiom,
% 0.07/0.32 ! [B2: b,A: b] :
% 0.07/0.32 ( ( member_b @ B2 @ ( insert_b @ A @ bot_bot_set_b ) )
% 0.07/0.32 = ( B2 = A ) ) ).
% 0.07/0.32
% 0.07/0.32 % singleton_iff
% 0.07/0.32 thf(fact_66_singletonD,axiom,
% 0.07/0.32 ! [B2: b,A: b] :
% 0.07/0.32 ( ( member_b @ B2 @ ( insert_b @ A @ bot_bot_set_b ) )
% 0.07/0.32 => ( B2 = A ) ) ).
% 0.07/0.32
% 0.07/0.32 % singletonD
% 0.07/0.32 thf(fact_67_Collect__conv__if,axiom,
% 0.07/0.32 ! [P: b > $o,A: b] :
% 0.07/0.32 ( ( ( P @ A )
% 0.07/0.32 => ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( X4 = A )
% 0.07/0.32 & ( P @ X4 ) ) )
% 0.07/0.32 = ( insert_b @ A @ bot_bot_set_b ) ) )
% 0.07/0.32 & ( ~ ( P @ A )
% 0.07/0.32 => ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( X4 = A )
% 0.07/0.32 & ( P @ X4 ) ) )
% 0.07/0.32 = bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Collect_conv_if
% 0.07/0.32 thf(fact_68_Collect__conv__if2,axiom,
% 0.07/0.32 ! [P: b > $o,A: b] :
% 0.07/0.32 ( ( ( P @ A )
% 0.07/0.32 => ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( A = X4 )
% 0.07/0.32 & ( P @ X4 ) ) )
% 0.07/0.32 = ( insert_b @ A @ bot_bot_set_b ) ) )
% 0.07/0.32 & ( ~ ( P @ A )
% 0.07/0.32 => ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( A = X4 )
% 0.07/0.32 & ( P @ X4 ) ) )
% 0.07/0.32 = bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Collect_conv_if2
% 0.07/0.32 thf(fact_69_is__singleton__def,axiom,
% 0.07/0.32 ( is_singleton_b
% 0.07/0.32 = ( ^ [A3: set_b] :
% 0.07/0.32 ? [X4: b] :
% 0.07/0.32 ( A3
% 0.07/0.32 = ( insert_b @ X4 @ bot_bot_set_b ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % is_singleton_def
% 0.07/0.32 thf(fact_70_is__singletonE,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( is_singleton_b @ A2 )
% 0.07/0.32 => ~ ! [X: b] :
% 0.07/0.32 ( A2
% 0.07/0.32 != ( insert_b @ X @ bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % is_singletonE
% 0.07/0.32 thf(fact_71_is__singleton__the__elem,axiom,
% 0.07/0.32 ( is_singleton_b
% 0.07/0.32 = ( ^ [A3: set_b] :
% 0.07/0.32 ( A3
% 0.07/0.32 = ( insert_b @ ( the_elem_b @ A3 ) @ bot_bot_set_b ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % is_singleton_the_elem
% 0.07/0.32 thf(fact_72_the__elem__eq,axiom,
% 0.07/0.32 ! [X2: b] :
% 0.07/0.32 ( ( the_elem_b @ ( insert_b @ X2 @ bot_bot_set_b ) )
% 0.07/0.32 = X2 ) ).
% 0.07/0.32
% 0.07/0.32 % the_elem_eq
% 0.07/0.32 thf(fact_73_image__eqI,axiom,
% 0.07/0.32 ! [B2: b,F: b > b,X2: b,A2: set_b] :
% 0.07/0.32 ( ( B2
% 0.07/0.32 = ( F @ X2 ) )
% 0.07/0.32 => ( ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( member_b @ B2 @ ( image_b_b @ F @ A2 ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % image_eqI
% 0.07/0.32 thf(fact_74_image__is__empty,axiom,
% 0.07/0.32 ! [F: b > b,A2: set_b] :
% 0.07/0.32 ( ( ( image_b_b @ F @ A2 )
% 0.07/0.32 = bot_bot_set_b )
% 0.07/0.32 = ( A2 = bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % image_is_empty
% 0.07/0.32 thf(fact_75_empty__is__image,axiom,
% 0.07/0.32 ! [F: b > b,A2: set_b] :
% 0.07/0.32 ( ( bot_bot_set_b
% 0.07/0.32 = ( image_b_b @ F @ A2 ) )
% 0.07/0.32 = ( A2 = bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % empty_is_image
% 0.07/0.32 thf(fact_76_image__empty,axiom,
% 0.07/0.32 ! [F: b > b] :
% 0.07/0.32 ( ( image_b_b @ F @ bot_bot_set_b )
% 0.07/0.32 = bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % image_empty
% 0.07/0.32 thf(fact_77_imageE,axiom,
% 0.07/0.32 ! [B2: b,F: b > b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ B2 @ ( image_b_b @ F @ A2 ) )
% 0.07/0.32 => ~ ! [X: b] :
% 0.07/0.32 ( ( B2
% 0.07/0.32 = ( F @ X ) )
% 0.07/0.32 => ~ ( member_b @ X @ A2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % imageE
% 0.07/0.32 thf(fact_78_imageI,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b,F: b > b] :
% 0.07/0.32 ( ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( member_b @ ( F @ X2 ) @ ( image_b_b @ F @ A2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % imageI
% 0.07/0.32 thf(fact_79_rev__image__eqI,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b,B2: b,F: b > b] :
% 0.07/0.32 ( ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( ( B2
% 0.07/0.32 = ( F @ X2 ) )
% 0.07/0.32 => ( member_b @ B2 @ ( image_b_b @ F @ A2 ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % rev_image_eqI
% 0.07/0.32 thf(fact_80_Compr__image__eq,axiom,
% 0.07/0.32 ! [F: b > b,A2: set_b,P: b > $o] :
% 0.07/0.32 ( ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( member_b @ X4 @ ( image_b_b @ F @ A2 ) )
% 0.07/0.32 & ( P @ X4 ) ) )
% 0.07/0.32 = ( image_b_b @ F
% 0.07/0.32 @ ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( member_b @ X4 @ A2 )
% 0.07/0.32 & ( P @ ( F @ X4 ) ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Compr_image_eq
% 0.07/0.32 thf(fact_81_inv__into__into,axiom,
% 0.07/0.32 ! [X2: b,F: b > b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ X2 @ ( image_b_b @ F @ A2 ) )
% 0.07/0.32 => ( member_b @ ( hilbert_inv_into_b_b @ A2 @ F @ X2 ) @ A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % inv_into_into
% 0.07/0.32 thf(fact_82_image__constant,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b,C: b] :
% 0.07/0.32 ( ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( ( image_b_b
% 0.07/0.32 @ ^ [X4: b] : C
% 0.07/0.32 @ A2 )
% 0.07/0.32 = ( insert_b @ C @ bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % image_constant
% 0.07/0.32 thf(fact_83_image__constant__conv,axiom,
% 0.07/0.32 ! [A2: set_b,C: b] :
% 0.07/0.32 ( ( ( A2 = bot_bot_set_b )
% 0.07/0.32 => ( ( image_b_b
% 0.07/0.32 @ ^ [X4: b] : C
% 0.07/0.32 @ A2 )
% 0.07/0.32 = bot_bot_set_b ) )
% 0.07/0.32 & ( ( A2 != bot_bot_set_b )
% 0.07/0.32 => ( ( image_b_b
% 0.07/0.32 @ ^ [X4: b] : C
% 0.07/0.32 @ A2 )
% 0.07/0.32 = ( insert_b @ C @ bot_bot_set_b ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % image_constant_conv
% 0.07/0.32 thf(fact_84_bij__betw__empty2,axiom,
% 0.07/0.32 ! [F: b > b,A2: set_b] :
% 0.07/0.32 ( ( bij_betw_b_b @ F @ A2 @ bot_bot_set_b )
% 0.07/0.32 => ( A2 = bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % bij_betw_empty2
% 0.07/0.32 thf(fact_85_bij__betw__empty1,axiom,
% 0.07/0.32 ! [F: b > b,A2: set_b] :
% 0.07/0.32 ( ( bij_betw_b_b @ F @ bot_bot_set_b @ A2 )
% 0.07/0.32 => ( A2 = bot_bot_set_b ) ) ).
% 0.07/0.32
% 0.07/0.32 % bij_betw_empty1
% 0.07/0.32 thf(fact_86_inj__singleton,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( inj_on_b_set_b
% 0.07/0.32 @ ^ [X4: b] : ( insert_b @ X4 @ bot_bot_set_b )
% 0.07/0.32 @ A2 ) ).
% 0.07/0.32
% 0.07/0.32 % inj_singleton
% 0.07/0.32 thf(fact_87_inj__img__insertE,axiom,
% 0.07/0.32 ! [F: b > b,A2: set_b,X2: b,B: set_b] :
% 0.07/0.32 ( ( inj_on_b_b @ F @ A2 )
% 0.07/0.32 => ( ~ ( member_b @ X2 @ B )
% 0.07/0.32 => ( ( ( insert_b @ X2 @ B )
% 0.07/0.32 = ( image_b_b @ F @ A2 ) )
% 0.07/0.32 => ~ ! [X6: b,A5: set_b] :
% 0.07/0.32 ( ~ ( member_b @ X6 @ A5 )
% 0.07/0.32 => ( ( A2
% 0.07/0.32 = ( insert_b @ X6 @ A5 ) )
% 0.07/0.32 => ( ( X2
% 0.07/0.32 = ( F @ X6 ) )
% 0.07/0.32 => ( B
% 0.07/0.32 != ( image_b_b @ F @ A5 ) ) ) ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % inj_img_insertE
% 0.07/0.32 thf(fact_88_inj__image__mem__iff,axiom,
% 0.07/0.32 ! [F: b > b,A: b,A2: set_b] :
% 0.07/0.32 ( ( inj_on_b_b @ F @ top_top_set_b )
% 0.07/0.32 => ( ( member_b @ ( F @ A ) @ ( image_b_b @ F @ A2 ) )
% 0.07/0.32 = ( member_b @ A @ A2 ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % inj_image_mem_iff
% 0.07/0.32 thf(fact_89_inj__on__insert,axiom,
% 0.07/0.32 ! [F: b > b,A: b,A2: set_b] :
% 0.07/0.32 ( ( inj_on_b_b @ F @ ( insert_b @ A @ A2 ) )
% 0.07/0.32 = ( ( inj_on_b_b @ F @ A2 )
% 0.07/0.32 & ~ ( member_b @ ( F @ A ) @ ( image_b_b @ F @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % inj_on_insert
% 0.07/0.32 thf(fact_90_DiffI,axiom,
% 0.07/0.32 ! [C: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ( member_b @ C @ A2 )
% 0.07/0.32 => ( ~ ( member_b @ C @ B )
% 0.07/0.32 => ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % DiffI
% 0.07/0.32 thf(fact_91_Diff__iff,axiom,
% 0.07/0.32 ! [C: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 0.07/0.32 = ( ( member_b @ C @ A2 )
% 0.07/0.32 & ~ ( member_b @ C @ B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_iff
% 0.07/0.32 thf(fact_92_Diff__empty,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( minus_minus_set_b @ A2 @ bot_bot_set_b )
% 0.07/0.32 = A2 ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_empty
% 0.07/0.32 thf(fact_93_empty__Diff,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( minus_minus_set_b @ bot_bot_set_b @ A2 )
% 0.07/0.32 = bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % empty_Diff
% 0.07/0.32 thf(fact_94_Diff__cancel,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( minus_minus_set_b @ A2 @ A2 )
% 0.07/0.32 = bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_cancel
% 0.07/0.32 thf(fact_95_insert__Diff1,axiom,
% 0.07/0.32 ! [X2: b,B: set_b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ X2 @ B )
% 0.07/0.32 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ B )
% 0.07/0.32 = ( minus_minus_set_b @ A2 @ B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_Diff1
% 0.07/0.32 thf(fact_96_Diff__insert0,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ~ ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( ( minus_minus_set_b @ A2 @ ( insert_b @ X2 @ B ) )
% 0.07/0.32 = ( minus_minus_set_b @ A2 @ B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_insert0
% 0.07/0.32 thf(fact_97_insert__Diff__single,axiom,
% 0.07/0.32 ! [A: b,A2: set_b] :
% 0.07/0.32 ( ( insert_b @ A @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) )
% 0.07/0.32 = ( insert_b @ A @ A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_Diff_single
% 0.07/0.32 thf(fact_98_Diff__UNIV,axiom,
% 0.07/0.32 ! [A2: set_b] :
% 0.07/0.32 ( ( minus_minus_set_b @ A2 @ top_top_set_b )
% 0.07/0.32 = bot_bot_set_b ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_UNIV
% 0.07/0.32 thf(fact_99_Diff__insert__absorb,axiom,
% 0.07/0.32 ! [X2: b,A2: set_b] :
% 0.07/0.32 ( ~ ( member_b @ X2 @ A2 )
% 0.07/0.32 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ ( insert_b @ X2 @ bot_bot_set_b ) )
% 0.07/0.32 = A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_insert_absorb
% 0.07/0.32 thf(fact_100_Diff__insert2,axiom,
% 0.07/0.32 ! [A2: set_b,A: b,B: set_b] :
% 0.07/0.32 ( ( minus_minus_set_b @ A2 @ ( insert_b @ A @ B ) )
% 0.07/0.32 = ( minus_minus_set_b @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) @ B ) ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_insert2
% 0.07/0.32 thf(fact_101_insert__Diff,axiom,
% 0.07/0.32 ! [A: b,A2: set_b] :
% 0.07/0.32 ( ( member_b @ A @ A2 )
% 0.07/0.32 => ( ( insert_b @ A @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) )
% 0.07/0.32 = A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_Diff
% 0.07/0.32 thf(fact_102_Diff__insert,axiom,
% 0.07/0.32 ! [A2: set_b,A: b,B: set_b] :
% 0.07/0.32 ( ( minus_minus_set_b @ A2 @ ( insert_b @ A @ B ) )
% 0.07/0.32 = ( minus_minus_set_b @ ( minus_minus_set_b @ A2 @ B ) @ ( insert_b @ A @ bot_bot_set_b ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % Diff_insert
% 0.07/0.32 thf(fact_103_in__image__insert__iff,axiom,
% 0.07/0.32 ! [B: set_set_b,X2: b,A2: set_b] :
% 0.07/0.32 ( ! [C3: set_b] :
% 0.07/0.32 ( ( member_set_b @ C3 @ B )
% 0.07/0.32 => ~ ( member_b @ X2 @ C3 ) )
% 0.07/0.32 => ( ( member_set_b @ A2 @ ( image_set_b_set_b @ ( insert_b @ X2 ) @ B ) )
% 0.07/0.32 = ( ( member_b @ X2 @ A2 )
% 0.07/0.32 & ( member_set_b @ ( minus_minus_set_b @ A2 @ ( insert_b @ X2 @ bot_bot_set_b ) ) @ B ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % in_image_insert_iff
% 0.07/0.32 thf(fact_104_DiffE,axiom,
% 0.07/0.32 ! [C: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 0.07/0.32 => ~ ( ( member_b @ C @ A2 )
% 0.07/0.32 => ( member_b @ C @ B ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % DiffE
% 0.07/0.32 thf(fact_105_DiffD1,axiom,
% 0.07/0.32 ! [C: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 0.07/0.32 => ( member_b @ C @ A2 ) ) ).
% 0.07/0.32
% 0.07/0.32 % DiffD1
% 0.07/0.32 thf(fact_106_DiffD2,axiom,
% 0.07/0.32 ! [C: b,A2: set_b,B: set_b] :
% 0.07/0.32 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 0.07/0.32 => ~ ( member_b @ C @ B ) ) ).
% 0.07/0.32
% 0.07/0.32 % DiffD2
% 0.07/0.32 thf(fact_107_set__diff__eq,axiom,
% 0.07/0.32 ( minus_minus_set_b
% 0.07/0.32 = ( ^ [A3: set_b,B4: set_b] :
% 0.07/0.32 ( collect_b
% 0.07/0.32 @ ^ [X4: b] :
% 0.07/0.32 ( ( member_b @ X4 @ A3 )
% 0.07/0.32 & ~ ( member_b @ X4 @ B4 ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % set_diff_eq
% 0.07/0.32 thf(fact_108_insert__Diff__if,axiom,
% 0.07/0.32 ! [X2: b,B: set_b,A2: set_b] :
% 0.07/0.32 ( ( ( member_b @ X2 @ B )
% 0.07/0.32 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ B )
% 0.07/0.32 = ( minus_minus_set_b @ A2 @ B ) ) )
% 0.07/0.32 & ( ~ ( member_b @ X2 @ B )
% 0.07/0.32 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ B )
% 0.07/0.32 = ( insert_b @ X2 @ ( minus_minus_set_b @ A2 @ B ) ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % insert_Diff_if
% 0.07/0.32 thf(fact_109_remove__def,axiom,
% 0.07/0.32 ( remove_b
% 0.07/0.32 = ( ^ [X4: b,A3: set_b] : ( minus_minus_set_b @ A3 @ ( insert_b @ X4 @ bot_bot_set_b ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 % remove_def
% 0.07/0.32
% 0.07/0.32 % Conjectures (2)
% 0.07/0.32 thf(conj_0,hypothesis,
% 0.07/0.32 ! [X5: a] :
% 0.07/0.32 ( ( p @ X5 )
% 0.07/0.32 => ? [X_12: b] : ( q @ X5 @ X_12 ) ) ).
% 0.07/0.32
% 0.07/0.32 thf(conj_1,conjecture,
% 0.07/0.32 ! [X: a] :
% 0.07/0.32 ( ~ ( p @ X )
% 0.07/0.32 | ( q @ X @ ( hilbert_Eps_b @ ( q @ X ) ) ) ) ).
% 0.07/0.32
% 0.07/0.32 %------------------------------------------------------------------------------
% 0.07/0.32 ------------------------
% 1.15/0.98 ---- Embedded in THF ---
% 1.15/0.98 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.15/0.98 %%% Generated on Tue Feb 24 03:27:41 EST 2026
% 1.15/0.98 %%% using '$$dhol' embedding, version 1.3.0.
% 1.15/0.98 %%% Logic specification used:
% 1.15/0.98 %%% thf(spec, logic, $$dhol).
% 1.15/0.98
% 1.15/0.98 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2DTF5930.p
% See solution above
% 1.15/0.98 ------------------------
% 1.15/0.99 ---- Cleaned THF ---
% 1.15/1.00 thf(ty_n_t__Set__Oset_It__Set__Oset_Itf__b_J_J,type,
% 1.15/1.00 set_set_b: $tType ).
% 1.15/1.00
% 1.15/1.00 thf(ty_n_t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 set_b: $tType ).
% 1.15/1.00
% 1.15/1.00 thf(ty_n_tf__b,type,
% 1.15/1.00 b: $tType ).
% 1.15/1.00
% 1.15/1.00 thf(ty_n_tf__a,type,
% 1.15/1.00 a: $tType ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Fun_Obij__betw_001tf__b_001tf__b,type,
% 1.15/1.00 bij_betw_b_b: ( b > b ) > set_b > set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Fun_Oinj__on_001tf__b_001t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 inj_on_b_set_b: ( b > set_b ) > set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Fun_Oinj__on_001tf__b_001tf__b,type,
% 1.15/1.00 inj_on_b_b: ( b > b ) > set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Groups_Ominus__class_Ominus_001t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 minus_minus_set_b: set_b > set_b > set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Hilbert__Choice_OEps_001tf__b,type,
% 1.15/1.00 hilbert_Eps_b: ( b > $o ) > b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Hilbert__Choice_Oinv__into_001tf__b_001tf__b,type,
% 1.15/1.00 hilbert_inv_into_b_b: set_b > ( b > b ) > b > b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Orderings_Obot__class_Obot_001_062_Itf__b_M_Eo_J,type,
% 1.15/1.00 bot_bot_b_o: b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Orderings_Obot__class_Obot_001t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 bot_bot_set_b: set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Orderings_Otop__class_Otop_001_062_Itf__b_M_Eo_J,type,
% 1.15/1.00 top_top_b_o: b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Orderings_Otop__class_Otop_001t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 top_top_set_b: set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_OCollect_001tf__b,type,
% 1.15/1.00 collect_b: ( b > $o ) > set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Oimage_001t__Set__Oset_Itf__b_J_001t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 image_set_b_set_b: ( set_b > set_b ) > set_set_b > set_set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Oimage_001tf__b_001tf__b,type,
% 1.15/1.00 image_b_b: ( b > b ) > set_b > set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Oinsert_001tf__b,type,
% 1.15/1.00 insert_b: b > set_b > set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Ois__empty_001tf__b,type,
% 1.15/1.00 is_empty_b: set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Ois__singleton_001tf__b,type,
% 1.15/1.00 is_singleton_b: set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Oremove_001tf__b,type,
% 1.15/1.00 remove_b: b > set_b > set_b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_Set_Othe__elem_001tf__b,type,
% 1.15/1.00 the_elem_b: set_b > b ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_member_001t__Set__Oset_Itf__b_J,type,
% 1.15/1.00 member_set_b: set_b > set_set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_c_member_001tf__b,type,
% 1.15/1.00 member_b: b > set_b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_v_P,type,
% 1.15/1.00 p: a > $o ).
% 1.15/1.00
% 1.15/1.00 thf(sy_v_Q,type,
% 1.15/1.00 q: a > b > $o ).
% 1.15/1.00
% 1.15/1.00 thf(fact_0_some__equality,axiom,
% 1.15/1.00 ! [P: b > $o,A: b] :
% 1.15/1.00 ( ( P @ A )
% 1.15/1.00 => ( ! [X: b] :
% 1.15/1.00 ( ( P @ X )
% 1.15/1.00 => ( X = A ) )
% 1.15/1.00 => ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = A ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_1_some__eq__trivial,axiom,
% 1.15/1.00 ! [X2: b] :
% 1.15/1.00 ( ( hilbert_Eps_b
% 1.15/1.00 @ ^ [Y: b] : ( Y = X2 ) )
% 1.15/1.00 = X2 ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_2_some__sym__eq__trivial,axiom,
% 1.15/1.00 ! [X2: b] :
% 1.15/1.00 ( ( hilbert_Eps_b
% 1.15/1.00 @ ( ^ [Y2: b,Z: b] : ( Y2 = Z )
% 1.15/1.00 @ X2 ) )
% 1.15/1.00 = X2 ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_3_verit__sko__ex_H,axiom,
% 1.15/1.00 ! [P: b > $o,A2: $o] :
% 1.15/1.00 ( ( ( P @ ( hilbert_Eps_b @ P ) )
% 1.15/1.00 = A2 )
% 1.15/1.00 => ( ( ? [X3: b] : ( P @ X3 ) )
% 1.15/1.00 = A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_4_verit__sko__forall,axiom,
% 1.15/1.00 ( ( ^ [P2: b > $o] :
% 1.15/1.00 ! [X3: b] : ( P2 @ X3 ) )
% 1.15/1.00 = ( ^ [P3: b > $o] :
% 1.15/1.00 ( P3
% 1.15/1.00 @ ( hilbert_Eps_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ~ ( P3 @ X4 ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_5_someI2,axiom,
% 1.15/1.00 ! [P: b > $o,A: b,Q: b > $o] :
% 1.15/1.00 ( ( P @ A )
% 1.15/1.00 => ( ! [X: b] :
% 1.15/1.00 ( ( P @ X )
% 1.15/1.00 => ( Q @ X ) )
% 1.15/1.00 => ( Q @ ( hilbert_Eps_b @ P ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_6_verit__sko__forall_H,axiom,
% 1.15/1.00 ! [P: b > $o,A2: $o] :
% 1.15/1.00 ( ( ( P
% 1.15/1.00 @ ( hilbert_Eps_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ~ ( P @ X4 ) ) )
% 1.15/1.00 = A2 )
% 1.15/1.00 => ( ( ! [X3: b] : ( P @ X3 ) )
% 1.15/1.00 = A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_7_verit__sko__forall_H_H,axiom,
% 1.15/1.00 ! [B: b,A2: b,P: b > $o] :
% 1.15/1.00 ( ( B = A2 )
% 1.15/1.00 => ( ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = A2 )
% 1.15/1.00 = ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_8_someI__ex,axiom,
% 1.15/1.00 ! [P: b > $o] :
% 1.15/1.00 ( ? [X_1: b] : ( P @ X_1 )
% 1.15/1.00 => ( P @ ( hilbert_Eps_b @ P ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_9_someI2__ex,axiom,
% 1.15/1.00 ! [P: b > $o,Q: b > $o] :
% 1.15/1.00 ( ? [X_1: b] : ( P @ X_1 )
% 1.15/1.00 => ( ! [X: b] :
% 1.15/1.00 ( ( P @ X )
% 1.15/1.00 => ( Q @ X ) )
% 1.15/1.00 => ( Q @ ( hilbert_Eps_b @ P ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_10_someI2__bex,axiom,
% 1.15/1.00 ! [A2: set_b,P: b > $o,Q: b > $o] :
% 1.15/1.00 ( ? [X5: b] :
% 1.15/1.00 ( ( member_b @ X5 @ A2 )
% 1.15/1.00 & ( P @ X5 ) )
% 1.15/1.00 => ( ! [X: b] :
% 1.15/1.00 ( ( ( member_b @ X @ A2 )
% 1.15/1.00 & ( P @ X ) )
% 1.15/1.00 => ( Q @ X ) )
% 1.15/1.00 => ( Q
% 1.15/1.00 @ ( hilbert_Eps_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( member_b @ X4 @ A2 )
% 1.15/1.00 & ( P @ X4 ) ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_11_some__eq__ex,axiom,
% 1.15/1.00 ! [P: b > $o] :
% 1.15/1.00 ( ( P @ ( hilbert_Eps_b @ P ) )
% 1.15/1.00 = ( ? [X3: b] : ( P @ X3 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_12_some__eq__imp,axiom,
% 1.15/1.00 ! [P: b > $o,A: b,B2: b] :
% 1.15/1.00 ( ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = A )
% 1.15/1.00 => ( ( P @ B2 )
% 1.15/1.00 => ( P @ A ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_13_tfl__some,axiom,
% 1.15/1.00 ! [P4: b > $o,X5: b] :
% 1.15/1.00 ( ( P4 @ X5 )
% 1.15/1.00 => ( P4 @ ( hilbert_Eps_b @ P4 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_14_Eps__cong,axiom,
% 1.15/1.00 ! [P: b > $o,Q: b > $o] :
% 1.15/1.00 ( ! [X: b] :
% 1.15/1.00 ( ( P @ X )
% 1.15/1.00 = ( Q @ X ) )
% 1.15/1.00 => ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = ( hilbert_Eps_b @ Q ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_15_someI,axiom,
% 1.15/1.00 ! [P: b > $o,X2: b] :
% 1.15/1.00 ( ( P @ X2 )
% 1.15/1.00 => ( P @ ( hilbert_Eps_b @ P ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_16_verit__sko__forall__indirect2,axiom,
% 1.15/1.00 ! [X2: b,P: b > $o,P5: b > $o] :
% 1.15/1.00 ( ( X2
% 1.15/1.00 = ( hilbert_Eps_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ~ ( P @ X4 ) ) )
% 1.15/1.00 => ( ! [X: b] :
% 1.15/1.00 ( ( P @ X )
% 1.15/1.00 = ( P5 @ X ) )
% 1.15/1.00 => ( ( ! [X3: b] : ( P5 @ X3 ) )
% 1.15/1.00 = ( P @ X2 ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_17_verit__sko__forall__indirect,axiom,
% 1.15/1.00 ! [X2: b,P: b > $o] :
% 1.15/1.00 ( ( X2
% 1.15/1.00 = ( hilbert_Eps_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ~ ( P @ X4 ) ) )
% 1.15/1.00 => ( ( ! [X3: b] : ( P @ X3 ) )
% 1.15/1.00 = ( P @ X2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_18_some1__equality,axiom,
% 1.15/1.00 ! [P: b > $o,A: b] :
% 1.15/1.00 ( ? [X5: b] :
% 1.15/1.00 ( ( P @ X5 )
% 1.15/1.00 & ! [Y3: b] :
% 1.15/1.00 ( ( P @ Y3 )
% 1.15/1.00 => ( Y3 = X5 ) ) )
% 1.15/1.00 => ( ( P @ A )
% 1.15/1.00 => ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = A ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_19_verit__sko__ex__indirect2,axiom,
% 1.15/1.00 ! [X2: b,P: b > $o,P5: b > $o] :
% 1.15/1.00 ( ( X2
% 1.15/1.00 = ( hilbert_Eps_b @ P ) )
% 1.15/1.00 => ( ! [X: b] :
% 1.15/1.00 ( ( P @ X )
% 1.15/1.00 = ( P5 @ X ) )
% 1.15/1.00 => ( ( ? [X3: b] : ( P5 @ X3 ) )
% 1.15/1.00 = ( P @ X2 ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_20_verit__sko__ex__indirect,axiom,
% 1.15/1.00 ! [X2: b,P: b > $o] :
% 1.15/1.00 ( ( X2
% 1.15/1.00 = ( hilbert_Eps_b @ P ) )
% 1.15/1.00 => ( ( ? [X3: b] : ( P @ X3 ) )
% 1.15/1.00 = ( P @ X2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_21_Nitpick_OEps__psimp,axiom,
% 1.15/1.00 ! [P: b > $o,X2: b,Y4: b] :
% 1.15/1.00 ( ( P @ X2 )
% 1.15/1.00 => ( ~ ( P @ Y4 )
% 1.15/1.00 => ( ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = Y4 )
% 1.15/1.00 => ( ( hilbert_Eps_b @ P )
% 1.15/1.00 = X2 ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_22_some__in__eq,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( member_b
% 1.15/1.00 @ ( hilbert_Eps_b
% 1.15/1.00 @ ^ [X4: b] : ( member_b @ X4 @ A2 ) )
% 1.15/1.00 @ A2 )
% 1.15/1.00 = ( A2 != bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_23_exE__some,axiom,
% 1.15/1.00 ! [P: b > $o,C: b] :
% 1.15/1.00 ( ? [X_1: b] : ( P @ X_1 )
% 1.15/1.00 => ( ( C
% 1.15/1.00 = ( hilbert_Eps_b @ P ) )
% 1.15/1.00 => ( P @ C ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_24_empty__Collect__eq,axiom,
% 1.15/1.00 ! [P: b > $o] :
% 1.15/1.00 ( ( bot_bot_set_b
% 1.15/1.00 = ( collect_b @ P ) )
% 1.15/1.00 = ( ! [X4: b] :
% 1.15/1.00 ~ ( P @ X4 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_25_Collect__empty__eq,axiom,
% 1.15/1.00 ! [P: b > $o] :
% 1.15/1.00 ( ( ( collect_b @ P )
% 1.15/1.00 = bot_bot_set_b )
% 1.15/1.00 = ( ! [X4: b] :
% 1.15/1.00 ~ ( P @ X4 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_26_all__not__in__conv,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( ! [X4: b] :
% 1.15/1.00 ~ ( member_b @ X4 @ A2 ) )
% 1.15/1.00 = ( A2 = bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_27_empty__iff,axiom,
% 1.15/1.00 ! [C: b] :
% 1.15/1.00 ~ ( member_b @ C @ bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_28_mem__Collect__eq,axiom,
% 1.15/1.00 ! [A: b,P: b > $o] :
% 1.15/1.00 ( ( member_b @ A @ ( collect_b @ P ) )
% 1.15/1.00 = ( P @ A ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_29_Collect__mem__eq,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] : ( member_b @ X4 @ A2 ) )
% 1.15/1.00 = A2 ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_30_bot__set__def,axiom,
% 1.15/1.00 ( bot_bot_set_b
% 1.15/1.00 = ( collect_b @ bot_bot_b_o ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_31_emptyE,axiom,
% 1.15/1.00 ! [A: b] :
% 1.15/1.00 ~ ( member_b @ A @ bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_32_equals0D,axiom,
% 1.15/1.00 ! [A2: set_b,A: b] :
% 1.15/1.00 ( ( A2 = bot_bot_set_b )
% 1.15/1.00 => ~ ( member_b @ A @ A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_33_equals0I,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ! [Y3: b] :
% 1.15/1.00 ~ ( member_b @ Y3 @ A2 )
% 1.15/1.00 => ( A2 = bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_34_ex__in__conv,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( ? [X4: b] : ( member_b @ X4 @ A2 ) )
% 1.15/1.00 = ( A2 != bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_35_empty__def,axiom,
% 1.15/1.00 ( bot_bot_set_b
% 1.15/1.00 = ( collect_b
% 1.15/1.00 @ ^ [X4: b] : $false ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_36_Set_Ois__empty__def,axiom,
% 1.15/1.00 ( is_empty_b
% 1.15/1.00 = ( ^ [A3: set_b] : ( A3 = bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_37_Collect__empty__eq__bot,axiom,
% 1.15/1.00 ! [P: b > $o] :
% 1.15/1.00 ( ( ( collect_b @ P )
% 1.15/1.00 = bot_bot_set_b )
% 1.15/1.00 = ( P = bot_bot_b_o ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_38_bot__empty__eq,axiom,
% 1.15/1.00 ( bot_bot_b_o
% 1.15/1.00 = ( ^ [X4: b] : ( member_b @ X4 @ bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_39_is__singletonI_H,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( A2 != bot_bot_set_b )
% 1.15/1.00 => ( ! [X: b,Y3: b] :
% 1.15/1.00 ( ( member_b @ X @ A2 )
% 1.15/1.00 => ( ( member_b @ Y3 @ A2 )
% 1.15/1.00 => ( X = Y3 ) ) )
% 1.15/1.00 => ( is_singleton_b @ A2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_40_UNIV__I,axiom,
% 1.15/1.00 ! [X2: b] : ( member_b @ X2 @ top_top_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_41_Collect__const,axiom,
% 1.15/1.00 ! [P: $o] :
% 1.15/1.00 ( ( P
% 1.15/1.00 => ( ( collect_b
% 1.15/1.00 @ ^ [S: b] : P )
% 1.15/1.00 = top_top_set_b ) )
% 1.15/1.00 & ( ~ P
% 1.15/1.00 => ( ( collect_b
% 1.15/1.00 @ ^ [S: b] : P )
% 1.15/1.00 = bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_42_UNIV__eq__I,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ! [X: b] : ( member_b @ X @ A2 )
% 1.15/1.00 => ( top_top_set_b = A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_43_UNIV__witness,axiom,
% 1.15/1.00 ? [X: b] : ( member_b @ X @ top_top_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_44_empty__not__UNIV,axiom,
% 1.15/1.00 bot_bot_set_b != top_top_set_b ).
% 1.15/1.00
% 1.15/1.00 thf(fact_45_iso__tuple__UNIV__I,axiom,
% 1.15/1.00 ! [X2: b] : ( member_b @ X2 @ top_top_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_46_is__singletonI,axiom,
% 1.15/1.00 ! [X2: b] : ( is_singleton_b @ ( insert_b @ X2 @ bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_47_insert__iff,axiom,
% 1.15/1.00 ! [A: b,B2: b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ A @ ( insert_b @ B2 @ A2 ) )
% 1.15/1.00 = ( ( A = B2 )
% 1.15/1.00 | ( member_b @ A @ A2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_48_insertCI,axiom,
% 1.15/1.00 ! [A: b,B: set_b,B2: b] :
% 1.15/1.00 ( ( ~ ( member_b @ A @ B )
% 1.15/1.00 => ( A = B2 ) )
% 1.15/1.00 => ( member_b @ A @ ( insert_b @ B2 @ B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_49_singletonI,axiom,
% 1.15/1.00 ! [A: b] : ( member_b @ A @ ( insert_b @ A @ bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_50_singleton__conv,axiom,
% 1.15/1.00 ! [A: b] :
% 1.15/1.00 ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] : ( X4 = A ) )
% 1.15/1.00 = ( insert_b @ A @ bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_51_singleton__conv2,axiom,
% 1.15/1.00 ! [A: b] :
% 1.15/1.00 ( ( collect_b
% 1.15/1.00 @ ( ^ [Y2: b,Z: b] : ( Y2 = Z )
% 1.15/1.00 @ A ) )
% 1.15/1.00 = ( insert_b @ A @ bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_52_mk__disjoint__insert,axiom,
% 1.15/1.00 ! [A: b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ A @ A2 )
% 1.15/1.00 => ? [B3: set_b] :
% 1.15/1.00 ( ( A2
% 1.15/1.00 = ( insert_b @ A @ B3 ) )
% 1.15/1.00 & ~ ( member_b @ A @ B3 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_53_insert__eq__iff,axiom,
% 1.15/1.00 ! [A: b,A2: set_b,B2: b,B: set_b] :
% 1.15/1.00 ( ~ ( member_b @ A @ A2 )
% 1.15/1.00 => ( ~ ( member_b @ B2 @ B )
% 1.15/1.00 => ( ( ( insert_b @ A @ A2 )
% 1.15/1.00 = ( insert_b @ B2 @ B ) )
% 1.15/1.00 = ( ( ( A = B2 )
% 1.15/1.00 => ( A2 = B ) )
% 1.15/1.00 & ( ( A != B2 )
% 1.15/1.00 => ? [C2: set_b] :
% 1.15/1.00 ( ( A2
% 1.15/1.00 = ( insert_b @ B2 @ C2 ) )
% 1.15/1.00 & ~ ( member_b @ B2 @ C2 )
% 1.15/1.00 & ( B
% 1.15/1.00 = ( insert_b @ A @ C2 ) )
% 1.15/1.00 & ~ ( member_b @ A @ C2 ) ) ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_54_insert__absorb,axiom,
% 1.15/1.00 ! [A: b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ A @ A2 )
% 1.15/1.00 => ( ( insert_b @ A @ A2 )
% 1.15/1.00 = A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_55_insert__ident,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ~ ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( ~ ( member_b @ X2 @ B )
% 1.15/1.00 => ( ( ( insert_b @ X2 @ A2 )
% 1.15/1.00 = ( insert_b @ X2 @ B ) )
% 1.15/1.00 = ( A2 = B ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_56_insert__compr,axiom,
% 1.15/1.00 ( insert_b
% 1.15/1.00 = ( ^ [A4: b,B4: set_b] :
% 1.15/1.00 ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( X4 = A4 )
% 1.15/1.00 | ( member_b @ X4 @ B4 ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_57_Set_Oset__insert,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ X2 @ A2 )
% 1.15/1.00 => ~ ! [B3: set_b] :
% 1.15/1.00 ( ( A2
% 1.15/1.00 = ( insert_b @ X2 @ B3 ) )
% 1.15/1.00 => ( member_b @ X2 @ B3 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_58_insertI2,axiom,
% 1.15/1.00 ! [A: b,B: set_b,B2: b] :
% 1.15/1.00 ( ( member_b @ A @ B )
% 1.15/1.00 => ( member_b @ A @ ( insert_b @ B2 @ B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_59_insertI1,axiom,
% 1.15/1.00 ! [A: b,B: set_b] : ( member_b @ A @ ( insert_b @ A @ B ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_60_insertE,axiom,
% 1.15/1.00 ! [A: b,B2: b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ A @ ( insert_b @ B2 @ A2 ) )
% 1.15/1.00 => ( ( A != B2 )
% 1.15/1.00 => ( member_b @ A @ A2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_61_top__empty__eq,axiom,
% 1.15/1.00 ( top_top_b_o
% 1.15/1.00 = ( ^ [X4: b] : ( member_b @ X4 @ top_top_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_62_singleton__inject,axiom,
% 1.15/1.00 ! [A: b,B2: b] :
% 1.15/1.00 ( ( ( insert_b @ A @ bot_bot_set_b )
% 1.15/1.00 = ( insert_b @ B2 @ bot_bot_set_b ) )
% 1.15/1.00 => ( A = B2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_63_insert__not__empty,axiom,
% 1.15/1.00 ! [A: b,A2: set_b] :
% 1.15/1.00 ( ( insert_b @ A @ A2 )
% 1.15/1.00 != bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_64_doubleton__eq__iff,axiom,
% 1.15/1.00 ! [A: b,B2: b,C: b,D: b] :
% 1.15/1.00 ( ( ( insert_b @ A @ ( insert_b @ B2 @ bot_bot_set_b ) )
% 1.15/1.00 = ( insert_b @ C @ ( insert_b @ D @ bot_bot_set_b ) ) )
% 1.15/1.00 = ( ( ( A = C )
% 1.15/1.00 & ( B2 = D ) )
% 1.15/1.00 | ( ( A = D )
% 1.15/1.00 & ( B2 = C ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_65_singleton__iff,axiom,
% 1.15/1.00 ! [B2: b,A: b] :
% 1.15/1.00 ( ( member_b @ B2 @ ( insert_b @ A @ bot_bot_set_b ) )
% 1.15/1.00 = ( B2 = A ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_66_singletonD,axiom,
% 1.15/1.00 ! [B2: b,A: b] :
% 1.15/1.00 ( ( member_b @ B2 @ ( insert_b @ A @ bot_bot_set_b ) )
% 1.15/1.00 => ( B2 = A ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_67_Collect__conv__if,axiom,
% 1.15/1.00 ! [P: b > $o,A: b] :
% 1.15/1.00 ( ( ( P @ A )
% 1.15/1.00 => ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( X4 = A )
% 1.15/1.00 & ( P @ X4 ) ) )
% 1.15/1.00 = ( insert_b @ A @ bot_bot_set_b ) ) )
% 1.15/1.00 & ( ~ ( P @ A )
% 1.15/1.00 => ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( X4 = A )
% 1.15/1.00 & ( P @ X4 ) ) )
% 1.15/1.00 = bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_68_Collect__conv__if2,axiom,
% 1.15/1.00 ! [P: b > $o,A: b] :
% 1.15/1.00 ( ( ( P @ A )
% 1.15/1.00 => ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( A = X4 )
% 1.15/1.00 & ( P @ X4 ) ) )
% 1.15/1.00 = ( insert_b @ A @ bot_bot_set_b ) ) )
% 1.15/1.00 & ( ~ ( P @ A )
% 1.15/1.00 => ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( A = X4 )
% 1.15/1.00 & ( P @ X4 ) ) )
% 1.15/1.00 = bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_69_is__singleton__def,axiom,
% 1.15/1.00 ( is_singleton_b
% 1.15/1.00 = ( ^ [A3: set_b] :
% 1.15/1.00 ? [X4: b] :
% 1.15/1.00 ( A3
% 1.15/1.00 = ( insert_b @ X4 @ bot_bot_set_b ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_70_is__singletonE,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( is_singleton_b @ A2 )
% 1.15/1.00 => ~ ! [X: b] :
% 1.15/1.00 ( A2
% 1.15/1.00 != ( insert_b @ X @ bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_71_is__singleton__the__elem,axiom,
% 1.15/1.00 ( is_singleton_b
% 1.15/1.00 = ( ^ [A3: set_b] :
% 1.15/1.00 ( A3
% 1.15/1.00 = ( insert_b @ ( the_elem_b @ A3 ) @ bot_bot_set_b ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_72_the__elem__eq,axiom,
% 1.15/1.00 ! [X2: b] :
% 1.15/1.00 ( ( the_elem_b @ ( insert_b @ X2 @ bot_bot_set_b ) )
% 1.15/1.00 = X2 ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_73_image__eqI,axiom,
% 1.15/1.00 ! [B2: b,F: b > b,X2: b,A2: set_b] :
% 1.15/1.00 ( ( B2
% 1.15/1.00 = ( F @ X2 ) )
% 1.15/1.00 => ( ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( member_b @ B2 @ ( image_b_b @ F @ A2 ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_74_image__is__empty,axiom,
% 1.15/1.00 ! [F: b > b,A2: set_b] :
% 1.15/1.00 ( ( ( image_b_b @ F @ A2 )
% 1.15/1.00 = bot_bot_set_b )
% 1.15/1.00 = ( A2 = bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_75_empty__is__image,axiom,
% 1.15/1.00 ! [F: b > b,A2: set_b] :
% 1.15/1.00 ( ( bot_bot_set_b
% 1.15/1.00 = ( image_b_b @ F @ A2 ) )
% 1.15/1.00 = ( A2 = bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_76_image__empty,axiom,
% 1.15/1.00 ! [F: b > b] :
% 1.15/1.00 ( ( image_b_b @ F @ bot_bot_set_b )
% 1.15/1.00 = bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_77_imageE,axiom,
% 1.15/1.00 ! [B2: b,F: b > b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ B2 @ ( image_b_b @ F @ A2 ) )
% 1.15/1.00 => ~ ! [X: b] :
% 1.15/1.00 ( ( B2
% 1.15/1.00 = ( F @ X ) )
% 1.15/1.00 => ~ ( member_b @ X @ A2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_78_imageI,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b,F: b > b] :
% 1.15/1.00 ( ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( member_b @ ( F @ X2 ) @ ( image_b_b @ F @ A2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_79_rev__image__eqI,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b,B2: b,F: b > b] :
% 1.15/1.00 ( ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( ( B2
% 1.15/1.00 = ( F @ X2 ) )
% 1.15/1.00 => ( member_b @ B2 @ ( image_b_b @ F @ A2 ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_80_Compr__image__eq,axiom,
% 1.15/1.00 ! [F: b > b,A2: set_b,P: b > $o] :
% 1.15/1.00 ( ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( member_b @ X4 @ ( image_b_b @ F @ A2 ) )
% 1.15/1.00 & ( P @ X4 ) ) )
% 1.15/1.00 = ( image_b_b @ F
% 1.15/1.00 @ ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( member_b @ X4 @ A2 )
% 1.15/1.00 & ( P @ ( F @ X4 ) ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_81_inv__into__into,axiom,
% 1.15/1.00 ! [X2: b,F: b > b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ X2 @ ( image_b_b @ F @ A2 ) )
% 1.15/1.00 => ( member_b @ ( hilbert_inv_into_b_b @ A2 @ F @ X2 ) @ A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_82_image__constant,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b,C: b] :
% 1.15/1.00 ( ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( ( image_b_b
% 1.15/1.00 @ ^ [X4: b] : C
% 1.15/1.00 @ A2 )
% 1.15/1.00 = ( insert_b @ C @ bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_83_image__constant__conv,axiom,
% 1.15/1.00 ! [A2: set_b,C: b] :
% 1.15/1.00 ( ( ( A2 = bot_bot_set_b )
% 1.15/1.00 => ( ( image_b_b
% 1.15/1.00 @ ^ [X4: b] : C
% 1.15/1.00 @ A2 )
% 1.15/1.00 = bot_bot_set_b ) )
% 1.15/1.00 & ( ( A2 != bot_bot_set_b )
% 1.15/1.00 => ( ( image_b_b
% 1.15/1.00 @ ^ [X4: b] : C
% 1.15/1.00 @ A2 )
% 1.15/1.00 = ( insert_b @ C @ bot_bot_set_b ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_84_bij__betw__empty2,axiom,
% 1.15/1.00 ! [F: b > b,A2: set_b] :
% 1.15/1.00 ( ( bij_betw_b_b @ F @ A2 @ bot_bot_set_b )
% 1.15/1.00 => ( A2 = bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_85_bij__betw__empty1,axiom,
% 1.15/1.00 ! [F: b > b,A2: set_b] :
% 1.15/1.00 ( ( bij_betw_b_b @ F @ bot_bot_set_b @ A2 )
% 1.15/1.00 => ( A2 = bot_bot_set_b ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_86_inj__singleton,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( inj_on_b_set_b
% 1.15/1.00 @ ^ [X4: b] : ( insert_b @ X4 @ bot_bot_set_b )
% 1.15/1.00 @ A2 ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_87_inj__img__insertE,axiom,
% 1.15/1.00 ! [F: b > b,A2: set_b,X2: b,B: set_b] :
% 1.15/1.00 ( ( inj_on_b_b @ F @ A2 )
% 1.15/1.00 => ( ~ ( member_b @ X2 @ B )
% 1.15/1.00 => ( ( ( insert_b @ X2 @ B )
% 1.15/1.00 = ( image_b_b @ F @ A2 ) )
% 1.15/1.00 => ~ ! [X6: b,A5: set_b] :
% 1.15/1.00 ( ~ ( member_b @ X6 @ A5 )
% 1.15/1.00 => ( ( A2
% 1.15/1.00 = ( insert_b @ X6 @ A5 ) )
% 1.15/1.00 => ( ( X2
% 1.15/1.00 = ( F @ X6 ) )
% 1.15/1.00 => ( B
% 1.15/1.00 != ( image_b_b @ F @ A5 ) ) ) ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_88_inj__image__mem__iff,axiom,
% 1.15/1.00 ! [F: b > b,A: b,A2: set_b] :
% 1.15/1.00 ( ( inj_on_b_b @ F @ top_top_set_b )
% 1.15/1.00 => ( ( member_b @ ( F @ A ) @ ( image_b_b @ F @ A2 ) )
% 1.15/1.00 = ( member_b @ A @ A2 ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_89_inj__on__insert,axiom,
% 1.15/1.00 ! [F: b > b,A: b,A2: set_b] :
% 1.15/1.00 ( ( inj_on_b_b @ F @ ( insert_b @ A @ A2 ) )
% 1.15/1.00 = ( ( inj_on_b_b @ F @ A2 )
% 1.15/1.00 & ~ ( member_b @ ( F @ A ) @ ( image_b_b @ F @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_90_DiffI,axiom,
% 1.15/1.00 ! [C: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ( member_b @ C @ A2 )
% 1.15/1.00 => ( ~ ( member_b @ C @ B )
% 1.15/1.00 => ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_91_Diff__iff,axiom,
% 1.15/1.00 ! [C: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 1.15/1.00 = ( ( member_b @ C @ A2 )
% 1.15/1.00 & ~ ( member_b @ C @ B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_92_Diff__empty,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( minus_minus_set_b @ A2 @ bot_bot_set_b )
% 1.15/1.00 = A2 ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_93_empty__Diff,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( minus_minus_set_b @ bot_bot_set_b @ A2 )
% 1.15/1.00 = bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_94_Diff__cancel,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( minus_minus_set_b @ A2 @ A2 )
% 1.15/1.00 = bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_95_insert__Diff1,axiom,
% 1.15/1.00 ! [X2: b,B: set_b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ X2 @ B )
% 1.15/1.00 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ B )
% 1.15/1.00 = ( minus_minus_set_b @ A2 @ B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_96_Diff__insert0,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ~ ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( ( minus_minus_set_b @ A2 @ ( insert_b @ X2 @ B ) )
% 1.15/1.00 = ( minus_minus_set_b @ A2 @ B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_97_insert__Diff__single,axiom,
% 1.15/1.00 ! [A: b,A2: set_b] :
% 1.15/1.00 ( ( insert_b @ A @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) )
% 1.15/1.00 = ( insert_b @ A @ A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_98_Diff__UNIV,axiom,
% 1.15/1.00 ! [A2: set_b] :
% 1.15/1.00 ( ( minus_minus_set_b @ A2 @ top_top_set_b )
% 1.15/1.00 = bot_bot_set_b ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_99_Diff__insert__absorb,axiom,
% 1.15/1.00 ! [X2: b,A2: set_b] :
% 1.15/1.00 ( ~ ( member_b @ X2 @ A2 )
% 1.15/1.00 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ ( insert_b @ X2 @ bot_bot_set_b ) )
% 1.15/1.00 = A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_100_Diff__insert2,axiom,
% 1.15/1.00 ! [A2: set_b,A: b,B: set_b] :
% 1.15/1.00 ( ( minus_minus_set_b @ A2 @ ( insert_b @ A @ B ) )
% 1.15/1.00 = ( minus_minus_set_b @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) @ B ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_101_insert__Diff,axiom,
% 1.15/1.00 ! [A: b,A2: set_b] :
% 1.15/1.00 ( ( member_b @ A @ A2 )
% 1.15/1.00 => ( ( insert_b @ A @ ( minus_minus_set_b @ A2 @ ( insert_b @ A @ bot_bot_set_b ) ) )
% 1.15/1.00 = A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_102_Diff__insert,axiom,
% 1.15/1.00 ! [A2: set_b,A: b,B: set_b] :
% 1.15/1.00 ( ( minus_minus_set_b @ A2 @ ( insert_b @ A @ B ) )
% 1.15/1.00 = ( minus_minus_set_b @ ( minus_minus_set_b @ A2 @ B ) @ ( insert_b @ A @ bot_bot_set_b ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_103_in__image__insert__iff,axiom,
% 1.15/1.00 ! [B: set_set_b,X2: b,A2: set_b] :
% 1.15/1.00 ( ! [C3: set_b] :
% 1.15/1.00 ( ( member_set_b @ C3 @ B )
% 1.15/1.00 => ~ ( member_b @ X2 @ C3 ) )
% 1.15/1.00 => ( ( member_set_b @ A2 @ ( image_set_b_set_b @ ( insert_b @ X2 ) @ B ) )
% 1.15/1.00 = ( ( member_b @ X2 @ A2 )
% 1.15/1.00 & ( member_set_b @ ( minus_minus_set_b @ A2 @ ( insert_b @ X2 @ bot_bot_set_b ) ) @ B ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_104_DiffE,axiom,
% 1.15/1.00 ! [C: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 1.15/1.00 => ~ ( ( member_b @ C @ A2 )
% 1.15/1.00 => ( member_b @ C @ B ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_105_DiffD1,axiom,
% 1.15/1.00 ! [C: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 1.15/1.00 => ( member_b @ C @ A2 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_106_DiffD2,axiom,
% 1.15/1.00 ! [C: b,A2: set_b,B: set_b] :
% 1.15/1.00 ( ( member_b @ C @ ( minus_minus_set_b @ A2 @ B ) )
% 1.15/1.00 => ~ ( member_b @ C @ B ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_107_set__diff__eq,axiom,
% 1.15/1.00 ( minus_minus_set_b
% 1.15/1.00 = ( ^ [A3: set_b,B4: set_b] :
% 1.15/1.00 ( collect_b
% 1.15/1.00 @ ^ [X4: b] :
% 1.15/1.00 ( ( member_b @ X4 @ A3 )
% 1.15/1.00 & ~ ( member_b @ X4 @ B4 ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_108_insert__Diff__if,axiom,
% 1.15/1.00 ! [X2: b,B: set_b,A2: set_b] :
% 1.15/1.00 ( ( ( member_b @ X2 @ B )
% 1.15/1.00 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ B )
% 1.15/1.00 = ( minus_minus_set_b @ A2 @ B ) ) )
% 1.15/1.00 & ( ~ ( member_b @ X2 @ B )
% 1.15/1.00 => ( ( minus_minus_set_b @ ( insert_b @ X2 @ A2 ) @ B )
% 1.15/1.00 = ( insert_b @ X2 @ ( minus_minus_set_b @ A2 @ B ) ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(fact_109_remove__def,axiom,
% 1.15/1.00 ( remove_b
% 1.15/1.00 = ( ^ [X4: b,A3: set_b] : ( minus_minus_set_b @ A3 @ ( insert_b @ X4 @ bot_bot_set_b ) ) ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(conj_0,hypothesis,
% 1.15/1.00 ! [X5: a] :
% 1.15/1.00 ( ( p @ X5 )
% 1.15/1.00 => ? [X_12: b] : ( q @ X5 @ X_12 ) ) ).
% 1.15/1.00
% 1.15/1.00 thf(conj_1,conjecture,
% 1.15/1.00 ! [X: a] :
% 1.15/1.00 ( ~ ( p @ X )
% 1.15/1.00 | ( q @ X @ ( hilbert_Eps_b @ ( q @ X ) ) ) ) ).
% 1.15/1.00 ------------------------
% 1.15/1.01 % (6195)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_5930 for (2999ds/183Mi)
% 1.15/1.01 % (6196)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_5930 for (2999ds/4Mi)
% 1.15/1.01 % (6197)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_5930 for (2999ds/27Mi)
% 1.15/1.01 % (6198)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_5930 for (2999ds/2Mi)
% 1.15/1.01 % (6199)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_5930 for (2999ds/2Mi)
% 1.15/1.01 % (6200)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_5930 for (2999ds/275Mi)
% 1.15/1.01 % (6201)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_5930 for (2999ds/18Mi)
% 1.15/1.01 % (6196)Instruction limit reached!
% 1.15/1.01 % (6196)------------------------------
% 1.15/1.01 % (6196)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.15/1.01 % (6196)Termination reason: Unknown
% 1.15/1.01 % (6196)Termination phase: shuffling
% 1.15/1.01
% 1.15/1.01 % (6196)Memory used [KB]: 1151
% 1.15/1.01 % (6196)Time elapsed: 0.002 s
% 1.15/1.01 % (6196)Instructions burned: 4 (million)
% 1.15/1.01 % (6198)Instruction limit reached!
% 1.15/1.01 % (6198)------------------------------
% 1.15/1.01 % (6198)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.15/1.01 % (6196)------------------------------
% 1.15/1.01 % (6196)------------------------------
% 1.15/1.01 % (6198)Termination reason: Unknown
% 1.37/1.01 % (6198)Termination phase: shuffling
% 1.37/1.01 % (6199)Instruction limit reached!
% 1.37/1.01 % (6199)------------------------------
% 1.37/1.01 % (6199)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.01 % (6199)Termination reason: Unknown
% 1.37/1.01 % (6199)Termination phase: shuffling
% 1.37/1.01
% 1.37/1.01 % (6199)Memory used [KB]: 1151
% 1.37/1.01 % (6199)Time elapsed: 0.002 s
% 1.37/1.01 % (6199)Instructions burned: 4 (million)
% 1.37/1.01 % (6199)------------------------------
% 1.37/1.01 % (6199)------------------------------
% 1.37/1.01
% 1.37/1.01 % (6198)Memory used [KB]: 1151
% 1.37/1.01 % (6198)Time elapsed: 0.002 s
% 1.37/1.01 % (6198)Instructions burned: 3 (million)
% 1.37/1.01 % (6198)------------------------------
% 1.37/1.01 % (6198)------------------------------
% 1.37/1.02 % (6201)Instruction limit reached!
% 1.37/1.02 % (6201)------------------------------
% 1.37/1.02 % (6201)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.02 % (6201)Termination reason: Unknown
% 1.37/1.02 % (6201)Termination phase: Property scanning
% 1.37/1.02
% 1.37/1.02 % (6201)Memory used [KB]: 1407
% 1.37/1.02 % (6201)Time elapsed: 0.007 s
% 1.37/1.02 % (6201)Instructions burned: 21 (million)
% 1.37/1.02 % (6201)------------------------------
% 1.37/1.02 % (6201)------------------------------
% 1.37/1.02 % (6200)First to succeed.
% 1.37/1.02 % (6197)Instruction limit reached!
% 1.37/1.02 % (6197)------------------------------
% 1.37/1.02 % (6197)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.02 % (6197)Termination reason: Unknown
% 1.37/1.02 % (6197)Termination phase: Property scanning
% 1.37/1.02
% 1.37/1.02 % (6197)Memory used [KB]: 1407
% 1.37/1.02 % (6197)Time elapsed: 0.009 s
% 1.37/1.02 % (6197)Instructions burned: 29 (million)
% 1.37/1.02 % (6197)------------------------------
% 1.37/1.02 % (6197)------------------------------
% 1.37/1.02 % (6200)Refutation found. Thanks to Tanya!
% 1.37/1.02 % SZS status Theorem for DTF2THF_5930
% 1.37/1.02 % SZS output start Proof for DTF2THF_5930
% 1.37/1.02 thf(type_def_5, type, b: $tType).
% 1.37/1.02 thf(type_def_7, type, set_b: $tType).
% 1.37/1.02 thf(type_def_8, type, set_set_b: $tType).
% 1.37/1.02 thf(type_def_9, type, a: $tType).
% 1.37/1.02 thf(func_def_0, type, set_set_b: $tType).
% 1.37/1.02 thf(func_def_1, type, set_b: $tType).
% 1.37/1.02 thf(func_def_2, type, b: $tType).
% 1.37/1.02 thf(func_def_3, type, a: $tType).
% 1.37/1.02 thf(func_def_4, type, bij_betw_b_b: (b > b) > set_b > set_b > $o).
% 1.37/1.02 thf(func_def_5, type, inj_on_b_set_b: (b > set_b) > set_b > $o).
% 1.37/1.02 thf(func_def_6, type, inj_on_b_b: (b > b) > set_b > $o).
% 1.37/1.02 thf(func_def_7, type, minus_minus_set_b: set_b > set_b > set_b).
% 1.37/1.02 thf(func_def_8, type, hilbert_Eps_b: (b > $o) > b).
% 1.37/1.02 thf(func_def_9, type, hilbert_inv_into_b_b: set_b > (b > b) > b > b).
% 1.37/1.02 thf(func_def_10, type, bot_bot_b_o: b > $o).
% 1.37/1.02 thf(func_def_11, type, bot_bot_set_b: set_b).
% 1.37/1.02 thf(func_def_12, type, top_top_b_o: b > $o).
% 1.37/1.02 thf(func_def_13, type, top_top_set_b: set_b).
% 1.37/1.02 thf(func_def_14, type, collect_b: (b > $o) > set_b).
% 1.37/1.02 thf(func_def_15, type, image_set_b_set_b: (set_b > set_b) > set_set_b > set_set_b).
% 1.37/1.02 thf(func_def_16, type, image_b_b: (b > b) > set_b > set_b).
% 1.37/1.02 thf(func_def_17, type, insert_b: b > set_b > set_b).
% 1.37/1.02 thf(func_def_18, type, is_empty_b: set_b > $o).
% 1.37/1.02 thf(func_def_19, type, is_singleton_b: set_b > $o).
% 1.37/1.02 thf(func_def_20, type, remove_b: b > set_b > set_b).
% 1.37/1.02 thf(func_def_21, type, the_elem_b: set_b > b).
% 1.37/1.02 thf(func_def_22, type, member_set_b: set_b > set_set_b > $o).
% 1.37/1.02 thf(func_def_23, type, member_b: b > set_b > $o).
% 1.37/1.02 thf(func_def_24, type, p: a > $o).
% 1.37/1.02 thf(func_def_25, type, q: a > b > $o).
% 1.37/1.02 thf(func_def_39, type, sK0: (b > $o) > b).
% 1.37/1.02 thf(func_def_40, type, sK1: (b > $o) > b).
% 1.37/1.02 thf(func_def_41, type, sK2: a > b).
% 1.37/1.02 thf(func_def_42, type, sK3: b > (b > $o) > b).
% 1.37/1.02 thf(func_def_43, type, sK4: b > (b > $o) > b).
% 1.37/1.02 thf(func_def_44, type, sK5: (b > $o) > (b > $o) > b).
% 1.37/1.02 thf(func_def_45, type, sK6: (b > $o) > b).
% 1.37/1.02 thf(func_def_46, type, sK7: (b > $o) > (b > $o) > b).
% 1.37/1.02 thf(func_def_47, type, sK8: (b > $o) > (b > $o) > b).
% 1.37/1.02 thf(func_def_48, type, sK9: (b > $o) > (b > $o) > b).
% 1.37/1.02 thf(func_def_49, type, sK10: a).
% 1.37/1.02 thf(func_def_50, type, sK11: (b > $o) > b).
% 1.37/1.02 thf(func_def_52, type, ph13: !>[X0: $tType]:(X0)).
% 1.37/1.02 thf(f481,plain,(
% 1.37/1.02 $false),
% 1.37/1.02 inference(subsumption_resolution,[status(thm)],[f459,f389])).
% 1.37/1.02 thf(f389,plain,(
% 1.37/1.02 ($true = (p @ sK10))),
% 1.37/1.02 inference(cnf_transformation,[status(thm)],[f362])).
% 1.37/1.02 thf(f362,plain,(
% 1.37/1.02 ((q @ sK10 @ (hilbert_Eps_b @ (q @ sK10))) != $true) & ($true = (p @ sK10))),
% 1.37/1.02 inference(skolemisation,[status(esa),new_symbols(skolem,[sK10])],[f322,f361])).
% 1.37/1.02 thf(f361,plain,(
% 1.37/1.02 ? [X0 : a] : (($true != (q @ X0 @ (hilbert_Eps_b @ (q @ X0)))) & ($true = (p @ X0))) => (((q @ sK10 @ (hilbert_Eps_b @ (q @ sK10))) != $true) & ($true = (p @ sK10)))),
% 1.37/1.02 introduced(definition,[],[choice_axiom])).
% 1.37/1.02 thf(f322,plain,(
% 1.37/1.02 ? [X0 : a] : (($true != (q @ X0 @ (hilbert_Eps_b @ (q @ X0)))) & ($true = (p @ X0)))),
% 1.37/1.02 inference(ennf_transformation,[status(thm)],[f308])).
% 1.37/1.02 thf(f308,plain,(
% 1.37/1.02 ~! [X0 : a] : (($true = (q @ X0 @ (hilbert_Eps_b @ (q @ X0)))) | ($true != (p @ X0)))),
% 1.37/1.02 inference(flattening,[status(thm)],[f168])).
% 1.37/1.02 thf(f168,plain,(
% 1.37/1.02 ~! [X0 : a] : (($true = (q @ X0 @ (hilbert_Eps_b @ (q @ X0)))) | ~($true = (p @ X0)))),
% 1.37/1.02 inference(fool_elimination,[status(thm)],[f167])).
% 1.37/1.02 thf(f167,plain,(
% 1.37/1.02 ~! [X0 : a] : ((q @ X0 @ (hilbert_Eps_b @ (q @ X0))) | ~(p @ X0))),
% 1.37/1.02 inference(rectify,[status(thm)],[f113])).
% 1.37/1.02 thf(f113,negated_conjecture,(
% 1.37/1.02 ~! [X2 : a] : ((q @ X2 @ (hilbert_Eps_b @ (q @ X2))) | ~(p @ X2))),
% 1.37/1.02 inference(negated_conjecture,[status(cth)],[f112])).
% 1.37/1.02 thf(f112,conjecture,(
% 1.37/1.02 ! [X2 : a] : ((q @ X2 @ (hilbert_Eps_b @ (q @ X2))) | ~(p @ X2))),
% 1.37/1.02 file('/export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2THF_5930.p',conj_1)).
% 1.37/1.02 thf(f459,plain,(
% 1.37/1.02 ($true != (p @ sK10))),
% 1.37/1.02 inference(trivial_inequality_removal,[status(thm)],[f438])).
% 1.37/1.02 thf(f438,plain,(
% 1.37/1.02 ($true != (p @ sK10)) | ($true != $true)),
% 1.37/1.02 inference(superposition,[status(thm)],[f433,f372])).
% 1.37/1.02 thf(f372,plain,(
% 1.37/1.02 ( ! [X0 : a] : (($true = (q @ X0 @ (sK2 @ X0))) | ($true != (p @ X0))) )),
% 1.37/1.02 inference(cnf_transformation,[status(thm)],[f345])).
% 1.37/1.02 thf(f345,plain,(
% 1.37/1.02 ! [X0 : a] : (($true = (q @ X0 @ (sK2 @ X0))) | ($true != (p @ X0)))),
% 1.37/1.02 inference(skolemisation,[status(esa),new_symbols(skolem,[sK2])],[f330,f344])).
% 1.37/1.02 thf(f344,plain,(
% 1.37/1.02 ! [X0 : a] : (? [X1 : b] : ($true = (q @ X0 @ X1)) => ($true = (q @ X0 @ (sK2 @ X0))))),
% 1.37/1.02 introduced(definition,[],[choice_axiom])).
% 1.37/1.02 thf(f330,plain,(
% 1.37/1.02 ! [X0 : a] : (? [X1 : b] : ($true = (q @ X0 @ X1)) | ($true != (p @ X0)))),
% 1.37/1.02 inference(ennf_transformation,[status(thm)],[f201])).
% 1.37/1.02 thf(f201,plain,(
% 1.37/1.02 ! [X0 : a] : (($true = (p @ X0)) => ? [X1 : b] : ($true = (q @ X0 @ X1)))),
% 1.37/1.02 inference(fool_elimination,[status(thm)],[f200])).
% 1.37/1.02 thf(f200,plain,(
% 1.37/1.02 ! [X0 : a] : ((p @ X0) => ? [X1 : b] : (q @ X0 @ X1))),
% 1.37/1.02 inference(rectify,[status(thm)],[f111])).
% 1.37/1.02 thf(f111,axiom,(
% 1.37/1.02 ! [X15 : a] : ((p @ X15) => ? [X33 : b] : (q @ X15 @ X33))),
% 1.37/1.02 file('/export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2THF_5930.p',conj_0)).
% 1.37/1.02 thf(f433,plain,(
% 1.37/1.02 ( ! [X0 : b] : (($true != (q @ sK10 @ X0))) )),
% 1.37/1.02 inference(trivial_inequality_removal,[status(thm)],[f416])).
% 1.37/1.02 thf(f416,plain,(
% 1.37/1.02 ( ! [X0 : b] : (($true != (q @ sK10 @ X0)) | ($true != $true)) )),
% 1.37/1.02 inference(superposition,[status(thm)],[f390,f398])).
% 1.37/1.02 thf(f398,plain,(
% 1.37/1.02 ( ! [X2 : b,X0 : b > $o] : (((X0 @ (hilbert_Eps_b @ X0)) = $true) | ((X0 @ X2) != $true)) )),
% 1.37/1.02 inference(equality_resolution,[status(thm)],[f371])).
% 1.37/1.02 thf(f371,plain,(
% 1.37/1.02 ( ! [X2 : b,X0 : b > $o,X1 : b] : (((X0 @ X1) = $true) | ((X0 @ X2) != $true) | ((hilbert_Eps_b @ X0) != X1)) )),
% 1.37/1.02 inference(cnf_transformation,[status(thm)],[f343])).
% 1.37/1.02 thf(f343,plain,(
% 1.37/1.02 ! [X0 : b > $o,X1 : b] : (((((X0 @ X1) = $true) | ! [X2 : b] : ((X0 @ X2) != $true)) & (($true = (X0 @ (sK1 @ X0))) | ((X0 @ X1) != $true))) | ((hilbert_Eps_b @ X0) != X1))),
% 1.37/1.02 inference(skolemisation,[status(esa),new_symbols(skolem,[sK1])],[f341,f342])).
% 1.37/1.02 thf(f342,plain,(
% 1.37/1.02 ! [X0 : b > $o] : (? [X3 : b] : ((X0 @ X3) = $true) => ($true = (X0 @ (sK1 @ X0))))),
% 1.37/1.02 introduced(definition,[],[choice_axiom])).
% 1.37/1.02 thf(f341,plain,(
% 1.37/1.02 ! [X0 : b > $o,X1 : b] : (((((X0 @ X1) = $true) | ! [X2 : b] : ((X0 @ X2) != $true)) & (? [X3 : b] : ((X0 @ X3) = $true) | ((X0 @ X1) != $true))) | ((hilbert_Eps_b @ X0) != X1))),
% 1.37/1.02 inference(rectify,[status(thm)],[f340])).
% 1.37/1.02 thf(f340,plain,(
% 1.37/1.02 ! [X0 : b > $o,X1 : b] : (((((X0 @ X1) = $true) | ! [X2 : b] : ((X0 @ X2) != $true)) & (? [X2 : b] : ((X0 @ X2) = $true) | ((X0 @ X1) != $true))) | ((hilbert_Eps_b @ X0) != X1))),
% 1.37/1.02 inference(nnf_transformation,[status(thm)],[f313])).
% 1.37/1.02 thf(f313,plain,(
% 1.37/1.02 ! [X0 : b > $o,X1 : b] : ((((X0 @ X1) = $true) <=> ? [X2 : b] : ((X0 @ X2) = $true)) | ((hilbert_Eps_b @ X0) != X1))),
% 1.37/1.02 inference(ennf_transformation,[status(thm)],[f192])).
% 1.37/1.02 thf(f192,plain,(
% 1.37/1.02 ! [X0 : b > $o,X1 : b] : (((hilbert_Eps_b @ X0) = X1) => (((X0 @ X1) = $true) <=> ? [X2 : b] : ((X0 @ X2) = $true)))),
% 1.37/1.02 inference(fool_elimination,[status(thm)],[f191])).
% 1.37/1.02 thf(f191,plain,(
% 1.37/1.02 ! [X0 : b > $o,X1 : b] : (((hilbert_Eps_b @ X0) = X1) => ((X0 @ X1) = ? [X2 : b] : (X0 @ X2)))),
% 1.37/1.02 inference(rectify,[status(thm)],[f21])).
% 1.37/1.02 thf(f21,axiom,(
% 1.37/1.02 ! [X0 : b > $o,X3 : b] : (((hilbert_Eps_b @ X0) = X3) => ((X0 @ X3) = ? [X8 : b] : (X0 @ X8)))),
% 1.37/1.02 file('/export/starexec/sandbox/tmp/tmp.DWtPnDx5ZE/DTF2THF_5930.p',fact_20_verit__sko__ex__indirect)).
% 1.37/1.02 thf(f390,plain,(
% 1.37/1.02 ((q @ sK10 @ (hilbert_Eps_b @ (q @ sK10))) != $true)),
% 1.37/1.02 inference(cnf_transformation,[status(thm)],[f362])).
% 1.37/1.02 % SZS output end Proof for DTF2THF_5930
% 1.37/1.02 % (6200)------------------------------
% 1.37/1.02 % (6200)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.37/1.02 % (6200)Termination reason: Refutation
% 1.37/1.02
% 1.37/1.02 % (6200)Memory used [KB]: 5884
% 1.37/1.02 % (6200)Time elapsed: 0.009 s
% 1.37/1.02 % (6200)Instructions burned: 22 (million)
% 1.37/1.02 % (6200)------------------------------
% 1.37/1.02 % (6200)------------------------------
% 1.37/1.02 % (6194)Success in time 0.01 s
%------------------------------------------------------------------------------