%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP020^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 : n019.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:12 AM UTC 2026
% Result : Theorem 2.28s 1.66s
% Output : Refutation 2.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : ITP020^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.31 % Computer : n019.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.31 % CPULimit : 300
% 0.13/0.31 % WCLimit : 300
% 0.13/0.31 % DateTime : Tue Feb 24 08:22:09 EST 2026
% 0.13/0.31 % CPUTime :
% 0.13/0.31 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.42 ---- Original DTF file ---
% 0.17/0.42 thf(spec,logic,$$dhol).
% 0.17/0.42 %------------------------------------------------------------------------------
% 0.17/0.42 % File : ITP020^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.17/0.42 % Domain : Interactive Theorem Proving
% 0.17/0.42 % Problem : HOL4 syntactic export of thm_2Eutil__prob_2ENUM__2D__BIJ__INV.p, bushy mode
% 0.17/0.42 % Version : [BG+19] axioms.
% 0.17/0.42 % English :
% 0.17/0.42
% 0.17/0.42 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.17/0.42 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.17/0.42 % Source : [BG+19]
% 0.17/0.42 % Names : thm_2Eutil__prob_2ENUM__2D__BIJ__INV.p [Gau19]
% 0.17/0.42 % : HL409501^3.p [TPAP]
% 0.17/0.42
% 0.17/0.42 % Status : Theorem
% 0.17/0.42 % Rating : 0.33 v8.1.0, 0.25 v7.5.0
% 0.17/0.42 % Syntax : Number of formulae : 55 ( 7 unt; 16 typ; 0 def)
% 0.17/0.42 % Number of atoms : 95 ( 9 equ; 40 cnn)
% 0.17/0.42 % Maximal formula atoms : 8 ( 2 avg)
% 0.17/0.42 % Number of connectives : 301 ( 40 ~; 36 |; 29 &; 123 @)
% 0.17/0.42 % ( 45 <=>; 28 =>; 0 <=; 0 <~>)
% 0.17/0.42 % Maximal formula depth : 12 ( 7 avg)
% 0.17/0.42 % Number of types : 3 ( 2 usr)
% 0.17/0.42 % Number of type conns : 49 ( 49 >; 0 *; 0 +; 0 <<)
% 0.17/0.42 % Number of symbols : 16 ( 14 usr; 3 con; 0-5 aty)
% 0.17/0.42 % Number of variables : 116 ( 0 ^; 92 !; 16 ?; 116 :)
% 0.17/0.42 % ( 8 !>; 0 ?*; 0 @-; 0 @+)
% 0.17/0.42 % SPC : TH1_THM_EQU_NAR
% 0.17/0.42
% 0.17/0.42 % Comments :
% 0.17/0.42 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.17/0.42 %------------------------------------------------------------------------------
% 0.17/0.42 thf(tyop_2Emin_2Ebool,type,
% 0.17/0.42 tyop_2Emin_2Ebool: $tType ).
% 0.17/0.42
% 0.17/0.42 thf(tyop_2Emin_2Efun,type,
% 0.17/0.42 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 0.17/0.42
% 0.17/0.42 thf(tyop_2Enum_2Enum,type,
% 0.17/0.42 tyop_2Enum_2Enum: $tType ).
% 0.17/0.42
% 0.17/0.42 thf(tyop_2Epair_2Eprod,type,
% 0.17/0.42 tyop_2Epair_2Eprod: $tType > $tType > $tType ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2E_21,type,
% 0.17/0.42 c_2Ebool_2E_21:
% 0.17/0.42 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2E_2F_5C,type,
% 0.17/0.42 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Emin_2E_3D,type,
% 0.17/0.42 c_2Emin_2E_3D:
% 0.17/0.42 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Emin_2E_3D_3D_3E,type,
% 0.17/0.42 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2E_3F,type,
% 0.17/0.42 c_2Ebool_2E_3F:
% 0.17/0.42 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Epred__set_2EBIJ,type,
% 0.17/0.42 c_2Epred__set_2EBIJ:
% 0.17/0.42 !>[A_27a: $tType,A_27b: $tType] : ( ( A_27a > A_27b ) > ( A_27a > $o ) > ( A_27b > $o ) > $o ) ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Epred__set_2ECROSS,type,
% 0.17/0.42 c_2Epred__set_2ECROSS:
% 0.17/0.42 !>[A_27a: $tType,A_27b: $tType] : ( ( A_27a > $o ) > ( A_27b > $o ) > ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) > $o ) ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2EF,type,
% 0.17/0.42 c_2Ebool_2EF: $o ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2ET,type,
% 0.17/0.42 c_2Ebool_2ET: $o ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Epred__set_2EUNIV,type,
% 0.17/0.42 c_2Epred__set_2EUNIV:
% 0.17/0.42 !>[A_27a: $tType] : ( A_27a > $o ) ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2E_5C_2F,type,
% 0.17/0.42 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.17/0.42
% 0.17/0.42 thf(c_2Ebool_2E_7E,type,
% 0.17/0.42 c_2Ebool_2E_7E: $o > $o ).
% 0.17/0.42
% 0.17/0.42 thf(logicdef_2E_2F_5C,axiom,
% 0.17/0.42 ! [V0: $o,V1: $o] :
% 0.17/0.42 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.17/0.42 <=> ( V0
% 0.17/0.42 & V1 ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(logicdef_2E_5C_2F,axiom,
% 0.17/0.42 ! [V0: $o,V1: $o] :
% 0.17/0.42 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.17/0.42 <=> ( V0
% 0.17/0.42 | V1 ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(logicdef_2E_7E,axiom,
% 0.17/0.42 ! [V0: $o] :
% 0.17/0.42 ( ( c_2Ebool_2E_7E @ V0 )
% 0.17/0.42 <=> ( (~) @ V0 ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(logicdef_2E_3D_3D_3E,axiom,
% 0.17/0.42 ! [V0: $o,V1: $o] :
% 0.17/0.42 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.17/0.42 <=> ( V0
% 0.17/0.42 => V1 ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(logicdef_2E_3D,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 0.17/0.42 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 0.17/0.42 <=> ( V0 = V1 ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(quantdef_2E_21,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.17/0.42 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 0.17/0.42 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(quantdef_2E_3F,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.17/0.42 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 0.17/0.42 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ETRUTH,axiom,
% 0.17/0.42 c_2Ebool_2ET ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 0.17/0.42 ! [V0t1: $o,V1t2: $o] :
% 0.17/0.42 ( ( V0t1
% 0.17/0.42 => V1t2 )
% 0.17/0.42 => ( ( V1t2
% 0.17/0.42 => V0t1 )
% 0.17/0.42 => ( V0t1 = V1t2 ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EIMP__F,axiom,
% 0.17/0.42 ! [V0t: $o] :
% 0.17/0.42 ( ( V0t
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 => ( (~) @ V0t ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EF__IMP,axiom,
% 0.17/0.42 ! [V0t: $o] :
% 0.17/0.42 ( ( (~) @ V0t )
% 0.17/0.42 => ( V0t
% 0.17/0.42 => c_2Ebool_2EF ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 0.17/0.42 ! [V0t: $o] :
% 0.17/0.42 ( ( ( c_2Ebool_2ET
% 0.17/0.42 => V0t )
% 0.17/0.42 <=> V0t )
% 0.17/0.42 & ( ( V0t
% 0.17/0.42 => c_2Ebool_2ET )
% 0.17/0.42 <=> c_2Ebool_2ET )
% 0.17/0.42 & ( ( c_2Ebool_2EF
% 0.17/0.42 => V0t )
% 0.17/0.42 <=> c_2Ebool_2ET )
% 0.17/0.42 & ( ( V0t
% 0.17/0.42 => V0t )
% 0.17/0.42 <=> c_2Ebool_2ET )
% 0.17/0.42 & ( ( V0t
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 <=> ( (~) @ V0t ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 0.17/0.42 ( ! [V0t: $o] :
% 0.17/0.42 ( ( (~) @ ( (~) @ V0t ) )
% 0.17/0.42 <=> V0t )
% 0.17/0.42 & ( ( (~) @ c_2Ebool_2ET )
% 0.17/0.42 <=> c_2Ebool_2EF )
% 0.17/0.42 & ( ( (~) @ c_2Ebool_2EF )
% 0.17/0.42 <=> c_2Ebool_2ET ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 0.17/0.42 ( ( V0x = V1y )
% 0.17/0.42 <=> ( V1y = V0x ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 0.17/0.42 ! [V0t: $o] :
% 0.17/0.42 ( ( ( c_2Ebool_2ET = V0t )
% 0.17/0.42 <=> V0t )
% 0.17/0.42 & ( ( V0t = c_2Ebool_2ET )
% 0.17/0.42 <=> V0t )
% 0.17/0.42 & ( ( c_2Ebool_2EF = V0t )
% 0.17/0.42 <=> ( (~) @ V0t ) )
% 0.17/0.42 & ( ( V0t = c_2Ebool_2EF )
% 0.17/0.42 <=> ( (~) @ V0t ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ENOT__EXISTS__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: A_27a > $o] :
% 0.17/0.42 ( ( (~)
% 0.17/0.42 @ ? [V1x: A_27a] : ( V0P @ V1x ) )
% 0.17/0.42 <=> ! [V2x: A_27a] : ( (~) @ ( V0P @ V2x ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ELEFT__AND__FORALL__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: A_27a > $o,V1Q: $o] :
% 0.17/0.42 ( ( ! [V2x: A_27a] : ( V0P @ V2x )
% 0.17/0.42 & V1Q )
% 0.17/0.42 <=> ! [V3x: A_27a] :
% 0.17/0.42 ( ( V0P @ V3x )
% 0.17/0.42 & V1Q ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ERIGHT__AND__FORALL__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 0.17/0.42 ( ( V0P
% 0.17/0.42 & ! [V2x: A_27a] : ( V1Q @ V2x ) )
% 0.17/0.42 <=> ! [V3x: A_27a] :
% 0.17/0.42 ( V0P
% 0.17/0.42 & ( V1Q @ V3x ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ELEFT__OR__EXISTS__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: A_27a > $o,V1Q: $o] :
% 0.17/0.42 ( ( ? [V2x: A_27a] : ( V0P @ V2x )
% 0.17/0.42 | V1Q )
% 0.17/0.42 <=> ? [V3x: A_27a] :
% 0.17/0.42 ( ( V0P @ V3x )
% 0.17/0.42 | V1Q ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ERIGHT__OR__EXISTS__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 0.17/0.42 ( ( V0P
% 0.17/0.42 | ? [V2x: A_27a] : ( V1Q @ V2x ) )
% 0.17/0.42 <=> ? [V3x: A_27a] :
% 0.17/0.42 ( V0P
% 0.17/0.42 | ( V1Q @ V3x ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ELEFT__EXISTS__AND__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: A_27a > $o,V1Q: $o] :
% 0.17/0.42 ( ? [V2x: A_27a] :
% 0.17/0.42 ( ( V0P @ V2x )
% 0.17/0.42 & V1Q )
% 0.17/0.42 <=> ( ? [V3x: A_27a] : ( V0P @ V3x )
% 0.17/0.42 & V1Q ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ERIGHT__EXISTS__AND__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 0.17/0.42 ( ? [V2x: A_27a] :
% 0.17/0.42 ( V0P
% 0.17/0.42 & ( V1Q @ V2x ) )
% 0.17/0.42 <=> ( V0P
% 0.17/0.42 & ? [V3x: A_27a] : ( V1Q @ V3x ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ELEFT__FORALL__OR__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0Q: $o,V1P: A_27a > $o] :
% 0.17/0.42 ( ! [V2x: A_27a] :
% 0.17/0.42 ( ( V1P @ V2x )
% 0.17/0.42 | V0Q )
% 0.17/0.42 <=> ( ! [V3x: A_27a] : ( V1P @ V3x )
% 0.17/0.42 | V0Q ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ERIGHT__FORALL__OR__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 0.17/0.42 ( ! [V2x: A_27a] :
% 0.17/0.42 ( V0P
% 0.17/0.42 | ( V1Q @ V2x ) )
% 0.17/0.42 <=> ( V0P
% 0.17/0.42 | ! [V3x: A_27a] : ( V1Q @ V3x ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2EDISJ__SYM,axiom,
% 0.17/0.42 ! [V0A: $o,V1B: $o] :
% 0.17/0.42 ( ( V0A
% 0.17/0.42 | V1B )
% 0.17/0.42 <=> ( V1B
% 0.17/0.42 | V0A ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Ebool_2ESKOLEM__THM,axiom,
% 0.17/0.42 ! [A_27a: $tType,A_27b: $tType,V0P: A_27a > A_27b > $o] :
% 0.17/0.42 ( ! [V1x: A_27a] :
% 0.17/0.42 ? [V2y: A_27b] : ( V0P @ V1x @ V2y )
% 0.17/0.42 <=> ? [V3f: A_27a > A_27b] :
% 0.17/0.42 ! [V4x: A_27a] : ( V0P @ V4x @ ( V3f @ V4x ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Epred__set_2EBIJ__SYM,axiom,
% 0.17/0.42 ! [A_27a: $tType,A_27b: $tType,V0s: A_27a > $o,V1t: A_27b > $o] :
% 0.17/0.42 ( ? [V2f: A_27a > A_27b] : ( c_2Epred__set_2EBIJ @ A_27a @ A_27b @ V2f @ V0s @ V1t )
% 0.17/0.42 <=> ? [V3g: A_27b > A_27a] : ( c_2Epred__set_2EBIJ @ A_27b @ A_27a @ V3g @ V1t @ V0s ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2ENOT__NOT,axiom,
% 0.17/0.42 ! [V0t: $o] :
% 0.17/0.42 ( ( (~) @ ( (~) @ V0t ) )
% 0.17/0.42 <=> V0t ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 0.17/0.42 ! [V0A: $o] :
% 0.17/0.42 ( V0A
% 0.17/0.42 => ( ( (~) @ V0A )
% 0.17/0.42 => c_2Ebool_2EF ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 0.17/0.42 ! [V0B: $o,V1A: $o] :
% 0.17/0.42 ( ( ( (~)
% 0.17/0.42 @ ( V1A
% 0.17/0.42 | V0B ) )
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 <=> ( ( V1A
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 => ( ( (~) @ V0B )
% 0.17/0.42 => c_2Ebool_2EF ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 0.17/0.42 ! [V0B: $o,V1A: $o] :
% 0.17/0.42 ( ( ( (~)
% 0.17/0.42 @ ( ( (~) @ V1A )
% 0.17/0.42 | V0B ) )
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 <=> ( V1A
% 0.17/0.42 => ( ( (~) @ V0B )
% 0.17/0.42 => c_2Ebool_2EF ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2EAND__INV2,axiom,
% 0.17/0.42 ! [V0A: $o] :
% 0.17/0.42 ( ( ( (~) @ V0A )
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 => ( ( V0A
% 0.17/0.42 => c_2Ebool_2EF )
% 0.17/0.42 => c_2Ebool_2EF ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2Edc__eq,axiom,
% 0.17/0.42 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.17/0.42 ( ( V2p
% 0.17/0.42 <=> ( V1q = V0r ) )
% 0.17/0.42 <=> ( ( V2p
% 0.17/0.42 | V1q
% 0.17/0.42 | V0r )
% 0.17/0.42 & ( V2p
% 0.17/0.42 | ( (~) @ V0r )
% 0.17/0.42 | ( (~) @ V1q ) )
% 0.17/0.42 & ( V1q
% 0.17/0.42 | ( (~) @ V0r )
% 0.17/0.42 | ( (~) @ V2p ) )
% 0.17/0.42 & ( V0r
% 0.17/0.42 | ( (~) @ V1q )
% 0.17/0.42 | ( (~) @ V2p ) ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2Edc__conj,axiom,
% 0.17/0.42 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.17/0.42 ( ( V2p
% 0.17/0.42 <=> ( V1q
% 0.17/0.42 & V0r ) )
% 0.17/0.42 <=> ( ( V2p
% 0.17/0.42 | ( (~) @ V1q )
% 0.17/0.42 | ( (~) @ V0r ) )
% 0.17/0.42 & ( V1q
% 0.17/0.42 | ( (~) @ V2p ) )
% 0.17/0.42 & ( V0r
% 0.17/0.42 | ( (~) @ V2p ) ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2Edc__disj,axiom,
% 0.17/0.42 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.17/0.42 ( ( V2p
% 0.17/0.42 <=> ( V1q
% 0.17/0.42 | V0r ) )
% 0.17/0.42 <=> ( ( V2p
% 0.17/0.42 | ( (~) @ V1q ) )
% 0.17/0.42 & ( V2p
% 0.17/0.42 | ( (~) @ V0r ) )
% 0.17/0.42 & ( V1q
% 0.17/0.42 | V0r
% 0.17/0.42 | ( (~) @ V2p ) ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2Edc__imp,axiom,
% 0.17/0.42 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.17/0.42 ( ( V2p
% 0.17/0.42 <=> ( V1q
% 0.17/0.42 => V0r ) )
% 0.17/0.42 <=> ( ( V2p
% 0.17/0.42 | V1q )
% 0.17/0.42 & ( V2p
% 0.17/0.42 | ( (~) @ V0r ) )
% 0.17/0.42 & ( ( (~) @ V1q )
% 0.17/0.42 | V0r
% 0.17/0.42 | ( (~) @ V2p ) ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Esat_2Edc__neg,axiom,
% 0.17/0.42 ! [V0q: $o,V1p: $o] :
% 0.17/0.42 ( ( V1p
% 0.17/0.42 <=> ( (~) @ V0q ) )
% 0.17/0.42 <=> ( ( V1p
% 0.17/0.42 | V0q )
% 0.17/0.42 & ( ( (~) @ V0q )
% 0.17/0.42 | ( (~) @ V1p ) ) ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Eutil__prob_2ENUM__2D__BIJ,axiom,
% 0.17/0.42 ? [V0f: ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) > tyop_2Enum_2Enum] : ( c_2Epred__set_2EBIJ @ ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ tyop_2Enum_2Enum @ V0f @ ( c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) ) ).
% 0.17/0.42
% 0.17/0.42 thf(thm_2Eutil__prob_2ENUM__2D__BIJ__INV,conjecture,
% 0.17/0.42 ? [V0f: tyop_2Enum_2Enum > ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum )] : ( c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ V0f @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) @ ( c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) ) ) ).
% 0.17/0.42
% 0.17/0.42 %------------------------------------------------------------------------------
% 0.17/0.42 ------------------------
% 2.28/1.61 ---- Embedded in THF ---
% 2.28/1.62 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 2.28/1.62 %%% Generated on Tue Feb 24 08:22:10 EST 2026
% 2.28/1.62 %%% using '$$dhol' embedding, version 1.3.0.
% 2.28/1.62 %%% Logic specification used:
% 2.28/1.62 %%% thf(spec, logic, $$dhol).
% 2.28/1.62
% 2.28/1.62 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.sh1aevIe5y/DTF2DTF20047.p
% 2.28/1.62 thf(tyop_2Emin_2Ebool, type, tyop_2Emin_2Ebool: $tType).
% 2.28/1.62 thf(tyop_2Emin_2Efun, type, tyop_2Emin_2Efun: ($tType > ($tType > $tType))).
% 2.28/1.62 thf(tyop_2Enum_2Enum, type, tyop_2Enum_2Enum: $tType).
% 2.28/1.62 thf(tyop_2Epair_2Eprod, type, tyop_2Epair_2Eprod: ($tType > ($tType > $tType))).
% 2.28/1.62 thf(c_2Ebool_2E_21, type, c_2Ebool_2E_21: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 2.28/1.62 thf(c_2Ebool_2E_2F_5C, type, c_2Ebool_2E_2F_5C: ($o > ($o > $o))).
% 2.28/1.62 thf(c_2Emin_2E_3D, type, c_2Emin_2E_3D: (!> [A_27a:$tType]: ((A_27a > (A_27a > $o))))).
% 2.28/1.62 thf(c_2Emin_2E_3D_3D_3E, type, c_2Emin_2E_3D_3D_3E: ($o > ($o > $o))).
% 2.28/1.62 thf(c_2Ebool_2E_3F, type, c_2Ebool_2E_3F: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 2.28/1.62 thf(c_2Epred__set_2EBIJ, type, c_2Epred__set_2EBIJ: (!> [A_27a:$tType,A_27b:$tType]: (((A_27a > A_27b) > ((A_27a > $o) > ((A_27b > $o) > $o)))))).
% 2.28/1.62 thf(c_2Epred__set_2ECROSS, type, c_2Epred__set_2ECROSS: (!> [A_27a:$tType,A_27b:$tType]: (((A_27a > $o) > ((A_27b > $o) > (((tyop_2Epair_2Eprod @ A_27a) @ A_27b) > $o)))))).
% 2.28/1.62 thf(c_2Ebool_2EF, type, c_2Ebool_2EF: $o).
% 2.28/1.62 thf(c_2Ebool_2ET, type, c_2Ebool_2ET: $o).
% 2.28/1.62 thf(c_2Epred__set_2EUNIV, type, c_2Epred__set_2EUNIV: (!> [A_27a:$tType]: ((A_27a > $o)))).
% 2.28/1.62 thf(c_2Ebool_2E_5C_2F, type, c_2Ebool_2E_5C_2F: ($o > ($o > $o))).
% 2.28/1.62 thf(c_2Ebool_2E_7E, type, c_2Ebool_2E_7E: ($o > $o)).
% 2.28/1.62 thf(logicdef_2E_2F_5C, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_2F_5C @ V0) @ V1) <=> (V0 & V1))))).
% 2.28/1.62 thf(logicdef_2E_5C_2F, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_5C_2F @ V0) @ V1) <=> (V0 | V1))))).
% 2.28/1.62 thf(logicdef_2E_7E, axiom, (! [V0:$o]: (((c_2Ebool_2E_7E @ V0) <=> ((~) @ V0))))).
% 2.28/1.62 thf(logicdef_2E_3D_3D_3E, axiom, (! [V0:$o,V1:$o]: ((((c_2Emin_2E_3D_3D_3E @ V0) @ V1) <=> (V0 => V1))))).
% 2.28/1.62 thf(logicdef_2E_3D, axiom, (! [A_27a:$tType,V0:A_27a,V1:A_27a]: (((((c_2Emin_2E_3D @ A_27a) @ V0) @ V1) <=> (V0 = V1))))).
% 2.28/1.62 thf(quantdef_2E_21, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_21 @ A_27a) @ V0f) <=> (! [V1x:A_27a]: ((V0f @ V1x))))))).
% 2.28/1.62 thf(quantdef_2E_3F, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_3F @ A_27a) @ V0f) <=> (? [V1x:A_27a]: ((V0f @ V1x))))))).
% 2.28/1.62 thf(thm_2Ebool_2ETRUTH, axiom, c_2Ebool_2ET).
% 2.28/1.62 thf(thm_2Ebool_2EIMP__ANTISYM__AX, axiom, (! [V0t1:$o,V1t2:$o]: (((V0t1 => V1t2) => ((V1t2 => V0t1) => (V0t1 = V1t2)))))).
% 2.28/1.62 thf(thm_2Ebool_2EIMP__F, axiom, (! [V0t:$o]: (((V0t => c_2Ebool_2EF) => ((~) @ V0t))))).
% 2.28/1.62 thf(thm_2Ebool_2EF__IMP, axiom, (! [V0t:$o]: ((((~) @ V0t) => (V0t => c_2Ebool_2EF))))).
% 2.28/1.62 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))))))))).
% 2.28/1.62 thf(thm_2Ebool_2ENOT__CLAUSES, axiom, ((! [V0t:$o]: ((((~) @ ((~) @ V0t)) <=> V0t))) & ((((~) @ c_2Ebool_2ET) <=> c_2Ebool_2EF) & (((~) @ c_2Ebool_2EF) <=> c_2Ebool_2ET)))).
% 2.28/1.62 thf(thm_2Ebool_2EEQ__SYM__EQ, axiom, (! [A_27a:$tType,V0x:A_27a,V1y:A_27a]: (((V0x = V1y) <=> (V1y = V0x))))).
% 2.28/1.62 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)))))))).
% 2.28/1.62 thf(thm_2Ebool_2ENOT__EXISTS__THM, axiom, (! [A_27a:$tType,V0P:(A_27a > $o)]: ((((~) @ (? [V1x:A_27a]: ((V0P @ V1x)))) <=> (! [V2x:A_27a]: (((~) @ (V0P @ V2x)))))))).
% 2.28/1.62 thf(thm_2Ebool_2ELEFT__AND__FORALL__THM, axiom, (! [A_27a:$tType,V0P:(A_27a > $o),V1Q:$o]: ((((! [V2x:A_27a]: ((V0P @ V2x))) & V1Q) <=> (! [V3x:A_27a]: (((V0P @ V3x) & V1Q))))))).
% 2.28/1.62 thf(thm_2Ebool_2ERIGHT__AND__FORALL__THM, axiom, (! [A_27a:$tType,V0P:$o,V1Q:(A_27a > $o)]: (((V0P & (! [V2x:A_27a]: ((V1Q @ V2x)))) <=> (! [V3x:A_27a]: ((V0P & (V1Q @ V3x)))))))).
% 2.28/1.62 thf(thm_2Ebool_2ELEFT__OR__EXISTS__THM, axiom, (! [A_27a:$tType,V0P:(A_27a > $o),V1Q:$o]: ((((? [V2x:A_27a]: ((V0P @ V2x))) | V1Q) <=> (? [V3x:A_27a]: (((V0P @ V3x) | V1Q))))))).
% 2.28/1.62 thf(thm_2Ebool_2ERIGHT__OR__EXISTS__THM, axiom, (! [A_27a:$tType,V0P:$o,V1Q:(A_27a > $o)]: (((V0P | (? [V2x:A_27a]: ((V1Q @ V2x)))) <=> (? [V3x:A_27a]: ((V0P | (V1Q @ V3x)))))))).
% 2.28/1.62 thf(thm_2Ebool_2ELEFT__EXISTS__AND__THM, axiom, (! [A_27a:$tType,V0P:(A_27a > $o),V1Q:$o]: (((? [V2x:A_27a]: (((V0P @ V2x) & V1Q))) <=> ((? [V3x:A_27a]: ((V0P @ V3x))) & V1Q))))).
% 2.28/1.62 thf(thm_2Ebool_2ERIGHT__EXISTS__AND__THM, axiom, (! [A_27a:$tType,V0P:$o,V1Q:(A_27a > $o)]: (((? [V2x:A_27a]: ((V0P & (V1Q @ V2x)))) <=> (V0P & (? [V3x:A_27a]: ((V1Q @ V3x)))))))).
% 2.28/1.62 thf(thm_2Ebool_2ELEFT__FORALL__OR__THM, axiom, (! [A_27a:$tType,V0Q:$o,V1P:(A_27a > $o)]: (((! [V2x:A_27a]: (((V1P @ V2x) | V0Q))) <=> ((! [V3x:A_27a]: ((V1P @ V3x))) | V0Q))))).
% 2.28/1.62 thf(thm_2Ebool_2ERIGHT__FORALL__OR__THM, axiom, (! [A_27a:$tType,V0P:$o,V1Q:(A_27a > $o)]: (((! [V2x:A_27a]: ((V0P | (V1Q @ V2x)))) <=> (V0P | (! [V3x:A_27a]: ((V1Q @ V3x)))))))).
% 2.28/1.62 thf(thm_2Ebool_2EDISJ__SYM, axiom, (! [V0A:$o,V1B:$o]: (((V0A | V1B) <=> (V1B | V0A))))).
% 2.28/1.62 thf(thm_2Ebool_2ESKOLEM__THM, axiom, (! [A_27a:$tType,A_27b:$tType,V0P:(A_27a > (A_27b > $o))]: (((! [V1x:A_27a]: ((? [V2y:A_27b]: (((V0P @ V1x) @ V2y))))) <=> (? [V3f:(A_27a > A_27b)]: ((! [V4x:A_27a]: (((V0P @ V4x) @ (V3f @ V4x)))))))))).
% 2.28/1.62 thf(thm_2Epred__set_2EBIJ__SYM, axiom, (! [A_27a:$tType,A_27b:$tType,V0s:(A_27a > $o),V1t:(A_27b > $o)]: (((? [V2f:(A_27a > A_27b)]: ((((((c_2Epred__set_2EBIJ @ A_27a) @ A_27b) @ V2f) @ V0s) @ V1t))) <=> (? [V3g:(A_27b > A_27a)]: ((((((c_2Epred__set_2EBIJ @ A_27b) @ A_27a) @ V3g) @ V1t) @ V0s))))))).
% 2.28/1.62 thf(thm_2Esat_2ENOT__NOT, axiom, (! [V0t:$o]: ((((~) @ ((~) @ V0t)) <=> V0t)))).
% 2.28/1.62 thf(thm_2Esat_2EAND__INV__IMP, axiom, (! [V0A:$o]: ((V0A => (((~) @ V0A) => c_2Ebool_2EF))))).
% 2.28/1.62 thf(thm_2Esat_2EOR__DUAL2, axiom, (! [V0B:$o,V1A:$o]: (((((~) @ (V1A | V0B)) => c_2Ebool_2EF) <=> ((V1A => c_2Ebool_2EF) => (((~) @ V0B) => c_2Ebool_2EF)))))).
% 2.28/1.62 thf(thm_2Esat_2EOR__DUAL3, axiom, (! [V0B:$o,V1A:$o]: (((((~) @ (((~) @ V1A) | V0B)) => c_2Ebool_2EF) <=> (V1A => (((~) @ V0B) => c_2Ebool_2EF)))))).
% 2.28/1.62 thf(thm_2Esat_2EAND__INV2, axiom, (! [V0A:$o]: (((((~) @ V0A) => c_2Ebool_2EF) => ((V0A => c_2Ebool_2EF) => c_2Ebool_2EF))))).
% 2.28/1.62 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)))))))))).
% 2.28/1.62 thf(thm_2Esat_2Edc__conj, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q & V0r)) <=> ((V2p | (((~) @ V1q) | ((~) @ V0r))) & ((V1q | ((~) @ V2p)) & (V0r | ((~) @ V2p)))))))).
% 2.28/1.62 thf(thm_2Esat_2Edc__disj, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q | V0r)) <=> ((V2p | ((~) @ V1q)) & ((V2p | ((~) @ V0r)) & (V1q | (V0r | ((~) @ V2p))))))))).
% 2.28/1.62 thf(thm_2Esat_2Edc__imp, axiom, (! [V0r:$o,V1q:$o,V2p:$o]: (((V2p <=> (V1q => V0r)) <=> ((V2p | V1q) & ((V2p | ((~) @ V0r)) & (((~) @ V1q) | (V0r | ((~) @ V2p))))))))).
% 2.28/1.62 thf(thm_2Esat_2Edc__neg, axiom, (! [V0q:$o,V1p:$o]: (((V1p <=> ((~) @ V0q)) <=> ((V1p | V0q) & (((~) @ V0q) | ((~) @ V1p))))))).
% 2.28/1.62 thf(thm_2Eutil__prob_2ENUM__2D__BIJ, axiom, (? [V0f:(((tyop_2Epair_2Eprod @ tyop_2Enum_2Enum) @ tyop_2Enum_2Enum) > tyop_2Enum_2Enum)]: ((((((c_2Epred__set_2EBIJ @ ((tyop_2Epair_2Eprod @ tyop_2Enum_2Enum) @ tyop_2Enum_2Enum)) @ tyop_2Enum_2Enum) @ V0f) @ ((((c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum) @ tyop_2Enum_2Enum) @ (c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)) @ (c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))) @ (c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))))).
% 2.28/1.62 thf(thm_2Eutil__prob_2ENUM__2D__BIJ__INV, conjecture, (? [V0f:(tyop_2Enum_2Enum > ((tyop_2Epair_2Eprod @ tyop_2Enum_2Enum) @ tyop_2Enum_2Enum))]: ((((((c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum) @ ((tyop_2Epair_2Eprod @ tyop_2Enum_2Enum) @ tyop_2Enum_2Enum)) @ V0f) @ (c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)) @ ((((c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum) @ tyop_2Enum_2Enum) @ (c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)) @ (c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)))))).
% 2.28/1.62 % SZS output end ListOfTHF for /export/starexec/sandbox/tmp/tmp.sh1aevIe5y/DTF2DTF20047.p
% 2.28/1.62 ------------------------
% 2.28/1.63 ---- Cleaned THF ---
% 2.28/1.63 thf(tyop_2Emin_2Ebool,type,
% 2.28/1.63 tyop_2Emin_2Ebool: $tType ).
% 2.28/1.63
% 2.28/1.63 thf(tyop_2Emin_2Efun,type,
% 2.28/1.63 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 2.28/1.63
% 2.28/1.63 thf(tyop_2Enum_2Enum,type,
% 2.28/1.63 tyop_2Enum_2Enum: $tType ).
% 2.28/1.63
% 2.28/1.63 thf(tyop_2Epair_2Eprod,type,
% 2.28/1.63 tyop_2Epair_2Eprod: $tType > $tType > $tType ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2E_21,type,
% 2.28/1.63 c_2Ebool_2E_21:
% 2.28/1.63 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2E_2F_5C,type,
% 2.28/1.63 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Emin_2E_3D,type,
% 2.28/1.63 c_2Emin_2E_3D:
% 2.28/1.63 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Emin_2E_3D_3D_3E,type,
% 2.28/1.63 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2E_3F,type,
% 2.28/1.63 c_2Ebool_2E_3F:
% 2.28/1.63 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Epred__set_2EBIJ,type,
% 2.28/1.63 c_2Epred__set_2EBIJ:
% 2.28/1.63 !>[A_27a: $tType,A_27b: $tType] : ( ( A_27a > A_27b ) > ( A_27a > $o ) > ( A_27b > $o ) > $o ) ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Epred__set_2ECROSS,type,
% 2.28/1.63 c_2Epred__set_2ECROSS:
% 2.28/1.63 !>[A_27a: $tType,A_27b: $tType] : ( ( A_27a > $o ) > ( A_27b > $o ) > ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) > $o ) ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2EF,type,
% 2.28/1.63 c_2Ebool_2EF: $o ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2ET,type,
% 2.28/1.63 c_2Ebool_2ET: $o ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Epred__set_2EUNIV,type,
% 2.28/1.63 c_2Epred__set_2EUNIV:
% 2.28/1.63 !>[A_27a: $tType] : ( A_27a > $o ) ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2E_5C_2F,type,
% 2.28/1.63 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 2.28/1.63
% 2.28/1.63 thf(c_2Ebool_2E_7E,type,
% 2.28/1.63 c_2Ebool_2E_7E: $o > $o ).
% 2.28/1.63
% 2.28/1.63 thf(logicdef_2E_2F_5C,axiom,
% 2.28/1.63 ! [V0: $o,V1: $o] :
% 2.28/1.63 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 2.28/1.63 <=> ( V0
% 2.28/1.63 & V1 ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(logicdef_2E_5C_2F,axiom,
% 2.28/1.63 ! [V0: $o,V1: $o] :
% 2.28/1.63 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 2.28/1.63 <=> ( V0
% 2.28/1.63 | V1 ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(logicdef_2E_7E,axiom,
% 2.28/1.63 ! [V0: $o] :
% 2.28/1.63 ( ( c_2Ebool_2E_7E @ V0 )
% 2.28/1.63 <=> ( (~) @ V0 ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(logicdef_2E_3D_3D_3E,axiom,
% 2.28/1.63 ! [V0: $o,V1: $o] :
% 2.28/1.63 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 2.28/1.63 <=> ( V0
% 2.28/1.63 => V1 ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(logicdef_2E_3D,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 2.28/1.63 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 2.28/1.63 <=> ( V0 = V1 ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(quantdef_2E_21,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0f: A_27a > $o] :
% 2.28/1.63 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 2.28/1.63 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(quantdef_2E_3F,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0f: A_27a > $o] :
% 2.28/1.63 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 2.28/1.63 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ETRUTH,axiom,
% 2.28/1.63 c_2Ebool_2ET ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 2.28/1.63 ! [V0t1: $o,V1t2: $o] :
% 2.28/1.63 ( ( V0t1
% 2.28/1.63 => V1t2 )
% 2.28/1.63 => ( ( V1t2
% 2.28/1.63 => V0t1 )
% 2.28/1.63 => ( V0t1 = V1t2 ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EIMP__F,axiom,
% 2.28/1.63 ! [V0t: $o] :
% 2.28/1.63 ( ( V0t
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 => ( (~) @ V0t ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EF__IMP,axiom,
% 2.28/1.63 ! [V0t: $o] :
% 2.28/1.63 ( ( (~) @ V0t )
% 2.28/1.63 => ( V0t
% 2.28/1.63 => c_2Ebool_2EF ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 2.28/1.63 ! [V0t: $o] :
% 2.28/1.63 ( ( ( c_2Ebool_2ET
% 2.28/1.63 => V0t )
% 2.28/1.63 <=> V0t )
% 2.28/1.63 & ( ( V0t
% 2.28/1.63 => c_2Ebool_2ET )
% 2.28/1.63 <=> c_2Ebool_2ET )
% 2.28/1.63 & ( ( c_2Ebool_2EF
% 2.28/1.63 => V0t )
% 2.28/1.63 <=> c_2Ebool_2ET )
% 2.28/1.63 & ( ( V0t
% 2.28/1.63 => V0t )
% 2.28/1.63 <=> c_2Ebool_2ET )
% 2.28/1.63 & ( ( V0t
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 <=> ( (~) @ V0t ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 2.28/1.63 ( ! [V0t: $o] :
% 2.28/1.63 ( ( (~) @ ( (~) @ V0t ) )
% 2.28/1.63 <=> V0t )
% 2.28/1.63 & ( ( (~) @ c_2Ebool_2ET )
% 2.28/1.63 <=> c_2Ebool_2EF )
% 2.28/1.63 & ( ( (~) @ c_2Ebool_2EF )
% 2.28/1.63 <=> c_2Ebool_2ET ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 2.28/1.63 ( ( V0x = V1y )
% 2.28/1.63 <=> ( V1y = V0x ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 2.28/1.63 ! [V0t: $o] :
% 2.28/1.63 ( ( ( c_2Ebool_2ET = V0t )
% 2.28/1.63 <=> V0t )
% 2.28/1.63 & ( ( V0t = c_2Ebool_2ET )
% 2.28/1.63 <=> V0t )
% 2.28/1.63 & ( ( c_2Ebool_2EF = V0t )
% 2.28/1.63 <=> ( (~) @ V0t ) )
% 2.28/1.63 & ( ( V0t = c_2Ebool_2EF )
% 2.28/1.63 <=> ( (~) @ V0t ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ENOT__EXISTS__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: A_27a > $o] :
% 2.28/1.63 ( ( (~)
% 2.28/1.63 @ ? [V1x: A_27a] : ( V0P @ V1x ) )
% 2.28/1.63 <=> ! [V2x: A_27a] : ( (~) @ ( V0P @ V2x ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ELEFT__AND__FORALL__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: A_27a > $o,V1Q: $o] :
% 2.28/1.63 ( ( ! [V2x: A_27a] : ( V0P @ V2x )
% 2.28/1.63 & V1Q )
% 2.28/1.63 <=> ! [V3x: A_27a] :
% 2.28/1.63 ( ( V0P @ V3x )
% 2.28/1.63 & V1Q ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ERIGHT__AND__FORALL__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 2.28/1.63 ( ( V0P
% 2.28/1.63 & ! [V2x: A_27a] : ( V1Q @ V2x ) )
% 2.28/1.63 <=> ! [V3x: A_27a] :
% 2.28/1.63 ( V0P
% 2.28/1.63 & ( V1Q @ V3x ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ELEFT__OR__EXISTS__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: A_27a > $o,V1Q: $o] :
% 2.28/1.63 ( ( ? [V2x: A_27a] : ( V0P @ V2x )
% 2.28/1.63 | V1Q )
% 2.28/1.63 <=> ? [V3x: A_27a] :
% 2.28/1.63 ( ( V0P @ V3x )
% 2.28/1.63 | V1Q ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ERIGHT__OR__EXISTS__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 2.28/1.63 ( ( V0P
% 2.28/1.63 | ? [V2x: A_27a] : ( V1Q @ V2x ) )
% 2.28/1.63 <=> ? [V3x: A_27a] :
% 2.28/1.63 ( V0P
% 2.28/1.63 | ( V1Q @ V3x ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ELEFT__EXISTS__AND__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: A_27a > $o,V1Q: $o] :
% 2.28/1.63 ( ? [V2x: A_27a] :
% 2.28/1.63 ( ( V0P @ V2x )
% 2.28/1.63 & V1Q )
% 2.28/1.63 <=> ( ? [V3x: A_27a] : ( V0P @ V3x )
% 2.28/1.63 & V1Q ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ERIGHT__EXISTS__AND__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 2.28/1.63 ( ? [V2x: A_27a] :
% 2.28/1.63 ( V0P
% 2.28/1.63 & ( V1Q @ V2x ) )
% 2.28/1.63 <=> ( V0P
% 2.28/1.63 & ? [V3x: A_27a] : ( V1Q @ V3x ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ELEFT__FORALL__OR__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0Q: $o,V1P: A_27a > $o] :
% 2.28/1.63 ( ! [V2x: A_27a] :
% 2.28/1.63 ( ( V1P @ V2x )
% 2.28/1.63 | V0Q )
% 2.28/1.63 <=> ( ! [V3x: A_27a] : ( V1P @ V3x )
% 2.28/1.63 | V0Q ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ERIGHT__FORALL__OR__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,V0P: $o,V1Q: A_27a > $o] :
% 2.28/1.63 ( ! [V2x: A_27a] :
% 2.28/1.63 ( V0P
% 2.28/1.63 | ( V1Q @ V2x ) )
% 2.28/1.63 <=> ( V0P
% 2.28/1.63 | ! [V3x: A_27a] : ( V1Q @ V3x ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2EDISJ__SYM,axiom,
% 2.28/1.63 ! [V0A: $o,V1B: $o] :
% 2.28/1.63 ( ( V0A
% 2.28/1.63 | V1B )
% 2.28/1.63 <=> ( V1B
% 2.28/1.63 | V0A ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Ebool_2ESKOLEM__THM,axiom,
% 2.28/1.63 ! [A_27a: $tType,A_27b: $tType,V0P: A_27a > A_27b > $o] :
% 2.28/1.63 ( ! [V1x: A_27a] :
% 2.28/1.63 ? [V2y: A_27b] : ( V0P @ V1x @ V2y )
% 2.28/1.63 <=> ? [V3f: A_27a > A_27b] :
% 2.28/1.63 ! [V4x: A_27a] : ( V0P @ V4x @ ( V3f @ V4x ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Epred__set_2EBIJ__SYM,axiom,
% 2.28/1.63 ! [A_27a: $tType,A_27b: $tType,V0s: A_27a > $o,V1t: A_27b > $o] :
% 2.28/1.63 ( ? [V2f: A_27a > A_27b] : ( c_2Epred__set_2EBIJ @ A_27a @ A_27b @ V2f @ V0s @ V1t )
% 2.28/1.63 <=> ? [V3g: A_27b > A_27a] : ( c_2Epred__set_2EBIJ @ A_27b @ A_27a @ V3g @ V1t @ V0s ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2ENOT__NOT,axiom,
% 2.28/1.63 ! [V0t: $o] :
% 2.28/1.63 ( ( (~) @ ( (~) @ V0t ) )
% 2.28/1.63 <=> V0t ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 2.28/1.63 ! [V0A: $o] :
% 2.28/1.63 ( V0A
% 2.28/1.63 => ( ( (~) @ V0A )
% 2.28/1.63 => c_2Ebool_2EF ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 2.28/1.63 ! [V0B: $o,V1A: $o] :
% 2.28/1.63 ( ( ( (~)
% 2.28/1.63 @ ( V1A
% 2.28/1.63 | V0B ) )
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 <=> ( ( V1A
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 => ( ( (~) @ V0B )
% 2.28/1.63 => c_2Ebool_2EF ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 2.28/1.63 ! [V0B: $o,V1A: $o] :
% 2.28/1.63 ( ( ( (~)
% 2.28/1.63 @ ( ( (~) @ V1A )
% 2.28/1.63 | V0B ) )
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 <=> ( V1A
% 2.28/1.63 => ( ( (~) @ V0B )
% 2.28/1.63 => c_2Ebool_2EF ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2EAND__INV2,axiom,
% 2.28/1.63 ! [V0A: $o] :
% 2.28/1.63 ( ( ( (~) @ V0A )
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 => ( ( V0A
% 2.28/1.63 => c_2Ebool_2EF )
% 2.28/1.63 => c_2Ebool_2EF ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2Edc__eq,axiom,
% 2.28/1.63 ! [V0r: $o,V1q: $o,V2p: $o] :
% 2.28/1.63 ( ( V2p
% 2.28/1.63 <=> ( V1q = V0r ) )
% 2.28/1.63 <=> ( ( V2p
% 2.28/1.63 | V1q
% 2.28/1.63 | V0r )
% 2.28/1.63 & ( V2p
% 2.28/1.63 | ( (~) @ V0r )
% 2.28/1.63 | ( (~) @ V1q ) )
% 2.28/1.63 & ( V1q
% 2.28/1.63 | ( (~) @ V0r )
% 2.28/1.63 | ( (~) @ V2p ) )
% 2.28/1.63 & ( V0r
% 2.28/1.63 | ( (~) @ V1q )
% 2.28/1.63 | ( (~) @ V2p ) ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2Edc__conj,axiom,
% 2.28/1.63 ! [V0r: $o,V1q: $o,V2p: $o] :
% 2.28/1.63 ( ( V2p
% 2.28/1.63 <=> ( V1q
% 2.28/1.63 & V0r ) )
% 2.28/1.63 <=> ( ( V2p
% 2.28/1.63 | ( (~) @ V1q )
% 2.28/1.63 | ( (~) @ V0r ) )
% 2.28/1.63 & ( V1q
% 2.28/1.63 | ( (~) @ V2p ) )
% 2.28/1.63 & ( V0r
% 2.28/1.63 | ( (~) @ V2p ) ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2Edc__disj,axiom,
% 2.28/1.63 ! [V0r: $o,V1q: $o,V2p: $o] :
% 2.28/1.63 ( ( V2p
% 2.28/1.63 <=> ( V1q
% 2.28/1.63 | V0r ) )
% 2.28/1.63 <=> ( ( V2p
% 2.28/1.63 | ( (~) @ V1q ) )
% 2.28/1.63 & ( V2p
% 2.28/1.63 | ( (~) @ V0r ) )
% 2.28/1.63 & ( V1q
% 2.28/1.63 | V0r
% 2.28/1.63 | ( (~) @ V2p ) ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2Edc__imp,axiom,
% 2.28/1.63 ! [V0r: $o,V1q: $o,V2p: $o] :
% 2.28/1.63 ( ( V2p
% 2.28/1.63 <=> ( V1q
% 2.28/1.63 => V0r ) )
% 2.28/1.63 <=> ( ( V2p
% 2.28/1.63 | V1q )
% 2.28/1.63 & ( V2p
% 2.28/1.63 | ( (~) @ V0r ) )
% 2.28/1.63 & ( ( (~) @ V1q )
% 2.28/1.63 | V0r
% 2.28/1.63 | ( (~) @ V2p ) ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Esat_2Edc__neg,axiom,
% 2.28/1.63 ! [V0q: $o,V1p: $o] :
% 2.28/1.63 ( ( V1p
% 2.28/1.63 <=> ( (~) @ V0q ) )
% 2.28/1.63 <=> ( ( V1p
% 2.28/1.63 | V0q )
% 2.28/1.63 & ( ( (~) @ V0q )
% 2.28/1.63 | ( (~) @ V1p ) ) ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Eutil__prob_2ENUM__2D__BIJ,axiom,
% 2.28/1.63 ? [V0f: ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) > tyop_2Enum_2Enum] : ( c_2Epred__set_2EBIJ @ ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ tyop_2Enum_2Enum @ V0f @ ( c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) ) ).
% 2.28/1.63
% 2.28/1.63 thf(thm_2Eutil__prob_2ENUM__2D__BIJ__INV,conjecture,
% 2.28/1.63 ? [V0f: tyop_2Enum_2Enum > ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum )] : ( c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ ( tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ V0f @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) @ ( c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum ) ) ) ).
% 2.28/1.63 ------------------------
% 2.28/1.65 % (20150)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_20047 for (2999ds/2Mi)
% 2.28/1.65 % (20147)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_20047 for (2999ds/4Mi)
% 2.28/1.65 % (20149)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_20047 for (2999ds/2Mi)
% 2.28/1.65 % (20151)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_20047 for (2999ds/275Mi)
% 2.28/1.65 % (20146)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_20047 for (2999ds/183Mi)
% 2.28/1.65 % (20152)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_20047 for (2999ds/18Mi)
% 2.28/1.65 % (20149)Instruction limit reached!
% 2.28/1.65 % (20149)------------------------------
% 2.28/1.65 % (20149)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.28/1.65 % (20149)Termination reason: Unknown
% 2.28/1.65 % (20149)Termination phase: Property scanning
% 2.28/1.65
% 2.28/1.65 % (20149)Memory used [KB]: 1023
% 2.28/1.65 % (20149)Time elapsed: 0.004 s
% 2.28/1.65 % (20149)Instructions burned: 3 (million)
% 2.28/1.65 % (20149)------------------------------
% 2.28/1.65 % (20149)------------------------------
% 2.28/1.65 % (20150)Instruction limit reached!
% 2.28/1.65 % (20150)------------------------------
% 2.28/1.65 % (20150)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.28/1.65 % (20150)Termination reason: Unknown
% 2.28/1.65 % (20150)Termination phase: shuffling
% 2.28/1.65
% 2.28/1.65 % (20150)Memory used [KB]: 1023
% 2.28/1.65 % (20150)Time elapsed: 0.004 s
% 2.28/1.65 % (20150)Instructions burned: 3 (million)
% 2.28/1.65 % (20150)------------------------------
% 2.28/1.65 % (20150)------------------------------
% 2.28/1.66 % (20147)Instruction limit reached!
% 2.28/1.66 % (20147)------------------------------
% 2.28/1.66 % (20147)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.28/1.66 % (20147)Termination reason: Unknown
% 2.28/1.66 % (20147)Termination phase: shuffling
% 2.28/1.66
% 2.28/1.66 % (20147)Memory used [KB]: 1023
% 2.28/1.66 % (20147)Time elapsed: 0.004 s
% 2.28/1.66 % (20147)Instructions burned: 5 (million)
% 2.28/1.66 % (20147)------------------------------
% 2.28/1.66 % (20147)------------------------------
% 2.28/1.66 % (20148)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_20047 for (2999ds/27Mi)
% 2.28/1.66 % (20151)First to succeed.
% 2.28/1.66 % (20152)Instruction limit reached!
% 2.28/1.66 % (20152)------------------------------
% 2.28/1.66 % (20152)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.28/1.66 % (20152)Termination reason: Unknown
% 2.28/1.66 % (20152)Termination phase: Saturation
% 2.28/1.66
% 2.28/1.66 % (20152)Memory used [KB]: 5756
% 2.28/1.66 % (20152)Time elapsed: 0.012 s
% 2.28/1.66 % (20152)Instructions burned: 19 (million)
% 2.28/1.66 % (20152)------------------------------
% 2.28/1.66 % (20152)------------------------------
% 2.28/1.66 % (20151)Refutation found. Thanks to Tanya!
% 2.28/1.66 % SZS status Theorem for DTF2THF_20047
% 2.28/1.66 % SZS output start Proof for DTF2THF_20047
% 2.28/1.66 thf(type_def_6, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 2.28/1.66 thf(type_def_7, type, tyop_2Enum_2Enum: $tType).
% 2.28/1.66 thf(func_def_0, type, tyop_2Emin_2Ebool: $tType).
% 2.28/1.66 thf(func_def_1, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 2.28/1.66 thf(func_def_2, type, tyop_2Enum_2Enum: $tType).
% 2.28/1.66 thf(func_def_3, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 2.28/1.66 thf(func_def_4, type, c_2Ebool_2E_21: !>[X0: $tType]:((X0 > $o) > $o)).
% 2.28/1.66 thf(func_def_5, type, c_2Ebool_2E_2F_5C: $o > $o > $o).
% 2.28/1.66 thf(func_def_6, type, c_2Emin_2E_3D: !>[X0: $tType]:(X0 > X0 > $o)).
% 2.28/1.66 thf(func_def_7, type, c_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 2.28/1.66 thf(func_def_8, type, c_2Ebool_2E_3F: !>[X0: $tType]:((X0 > $o) > $o)).
% 2.28/1.66 thf(func_def_9, type, c_2Epred__set_2EBIJ: !>[X0: $tType, X1: $tType]:((X0 > X1) > (X0 > $o) > (X1 > $o) > $o)).
% 2.28/1.66 thf(func_def_10, type, c_2Epred__set_2ECROSS: !>[X0: $tType, X1: $tType]:((X0 > $o) > (X1 > $o) > tyop_2Epair_2Eprod @ X0 @ X1 > $o)).
% 2.28/1.66 thf(func_def_13, type, c_2Epred__set_2EUNIV: !>[X0: $tType]:(X0 > $o)).
% 2.28/1.66 thf(func_def_14, type, c_2Ebool_2E_5C_2F: $o > $o > $o).
% 2.28/1.66 thf(func_def_15, type, c_2Ebool_2E_7E: $o > $o).
% 2.28/1.66 thf(func_def_24, type, sK0: !>[X0: $tType, X1: $tType]:((X0 > X1 > $o) > X0 > X1)).
% 2.28/1.66 thf(func_def_25, type, sK1: !>[X0: $tType, X1: $tType]:((X0 > X1 > $o) > X0)).
% 2.28/1.66 thf(func_def_26, type, sK2: !>[X0: $tType, X1: $tType]:(X0 > (X0 > X1 > $o) > X1)).
% 2.28/1.66 thf(func_def_27, type, sK3: !>[X0: $tType, X1: $tType]:((X0 > X1) > (X0 > X1 > $o) > X0)).
% 2.28/1.66 thf(func_def_28, type, sK4: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_29, type, sK5: !>[X0: $tType]:((X0 > $o) > $o > X0)).
% 2.28/1.66 thf(func_def_30, type, sK6: !>[X0: $tType]:((X0 > $o) > $o > X0)).
% 2.28/1.66 thf(func_def_31, type, sK7: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_32, type, sK8: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_33, type, sK9: !>[X0: $tType]:((X0 > $o) > $o > X0)).
% 2.28/1.66 thf(func_def_34, type, sK10: tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum).
% 2.28/1.66 thf(func_def_35, type, sK11: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_36, type, sK12: !>[X0: $tType]:((X0 > $o) > $o > X0)).
% 2.28/1.66 thf(func_def_37, type, sK13: !>[X0: $tType]:($o > (X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_38, type, sK14: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_39, type, sK15: !>[X0: $tType, X1: $tType]:((X1 > $o) > (X0 > $o) > X0 > X1)).
% 2.28/1.66 thf(func_def_40, type, sK16: !>[X0: $tType, X1: $tType]:((X1 > $o) > (X0 > $o) > X1 > X0)).
% 2.28/1.66 thf(func_def_41, type, sK17: !>[X0: $tType]:($o > (X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_42, type, sK18: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_43, type, sK19: !>[X0: $tType]:($o > (X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_44, type, sK20: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_45, type, sK21: !>[X0: $tType]:((X0 > $o) > $o > X0)).
% 2.28/1.66 thf(func_def_46, type, sK22: !>[X0: $tType]:((X0 > $o) > X0)).
% 2.28/1.66 thf(func_def_48, type, ph24: !>[X0: $tType]:(X0)).
% 2.28/1.66 thf(f291,plain,(
% 2.28/1.66 $false),
% 2.28/1.66 inference(trivial_inequality_removal,[status(thm)],[f286])).
% 2.28/1.66 thf(f286,plain,(
% 2.28/1.66 ($true != $true)),
% 2.28/1.66 inference(superposition,[status(thm)],[f273,f211])).
% 2.28/1.66 thf(f211,plain,(
% 2.28/1.66 ((c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ sK10 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) = $true)),
% 2.28/1.66 inference(cnf_transformation,[status(thm)],[f151])).
% 2.28/1.66 thf(f151,plain,(
% 2.28/1.66 ((c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ sK10 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) = $true)),
% 2.28/1.66 inference(skolemisation,[status(esa),new_symbols(skolem,[sK10])],[f113,f150])).
% 2.28/1.66 thf(f150,plain,(
% 2.28/1.66 ? [X0 : tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum] : ($true = (c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)) => ((c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ sK10 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) = $true)),
% 2.28/1.66 introduced(definition,[],[choice_axiom])).
% 2.28/1.66 thf(f113,plain,(
% 2.28/1.66 ? [X0 : tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum] : ($true = (c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))),
% 2.28/1.66 inference(fool_elimination,[status(thm)],[f112])).
% 2.28/1.66 thf(f112,plain,(
% 2.28/1.66 ? [X0 : tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum] : (c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)),
% 2.28/1.66 inference(rectify,[status(thm)],[f38])).
% 2.28/1.66 thf(f38,axiom,(
% 2.28/1.66 ? [X4 : tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum] : (c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X4 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)),
% 2.28/1.66 file('/export/starexec/sandbox/tmp/tmp.sh1aevIe5y/DTF2THF_20047.p',thm_2Eutil__prob_2ENUM__2D__BIJ)).
% 2.28/1.66 thf(f273,plain,(
% 2.28/1.66 ( ! [X0 : tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum] : (($true != (c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))) )),
% 2.28/1.66 inference(trivial_inequality_removal,[status(thm)],[f269])).
% 2.28/1.66 thf(f269,plain,(
% 2.28/1.66 ( ! [X0 : tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum > tyop_2Enum_2Enum] : (($true != $true) | ($true != (c_2Epred__set_2EBIJ @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum) @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))) )),
% 2.28/1.66 inference(superposition,[status(thm)],[f222,f221])).
% 2.28/1.66 thf(f221,plain,(
% 2.28/1.66 ( ! [X1 : $tType,X0 : $tType,X2 : X0 > $o,X3 : X1 > $o,X5 : X1 > X0] : (((c_2Epred__set_2EBIJ @ X0 @ X1 @ (sK15 @ X0 @ X1 @ X3 @ X2) @ X2 @ X3) = $true) | ((c_2Epred__set_2EBIJ @ X1 @ X0 @ X5 @ X3 @ X2) != $true)) )),
% 2.28/1.66 inference(cnf_transformation,[status(thm)],[f168])).
% 2.28/1.66 thf(f168,plain,(
% 2.28/1.66 ! [X0 : $tType,X1 : $tType,X2 : X0 > $o,X3 : X1 > $o] : ((((c_2Epred__set_2EBIJ @ X0 @ X1 @ (sK15 @ X0 @ X1 @ X3 @ X2) @ X2 @ X3) = $true) | ! [X5 : X1 > X0] : ((c_2Epred__set_2EBIJ @ X1 @ X0 @ X5 @ X3 @ X2) != $true)) & (((c_2Epred__set_2EBIJ @ X1 @ X0 @ (sK16 @ X0 @ X1 @ X3 @ X2) @ X3 @ X2) = $true) | ! [X7 : X0 > X1] : ((c_2Epred__set_2EBIJ @ X0 @ X1 @ X7 @ X2 @ X3) != $true)))),
% 2.28/1.66 inference(skolemisation,[status(esa),new_symbols(skolem,[sK15,sK16])],[f165,f167,f166])).
% 2.28/1.66 thf(f166,plain,(
% 2.28/1.66 ! [X1 : $tType,X0 : $tType,X2 : X0 > $o,X3 : X1 > $o] : (? [X4 : X0 > X1] : ($true = (c_2Epred__set_2EBIJ @ X0 @ X1 @ X4 @ X2 @ X3)) => ((c_2Epred__set_2EBIJ @ X0 @ X1 @ (sK15 @ X0 @ X1 @ X3 @ X2) @ X2 @ X3) = $true))),
% 2.28/1.66 introduced(definition,[],[choice_axiom])).
% 2.28/1.66 thf(f167,plain,(
% 2.28/1.66 ! [X1 : $tType,X0 : $tType,X2 : X0 > $o,X3 : X1 > $o] : (? [X6 : X1 > X0] : ($true = (c_2Epred__set_2EBIJ @ X1 @ X0 @ X6 @ X3 @ X2)) => ((c_2Epred__set_2EBIJ @ X1 @ X0 @ (sK16 @ X0 @ X1 @ X3 @ X2) @ X3 @ X2) = $true))),
% 2.28/1.66 introduced(definition,[],[choice_axiom])).
% 2.28/1.66 thf(f165,plain,(
% 2.28/1.66 ! [X0 : $tType,X1 : $tType,X2 : X0 > $o,X3 : X1 > $o] : ((? [X4 : X0 > X1] : ($true = (c_2Epred__set_2EBIJ @ X0 @ X1 @ X4 @ X2 @ X3)) | ! [X5 : X1 > X0] : ((c_2Epred__set_2EBIJ @ X1 @ X0 @ X5 @ X3 @ X2) != $true)) & (? [X6 : X1 > X0] : ($true = (c_2Epred__set_2EBIJ @ X1 @ X0 @ X6 @ X3 @ X2)) | ! [X7 : X0 > X1] : ((c_2Epred__set_2EBIJ @ X0 @ X1 @ X7 @ X2 @ X3) != $true)))),
% 2.28/1.66 inference(rectify,[status(thm)],[f164])).
% 2.28/1.66 thf(f164,plain,(
% 2.28/1.66 ! [X0 : $tType,X1 : $tType,X2 : X0 > $o,X3 : X1 > $o] : ((? [X5 : X0 > X1] : ($true = (c_2Epred__set_2EBIJ @ X0 @ X1 @ X5 @ X2 @ X3)) | ! [X4 : X1 > X0] : ((c_2Epred__set_2EBIJ @ X1 @ X0 @ X4 @ X3 @ X2) != $true)) & (? [X4 : X1 > X0] : ((c_2Epred__set_2EBIJ @ X1 @ X0 @ X4 @ X3 @ X2) = $true) | ! [X5 : X0 > X1] : ($true != (c_2Epred__set_2EBIJ @ X0 @ X1 @ X5 @ X2 @ X3))))),
% 2.28/1.66 inference(nnf_transformation,[status(thm)],[f53])).
% 2.28/1.66 thf(f53,plain,(
% 2.28/1.66 ! [X0 : $tType,X1 : $tType,X2 : X0 > $o,X3 : X1 > $o] : (? [X5 : X0 > X1] : ($true = (c_2Epred__set_2EBIJ @ X0 @ X1 @ X5 @ X2 @ X3)) <=> ? [X4 : X1 > X0] : ((c_2Epred__set_2EBIJ @ X1 @ X0 @ X4 @ X3 @ X2) = $true))),
% 2.28/1.66 inference(fool_elimination,[status(thm)],[f52])).
% 2.28/1.66 thf(f52,plain,(
% 2.28/1.66 ! [X0 : $tType,X1 : $tType,X2 : X0 > $o,X3 : X1 > $o] : (? [X4 : X1 > X0] : (c_2Epred__set_2EBIJ @ X1 @ X0 @ X4 @ X3 @ X2) <=> ? [X5 : X0 > X1] : (c_2Epred__set_2EBIJ @ X0 @ X1 @ X5 @ X2 @ X3))),
% 2.28/1.66 inference(rectify,[status(thm)],[f27])).
% 2.28/1.66 thf(f27,axiom,(
% 2.28/1.66 ! [X0 : $tType,X1 : $tType,X22 : X0 > $o,X23 : X1 > $o] : (? [X25 : X1 > X0] : (c_2Epred__set_2EBIJ @ X1 @ X0 @ X25 @ X23 @ X22) <=> ? [X24 : X0 > X1] : (c_2Epred__set_2EBIJ @ X0 @ X1 @ X24 @ X22 @ X23))),
% 2.28/1.66 file('/export/starexec/sandbox/tmp/tmp.sh1aevIe5y/DTF2THF_20047.p',thm_2Epred__set_2EBIJ__SYM)).
% 2.28/1.66 thf(f222,plain,(
% 2.28/1.66 ( ! [X0 : tyop_2Enum_2Enum > tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum] : (($true != (c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)))) )),
% 2.28/1.66 inference(cnf_transformation,[status(thm)],[f119])).
% 2.28/1.66 thf(f119,plain,(
% 2.28/1.66 ! [X0 : tyop_2Enum_2Enum > tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum] : ($true != (c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)))),
% 2.28/1.66 inference(ennf_transformation,[status(thm)],[f91])).
% 2.28/1.66 thf(f91,plain,(
% 2.28/1.66 ~? [X0 : tyop_2Enum_2Enum > tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum] : ($true = (c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum)))),
% 2.28/1.66 inference(fool_elimination,[status(thm)],[f90])).
% 2.28/1.66 thf(f90,plain,(
% 2.28/1.66 ~? [X0 : tyop_2Enum_2Enum > tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum] : (c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X0 @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))),
% 2.28/1.66 inference(rectify,[status(thm)],[f40])).
% 2.28/1.66 thf(f40,negated_conjecture,(
% 2.28/1.66 ~? [X4 : tyop_2Enum_2Enum > tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum] : (c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X4 @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))),
% 2.28/1.66 inference(negated_conjecture,[status(cth)],[f39])).
% 2.28/1.66 thf(f39,conjecture,(
% 2.28/1.66 ? [X4 : tyop_2Enum_2Enum > tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum] : (c_2Epred__set_2EBIJ @ tyop_2Enum_2Enum @ tyop_2Epair_2Eprod @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ X4 @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ (c_2Epred__set_2ECROSS @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum @ c_2Epred__set_2EUNIV @ tyop_2Enum_2Enum))),
% 2.28/1.66 file('/export/starexec/sandbox/tmp/tmp.sh1aevIe5y/DTF2THF_20047.p',thm_2Eutil__prob_2ENUM__2D__BIJ__INV)).
% 2.28/1.66 % SZS output end Proof for DTF2THF_20047
% 2.28/1.66 % (20151)------------------------------
% 2.28/1.66 % (20151)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.28/1.66 % (20151)Termination reason: Refutation
% 2.28/1.66
% 2.28/1.66 % (20151)Memory used [KB]: 5756
% 2.28/1.66 % (20151)Time elapsed: 0.011 s
% 2.28/1.66 % (20151)Instructions burned: 12 (million)
% 2.28/1.66 % (20151)------------------------------
% 2.28/1.66 % (20151)------------------------------
% 2.28/1.66 % (20144)Success in time 0.028 s
%------------------------------------------------------------------------------