%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP015^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:04:03 AM UTC 2026
% Result : Theorem 18.37s 2.96s
% Output : CNFRefutation 18.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 24
% Syntax : Number of formulae : 104 ( 78 unt; 0 typ; 0 def)
% Number of atoms : 190 ( 72 equ; 0 cnn)
% Maximal formula atoms : 19 ( 1 avg)
% Number of connectives : 1196 ( 58 ~; 43 |; 18 &;1059 @)
% ( 8 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Number of types : 5 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 33 ( 30 usr; 15 con; 0-2 aty)
% Number of variables : 104 ( 0 ^; 104 !; 0 ?; 104 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
del: $tType ).
thf(decl_sort2,type,
tp__ty_2Einteger_2Eint: $tType ).
thf(decl_sort3,type,
tp__ty_2Enum_2Enum: $tType ).
thf(decl_23,type,
bool: del ).
thf(decl_25,type,
arr: del > del > del ).
thf(decl_26,type,
mem: $i > del > $o ).
thf(decl_27,type,
ap: $i > $i > $i ).
thf(decl_29,type,
p: $i > $o ).
thf(decl_30,type,
inj__o: $o > $i ).
thf(decl_32,type,
c_2Ebool_2ET: $i ).
thf(decl_33,type,
c_2Ebool_2EF: $i ).
thf(decl_36,type,
ty_2Einteger_2Eint: del ).
thf(decl_37,type,
inj__ty_2Einteger_2Eint: tp__ty_2Einteger_2Eint > $i ).
thf(decl_38,type,
surj__ty_2Einteger_2Eint: $i > tp__ty_2Einteger_2Eint ).
thf(decl_39,type,
c_2Einteger_2Eint__neg: $i ).
thf(decl_40,type,
fo__c_2Einteger_2Eint__neg: tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint ).
thf(decl_41,type,
ty_2Enum_2Enum: del ).
thf(decl_42,type,
inj__ty_2Enum_2Enum: tp__ty_2Enum_2Enum > $i ).
thf(decl_43,type,
surj__ty_2Enum_2Enum: $i > tp__ty_2Enum_2Enum ).
thf(decl_44,type,
c_2Einteger_2ENum: $i ).
thf(decl_45,type,
fo__c_2Einteger_2ENum: tp__ty_2Einteger_2Eint > tp__ty_2Enum_2Enum ).
thf(decl_46,type,
c_2Einteger_2Eint__of__num: $i ).
thf(decl_47,type,
fo__c_2Einteger_2Eint__of__num: tp__ty_2Enum_2Enum > tp__ty_2Einteger_2Eint ).
thf(decl_48,type,
c_2Einteger_2Eint__lt: $i ).
thf(decl_49,type,
c_2Ebool_2ECOND: del > $i ).
thf(decl_50,type,
ty_2Efcp_2Ecart: del > del > del ).
thf(decl_51,type,
c_2Einteger__word_2Ei2w: del > $i ).
thf(decl_52,type,
c_2Eprim__rec_2E_3C: $i ).
thf(decl_60,type,
c_2Enum_2E0: $i ).
thf(decl_61,type,
fo__c_2Enum_2E0: tp__ty_2Enum_2Enum ).
thf(decl_62,type,
c_2Ewords_2En2w: del > $i ).
thf(decl_63,type,
c_2Ewords_2Eword__2comp: del > $i ).
thf(decl_65,type,
esk1_0: del ).
thf(conj_thm_2Eprim__rec_2ENOT__LESS__0,axiom,
! [X43: tp__ty_2Enum_2Enum] :
~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X43 ) ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Eprim__rec_2ENOT__LESS__0) ).
thf(stp_iso_mem_o,axiom,
! [X2: $i] :
( ( mem @ X2 @ bool )
=> ( X2
= ( inj__o @ ( p @ X2 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_iso_mem_o) ).
thf(ax_false_p,axiom,
~ ( p @ c_2Ebool_2EF ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',ax_false_p) ).
thf(conj_thm_2Einteger_2EINT__LT__CALCULATE,axiom,
! [X43: tp__ty_2Enum_2Enum,X44: tp__ty_2Enum_2Enum] :
( ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) )
<=> ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X43 ) ) @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) )
& ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) ) )
<=> ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X44 ) ) @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) )
& ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) )
<=> ( ( X43 != fo__c_2Enum_2E0 )
| ( X44 != fo__c_2Enum_2E0 ) ) )
& ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) ) )
<=> ~ $true ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Einteger_2EINT__LT__CALCULATE) ).
thf(stp_inj_surj_ty_2Einteger_2Eint,axiom,
! [X15: tp__ty_2Einteger_2Eint] :
( ( surj__ty_2Einteger_2Eint @ ( inj__ty_2Einteger_2Eint @ X15 ) )
= X15 ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_inj_surj_ty_2Einteger_2Eint) ).
thf(stp_eq_fo_c_2Einteger_2Eint__of__num,axiom,
! [X22: tp__ty_2Enum_2Enum] :
( ( inj__ty_2Einteger_2Eint @ ( fo__c_2Einteger_2Eint__of__num @ X22 ) )
= ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X22 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_eq_fo_c_2Einteger_2Eint__of__num) ).
thf(stp_inj_mem_ty_2Einteger_2Eint,axiom,
! [X16: tp__ty_2Einteger_2Eint] : ( mem @ ( inj__ty_2Einteger_2Eint @ X16 ) @ ty_2Einteger_2Eint ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_inj_mem_ty_2Einteger_2Eint) ).
thf(stp_eq_fo_c_2Einteger_2Eint__neg,axiom,
! [X18: tp__ty_2Einteger_2Eint] :
( ( inj__ty_2Einteger_2Eint @ ( fo__c_2Einteger_2Eint__neg @ X18 ) )
= ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X18 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_eq_fo_c_2Einteger_2Eint__neg) ).
thf(stp_inj_mem_ty_2Enum_2Enum,axiom,
! [X20: tp__ty_2Enum_2Enum] : ( mem @ ( inj__ty_2Enum_2Enum @ X20 ) @ ty_2Enum_2Enum ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_inj_mem_ty_2Enum_2Enum) ).
thf(stp_eq_fo_c_2Einteger_2ENum,axiom,
! [X18: tp__ty_2Einteger_2Eint] :
( ( inj__ty_2Enum_2Enum @ ( fo__c_2Einteger_2ENum @ X18 ) )
= ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X18 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_eq_fo_c_2Einteger_2ENum) ).
thf(stp_eq_fo_c_2Enum_2E0,axiom,
( ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 )
= c_2Enum_2E0 ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_eq_fo_c_2Enum_2E0) ).
thf(mem_c_2Ebool_2EF,axiom,
mem @ c_2Ebool_2EF @ bool,
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',mem_c_2Ebool_2EF) ).
thf(ap_tp,axiom,
! [X3: del,X4: del,X5: $i] :
( ( mem @ X5 @ ( arr @ X3 @ X4 ) )
=> ! [X6: $i] :
( ( mem @ X6 @ X3 )
=> ( mem @ ( ap @ X5 @ X6 ) @ X4 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',ap_tp) ).
thf(mem_c_2Einteger_2Eint__lt,axiom,
mem @ c_2Einteger_2Eint__lt @ ( arr @ ty_2Einteger_2Eint @ ( arr @ ty_2Einteger_2Eint @ bool ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',mem_c_2Einteger_2Eint__lt) ).
thf(conj_thm_2Einteger_2ENUM__OF__INT,axiom,
! [X43: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) )
= X43 ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Einteger_2ENUM__OF__INT) ).
thf(ax_thm_2Einteger__word_2Ei2w__def,axiom,
! [X23: del,X45: tp__ty_2Einteger_2Eint] :
( ( ap @ ( c_2Einteger__word_2Ei2w @ X23 ) @ ( inj__ty_2Einteger_2Eint @ X45 ) )
= ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ ( ty_2Efcp_2Ecart @ bool @ X23 ) ) @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( inj__ty_2Einteger_2Eint @ X45 ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) ) @ ( ap @ ( c_2Ewords_2Eword__2comp @ X23 ) @ ( ap @ ( c_2Ewords_2En2w @ X23 ) @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X45 ) ) ) ) ) ) @ ( ap @ ( c_2Ewords_2En2w @ X23 ) @ ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X45 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',ax_thm_2Einteger__word_2Ei2w__def) ).
thf(stp_iso_mem_ty_2Einteger_2Eint,axiom,
! [X17: $i] :
( ( mem @ X17 @ ty_2Einteger_2Eint )
=> ( X17
= ( inj__ty_2Einteger_2Eint @ ( surj__ty_2Einteger_2Eint @ X17 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_iso_mem_ty_2Einteger_2Eint) ).
thf(conj_thm_2Einteger_2EINT__NEG__0,axiom,
( ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) )
= ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Einteger_2EINT__NEG__0) ).
thf(stp_iso_mem_ty_2Enum_2Enum,axiom,
! [X21: $i] :
( ( mem @ X21 @ ty_2Enum_2Enum )
=> ( X21
= ( inj__ty_2Enum_2Enum @ ( surj__ty_2Enum_2Enum @ X21 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',stp_iso_mem_ty_2Enum_2Enum) ).
thf(conj_thm_2Ewords_2EWORD__NEG__0,axiom,
! [X23: del] :
( ( ap @ ( c_2Ewords_2Eword__2comp @ X23 ) @ ( ap @ ( c_2Ewords_2En2w @ X23 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
= ( ap @ ( c_2Ewords_2En2w @ X23 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Ewords_2EWORD__NEG__0) ).
thf(conj_thm_2Einteger__word_2Ei2w__0,conjecture,
! [X23: del] :
( ( ap @ ( c_2Einteger__word_2Ei2w @ X23 ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
= ( ap @ ( c_2Ewords_2En2w @ X23 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Einteger__word_2Ei2w__0) ).
thf(conj_thm_2Ebool_2Ebool__case__thm,axiom,
! [X23: del] :
( ! [X29: $i] :
( ( mem @ X29 @ X23 )
=> ! [X30: $i] :
( ( mem @ X30 @ X23 )
=> ( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ X23 ) @ c_2Ebool_2ET ) @ X29 ) @ X30 )
= X29 ) ) )
& ! [X41: $i] :
( ( mem @ X41 @ X23 )
=> ! [X42: $i] :
( ( mem @ X42 @ X23 )
=> ( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ X23 ) @ c_2Ebool_2EF ) @ X41 ) @ X42 )
= X42 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',conj_thm_2Ebool_2Ebool__case__thm) ).
thf(mem_c_2Ewords_2En2w,axiom,
! [X23: del] : ( mem @ ( c_2Ewords_2En2w @ X23 ) @ ( arr @ ty_2Enum_2Enum @ ( ty_2Efcp_2Ecart @ bool @ X23 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',mem_c_2Ewords_2En2w) ).
thf(mem_c_2Enum_2E0,axiom,
mem @ c_2Enum_2E0 @ ty_2Enum_2Enum,
file('/export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p',mem_c_2Enum_2E0) ).
thf(c_0_24,plain,
! [X43: tp__ty_2Enum_2Enum] :
~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X43 ) ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Eprim__rec_2ENOT__LESS__0]) ).
thf(c_0_25,axiom,
! [X2: $i] :
( ( mem @ X2 @ bool )
=> ( ( ~ ( p @ X2 )
| ( X2
= ( inj__o @ $true ) ) )
& ( ( p @ X2 )
| ( X2
= ( inj__o @ $false ) ) ) ) ),
inference(fool_unroll,[status(thm)],[stp_iso_mem_o]) ).
thf(c_0_26,plain,
~ ( p @ c_2Ebool_2EF ),
inference(fof_simplification,[status(thm)],[ax_false_p]) ).
thf(c_0_27,plain,
! [X43: tp__ty_2Enum_2Enum,X44: tp__ty_2Enum_2Enum] :
( ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) )
<=> ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X43 ) ) @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) )
& ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) ) )
<=> ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X44 ) ) @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) )
& ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) )
<=> ( ( X43 != fo__c_2Enum_2E0 )
| ( X44 != fo__c_2Enum_2E0 ) ) )
& ( ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X43 ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X44 ) ) ) ) )
<=> ~ $true ) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Einteger_2EINT__LT__CALCULATE]) ).
thf(c_0_28,plain,
! [X136: tp__ty_2Enum_2Enum] :
~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X136 ) ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_24])]) ).
thf(c_0_29,plain,
! [X164: $i] :
( ( ~ ( p @ X164 )
| ( X164
= ( inj__o @ $true ) )
| ~ ( mem @ X164 @ bool ) )
& ( ( p @ X164 )
| ( X164
= ( inj__o @ $false ) )
| ~ ( mem @ X164 @ bool ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])]) ).
thf(c_0_30,plain,
~ ( p @ c_2Ebool_2EF ),
inference(fof_nnf,[status(thm)],[c_0_26]) ).
thf(c_0_31,plain,
! [X167: tp__ty_2Einteger_2Eint] :
( ( surj__ty_2Einteger_2Eint @ ( inj__ty_2Einteger_2Eint @ X167 ) )
= X167 ),
inference(variable_rename,[status(thm)],[stp_inj_surj_ty_2Einteger_2Eint]) ).
thf(c_0_32,plain,
! [X142: tp__ty_2Enum_2Enum] :
( ( inj__ty_2Einteger_2Eint @ ( fo__c_2Einteger_2Eint__of__num @ X142 ) )
= ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X142 ) ) ),
inference(variable_rename,[status(thm)],[stp_eq_fo_c_2Einteger_2Eint__of__num]) ).
thf(c_0_33,plain,
! [X144: tp__ty_2Einteger_2Eint] : ( mem @ ( inj__ty_2Einteger_2Eint @ X144 ) @ ty_2Einteger_2Eint ),
inference(variable_rename,[status(thm)],[stp_inj_mem_ty_2Einteger_2Eint]) ).
thf(c_0_34,plain,
! [X169: tp__ty_2Einteger_2Eint] :
( ( inj__ty_2Einteger_2Eint @ ( fo__c_2Einteger_2Eint__neg @ X169 ) )
= ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X169 ) ) ),
inference(variable_rename,[status(thm)],[stp_eq_fo_c_2Einteger_2Eint__neg]) ).
thf(c_0_35,plain,
! [X130: tp__ty_2Enum_2Enum] : ( mem @ ( inj__ty_2Enum_2Enum @ X130 ) @ ty_2Enum_2Enum ),
inference(variable_rename,[status(thm)],[stp_inj_mem_ty_2Enum_2Enum]) ).
thf(c_0_36,plain,
! [X165: tp__ty_2Einteger_2Eint] :
( ( inj__ty_2Enum_2Enum @ ( fo__c_2Einteger_2ENum @ X165 ) )
= ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X165 ) ) ),
inference(variable_rename,[status(thm)],[stp_eq_fo_c_2Einteger_2ENum]) ).
thf(c_0_37,plain,
! [X132: tp__ty_2Enum_2Enum,X133: tp__ty_2Enum_2Enum] :
( ( ~ ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) )
| ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X132 ) ) @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) )
& ( ~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X132 ) ) @ ( inj__ty_2Enum_2Enum @ X133 ) ) )
| ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) )
& ( ~ ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) )
| ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X133 ) ) @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) )
& ( ~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X133 ) ) @ ( inj__ty_2Enum_2Enum @ X132 ) ) )
| ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) ) )
& ( ~ ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) )
| ( X132 != fo__c_2Enum_2E0 )
| ( X133 != fo__c_2Enum_2E0 ) )
& ( ( X132 = fo__c_2Enum_2E0 )
| ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) )
& ( ( X133 = fo__c_2Enum_2E0 )
| ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) )
& ( ~ ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) )
| ~ $true )
& ( $true
| ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X132 ) ) ) @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X133 ) ) ) ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])]) ).
thf(c_0_38,plain,
! [X19: tp__ty_2Enum_2Enum] :
~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X19 ) ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
thf(c_0_39,plain,
( ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 )
= c_2Enum_2E0 ),
inference(split_conjunct,[status(thm)],[stp_eq_fo_c_2Enum_2E0]) ).
thf(c_0_40,plain,
! [X2: $i] :
( ( p @ X2 )
| ( X2
= ( inj__o @ ~ $true ) )
| ~ ( mem @ X2 @ bool ) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_41,plain,
mem @ c_2Ebool_2EF @ bool,
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2EF]) ).
thf(c_0_42,plain,
~ ( p @ c_2Ebool_2EF ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
thf(c_0_43,plain,
! [X112: del,X113: del,X114: $i,X115: $i] :
( ~ ( mem @ X114 @ ( arr @ X112 @ X113 ) )
| ~ ( mem @ X115 @ X112 )
| ( mem @ ( ap @ X114 @ X115 ) @ X113 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])])]) ).
thf(c_0_44,plain,
! [X15: tp__ty_2Einteger_2Eint] :
( ( surj__ty_2Einteger_2Eint @ ( inj__ty_2Einteger_2Eint @ X15 ) )
= X15 ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_45,plain,
! [X19: tp__ty_2Enum_2Enum] :
( ( inj__ty_2Einteger_2Eint @ ( fo__c_2Einteger_2Eint__of__num @ X19 ) )
= ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_46,plain,
! [X15: tp__ty_2Einteger_2Eint] : ( mem @ ( inj__ty_2Einteger_2Eint @ X15 ) @ ty_2Einteger_2Eint ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_47,plain,
! [X15: tp__ty_2Einteger_2Eint] :
( ( inj__ty_2Einteger_2Eint @ ( fo__c_2Einteger_2Eint__neg @ X15 ) )
= ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
thf(c_0_48,plain,
! [X19: tp__ty_2Enum_2Enum] : ( mem @ ( inj__ty_2Enum_2Enum @ X19 ) @ ty_2Enum_2Enum ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
thf(c_0_49,plain,
! [X15: tp__ty_2Einteger_2Eint] :
( ( inj__ty_2Enum_2Enum @ ( fo__c_2Einteger_2ENum @ X15 ) )
= ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
thf(c_0_50,plain,
! [X19: tp__ty_2Enum_2Enum,X20: tp__ty_2Enum_2Enum] :
( ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X19 ) ) @ ( inj__ty_2Enum_2Enum @ X20 ) ) )
| ~ ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X20 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
thf(c_0_51,plain,
! [X19: tp__ty_2Enum_2Enum] :
~ ( p @ ( ap @ ( ap @ c_2Eprim__rec_2E_3C @ ( inj__ty_2Enum_2Enum @ X19 ) ) @ c_2Enum_2E0 ) ),
inference(rw,[status(thm)],[c_0_38,c_0_39]) ).
thf(c_0_52,plain,
( ( inj__o @ ~ $true )
= c_2Ebool_2EF ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_42]) ).
thf(c_0_53,plain,
! [X2: $i,X5: $i,X4: del,X3: del] :
( ( mem @ ( ap @ X2 @ X5 ) @ X4 )
| ~ ( mem @ X2 @ ( arr @ X3 @ X4 ) )
| ~ ( mem @ X5 @ X3 ) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
thf(c_0_54,plain,
mem @ c_2Einteger_2Eint__lt @ ( arr @ ty_2Einteger_2Eint @ ( arr @ ty_2Einteger_2Eint @ bool ) ),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2Eint__lt]) ).
thf(c_0_55,plain,
! [X19: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) )
= ( fo__c_2Einteger_2Eint__of__num @ X19 ) ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
thf(c_0_56,plain,
! [X15: tp__ty_2Einteger_2Eint] : ( mem @ ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X15 ) ) @ ty_2Einteger_2Eint ),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
thf(c_0_57,plain,
! [X128: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X128 ) ) ) )
= X128 ),
inference(variable_rename,[status(thm)],[conj_thm_2Einteger_2ENUM__OF__INT]) ).
thf(c_0_58,plain,
! [X15: tp__ty_2Einteger_2Eint] : ( mem @ ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X15 ) ) @ ty_2Enum_2Enum ),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
thf(c_0_59,plain,
! [X19: tp__ty_2Enum_2Enum] :
~ ( p @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_39]),c_0_51]) ).
thf(c_0_60,plain,
! [X2: $i] :
( ( X2 = c_2Ebool_2EF )
| ( p @ X2 )
| ~ ( mem @ X2 @ bool ) ),
inference(rw,[status(thm)],[c_0_40,c_0_52]) ).
thf(c_0_61,plain,
! [X2: $i] :
( ( mem @ ( ap @ c_2Einteger_2Eint__lt @ X2 ) @ ( arr @ ty_2Einteger_2Eint @ bool ) )
| ~ ( mem @ X2 @ ty_2Einteger_2Eint ) ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
thf(c_0_62,plain,
! [X19: tp__ty_2Enum_2Enum] : ( mem @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) @ ty_2Einteger_2Eint ),
inference(spm,[status(thm)],[c_0_46,c_0_45]) ).
thf(c_0_63,plain,
! [X134: del,X135: tp__ty_2Einteger_2Eint] :
( ( ap @ ( c_2Einteger__word_2Ei2w @ X134 ) @ ( inj__ty_2Einteger_2Eint @ X135 ) )
= ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ ( ty_2Efcp_2Ecart @ bool @ X134 ) ) @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( inj__ty_2Einteger_2Eint @ X135 ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) ) @ ( ap @ ( c_2Ewords_2Eword__2comp @ X134 ) @ ( ap @ ( c_2Ewords_2En2w @ X134 ) @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X135 ) ) ) ) ) ) @ ( ap @ ( c_2Ewords_2En2w @ X134 ) @ ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X135 ) ) ) ) ),
inference(variable_rename,[status(thm)],[ax_thm_2Einteger__word_2Ei2w__def]) ).
thf(c_0_64,plain,
! [X168: $i] :
( ~ ( mem @ X168 @ ty_2Einteger_2Eint )
| ( X168
= ( inj__ty_2Einteger_2Eint @ ( surj__ty_2Einteger_2Eint @ X168 ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[stp_iso_mem_ty_2Einteger_2Eint])])]) ).
thf(c_0_65,plain,
( ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) )
= ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) ),
inference(split_conjunct,[status(thm)],[conj_thm_2Einteger_2EINT__NEG__0]) ).
thf(c_0_66,plain,
( ( fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0 )
= ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ),
inference(spm,[status(thm)],[c_0_55,c_0_39]) ).
thf(c_0_67,plain,
! [X19: tp__ty_2Enum_2Enum] : ( mem @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ty_2Einteger_2Eint ),
inference(spm,[status(thm)],[c_0_56,c_0_45]) ).
thf(c_0_68,plain,
! [X131: $i] :
( ~ ( mem @ X131 @ ty_2Enum_2Enum )
| ( X131
= ( inj__ty_2Enum_2Enum @ ( surj__ty_2Enum_2Enum @ X131 ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[stp_iso_mem_ty_2Enum_2Enum])])]) ).
thf(c_0_69,plain,
! [X19: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) )
= X19 ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
thf(c_0_70,plain,
! [X19: tp__ty_2Enum_2Enum] : ( mem @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ty_2Enum_2Enum ),
inference(spm,[status(thm)],[c_0_58,c_0_45]) ).
thf(c_0_71,plain,
! [X137: del] :
( ( ap @ ( c_2Ewords_2Eword__2comp @ X137 ) @ ( ap @ ( c_2Ewords_2En2w @ X137 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
= ( ap @ ( c_2Ewords_2En2w @ X137 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(variable_rename,[status(thm)],[conj_thm_2Ewords_2EWORD__NEG__0]) ).
thf(c_0_72,plain,
! [X19: tp__ty_2Enum_2Enum] :
( ( ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= c_2Ebool_2EF )
| ~ ( mem @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) @ bool ) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
thf(c_0_73,plain,
! [X5: $i,X2: $i] :
( ( mem @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ X2 ) @ X5 ) @ bool )
| ~ ( mem @ X5 @ ty_2Einteger_2Eint )
| ~ ( mem @ X2 @ ty_2Einteger_2Eint ) ),
inference(spm,[status(thm)],[c_0_53,c_0_61]) ).
thf(c_0_74,plain,
mem @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) @ ty_2Einteger_2Eint,
inference(spm,[status(thm)],[c_0_62,c_0_39]) ).
thf(c_0_75,plain,
! [X3: del,X15: tp__ty_2Einteger_2Eint] :
( ( ap @ ( c_2Einteger__word_2Ei2w @ X3 ) @ ( inj__ty_2Einteger_2Eint @ X15 ) )
= ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ ( ty_2Efcp_2Ecart @ bool @ X3 ) ) @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( inj__ty_2Einteger_2Eint @ X15 ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ) ) @ ( ap @ ( c_2Ewords_2Eword__2comp @ X3 ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ) ) ) ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
thf(c_0_76,plain,
! [X2: $i] :
( ( X2
= ( inj__ty_2Einteger_2Eint @ ( surj__ty_2Einteger_2Eint @ X2 ) ) )
| ~ ( mem @ X2 @ ty_2Einteger_2Eint ) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
thf(c_0_77,plain,
( ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) )
= ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_65,c_0_39]),c_0_39]) ).
thf(c_0_78,plain,
( ( inj__ty_2Einteger_2Eint @ ( surj__ty_2Einteger_2Eint @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) )
= ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_66]),c_0_39]) ).
thf(c_0_79,plain,
mem @ ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) @ ty_2Einteger_2Eint,
inference(spm,[status(thm)],[c_0_67,c_0_39]) ).
thf(c_0_80,plain,
! [X2: $i] :
( ( X2
= ( inj__ty_2Enum_2Enum @ ( surj__ty_2Enum_2Enum @ X2 ) ) )
| ~ ( mem @ X2 @ ty_2Enum_2Enum ) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
thf(c_0_81,plain,
( ( surj__ty_2Enum_2Enum @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) )
= fo__c_2Enum_2E0 ),
inference(spm,[status(thm)],[c_0_69,c_0_39]) ).
thf(c_0_82,plain,
mem @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) @ ty_2Enum_2Enum,
inference(spm,[status(thm)],[c_0_70,c_0_39]) ).
thf(c_0_83,plain,
! [X3: del] :
( ( ap @ ( c_2Ewords_2Eword__2comp @ X3 ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
= ( ap @ ( c_2Ewords_2En2w @ X3 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
thf(c_0_84,plain,
! [X19: tp__ty_2Enum_2Enum] :
( ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ X19 ) ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= c_2Ebool_2EF ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_73]),c_0_74]),c_0_62])]) ).
thf(c_0_85,negated_conjecture,
~ ! [X23: del] :
( ( ap @ ( c_2Einteger__word_2Ei2w @ X23 ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
= ( ap @ ( c_2Ewords_2En2w @ X23 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(assume_negation,[status(cth)],[conj_thm_2Einteger__word_2Ei2w__0]) ).
thf(c_0_86,plain,
! [X158: del,X159: $i,X160: $i,X161: $i,X162: $i] :
( ( ~ ( mem @ X159 @ X158 )
| ~ ( mem @ X160 @ X158 )
| ( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ X158 ) @ c_2Ebool_2ET ) @ X159 ) @ X160 )
= X159 ) )
& ( ~ ( mem @ X161 @ X158 )
| ~ ( mem @ X162 @ X158 )
| ( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ X158 ) @ c_2Ebool_2EF ) @ X161 ) @ X162 )
= X162 ) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ebool_2Ebool__case__thm])])])]) ).
thf(c_0_87,plain,
! [X3: del,X15: tp__ty_2Einteger_2Eint] :
( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ ( ty_2Efcp_2Ecart @ bool @ X3 ) ) @ ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( inj__ty_2Einteger_2Eint @ X15 ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ) @ ( ap @ ( c_2Ewords_2Eword__2comp @ X3 ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__neg @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ) ) ) ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ ( ap @ c_2Einteger_2ENum @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ) )
= ( ap @ ( c_2Einteger__word_2Ei2w @ X3 ) @ ( inj__ty_2Einteger_2Eint @ X15 ) ) ),
inference(rw,[status(thm)],[c_0_75,c_0_39]) ).
thf(c_0_88,plain,
( ( ap @ c_2Einteger_2Eint__neg @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_77]),c_0_78]),c_0_79])]) ).
thf(c_0_89,plain,
( ( ap @ c_2Einteger_2ENum @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= c_2Enum_2E0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_81]),c_0_39]),c_0_82])]) ).
thf(c_0_90,plain,
! [X3: del] :
( ( ap @ ( c_2Ewords_2Eword__2comp @ X3 ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) )
= ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_83,c_0_39]),c_0_39]) ).
thf(c_0_91,plain,
( ( ap @ ( ap @ c_2Einteger_2Eint__lt @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= c_2Ebool_2EF ),
inference(spm,[status(thm)],[c_0_84,c_0_39]) ).
thf(c_0_92,plain,
! [X138: del] : ( mem @ ( c_2Ewords_2En2w @ X138 ) @ ( arr @ ty_2Enum_2Enum @ ( ty_2Efcp_2Ecart @ bool @ X138 ) ) ),
inference(variable_rename,[status(thm)],[mem_c_2Ewords_2En2w]) ).
thf(c_0_93,negated_conjecture,
( ( ap @ ( c_2Einteger__word_2Ei2w @ esk1_0 ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
!= ( ap @ ( c_2Ewords_2En2w @ esk1_0 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_85])])])]) ).
thf(c_0_94,plain,
! [X2: $i,X5: $i,X3: del] :
( ( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ X3 ) @ c_2Ebool_2EF ) @ X2 ) @ X5 )
= X5 )
| ~ ( mem @ X2 @ X3 )
| ~ ( mem @ X5 @ X3 ) ),
inference(split_conjunct,[status(thm)],[c_0_86]) ).
thf(c_0_95,plain,
! [X3: del] :
( ( ap @ ( ap @ ( ap @ ( c_2Ebool_2ECOND @ ( ty_2Efcp_2Ecart @ bool @ X3 ) ) @ c_2Ebool_2EF ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) ) @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) )
= ( ap @ ( c_2Einteger__word_2Ei2w @ X3 ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_78]),c_0_88]),c_0_89]),c_0_90]),c_0_89]),c_0_91]) ).
thf(c_0_96,plain,
! [X3: del] : ( mem @ ( c_2Ewords_2En2w @ X3 ) @ ( arr @ ty_2Enum_2Enum @ ( ty_2Efcp_2Ecart @ bool @ X3 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_92]) ).
thf(c_0_97,negated_conjecture,
( ( ap @ ( c_2Einteger__word_2Ei2w @ esk1_0 ) @ ( ap @ c_2Einteger_2Eint__of__num @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) )
!= ( ap @ ( c_2Ewords_2En2w @ esk1_0 ) @ ( inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_93]) ).
thf(c_0_98,plain,
! [X3: del] :
( ( ( ap @ ( c_2Einteger__word_2Ei2w @ X3 ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) )
| ~ ( mem @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) @ ( ty_2Efcp_2Ecart @ bool @ X3 ) ) ),
inference(spm,[status(thm)],[c_0_94,c_0_95]) ).
thf(c_0_99,plain,
! [X3: del,X2: $i] :
( ( mem @ ( ap @ ( c_2Ewords_2En2w @ X3 ) @ X2 ) @ ( ty_2Efcp_2Ecart @ bool @ X3 ) )
| ~ ( mem @ X2 @ ty_2Enum_2Enum ) ),
inference(spm,[status(thm)],[c_0_53,c_0_96]) ).
thf(c_0_100,plain,
mem @ c_2Enum_2E0 @ ty_2Enum_2Enum,
inference(split_conjunct,[status(thm)],[mem_c_2Enum_2E0]) ).
thf(c_0_101,negated_conjecture,
( ( ap @ ( c_2Einteger__word_2Ei2w @ esk1_0 ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
!= ( ap @ ( c_2Ewords_2En2w @ esk1_0 ) @ c_2Enum_2E0 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_97,c_0_39]),c_0_39]) ).
thf(c_0_102,plain,
! [X3: del] :
( ( ap @ ( c_2Einteger__word_2Ei2w @ X3 ) @ ( ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0 ) )
= ( ap @ ( c_2Ewords_2En2w @ X3 ) @ c_2Enum_2E0 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98,c_0_99]),c_0_100])]) ).
thf(c_0_103,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101,c_0_102])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP015^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.18 % Computer : n026.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Tue Sep 29 19:32:02 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.23 Running higher-order theorem proving
% 0.06/0.25 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.mjN1EGPRip/E---3.1_1061920.p
% 18.37/2.96 % Version: 3.5.1-ho
% 18.37/2.96 % Preprocessing class: HSLSSMSMSSSNSFA.
% 18.37/2.96 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 18.37/2.96 % Starting new_ho_10 with 900s (3) cores
% 18.37/2.96 % Starting sh2lt with 300s (1) cores
% 18.37/2.96 % Starting new_ho_5 with 300s (1) cores
% 18.37/2.96 % Starting full_lambda_5 with 300s (1) cores
% 18.37/2.96 % Starting sh9 with 300s (1) cores
% 18.37/2.96 % Starting ehoh_best8_lambda with 300s (1) cores
% 18.37/2.96 % new_ho_5 with pid 1061935 completed with status 0
% 18.37/2.96 % Result found by new_ho_5
% 18.37/2.96 % Preprocessing class: HSLSSMSMSSSNSFA.
% 18.37/2.96 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 18.37/2.96 % Starting new_ho_10 with 900s (3) cores
% 18.37/2.96 % Starting sh2lt with 300s (1) cores
% 18.37/2.96 % Starting new_ho_5 with 300s (1) cores
% 18.37/2.96 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,7,,3,20000,1.0,true))
% 18.37/2.96 % SinE strategy is GSinE(CountFormulas,hypos,7,,3,20000,1.0,true)
% 18.37/2.96 % Search class: HGHSM-FFMM31-DSFFFFBN
% 18.37/2.96 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 18.37/2.96 % Starting SubtermCWHack with 31s (1) cores
% 18.37/2.96 % SubtermCWHack with pid 1061941 completed with status 0
% 18.37/2.96 % Result found by SubtermCWHack
% 18.37/2.96 % Preprocessing class: HSLSSMSMSSSNSFA.
% 18.37/2.96 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 18.37/2.96 % Starting new_ho_10 with 900s (3) cores
% 18.37/2.96 % Starting sh2lt with 300s (1) cores
% 18.37/2.96 % Starting new_ho_5 with 300s (1) cores
% 18.37/2.96 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,7,,3,20000,1.0,true))
% 18.37/2.96 % SinE strategy is GSinE(CountFormulas,hypos,7,,3,20000,1.0,true)
% 18.37/2.96 % Search class: HGHSM-FFMM31-DSFFFFBN
% 18.37/2.96 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 18.37/2.96 % Starting SubtermCWHack with 31s (1) cores
% 18.37/2.96 % Preprocessing time : 0.002 s
% 18.37/2.96
% 18.37/2.96 % Proof found!
% 18.37/2.96 % SZS status Theorem
% 18.37/2.96 % SZS output start CNFRefutation
% See solution above
% 18.37/2.96 % Parsed axioms : 108
% 18.37/2.96 % Removed by relevancy pruning/SinE : 60
% 18.37/2.96 % Initial clauses : 82
% 18.37/2.96 % Removed in clause preprocessing : 24
% 18.37/2.96 % Initial clauses in saturation : 58
% 18.37/2.96 % Processed clauses : 9217
% 18.37/2.96 % ...of these trivial : 983
% 18.37/2.96 % ...subsumed : 5815
% 18.37/2.96 % ...remaining for further processing : 2419
% 18.37/2.96 % Other redundant clauses eliminated : 26
% 18.37/2.96 % Clauses deleted for lack of memory : 0
% 18.37/2.96 % Backward-subsumed : 6
% 18.37/2.96 % Backward-rewritten : 63
% 18.37/2.96 % Generated clauses : 156210
% 18.37/2.96 % ...of the previous two non-redundant : 129736
% 18.37/2.96 % ...aggressively subsumed : 0
% 18.37/2.96 % Contextual simplify-reflections : 13
% 18.37/2.96 % Paramodulations : 156174
% 18.37/2.96 % Factorizations : 4
% 18.37/2.96 % NegExts : 0
% 18.37/2.96 % Equation resolutions : 35
% 18.37/2.96 % Disequality decompositions : 0
% 18.37/2.96 % Total rewrite steps : 74318
% 18.37/2.96 % ...of those cached : 68627
% 18.37/2.96 % Propositional unsat checks : 0
% 18.37/2.96 % Propositional check models : 0
% 18.37/2.96 % Propositional check unsatisfiable : 0
% 18.37/2.96 % Propositional clauses : 0
% 18.37/2.96 % Propositional clauses after purity: 0
% 18.37/2.96 % Propositional unsat core size : 0
% 18.37/2.96 % Propositional preprocessing time : 0.000
% 18.37/2.96 % Propositional encoding time : 0.000
% 18.37/2.96 % Propositional solver time : 0.000
% 18.37/2.96 % Success case prop preproc time : 0.000
% 18.37/2.96 % Success case prop encoding time : 0.000
% 18.37/2.96 % Success case prop solver time : 0.000
% 18.37/2.96 % Current number of processed clauses : 2345
% 18.37/2.96 % Positive orientable unit clauses : 1172
% 18.37/2.96 % Positive unorientable unit clauses: 0
% 18.37/2.96 % Negative unit clauses : 4
% 18.37/2.96 % Non-unit-clauses : 1169
% 18.37/2.96 % Current number of unprocessed clauses: 120162
% 18.37/2.96 % ...number of literals in the above : 242056
% 18.37/2.96 % Current number of archived formulas : 0
% 18.37/2.96 % Current number of archived clauses : 69
% 18.37/2.96 % Clause-clause subsumption calls (NU) : 278817
% 18.37/2.96 % Rec. Clause-clause subsumption calls : 266746
% 18.37/2.96 % Non-unit clause-clause subsumptions : 4445
% 18.37/2.96 % Unit Clause-clause subsumption calls : 1071
% 18.37/2.96 % Rewrite failures with RHS unbound : 0
% 18.37/2.96 % BW rewrite match attempts : 138035
% 18.37/2.96 % BW rewrite match successes : 52
% 18.37/2.96 % Condensation attempts : 0
% 18.37/2.96 % Condensation successes : 0
% 18.37/2.96 % Termbank termtop insertions : 3814778
% 18.37/2.96 % Search garbage collected termcells : 1496
% 18.37/2.96
% 18.37/2.96 % -------------------------------------------------
% 18.37/2.96 % User time : 2.515 s
% 18.37/2.96 % System time : 0.107 s
% 18.37/2.96 % Total time : 2.622 s
% 18.37/2.96 % Maximum resident set size: 4020 pages
% 18.37/2.96
% 18.37/2.96 % -------------------------------------------------
% 18.37/2.96 % User time : 2.519 s
% 18.37/2.96 % System time : 0.111 s
% 18.37/2.96 % Total time : 2.631 s
% 18.37/2.96 % Maximum resident set size: 4608 pages
% 18.37/2.96 % E exiting
%------------------------------------------------------------------------------