%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP003^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:03:57 AM UTC 2026
% Result : Theorem 35.22s 6.14s
% Output : CNFRefutation 35.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 24
% Syntax : Number of formulae : 112 ( 55 unt; 0 typ; 0 def)
% Number of atoms : 257 ( 125 equ; 0 cnn)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1003 ( 103 ~; 92 |; 33 &; 761 @)
% ( 7 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 6 ( 6 >; 0 *; 0 +; 0 <<)
% Number of symbols : 24 ( 21 usr; 5 con; 0-3 aty)
% Number of variables : 139 ( 0 ^; 137 !; 2 ?; 139 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
mono_2Etyop_2Enum_2Enum: $tType ).
thf(decl_211,type,
mono_2Ec_2Enum_2E0: mono_2Etyop_2Enum_2Enum ).
thf(decl_215,type,
mono_2Ec_2Enum_2ESUC: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_523,type,
mono_2Ec_2Eprim__rec_2E_3C: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o ).
thf(decl_525,type,
mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum: $o > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_590,type,
mono_2Ec_2Earithmetic_2E_2A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_591,type,
mono_2Ec_2Earithmetic_2E_2B: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_592,type,
mono_2Ec_2Earithmetic_2E_2D: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_593,type,
mono_2Ec_2Earithmetic_2E_3C_3D: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o ).
thf(decl_597,type,
mono_2Ec_2Earithmetic_2EBIT1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_598,type,
mono_2Ec_2Earithmetic_2EBIT2: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_599,type,
mono_2Ec_2Earithmetic_2EDIV: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_601,type,
mono_2Ec_2Earithmetic_2EEVEN: mono_2Etyop_2Enum_2Enum > $o ).
thf(decl_606,type,
mono_2Ec_2Earithmetic_2EMOD: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_607,type,
mono_2Ec_2Earithmetic_2ENUMERAL: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_608,type,
mono_2Ec_2Earithmetic_2EODD: mono_2Etyop_2Enum_2Enum > $o ).
thf(decl_610,type,
mono_2Ec_2Earithmetic_2EZERO: mono_2Etyop_2Enum_2Enum ).
thf(decl_615,type,
esk1_0: mono_2Etyop_2Enum_2Enum ).
thf(decl_626,type,
esk12_1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_627,type,
esk13_1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_657,type,
esk42_3: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > ( mono_2Etyop_2Enum_2Enum > $o ) > mono_2Etyop_2Enum_2Enum ).
thf(decl_658,type,
esk43_3: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > ( mono_2Etyop_2Enum_2Enum > $o ) > mono_2Etyop_2Enum_2Enum ).
thf(thm_2Earithmetic_2EMOD__2,conjecture,
! [X331: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2EMOD @ X331 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2EEVEN @ X331 ) @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EMOD__2) ).
thf(thm_2Earithmetic_2EONE,axiom,
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EONE) ).
thf(thm_2Earithmetic_2EALT__ZERO,axiom,
mono_2Ec_2Earithmetic_2EZERO = mono_2Ec_2Enum_2E0,
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EALT__ZERO) ).
thf(thm_2Earithmetic_2ENUMERAL__DEF,axiom,
! [X783: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ X783 )
= X783 ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ENUMERAL__DEF) ).
thf(thm_2Earithmetic_2ESUB__ELIM__THM,axiom,
! [X1108: mono_2Etyop_2Enum_2Enum,X1109: mono_2Etyop_2Enum_2Enum,X1110: mono_2Etyop_2Enum_2Enum > $o] :
( ( X1110 @ ( mono_2Ec_2Earithmetic_2E_2D @ X1109 @ X1108 ) )
<=> ! [X1111: mono_2Etyop_2Enum_2Enum] :
( ( ( X1108
= ( mono_2Ec_2Earithmetic_2E_2B @ X1109 @ X1111 ) )
=> ( X1110 @ mono_2Ec_2Enum_2E0 ) )
& ( ( X1109
= ( mono_2Ec_2Earithmetic_2E_2B @ X1108 @ X1111 ) )
=> ( X1110 @ X1111 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ESUB__ELIM__THM) ).
thf(thm_2Earithmetic_2EADD1,axiom,
! [X838: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2ESUC @ X838 )
= ( mono_2Ec_2Earithmetic_2E_2B @ X838 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EADD1) ).
thf(thm_2Earithmetic_2ENOT__NUM__EQ,axiom,
! [X981: mono_2Etyop_2Enum_2Enum,X333: mono_2Etyop_2Enum_2Enum] :
( ( X981 != X333 )
<=> ( ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X981 ) @ X333 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X333 ) @ X981 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ENOT__NUM__EQ) ).
thf(thm_2Earithmetic_2ESUC__NOT,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] :
( mono_2Ec_2Enum_2E0
!= ( mono_2Ec_2Enum_2ESUC @ X331 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ESUC__NOT) ).
thf(thm_2Earithmetic_2ELESS__EQ__0,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_3C_3D @ X331 @ mono_2Ec_2Enum_2E0 )
<=> ( X331 = mono_2Ec_2Enum_2E0 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ELESS__EQ__0) ).
thf(thm_2Earithmetic_2EMULT__LEFT__1,axiom,
! [X843: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X843 )
= X843 ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EMULT__LEFT__1) ).
thf(thm_2Earithmetic_2ESUB,axiom,
( ! [X784: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ mono_2Ec_2Enum_2E0 @ X784 )
= mono_2Ec_2Enum_2E0 )
& ! [X781: mono_2Etyop_2Enum_2Enum,X785: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X781 ) @ X785 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Eprim__rec_2E_3C @ X781 @ X785 ) @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X781 @ X785 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ESUB) ).
thf(thm_2Earithmetic_2ESUC__SUB,axiom,
! [X328: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X328 ) @ X328 )
= ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ESUC__SUB) ).
thf(thm_2Eprim__rec_2ELESS__REFL,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Eprim__rec_2E_3C @ X331 @ X331 ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Eprim__rec_2ELESS__REFL) ).
thf(thm_2Earithmetic_2EEVEN__DOUBLE,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EEVEN @ ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X331 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EEVEN__DOUBLE) ).
thf(thm_2Earithmetic_2ETWO,axiom,
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) )
= ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ETWO) ).
thf(thm_2Earithmetic_2EMULT__EQ__DIV,axiom,
! [X1088: mono_2Etyop_2Enum_2Enum,X1089: mono_2Etyop_2Enum_2Enum,X1090: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X1090 )
=> ( ( ( mono_2Ec_2Earithmetic_2E_2A @ X1090 @ X1089 )
= X1088 )
<=> ( ( X1089
= ( mono_2Ec_2Earithmetic_2EDIV @ X1088 @ X1090 ) )
& ( ( mono_2Ec_2Earithmetic_2EMOD @ X1088 @ X1090 )
= mono_2Ec_2Enum_2E0 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EMULT__EQ__DIV) ).
thf(thm_2Earithmetic_2ELT__MULT__CANCEL__RBARE,axiom,
! [X331: mono_2Etyop_2Enum_2Enum,X781: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X781 @ X331 ) @ X781 )
<=> ( ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X781 )
& ( X331 = mono_2Ec_2Enum_2E0 ) ) )
& ( ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X781 @ X331 ) @ X331 )
<=> ( ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X331 )
& ( X781 = mono_2Ec_2Enum_2E0 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ELT__MULT__CANCEL__RBARE) ).
thf(thm_2Eprim__rec_2ELESS__LEMMA1,axiom,
! [X704: mono_2Etyop_2Enum_2Enum,X333: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ X704 @ ( mono_2Ec_2Enum_2ESUC @ X333 ) )
=> ( ( X704 = X333 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ X704 @ X333 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Eprim__rec_2ELESS__LEMMA1) ).
thf(thm_2Earithmetic_2EMOD__LESS,axiom,
! [X1050: mono_2Etyop_2Enum_2Enum,X333: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X333 )
=> ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2EMOD @ X1050 @ X333 ) @ X333 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EMOD__LESS) ).
thf(thm_2Eprim__rec_2ELESS__0,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ X331 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Eprim__rec_2ELESS__0) ).
thf(thm_2Earithmetic_2EEVEN__ODD__EXISTS,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2EEVEN @ X331 )
=> ? [X781: mono_2Etyop_2Enum_2Enum] :
( X331
= ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X781 ) ) )
& ( ( mono_2Ec_2Earithmetic_2EODD @ X331 )
=> ? [X970: mono_2Etyop_2Enum_2Enum] :
( X331
= ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X970 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2EEVEN__ODD__EXISTS) ).
thf(thm_2Earithmetic_2ESUB__EQUAL__0,axiom,
! [X939: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ X939 @ X939 )
= mono_2Ec_2Enum_2E0 ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Earithmetic_2ESUB__EQUAL__0) ).
thf(thm_2Eprim__rec_2ELESS__SUC__REFL,axiom,
! [X331: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ X331 @ ( mono_2Ec_2Enum_2ESUC @ X331 ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Eprim__rec_2ELESS__SUC__REFL) ).
thf(thm_2Eprim__rec_2ELESS__SUC__SUC,axiom,
! [X719: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ X719 @ ( mono_2Ec_2Enum_2ESUC @ X719 ) )
& ( mono_2Ec_2Eprim__rec_2E_3C @ X719 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ X719 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p',thm_2Eprim__rec_2ELESS__SUC__SUC) ).
thf(c_0_24,negated_conjecture,
~ ! [X331: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2EMOD @ X331 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2EEVEN @ X331 ) @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
inference(assume_negation,[status(cth)],[thm_2Earithmetic_2EMOD__2]) ).
thf(c_0_25,negated_conjecture,
~ ! [X331: mono_2Etyop_2Enum_2Enum] :
( ( ~ ( mono_2Ec_2Earithmetic_2EEVEN @ X331 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X331 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) )
& ( ( mono_2Ec_2Earithmetic_2EEVEN @ X331 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X331 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $false @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ),
inference(fool_unroll,[status(thm)],[c_0_24]) ).
thf(c_0_26,plain,
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ),
inference(split_conjunct,[status(thm)],[thm_2Earithmetic_2EONE]) ).
thf(c_0_27,plain,
mono_2Ec_2Earithmetic_2EZERO = mono_2Ec_2Enum_2E0,
inference(split_conjunct,[status(thm)],[thm_2Earithmetic_2EALT__ZERO]) ).
thf(c_0_28,plain,
! [X2491: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ X2491 )
= X2491 ),
inference(variable_rename,[status(thm)],[thm_2Earithmetic_2ENUMERAL__DEF]) ).
thf(c_0_29,negated_conjecture,
( ( ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 ) )
& ( ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $false @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) )
| ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 ) )
& ( ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) )
& ( ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $false @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])])]) ).
thf(c_0_30,plain,
! [X2973: mono_2Etyop_2Enum_2Enum,X2974: mono_2Etyop_2Enum_2Enum,X2975: mono_2Etyop_2Enum_2Enum > $o,X2976: mono_2Etyop_2Enum_2Enum,X2977: mono_2Etyop_2Enum_2Enum,X2978: mono_2Etyop_2Enum_2Enum,X2979: mono_2Etyop_2Enum_2Enum,X2980: mono_2Etyop_2Enum_2Enum > $o] :
( ( ( X2973
!= ( mono_2Ec_2Earithmetic_2E_2B @ X2974 @ X2976 ) )
| ( X2975 @ mono_2Ec_2Enum_2E0 )
| ~ ( X2975 @ ( mono_2Ec_2Earithmetic_2E_2D @ X2974 @ X2973 ) ) )
& ( ( X2974
!= ( mono_2Ec_2Earithmetic_2E_2B @ X2973 @ X2977 ) )
| ( X2975 @ X2977 )
| ~ ( X2975 @ ( mono_2Ec_2Earithmetic_2E_2D @ X2974 @ X2973 ) ) )
& ( ( X2979
= ( mono_2Ec_2Earithmetic_2E_2B @ X2978 @ ( esk43_3 @ X2978 @ X2979 @ X2980 ) ) )
| ( X2978
= ( mono_2Ec_2Earithmetic_2E_2B @ X2979 @ ( esk42_3 @ X2978 @ X2979 @ X2980 ) ) )
| ( X2980 @ ( mono_2Ec_2Earithmetic_2E_2D @ X2979 @ X2978 ) ) )
& ( ~ ( X2980 @ ( esk43_3 @ X2978 @ X2979 @ X2980 ) )
| ( X2978
= ( mono_2Ec_2Earithmetic_2E_2B @ X2979 @ ( esk42_3 @ X2978 @ X2979 @ X2980 ) ) )
| ( X2980 @ ( mono_2Ec_2Earithmetic_2E_2D @ X2979 @ X2978 ) ) )
& ( ( X2979
= ( mono_2Ec_2Earithmetic_2E_2B @ X2978 @ ( esk43_3 @ X2978 @ X2979 @ X2980 ) ) )
| ~ ( X2980 @ mono_2Ec_2Enum_2E0 )
| ( X2980 @ ( mono_2Ec_2Earithmetic_2E_2D @ X2979 @ X2978 ) ) )
& ( ~ ( X2980 @ ( esk43_3 @ X2978 @ X2979 @ X2980 ) )
| ~ ( X2980 @ mono_2Ec_2Enum_2E0 )
| ( X2980 @ ( mono_2Ec_2Earithmetic_2E_2D @ X2979 @ X2978 ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Earithmetic_2ESUB__ELIM__THM])])])])])])]) ).
thf(c_0_31,plain,
! [X2492: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2ESUC @ X2492 )
= ( mono_2Ec_2Earithmetic_2E_2B @ X2492 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
inference(variable_rename,[status(thm)],[thm_2Earithmetic_2EADD1]) ).
thf(c_0_32,plain,
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ),
inference(rw,[status(thm)],[c_0_26,c_0_27]) ).
thf(c_0_33,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ X278 )
= X278 ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
thf(c_0_34,plain,
! [X981: mono_2Etyop_2Enum_2Enum,X333: mono_2Etyop_2Enum_2Enum] :
( ( X981 != X333 )
<=> ( ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X981 ) @ X333 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X333 ) @ X981 ) ) ),
inference(fof_simplification,[status(thm)],[thm_2Earithmetic_2ENOT__NUM__EQ]) ).
thf(c_0_35,plain,
! [X331: mono_2Etyop_2Enum_2Enum] :
( mono_2Ec_2Enum_2E0
!= ( mono_2Ec_2Enum_2ESUC @ X331 ) ),
inference(fof_simplification,[status(thm)],[thm_2Earithmetic_2ESUC__NOT]) ).
thf(c_0_36,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_37,negated_conjecture,
( ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_38,plain,
! [X274: mono_2Etyop_2Enum_2Enum > $o,X296: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum,X278: mono_2Etyop_2Enum_2Enum] :
( ( X274 @ mono_2Ec_2Enum_2E0 )
| ( X278
!= ( mono_2Ec_2Earithmetic_2E_2B @ X294 @ X296 ) )
| ~ ( X274 @ ( mono_2Ec_2Earithmetic_2E_2D @ X294 @ X278 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
thf(c_0_39,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2ESUC @ X278 )
= ( mono_2Ec_2Earithmetic_2E_2B @ X278 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_40,plain,
( ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Enum_2E0 )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ),
inference(rw,[status(thm)],[c_0_32,c_0_33]) ).
thf(c_0_41,plain,
! [X3157: mono_2Etyop_2Enum_2Enum] :
( ( ~ ( mono_2Ec_2Earithmetic_2E_3C_3D @ X3157 @ mono_2Ec_2Enum_2E0 )
| ( X3157 = mono_2Ec_2Enum_2E0 ) )
& ( ( X3157 != mono_2Ec_2Enum_2E0 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ X3157 @ mono_2Ec_2Enum_2E0 ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Earithmetic_2ELESS__EQ__0])])]) ).
thf(c_0_42,plain,
! [X3180: mono_2Etyop_2Enum_2Enum,X3181: mono_2Etyop_2Enum_2Enum] :
( ( ( X3180 = X3181 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X3180 ) @ X3181 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X3181 ) @ X3180 ) )
& ( ~ ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X3180 ) @ X3181 )
| ( X3180 != X3181 ) )
& ( ~ ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X3181 ) @ X3180 )
| ( X3180 != X3181 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_34])])])]) ).
thf(c_0_43,plain,
! [X2845: mono_2Etyop_2Enum_2Enum] :
( mono_2Ec_2Enum_2E0
!= ( mono_2Ec_2Enum_2ESUC @ X2845 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_35])]) ).
thf(c_0_44,plain,
! [X2494: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X2494 )
= X2494 ),
inference(variable_rename,[status(thm)],[thm_2Earithmetic_2EMULT__LEFT__1]) ).
thf(c_0_45,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_27]),c_0_27]) ).
thf(c_0_46,axiom,
( ! [X784: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ mono_2Ec_2Enum_2E0 @ X784 )
= mono_2Ec_2Enum_2E0 )
& ! [X781: mono_2Etyop_2Enum_2Enum,X785: mono_2Etyop_2Enum_2Enum] :
( ( ~ ( mono_2Ec_2Eprim__rec_2E_3C @ X781 @ X785 )
| ( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X781 ) @ X785 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X781 @ X785 ) ) ) ) )
& ( ( mono_2Ec_2Eprim__rec_2E_3C @ X781 @ X785 )
| ( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X781 ) @ X785 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $false @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X781 @ X785 ) ) ) ) ) ) ),
inference(fool_unroll,[status(thm)],[thm_2Earithmetic_2ESUB]) ).
thf(c_0_47,plain,
! [X2503: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X2503 ) @ X2503 )
= ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ),
inference(variable_rename,[status(thm)],[thm_2Earithmetic_2ESUC__SUB]) ).
thf(c_0_48,plain,
! [X331: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Eprim__rec_2E_3C @ X331 @ X331 ),
inference(fof_simplification,[status(thm)],[thm_2Eprim__rec_2ELESS__REFL]) ).
thf(c_0_49,negated_conjecture,
( ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Enum_2E0 ) ) ) )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37,c_0_27]),c_0_27]) ).
thf(c_0_50,plain,
! [X274: mono_2Etyop_2Enum_2Enum > $o,X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( X274 @ mono_2Ec_2Enum_2E0 )
| ~ ( X274 @ ( mono_2Ec_2Earithmetic_2E_2D @ X278 @ ( mono_2Ec_2Earithmetic_2E_2B @ X278 @ X294 ) ) ) ),
inference(er,[status(thm)],[c_0_38]) ).
thf(c_0_51,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2B @ X278 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Enum_2ESUC @ X278 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_39,c_0_27]),c_0_40]),c_0_33]) ).
thf(c_0_52,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( X278 = mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Earithmetic_2E_3C_3D @ X278 @ mono_2Ec_2Enum_2E0 ) ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
thf(c_0_53,plain,
! [X294: mono_2Etyop_2Enum_2Enum,X278: mono_2Etyop_2Enum_2Enum] :
( ( X278 = X294 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X294 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X294 ) @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
thf(c_0_54,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( mono_2Ec_2Enum_2E0
!= ( mono_2Ec_2Enum_2ESUC @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
thf(c_0_55,plain,
! [X294: mono_2Etyop_2Enum_2Enum,X278: mono_2Etyop_2Enum_2Enum] :
( ~ ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X294 )
| ( X294 != X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
thf(c_0_56,plain,
! [X2554: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EEVEN @ ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X2554 ) ),
inference(variable_rename,[status(thm)],[thm_2Earithmetic_2EEVEN__DOUBLE]) ).
thf(c_0_57,plain,
( ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) )
= ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ),
inference(split_conjunct,[status(thm)],[thm_2Earithmetic_2ETWO]) ).
thf(c_0_58,plain,
! [X2636: mono_2Etyop_2Enum_2Enum,X2637: mono_2Etyop_2Enum_2Enum,X2638: mono_2Etyop_2Enum_2Enum] :
( ( ( X2637
= ( mono_2Ec_2Earithmetic_2EDIV @ X2636 @ X2638 ) )
| ( ( mono_2Ec_2Earithmetic_2E_2A @ X2638 @ X2637 )
!= X2636 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X2638 ) )
& ( ( ( mono_2Ec_2Earithmetic_2EMOD @ X2636 @ X2638 )
= mono_2Ec_2Enum_2E0 )
| ( ( mono_2Ec_2Earithmetic_2E_2A @ X2638 @ X2637 )
!= X2636 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X2638 ) )
& ( ( X2637
!= ( mono_2Ec_2Earithmetic_2EDIV @ X2636 @ X2638 ) )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X2636 @ X2638 )
!= mono_2Ec_2Enum_2E0 )
| ( ( mono_2Ec_2Earithmetic_2E_2A @ X2638 @ X2637 )
= X2636 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X2638 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Earithmetic_2EMULT__EQ__DIV])])])]) ).
thf(c_0_59,plain,
! [X3315: mono_2Etyop_2Enum_2Enum,X3316: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X3316 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X3316 @ X3315 ) @ X3316 ) )
& ( ( X3315 = mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X3316 @ X3315 ) @ X3316 ) )
& ( ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X3316 )
| ( X3315 != mono_2Ec_2Enum_2E0 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X3316 @ X3315 ) @ X3316 ) )
& ( ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X3315 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X3316 @ X3315 ) @ X3315 ) )
& ( ( X3316 = mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X3316 @ X3315 ) @ X3315 ) )
& ( ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X3315 )
| ( X3316 != mono_2Ec_2Enum_2E0 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X3316 @ X3315 ) @ X3315 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Earithmetic_2ELT__MULT__CANCEL__RBARE])])])]) ).
thf(c_0_60,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X278 )
= X278 ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
thf(c_0_61,plain,
! [X2830: mono_2Etyop_2Enum_2Enum,X2831: mono_2Etyop_2Enum_2Enum] :
( ~ ( mono_2Ec_2Eprim__rec_2E_3C @ X2830 @ ( mono_2Ec_2Enum_2ESUC @ X2831 ) )
| ( X2830 = X2831 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ X2830 @ X2831 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Eprim__rec_2ELESS__LEMMA1])])]) ).
thf(c_0_62,plain,
! [X2601: mono_2Etyop_2Enum_2Enum,X2602: mono_2Etyop_2Enum_2Enum] :
( ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X2602 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2EMOD @ X2601 @ X2602 ) @ X2602 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Earithmetic_2EMOD__LESS])])]) ).
thf(c_0_63,plain,
! [X2820: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ X2820 ) ),
inference(variable_rename,[status(thm)],[thm_2Eprim__rec_2ELESS__0]) ).
thf(c_0_64,plain,
! [X2555: mono_2Etyop_2Enum_2Enum,X2557: mono_2Etyop_2Enum_2Enum] :
( ( ~ ( mono_2Ec_2Earithmetic_2EEVEN @ X2555 )
| ( X2555
= ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ ( esk12_1 @ X2555 ) ) ) )
& ( ~ ( mono_2Ec_2Earithmetic_2EODD @ X2557 )
| ( X2557
= ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ ( esk13_1 @ X2557 ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[thm_2Earithmetic_2EEVEN__ODD__EXISTS])])])])])]) ).
thf(c_0_65,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ) ),
inference(rw,[status(thm)],[c_0_45,c_0_32]) ).
thf(c_0_66,plain,
! [X2471: mono_2Etyop_2Enum_2Enum,X2472: mono_2Etyop_2Enum_2Enum,X2473: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2E_2D @ mono_2Ec_2Enum_2E0 @ X2471 )
= mono_2Ec_2Enum_2E0 )
& ( ~ ( mono_2Ec_2Eprim__rec_2E_3C @ X2472 @ X2473 )
| ( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X2472 ) @ X2473 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X2472 @ X2473 ) ) ) ) )
& ( ( mono_2Ec_2Eprim__rec_2E_3C @ X2472 @ X2473 )
| ( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X2472 ) @ X2473 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $false @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X2472 @ X2473 ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_46])])]) ).
thf(c_0_67,plain,
! [X2934: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ X2934 @ X2934 )
= mono_2Ec_2Enum_2E0 ),
inference(variable_rename,[status(thm)],[thm_2Earithmetic_2ESUB__EQUAL__0]) ).
thf(c_0_68,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X278 )
= ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
thf(c_0_69,plain,
! [X2998: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Eprim__rec_2E_3C @ X2998 @ X2998 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_48])]) ).
thf(c_0_70,negated_conjecture,
( ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 ) ),
inference(rw,[status(thm)],[c_0_49,c_0_32]) ).
thf(c_0_71,plain,
! [X274: mono_2Etyop_2Enum_2Enum > $o,X278: mono_2Etyop_2Enum_2Enum] :
( ( X274 @ mono_2Ec_2Enum_2E0 )
| ~ ( X274 @ ( mono_2Ec_2Earithmetic_2E_2D @ X278 @ ( mono_2Ec_2Enum_2ESUC @ X278 ) ) ) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
thf(c_0_72,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( X278 = mono_2Ec_2Enum_2E0 )
| ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) @ X278 ) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_54]) ).
thf(c_0_73,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Earithmetic_2E_3C_3D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X278 ),
inference(er,[status(thm)],[c_0_55]) ).
thf(c_0_74,plain,
! [X2827: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ X2827 @ ( mono_2Ec_2Enum_2ESUC @ X2827 ) ),
inference(variable_rename,[status(thm)],[thm_2Eprim__rec_2ELESS__SUC__REFL]) ).
thf(c_0_75,plain,
! [X278: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EEVEN @ ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
thf(c_0_76,plain,
( ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 )
= ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_57,c_0_27]),c_0_33]),c_0_27]),c_0_40]),c_0_33]) ).
thf(c_0_77,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum,X296: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2E_2A @ X296 @ X278 )
= X294 )
| ( X278
!= ( mono_2Ec_2Earithmetic_2EDIV @ X294 @ X296 ) )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X294 @ X296 )
!= mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X296 ) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
thf(c_0_78,plain,
! [X2841: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ X2841 @ ( mono_2Ec_2Enum_2ESUC @ X2841 ) )
& ( mono_2Ec_2Eprim__rec_2E_3C @ X2841 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ X2841 ) ) ) ),
inference(variable_rename,[status(thm)],[thm_2Eprim__rec_2ELESS__SUC__SUC]) ).
thf(c_0_79,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( X278 = mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2E_2A @ X294 @ X278 ) @ X294 ) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
thf(c_0_80,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) @ X278 )
= X278 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_60,c_0_27]),c_0_40]),c_0_33]) ).
thf(c_0_81,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( X278 = X294 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ X294 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ ( mono_2Ec_2Enum_2ESUC @ X294 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
thf(c_0_82,plain,
! [X294: mono_2Etyop_2Enum_2Enum,X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2EMOD @ X294 @ X278 ) @ X278 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
thf(c_0_83,plain,
! [X278: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
thf(c_0_84,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X296: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ X294 )
= mono_2Ec_2Enum_2E0 )
| ( ( mono_2Ec_2Earithmetic_2E_2A @ X294 @ X296 )
!= X278 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X294 ) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
thf(c_0_85,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( X278
= ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Earithmetic_2EZERO ) ) @ ( esk12_1 @ X278 ) ) )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
thf(c_0_86,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ) ),
inference(rw,[status(thm)],[c_0_65,c_0_33]) ).
thf(c_0_87,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ X294 )
| ( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X294 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X278 @ X294 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
thf(c_0_88,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ X278 @ X278 )
= mono_2Ec_2Enum_2E0 ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
thf(c_0_89,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X278 )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68,c_0_27]),c_0_40]),c_0_33]) ).
thf(c_0_90,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ X278 ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
thf(c_0_91,negated_conjecture,
( ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Earithmetic_2EBIT2 @ mono_2Ec_2Enum_2E0 ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 ) ),
inference(rw,[status(thm)],[c_0_70,c_0_33]) ).
thf(c_0_92,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2E_2D @ ( mono_2Ec_2Enum_2ESUC @ X278 ) @ X294 )
= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Earithmetic_2E_2D @ X278 @ X294 ) ) ) )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ X294 ) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
thf(c_0_93,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2D @ X278 @ ( mono_2Ec_2Enum_2ESUC @ X278 ) )
= mono_2Ec_2Enum_2E0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_72]),c_0_73]) ).
thf(c_0_94,plain,
! [X278: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ ( mono_2Ec_2Enum_2ESUC @ X278 ) ),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
thf(c_0_95,plain,
! [X278: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EEVEN @ ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) @ X278 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_75,c_0_27]),c_0_76]),c_0_33]) ).
thf(c_0_96,plain,
! [X294: mono_2Etyop_2Enum_2Enum,X278: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2E_2A @ X278 @ ( mono_2Ec_2Earithmetic_2EDIV @ X294 @ X278 ) )
= X294 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X294 @ X278 )
!= mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X278 ) ),
inference(er,[status(thm)],[c_0_77]) ).
thf(c_0_97,plain,
! [X278: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ X278 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
thf(c_0_98,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( X278 = mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ X278 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ),
inference(spm,[status(thm)],[c_0_79,c_0_80]) ).
thf(c_0_99,plain,
! [X278: mono_2Etyop_2Enum_2Enum,X294: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ ( mono_2Ec_2Enum_2ESUC @ X294 ) )
= X294 )
| ( mono_2Ec_2Eprim__rec_2E_3C @ ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ ( mono_2Ec_2Enum_2ESUC @ X294 ) ) @ X294 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_82]),c_0_83])]) ).
thf(c_0_100,plain,
! [X294: mono_2Etyop_2Enum_2Enum,X278: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2EMOD @ ( mono_2Ec_2Earithmetic_2E_2A @ X278 @ X294 ) @ X278 )
= mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Eprim__rec_2E_3C @ mono_2Ec_2Enum_2E0 @ X278 ) ),
inference(er,[status(thm)],[c_0_84]) ).
thf(c_0_101,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2E_2A @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) @ ( esk12_1 @ X278 ) )
= X278 )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ X278 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_85,c_0_27]),c_0_76]),c_0_33]) ).
thf(c_0_102,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ) ),
inference(rw,[status(thm)],[c_0_86,c_0_76]) ).
thf(c_0_103,plain,
( ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ ~ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_88]),c_0_89]),c_0_90]) ).
thf(c_0_104,negated_conjecture,
( ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 ) ),
inference(rw,[status(thm)],[c_0_91,c_0_76]) ).
thf(c_0_105,plain,
( ( mono_2Ec_2Ebool_2ECOND_2Emono_2Etyop_2Enum_2Enum @ $true @ mono_2Ec_2Enum_2E0 @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) )
= mono_2Ec_2Enum_2E0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_93]),c_0_88]),c_0_94])]) ).
thf(c_0_106,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2EEVEN @ X278 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
!= mono_2Ec_2Enum_2E0 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95,c_0_96]),c_0_97])]) ).
thf(c_0_107,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
= mono_2Ec_2Enum_2E0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ),
inference(spm,[status(thm)],[c_0_98,c_0_99]) ).
thf(c_0_108,plain,
! [X278: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Earithmetic_2EMOD @ X278 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
= mono_2Ec_2Enum_2E0 )
| ~ ( mono_2Ec_2Earithmetic_2EEVEN @ X278 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100,c_0_101]),c_0_97])]) ).
thf(c_0_109,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EEVEN @ esk1_0 )
| ( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
!= ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) ),
inference(rw,[status(thm)],[c_0_102,c_0_103]) ).
thf(c_0_110,negated_conjecture,
( ( mono_2Ec_2Earithmetic_2EMOD @ esk1_0 @ ( mono_2Ec_2Enum_2ESUC @ ( mono_2Ec_2Enum_2ESUC @ mono_2Ec_2Enum_2E0 ) ) )
!= mono_2Ec_2Enum_2E0 ),
inference(csr,[status(thm)],[inference(rw,[status(thm)],[c_0_104,c_0_105]),c_0_106]) ).
thf(c_0_111,plain,
$false,
inference(cdclpropres,[status(thm)],[c_0_107,c_0_108,c_0_109,c_0_110]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP003^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.17 % Computer : n010.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Tue Sep 29 19:20:33 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.74/0.82 Running: /export/starexec/sandbox/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/sandbox/tmp/tmp.uaIl0AtBTX/E---3.1_3287459.p
% 35.22/6.14 % Version: 3.5.1-ho
% 35.22/6.14 % Preprocessing class: HMLMSLSLSSSCHFA.
% 35.22/6.14 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 35.22/6.14 % Starting new_ho_2 with 1200s (4) cores
% 35.22/6.14 % Starting sh3l with 600s (2) cores
% 35.22/6.14 % Starting lpo5_rw_fix with 300s (1) cores
% 35.22/6.14 % Starting full_lambda_7 with 300s (1) cores
% 35.22/6.14 % sh3l with pid 3287473 completed with status 0
% 35.22/6.14 % Result found by sh3l
% 35.22/6.14 % Preprocessing class: HMLMSLSLSSSCHFA.
% 35.22/6.14 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 35.22/6.14 % Starting new_ho_2 with 1200s (4) cores
% 35.22/6.14 % Starting sh3l with 600s (2) cores
% 35.22/6.14 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 35.22/6.14 % SinE strategy is gf120_gu_RUU_F100_L01000
% 35.22/6.14 % Search class: HGHSM-FSLM32-DHFFFFBC
% 35.22/6.14 % partial match(1): HGHSM-FSLM32-DHFFFFBN
% 35.22/6.14 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 35.22/6.14 % Starting SubtermCWHack with 55s (1) cores
% 35.22/6.14 % Starting sh3l with 61s (1) cores
% 35.22/6.14 % sh3l with pid 3287478 completed with status 0
% 35.22/6.14 % Result found by sh3l
% 35.22/6.14 % Preprocessing class: HMLMSLSLSSSCHFA.
% 35.22/6.14 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 35.22/6.14 % Starting new_ho_2 with 1200s (4) cores
% 35.22/6.14 % Starting sh3l with 600s (2) cores
% 35.22/6.14 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 35.22/6.14 % SinE strategy is gf120_gu_RUU_F100_L01000
% 35.22/6.14 % Search class: HGHSM-FSLM32-DHFFFFBC
% 35.22/6.14 % partial match(1): HGHSM-FSLM32-DHFFFFBN
% 35.22/6.14 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 35.22/6.14 % Starting SubtermCWHack with 55s (1) cores
% 35.22/6.14 % Starting sh3l with 61s (1) cores
% 35.22/6.14 % Preprocessing time : 0.024 s
% 35.22/6.14 % Presaturation interreduction done
% 35.22/6.14 % SatCheck found unsatisfiable ground set
% 35.22/6.14
% 35.22/6.14 % Proof found!
% 35.22/6.14 % SZS status Theorem
% 35.22/6.14 % SZS output start CNFRefutation
% See solution above
% 35.22/6.15 % Parsed axioms : 3527
% 35.22/6.15 % Removed by relevancy pruning/SinE : 3045
% 35.22/6.15 % Initial clauses : 1073
% 35.22/6.15 % Removed in clause preprocessing : 180
% 35.22/6.15 % Initial clauses in saturation : 893
% 35.22/6.15 % Processed clauses : 21728
% 35.22/6.15 % ...of these trivial : 525
% 35.22/6.15 % ...subsumed : 16203
% 35.22/6.15 % ...remaining for further processing : 5000
% 35.22/6.15 % Other redundant clauses eliminated : 4334
% 35.22/6.15 % Clauses deleted for lack of memory : 0
% 35.22/6.15 % Backward-subsumed : 287
% 35.22/6.15 % Backward-rewritten : 313
% 35.22/6.15 % Generated clauses : 261376
% 35.22/6.15 % ...of the previous two non-redundant : 233116
% 35.22/6.15 % ...aggressively subsumed : 0
% 35.22/6.15 % Contextual simplify-reflections : 46
% 35.22/6.15 % Paramodulations : 256766
% 35.22/6.15 % Factorizations : 24
% 35.22/6.15 % NegExts : 0
% 35.22/6.15 % Equation resolutions : 4372
% 35.22/6.15 % Disequality decompositions : 0
% 35.22/6.15 % Total rewrite steps : 91967
% 35.22/6.15 % ...of those cached : 81842
% 35.22/6.15 % Propositional unsat checks : 1
% 35.22/6.15 % Propositional check models : 0
% 35.22/6.15 % Propositional check unsatisfiable : 1
% 35.22/6.15 % Propositional clauses : 215136
% 35.22/6.15 % Propositional clauses after purity: 64175
% 35.22/6.15 % Propositional unsat core size : 4
% 35.22/6.15 % Propositional preprocessing time : 0.000
% 35.22/6.15 % Propositional encoding time : 0.412
% 35.22/6.15 % Propositional solver time : 0.040
% 35.22/6.15 % Success case prop preproc time : 0.000
% 35.22/6.15 % Success case prop encoding time : 0.412
% 35.22/6.15 % Success case prop solver time : 0.040
% 35.22/6.15 % Current number of processed clauses : 3752
% 35.22/6.15 % Positive orientable unit clauses : 438
% 35.22/6.15 % Positive unorientable unit clauses: 17
% 35.22/6.15 % Negative unit clauses : 1512
% 35.22/6.15 % Non-unit-clauses : 1785
% 35.22/6.15 % Current number of unprocessed clauses: 211384
% 35.22/6.15 % ...number of literals in the above : 470132
% 35.22/6.15 % Current number of archived formulas : 0
% 35.22/6.15 % Current number of archived clauses : 1170
% 35.22/6.15 % Clause-clause subsumption calls (NU) : 909599
% 35.22/6.15 % Rec. Clause-clause subsumption calls : 620376
% 35.22/6.15 % Non-unit clause-clause subsumptions : 3831
% 35.22/6.15 % Unit Clause-clause subsumption calls : 779254
% 35.22/6.15 % Rewrite failures with RHS unbound : 0
% 35.22/6.15 % BW rewrite match attempts : 3967
% 35.22/6.15 % BW rewrite match successes : 1418
% 35.22/6.15 % Condensation attempts : 0
% 35.22/6.15 % Condensation successes : 0
% 35.22/6.15 % Termbank termtop insertions : 10510203
% 35.22/6.15 % Search garbage collected termcells : 38172
% 35.22/6.15
% 35.22/6.15 % -------------------------------------------------
% 35.22/6.15 % User time : 4.835 s
% 35.22/6.15 % System time : 0.206 s
% 35.22/6.15 % Total time : 5.041 s
% 35.22/6.15 % Maximum resident set size: 11268 pages
% 35.22/6.15
% 35.22/6.15 % -------------------------------------------------
% 35.22/6.15 % User time : 9.833 s
% 35.22/6.15 % System time : 0.356 s
% 35.22/6.15 % Total time : 10.189 s
% 35.22/6.15 % Maximum resident set size: 9728 pages
% 35.22/6.15 % E exiting
%------------------------------------------------------------------------------