%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP015^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:53:43 AM UTC 2026
% Result : Theorem 1.83s 1.50s
% Output : Refutation 1.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP015^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/0.34 % Computer : n004.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue Feb 24 08:20:41 EST 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.24/0.46 ---- Original DTF file ---
% 0.24/0.47 thf(spec,logic,$$dhol).
% 0.24/0.47 %------------------------------------------------------------------------------
% 0.24/0.47 % File : ITP015^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.24/0.47 % Domain : Interactive Theorem Proving
% 0.24/0.47 % Problem : HOL4 syntactic export of thm_2Einteger__word_2Ei2w__0.p, bushy mode
% 0.24/0.47 % Version : [BG+19] axioms.
% 0.24/0.47 % English :
% 0.24/0.47
% 0.24/0.47 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.24/0.47 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.24/0.47 % Source : [BG+19]
% 0.24/0.47 % Names : thm_2Einteger__word_2Ei2w__0.p [Gau19]
% 0.24/0.47 % : HL407001^3.p [TPAP]
% 0.24/0.47
% 0.24/0.47 % Status : Theorem
% 0.24/0.47 % Rating : 0.33 v8.1.0, 0.25 v7.5.0
% 0.24/0.47 % Syntax : Number of formulae : 51 ( 13 unt; 28 typ; 0 def)
% 0.24/0.47 % Number of atoms : 49 ( 23 equ; 5 cnn)
% 0.24/0.47 % Maximal formula atoms : 8 ( 2 avg)
% 0.24/0.47 % Number of connectives : 162 ( 5 ~; 2 |; 8 &; 123 @)
% 0.24/0.47 % ( 12 <=>; 12 =>; 0 <=; 0 <~>)
% 0.24/0.47 % Maximal formula depth : 13 ( 5 avg)
% 0.24/0.47 % Number of types : 4 ( 3 usr)
% 0.24/0.47 % Number of type conns : 36 ( 36 >; 0 *; 0 +; 0 <<)
% 0.24/0.47 % Number of symbols : 27 ( 25 usr; 4 con; 0-4 aty)
% 0.24/0.47 % Number of variables : 59 ( 0 ^; 49 !; 1 ?; 59 :)
% 0.24/0.47 % ( 9 !>; 0 ?*; 0 @-; 0 @+)
% 0.24/0.47 % SPC : TH1_THM_EQU_NAR
% 0.24/0.47
% 0.24/0.47 % Comments :
% 0.24/0.47 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.24/0.47 %------------------------------------------------------------------------------
% 0.24/0.47 thf(tyop_2Ebool_2Eitself,type,
% 0.24/0.47 tyop_2Ebool_2Eitself: $tType > $tType ).
% 0.24/0.47
% 0.24/0.47 thf(tyop_2Efcp_2Ecart,type,
% 0.24/0.47 tyop_2Efcp_2Ecart: $tType > $tType > $tType ).
% 0.24/0.47
% 0.24/0.47 thf(tyop_2Einteger_2Eint,type,
% 0.24/0.47 tyop_2Einteger_2Eint: $tType ).
% 0.24/0.47
% 0.24/0.47 thf(tyop_2Emin_2Ebool,type,
% 0.24/0.47 tyop_2Emin_2Ebool: $tType ).
% 0.24/0.47
% 0.24/0.47 thf(tyop_2Emin_2Efun,type,
% 0.24/0.47 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 0.24/0.47
% 0.24/0.47 thf(tyop_2Enum_2Enum,type,
% 0.24/0.47 tyop_2Enum_2Enum: $tType ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2E_21,type,
% 0.24/0.47 c_2Ebool_2E_21:
% 0.24/0.47 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2E_2F_5C,type,
% 0.24/0.47 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Enum_2E0,type,
% 0.24/0.47 c_2Enum_2E0: tyop_2Enum_2Enum ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Eprim__rec_2E_3C,type,
% 0.24/0.47 c_2Eprim__rec_2E_3C: tyop_2Enum_2Enum > tyop_2Enum_2Enum > $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Emin_2E_3D,type,
% 0.24/0.47 c_2Emin_2E_3D:
% 0.24/0.47 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Emin_2E_3D_3D_3E,type,
% 0.24/0.47 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2E_3F,type,
% 0.24/0.47 c_2Ebool_2E_3F:
% 0.24/0.47 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2ECOND,type,
% 0.24/0.47 c_2Ebool_2ECOND:
% 0.24/0.47 !>[A_27a: $tType] : ( $o > A_27a > A_27a > A_27a ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2EF,type,
% 0.24/0.47 c_2Ebool_2EF: $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Earithmetic_2EMOD,type,
% 0.24/0.47 c_2Earithmetic_2EMOD: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Einteger_2ENum,type,
% 0.24/0.47 c_2Einteger_2ENum: tyop_2Einteger_2Eint > tyop_2Enum_2Enum ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2ET,type,
% 0.24/0.47 c_2Ebool_2ET: $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2E_5C_2F,type,
% 0.24/0.47 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ewords_2Edimword,type,
% 0.24/0.47 c_2Ewords_2Edimword:
% 0.24/0.47 !>[A_27a: $tType] : ( ( tyop_2Ebool_2Eitself @ A_27a ) > tyop_2Enum_2Enum ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Einteger__word_2Ei2w,type,
% 0.24/0.47 c_2Einteger__word_2Ei2w:
% 0.24/0.47 !>[A_27a: $tType] : ( tyop_2Einteger_2Eint > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Einteger_2Eint__lt,type,
% 0.24/0.47 c_2Einteger_2Eint__lt: tyop_2Einteger_2Eint > tyop_2Einteger_2Eint > $o ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Einteger_2Eint__neg,type,
% 0.24/0.47 c_2Einteger_2Eint__neg: tyop_2Einteger_2Eint > tyop_2Einteger_2Eint ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Einteger_2Eint__of__num,type,
% 0.24/0.47 c_2Einteger_2Eint__of__num: tyop_2Enum_2Enum > tyop_2Einteger_2Eint ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ewords_2En2w,type,
% 0.24/0.47 c_2Ewords_2En2w:
% 0.24/0.47 !>[A_27a: $tType] : ( tyop_2Enum_2Enum > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2Ethe__value,type,
% 0.24/0.47 c_2Ebool_2Ethe__value:
% 0.24/0.47 !>[A_27a: $tType] : ( tyop_2Ebool_2Eitself @ A_27a ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ewords_2Eword__2comp,type,
% 0.24/0.47 c_2Ewords_2Eword__2comp:
% 0.24/0.47 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(c_2Ebool_2E_7E,type,
% 0.24/0.47 c_2Ebool_2E_7E: $o > $o ).
% 0.24/0.47
% 0.24/0.47 thf(logicdef_2E_2F_5C,axiom,
% 0.24/0.47 ! [V0: $o,V1: $o] :
% 0.24/0.47 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.24/0.47 <=> ( V0
% 0.24/0.47 & V1 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(logicdef_2E_5C_2F,axiom,
% 0.24/0.47 ! [V0: $o,V1: $o] :
% 0.24/0.47 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.24/0.47 <=> ( V0
% 0.24/0.47 | V1 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(logicdef_2E_7E,axiom,
% 0.24/0.47 ! [V0: $o] :
% 0.24/0.47 ( ( c_2Ebool_2E_7E @ V0 )
% 0.24/0.47 <=> ( (~) @ V0 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(logicdef_2E_3D_3D_3E,axiom,
% 0.24/0.47 ! [V0: $o,V1: $o] :
% 0.24/0.47 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.24/0.47 <=> ( V0
% 0.24/0.47 => V1 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(logicdef_2E_3D,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 0.24/0.47 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 0.24/0.47 <=> ( V0 = V1 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(quantdef_2E_21,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.24/0.47 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 0.24/0.47 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(quantdef_2E_3F,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.24/0.47 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 0.24/0.47 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2ETRUTH,axiom,
% 0.24/0.47 c_2Ebool_2ET ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 0.24/0.47 ! [V0t1: $o,V1t2: $o] :
% 0.24/0.47 ( ( V0t1
% 0.24/0.47 => V1t2 )
% 0.24/0.47 => ( ( V1t2
% 0.24/0.47 => V0t1 )
% 0.24/0.47 => ( V0t1 = V1t2 ) ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2EFALSITY,axiom,
% 0.24/0.47 ! [V0t: $o] :
% 0.24/0.47 ( c_2Ebool_2EF
% 0.24/0.47 => V0t ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2EREFL__CLAUSE,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0x: A_27a] :
% 0.24/0.47 ( ( V0x = V0x )
% 0.24/0.47 <=> c_2Ebool_2ET ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 0.24/0.47 ( ( V0x = V1y )
% 0.24/0.47 <=> ( V1y = V0x ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2EAND__IMP__INTRO,axiom,
% 0.24/0.47 ! [V0t1: $o,V1t2: $o,V2t3: $o] :
% 0.24/0.47 ( ( V0t1
% 0.24/0.47 => ( V1t2
% 0.24/0.47 => V2t3 ) )
% 0.24/0.47 <=> ( ( V0t1
% 0.24/0.47 & V1t2 )
% 0.24/0.47 => V2t3 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2ECOND__CONG,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0P: $o,V1Q: $o,V2x: A_27a,V3x_27: A_27a,V4y: A_27a,V5y_27: A_27a] :
% 0.24/0.47 ( ( ( V0P = V1Q )
% 0.24/0.47 & ( V1Q
% 0.24/0.47 => ( V2x = V3x_27 ) )
% 0.24/0.47 & ( ( (~) @ V1Q )
% 0.24/0.47 => ( V4y = V5y_27 ) ) )
% 0.24/0.47 => ( ( c_2Ebool_2ECOND @ A_27a @ V0P @ V2x @ V4y )
% 0.24/0.47 = ( c_2Ebool_2ECOND @ A_27a @ V1Q @ V3x_27 @ V5y_27 ) ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ebool_2Ebool__case__thm,axiom,
% 0.24/0.47 ! [A_27a: $tType] :
% 0.24/0.47 ( ! [V0t1: A_27a,V1t2: A_27a] :
% 0.24/0.47 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2ET @ V0t1 @ V1t2 )
% 0.24/0.47 = V0t1 )
% 0.24/0.47 & ! [V2t1: A_27a,V3t2: A_27a] :
% 0.24/0.47 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2EF @ V2t1 @ V3t2 )
% 0.24/0.47 = V3t2 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Einteger_2EINT__NEG__0,axiom,
% 0.24/0.47 ( ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
% 0.24/0.47 = ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Einteger_2EINT__LT__CALCULATE,axiom,
% 0.24/0.47 ! [V0n: tyop_2Enum_2Enum,V1m: tyop_2Enum_2Enum] :
% 0.24/0.47 ( ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__of__num @ V0n ) @ ( c_2Einteger_2Eint__of__num @ V1m ) )
% 0.24/0.47 = ( c_2Eprim__rec_2E_3C @ V0n @ V1m ) )
% 0.24/0.47 & ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V0n ) ) @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V1m ) ) )
% 0.24/0.47 = ( c_2Eprim__rec_2E_3C @ V1m @ V0n ) )
% 0.24/0.47 & ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V0n ) ) @ ( c_2Einteger_2Eint__of__num @ V1m ) )
% 0.24/0.47 <=> ( ( (~) @ ( V0n = c_2Enum_2E0 ) )
% 0.24/0.47 | ( (~) @ ( V1m = c_2Enum_2E0 ) ) ) )
% 0.24/0.47 & ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__of__num @ V0n ) @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V1m ) ) )
% 0.24/0.47 = c_2Ebool_2EF ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Einteger_2ENUM__OF__INT,axiom,
% 0.24/0.47 ! [V0n: tyop_2Enum_2Enum] :
% 0.24/0.47 ( ( c_2Einteger_2ENum @ ( c_2Einteger_2Eint__of__num @ V0n ) )
% 0.24/0.47 = V0n ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Einteger__word_2Ei2w__def,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0i: tyop_2Einteger_2Eint] :
% 0.24/0.47 ( ( c_2Einteger__word_2Ei2w @ A_27a @ V0i )
% 0.24/0.47 = ( c_2Ebool_2ECOND @ ( tyop_2Efcp_2Ecart @ $o @ A_27a ) @ ( c_2Einteger_2Eint__lt @ V0i @ ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) @ ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ ( c_2Einteger_2ENum @ ( c_2Einteger_2Eint__neg @ V0i ) ) ) ) @ ( c_2Ewords_2En2w @ A_27a @ ( c_2Einteger_2ENum @ V0i ) ) ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Eprim__rec_2ENOT__LESS__0,axiom,
% 0.24/0.47 ! [V0n: tyop_2Enum_2Enum] : ( (~) @ ( c_2Eprim__rec_2E_3C @ V0n @ c_2Enum_2E0 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ewords_2En2w__11,axiom,
% 0.24/0.47 ! [A_27a: $tType,V0m: tyop_2Enum_2Enum,V1n: tyop_2Enum_2Enum] :
% 0.24/0.47 ( ( ( c_2Ewords_2En2w @ A_27a @ V0m )
% 0.24/0.47 = ( c_2Ewords_2En2w @ A_27a @ V1n ) )
% 0.24/0.47 <=> ( ( c_2Earithmetic_2EMOD @ V0m @ ( c_2Ewords_2Edimword @ A_27a @ ( c_2Ebool_2Ethe__value @ A_27a ) ) )
% 0.24/0.47 = ( c_2Earithmetic_2EMOD @ V1n @ ( c_2Ewords_2Edimword @ A_27a @ ( c_2Ebool_2Ethe__value @ A_27a ) ) ) ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Ewords_2EWORD__NEG__0,axiom,
% 0.24/0.47 ! [A_27a: $tType] :
% 0.24/0.47 ( ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ c_2Enum_2E0 ) )
% 0.24/0.47 = ( c_2Ewords_2En2w @ A_27a @ c_2Enum_2E0 ) ) ).
% 0.24/0.47
% 0.24/0.47 thf(thm_2Einteger__word_2Ei2w__0,conjecture,
% 0.24/0.47 ! [A_27a: $tType] :
% 0.24/0.47 ( ( c_2Einteger__word_2Ei2w @ A_27a @ ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
% 0.24/0.47 = ( c_2Ewords_2En2w @ A_27a @ c_2Enum_2E0 ) ) ).
% 0.24/0.47
% 0.24/0.47 %------------------------------------------------------------------------------
% 0.24/0.47 ------------------------
% 1.76/1.33 ---- Embedded in THF ---
% 1.76/1.33 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.76/1.33 %%% Generated on Tue Feb 24 08:20:42 EST 2026
% 1.76/1.33 %%% using '$$dhol' embedding, version 1.3.0.
% 1.76/1.33 %%% Logic specification used:
% 1.76/1.33 %%% thf(spec, logic, $$dhol).
% 1.76/1.33
% 1.76/1.33 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2DTF4447.p
% 1.76/1.33 thf(tyop_2Ebool_2Eitself, type, tyop_2Ebool_2Eitself: ($tType > $tType)).
% 1.76/1.33 thf(tyop_2Efcp_2Ecart, type, tyop_2Efcp_2Ecart: ($tType > ($tType > $tType))).
% 1.76/1.33 thf(tyop_2Einteger_2Eint, type, tyop_2Einteger_2Eint: $tType).
% 1.76/1.33 thf(tyop_2Emin_2Ebool, type, tyop_2Emin_2Ebool: $tType).
% 1.76/1.33 thf(tyop_2Emin_2Efun, type, tyop_2Emin_2Efun: ($tType > ($tType > $tType))).
% 1.76/1.33 thf(tyop_2Enum_2Enum, type, tyop_2Enum_2Enum: $tType).
% 1.76/1.33 thf(c_2Ebool_2E_21, type, c_2Ebool_2E_21: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.76/1.33 thf(c_2Ebool_2E_2F_5C, type, c_2Ebool_2E_2F_5C: ($o > ($o > $o))).
% 1.76/1.33 thf(c_2Enum_2E0, type, c_2Enum_2E0: tyop_2Enum_2Enum).
% 1.76/1.33 thf(c_2Eprim__rec_2E_3C, type, c_2Eprim__rec_2E_3C: (tyop_2Enum_2Enum > (tyop_2Enum_2Enum > $o))).
% 1.76/1.33 thf(c_2Emin_2E_3D, type, c_2Emin_2E_3D: (!> [A_27a:$tType]: ((A_27a > (A_27a > $o))))).
% 1.76/1.33 thf(c_2Emin_2E_3D_3D_3E, type, c_2Emin_2E_3D_3D_3E: ($o > ($o > $o))).
% 1.76/1.33 thf(c_2Ebool_2E_3F, type, c_2Ebool_2E_3F: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.76/1.33 thf(c_2Ebool_2ECOND, type, c_2Ebool_2ECOND: (!> [A_27a:$tType]: (($o > (A_27a > (A_27a > A_27a)))))).
% 1.76/1.33 thf(c_2Ebool_2EF, type, c_2Ebool_2EF: $o).
% 1.76/1.33 thf(c_2Earithmetic_2EMOD, type, c_2Earithmetic_2EMOD: (tyop_2Enum_2Enum > (tyop_2Enum_2Enum > tyop_2Enum_2Enum))).
% 1.76/1.33 thf(c_2Einteger_2ENum, type, c_2Einteger_2ENum: (tyop_2Einteger_2Eint > tyop_2Enum_2Enum)).
% 1.76/1.33 thf(c_2Ebool_2ET, type, c_2Ebool_2ET: $o).
% 1.76/1.33 thf(c_2Ebool_2E_5C_2F, type, c_2Ebool_2E_5C_2F: ($o > ($o > $o))).
% 1.76/1.33 thf(c_2Ewords_2Edimword, type, c_2Ewords_2Edimword: (!> [A_27a:$tType]: (((tyop_2Ebool_2Eitself @ A_27a) > tyop_2Enum_2Enum)))).
% 1.76/1.33 thf(c_2Einteger__word_2Ei2w, type, c_2Einteger__word_2Ei2w: (!> [A_27a:$tType]: ((tyop_2Einteger_2Eint > ((tyop_2Efcp_2Ecart @ $o) @ A_27a))))).
% 1.76/1.33 thf(c_2Einteger_2Eint__lt, type, c_2Einteger_2Eint__lt: (tyop_2Einteger_2Eint > (tyop_2Einteger_2Eint > $o))).
% 1.76/1.33 thf(c_2Einteger_2Eint__neg, type, c_2Einteger_2Eint__neg: (tyop_2Einteger_2Eint > tyop_2Einteger_2Eint)).
% 1.76/1.33 thf(c_2Einteger_2Eint__of__num, type, c_2Einteger_2Eint__of__num: (tyop_2Enum_2Enum > tyop_2Einteger_2Eint)).
% 1.76/1.33 thf(c_2Ewords_2En2w, type, c_2Ewords_2En2w: (!> [A_27a:$tType]: ((tyop_2Enum_2Enum > ((tyop_2Efcp_2Ecart @ $o) @ A_27a))))).
% 1.76/1.33 thf(c_2Ebool_2Ethe__value, type, c_2Ebool_2Ethe__value: (!> [A_27a:$tType]: ((tyop_2Ebool_2Eitself @ A_27a)))).
% 1.76/1.33 thf(c_2Ewords_2Eword__2comp, type, c_2Ewords_2Eword__2comp: (!> [A_27a:$tType]: ((((tyop_2Efcp_2Ecart @ $o) @ A_27a) > ((tyop_2Efcp_2Ecart @ $o) @ A_27a))))).
% 1.76/1.33 thf(c_2Ebool_2E_7E, type, c_2Ebool_2E_7E: ($o > $o)).
% 1.76/1.33 thf(logicdef_2E_2F_5C, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_2F_5C @ V0) @ V1) <=> (V0 & V1))))).
% 1.76/1.33 thf(logicdef_2E_5C_2F, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_5C_2F @ V0) @ V1) <=> (V0 | V1))))).
% 1.76/1.33 thf(logicdef_2E_7E, axiom, (! [V0:$o]: (((c_2Ebool_2E_7E @ V0) <=> ((~) @ V0))))).
% 1.76/1.33 thf(logicdef_2E_3D_3D_3E, axiom, (! [V0:$o,V1:$o]: ((((c_2Emin_2E_3D_3D_3E @ V0) @ V1) <=> (V0 => V1))))).
% 1.76/1.33 thf(logicdef_2E_3D, axiom, (! [A_27a:$tType,V0:A_27a,V1:A_27a]: (((((c_2Emin_2E_3D @ A_27a) @ V0) @ V1) <=> (V0 = V1))))).
% 1.76/1.33 thf(quantdef_2E_21, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_21 @ A_27a) @ V0f) <=> (! [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.76/1.33 thf(quantdef_2E_3F, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_3F @ A_27a) @ V0f) <=> (? [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.76/1.33 thf(thm_2Ebool_2ETRUTH, axiom, c_2Ebool_2ET).
% 1.76/1.33 thf(thm_2Ebool_2EIMP__ANTISYM__AX, axiom, (! [V0t1:$o,V1t2:$o]: (((V0t1 => V1t2) => ((V1t2 => V0t1) => (V0t1 = V1t2)))))).
% 1.76/1.33 thf(thm_2Ebool_2EFALSITY, axiom, (! [V0t:$o]: ((c_2Ebool_2EF => V0t)))).
% 1.76/1.33 thf(thm_2Ebool_2EREFL__CLAUSE, axiom, (! [A_27a:$tType,V0x:A_27a]: (((V0x = V0x) <=> c_2Ebool_2ET)))).
% 1.76/1.33 thf(thm_2Ebool_2EEQ__SYM__EQ, axiom, (! [A_27a:$tType,V0x:A_27a,V1y:A_27a]: (((V0x = V1y) <=> (V1y = V0x))))).
% 1.76/1.33 thf(thm_2Ebool_2EAND__IMP__INTRO, axiom, (! [V0t1:$o,V1t2:$o,V2t3:$o]: (((V0t1 => (V1t2 => V2t3)) <=> ((V0t1 & V1t2) => V2t3))))).
% 1.76/1.33 thf(thm_2Ebool_2ECOND__CONG, axiom, (! [A_27a:$tType,V0P:$o,V1Q:$o,V2x:A_27a,V3x_27:A_27a,V4y:A_27a,V5y_27:A_27a]: ((((V0P = V1Q) & ((V1Q => (V2x = V3x_27)) & (((~) @ V1Q) => (V4y = V5y_27)))) => (((((c_2Ebool_2ECOND @ A_27a) @ V0P) @ V2x) @ V4y) = ((((c_2Ebool_2ECOND @ A_27a) @ V1Q) @ V3x_27) @ V5y_27)))))).
% 1.76/1.33 thf(thm_2Ebool_2Ebool__case__thm, axiom, (! [A_27a:$tType]: (((! [V0t1:A_27a,V1t2:A_27a]: ((((((c_2Ebool_2ECOND @ A_27a) @ c_2Ebool_2ET) @ V0t1) @ V1t2) = V0t1))) & (! [V2t1:A_27a,V3t2:A_27a]: ((((((c_2Ebool_2ECOND @ A_27a) @ c_2Ebool_2EF) @ V2t1) @ V3t2) = V3t2))))))).
% 1.76/1.33 thf(thm_2Einteger_2EINT__NEG__0, axiom, ((c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) = (c_2Einteger_2Eint__of__num @ c_2Enum_2E0))).
% 1.76/1.33 thf(thm_2Einteger_2EINT__LT__CALCULATE, axiom, (! [V0n:tyop_2Enum_2Enum,V1m:tyop_2Enum_2Enum]: (((((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ V0n)) @ (c_2Einteger_2Eint__of__num @ V1m)) = ((c_2Eprim__rec_2E_3C @ V0n) @ V1m)) & ((((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ V0n))) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ V1m))) = ((c_2Eprim__rec_2E_3C @ V1m) @ V0n)) & ((((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ V0n))) @ (c_2Einteger_2Eint__of__num @ V1m)) <=> (((~) @ (V0n = c_2Enum_2E0)) | ((~) @ (V1m = c_2Enum_2E0)))) & (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ V0n)) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ V1m))) = c_2Ebool_2EF))))))).
% 1.76/1.33 thf(thm_2Einteger_2ENUM__OF__INT, axiom, (! [V0n:tyop_2Enum_2Enum]: (((c_2Einteger_2ENum @ (c_2Einteger_2Eint__of__num @ V0n)) = V0n)))).
% 1.76/1.33 thf(thm_2Einteger__word_2Ei2w__def, axiom, (! [A_27a:$tType,V0i:tyop_2Einteger_2Eint]: ((((c_2Einteger__word_2Ei2w @ A_27a) @ V0i) = ((((c_2Ebool_2ECOND @ ((tyop_2Efcp_2Ecart @ $o) @ A_27a)) @ ((c_2Einteger_2Eint__lt @ V0i) @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0))) @ ((c_2Ewords_2Eword__2comp @ A_27a) @ ((c_2Ewords_2En2w @ A_27a) @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__neg @ V0i))))) @ ((c_2Ewords_2En2w @ A_27a) @ (c_2Einteger_2ENum @ V0i))))))).
% 1.76/1.33 thf(thm_2Eprim__rec_2ENOT__LESS__0, axiom, (! [V0n:tyop_2Enum_2Enum]: (((~) @ ((c_2Eprim__rec_2E_3C @ V0n) @ c_2Enum_2E0))))).
% 1.76/1.33 thf(thm_2Ewords_2En2w__11, axiom, (! [A_27a:$tType,V0m:tyop_2Enum_2Enum,V1n:tyop_2Enum_2Enum]: (((((c_2Ewords_2En2w @ A_27a) @ V0m) = ((c_2Ewords_2En2w @ A_27a) @ V1n)) <=> (((c_2Earithmetic_2EMOD @ V0m) @ ((c_2Ewords_2Edimword @ A_27a) @ (c_2Ebool_2Ethe__value @ A_27a))) = ((c_2Earithmetic_2EMOD @ V1n) @ ((c_2Ewords_2Edimword @ A_27a) @ (c_2Ebool_2Ethe__value @ A_27a)))))))).
% 1.76/1.33 thf(thm_2Ewords_2EWORD__NEG__0, axiom, (! [A_27a:$tType]: ((((c_2Ewords_2Eword__2comp @ A_27a) @ ((c_2Ewords_2En2w @ A_27a) @ c_2Enum_2E0)) = ((c_2Ewords_2En2w @ A_27a) @ c_2Enum_2E0))))).
% 1.76/1.33 thf(thm_2Einteger__word_2Ei2w__0, conjecture, (! [A_27a:$tType]: ((((c_2Einteger__word_2Ei2w @ A_27a) @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) = ((c_2Ewords_2En2w @ A_27a) @ c_2Enum_2E0))))).
% 1.76/1.33 % SZS output end ListOfTHF for /export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2DTF4447.p
% 1.76/1.33 ------------------------
% 1.76/1.34 ---- Cleaned THF ---
% 1.76/1.34 thf(tyop_2Ebool_2Eitself,type,
% 1.76/1.34 tyop_2Ebool_2Eitself: $tType > $tType ).
% 1.76/1.34
% 1.76/1.34 thf(tyop_2Efcp_2Ecart,type,
% 1.76/1.34 tyop_2Efcp_2Ecart: $tType > $tType > $tType ).
% 1.76/1.34
% 1.76/1.34 thf(tyop_2Einteger_2Eint,type,
% 1.76/1.34 tyop_2Einteger_2Eint: $tType ).
% 1.76/1.34
% 1.76/1.34 thf(tyop_2Emin_2Ebool,type,
% 1.76/1.34 tyop_2Emin_2Ebool: $tType ).
% 1.76/1.34
% 1.76/1.34 thf(tyop_2Emin_2Efun,type,
% 1.76/1.34 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 1.76/1.34
% 1.76/1.34 thf(tyop_2Enum_2Enum,type,
% 1.76/1.34 tyop_2Enum_2Enum: $tType ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2E_21,type,
% 1.76/1.34 c_2Ebool_2E_21:
% 1.76/1.34 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2E_2F_5C,type,
% 1.76/1.34 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Enum_2E0,type,
% 1.76/1.34 c_2Enum_2E0: tyop_2Enum_2Enum ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Eprim__rec_2E_3C,type,
% 1.76/1.34 c_2Eprim__rec_2E_3C: tyop_2Enum_2Enum > tyop_2Enum_2Enum > $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Emin_2E_3D,type,
% 1.76/1.34 c_2Emin_2E_3D:
% 1.76/1.34 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Emin_2E_3D_3D_3E,type,
% 1.76/1.34 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2E_3F,type,
% 1.76/1.34 c_2Ebool_2E_3F:
% 1.76/1.34 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2ECOND,type,
% 1.76/1.34 c_2Ebool_2ECOND:
% 1.76/1.34 !>[A_27a: $tType] : ( $o > A_27a > A_27a > A_27a ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2EF,type,
% 1.76/1.34 c_2Ebool_2EF: $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Earithmetic_2EMOD,type,
% 1.76/1.34 c_2Earithmetic_2EMOD: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Einteger_2ENum,type,
% 1.76/1.34 c_2Einteger_2ENum: tyop_2Einteger_2Eint > tyop_2Enum_2Enum ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2ET,type,
% 1.76/1.34 c_2Ebool_2ET: $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2E_5C_2F,type,
% 1.76/1.34 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ewords_2Edimword,type,
% 1.76/1.34 c_2Ewords_2Edimword:
% 1.76/1.34 !>[A_27a: $tType] : ( ( tyop_2Ebool_2Eitself @ A_27a ) > tyop_2Enum_2Enum ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Einteger__word_2Ei2w,type,
% 1.76/1.34 c_2Einteger__word_2Ei2w:
% 1.76/1.34 !>[A_27a: $tType] : ( tyop_2Einteger_2Eint > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Einteger_2Eint__lt,type,
% 1.76/1.34 c_2Einteger_2Eint__lt: tyop_2Einteger_2Eint > tyop_2Einteger_2Eint > $o ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Einteger_2Eint__neg,type,
% 1.76/1.34 c_2Einteger_2Eint__neg: tyop_2Einteger_2Eint > tyop_2Einteger_2Eint ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Einteger_2Eint__of__num,type,
% 1.76/1.34 c_2Einteger_2Eint__of__num: tyop_2Enum_2Enum > tyop_2Einteger_2Eint ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ewords_2En2w,type,
% 1.76/1.34 c_2Ewords_2En2w:
% 1.76/1.34 !>[A_27a: $tType] : ( tyop_2Enum_2Enum > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2Ethe__value,type,
% 1.76/1.34 c_2Ebool_2Ethe__value:
% 1.76/1.34 !>[A_27a: $tType] : ( tyop_2Ebool_2Eitself @ A_27a ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ewords_2Eword__2comp,type,
% 1.76/1.34 c_2Ewords_2Eword__2comp:
% 1.76/1.34 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(c_2Ebool_2E_7E,type,
% 1.76/1.34 c_2Ebool_2E_7E: $o > $o ).
% 1.76/1.34
% 1.76/1.34 thf(logicdef_2E_2F_5C,axiom,
% 1.76/1.34 ! [V0: $o,V1: $o] :
% 1.76/1.34 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 1.76/1.34 <=> ( V0
% 1.76/1.34 & V1 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(logicdef_2E_5C_2F,axiom,
% 1.76/1.34 ! [V0: $o,V1: $o] :
% 1.76/1.34 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 1.76/1.34 <=> ( V0
% 1.76/1.34 | V1 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(logicdef_2E_7E,axiom,
% 1.76/1.34 ! [V0: $o] :
% 1.76/1.34 ( ( c_2Ebool_2E_7E @ V0 )
% 1.76/1.34 <=> ( (~) @ V0 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(logicdef_2E_3D_3D_3E,axiom,
% 1.76/1.34 ! [V0: $o,V1: $o] :
% 1.76/1.34 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 1.76/1.34 <=> ( V0
% 1.76/1.34 => V1 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(logicdef_2E_3D,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 1.76/1.34 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 1.76/1.34 <=> ( V0 = V1 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(quantdef_2E_21,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.76/1.34 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 1.76/1.34 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(quantdef_2E_3F,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.76/1.34 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 1.76/1.34 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2ETRUTH,axiom,
% 1.76/1.34 c_2Ebool_2ET ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2EIMP__ANTISYM__AX,axiom,
% 1.76/1.34 ! [V0t1: $o,V1t2: $o] :
% 1.76/1.34 ( ( V0t1
% 1.76/1.34 => V1t2 )
% 1.76/1.34 => ( ( V1t2
% 1.76/1.34 => V0t1 )
% 1.76/1.34 => ( V0t1 = V1t2 ) ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2EFALSITY,axiom,
% 1.76/1.34 ! [V0t: $o] :
% 1.76/1.34 ( c_2Ebool_2EF
% 1.76/1.34 => V0t ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2EREFL__CLAUSE,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0x: A_27a] :
% 1.76/1.34 ( ( V0x = V0x )
% 1.76/1.34 <=> c_2Ebool_2ET ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 1.76/1.34 ( ( V0x = V1y )
% 1.76/1.34 <=> ( V1y = V0x ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2EAND__IMP__INTRO,axiom,
% 1.76/1.34 ! [V0t1: $o,V1t2: $o,V2t3: $o] :
% 1.76/1.34 ( ( V0t1
% 1.76/1.34 => ( V1t2
% 1.76/1.34 => V2t3 ) )
% 1.76/1.34 <=> ( ( V0t1
% 1.76/1.34 & V1t2 )
% 1.76/1.34 => V2t3 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2ECOND__CONG,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0P: $o,V1Q: $o,V2x: A_27a,V3x_27: A_27a,V4y: A_27a,V5y_27: A_27a] :
% 1.76/1.34 ( ( ( V0P = V1Q )
% 1.76/1.34 & ( V1Q
% 1.76/1.34 => ( V2x = V3x_27 ) )
% 1.76/1.34 & ( ( (~) @ V1Q )
% 1.76/1.34 => ( V4y = V5y_27 ) ) )
% 1.76/1.34 => ( ( c_2Ebool_2ECOND @ A_27a @ V0P @ V2x @ V4y )
% 1.76/1.34 = ( c_2Ebool_2ECOND @ A_27a @ V1Q @ V3x_27 @ V5y_27 ) ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ebool_2Ebool__case__thm,axiom,
% 1.76/1.34 ! [A_27a: $tType] :
% 1.76/1.34 ( ! [V0t1: A_27a,V1t2: A_27a] :
% 1.76/1.34 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2ET @ V0t1 @ V1t2 )
% 1.76/1.34 = V0t1 )
% 1.76/1.34 & ! [V2t1: A_27a,V3t2: A_27a] :
% 1.76/1.34 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2EF @ V2t1 @ V3t2 )
% 1.76/1.34 = V3t2 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Einteger_2EINT__NEG__0,axiom,
% 1.76/1.34 ( ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
% 1.76/1.34 = ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Einteger_2EINT__LT__CALCULATE,axiom,
% 1.76/1.34 ! [V0n: tyop_2Enum_2Enum,V1m: tyop_2Enum_2Enum] :
% 1.76/1.34 ( ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__of__num @ V0n ) @ ( c_2Einteger_2Eint__of__num @ V1m ) )
% 1.76/1.34 = ( c_2Eprim__rec_2E_3C @ V0n @ V1m ) )
% 1.76/1.34 & ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V0n ) ) @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V1m ) ) )
% 1.76/1.34 = ( c_2Eprim__rec_2E_3C @ V1m @ V0n ) )
% 1.76/1.34 & ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V0n ) ) @ ( c_2Einteger_2Eint__of__num @ V1m ) )
% 1.76/1.34 <=> ( ( (~) @ ( V0n = c_2Enum_2E0 ) )
% 1.76/1.34 | ( (~) @ ( V1m = c_2Enum_2E0 ) ) ) )
% 1.76/1.34 & ( ( c_2Einteger_2Eint__lt @ ( c_2Einteger_2Eint__of__num @ V0n ) @ ( c_2Einteger_2Eint__neg @ ( c_2Einteger_2Eint__of__num @ V1m ) ) )
% 1.76/1.34 = c_2Ebool_2EF ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Einteger_2ENUM__OF__INT,axiom,
% 1.76/1.34 ! [V0n: tyop_2Enum_2Enum] :
% 1.76/1.34 ( ( c_2Einteger_2ENum @ ( c_2Einteger_2Eint__of__num @ V0n ) )
% 1.76/1.34 = V0n ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Einteger__word_2Ei2w__def,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0i: tyop_2Einteger_2Eint] :
% 1.76/1.34 ( ( c_2Einteger__word_2Ei2w @ A_27a @ V0i )
% 1.76/1.34 = ( c_2Ebool_2ECOND @ ( tyop_2Efcp_2Ecart @ $o @ A_27a ) @ ( c_2Einteger_2Eint__lt @ V0i @ ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) @ ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ ( c_2Einteger_2ENum @ ( c_2Einteger_2Eint__neg @ V0i ) ) ) ) @ ( c_2Ewords_2En2w @ A_27a @ ( c_2Einteger_2ENum @ V0i ) ) ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Eprim__rec_2ENOT__LESS__0,axiom,
% 1.76/1.34 ! [V0n: tyop_2Enum_2Enum] : ( (~) @ ( c_2Eprim__rec_2E_3C @ V0n @ c_2Enum_2E0 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ewords_2En2w__11,axiom,
% 1.76/1.34 ! [A_27a: $tType,V0m: tyop_2Enum_2Enum,V1n: tyop_2Enum_2Enum] :
% 1.76/1.34 ( ( ( c_2Ewords_2En2w @ A_27a @ V0m )
% 1.76/1.34 = ( c_2Ewords_2En2w @ A_27a @ V1n ) )
% 1.76/1.34 <=> ( ( c_2Earithmetic_2EMOD @ V0m @ ( c_2Ewords_2Edimword @ A_27a @ ( c_2Ebool_2Ethe__value @ A_27a ) ) )
% 1.76/1.34 = ( c_2Earithmetic_2EMOD @ V1n @ ( c_2Ewords_2Edimword @ A_27a @ ( c_2Ebool_2Ethe__value @ A_27a ) ) ) ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Ewords_2EWORD__NEG__0,axiom,
% 1.76/1.34 ! [A_27a: $tType] :
% 1.76/1.34 ( ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ c_2Enum_2E0 ) )
% 1.76/1.34 = ( c_2Ewords_2En2w @ A_27a @ c_2Enum_2E0 ) ) ).
% 1.76/1.34
% 1.76/1.34 thf(thm_2Einteger__word_2Ei2w__0,conjecture,
% 1.76/1.34 ! [A_27a: $tType] :
% 1.76/1.34 ( ( c_2Einteger__word_2Ei2w @ A_27a @ ( c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
% 1.76/1.34 = ( c_2Ewords_2En2w @ A_27a @ c_2Enum_2E0 ) ) ).
% 1.76/1.34 ------------------------
% 1.76/1.36 % (4796)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_4447 for (2999ds/2Mi)
% 1.76/1.36 % (4795)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/2Mi)
% 1.76/1.36 % Exception at run slice level
% 1.76/1.36 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.36 % (4795)Instruction limit reached!
% 1.76/1.36 % (4795)------------------------------
% 1.76/1.36 % (4795)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.36 % (4795)Termination reason: Unknown
% 1.76/1.36 % (4795)Termination phase: Property scanning
% 1.76/1.36
% 1.76/1.36 % (4795)Memory used [KB]: 1023
% 1.76/1.36 % (4795)Time elapsed: 0.002 s
% 1.76/1.36 % (4795)Instructions burned: 2 (million)
% 1.76/1.36 % (4795)------------------------------
% 1.76/1.36 % (4795)------------------------------
% 1.76/1.36 % (4791)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/183Mi)
% 1.76/1.36 % (4792)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_4447 for (2999ds/4Mi)
% 1.76/1.36 % (4797)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_4447 for (2999ds/275Mi)
% 1.76/1.36 % (4794)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_4447 for (2999ds/27Mi)
% 1.76/1.37 % (4798)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/18Mi)
% 1.76/1.37 % (4792)Instruction limit reached!
% 1.76/1.37 % (4792)------------------------------
% 1.76/1.37 % (4792)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.37 % (4792)Termination reason: Unknown
% 1.76/1.37 % (4792)Termination phase: Property scanning
% 1.76/1.37
% 1.76/1.37 % (4792)Memory used [KB]: 1023
% 1.76/1.37 % (4792)Time elapsed: 0.004 s
% 1.76/1.37 % (4792)Instructions burned: 4 (million)
% 1.76/1.37 % (4792)------------------------------
% 1.76/1.37 % (4792)------------------------------
% 1.76/1.37 % (4801)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/3Mi)
% 1.76/1.37 % (4797)Refutation not found, incomplete strategy
% 1.76/1.37 % (4797)------------------------------
% 1.76/1.37 % (4797)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.37 % (4797)Termination reason: Refutation not found, incomplete strategy
% 1.76/1.37
% 1.76/1.37
% 1.76/1.37 % (4797)Memory used [KB]: 5500
% 1.76/1.37 % (4797)Time elapsed: 0.005 s
% 1.76/1.37 % (4797)Instructions burned: 4 (million)
% 1.76/1.37 % (4797)------------------------------
% 1.76/1.37 % (4797)------------------------------
% 1.76/1.37 % (4801)Instruction limit reached!
% 1.76/1.37 % (4801)------------------------------
% 1.76/1.37 % (4801)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.37 % (4801)Termination reason: Unknown
% 1.76/1.37 % (4801)Termination phase: Preprocessing 3
% 1.76/1.37
% 1.76/1.37 % (4801)Memory used [KB]: 1023
% 1.76/1.37 % (4801)Time elapsed: 0.002 s
% 1.76/1.37 % (4801)Instructions burned: 3 (million)
% 1.76/1.37 % (4801)------------------------------
% 1.76/1.37 % (4801)------------------------------
% 1.76/1.37 % (4802)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/37Mi)
% 1.76/1.37 % Exception at run slice level
% 1.76/1.37 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.38 % (4798)Instruction limit reached!
% 1.76/1.38 % (4798)------------------------------
% 1.76/1.38 % (4798)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.38 % (4798)Termination reason: Unknown
% 1.76/1.38 % (4798)Termination phase: Saturation
% 1.76/1.38
% 1.76/1.38 % (4798)Memory used [KB]: 5756
% 1.76/1.38 % (4798)Time elapsed: 0.014 s
% 1.76/1.38 % (4798)Instructions burned: 18 (million)
% 1.76/1.38 % (4798)------------------------------
% 1.76/1.38 % (4798)------------------------------
% 1.76/1.38 % (4809)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/3Mi)
% 1.76/1.38 % (4809)Instruction limit reached!
% 1.76/1.38 % (4809)------------------------------
% 1.76/1.38 % (4809)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.38 % (4809)Termination reason: Unknown
% 1.76/1.38 % (4809)Termination phase: Preprocessing 3
% 1.76/1.38
% 1.76/1.38 % (4809)Memory used [KB]: 1023
% 1.76/1.38 % (4809)Time elapsed: 0.002 s
% 1.76/1.38 % (4809)Instructions burned: 3 (million)
% 1.76/1.38 % (4809)------------------------------
% 1.76/1.38 % (4809)------------------------------
% 1.76/1.38 % (4810)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/1041Mi)
% 1.76/1.38 % Exception at run slice level
% 1.76/1.38 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.38 % (4807)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/15Mi)
% 1.76/1.38 % (4794)Instruction limit reached!
% 1.76/1.38 % (4794)------------------------------
% 1.76/1.38 % (4794)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.38 % (4794)Termination reason: Unknown
% 1.76/1.38 % (4794)Termination phase: Saturation
% 1.76/1.38
% 1.76/1.38 % (4794)Memory used [KB]: 5756
% 1.76/1.38 % (4794)Time elapsed: 0.021 s
% 1.76/1.38 % (4794)Instructions burned: 27 (million)
% 1.76/1.38 % (4794)------------------------------
% 1.76/1.38 % (4794)------------------------------
% 1.76/1.39 % (4811)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/7Mi)
% 1.76/1.39 % (4813)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/3Mi)
% 1.76/1.39 % (4813)Instruction limit reached!
% 1.76/1.39 % (4813)------------------------------
% 1.76/1.39 % (4813)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.39 % (4813)Termination reason: Unknown
% 1.76/1.39 % (4813)Termination phase: Preprocessing 3
% 1.76/1.39
% 1.76/1.39 % (4813)Memory used [KB]: 1023
% 1.76/1.39 % (4813)Time elapsed: 0.002 s
% 1.76/1.39 % (4813)Instructions burned: 3 (million)
% 1.76/1.39 % (4813)------------------------------
% 1.76/1.39 % (4813)------------------------------
% 1.76/1.39 % (4807)Refutation not found, incomplete strategy
% 1.76/1.39 % (4807)------------------------------
% 1.76/1.39 % (4807)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.39 % (4807)Termination reason: Refutation not found, incomplete strategy
% 1.76/1.39
% 1.76/1.39
% 1.76/1.39 % (4807)Memory used [KB]: 5628
% 1.76/1.39 % (4807)Time elapsed: 0.008 s
% 1.76/1.39 % (4807)Instructions burned: 10 (million)
% 1.76/1.39 % (4807)------------------------------
% 1.76/1.39 % (4807)------------------------------
% 1.76/1.39 % (4814)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/3Mi)
% 1.76/1.39 % (4811)Instruction limit reached!
% 1.76/1.39 % (4811)------------------------------
% 1.76/1.39 % (4811)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.39 % (4811)Termination reason: Unknown
% 1.76/1.39 % (4811)Termination phase: Saturation
% 1.76/1.39
% 1.76/1.39 % (4811)Memory used [KB]: 1023
% 1.76/1.39 % (4811)Time elapsed: 0.006 s
% 1.76/1.39 % (4811)Instructions burned: 7 (million)
% 1.76/1.39 % (4811)------------------------------
% 1.76/1.39 % (4811)------------------------------
% 1.76/1.39 % (4814)Instruction limit reached!
% 1.76/1.39 % (4814)------------------------------
% 1.76/1.39 % (4814)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.39 % (4814)Termination reason: Unknown
% 1.76/1.39 % (4814)Termination phase: Preprocessing 3
% 1.76/1.39
% 1.76/1.39 % (4814)Memory used [KB]: 1023
% 1.76/1.39 % (4814)Time elapsed: 0.003 s
% 1.76/1.39 % (4814)Instructions burned: 4 (million)
% 1.76/1.39 % (4814)------------------------------
% 1.76/1.39 % (4814)------------------------------
% 1.76/1.39 % (4812)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/16Mi)
% 1.83/1.40 % (4816)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/3Mi)
% 1.83/1.40 % Exception at run slice level
% 1.83/1.40 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.40 % (4819)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/710Mi)
% 1.83/1.40 % (4815)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/7Mi)
% 1.83/1.40 % (4812)Instruction limit reached!
% 1.83/1.40 % (4812)------------------------------
% 1.83/1.40 % (4812)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.40 % (4812)Termination reason: Unknown
% 1.83/1.40 % (4812)Termination phase: Saturation
% 1.83/1.40
% 1.83/1.40 % (4812)Memory used [KB]: 5628
% 1.83/1.40 % (4812)Time elapsed: 0.012 s
% 1.83/1.40 % (4812)Instructions burned: 16 (million)
% 1.83/1.40 % (4812)------------------------------
% 1.83/1.40 % (4812)------------------------------
% 1.83/1.41 % (4815)Instruction limit reached!
% 1.83/1.41 % (4815)------------------------------
% 1.83/1.41 % (4815)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.41 % (4815)Termination reason: Unknown
% 1.83/1.41 % (4815)Termination phase: Saturation
% 1.83/1.41
% 1.83/1.41 % (4815)Memory used [KB]: 5500
% 1.83/1.41 % (4815)Time elapsed: 0.007 s
% 1.83/1.41 % (4815)Instructions burned: 7 (million)
% 1.83/1.41 % (4815)------------------------------
% 1.83/1.41 % (4815)------------------------------
% 1.83/1.41 % (4817)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/4Mi)
% 1.83/1.41 % (4823)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/6Mi)
% 1.83/1.41 % (4818)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/18Mi)
% 1.83/1.41 % (4817)Instruction limit reached!
% 1.83/1.41 % (4817)------------------------------
% 1.83/1.41 % (4817)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.41 % (4817)Termination reason: Unknown
% 1.83/1.41 % (4817)Termination phase: Property scanning
% 1.83/1.41
% 1.83/1.41 % (4817)Memory used [KB]: 1023
% 1.83/1.41 % (4817)Time elapsed: 0.004 s
% 1.83/1.41 % (4817)Instructions burned: 4 (million)
% 1.83/1.41 % (4817)------------------------------
% 1.83/1.41 % (4817)------------------------------
% 1.83/1.41 % (4823)Instruction limit reached!
% 1.83/1.41 % (4823)------------------------------
% 1.83/1.41 % (4823)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.41 % (4823)Termination reason: Unknown
% 1.83/1.41 % (4823)Termination phase: Saturation
% 1.83/1.41
% 1.83/1.41 % (4823)Memory used [KB]: 5500
% 1.83/1.41 % (4823)Time elapsed: 0.003 s
% 1.83/1.41 % (4823)Instructions burned: 6 (million)
% 1.83/1.41 % (4823)------------------------------
% 1.83/1.41 % (4823)------------------------------
% 1.83/1.42 % (4831)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/6Mi)
% 1.83/1.42 % (4826)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/902Mi)
% 1.83/1.42 % (4818)Instruction limit reached!
% 1.83/1.42 % (4818)------------------------------
% 1.83/1.42 % (4818)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.42 % (4818)Termination reason: Unknown
% 1.83/1.42 % (4818)Termination phase: Saturation
% 1.83/1.42
% 1.83/1.42 % (4818)Memory used [KB]: 5628
% 1.83/1.42 % (4818)Time elapsed: 0.014 s
% 1.83/1.42 % (4818)Instructions burned: 19 (million)
% 1.83/1.42 % (4818)------------------------------
% 1.83/1.42 % (4818)------------------------------
% 1.83/1.42 % Exception at run slice level
% 1.83/1.42 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.42 % (4826)Refutation not found, incomplete strategy
% 1.83/1.42 % (4826)------------------------------
% 1.83/1.42 % (4826)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.42 % (4826)Termination reason: Refutation not found, incomplete strategy
% 1.83/1.42
% 1.83/1.42
% 1.83/1.42 % (4826)Memory used [KB]: 5628
% 1.83/1.42 % (4826)Time elapsed: 0.004 s
% 1.83/1.42 % (4826)Instructions burned: 7 (million)
% 1.83/1.42 % (4826)------------------------------
% 1.83/1.42 % (4826)------------------------------
% 1.83/1.42 % (4828)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/21Mi)
% 1.83/1.42 % (4819)Refutation not found, incomplete strategy
% 1.83/1.42 % (4819)------------------------------
% 1.83/1.42 % (4819)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.42 % (4819)Termination reason: Refutation not found, incomplete strategy
% 1.83/1.42
% 1.83/1.42
% 1.83/1.42 % (4819)Memory used [KB]: 5756
% 1.83/1.42 % (4819)Time elapsed: 0.025 s
% 1.83/1.42 % (4819)Instructions burned: 66 (million)
% 1.83/1.42 % (4819)------------------------------
% 1.83/1.42 % (4819)------------------------------
% 1.83/1.43 % (4830)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/5Mi)
% 1.83/1.43 % Exception at run slice level
% 1.83/1.43 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.43 % (4836)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/779Mi)
% 1.83/1.43 % Exception at run slice level
% 1.83/1.43 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.43 % (4837)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/19Mi)
% 1.83/1.44 % Exception at run slice level
% 1.83/1.44 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.44 % (4838)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/879Mi)
% 1.83/1.44 % (4835)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/377Mi)
% 1.83/1.44 % (4828)Instruction limit reached!
% 1.83/1.44 % (4828)------------------------------
% 1.83/1.44 % (4828)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.44 % (4828)Termination reason: Unknown
% 1.83/1.44 % (4828)Termination phase: Saturation
% 1.83/1.44
% 1.83/1.44 % (4828)Memory used [KB]: 5756
% 1.83/1.44 % (4828)Time elapsed: 0.016 s
% 1.83/1.44 % (4828)Instructions burned: 21 (million)
% 1.83/1.44 % (4828)------------------------------
% 1.83/1.44 % (4828)------------------------------
% 1.83/1.44 % (4840)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/3Mi)
% 1.83/1.44 % (4839)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/17Mi)
% 1.83/1.44 % (4840)Instruction limit reached!
% 1.83/1.44 % (4840)------------------------------
% 1.83/1.44 % (4840)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.44 % (4840)Termination reason: Unknown
% 1.83/1.44 % (4840)Termination phase: Preprocessing 3
% 1.83/1.44
% 1.83/1.44 % (4840)Memory used [KB]: 1023
% 1.83/1.44 % (4840)Time elapsed: 0.002 s
% 1.83/1.44 % (4840)Instructions burned: 3 (million)
% 1.83/1.44 % (4840)------------------------------
% 1.83/1.44 % (4840)------------------------------
% 1.83/1.45 % (4843)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/30Mi)
% 1.83/1.45 % (4791)Instruction limit reached!
% 1.83/1.45 % (4791)------------------------------
% 1.83/1.45 % (4791)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.45 % (4791)Termination reason: Unknown
% 1.83/1.45 % (4791)Termination phase: Saturation
% 1.83/1.45
% 1.83/1.45 % (4791)Memory used [KB]: 6652
% 1.83/1.45 % (4791)Time elapsed: 0.085 s
% 1.83/1.45 % (4791)Instructions burned: 183 (million)
% 1.83/1.45 % (4791)------------------------------
% 1.83/1.45 % (4791)------------------------------
% 1.83/1.45 % (4839)Instruction limit reached!
% 1.83/1.45 % (4839)------------------------------
% 1.83/1.45 % (4839)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.45 % (4839)Termination reason: Unknown
% 1.83/1.45 % (4839)Termination phase: Saturation
% 1.83/1.45
% 1.83/1.45 % (4839)Memory used [KB]: 5756
% 1.83/1.45 % (4839)Time elapsed: 0.029 s
% 1.83/1.45 % (4839)Instructions burned: 17 (million)
% 1.83/1.45 % (4839)------------------------------
% 1.83/1.45 % (4839)------------------------------
% 1.83/1.45 % (4848)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/100Mi)
% 1.83/1.46 % (4846)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_4447 for (2999ds/127Mi)
% 1.83/1.46 % (4843)Instruction limit reached!
% 1.83/1.46 % (4843)------------------------------
% 1.83/1.46 % (4843)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.46 % (4843)Termination reason: Unknown
% 1.83/1.46 % (4843)Termination phase: Saturation
% 1.83/1.46
% 1.83/1.46 % (4843)Memory used [KB]: 5756
% 1.83/1.46 % (4843)Time elapsed: 0.013 s
% 1.83/1.46 % (4843)Instructions burned: 31 (million)
% 1.83/1.46 % (4843)------------------------------
% 1.83/1.46 % (4843)------------------------------
% 1.83/1.46 % (4849)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/3Mi)
% 1.83/1.46 % (4850)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/20Mi)
% 1.83/1.46 % Exception at run slice level
% 1.83/1.46 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.47 % (4850)Instruction limit reached!
% 1.83/1.47 % (4850)------------------------------
% 1.83/1.47 % (4850)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.47 % (4850)Termination reason: Unknown
% 1.83/1.47 % (4850)Termination phase: Saturation
% 1.83/1.47
% 1.83/1.47 % (4850)Memory used [KB]: 5756
% 1.83/1.47 % (4850)Time elapsed: 0.010 s
% 1.83/1.47 % (4850)Instructions burned: 22 (million)
% 1.83/1.47 % (4850)------------------------------
% 1.83/1.47 % (4850)------------------------------
% 1.83/1.47 % (4852)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/86Mi)
% 1.83/1.47 % (4853)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/107Mi)
% 1.83/1.48 % (4858)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/39Mi)
% 1.83/1.48 % Exception at run slice level
% 1.83/1.48 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.48 % (4848)Instruction limit reached!
% 1.83/1.48 % (4848)------------------------------
% 1.83/1.48 % (4848)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.48 % (4848)Termination reason: Unknown
% 1.83/1.48 % (4848)Termination phase: Saturation
% 1.83/1.48
% 1.83/1.48 % (4848)Memory used [KB]: 6012
% 1.83/1.48 % (4848)Time elapsed: 0.056 s
% 1.83/1.48 % (4848)Instructions burned: 100 (million)
% 1.83/1.48 % (4848)------------------------------
% 1.83/1.48 % (4848)------------------------------
% 1.83/1.49 % (4863)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/448Mi)
% 1.83/1.49 % Exception at run slice level
% 1.83/1.49 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.49 % (4865)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/46Mi)
% 1.83/1.50 % (4853)First to succeed.
% 1.83/1.50 % (4868)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_4447 for (2998ds/98Mi)
% 1.83/1.50 % (4852)Instruction limit reached!
% 1.83/1.50 % (4852)------------------------------
% 1.83/1.50 % (4852)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.50 % (4852)Termination reason: Unknown
% 1.83/1.50 % (4852)Termination phase: Saturation
% 1.83/1.50
% 1.83/1.50 % (4852)Memory used [KB]: 6012
% 1.83/1.50 % (4852)Time elapsed: 0.033 s
% 1.83/1.50 % (4852)Instructions burned: 87 (million)
% 1.83/1.50 % (4852)------------------------------
% 1.83/1.50 % (4852)------------------------------
% 1.83/1.50 % Exception at run slice level
% 1.83/1.50 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.83/1.50 % (4853)Refutation found. Thanks to Tanya!
% 1.83/1.50 % SZS status Theorem for DTF2THF_4447
% 1.83/1.50 % SZS output start Proof for DTF2THF_4447
% 1.83/1.50 thf(type_def_6, type, tyop_2Enum_2Enum: $tType).
% 1.83/1.50 thf(type_def_7, type, tyop_2Einteger_2Eint: $tType).
% 1.83/1.50 thf(type_def_8, type, tyop_2Ebool_2Eitself: ($tType) > $tType).
% 1.83/1.50 thf(type_def_9, type, tyop_2Efcp_2Ecart: ($tType * $tType) > $tType).
% 1.83/1.50 thf(type_def_10, type, sK2: $tType).
% 1.83/1.50 thf(func_def_0, type, tyop_2Ebool_2Eitself: ($tType) > $tType).
% 1.83/1.50 thf(func_def_1, type, tyop_2Efcp_2Ecart: ($tType * $tType) > $tType).
% 1.83/1.50 thf(func_def_2, type, tyop_2Einteger_2Eint: $tType).
% 1.83/1.50 thf(func_def_3, type, tyop_2Emin_2Ebool: $tType).
% 1.83/1.50 thf(func_def_4, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 1.83/1.50 thf(func_def_5, type, tyop_2Enum_2Enum: $tType).
% 1.83/1.50 thf(func_def_6, type, c_2Ebool_2E_21: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.83/1.50 thf(func_def_7, type, c_2Ebool_2E_2F_5C: $o > $o > $o).
% 1.83/1.50 thf(func_def_8, type, c_2Enum_2E0: tyop_2Enum_2Enum).
% 1.83/1.50 thf(func_def_9, type, c_2Eprim__rec_2E_3C: tyop_2Enum_2Enum > tyop_2Enum_2Enum > $o).
% 1.83/1.50 thf(func_def_10, type, c_2Emin_2E_3D: !>[X0: $tType]:(X0 > X0 > $o)).
% 1.83/1.50 thf(func_def_11, type, c_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 1.83/1.50 thf(func_def_12, type, c_2Ebool_2E_3F: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.83/1.50 thf(func_def_13, type, c_2Ebool_2ECOND: !>[X0: $tType]:($o > X0 > X0 > X0)).
% 1.83/1.50 thf(func_def_15, type, c_2Earithmetic_2EMOD: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum).
% 1.83/1.50 thf(func_def_16, type, c_2Einteger_2ENum: tyop_2Einteger_2Eint > tyop_2Enum_2Enum).
% 1.83/1.50 thf(func_def_18, type, c_2Ebool_2E_5C_2F: $o > $o > $o).
% 1.83/1.50 thf(func_def_19, type, c_2Ewords_2Edimword: !>[X0: $tType]:(tyop_2Ebool_2Eitself @ X0 > tyop_2Enum_2Enum)).
% 1.83/1.50 thf(func_def_20, type, c_2Einteger__word_2Ei2w: !>[X0: $tType]:(tyop_2Einteger_2Eint > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.83/1.50 thf(func_def_21, type, c_2Einteger_2Eint__lt: tyop_2Einteger_2Eint > tyop_2Einteger_2Eint > $o).
% 1.83/1.50 thf(func_def_22, type, c_2Einteger_2Eint__neg: tyop_2Einteger_2Eint > tyop_2Einteger_2Eint).
% 1.83/1.50 thf(func_def_23, type, c_2Einteger_2Eint__of__num: tyop_2Enum_2Enum > tyop_2Einteger_2Eint).
% 1.83/1.50 thf(func_def_24, type, c_2Ewords_2En2w: !>[X0: $tType]:(tyop_2Enum_2Enum > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.83/1.50 thf(func_def_25, type, c_2Ebool_2Ethe__value: !>[X0: $tType]:(tyop_2Ebool_2Eitself @ X0)).
% 1.83/1.50 thf(func_def_26, type, c_2Ewords_2Eword__2comp: !>[X0: $tType]:(tyop_2Efcp_2Ecart @ $o @ X0 > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.83/1.50 thf(func_def_27, type, c_2Ebool_2E_7E: $o > $o).
% 1.83/1.50 thf(func_def_33, type, sP0: !>[X0: $tType]:(X0 > X0 > $o > $o)).
% 1.83/1.50 thf(func_def_34, type, sP1: $o > $o > $o).
% 1.83/1.50 thf(func_def_36, type, ph4: !>[X0: $tType]:(X0)).
% 1.83/1.50 thf(f428,plain,(
% 1.83/1.50 $false),
% 1.83/1.50 inference(avatar_sat_refutation,[status(thm)],[f178,f182,f190,f193,f310,f427])).
% 1.83/1.50 thf(f427,plain,(
% 1.83/1.50 ~spl3_2),
% 1.83/1.50 inference(avatar_contradiction_clause,[status(thm)],[f426])).
% 1.83/1.50 thf(f426,plain,(
% 1.83/1.50 $false | ~spl3_2),
% 1.83/1.50 inference(subsumption_resolution,[status(thm)],[f342,f411])).
% 1.83/1.50 thf(f411,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : ((c_2Enum_2E0 = X0)) ) | ~spl3_2),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f382])).
% 1.83/1.50 thf(f382,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : ((c_2Enum_2E0 = X0) | ($true = $false)) ) | ~spl3_2),
% 1.83/1.50 inference(backward_demodulation,[status(thm)],[f159,f354])).
% 1.83/1.50 thf(f354,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (($false = X0)) ) | ~spl3_2),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f334])).
% 1.83/1.50 thf(f334,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (($true = $false) | ($false = X0)) ) | ~spl3_2),
% 1.83/1.50 inference(superposition,[status(thm)],[f168,f177])).
% 1.83/1.50 thf(f177,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (($true = X0)) ) | ~spl3_2),
% 1.83/1.50 inference(avatar_component_clause,[status(thm)],[f176])).
% 1.83/1.50 thf(f176,definition,(
% 1.83/1.50 spl3_2 <=> ! [X0 : $o] : ($true = X0)),
% 1.83/1.50 introduced(definition,[new_symbols(naming,[spl3_2])],[avatar_definition])).
% 1.83/1.50 thf(f168,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (((c_2Ebool_2E_7E @ X0) = $false) | ($false = X0)) )),
% 1.83/1.50 inference(not_proxy_clausification,[status(thm)],[f165])).
% 1.83/1.50 thf(f165,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (((c_2Ebool_2E_7E @ X0) = $false) | ((~ X0) = $true)) )),
% 1.83/1.50 inference(binary_proxy_clausification,[status(thm)],[f120])).
% 1.83/1.50 thf(f120,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (((~ X0) = (c_2Ebool_2E_7E @ X0))) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f53])).
% 1.83/1.50 thf(f53,plain,(
% 1.83/1.50 ! [X0 : $o] : ((~ X0) = (c_2Ebool_2E_7E @ X0))),
% 1.83/1.50 inference(fool_elimination,[status(thm)],[f52])).
% 1.83/1.50 thf(f52,plain,(
% 1.83/1.50 ! [X0 : $o] : ((c_2Ebool_2E_7E @ X0) <=> (~ X0))),
% 1.83/1.50 inference(rectify,[status(thm)],[f3])).
% 1.83/1.50 thf(f3,axiom,(
% 1.83/1.50 ! [X1 : $o] : ((c_2Ebool_2E_7E @ X1) <=> (~ X1))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',logicdef_2E_7E)).
% 1.83/1.50 thf(f159,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | (c_2Enum_2E0 = X0)) )),
% 1.83/1.50 inference(equality_proxy_clausification,[status(thm)],[f158])).
% 1.83/1.50 thf(f158,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true = (c_2Enum_2E0 = X0)) | ($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1)))) )),
% 1.83/1.50 inference(not_proxy_clausification,[status(thm)],[f114])).
% 1.83/1.50 thf(f114,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true != (~ (c_2Enum_2E0 = X0))) | ($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1)))) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f84])).
% 1.83/1.50 thf(f84,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__of__num @ X1)) = (c_2Eprim__rec_2E_3C @ X0 @ X1)) & (c_2Ebool_2EF = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & ((c_2Eprim__rec_2E_3C @ X1 @ X0) = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & (($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | (($true != (~ (c_2Enum_2E0 = X1))) & ($true != (~ (c_2Enum_2E0 = X0))))) & (($true = (~ (c_2Enum_2E0 = X1))) | ($true = (~ (c_2Enum_2E0 = X0))) | ($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1)))))),
% 1.83/1.50 inference(flattening,[status(thm)],[f83])).
% 1.83/1.50 thf(f83,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__of__num @ X1)) = (c_2Eprim__rec_2E_3C @ X0 @ X1)) & (c_2Ebool_2EF = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & ((c_2Eprim__rec_2E_3C @ X1 @ X0) = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & ((($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | (($true != (~ (c_2Enum_2E0 = X1))) & ($true != (~ (c_2Enum_2E0 = X0))))) & ((($true = (~ (c_2Enum_2E0 = X1))) | ($true = (~ (c_2Enum_2E0 = X0)))) | ($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))))))),
% 1.83/1.50 inference(nnf_transformation,[status(thm)],[f51])).
% 1.83/1.50 thf(f51,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__of__num @ X1)) = (c_2Eprim__rec_2E_3C @ X0 @ X1)) & (c_2Ebool_2EF = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & ((c_2Eprim__rec_2E_3C @ X1 @ X0) = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & (($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) <=> (($true = (~ (c_2Enum_2E0 = X1))) | ($true = (~ (c_2Enum_2E0 = X0))))))),
% 1.83/1.50 inference(fool_elimination,[status(thm)],[f50])).
% 1.83/1.50 thf(f50,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ((c_2Ebool_2EF = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))) & ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1)) <=> ((~ (c_2Enum_2E0 = X0)) | (~ (c_2Enum_2E0 = X1)))) & ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__of__num @ X1)) = (c_2Eprim__rec_2E_3C @ X0 @ X1)) & ((c_2Eprim__rec_2E_3C @ X1 @ X0) = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1)))))),
% 1.83/1.50 inference(rectify,[status(thm)],[f17])).
% 1.83/1.50 thf(f17,axiom,(
% 1.83/1.50 ! [X19 : tyop_2Enum_2Enum,X20 : tyop_2Enum_2Enum] : ((c_2Ebool_2EF = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X19) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X20)))) & ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X19)) @ (c_2Einteger_2Eint__of__num @ X20)) <=> ((~ (c_2Enum_2E0 = X19)) | (~ (c_2Enum_2E0 = X20)))) & ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X19) @ (c_2Einteger_2Eint__of__num @ X20)) = (c_2Eprim__rec_2E_3C @ X19 @ X20)) & ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X19)) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X20))) = (c_2Eprim__rec_2E_3C @ X20 @ X19)))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Einteger_2EINT__LT__CALCULATE)).
% 1.83/1.50 thf(f342,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : ((c_2Enum_2E0 != X0)) ) | ~spl3_2),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f341])).
% 1.83/1.50 thf(f341,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : (($true != $true) | (c_2Enum_2E0 != X0)) ) | ~spl3_2),
% 1.83/1.50 inference(superposition,[status(thm)],[f215,f177])).
% 1.83/1.50 thf(f215,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : (($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0) @ (c_2Einteger_2Eint__of__num @ X0))) | (c_2Enum_2E0 != X0)) )),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f212])).
% 1.83/1.50 thf(f212,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : ((c_2Enum_2E0 != X0) | (c_2Enum_2E0 != c_2Enum_2E0) | ($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0) @ (c_2Einteger_2Eint__of__num @ X0)))) )),
% 1.83/1.50 inference(superposition,[status(thm)],[f163,f119])).
% 1.83/1.50 thf(f119,plain,(
% 1.83/1.50 ((c_2Einteger_2Eint__of__num @ c_2Enum_2E0) = (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)))),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f16])).
% 1.83/1.50 thf(f16,axiom,(
% 1.83/1.50 ((c_2Einteger_2Eint__of__num @ c_2Enum_2E0) = (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Einteger_2EINT__NEG__0)).
% 1.83/1.50 thf(f163,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | (c_2Enum_2E0 != X1) | (c_2Enum_2E0 != X0)) )),
% 1.83/1.50 inference(equality_proxy_clausification,[status(thm)],[f162])).
% 1.83/1.50 thf(f162,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | (c_2Enum_2E0 != X0) | ($false = (c_2Enum_2E0 = X1))) )),
% 1.83/1.50 inference(not_proxy_clausification,[status(thm)],[f161])).
% 1.83/1.50 thf(f161,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ((c_2Enum_2E0 != X0) | ($true = (~ (c_2Enum_2E0 = X1))) | ($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1)))) )),
% 1.83/1.50 inference(equality_proxy_clausification,[status(thm)],[f160])).
% 1.83/1.50 thf(f160,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Enum_2E0 = X0) = $false) | ($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | ($true = (~ (c_2Enum_2E0 = X1)))) )),
% 1.83/1.50 inference(not_proxy_clausification,[status(thm)],[f113])).
% 1.83/1.50 thf(f113,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true = (~ (c_2Enum_2E0 = X0))) | ($true != (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0)) @ (c_2Einteger_2Eint__of__num @ X1))) | ($true = (~ (c_2Enum_2E0 = X1)))) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f84])).
% 1.83/1.50 thf(f310,plain,(
% 1.83/1.50 ~spl3_5),
% 1.83/1.50 inference(avatar_contradiction_clause,[status(thm)],[f309])).
% 1.83/1.50 thf(f309,plain,(
% 1.83/1.50 $false | ~spl3_5),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f308])).
% 1.83/1.50 thf(f308,plain,(
% 1.83/1.50 ((c_2Ewords_2En2w @ sK2 @ c_2Enum_2E0) != (c_2Ewords_2En2w @ sK2 @ c_2Enum_2E0)) | ~spl3_5),
% 1.83/1.50 inference(superposition,[status(thm)],[f97,f300])).
% 1.83/1.50 thf(f300,plain,(
% 1.83/1.50 ( ! [X1 : $tType,X0 : tyop_2Enum_2Enum] : (((c_2Einteger__word_2Ei2w @ X1 @ (c_2Einteger_2Eint__of__num @ X0)) = (c_2Ewords_2En2w @ X1 @ X0))) ) | ~spl3_5),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f299])).
% 1.83/1.50 thf(f299,plain,(
% 1.83/1.50 ( ! [X1 : $tType,X0 : tyop_2Enum_2Enum] : (($true = $false) | ((c_2Einteger__word_2Ei2w @ X1 @ (c_2Einteger_2Eint__of__num @ X0)) = (c_2Ewords_2En2w @ X1 @ X0))) ) | ~spl3_5),
% 1.83/1.50 inference(forward_demodulation,[status(thm)],[f298,f164])).
% 1.83/1.50 thf(f164,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : (((c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0) = $false)) )),
% 1.83/1.50 inference(not_proxy_clausification,[status(thm)],[f86])).
% 1.83/1.50 thf(f86,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : (((~ (c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0)) = $true)) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f41])).
% 1.83/1.50 thf(f41,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum] : ((~ (c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0)) = $true)),
% 1.83/1.50 inference(fool_elimination,[status(thm)],[f40])).
% 1.83/1.50 thf(f40,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum] : (~ (c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0))),
% 1.83/1.50 inference(rectify,[status(thm)],[f20])).
% 1.83/1.50 thf(f20,axiom,(
% 1.83/1.50 ! [X19 : tyop_2Enum_2Enum] : (~ (c_2Eprim__rec_2E_3C @ X19 @ c_2Enum_2E0))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Eprim__rec_2ENOT__LESS__0)).
% 1.83/1.50 thf(f298,plain,(
% 1.83/1.50 ( ! [X1 : $tType,X0 : tyop_2Enum_2Enum] : (($true = (c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0)) | ((c_2Einteger__word_2Ei2w @ X1 @ (c_2Einteger_2Eint__of__num @ X0)) = (c_2Ewords_2En2w @ X1 @ X0))) ) | ~spl3_5),
% 1.83/1.50 inference(forward_demodulation,[status(thm)],[f297,f195])).
% 1.83/1.50 thf(f195,plain,(
% 1.83/1.50 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ $false @ X1 @ X2) = X2)) ) | ~spl3_5),
% 1.83/1.50 inference(backward_demodulation,[status(thm)],[f92,f189])).
% 1.83/1.50 thf(f189,plain,(
% 1.83/1.50 (c_2Ebool_2EF = $false) | ~spl3_5),
% 1.83/1.50 inference(avatar_component_clause,[status(thm)],[f187])).
% 1.83/1.50 thf(f187,definition,(
% 1.83/1.50 spl3_5 <=> (c_2Ebool_2EF = $false)),
% 1.83/1.50 introduced(definition,[new_symbols(naming,[spl3_5])],[avatar_definition])).
% 1.83/1.50 thf(f92,plain,(
% 1.83/1.50 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2) = X2)) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f57])).
% 1.83/1.50 thf(f57,plain,(
% 1.83/1.50 ! [X0 : $tType] : (! [X1 : X0,X2 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2) = X2) & ! [X3 : X0,X4 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X3 @ X4) = X3))),
% 1.83/1.50 inference(rectify,[status(thm)],[f15])).
% 1.83/1.50 thf(f15,axiom,(
% 1.83/1.50 ! [X0 : $tType] : (! [X17 : X0,X18 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X17 @ X18) = X18) & ! [X5 : X0,X6 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X5 @ X6) = X5))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Ebool_2Ebool__case__thm)).
% 1.83/1.50 thf(f297,plain,(
% 1.83/1.50 ( ! [X1 : $tType,X0 : tyop_2Enum_2Enum] : (($true = (c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0)) | ((c_2Einteger__word_2Ei2w @ X1 @ (c_2Einteger_2Eint__of__num @ X0)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X1 @ $false @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0))))) @ (c_2Ewords_2En2w @ X1 @ X0)))) )),
% 1.83/1.50 inference(forward_demodulation,[status(thm)],[f286,f94])).
% 1.83/1.50 thf(f94,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum] : (((c_2Einteger_2ENum @ (c_2Einteger_2Eint__of__num @ X0)) = X0)) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f58])).
% 1.83/1.50 thf(f58,plain,(
% 1.83/1.50 ! [X0 : tyop_2Enum_2Enum] : ((c_2Einteger_2ENum @ (c_2Einteger_2Eint__of__num @ X0)) = X0)),
% 1.83/1.50 inference(rectify,[status(thm)],[f18])).
% 1.83/1.50 thf(f18,axiom,(
% 1.83/1.50 ! [X19 : tyop_2Enum_2Enum] : ((c_2Einteger_2ENum @ (c_2Einteger_2Eint__of__num @ X19)) = X19)),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Einteger_2ENUM__OF__INT)).
% 1.83/1.50 thf(f286,plain,(
% 1.83/1.50 ( ! [X1 : $tType,X0 : tyop_2Enum_2Enum] : (((c_2Einteger__word_2Ei2w @ X1 @ (c_2Einteger_2Eint__of__num @ X0)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X1 @ $false @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X0))))) @ (c_2Ewords_2En2w @ X1 @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__of__num @ X0))))) | ($true = (c_2Eprim__rec_2E_3C @ X0 @ c_2Enum_2E0))) )),
% 1.83/1.50 inference(superposition,[status(thm)],[f96,f154])).
% 1.83/1.50 thf(f154,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__of__num @ X1)) = $false) | ($true = (c_2Eprim__rec_2E_3C @ X0 @ X1))) )),
% 1.83/1.50 inference(binary_proxy_clausification,[status(thm)],[f118])).
% 1.83/1.50 thf(f118,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__of__num @ X1)) = (c_2Eprim__rec_2E_3C @ X0 @ X1))) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f84])).
% 1.83/1.50 thf(f96,plain,(
% 1.83/1.50 ( ! [X0 : $tType,X1 : tyop_2Einteger_2Eint] : (((c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ (c_2Einteger_2Eint__lt @ X1 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__neg @ X1)))) @ (c_2Ewords_2En2w @ X0 @ (c_2Einteger_2ENum @ X1))) = (c_2Einteger__word_2Ei2w @ X0 @ X1))) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f59])).
% 1.83/1.50 thf(f59,plain,(
% 1.83/1.50 ! [X0 : $tType,X1 : tyop_2Einteger_2Eint] : ((c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ (c_2Einteger_2Eint__lt @ X1 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__neg @ X1)))) @ (c_2Ewords_2En2w @ X0 @ (c_2Einteger_2ENum @ X1))) = (c_2Einteger__word_2Ei2w @ X0 @ X1))),
% 1.83/1.50 inference(rectify,[status(thm)],[f19])).
% 1.83/1.50 thf(f19,axiom,(
% 1.83/1.50 ! [X0 : $tType,X21 : tyop_2Einteger_2Eint] : ((c_2Einteger__word_2Ei2w @ X0 @ X21) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ (c_2Einteger_2Eint__lt @ X21 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Einteger_2ENum @ (c_2Einteger_2Eint__neg @ X21)))) @ (c_2Ewords_2En2w @ X0 @ (c_2Einteger_2ENum @ X21))))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Einteger__word_2Ei2w__def)).
% 1.83/1.50 thf(f97,plain,(
% 1.83/1.50 ((c_2Einteger__word_2Ei2w @ sK2 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) != (c_2Ewords_2En2w @ sK2 @ c_2Enum_2E0))),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f76])).
% 1.83/1.50 thf(f76,plain,(
% 1.83/1.50 ((c_2Einteger__word_2Ei2w @ sK2 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) != (c_2Ewords_2En2w @ sK2 @ c_2Enum_2E0))),
% 1.83/1.50 inference(skolemisation,[status(esa),new_symbols(skolem,[sK2])],[f66,f75])).
% 1.83/1.50 thf(f75,plain,(
% 1.83/1.50 ? [X0 : $tType] : ((c_2Ewords_2En2w @ X0 @ c_2Enum_2E0) != (c_2Einteger__word_2Ei2w @ X0 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0))) => ((c_2Einteger__word_2Ei2w @ sK2 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) != (c_2Ewords_2En2w @ sK2 @ c_2Enum_2E0))),
% 1.83/1.50 introduced(definition,[],[choice_axiom])).
% 1.83/1.50 thf(f66,plain,(
% 1.83/1.50 ? [X0 : $tType] : ((c_2Ewords_2En2w @ X0 @ c_2Enum_2E0) != (c_2Einteger__word_2Ei2w @ X0 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)))),
% 1.83/1.50 inference(ennf_transformation,[status(thm)],[f24])).
% 1.83/1.50 thf(f24,negated_conjecture,(
% 1.83/1.50 ~! [X0 : $tType] : ((c_2Ewords_2En2w @ X0 @ c_2Enum_2E0) = (c_2Einteger__word_2Ei2w @ X0 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)))),
% 1.83/1.50 inference(negated_conjecture,[status(cth)],[f23])).
% 1.83/1.50 thf(f23,conjecture,(
% 1.83/1.50 ! [X0 : $tType] : ((c_2Ewords_2En2w @ X0 @ c_2Enum_2E0) = (c_2Einteger__word_2Ei2w @ X0 @ (c_2Einteger_2Eint__of__num @ c_2Enum_2E0)))),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Einteger__word_2Ei2w__0)).
% 1.83/1.50 thf(f193,plain,(
% 1.83/1.50 ~spl3_3 | ~spl3_4),
% 1.83/1.50 inference(avatar_contradiction_clause,[status(thm)],[f192])).
% 1.83/1.50 thf(f192,plain,(
% 1.83/1.50 $false | (~spl3_3 | ~spl3_4)),
% 1.83/1.50 inference(trivial_inequality_removal,[status(thm)],[f191])).
% 1.83/1.50 thf(f191,plain,(
% 1.83/1.50 ($true = $false) | (~spl3_3 | ~spl3_4)),
% 1.83/1.50 inference(forward_demodulation,[status(thm)],[f185,f181])).
% 1.83/1.50 thf(f181,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))) = $false)) ) | ~spl3_3),
% 1.83/1.50 inference(avatar_component_clause,[status(thm)],[f180])).
% 1.83/1.50 thf(f180,definition,(
% 1.83/1.50 spl3_3 <=> ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))) = $false)),
% 1.83/1.50 introduced(definition,[new_symbols(naming,[spl3_3])],[avatar_definition])).
% 1.83/1.50 thf(f185,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : (($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))))) ) | ~spl3_4),
% 1.83/1.50 inference(avatar_component_clause,[status(thm)],[f184])).
% 1.83/1.50 thf(f184,definition,(
% 1.83/1.50 spl3_4 <=> ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))))),
% 1.83/1.50 introduced(definition,[new_symbols(naming,[spl3_4])],[avatar_definition])).
% 1.83/1.50 thf(f190,plain,(
% 1.83/1.50 spl3_4 | spl3_5),
% 1.83/1.50 inference(avatar_split_clause,[status(thm)],[f156,f187,f184])).
% 1.83/1.50 thf(f156,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ((c_2Ebool_2EF = $false) | ($true = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))))) )),
% 1.83/1.50 inference(binary_proxy_clausification,[status(thm)],[f117])).
% 1.83/1.50 thf(f117,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ((c_2Ebool_2EF = (c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))))) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f84])).
% 1.83/1.50 thf(f182,plain,(
% 1.83/1.50 spl3_3 | spl3_1),
% 1.83/1.50 inference(avatar_split_clause,[status(thm)],[f155,f172,f180])).
% 1.83/1.50 thf(f172,definition,(
% 1.83/1.50 spl3_1 <=> (c_2Ebool_2EF = $true)),
% 1.83/1.50 introduced(definition,[new_symbols(naming,[spl3_1])],[avatar_definition])).
% 1.83/1.50 thf(f155,plain,(
% 1.83/1.50 ( ! [X0 : tyop_2Enum_2Enum,X1 : tyop_2Enum_2Enum] : ((c_2Ebool_2EF = $true) | ((c_2Einteger_2Eint__lt @ (c_2Einteger_2Eint__of__num @ X0) @ (c_2Einteger_2Eint__neg @ (c_2Einteger_2Eint__of__num @ X1))) = $false)) )),
% 1.83/1.50 inference(binary_proxy_clausification,[status(thm)],[f117])).
% 1.83/1.50 thf(f178,plain,(
% 1.83/1.50 ~spl3_1 | spl3_2),
% 1.83/1.50 inference(avatar_split_clause,[status(thm)],[f93,f176,f172])).
% 1.83/1.50 thf(f93,plain,(
% 1.83/1.50 ( ! [X0 : $o] : (($true = X0) | (c_2Ebool_2EF != $true)) )),
% 1.83/1.50 inference(cnf_transformation,[status(thm)],[f61])).
% 1.83/1.50 thf(f61,plain,(
% 1.83/1.50 ! [X0 : $o] : ((c_2Ebool_2EF != $true) | ($true = X0))),
% 1.83/1.50 inference(ennf_transformation,[status(thm)],[f49])).
% 1.83/1.50 thf(f49,plain,(
% 1.83/1.50 ! [X0 : $o] : ((c_2Ebool_2EF = $true) => ($true = X0))),
% 1.83/1.50 inference(fool_elimination,[status(thm)],[f48])).
% 1.83/1.50 thf(f48,plain,(
% 1.83/1.50 ! [X0 : $o] : (c_2Ebool_2EF => X0)),
% 1.83/1.50 inference(rectify,[status(thm)],[f10])).
% 1.83/1.50 thf(f10,axiom,(
% 1.83/1.50 ! [X7 : $o] : (c_2Ebool_2EF => X7)),
% 1.83/1.50 file('/export/starexec/sandbox2/tmp/tmp.seHL8kzcNJ/DTF2THF_4447.p',thm_2Ebool_2EFALSITY)).
% 1.83/1.50 % SZS output end Proof for DTF2THF_4447
% 1.83/1.50 % (4853)------------------------------
% 1.83/1.50 % (4853)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.50 % (4853)Termination reason: Refutation
% 1.83/1.50
% 1.83/1.50 % (4853)Memory used [KB]: 5884
% 1.83/1.50 % (4853)Time elapsed: 0.031 s
% 1.83/1.50 % (4853)Instructions burned: 82 (million)
% 1.83/1.50 % (4853)------------------------------
% 1.83/1.50 % (4853)------------------------------
% 1.83/1.50 % (4789)Success in time 0.156 s
%------------------------------------------------------------------------------